CBMC
dfcc_instrumentt Class Reference

This class instruments GOTO functions or instruction sequences for frame condition checking and loop contracts. More...

#include <dfcc_instrument.h>

+ Collaboration diagram for dfcc_instrumentt:

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_exprtget_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< exprtis_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_modeltgoto_model
 
message_handlertmessage_handler
 
messaget log
 
dfcc_librarytlibrary
 
dfcc_spec_functionstspec_functions
 
dfcc_contract_clauses_codegentcontract_clauses_codegen
 
dfcc_instrument_loopt instrument_loop
 
namespacet ns
 
std::set< irep_idtinternal_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_idtfunction_cache
 Keeps track of instrumented functions, so that no function gets instrumented more than once. More...
 

Detailed Description

This class instruments GOTO functions or instruction sequences for frame condition checking and loop contracts.

Definition at line 43 of file dfcc_instrument.h.

Constructor & Destructor Documentation

◆ dfcc_instrumentt()

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.

Member Function Documentation

◆ apply_loop_contracts()

void dfcc_instrumentt::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 
)
protected

Applies loop contracts transformations to the given GOTO function, using the given cfg_info instance to drive the transformation.

Precondition
Instructions of the function must already have been instrumented for DFCC using the same cfg_info.

Definition at line 1227 of file dfcc_instrument.cpp.

◆ do_not_instrument()

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.

◆ get_instrumented_functions()

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.

◆ get_local_statics()

std::set< symbol_exprt > dfcc_instrumentt::get_local_statics ( const irep_idt function_id)
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 .

Parameters
[in]function_idFunction name used to collect the statics.

Definition at line 299 of file dfcc_instrument.cpp.

◆ get_max_assigns_clause_size()

std::size_t dfcc_instrumentt::get_max_assigns_clause_size ( ) const
Returns
The maximum assigns clause size discovered when instrumenting loop contracts

Definition at line 109 of file dfcc_instrument.cpp.

◆ insert_add_decl_call()

void dfcc_instrumentt::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 
)
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.

IF !write_set GOTO skip_target;
skip_target: SKIP;
void __CPROVER_contracts_write_set_add_decl(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Adds the pointer ptr to set->allocated.
@ SKIP
Definition: goto_program.h:38
@ GOTO
Definition: goto_program.h:34
Parameters
function_idName of the function in which the instructions is added
write_setThe write set to the symbol expr to
symbol_exprThe symbol to add to the write set
targetThe instruction pointer to insert at
goto_programthe goto_program being instrumented

Definition at line 583 of file dfcc_instrument.cpp.

◆ insert_record_dead_call()

void dfcc_instrumentt::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 
)
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.

IF !write_set GOTO skip_target;
skip_target: SKIP;
void __CPROVER_contracts_write_set_record_dead(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Records that an object is dead by removing the pointer ptr from set->allocated.
Parameters
function_idName of the function in which the instructions is added
write_setThe write set to the symbol expr to
symbol_exprThe symbol to add to the write set
targetThe instruction pointer to insert at
goto_programthe goto_program being instrumented

Definition at line 630 of file dfcc_instrument.cpp.

◆ instrument_assign()

void dfcc_instrumentt::instrument_assign ( const irep_idt function_id,
goto_programt::targett target,
goto_programt goto_program,
dfcc_cfg_infot cfg_info 
)
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.

Precondition
target points to an ASSIGN instruction.

Definition at line 763 of file dfcc_instrument.cpp.

◆ instrument_call_instruction()

void dfcc_instrumentt::instrument_call_instruction ( const exprt write_set,
goto_programt::targett target,
goto_programt goto_program 
)
protected

Adds the write_set as extra argument to a function of function pointer call instruction.

Precondition
target points to a CALL instruction.

Definition at line 898 of file dfcc_instrument.cpp.

◆ instrument_dead()

void dfcc_instrumentt::instrument_dead ( const irep_idt function_id,
goto_programt::targett target,
goto_programt goto_program,
dfcc_cfg_infot cfg_info 
)
protected

Instruments a DEAD x instruction.

Precondition
target points to a DEAD instruction
----
DEAD x;
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 ...
@ DEAD
Definition: goto_program.h:48

Definition at line 661 of file dfcc_instrument.cpp.

◆ instrument_deallocate_call()

void dfcc_instrumentt::instrument_deallocate_call ( const irep_idt function_id,
const exprt write_set,
goto_programt::targett target,
goto_programt goto_program 
)
protected

Inserts deallocation checks and a write set update before a call to the __CPROVER_deallocate function.

Precondition
target points to a CALL __CPROVER_deallocate instruction.

Definition at line 926 of file dfcc_instrument.cpp.

◆ instrument_decl()

void dfcc_instrumentt::instrument_decl ( const irep_idt function_id,
goto_programt::targett target,
goto_programt goto_program,
dfcc_cfg_infot cfg_info 
)
protected

Instruments a DECL x instruction.

Precondition
target points to a DECL instruction
DECL x;
----
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...
@ DECL
Definition: goto_program.h:47

Definition at line 613 of file dfcc_instrument.cpp.

◆ instrument_fptr_call_instruction_dynamic_lookup()

void dfcc_instrumentt::instrument_fptr_call_instruction_dynamic_lookup ( const exprt write_set,
goto_programt::targett target,
goto_programt goto_program 
)
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.

Precondition
target points to a CALL instruction where the function expression is not a symbol_exprt.

Definition at line 848 of file dfcc_instrument.cpp.

◆ instrument_function()

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.

Precondition
The function must not be one of the functions checked against a contract or replaced by a contract. The method instrument_wrapped_function must be used to instrument check/replaced functions instead.
Parameters
function_idThe name of the function, used to retrieve the function to instrument and used as prefix when generating new symbols during instrumentation.
loop_contract_configConfig to use for loop contracts
function_pointer_contractsContracts discovered in calls to the obeys_contract predicate are added to this set.

Definition at line 317 of file dfcc_instrument.cpp.

◆ instrument_function_call()

void dfcc_instrumentt::instrument_function_call ( const irep_idt function_id,
goto_programt::targett target,
goto_programt goto_program,
dfcc_cfg_infot cfg_info 
)
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.

Precondition
target points to a CALL instruction.

Definition at line 995 of file dfcc_instrument.cpp.

◆ instrument_goto_function()

void dfcc_instrumentt::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 
)
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.

