Generates the body of a wrapper function from a contract specified using requires, assigns, frees, ensures, clauses attached to a function symbol. More...

#include <dfcc_wrapper_program.h>

Collaboration diagram for dfcc_wrapper_programt:

Public Member Functions
	dfcc_wrapper_programt (const dfcc_contract_modet contract_mode, const symbolt &wrapper_symbol, const symbolt &wrapped_symbol, const dfcc_contract_functionst &contract_functions, const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates)

void	add_to_dest (goto_programt &dest, std::set< irep_idt > &dest_fp_contracts)
	Adds the whole program to `dest` and the discovered function pointer contracts `dest_fp_contracts`.

Protected Member Functions
void	add_to_dest (goto_programt &dest)
	Adds the whole generated program to `dest`, which is meant to be a part of the body of the `wrapper_symbol`.

void	encode_requires_write_set ()
	Encodes the empty write set used to check for side effects in requires.

void	encode_ensures_write_set ()
	Encodes the empty write set used to check for side effects in ensures.

void	encode_contract_write_set ()
	Encodes the write set of the contract being checked/replaced (populated by calling functions provided in contract_functions)

void	encode_ptr_pred_ctx ()
	Encodes the pointer predicates evaluation context object.

void	encode_requires_clauses ()
	Encodes preconditions, instruments them to check for side effects.

void	encode_ensures_clauses ()
	Encodes postconditions, instruments them to check for side effects.

void	encode_function_call ()
	Encodes the function call section of the wrapper program.

void	encode_checked_function_call ()
	Creates a checked function call to the wrapped function, passing it the contract-derived write set as parameter.

void	encode_havoced_function_call ()
	Creates instructions that havoc the contract write set, create a nondet return value, nondeterministically free the freeable part of the write set.

Protected Attributes
const dfcc_contract_modet	contract_mode

const symbolt &	wrapper_symbol

const symbolt &	wrapped_symbol

const dfcc_contract_functionst &	contract_functions

const symbolt &	contract_symbol

const code_with_contract_typet &	contract_code_type

const symbol_exprt	caller_write_set

const source_locationt	wrapper_sl
	Source location with wrapper function name as function name.

std::optional< symbol_exprt >	return_value_opt
	Symbol for the return value of the wrapped function.

const symbol_exprt	contract_write_set
	Symbol for the write set object derived from the contract.

const symbol_exprt	addr_of_contract_write_set
	Symbol for the pointer to the write set object derived from the contract.

const symbol_exprt	requires_write_set
	Symbol for the write set used to check requires clauses for side effects.

const symbol_exprt	addr_of_requires_write_set
	Symbol for the pointer to the write set used to check requires clauses.

const symbol_exprt	ensures_write_set
	Symbol for the write set used to check ensures clauses for side effects.

const symbol_exprt	addr_of_ensures_write_set
	Symbol for the pointer to the write set used to check ensures clauses.

const symbol_exprt	ptr_pred_ctx
	Symbol for the object set used to evaluate is_fresh predicates.

const symbol_exprt	addr_of_ptr_pred_ctx
	Symbol for the pointer to the is_fresh object set.

std::set< irep_idt >	function_pointer_contracts
	Set of required or ensured contracts for function pointers discovered when processing the contract of interest.

goto_modelt &	goto_model

message_handlert &	message_handler

messaget	log

dfcc_libraryt &	library

dfcc_instrumentt &	instrument

dfcc_lift_memory_predicatest &	memory_predicates

namespacet	ns

goto_convertt	converter

exprt::operandst	contract_lambda_parameters
	Vector of arguments to use to instantiate the lambdas wrapping the contract clauses.

goto_programt	preamble

goto_programt	link_ptr_pred_ctx

goto_programt	preconditions

goto_programt	history

goto_programt	write_set_checks

goto_programt	function_call

goto_programt	link_allocated_caller

goto_programt	link_deallocated_contract

goto_programt	postconditions

goto_programt	postamble

Detailed Description

