#include <contracts.h>

Collaboration diagram for code_contractst:

Public Types
enum class	skipt { DontSkip , Skip }
	Tells wether to skip or not skip an action. More...

Public Member Functions
	code_contractst (goto_modelt &goto_model, messaget &log)

bool	replace_calls (const std::set< std::string > &)
	Replace all calls to each function in the list with that function's contract.

bool	enforce_contracts (const std::set< std::string > &functions)
	Turn requires & ensures into assumptions and assertions for each of the named functions.

void	apply_loop_contracts ()

void	check_apply_loop_contracts (const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode)

symbol_tablet &	get_symbol_table ()

goto_functionst &	get_goto_functions ()

Public Attributes
namespacet	ns

Protected Member Functions
bool	enforce_contract (const irep_idt &function)
	Enforce contract of a single function.

bool	check_frame_conditions_function (const irep_idt &function)
	Instrument functions to check frame conditions.

void	check_frame_conditions (const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt)
	Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.

bool	check_for_looped_mallocs (const goto_programt &program)
	Check if there are any malloc statements which may be repeated because of a goto statement that jumps back.

void	instrument_assign_statement (goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
	Inserts an assertion into program immediately before the assignment instruction_it, to ensure that the left-hand-side of the assignment is "included" in the (conditional address ranges in the) write set.

void	instrument_call_statement (goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
	Inserts an assertion into program immediately before the function call at instruction_it, to ensure that all memory locations written to by the.

void	apply_loop_contract (const irep_idt &function, goto_functionst::goto_functiont &goto_function)
	Apply loop contracts, whenever available, to all loops in `function`.

bool	apply_function_contract (const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target)
	Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses.

void	add_contract_check (const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)
	Instruments `wrapper_function` adding assumptions based on requires clauses and assertions based on ensures clauses.

void	add_quantified_variable (const exprt &expression, replace_symbolt &replace, const irep_idt &mode)
	This function recursively searches the expression to find nested or non-nested quantified expressions.

void	replace_history_parameter (exprt &expr, std::map< exprt, exprt > &parameter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)
	This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables.

std::pair< goto_programt, goto_programt >	create_ensures_instruction (codet &expression, source_locationt location, const irep_idt &mode)
	This function creates and returns an instruction that corresponds to the ensures clause.

Protected Attributes
symbol_tablet &	symbol_table

goto_functionst &	goto_functions

messaget &	log

goto_convertt	converter

std::unordered_set< irep_idt >	summarized

Detailed Description

Definition at line 53 of file contracts.h.

Member Enumeration Documentation

◆ skipt

enum class code_contractst::skipt

strong

Tells wether to skip or not skip an action.

Enumerator
DontSkip
Skip

Definition at line 115 of file contracts.h.

Constructor & Destructor Documentation

◆ code_contractst()

code_contractst::code_contractst	(	goto_modelt &	goto_model,
		messaget &	log
	)

inline

Definition at line 56 of file contracts.h.

Member Function Documentation

◆ add_contract_check()

void code_contractst::add_contract_check	(	const irep_idt &	wrapper_function,
		const irep_idt &	mangled_function,
		goto_programt &	dest
	)

protected

Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ensures clauses.

Definition at line 1414 of file contracts.cpp.

◆ add_quantified_variable()

void code_contractst::add_quantified_variable	(	const exprt &	expression,
		replace_symbolt &	replace,
		const irep_idt &	mode
	)

protected

This function recursively searches the expression to find nested or non-nested quantified expressions.

When a quantified expression is found, the quantified variable is added to the symbol table and to the expression map.

Definition at line 499 of file contracts.cpp.

◆ apply_function_contract()

bool code_contractst::apply_function_contract	(	const irep_idt &	function,
		const source_locationt &	location,
		goto_programt &	function_body,
		goto_programt::targett &	target
	)

protected

Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses.

Definition at line 661 of file contracts.cpp.

◆ apply_loop_contract()

void code_contractst::apply_loop_contract	(	const irep_idt &	function,
		goto_functionst::goto_functiont &	goto_function
	)

protected

Apply loop contracts, whenever available, to all loops in function.

Loop invariants, loop variants, and loop assigns clauses.

Definition at line 870 of file contracts.cpp.

◆ apply_loop_contracts()

void code_contractst::apply_loop_contracts ( )

Definition at line 1610 of file contracts.cpp.

◆ check_apply_loop_contracts()

void code_contractst::check_apply_loop_contracts	(	const irep_idt &	function_name,
		goto_functionst::goto_functiont &	goto_function,
		const local_may_aliast &	local_may_alias,
		goto_programt::targett	loop_head,
		const loopt &	loop,
		const irep_idt &	mode
	)

Definition at line 138 of file contracts.cpp.

◆ check_for_looped_mallocs()

bool code_contractst::check_for_looped_mallocs ( const goto_programt & program )

protected

Check if there are any malloc statements which may be repeated because of a goto statement that jumps back.

Definition at line 1025 of file contracts.cpp.

◆ check_frame_conditions()

void code_contractst::check_frame_conditions	(	const irep_idt &	function,
		goto_programt &	body,
		goto_programt::targett	instruction_it,
		const goto_programt::targett &	instruction_end,
		instrument_spec_assignst &	instrument_spec_assigns,
		skipt	skip_parameter_assigns,
		optionalt< cfg_infot > &	cfg_info_opt
	)

protected

Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.

Parameters

function	Name of the function getting instrumented.
body	Body of the function getting instrumented.
instruction_it	Iterator to the instruction from which to start instrumentation (inclusive).
instruction_end	Iterator to the instruction at which to stop instrumentation (exclusive).
instrument_spec_assigns	Assigns clause instrumenter of the function
skip_parameter_assigns	If true, will cause assignments to symbol marked as is_parameter to not be instrumented.
cfg_info_opt	Control flow graph information can will be used for write set optimisation if available.

Definition at line 1253 of file contracts.cpp.

◆ check_frame_conditions_function()

bool code_contractst::check_frame_conditions_function ( const irep_idt & function )

protected

Instrument functions to check frame conditions.

Definition at line 1088 of file contracts.cpp.

◆ create_ensures_instruction()

std::pair< goto_programt, goto_programt > code_contractst::create_ensures_instruction	(	codet &	expression,
		source_locationt	location,
		const irep_idt &	mode
	)

protected

This function creates and returns an instruction that corresponds to the ensures clause.

It also returns a list of instructions related to initializing history variables, if required.

Definition at line 639 of file contracts.cpp.

◆ enforce_contract()

bool code_contractst::enforce_contract ( const irep_idt & function )

protected

Enforce contract of a single function.

Definition at line 1351 of file contracts.cpp.

◆ enforce_contracts()

bool code_contractst::enforce_contracts ( const std::set< std::string > & functions )

Turn requires & ensures into assumptions and assertions for each of the named functions.

Use this function to prove the correctness of a function F independently of its calling context. If you have proved that F is correct, then you can soundly replace all calls to F with F's contract using the code_contractst::replace_calls() function; this means that symbolic execution does not need to explore F every time it is called, increasing scalability.

Implementation: mangle the name of each function F into a new name, __CPROVER_contracts_original_F (CF for short). Then mint a new function called F that assumes CF's requires clause, calls CF, and then asserts CF's ensures clause.

Returns: true on failure, false otherwise

Definition at line 1616 of file contracts.cpp.

◆ get_goto_functions()

goto_functionst & code_contractst::get_goto_functions ( )

Definition at line 958 of file contracts.cpp.

◆ get_symbol_table()

symbol_tablet & code_contractst::get_symbol_table ( )

Definition at line 953 of file contracts.cpp.

◆ instrument_assign_statement()

void code_contractst::instrument_assign_statement	(	goto_programt::targett &	instruction_it,
		goto_programt &	program,
		instrument_spec_assignst &	instrument_spec_assigns,
		optionalt< cfg_infot > &	cfg_info_opt
	)

protected

Inserts an assertion into program immediately before the assignment instruction_it, to ensure that the left-hand-side of the assignment is "included" in the (conditional address ranges in the) write set.

Definition at line 963 of file contracts.cpp.

◆ instrument_call_statement()

void code_contractst::instrument_call_statement	(	goto_programt::targett &	instruction_it,
		const irep_idt &	function,
		goto_programt &	body,
		instrument_spec_assignst &	instrument_spec_assigns,
		optionalt< cfg_infot > &	cfg_info_opt
	)

protected

Inserts an assertion into program immediately before the function call at instruction_it, to ensure that all memory locations written to by the.

Definition at line 977 of file contracts.cpp.

◆ replace_calls()

bool code_contractst::replace_calls ( const std::set< std::string > & to_replace )

Replace all calls to each function in the list with that function's contract.

Use this function when proving code that calls into an expensive function, F. You can write a contract for F using __CPROVER_requires and __CPROVER_ensures, and then use this function to replace all calls to F with an assertion that the requires clause holds followed by an assumption that the ensures clause holds. In order to ensure that F actually abides by its ensures and requires clauses, you should separately call code_constractst::enforce_contracts() on F and verify it using cbmc --function F.

Returns: true on failure, false otherwise

Definition at line 1567 of file contracts.cpp.

◆ replace_history_parameter()

void code_contractst::replace_history_parameter	(	exprt &	expr,
		std::map< exprt, exprt > &	parameter2history,
		source_locationt	location,
		const irep_idt &	mode,
		goto_programt &	history,
		const irep_idt &	id
	)

protected

This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables.

Definition at line 565 of file contracts.cpp.

Member Data Documentation

◆ converter

goto_convertt code_contractst::converter

protected

Definition at line 126 of file contracts.h.

◆ goto_functions

goto_functionst& code_contractst::goto_functions

protected

Definition at line 123 of file contracts.h.

◆ log

messaget& code_contractst::log

protected

Definition at line 125 of file contracts.h.

◆ ns

namespacet code_contractst::ns

Definition at line 112 of file contracts.h.

◆ summarized

std::unordered_set<irep_idt> code_contractst::summarized

protected

Definition at line 128 of file contracts.h.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table

protected

Definition at line 122 of file contracts.h.

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

goto-instrument/contracts/contracts.h
goto-instrument/contracts/contracts.cpp

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ skipt

Constructor & Destructor Documentation

◆ code_contractst()

Member Function Documentation

◆ add_contract_check()

◆ add_quantified_variable()

◆ apply_function_contract()

◆ apply_loop_contract()

◆ apply_loop_contracts()

◆ check_apply_loop_contracts()

◆ check_for_looped_mallocs()

◆ check_frame_conditions()

◆ check_frame_conditions_function()

◆ create_ensures_instruction()

◆ enforce_contract()

◆ enforce_contracts()

◆ get_goto_functions()

◆ get_symbol_table()

◆ instrument_assign_statement()

◆ instrument_call_statement()

◆ replace_calls()

◆ replace_history_parameter()

Member Data Documentation

◆ converter

◆ goto_functions

◆ log

◆ ns

◆ summarized

◆ symbol_table