58 std::pair<irep_idt, std::pair<dfcc_contract_modet, loop_contract_configt>>>
66 std::set<irep_idt> &function_pointer_contracts,
67 bool allow_recursive_calls)
69 auto pair =
cache.insert(
70 {function_id, {contract_id, {contract_mode, loop_contract_config}}});
71 auto inserted = pair.second;
75 irep_idt old_contract_id = pair.first->second.first;
78 pair.first->second.second.second;
82 old_contract_id != contract_id || old_contract_mode != contract_mode ||
83 old_loop_contract_config != loop_contract_config)
85 std::ostringstream err_msg;
86 err_msg <<
"DFCC: multiple attempts to swap and wrap function '"
87 << function_id <<
"':\n";
88 err_msg <<
"- with '" << old_contract_id <<
"' in "
90 << old_loop_contract_config.
to_string() <<
"\n";
91 err_msg <<
"- with '" << contract_id <<
"' in "
93 << loop_contract_config.
to_string() <<
"\n";
101 switch(contract_mode)
106 loop_contract_config,
109 function_pointer_contracts,
110 allow_recursive_calls);
125 dest.insert(it.first);
157 std::set<irep_idt> &function_pointer_contracts,
158 bool allow_recursive_calls)
161 const irep_idt &wrapper_id = function_id;
163 id2string(wrapper_id) +
"_wrapped_for_contract_checking";
169 const auto &wrapper_symbol =
176 "__contract_check_in_progress",
177 wrapper_symbol.location,
179 wrapper_symbol.module,
187 "__contract_checked_once",
188 wrapper_symbol.location,
190 wrapper_symbol.module,
195 check_started, wrapper_symbol.location));
207 "Only a single top-level call to function " +
id2string(function_id) +
208 " when checking contract " +
id2string(contract_id));
211 check_started,
true_exprt(), wrapper_symbol.location));
216 "__write_set_to_check",
226 function_pointer_contracts);
229 check_completed,
true_exprt(), wrapper_symbol.location));
231 check_started,
false_exprt(), wrapper_symbol.location));
234 auto goto_end_function =
238 auto contract_replacement_label =
240 check_started_goto->complete_goto(contract_replacement_label);
242 if(allow_recursive_calls)
251 function_pointer_contracts);
259 "No recursive call to function " +
id2string(function_id) +
260 " when checking contract " +
id2string(contract_id));
266 auto end_function_label =
268 goto_end_function->complete_goto(end_function_label);
271 goto_model.goto_functions.function_map.at(function_id).body.swap(body);
276 goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
280 wrapped_id, wrapper_id, loop_contract_config, function_pointer_contracts);
288 std::set<irep_idt> &function_pointer_contracts)
290 const irep_idt &wrapper_id = function_id;
292 id2string(function_id) +
"_wrapped_for_replacement_with_contract";
298 "__write_set_to_check",
310 function_pointer_contracts);
316 goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
319 goto_model.goto_functions.function_map.at(function_id).body.swap(body);
API to expression classes that are internal to the C frontend.
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
A contract is represented by a function declaration or definition with contract clauses attached to i...
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.
This class rewrites GOTO functions that use the built-ins:
void check_contract(const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
Swaps-and-wraps the given function_id in a wrapper function that checks the given contract_id.
message_handlert & message_handler
dfcc_spec_functionst & spec_functions
dfcc_swap_and_wrapt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_spec_functionst &spec_functions, dfcc_contract_handlert &contract_handler)
void get_swapped_functions(std::set< irep_idt > &dest) const
Adds the set of swapped functions to dest.
static std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, loop_contract_configt > > > cache
remember all functions that were swapped/wrapped and in which mode
dfcc_instrumentt & instrument
dfcc_contract_handlert & contract_handler
void replace_with_contract(const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts)
Swaps-and-wraps the given function_id in a wrapper function that models the abstract behaviour of con...
void swap_and_wrap(const dfcc_contract_modet contract_mode, const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
The Boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
void set_function(const irep_idt &function)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The Boolean constant true.
std::string dfcc_contract_mode_to_string(const dfcc_contract_modet mode)
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
@ CAR_SET_PTR
type of pointers to sets of CAR
Given a function_id and contract_id, swaps its body to a function with a fresh mangled name,...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
Goto Programs with Functions.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
API to expression classes for Pointers.
Various predicates over pointers in programs.
API to expression classes.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static const symbolt & create_new_parameter_symbol(symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
Creates a new parameter symbol for the given function_id.
static void wrap_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
Given a function to wrap foo and a new name wrapped_foo
static const symbolt & create_static_symbol(symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol ...
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
Loop contract configurations.
std::string to_string() const