CBMC
dfcc_wrapper_programt Class Reference

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. More...
 

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. More...
 
void encode_requires_write_set ()
 Encodes the empty write set used to check for side effects in requires. More...
 
void encode_ensures_write_set ()
 Encodes the empty write set used to check for side effects in ensures. More...
 
void encode_contract_write_set ()
 Encodes the write set of the contract being checked/replaced (populated by calling functions provided in contract_functions) More...
 
void encode_is_fresh_set ()
 Encodes the object set used to evaluate is fresh predicates,. More...
 
void encode_requires_clauses ()
 Encodes preconditions, instruments them to check for side effects. More...
 
void encode_ensures_clauses ()
 Encodes postconditions, instruments them to check for side effects. More...
 
void encode_function_call ()
 Encodes the function call section of the wrapper program. More...
 
void encode_checked_function_call ()
 Creates a checked function call to the wrapped function, passing it the contract-derived write set as parameter. More...
 
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. More...
 

Protected Attributes

const dfcc_contract_modet contract_mode
 
const symboltwrapper_symbol
 
const symboltwrapped_symbol
 
const dfcc_contract_functionstcontract_functions
 
const symboltcontract_symbol
 
const code_with_contract_typetcontract_code_type
 
const symbol_exprt caller_write_set
 
const source_locationt wrapper_sl
 Source location with wrapper function name as function name. More...
 
std::optional< symbol_exprtreturn_value_opt
 Symbol for the return value of the wrapped function. More...
 
const symbol_exprt contract_write_set
 Symbol for the write set object derived from the contract. More...
 
const symbol_exprt addr_of_contract_write_set
 Symbol for the pointer to the write set object derived from the contract. More...
 
const symbol_exprt requires_write_set
 Symbol for the write set used to check requires clauses for side effects. More...
 
const symbol_exprt addr_of_requires_write_set
 Symbol for the pointer to the write set used to check requires clauses. More...
 
const symbol_exprt ensures_write_set
 Symbol for the write set used to check ensures clauses for side effects. More...
 
const symbol_exprt addr_of_ensures_write_set
 Symbol for the pointer to the write set used to check ensures clauses. More...
 
const symbol_exprt is_fresh_set
 Symbol for the object set used to evaluate is_fresh predicates. More...
 
const symbol_exprt addr_of_is_fresh_set
 Symbol for the pointer to the is_fresh object set. More...
 
std::set< irep_idtfunction_pointer_contracts
 Set of required or ensured contracts for function pointers discovered when processing the contract of interest. More...
 
goto_modeltgoto_model
 
message_handlertmessage_handler
 
messaget log
 
dfcc_librarytlibrary
 
dfcc_instrumenttinstrument
 
dfcc_lift_memory_predicatestmemory_predicates
 
namespacet ns
 
goto_convertt converter
 
exprt::operandst contract_lambda_parameters
 Vector of arguments to use to instantiate the lambdas wrapping the contract clauses. More...
 
goto_programt preamble
 
goto_programt link_is_fresh
 
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:

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 95 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_modechecking or replacement mode for the contract
wrapper_symbolfunction symbol receiving the generated instructions
wrapped_symbolfunction symbol being checked or replaced
contract_functionscontains the contract expressions and the assigns/frees/havoc functions symbols derived from the contract
caller_write_set_symbolsymbol representing the write set passed to the wrapper function by its caller.
goto_modelthe goto model being transformed
message_handlerused for debug/warning/error messages
librarythe contracts instrumentation library
instrumentthe instrumenter class for goto functions/goto programs
memory_predicateshandler for user-defed memory predicates, used to adjust call parameters for user defined predicates used in requires and ensures clauses.

Definition at line 144 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 244 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 235 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 656 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)

Definition at line 414 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 588 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 331 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 648 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 692 of file dfcc_wrapper_program.cpp.

◆ encode_is_fresh_set()

void dfcc_wrapper_programt::encode_is_fresh_set ( )
protected

Encodes the object set used to evaluate is fresh predicates,.

  • Adds declaration of object set and pointer to set to preamble
  • Adds initialisation function call in preamble
  • Adds release function call in postamble

Definition at line 502 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 537 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 259 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 147 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 159 of file dfcc_wrapper_program.h.

◆ addr_of_is_fresh_set

const symbol_exprt dfcc_wrapper_programt::addr_of_is_fresh_set
protected

