This class rewrites GOTO functions that use the built-ins: More...

#include <dfcc_spec_functions.h>

Collaboration diagram for dfcc_spec_functionst:

Public Member Functions
	dfcc_spec_functionst (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)

void	generate_havoc_function (const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
	Generates the havoc function for a function contract.

void	generate_havoc_instructions (const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets)
	Translates `original_program` that specifies assignable targets into a program that havocs the targets.

void	to_spec_assigns_function (const irep_idt &function_id, std::size_t &nof_targets)
	Transforms (in place) a function.

void	to_spec_assigns_instructions (const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
	Rewrites in place `program` expressed in terms of built-ins specifying assignable targets declaratively using `__CPROVER_assignable`, `__CPROVER_object_whole`, `__CPROVER_object_from`, `__CPROVER_object_upto` into a program populating `write_set_to_fill`.

void	to_spec_frees_function (const irep_idt &function_id, std::size_t &nof_targets)
	Transforms (in place) a function.

void	to_spec_frees_instructions (const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
	Rewrites in place `program` expressed in terms of built-ins specifying freeable targets declaratively using `__CPROVER_freeable` into a program populating `write_set_to_fill`.

Protected Member Functions
const typet &	get_target_type (const exprt &expr)
	Extracts the type of an assigns clause target expression The expression must be of the form: `expr = cast(address_of(target), empty*)`

Protected Attributes
goto_modelt &	goto_model

message_handlert &	message_handler

messaget	log

dfcc_libraryt &	library

namespacet	ns

Detailed Description

This class rewrites GOTO functions that use the built-ins:

__CPROVER_assignable,
__CPROVER_object_whole,
__CRPOVER_object_from,
__CPROVER_object_upto,
__CPROVER_freeable into GOTO functions that populate a write set instance or havoc a write set by calling the library implementation of these built-ins.

Definition at line 56 of file dfcc_spec_functions.h.

Constructor & Destructor Documentation

◆ dfcc_spec_functionst()

dfcc_spec_functionst::dfcc_spec_functionst	(	goto_modelt &	goto_model,
		message_handlert &	message_handler,
		dfcc_libraryt &	library
	)

Definition at line 21 of file dfcc_spec_functions.cpp.

Member Function Documentation

◆ generate_havoc_function()

void dfcc_spec_functionst::generate_havoc_function	(	const irep_idt &	function_id,
		const irep_idt &	havoc_function_id,
		std::size_t &	nof_targets
	)

Generates the havoc function for a function contract.

Pointer-typed targets are turned into invalid pointers by the havoc.

From a function:

void function_id(params);

generates a new function:

void havoc_function_id(__CPROVER_assignable_set_ptr_t write_set_to_havoc);

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:562

Which havocs the targets specified by function_id, passed

Parameters

[in]	function_id	function to generate instructions from
[in]	havoc_function_id	write set variable to havoc
[out]	nof_targets	maximum number of targets to havoc

Definition at line 43 of file dfcc_spec_functions.cpp.

◆ generate_havoc_instructions()

void dfcc_spec_functionst::generate_havoc_instructions	(	const irep_idt &	function_id,
		const goto_programt &	original_program,
		const exprt &	write_set_to_havoc,
		dfcc_ptr_havoc_modet	ptr_havoc_mode,
		goto_programt &	havoc_program,
		std::size_t &	nof_targets
	)

Translates original_program that specifies assignable targets into a program that havocs the targets.

Precondition: The original_program must be already fully inlined, and the only function calls allowed are to the built-ins that specify assignable targets: __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto.

The original_program is assumed to encode an assigns clause using the built-ins __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto. The method traverses original_program and emits a sequence of GOTO instructions in havoc_program that encode the havocing of the target write set write_set_to_havoc.

Parameters

[in]	function_id	function id to use for prefixing fresh variables
[in]	original_program	program from which to derive the havoc program
[in]	write_set_to_havoc	write set symbol to havoc
[in]	ptr_havoc_mode	havocing mode for pointers
[out]	havoc_program	destination program for havoc instructions
[out]	nof_targets	max number of havoc targets discovered

Definition at line 144 of file dfcc_spec_functions.cpp.

◆ get_target_type()

const typet & dfcc_spec_functionst::get_target_type ( const exprt & expr )

protected

Extracts the type of an assigns clause target expression The expression must be of the form: expr = cast(address_of(target), empty*)

Definition at line 33 of file dfcc_spec_functions.cpp.

◆ to_spec_assigns_function()

void dfcc_spec_functionst::to_spec_assigns_function	(	const irep_idt &	function_id,
		std::size_t &	nof_targets
	)

Transforms (in place) a function.

void function_id(params);

into a function

void function_id(
  params,
  __CPROVER_assignable_set_t write_set_to_fill,
)

Where:

write_set_to_fill is the write set to populate.

Parameters

function_id	function to transform in place
nof_targets	receives the estimated size of the write set

Definition at line 278 of file dfcc_spec_functions.cpp.

◆ to_spec_assigns_instructions()

void dfcc_spec_functionst::to_spec_assigns_instructions	(	const exprt &	write_set_to_fill,
		const irep_idt &	language_mode,
		goto_programt &	program,
		std::size_t &	nof_targets
	)

Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively using __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto into a program populating write_set_to_fill.

It is the responsibility of the caller of this method to instrument the resulting program against another write set instance to check them for unwanted side effects.

Precondition: The program must be already fully inlined, and the only function calls allowed are to the built-ins that specify assignable targets: __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto.

Parameters

[in]	write_set_to_fill	write set to populate.
[in]	language_mode	used to format expressions.
[in,out]	program	function to transform in place
[out]	nof_targets	receives the estimated size of the write set

Definition at line 304 of file dfcc_spec_functions.cpp.

◆ to_spec_frees_function()

void dfcc_spec_functionst::to_spec_frees_function	(	const irep_idt &	function_id,
		std::size_t &	nof_targets
	)

Transforms (in place) a function.

void function_id(params);

into a function

void function_id(
  params,
  __CPROVER_assignable_set_t write_set_to_fill,
)

Where:

write_set_to_fill is the write set to populate.

The function must be fully inlined and loop free.

Parameters

function_id	function to transform in place
nof_targets	receives the estimated size of the write set

Definition at line 361 of file dfcc_spec_functions.cpp.

◆ to_spec_frees_instructions()

void dfcc_spec_functionst::to_spec_frees_instructions	(	const exprt &	write_set_to_fill,
		const irep_idt &	language_mode,
		goto_programt &	program,
		std::size_t &	nof_targets
	)

Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively using __CPROVER_freeable into a program populating write_set_to_fill.

It is the responsibility of the caller of this method to instrument the resulting program against another write set instance to check them for unwanted side effects.

Precondition: The program must be already fully inlined, and the only function calls allowed are to the built-ins that specify freeable targets: __CPROVER_freeable.

Parameters

[in]	write_set_to_fill	write set to populate.
[in]	language_mode	used to format expressions.
[in,out]	program	function to transform in place
[out]	nof_targets	receives the estimated size of the write set

Definition at line 387 of file dfcc_spec_functions.cpp.

Member Data Documentation

◆ goto_model

goto_modelt& dfcc_spec_functionst::goto_model

protected

Definition at line 218 of file dfcc_spec_functions.h.

◆ library

dfcc_libraryt& dfcc_spec_functionst::library

protected

Definition at line 221 of file dfcc_spec_functions.h.

◆ log

messaget dfcc_spec_functionst::log

protected

Definition at line 220 of file dfcc_spec_functions.h.

◆ message_handler

message_handlert& dfcc_spec_functionst::message_handler

protected

Definition at line 219 of file dfcc_spec_functions.h.

◆ ns

namespacet dfcc_spec_functionst::ns

protected

Definition at line 222 of file dfcc_spec_functions.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_spec_functionst()

Member Function Documentation

◆ generate_havoc_function()

◆ generate_havoc_instructions()

◆ get_target_type()

◆ to_spec_assigns_function()

◆ to_spec_assigns_instructions()

◆ to_spec_frees_function()

◆ to_spec_frees_instructions()

Member Data Documentation

◆ goto_model

◆ library

◆ log

◆ message_handler

◆ ns