CBMC
goto_symex_statet Class Referencefinal

Central data structure: state. More...

#include <goto_symex_state.h>

+ Inheritance diagram for goto_symex_statet:
+ Collaboration diagram for goto_symex_statet:

Classes

struct  threadt
 

Public Types

enum class  write_is_shared_resultt { NOT_SHARED , IN_ATOMIC_SECTION , SHARED }
 
typedef std::pair< unsigned, std::list< guardt > > a_s_r_entryt
 
typedef std::list< guardta_s_w_entryt
 

Public Member Functions

 goto_symex_statet (const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, bool should_simplify, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
 
 ~goto_symex_statet ()
 
 goto_symex_statet (const goto_symex_statet &other, symex_target_equationt *const target)
 Fake "copy constructor" that initializes the symex_target member. More...
 
template<levelt level = L2>
renamedt< exprt, level > rename (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. More...
 
template<levelt level>
renamedt< ssa_exprt, level > rename_ssa (ssa_exprt ssa, const namespacet &ns)
 Version of rename which is specialized for SSA exprt. More...
 
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, L2assignment (ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
 
call_stacktcall_stack ()
 
const call_stacktcall_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. More...
 
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. More...
 
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. More...
 
bool l2_thread_read_encoding (ssa_exprt &expr, const namespacet &ns)
 thread encoding More...
 
bool l2_thread_write_encoding (const ssa_exprt &expr, const namespacet &ns)
 thread encoding More...
 
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. More...
 
void drop_l1_name (const irep_idt &l1_identifier)
 Drops an L1 name from the local L2 map. More...
 
std::function< std::size_t(const irep_idt &)> get_l2_name_provider () const
 
- Public Member Functions inherited from goto_statet
const symex_level2tget_level2 () const
 
void output_propagation_map (std::ostream &)
 Print the constant propagation map in a human-friendly format. More...
 
 goto_statet ()=delete
 Constructors. More...
 
goto_statetoperator= (const goto_statet &other)=delete
 
goto_statetoperator= (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. More...
 

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

Public Attributes

symex_targett::sourcet source
 
symbol_tablet symbol_table
 contains symbols that are minted during symbolic execution, such as dynamically created objects etc. More...
 
guard_managertguard_manager
 
symex_target_equationtsymex_target
 
symex_level1t level1
 
field_sensitivityt field_sensitivity
 
shadow_memory_statet shadow_memory
 
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hashread_in_atomic_section
 
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hashwritten_in_atomic_section
 
std::vector< threadtthreads
 
std::stack< bool > record_events
 
const incremental_dirtytdirty = nullptr
 
goto_programt::const_targett saved_target
 
bool has_saved_jump_target
 This state is saved, with the PC pointing to the target of a GOTO. More...
 
bool has_saved_next_instruction
 This state is saved, with the PC pointing to the next instruction of a GOTO. More...
 
bool run_validation_checks
 Should the additional validation checks be run? More...
 
unsigned total_vccs = 0
 
unsigned remaining_vccs = 0
 
- Public Attributes inherited from goto_statet
unsigned depth = 0
 Distance from entry. More...
 
sharing_mapt< exprt, symbol_exprt, false, irep_hashdereference_cache
 This is used for eliminating repeated complicated dereferences. More...
 
value_sett value_set
 Uses level 1 names, and is used to do dereferencing. More...
 
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. More...
 
sharing_mapt< irep_idt, exprtpropagation
 
unsigned atomic_section_id = 0
 Threads. More...
 

Protected Types

typedef std::unordered_map< irep_idt, typetl1_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. More...
 
template<>
renamedt< ssa_exprt, L0set_indices (ssa_exprt ssa_expr, const namespacet &ns)
 
template<>
renamedt< ssa_exprt, L1set_indices (ssa_exprt ssa_expr, const namespacet &ns)
 
template<>
renamedt< ssa_exprt, L2set_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. More...
 

Private Attributes

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 42 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

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

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,
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
exprSymbol to be instantiated
index_generatorA function to produce a new index for a given name
nsA namespace
Returns
L1-renamed SSA expression

Definition at line 818 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 73 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 843 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 313 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 384 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 550 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
outstream to write to

Definition at line 797 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 171 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 708 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 579 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 152 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, L2> goto_symex_statet::set_indices ( ssa_exprt  ssa_expr,
const namespacet ns 
)
protected

Definition at line 49 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 49 of file goto_symex_state.cpp.

◆ set_indices() [4/4]

template<>
renamedt<ssa_exprt, L0> goto_symex_statet::set_indices ( ssa_exprt  ssa_expr,
const namespacet ns 
)
protected

Definition at line 49 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 522 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 262 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

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

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.

◆ 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

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

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: