Entry point into the contracts transformation. More...

#include <dfcc.h>

Collaboration diagram for dfcct:

Public Member Functions
	dfcct (const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< std::pair< irep_idt, irep_idt >> &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const dfcc_loop_contract_modet loop_contract_mode, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static)
	Class constructor. More...

void	transform_goto_model ()
	Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame condition checking approach. More...

Protected Member Functions
void	check_transform_goto_model_preconditions ()
	Checks preconditions on arguments of transform_goto_model. More...

void	partition_function_symbols (std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols)
	Partitions the function symbols of the symbol table into pure contracts and other function symbols symbols. More...

void	link_model_and_load_dfcc_library ()

void	instrument_harness_function ()

void	lift_memory_predicates ()

void	wrap_checked_function ()

void	wrap_replaced_functions ()

void	wrap_discovered_function_pointer_contracts ()

void	instrument_other_functions ()

void	reinitialize_model ()
	Re-initialise the GOTO model. More...

Protected Attributes
const optionst &	options

goto_modelt &	goto_model

const irep_idt &	harness_id

const std::optional< std::pair< irep_idt, irep_idt > > &	to_check

const bool	allow_recursive_calls

const std::map< irep_idt, irep_idt > &	to_replace

const dfcc_loop_contract_modet	loop_contract_mode

const std::set< std::string > &	to_exclude_from_nondet_static

message_handlert &	message_handler

messaget	log

dfcc_libraryt	library

namespacet	ns

dfcc_spec_functionst	spec_functions

dfcc_contract_clauses_codegent	contract_clauses_codegen

dfcc_instrumentt	instrument

dfcc_lift_memory_predicatest	memory_predicates

dfcc_contract_handlert	contract_handler

dfcc_swap_and_wrapt	swap_and_wrap

std::size_t	max_assigns_clause_size
	Tracks the maximum number of targets in any assigns clause handled in the transformation (used to specialize/unwind loops in DFCC library functions) More...

std::set< irep_idt >	pure_contract_symbols

std::set< irep_idt >	other_symbols

std::set< irep_idt >	function_pointer_contracts

Detailed Description

Entry point into the contracts transformation.

Definition at line 152 of file dfcc.h.

Constructor & Destructor Documentation

◆ dfcct()

dfcct::dfcct	(	const optionst &	options,
		goto_modelt &	goto_model,
		const irep_idt &	harness_id,
		const std::optional< std::pair< irep_idt, irep_idt >> &	to_check,
		const bool	allow_recursive_calls,
		const std::map< irep_idt, irep_idt > &	to_replace,
		const dfcc_loop_contract_modet	loop_contract_mode,
		message_handlert &	message_handler,
		const std::set< std::string > &	to_exclude_from_nondet_static
	)

Class constructor.

Parameters

options	CLI options (used to lookup options for language config when re-defining the model's entry point)
goto_model	GOTO model to transform
harness_id	Proof harness name, must be the entry point of the model
to_check	(function,contract) pair for contract checking
allow_recursive_calls	Allow the checked function to be recursive
to_replace	functions-to-contract mapping for replacement
loop_contract_mode	mode to use for loop contracts
message_handler	used for debug/warning/error messages
to_exclude_from_nondet_static	set of symbols to exclude when

Definition at line 170 of file dfcc.cpp.

Member Function Documentation

◆ check_transform_goto_model_preconditions()

void dfcct::check_transform_goto_model_preconditions ( )

protected

Checks preconditions on arguments of transform_goto_model.

The preconditions are:

The harness function exists in the model and has a body,
The model's entry point is the harness function,
The harness function is distinct from any checked or replaced function,
The harness function is distinct from any contract,
All function to check exist and have a body available,
All function to replace exist (body is not necessary),
All contracts to check or replace exist as pure contract symbols,
The checked function cannot be also replaced,
compiler built-ins or __CPROVER_* functions cannot be checked against a contract (because they cannot be instrumented),
all symbols of to_exclude_from_nondet_static exist in the model.

Definition at line 221 of file dfcc.cpp.

◆ instrument_harness_function()

void dfcct::instrument_harness_function ( )

protected

Definition at line 334 of file dfcc.cpp.

◆ instrument_other_functions()

void dfcct::instrument_other_functions ( )

protected

Definition at line 475 of file dfcc.cpp.

◆ lift_memory_predicates()

void dfcct::lift_memory_predicates ( )

protected

Definition at line 347 of file dfcc.cpp.

◆ link_model_and_load_dfcc_library()

void dfcct::link_model_and_load_dfcc_library ( )

protected

Definition at line 312 of file dfcc.cpp.

◆ partition_function_symbols()

void dfcct::partition_function_symbols	(	std::set< irep_idt > &	pure_contract_symbols,
		std::set< irep_idt > &	other_symbols
	)

protected

Partitions the function symbols of the symbol table into pure contracts and other function symbols symbols.

Definition at line 285 of file dfcc.cpp.

◆ reinitialize_model()

void dfcct::reinitialize_model ( )

protected

Re-initialise the GOTO model.

The new entry point must be the proof harness function specified for instrumentation.

The "initialize" (aka INITIALIZE_FUNCTION) is the function that assigns initial values to all statics of the model;

The initialize function must do the following:

assign a nondet value to all statics of the user program
assign the specified initial value to all instrumentation statics
add an entry in the static unbounded map of instrumented functions for each instrumented function

A call to nondet_static will re-generate the initialize function with nondet values. The instrumentation statics will not get nondet initialised by virtue of being tagged with ID_C_no_nondet_initialization.

However, nondet_static expects instructions to be either function calls or assignments with a symbol_exprt LHS. Since entries for the instrumented function maps are not symbol_exprts but index_exprts they need to be moved to the harness function.

The "start" function (aka goto_functionst::entry_point()) is the function from which SymEx starts.

The start function must do the following:

call the initialize function,
generate nondet values for the arguments of the proof harness function
call the harness function with said nondet arguments

All of which can be done using a call to generate_ansi_c_start_function, assuming the initialize function is already available in the symbol table.

So we do the following:

regenerate the "initialize" function
call nondet_static
add extra instructions at the end of the harness function for the instrumented functions map
call generate_ansi_c_start_function Make all user-defined statics nondet. Other statics added by the instrumentation will be unaffected because they are tagged with ID_C_no_nondet_initialization when created Update statics and static function maps

Definition at line 550 of file dfcc.cpp.

◆ transform_goto_model()

void dfcct::transform_goto_model ( )

Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame condition checking approach.

Functions to check/replace are explicitly mapped to contracts. When checking function foo against contract bar, we require the actual contract symbol to exist as contract::bar in the symbol table.

Transformation steps:

check preconditions on existence and absence of clash between harness, functions and contract symbols parameters.
link the goto model to the standard library
instrument the harness function.
partition function symbols of the model into
- contract:: symbols
- assigns/frees clause specification functions (not instrumented)
- all other functions (instrumented)
swap-and-wrap/instrument functions to check with their contract
swap-and-wrap/instrument functions to replace with their contract
swap-and-wrap all discovered function pointer contracts with themselves (replacement mode)
instrument all remaining functions GOTO model
(this includes standard library functions).
specialise the instrumentation functions by unwinding loops they contain to the maximum size of any assigns clause involved in the model.

Definition at line 495 of file dfcc.cpp.

◆ wrap_checked_function()

void dfcct::wrap_checked_function ( )

protected

Definition at line 359 of file dfcc.cpp.

◆ wrap_discovered_function_pointer_contracts()

void dfcct::wrap_discovered_function_pointer_contracts ( )

protected

Definition at line 405 of file dfcc.cpp.

◆ wrap_replaced_functions()

void dfcct::wrap_replaced_functions ( )

protected

Definition at line 388 of file dfcc.cpp.

Member Data Documentation

◆ allow_recursive_calls

const bool dfcct::allow_recursive_calls

protected

Definition at line 208 of file dfcc.h.

◆ contract_clauses_codegen

dfcc_contract_clauses_codegent dfcct::contract_clauses_codegen

protected

Definition at line 220 of file dfcc.h.

◆ contract_handler

dfcc_contract_handlert dfcct::contract_handler

protected

Definition at line 223 of file dfcc.h.

◆ function_pointer_contracts

std::set<irep_idt> dfcct::function_pointer_contracts

protected

Definition at line 233 of file dfcc.h.

◆ goto_model

goto_modelt& dfcct::goto_model

protected

Definition at line 205 of file dfcc.h.

◆ harness_id

const irep_idt& dfcct::harness_id

protected

Definition at line 206 of file dfcc.h.

◆ instrument

dfcc_instrumentt dfcct::instrument

protected

Definition at line 221 of file dfcc.h.

◆ library

dfcc_libraryt dfcct::library

protected

Definition at line 217 of file dfcc.h.

◆ log

messaget dfcct::log

protected

Definition at line 213 of file dfcc.h.

◆ loop_contract_mode

const dfcc_loop_contract_modet dfcct::loop_contract_mode

protected

Definition at line 210 of file dfcc.h.

◆ max_assigns_clause_size

std::size_t dfcct::max_assigns_clause_size

protected

Tracks the maximum number of targets in any assigns clause handled in the transformation (used to specialize/unwind loops in DFCC library functions)

Definition at line 228 of file dfcc.h.

◆ memory_predicates

dfcc_lift_memory_predicatest dfcct::memory_predicates

protected

Definition at line 222 of file dfcc.h.

◆ message_handler

message_handlert& dfcct::message_handler

protected

Definition at line 212 of file dfcc.h.

◆ ns

namespacet dfcct::ns

protected

Definition at line 218 of file dfcc.h.

◆ options

const optionst& dfcct::options

protected

Definition at line 204 of file dfcc.h.

◆ other_symbols

std::set<irep_idt> dfcct::other_symbols

protected

Definition at line 232 of file dfcc.h.

◆ pure_contract_symbols

std::set<irep_idt> dfcct::pure_contract_symbols

protected

Definition at line 231 of file dfcc.h.

◆ spec_functions

dfcc_spec_functionst dfcct::spec_functions

protected

Definition at line 219 of file dfcc.h.

◆ swap_and_wrap

dfcc_swap_and_wrapt dfcct::swap_and_wrap

protected

Definition at line 224 of file dfcc.h.

◆ to_check

const std::optional<std::pair<irep_idt, irep_idt> >& dfcct::to_check

protected

Definition at line 207 of file dfcc.h.

◆ to_exclude_from_nondet_static

const std::set<std::string>& dfcct::to_exclude_from_nondet_static

protected

Definition at line 211 of file dfcc.h.

◆ to_replace

const std::map<irep_idt, irep_idt>& dfcct::to_replace

protected

Definition at line 209 of file dfcc.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcct()

Member Function Documentation

◆ check_transform_goto_model_preconditions()

◆ instrument_harness_function()

◆ instrument_other_functions()

◆ lift_memory_predicates()

◆ link_model_and_load_dfcc_library()

◆ partition_function_symbols()

◆ reinitialize_model()

◆ transform_goto_model()

◆ wrap_checked_function()

◆ wrap_discovered_function_pointer_contracts()

◆ wrap_replaced_functions()

Member Data Documentation

◆ allow_recursive_calls

◆ contract_clauses_codegen

◆ contract_handler

◆ function_pointer_contracts

◆ goto_model

◆ harness_id

◆ instrument

◆ library

◆ log

◆ loop_contract_mode

◆ max_assigns_clause_size

◆ memory_predicates

◆ message_handler

◆ ns

◆ options

◆ other_symbols

◆ pure_contract_symbols

◆ spec_functions

◆ swap_and_wrap

◆ to_check

◆ to_exclude_from_nondet_static

◆ to_replace