Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent version, which differs depending on which level you requested.

template<levelt level>

renamedt< ssa_exprt, level > rename_ssa (ssa_exprt ssa, const namespacet &ns)

Version of rename which is specialized for SSA exprt.

template<levelt level = L2>

void rename (typet &type, const irep_idt &l1_identifier, const namespacet &ns)

exprt l2_rename_rvalues (exprt lvalue, const namespacet &ns)

renamedt< ssa_exprt, L2 > assignment (ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)

call_stackt & call_stack ()

const call_stackt & call_stack () const

ssa_exprt add_object (const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)

Instantiate the object expr.

ssa_exprt declare (ssa_exprt ssa, const namespacet &ns)

Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of symbols in fields of ssa are at 1, and rename ssa to level 2.

void print_backtrace (std::ostream &) const

Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread.

bool l2_thread_read_encoding (ssa_exprt &expr, const namespacet &ns)

thread encoding

bool l2_thread_write_encoding (const ssa_exprt &expr, const namespacet &ns)

thread encoding

write_is_shared_resultt write_is_shared (const ssa_exprt &expr, const namespacet &ns) const

void drop_existing_l1_name (const irep_idt &l1_identifier)

Drops an L1 name from the local L2 map.

void drop_l1_name (const irep_idt &l1_identifier)

Drops an L1 name from the local L2 map.

std::function< std::size_t(const irep_idt &)> get_l2_name_provider () const

- Public Member Functions inherited from goto_statet

const symex_level2t & get_level2 () const

void output_propagation_map (std::ostream &)

Print the constant propagation map in a human-friendly format.

goto_statet ()=delete

Constructors.

goto_statet & operator= (const goto_statet &other)=delete

goto_statet & operator= (goto_statet &&other)=default

goto_statet (const goto_statet &other)=default

goto_statet (goto_statet &&other)=default

goto_statet (guard_managert &guard_manager)

void apply_condition (const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)

Given a condition that must hold on this path, propagate as much knowledge as possible.

Static Public Member Functions

static irep_idt guard_identifier ()

static bool is_read_only_object (const exprt &lvalue)

Returns true if lvalue is a read-only object, such as the null object.

Public Attributes

symex_targett::sourcet source

symbol_tablet symbol_table

contains symbols that are minted during symbolic execution, such as dynamically created objects etc.

guard_managert & guard_manager

symex_target_equationt * symex_target = nullptr

symex_level1t level1

field_sensitivityt field_sensitivity

shadow_memory_statet shadow_memory

std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section

std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section

std::vector< threadt > threads

std::stack< bool > record_events

const incremental_dirtyt * dirty = nullptr

goto_programt::const_targett saved_target

bool has_saved_jump_target = false

This state is saved, with the PC pointing to the target of a GOTO.

bool has_saved_next_instruction = false

This state is saved, with the PC pointing to the next instruction of a GOTO.

bool run_validation_checks = false

Should the additional validation checks be run?

unsigned total_vccs = 0

unsigned remaining_vccs = 0

- Public Attributes inherited from goto_statet

unsigned depth = 0

Distance from entry.

sharing_mapt< exprt, symbol_exprt, false, irep_hash > dereference_cache

This is used for eliminating repeated complicated dereferences.

value_sett value_set

Uses level 1 names, and is used to do dereferencing.

guardt guard

bool reachable

Is this code reachable? If not we can take shortcuts such as not entering function calls, but we still conduct guard arithmetic as usual.

sharing_mapt< irep_idt, exprt > propagation

unsigned atomic_section_id = 0

Threads.

Protected Types

typedef std::unordered_map< irep_idt, typet > l1_typest

Protected Member Functions

template<levelt >

void rename_address (exprt &expr, const namespacet &ns)

template<levelt level>

renamedt< ssa_exprt, level > set_indices (ssa_exprt expr, const namespacet &ns)

Update values up to level.

template<>

renamedt< ssa_exprt, L0 > set_indices (ssa_exprt ssa_expr, const namespacet &ns)

template<>

renamedt< ssa_exprt, L1 > set_indices (ssa_exprt ssa_expr, const namespacet &ns)

template<>

renamedt< ssa_exprt, L2 > set_indices (ssa_exprt ssa_expr, const namespacet &ns)

