CBMC
|
This class instruments GOTO functions or instruction sequences for frame condition checking and loop contracts. More...
#include <dfcc_instrument.h>
Public Member Functions | |
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) | |
bool | is_internal_symbol (const irep_idt &id) const |
True iff the symbol an internal symbol. More... | |
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. More... | |
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. More... | |
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 instructions against the write set. More... | |
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 checks in its GOTO program, as well as instructions to automatically insert and remove locally declared static variables in the write set. More... | |
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. More... | |
void | get_instrumented_functions (std::set< irep_idt > &dest) const |
Adds the names of instrumented functions to dest . More... | |
std::size_t | get_max_assigns_clause_size () const |
Protected Member Functions | |
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 source location where the function field is equal to the given function_id . More... | |
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 the target, and moves the target forward. More... | |
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 the target, and moves the target forward. More... | |
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. More... | |
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 of goto_program against the given write_set variable. More... | |
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. More... | |
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. More... | |
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 write_set . More... | |
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. More... | |
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_set . More... | |
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. More... | |
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 provided by dfcc_libraryt::get_instrumented_functions_map_symbol, and passes the write_set parameter to the function pointer only if it points to a function known to be instrumented and hence able to accept this parameter. More... | |
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. More... | |
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_set , and passing write_set as an extra argument to the function call. More... | |
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. More... | |
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 to drive the transformation. More... | |
Protected Attributes | |
goto_modelt & | goto_model |
message_handlert & | message_handler |
messaget | log |
dfcc_libraryt & | library |
dfcc_spec_functionst & | spec_functions |
dfcc_contract_clauses_codegent & | contract_clauses_codegen |
dfcc_instrument_loopt | instrument_loop |
namespacet | ns |
std::set< irep_idt > | internal_symbols |
Set of internal symbols which implementation is generated and inlined into the model at conversion or symex time and must not be instrumented. More... | |
Static Protected Attributes | |
static std::set< irep_idt > | function_cache |
Keeps track of instrumented functions, so that no function gets instrumented more than once. More... | |
This class instruments GOTO functions or instruction sequences for frame condition checking and loop contracts.
Definition at line 43 of file dfcc_instrument.h.
dfcc_instrumentt::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 | ||
) |
These builtins are translated to no-ops and must not be instrumented
These builtins are valist management functions and interpreted natively in src/goto-symex/symex_builtin_functions.cpp and must not be instrumented
These builtins get translated to CPROVER equivalents and must not be instrumented
Definition at line 48 of file dfcc_instrument.cpp.
|
protected |
Applies loop contracts transformations to the given GOTO function, using the given cfg_info instance to drive the transformation.
Definition at line 1227 of file dfcc_instrument.cpp.
bool dfcc_instrumentt::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.
Definition at line 232 of file dfcc_instrument.cpp.
void dfcc_instrumentt::get_instrumented_functions | ( | std::set< irep_idt > & | dest | ) | const |
Adds the names of instrumented functions to dest
.
The names are kept track of in the function_cache field.
Definition at line 101 of file dfcc_instrument.cpp.
|
protected |
Returns the set of names from the symbol table that have the static flag set to true and have a source location where the function field is equal to the given function_id
.
[in] | function_id | Function name used to collect the statics. |
Definition at line 299 of file dfcc_instrument.cpp.
std::size_t dfcc_instrumentt::get_max_assigns_clause_size | ( | ) | const |
Definition at line 109 of file dfcc_instrument.cpp.
|
protected |
Generates a guarded call to record a locally allocated symbol and inserts it in the goto_program at the target, and moves the target forward.
function_id | Name of the function in which the instructions is added |
write_set | The write set to the symbol expr to |
symbol_expr | The symbol to add to the write set |
target | The instruction pointer to insert at |
goto_program | the goto_program being instrumented |
Definition at line 583 of file dfcc_instrument.cpp.
|
protected |
Generates a guarded call to record the death of a local symbol and inserts it in the goto_program at the target, and moves the target forward.
function_id | Name of the function in which the instructions is added |
write_set | The write set to the symbol expr to |
symbol_expr | The symbol to add to the write set |
target | The instruction pointer to insert at |
goto_program | the goto_program being instrumented |
Definition at line 630 of file dfcc_instrument.cpp.
|
protected |
Instrument the lhs
of an ASSIGN lhs := rhs
instruction by adding an inclusion check of lhs
in write_set
.
If is_dead_object_update returns a successful match, the matched pointer expression is removed from write_set
. If rhs
is a side_effect_expr(ID_allocate)
, the allocated pointer gets added to the write_set
.
target
points to an ASSIGN
instruction. Definition at line 763 of file dfcc_instrument.cpp.
|
protected |
Adds the write_set
as extra argument to a function of function pointer call instruction.
target
points to a CALL
instruction. Definition at line 898 of file dfcc_instrument.cpp.
|
protected |
Instruments a DEAD x
instruction.
target
points to a DEAD
instructionDefinition at line 661 of file dfcc_instrument.cpp.
|
protected |
Inserts deallocation checks and a write set update before a call to the __CPROVER_deallocate function.
target
points to a CALL __CPROVER_deallocate
instruction. Definition at line 926 of file dfcc_instrument.cpp.
|
protected |
Instruments a DECL x
instruction.
target
points to a DECL
instructionDefinition at line 613 of file dfcc_instrument.cpp.
|
protected |
Before calling a function pointer, performs a dynamic lookup into the map of instrumented function provided by dfcc_libraryt::get_instrumented_functions_map_symbol, and passes the write_set parameter to the function pointer only if it points to a function known to be instrumented and hence able to accept this parameter.
target
points to a CALL
instruction where the function expression is not a symbol_exprt. Definition at line 848 of file dfcc_instrument.cpp.
void dfcc_instrumentt::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 instructions against the write set.
Adds ghost instructions that automatically insert locally declared static variables to the write set when entering the function and removing them upon exit.
function_id | The name of the function, used to retrieve the function to instrument and used as prefix when generating new symbols during instrumentation. |
loop_contract_config | Config to use for loop contracts |
function_pointer_contracts | Contracts discovered in calls to the obeys_contract predicate are added to this set. |
Definition at line 317 of file dfcc_instrument.cpp.
|
protected |
Instruments a CALL lhs := function(params)
instruction by adding an inclusion check of lhs
in write_set
, and passing write_set
as an extra argument to the function call.
target
points to a CALL
instruction. Definition at line 995 of file dfcc_instrument.cpp.
|
protected |
Instruments the body of a GOTO function against a given write set.
Adds the given local statics to the write set in pre and removes them post.
Definition at line 428 of file dfcc_instrument.cpp.
void dfcc_instrumentt::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.
is_parameter
flag set to true, which represent parameters of the enclosing function, are not considered implicitly assignable. function_id | Name used as prefix when creating new symbols during instrumentation. |
goto_program | GOTO program to instrument. |
write_set | Write set variable to use for instrumentation. |
function_pointer_contracts | Discovered function pointer contracts |
Definition at line 390 of file dfcc_instrument.cpp.
void dfcc_instrumentt::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.
Proof harnesses are closed functions without parameters, so we declare a local write set pointer and initialise it to NULL, and check body instructions against that NULL write set.
By using a NULL write set pointer we ensure that no checks are being performed in the harness or in the functions called from the harness, except in the following cases:
function_id | Function to instrument |
loop_contract_config | Config to use for loop contracts |
function_pointer_contracts | Contract names discovered in calls to the obeys_contract predicate are added to this set. |
Definition at line 238 of file dfcc_instrument.cpp.
|
protected |
Instruments the instructions found between first_instruction
and last_instruction
in the instructions of goto_program
against the given write_set
variable.
function_id | Name of the enclosing function used as prefix for new variables generated during instrumentation. |
goto_program | Program to instrument the instructions of |
first_instruction | First instruction to instrument in the program |
last_instruction | Last instruction to instrument (excluded !!!) |
cfg_info | Computes local and dirty variables to discard some checks |
function_pointer_contracts | Contracts discovered in calls to the obeys_contract predicate are added to this set. |
Definition at line 520 of file dfcc_instrument.cpp.
|
protected |
Instruments the LHS of an assignment instruction instruction by adding an inclusion check of lhs
in write_set
.
Definition at line 676 of file dfcc_instrument.cpp.
|
protected |
Instruments a OTHER statement;
instruction.
OTHER instructions can be an array_set, array_copy, array_replace or a havoc_object instruction.
target
points to an OTHER
instruction. Definition at line 1029 of file dfcc_instrument.cpp.
void dfcc_instrumentt::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 checks in its GOTO program, as well as instructions to automatically insert and remove locally declared static variables in the write set.
wrapped_function_id | The name of the function, used to retrieve the function to instrument and used as prefix when generating new symbols during instrumentation. |
initial_function_id | The initial name of the function, before mangling. This is the name used to identify statics symbols in the symbol table that were locally declared in the function. |
loop_contract_config | Config to use for loop contracts |
function_pointer_contracts | contracts discovered in calls to the obeys_contract predicate are added to this set. |
Definition at line 352 of file dfcc_instrument.cpp.
|
protected |
Checks if lhs
is the dead_object
, and if rhs
is an if_exprt(nondet, ptr, dead_object)
expression.
Checks if lhs is the dead_object
, and if the rhs is an if_exprt(nondet, ptr, dead_object)
expression.
Returns a pointer to the ptr
expression if the pattern was matched, returns nullptr
otherwise.
Returns ptr
if the pattern was matched, nullptr otherwise.
Definition at line 742 of file dfcc_instrument.cpp.
bool dfcc_instrumentt::is_internal_symbol | ( | const irep_idt & | id | ) | const |
True iff the symbol an internal symbol.
True iff the symbol must not be instrumented.
Definition at line 227 of file dfcc_instrument.cpp.
|
protected |
Definition at line 171 of file dfcc_instrument.h.
|
staticprotected |
Keeps track of instrumented functions, so that no function gets instrumented more than once.
Definition at line 177 of file dfcc_instrument.h.
|
protected |
Definition at line 166 of file dfcc_instrument.h.
|
protected |
Definition at line 172 of file dfcc_instrument.h.
|
protected |
Set of internal symbols which implementation is generated and inlined into the model at conversion or symex time and must not be instrumented.
Definition at line 182 of file dfcc_instrument.h.
|
protected |
Definition at line 169 of file dfcc_instrument.h.
|
protected |
Definition at line 168 of file dfcc_instrument.h.
|
protected |
Definition at line 167 of file dfcc_instrument.h.
|
protected |
Definition at line 173 of file dfcc_instrument.h.
|
protected |
Definition at line 170 of file dfcc_instrument.h.