Symbol for the pointer to the is_fresh object set.

Definition at line 165 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 153 of file dfcc_wrapper_program.h.

◆ caller_write_set

const symbol_exprt dfcc_wrapper_programt::caller_write_set
protected

Definition at line 135 of file dfcc_wrapper_program.h.

◆ contract_code_type

const code_with_contract_typet& dfcc_wrapper_programt::contract_code_type
protected

Definition at line 134 of file dfcc_wrapper_program.h.

◆ contract_functions

const dfcc_contract_functionst& dfcc_wrapper_programt::contract_functions
protected

Definition at line 132 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 182 of file dfcc_wrapper_program.h.

◆ contract_mode

const dfcc_contract_modet dfcc_wrapper_programt::contract_mode
protected

Definition at line 129 of file dfcc_wrapper_program.h.

◆ contract_symbol

const symbolt& dfcc_wrapper_programt::contract_symbol
protected

Definition at line 133 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 144 of file dfcc_wrapper_program.h.

◆ converter

goto_convertt dfcc_wrapper_programt::converter
protected

Definition at line 178 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 156 of file dfcc_wrapper_program.h.

◆ function_call

goto_programt dfcc_wrapper_programt::function_call
protected

Definition at line 194 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 169 of file dfcc_wrapper_program.h.

◆ goto_model

goto_modelt& dfcc_wrapper_programt::goto_model
protected

Definition at line 171 of file dfcc_wrapper_program.h.

◆ history

goto_programt dfcc_wrapper_programt::history
protected

Definition at line 192 of file dfcc_wrapper_program.h.

◆ instrument

dfcc_instrumentt& dfcc_wrapper_programt::instrument
protected

Definition at line 175 of file dfcc_wrapper_program.h.

◆ is_fresh_set

const symbol_exprt dfcc_wrapper_programt::is_fresh_set
protected

Symbol for the object set used to evaluate is_fresh predicates.

Definition at line 162 of file dfcc_wrapper_program.h.

◆ library

dfcc_libraryt& dfcc_wrapper_programt::library
protected

Definition at line 174 of file dfcc_wrapper_program.h.

◆ link_allocated_caller

goto_programt dfcc_wrapper_programt::link_allocated_caller
protected

Definition at line 195 of file dfcc_wrapper_program.h.

◆ link_deallocated_contract

goto_programt dfcc_wrapper_programt::link_deallocated_contract
protected

Definition at line 196 of file dfcc_wrapper_program.h.

◆ link_is_fresh

goto_programt dfcc_wrapper_programt::link_is_fresh
protected

Definition at line 190 of file dfcc_wrapper_program.h.

◆ log

messaget dfcc_wrapper_programt::log
protected

Definition at line 173 of file dfcc_wrapper_program.h.

◆ memory_predicates

dfcc_lift_memory_predicatest& dfcc_wrapper_programt::memory_predicates
protected

Definition at line 176 of file dfcc_wrapper_program.h.

◆ message_handler

message_handlert& dfcc_wrapper_programt::message_handler
protected

Definition at line 172 of file dfcc_wrapper_program.h.

◆ ns

namespacet dfcc_wrapper_programt::ns
protected

Definition at line 177 of file dfcc_wrapper_program.h.

◆ postamble

goto_programt dfcc_wrapper_programt::postamble
protected

Definition at line 198 of file dfcc_wrapper_program.h.

◆ postconditions

goto_programt dfcc_wrapper_programt::postconditions
protected

Definition at line 197 of file dfcc_wrapper_program.h.

◆ preamble

goto_programt dfcc_wrapper_programt::preamble
protected

Definition at line 189 of file dfcc_wrapper_program.h.

◆ preconditions

goto_programt dfcc_wrapper_programt::preconditions
protected

Definition at line 191 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 150 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 141 of file dfcc_wrapper_program.h.

◆ wrapped_symbol

const symbolt& dfcc_wrapper_programt::wrapped_symbol
protected

Definition at line 131 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 138 of file dfcc_wrapper_program.h.

◆ wrapper_symbol

const symbolt& dfcc_wrapper_programt::wrapper_symbol
protected

Definition at line 130 of file dfcc_wrapper_program.h.

◆ write_set_checks

goto_programt dfcc_wrapper_programt::write_set_checks
protected

Definition at line 193 of file dfcc_wrapper_program.h.


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