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 () | |
~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_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 | 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_equationt * | symex_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, typet > | 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 |
Private Member Functions | |
goto_symex_statet (const goto_symex_statet &other)=default | |
Dangerous, do not use. More... | |
Definition at line 32 of file goto_symex_state.h.
typedef std::pair<unsigned, std::list<guardt> > goto_symex_statet::a_s_r_entryt |
Definition at line 338 of file goto_symex_state.h.
typedef std::list<guardt> goto_symex_statet::a_s_w_entryt |
Definition at line 341 of file goto_symex_state.h.
typedef std::vector<framet> goto_symex_statet::call_stackt |
Definition at line 306 of file goto_symex_state.h.
typedef std::list<goto_statet> goto_symex_statet::goto_state_listt |
Definition at line 257 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 259 of file goto_symex_state.h.
typedef std::set<irep_idt> goto_symex_statet::l1_historyt |
Definition at line 64 of file goto_symex_state.h.
|
protected |
Definition at line 196 of file goto_symex_state.h.
typedef std::map<irep_idt, irep_idt> goto_symex_statet::original_identifierst |
Definition at line 61 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 340 of file goto_symex_state.h.
typedef std::vector<threadt> goto_symex_statet::threadst |
Definition at line 362 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 343 of file goto_symex_state.h.
Enumerator | |
---|---|
L0 | |
L1 | |
L2 |
Definition at line 163 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.
|
default |
|
inlineexplicit |
Fake "copy constructor" that initializes the symex_target
member.
Definition at line 39 of file goto_symex_state.h.
References symex_target.
|
inlineexplicit |
Definition at line 245 of file goto_symex_state.h.
References goto_symex_statet::renaming_levelt::current_names, level2, and goto_symex_statet::goto_statet::level2_current_names.
|
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.
void 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 |
||
) |
Definition at line 309 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(), irept::id(), id2string(), goto_symex_statet::renaming_levelt::increase_counter(), is_shared(), L1, L2, l2_thread_write_encoding(), level2, namespacet::lookup(), value_sett::output(), PRECONDITION, 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 308 of file goto_symex_state.h.
References PRECONDITION, source, symex_targett::sourcet::thread_nr, and threads.
Referenced by goto_symext::dereference(), goto_symext::initialize_entry_point(), new_frame(), pop_frame(), goto_symext::pop_frame(), previous_frame(), goto_symext::symex_function_call_code(), goto_symext::symex_goto(), goto_symext::symex_step(), goto_symext::symex_threaded_step(), goto_symext::symex_throw(), goto_symext::symex_transition(), goto_symext::symex_with_state(), and top().
|
inline |
Definition at line 314 of file goto_symex_state.h.
References PRECONDITION, 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 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().
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().
|
protected |
Definition at line 899 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 859 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(), goto_symext::dereference_rec(), get_original_name(), postconditiont::is_used(), and postconditiont::strengthen().
void goto_symex_statet::get_original_name | ( | typet & | type | ) | const |
Definition at line 871 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().
bool goto_symex_statet::l2_thread_read_encoding | ( | ssa_exprt & | expr, |
const namespacet & | ns | ||
) |
thread encoding
Definition at line 531 of file goto_symex_state.cpp.
References guardt::add(), irept::add(), guardt::as_expr(), symex_target_equationt::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_target_equationt::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 676 of file goto_symex_state.cpp.
References guardt::as_expr(), atomic_section_id, dirty, ssa_exprt::get_object_name(), guard, namespacet::lookup(), record_events, ssa_exprt::remove_level_2(), symex_target_equationt::shared_write(), source, symex_target, threads, and written_in_atomic_section.
Referenced by assignment().
|
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().
|
inline |
Definition at line 333 of file goto_symex_state.h.
References call_stack().
Referenced by goto_symext::pop_frame().
void goto_symex_statet::populate_dirty_for_function | ( | const irep_idt & | id, |
const goto_functiont & | |||
) |
|
inline |
Definition at line 334 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 433 of file goto_symex_state.cpp.
References DATA_INVARIANT, 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_allocate(), 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_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 788 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 711 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, PRECONDITION, 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 400 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, symex_targett::sourcet::thread_nr, and UNREACHABLE.
Referenced by assignment(), l2_thread_read_encoding(), rename(), and rename_address().
void goto_symex_statet::switch_to_thread | ( | unsigned | t | ) |
Definition at line 911 of file goto_symex_state.cpp.
References atomic_section_id, guard, symex_targett::sourcet::pc, PRECONDITION, source, symex_targett::sourcet::thread_nr, and threads.
Referenced by goto_symext::symex_threaded_step().
|
inline |
Definition at line 320 of file goto_symex_state.h.
References call_stack(), and PRECONDITION.
Referenced by goto_symext::initialize_entry_point(), goto_symext::locality(), goto_symext::merge_gotos(), new_frame(), goto_symext::pop_frame(), goto_symext::return_assignment(), goto_symext::symex_assign(), goto_symext::symex_decl(), goto_symext::symex_function_call_code(), goto_symext::symex_goto(), goto_symext::symex_start_thread(), goto_symext::symex_transition(), and goto_symext::symex_with_state().
|
inline |
Definition at line 326 of file goto_symex_state.h.
References call_stack(), and PRECONDITION.
unsigned goto_symex_statet::atomic_section_id |
Definition at line 337 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 |
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().
incremental_dirtyt goto_symex_statet::dirty |
Definition at line 373 of file goto_symex_state.h.
Referenced by goto_symext::initialize_entry_point(), l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::phi_function(), goto_symext::pop_frame(), goto_symext::symex_decl(), and goto_symext::symex_function_call_code().
guardt goto_symex_statet::guard |
Definition at line 55 of file goto_symex_state.h.
Referenced by goto_symext::havoc_rec(), 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(), symex_bmct::symex_step(), goto_symext::symex_step(), goto_symext::symex_step_goto(), goto_symext::symex_trace(), and goto_symext::vcc().
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().
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_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().
|
protected |
Definition at line 197 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(), goto_symex_statet(), 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 344 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 372 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().
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().
bool goto_symex_statet::saved_target_is_backwards |
Definition at line 383 of file goto_symex_state.h.
Referenced by goto_symext::symex_goto().
symex_targett::sourcet goto_symex_statet::source |
Definition at line 56 of file goto_symex_state.h.
Referenced by call_stack(), goto_symext::dereference_rec(), goto_symext::havoc_rec(), goto_symext::initialize_entry_point(), 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::parameter_assignments(), goto_symext::phi_function(), goto_symext::return_assignment(), set_ssa_indices(), switch_to_thread(), goto_symext::symex_allocate(), 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_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_instruction_range(), goto_symext::symex_other(), goto_symext::symex_output(), goto_symext::symex_printf(), goto_symext::symex_start_thread(), symex_bmct::symex_step(), goto_symext::symex_step(), goto_symext::symex_step_goto(), goto_symext::symex_threaded_step(), goto_symext::symex_throw(), goto_symext::symex_trace(), goto_symext::symex_transition(), and goto_symext::vcc().
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_equationt* goto_symex_statet::symex_target |
Definition at line 57 of file goto_symex_state.h.
Referenced by goto_symex_statet(), goto_symext::initialize_entry_point(), l2_thread_read_encoding(), and l2_thread_write_encoding().
threadst goto_symex_statet::threads |
Definition at line 363 of file goto_symex_state.h.
Referenced by call_stack(), goto_symext::dereference_rec(), goto_symex_statet(), goto_symext::initialize_entry_point(), l2_thread_read_encoding(), l2_thread_write_encoding(), goto_symext::locality(), goto_symext::phi_function(), goto_symext::pop_frame(), switch_to_thread(), goto_symext::symex_assume(), goto_symext::symex_start_thread(), goto_symext::symex_step(), and goto_symext::symex_threaded_step().
value_sett goto_symex_statet::value_set |
Definition at line 202 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 345 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().