The shadow memory instrumentation performed during symbolic execution. More...

#include <shadow_memory.h>

Collaboration diagram for shadow_memoryt:

Public Member Functions
	shadow_memoryt (const std::function< void(goto_symex_statet &, const exprt &, const exprt &)> symex_assign, const namespacet &ns, message_handlert &message_handler)

void	symex_field_static_init (goto_symex_statet &state, const ssa_exprt &lhs)
	Initialize global-scope shadow memory for global/static variables.

void	symex_field_static_init_string_constant (goto_symex_statet &state, const ssa_exprt &expr, const exprt &rhs)
	Initialize global-scope shadow memory for string constants.

void	symex_field_local_init (goto_symex_statet &state, const ssa_exprt &expr)
	Initialize local-scope shadow memory for local variables and parameters.

void	symex_field_dynamic_init (goto_symex_statet &state, const exprt &expr, const side_effect_exprt &code)
	Initialize global-scope shadow memory for dynamically allocated memory.

void	symex_get_field (goto_symex_statet &state, const exprt &lhs, const exprt::operandst &arguments)
	Symbolically executes a __CPROVER_get_field call.

void	symex_set_field (goto_symex_statet &state, const exprt::operandst &arguments)
	Symbolically executes a __CPROVER_set_field call.

Static Public Member Functions
static shadow_memory_field_definitionst	gather_field_declarations (const abstract_goto_modelt &goto_model, message_handlert &message_handler)
	Gathers the available shadow memory field definitions (__CPROVER_field_decl calls) from the goto model.

Private Member Functions
void	initialize_shadow_memory (goto_symex_statet &state, exprt expr, const shadow_memory_field_definitionst::field_definitiont &fields)
	Allocates and initializes a shadow memory field for the given original memory.

const symbol_exprt &	add_field (goto_symex_statet &state, const exprt &expr, const irep_idt &field_name, const typet &field_type)
	Registers a shadow memory field for the given original memory.

Static Private Member Functions
static void	convert_field_declaration (const code_function_callt &code_function_call, shadow_memory_field_definitionst::field_definitiont &fields, bool is_global, message_handlert &message_handler)
	Converts a field declaration.

Private Attributes
const std::function< void(goto_symex_statet &, const exprt &, const exprt)>	symex_assign

const namespacet &	ns

messaget	log

Detailed Description

The shadow memory instrumentation performed during symbolic execution.

Definition at line 36 of file shadow_memory.h.

Constructor & Destructor Documentation

◆ shadow_memoryt()

shadow_memoryt::shadow_memoryt	(	const std::function< void(goto_symex_statet &, const exprt &, const exprt &)>	symex_assign,
		const namespacet &	ns,
		message_handlert &	message_handler )

inline

Definition at line 39 of file shadow_memory.h.

Member Function Documentation

◆ add_field()

const symbol_exprt & shadow_memoryt::add_field	(	goto_symex_statet &	state,
		const exprt &	expr,
		const irep_idt &	field_name,
		const typet &	field_type )

private

Registers a shadow memory field for the given original memory.

Parameters

state	The symex state
expr	The expression for which shadow memory should be allocated
field_name	The field name
field_type	The field type

Returns: The resulting shadow memory symbol expression

Definition at line 67 of file shadow_memory.cpp.

◆ convert_field_declaration()

void shadow_memoryt::convert_field_declaration	(	const code_function_callt &	code_function_call,
		shadow_memory_field_definitionst::field_definitiont &	fields,
		bool	is_global,
		message_handlert &	message_handler )

staticprivate

Converts a field declaration.

Parameters

code_function_call	The __CPROVER_field_decl_* call
fields	The field declaration to be extended
is_global	True if the declaration is global
message_handler	For logging

Definition at line 509 of file shadow_memory.cpp.

◆ gather_field_declarations()

shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations	(	const abstract_goto_modelt &	goto_model,
		message_handlert &	message_handler )

static

