goto_symext Class Reference

Primay symbolic execution class. More...

#include <goto_symex.h>

Inheritance diagram for goto_symext:

Classes
class	allocated_obj
	Records for dynamically allocated blobs of memory. More...
class	symex_resultt
	Class recording the outcome of symbolic execution. More...
struct	deferred_assumptiont

Public Types
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
	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.
virtual void	symex_step (reachability_treet &art)
	Symbolically execute one instruction.
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 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.

Protected Member Functions
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.
virtual void	symex_goto (const expr2tc &old_guard)
	Perform GOTO jump using current instruction.
virtual void	record_parked_path (goto_programt::const_targett, statet::merge_state_listt::iterator)
	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	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.
virtual void	claim (const expr2tc &expr, const std::string &msg)
	Perform an assertion.
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.
virtual void	assume (const expr2tc &assumption)
	Perform an assumption.
virtual void	defer_assumption (const expr2tc &assumption)
	Hold back the assume that ends a path at a Python assert (#8242).
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.
virtual void	note_bounded_loop_truncation ()
	Records that a loop was cut off at the unwinding bound with nothing to flag it.
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.
virtual void	symex_assign (const expr2tc &code, const bool hidden=false, const guard2tc &guard=guard2tc())
	Make symbolic assignment.
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.
virtual void	symex_printf (const expr2tc &lhs, expr2tc &code)
	Symbolic implementation of printf.
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.
virtual unsigned int &	get_dynamic_counter ()=0
	Fetch reference to global dynamic object counter.
virtual unsigned int &	get_nondet_counter ()=0
	Fetch reference to global nondet object counter.
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.
virtual void	analyze_args (const expr2tc &expr)=0
	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.
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
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.

Static Protected Attributes
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.

Friends
class	symex_dereference_statet
class	bmct
class	reachability_treet
void	build_goto_symex_classes ()

Detailed Description

Primay symbolic execution class.

Contains very little state data, instead implements a large number of methods that actually perform the symbolic execution and keep data elsewhere. Interprets actual GOTO functions. Fixes up assignments and formats operations into something suitable for being fed to the symex target object. Also maintains renaming hierarchies, call stacks, pointer tracking goo.

Member Typedef Documentation

conjunct_indext

using goto_symext::conjunct_indext = persistent_map<expr2tc, size_t, irep2_hash>

Rewritten conjunct -> position of the first conjunct rewriting to it.

statet

typedef goto_symex_statet goto_symext::statet

Constructor & Destructor Documentation

goto_symext() [1/2]

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.

Performs base initialization, storing namespace and the symex target we'll be assigning at.

Parameters

_ns	Namespace we'll be working in.
_new_context	Context we'll be working in.
_target	Symex target that actions will be recorded into.
opts	Options we'll be running with.

goto_symext() [2/2]

goto_symext::goto_symext

(

const goto_symext &

sym

)

Member Function Documentation

add_memory_leak_checks()

void goto_symext::add_memory_leak_checks

(

)

Perform accounting checks / assertions at end of a program run.

This should contain anything that must happen at the end of a program run, for example assertions about dynamic memory being freed.

analyze_args()

virtual void goto_symext::analyze_args ( const expr2tc & expr )

protectedpure virtual

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.

Implemented in execution_statet.

analyze_old_object()

void goto_symext::analyze_old_object ( const expr2tc & old_obj, type2tc & elem_type, expr2tc & old_base_array, bool & old_is_array )

protected

Analyze an object a reallocated pointer may point to.

Parameters

old_obj	The object, as found by an internal dereference.
elem_type	Output parameter for the element type.
old_base_array	Output parameter for the base array symbol.
old_is_array	Output parameter indicating if it's a typed array.

argument_assignments()

unsigned goto_symext::argument_assignments ( const irep_idt & function_identifier, const code_type2t & function_type, const std::vector< expr2tc > & arguments )

protected

Join up function arguments.

Assigns the value of arguments to a function to the actual argument variables of the function being called.

Parameters

function_type	type containing argument types of func call.
arguments	The arguments to assign to function arg variables.

Returns

the va_index for this function, if any, otherwise UINT_MAX

argument_value()

expr2tc goto_symext::argument_value ( const type2tc & arg_type, const expr2tc & rhs, const irep_idt & identifier )

protected

Convert an actual argument to its parameter's type, claiming the call undefined when the two are incompatible.

assertion()

void goto_symext::assertion ( const expr2tc & assertion, const std::string & msg )

protectedvirtual

Perform an assertion.

Adds to target an assertion that must be checked.

Parameters

assertion	Assertion that must be checked.
msg	Textual message explaining assertion.

assertion_message()

std::string goto_symext::assertion_message ( const namespacet & ns, const goto_programt::instructiont & i )

static

The message of the claim an ASSERT instruction raises for itself, as opposed to a check symex raises while evaluating its guard.

assume()

void goto_symext::assume ( const expr2tc & assumption )

protectedvirtual

Perform an assumption.

Adds to target an assumption that must always be true.

Parameters

assumption

Assumption that must always be true.

Reimplemented in execution_statet.

assume_loop_continues()

void goto_symext::assume_loop_continues ( const goto_programt::instructiont & instruction, const expr2tc & guard, bool forward, bool always_jumps )

protected

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.

Call after snapshot_interval_domain.

assume_printf_length()

void goto_symext::assume_printf_length ( const expr2tc & retval, const expr2tc & len )

protected

Assume a printf-family call's return value equals the length of its output, when both are known.

assume_printf_range()

void goto_symext::assume_printf_range ( const expr2tc & retval, const BigInt & lo, const BigInt & hi, bool may_fail )

protected

Assume a printf-family call's return value lies in [lo, hi], or is -1 when may_fail.

assume_uf_congruence()

void goto_symext::assume_uf_congruence ( const irep_idt & identifier, const irep_idt & name, const std::vector< expr2tc > & arguments, const expr2tc & result, const type2tc & ret_type )

protected

Assume equal arguments imply an equal result against every earlier application of identifier, and record this one.

Ackermannise rather than drop congruence outright: for every earlier application of this callee, assume equal arguments imply an equal result.

See also

symex_uninterpreted_function

That is the defining property of an uninterpreted function, and stating it here keeps the tuple-sorted symbol out of the solver (GitHub #6965). Sound: it rules out only non-functional behaviour. It needs operands the encoding can compare, so aggregates still fall through uncongruent.

bound_dynamic_object_size()

void goto_symext::bound_dynamic_object_size ( const code_assign2t & code )

protected

Bound at PTRDIFF_MAX the object size an assignment records, reporting a constant request that exceeds it rather than assuming it away.

Only an assignment to a dynamic_size2t records one – a VLA declaration is the only way a stack object's size reaches symex, and renaming has exposed its constness by then. R40.

Parameters

code	The assignment, unrenamed.

branch_decision_guard()

expr2tc goto_symext::branch_decision_guard ( const expr2tc & guard ) const

protected

The guard a branch decision is read from.

is_false/is_true are syntactic, so they hold only once the guard is folded to a literal, and do_simplify is a no-op under –no-simplify. Returns an unconditionally simplified copy under that flag, so a bounded loop can still be seen to exit, and guard untouched otherwise.

Parameters

guard

The renamed branch guard.

bump_call()

void goto_symext::bump_call ( const code_function_call2t & func_call, const std::string & symname )

protected

calculate_element_count()

expr2tc goto_symext::calculate_element_count ( const expr2tc & size_bytes, const expr2tc & elem_size )

protected

Calculate number of elements from byte size.

Converts a size in bytes to a number of elements by dividing by the element size, handling potential rounding and alignment issues.

Parameters

size_bytes	Total size in bytes.
elem_size	Size of each element in bytes.

Returns

Expression representing the number of elements.

calculate_old_element_count()

expr2tc goto_symext::calculate_old_element_count ( const expr2tc & old_base_array, const type2tc & elem_type, bool old_is_array )

protected

Calculate the number of elements in the old memory object.

Determines how many elements of the specified type exist in the old allocated memory, accounting for whether it's an array type or raw bytes.

Parameters

old_base_array	The base array of the old memory object.
elem_type	The type of elements being counted.
old_is_array	Whether the old object is a typed array.

Returns

Expression representing the number of old elements.

chase_copies()

bool goto_symext::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.

Used by path-guard subsumption to compare branch conditions from different scopes structurally; the result is for comparison only and is never fed back into the symex state or the SSA equation.

Parameters

expr	Expression to rewrite; modified in place.

Returns

true if any substitution was made.

check_incremental()

bool goto_symext::check_incremental ( const expr2tc & expr, const std::string & msg )

protected

Perform incremental SMT solving for assert and assume statements.

Parameters

expr	Expression that must be checked.
msg	Textual message explaining assertion.

Returns

True if incremental solving conclusively resolved the claim (held, or refuted with a counterexample recorded); false if the result was unknown.

check_stack_size()

void goto_symext::check_stack_size ( const expr2tc & expr, const std::string & subject = "" )

protected

Account expr's storage against the current frame and claim that neither –stack-limit nor –total-stack-limit is exceeded.

Parameters

expr	Expr whose type gives the storage to account for.
subject	Suffix naming what was being placed on the stack.

claim()

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

protectedvirtual

Perform an assertion.

Encodes an assertion that the expression claimed is always true. This adds the requirement that the current state guard is true as well.

Parameters

expr	Expression that must always be true.
msg	Textual message explaining assertion.

Reimplemented in execution_statet, and schedule_execution_statet.

claim_nonnull_operand()

void goto_symext::claim_nonnull_operand ( const expr2tc & ptr, const expr2tc & n, const std::string & func )

protected

Claims ptr is not NULL unless n is zero.

claim_not_code()

void goto_symext::claim_not_code ( const expr2tc & guard )

protected

Claim that a memory builtin's operand, on the path guard selects, is not a code object; nothing under –no-pointer-check.

claim_valid_operand()

void goto_symext::claim_valid_operand ( const expr2tc & ptr, const expr2tc & n, const std::string & func )

protected

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.

copy_memory_content()

void goto_symext::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 )

protected

Copy memory content from old to new allocation.

Implements the bulk copying of preserved data during realloc, copying the minimum of old and new element counts to preserve existing data while respecting the new allocation size.

Parameters

old_base_array	The source array containing existing data.
new_array	The destination array for copied data.
old_elem_count	Number of elements in the old allocation.
new_elem_count	Number of elements in the new allocation.
elem_type	Type of elements being copied.
old_is_array	Whether old object is accessed as typed array.
guard	Guard condition for the copy operations.

copy_old_objects()

void goto_symext::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 )

