Class for storing a particular threads state. More...

#include <goto_symex_state.h>

Classes
class	merge_statet
	Snapshot of the symbolic data needed to merge a deferred path. More...
class	framet
	Stack frame tracking class. More...

Public Types
typedef std::list< merge_statet >	merge_state_listt
typedef std::map< goto_programt::const_targett, merge_state_listt >	merge_state_mapt
typedef std::vector< framet >	call_stackt
typedef persistent_set< renaming::level2t::name_record, renaming::level2t::name_rec_hash >	variable_name_sett
typedef std::unordered_map< unsigned, BigInt >	loop_iterationst
	Record of how many loop unwinds we've performed.

Public Member Functions
	goto_symex_statet (renaming::level2t &l2, value_sett &vs, const namespacet &_ns, bool no_propagation)
	Default constructor.
	goto_symex_statet (const goto_symex_statet &state, renaming::level2t &l2, value_sett &vs)
	Copy constructor.
	goto_symex_statet (goto_symex_statet const &)=default
goto_symex_statet &	operator= (const goto_symex_statet &state)
void	current_name (expr2tc &symirep) const
	Perform both levels of renaming.
void	current_name (const renaming::level2t &plevel2, expr2tc &symirep) const
	Perform both levels of renaming.
void	current_name (const merge_statet &merge_state, expr2tc &symirep) const
	Perform both levels of renaming.
framet &	top ()
	Fetch topmost stack frame.
const framet &	top () const
BigInt	total_stack_size () const
	Storage, in bits, held by every activation record currently on the call stack.
framet &	new_frame (unsigned int thread_id)
	Push a new fresh stack frame on the stack.
void	pop_frame ()
	Clear topmost stackframe from the stack.
const framet &	previous_frame ()
	Return stack frame of previous function call.
void	initialize (const goto_programt::const_targett &start, const goto_programt::const_targett &end, const goto_programt *prog, unsigned int thread_id)
	Initialize state with a function call.
void	rename (expr2tc &expr)
	Perform both levels of renaming on an expression.
void	rename_type (expr2tc &expr)
void	rename_array_sizes (type2tc &type)
void	rename_address (expr2tc &expr)
	Perform renaming of contents of an address_of operation.
void	rename_address (expr2tc &expr, const std::set< irep_idt > &bound)
void	rename_quantified (expr2tc &expr, const std::set< irep_idt > &bound)
	Rename an expression occurring under quantifiers, stopping at L1 for the variables they bind so those stay free for the solver.
void	assignment (expr2tc &lhs, const expr2tc &rhs)
	Make an L2 and value set assignment.
expr2tc	shallow_array_update (const expr2tc &rhs, const expr2tc &l1_lhs) const
	`rhs` with the earlier writes under its top-level array with replaced by `l1_lhs`, when they all write that same object.
bool	constant_propagation (const expr2tc &expr) const
	Determine whether to constant propagate the value of an expression.
expr2tc	pin_symbolic_updates (const expr2tc &rhs, const expr2tc &l2_lhs) const
	Re-offer the with updates of `rhs` that constant_propagation refuses as reads of `l2_lhs`, the name the assignment has just defined, so a symbolic member write no longer drops the sibling members with it (#7597).
bool	constant_propagation_reference (const expr2tc &expr) const
	Decide whether to constant_propagate an address_of.
void	get_original_name (expr2tc &expr) const
	Fetch an original l0 identifer.
void	print_stack_trace (unsigned int indent, std::ostream &os) const
	Print stack trace of state to an output stream.
std::vector< stack_framet >	gen_stack_trace () const
	Generate a stack trace as a vector of stack_framet, one per function invocation on the current call stack.
void	fixup_renamed_type (expr2tc &expr, const type2tc &orig_type)
	Fixup types after renaming: we might rename a symbol that we believe to be a uint32_t ptr, to be what it points at, the address of a byte array.
void	advance_witness_position ()

Public Attributes
unsigned	num_instructions
	Number of instructions executed in this thread.
bool	thread_ended
	Flag indicating this thread has stopped executing.
guard2tc	guard
	Current state guard of this thread.
guard2tc	global_guard
	Guard of global context.
symex_targett::sourcet	source
	Current program location of this thread.
std::map< irep_idt, unsigned >	variable_instance_nums
	Counter for how many times a particular variable has been declared: becomes the l1 renaming number in renamed variables.
loop_iterationst	loop_iterations
std::map< irep_idt, BigInt >	function_unwind
	Record of how many times we've unwound function recursion.
bool	use_value_set
	Flag saying whether to maintain pointer value set tracking.
bool	no_propagation = false
	Flag saying constant propagation was disabled with –no-propagation.
renaming::level2t &	level2
	Reference to global l2 state.
value_sett &	value_set
	Reference to global pointer tracking state.
call_stackt	call_stack
	Stack of framet's recording current function call stack.
const namespacet &	ns
	Namespace to work with.
std::map< expr2tc, unsigned >	realloc_map
	Map of what pointer values have been realloc'd, and what their new realloc number is.
std::vector< std::vector< waypoint > >	witness_segs
	witness_segs[seg]: all actionable waypoints per segment
size_t	cur_seg
bool	witness_target_reached
	Set to true the first time the target assertion is allowed through.
std::unordered_map< irep_idt, bool >	cycle_branch_map
	Pre-built O(1) lookup for branching(cycle) waypoints.

Detailed Description

Class for storing a particular threads state.

This means storing information about its program counter, its call stack, the locality of all the variables in that stack, its execution guard, the number of jumps and states that are hanging around... the everything, really. Notably, we're storing all that stuff here, we're not mainpulating it. Instead, that all occurs in the goto_symext class.

Member Typedef Documentation

◆ call_stackt

typedef std::vector<framet> goto_symex_statet::call_stackt

◆ loop_iterationst

typedef std::unordered_map<unsigned, BigInt> goto_symex_statet::loop_iterationst

Record of how many loop unwinds we've performed.

For each target in the program that contains a loop, record how many times we've unwound round it.

◆ merge_state_listt

typedef std::list<merge_statet> goto_symex_statet::merge_state_listt

◆ merge_state_mapt

typedef std::map<goto_programt::const_targett, merge_state_listt> goto_symex_statet::merge_state_mapt

◆ variable_name_sett

typedef persistent_set< renaming::level2t::name_record, renaming::level2t::name_rec_hash> goto_symex_statet::variable_name_sett

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/3]