Generates the body of a wrapper function from a contract specified using requires, assigns, frees, ensures, clauses attached to a function symbol.

The desired mode CHECK or REPLACE is given to the constructor of the class.

The body of the wrapper is divided into a number of sections represented as separate goto_programs:

preamble
- create ptr_pred_ctx, requires_write_set, ensures_write_set, contract_write_set variables
link_ptr_pred_ctx
- link the ptr_pred_ctx to requires_write_set and ensures_write_set
- in REPLACE mode, link the caller_write_set to the contract_write_set so that deallocations and allocations are reflected in the caller
preconditions
- evaluate preconditions, while checking the absence of side effects against the empty requires_write_set
history
- declare and snapshot history variables
write_set_checks
- populate the contract write set and check it for inclusion against the caller write set if REPLACE mode is selected.
function_call
- in CHECK mode
  CALL retval = foo(params, contract_write_set);
  
  ait
  ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
  Definition ai.h:562
  
  dfcc_wrapper_programt::contract_write_set
  const symbol_exprt contract_write_set
  Symbol for the write set object derived from the contract.
  Definition dfcc_wrapper_program.h:146
- in REPLACE mode
  CALL foo::havoc(contract_write_set);
  
  CALL deallocate_freeable(contract_write_set, caller_write_set);
  
  ASSIGN retval = nondet
  
  dfcc_wrapper_programt::caller_write_set
  const symbol_exprt caller_write_set
  Definition dfcc_wrapper_program.h:137
  
  ASSIGN
  @ ASSIGN
  Definition goto_program.h:46
link_allocated_caller in REPLACE mode, links the allocated set of the caller to the ensures_write_set, so that allocations performed by is fresh in post conditions get recorded in the caller write set and are considered as assignable for the caller (In CHECK mode, the caller write set comes from the proof harness and is NULL and ignored).
CALL link_allocated(ensures_write_set, caller_write_set);

dfcc_wrapper_programt::ensures_write_set
const symbol_exprt ensures_write_set
Symbol for the write set used to check ensures clauses for side effects.
Definition dfcc_wrapper_program.h:158
link_deallocated_contract links the deallocated set of the contract_write_set to the ensures_write_set, so that was_freed predicates can be evaluated in the post conditions.
CALL link_allocated(ensures_write_set, caller_write_set);
postconditions
- reset pointer predicate context object, evaluate preconditions while checking absence of side effects against the empty ensures_write_set
postamble
- release all object sets and write set variables

There a private method per type of contract clause, which adds contents encoding the semantics of the clause to the appropriate section when called.

The public method add_to_dest calls the private methods to populate the sections, and then adds the contents of these sections in order to the given destination program.

Definition at line 97 of file dfcc_wrapper_program.h.

Constructor & Destructor Documentation

◆ dfcc_wrapper_programt()

dfcc_wrapper_programt::dfcc_wrapper_programt	(	const dfcc_contract_modet	contract_mode,
		const symbolt &	wrapper_symbol,
		const symbolt &	wrapped_symbol,
		const dfcc_contract_functionst &	contract_functions,
		const symbolt &	caller_write_set_symbol,
		goto_modelt &	goto_model,
		message_handlert &	message_handler,
		dfcc_libraryt &	library,
		dfcc_instrumentt &	instrument,
		dfcc_lift_memory_predicatest &	memory_predicates
	)

Parameters

contract_mode	checking or replacement mode for the contract
wrapper_symbol	function symbol receiving the generated instructions
wrapped_symbol	function symbol being checked or replaced
contract_functions	contains the contract expressions and the assigns/frees/havoc functions symbols derived from the contract
caller_write_set_symbol	symbol representing the write set passed to the wrapper function by its caller.
goto_model	the goto model being transformed
message_handler	used for debug/warning/error messages
library	the contracts instrumentation library
instrument	the instrumenter class for goto functions/goto programs
memory_predicates	handler for user-defed memory predicates, used to adjust call parameters for user defined predicates used in requires and ensures clauses.