protected

Copy each object a reallocated pointer may point to into the new allocation, guarded by the pointer pointing to it.

Parameters

old_objects	The objects found by an internal dereference.
new_array	The destination array for copied data.
new_elem_count	Number of elements in the new allocation.
elem_type	Element type of the new allocation.
guard	Guard condition for the copy operations.

copy_single_element()

void goto_symext::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 )

protected

Copy a single element between old and new arrays.

Performs the copying of one element from the old memory location to the new one, handling type conversions and array vs non-array access patterns.

Parameters

old_base_array	The source array to copy from.
new_array	The destination array to copy to.
idx	Index of the element to copy.
elem_type	Type of elements in the old array.
new_elem_type	Type of elements in the new array.
old_is_array	Whether old object is accessed as typed array.
guard	Guard condition for this copy operation.

create_dynamic_memory_symbol()

expr2tc goto_symext::create_dynamic_memory_symbol ( const type2tc & elem_type, const expr2tc & size_expr, const std::string & name_prefix )

protected

Create a new dynamic memory symbol.

Generates a fresh symbol representing dynamically allocated memory, with appropriate array type and symbolic size for use in realloc and other dynamic memory operations.

Parameters

elem_type	Type of elements in the dynamic array.
size_expr	Expression representing the array size.
name_prefix	Prefix for generating the symbol name.

Returns

Symbol expression representing the new dynamic memory.

create_result_pointer()

expr2tc goto_symext::create_result_pointer ( const expr2tc & new_array, const type2tc & lhs_type )

protected

Create result pointer from newly allocated array.

Constructs the appropriate pointer expression that points to the base of the newly allocated dynamic memory array, with proper type casting.

Parameters

new_array	The newly allocated array symbol.
lhs_type	The expected type of the result pointer.

Returns

Pointer expression to the new array.

default_replace_dynamic_allocation()

void goto_symext::default_replace_dynamic_allocation ( expr2tc & expr )

protected

defer_assumption()

void goto_symext::defer_assumption ( const expr2tc & assumption )

protectedvirtual

