CBMC
dfcc_contract_handlert Class Reference

A contract is represented by a function declaration or definition with contract clauses attached to its signature: More...

#include <dfcc_contract_handler.h>

+ Collaboration diagram for dfcc_contract_handlert:

Public Member Functions

 dfcc_contract_handlert (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
 
void add_contract_instructions (const dfcc_contract_modet contract_mode, const irep_idt &wrapper_id, const irep_idt &wrapped_id, const irep_idt &contract_id, const symbolt &wrapper_write_set_symbol, goto_programt &dest, std::set< irep_idt > &function_pointer_contracts)
 Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the function receiving the instructions. More...
 
const std::size_t get_assigns_clause_size (const irep_idt &contract_id)
 Returns the size assigns clause of the given contract in number of targets. More...
 
const symboltget_pure_contract_symbol (const irep_idt &contract_id, const std::optional< irep_idt > function_id_opt={})
 Searches for a symbol named "contract::contract_id" in the symbol table. More...
 

Protected Member Functions

const dfcc_contract_functionstget_contract_functions (const irep_idt &contract_id)
 Returns the dfcc_contract_functionst object for the given contract from the cache, creates it if it does not exists. More...
 
void check_signature_compat (const irep_idt &contract_id, const code_typet &contract_type, const irep_idt &pure_contract_id, const code_typet &pure_contract_type)
 Throws an error if the type signatures are not compatible. More...
 

Protected Attributes

goto_modeltgoto_model
 
message_handlertmessage_handler
 
messaget log
 
dfcc_librarytlibrary
 
dfcc_instrumenttinstrument
 
dfcc_lift_memory_predicatestmemory_predicates
 
dfcc_spec_functionstspec_functions
 
dfcc_contract_clauses_codegentcontract_clauses_codegen
 
namespacet ns
 

Static Protected Attributes

static std::map< irep_idt, dfcc_contract_functionstcontract_cache
 

Detailed Description

A contract is represented by a function declaration or definition with contract clauses attached to its signature:

ret_t foo(foo_params)
__CPROVER_requires(R)
__CPROVER_assigns(A)
__CPROVER_frees(F)
__CPROVER_ensures(E)
{ foo_body; } [optional]

In the symbol table, this declaration creates two symbols:

  • ret_t foo(foo_params) which represents the function (with optional body)
  • ret_t contract::foo(foo_params) which represents the pure contract part and carries the contract clauses in its .type attribute.

This class allows, given a contract name foo, to lookup the symbol contract::foo and translate its assigns and frees clauses into GOTO functions that build dynamic frames at runtime (stored in an object of type dfcc_contract_functionst).

Translation results are cached so it is safe to call get_contract_functions several times.

This class also implements the dfcc_contract_handlert interface and allows to generate instructions modelling contract checking and contract replacement.

Definition at line 64 of file dfcc_contract_handler.h.

Constructor & Destructor Documentation

◆ dfcc_contract_handlert()

dfcc_contract_handlert::dfcc_contract_handlert ( goto_modelt goto_model,
message_handlert message_handler,
dfcc_libraryt library,
dfcc_instrumentt instrument,
dfcc_lift_memory_predicatest memory_predicates,
dfcc_spec_functionst spec_functions,
dfcc_contract_clauses_codegent contract_clauses_codegen 
)

Definition at line 38 of file dfcc_contract_handler.cpp.

Member Function Documentation

◆ add_contract_instructions()

void dfcc_contract_handlert::add_contract_instructions ( const dfcc_contract_modet  contract_mode,
const irep_idt wrapper_id,
const irep_idt wrapped_id,
const irep_idt contract_id,
const symbolt wrapper_write_set_symbol,
goto_programt dest,
std::set< irep_idt > &  function_pointer_contracts 
)

Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the function receiving the instructions.

Parameters
[in]contract_modechecking or replacement mode
[in]wrapper_idname of function receiving the instructions
[in]wrapped_idname of function that is being checked/replaced
[in]contract_idname of the contract to check
[in]wrapper_write_set_symbolwrite_set parameter of the wrapper
[out]destdestination program where instructions are added (should eventually become the body of wrapper_id)
[out]function_pointer_contractslist of contracts found in either pre or post conditions of the processed contract. These contracts need to be swapped_and_wrapped in replacement mode if they are not already.

Definition at line 88 of file dfcc_contract_handler.cpp.

◆ check_signature_compat()

void dfcc_contract_handlert::check_signature_compat ( const irep_idt contract_id,
const code_typet contract_type,
const irep_idt pure_contract_id,
const code_typet pure_contract_type 
)
protected

Throws an error if the type signatures are not compatible.

Parameters
contract_idname of the function that carries the contract
contract_typecode_type of contract_id
pure_contract_idname of the pure contract symbol for contract_id
pure_contract_typecode_type of pure_contract_id

Definition at line 171 of file dfcc_contract_handler.cpp.

◆ get_assigns_clause_size()

const std::size_t dfcc_contract_handlert::get_assigns_clause_size ( const irep_idt contract_id)

Returns the size assigns clause of the given contract in number of targets.

Definition at line 83 of file dfcc_contract_handler.cpp.

◆ get_contract_functions()

const dfcc_contract_functionst & dfcc_contract_handlert::get_contract_functions ( const irep_idt contract_id)
protected

Returns the dfcc_contract_functionst object for the given contract from the cache, creates it if it does not exists.

Definition at line 59 of file dfcc_contract_handler.cpp.

◆ get_pure_contract_symbol()

const symbolt & dfcc_contract_handlert::get_pure_contract_symbol ( const irep_idt contract_id,
const std::optional< irep_idt function_id_opt = {} 
)

Searches for a symbol named "contract::contract_id" in the symbol table.

If the "contract::contract_id" is found and function_id_opt is present, type signature compatibility is checked between the contract and the function, and an exception is thrown if they are incompatible. If the symbol was not found and function_id_opt was provided, the function is used as a template to derive a new default contract with empty requires, empty assigns, empty frees, empty ensures clauses. If the symbol was not found and function_id_opt was not provided, a PRECONDITION is triggered.

Definition at line 111 of file dfcc_contract_handler.cpp.

Member Data Documentation

◆ contract_cache

std::map< irep_idt, dfcc_contract_functionst > dfcc_contract_handlert::contract_cache
staticprotected

Definition at line 127 of file dfcc_contract_handler.h.

◆ contract_clauses_codegen

dfcc_contract_clauses_codegent& dfcc_contract_handlert::contract_clauses_codegen
protected

Definition at line 123 of file dfcc_contract_handler.h.

◆ goto_model

goto_modelt& dfcc_contract_handlert::goto_model
protected

Definition at line 116 of file dfcc_contract_handler.h.

◆ instrument

dfcc_instrumentt& dfcc_contract_handlert::instrument
protected

Definition at line 120 of file dfcc_contract_handler.h.

◆ library

dfcc_libraryt& dfcc_contract_handlert::library
protected

Definition at line 119 of file dfcc_contract_handler.h.

◆ log

messaget dfcc_contract_handlert::log
protected

Definition at line 118 of file dfcc_contract_handler.h.

◆ memory_predicates

dfcc_lift_memory_predicatest& dfcc_contract_handlert::memory_predicates
protected

Definition at line 121 of file dfcc_contract_handler.h.

◆ message_handler

message_handlert& dfcc_contract_handlert::message_handler
protected

Definition at line 117 of file dfcc_contract_handler.h.

◆ ns

namespacet dfcc_contract_handlert::ns
protected

Definition at line 124 of file dfcc_contract_handler.h.

◆ spec_functions

dfcc_spec_functionst& dfcc_contract_handlert::spec_functions
protected

Definition at line 122 of file dfcc_contract_handler.h.


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