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

Protected Member Functions
const dfcc_contract_functionst &	get_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_modelt &	goto_model

message_handlert &	message_handler

messaget	log

dfcc_libraryt &	library

dfcc_instrumentt &	instrument

dfcc_lift_memory_predicatest &	memory_predicates

dfcc_spec_functionst &	spec_functions

dfcc_contract_clauses_codegent &	contract_clauses_codegen

namespacet	ns

Static Protected Attributes
static std::map< irep_idt, dfcc_contract_functionst >	contract_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_mode	checking or replacement mode
[in]	wrapper_id	name of function receiving the instructions
[in]	wrapped_id	name of function that is being checked/replaced
[in]	contract_id	name of the contract to check
[in]	wrapper_write_set_symbol	write_set parameter of the wrapper
[out]	dest	destination program where instructions are added (should eventually become the body of wrapper_id)
[out]	function_pointer_contracts	list 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_id	name of the function that carries the contract
contract_type	code_type of contract_id
pure_contract_id	name of the pure contract symbol for contract_id
pure_contract_type	code_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:

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

Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_contract_handlert()

Member Function Documentation

◆ add_contract_instructions()

◆ check_signature_compat()

◆ get_assigns_clause_size()

◆ get_contract_functions()

◆ get_pure_contract_symbol()

Member Data Documentation

◆ contract_cache

◆ contract_clauses_codegen

◆ goto_model

◆ instrument

◆ library

◆ log

◆ memory_predicates

◆ message_handler

◆ ns

◆ spec_functions