59 const std::set<irep_idt> &predicates)
64 instruction.is_function_call() &&
65 instruction.call_function().id() == ID_symbol)
67 const auto &callee_id =
72 predicates.find(callee_id) != predicates.end())
82 std::set<irep_idt> &discovered_function_pointer_contracts)
84 std::set<irep_idt> candidates;
85 for(
const auto &pair :
goto_model.symbol_table)
88 pair.second.type.id() == ID_code &&
92 goto_model.goto_functions.function_map.find(pair.first);
94 iter !=
goto_model.goto_functions.function_map.end() &&
95 iter->second.body_available())
97 candidates.insert(pair.first);
102 std::set<irep_idt> predicates;
105 bool new_predicates_found =
true;
106 while(new_predicates_found)
108 new_predicates_found =
false;
109 for(
const auto &function_id : candidates)
112 predicates.find(function_id) == predicates.end() &&
114 goto_model.goto_functions.function_map[function_id].body, predicates))
116 predicates.insert(function_id);
117 new_predicates_found =
true;
122 if(predicates.empty())
126 struct dep_graph_nodet :
public graph_nodet<empty_edget>
129 explicit dep_graph_nodet(
const irep_idt &function_id)
130 : function_id(function_id)
138 std::map<irep_idt, std::size_t> id_to_node_map;
140 for(
auto &predicate : predicates)
142 id_to_node_map.insert({predicate, dep_graph.
add_node(predicate)});
146 for(
auto &caller : predicates)
148 const auto caller_id = id_to_node_map[caller];
149 for(
const auto &instruction :
150 goto_model.goto_functions.function_map[caller].body.instructions)
153 instruction.is_function_call() &&
154 instruction.call_function().id() == ID_symbol)
158 if(predicates.find(callee) != predicates.end())
161 mstream <<
"Memory predicate dependency " << caller <<
" -> "
162 << callee << messaget::eom;
164 const auto callee_id = id_to_node_map[callee];
166 dep_graph.
add_edge(callee_id, caller_id);
173 auto sorted = dep_graph.
topsort();
176 "could not determine instrumentation order for memory predicates, most "
177 "likely due to mutual recursion");
178 for(
const auto &idx : sorted)
181 dep_graph[idx].function_id, discovered_function_pointer_contracts);
190 const std::map<irep_idt, std::size_t> ¶meter_rank)
192 if(expr.
id() == ID_typecast)
197 else if(expr.
id() == ID_symbol)
200 const auto found = parameter_rank.find(ident);
201 if(found != parameter_rank.end())
203 return {found->second};
220 const symbolt &function_symbol =
223 std::map<irep_idt, std::size_t> parameter_rank;
225 for(std::size_t rank = 0; rank < parameters.size(); rank++)
227 parameter_rank[parameters[rank].get_identifier()] = rank;
230 goto_model.goto_functions.function_map[function_id].body;
235 if(it.is_function_call() && it.call_function().id() == ID_symbol)
241 auto opt_rank =
is_param_expr(it.call_arguments()[0], parameter_rank);
242 if(opt_rank.has_value())
249 auto opt_rank =
is_param_expr(it.call_arguments()[0], parameter_rank);
250 if(opt_rank.has_value())
257 auto opt_rank =
is_param_expr(it.call_arguments()[1], parameter_rank);
258 if(opt_rank.has_value())
265 auto opt_rank =
is_param_expr(it.call_arguments()[0], parameter_rank);
266 if(opt_rank.has_value())
278 is_param_expr(it.call_arguments()[callee_rank], parameter_rank);
279 if(opt_rank.has_value())
291 const std::size_t parameter_rank,
298 auto ¶meter_id = parameters[parameter_rank].get_identifier();
299 auto entry =
goto_model.symbol_table.symbols.find(parameter_id);
301 mstream <<
"adding pointer type to " << function_id <<
" " << parameter_id
304 const symbolt &old_symbol = entry->second;
305 const auto &old_symbol_expr = old_symbol.
symbol_expr();
319 std::pair<symbolt &, bool> res =
320 goto_model.symbol_table.insert(std::move(new_symbol));
322 replace_lifted_param.
insert(
327 parameters[parameter_rank] = parameter;
332 std::set<irep_idt> &discovered_function_pointer_contracts)
340 auto &body =
goto_model.goto_functions.function_map[function_id].body;
342 for(
auto &instruction : body.instructions)
345 instruction.transform([&replace_lifted_params](
exprt expr) {
346 const bool changed = !replace_lifted_params.
replace(expr);
347 return changed ? std::optional<exprt>{expr} : std::nullopt;
353 instruction.is_function_call() &&
354 instruction.call_function().id() == ID_symbol)
363 const auto arg = instruction.call_arguments()[rank];
365 mstream <<
"Adding address_of to call " << callee_id
366 <<
", argument " << format(arg) << messaget::eom;
377 std::set<irep_idt> &discovered_function_pointer_contracts)
382 log.status() <<
"Instrumenting memory predicate '" << function_id <<
"'"
390 function_id, discovered_function_pointer_contracts);
393 mstream <<
"Ranks of lifted parameters for " << function_id <<
": ";
394 for(const auto rank : lifted_parameters[function_id])
395 mstream << rank <<
", ";
396 mstream << messaget::eom;
404 discovered_function_pointer_contracts);
417 for(
auto target = first_instruction; target != last_instruction; target++)
419 if(target->is_function_call())
421 const auto &function = target->call_function();
423 if(function.id() == ID_symbol)
432 target->call_arguments()[rank] =
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
void set_base_name(const irep_idt &name)
void set_identifier(const irep_idt &identifier)
const parameterst & parameters() const
Operator to dereference a pointer.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
dfcc_instrumentt & instrument
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
void collect_parameters_to_lift(const irep_idt &function_id)
Computes the subset of function parameters of function_id that are passed directly to core predicates...
void lift_predicate(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
void add_pointer_type(const irep_idt &function_id, const std::size_t parameter_rank, replace_symbolt &replace_lifted_param)
adds a pointer_type to the parameter of a function
dfcc_lift_memory_predicatest(goto_modelt &goto_model, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler)
std::map< irep_idt, std::set< std::size_t > > lifted_parameters
void lift_parameters_and_update_body(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
bool calls_memory_predicates(const goto_programt &goto_program, const std::set< irep_idt > &predicates)
Returns true iff goto_program calls core memory predicates.
bool is_lifted_function(const irep_idt &function_id)
True if a function at least had one of its parameters lifted.
std::set< irep_idt > lift_predicates(std::set< irep_idt > &discovered_function_pointer_contracts)
Collects and lifts all user-defined memory predicates.
Base class for all expressions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
This class represents a node in a directed graph.
A generic directed graph with a parametric node type.
node_indext add_node(arguments &&... values)
void add_edge(node_indext a, node_indext b)
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
const irep_idt & id() const
Replace a symbol expression by a given expression.
virtual bool replace(exprt &dest) const
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
const irep_idt & get_identifier() const
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
static bool is_core_memory_predicate(const irep_idt &function_id)
True iff function_id is a core memory predicate.
static std::optional< std::size_t > is_param_expr(const exprt &expr, const std::map< irep_idt, std::size_t > ¶meter_rank)
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Dynamic frame condition checking utility functions.
A Template Class for Graphs.
API to expression classes for Pointers.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define CHECK_RETURN(CONDITION)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Loop contract configurations.