Thread-aware symex state explored by reachability_treet. More...

#include <execution_state.h>

Inheritance diagram for execution_statet:

Classes
struct	parked_patht
	A path the transition parked for a deferred merge: the sibling arm of a branch, or the continuation a return parked at end_of_function. More...
struct	transition_resultt
class	ex_state_level2t
	execution_statet specific level2t. More...
class	state_hashing_level2t
	State-hashing level2t. More...
struct	transition_footprintt
	The objects one transition read and wrote, as MPOR records them. More...

Public Types
enum class	access_kindt { READ , WRITE }
	Kind of memory access, used by get_expr_globals to decide whether a read-only global can be filtered out of cswitch-triggering sets. More...
typedef goto_symex_statet::merge_statet	merge_statet
Public Types inherited from goto_symext
typedef goto_symex_statet	statet
using	conjunct_indext = persistent_map<expr2tc, size_t, irep2_hash>
	Rewritten conjunct -> position of the first conjunct rewriting to it.

Public Member Functions
	execution_statet (const goto_functionst &goto_functions, const namespacet &ns, reachability_treet *art, std::shared_ptr< symex_targett > _target, contextt &context, std::shared_ptr< ex_state_level2t > l2init, optionst &options)
	Default constructor.
	execution_statet (const execution_statet &ex)
	Default copy constructor.
execution_statet &	operator= (const execution_statet &ex)=delete
	Public assignment is deleted: a standalone a = b would not be correct here (it would leave the base goto_symext slice, threads_state, cur_state, and state_level2 as a's old objects).
virtual	~execution_statet ()=default
	Default destructor.
void	increment_context_switch ()
	Increase number of context switches this ex_state has taken.
int	get_context_switch () const
	Get the number of context switches performed by this ex_state.
unsigned int	get_active_state_number () const
	Fetch the thread ID of the current active thread.
void	set_thread_start_data (unsigned int tid, const expr2tc &argdata)
	Set internal thread startup data.
const expr2tc &	get_thread_start_data (unsigned int tid) const
	Fetch internal thread startup data.
virtual std::shared_ptr< execution_statet >	clone () const =0
	Duplicate this execution state.
void	symex_step (reachability_treet &art) override
	Make one symbolic execution step.
void	symex_end_function (reachability_treet &art, const goto_programt::instructiont &instruction)
void	symex_assign (const expr2tc &code, const bool hidden, const guard2tc &guard) override
	Symbolically assign a value.
void	claim (const expr2tc &expr, const std::string &msg) override
	Symbolically assert something.
void	symex_goto (const expr2tc &old_guard) override
	Perform a jump across GOTO code.
void	assume (const expr2tc &assumption) override
	Assume some expression is true.
void	defer_assumption (const expr2tc &assumption) override
	As assume(), the deferred assumption reads its condition now.
void	symex_printf (const expr2tc &lhs, expr2tc &code) override
	Implemented by goto_symext::symex_printf.
void	note_bounded_loop_truncation () override
	Under –no-unwinding-assertions a truncated loop is cut with an assumption, which drives the state guard false and so is indistinguishable at the scheduler from a genuinely infeasible path.
unsigned int &	get_dynamic_counter () override
	Fetch reference to count of dynamic objects in this state.
unsigned int &	get_nondet_counter () override
	Like get_dynamic_counter, but with nondet symbols.
expr2tc	get_guard_identifier ()
	Fetch name of current execution guard.
goto_symex_statet &	get_active_state ()
	Get reference to current thread state.
const goto_symex_statet &	get_active_state () const
unsigned int	get_active_atomic_number () const
	Get atomic number count for current thread state.
void	increment_active_atomic_number ()
	Increase current threads atomic number count.
void	decrement_active_atomic_number ()
	Decrease current threads atomic number count.
void	switch_to_thread (unsigned int i)
	Perform a context switch to thread ID i.
bool	is_cur_state_guard_false (const expr2tc &guard)
	Determines if current state guard is false.
void	execute_guard ()
	Generates execution guard that's true if this interleaving can be reached.
bool	check_if_ileaves_blocked ()
	Test to see if interleavings are blocked by the current state.
bool	all_threads_terminal () const
	True iff every thread in this schedule has reached a terminal state, i.e.
unsigned int	add_thread (const goto_programt *prog)
	Create a new thread.
void	end_thread ()
	Record a thread as ended.
void	update_after_switch_point ()
	Perform any necessary steps after a context switch point.
void	preserve_last_paths (const transition_resultt &transition)
void	cull_all_paths ()
void	restore_last_paths ()
void	record_parked_path (goto_programt::const_targett target, statet::merge_state_listt::iterator parked) override
	Hook called when a step parks a merge_statet snapshot for a deferred merge — a GOTO forking off its sibling arm, or a RETURN parking the continuation at end_of_function.
void	analyze_assign (const expr2tc &assign)
	Analyze the contents of an assignment for threading.
void	analyze_read (const expr2tc &expr)
	Analyze the contents of a read for threading.
void	get_expr_globals (const namespacet &ns, const expr2tc &expr, std::set< expr2tc > &global_list, access_kindt kind, bool under_deref=false)
	Get list of globals accessed by expr.
expr2tc	resolve_pointer_target (const namespacet &ns, const expr2tc &ptr, bool &to_global, bool through_deref)
	Resolve one pointer level: the object ptr's value set names, or nil.
void	record_aggregate_held_target (const namespacet &ns, const expr2tc &expr, std::set< expr2tc > &global_list, access_kindt kind)
	Record what a dereference reaches when the pointer it goes through is not a bare symbol (R29).
void	record_access_key (const expr2tc &key, std::set< expr2tc > &global_list, access_kindt kind)
	Record key as an object accessed by this transition, for MPOR.
bool	check_mpor_dependency (unsigned int j, unsigned int l) const
	Check for scheduling dependencies.
transition_footprintt	last_transition_footprint (unsigned int tid) const
	Footprint of the transition thread tid most recently completed.
bool	check_mpor_dependency (unsigned int j, const transition_footprintt &fp) const
	As check_mpor_dependency, but against a footprint captured earlier rather than against a thread's current one.
void	calculate_mpor_constraints ()
	Calculate MPOR schedulable threads.
bool	is_transition_blocked_by_mpor () const
	Read-only accessor for mpor_says_no.
const std::vector< std::vector< int > > &	get_dependency_chain () const
	Read-only accessor for the MPOR dependency chain, for the A6.4 harness.
const std::vector< unsigned int > &	get_thread_last_transition () const
	Read-only accessor for the chain's run order, for the A6.4 harness.
void	force_cswitch ()
	Accessor method for cswitch_forced.
bool	has_cswitch_point_occured () const
	Has a context switch point occurred.
bool	can_execution_continue () const
	Can execution continue in this thread?
std::size_t	generate_hash () const
	Generate hash of entire execution state.
std::size_t	update_hash_for_assignment (const expr2tc &rhs)
	Generate hash of an expression.
void	print_stack_traces (unsigned int indent=0) const
	Print stack trace of each thread to stdout.
void	switch_to_monitor ()
	Switch to registered monitor thread.
void	switch_away_from_monitor ()
	Switch away from registered monitor thread.
void	kill_monitor_thread ()
	Makr registered monitor thread as ended.
void	analyze_args (const expr2tc &expr) override
	Analyze the shared varables in a function call, this is because an argumemt may be renamed to constant bool in symex_function_call_code(), while we need to get the information for context switch.
Public Member Functions inherited from goto_symext
	goto_symext (const namespacet &_ns, contextt &_new_context, const goto_functionst &goto_functions, std::shared_ptr< symex_targett > _target, optionst &opts)
	Default constructor.
	goto_symext (const goto_symext &sym)
goto_symext &	operator= (const goto_symext &sym)
expr2tc	guard_identifier ()
	Return identifier for goto guards.
bool	chase_copies (expr2tc &expr) const
	Rewrite an expression onto the canonical basis of its copy chains: every L2 symbol with an entry in copy_definitions is replaced by the value it was assigned.
tvt::tv_enumt	path_guard_decides (const expr2tc &new_guard, bool already_false, bool already_true)
	Whether the accumulated path guard already decides a branch condition: TV_TRUE when a conjunct matches it, TV_FALSE when one matches its negation, TV_UNKNOWN otherwise.
void	record_guard_definition (const expr2tc &guard_expr, const expr2tc &rhs)
	Remember a guard generation's defining condition for path_guard_decides.
expr2tc	rewrite_conjunct (const expr2tc &conjunct)
	A path-guard conjunct rewritten onto the canonical basis path_guard_decides compares on.
conjunct_indext	prefix_index (const guard2tc &guard)
	The conjunct index of `guard`, which must not be true.
void	record_copy_definition (const expr2tc &renamed_lhs, const expr2tc &rhs)
	Record a copy chain for chase_copies after an unconditional assignment, when the rhs is a stable value: a (possibly typecast) L2 symbol, or a pure bitvector computation over such leaves.
goto_symext::symex_resultt	get_symex_result ()
	Create a symex result for this run.
void	add_memory_leak_checks ()
	Perform accounting checks / assertions at end of a program run.
void	release_symex_caches ()
	Free what only symex reads, once a formula is built: the guard prefix index grows with every branching goto and would otherwise live through solving.

Static Public Member Functions
static void	reset_dynamic_counter ()
	Zero the dynamic-object counter.
Static Public Member Functions inherited from goto_symext
static std::string	assertion_message (const namespacet &ns, const goto_programt::instructiont &i)
	The message of the claim an ASSERT instruction raises for itself, as opposed to a check symex raises while evaluating its guard.

Public Attributes
std::vector< goto_symex_statet >	threads_state
	Stack of thread states.
std::vector< std::list< std::pair< goto_programt::const_targett, merge_statet > > >	preserved_paths
	Preserved paths.
std::vector< unsigned int >	atomic_numbers
	Atomic section count.
std::vector< expr2tc >	thread_start_data
	Storage for threading libraries thread start data.
unsigned int	last_active_thread
	Last active thread's ID.
transition_resultt	last_transition
	Explicit result of the last symbolic transition taken.
std::shared_ptr< ex_state_level2t >	state_level2
	Global L2 state of this execution_statet.
value_sett	global_value_set
	Global pointer tracking state record.
unsigned int	active_thread
	Current active states thread ID.
irep_idt	guard_execution
	Name prefix for execution guard.
unsigned	nondet_count
	Number of nondeterministic symbols in this state.
unsigned int	node_id
	Identifying number for this execution state.
bool	interleaving_unviable
	True if the guard on this interleaving becomes false.
bool	main_returned
	True once main has returned and the exit-time code is running.
unsigned int	monitor_tid
	TID of monitor thread, for monitor intrinsics.
bool	tid_is_set
	Whether monitor_tid is set.
unsigned int	monitor_from_tid
	TID of thread that switched to monitor.
bool	mon_from_tid
	Whether monitor_from_tid is set.
unsigned int	thread_cswitch_threshold
	Minimum number of threads to exist to consider a context switch.

Static Public Attributes
static constexpr const char *	guard_execution_name
	Name of the top-level execution guard symbol.
static unsigned	dynamic_counter = 0
	Number of dynamic objects in this state.
static unsigned int	node_count = 0

Protected Member Functions
void	copy_derived_from (const execution_statet &ex)
	Copy execution_statet's own scheduling fields from ex.
Protected Member Functions inherited from goto_symext
virtual void	do_simplify (expr2tc &expr)
	Perform simplification on an expression.
expr2tc	branch_decision_guard (const expr2tc &guard) const
	The guard a branch decision is read from.
void	dereference (expr2tc &expr, dereferencet::modet mode, bool block_assertions=false)
	Dereference an expression.
void	symex_return (const expr2tc &code)
	Perform interpretation of RETURN instruction.
void	symex_witness_function_return (expr2tc ret_val, const irep_idt &call_line)
bool	symex_witness_function_enter (const irep_idt &call_line)
void	symex_witness_branching (const expr2tc &old_guard, const expr2tc &new_guard, bool forward, bool &new_guard_true, bool &new_guard_false, const goto_programt::instructiont &instruction)
void	symex_witness_assert (expr2tc &new_expr, const std::string &msg)
void	symex_other (const expr2tc &code)
	Interpret an OTHER instruction.
void	symex_decl (const expr2tc &code)
	Interpret an DECL instruction.
void	symex_dead (const expr2tc &code)
	Interpret an DEAD instruction.
bool	stack_checks_enabled () const
	True when either stack limit is on.
void	check_stack_size (const expr2tc &expr, const std::string &subject="")
	Account expr's storage against the current frame and claim that neither –stack-limit nor –total-stack-limit is exceeded.
void	symex_assume ()
	Interpret an ASSUME instruction.
void	symex_assert ()
	Interpret an ASSERT instruction.
bool	check_incremental (const expr2tc &expr, const std::string &msg)
	Perform incremental SMT solving for assert and assume statements.
void	record_property_verdict (const std::string &msg, property_verdictt verdict, const std::string &note="")
	Record a verdict for the claim being symbolically executed.
virtual void	assertion (const expr2tc &assertion, const std::string &msg)
	Perform an assertion.
void	propagate_assume_equality (const expr2tc &the_assumption)
	Lift var == const from an assume into the level2 constant propagator so subsequent renames of var substitute the constant directly.
void	flush_deferred_assumptions ()
	Before a claim that needs them, emit every deferred assumption into the target equation.
void	merge_gotos ()
	Merge converging states into current state.
void	merge_value_sets (const statet::merge_statet &merge_state)
	Merge pointer tracking value sets in a phi function.
void	merge_locality (const statet::merge_statet &merge_state)
void	snapshot_interval_domain (statet::merge_statet &merge_state)
	Record the online interval domain in a path being parked, so merge_interval_domain can join it back in (#8047).
void	assume_loop_continues (const goto_programt::instructiont &instruction, const expr2tc &guard, bool forward, bool always_jumps)
	Narrow the online interval domain by the condition under which a loop GOTO's continuing path proceeds; nothing when the GOTO always jumps, since that path is dead.
void	merge_interval_domain (const statet::merge_statet &merge_state)
	Join a parked path's interval domain into the shared one; a path parked without a snapshot sends the domain to top.
void	phi_function (const statet::merge_statet &merge_state)
	Join a previous jump's merge snapshot into the active thread state.
bool	get_unwind (const symex_targett::sourcet &source, const BigInt &unwind)
	Test whether unwinding bound has been exceeded.
void	loop_bound_exceeded (const expr2tc &guard)
	Encode unwinding assertions and assumption.
void	pop_frame ()
	Pop a stack frame.
bool	is_python_gc_object (const symbolt *base) const
	Whether base is a user-defined Python class instance that follows garbage-collected lifetime semantics (issue #4773).
bool	make_return_assignment (expr2tc &assign, const expr2tc &code_return)
	Create assignment for return statement.
void	symex_function_call (const expr2tc &call)
	Perform function call.
void	symex_end_of_function ()
	End a functions interpretation.
virtual void	symex_function_call_deref (const expr2tc &call)
	Handle an indirect function call, to a pointer.
virtual void	symex_function_call_code (const expr2tc &call)
	Handle a call to a statically-known function: checks recursion bounds, sets up the new frame, assigns arguments, and jumps to the body.
bool	symex_uninterpreted_function (const code_function_call2t &call, const irep_idt &identifier)
	Model a call to a "__ESBMC_uninterpreted_" or "__CPROVER_uninterpreted_" function as a genuine uninterpreted function: assign the return an uninterpreted_func2t application of the (mangled) callee to its renamed arguments.
bool	get_unwind_recursion (const irep_idt &identifier, BigInt unwind)
	Discover whether recursion bound has been exceeded.
expr2tc	argument_value (const type2tc &arg_type, const expr2tc &rhs, const irep_idt &identifier)
	Convert an actual argument to its parameter's type, claiming the call undefined when the two are incompatible.
unsigned int	argument_assignments (const irep_idt &function_identifier, const code_type2t &function_type, const std::vector< expr2tc > &arguments)
	Join up function arguments.
bool	run_next_function_ptr_target (bool first)
	Setup next function in a chain of func ptr calls.
void	run_intrinsic (const code_function_call2t &call, reachability_treet &art, const std::string &symname)
	Run an intrinsic, something prefixed with __ESBMC.
bool	run_builtin (const code_function_call2t &call, const std::string &symname)
	Run a builtin, something prefixed with __builtin.
void	symex_bounded_math (const code_function_call2t &call, const std::string &function)
	_builtin_bounded<function>(x, exact): the bounded result of a transcendental function, from util/arith/transcendental.h.
void	intrinsic_yield (reachability_treet &arg)
	Perform yield; forces a context switch point.
void	intrinsic_switch_to (const code_function_call2t &c, reachability_treet &art)
	Perform switch_to; switches control to explicit thread ID.
void	intrinsic_switch_from (reachability_treet &arg)
	Yield, always switching away from this thread.
void	intrinsic_get_thread_id (const code_function_call2t &call, reachability_treet &art)
	Perform get_thread_id; return the current thread identifier.
void	intrinsic_set_thread_data (const code_function_call2t &call, reachability_treet &art)
	Perform set_thread_state; store thread startup information.
void	intrinsic_get_thread_data (const code_function_call2t &call, reachability_treet &art)
	Perform get_thread_data; get thread startup information.
void	intrinsic_spawn_thread (const code_function_call2t &call, reachability_treet &art)
	Perform spawn_thread; Generates a new thread at a named function.
void	intrinsic_terminate_thread (reachability_treet &art)
	Perform terminate_thread; Record thread as terminated.
void	intrinsic_havoc_object (const code_function_call2t &call)
	Perform havoc_object; assign nondet to every object the argument may point to, whole and of any size.
void	intrinsic_init_thread_local (reachability_treet &art)
	Perform init_thread_local; seeds each __thread-qualified global to its static initializer in the active thread's renaming scope.
void	intrinsic_really_atomic_begin (reachability_treet &art)
	Really atomic start/end - atomic blocks that just disable ileaves.
void	intrinsic_really_atomic_end (reachability_treet &art)
	Really atomic start/end - atomic blocks that just disable ileaves.
void	intrinsic_switch_to_monitor (reachability_treet &art)
	Context switch to the monitor thread.
void	intrinsic_switch_from_monitor (reachability_treet &art)
	Context switch from the monitor thread.
void	intrinsic_register_monitor (const code_function_call2t &call, reachability_treet &art)
	Register which thread is the monitor thread.
void	intrinsic_kill_monitor (reachability_treet &art)
	Terminate the monitor thread.
void	intrinsic_memset (reachability_treet &art, const code_function_call2t &func_call)
	Intrinsic call for C memset function call.
void	intrinsic_memcpy (reachability_treet &art, const code_function_call2t &func_call)
	Intrinsic call for C memcpy function call.
void	intrinsic_memchr (reachability_treet &art, const code_function_call2t &func_call)
	Intrinsic call for C memchr function call.
void	intrinsic_memcmp (reachability_treet &art, const code_function_call2t &func_call)
	Models __ESBMC_memcmp(s1, s2, n): for a constant n with both pointers resolving to concrete primitive objects, build the lexicographic comparison result as a single nested-ite expression over the n byte reads (no loop, no unwinding) and assign it to the call's return.
bool	memcpy_symbolic_length (const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg)
	Models a memcpy/memmove whose length is not a constant, the case intrinsic_memcpy_impl otherwise defers to the C byte loop (which then unwinds –unwind times per call).
void	memcpy_finish (const code_function_call2t &func_call, const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg)
	The NULL checks and return-value assignment shared by both of intrinsic_memcpy_impl's paths.
void	claim_valid_operand (const expr2tc &ptr, const expr2tc &n, const std::string &func)
	An INTERNAL dereference drops an unknown or invalid target without a claim, so the memory builtins claim it themselves when `ptr's` value set holds one and `n` is nonzero.
void	claim_not_code (const expr2tc &guard)
	Claim that a memory builtin's operand, on the path `guard` selects, is not a code object; nothing under –no-pointer-check.
bool	memcmp_resolve_operand (const expr2tc &ptr, unsigned long number_of_bytes, expr2tc &object, uint64_t &offset, uint64_t &avail_bytes, bool rename_object=true)
	Helper for intrinsic_memcmp: resolve `ptr` to a single concrete primitive object with a constant offset, validating that an `number_of_bytes` read stays in bounds.
void	claim_nonnull_operand (const expr2tc &ptr, const expr2tc &n, const std::string &func)
	Claims `ptr` is not NULL unless `n` is zero.
void	intrinsic_memmove (reachability_treet &art, const code_function_call2t &func_call)
	Models __ESBMC_memmove.
void	intrinsic_memcpy_impl (reachability_treet &art, const code_function_call2t &func_call, const std::string &bump_name)
	Shared core for intrinsic_memcpy / intrinsic_memmove; `bump_name` is the C fallback (__memcpy_impl / __memmove_impl) used when the byte-exact optimisation cannot apply.
void	bump_call (const code_function_call2t &func_call, const std::string &symname)
void	intrinsic_get_object_size (const code_function_call2t &func_call, reachability_treet &art)
	Returns the size of the object.
void	intrinsic_builtin_object_size (const code_function_call2t &func_call, reachability_treet &art)
	Implements GCC's __builtin_object_size intrinsic for object size determination.
void	replace_races_check (expr2tc &expr)
void	simplify_python_builtins (expr2tc &expr)
void	reject_untyped_isinstance (const expr2tc &value)
void	volatile_check (expr2tc &expr)
void	finalize_realloc_result (const expr2tc &lhs, const expr2tc &result, const expr2tc &new_array, const guard2tc &guard, const expr2tc &realloc_size, const expr2tc &alloc_fail)
	Finalize the result of a realloc operation.
void	update_pointer_validity (const expr2tc &old_ptr, const expr2tc &alloc_fail, const guard2tc &guard)
	Update pointer validity information after realloc.
expr2tc	model_allocation_failure (const expr2tc &result, const expr2tc &old_ptr, const guard2tc &guard, const expr2tc &over_cap, expr2tc &alloc_fail)
	Model allocation failure behavior for realloc.
void	bound_dynamic_object_size (const code_assign2t &code)
	Bound at PTRDIFF_MAX the object size an assignment records, reporting a constant request that exceeds it rather than assuming it away.
expr2tc	create_result_pointer (const expr2tc &new_array, const type2tc &lhs_type)
	Create result pointer from newly allocated array.
expr2tc	calculate_old_element_count (const expr2tc &old_base_array, const type2tc &elem_type, bool old_is_array)
	Calculate the number of elements in the old memory object.
expr2tc	calculate_element_count (const expr2tc &size_bytes, const expr2tc &elem_size)
	Calculate number of elements from byte size.
type2tc	determine_fallback_element_type (const sideeffect2t &code, const expr2tc &lhs)
	Determine fallback element type for realloc.
void	analyze_old_object (const expr2tc &old_obj, type2tc &elem_type, expr2tc &old_base_array, bool &old_is_array)
	Analyze an object a reallocated pointer may point to.
void	copy_old_objects (const std::list< dereference_callbackt::internal_item > &old_objects, const expr2tc &new_array, const expr2tc &new_elem_count, const type2tc &elem_type, const guard2tc &guard)
	Copy each object a reallocated pointer may point to into the new allocation, guarded by the pointer pointing to it.
bool	handle_realloc_zero_size (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard, const expr2tc &realloc_size)
	Handle realloc with zero size parameter.
void	copy_single_element (const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &idx, const type2tc &elem_type, const type2tc &new_elem_type, bool old_is_array, const guard2tc &guard)
	Copy a single element between old and new arrays.
void	copy_memory_content (const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &old_elem_count, const expr2tc &new_elem_count, const type2tc &elem_type, bool old_is_array, const guard2tc &guard)
	Copy memory content from old to new allocation.
expr2tc	create_dynamic_memory_symbol (const type2tc &elem_type, const expr2tc &size_expr, const std::string &name_prefix)
	Create a new dynamic memory symbol.
bool	terminate_handler ()
	Call terminate function handler when needed.
bool	unexpected_handler ()
	Call unexpected function handler when needed.
void	replace_dynamic_allocation (expr2tc &expr)
	Replace ireps regarding dynamic allocations with code.
std::vector< expr2tc >	value_set_objects (const expr2tc &ptr, bool &complete)
	The objects the value set says `ptr` may address.
expr2tc	named_object (const expr2tc &base) const
	`base` if it is a named object, nil otherwise.
bool	resolve_by_value_set (expr2tc &expr, const expr2tc &ptr, const std::function< expr2tc(const expr2tc &)> &resolve)
	A pointer reaching a check through a parameter or a local variable is a plain symbol, so the syntactic address_of tests below find no name and the check falls back on __ESBMC_alloc and DYNAMIC_SIZE.
bool	resolve_valid_object_by_value_set (expr2tc &expr, const expr2tc &obj_ref)
	Decide VALID_OBJECT from the object the value set names, if it names one.
bool	resolve_dynamic_size_by_value_set (expr2tc &expr)
	Size a heap object by its allocation, and an object with automatic or static storage by its type.
void	replace_valid_object (expr2tc &expr)
	Decide VALID_OBJECT / DEALLOCATED_OBJ against the object the pointer names.
void	replace_dynamic_size (expr2tc &expr)
	Size the object DYNAMIC_SIZE names, falling back to the heap-only table.
void	default_replace_dynamic_allocation (expr2tc &expr)
bool	is_valid_object (const symbolt &symbol)
	Decide if symbol is valid or not.
void	handle_sideeffect (const expr2tc &lhs, const sideeffect2t &effect, const guard2tc &guard)
	Handle side effects in the symbolic execution.
bool	handle_conditional (const expr2tc &lhs, const if2t &if_effect, const guard2tc &guard)
	Handle conditional expressions (if2t) in the symbolic execution.
expr2tc	materialise_old_snapshot (const expr2tc &value, const guard2tc &guard)
	Give a value storage of its own, for __ESBMC_old.
void	symex_assign_rec (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc full_rhs, guard2tc &guard, const bool hidden)
	Recursively perform symex assign.
void	symex_assign_symbol (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to a symbol.
void	symex_assign_structure (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to a structure.
void	symex_assign_array_structure (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to an array literal.
void	symex_assign_union (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to a union.
void	symex_assign_extract (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to an extract irep.
void	symex_assign_typecast (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to a typecast irep.
void	symex_assign_array (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to an array.
void	symex_assign_member (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to a struct.
void	symex_assign_if (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to an "if".
void	symex_assign_byte_extract (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Perform assignment to a byte extract.
void	symex_assign_concat (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	Assign through a 'concat' operation.
void	symex_assign_bitfield (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
	This method is used when we need to assign a value to a struct bitfield which is obtained via applying a bit-mask and bit-shifting.
expr2tc	symex_malloc (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
	Symbolic implementation of malloc.
void	symex_realloc (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
	Implementation of realloc.
expr2tc	symex_alloca (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
	Symbolic implementation of alloca.
expr2tc	symex_mem (const bool is_malloc, const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
	Wrapper around for alloca and malloc.
void	offer_malloc_zero_null (const expr2tc &size, expr2tc &rhs, guard2tc &alloc_guard)
	Offer both outcomes C17 7.22.3p1 permits for a zero-sized malloc, under –malloc-zero-is-null.
expr2tc	symex_mem_inf (const expr2tc &lhs, const type2tc &base_type, const guard2tc &guard)
	Wrapper around for infinite array allocation.
void	track_new_pointer (const expr2tc &ptr_obj, const type2tc &new_type, const guard2tc &guard, const expr2tc &size=expr2tc())
	Pointer modelling update function.
void	record_frame_alloca (const expr2tc &lhs, const expr2tc &object, bool is_malloc)
	Records an alloca'd object on the current frame, to die when it returns.
void	symex_free (const expr2tc &expr)
	Symbolic implementation of free.
void	invalidate_object (const expr2tc &ptr)
	Clear the valid bit of the object `ptr` points to, with no free checks.
void	symex_cpp_delete (const expr2tc &code)
	Symbolic implementation of c++'s delete.
void	symex_cpp_new (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
	Symbolic implementation of c++'s new.
expr2tc	symex_sprintf_store (const code_printf2t &call)
	Store an unrenamed sprintf or snprintf call's output in its destination buffer, when the format bounds that output's length.
expr2tc	sprintf_output (const code_printf2t &call, size_t fmt_idx, const type2tc &char_type, std::vector< expr2tc > &chars)
	The output of an unrenamed sprintf or snprintf call: its characters before the NUL in chars, and its length, nil when unknown.
expr2tc	printf_output_length (const code_printf2t &call, size_t fmt_idx, size_t &max_len)
	The length of an unrenamed printf-family call's output whose constant format holds only text and d, i, u or s conversions without flags, width or precision, with its largest value in max_len; nil for any other format.
expr2tc	string_length (const expr2tc &ptr, size_t &max_len)
	The characters a s conversion prints for the unrenamed char pointer ptr, adding its largest value to max_len; nil unless ptr resolves to one byte array at a constant offset.
expr2tc	printf_return_length (const expr2tc &lhs, const code_printf2t &call, size_t fmt_idx)
	Store an unrenamed sprintf-family call's output and return the length that call returns: the stored length, or for printf, fprintf and dprintf with a used result, printf_output_length.
void	assume_printf_length (const expr2tc &retval, const expr2tc &len)
	Assume a printf-family call's return value equals the length of its output, when both are known.
void	assume_printf_range (const expr2tc &retval, const BigInt &lo, const BigInt &hi, bool may_fail)
	Assume a printf-family call's return value lies in [lo, hi], or is -1 when may_fail.
void	symex_asprintf_buffer (const expr2tc &strp, const expr2tc &retval)
	Point an asprintf/vasprintf call's strp at a fresh heap buffer of retval + 1 bytes, allocated only when retval is non-negative.
bool	format_printf_output (const code_printf2t &call, size_t fmt_idx, printf_formattert &formatter, bool &constant_args)
	Run formatter over an unrenamed printf-family call; false when the format is not a constant.
bool	recover_va_list_args (const code_printf2t &call, size_t fmt_idx, std::list< expr2tc > &out)
	Recover the variadic arguments hidden behind a va_list operand of a v*printf-family call (vprintf/vfprintf/vsprintf/vsnprintf/vasprintf).
void	symex_input (const code_function_call2t &expr)
	Symbolic implementation of scanf and fscanf.
void	symex_va_arg (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
	Symbolic implementation of va_arg.
std::optional< renaming::level2t::name_record >	va_list_l1_record (const expr2tc &va_list_expr) const
	Resolve a va_list expression to the l1 identity record of the local variable backing it; nullopt when it cannot be pinned down to one.
std::vector< renaming::level2t::name_record >	va_list_pointee_records (const expr2tc &va_list_expr) const
	The l1 identity records of the local va_lists a pointer-valued expression may point to.
bool	va_list_is_started (const expr2tc &va_list_expr) const
	Whether the va_list denoted by this expression is known (or assumed) to have been initialised by va_start/va_copy.
void	va_list_mark_started (const expr2tc &va_list_expr, bool started, const expr2tc &cursor)
	Record the started-by-va_start state of the va_list denoted by this expression, and the va_arg index it reads next, if known (nil if not).
void	va_list_start (const expr2tc &va_list_expr)
	va_start: the va_list reads this frame's first variadic argument next.
expr2tc	va_list_cursor_symbol (const renaming::level2t::name_record &rec)
	The l1 symbol holding the va_arg index a local va_list reads next.
expr2tc	va_list_cursor (const expr2tc &va_list_expr)
	The cursor symbol of a started local va_list; nil when its cursor is not known, and the frame's cursor applies.
std::vector< renaming::level2t::name_record >	va_list_owner_records (const expr2tc &va_list_expr) const
	The records va_list_frame looks for: a va_copy destination's are those of the va_list it was copied from.
void	va_list_copy (const expr2tc &dst, const expr2tc &src)
	va_copy: start dst as src is, reading where src reads next.
goto_symex_statet::framet &	va_list_frame (const expr2tc &va_list_expr)
	The frame whose variadic arguments a va_list reads: the activation that declared it, which is a caller's when the va_list was passed down.
void	replace_nondet (expr2tc &expr)
	Replace nondet func calls with nondeterminism.
bool	is_assume_false (const expr2tc &assumption)
	Incrementally check the assumption.
void	assume_uf_congruence (const irep_idt &identifier, const irep_idt &name, const std::vector< expr2tc > &arguments, const expr2tc &result, const type2tc &ret_type)
	Assume equal arguments imply an equal result against every earlier application of `identifier`, and record this one.
void	key_intrinsic_pointer_reads (const code_function_call2t &call, const irep_idt &id)
	Key the reads the memcpy/memmove/memcmp/memchr intrinsics perform, which symex carries out internally rather than through a dereference (#7826).

Protected Attributes
int	CS_number
	Number of context switches performed by this ex_state.
std::vector< std::set< expr2tc > >	thread_last_reads
	For each thread, a set of symbols that were read by the thread in the last transition (run).
std::vector< std::set< expr2tc > >	thread_last_writes
	For each thread, a set of symbols that were written by the thread in the last transition (run).
std::vector< std::vector< int > >	dependency_chain
	Dependancy chain for POR calculations.
std::vector< unsigned int >	thread_last_transition
	Run-order ordinal of each thread's last completed transition; 0 for a thread that has not run.
unsigned int	transition_ordinal
	Ordinal issued to the next completed transition.
bool	mpor_says_no
	MPOR scheduling outcome.
bool	cswitch_forced
	Indicates a mandatory context switch should occur.
bool	symex_trace
	Are we tracing / printing symex instructions?
bool	smt_during_symex
	Are we encoding SMT during exploration?
bool	smt_thread_guard
	Are we evaluating the thread guard in the SMT solver during context switching?
bool	no_propagation
	Was constant propagation disabled with –no-propagation?
Protected Attributes inherited from goto_symext
optionst &	options
	Options we're working with.
irep_idt	guard_identifier_s
	Symbol prefix for guards.
persistent_map< irep_idt, expr2tc, irep_id_hash >	guard_definitions
	Defining condition of each L2 guard symbol generation, i.e.
persistent_map< irep_idt, expr2tc, irep_id_hash >	copy_definitions
	Copy chains between L2 symbol generations: lhs generation -> the stable value it was unconditionally assigned — a (possibly typecast) L2 symbol, or a pure bitvector computation over such leaves (the operand-split idiom).
persistent_map< expr2tc, conjunct_indext, irep2_hash >	guard_prefix_index
	prefix_index's result per and-chain node of a path guard.
std::vector< deferred_assumptiont >	deferred_assumptions
	Assumptions defer_assumption() holds back, in program order.
bool	claim_skips_deferred = false
	Set while claim() handles a Python assert's own condition, which needs no deferred assumption.
std::unordered_map< irep_idt, expr2tc >	dynamic_object_sizes
	The renamed byte size each heap object was allocated with, by symbol.
unsigned	first_loop
	Loop numbers.
unsigned	total_claims
	Number of assertions executed.
unsigned	remaining_claims
	Number of assertions remaining to be discharged.
unsigned	simplified_claims
	Number of assertions that were trivially verified.
unsigned	bounded_loop_truncations = 0
	Loops cut off at the unwinding bound with no unwinding assertion to flag it, i.e.
reachability_treet *	art1
	Reachability tree we're working with.
std::map< unsigned, BigInt >	unwind_set
	Unwind bounds, loop number -> max unwinds.
std::map< std::pair< std::string, unsigned >, BigInt >	unwind_func_set
	Unwind bounds by function name and per-function loop index (0-indexed), (function name, loop index) -> max unwinds.
std::map< unsigned, std::pair< std::string, unsigned > >	loop_id_to_func_index
	Mapping global loop ID -> (function name, per-function loop index).
BigInt	max_unwind
	Global maximum number of unwinds.
std::optional< interval_domaint >	interval_domain_state
	Online interval domain: guard pruning is on by default (disable with –no-interval-symex-guard); assertion pruning via –interval-symex-assert discharges claims proven TRUE.
const namespacet &	ns
	Namespace we're working in.
contextt &	new_context
	Context we're working with.
const goto_functionst &	goto_functions
	GOTO functions that we're operating over.
std::shared_ptr< symex_targett >	target
	Target listening to the execution trace.
goto_symex_statet *	cur_state
	Target thread we're currently operating upon.
irep_idt	valid_ptr_arr_name
	Symbol names for modelling arrays.
irep_idt	alloc_size_arr_name
irep_idt	dyn_info_arr_name
std::list< allocated_obj >	dynamic_memory
	List of all allocated objects.
std::map< irep_idt, std::vector< std::pair< std::vector< expr2tc >, expr2tc > > >	uf_applications
	Per-callee history of uninterpreted-function applications the SMT backend cannot encode natively, keyed on the mangled callee name.
std::unordered_map< renaming::level2t::name_record, bool, renaming::level2t::name_rec_hash >	va_started
	Level-1 identities (base name, activation, thread) of va_list objects initialised by va_start, or by va_copy from a started source, and whether each has a cursor symbol of its own.
std::unordered_map< renaming::level2t::name_record, renaming::level2t::name_record, renaming::level2t::name_rec_hash >	va_copied_from
	For each va_copy destination, the local va_list whose frame's variadic arguments it reads, so a copy made in a callee reads the caller's.
bool	no_return_value_opt
	Disable return value optimization.
unsigned long	stack_limit
	Limit size, in bits, for a single stack frame.
unsigned long	total_stack_limit
	Limit size, in bits, for every live stack frame taken together.
unsigned long	depth_limit
	Depth limit, as given by the –depth option.
unsigned long	break_insn
	Instruction number we are to break at – that is, trap, to the debugger.
bool	memory_leak_check
	Flag as to whether we're performing memory leak checks.
bool	no_reachable_memleak
	Flag as to whether we're pruning the objects from the memory leak check that are still reachable via global pointers.
bool	no_assertions
	Flag as to whether we're checking user assertions.
bool	no_simplify
	Flag as to whether we're not simplifying exprs.
bool	no_unwinding_assertions
	Flag as to whether we're inserting unwinding assertions.
bool	partial_loops
	Flag as to whether we're not enabling partial loops.
bool	k_induction
	Flag as to whether we're doing a k-induction.
bool	base_case
	Flag as to whether we're doing a k-induction base case.
bool	forward_condition
	Flag as to whether we're doing a k-induction forward condition.
bool	inductive_step
	Flag as to whether we're doing a k-induction inductive step.
bool	validate_witness
	Cached from –validate-violation-witness; checked on every branch/intrinsic.
std::list< dereference_callbackt::internal_item >	internal_deref_items
	Set of dereference state records; this field is used as a mailbox between the dereference code and the caller, who will inspect the contents after a call to dereference (in INTERNAL mode) completes.

Friends
void	build_goto_symex_classes ()

Additional Inherited Members
Static Protected Attributes inherited from goto_symext
static constexpr size_t	max_copy_definition_nodes = 64
	Cap on one recorded copy definition's flattened node count: canonicalization doubles nested arithmetic chains per link, and an oversized definition costs more to match than it prunes.

Detailed Description

Thread-aware symex state explored by reachability_treet.

Holds the global SSA renaming state (level 2) and value set, plus a vector of per-thread goto_symex_statet recording each thread's call stack, program counter, and local guard. reachability_treet drives this object one instruction at a time via symex_step; threading-specific instructions (thread spawn, atomic begin/end, yield, monitor) are handled here while the rest fall through to goto_symext::symex_step.

Context switches are not detected by ad-hoc hooks. Instead, every symex_step records the executed transition into last_transition (thread id, optional parent guard, optional parked_patht). When the scheduler later decides to switch threads, preserve_last_paths reads last_transition to know which deferred-merge snapshots to carry across the switch — including a direct iterator to the path parked by goto_symext::symex_goto or symex_return via the record_parked_path hook.

goto_symext occasionally needs data only execution_statet has (current thread id, the ability to spawn a new thread); those flow back through __ESBMC_* intrinsic calls dispatched in symex_step.

Member Typedef Documentation

◆ merge_statet

typedef goto_symex_statet::merge_statet execution_statet::merge_statet

Member Enumeration Documentation

◆ access_kindt

enum class execution_statet::access_kindt

strong

Kind of memory access, used by get_expr_globals to decide whether a read-only global can be filtered out of cswitch-triggering sets.

Enumerator
READ
WRITE

Constructor & Destructor Documentation

◆ execution_statet() [1/2]

execution_statet::execution_statet	(	const goto_functionst &	goto_functions,
		const namespacet &	ns,
		reachability_treet *	art,
		std::shared_ptr< symex_targett >	_target,
		contextt &	context,
		std::shared_ptr< ex_state_level2t >	l2init,
		optionst &	options )

Default constructor.

Takes the environment we'll be working with, and sets up a single thread with a function call to the "main" function just encoded. Two of these arguments can have unknown subclasses: _target and l2init get clone'd each time we need a new one (think the factory pattern).

Parameters

goto_functions	GOTO functions we'll operate over.
ns	Namespace we're working with.
_target	Symex target to receive assigns/asserts/etc in trace.
context	Context we'll be working in.
l2init	Initial level2t state (blank).
options	Options we're going to operate with.s

◆ execution_statet() [2/2]

execution_statet::execution_statet ( const execution_statet & ex )

Default copy constructor.

Used each time we duplicate an execution_statet in reachability_treet. Does what you might expect, but also updates any ex_state_level2t objects in the new execution_statet to point at the right object.

◆ ~execution_statet()

virtual execution_statet::~execution_statet ( )

virtualdefault

Default destructor.

Member Function Documentation

◆ add_thread()

unsigned int execution_statet::add_thread ( const goto_programt * prog )

Create a new thread.

Creates and initializes a new thread, running at the start of the GOTO program prog.

Parameters

prog	GOTO program to start new thread at.

Returns: Thread ID of newly created thread.

◆ all_threads_terminal()

bool execution_statet::all_threads_terminal ( ) const

True iff every thread in this schedule has reached a terminal state, i.e.

has either ended or has an empty call stack. This is the precondition for treating the schedule's tail as program termination — only then is it sound to fire end-of-program checks such as the memory-leak walker, since a still-running thread may hold the only live reference to a dynamic object via its stack frames.

◆ analyze_args()

void execution_statet::analyze_args ( const expr2tc & expr )

overridevirtual

Analyze the shared varables in a function call, this is because an argumemt may be renamed to constant bool in symex_function_call_code(), while we need to get the information for context switch.

Implements goto_symext.

◆ analyze_assign()

void execution_statet::analyze_assign ( const expr2tc & assign )

Analyze the contents of an assignment for threading.

If the assignment touches any kind of shared state, we track the accessed variables for POR decisions made in the future, and also ask the RT obj whether or not it wants to generate an interleaving.

Parameters

assign Container of code_assign2t object.

◆ analyze_read()

void execution_statet::analyze_read ( const expr2tc & expr )

Analyze the contents of a read for threading.

If the read touches any kind of shared state, we track the accessed variables for POR decisions made in the future, and also ask the RT obj whether or not it wants to generate an interleaving.

Parameters

expr	Container of expression possibly touching global state.

◆ assume()

void execution_statet::assume ( const expr2tc & assumption )

overridevirtual

Assume some expression is true.

Implemented by goto_symext::assume. Potentially causes a context switch, so we pass the assumption expression on to a reachability_treet analysis function.

Parameters

assumption Expression of the thing we're assuming to be true.

Reimplemented from goto_symext.

◆ calculate_mpor_constraints()

void execution_statet::calculate_mpor_constraints ( )

Calculate MPOR schedulable threads.

I.E. what threads we can schedule right now without violating the "quasi-monotonic" property.

◆ can_execution_continue()

bool execution_statet::can_execution_continue ( ) const

Can execution continue in this thread?

Answer is no if the thread has ended or there's nothing on the call stack

Returns: False if there are no further instructions to execute.

◆ check_if_ileaves_blocked()

bool execution_statet::check_if_ileaves_blocked ( )

Test to see if interleavings are blocked by the current state.

There can be a variety of reasons why interleavings are blocked; there can be only one thread, we can be in an atomic block or insn, we can have reached our context bound.

Returns: True if the current state prohibits context switches.

◆ check_mpor_dependency() [1/2]

bool execution_statet::check_mpor_dependency	(	unsigned int	j,
		const transition_footprintt &	fp ) const

As check_mpor_dependency, but against a footprint captured earlier rather than against a thread's current one.

Sleep sets need this: the transition a sleeping thread would take is the one it took when it was put to sleep, which its thread_last_* entries no longer describe.

◆ check_mpor_dependency() [2/2]

bool execution_statet::check_mpor_dependency	(	unsigned int	j,
		unsigned int	l ) const

Check for scheduling dependencies.

Whether it exists between the variables accessed by the last transition of thread j and the last transition of thread l.

Parameters

j	Most recently executed thread id
l	Other thread id to check dependency with

Returns: True if scheduling dependency exists between threads j and l

◆ claim()

void execution_statet::claim	(	const expr2tc &	expr,
		const std::string &	msg )

overridevirtual

Symbolically assert something.

Implemented by calling goto_symext::claim. However, we also pass the claimed expression onto the reachability_treet analysis functions, to see whether or not we should generate a context switch because of a read in this claim.

Parameters

expr	Expression that we're asserting is true.
msg	Textual message explaining this assertion.

Reimplemented from goto_symext.

Reimplemented in schedule_execution_statet.

◆ clone()

virtual std::shared_ptr< execution_statet > execution_statet::clone ( ) const

pure virtual

Duplicate this execution state.

This is just a vehicle for subclasses to get their hooks in when this class gets duplicated.

See also: schedule_execution_statet; dfs_execution_statet

Returns: New, duplicated execution state

Implemented in dfs_execution_statet, and schedule_execution_statet.

◆ copy_derived_from()

void execution_statet::copy_derived_from ( const execution_statet & ex )

protected

Copy execution_statet's own scheduling fields from ex.

The base goto_symext slice is left untouched (the copy constructor's initialiser list handles it once). state_level2 and threads_state are also left untouched: state_level2 is cloned in the initialiser list, and threads_state is rebuilt by the copy constructor body against that clone.

◆ cull_all_paths()

void execution_statet::cull_all_paths ( )

◆ decrement_active_atomic_number()

void execution_statet::decrement_active_atomic_number ( )

Decrease current threads atomic number count.

◆ defer_assumption()

void execution_statet::defer_assumption ( const expr2tc & assumption )

overridevirtual

As assume(), the deferred assumption reads its condition now.

Reimplemented from goto_symext.

◆ end_thread()

void execution_statet::end_thread ( )

Record a thread as ended.

Updates internal records to say that the thread has ended. The thread itself can continue executing until the next context switch point, when the scheduler notices it's unschedulable. So, always ensure end_thread is followed by forcing a context switch.

◆ execute_guard()

void execution_statet::execute_guard ( )

Generates execution guard that's true if this interleaving can be reached.

We can context switch between many points in many threads; not all of them are feasible though, and some of them place later constraints on the contents of program state. This is because the instruction causing the switch can be guarded in an if/else block. The test 01_pthread27 is an excellent example of this.

To get around this, we have a state guard that is only true if the guards at the context switch points up to here are all true. We copy the symbol for this value into the guards of all currently executing threads. This means that any assertion after a context switch is guarded by the conditions on all the previous switches that have happened.

◆ force_cswitch()

void execution_statet::force_cswitch ( )

inline

Accessor method for cswitch_forced.

Sets it to true.

◆ generate_hash()

std::size_t execution_statet::generate_hash ( ) const

Generate hash of entire execution state.

This takes all current symbolic assignments to variables contained in the l2 renaming object, and their precomputed hashes, concatonates them with the current program counter of each thread, and hashes that. This results in a full hash of the current execution state.

Returns: Hash of entire current execution state.

◆ get_active_atomic_number()

unsigned int execution_statet::get_active_atomic_number ( ) const

Get atomic number count for current thread state.

See also: atomic_numbers

Returns: Atomic number count for current thread state.

◆ get_active_state() [1/2]

goto_symex_statet & execution_statet::get_active_state ( )

Get reference to current thread state.

Returns: Reference to current thread state.

◆ get_active_state() [2/2]

const goto_symex_statet & execution_statet::get_active_state ( ) const

◆ get_active_state_number()

unsigned int execution_statet::get_active_state_number ( ) const

inline

Fetch the thread ID of the current active thread.

◆ get_context_switch()

int execution_statet::get_context_switch ( ) const

inline

Get the number of context switches performed by this ex_state.

◆ get_dependency_chain()

const std::vector< std::vector< int > > & execution_statet::get_dependency_chain ( ) const

inline

Read-only accessor for the MPOR dependency chain, for the A6.4 harness.

◆ get_dynamic_counter()

unsigned int & execution_statet::get_dynamic_counter ( )

overridevirtual

Fetch reference to count of dynamic objects in this state.

The goto_symext class knows that such a count exists, just it doesn't store it itself. So we instead provide a hook for it to fetch a reference to the true counter.

Returns: Reference to the count of global dynamic objects.

Implements goto_symext.

◆ get_expr_globals()

void execution_statet::get_expr_globals	(	const namespacet &	ns,
		const expr2tc &	expr,
		std::set< expr2tc > &	global_list,
		access_kindt	kind,
		bool	under_deref = false )

Get list of globals accessed by expr.

Reads of globals that are provably never written anywhere in the program are filtered out — they cannot participate in data races and should not force a context switch.

Parameters

ns	Namespace to work under.
expr	Expression to count global refs in.
global_list	Output set of global refs.
kind	Whether this access is a READ or a WRITE.
under_deref	Whether expr sits beneath a dereference.

◆ get_guard_identifier()

expr2tc execution_statet::get_guard_identifier ( )

Fetch name of current execution guard.

The execution guard being the guard of the interleavings up to this point being true and feasable. This is a symbolic name for it.

See also: execute_guard

Returns: Symbol of current execution state guard

◆ get_nondet_counter()

unsigned int & execution_statet::get_nondet_counter ( )

overridevirtual

Like get_dynamic_counter, but with nondet symbols.

Implements goto_symext.

◆ get_thread_last_transition()

const std::vector< unsigned int > & execution_statet::get_thread_last_transition ( ) const

inline

Read-only accessor for the chain's run order, for the A6.4 harness.

◆ get_thread_start_data()

const expr2tc & execution_statet::get_thread_start_data ( unsigned int tid ) const

inline

Fetch internal thread startup data.

◆ has_cswitch_point_occured()

bool execution_statet::has_cswitch_point_occured ( ) const

Has a context switch point occurred.

Two things can justify this:

cswitch forced by atomic end or yield.
Global data read/written.
Returns
True if context switch is now triggered

◆ increment_active_atomic_number()

void execution_statet::increment_active_atomic_number ( )

Increase current threads atomic number count.

◆ increment_context_switch()

void execution_statet::increment_context_switch ( )

inline

Increase number of context switches this ex_state has taken.

◆ is_cur_state_guard_false()

bool execution_statet::is_cur_state_guard_false ( const expr2tc & guard )

Determines if current state guard is false.

Used to check whether the interleaving we're exploring has a false guard, meaning that any further interleaving we take is unviable. If –smt-thread-guard is enabled, we ask the solver.

Returns: True when state guard is false

◆ is_transition_blocked_by_mpor()

bool execution_statet::is_transition_blocked_by_mpor ( ) const

inline

Read-only accessor for mpor_says_no.

◆ kill_monitor_thread()

void execution_statet::kill_monitor_thread ( )

Makr registered monitor thread as ended.

Designed to be used by ltl2ba produced code when the monitor is to be ended.

◆ last_transition_footprint()

transition_footprintt execution_statet::last_transition_footprint ( unsigned int tid ) const

inline

Footprint of the transition thread tid most recently completed.

◆ note_bounded_loop_truncation()

void execution_statet::note_bounded_loop_truncation ( )

overridevirtual

Under –no-unwinding-assertions a truncated loop is cut with an assumption, which drives the state guard false and so is indistinguishable at the scheduler from a genuinely infeasible path.

The remaining iterations are not infeasible, only unexplored, so the subtree is not exhausted and no thread may be put to sleep against it (issue #6831).

Reimplemented from goto_symext.

Reimplemented in schedule_execution_statet.

◆ operator=()

execution_statet & execution_statet::operator= ( const execution_statet & ex )

delete

Public assignment is deleted: a standalone a = b would not be correct here (it would leave the base goto_symext slice, threads_state, cur_state, and state_level2 as a's old objects).

Cloning happens via the copy constructor, which uses copy_derived_from internally to populate execution_statet's own fields without re-copying the base.

◆ preserve_last_paths()

void execution_statet::preserve_last_paths ( const transition_resultt & transition )

◆ print_stack_traces()

void execution_statet::print_stack_traces ( unsigned int indent = 0 ) const

Print stack trace of each thread to stdout.

Uses the passed in namespace; also uses whatever level of indentation the caller provides. Primarily a debug feature.

Parameters

ns	Namespace to work in.
indent	Indentation to print each stack trace with

◆ record_access_key()

void execution_statet::record_access_key	(	const expr2tc &	key,
		std::set< expr2tc > &	global_list,
		access_kindt	kind )

Record key as an object accessed by this transition, for MPOR.

◆ record_aggregate_held_target()

void execution_statet::record_aggregate_held_target	(	const namespacet &	ns,
		const expr2tc &	expr,
		std::set< expr2tc > &	global_list,
		access_kindt	kind )

Record what a dereference reaches when the pointer it goes through is not a bare symbol (R29).

No-op on any other expression, and on a target that is not shared.

◆ record_parked_path()

void execution_statet::record_parked_path	(	goto_programt::const_targett	,
		statet::merge_state_listt::iterator	)

overridevirtual

Hook called when a step parks a merge_statet snapshot for a deferred merge — a GOTO forking off its sibling arm, or a RETURN parking the continuation at end_of_function.

Used by execution_statet to record an explicit reference to that path on the active transition result, so it can be preserved across context switches without re-discovering it by scanning merge_state_map. No-op for non-concurrent symex.

Reimplemented from goto_symext.

◆ reset_dynamic_counter()

void execution_statet::reset_dynamic_counter ( )

static

Zero the dynamic-object counter.

Called once per exploration from reachability_treet::setup_for_new_explore – never from this class's constructor, which the reachability tree runs per interleaving and where a reset would mint colliding object names (R15).

◆ resolve_pointer_target()

expr2tc execution_statet::resolve_pointer_target	(	const namespacet &	ns,
		const expr2tc &	ptr,
		bool &	to_global,
		bool	through_deref )

Resolve one pointer level: the object ptr's value set names, or nil.

Parameters

to_global	Set when the resolved object is shared.
through_deref	Whether the pointer is dereferenced. Only then does an address-taken local count as shared: copying a pointer to it accesses nothing. Intrinsics that read through a pointer argument are keyed where symex dispatches them.

◆ restore_last_paths()

void execution_statet::restore_last_paths ( )

◆ set_thread_start_data()

void execution_statet::set_thread_start_data	(	unsigned int	tid,
		const expr2tc &	argdata )

inline

Set internal thread startup data.

◆ switch_away_from_monitor()

void execution_statet::switch_away_from_monitor ( )

Switch away from registered monitor thread.

Switches away from the registered monitor thread, to whatever thread caused switch_to_monitor to be called in the past

See also: switch_to_monitor

◆ switch_to_monitor()

void execution_statet::switch_to_monitor ( )

Switch to registered monitor thread.

Switches the currently executing thread to the monitor thread that's been previously registered. This does not result in the context switch counter being incremented. Stores which thread ID we switched from for a future switch back.

◆ switch_to_thread()

void execution_statet::switch_to_thread ( unsigned int i )

Perform a context switch to thread ID i.

Essentially this just updates the counter indicating which thread is currently active. Callers taking a scheduling switch must follow this with update_after_switch_point(), which re-executes the execution guard.

See also: execute_guard.

Parameters

i	Thread ID to switch to.

◆ symex_assign()

void execution_statet::symex_assign	(	const expr2tc &	code,
		const bool	hidden,
		const guard2tc &	guard )

overridevirtual

Symbolically assign a value.

Entirely handed off to goto_symext::symex_assign. However this method also passes the assignment to a reachability_treet analysis function to see whether the assignment should be generating a context switch.

Parameters

code	Code representing assignment we're making.
hidden	Whether the assignment is hidden from the trace.
guard	A guard for the assignment.

Reimplemented from goto_symext.

◆ symex_end_function()

void execution_statet::symex_end_function	(	reachability_treet &	art,
		const goto_programt::instructiont &	instruction )

◆ symex_goto()

void execution_statet::symex_goto ( const expr2tc & old_guard )

overridevirtual

Perform a jump across GOTO code.

Implemented by goto_symext::symex_goto. This is a concrete action, not symbolic. Although the guard is symbolic. The expression of the guard can read global state, and can thus possibly result in a context switch being generated; so we pass the guard to a reachability_treet analysis function too.

Parameters

old_guard Guard of the goto jump being performed.

Reimplemented from goto_symext.

◆ symex_printf()

void execution_statet::symex_printf	(	const expr2tc &	lhs,
		expr2tc &	code )

overridevirtual

Implemented by goto_symext::symex_printf.

Overridden only to record the globals the arguments read: the frontend lowers a printf call to an OTHER instruction, so the function-call path never analyses them.

Reimplemented from goto_symext.

◆ symex_step()

void execution_statet::symex_step ( reachability_treet & art )

overridevirtual

Make one symbolic execution step.

Take one instruction and interpret it. Can result in any action, such as a thread ending, causing a context switch, a function call being taken, a thread being created, and so forth.

Parameters

art	reachability_treet driving the exploration; forwarded to goto_symext::symex_step so threading intrinsics can call back into it.

Reimplemented from goto_symext.

◆ update_after_switch_point()

void execution_statet::update_after_switch_point ( )

Perform any necessary steps after a context switch point.

Whether or not it was taken. Resets DFS record, POR records, executes thread guard.

◆ update_hash_for_assignment()

std::size_t execution_statet::update_hash_for_assignment ( const expr2tc & rhs )

Generate hash of an expression.

Parameters

rhs	Expression to hash.

Returns: Hash of passed in expression.

◆ build_goto_symex_classes

void build_goto_symex_classes ( )

friend

Member Data Documentation

◆ active_thread

unsigned int execution_statet::active_thread

Current active states thread ID.

◆ atomic_numbers

std::vector<unsigned int> execution_statet::atomic_numbers

Atomic section count.

Every time an atomic begin is executed, the atomic_number corresponding to the thread is incremented, allowing nested atomic begins and ends. A nonzero atomic number for a thread means that interleavings are disabled currently.

◆ CS_number

int execution_statet::CS_number

protected

Number of context switches performed by this ex_state.

◆ cswitch_forced

bool execution_statet::cswitch_forced

protected

Indicates a mandatory context switch should occur.

Can happen when an atomic_end instruction has occurred, or when a __ESBMC_yield(); runs

◆ dependency_chain

std::vector<std::vector<int> > execution_statet::dependency_chain

protected

Dependancy chain for POR calculations.

In mpor paper, DCij elements map to dependency_chain[i][j] here.

◆ dynamic_counter

unsigned int execution_statet::dynamic_counter = 0

thread_localstatic

Number of dynamic objects in this state.

thread_local so parallel symex doesn't race on the counter.

◆ global_value_set

value_sett execution_statet::global_value_set

Global pointer tracking state record.

◆ guard_execution

irep_idt execution_statet::guard_execution

Name prefix for execution guard.

◆ guard_execution_name

const char* execution_statet::guard_execution_name

staticconstexpr

Initial value:

=

"execution_statet::\\guard_exec"

Name of the top-level execution guard symbol.

◆ interleaving_unviable

bool execution_statet::interleaving_unviable

True if the guard on this interleaving becomes false.

Means that there is no path from here on where any assertion may become satisfiable.

◆ last_active_thread

unsigned int execution_statet::last_active_thread

Last active thread's ID.

◆ last_transition

transition_resultt execution_statet::last_transition

Explicit result of the last symbolic transition taken.

◆ main_returned

bool execution_statet::main_returned

True once main has returned and the exit-time code is running.

◆ mon_from_tid

bool execution_statet::mon_from_tid

Whether monitor_from_tid is set.

◆ monitor_from_tid

unsigned int execution_statet::monitor_from_tid

TID of thread that switched to monitor.

◆ monitor_tid

unsigned int execution_statet::monitor_tid

TID of monitor thread, for monitor intrinsics.

◆ mpor_says_no

bool execution_statet::mpor_says_no

protected

MPOR scheduling outcome.

If we've just taken a transition that MPOR rejects, this becomes true. For various reasons, we can't tell whether or not MPOR rejects a transition in advance.

◆ no_propagation

bool execution_statet::no_propagation

protected

Was constant propagation disabled with –no-propagation?

Seeds every thread's goto_symex_statet, so the option is looked up once per run rather than once per thread creation.

◆ node_count

unsigned int execution_statet::node_count = 0

thread_localstatic

◆ node_id

unsigned int execution_statet::node_id

Identifying number for this execution state.

Used to distinguish runs in –schedule mode.

◆ nondet_count

unsigned execution_statet::nondet_count

Number of nondeterministic symbols in this state.

◆ preserved_paths

std::vector<std::list<std::pair<goto_programt::const_targett, merge_statet> > > execution_statet::preserved_paths

Preserved paths.

After switching out of a thread, only the paths active at the time the switch occurred are allowed to live, and are stored here. Format is: for each thread, a list of paths made from the instruction where the path merges and the merge_statet snapshot captured when we switched away. Preserved paths can only be in the top() frame.

◆ smt_during_symex

bool execution_statet::smt_during_symex

protected

Are we encoding SMT during exploration?

◆ smt_thread_guard

bool execution_statet::smt_thread_guard

protected

Are we evaluating the thread guard in the SMT solver during context switching?

◆ state_level2

std::shared_ptr<ex_state_level2t> execution_statet::state_level2

Global L2 state of this execution_statet.

It's also copied as a reference into each threads own state.

◆ symex_trace

bool execution_statet::symex_trace

protected

Are we tracing / printing symex instructions?

◆ thread_cswitch_threshold

unsigned int execution_statet::thread_cswitch_threshold

Minimum number of threads to exist to consider a context switch.

In certain special cases, such as LTL checking, various pieces of code and information are bunged into separate threads which aren't necessarily scheduled. In these cases we don't want to consider cswitches, because even though they're not taken, they'll heavily inflate memory size. So, instead of considering context switches where more than one thread exists, compare the number of threads against this threshold.

◆ thread_last_reads

std::vector<std::set<expr2tc> > execution_statet::thread_last_reads

protected

For each thread, a set of symbols that were read by the thread in the last transition (run).

Renamed to level1, as that identifies each piece of data that could have storage in C.

◆ thread_last_transition

std::vector<unsigned int> execution_statet::thread_last_transition

protected

Run-order ordinal of each thread's last completed transition; 0 for a thread that has not run.

Only advanced where the chain is maintained, which is why it is the chain's own notion of time rather than CS_number. DCij asserts a chain from Ti's last transition to Tj's, so every 1 must point forward in this order (A6.4).

◆ thread_last_writes

std::vector<std::set<expr2tc> > execution_statet::thread_last_writes

protected

For each thread, a set of symbols that were written by the thread in the last transition (run).

Renamed to level1, as that identifies each piece of data that could have storage in C.

◆ thread_start_data

std::vector<expr2tc> execution_statet::thread_start_data

Storage for threading libraries thread start data.

See version history of when this was introduced to fully understand why; essentially this is a workaround to prevent too much nondeterminism entering into the thread starting process.

◆ threads_state

std::vector<goto_symex_statet> execution_statet::threads_state

Stack of thread states.

The index into this vector is the thread ID of the goto_symex_statet at that location. The reachability_treet that owns this state is reachable via the inherited goto_symext::art1.

◆ tid_is_set

bool execution_statet::tid_is_set

Whether monitor_tid is set.

◆ transition_ordinal

unsigned int execution_statet::transition_ordinal

protected

Ordinal issued to the next completed transition.

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

src/goto-symex/scheduler/execution_state.h
src/goto-symex/scheduler/execution_state.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Static Public Attributes

Protected Member Functions

Protected Attributes

Friends

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ merge_statet

Member Enumeration Documentation

◆ access_kindt

Constructor & Destructor Documentation

◆ execution_statet() [1/2]

◆ execution_statet() [2/2]

◆ ~execution_statet()

Member Function Documentation

◆ add_thread()

◆ all_threads_terminal()

◆ analyze_args()

◆ analyze_assign()

◆ analyze_read()

◆ assume()

◆ calculate_mpor_constraints()

◆ can_execution_continue()

◆ check_if_ileaves_blocked()

◆ check_mpor_dependency() [1/2]

◆ check_mpor_dependency() [2/2]

◆ claim()

◆ clone()

◆ copy_derived_from()

◆ cull_all_paths()

◆ decrement_active_atomic_number()

◆ defer_assumption()

◆ end_thread()

◆ execute_guard()

◆ force_cswitch()

◆ generate_hash()

◆ get_active_atomic_number()

◆ get_active_state() [1/2]

◆ get_active_state() [2/2]

◆ get_active_state_number()

◆ get_context_switch()

◆ get_dependency_chain()

◆ get_dynamic_counter()

◆ get_expr_globals()

◆ get_guard_identifier()

◆ get_nondet_counter()

◆ get_thread_last_transition()

◆ get_thread_start_data()

◆ has_cswitch_point_occured()

◆ increment_active_atomic_number()

◆ increment_context_switch()

◆ is_cur_state_guard_false()

◆ is_transition_blocked_by_mpor()

◆ kill_monitor_thread()

◆ last_transition_footprint()

◆ note_bounded_loop_truncation()

◆ operator=()

◆ preserve_last_paths()

◆ print_stack_traces()

◆ record_access_key()

◆ record_aggregate_held_target()

◆ record_parked_path()

◆ reset_dynamic_counter()

◆ resolve_pointer_target()

◆ restore_last_paths()

◆ set_thread_start_data()

◆ switch_away_from_monitor()

◆ switch_to_monitor()

◆ switch_to_thread()

◆ symex_assign()

◆ symex_end_function()

◆ symex_goto()

◆ symex_printf()

◆ symex_step()

◆ update_after_switch_point()