#include <dfcc_lift_memory_predicates.h>

Collaboration diagram for dfcc_lift_memory_predicatest:

Public Member Functions
	dfcc_lift_memory_predicatest (goto_modelt &goto_model, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler)
std::set< irep_idt >	lift_predicates (std::set< irep_idt > &discovered_function_pointer_contracts)
	Collects and lifts all user-defined memory predicates.
void	fix_calls (goto_programt &program)
	Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position.
void	fix_calls (goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction)
	Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position, between first_instruction (included) and last_instruction (excluded).

Protected Member Functions
bool	calls_memory_predicates (const goto_programt &goto_program, const std::set< irep_idt > &predicates)
	Returns true iff `goto_program` calls core memory predicates.
void	lift_predicate (const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
void	lift_parameters_and_update_body (const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
void	add_pointer_type (const irep_idt &function_id, const std::size_t parameter_rank, replace_symbolt &replace_lifted_param)
	adds a pointer_type to the parameter of a function
void	collect_parameters_to_lift (const irep_idt &function_id)
	Computes the subset of function parameters of function_id that are passed directly to core predicates and must be lifted.
bool	is_lifted_function (const irep_idt &function_id)
	True if a function at least had one of its parameters lifted.

Protected Attributes
goto_modelt &	goto_model
dfcc_libraryt &	library
dfcc_instrumentt &	instrument
messaget	log
std::map< irep_idt, std::set< std::size_t > >	lifted_parameters

Detailed Description

Definition at line 35 of file dfcc_lift_memory_predicates.h.

Constructor & Destructor Documentation

◆ dfcc_lift_memory_predicatest()

dfcc_lift_memory_predicatest::dfcc_lift_memory_predicatest	(	goto_modelt &	goto_model,
		dfcc_libraryt &	library,
		dfcc_instrumentt &	instrument,
		message_handlert &	message_handler )

Parameters

goto_model	The goto model to process
library	The contracts instrumentation library
instrument	The DFCC instrumenter object
message_handler	Used for messages

Definition at line 29 of file dfcc_lift_memory_predicates.cpp.

Member Function Documentation

◆ add_pointer_type()

void dfcc_lift_memory_predicatest::add_pointer_type	(	const irep_idt &	function_id,
		const std::size_t	parameter_rank,
		replace_symbolt &	replace_lifted_param )

protected

adds a pointer_type to the parameter of a function

Parameters

function_id	The function to update
parameter_rank	The parameter to update
replace_lifted_param	Symbol replacer (receives p ~> *p mappings) The parameter symbol gets updated in the symbol table and the function signature gets updated with the new type.

Definition at line 289 of file dfcc_lift_memory_predicates.cpp.

◆ calls_memory_predicates()

bool dfcc_lift_memory_predicatest::calls_memory_predicates	(	const goto_programt &	goto_program,
		const std::set< irep_idt > &	predicates )

protected

Returns true iff goto_program calls core memory predicates.

or one of the functions found in predicates .

Definition at line 57 of file dfcc_lift_memory_predicates.cpp.

◆ collect_parameters_to_lift()

void dfcc_lift_memory_predicatest::collect_parameters_to_lift ( const irep_idt & function_id )

protected

Computes the subset of function parameters of function_id that are passed directly to core predicates and must be lifted.

Definition at line 217 of file dfcc_lift_memory_predicates.cpp.

◆ fix_calls() [1/2]

void dfcc_lift_memory_predicatest::fix_calls ( goto_programt & program )

Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position.

Definition at line 407 of file dfcc_lift_memory_predicates.cpp.

◆ fix_calls() [2/2]

void dfcc_lift_memory_predicatest::fix_calls	(	goto_programt &	program,
		goto_programt::targett	first_instruction,
		const goto_programt::targett &	last_instruction )

Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position, between first_instruction (included) and last_instruction (excluded).

Definition at line 412 of file dfcc_lift_memory_predicates.cpp.

◆ is_lifted_function()

bool dfcc_lift_memory_predicatest::is_lifted_function ( const irep_idt & function_id )

protected

True if a function at least had one of its parameters lifted.

True if a function had at least one of its parameters lifted.

Definition at line 42 of file dfcc_lift_memory_predicates.cpp.

◆ lift_parameters_and_update_body()

void dfcc_lift_memory_predicatest::lift_parameters_and_update_body	(	const irep_idt &	function_id,
		std::set< irep_idt > &	discovered_function_pointer_contracts )

protected

Definition at line 330 of file dfcc_lift_memory_predicates.cpp.

◆ lift_predicate()

void dfcc_lift_memory_predicatest::lift_predicate	(	const irep_idt &	function_id,
		std::set< irep_idt > &	discovered_function_pointer_contracts )

protected

Definition at line 375 of file dfcc_lift_memory_predicates.cpp.

◆ lift_predicates()

std::set< irep_idt > dfcc_lift_memory_predicatest::lift_predicates ( std::set< irep_idt > & discovered_function_pointer_contracts )

Collects and lifts all user-defined memory predicates.

Parameters

[out] discovered_function_pointer_contracts Set of function pointer contracts discovered during instrumentation

Returns: The set of predicates that were lifted

Definition at line 81 of file dfcc_lift_memory_predicates.cpp.

Member Data Documentation

◆ goto_model

goto_modelt& dfcc_lift_memory_predicatest::goto_model

protected

Definition at line 68 of file dfcc_lift_memory_predicates.h.

◆ instrument

dfcc_instrumentt& dfcc_lift_memory_predicatest::instrument

protected

Definition at line 70 of file dfcc_lift_memory_predicates.h.

◆ library

dfcc_libraryt& dfcc_lift_memory_predicatest::library

protected

Definition at line 69 of file dfcc_lift_memory_predicates.h.

◆ lifted_parameters

std::map<irep_idt, std::set<std::size_t> > dfcc_lift_memory_predicatest::lifted_parameters

protected

Definition at line 73 of file dfcc_lift_memory_predicates.h.

◆ log

messaget dfcc_lift_memory_predicatest::log

protected

Definition at line 71 of file dfcc_lift_memory_predicates.h.

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

goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h
goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_lift_memory_predicatest()

Member Function Documentation

◆ add_pointer_type()

◆ calls_memory_predicates()

◆ collect_parameters_to_lift()

◆ fix_calls() [1/2]

◆ fix_calls() [2/2]

◆ is_lifted_function()

◆ lift_parameters_and_update_body()

◆ lift_predicate()

◆ lift_predicates()

Member Data Documentation

◆ goto_model

◆ instrument

◆ library

◆ lifted_parameters

◆ log