Central data structure: state. More...

#include <goto_symex_state.h>

Inheritance diagram for goto_symex_statet:

Collaboration diagram for goto_symex_statet:

Classes
struct	threadt

Public Types
enum class	write_is_shared_resultt { NOT_SHARED , IN_ATOMIC_SECTION , SHARED }

typedef std::pair< unsigned, std::list< guardt > >	a_s_r_entryt

typedef std::list< guardt >	a_s_w_entryt

Public Member Functions
	goto_symex_statet (const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, bool should_simplify, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)

	~goto_symex_statet ()

	goto_symex_statet (const goto_symex_statet &other, symex_target_equationt *const target)
	Fake "copy constructor" that initializes the `symex_target` member. More...

template<levelt level = L2>
renamedt< exprt, level >	rename (exprt expr, const namespacet &ns)
	Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent version, which differs depending on which level you requested. More...

template<levelt level>
renamedt< ssa_exprt, level >	rename_ssa (ssa_exprt ssa, const namespacet &ns)
	Version of rename which is specialized for SSA exprt. More...

template<levelt level = L2>
void	rename (typet &type, const irep_idt &l1_identifier, const namespacet &ns)

exprt	l2_rename_rvalues (exprt lvalue, const namespacet &ns)

renamedt< ssa_exprt, L2 >	assignment (ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)

call_stackt &	call_stack ()

const call_stackt &	call_stack () const