Definition at line 146 of file dfcc_wrapper_program.cpp.

Member Function Documentation

◆ add_to_dest() [1/2]

void dfcc_wrapper_programt::add_to_dest ( goto_programt & dest )

protected

Adds the whole generated program to dest, which is meant to be a part of the body of the wrapper_symbol.

Definition at line 246 of file dfcc_wrapper_program.cpp.

◆ add_to_dest() [2/2]

void dfcc_wrapper_programt::add_to_dest	(	goto_programt &	dest,
		std::set< irep_idt > &	dest_fp_contracts
	)

Adds the whole program to dest and the discovered function pointer contracts dest_fp_contracts.

Definition at line 237 of file dfcc_wrapper_program.cpp.

◆ encode_checked_function_call()

void dfcc_wrapper_programt::encode_checked_function_call ( )

protected

Creates a checked function call to the wrapped function, passing it the contract-derived write set as parameter.

Definition at line 764 of file dfcc_wrapper_program.cpp.

◆ encode_contract_write_set()

void dfcc_wrapper_programt::encode_contract_write_set ( )

protected

Encodes the write set of the contract being checked/replaced (populated by calling functions provided in contract_functions)

Adds declaration of write set and pointer to write set to preamble
Adds initialisation function call in write_set_checks
Adds contract::c_assigns and contract::frees function call in write_set_checks
Adds release function call in postamble

Definition at line 416 of file dfcc_wrapper_program.cpp.

◆ encode_ensures_clauses()

void dfcc_wrapper_programt::encode_ensures_clauses ( )

protected

Encodes postconditions, instruments them to check for side effects.

Definition at line 692 of file dfcc_wrapper_program.cpp.

◆ encode_ensures_write_set()

void dfcc_wrapper_programt::encode_ensures_write_set ( )

protected

Encodes the empty write set used to check for side effects in ensures.

Adds declaration of write set and pointer to write set to preamble
Adds initialisation function call in preamble
Adds alloc/deallocation checking assertion in postamble
Adds release function call in postamble

Definition at line 333 of file dfcc_wrapper_program.cpp.

◆ encode_function_call()

void dfcc_wrapper_programt::encode_function_call ( )

protected

Encodes the function call section of the wrapper program.

Definition at line 756 of file dfcc_wrapper_program.cpp.

◆ encode_havoced_function_call()

void dfcc_wrapper_programt::encode_havoced_function_call ( )

protected

Creates instructions that havoc the contract write set, create a nondet return value, nondeterministically free the freeable part of the write set.

Definition at line 800 of file dfcc_wrapper_program.cpp.

◆ encode_ptr_pred_ctx()

void dfcc_wrapper_programt::encode_ptr_pred_ctx ( )

protected

Encodes the pointer predicates evaluation context object.

Adds declaration of context object and pointer to preamble
Adds init function call in preamble
Adds reset function call in link_deallocated_contract
Adds dead instruction in postamble

Definition at line 504 of file dfcc_wrapper_program.cpp.

◆ encode_requires_clauses()

void dfcc_wrapper_programt::encode_requires_clauses ( )

protected

Encodes preconditions, instruments them to check for side effects.

Definition at line 636 of file dfcc_wrapper_program.cpp.

◆ encode_requires_write_set()

void dfcc_wrapper_programt::encode_requires_write_set ( )

protected

Encodes the empty write set used to check for side effects in requires.

Adds declaration of write set and pointer to write set to preamble
Adds initialisation function call in preamble
Adds alloc/deallocation checking assertion in postamble
Adds release function call in postamble

Definition at line 261 of file dfcc_wrapper_program.cpp.

Member Data Documentation

◆ addr_of_contract_write_set

const symbol_exprt dfcc_wrapper_programt::addr_of_contract_write_set

protected

Symbol for the pointer to the write set object derived from the contract.

Definition at line 149 of file dfcc_wrapper_program.h.

◆ addr_of_ensures_write_set

