44 : goto_model(goto_model),
45 message_handler(message_handler),
48 instrument(instrument),
49 spec_functions(spec_functions),
50 contract_handler(contract_handler),
51 ns(goto_model.symbol_table)
58 std::pair<irep_idt, std::pair<dfcc_contract_modet, dfcc_loop_contract_modet>>>
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_mode}}});
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_mode != loop_contract_mode)
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 "
92 err_msg <<
"- with '" << contract_id <<
"' in "
102 switch(contract_mode)
110 function_pointer_contracts,
111 allow_recursive_calls);
126 dest.insert(it.first);
158 std::set<irep_idt> &function_pointer_contracts,
159 bool allow_recursive_calls)
162 const irep_idt &wrapper_id = function_id;
164 id2string(wrapper_id) +
"_wrapped_for_contract_checking";
170 const auto &wrapper_symbol =
177 "__contract_check_in_progress",
178 wrapper_symbol.location,
180 wrapper_symbol.module,
188 "__contract_checked_once",
189 wrapper_symbol.location,
191 wrapper_symbol.module,
196 check_started, wrapper_symbol.location));
208 "Only a single top-level call to function " +
id2string(function_id) +
209 " when checking contract " +
id2string(contract_id));
212 check_started,
true_exprt(), wrapper_symbol.location));
217 "__write_set_to_check",
227 function_pointer_contracts);
230 check_completed,
true_exprt(), wrapper_symbol.location));
232 check_started,
false_exprt(), wrapper_symbol.location));
235 auto goto_end_function =
239 auto contract_replacement_label =
241 check_started_goto->complete_goto(contract_replacement_label);
243 if(allow_recursive_calls)
252 function_pointer_contracts);
260 "No recursive call to function " +
id2string(function_id) +
261 " when checking contract " +
id2string(contract_id));
267 auto end_function_label =
269 goto_end_function->complete_goto(end_function_label);
281 wrapped_id, wrapper_id, loop_contract_mode, function_pointer_contracts);
289 std::set<irep_idt> &function_pointer_contracts)
291 const irep_idt &wrapper_id = function_id;
293 id2string(function_id) +
"_wrapped_for_replacement_with_contract";
299 "__write_set_to_check",
311 function_pointer_contracts);
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...
void add_contract_instructions(const dfcc_contract_modet contract_mode, const irep_idt &wrapper_id, const irep_idt &wrapped_id, const irep_idt &contract_id, const symbolt &wrapper_write_set_symbol, goto_programt &dest, std::set< irep_idt > &function_pointer_contracts)
Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the f...
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
void instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and inserting frame condition chec...
Class interface to library types and functions defined in cprover_contracts.c.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
This class rewrites GOTO functions that use the built-ins:
void swap_and_wrap(const dfcc_contract_modet contract_mode, const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
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.
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...
static std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, dfcc_loop_contract_modet > > > cache
remember all functions that were swapped/wrapped and in which mode
void check_contract(const dfcc_loop_contract_modet loop_contract_mode, 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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
The Boolean constant false.
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.
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)
source_locationt location
Source code location of definition of symbol.
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
std::string dfcc_loop_contract_mode_to_string(const dfcc_loop_contract_modet mode)
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
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.