#include <contracts.h>

Collaboration diagram for code_contractst:

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

void	check_all_functions_found (const std::set< std::string > &functions) const
	Throws an exception if some function `functions` is found in the program. More...

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

void	enforce_contracts (const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={})
	Turn requires & ensures into assumptions and assertions for each of the named functions. More...

void	apply_loop_contracts (const std::set< std::string > &to_exclude_from_nondet_init={})
	Applies loop contract transformations. More...

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, goto_programt::targett loop_end, const loopt &loop, exprt assigns_clause, exprt invariant, exprt decreases_clause, const irep_idt &mode)

symbol_tablet &	get_symbol_table ()

goto_functionst &	get_goto_functions ()

void	assert_function_pointer_obeys_contract (const function_pointer_obeys_contract_exprt &expr, const irep_idt &property_class, const irep_idt &mode, goto_programt &dest)
	Translates a function_pointer_obeys_contract_exprt into an assertion. More...

void	assume_function_pointer_obeys_contract (const function_pointer_obeys_contract_exprt &expr, const irep_idt &mode, goto_programt &dest)
	Translates a function_pointer_obeys_contract_exprt into an assignment. More...

void	enforce_contract (const irep_idt &function)
	Enforce contract of a single function. More...

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

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

void	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. More...

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

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

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

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

Public Attributes
namespacet	ns

Protected Attributes
goto_modelt &	goto_model

symbol_tablet &	symbol_table

goto_functionst &	goto_functions

messaget &	log

goto_convertt	converter

std::unordered_set< irep_idt >	summarized

Detailed Description

Definition at line 55 of file contracts.h.

Constructor & Destructor Documentation

◆ code_contractst()

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

inline

Definition at line 58 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
	)

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

Definition at line 1369 of file contracts.cpp.

◆ add_quantified_variable()

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

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

When a quantified expression is found, a fresh quantified variable is added to the symbol table and expression is updated to use this fresh variable.

Definition at line 489 of file contracts.cpp.

◆ apply_function_contract()

void code_contractst::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.

Definition at line 680 of file contracts.cpp.

◆ apply_loop_contract()

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

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

Loop invariants, loop variants, and loop assigns clauses.

Definition at line 929 of file contracts.cpp.

◆ apply_loop_contracts()

void code_contractst::apply_loop_contracts ( const std::set< std::string > & to_exclude_from_nondet_init = {} )

Applies loop contract transformations.

Static variables of the model are nondet-initialized, except for the ones specified in to_exclude_from_nondet_init.

Definition at line 1607 of file contracts.cpp.

◆ assert_function_pointer_obeys_contract()

void code_contractst::assert_function_pointer_obeys_contract	(	const function_pointer_obeys_contract_exprt &	expr,
		const irep_idt &	property_class,
		const irep_idt &	mode,
		goto_programt &	dest
	)

Translates a function_pointer_obeys_contract_exprt into an assertion.

ASSERT function_pointer == contract;

Parameters

expr	expression to translate
property_class	property class to use for the generated assertions
mode	language mode to use for goto_conversion and prints
dest	goto_program where generated instructions are appended

Definition at line 1331 of file contracts.cpp.

◆ assume_function_pointer_obeys_contract()

void code_contractst::assume_function_pointer_obeys_contract	(	const function_pointer_obeys_contract_exprt &	expr,
		const irep_idt &	mode,
		goto_programt &	dest
	)

Translates a function_pointer_obeys_contract_exprt into an assignment.

ASSIGN function_pointer = contract;

Parameters

expr	expression to translate
mode	language mode to use for goto_conversion and prints
dest	goto_program where generated instructions are appended

Definition at line 1353 of file contracts.cpp.

◆ check_all_functions_found()

void code_contractst::check_all_functions_found ( const std::set< std::string > & functions ) const

Throws an exception if some function functions is found in the program.

Definition at line 1552 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,
		goto_programt::targett	loop_end,
		const loopt &	loop,
		exprt	assigns_clause,
		exprt	invariant,
		exprt	decreases_clause,
		const irep_idt &	mode
	)

Definition at line 51 of file contracts.cpp.

◆ check_frame_conditions_function()

void code_contractst::check_frame_conditions_function ( const irep_idt & function )

Instrument functions to check frame conditions.

Definition at line 1186 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
	)

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 635 of file contracts.cpp.

◆ enforce_contract()

void code_contractst::enforce_contract ( const irep_idt & function )

Enforce contract of a single function.

Definition at line 1277 of file contracts.cpp.

◆ enforce_contracts()

void code_contractst::enforce_contracts	(	const std::set< std::string > &	to_enforce,
		const std::set< std::string > &	to_exclude_from_nondet_init = `{}`
	)

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

Throws an exception if some to_enforce functions are not found.

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.

Static variables of the model are nondet-initialized, except for the ones specified in to_exclude_from_nondet_init.

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.

Definition at line 1619 of file contracts.cpp.

◆ get_goto_functions()

goto_functionst & code_contractst::get_goto_functions ( )

Definition at line 1181 of file contracts.cpp.

◆ get_symbol_table()

symbol_tablet & code_contractst::get_symbol_table ( )

Definition at line 1176 of file contracts.cpp.

◆ replace_calls()

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

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

Throws an exception if some to_replace functions are not found.

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.

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
	)

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

Definition at line 560 of file contracts.cpp.

Member Data Documentation

◆ converter

goto_convertt code_contractst::converter

protected

Definition at line 140 of file contracts.h.

◆ goto_functions

goto_functionst& code_contractst::goto_functions

protected

Definition at line 137 of file contracts.h.

◆ goto_model

goto_modelt& code_contractst::goto_model

protected

Definition at line 135 of file contracts.h.

◆ log

messaget& code_contractst::log

protected

Definition at line 139 of file contracts.h.

◆ ns

namespacet code_contractst::ns

Definition at line 132 of file contracts.h.

◆ summarized

std::unordered_set<irep_idt> code_contractst::summarized

protected

Definition at line 142 of file contracts.h.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table

protected

Definition at line 136 of file contracts.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/contracts/contracts.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/contracts/contracts.cpp

Public Member Functions

Public Attributes

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ code_contractst()

Member Function Documentation

◆ add_contract_check()

◆ add_quantified_variable()

◆ apply_function_contract()

◆ apply_loop_contract()

◆ apply_loop_contracts()

◆ assert_function_pointer_obeys_contract()

◆ assume_function_pointer_obeys_contract()

◆ check_all_functions_found()

◆ check_apply_loop_contracts()

◆ check_frame_conditions_function()

◆ create_ensures_instruction()

◆ enforce_contract()

◆ enforce_contracts()

◆ get_goto_functions()

◆ get_symbol_table()

◆ replace_calls()

◆ replace_history_parameter()

Member Data Documentation

◆ converter

◆ goto_functions

◆ goto_model

◆ log

◆ ns

◆ summarized

◆ symbol_table