goto_symex_statet::goto_symex_statet	(	renaming::level2t &	l2,
		value_sett &	vs,
		const namespacet &	_ns,
		bool	no_propagation )

Default constructor.

Sets up blank contents for the call stack, a dummy guard, no data of interest. Takes references to pieces of global state, the l2 renaming and value set / pointer tracking situations.

Parameters

l2	Global L2 state reference.
vs	Global value set reference.
no_propagation	Value of –no-propagation, from the live optionst.

◆ goto_symex_statet() [2/3]

goto_symex_statet::goto_symex_statet	(	const goto_symex_statet &	state,
		renaming::level2t &	l2,
		value_sett &	vs )

Copy constructor.

Performs your normal copy constructor activity; however requires a new l2 state, because in the majority of circumstances where copy constructors are needed, it's because a higher up object is getting cloned and we need to change global state references.

Parameters

state	State to copy from
l2	New L2 state to refer to.
vs	New value set to refer to.

◆ goto_symex_statet() [3/3]

goto_symex_statet::goto_symex_statet ( goto_symex_statet const & )

default

Member Function Documentation

◆ advance_witness_position()

void goto_symex_statet::advance_witness_position ( )

◆ assignment()

void goto_symex_statet::assignment	(	expr2tc &	lhs,
		const expr2tc &	rhs )

Make an L2 and value set assignment.

Records an assignment with L2 renaming context and the value set pointer tracking state.

Parameters

lhs	Symbol being assigned to.
rhs	Value being assigned to symbol.

◆ constant_propagation()

bool goto_symex_statet::constant_propagation ( const expr2tc & expr ) const

Determine whether to constant propagate the value of an expression.

These obey a few efficiency rules regarding whether or not its efficient to fully constant propagate away things like "WITH" updates to structs. Generally any update of an integer that can be simplified, is.

Parameters

expr	Expression to decide whether to const propagate.

Returns: True if constant propagation should be enabled.

◆ constant_propagation_reference()

bool goto_symex_statet::constant_propagation_reference ( const expr2tc & expr ) const

Decide whether to constant_propagate an address_of.

See also: constant_propagation.

Parameters

expr	Expression to decide whether to const propagate.

Returns: True if constant propagation should be enabled.

◆ current_name() [1/3]

void goto_symex_statet::current_name	(	const merge_statet &	merge_state,
		expr2tc &	symirep ) const

inline

Perform both levels of renaming.

Parameters

merge_state	Deferred-path snapshot containing L2 state to rename with.
symirep	Symbol irep to rename

◆ current_name() [2/3]

void goto_symex_statet::current_name	(	const renaming::level2t &	plevel2,
		expr2tc &	symirep ) const

inline

Perform both levels of renaming.

Parameters

plevel2	L2 renaming context to rename with.
symirep	Symbol irep to rename

◆ current_name() [3/3]

void goto_symex_statet::current_name ( expr2tc & symirep ) const

inline

Perform both levels of renaming.

Parameters

symirep Symbol to perform renaming on.

◆ fixup_renamed_type()

