#include <contracts.h>

Collaboration diagram for code_contractst:

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

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)

std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash >	get_original_loop_number_map () const

std::unordered_set< goto_programt::const_targett, const_target_hash >	get_loop_havoc_set () const

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

Public Attributes
const namespacet	ns

Protected Attributes
goto_modelt &	goto_model

symbol_tablet &	symbol_table

goto_functionst &	goto_functions

messaget &	log

std::unordered_set< irep_idt >	summarized

std::list< std::string >	loop_names
	Name of loops we are going to unwind. More...

std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash >	original_loop_number_map
	Store the map from instrumented instructions for loop contracts to their original loop numbers. More...

std::unordered_set< goto_programt::const_targett, const_target_hash >	loop_havoc_set
	Loop havoc instructions instrumented during applying loop contracts. More...

loop_contract_configt	loop_contract_config

Detailed Description

Definition at line 62 of file contracts.h.

Constructor & Destructor Documentation

◆ code_contractst()

code_contractst::code_contractst	(	goto_modelt &	goto_model,
		messaget &	log,
		const loop_contract_configt &	loop_contract_config
	)

inline

Definition at line 65 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 1269 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 609 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 836 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 1482 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 1427 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 49 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 1122 of file contracts.cpp.

◆ enforce_contract()

void code_contractst::enforce_contract ( const irep_idt & function )

Enforce contract of a single function.

Definition at line 1213 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 1563 of file contracts.cpp.

◆ get_loop_havoc_set()

std::unordered_set<goto_programt::const_targett, const_target_hash> code_contractst::get_loop_havoc_set ( ) const

inline

Definition at line 145 of file contracts.h.

◆ get_original_loop_number_map()

std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash> code_contractst::get_original_loop_number_map ( ) const

inline

Definition at line 139 of file contracts.h.

◆ 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_contractst::enforce_contracts() on F and verify it using cbmc --function F.

Definition at line 1442 of file contracts.cpp.

Member Data Documentation

◆ goto_functions

goto_functionst& code_contractst::goto_functions

protected

Definition at line 155 of file contracts.h.

◆ goto_model

goto_modelt& code_contractst::goto_model

protected

Definition at line 153 of file contracts.h.

◆ log

messaget& code_contractst::log

protected

Definition at line 157 of file contracts.h.

◆ loop_contract_config

loop_contract_configt code_contractst::loop_contract_config

protected

Definition at line 176 of file contracts.h.

◆ loop_havoc_set

std::unordered_set<goto_programt::const_targett, const_target_hash> code_contractst::loop_havoc_set

protected

Loop havoc instructions instrumented during applying loop contracts.

Definition at line 173 of file contracts.h.

◆ loop_names

std::list<std::string> code_contractst::loop_names

protected

Name of loops we are going to unwind.

Definition at line 162 of file contracts.h.

◆ ns

const namespacet code_contractst::ns

Definition at line 150 of file contracts.h.

◆ original_loop_number_map

std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash> code_contractst::original_loop_number_map

protected

Store the map from instrumented instructions for loop contracts to their original loop numbers.

Following instrumented instructions are stored.

loop-havoc — begin of transformed loops
ASSIGN ENTERED_LOOP = TRUE — end of transformed loops

Definition at line 169 of file contracts.h.

◆ summarized

std::unordered_set<irep_idt> code_contractst::summarized

protected

Definition at line 159 of file contracts.h.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table

protected

Definition at line 154 of file contracts.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/contracts.h
/home/runner/work/cbmc/cbmc/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()

◆ apply_function_contract()

◆ apply_loop_contract()

◆ apply_loop_contracts()

◆ check_all_functions_found()

◆ check_apply_loop_contracts()

◆ check_frame_conditions_function()

◆ enforce_contract()

◆ enforce_contracts()

◆ get_loop_havoc_set()

◆ get_original_loop_number_map()

◆ replace_calls()

Member Data Documentation

◆ goto_functions

◆ goto_model

◆ log

◆ loop_contract_config

◆ loop_havoc_set

◆ loop_names

◆ ns

◆ original_loop_number_map

◆ summarized

◆ symbol_table