Hold back the assume that ends a path at a Python assert (#8242).

A later Python assert fails whether or not an earlier one ended the path, so only other claims need it; claim() emits it before them. Keeping it out of the equation until then spares each later assertion and guard check the earlier assertions' constraints.

Parameters

assumption

The assert's condition.

Reimplemented in execution_statet.

dereference()

void goto_symext::dereference ( expr2tc & expr, dereferencet::modet mode, bool block_assertions = false )

protected

Dereference an expression.

Finds dereference expressions within expr, takes the set of things that it might point at, according to value set tracking, and builds an if-then-else list of concrete references that it might point at.

Parameters

expr	Expression to eliminate dereferences from.
mode	The dereference mode.
block_assertions	Suppress the pointer-safety claims this dereference would otherwise record. Only for probing what a pointer may designate before deciding whether the access happens.

determine_fallback_element_type()

type2tc goto_symext::determine_fallback_element_type ( const sideeffect2t & code, const expr2tc & lhs )

protected

Determine fallback element type for realloc.

When the old object's type cannot be determined, selects an appropriate fallback element type based on the realloc context and target type.

Parameters

code	The realloc side effect being processed.
lhs	The left-hand side target of the realloc.

Returns

Appropriate element type to use as fallback.

do_simplify()

void goto_symext::do_simplify ( expr2tc & expr )

protectedvirtual

Perform simplification on an expression.

Essentially is just a call to simplify, but is guarded by the –no-simplify option being turned off.

Parameters

expr	Expression to simplify, in place.

finalize_realloc_result()

void goto_symext::finalize_realloc_result ( const expr2tc & lhs, const expr2tc & result, const expr2tc & new_array, const guard2tc & guard, const expr2tc & realloc_size, const expr2tc & alloc_fail )

protected

Finalize the result of a realloc operation.

Creates the final assignment of the realloc result pointer to the lhs, handling both successful allocation and failure cases. Updates pointer tracking and validity information for the newly allocated memory.

Parameters

lhs	Left-hand side expression to receive the realloc result.
result	The result pointer expression from realloc.
new_array	The newly allocated array symbol.
guard	Guard condition for this assignment.
realloc_size	The size parameter passed to realloc.
alloc_fail	Failure condition from model_allocation_failure, or nil when realloc cannot fail.

flush_deferred_assumptions()

void goto_symext::flush_deferred_assumptions ( )

protected

Before a claim that needs them, emit every deferred assumption into the target equation.

format_printf_output()

bool goto_symext::format_printf_output ( const code_printf2t & call, size_t fmt_idx, printf_formattert & formatter, bool & constant_args )

protected

Run formatter over an unrenamed printf-family call; false when the format is not a constant.

constant_args is set when every argument is a constant.

get_dynamic_counter()

virtual unsigned int & goto_symext::get_dynamic_counter ( )

protectedpure virtual

Fetch reference to global dynamic object counter.

Returns

Reference to global dynamic object counter.

Implemented in execution_statet.

get_nondet_counter()

virtual unsigned int & goto_symext::get_nondet_counter ( )

protectedpure virtual

Fetch reference to global nondet object counter.

Returns

Reference to global nondet object counter.

Implemented in execution_statet.

get_symex_result()

goto_symext::symex_resultt goto_symext::get_symex_result

(

)

Create a symex result for this run.

get_unwind()

bool goto_symext::get_unwind ( const symex_targett::sourcet & source, const BigInt & unwind )

protected

Test whether unwinding bound has been exceeded.

This looks up a look number, checks the limit on unwindings against the given number of unwinds already performed, and returns whether that limit has been exceeded.

Parameters

source	Program location to check for loops against.
unwind	Number of unwinds that have already occured.

Returns

True if we've unwound past the unwinding limit.

get_unwind_recursion()

bool goto_symext::get_unwind_recursion ( const irep_idt & identifier, BigInt unwind )

protected

Discover whether recursion bound has been exceeded.

See also

get_unwind

Parameters

identifier	Name of function to consider recursion of.
unwind	Number of times its been unwound already.

Returns

True if unwind recursion has been exceeded.

guard_identifier()

expr2tc goto_symext::guard_identifier ( )

inline

Return identifier for goto guards.

These guards are symbolic names for the truth of a guard on a GOTO jump. Assertions and other activity during the course of symbolic execution encode these execution guard in them.

Returns

Symbol expression naming the guard

handle_conditional()

bool goto_symext::handle_conditional ( const expr2tc & lhs, const if2t & if_effect, const guard2tc & guard )

protected

Handle conditional expressions (if2t) in the symbolic execution.

Parameters

lhs	The left-hand side expression (target of the assignment).
if_effect	The conditional expression (if2t) to be handled, containing the condition, true branch, and false branch.

This function returns true if there is a sideeffect.

handle_realloc_zero_size()

bool goto_symext::handle_realloc_zero_size ( const expr2tc & lhs, const sideeffect2t & code, const guard2tc & guard, const expr2tc & realloc_size )

protected

Handle realloc with zero size parameter.

Implements the special case where realloc is called with size 0, which according to C standard may free the memory and return NULL or a unique pointer that should not be dereferenced.

Parameters

lhs	Left-hand side expression to receive the result.
code	The realloc side effect being processed.
guard	Guard condition for this operation.
realloc_size	The size parameter (should be zero).

Returns

True if zero size case was handled, false otherwise.

handle_sideeffect()

void goto_symext::handle_sideeffect ( const expr2tc & lhs, const sideeffect2t & effect, const guard2tc & guard )

protected

Handle side effects in the symbolic execution.

Parameters

lhs	The left-hand side expression (target of the assignment).
effect	The side effect expression to be handled, typically one of the sideeffect2t kinds like malloc, realloc, etc.

This function does not return any value; it modifies the symbolic execution state based on the side effect encountered.

intrinsic_builtin_object_size()

void goto_symext::intrinsic_builtin_object_size ( const code_function_call2t & func_call, reachability_treet & art )

protected

Implements GCC's __builtin_object_size intrinsic for object size determination.

Parameters

func_call	Function call with 2 operands: pointer and type parameter
art	Reachability tree (unused)

Returns the size in bytes of the object pointed to by the first argument.

The type parameter (0–3) controls the result:

• type 0: maximum accessible size of the whole object
• type 1: remaining size after the current pointer offset
• type 2: like type 0, but returns 0 instead of (size_t)-1 if unknown
• type 3: like type 1, but returns 0 instead of (size_t)-1 if unknown

Fallback behavior when the object cannot be determined:

• For type 0/1 → returns (size_t)-1
• For type 2/3 → returns 0

intrinsic_get_object_size()

void goto_symext::intrinsic_get_object_size ( const code_function_call2t & func_call, reachability_treet & art )

protected

Returns the size of the object.

If the object is invalid, then this function will return 0

intrinsic_get_thread_data()

void goto_symext::intrinsic_get_thread_data ( const code_function_call2t & call, reachability_treet & art )

protected

Perform get_thread_data; get thread startup information.

intrinsic_get_thread_id()

void goto_symext::intrinsic_get_thread_id ( const code_function_call2t & call, reachability_treet & art )

protected

Perform get_thread_id; return the current thread identifier.

intrinsic_havoc_object()

void goto_symext::intrinsic_havoc_object ( const code_function_call2t & call )

protected

Perform havoc_object; assign nondet to every object the argument may point to, whole and of any size.

k-induction emits it at a loop head for a pointer the loop writes through at offsets it cannot bound.

intrinsic_init_thread_local()

void goto_symext::intrinsic_init_thread_local ( reachability_treet & art )

protected

Perform init_thread_local; seeds each __thread-qualified global to its static initializer in the active thread's renaming scope.

intrinsic_kill_monitor()

void goto_symext::intrinsic_kill_monitor ( reachability_treet & art )

protected

Terminate the monitor thread.

intrinsic_memchr()

void goto_symext::intrinsic_memchr ( reachability_treet & art, const code_function_call2t & func_call )

protected

Intrinsic call for C memchr function call.

Intrinsic for C memchr.

This will either invoke our operational model (at string.c) or build the result pointer directly: it scans the first n bytes of the object pointed to by buf and returns a pointer to the first byte equal to the (unsigned char) value ch, or NULL if no such byte is found.

Parameters

art
func_call	memchr function call

memchr(const void *buf, int ch, size_t n) scans the first n bytes of the object pointed to by buf for the first byte equal to (unsigned char)ch and returns a pointer to it, or NULL if no such byte appears in those n bytes.

Instead of unwinding the operational-model loop (one branch per byte), we read the n candidate bytes with byte_extract and fold them into a single nested-ite pointer expression:

res = ite(byte[0] == ch, buf + 0, ite(byte[1] == ch, buf + 1, ... ite(byte[n-1] == ch, buf + (n-1), NULL)))

Building from the last position outward keeps the first match as the outermost selected arm. ch is symbolic-friendly (the comparison is encoded); only n must be a known constant. If the object/offset cannot be resolved to constants we bump to the __memchr_impl loop.

intrinsic_memcmp()

void goto_symext::intrinsic_memcmp ( reachability_treet & art, const code_function_call2t & func_call )

protected

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.

Falls back to the C __memcmp_impl loop otherwise.

intrinsic_memcpy()

void goto_symext::intrinsic_memcpy ( reachability_treet & art, const code_function_call2t & func_call )

protected

Intrinsic call for C memcpy function call.

This will either invoke our operational model (at string.c) or try to compute the resulting value directly

Parameters

art
func_call	memcpy function call

intrinsic_memcpy_impl()

void goto_symext::intrinsic_memcpy_impl ( reachability_treet & art, const code_function_call2t & func_call, const std::string & bump_name )

protected

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.

intrinsic_memmove()

void goto_symext::intrinsic_memmove ( reachability_treet & art, const code_function_call2t & func_call )

protected

Models __ESBMC_memmove.

Identical optimisation to memcpy (the new value is built from the current src/dst bytes before assigning, so overlapping regions are correct); only the C fallback differs.

intrinsic_memset()

void goto_symext::intrinsic_memset ( reachability_treet & art, const code_function_call2t & func_call )

protected

Intrinsic call for C memset function call.

This function will try to initialize the object pointed by the address in a smarter way, minimizing the number of assignments.

This will either invoke our operational model (at string.c) or try to compute the resulting value directly

Parameters

art
func_call	memset function call

This is intend to optimize the behavior of a memset operation:

memset(void* ptr, int value, size_t num_of_bytes)

• ptr can point to anything. We have to add checks!
• value is interpreted as a uchar.
• num_of_bytes must be known. If it is nondet, we will bump the call

In plain C, the objective of a call such as:

int a; memset(&a, value, num)

Would generate something as:

int temp = 0; for(int i = 0; i < num; i++) temp = byte | (temp << 8); a = temp;

This is just a simplification for understanding though. During the instrumentation size checks will be added, and also, the original bytes from a that were not overwritten must be mantained! Arrays will need to be added up to an nth element.

In ESBMC though, we have 2 main methods of dealing with memory objects:

A. Heap objects, which are valid/invalid. They are the easiest to deal with, as the dereference will actually return a big array of char to us. For this case, we can just overwrite the members directly with the value

B. Stack objects, which are typed. It will be hard, this will require operations which depends on the base type and also on padding.

intrinsic_really_atomic_begin()

void goto_symext::intrinsic_really_atomic_begin ( reachability_treet & art )

protected

Really atomic start/end - atomic blocks that just disable ileaves.

intrinsic_really_atomic_end()

void goto_symext::intrinsic_really_atomic_end ( reachability_treet & art )

protected

Really atomic start/end - atomic blocks that just disable ileaves.

intrinsic_register_monitor()

void goto_symext::intrinsic_register_monitor ( const code_function_call2t & call, reachability_treet & art )

protected

Register which thread is the monitor thread.

intrinsic_set_thread_data()

void goto_symext::intrinsic_set_thread_data ( const code_function_call2t & call, reachability_treet & art )

protected

Perform set_thread_state; store thread startup information.

intrinsic_spawn_thread()

void goto_symext::intrinsic_spawn_thread ( const code_function_call2t & call, reachability_treet & art )

protected

Perform spawn_thread; Generates a new thread at a named function.

intrinsic_switch_from()

void goto_symext::intrinsic_switch_from ( reachability_treet & arg )

protected

Yield, always switching away from this thread.

intrinsic_switch_from_monitor()

void goto_symext::intrinsic_switch_from_monitor ( reachability_treet & art )

protected

Context switch from the monitor thread.

intrinsic_switch_to()

void goto_symext::intrinsic_switch_to ( const code_function_call2t & c, reachability_treet & art )

protected

Perform switch_to; switches control to explicit thread ID.

intrinsic_switch_to_monitor()

void goto_symext::intrinsic_switch_to_monitor ( reachability_treet & art )

protected

Context switch to the monitor thread.

intrinsic_terminate_thread()

void goto_symext::intrinsic_terminate_thread ( reachability_treet & art )

protected

Perform terminate_thread; Record thread as terminated.

intrinsic_yield()

void goto_symext::intrinsic_yield ( reachability_treet & arg )

protected

Perform yield; forces a context switch point.

invalidate_object()

void goto_symext::invalidate_object ( const expr2tc & ptr )

protected

Clear the valid bit of the object ptr points to, with no free checks.

is_assume_false()

bool goto_symext::is_assume_false ( const expr2tc & assumption )

protected

Incrementally check the assumption.

is_python_gc_object()

bool goto_symext::is_python_gc_object ( const symbolt * base ) const

protected

Whether base is a user-defined Python class instance that follows garbage-collected lifetime semantics (issue #4773).

Such objects are kept alive past their defining frame so references captured into a returned or otherwise escaping aggregate stay valid, matching CPython (which heap- allocates objects and frees them only when unreachable). Internal Python model aggregates (tuples, dicts, and the list/slice/object/type operational-model structs) are excluded: they manage their own representation and must not have frame teardown skipped.

is_valid_object()

bool goto_symext::is_valid_object ( const symbolt & symbol )

protected

Decide if symbol is valid or not.

i.e., whether it's live or not.

Returns

True if symbol is valid.

key_intrinsic_pointer_reads()

void goto_symext::key_intrinsic_pointer_reads ( const code_function_call2t & call, const irep_idt & id )

protected

Key the reads the memcpy/memmove/memcmp/memchr intrinsics perform, which symex carries out internally rather than through a dereference (#7826).

loop_bound_exceeded()

void goto_symext::loop_bound_exceeded ( const expr2tc & guard )

protected

Encode unwinding assertions and assumption.

If unwinding assertions are on, assert that the unwinding bound is not exceeded. If partial loops are off, assume that the unwinding bound was not exceeded. Otherwise, just continue execution.

Parameters

guard

Current state guard.

make_return_assignment()

bool goto_symext::make_return_assignment ( expr2tc & assign, const expr2tc & code_return )

protected

Create assignment for return statement.

Generate an assignment to the return variable from this return statement.

Parameters

assign	Assignment expression. Output.
code	The return statement we're interpreting.

Returns

True if a return assignment was generated.

materialise_old_snapshot()

expr2tc goto_symext::materialise_old_snapshot ( const expr2tc & value, const guard2tc & guard )

protected

Give a value storage of its own, for __ESBMC_old.

Give value storage of its own and return a reference to it, so that the caller has something addressable holding the pre-state value.

Only an lvalue has an address, and dereference lowering can turn a read through an untyped allocation into a value rebuilt from bytes. Snapshot such a value into a symbol so the caller has something to point at.

Returns

A reference to the new storage, holding value.

memcmp_resolve_operand()

bool goto_symext::memcmp_resolve_operand ( const expr2tc & ptr, unsigned long number_of_bytes, expr2tc & object, uint64_t & offset, uint64_t & avail_bytes, bool rename_object = true )

protected

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.

Returns false (bump to the C loop) on any miss.

memcpy_finish()

void goto_symext::memcpy_finish ( const code_function_call2t & func_call, const expr2tc & dst_arg, const expr2tc & src_arg, const expr2tc & n_arg )

protected

The NULL checks and return-value assignment shared by both of intrinsic_memcpy_impl's paths.

memcpy_symbolic_length()

bool goto_symext::memcpy_symbolic_length ( const expr2tc & dst_arg, const expr2tc & src_arg, const expr2tc & n_arg )

protected

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).

Mirrors intrinsic_memcmp's symbolic-n path: bound the copy by the objects' own widths, guard each byte position with i < n, and claim n <= that bound so an over-long copy is still reported. Returns false when the operands cannot be resolved, leaving the caller to bump.

merge_gotos()

void goto_symext::merge_gotos ( )

protected

Merge converging states into current state.

Jumps forwards are handled by recording a merge of the current state in the future; then when we hit that future state, a phi function is performed that joins the states converging at this point, according to the truth of their guards.

merge_interval_domain()

void goto_symext::merge_interval_domain ( const statet::merge_statet & merge_state )

protected

Join a parked path's interval domain into the shared one; a path parked without a snapshot sends the domain to top.

merge_locality()

void goto_symext::merge_locality ( const statet::merge_statet & merge_state )

protected

merge_value_sets()

void goto_symext::merge_value_sets ( const statet::merge_statet & merge_state )

protected

Merge pointer tracking value sets in a phi function.

See merge_gotos - when we're merging states together due to previous jumps, this function implements the merging of pointer tracking data.

Parameters

merge_state

Previously recorded merge snapshot to be merged in.

model_allocation_failure()

expr2tc goto_symext::model_allocation_failure ( const expr2tc & result, const expr2tc & old_ptr, const guard2tc & guard, const expr2tc & over_cap, expr2tc & alloc_fail )

protected

Model allocation failure behavior for realloc.

Creates conditional logic to handle the case where realloc fails to allocate memory, returning NULL while preserving the original pointer's validity according to C standard semantics.

Parameters

result	The result pointer from realloc attempt.
old_ptr	The original pointer being reallocated.
guard	Guard condition for this modeling.
alloc_fail	Set to the failure condition, or nil when realloc cannot fail.

Returns

Expression representing the final result considering failure.

named_object()

expr2tc goto_symext::named_object ( const expr2tc & base ) const

protected

base if it is a named object, nil otherwise.

note_bounded_loop_truncation()

virtual void goto_symext::note_bounded_loop_truncation ( )

inlineprotectedvirtual

Records that a loop was cut off at the unwinding bound with nothing to flag it.

Virtual because –schedule runs each path in its own execution state, so the count also has to accumulate outside them.

Reimplemented in execution_statet, and schedule_execution_statet.

offer_malloc_zero_null()

void goto_symext::offer_malloc_zero_null ( const expr2tc & size, expr2tc & rhs, guard2tc & alloc_guard )

protected

Offer both outcomes C17 7.22.3p1 permits for a zero-sized malloc, under –malloc-zero-is-null.

Widens alloc_guard and rhs.

operator=()

goto_symext & goto_symext::operator=

(

const goto_symext &

sym

)

path_guard_decides()

tvt::tv_enumt goto_symext::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.

Whether the accumulated path guard already decides new_guard: TV_TRUE when a conjunct matches it, TV_FALSE when one matches its negation, TV_UNKNOWN otherwise.

See symex_goto.cpp for the matching discipline.

Conjuncts are usually guard SYMBOLS (possibly negated); level2 renaming never substitutes into an already-L2 symbol, so their defining conditions are looked up in guard_definitions instead. Both sides are rewritten onto the canonical copy-chain basis — conditions from different scopes name the same value through different symbol generations — and compared structurally; comparison negations are canonicalized by the simplifier. The rewritten forms are for matching only and never reach the SSA equation.

phi_function()

void goto_symext::phi_function ( const statet::merge_statet & merge_state )

protected

Join a previous jump's merge snapshot into the active thread state.

This combines together two thread states by using if-then-elses to decide the new value of a variable, according to the truth of the guards of the states being joined.

Parameters

merge_state

Previous jump snapshot to be merged into the current state.

pop_frame()

void goto_symext::pop_frame ( )

protected

Pop a stack frame.

This frees/removes the top stack frame, and removes any relevant local variables from the l2 renaming, and value set tracking.

prefix_index()

goto_symext::conjunct_indext goto_symext::prefix_index

(

const guard2tc &

guard

)

The conjunct index of guard, which must not be true.

Extends the index of the longest prefix already in guard_prefix_index.

printf_output_length()

expr2tc goto_symext::printf_output_length ( const code_printf2t & call, size_t fmt_idx, size_t & max_len )

protected

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.

printf_return_length()

expr2tc goto_symext::printf_return_length ( const expr2tc & lhs, const code_printf2t & call, size_t fmt_idx )

protected

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.

Nil when unknown.

propagate_assume_equality()

void goto_symext::propagate_assume_equality ( const expr2tc & the_assumption )

protected

Lift var == const from an assume into the level2 constant propagator so subsequent renames of var substitute the constant directly.

Called from symex_assume() after the assumption has been recorded into the SSA target, so the constraint itself is preserved and the lift only affects future renames.

Peels outer typecasts (the C frontend wraps the equality as (bool)(int)(x == k) for __VERIFIER_assume-style intrinsics), matches symbol == const or const == symbol, and writes the constant into the level2 entry for the symbol via cur_state->assignment.

Skips IEEE-754 zero constants: +0.0 and -0.0 compare equal under IEEE equality but have distinct bit patterns, so propagating either would silently fold signbit-sensitive code (1.0/x, copysign, bit reinterpretation) and mask real bugs.

record_copy_definition()

void goto_symext::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.

The rhs is canonicalized through existing chains first and dropped if the canonical form exceeds max_copy_definition_nodes.

Parameters

renamed_lhs	L2 symbol generation just assigned.
rhs	Renamed, simplified assignment rhs.

record_frame_alloca()

void goto_symext::record_frame_alloca ( const expr2tc & lhs, const expr2tc & object, bool is_malloc )

protected

Records an alloca'd object on the current frame, to die when it returns.

record_guard_definition()

void goto_symext::record_guard_definition	(	const expr2tc &	guard_expr,
		const expr2tc &	rhs )

Remember a guard generation's defining condition for path_guard_decides.

record_parked_path()

virtual void goto_symext::record_parked_path ( goto_programt::const_targett , statet::merge_state_listt::iterator  )

inlineprotectedvirtual

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 in execution_statet.

record_property_verdict()

void goto_symext::record_property_verdict ( const std::string & msg, property_verdictt verdict, const std::string & note = "" )

protected

Record a verdict for the claim being symbolically executed.

Used for claims symex discharges itself, so that they are reported once per run alongside the ones the solver discharges, rather than once per thread interleaving.

Parameters

msg	Textual message explaining the claim.
verdict	Outcome to record.
note	How the verdict was reached, when it needs qualifying.

recover_va_list_args()

bool goto_symext::recover_va_list_args ( const code_printf2t & call, size_t fmt_idx, std::list< expr2tc > & out )

protected

Recover the variadic arguments hidden behind a va_list operand of a v*printf-family call (vprintf/vfprintf/vsprintf/vsnprintf/vasprintf).

Succeeds only under conservative conditions guaranteeing the mapping is exact: the call must sit in the variadic function's own frame, the va_list operand must be one of that function's own non-parameter locals, and no va_arg may have been consumed in the activation yet. On success fills out with the activation's L2-renamed va_arg values (in declaration order) and returns true; otherwise returns false and the caller must keep treating the arguments as unreliable (sound fallback).

Parameters

call	The original (unrenamed) printf side effect.
fmt_idx	Index of the format-string operand within call.
out	Receives the recovered argument expressions on success.

reject_untyped_isinstance()

void goto_symext::reject_untyped_isinstance ( const expr2tc & value )

protected

release_symex_caches()

void goto_symext::release_symex_caches ( )

inline

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.

replace_dynamic_allocation()

void goto_symext::replace_dynamic_allocation ( expr2tc & expr )

protected

Replace ireps regarding dynamic allocations with code.

Things like "invalid-object" and suchlike are replaced here with references to array members, or more elaborate expressions, representing how that information is actually stored in the resulting SMT. In the past this has been done in the solver backend, but that seems slightly the wrong place.

Parameters

expr	Expression we're replacing the contents of.

replace_dynamic_size()

void goto_symext::replace_dynamic_size ( expr2tc & expr )

protected

Size the object DYNAMIC_SIZE names, falling back to the heap-only table.

replace_nondet()

void goto_symext::replace_nondet ( expr2tc & expr )

protected

Replace nondet func calls with nondeterminism.

Creates a new nondeterministic symbol, with a globally unique counter encoded into its name. Is left as a free variable.

Parameters

expr	Expr to search for nondet symbols.

replace_races_check()

void goto_symext::replace_races_check ( expr2tc & expr )

protected

replace_valid_object()

void goto_symext::replace_valid_object ( expr2tc & expr )

protected

Decide VALID_OBJECT / DEALLOCATED_OBJ against the object the pointer names.

resolve_by_value_set()

bool goto_symext::resolve_by_value_set ( expr2tc & expr, const expr2tc & ptr, const std::function< expr2tc(const expr2tc &)> & resolve )

protected

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.

Neither is maintained for automatic storage, so the solver may pick a live stack object invalid or size it arbitrarily, and a caller cannot discharge an is_fresh precondition it plainly satisfies (#7464).

Replace expr, a query about ptr, by what resolve answers for each object the value set says ptr may address. With several candidates, or one resolve cannot answer for, each answer is selected by SAME-OBJECT and the heap-only default covers the rest (#9000).

resolve_dynamic_size_by_value_set()

bool goto_symext::resolve_dynamic_size_by_value_set ( expr2tc & expr )

protected

Size a heap object by its allocation, and an object with automatic or static storage by its type.

DYNAMIC_SIZE is maintained for the heap alone, so it says nothing about the extent an is_fresh precondition has to compare against for such an object (#7464).

resolve_valid_object_by_value_set()

bool goto_symext::resolve_valid_object_by_value_set ( expr2tc & expr, const expr2tc & obj_ref )

protected

Decide VALID_OBJECT from the object the value set names, if it names one.

is_valid_object() answers false for every automatic object: the scope tracking it would need is #if 0'd out at the end of this file. The syntactic path never reaches it, because a named object returns its declared extent and drops this conjunct. Do the same once the value set has named the object, which is valid for as long as it is live (#7464); the extent is checked separately.

rewrite_conjunct()

expr2tc goto_symext::rewrite_conjunct

(

const expr2tc &

conjunct

)

A path-guard conjunct rewritten onto the canonical basis path_guard_decides compares on.

run_builtin()

bool goto_symext::run_builtin ( const code_function_call2t & call, const std::string & symname )

protected

Run a builtin, something prefixed with __builtin.

This looks through a set of builtin functions that are implemented in ESBMC, and calls the appropriate one.

Parameters

call	Function call being performed.
symname	Name of builtin we're calling.

Returns

true if we handled the builtin

run_intrinsic()

void goto_symext::run_intrinsic ( const code_function_call2t & call, reachability_treet & art, const std::string & symname )

protected

Run an intrinsic, something prefixed with __ESBMC.

This looks through a set of intrinsic functions that are implemented in ESBMC, and calls the appropriate one. Examples include starting a thread, ending a thread, switching to another thread.

Parameters

call	Function call being performed.
art	Reachability tree we're operating on.
symname	Name of intrinsic we're calling.

run_next_function_ptr_target()

bool goto_symext::run_next_function_ptr_target ( bool first )

protected

Setup next function in a chain of func ptr calls.

See also

symex_function_call_deref

Parameters

first

Whether this is the first func ptr invocation.

Returns

True if a function pointer invocation was set up.

simplify_python_builtins()

void goto_symext::simplify_python_builtins ( expr2tc & expr )

protected

snapshot_interval_domain()

void goto_symext::snapshot_interval_domain ( statet::merge_statet & merge_state )

protected

Record the online interval domain in a path being parked, so merge_interval_domain can join it back in (#8047).

sprintf_output()

expr2tc goto_symext::sprintf_output ( const code_printf2t & call, size_t fmt_idx, const type2tc & char_type, std::vector< expr2tc > & chars )

protected

The output of an unrenamed sprintf or snprintf call: its characters before the NUL in chars, and its length, nil when unknown.

stack_checks_enabled()

bool goto_symext::stack_checks_enabled ( ) const

inlineprotected

True when either stack limit is on.

The DECL, DEAD and return sites must agree, or the accounting desynchronises from the frames.

string_length()

expr2tc goto_symext::string_length ( const expr2tc & ptr, size_t & max_len )

protected

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.

symex_alloca()

expr2tc goto_symext::symex_alloca ( const expr2tc & lhs, const sideeffect2t & code, const guard2tc & guard )

protected

Symbolic implementation of alloca.

symex_asprintf_buffer()

void goto_symext::symex_asprintf_buffer ( const expr2tc & strp, const expr2tc & retval )

protected

Point an asprintf/vasprintf call's strp at a fresh heap buffer of retval + 1 bytes, allocated only when retval is non-negative.

When the result is discarded (retval nil) the buffer is 1 byte.

symex_assert()

void goto_symext::symex_assert ( )

protected

Interpret an ASSERT instruction.

symex_assign()

void goto_symext::symex_assign ( const expr2tc & code, const bool hidden = false, const guard2tc & guard = guard2tc() )

protectedvirtual

Make symbolic assignment.

Renames things; records assignment in symex target, and all the relevant renaming and value set tracking objects. The primary task of this routine is to rewrite assignments to arrays, structs, and byte_selects into the equivalent uses of WITH, or byte_update, and so forth. The end result is a single new value to be bound to a new symbol.

Parameters

code	Code to assign; with lhs and rhs.
hidden	Whether the resulting SSA steps are marked hidden (default visible)
guard	A guard for the assignment, true by default

Reimplemented in execution_statet.

symex_assign_array()

void goto_symext::symex_assign_array ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to an array.

lhs transformed to the container of the array, or the symbol for its destination. rhs converted to a WITH statement, updating the contents of the original array with the value of the original rhs.

Parameters

lhs	Array to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to symbol
guard	Guard; intent unknown

symex_assign_array_structure()

void goto_symext::symex_assign_array_structure ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to an array literal.

Mirrors symex_assign_structure for a constant_array lhs: project each element out and recurse, so a reconstituted array (e.g. an array-typed struct member surfaced by symex_assign_structure) is assigned element-wise instead of hitting the unhandled-lhs abort.

Parameters

lhs	Array literal to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to the array
guard	Guard of the current assignment

symex_assign_bitfield()

void goto_symext::symex_assign_bitfield ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

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.

Such "masking" is typically applied to 'index', 'byte_extract' or 'concat'.

Parameters

lhs	Bitfield to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to lhs
guard	Assignment guard.

symex_assign_byte_extract()

void goto_symext::symex_assign_byte_extract ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to a byte extract.

Results in a byte update of the relevant part of the lhs with the right hand side at the appropriate position. Currently a problem , as assignments of something that's bigger than a byte fails.

Parameters

lhs	Byte extract to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to lhs
guard	Guard; intent unknown

symex_assign_concat()

void goto_symext::symex_assign_concat ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Assign through a 'concat' operation.

These are generated when we fail to dereference something correctly, and generate a series of byte operations that we then stitch back together. When that's on the left hand side of an expression, this means that we have to decompose the right hand side into a series of byte assignments.

Parameters

lhs	Concat to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to lhs
guard	Assignment guard.

symex_assign_extract()

void goto_symext::symex_assign_extract ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to an extract irep.

Currently these extract assignments can crop up when we're assigning into a bitfield. We can't rewrite the assignment in the front end, because there isn't enough context there to know whether an expression is on the lhs or rhs of an expression. Thus we have to take the operand of the extract irep, and read/modify/write it.

Parameters

lhs	Extract irep to assign into
rhs	Value to assign to bitfield
guard	Guard of the current assignment

symex_assign_if()

void goto_symext::symex_assign_if ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to an "if".

This ends up being two assignments, one to one branch of the if, the other to the other. The appropriate guard is executed in either case.

Parameters

lhs	"If" to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to lhs
guard	Guard; intent unknown

symex_assign_member()

void goto_symext::symex_assign_member ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to a struct.

Exactly like with arrays, but with structs and members.

See also

symex_assign_array

Parameters

lhs	Struct to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to lhs
guard	Guard; intent unknown

symex_assign_rec()

void goto_symext::symex_assign_rec ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc full_rhs, guard2tc & guard, const bool hidden )

protected

Recursively perform symex assign.

See also

symex_assign

symex_assign_structure()

void goto_symext::symex_assign_structure ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to a structure.

Performed when a constant structure appears on the left hand side. These kinds of assignments are permitted by C99, and some C++ fudge. Decomposes structure into each particular field, and encodes an assignment for each pair of fields.

(It's not intuitive that one may assign to a /constant/ structure, however a number of pieces of code need to be able to create structures out of thin air, or more often an array of bytes. In lieu of better distinction between a struct literal and a group of values arranged as a structure, the constant_struct irep is used).

Parameters

lhs	Symbol to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to symbol
guard	Guard; intent unknown

symex_assign_symbol()

void goto_symext::symex_assign_symbol ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to a symbol.

Renames further, performs goto_symex_statet::assignment and symex target assignments.

Parameters

lhs	Symbol to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to symbol
guard	Guard; intent unknown

symex_assign_typecast()

void goto_symext::symex_assign_typecast ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to a typecast irep.

This just ends up moving the typecast from the lhs to the rhs.

Parameters

lhs	Typecast to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to lhs
guard	Guard; intent unknown

symex_assign_union()

void goto_symext::symex_assign_union ( const expr2tc & lhs, const expr2tc & full_lhs, expr2tc & rhs, expr2tc & full_rhs, guard2tc & guard, const bool hidden )

protected

Perform assignment to a union.

Parameters

lhs	Symbol to assign to
full_lhs	The original assignment symbol
rhs	Value to assign to symbol
guard	Guard; intent unknown

symex_assume()

void goto_symext::symex_assume ( )

protected

Interpret an ASSUME instruction.

symex_bounded_math()

void goto_symext::symex_bounded_math ( const code_function_call2t & call, const std::string & function )

protected

_builtin_bounded<function>(x, exact): the bounded result of a transcendental function, from util/arith/transcendental.h.

symex_cpp_delete()

void goto_symext::symex_cpp_delete ( const expr2tc & code )

protected

Symbolic implementation of c++'s delete.

symex_cpp_new()

void goto_symext::symex_cpp_new ( const expr2tc & lhs, const sideeffect2t & code, const guard2tc & guard )

protected

Symbolic implementation of c++'s new.

symex_dead()

void goto_symext::symex_dead ( const expr2tc & code )

protected

Interpret an DEAD instruction.

It calls free on alloca'd symbols and erase the symbols from the propagation map.

symex_decl()

void goto_symext::symex_decl ( const expr2tc & code )

protected

Interpret an DECL instruction.

It creates renamed symbols. These names are all the names of local variables, renamed to level 1. We also bump up the level 1 renaming number, effectively making all the local variables new instances of those variables (which is what entering a function and declaring variables does).

symex_end_of_function()

void goto_symext::symex_end_of_function ( )

protected

End a functions interpretation.

This routine pops a stack frame, and returns control to the caller; except in the case of function pointer interpretation, where we instead switch to interpreting the next pointed to function.

symex_free()

void goto_symext::symex_free ( const expr2tc & expr )

protected

Symbolic implementation of free.

symex_function_call()

void goto_symext::symex_function_call ( const expr2tc & call )

protected

Perform function call.

Handles all kinds of function call instructions, symbols or function pointers.

Parameters

call	Function call we're working on.

symex_function_call_code()

void goto_symext::symex_function_call_code ( const expr2tc & call )

protectedvirtual

Handle a call to a statically-known function: checks recursion bounds, sets up the new frame, assigns arguments, and jumps to the body.

Parameters

call	Function call to interpret.

symex_function_call_deref()

void goto_symext::symex_function_call_deref ( const expr2tc & call )

protectedvirtual

Handle an indirect function call, to a pointer.

Finds all potential targets, and sets up calls to them with the appropriate guards and targets. They are then put in a list, the first one run, then at the end of each of these function calls we switch to the next in the list. Finally, when the insn after the func ptr call is run, all func ptr call states are merged in.

Parameters

call	Function call to interpret.

symex_goto()

void goto_symext::symex_goto ( const expr2tc & old_guard )

protectedvirtual

Perform GOTO jump using current instruction.

Handle a GOTO jump between locations. This isn't just the factor of there being jumps where the guards are nondeterministic, it's that we have to handle editing the unwind bound when these things occur, and set up state merges in the future to handle each path thats taken.

Parameters

old_guard

Branch guard, dereferenced but not yet L2-renamed (symex_goto renames it itself).

Reimplemented in execution_statet.

symex_input()

void goto_symext::symex_input ( const code_function_call2t & expr )

protected

Symbolic implementation of scanf and fscanf.

symex_malloc()

expr2tc goto_symext::symex_malloc ( const expr2tc & lhs, const sideeffect2t & code, const guard2tc & guard )

protected

Symbolic implementation of malloc.

symex_mem()

expr2tc goto_symext::symex_mem ( const bool is_malloc, const expr2tc & lhs, const sideeffect2t & code, const guard2tc & guard )

protected

Wrapper around for alloca and malloc.

symex_mem_inf()

expr2tc goto_symext::symex_mem_inf ( const expr2tc & lhs, const type2tc & base_type, const guard2tc & guard )

protected

Wrapper around for infinite array allocation.

symex_other()

void goto_symext::symex_other ( const expr2tc & code )

protected

Interpret an OTHER instruction.

These can take many forms; memory management functions are OTHERs for example (ideally they should be intrinsics...), but also printf and inline asm are handled here.

symex_printf()

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

protectedvirtual

Symbolic implementation of printf.

Reimplemented in execution_statet.

symex_realloc()

void goto_symext::symex_realloc ( const expr2tc & lhs, const sideeffect2t & code, const guard2tc & guard )

protected

Implementation of realloc.

symex_return()

void goto_symext::symex_return ( const expr2tc & code )

protected

Perform interpretation of RETURN instruction.

Parameters

code	return statement.

symex_sprintf_store()

expr2tc goto_symext::symex_sprintf_store ( const code_printf2t & call )

protected

Store an unrenamed sprintf or snprintf call's output in its destination buffer, when the format bounds that output's length.

Returns the output's length, nil when nothing is stored.

symex_step()

void goto_symext::symex_step ( reachability_treet & art )

virtual

Symbolically execute one instruction.

Essentially a despatcher. Performs some renaming and dereferencing, then hands off an expression to be claimed, or assigned, or possibly for some control flow beating to occur (goto, func call, return). Threading specific operations are handled by execution_statet, which overrides this.

Parameters

art	Reachability tree we're working with.

Reimplemented in execution_statet.

symex_uninterpreted_function()

bool goto_symext::symex_uninterpreted_function ( const code_function_call2t & call, const irep_idt & identifier )

protected

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.

Functional congruence (equal arguments imply an equal result) is enforced downstream by the SMT backend's native uninterpreted-function support, not here. The concrete body, if present, is deliberately ignored (CBMC semantics). Returns true when the call was handled here (caller must then advance the program counter).

Parameters

call	The function-call code being executed.
identifier	The (mangled) callee symbol name.

symex_va_arg()

void goto_symext::symex_va_arg ( const expr2tc & lhs, const sideeffect2t & code, const guard2tc & guard )

protected

Symbolic implementation of va_arg.

symex_witness_assert()

void goto_symext::symex_witness_assert ( expr2tc & new_expr, const std::string & msg )

protected

symex_witness_branching()

void goto_symext::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 )

protected

symex_witness_function_enter()

bool goto_symext::symex_witness_function_enter ( const irep_idt & call_line )

protected

symex_witness_function_return()

void goto_symext::symex_witness_function_return ( expr2tc ret_val, const irep_idt & call_line )

protected

terminate_handler()

bool goto_symext::terminate_handler ( )

protected

Call terminate function handler when needed.

track_new_pointer()

void goto_symext::track_new_pointer ( const expr2tc & ptr_obj, const type2tc & new_type, const guard2tc & guard, const expr2tc & size = expr2tc() )

protected

Pointer modelling update function.

unexpected_handler()

bool goto_symext::unexpected_handler ( )

protected

Call unexpected function handler when needed.

update_pointer_validity()

void goto_symext::update_pointer_validity ( const expr2tc & old_ptr, const expr2tc & alloc_fail, const guard2tc & guard )

protected

Update pointer validity information after realloc.

Marks the old pointer as invalid when realloc succeeds, and handles the validity state transitions in the pointer tracking arrays.

Parameters

old_ptr	The original pointer being reallocated.
alloc_fail	Expression indicating allocation failure condition.
guard	Guard condition for this update.

va_list_copy()

void goto_symext::va_list_copy ( const expr2tc & dst, const expr2tc & src )

protected

va_copy: start dst as src is, reading where src reads next.

va_list_cursor()

expr2tc goto_symext::va_list_cursor ( const expr2tc & va_list_expr )

protected

The cursor symbol of a started local va_list; nil when its cursor is not known, and the frame's cursor applies.

va_list_cursor_symbol()

expr2tc goto_symext::va_list_cursor_symbol ( const renaming::level2t::name_record & rec )

protected

The l1 symbol holding the va_arg index a local va_list reads next.

It is an SSA variable so that a va_arg on one branch moves it on that branch only.

va_list_frame()

goto_symex_statet::framet & goto_symext::va_list_frame ( const expr2tc & va_list_expr )

protected

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.

Falls back to the current frame when that cannot be pinned down.

va_list_is_started()

bool goto_symext::va_list_is_started ( const expr2tc & va_list_expr ) const

protected

Whether the va_list denoted by this expression is known (or assumed) to have been initialised by va_start/va_copy.

va_lists whose base cannot be resolved to a local variable's symbol are conservatively assumed started.

va_list_l1_record()

std::optional< renaming::level2t::name_record > goto_symext::va_list_l1_record ( const expr2tc & va_list_expr ) const

protected

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.

va_list_mark_started()

void goto_symext::va_list_mark_started ( const expr2tc & va_list_expr, bool started, const expr2tc & cursor )

protected

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).

No-op if the base cannot be resolved to a local variable's symbol.

va_list_owner_records()

std::vector< renaming::level2t::name_record > goto_symext::va_list_owner_records ( const expr2tc & va_list_expr ) const

protected

The records va_list_frame looks for: a va_copy destination's are those of the va_list it was copied from.

va_list_pointee_records()

std::vector< renaming::level2t::name_record > goto_symext::va_list_pointee_records ( const expr2tc & va_list_expr ) const

protected

The l1 identity records of the local va_lists a pointer-valued expression may point to.

va_list_start()

void goto_symext::va_list_start ( const expr2tc & va_list_expr )

protected

va_start: the va_list reads this frame's first variadic argument next.

value_set_objects()

std::vector< expr2tc > goto_symext::value_set_objects ( const expr2tc & ptr, bool & complete )

protected

The objects the value set says ptr may address.

complete is cleared when a target names no object (NULL, unknown, invalid).

volatile_check()

void goto_symext::volatile_check ( expr2tc & expr )

protected

Friends And Related Symbol Documentation

bmct

friend class bmct

friend

build_goto_symex_classes

void build_goto_symex_classes ( )

friend

reachability_treet

friend class reachability_treet

friend

symex_dereference_statet

friend class symex_dereference_statet

friend

Member Data Documentation

alloc_size_arr_name

irep_idt goto_symext::alloc_size_arr_name

protected

art1

reachability_treet* goto_symext::art1

protected

Reachability tree we're working with.

base_case

bool goto_symext::base_case

protected

Flag as to whether we're doing a k-induction base case.

Corresponds to the option –base-case

bounded_loop_truncations

unsigned goto_symext::bounded_loop_truncations = 0

protected

Loops cut off at the unwinding bound with no unwinding assertion to flag it, i.e.

under –no-unwinding-assertions (which the coverage modes force on whenever –unwind is given). Exploration stopped there silently, so a coverage percentage measured on such a run is a lower bound: goals past the bound were never reached (issue #6387).

break_insn

unsigned long goto_symext::break_insn

protected

Instruction number we are to break at – that is, trap, to the debugger.

Zero means no trap; there is a zero instruction, but there are better ways of trapping at the start of symbolic execution to get at that.

claim_skips_deferred

bool goto_symext::claim_skips_deferred = false

protected

Set while claim() handles a Python assert's own condition, which needs no deferred assumption.

copy_definitions

persistent_map<irep_idt, expr2tc, irep_id_hash> goto_symext::copy_definitions

protected

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).

Values are canonicalized at insertion, so one substitution pass reaches the root of a chain. Path-guard subsumption uses this to rewrite branch conditions onto a common basis before structural comparison — a value handed across a call boundary gets a fresh symbol at every hop, and without the rewrite a callee's re-check of a caller-established condition never matches. Deliberately NOT fed into constant propagation: substituting copies globally slices away the originals' assignments and degrades counterexamples.

cur_state

goto_symex_statet* goto_symext::cur_state

protected

Target thread we're currently operating upon.

deferred_assumptions

std::vector<deferred_assumptiont> goto_symext::deferred_assumptions

protected

Assumptions defer_assumption() holds back, in program order.

depth_limit

unsigned long goto_symext::depth_limit

protected

Depth limit, as given by the –depth option.

dyn_info_arr_name

irep_idt goto_symext::dyn_info_arr_name

protected

dynamic_memory

std::list<allocated_obj> goto_symext::dynamic_memory

protected

List of all allocated objects.

Used to track what we should level memory-leak-assertions against when the program execution has finished

dynamic_object_sizes

std::unordered_map<irep_idt, expr2tc> goto_symext::dynamic_object_sizes

protected

The renamed byte size each heap object was allocated with, by symbol.

__ESBMC_alloc_size holds it too, but symex cannot read that array back, so a DYNAMIC_SIZE loop bound would never become constant.

first_loop

unsigned goto_symext::first_loop

protected

Loop numbers.

forward_condition

bool goto_symext::forward_condition

protected

Flag as to whether we're doing a k-induction forward condition.

Corresponds to the option –forward-condition

goto_functions

const goto_functionst& goto_symext::goto_functions

protected

GOTO functions that we're operating over.

guard_definitions

persistent_map<irep_idt, expr2tc, irep_id_hash> goto_symext::guard_definitions

protected

Defining condition of each L2 guard symbol generation, i.e.

the (renamed, simplified) rhs it was assigned in symex_goto. Guard symbols are SSA: each generation is assigned exactly once, so a single map for the whole symex object is sound. symex_goto uses it to resolve path-guard conjuncts back to branch conditions — level2 renaming cannot do that, as it never substitutes into symbols that are already level2. Keyed by the L2-qualified symbol name (an interned irep_idt with a cached hash) rather than the expression, so a lookup never deep-compares expression trees. Persistent, like the maps below: a forked execution state copies it in O(1).

guard_identifier_s

irep_idt goto_symext::guard_identifier_s

protected

Symbol prefix for guards.

These guards are the symbolic names for the truth of whether a particular branch has been taken during symbolic execution.

See also

guard_identifier

guard_prefix_index

persistent_map<expr2tc, conjunct_indext, irep2_hash> goto_symext::guard_prefix_index

protected

prefix_index's result per and-chain node of a path guard.

A node is the cached base of one guard prefix, and a guard grows by appending to that base, so a goto extends the index of its guard's longest indexed prefix instead of rescanning every conjunct (#9150). Never stale: conjuncts are L2, which renaming leaves alone, and the two maps above bind each generation once.

inductive_step

bool goto_symext::inductive_step

protected

Flag as to whether we're doing a k-induction inductive step.

Corresponds to the option –inductive-step

internal_deref_items

std::list<dereference_callbackt::internal_item> goto_symext::internal_deref_items

protected

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.

interval_domain_state

std::optional<interval_domaint> goto_symext::interval_domain_state

protected

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.

k_induction

bool goto_symext::k_induction

protected

Flag as to whether we're doing a k-induction.

Corresponds to the options –k-induction and –k-induction-parallel

loop_id_to_func_index

std::map<unsigned, std::pair<std::string, unsigned> > goto_symext::loop_id_to_func_index

protected

Mapping global loop ID -> (function name, per-function loop index).

max_copy_definition_nodes

size_t goto_symext::max_copy_definition_nodes = 64

staticconstexprprotected

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.

max_unwind

BigInt goto_symext::max_unwind

protected

Global maximum number of unwinds.

memory_leak_check

bool goto_symext::memory_leak_check

protected

Flag as to whether we're performing memory leak checks.

Corresponds to the option –memory-leak-check

new_context

contextt& goto_symext::new_context

protected

Context we're working with.

no_assertions

bool goto_symext::no_assertions

protected

Flag as to whether we're checking user assertions.

Corresponds to the option –no-assertions

no_reachable_memleak

bool goto_symext::no_reachable_memleak

protected

Flag as to whether we're pruning the objects from the memory leak check that are still reachable via global pointers.

Corresponds to the option –no-reachable-memory-leak

no_return_value_opt

bool goto_symext::no_return_value_opt

protected

Disable return value optimization.

no_simplify

bool goto_symext::no_simplify

protected

Flag as to whether we're not simplifying exprs.

Corresponds to the option –no-simplify

no_unwinding_assertions

bool goto_symext::no_unwinding_assertions

protected

Flag as to whether we're inserting unwinding assertions.

Corresponds to the option –no-unwinding-assertions

ns

const namespacet& goto_symext::ns

protected

Namespace we're working in.

options

optionst& goto_symext::options

protected

Options we're working with.

partial_loops

bool goto_symext::partial_loops

protected

Flag as to whether we're not enabling partial loops.

Corresponds to the option –partial-loops

remaining_claims

unsigned goto_symext::remaining_claims

protected

Number of assertions remaining to be discharged.

simplified_claims

unsigned goto_symext::simplified_claims

protected

Number of assertions that were trivially verified.

stack_limit

unsigned long goto_symext::stack_limit

protected

Limit size, in bits, for a single stack frame.

target

std::shared_ptr<symex_targett> goto_symext::target

protected

Target listening to the execution trace.

total_claims

unsigned goto_symext::total_claims

protected

Number of assertions executed.

total_stack_limit

unsigned long goto_symext::total_stack_limit

protected

Limit size, in bits, for every live stack frame taken together.

Catches overruns that come from call depth rather than from one oversized frame, which stack_limit alone cannot see (esbmc/esbmc#4605).

uf_applications

std::map<irep_idt, std::vector<std::pair<std::vector<expr2tc>, expr2tc> > > goto_symext::uf_applications

protected

Per-callee history of uninterpreted-function applications the SMT backend cannot encode natively, keyed on the mangled callee name.

Each entry pairs the renamed argument terms with the symbol standing for that application's result, so a later call can be Ackermannised against it.

See also

symex_uninterpreted_function

unwind_func_set

std::map<std::pair<std::string, unsigned>, BigInt> goto_symext::unwind_func_set

protected

Unwind bounds by function name and per-function loop index (0-indexed), (function name, loop index) -> max unwinds.

unwind_set

std::map<unsigned, BigInt> goto_symext::unwind_set

protected

Unwind bounds, loop number -> max unwinds.

va_copied_from

std::unordered_map< renaming::level2t::name_record, renaming::level2t::name_record, renaming::level2t::name_rec_hash> goto_symext::va_copied_from

protected

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.

va_started

std::unordered_map< renaming::level2t::name_record, bool, renaming::level2t::name_rec_hash> goto_symext::va_started

protected

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.

Keyed on the l1 renaming so the same object is recognised across frames (a va_list reached through a pointer dereferences to the owning activation's l1 name) and across recursion or loop re-declaration (each DECL of a va_list bumps the l1 number, as va_start takes its address, so a fresh activation needs a fresh va_start). Insertion ignores the path guard, over-approximating towards "started", so a conditional va_start can never yield a false positive.

valid_ptr_arr_name

irep_idt goto_symext::valid_ptr_arr_name

protected

Symbol names for modelling arrays.

These irep_idts contain the names of the arrays being used to store data modelling what pointers are active, which are freed, and so forth. They can change between C and C++, unfortunately.

validate_witness

bool goto_symext::validate_witness

protected

Cached from –validate-violation-witness; checked on every branch/intrinsic.

---

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

• src/goto-symex/engine/goto_symex.h
• src/goto-symex/engine/builtin_functions/bounded_math.cpp
• src/goto-symex/engine/builtin_functions/cpp_memory.cpp
• src/goto-symex/engine/builtin_functions/io.cpp
• src/goto-symex/engine/builtin_functions/memory_alloc.cpp
• src/goto-symex/engine/builtin_functions/memory_ops.cpp
• src/goto-symex/engine/builtin_functions/misc.cpp
• src/goto-symex/engine/builtin_functions/object_size.cpp
• src/goto-symex/engine/builtin_functions/python_builtins.cpp
• src/goto-symex/engine/builtin_functions/run_builtin.cpp
• src/goto-symex/engine/builtin_functions/threads.cpp
• src/goto-symex/engine/builtin_functions/va_arg.cpp
• src/goto-symex/engine/builtin_functions/witness.cpp
• src/goto-symex/engine/dynamic_allocation.cpp
• src/goto-symex/engine/symex_assign.cpp
• src/goto-symex/engine/symex_dereference.cpp
• src/goto-symex/engine/symex_function.cpp
• src/goto-symex/engine/symex_goto.cpp
• src/goto-symex/engine/symex_main.cpp
• src/goto-symex/engine/symex_other.cpp
• src/goto-symex/engine/symex_stack.cpp
• src/goto-symex/engine/symex_valid_object.cpp