void goto_symex_statet::fixup_renamed_type	(	expr2tc &	expr,
		const type2tc &	orig_type )

Fixup types after renaming: we might rename a symbol that we believe to be a uint32_t ptr, to be what it points at, the address of a byte array.

The renaming process changes the ptr type of the expression, making all subsequent pointer arithmetic croak.

This used to be just for pointers, but is now for everything in general, because a variety of code (01_cbmc_Pointer7 for example) is renaming symbols to differently sized constants, which leads to Problems.

Parameters

expr	The expression that's just been renamed
orig_type	The original type of the expression, before renaming.

◆ gen_stack_trace()

std::vector< stack_framet > goto_symex_statet::gen_stack_trace ( ) const

Generate a stack trace as a vector of stack_framet, one per function invocation on the current call stack.

Returns: Vector of stack frames.

◆ get_original_name()

void goto_symex_statet::get_original_name ( expr2tc & expr ) const

Fetch an original l0 identifer.

Revokes both levels of renaming on an identifer, leaves us with the original c-level identifier for a symbol. This method applies this to all contents of an expression.

Parameters

expr	The expression to un-rename in place.

◆ initialize()

void goto_symex_statet::initialize	(	const goto_programt::const_targett &	start,
		const goto_programt::const_targett &	end,
		const goto_programt *	prog,
		unsigned int	thread_id )

Initialize state with a function call.

Sets up a function call on the stack of the goto program passed in, between the two iterators passed in.

Parameters

start	GOTO instruction to start at.
end	GOTO instruction to end function at.
prog	Goto program we're operating over.
thread_id	Thread identifier of this state.

◆ new_frame()

framet & goto_symex_statet::new_frame ( unsigned int thread_id )

inline

Push a new fresh stack frame on the stack.

Parameters

thread_id Thread identifier of current state.

Returns: New stack frame.

◆ operator=()

goto_symex_statet & goto_symex_statet::operator= ( const goto_symex_statet & state )

◆ pin_symbolic_updates()

expr2tc goto_symex_statet::pin_symbolic_updates	(	const expr2tc &	rhs,
		const expr2tc &	l2_lhs ) const