Gathers the available shadow memory field definitions (__CPROVER_field_decl calls) from the goto model.

Parameters

goto_model	The goto model
message_handler	For logging

Returns: The field definitions

Definition at line 461 of file shadow_memory.cpp.

◆ initialize_shadow_memory()

void shadow_memoryt::initialize_shadow_memory	(	goto_symex_statet &	state,
		exprt	expr,
		const shadow_memory_field_definitionst::field_definitiont &	fields )

private

Allocates and initializes a shadow memory field for the given original memory.

Parameters

state	The symex state
expr	The expression for which shadow memory should be allocated
fields	The field definition to be used

Definition at line 28 of file shadow_memory.cpp.

◆ symex_field_dynamic_init()

void shadow_memoryt::symex_field_dynamic_init	(	goto_symex_statet &	state,
		const exprt &	expr,
		const side_effect_exprt &	code )

Initialize global-scope shadow memory for dynamically allocated memory.

Parameters

state	The symex state
expr	The dynamic object symbol expression
code	The allocation side effect code

Definition at line 449 of file shadow_memory.cpp.

◆ symex_field_local_init()

void shadow_memoryt::symex_field_local_init	(	goto_symex_statet &	state,
		const ssa_exprt &	expr )

Initialize local-scope shadow memory for local variables and parameters.

Parameters

state	The symex state
expr	The declared symbol expression

Definition at line 406 of file shadow_memory.cpp.

◆ symex_field_static_init()

void shadow_memoryt::symex_field_static_init	(	goto_symex_statet &	state,
		const ssa_exprt &	lhs )

Initialize global-scope shadow memory for global/static variables.

Parameters

state	The symex state
lhs	The LHS expression of the initializer assignment

Definition at line 343 of file shadow_memory.cpp.

◆ symex_field_static_init_string_constant()

void shadow_memoryt::symex_field_static_init_string_constant	(	goto_symex_statet &	state,
		const ssa_exprt &	expr,
		const exprt &	rhs )

Initialize global-scope shadow memory for string constants.

Parameters

state	The symex state
expr	The defined symbol expression
rhs	The RHS expression of the initializer assignment

Definition at line 381 of file shadow_memory.cpp.

◆ symex_get_field()

void shadow_memoryt::symex_get_field	(	goto_symex_statet &	state,
		const exprt &	lhs,
		const exprt::operandst &	arguments )

Symbolically executes a __CPROVER_get_field call.

Parameters

state	The symex state
lhs	The LHS of the call
arguments	The call arguments

Definition at line 194 of file shadow_memory.cpp.

◆ symex_set_field()

void shadow_memoryt::symex_set_field	(	goto_symex_statet &	state,
		const exprt::operandst &	arguments )

Symbolically executes a __CPROVER_set_field call.

Parameters

state	The symex state
arguments	The call arguments

Definition at line 91 of file shadow_memory.cpp.

Member Data Documentation

◆ log

messaget shadow_memoryt::log

private

Definition at line 138 of file shadow_memory.h.

◆ ns

const namespacet& shadow_memoryt::ns

private

Definition at line 137 of file shadow_memory.h.

◆ symex_assign

const std::function<void(goto_symex_statet &, const exprt &, const exprt)> shadow_memoryt::symex_assign

private

Definition at line 136 of file shadow_memory.h.

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

goto-symex/shadow_memory.h
goto-symex/shadow_memory.cpp

Public Member Functions

Static Public Member Functions

Private Member Functions

Static Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ shadow_memoryt()

Member Function Documentation

◆ add_field()

◆ convert_field_declaration()

◆ gather_field_declarations()

◆ initialize_shadow_memory()

◆ symex_field_dynamic_init()

◆ symex_field_local_init()

◆ symex_field_static_init()

◆ symex_field_static_init_string_constant()

◆ symex_get_field()

◆ symex_set_field()

Member Data Documentation

◆ log

◆ ns

◆ symex_assign