cprover
goto_symex_statet Class Referencefinal

#include <goto_symex_state.h>

Collaboration diagram for goto_symex_statet:
[legend]

Classes

class  framet
 
class  goto_statet
 
struct  level0t
 
struct  level1t
 
struct  level2t
 
class  propagationt
 
struct  renaming_levelt
 
class  threadt
 

Public Types

enum  levelt { L0 =0, L1 =1, L2 =2 }
 
typedef std::map< irep_idt, irep_idtoriginal_identifierst
 
typedef std::set< irep_idtl1_historyt
 
typedef std::list< goto_statetgoto_state_listt
 
typedef std::map< goto_programt::const_targett, goto_state_listtgoto_state_mapt
 
typedef std::vector< frametcall_stackt
 
typedef std::pair< unsigned, std::list< guardt > > a_s_r_entryt
 
typedef std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hashread_in_atomic_sectiont
 
typedef std::list< guardta_s_w_entryt
 
typedef std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hashwritten_in_atomic_sectiont
 
typedef std::vector< threadtthreadst
 

Public Member Functions

 goto_symex_statet ()
 
 ~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...
 
void rename (exprt &expr, const namespacet &ns, levelt level=L2)
 
void rename (typet &type, const irep_idt &l1_identifier, const namespacet &ns, levelt level=L2)
 
void assignment (ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
 
bool constant_propagation (const exprt &expr) const
 This function determines what expressions are to be propagated as "constants". More...
 
bool constant_propagation_reference (const exprt &expr) const
 this function determines which reference-typed expressions are constant More...
 
void get_original_name (exprt &expr) const
 
void get_original_name (typet &type) const
 
 goto_symex_statet (const goto_statet &s)
 
call_stacktcall_stack ()
 
const call_stacktcall_stack () const
 
framettop ()
 
const framettop () const
 
frametnew_frame ()
 
void pop_frame ()
 
const frametprevious_frame ()
 
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...
 
void populate_dirty_for_function (const irep_idt &id, const goto_functiont &)
 
void switch_to_thread (unsigned t)
 

Public Attributes

symbol_tablet symbol_table
 contains symbols that are minted during symbolic execution, such as dynamically created objects etc. More...
 
unsigned depth
 distance from entry More...
 
guardt guard
 
symex_targett::sourcet source
 
symex_target_equationtsymex_target
 
l1_historyt l1_history
 
goto_symex_statet::level0t level0
 
goto_symex_statet::level1t level1
 
goto_symex_statet::level2t level2
 
class goto_symex_statet::propagationt propagation
 
value_sett value_set
 
unsigned atomic_section_id
 
read_in_atomic_sectiont read_in_atomic_section
 
written_in_atomic_sectiont written_in_atomic_section
 
threadst threads
 
bool record_events
 
incremental_dirtyt dirty
 
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 saved_target_is_backwards
 

Protected Types

typedef std::unordered_map< irep_idt, typetl1_typest
 

Protected Member Functions

void rename_address (exprt &expr, const namespacet &ns, levelt level)
 
void set_ssa_indices (ssa_exprt &expr, const namespacet &ns, levelt level=L2)
 
void get_l1_name (exprt &expr) const
 

Protected Attributes

l1_typest l1_types
 

Private Member Functions

 goto_symex_statet (const goto_symex_statet &other)=default
 Dangerous, do not use. More...
 

Detailed Description

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

◆ a_s_w_entryt

Definition at line 341 of file goto_symex_state.h.

◆ call_stackt

typedef std::vector<framet> goto_symex_statet::call_stackt

Definition at line 306 of file goto_symex_state.h.

◆ goto_state_listt

Definition at line 257 of file goto_symex_state.h.

◆ goto_state_mapt

◆ l1_historyt

Definition at line 64 of file goto_symex_state.h.

◆ l1_typest

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

Definition at line 196 of file goto_symex_state.h.

◆ original_identifierst

Definition at line 61 of file goto_symex_state.h.

◆ read_in_atomic_sectiont

Definition at line 340 of file goto_symex_state.h.

◆ threadst

typedef std::vector<threadt> goto_symex_statet::threadst

Definition at line 362 of file goto_symex_state.h.

◆ written_in_atomic_sectiont

Definition at line 343 of file goto_symex_state.h.

Member Enumeration Documentation

◆ levelt

Enumerator
L0 
L1 
L2 

Definition at line 163 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/4]

goto_symex_statet::goto_symex_statet ( )

Definition at line 24 of file goto_symex_state.cpp.

References new_frame(), and threads.

◆ ~goto_symex_statet()

goto_symex_statet::~goto_symex_statet ( )
default

◆ goto_symex_statet() [2/4]

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 39 of file goto_symex_state.h.

References symex_target.

◆ goto_symex_statet() [3/4]