const symbol_exprt dfcc_wrapper_programt::addr_of_ensures_write_set

protected

Symbol for the pointer to the write set used to check ensures clauses.

Definition at line 161 of file dfcc_wrapper_program.h.

◆ addr_of_ptr_pred_ctx

const symbol_exprt dfcc_wrapper_programt::addr_of_ptr_pred_ctx

protected

Symbol for the pointer to the is_fresh object set.

Definition at line 167 of file dfcc_wrapper_program.h.

◆ addr_of_requires_write_set

const symbol_exprt dfcc_wrapper_programt::addr_of_requires_write_set

protected

Symbol for the pointer to the write set used to check requires clauses.

Definition at line 155 of file dfcc_wrapper_program.h.

◆ caller_write_set

const symbol_exprt dfcc_wrapper_programt::caller_write_set

protected

Definition at line 137 of file dfcc_wrapper_program.h.

◆ contract_code_type

const code_with_contract_typet& dfcc_wrapper_programt::contract_code_type

protected

Definition at line 136 of file dfcc_wrapper_program.h.

◆ contract_functions

const dfcc_contract_functionst& dfcc_wrapper_programt::contract_functions

protected

Definition at line 134 of file dfcc_wrapper_program.h.

◆ contract_lambda_parameters

exprt::operandst dfcc_wrapper_programt::contract_lambda_parameters

protected

Vector of arguments to use to instantiate the lambdas wrapping the contract clauses.

Definition at line 184 of file dfcc_wrapper_program.h.

◆ contract_mode

const dfcc_contract_modet dfcc_wrapper_programt::contract_mode

protected

Definition at line 131 of file dfcc_wrapper_program.h.

◆ contract_symbol

const symbolt& dfcc_wrapper_programt::contract_symbol

protected

Definition at line 135 of file dfcc_wrapper_program.h.

◆ contract_write_set

const symbol_exprt dfcc_wrapper_programt::contract_write_set

protected

Symbol for the write set object derived from the contract.

Definition at line 146 of file dfcc_wrapper_program.h.

◆ converter

goto_convertt dfcc_wrapper_programt::converter

protected

Definition at line 180 of file dfcc_wrapper_program.h.

◆ ensures_write_set

const symbol_exprt dfcc_wrapper_programt::ensures_write_set

protected

Symbol for the write set used to check ensures clauses for side effects.

Definition at line 158 of file dfcc_wrapper_program.h.

◆ function_call

goto_programt dfcc_wrapper_programt::function_call

protected

Definition at line 196 of file dfcc_wrapper_program.h.

◆ function_pointer_contracts

std::set<irep_idt> dfcc_wrapper_programt::function_pointer_contracts

protected

Set of required or ensured contracts for function pointers discovered when processing the contract of interest.

Definition at line 171 of file dfcc_wrapper_program.h.

◆ goto_model

goto_modelt& dfcc_wrapper_programt::goto_model

protected

Definition at line 173 of file dfcc_wrapper_program.h.

◆ history

goto_programt dfcc_wrapper_programt::history

protected

Definition at line 194 of file dfcc_wrapper_program.h.

◆ instrument

dfcc_instrumentt& dfcc_wrapper_programt::instrument

protected

Definition at line 177 of file dfcc_wrapper_program.h.

◆ library

dfcc_libraryt& dfcc_wrapper_programt::library

protected

Definition at line 176 of file dfcc_wrapper_program.h.

◆ link_allocated_caller

goto_programt dfcc_wrapper_programt::link_allocated_caller

protected

Definition at line 197 of file dfcc_wrapper_program.h.

◆ link_deallocated_contract

goto_programt dfcc_wrapper_programt::link_deallocated_contract

protected

Definition at line 198 of file dfcc_wrapper_program.h.

◆ link_ptr_pred_ctx

goto_programt dfcc_wrapper_programt::link_ptr_pred_ctx

protected

Definition at line 192 of file dfcc_wrapper_program.h.

◆ log

messaget dfcc_wrapper_programt::log