◆ instrument_goto_program()

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.

Remarks
This function is meant to instrument instruction sequences generated from contract clauses.
Only variables declared within the instruction sequence are considered local and implicitly assignable. In particular, occurrences of symbols with the is_parameter flag set to true, which represent parameters of the enclosing function, are not considered implicitly assignable.
Loop contracts are never applied.
Local statics are not collected and added to the write set.
Parameters
function_idName used as prefix when creating new symbols during instrumentation.
goto_programGOTO program to instrument.
write_setWrite set variable to use for instrumentation.
function_pointer_contractsDiscovered function pointer contracts

Definition at line 390 of file dfcc_instrument.cpp.

◆ instrument_harness_function()

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:

  1. One of the functions called directly (or indirectly) by the harness is a verification wrapper function that checks some contract against some function. This wrapper will ignore the NULL write set it received from the harness and will instantiate its own write set from the contract and pass it to the function under analysis.
  2. The harness function contains loops that have contracts. A write set is created for each loop and loop instructions instrumented against that write set. The write set is propagated to all functions called from the loop.
Parameters
function_idFunction to instrument
loop_contract_configConfig to use for loop contracts
function_pointer_contractsContract names discovered in calls to the obeys_contract predicate are added to this set.

Definition at line 238 of file dfcc_instrument.cpp.

◆ instrument_instructions()

void dfcc_instrumentt::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 
)
protected

Instruments the instructions found between first_instruction and last_instruction in the instructions of goto_program against the given write_set variable.

Parameters
function_idName of the enclosing function used as prefix for new variables generated during instrumentation.
goto_programProgram to instrument the instructions of
first_instructionFirst instruction to instrument in the program
last_instructionLast instruction to instrument (excluded !!!)
cfg_infoComputes local and dirty variables to discard some checks
function_pointer_contractsContracts discovered in calls to the obeys_contract predicate are added to this set.

Definition at line 520 of file dfcc_instrument.cpp.

◆ instrument_lhs()

void dfcc_instrumentt::instrument_lhs ( const irep_idt function_id,
goto_programt::targett target,
const exprt lhs,
goto_programt goto_program,
dfcc_cfg_infot cfg_info 
)
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.

◆ instrument_other()

void dfcc_instrumentt::instrument_other ( const irep_idt function_id,
goto_programt::targett target,
goto_programt goto_program,
dfcc_cfg_infot cfg_info 
)
protected

Instruments a OTHER statement; instruction.

OTHER instructions can be an array_set, array_copy, array_replace or a havoc_object instruction.

Precondition
target points to an OTHER instruction.

Definition at line 1029 of file dfcc_instrument.cpp.

◆ instrument_wrapped_function()

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.

Precondition
The function must be a function wrapped for contract checking or replacement checking. For other functions instrument_function must be used instead. The difference is that checked or replaced functions have their name mangled, so the the search for local statics uses a possibly different function identifier as base name for static symbols.
Parameters
wrapped_function_idThe name of the function, used to retrieve the function to instrument and used as prefix when generating new symbols during instrumentation.
initial_function_idThe 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_configConfig to use for loop contracts
function_pointer_contractscontracts discovered in calls to the obeys_contract predicate are added to this set.

Definition at line 352 of file dfcc_instrument.cpp.

◆ is_dead_object_update()

std::optional< exprt > dfcc_instrumentt::is_dead_object_update ( const exprt lhs,
const exprt rhs 
)
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.

◆ is_internal_symbol()

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.

Member Data Documentation

◆ contract_clauses_codegen

dfcc_contract_clauses_codegent& dfcc_instrumentt::contract_clauses_codegen
protected

Definition at line 171 of file dfcc_instrument.h.

◆ function_cache

std::set< irep_idt > dfcc_instrumentt::function_cache
staticprotected

Keeps track of instrumented functions, so that no function gets instrumented more than once.

Definition at line 177 of file dfcc_instrument.h.

◆ goto_model

goto_modelt& dfcc_instrumentt::goto_model
protected

Definition at line 166 of file dfcc_instrument.h.

◆ instrument_loop

dfcc_instrument_loopt dfcc_instrumentt::instrument_loop
protected

Definition at line 172 of file dfcc_instrument.h.

◆ internal_symbols

std::set<irep_idt> dfcc_instrumentt::internal_symbols
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.

◆ library

dfcc_libraryt& dfcc_instrumentt::library
protected

Definition at line 169 of file dfcc_instrument.h.

◆ log

messaget dfcc_instrumentt::log
protected

Definition at line 168 of file dfcc_instrument.h.

◆ message_handler

message_handlert& dfcc_instrumentt::message_handler
protected

Definition at line 167 of file dfcc_instrument.h.

◆ ns

namespacet dfcc_instrumentt::ns
protected

Definition at line 173 of file dfcc_instrument.h.

◆ spec_functions

dfcc_spec_functionst& dfcc_instrumentt::spec_functions
protected

Definition at line 170 of file dfcc_instrument.h.


The documentation for this class was generated from the following files: