symex_goto.cpp File Reference

#include <cassert>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/equation/slice.h>
#include <goto-symex/equation/symex_target_equation.h>
#include <langapi/language_ui.h>
#include <solvers/smtlib/smtlib_conv.h>
#include <util/expr/expr_util.h>
#include <irep2/irep2.h>
#include <util/irep/migrate.h>
#include <util/base/prefix.h>
#include <util/irep/std_expr.h>

Include dependency graph for symex_goto.cpp:

Typedefs
using	phi_recordst
	Each entry pairs the record a phi assigns on this path with the record whose value the merged path contributes.

Functions
static bool	is_stable_value (const expr2tc &expr)
	A (possibly typecast) SSA symbol, or a pure bit operation over such leaves: neither changes meaning after its operands' assignments, so a copy chain built from one is a stable renaming of the same value.
static size_t	count_nodes_up_to (const expr2tc &expr, size_t limit)
	Flattened node count of expr, giving up once past limit.
static guard2tc	merge_state_guards (goto_symext::statet::merge_statet &merge_state, goto_symex_statet &state)
static void	collect_l1_phis (const renaming::level1t &level1, const goto_symext::statet::merge_statet &merge_state, phi_recordst &changed)
	A DECL re-run on a back-edge moves the frame to a fresh L1 instance (unless symex_decl reuses a dead one), while a path parked before it still holds its value in the older one (#7903).

Typedef Documentation

phi_recordst

using phi_recordst

Initial value:

 std::vector<
  std::pair<renaming::level2t::name_record, renaming::level2t::name_record>>

Each entry pairs the record a phi assigns on this path with the record whose value the merged path contributes.

Function Documentation

collect_l1_phis()

void collect_l1_phis ( const renaming::level1t & level1, const goto_symext::statet::merge_statet & merge_state, phi_recordst & changed )

static

A DECL re-run on a back-edge moves the frame to a fresh L1 instance (unless symex_decl reuses a dead one), while a path parked before it still holds its value in the older one (#7903).

Only instances still live on the parked path are carried over.

count_nodes_up_to()

size_t count_nodes_up_to ( const expr2tc & expr, size_t limit )

static

Flattened node count of expr, giving up once past limit.

is_stable_value()

bool is_stable_value ( const expr2tc & expr )

static

A (possibly typecast) SSA symbol, or a pure bit operation over such leaves: neither changes meaning after its operands' assignments, so a copy chain built from one is a stable renaming of the same value.

The computation form covers the operand-split idiom m = (mn >> 4) & 0x0F a caller and a callee both derive from one byte — without it their range checks never match and the callee's already-decided branches fork anyway. Computation nodes are restricted to bitvector types; symbol and constant leaves and the peeled typecasts stay accepted as in the bare-copy base. The restriction quarantines pointer-typed arithmetic in the chains — the leading suspect in the wrong FAILED verdicts the unrestricted form produced on the DebugOpt CI legs (cuda 003/024, python github_2937).

merge_state_guards()

guard2tc merge_state_guards ( goto_symext::statet::merge_statet & merge_state, goto_symex_statet & state )

inlinestatic