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 loop_contract_configt loop_contract_config, 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 loop_contract_configt	loop_contract_config

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 115 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 loop_contract_configt	loop_contract_config,
		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_config	configuration for applying loop contracts
message_handler	used for debug/warning/error messages
to_exclude_from_nondet_static	set of symbols to exclude when

Definition at line 141 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 192 of file dfcc.cpp.

◆ instrument_harness_function()

void dfcct::instrument_harness_function ( )

protected

Definition at line 305 of file dfcc.cpp.

◆ instrument_other_functions()

void dfcct::instrument_other_functions ( )

protected

Definition at line 446 of file dfcc.cpp.

◆ lift_memory_predicates()

void dfcct::lift_memory_predicates ( )

protected

Definition at line 318 of file dfcc.cpp.

◆ link_model_and_load_dfcc_library()

void dfcct::link_model_and_load_dfcc_library ( )

protected

Definition at line 283 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 256 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 521 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 466 of file dfcc.cpp.

◆ wrap_checked_function()

void dfcct::wrap_checked_function ( )

protected

Definition at line 330 of file dfcc.cpp.

◆ wrap_discovered_function_pointer_contracts()

void dfcct::wrap_discovered_function_pointer_contracts ( )

protected

Definition at line 376 of file dfcc.cpp.

◆ wrap_replaced_functions()

void dfcct::wrap_replaced_functions ( )

protected

Definition at line 359 of file dfcc.cpp.

Member Data Documentation

◆ allow_recursive_calls

const bool dfcct::allow_recursive_calls

protected

Definition at line 171 of file dfcc.h.

◆ contract_clauses_codegen

dfcc_contract_clauses_codegent dfcct::contract_clauses_codegen

protected

Definition at line 183 of file dfcc.h.

◆ contract_handler

dfcc_contract_handlert dfcct::contract_handler

protected

Definition at line 186 of file dfcc.h.

◆ function_pointer_contracts

std::set<irep_idt> dfcct::function_pointer_contracts

protected

Definition at line 196 of file dfcc.h.

◆ goto_model

goto_modelt& dfcct::goto_model

protected

Definition at line 168 of file dfcc.h.

◆ harness_id

const irep_idt& dfcct::harness_id

protected

Definition at line 169 of file dfcc.h.

◆ instrument

dfcc_instrumentt dfcct::instrument

protected

Definition at line 184 of file dfcc.h.

◆ library

dfcc_libraryt dfcct::library

protected

Definition at line 180 of file dfcc.h.

◆ log

messaget dfcct::log

protected

Definition at line 176 of file dfcc.h.

◆ loop_contract_config

const loop_contract_configt dfcct::loop_contract_config

protected

Definition at line 173 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 191 of file dfcc.h.

◆ memory_predicates

dfcc_lift_memory_predicatest dfcct::memory_predicates

protected

Definition at line 185 of file dfcc.h.

◆ message_handler

message_handlert& dfcct::message_handler

protected

Definition at line 175 of file dfcc.h.

◆ ns

namespacet dfcct::ns

protected

Definition at line 181 of file dfcc.h.

◆ options

const optionst& dfcct::options

protected

Definition at line 167 of file dfcc.h.

◆ other_symbols

std::set<irep_idt> dfcct::other_symbols

protected

Definition at line 195 of file dfcc.h.

◆ pure_contract_symbols

std::set<irep_idt> dfcct::pure_contract_symbols

protected

Definition at line 194 of file dfcc.h.

◆ spec_functions

dfcc_spec_functionst dfcct::spec_functions

protected

Definition at line 182 of file dfcc.h.

◆ swap_and_wrap

dfcc_swap_and_wrapt dfcct::swap_and_wrap

protected

Definition at line 187 of file dfcc.h.

◆ to_check

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

protected

Definition at line 170 of file dfcc.h.

◆ to_exclude_from_nondet_static

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

protected

Definition at line 174 of file dfcc.h.

◆ to_replace

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

protected

Definition at line 172 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_config

◆ 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