Class for the symex-slicer, this slicer is to be executed on SSA formula in order to remove every symbol that does not depends on it. More...

#include <slice.h>

Inheritance diagram for symex_slicet:

[legend]

Public Member Functions
	symex_slicet (const optionst &options)
bool	run (symex_target_equationt::SSA_stepst &eq) override
	Iterate over all steps of the \eq in REVERSE order, getting symbol dependencies.
Public Member Functions inherited from slicer
	slicer ()
BigInt	ignored () const override
	How many steps were ignored after this algorithm.
Public Member Functions inherited from ssa_step_algorithm
	ssa_step_algorithm (bool sideffect)
void	run_on_step (symex_target_equationt::SSA_stept &)
virtual void	run_on_output (symex_target_equationt::SSA_stept &)
virtual void	run_on_skip (symex_target_equationt::SSA_stept &)
virtual void	run_on_branching (symex_target_equationt::SSA_stept &)
Public Member Functions inherited from algorithm< symex_target_equationt::SSA_stepst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Static Public Member Functions
static expr2tc	get_nondet_symbol (const expr2tc &expr)

Public Attributes
std::unordered_set< std::string >	depends
	Holds the symbols the current equation depends on.
std::unordered_set< const expr2t * >	collected_cache
	BLACK set (two-color DFS in collect_dependencies): nodes already fully collected into depends.
std::unordered_map< std::string, std::unordered_set< size_t > >	index_reads
	Per-array-version read map: versioned array-symbol name -> set of constant indices that are actually read.
std::unordered_set< std::string >	array_disqualified
	Array versions whose element reads cannot be reasoned about per-index (whole-array use, symbolic index, array-as-value, …).
std::unordered_set< const expr2t * >	scanned_cache
	BLACK set for the scan_array_uses two-color DFS — independent of collected_cache.

Protected Member Functions
void	collect_dependencies (const expr2tc &expr)
	Collect every symbol of \expr into depends (mutating "reverse-taint" accumulation).
void	scan_array_uses (const expr2tc &expr)
	Record the array-element reads in \expr into index_reads, and disqualify (array_disqualified) any array version used in a way that defeats per-index reasoning.
bool	depends_on_tracked (const expr2tc &expr)
	Read-only: does \expr reference a tracked dependency (a symbol in depends or a no_slice symbol)?
void	run_on_assert (symex_target_equationt::SSA_stept &SSA_step) override
	Asserts are never sliced: collect the step's guard/cond symbols into depends and record their array reads.
void	run_on_assume (symex_target_equationt::SSA_stept &SSA_step) override
	Remove unneeded assumes from the formula.
void	run_on_assignment (symex_target_equationt::SSA_stept &SSA_step) override
	Remove unneeded assignments from the formula.
void	run_on_renumber (symex_target_equationt::SSA_stept &SSA_step) override
	Remove unneeded renumbers from the formula.

Protected Attributes
const bool	slice_assumes
	whether assumes should be sliced
const bool	slice_nondet
	Whether we should slice nondet symbols.
Protected Attributes inherited from slicer
BigInt	sliced = 0
	tracks how many steps were sliced
Protected Attributes inherited from algorithm< symex_target_equationt::SSA_stepst >
const bool	sideeffect

Detailed Description

Class for the symex-slicer, this slicer is to be executed on SSA formula in order to remove every symbol that does not depends on it.

It works by constructing a symbol dependency list by transversing the SSA formula in reverse order. If any assume, assignment, or renumber step does not belong into this dependency, then it will be ignored.

Constructor & Destructor Documentation

◆ symex_slicet()

symex_slicet::symex_slicet ( const optionst & options )

inlineexplicit

Member Function Documentation

◆ collect_dependencies()

void symex_slicet::collect_dependencies ( const expr2tc & expr )

protected

Collect every symbol of \expr into depends (mutating "reverse-taint" accumulation).

Walked with an explicit, memoised worklist — see the implementation for the two-color DFS that keeps this O(N) and stack-safe over deep guard and-chains.

Parameters

expr	expression whose symbols are added to depends

◆ depends_on_tracked()

bool symex_slicet::depends_on_tracked ( const expr2tc & expr )

protected

Read-only: does \expr reference a tracked dependency (a symbol in depends or a no_slice symbol)?

Used only on shallow exprs (an SSA lhs symbol, or an assume cond), never the deep guard, so it stays recursive and is NOT memoised — depends mutates across steps, so a node-memo would be unsound.

Parameters

expr	expression to test

Returns: true if \expr touches the tracked dependency set

◆ get_nondet_symbol()

expr2tc symex_slicet::get_nondet_symbol ( const expr2tc & expr )

static

◆ run()

bool symex_slicet::run ( symex_target_equationt::SSA_stepst & eq )

inlineoverridevirtual

Iterate over all steps of the \eq in REVERSE order, getting symbol dependencies.