goto_symex_statet::goto_symex_statet ( const goto_statet s)
inlineexplicit

◆ goto_symex_statet() [4/4]

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

◆ assignment()

◆ call_stack() [1/2]

◆ call_stack() [2/2]

const call_stackt& goto_symex_statet::call_stack ( ) const
inline

Definition at line 314 of file goto_symex_state.h.

References PRECONDITION, source, symex_targett::sourcet::thread_nr, and threads.

◆ constant_propagation()

bool goto_symex_statet::constant_propagation ( const exprt expr) const

This function determines what expressions are to be propagated as "constants".

Definition at line 84 of file goto_symex_state.cpp.

References constant_propagation_reference(), forall_operands, irept::id(), exprt::is_constant(), address_of_exprt::object(), unary_exprt::op(), exprt::op0(), to_address_of_expr(), and to_typecast_expr().

Referenced by assignment(), and constant_propagation_reference().

◆ constant_propagation_reference()

bool goto_symex_statet::constant_propagation_reference ( const exprt expr) const

this function determines which reference-typed expressions are constant

Definition at line 177 of file goto_symex_state.cpp.

References index_exprt::array(), constant_propagation(), irept::id(), index_exprt::index(), exprt::op0(), exprt::operands(), and to_index_expr().

Referenced by constant_propagation().

◆ get_l1_name()

void goto_symex_statet::get_l1_name ( exprt expr) const
protected

◆ get_original_name() [1/2]

◆ get_original_name() [2/2]

void goto_symex_statet::get_original_name ( typet type) const

◆ l2_thread_read_encoding()

◆ l2_thread_write_encoding()

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

◆ new_frame()

framet& goto_symex_statet::new_frame ( )
inline

Definition at line 332 of file goto_symex_state.h.

References call_stack(), and top().

Referenced by goto_symex_statet(), and goto_symext::symex_function_call_code().

◆ pop_frame()

void goto_symex_statet::pop_frame ( )
inline

Definition at line 333 of file goto_symex_state.h.

References call_stack().

Referenced by goto_symext::pop_frame().

◆ populate_dirty_for_function()

void goto_symex_statet::populate_dirty_for_function ( const irep_idt id,
const goto_functiont  
)

◆ previous_frame()

const framet& goto_symex_statet::previous_frame ( )
inline

Definition at line 334 of file goto_symex_state.h.

References call_stack().

Referenced by goto_symext::symex_function_call_code().

◆ rename() [1/2]

◆ rename() [2/2]

◆ rename_address()

◆ set_ssa_indices()

◆ switch_to_thread()

void goto_symex_statet::switch_to_thread ( unsigned  t)

◆ top() [1/2]

◆ top() [2/2]

const framet& goto_symex_statet::top ( ) const
inline

Definition at line 326 of file goto_symex_state.h.

References call_stack(), and PRECONDITION.

Member Data Documentation

◆ atomic_section_id

◆ depth

unsigned goto_symex_statet::depth

distance from entry

Definition at line 53 of file goto_symex_state.h.

Referenced by goto_symext::merge_goto(), symex_bmct::symex_step(), and goto_symext::symex_step().

◆ dirty

◆ guard

◆ 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 378 of file goto_symex_state.h.

Referenced by goto_symext::symex_goto(), and goto_symext::symex_with_state().

◆ 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 382 of file goto_symex_state.h.

Referenced by goto_symext::symex_goto(), and goto_symext::symex_with_state().

◆ l1_history

l1_historyt goto_symex_statet::l1_history

Definition at line 65 of file goto_symex_state.h.

Referenced by goto_symext::locality(), and goto_symext::symex_start_thread().

◆ l1_types

l1_typest goto_symex_statet::l1_types
protected

Definition at line 197 of file goto_symex_state.h.

Referenced by rename().

◆ level0

goto_symex_statet::level0t goto_symex_statet::level0

Referenced by set_ssa_indices().

◆ level1

◆ level2

◆ propagation

◆ read_in_atomic_section

read_in_atomic_sectiont goto_symex_statet::read_in_atomic_section

◆ record_events

◆ saved_target

goto_programt::const_targett goto_symex_statet::saved_target

Definition at line 375 of file goto_symex_state.h.

Referenced by goto_symext::symex_goto().

◆ saved_target_is_backwards

bool goto_symex_statet::saved_target_is_backwards

Definition at line 383 of file goto_symex_state.h.

Referenced by goto_symext::symex_goto().

◆ source

◆ 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 50 of file goto_symex_state.h.

Referenced by goto_symext::dereference_rec(), symex_dereference_statet::has_failed_symbol(), goto_symext::make_auto_object(), goto_symext::parameter_assignments(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_instruction_range(), and goto_symext::symex_with_state().

◆ symex_target

◆ threads

◆ value_set

◆ written_in_atomic_section


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