goto_symex_state.cpp File Reference

#include <cassert>
#include <goto-symex/scheduler/execution_state.h>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/state/goto_symex_state.h>
#include <goto-symex/scheduler/reachability_tree.h>
#include <map>
#include <optional>
#include <sstream>
#include <utility>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/base/prefix.h>
#include <irep2/irep2.h>
#include <irep2/irep2_utils.h>
#include <util/irep/migrate.h>

Include dependency graph for goto_symex_state.cpp:

Functions
static bool	type_has_constant_size (const type2tc &type)
static std::optional< BigInt >	array_element_count (const type2tc &t)
static bool	array_may_propagate (const expr2tc &e)
static const expr2tc *	propagation_passthrough (const expr2tc &e)
	The operand a wrapper node's propagatability is decided by, or null when e is not one.
static bool	is_const_foldable_arith (const expr2tc &e)
	Arithmetic whose result is known once its operands are.
static bool	immutable_read_type (const expr2tc &e)
	The types a read may be carried at.
static bool	is_immutable_value (const expr2tc &expr)
	A value that can never change once recorded: a level2 SSA generation (assigned once), a nondet$ free variable (never assigned; no level2 generation is minted for it), or a member / fixed-index read out of one.
static bool	update_may_propagate (const goto_symex_statet &state, const expr2tc &value, unsigned &symbolic)
	Whether a with update value may be carried, counting in symbolic the ones only is_immutable_value accepts – the class #7597 admits, and the one symbolic_chain_bound caps.
static type2tc	slot_type (const type2tc &aggregate, const expr2tc &field)
	The type an aggregate declares for the slot field names, or nil where the slot cannot be named.
static expr2tc	read_of_field (const expr2tc &l2_lhs, const expr2tc &field)
	A read of the location a write targets, out of l2_lhs – the name the enclosing assignment has just defined.
