54 : goto_model(goto_model),
55 message_handler(message_handler),
58 spec_functions(spec_functions),
59 contract_clauses_codegen(contract_clauses_codegen),
65 contract_clauses_codegen),
66 ns(goto_model.symbol_table)
102 std::set<irep_idt> &dest)
const
241 std::set<irep_idt> &function_pointer_contracts)
251 "Function '" +
id2string(function_id) +
"' must exist in the model.");
257 const auto &function_symbol =
263 "__write_set_to_check",
264 function_symbol.location);
275 loop_contract_config,
276 function_pointer_contracts);
278 auto &body = goto_function.
body;
298 std::set<symbol_exprt>
301 std::set<symbol_exprt> local_statics;
304 const auto &sym = sym_pair.second;
305 if(sym.is_static_lifetime)
307 const auto &loc = sym.location;
308 if(!loc.get_function().empty() && loc.get_function() == function_id)
310 local_statics.insert(sym.symbol_expr());
314 return local_statics;
320 std::set<irep_idt> &function_pointer_contracts)
330 "Function '" +
id2string(function_id) +
"' must exist in the model.");
335 "__write_set_to_check",
348 loop_contract_config,
349 function_pointer_contracts);
353 const irep_idt &wrapped_function_id,
354 const irep_idt &initial_function_id,
356 std::set<irep_idt> &function_pointer_contracts)
367 "Function '" +
id2string(wrapped_function_id) +
368 "' must exist in the model.");
373 "__write_set_to_check",
386 loop_contract_config,
387 function_pointer_contracts);
393 const exprt &write_set,
394 std::set<irep_idt> &function_pointer_contracts)
416 body.instructions.
begin(),
417 body.instructions.end(),
419 function_pointer_contracts);
422 goto_program.
clear();
431 const exprt &write_set,
432 const std::set<symbol_exprt> &local_statics,
434 std::set<irep_idt> &function_pointer_contracts)
439 std::string options =
"assert-false-assume-false";
448 auto &body = goto_function.
body;
456 loop_contract_config,
465 body.instructions.
begin(),
466 body.instructions.end(),
468 function_pointer_contracts);
479 loop_contract_config,
481 function_pointer_contracts);
485 auto begin = body.instructions.begin();
486 auto end = std::prev(body.instructions.end());
489 for(
const auto &local_static : local_statics)
503 for(
const auto ¶m : code_type.
parameters())
505 const irep_idt ¶m_id = param.get_identifier();
506 if(top_level_tracked.find(param_id) != top_level_tracked.end())
526 std::set<irep_idt> &function_pointer_contracts)
531 goto_program, first_instruction, last_instruction, cfg_info);
536 goto_program, first_instruction, last_instruction, cfg_info);
541 goto_program, first_instruction, last_instruction, cfg_info);
550 function_pointer_contracts);
553 auto &target = first_instruction;
556 while(target != last_instruction)
558 if(target->is_decl())
562 if(target->is_dead())
566 else if(target->is_assign())
570 else if(target->is_function_call())
574 else if(target->is_other())
585 const exprt &write_set,
591 const auto &target_location = target->source_location();
600 auto label_instruction =
602 goto_instruction->complete_goto(label_instruction);
621 const auto &decl_symbol = target->decl_symbol();
626 function_id, write_set, decl_symbol, target, goto_program);
632 const exprt &write_set,
638 const auto &target_location = target->source_location();
647 auto label_instruction =
650 goto_instruction->complete_goto(label_instruction);
670 const auto &decl_symbol = target->dead_symbol();
673 function_id, write_set, decl_symbol, target, goto_program);
688 const auto &lhs_source_location = target->source_location();
713 "__check_lhs_assignment",
714 lhs_source_location);
725 lhs_source_location),
726 lhs_source_location));
731 auto label_instruction =
733 goto_instruction->complete_goto(label_instruction);
745 lhs.
id() == ID_symbol &&
752 if_expr.cond().id() == ID_side_effect &&
754 if_expr.false_case() == lhs)
756 return if_expr.true_case();
769 const auto &lhs = target->assign_lhs();
770 const auto &rhs = target->assign_rhs();
771 const auto &target_location = target->source_location();
782 if(dead_ptr.has_value())
802 write_set, dead_ptr.value(), target_location),
805 auto label_instruction =
807 goto_instruction->complete_goto(label_instruction);
816 if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_allocate)
837 auto label_instruction =
839 goto_instruction->complete_goto(label_instruction);
849 const exprt &write_set,
869 const auto &target_location = target->source_location();
870 const auto &callf = target->call_function();
881 target->call_lhs(), target->call_function(), target->call_arguments());
882 call_inst.
arguments().push_back(write_set);
884 auto goto_end_inst = payload.
add(
887 goto_no_inst->complete_goto(no_inst_label);
889 target->call_lhs(), target->call_function(), target->call_arguments());
892 goto_end_inst->complete_goto(end_label);
894 target->turn_into_skip();
899 const exprt &write_set,
903 if(target->is_function_call())
905 if(target->call_function().id() == ID_symbol)
912 target->call_arguments().push_back(write_set);
921 write_set, target, goto_program);
928 const exprt &write_set,
932 INVARIANT(target->is_function_call(),
"target must be a function call");
934 target->call_function().id() == ID_symbol &&
939 auto &target_location = target->source_location();
960 "__check_deallocate",
965 const auto &ptr = target->call_arguments().at(0);
969 check_var, write_set, ptr, target_location),
988 auto label_instruction =
990 goto_instruction->complete_goto(label_instruction);
1002 target->is_function_call(),
1003 "the target must be a function call instruction");
1008 if(target->call_lhs().is_not_nil() && cfg_info.
must_check_lhs(target))
1011 function_id, target, target->call_lhs(), goto_program, cfg_info);
1014 const auto &call_function = target->call_function();
1016 call_function.id() == ID_symbol &&
1035 const auto &target_location = target->source_location();
1036 auto &statement = target->get_other().get_statement();
1041 if(statement == ID_array_set || statement == ID_array_copy)
1043 const bool is_array_set = statement == ID_array_set;
1063 is_array_set ?
"__check_array_set" :
"__check_array_copy",
1068 const auto &dest = target->get_other().operands().at(0);
1072 check_var, write_set, dest, target_location)
1074 check_var, write_set, dest, target_location),
1081 std::string fun_name = is_array_set ?
"array_set" :
"array_copy";
1083 std::string
comment =
"Check that " + fun_name +
"(" +
1085 ", ...) is allowed by the assigns clause";
1091 auto label_instruction =
1093 goto_instruction->complete_goto(label_instruction);
1097 else if(statement == ID_array_replace)
1118 "__check_array_replace",
1123 const auto &dest = target->get_other().operands().at(0);
1124 const auto &src = target->get_other().operands().at(1);
1128 check_var, write_set, dest, src, target_location),
1134 std::string
comment =
"Check that array_replace(" +
1136 ", ...) is allowed by the assigns clause";
1142 auto label_instruction =
1144 goto_instruction->complete_goto(label_instruction);
1148 else if(statement == ID_havoc_object)
1167 "__check_havoc_object",
1172 const auto &ptr = target->get_other().operands().at(0);
1176 check_var, write_set, ptr, target_location),
1182 std::string
comment =
"Check that havoc_object(" +
1184 ") is allowed by the assigns clause";
1190 auto label_instruction =
1192 goto_instruction->complete_goto(label_instruction);
1196 else if(statement == ID_expression)
1221 log.
warning() <<
"dfcc_instrument::instrument_other: statement type '"
1222 << statement <<
"' is not supported, analysis may be unsound"
1232 const std::set<symbol_exprt> &local_statics,
1233 std::set<irep_idt> &function_pointer_contracts)
1244 if(loop.must_skip())
1247 log.
warning() <<
"loop " << function_id <<
"." << loop.cbmc_loop_id
1248 <<
" does not have a contract, skipping instrumentation"
1259 function_pointer_contracts);
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
unsignedbv_typet unsigned_char_type()
Operator to return the address of an object.
goto_instruction_codet representation of a function call statement.
const parameterst & parameters() const
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const std::vector< std::size_t > & get_loops_toposorted() const
const std::unordered_set< irep_idt > & get_top_level_tracked()
Returns the set of top level symbols that must be tracked explicitly in the top level write set of th...
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
bool must_check_lhs(goto_programt::const_targett target) const
True iff the lhs of an assignment must be checked against the ambient write set.
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable to use for the given instruction Returns the write set for the loop,...
bool must_track_decl_or_dead(goto_programt::const_targett target) const
True iff a DECL ident must be tracked in the write set of the loop that contains the DECL.
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
std::size_t get_max_assigns_clause_size() const
Maximum number of assigns clause targets.
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...
void instrument_goto_program(const irep_idt &function_id, goto_programt &goto_program, const exprt &write_set, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO program against a given write set variable.
void instrument_call_instruction(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Adds the write_set as extra argument to a function of function pointer call instruction.
void instrument_lhs(const irep_idt &function_id, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments the LHS of an assignment instruction instruction by adding an inclusion check of lhs in w...
void instrument_other(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a OTHER statement; instruction.
void instrument_assign(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instrument the lhs of an ASSIGN lhs := rhs instruction by adding an inclusion check of lhs in write_s...
void instrument_deallocate_call(const irep_idt &function_id, const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Inserts deallocation checks and a write set update before a call to the __CPROVER_deallocate function...
std::set< irep_idt > internal_symbols
Set of internal symbols which implementation is generated and inlined into the model at conversion or...
dfcc_instrument_loopt instrument_loop
void get_instrumented_functions(std::set< irep_idt > &dest) const
Adds the names of instrumented functions to dest.
message_handlert & message_handler
static std::set< irep_idt > function_cache
Keeps track of instrumented functions, so that no function gets instrumented more than once.
void instrument_goto_function(const irep_idt &function_id, goto_functiont &goto_function, const exprt &write_set, const std::set< symbol_exprt > &local_statics, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments the body of a GOTO function against a given write set.
void instrument_function_call(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a CALL lhs := function(params) instruction by adding an inclusion check of lhs in write_s...
void instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_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 inserting frame condition chec...
void instrument_instructions(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Instruments the instructions found between first_instruction and last_instruction in the instructions...
std::optional< exprt > is_dead_object_update(const exprt &lhs, const exprt &rhs)
Checks if lhs is the dead_object, and if rhs is an if_exprt(nondet, ptr, dead_object) expression.
dfcc_instrumentt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
void instrument_decl(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DECL x instruction.
std::size_t get_max_assigns_clause_size() const
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.
void apply_loop_contracts(const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const loop_contract_configt &loop_contract_config, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
Applies loop contracts transformations to the given GOTO function, using the given cfg_info instance ...
void instrument_dead(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DEAD x instruction.
void instrument_harness_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
void insert_record_dead_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record the death of a local symbol and inserts it in the goto_program at ...
std::set< symbol_exprt > get_local_statics(const irep_idt &function_id)
Returns the set of names from the symbol table that have the static flag set to true and have a sourc...
bool is_internal_symbol(const irep_idt &id) const
True iff the symbol an internal symbol.
void insert_add_decl_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record a locally allocated symbol and inserts it in the goto_program at t...
void instrument_fptr_call_instruction_dynamic_lookup(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Before calling a function pointer, performs a dynamic lookup into the map of instrumented function pr...
Rewrites calls to is_freeable and was_freed predicates in goto programs encoding pre and post conditi...
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_freeable and was_freed predicates into calls to the library implementation in th...
Rewrites calls to is_fresh predicates into calls to the library implementation.
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_fresh predicates into calls to the library implementation in the given program,...
Class interface to library types and functions defined in cprover_contracts.c.
const code_function_callt write_set_record_dead_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_dead.
const code_function_callt write_set_check_assignment_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const exprt &size, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assignment.
const code_function_callt write_set_record_deallocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_deallocated.
const code_function_callt write_set_add_decl_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_decl.
const code_function_callt write_set_check_array_copy_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_copy.
const code_function_callt write_set_add_allocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_allocated.
const symbolt & get_instrumented_functions_map_symbol()
Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.
const code_function_callt write_set_check_array_set_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_set.
const code_function_callt write_set_check_array_replace_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const exprt &src, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_replace.
const code_function_callt write_set_check_deallocate_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_deallocate.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
const code_function_callt write_set_check_havoc_object_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_havoc_object.
Rewrites calls to obeys_contract predicates into calls to the library implementation.
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Rewrites calls to obeys_contract predicates into calls to the library implementation in the given pro...
Rewrites calls to pointer_in_range predicates into calls to the library implementation.
void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info)
Rewrites calls to pointer_in_range predicates into calls to the library implementation in the given p...
This class rewrites GOTO functions that use the built-ins:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string::const_iterator begin() const
Base class for all expressions.
const source_locationt & source_location() const
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
bool body_available() const
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.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
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())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
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())
const irep_idt & id() const
source_locationt source_location
mstreamt & warning() const
message_handlert & get_message_handler()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
const irep_idt & get_statement() const
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt mode
Language mode.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
bool has_prefix(const std::string &s, const std::string &prefix)
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Add instrumentation to a goto program to perform frame condition checks.
This class applies the loop contract transformation to a loop in a goto function.
bool dfcc_is_cprover_function_symbol(const irep_idt &id)
Returns true iff id is one of the known CPROVER functions or starts with __VERIFIER or nondet.
Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses o...
Instruments occurrences of is_fresh predicates in programs encoding requires and ensures clauses of c...
static const std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
Dynamic frame condition checking library loading.
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clause...
Instruments occurrences of pointer_in_range predicates in programs encoding requires and ensures clau...
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Dynamic frame condition checking utility functions.
Fresh auxiliary symbol creation.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
const std::string & id2string(const irep_idt &d)
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define PRECONDITION(CONDITION)
side_effect_exprt & to_side_effect_expr(exprt &expr)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_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.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
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.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
Loop contract configurations.
bool unwind_transformed_loops
bool apply_loop_contracts
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.