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 dfcc_loop_contract_modet loop_contract_mode, 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 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 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 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 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 dfcc_loop_contract_modet loop_contract_mode, 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 dfcc_loop_contract_modet loop_contract_mode, 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...

Detailed Description

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

Definition at line 42 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 dfcc_loop_contract_modet  loop_contract_mode, 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 1238 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_id

Function 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;
CALL __CPROVER_contracts_write_set_add_decl(write_set, &x);
skip_target: SKIP;

Parameters

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 581 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;
CALL __CPROVER_contracts_write_set_record_dead(write_set, &x);
skip_target: SKIP;

Parameters

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 628 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 775 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 909 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

insert_record_dead_call(...);
----
DEAD x;

Definition at line 659 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 937 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;
----
insert_add_decl_call(...);

Definition at line 611 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 859 of file dfcc_instrument.cpp.

instrument_function()

void dfcc_instrumentt::instrument_function	(	const irep_idt &	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 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_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_mode	Mode 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.

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 1006 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 dfcc_loop_contract_modet  loop_contract_mode, 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 427 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_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.

instrument_harness_function()

void dfcc_instrumentt::instrument_harness_function	(	const irep_idt &	function_id,
		const dfcc_loop_contract_modet	loop_contract_mode,
		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_id	Function to instrument
loop_contract_mode	Mode 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.

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_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 518 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 674 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 1040 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 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 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_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_mode	Mode 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.

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 756 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 170 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 176 of file dfcc_instrument.h.

goto_model

goto_modelt& dfcc_instrumentt::goto_model

protected

Definition at line 165 of file dfcc_instrument.h.

instrument_loop

dfcc_instrument_loopt dfcc_instrumentt::instrument_loop

protected

Definition at line 171 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 181 of file dfcc_instrument.h.

library

dfcc_libraryt& dfcc_instrumentt::library

protected

Definition at line 168 of file dfcc_instrument.h.

log

messaget dfcc_instrumentt::log

protected

Definition at line 167 of file dfcc_instrument.h.

message_handler

message_handlert& dfcc_instrumentt::message_handler

protected

Definition at line 166 of file dfcc_instrument.h.

ns

namespacet dfcc_instrumentt::ns

protected

Definition at line 172 of file dfcc_instrument.h.

spec_functions

dfcc_spec_functionst& dfcc_instrumentt::spec_functions

protected

Definition at line 169 of file dfcc_instrument.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h
• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp