cprover
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  write_is_shared_resultt { write_is_shared_resultt::NOT_SHARED, write_is_shared_resultt::IN_ATOMIC_SECTION, write_is_shared_resultt::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 &, 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)
 
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...
 
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
 
std::size_t increase_generation (const irep_idt l1_identifier, const ssa_exprt &lhs)
 Allocates a fresh L2 name for the given L1 identifier, and makes it the. More...
 
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 (const class goto_symex_statet &s)
 
 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...
 
std::size_t increase_generation (const irep_idt l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
 

Static Public Member Functions

static irep_idt guard_identifier ()
 

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_level0t level0
 
symex_level1t level1
 
field_sensitivityt field_sensitivity
 
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...
 
value_sett value_set
 Uses level 1 names, and is used to do dereferencing. More...
 
guardt guard
 
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 44 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 168 of file goto_symex_state.h.

◆ a_s_w_entryt

Definition at line 169 of file goto_symex_state.h.

◆ l1_typest

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

Definition at line 131 of file goto_symex_state.h.

Member Enumeration Documentation

◆ write_is_shared_resultt

Enumerator
NOT_SHARED 
IN_ATOMIC_SECTION 
SHARED 

Definition at line 189 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,
guard_managert manager,
std::function< std::size_t(const irep_idt &)>  fresh_l2_name_provider 
)

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

◆ call_stack() [1/2]

call_stackt& goto_symex_statet::call_stack ( )
inline

Definition at line 142 of file goto_symex_state.h.

◆ call_stack() [2/2]

const call_stackt& goto_symex_statet::call_stack ( ) const
inline

Definition at line 148 of file goto_symex_state.h.

◆ 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 230 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 236 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 241 of file goto_symex_state.h.

◆ guard_identifier()

static irep_idt goto_symex_statet::guard_identifier ( )
inlinestatic

Definition at line 136 of file goto_symex_state.h.

◆ increase_generation()

std::size_t goto_symex_statet::increase_generation ( const irep_idt  l1_identifier,
const ssa_exprt lhs 
)
inline

Allocates a fresh L2 name for the given L1 identifier, and makes it the.

Definition at line 223 of file goto_symex_state.h.

◆ l2_thread_read_encoding()

bool goto_symex_statet::l2_thread_read_encoding ( ssa_exprt expr,
const namespacet ns 
)

thread encoding

Definition at line 360 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

Definition at line 518 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 770 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 263 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 680 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 550 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 244 of file goto_symex_state.cpp.

◆ set_indices() [1/4]

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

Definition at line 150 of file goto_symex_state.cpp.

◆ 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 136 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 143 of file goto_symex_state.cpp.

◆ set_indices() [4/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.

◆ 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 491 of file goto_symex_state.cpp.

Member Data Documentation

◆ dirty

const incremental_dirtyt* goto_symex_statet::dirty = nullptr

Definition at line 203 of file goto_symex_state.h.

◆ field_sensitivity

field_sensitivityt goto_symex_statet::field_sensitivity

Definition at line 120 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 247 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 208 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 212 of file goto_symex_state.h.

◆ l1_types

l1_typest goto_symex_statet::l1_types
protected

Definition at line 132 of file goto_symex_state.h.

◆ level0

symex_level0t goto_symex_statet::level0

Definition at line 73 of file goto_symex_state.h.

◆ level1

symex_level1t goto_symex_statet::level1

Definition at line 74 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 170 of file goto_symex_state.h.

◆ record_events

std::stack<bool> goto_symex_statet::record_events

Definition at line 201 of file goto_symex_state.h.

◆ remaining_vccs

unsigned goto_symex_statet::remaining_vccs = 0

Definition at line 218 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 215 of file goto_symex_state.h.

◆ saved_target

goto_programt::const_targett goto_symex_statet::saved_target

Definition at line 205 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 187 of file goto_symex_state.h.

◆ total_vccs

unsigned goto_symex_statet::total_vccs = 0

Definition at line 217 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 172 of file goto_symex_state.h.


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