Protected Attributes

l1_typest l1_types

- Protected Attributes inherited from goto_statet

symex_level2t level2

Private Member Functions

goto_symex_statet (const goto_symex_statet &other)=default

Dangerous, do not use.

Private Attributes

const irep_idt language_mode

std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider

Detailed Description

Central data structure: state.

The state is a persistent data structure that symex maintains as it executes. As we walk over each instruction, state will be updated reflecting their effects until a branch occurs (such as an if), where parts of the state will be copied into a goto_statet, stored in a map for later reference and then merged again (via merge_goto) once it reaches a control-flow graph convergence.

Definition at line 41 of file goto_symex_state.h.

Member Typedef Documentation

◆ a_s_r_entryt

typedef std::pair<unsigned, std::list<guardt> > goto_symex_statet::a_s_r_entryt

Definition at line 179 of file goto_symex_state.h.

◆ a_s_w_entryt

typedef std::list<guardt> goto_symex_statet::a_s_w_entryt

Definition at line 180 of file goto_symex_state.h.

◆ l1_typest

typedef std::unordered_map<irep_idt, typet> goto_symex_statet::l1_typest

protected

Definition at line 136 of file goto_symex_state.h.

Member Enumeration Documentation

◆ write_is_shared_resultt

enum class goto_symex_statet::write_is_shared_resultt

strong

Enumerator
NOT_SHARED
IN_ATOMIC_SECTION
SHARED

Definition at line 201 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/3]

goto_symex_statet::goto_symex_statet ( const symex_targett::sourcet & _source,

std::size_t max_field_sensitive_array_size,

bool should_simplify,

const irep_idt language_mode,

guard_managert & manager,

std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider

)

Definition at line 31 of file goto_symex_state.cpp.

◆ ~goto_symex_statet()

goto_symex_statet::~goto_symex_statet ( )

default

◆ goto_symex_statet() [2/3]

goto_symex_statet::goto_symex_statet ( const goto_symex_statet & other,

symex_target_equationt *const target

)

inlineexplicit

Fake "copy constructor" that initializes the symex_target member.

Definition at line 54 of file goto_symex_state.h.

◆ goto_symex_statet() [3/3]

goto_symex_statet::goto_symex_statet ( const goto_symex_statet & other )

privatedefault

Dangerous, do not use.

Copying a state S1 to S2 risks S2 pointing to a deallocated symex_target_equationt if S1 (and the symex_target_equationt that its symex_target member points to) go out of scope. If your class has a goto_symex_statet member and needs a copy constructor, copy instances of this class using the public two-argument copy constructor constructor to ensure that the copy points to an allocated symex_target_equationt. The two-argument copy constructor uses this private copy constructor as a delegate.

Member Function Documentation

◆ add_object()

ssa_exprt goto_symex_statet::add_object ( const symbol_exprt & expr,

std::function< std::size_t(const irep_idt &)> index_generator,

const namespacet & ns

)

Instantiate the object expr.

An instance of an object is an L1-renamed SSA expression such that its L1-index has not previously been used.

Parameters: expr Symbol to be instantiated

index_generator A function to produce a new index for a given name

ns A namespace

Returns: L1-renamed SSA expression

Definition at line 804 of file goto_symex_state.cpp.

◆ assignment()

renamedt< ssa_exprt, L2 > goto_symex_statet::assignment ( ssa_exprt lhs,

const exprt & rhs,

const namespacet & ns,

bool rhs_is_simplified,

bool record_value,

bool allow_pointer_unsoundness = false

)

Returns: lhs renamed to level 2

Definition at line 78 of file goto_symex_state.cpp.

◆ call_stack() [1/2]

call_stackt & goto_symex_statet::call_stack ( )

inline

Definition at line 147 of file goto_symex_state.h.

◆ call_stack() [2/2]

const call_stackt & goto_symex_statet::call_stack ( ) const

inline

Definition at line 153 of file goto_symex_state.h.

◆ declare()

ssa_exprt goto_symex_statet::declare ( ssa_exprt ssa,

const namespacet & ns

)

Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of symbols in fields of ssa are at 1, and rename ssa to level 2.

Returns: ssa renamed to level 2

Definition at line 829 of file goto_symex_state.cpp.

◆ drop_existing_l1_name()

