cprover
|
#include <path_symex_state.h>
Classes | |
struct | framet |
struct | threadt |
struct | var_statet |
Public Types | |
typedef path_symex_stept | stept |
typedef std::vector< var_statet > | var_valt |
typedef std::map< unsigned, var_statet > | var_state_mapt |
typedef std::vector< framet > | call_stackt |
typedef std::vector< threadt > | threadst |
typedef std::map< loc_reft, unsigned > | unwinding_mapt |
typedef std::map< irep_idt, unsigned > | recursion_mapt |
Public Member Functions | |
path_symex_statet (var_mapt &_var_map, const locst &_locs, path_symex_historyt &_path_symex_history) | |
var_statet & | get_var_state (const var_mapt::var_infot &var_info) |
unsigned | get_current_thread () const |
void | set_current_thread (unsigned _thread) |
goto_programt::const_targett | get_instruction () const |
bool | is_executable () const |
void | record_step () |
threadt & | add_thread () |
void | disable_current_thread () |
loc_reft | pc () const |
void | next_pc () |
void | set_pc (loc_reft new_pc) |
void | output (std::ostream &out) const |
void | output (const threadt &thread, std::ostream &out) const |
exprt | read (const exprt &src) |
exprt | read_no_propagate (const exprt &src) |
exprt | dereference_rec (const exprt &src, bool propagate) |
std::string | array_index_as_string (const exprt &) const |
unsigned | get_no_thread_interleavings () const |
unsigned | get_depth () const |
unsigned | get_no_branches () const |
bool | last_was_branch () const |
bool | is_feasible (class decision_proceduret &) const |
bool | check_assertion (class decision_proceduret &) |
Public Attributes | |
var_mapt & | var_map |
const locst & | locs |
var_valt | shared_vars |
threadst | threads |
bool | inside_atomic_section |
path_symex_step_reft | history |
unwinding_mapt | unwinding_map |
recursion_mapt | recursion_map |
Protected Member Functions | |
exprt | read (const exprt &src, bool propagate) |
exprt | instantiate_rec (const exprt &src, bool propagate) |
exprt | expand_structs_and_arrays (const exprt &src) |
exprt | array_theory (const exprt &src, bool propagate) |
exprt | instantiate_rec_address (const exprt &src, bool propagate) |
exprt | read_symbol_member_index (const exprt &src, bool propagate) |
bool | is_symbol_member_index (const exprt &src) const |
Protected Attributes | |
unsigned | current_thread |
unsigned | no_thread_interleavings |
unsigned | no_branches |
unsigned | depth |
Definition at line 21 of file path_symex_state.h.
typedef std::vector<framet> path_symex_statet::call_stackt |
Definition at line 82 of file path_symex_state.h.
typedef std::map<irep_idt, unsigned> path_symex_statet::recursion_mapt |
Definition at line 211 of file path_symex_state.h.
Definition at line 39 of file path_symex_state.h.
typedef std::vector<threadt> path_symex_statet::threadst |
Definition at line 98 of file path_symex_state.h.
typedef std::map<loc_reft, unsigned> path_symex_statet::unwinding_mapt |
Definition at line 207 of file path_symex_state.h.
typedef std::map<unsigned, var_statet> path_symex_statet::var_state_mapt |
Definition at line 69 of file path_symex_state.h.
typedef std::vector<var_statet> path_symex_statet::var_valt |
Definition at line 65 of file path_symex_state.h.
|
inline |
Definition at line 24 of file path_symex_state.h.
|
inline |
Definition at line 135 of file path_symex_state.h.
References threads.
Referenced by initial_state(), and path_symext::operator()().
std::string path_symex_statet::array_index_as_string | ( | const exprt & | src | ) | const |
Definition at line 480 of file path_symex_state_read.cpp.
References integer2string(), var_mapt::ns, simplify_expr(), to_integer(), and var_map.
Referenced by read_symbol_member_index().
Definition at line 162 of file path_symex_state_read.cpp.
References index_exprt::array(), from_integer(), irept::id(), index_exprt::index(), integer2size_t(), exprt::is_constant(), irept::is_nil(), var_mapt::ns, read(), simplify_expr(), array_typet::size(), typet::subtype(), to_array_type(), to_index_expr(), to_integer(), exprt::type(), and var_map.
Referenced by read_symbol_member_index().
bool path_symex_statet::check_assertion | ( | class decision_proceduret & | decision_procedure | ) |
Definition at line 121 of file path_symex_state.cpp.
References decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, decision_proceduret::dec_solve(), get_instruction(), history, read(), and decision_proceduret::set_to().
Referenced by path_searcht::check_assertion().
Definition at line 491 of file path_symex_state_read.cpp.
References dereference(), Forall_operands, exprt::has_operands(), irept::id(), var_mapt::ns, dereference_exprt::pointer(), read(), to_dereference_expr(), and var_map.
Referenced by read().
|
inline |
Definition at line 141 of file path_symex_state.h.
References current_thread, and threads.
Referenced by path_symext::operator()(), and path_symext::return_from_function().
Definition at line 49 of file path_symex_state_read.cpp.
References struct_union_typet::components(), namespace_baset::follow(), from_expr(), from_integer(), irept::id(), integer2size_t(), exprt::is_constant(), var_mapt::ns, exprt::operands(), simplify_expr(), array_typet::size(), vector_typet::size(), typet::subtype(), to_array_type(), to_integer(), to_struct_type(), to_vector_type(), exprt::type(), and var_map.
Referenced by read_symbol_member_index().
|
inline |
Definition at line 106 of file path_symex_state.h.
References current_thread.
Referenced by build_goto_trace(), path_searcht::drop_state(), path_symext::function_call_rec(), path_symext::operator()(), path_searcht::operator()(), path_symext::return_from_function(), and path_symext::set_return_value().
|
inline |
Definition at line 187 of file path_symex_state.h.
References depth.
Referenced by path_searcht::drop_state(), and path_searcht::operator()().
|
inline |
Definition at line 116 of file path_symex_state.h.
Referenced by build_goto_trace(), path_searcht::check_assertion(), check_assertion(), path_symext::do_assert_fail(), path_symext::do_goto(), path_searcht::do_show_vcc(), path_searcht::drop_state(), path_symext::operator()(), path_searcht::operator()(), and record_step().
|
inline |
Definition at line 192 of file path_symex_state.h.
References no_branches.
Referenced by path_searcht::drop_state().
|
inline |
Definition at line 182 of file path_symex_state.h.
References no_thread_interleavings.
Referenced by path_searcht::drop_state().
path_symex_statet::var_statet & path_symex_statet::get_var_state | ( | const var_mapt::var_infot & | var_info | ) |
Definition at line 66 of file path_symex_state.cpp.
References current_thread, var_mapt::var_infot::is_shared(), var_mapt::var_infot::number, shared_vars, and threads.
Referenced by path_symext::assign_rec(), read_symbol_member_index(), and path_symext::symex_va_arg_next().
Definition at line 214 of file path_symex_state_read.cpp.
References symbol_tablet::add(), symbolt::base_name, namespace_baset::follow(), Forall_operands, from_expr(), irept::get_bool(), side_effect_exprt::get_statement(), exprt::has_operands(), irept::id(), id2string(), instantiate_rec_address(), irept::is_not_nil(), is_symbol_member_index(), symbolt::name, var_mapt::new_symbols, var_mapt::nondet_count, var_mapt::ns, exprt::op0(), exprt::operands(), irept::pretty(), read_symbol_member_index(), symbolt::symbol_expr(), to_member_expr(), to_side_effect_expr(), symbolt::type, exprt::type(), and var_map.
Referenced by instantiate_rec_address(), read(), and read_symbol_member_index().
Definition at line 527 of file path_symex_state_read.cpp.
References if_exprt::cond(), if_exprt::false_case(), irept::id(), irept::id_string(), instantiate_rec(), exprt::op0(), exprt::op1(), exprt::operands(), dereference_exprt::pointer(), irept::pretty(), member_exprt::struct_op(), to_dereference_expr(), to_if_expr(), to_member_expr(), and if_exprt::true_case().
Referenced by instantiate_rec().
|
inline |
Definition at line 121 of file path_symex_state.h.
References current_thread, and threads.
Referenced by path_searcht::operator()().
bool path_symex_statet::is_feasible | ( | class decision_proceduret & | decision_procedure | ) | const |
Definition at line 101 of file path_symex_state.cpp.
References decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, and history.
Referenced by path_searcht::is_feasible().
|
protected |
Definition at line 427 of file path_symex_state_read.cpp.
References index_exprt::array(), namespace_baset::follow(), irept::get_bool(), irept::id(), INVARIANT_STRUCTURED, var_mapt::ns, member_exprt::struct_op(), to_index_expr(), to_member_expr(), exprt::type(), and var_map.
Referenced by instantiate_rec().
|
inline |
Definition at line 197 of file path_symex_state.h.
References history, path_symex_stept::is_branch(), and path_symex_step_reft::is_nil().
Referenced by path_searcht::operator()().
|
inline |
Definition at line 152 of file path_symex_state.h.
References current_thread, and threads.
Referenced by path_symext::do_assert_fail(), path_symext::do_goto(), path_symext::function_call_rec(), and path_symext::operator()().
void path_symex_statet::output | ( | std::ostream & | out | ) | const |
Definition at line 56 of file path_symex_state.cpp.
References threads.
void path_symex_statet::output | ( | const threadt & | thread, |
std::ostream & | out | ||
) | const |
Definition at line 44 of file path_symex_state.cpp.
References path_symex_statet::threadt::call_stack, and path_symex_statet::threadt::pc.
|
inline |
Definition at line 146 of file path_symex_state.h.
References current_thread, PRECONDITION, and threads.
Referenced by path_symext::do_goto(), path_searcht::drop_state(), get_instruction(), path_symext::operator()(), and path_searcht::operator()().
Definition at line 167 of file path_symex_state.h.
Referenced by array_theory(), path_symext::assign(), path_searcht::check_assertion(), check_assertion(), dereference_rec(), path_symext::do_assert_fail(), path_symext::do_goto(), path_searcht::do_show_vcc(), path_symext::function_call(), path_symext::operator()(), read_no_propagate(), read_symbol_member_index(), path_symext::symex_malloc(), and path_symext::symex_va_arg_next().
Definition at line 24 of file path_symex_state_read.cpp.
References dereference_rec(), instantiate_rec(), var_mapt::ns, simplify_expr(), and var_map.
Definition at line 173 of file path_symex_state.h.
References read().
Referenced by path_symext::assign().
Definition at line 313 of file path_symex_state_read.cpp.
References index_exprt::array(), array_index_as_string(), array_theory(), dstringt::empty(), expand_structs_and_arrays(), namespace_baset::follow(), Forall_operands, var_mapt::var_infot::full_identifier, irept::get_bool(), member_exprt::get_component_name(), symbol_exprt::get_identifier(), get_var_state(), irept::id(), id2string(), index_exprt::index(), instantiate_rec(), irept::is_not_nil(), var_mapt::ns, read(), path_symex_statet::var_statet::ssa_symbol, var_mapt::var_infot::ssa_symbol(), member_exprt::struct_op(), to_index_expr(), to_member_expr(), to_symbol_expr(), exprt::type(), path_symex_statet::var_statet::value, and var_map.
Referenced by instantiate_rec().
void path_symex_statet::record_step | ( | ) |
Definition at line 78 of file path_symex_state.cpp.
References current_thread, depth, path_symex_step_reft::generate_successor(), get_instruction(), history, path_symex_step_reft::is_nil(), no_branches, no_thread_interleavings, path_symex_stept::pc, path_symex_stept::thread_nr, and threads.
Referenced by path_symext::assign_rec(), path_symext::do_assert_fail(), path_symext::do_goto(), path_symext::function_call_rec(), and path_symext::operator()().
|
inline |
Definition at line 111 of file path_symex_state.h.
References current_thread.
Referenced by initial_state().
|
inline |
Definition at line 157 of file path_symex_state.h.
References current_thread, and threads.
Referenced by path_symext::do_goto().
|
protected |
Definition at line 215 of file path_symex_state.h.
Referenced by disable_current_thread(), get_current_thread(), get_var_state(), is_executable(), next_pc(), pc(), record_step(), set_current_thread(), and set_pc().
|
protected |
Definition at line 218 of file path_symex_state.h.
Referenced by get_depth(), and record_step().
path_symex_step_reft path_symex_statet::history |
Definition at line 128 of file path_symex_state.h.
Referenced by path_symext::assign_rec(), build_goto_trace(), check_assertion(), path_symext::do_assert_fail(), path_symext::do_goto(), path_searcht::do_show_vcc(), path_symext::function_call_rec(), is_feasible(), last_was_branch(), path_symext::operator()(), path_replayt::path_replayt(), and record_step().
bool path_symex_statet::inside_atomic_section |
Definition at line 104 of file path_symex_state.h.
Referenced by path_symext::operator()().
const locst& path_symex_statet::locs |
Definition at line 44 of file path_symex_state.h.
Referenced by build_goto_trace(), path_symext::do_goto(), path_symext::function_call_rec(), get_instruction(), and path_symext::operator()().
|
protected |
Definition at line 217 of file path_symex_state.h.
Referenced by get_no_branches(), and record_step().
|
protected |
Definition at line 216 of file path_symex_state.h.
Referenced by get_no_thread_interleavings(), and record_step().
recursion_mapt path_symex_statet::recursion_map |
Definition at line 212 of file path_symex_state.h.
Referenced by path_searcht::drop_state(), path_symext::function_call_rec(), and path_symext::return_from_function().
var_valt path_symex_statet::shared_vars |
Definition at line 66 of file path_symex_state.h.
Referenced by get_var_state().
threadst path_symex_statet::threads |
Definition at line 99 of file path_symex_state.h.
Referenced by add_thread(), disable_current_thread(), path_symext::function_call_rec(), get_var_state(), is_executable(), next_pc(), path_symext::operator()(), path_searcht::operator()(), output(), pc(), record_step(), path_symext::return_from_function(), set_pc(), and path_symext::set_return_value().
unwinding_mapt path_symex_statet::unwinding_map |
Definition at line 208 of file path_symex_state.h.
Referenced by path_symext::do_goto(), and path_searcht::drop_state().
var_mapt& path_symex_statet::var_map |
Definition at line 43 of file path_symex_state.h.
Referenced by array_index_as_string(), array_theory(), path_symext::assign_rec(), dereference_rec(), expand_structs_and_arrays(), path_symext::function_call_rec(), instantiate_rec(), is_symbol_member_index(), read(), read_symbol_member_index(), path_symext::symex_malloc(), and path_symext::symex_va_arg_next().