protected

Definition at line 175 of file dfcc_wrapper_program.h.

◆ memory_predicates

dfcc_lift_memory_predicatest& dfcc_wrapper_programt::memory_predicates

protected

Definition at line 178 of file dfcc_wrapper_program.h.

◆ message_handler

message_handlert& dfcc_wrapper_programt::message_handler

protected

Definition at line 174 of file dfcc_wrapper_program.h.

◆ ns

namespacet dfcc_wrapper_programt::ns

protected

Definition at line 179 of file dfcc_wrapper_program.h.

◆ postamble

goto_programt dfcc_wrapper_programt::postamble

protected

Definition at line 200 of file dfcc_wrapper_program.h.

◆ postconditions

goto_programt dfcc_wrapper_programt::postconditions

protected

Definition at line 199 of file dfcc_wrapper_program.h.

◆ preamble

goto_programt dfcc_wrapper_programt::preamble

protected

Definition at line 191 of file dfcc_wrapper_program.h.

◆ preconditions

goto_programt dfcc_wrapper_programt::preconditions

protected

Definition at line 193 of file dfcc_wrapper_program.h.

◆ ptr_pred_ctx

const symbol_exprt dfcc_wrapper_programt::ptr_pred_ctx

protected

Symbol for the object set used to evaluate is_fresh predicates.

Definition at line 164 of file dfcc_wrapper_program.h.

◆ requires_write_set

const symbol_exprt dfcc_wrapper_programt::requires_write_set

protected

Symbol for the write set used to check requires clauses for side effects.

Definition at line 152 of file dfcc_wrapper_program.h.

◆ return_value_opt

std::optional<symbol_exprt> dfcc_wrapper_programt::return_value_opt

protected

Symbol for the return value of the wrapped function.

Definition at line 143 of file dfcc_wrapper_program.h.

◆ wrapped_symbol

const symbolt& dfcc_wrapper_programt::wrapped_symbol

protected

Definition at line 133 of file dfcc_wrapper_program.h.

◆ wrapper_sl

const source_locationt dfcc_wrapper_programt::wrapper_sl

protected

Source location with wrapper function name as function name.

Definition at line 140 of file dfcc_wrapper_program.h.

◆ wrapper_symbol

const symbolt& dfcc_wrapper_programt::wrapper_symbol

protected

Definition at line 132 of file dfcc_wrapper_program.h.

◆ write_set_checks

goto_programt dfcc_wrapper_programt::write_set_checks

protected

Definition at line 195 of file dfcc_wrapper_program.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_wrapper_programt()

Member Function Documentation

◆ add_to_dest() [1/2]

◆ add_to_dest() [2/2]

◆ encode_checked_function_call()

◆ encode_contract_write_set()

◆ encode_ensures_clauses()

◆ encode_ensures_write_set()

◆ encode_function_call()

◆ encode_havoced_function_call()

◆ encode_ptr_pred_ctx()

◆ encode_requires_clauses()

◆ encode_requires_write_set()

Member Data Documentation

◆ addr_of_contract_write_set

◆ addr_of_ensures_write_set

◆ addr_of_ptr_pred_ctx

◆ addr_of_requires_write_set

◆ caller_write_set

◆ contract_code_type

◆ contract_functions

◆ contract_lambda_parameters

◆ contract_mode

◆ contract_symbol

◆ contract_write_set

◆ converter

◆ ensures_write_set

◆ function_call

◆ function_pointer_contracts

◆ goto_model

◆ history

◆ instrument

◆ library

◆ link_allocated_caller

◆ link_deallocated_contract

◆ link_ptr_pred_ctx

◆ log

◆ memory_predicates

◆ message_handler

◆ ns

◆ postamble

◆ postconditions

◆ preamble

◆ preconditions

◆ ptr_pred_ctx

◆ requires_write_set

◆ return_value_opt

◆ wrapped_symbol

◆ wrapper_sl

◆ wrapper_symbol

◆ write_set_checks