static bool	aggregate_literal_may_propagate (const goto_symex_statet &state, const expr2tc &expr)
	Whether a constant aggregate literal may propagate: every element must itself propagate, or be immutable (#7597).
static bool	array_with_chain_may_propagate (const goto_symex_statet &state, const expr2tc &expr)
static bool	incremental_strategy_active ()
	Whether an incremental strategy is driving the unwind.
template<typename read_oft>
static bool	pin_refused_elements (const goto_symex_statet &state, std::vector< expr2tc > &elems, read_oft read_of)
	Replace every refused element of elems with the read read_of(i, type) names for it.
static expr2tc	pin_struct_literal (const goto_symex_statet &state, const expr2tc &rhs, const expr2tc &l2_lhs)
	Pin a struct literal's refused members to reads out of l2_lhs.
static expr2tc	pin_array_literal (const goto_symex_statet &state, const expr2tc &rhs, const expr2tc &l2_lhs)
	Pin an array literal's refused elements to reads out of l2_lhs.
static expr2tc	pin_literal_elements (const goto_symex_statet &state, const expr2tc &rhs, const expr2tc &l2_lhs)
	Pin the literal's elements.
static expr2tc	project_member (const expr2tc &arm, const irep_idt &name)
	The value arm holds for member name, or nil when the shape does not say.
static expr2tc	project_index (const expr2tc &arm, size_t i)
	The value arm holds at index i, or nil when the shape does not say – a symbolic index on the way down means the chain cannot be read off.
template<typename project_t, typename read_oft>
static std::optional< std::vector< expr2tc > >	split_phi (const goto_symex_statet &state, const if2t &phi, size_t count, project_t project, read_oft read_of)
	Decompose a merge into per-position values, or nothing when no position agrees – a rebuild that names every position folds nothing.
static expr2tc	pin_phi_members (const goto_symex_statet &state, const expr2tc &rhs, const expr2tc &l2_lhs)
	Pin a merge.
static expr2tc	pin_chain_updates (const goto_symex_statet &state, const expr2tc &rhs, const expr2tc &l2_lhs)
	Pin the chain's refused updates, rebuilding from the base up.
static bool	has_symbolic_array_size (const type2tc &type)
static std::optional< unsigned int >	pointee_width (const type2tc &subtype)

Variables
static constexpr unsigned	multidim_propagation_bound = 256
static constexpr unsigned	inf_array_write_bound = 256
static constexpr unsigned	symbolic_chain_bound = 1024
static constexpr unsigned	pinned_array_bound = 64

Function Documentation

aggregate_literal_may_propagate()

bool aggregate_literal_may_propagate ( const goto_symex_statet & state, const expr2tc & expr )

static

Whether a constant aggregate literal may propagate: every element must itself propagate, or be immutable (#7597).

array_element_count()

std::optional< BigInt > array_element_count ( const type2tc & t )

static

array_may_propagate()

bool array_may_propagate ( const expr2tc & e )

static

array_with_chain_may_propagate()

bool array_with_chain_may_propagate ( const goto_symex_statet & state, const expr2tc & expr )

static

has_symbolic_array_size()

bool has_symbolic_array_size ( const type2tc & type )

static

immutable_read_type()

bool immutable_read_type ( const expr2tc & e )

static

The types a read may be carried at.

Scalars, and fixed-size struct, union or array aggregates: a read of a whole member denotes it exactly and folds a sibling the same way, which is what a write into an array member needs (#7597). Infinite-size arrays stay out through type_has_constant_size, and oversized nests through array_may_propagate, because a read at a symbolic index inlines the whole constant. A union is admitted as a read only, for the reason given at the return below. A pointer stays out because carrying one resolves a later dereference against the wrong object, a false "Incorrect alignment when accessing data object" on the iterator read in regression/esbmc-cpp/cpp/github_5868_list_iterator_adl.

incremental_strategy_active()

bool incremental_strategy_active ( )

static

Whether an incremental strategy is driving the unwind.

Both re-bound it themselves rather than reading a folded guard, so carrying a with costs without paying (#7597, and constant_propagation's own opt-out).

is_const_foldable_arith()

bool is_const_foldable_arith ( const expr2tc & e )

static

Arithmetic whose result is known once its operands are.

Only add used to be treated that way, so n = sizeof(a) / sizeof(a[0]) was not propagated and a loop bounded by n never exited under –no-simplify, where do_simplify no longer folds the division to a literal first (#6778). The stored value stays unfolded, so the flag still decides the encoding; it is branch_decision_guard that folds it to decide the exit.

is_immutable_value()

bool is_immutable_value ( const expr2tc & expr )

static

A value that can never change once recorded: a level2 SSA generation (assigned once), a nondet$ free variable (never assigned; no level2 generation is minted for it), or a member / fixed-index read out of one.

Unlike constant_propagation's bare-symbol nondet$ exclusion, the value here sits inside a recorded aggregate, so the read folds to the free variable the trace shows anyway.

pin_array_literal()

expr2tc pin_array_literal ( const goto_symex_statet & state, const expr2tc & rhs, const expr2tc & l2_lhs )

static

Pin an array literal's refused elements to reads out of l2_lhs.

pin_chain_updates()

expr2tc pin_chain_updates ( const goto_symex_statet & state, const expr2tc & rhs, const expr2tc & l2_lhs )

static

Pin the chain's refused updates, rebuilding from the base up.

pin_literal_elements()

expr2tc pin_literal_elements ( const goto_symex_statet & state, const expr2tc & rhs, const expr2tc & l2_lhs )

static

Pin the literal's elements.

do_simplify folds a with over a propagated literal back into a literal, so a refused write reaches assignment() in this shape whenever the object still carried one – which is exactly the case #7597 turns on. Both shapes occur on the reporter's model.

pin_phi_members()

expr2tc pin_phi_members ( const goto_symex_statet & state, const expr2tc & rhs, const expr2tc & l2_lhs )

static

Pin a merge.

phi_function spells a branch that wrote one member as VAR = if(g, then, else) (symex_goto.cpp), a shape constant_propagation carries at no arm, so a conditional write drops the object – and the counter beside the written member – exactly as a refused write did before #7597. Rebuild it position by position: where the two arms agree the value is the branch's regardless of g and folds, and where they differ the position becomes a read of the name just defined, which denotes the merged value and cannot grow across iterations. An array decomposes the same way; pin_symbolic_updates has already capped its element count.

pin_refused_elements()

template<typename read_oft>

bool pin_refused_elements ( const goto_symex_statet & state, std::vector< expr2tc > & elems, read_oft read_of )

static

Replace every refused element of elems with the read read_of(i, type) names for it.

False when nothing was refused, so nothing changed.

pin_struct_literal()

expr2tc pin_struct_literal ( const goto_symex_statet & state, const expr2tc & rhs, const expr2tc & l2_lhs )

static

Pin a struct literal's refused members to reads out of l2_lhs.

pointee_width()

std::optional< unsigned int > pointee_width ( const type2tc & subtype )

static

project_index()

expr2tc project_index ( const expr2tc & arm, size_t i )

static

The value arm holds at index i, or nil when the shape does not say – a symbolic index on the way down means the chain cannot be read off.

Same reason as project_member for not going through the simplifier.

project_member()

expr2tc project_member ( const expr2tc & arm, const irep_idt & name )

static

The value arm holds for member name, or nil when the shape does not say.

Deliberately not member2tc(..)->simplify(): expr2t::simplify walks the operands before applying the projection, so asking a large carried value for one member would cost the size of the whole value, once per member.

propagation_passthrough()

const expr2tc * propagation_passthrough ( const expr2tc & e )

static

The operand a wrapper node's propagatability is decided by, or null when e is not one.

sizeof2t folds to its own value, which already holds clang's computed byte size, so it propagates exactly when that does – and declines for a VLA, whose value is a symbolic expression.

read_of_field()

expr2tc read_of_field ( const expr2tc & l2_lhs, const expr2tc & field )

static

A read of the location a write targets, out of l2_lhs – the name the enclosing assignment has just defined.

member(l2_lhs, f) after l2_lhs = with(.., f, v) denotes v exactly: a later write to the same location overwrites the read and the value alike. level2t::rename returns early on an L2 symbol, so the read neither re-expands nor grows across iterations, unlike a carried copy of v.

slot_type()

type2tc slot_type ( const type2tc & aggregate, const expr2tc & field )

static

The type an aggregate declares for the slot field names, or nil where the slot cannot be named.

This is what with2t checks its update value against (irep2_expr.cpp assert_consistency).

split_phi()

template<typename project_t, typename read_oft>

std::optional< std::vector< expr2tc > > split_phi ( const goto_symex_statet & state, const if2t & phi, size_t count, project_t project, read_oft read_of )

static

Decompose a merge into per-position values, or nothing when no position agrees – a rebuild that names every position folds nothing.

project reads a position out of one arm, read_of names the read a disagreeing position is pinned to.

type_has_constant_size()

bool type_has_constant_size ( const type2tc & type )

static

update_may_propagate()

bool update_may_propagate ( const goto_symex_statet & state, const expr2tc & value, unsigned & symbolic )

static

Whether a with update value may be carried, counting in symbolic the ones only is_immutable_value accepts – the class #7597 admits, and the one symbolic_chain_bound caps.

Variable Documentation

inf_array_write_bound

unsigned inf_array_write_bound = 256

staticconstexpr

multidim_propagation_bound

unsigned multidim_propagation_bound = 256

staticconstexpr

pinned_array_bound

unsigned pinned_array_bound = 64

staticconstexpr

symbolic_chain_bound

unsigned symbolic_chain_bound = 1024

staticconstexpr