cprover
|
#include <goto_symex_state.h>
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_idt > | original_identifierst |
typedef std::set< irep_idt > | l1_historyt |
typedef std::list< goto_statet > | goto_state_listt |
typedef std::map< goto_programt::const_targett, goto_state_listt > | goto_state_mapt |
typedef std::vector< framet > | call_stackt |
typedef std::pair< unsigned, std::list< guardt > > | a_s_r_entryt |
typedef std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > | read_in_atomic_sectiont |
typedef std::list< guardt > | a_s_w_entryt |
typedef std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > | written_in_atomic_sectiont |
typedef std::vector< threadt > | threadst |
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_stackt & | call_stack () |
const call_stackt & | call_stack () const |
framet & | top () |
const framet & | top () const |
framet & | new_frame () |
void | pop_frame () |
const framet & | previous_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) |
Protected Types | |
typedef std::unordered_map< irep_idt, typet, irep_id_hash > | l1_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 |
Definition at line 30 of file goto_symex_state.h.
typedef std::pair<unsigned, std::list<guardt> > goto_symex_statet::a_s_r_entryt |
Definition at line 312 of file goto_symex_state.h.
typedef std::list<guardt> goto_symex_statet::a_s_w_entryt |
Definition at line 315 of file goto_symex_state.h.
typedef std::vector<framet> goto_symex_statet::call_stackt |
Definition at line 280 of file goto_symex_state.h.
typedef std::list<goto_statet> goto_symex_statet::goto_state_listt |
Definition at line 230 of file goto_symex_state.h.
typedef std::map<goto_programt::const_targett, goto_state_listt> goto_symex_statet::goto_state_mapt |
Definition at line 232 of file goto_symex_state.h.
typedef std::set<irep_idt> goto_symex_statet::l1_historyt |
Definition at line 49 of file goto_symex_state.h.
|
protected |
Definition at line 180 of file goto_symex_state.h.
typedef std::map<irep_idt, irep_idt> goto_symex_statet::original_identifierst |
Definition at line 46 of file goto_symex_state.h.
typedef std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> goto_symex_statet::read_in_atomic_sectiont |
Definition at line 314 of file goto_symex_state.h.
typedef std::vector<threadt> goto_symex_statet::threadst |
Definition at line 336 of file goto_symex_state.h.
typedef std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash> goto_symex_statet::written_in_atomic_sectiont |
Definition at line 317 of file goto_symex_state.h.
Enumerator | |
---|---|
L0 | |
L1 | |
L2 |
Definition at line 148 of file goto_symex_state.h.
goto_symex_statet::goto_symex_statet | ( | ) |
Definition at line 24 of file goto_symex_state.cpp.
References new_frame(), and threads.
void goto_symex_statet::assignment | ( | ssa_exprt & | lhs, |
const exprt & | rhs, | ||
const namespacet & | ns, | ||
bool | rhs_is_simplified, | ||
bool | record_value | ||
) |
Definition at line 325 of file goto_symex_state.cpp.
References assert_l1_renaming(), assert_l2_renaming(), value_sett::assign(), constant_propagation(), goto_symex_statet::renaming_levelt::current_names, symbol_exprt::get_identifier(), get_l1_name(), get_original_name(), has_prefix(), id2string(), goto_symex_statet::renaming_levelt::increase_counter(), is_shared(), L1, L2, l2_thread_write_encoding(), level2, namespacet::lookup(), value_sett::output(), propagation, goto_symex_statet::propagationt::remove(), rename(), set_ssa_indices(), exprt::type(), ssa_exprt::update_type(), value_set, and goto_symex_statet::propagationt::values.
Referenced by l2_thread_read_encoding(), goto_symext::phi_function(), goto_symext::symex_assign_symbol(), and goto_symext::symex_goto().
|
inline |
Definition at line 282 of file goto_symex_state.h.
References source, symex_targett::sourcet::thread_nr, and threads.
Referenced by goto_symext::dereference(), new_frame(), goto_symext::operator()(), goto_symext::pop_frame(), pop_frame(), previous_frame(), goto_symext::symex_catch(), goto_symext::symex_function_call_code(), goto_symext::symex_step(), goto_symext::symex_throw(), goto_symext::symex_transition(), and top().
|
inline |
Definition at line 288 of file goto_symex_state.h.
References source, symex_targett::sourcet::thread_nr, and threads.
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().
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().
|
protected |
Definition at line 906 of file goto_symex_state.cpp.
References Forall_operands, irept::get_bool(), irept::id(), ssa_exprt::remove_level_2(), and to_ssa_expr().
Referenced by assignment().
void goto_symex_statet::get_original_name | ( | exprt & | expr | ) | const |
Definition at line 866 of file goto_symex_state.cpp.
References Forall_operands, irept::get_bool(), ssa_exprt::get_original_expr(), irept::id(), to_ssa_expr(), and exprt::type().
Referenced by assignment(), preconditiont::compute_rec(), get_original_name(), postconditiont::is_used(), and postconditiont::strengthen().
void goto_symex_statet::get_original_name | ( | typet & | type | ) | const |
Definition at line 878 of file goto_symex_state.cpp.
References struct_union_typet::components(), get_original_name(), irept::id(), typet::subtype(), to_array_type(), and to_struct_union_type().
void goto_symex_statet::initialize | ( | const goto_functionst & | goto_functions | ) |
Definition at line 35 of file goto_symex_state.cpp.
References goto_symex_statet::framet::calling_location, goto_symex_statet::framet::end_of_function, goto_functions_templatet< goto_programt >::entry_point(), goto_functions_templatet< bodyT >::function_map, goto_program_templatet< codeT, guardT >::instructions, symex_targett::sourcet::pc, source, and top().
bool goto_symex_statet::l2_thread_read_encoding | ( | ssa_exprt & | expr, |
const namespacet & | ns | ||
) |
thread encoding
Definition at line 536 of file goto_symex_state.cpp.
References guardt::add(), irept::add(), guardt::as_expr(), symex_targett::assignment(), assignment(), atomic_section_id, goto_symex_statet::renaming_levelt::current_count(), goto_symex_statet::renaming_levelt::current_names, dirty, if_exprt::false_case(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), ssa_exprt::get_original_expr(), guard, goto_symex_statet::renaming_levelt::increase_counter(), INVARIANT_STRUCTURED, exprt::is_false(), exprt::is_true(), L2, level2, namespacet::lookup(), symex_targett::PHI, read_in_atomic_section, record_events, ssa_exprt::remove_level_2(), set_ssa_indices(), symex_targett::shared_read(), source, irept::swap(), symex_target, threads, to_ssa_expr(), if_exprt::true_case(), and written_in_atomic_section.
Referenced by rename().
bool goto_symex_statet::l2_thread_write_encoding | ( | const ssa_exprt & | expr, |
const namespacet & | ns | ||
) |
thread encoding
Definition at line 682 of file goto_symex_state.cpp.
References guardt::as_expr(), atomic_section_id, dirty, ssa_exprt::get_object_name(), guard, INVARIANT_STRUCTURED, namespacet::lookup(), record_events, ssa_exprt::remove_level_2(), symex_targett::shared_write(), source, symex_target, threads, and written_in_atomic_section.
Referenced by assignment().
|
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().
|
inline |
Definition at line 307 of file goto_symex_state.h.
References call_stack().
Referenced by goto_symext::pop_frame().
|
inline |
Definition at line 308 of file goto_symex_state.h.
References call_stack().
Referenced by goto_symext::symex_function_call_code().
void goto_symex_statet::rename | ( | exprt & | expr, |
const namespacet & | ns, | ||
levelt | level = L2 |
||
) |
Definition at line 444 of file goto_symex_state.cpp.
References dstringt::empty(), namespace_baset::follow(), Forall_operands, irept::get_bool(), symbol_exprt::get_identifier(), ssa_exprt::get_level_2(), irept::id(), L0, L1, L2, l2_thread_read_encoding(), with_exprt::old(), exprt::op0(), exprt::operands(), propagation, rename_address(), set_ssa_indices(), typet::subtype(), to_if_expr(), to_ssa_expr(), to_symbol_expr(), to_with_expr(), if_exprt::true_case(), exprt::type(), ssa_exprt::update_type(), and goto_symex_statet::propagationt::values.
Referenced by assignment(), goto_symext::dereference(), scratch_programt::eval(), symex_dereference_statet::has_failed_symbol(), goto_symext::locality(), rename(), rename_address(), goto_symext::symex_assign_if(), goto_symext::symex_assign_symbol(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_function_call_code(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_goto(), goto_symext::symex_input(), goto_symext::symex_malloc(), goto_symext::symex_output(), goto_symext::symex_printf(), goto_symext::symex_start_thread(), goto_symext::symex_step(), goto_symext::symex_step_goto(), goto_symext::symex_trace(), and goto_symext::vcc().
void goto_symex_statet::rename | ( | typet & | type, |
const irep_idt & | l1_identifier, | ||
const namespacet & | ns, | ||
levelt | level = L2 |
||
) |
Definition at line 795 of file goto_symex_state.cpp.
References struct_union_typet::components(), dstringt::empty(), irept::id(), array_typet::is_complete(), array_typet::is_incomplete(), l1_types, L2, namespacet::lookup(), rename(), typet::subtype(), to_array_type(), to_struct_union_type(), to_symbol_type(), and symbolt::type.
|
protected |
Definition at line 718 of file goto_symex_state.cpp.
References index_exprt::array(), if_exprt::cond(), if_exprt::false_case(), Forall_operands, irept::get_bool(), struct_union_typet::get_component(), member_exprt::get_component_name(), symbol_exprt::get_identifier(), irept::id(), index_exprt::index(), L1, rename(), set_ssa_indices(), member_exprt::struct_op(), typet::subtype(), to_if_expr(), to_index_expr(), to_member_expr(), to_ssa_expr(), to_struct_union_type(), if_exprt::true_case(), exprt::type(), and ssa_exprt::update_type().
Referenced by rename().
|
protected |
Definition at line 411 of file goto_symex_state.cpp.
References goto_symex_statet::renaming_levelt::current_count(), dstringt::empty(), symbol_exprt::get_identifier(), ssa_exprt::get_level_1(), ssa_exprt::get_level_2(), L0, L1, L2, level0, level1, level2, ssa_exprt::set_level_2(), source, and symex_targett::sourcet::thread_nr.
Referenced by assignment(), l2_thread_read_encoding(), rename(), and rename_address().
void goto_symex_statet::switch_to_thread | ( | unsigned | t | ) |
Definition at line 918 of file goto_symex_state.cpp.
References atomic_section_id, guard, symex_targett::sourcet::pc, source, symex_targett::sourcet::thread_nr, and threads.
Referenced by goto_symext::operator()().
|
inline |
Definition at line 294 of file goto_symex_state.h.
References call_stack().
Referenced by initialize(), goto_symext::locality(), goto_symext::merge_gotos(), new_frame(), goto_symext::operator()(), goto_symext::pop_frame(), goto_symext::return_assignment(), goto_symext::symex_assign(), goto_symext::symex_catch(), goto_symext::symex_decl(), goto_symext::symex_function_call_code(), goto_symext::symex_goto(), goto_symext::symex_start_thread(), and goto_symext::symex_transition().
|
inline |
Definition at line 300 of file goto_symex_state.h.
References call_stack().
unsigned goto_symex_statet::atomic_section_id |
Definition at line 311 of file goto_symex_state.h.
Referenced by l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::merge_goto(), goto_symext::phi_function(), switch_to_thread(), goto_symext::symex_assume(), goto_symext::symex_atomic_begin(), goto_symext::symex_atomic_end(), goto_symext::symex_decl(), and goto_symext::symex_start_thread().
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().
const dirtyt* goto_symex_statet::dirty |
Definition at line 344 of file goto_symex_state.h.
Referenced by l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::operator()(), goto_symext::phi_function(), goto_symext::pop_frame(), and goto_symext::symex_decl().
guardt goto_symex_statet::guard |
Definition at line 38 of file goto_symex_state.h.
Referenced by l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::loop_bound_exceeded(), symex_bmct::merge_goto(), goto_symext::merge_goto(), goto_symext::merge_value_sets(), goto_symext::phi_function(), goto_symext::return_assignment(), switch_to_thread(), goto_symext::symex_assign_symbol(), goto_symext::symex_assume(), goto_symext::symex_atomic_begin(), goto_symext::symex_atomic_end(), goto_symext::symex_decl(), goto_symext::symex_end_of_function(), goto_symext::symex_function_call_code(), goto_symext::symex_function_call_symbol(), goto_symext::symex_goto(), goto_symext::symex_input(), goto_symext::symex_other(), goto_symext::symex_output(), goto_symext::symex_printf(), goto_symext::symex_start_thread(), goto_symext::symex_step(), symex_bmct::symex_step(), goto_symext::symex_step_goto(), goto_symext::symex_trace(), and goto_symext::vcc().
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().
|
protected |
Definition at line 181 of file goto_symex_state.h.
Referenced by rename().
goto_symex_statet::level0t goto_symex_statet::level0 |
Referenced by set_ssa_indices().
goto_symex_statet::level1t goto_symex_statet::level1 |
Referenced by goto_symext::locality(), goto_symext::pop_frame(), set_ssa_indices(), and goto_symext::symex_start_thread().
goto_symex_statet::level2t goto_symex_statet::level2 |
Referenced by assignment(), l2_thread_read_encoding(), goto_symext::phi_function(), goto_symext::pop_frame(), set_ssa_indices(), goto_symext::symex_assign_symbol(), goto_symext::symex_atomic_end(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_start_thread(), and goto_symext::trigger_auto_object().
class goto_symex_statet::propagationt goto_symex_statet::propagation |
Referenced by assignment(), goto_symext::phi_function(), rename(), goto_symext::symex_dead(), and goto_symext::symex_decl().
read_in_atomic_sectiont goto_symex_statet::read_in_atomic_section |
Definition at line 318 of file goto_symex_state.h.
Referenced by l2_thread_read_encoding(), goto_symext::symex_atomic_begin(), and goto_symext::symex_atomic_end().
bool goto_symex_statet::record_events |
Definition at line 343 of file goto_symex_state.h.
Referenced by l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::phi_function(), goto_symext::symex_assign_symbol(), goto_symext::symex_decl(), and goto_symext::symex_start_thread().
symex_targett::sourcet goto_symex_statet::source |
Definition at line 39 of file goto_symex_state.h.
Referenced by call_stack(), initialize(), l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::locality(), goto_symext::loop_bound_exceeded(), symex_bmct::merge_goto(), goto_symext::merge_gotos(), goto_symext::operator()(), goto_symext::parameter_assignments(), goto_symext::phi_function(), goto_symext::return_assignment(), set_ssa_indices(), switch_to_thread(), goto_symext::symex_assign(), goto_symext::symex_assign_symbol(), goto_symext::symex_assume(), goto_symext::symex_atomic_begin(), goto_symext::symex_atomic_end(), goto_symext::symex_catch(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_end_of_function(), goto_symext::symex_function_call_code(), goto_symext::symex_function_call_symbol(), goto_symext::symex_goto(), goto_symext::symex_input(), goto_symext::symex_other(), goto_symext::symex_output(), goto_symext::symex_printf(), goto_symext::symex_start_thread(), goto_symext::symex_step(), symex_bmct::symex_step(), goto_symext::symex_step_goto(), goto_symext::symex_throw(), goto_symext::symex_trace(), goto_symext::symex_transition(), and goto_symext::vcc().
symex_targett* goto_symex_statet::symex_target |
Definition at line 40 of file goto_symex_state.h.
Referenced by l2_thread_read_encoding(), l2_thread_write_encoding(), and goto_symext::operator()().
threadst goto_symex_statet::threads |
Definition at line 337 of file goto_symex_state.h.
Referenced by call_stack(), goto_symex_statet(), l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::locality(), goto_symext::operator()(), goto_symext::phi_function(), goto_symext::pop_frame(), switch_to_thread(), goto_symext::symex_assume(), goto_symext::symex_start_thread(), and goto_symext::symex_step().
value_sett goto_symex_statet::value_set |
Definition at line 186 of file goto_symex_state.h.
Referenced by assignment(), symex_dereference_statet::get_value_set(), goto_symext::merge_value_sets(), goto_symext::symex_dead(), and goto_symext::symex_decl().
written_in_atomic_sectiont goto_symex_statet::written_in_atomic_section |
Definition at line 319 of file goto_symex_state.h.
Referenced by l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::symex_atomic_begin(), and goto_symext::symex_atomic_end().