54 const std::set<irep_idt> &predicates)
59 instruction.is_function_call() &&
60 instruction.call_function().id() == ID_symbol)
62 const auto &callee_id =
67 predicates.find(callee_id) != predicates.end())
77 std::set<irep_idt> &discovered_function_pointer_contracts)
79 std::set<irep_idt> candidates;
80 for(
const auto &pair :
goto_model.symbol_table)
83 pair.second.type.id() == ID_code &&
87 goto_model.goto_functions.function_map.find(pair.first);
89 iter !=
goto_model.goto_functions.function_map.end() &&
90 iter->second.body_available())
92 candidates.insert(pair.first);
97 std::set<irep_idt> predicates;
100 bool new_predicates_found =
true;
101 while(new_predicates_found)
103 new_predicates_found =
false;
104 for(
const auto &function_id : candidates)
107 predicates.find(function_id) == predicates.end() &&
109 goto_model.goto_functions.function_map[function_id].body, predicates))
111 predicates.insert(function_id);
112 new_predicates_found =
true;
117 if(predicates.empty())
121 struct dep_graph_nodet :
public graph_nodet<empty_edget>
124 explicit dep_graph_nodet(
const irep_idt &function_id)
125 : function_id(function_id)
133 std::map<irep_idt, std::size_t> id_to_node_map;
135 for(
auto &predicate : predicates)
137 id_to_node_map.insert({predicate, dep_graph.
add_node(predicate)});
141 for(
auto &caller : predicates)
143 const auto caller_id = id_to_node_map[caller];
144 for(
const auto &instruction :
145 goto_model.goto_functions.function_map[caller].body.instructions)
148 instruction.is_function_call() &&
149 instruction.call_function().id() == ID_symbol)
153 if(predicates.find(callee) != predicates.end())
156 mstream <<
"Memory predicate dependency " << caller <<
" -> "
157 << callee << messaget::eom;
159 const auto callee_id = id_to_node_map[callee];
161 dep_graph.
add_edge(callee_id, caller_id);
168 auto sorted = dep_graph.
topsort();
171 "could not determine instrumentation order for memory predicates, most "
172 "likely due to mutual recursion");
173 for(
const auto &idx : sorted)
176 dep_graph[idx].function_id, discovered_function_pointer_contracts);
185 const std::map<irep_idt, std::size_t> ¶meter_rank)
187 if(expr.
id() == ID_typecast)
192 else if(expr.
id() == ID_symbol)
195 const auto found = parameter_rank.find(ident);
196 if(found != parameter_rank.end())
198 return {found->second};
215 const symbolt &function_symbol =
218 std::map<irep_idt, std::size_t> parameter_rank;
220 for(std::size_t rank = 0; rank < parameters.size(); rank++)
222 parameter_rank[parameters[rank].get_identifier()] = rank;
225 goto_model.goto_functions.function_map[function_id].body;
230 if(it.is_function_call() && it.call_function().id() == ID_symbol)
236 auto opt_rank =
is_param_expr(it.call_arguments()[0], parameter_rank);
237 if(opt_rank.has_value())
244 auto opt_rank =
is_param_expr(it.call_arguments()[1], parameter_rank);
245 if(opt_rank.has_value())
252 auto opt_rank =
is_param_expr(it.call_arguments()[0], parameter_rank);
253 if(opt_rank.has_value())
265 is_param_expr(it.call_arguments()[callee_rank], parameter_rank);
266 if(opt_rank.has_value())
278 const std::size_t parameter_rank,
285 auto ¶meter_id = parameters[parameter_rank].get_identifier();
286 auto entry =
goto_model.symbol_table.symbols.find(parameter_id);
288 mstream <<
"adding pointer type to " << function_id <<
" " << parameter_id
291 const symbolt &old_symbol = entry->second;
292 const auto &old_symbol_expr = old_symbol.
symbol_expr();
306 std::pair<symbolt &, bool> res =
307 goto_model.symbol_table.insert(std::move(new_symbol));
309 replace_lifted_param.
insert(
314 parameters[parameter_rank] = parameter;
319 std::set<irep_idt> &discovered_function_pointer_contracts)
327 auto &body =
goto_model.goto_functions.function_map[function_id].body;
329 for(
auto &instruction : body.instructions)
332 instruction.transform([&replace_lifted_params](
exprt expr) {
333 const bool changed = !replace_lifted_params.
replace(expr);
334 return changed ? std::optional<exprt>{expr} : std::nullopt;
340 instruction.is_function_call() &&
341 instruction.call_function().id() == ID_symbol)
350 const auto arg = instruction.call_arguments()[rank];
352 mstream <<
"Adding address_of to call " << callee_id
353 <<
", argument " << format(arg) << messaget::eom;
364 std::set<irep_idt> &discovered_function_pointer_contracts)
369 log.status() <<
"Instrumenting memory predicate '" << function_id <<
"'"
377 function_id, discovered_function_pointer_contracts);
380 mstream <<
"Ranks of lifted parameters for " << function_id <<
": ";
381 for(const auto rank : lifted_parameters[function_id])
382 mstream << rank <<
", ";
383 mstream << messaget::eom;
391 discovered_function_pointer_contracts);
404 for(
auto target = first_instruction; target != last_instruction; target++)
406 if(target->is_function_call())
408 const auto &function = target->call_function();
410 if(function.id() == ID_symbol)
419 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.