Re-offer the with updates of rhs that constant_propagation refuses as reads of l2_lhs, the name the assignment has just defined, so a symbolic member write no longer drops the sibling members with it (#7597).

Returns: The propagatable rebuild, or nil when nothing was pinned or the rebuild is still refused.

◆ pop_frame()

void goto_symex_statet::pop_frame ( )

inline

Clear topmost stackframe from the stack.

◆ previous_frame()

const framet & goto_symex_statet::previous_frame ( )

inline

Return stack frame of previous function call.

◆ print_stack_trace()

void goto_symex_statet::print_stack_trace	(	unsigned int	indent,
		std::ostream &	os ) const

Print stack trace of state to an output stream.

Takes all the current function calls and produces an indented stack trace, written to the given stream.

Parameters

indent	Number of spaces to indent contents by.
os	Output stream to write to.

◆ rename()

void goto_symex_statet::rename ( expr2tc & expr )

Perform both levels of renaming on an expression.

Parameters

expr	Expression to rename contents of.

◆ rename_address() [1/2]

void goto_symex_statet::rename_address ( expr2tc & expr )

Perform renaming of contents of an address_of operation.

This requires different behavior, because what we really want is a pointer to a global variable or l1 variable on the stack, or a heap object. So, don't perform second level of renaming in this function.

Parameters

expr	Expression to rename contents of.

◆ rename_address() [2/2]

void goto_symex_statet::rename_address	(	expr2tc &	expr,
		const std::set< irep_idt > &	bound )

◆ rename_array_sizes()

void goto_symex_statet::rename_array_sizes ( type2tc & type )

◆ rename_quantified()

void goto_symex_statet::rename_quantified	(	expr2tc &	expr,
		const std::set< irep_idt > &	bound )

Rename an expression occurring under quantifiers, stopping at L1 for the variables they bind so those stay free for the solver.

Otherwise identical to rename().

Parameters

expr	Expression to rename contents of.
bound	Names bound by the enclosing quantifiers.

◆ rename_type()

void goto_symex_statet::rename_type ( expr2tc & expr )

◆ shallow_array_update()

expr2tc goto_symex_statet::shallow_array_update	(	const expr2tc &	rhs,
		const expr2tc &	l1_lhs ) const

rhs with the earlier writes under its top-level array with replaced by l1_lhs, when they all write that same object.

◆ top() [1/2]

framet & goto_symex_statet::top ( )

inline

Fetch topmost stack frame.

I.E., give us the stack frame of the function call currently being interpreted.

Returns: Currently executing stack frame.

◆ top() [2/2]

const framet & goto_symex_statet::top ( ) const

inline

◆ total_stack_size()

BigInt goto_symex_statet::total_stack_size ( ) const

Storage, in bits, held by every activation record currently on the call stack.

Summed on demand rather than kept as a running counter so that it cannot drift from the frames: pop_frame, thread spawn and state merging all copy or drop whole frames.

Member Data Documentation

◆ call_stack

call_stackt goto_symex_statet::call_stack

Stack of framet's recording current function call stack.

◆ cur_seg

size_t goto_symex_statet::cur_seg

◆ cycle_branch_map

std::unordered_map<irep_idt, bool> goto_symex_statet::cycle_branch_map

Pre-built O(1) lookup for branching(cycle) waypoints.

Maps line_id → direction_true (from wp.value == "true"). Populated at init time; queried on every forward-goto without touching cur_seg (cycle branching is a persistent constraint, not a one-shot).

◆ function_unwind

std::map<irep_idt, BigInt> goto_symex_statet::function_unwind

Record of how many times we've unwound function recursion.

◆ global_guard

guard2tc goto_symex_statet::global_guard

Guard of global context.

◆ guard

guard2tc goto_symex_statet::guard

Current state guard of this thread.

◆ level2

renaming::level2t& goto_symex_statet::level2

Reference to global l2 state.

◆ loop_iterations

loop_iterationst goto_symex_statet::loop_iterations

◆ no_propagation

bool goto_symex_statet::no_propagation = false

Flag saying constant propagation was disabled with –no-propagation.

Cached because constant_propagation() runs on every assignment and get_bool_option does a string-keyed map lookup.

◆ ns

const namespacet& goto_symex_statet::ns

Namespace to work with.

◆ num_instructions

unsigned goto_symex_statet::num_instructions

Number of instructions executed in this thread.

◆ realloc_map

std::map<expr2tc, unsigned> goto_symex_statet::realloc_map

Map of what pointer values have been realloc'd, and what their new realloc number is.

No need for special consideration when merging states at phi nodes: the renumbering update itself is guarded at the SMT layer.

◆ source

symex_targett::sourcet goto_symex_statet::source

Current program location of this thread.

◆ thread_ended

bool goto_symex_statet::thread_ended

Flag indicating this thread has stopped executing.

◆ use_value_set

bool goto_symex_statet::use_value_set

Flag saying whether to maintain pointer value set tracking.

◆ value_set

value_sett& goto_symex_statet::value_set

Reference to global pointer tracking state.

◆ variable_instance_nums

std::map<irep_idt, unsigned> goto_symex_statet::variable_instance_nums

Counter for how many times a particular variable has been declared: becomes the l1 renaming number in renamed variables.

Used to be a counter for each function invocation, but the existence of decl insns makes l1 re-naming out of step with function invocations.

◆ witness_segs

std::vector<std::vector<waypoint> > goto_symex_statet::witness_segs

witness_segs[seg]: all actionable waypoints per segment

◆ witness_target_reached

bool goto_symex_statet::witness_target_reached

Set to true the first time the target assertion is allowed through.

Subsequent assertions at the target line (from continuation calls after the witness call chain returns) are filtered to avoid false positives.

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

src/goto-symex/state/goto_symex_state.h
src/goto-symex/engine/symex_stack.cpp
src/goto-symex/state/goto_symex_state.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ call_stackt

◆ loop_iterationst

◆ merge_state_listt

◆ merge_state_mapt

◆ variable_name_sett

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/3]

◆ goto_symex_statet() [2/3]

◆ goto_symex_statet() [3/3]

Member Function Documentation

◆ advance_witness_position()

◆ assignment()

◆ constant_propagation()

◆ constant_propagation_reference()

◆ current_name() [1/3]

◆ current_name() [2/3]

◆ current_name() [3/3]

◆ fixup_renamed_type()

◆ gen_stack_trace()

◆ get_original_name()

◆ initialize()

◆ new_frame()

◆ operator=()

◆ pin_symbolic_updates()

◆ pop_frame()

◆ previous_frame()

◆ print_stack_trace()

◆ rename()

◆ rename_address() [1/2]

◆ rename_address() [2/2]

◆ rename_array_sizes()

◆ rename_quantified()

◆ rename_type()

◆ shallow_array_update()

◆ top() [1/2]

◆ top() [2/2]

◆ total_stack_size()

Member Data Documentation

◆ call_stack

◆ cur_seg

◆ cycle_branch_map

◆ function_unwind

◆ global_guard

◆ guard

◆ level2

◆ loop_iterations

◆ no_propagation

◆ ns

◆ num_instructions

◆ realloc_map

◆ source

◆ thread_ended

◆ use_value_set

◆ value_set

◆ variable_instance_nums

◆ witness_segs

◆ witness_target_reached