30 : goto_model(goto_model),
32 instrument(instrument),
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;
83 pair.second.type.id() == ID_code &&
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() &&
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 :
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;
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();
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 =
309 replace_lifted_param.
insert(
314 parameters[parameter_rank] = parameter;
319 std::set<irep_idt> &discovered_function_pointer_contracts)
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 ...
void instrument_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
bool do_not_instrument(const irep_idt &id) const
True iff the symbol must not be instrumented because it is an internal symbol or a CPROVER symbol.
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
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
mstreamt & status() const
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
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
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
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 std::optional< std::size_t > is_param_expr(const exprt &expr, const std::map< irep_idt, std::size_t > ¶meter_rank)
static bool is_core_memory_predicate(const irep_idt &function_id)
True iff function_id is a core memory predicate.
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_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.