Assignment and renumber steps whose lhs is untracked are ignored; assume steps additionally require –slice-assumes.

Parameters

eq	symex formula to be sliced

Implements algorithm< symex_target_equationt::SSA_stepst >.

◆ run_on_assert()

void symex_slicet::run_on_assert ( symex_target_equationt::SSA_stept & SSA_step )

overrideprotectedvirtual

Asserts are never sliced: collect the step's guard/cond symbols into depends and record their array reads.

Parameters

SSA_step an assert step

Reimplemented from ssa_step_algorithm.

◆ run_on_assignment()

void symex_slicet::run_on_assignment ( symex_target_equationt::SSA_stept & SSA_step )

overrideprotectedvirtual

Remove unneeded assignments from the formula.

Check if the LHS symbol is in the depends, if it is not then mark the \SSA_Step as ignored.

If the LHS is tracked, collect the guard and rhs symbols into depends (with dead array-store elision — see the implementation).

Parameters

SSA_step an assignment step

Reimplemented from ssa_step_algorithm.

◆ run_on_assume()

void symex_slicet::run_on_assume ( symex_target_equationt::SSA_stept & SSA_step )

overrideprotectedvirtual

Remove unneeded assumes from the formula.

Check if the Assume cond symbol is in the depends, if it is not then mark the \SSA_Step as ignored.

If the assume cond is in the depends, then add its guards and cond into the depends

Note 1: All the conditions operands are going to be added into the depends. This makes that the condition itself as a "reverse taint"

TODO: What happens if the ASSUME would result in false?

Parameters

SSA_step an assume step

Reimplemented from ssa_step_algorithm.

◆ run_on_renumber()

void symex_slicet::run_on_renumber ( symex_target_equationt::SSA_stept & SSA_step )

overrideprotectedvirtual

Remove unneeded renumbers from the formula.

Check if the LHS symbol is in the depends, if it is not then mark the \SSA_Step as ignored. Renumber steps never contribute dependencies.

Parameters

SSA_step a renumber step

Reimplemented from ssa_step_algorithm.

◆ scan_array_uses()

void symex_slicet::scan_array_uses ( const expr2tc & expr )

protected

Record the array-element reads in \expr into index_reads, and disqualify (array_disqualified) any array version used in a way that defeats per-index reasoning.

Run on the guard/cond/rhs of every RETAINED step so that, by the time a store is examined in reverse order, every downstream read of that array version has already been recorded.

Walked with the same explicit two-color worklist as collect_dependencies but with its own memo (scanned_cache); both outputs are insert-only, so skipping an already-scanned subtree is sound and keeps the scan O(N).

Parameters

expr	expression whose array reads are recorded

Member Data Documentation

◆ array_disqualified

std::unordered_set<std::string> symex_slicet::array_disqualified

Array versions whose element reads cannot be reasoned about per-index (whole-array use, symbolic index, array-as-value, …).

INSERT-ONLY. A disqualified array never has any of its stores dropped.

◆ collected_cache

std::unordered_set<const expr2t *> symex_slicet::collected_cache

BLACK set (two-color DFS in collect_dependencies): nodes already fully collected into depends.

Persists across steps so the shared guard and-chain prefix is walked once overall (Θ(N²) -> O(N)). Collection is purely monotone (depends.insert only), so the memo is unconditional.

◆ depends

std::unordered_set<std::string> symex_slicet::depends

Holds the symbols the current equation depends on.

◆ index_reads

std::unordered_map<std::string, std::unordered_set<size_t> > symex_slicet::index_reads

Per-array-version read map: versioned array-symbol name -> set of constant indices that are actually read.

Propagation through a kept store inserts the live-out set minus the overwritten index, preserving any direct reads already recorded for the source version. A store to an index NOT present here is provably dead and may be elided. Populated by scan_array_uses, consulted by run_on_assignment to drop dead array stores.

◆ scanned_cache

std::unordered_set<const expr2t *> symex_slicet::scanned_cache

BLACK set for the scan_array_uses two-color DFS — independent of collected_cache.

Sound for the same reason: index_reads/array_disqualified are insert-only, so re-skipping an already-scanned subtree adds nothing.

◆ slice_assumes

const bool symex_slicet::slice_assumes

protected

whether assumes should be sliced

◆ slice_nondet

const bool symex_slicet::slice_nondet

protected

Whether we should slice nondet symbols.

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

src/goto-symex/equation/slice.h
src/goto-symex/equation/slice.cpp

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ symex_slicet()

Member Function Documentation

◆ collect_dependencies()

◆ depends_on_tracked()

◆ get_nondet_symbol()

◆ run()

◆ run_on_assert()

◆ run_on_assignment()

◆ run_on_assume()

◆ run_on_renumber()

◆ scan_array_uses()

Member Data Documentation

◆ array_disqualified

◆ collected_cache

◆ depends

◆ index_reads

◆ scanned_cache

◆ slice_assumes

◆ slice_nondet