cprover
goto_symex_statet Class Reference

#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 ()
 
void initialize (const goto_functionst &goto_functions)
 
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 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
 
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 switch_to_thread (unsigned t)
 

Public Attributes

unsigned depth
 
guardt guard
 
symex_targett::sourcet source
 
symex_targettsymex_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
 
const dirtytdirty
 

Protected Types

typedef std::unordered_map< irep_idt, typet, irep_id_hashl1_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
 

Detailed Description

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

◆ a_s_w_entryt

Definition at line 315 of file goto_symex_state.h.

◆ call_stackt

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

Definition at line 280 of file goto_symex_state.h.

◆ goto_state_listt

Definition at line 230 of file goto_symex_state.h.

◆ goto_state_mapt

◆ l1_historyt

Definition at line 49 of file goto_symex_state.h.

◆ l1_typest

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

Definition at line 180 of file goto_symex_state.h.

◆ original_identifierst

Definition at line 46 of file goto_symex_state.h.

◆ read_in_atomic_sectiont

Definition at line 314 of file goto_symex_state.h.

◆ threadst

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

Definition at line 336 of file goto_symex_state.h.

◆ written_in_atomic_sectiont

Definition at line 317 of file goto_symex_state.h.

Member Enumeration Documentation

◆ levelt

Enumerator
L0 
L1 
L2 

Definition at line 148 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ goto_symex_statet()

goto_symex_statet::goto_symex_statet ( )

Definition at line 24 of file goto_symex_state.cpp.

References new_frame(), and threads.

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

References 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 100 of file goto_symex_state.cpp.

References constant_propagation_reference(), forall_operands, irept::id(), exprt::is_constant(), address_of_exprt::object(), typecast_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 193 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

◆ initialize()

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

References call_stack().

Referenced by goto_symext::pop_frame().

◆ previous_frame()

const framet& goto_symex_statet::previous_frame ( )
inline

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

References call_stack().

Member Data Documentation

◆ atomic_section_id

◆ depth

unsigned goto_symex_statet::depth

Definition at line 36 of file goto_symex_state.h.

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

◆ dirty

◆ guard

◆ l1_history

l1_historyt goto_symex_statet::l1_history

Definition at line 50 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 181 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

◆ source

◆ symex_target

symex_targett* goto_symex_statet::symex_target

◆ threads

◆ value_set

◆ written_in_atomic_section


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