void goto_symex_statet::drop_existing_l1_name ( const irep_idt & l1_identifier )

inline

Drops an L1 name from the local L2 map.

Definition at line 233 of file goto_symex_state.h.

◆ drop_l1_name()

void goto_symex_statet::drop_l1_name ( const irep_idt & l1_identifier )

inline

Drops an L1 name from the local L2 map.

Definition at line 239 of file goto_symex_state.h.

◆ get_l2_name_provider()

std::function< std::size_t(const irep_idt &)> goto_symex_statet::get_l2_name_provider ( ) const

inline

Definition at line 244 of file goto_symex_state.h.

◆ guard_identifier()

static irep_idt goto_symex_statet::guard_identifier ( )

inlinestatic

Definition at line 141 of file goto_symex_state.h.

◆ is_read_only_object()

static bool goto_symex_statet::is_read_only_object ( const exprt & lvalue )

inlinestatic

Returns true if lvalue is a read-only object, such as the null object.

Definition at line 250 of file goto_symex_state.h.

◆ l2_rename_rvalues()

exprt goto_symex_statet::l2_rename_rvalues ( exprt lvalue,

const namespacet & ns

)

Definition at line 305 of file goto_symex_state.cpp.

◆ l2_thread_read_encoding()

bool goto_symex_statet::l2_thread_read_encoding ( ssa_exprt & expr,

const namespacet & ns

)

thread encoding

Definition at line 376 of file goto_symex_state.cpp.

◆ l2_thread_write_encoding()

bool goto_symex_statet::l2_thread_write_encoding ( const ssa_exprt & expr,

const namespacet & ns

)

thread encoding

Returns: true if expr is shared between threads

Definition at line 542 of file goto_symex_state.cpp.

◆ print_backtrace()

void goto_symex_statet::print_backtrace ( std::ostream & out ) const

Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread.

This is for use from the debugger or in debug code; please don't delete it just because it isn't called at present.

Parameters: out stream to write to

Definition at line 783 of file goto_symex_state.cpp.

◆ rename() [1/2]

template<levelt level>

template renamedt< exprt, L1 > goto_symex_statet::rename< L1 > ( exprt expr,

const namespacet & ns

)

Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent version, which differs depending on which level you requested.

Each level also updates its predecessors, so a L1 rename will update L1 and L0. A L2 will update L2, L1 and L0.

What happens at each level: L0. Applies a suffix giving the current thread number. (Excludes guards, dynamic objects and anything not considered thread-local) L1. Applies a suffix giving the current loop iteration or recursive function invocation. L2. Applies a suffix giving the generation of this variable.

Renaming will not increment any of these values, just update the expression with them. Levels matter when reading a variable, for example: reading the value of x really means reading the particular x symbol for this thread (L0 renaming, if applicable), the most recent instance of x (L1 renaming), and the most recent write to x (L2 renaming).

The above example after being renamed could look like this: 'x!0@0#42'. That states it's the 42nd generation of this variable, on the first thread, in the first frame.

A full explanation of SSA (which is why we do this renaming) is in the SSA section of background-concepts.md.

Definition at line 163 of file goto_symex_state.cpp.

◆ rename() [2/2]

template<levelt level>

void goto_symex_statet::rename ( typet & type,

const irep_idt & l1_identifier,

const namespacet & ns

)

Definition at line 700 of file goto_symex_state.cpp.

◆ rename_address()

template<levelt level>

void goto_symex_statet::rename_address ( exprt & expr,

const namespacet & ns

)

protected

Definition at line 571 of file goto_symex_state.cpp.

◆ rename_ssa()

template<levelt level>

template renamedt< ssa_exprt, L1 > goto_symex_statet::rename_ssa< L1 > ( ssa_exprt ssa,

const namespacet & ns

)

Version of rename which is specialized for SSA exprt.

Ensure rename_ssa gets compiled for L0.

Implementation only exists for level L0 and L1.

Definition at line 144 of file goto_symex_state.cpp.

◆ set_indices() [1/4]

template<levelt level>

renamedt< ssa_exprt, level > goto_symex_statet::set_indices ( ssa_exprt expr,

const namespacet & ns

)

protected

Update values up to level.

◆ set_indices() [2/4]

template<>

renamedt< ssa_exprt, L0 > goto_symex_statet::set_indices ( ssa_exprt ssa_expr,

const namespacet & ns

)

protected

Definition at line 54 of file goto_symex_state.cpp.

◆ set_indices() [3/4]

template<>

renamedt< ssa_exprt, L1 > goto_symex_statet::set_indices ( ssa_exprt ssa_expr,

const namespacet & ns

)

protected

Definition at line 54 of file goto_symex_state.cpp.

◆ set_indices() [4/4]

template<>

renamedt< ssa_exprt, L2 > goto_symex_statet::set_indices ( ssa_exprt ssa_expr,

const namespacet & ns

)

protected

Definition at line 54 of file goto_symex_state.cpp.

◆ write_is_shared()

goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared ( const ssa_exprt & expr,

const namespacet & ns

) const

Definition at line 514 of file goto_symex_state.cpp.

Member Data Documentation

◆ dirty

const incremental_dirtyt* goto_symex_statet::dirty = nullptr

Definition at line 215 of file goto_symex_state.h.

◆ field_sensitivity

field_sensitivityt goto_symex_statet::field_sensitivity

Definition at line 122 of file goto_symex_state.h.

◆ fresh_l2_name_provider

std::function<std::size_t(const irep_idt &)> goto_symex_statet::fresh_l2_name_provider

private

Definition at line 263 of file goto_symex_state.h.

◆ guard_manager

guard_managert& goto_symex_statet::guard_manager

Definition at line 70 of file goto_symex_state.h.

◆ has_saved_jump_target

bool goto_symex_statet::has_saved_jump_target = false

This state is saved, with the PC pointing to the target of a GOTO.

Definition at line 220 of file goto_symex_state.h.

◆ has_saved_next_instruction

bool goto_symex_statet::has_saved_next_instruction = false

This state is saved, with the PC pointing to the next instruction of a GOTO.

Definition at line 224 of file goto_symex_state.h.

◆ l1_types

l1_typest goto_symex_statet::l1_types

protected

Definition at line 137 of file goto_symex_state.h.

◆ language_mode

const irep_idt goto_symex_statet::language_mode

private

Definition at line 262 of file goto_symex_state.h.

◆ level1

symex_level1t goto_symex_statet::level1

Definition at line 73 of file goto_symex_state.h.

◆ read_in_atomic_section

std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> goto_symex_statet::read_in_atomic_section

Definition at line 181 of file goto_symex_state.h.

◆ record_events

std::stack<bool> goto_symex_statet::record_events

Definition at line 213 of file goto_symex_state.h.

◆ remaining_vccs

unsigned goto_symex_statet::remaining_vccs = 0

Definition at line 230 of file goto_symex_state.h.

◆ run_validation_checks

bool goto_symex_statet::run_validation_checks = false

Should the additional validation checks be run?

Definition at line 227 of file goto_symex_state.h.

◆ saved_target

goto_programt::const_targett goto_symex_statet::saved_target

Definition at line 217 of file goto_symex_state.h.

◆ shadow_memory

shadow_memory_statet goto_symex_statet::shadow_memory

Definition at line 124 of file goto_symex_state.h.

◆ source

symex_targett::sourcet goto_symex_statet::source

Definition at line 62 of file goto_symex_state.h.

◆ symbol_table

symbol_tablet goto_symex_statet::symbol_table

contains symbols that are minted during symbolic execution, such as dynamically created objects etc.

The names in this table are needed for error traces even after symbolic execution has finished.

Definition at line 67 of file goto_symex_state.h.

◆ symex_target

symex_target_equationt* goto_symex_statet::symex_target = nullptr

Definition at line 71 of file goto_symex_state.h.

◆ threads

std::vector<threadt> goto_symex_statet::threads

Definition at line 199 of file goto_symex_state.h.

◆ total_vccs

unsigned goto_symex_statet::total_vccs = 0

Definition at line 229 of file goto_symex_state.h.

◆ written_in_atomic_section

std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash> goto_symex_statet::written_in_atomic_section

Definition at line 183 of file goto_symex_state.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/goto_symex_state.h
/home/runner/work/cbmc/cbmc/src/goto-symex/goto_symex_state.cpp

goto_symex_statet
Generated by doxygen 1.9.8