ssa_exprt	add_object (const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
	Instantiate the object `expr`. More...

ssa_exprt	declare (ssa_exprt ssa, const namespacet &ns)
	Add `invalid` (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of symbols in fields of ssa are at 1, and rename ssa to level 2. More...

void	print_backtrace (std::ostream &) const
	Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread. More...

bool	l2_thread_read_encoding (ssa_exprt &expr, const namespacet &ns)
	thread encoding More...

bool	l2_thread_write_encoding (const ssa_exprt &expr, const namespacet &ns)
	thread encoding More...

write_is_shared_resultt	write_is_shared (const ssa_exprt &expr, const namespacet &ns) const

void	drop_existing_l1_name (const irep_idt &l1_identifier)
	Drops an L1 name from the local L2 map. More...

void	drop_l1_name (const irep_idt &l1_identifier)
	Drops an L1 name from the local L2 map. More...

std::function< std::size_t(const irep_idt &)>	get_l2_name_provider () const

Public Member Functions inherited from goto_statet
const symex_level2t &	get_level2 () const

void	output_propagation_map (std::ostream &)
	Print the constant propagation map in a human-friendly format. More...

	goto_statet ()=delete
	Constructors. More...

goto_statet &	operator= (const goto_statet &other)=delete

goto_statet &	operator= (goto_statet &&other)=default

	goto_statet (const goto_statet &other)=default

	goto_statet (goto_statet &&other)=default

	goto_statet (guard_managert &guard_manager)

void	apply_condition (const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
	Given a condition that must hold on this path, propagate as much knowledge as possible. More...

Static Public Member Functions
static irep_idt	guard_identifier ()

static bool	is_read_only_object (const exprt &lvalue)
	Returns true if `lvalue` is a read-only object, such as the null object. More...

Public Attributes
symex_targett::sourcet	source

symbol_tablet	symbol_table
	contains symbols that are minted during symbolic execution, such as dynamically created objects etc. More...

guard_managert &	guard_manager

symex_target_equationt *	symex_target

symex_level1t	level1

field_sensitivityt	field_sensitivity

shadow_memory_statet	shadow_memory

std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash >	read_in_atomic_section

std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash >	written_in_atomic_section

std::vector< threadt >	threads

std::stack< bool >	record_events

const incremental_dirtyt *	dirty = nullptr

goto_programt::const_targett	saved_target

bool	has_saved_jump_target
	This state is saved, with the PC pointing to the target of a GOTO. More...

bool	has_saved_next_instruction
	This state is saved, with the PC pointing to the next instruction of a GOTO. More...

bool	run_validation_checks
	Should the additional validation checks be run? More...

unsigned	total_vccs = 0

unsigned	remaining_vccs = 0

Public Attributes inherited from goto_statet
unsigned	depth = 0
	Distance from entry. More...

sharing_mapt< exprt, symbol_exprt, false, irep_hash >	dereference_cache
	This is used for eliminating repeated complicated dereferences. More...

value_sett	value_set
	Uses level 1 names, and is used to do dereferencing. More...

guardt	guard

bool	reachable
	Is this code reachable? If not we can take shortcuts such as not entering function calls, but we still conduct guard arithmetic as usual. More...

sharing_mapt< irep_idt, exprt >	propagation

unsigned	atomic_section_id = 0
	Threads. More...

Protected Types
typedef std::unordered_map< irep_idt, typet >	l1_typest

Protected Member Functions
template<levelt >
void	rename_address (exprt &expr, const namespacet &ns)

template<levelt level>
renamedt< ssa_exprt, level >	set_indices (ssa_exprt expr, const namespacet &ns)
	Update values up to `level`. More...

template<>
renamedt< ssa_exprt, L0 >	set_indices (ssa_exprt ssa_expr, const namespacet &ns)

template<>
renamedt< ssa_exprt, L1 >	set_indices (ssa_exprt ssa_expr, const namespacet &ns)

template<>
renamedt< ssa_exprt, L2 >	set_indices (ssa_exprt ssa_expr, const namespacet &ns)

Protected Attributes
l1_typest	l1_types

Protected Attributes inherited from goto_statet
symex_level2t	level2

Private Member Functions
	goto_symex_statet (const goto_symex_statet &other)=default
	Dangerous, do not use. More...

Private Attributes
std::function< std::size_t(const irep_idt &)>	fresh_l2_name_provider

Detailed Description

Central data structure: state.

The state is a persistent data structure that symex maintains as it executes. As we walk over each instruction, state will be updated reflecting their effects until a branch occurs (such as an if), where parts of the state will be copied into a goto_statet, stored in a map for later reference and then merged again (via merge_goto) once it reaches a control-flow graph convergence.

Definition at line 42 of file goto_symex_state.h.

Member Typedef Documentation

◆ a_s_r_entryt

typedef std::pair<unsigned, std::list<guardt> > goto_symex_statet::a_s_r_entryt

Definition at line 179 of file goto_symex_state.h.

◆ a_s_w_entryt

typedef std::list<guardt> goto_symex_statet::a_s_w_entryt

Definition at line 180 of file goto_symex_state.h.

◆ l1_typest

typedef std::unordered_map<irep_idt, typet> goto_symex_statet::l1_typest

protected

Definition at line 136 of file goto_symex_state.h.

Member Enumeration Documentation

◆ write_is_shared_resultt

enum goto_symex_statet::write_is_shared_resultt

strong

Enumerator
NOT_SHARED
IN_ATOMIC_SECTION
SHARED

Definition at line 201 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/3]

goto_symex_statet::goto_symex_statet	(	const symex_targett::sourcet &	_source,
		std::size_t	max_field_sensitive_array_size,
		bool	should_simplify,
		guard_managert &	manager,
		std::function< std::size_t(const irep_idt &)>	fresh_l2_name_provider
	)

Definition at line 31 of file goto_symex_state.cpp.

◆ ~goto_symex_statet()

goto_symex_statet::~goto_symex_statet ( )

default

◆ goto_symex_statet() [2/3]

goto_symex_statet::goto_symex_statet	(	const goto_symex_statet &	other,
		symex_target_equationt *const	target
	)

inlineexplicit

Fake "copy constructor" that initializes the symex_target member.

Definition at line 54 of file goto_symex_state.h.

◆ goto_symex_statet() [3/3]

goto_symex_statet::goto_symex_statet ( const goto_symex_statet & other )

privatedefault

Dangerous, do not use.

Copying a state S1 to S2 risks S2 pointing to a deallocated symex_target_equationt if S1 (and the symex_target_equationt that its symex_target member points to) go out of scope. If your class has a goto_symex_statet member and needs a copy constructor, copy instances of this class using the public two-argument copy constructor constructor to ensure that the copy points to an allocated symex_target_equationt. The two-argument copy constructor uses this private copy constructor as a delegate.

Member Function Documentation

◆ add_object()

ssa_exprt goto_symex_statet::add_object	(	const symbol_exprt &	expr,
		std::function< std::size_t(const irep_idt &)>	index_generator,
		const namespacet &	ns
	)

Instantiate the object expr.

An instance of an object is an L1-renamed SSA expression such that its L1-index has not previously been used.

Parameters

expr	Symbol to be instantiated
index_generator	A function to produce a new index for a given name
ns	A namespace

Returns: L1-renamed SSA expression

Definition at line 823 of file goto_symex_state.cpp.

◆ assignment()

renamedt< ssa_exprt, L2 > goto_symex_statet::assignment	(	ssa_exprt	lhs,
		const exprt &	rhs,
		const namespacet &	ns,
		bool	rhs_is_simplified,
		bool	record_value,
		bool	allow_pointer_unsoundness = `false`
	)

Returns: lhs renamed to level 2

Definition at line 73 of file goto_symex_state.cpp.

◆ call_stack() [1/2]

call_stackt& goto_symex_statet::call_stack ( )

inline

Definition at line 147 of file goto_symex_state.h.

◆ call_stack() [2/2]

const call_stackt& goto_symex_statet::call_stack ( ) const

inline

Definition at line 153 of file goto_symex_state.h.

◆ declare()

ssa_exprt goto_symex_statet::declare	(	ssa_exprt	ssa,
		const namespacet &	ns
	)

Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of symbols in fields of ssa are at 1, and rename ssa to level 2.

Returns: ssa renamed to level 2

Definition at line 848 of file goto_symex_state.cpp.

◆ drop_existing_l1_name()

void goto_symex_statet::drop_existing_l1_name ( const irep_idt & l1_identifier )

inline

Drops an L1 name from the local L2 map.

Definition at line 233 of file goto_symex_state.h.

◆ drop_l1_name()

void goto_symex_statet::drop_l1_name ( const irep_idt & l1_identifier )

inline

Drops an L1 name from the local L2 map.

Definition at line 239 of file goto_symex_state.h.

◆ get_l2_name_provider()

std::function<std::size_t(const irep_idt &)> goto_symex_statet::get_l2_name_provider ( ) const

inline

Definition at line 244 of file goto_symex_state.h.

◆ guard_identifier()

static irep_idt goto_symex_statet::guard_identifier ( )

inlinestatic

Definition at line 141 of file goto_symex_state.h.

◆ is_read_only_object()

static bool goto_symex_statet::is_read_only_object ( const exprt & lvalue )

inlinestatic

Returns true if lvalue is a read-only object, such as the null object.

Definition at line 250 of file goto_symex_state.h.

◆ l2_rename_rvalues()

exprt goto_symex_statet::l2_rename_rvalues	(	exprt	lvalue,
		const namespacet &	ns
	)

Definition at line 313 of file goto_symex_state.cpp.

◆ l2_thread_read_encoding()

bool goto_symex_statet::l2_thread_read_encoding	(	ssa_exprt &	expr,
		const namespacet &	ns
	)

thread encoding

Definition at line 384 of file goto_symex_state.cpp.

◆ l2_thread_write_encoding()

bool goto_symex_statet::l2_thread_write_encoding	(	const ssa_exprt &	expr,
		const namespacet &	ns
	)

thread encoding

Returns: true if expr is shared between threads

Definition at line 550 of file goto_symex_state.cpp.

◆ print_backtrace()

void goto_symex_statet::print_backtrace ( std::ostream & out ) const

Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread.

This is for use from the debugger or in debug code; please don't delete it just because it isn't called at present.

Parameters

out	stream to write to

Definition at line 802 of file goto_symex_state.cpp.

◆ rename() [1/2]

template<levelt level>

template renamedt< exprt, L1 > goto_symex_statet::rename< L1 >	(	exprt	expr,
		const namespacet &	ns
	)

Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent version, which differs depending on which level you requested.

Each level also updates its predecessors, so a L1 rename will update L1 and L0. A L2 will update L2, L1 and L0.

What happens at each level: L0. Applies a suffix giving the current thread number. (Excludes guards, dynamic objects and anything not considered thread-local) L1. Applies a suffix giving the current loop iteration or recursive function invocation. L2. Applies a suffix giving the generation of this variable.

Renaming will not increment any of these values, just update the expression with them. Levels matter when reading a variable, for example: reading the value of x really means reading the particular x symbol for this thread (L0 renaming, if applicable), the most recent instance of x (L1 renaming), and the most recent write to x (L2 renaming).

The above example after being renamed could look like this: 'x!0@0#42'. That states it's the 42nd generation of this variable, on the first thread, in the first frame.

A full explanation of SSA (which is why we do this renaming) is in the SSA section of background-concepts.md.

Definition at line 171 of file goto_symex_state.cpp.

◆ rename() [2/2]

template<levelt level>

void goto_symex_statet::rename	(	typet &	type,
		const irep_idt &	l1_identifier,
		const namespacet &	ns
	)

Definition at line 708 of file goto_symex_state.cpp.

◆ rename_address()

template<levelt level>

void goto_symex_statet::rename_address	(	exprt &	expr,
		const namespacet &	ns
	)

protected

Definition at line 579 of file goto_symex_state.cpp.

◆ rename_ssa()

template<levelt level>

template renamedt< ssa_exprt, L1 > goto_symex_statet::rename_ssa< L1 >	(	ssa_exprt	ssa,
		const namespacet &	ns
	)

Version of rename which is specialized for SSA exprt.

Ensure rename_ssa gets compiled for L0.

Implementation only exists for level L0 and L1.

Definition at line 152 of file goto_symex_state.cpp.

◆ set_indices() [1/4]

template<levelt level>

renamedt<ssa_exprt, level> goto_symex_statet::set_indices	(	ssa_exprt	expr,
		const namespacet &	ns
	)

protected

Update values up to level.

◆ set_indices() [2/4]

template<>

renamedt<ssa_exprt, L2> goto_symex_statet::set_indices	(	ssa_exprt	ssa_expr,
		const namespacet &	ns
	)

protected

Definition at line 49 of file goto_symex_state.cpp.

◆ set_indices() [3/4]

template<>

renamedt<ssa_exprt, L1> goto_symex_statet::set_indices	(	ssa_exprt	ssa_expr,
		const namespacet &	ns
	)

protected

Definition at line 49 of file goto_symex_state.cpp.

◆ set_indices() [4/4]

template<>

renamedt<ssa_exprt, L0> goto_symex_statet::set_indices	(	ssa_exprt	ssa_expr,
		const namespacet &	ns
	)

protected

Definition at line 49 of file goto_symex_state.cpp.

◆ write_is_shared()

goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared	(	const ssa_exprt &	expr,
		const namespacet &	ns
	)		const

Definition at line 522 of file goto_symex_state.cpp.

Member Data Documentation

◆ dirty

const incremental_dirtyt* goto_symex_statet::dirty = nullptr

Definition at line 215 of file goto_symex_state.h.

◆ field_sensitivity

field_sensitivityt goto_symex_statet::field_sensitivity

Definition at line 122 of file goto_symex_state.h.

◆ fresh_l2_name_provider

std::function<std::size_t(const irep_idt &)> goto_symex_statet::fresh_l2_name_provider

private

Definition at line 262 of file goto_symex_state.h.

◆ guard_manager

guard_managert& goto_symex_statet::guard_manager

Definition at line 70 of file goto_symex_state.h.

◆ has_saved_jump_target

bool goto_symex_statet::has_saved_jump_target

This state is saved, with the PC pointing to the target of a GOTO.

Definition at line 220 of file goto_symex_state.h.

◆ has_saved_next_instruction

bool goto_symex_statet::has_saved_next_instruction

This state is saved, with the PC pointing to the next instruction of a GOTO.

Definition at line 224 of file goto_symex_state.h.

◆ l1_types

l1_typest goto_symex_statet::l1_types

protected

Definition at line 137 of file goto_symex_state.h.

◆ level1

symex_level1t goto_symex_statet::level1

Definition at line 73 of file goto_symex_state.h.

◆ read_in_atomic_section

std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> goto_symex_statet::read_in_atomic_section

Definition at line 181 of file goto_symex_state.h.

◆ record_events

std::stack<bool> goto_symex_statet::record_events

Definition at line 213 of file goto_symex_state.h.

◆ remaining_vccs

unsigned goto_symex_statet::remaining_vccs = 0

Definition at line 230 of file goto_symex_state.h.

◆ run_validation_checks

bool goto_symex_statet::run_validation_checks

Should the additional validation checks be run?

Definition at line 227 of file goto_symex_state.h.

◆ saved_target

goto_programt::const_targett goto_symex_statet::saved_target

Definition at line 217 of file goto_symex_state.h.

◆ shadow_memory

shadow_memory_statet goto_symex_statet::shadow_memory

Definition at line 124 of file goto_symex_state.h.

◆ source

symex_targett::sourcet goto_symex_statet::source

Definition at line 62 of file goto_symex_state.h.

◆ symbol_table

symbol_tablet goto_symex_statet::symbol_table

contains symbols that are minted during symbolic execution, such as dynamically created objects etc.

The names in this table are needed for error traces even after symbolic execution has finished.

Definition at line 67 of file goto_symex_state.h.

◆ symex_target

symex_target_equationt* goto_symex_statet::symex_target

Definition at line 71 of file goto_symex_state.h.

◆ threads

std::vector<threadt> goto_symex_statet::threads

Definition at line 199 of file goto_symex_state.h.

◆ total_vccs

unsigned goto_symex_statet::total_vccs = 0

Definition at line 229 of file goto_symex_state.h.

◆ written_in_atomic_section

std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash> goto_symex_statet::written_in_atomic_section

Definition at line 183 of file goto_symex_state.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/goto_symex_state.h
/home/runner/work/cbmc/cbmc/src/goto-symex/goto_symex_state.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ a_s_r_entryt

◆ a_s_w_entryt

◆ l1_typest

Member Enumeration Documentation

◆ write_is_shared_resultt

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/3]

◆ ~goto_symex_statet()

◆ goto_symex_statet() [2/3]

◆ goto_symex_statet() [3/3]

Member Function Documentation

◆ add_object()

◆ assignment()

◆ call_stack() [1/2]

◆ call_stack() [2/2]

◆ declare()

◆ drop_existing_l1_name()

◆ drop_l1_name()

◆ get_l2_name_provider()

◆ guard_identifier()

◆ is_read_only_object()

◆ l2_rename_rvalues()

◆ l2_thread_read_encoding()

◆ l2_thread_write_encoding()

◆ print_backtrace()

◆ rename() [1/2]

◆ rename() [2/2]

◆ rename_address()

◆ rename_ssa()

◆ set_indices() [1/4]

◆ set_indices() [2/4]

◆ set_indices() [3/4]

◆ set_indices() [4/4]

◆ write_is_shared()

Member Data Documentation

◆ dirty

◆ field_sensitivity

◆ fresh_l2_name_provider

◆ guard_manager

◆ has_saved_jump_target

◆ has_saved_next_instruction

◆ l1_types

◆ level1

◆ read_in_atomic_section

◆ record_events

◆ remaining_vccs

◆ run_validation_checks

◆ saved_target

◆ shadow_memory

◆ source

◆ symbol_table

◆ symex_target

◆ threads

◆ total_vccs

◆ written_in_atomic_section