cprover
|
The main class for the forward symbolic simulator. More...
#include <goto_symex.h>
Public Types | |
typedef goto_symex_statet | statet |
typedef std::function< const goto_functionst::goto_functiont &(const irep_idt &)> | get_goto_functiont |
Public Member Functions | |
goto_symext (message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage) | |
virtual | ~goto_symext () |
virtual void | symex_from_entry_point_of (const goto_functionst &goto_functions, symbol_tablet &new_symbol_table) |
symex entire program starting from entry point More... | |
virtual void | symex_from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table) |
symex entire program starting from entry point More... | |
virtual void | resume_symex_from_saved_state (const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *const saved_equation, symbol_tablet &new_symbol_table) |
Performs symbolic execution using a state and equation that have already been used to symex part of the program. More... | |
virtual void | symex_with_state (statet &, const goto_functionst &, symbol_tablet &) |
symex entire program starting from entry point More... | |
virtual void | symex_with_state (statet &, const get_goto_functiont &, symbol_tablet &) |
symex entire program starting from entry point More... | |
virtual void | symex_instruction_range (statet &, const goto_functionst &, goto_programt::const_targett first, goto_programt::const_targett limit) |
Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached. More... | |
virtual void | symex_instruction_range (statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett first, goto_programt::const_targett limit) |
Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached. More... | |
virtual void | symex_step_goto (statet &, bool taken) |
Public Attributes | |
bool | should_pause_symex |
Have states been pushed onto the workqueue? More... | |
unsigned | total_vccs |
unsigned | remaining_vccs |
bool | constant_propagation |
bool | self_loops_to_assumptions |
irep_idt | language_mode |
language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise. More... | |
Protected Types | |
typedef symex_targett::assignment_typet | assignment_typet |
Protected Member Functions | |
void | initialize_entry_point (statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett pc, goto_programt::const_targett limit) |
Initialise the symbolic execution and the given state with pc as entry point. More... | |
void | symex_threaded_step (statet &, const get_goto_functiont &) |
Invokes symex_step and verifies whether additional threads can be executed. More... | |
virtual void | symex_step (const get_goto_functiont &, statet &) |
do just one step More... | |
void | clean_expr (exprt &, statet &, bool write) |
void | trigger_auto_object (const exprt &, statet &) |
void | initialize_auto_object (const exprt &, statet &) |
void | process_array_expr (exprt &) |
Given an expression, find the root object and the offset into it. More... | |
exprt | make_auto_object (const typet &, statet &) |
virtual void | dereference (exprt &, statet &, const bool write) |
void | dereference_rec (exprt &, statet &, guardt &, const bool write) |
void | dereference_rec_address_of (exprt &, statet &, guardt &) |
exprt | address_arithmetic (const exprt &, statet &, guardt &, bool keep_array) |
Evaluate an ID_address_of expression. More... | |
virtual void | symex_transition (statet &, goto_programt::const_targett to, bool is_backwards_goto=false) |
virtual void | symex_transition (statet &state) |
virtual void | symex_goto (statet &) |
virtual void | symex_start_thread (statet &) |
virtual void | symex_atomic_begin (statet &) |
virtual void | symex_atomic_end (statet &) |
virtual void | symex_decl (statet &) |
virtual void | symex_decl (statet &, const symbol_exprt &expr) |
virtual void | symex_dead (statet &) |
virtual void | symex_other (statet &) |
virtual void | vcc (const exprt &, const std::string &msg, statet &) |
virtual void | symex_assume (statet &, const exprt &cond) |
void | merge_gotos (statet &) |
virtual void | merge_goto (const statet::goto_statet &goto_state, statet &) |
void | merge_value_sets (const statet::goto_statet &goto_state, statet &dest) |
void | phi_function (const statet::goto_statet &goto_state, statet &) |
virtual bool | get_unwind (const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind) |
virtual void | loop_bound_exceeded (statet &, const exprt &guard) |
void | pop_frame (statet &) |
pop one call frame More... | |
void | return_assignment (statet &) |
virtual void | no_body (const irep_idt &) |
virtual void | symex_function_call (const get_goto_functiont &, statet &, const code_function_callt &) |
virtual void | symex_end_of_function (statet &) |
do function call by inlining More... | |
virtual void | symex_function_call_symbol (const get_goto_functiont &, statet &, const code_function_callt &) |
virtual void | symex_function_call_code (const get_goto_functiont &, statet &, const code_function_callt &) |
do function call by inlining More... | |
virtual bool | get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) |
void | parameter_assignments (const irep_idt function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments) |
void | locality (const irep_idt function_identifier, statet &, const goto_functionst::goto_functiont &) |
preserves locality of local variables of a given function by applying L1 renaming to the local identifiers More... | |
void | add_end_of_function (exprt &code, const irep_idt &identifier) |
nondet_symbol_exprt | build_symex_nondet (typet &type) |
void | symex_throw (statet &) |
void | symex_catch (statet &) |
virtual void | do_simplify (exprt &) |
void | symex_assign (statet &, const code_assignt &) |
void | havoc_rec (statet &, const guardt &, const exprt &) |
void | symex_assign_rec (statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
void | symex_assign_symbol (statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
void | symex_assign_typecast (statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
void | symex_assign_array (statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
void | symex_assign_struct_member (statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
void | symex_assign_if (statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
void | symex_assign_byte_extract (statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
virtual void | symex_gcc_builtin_va_arg_next (statet &, const exprt &lhs, const side_effect_exprt &) |
virtual void | symex_allocate (statet &, const exprt &lhs, const side_effect_exprt &) |
virtual void | symex_cpp_delete (statet &, const codet &) |
virtual void | symex_cpp_new (statet &, const exprt &lhs, const side_effect_exprt &) |
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes. More... | |
virtual void | symex_fkt (statet &, const code_function_callt &) |
virtual void | symex_macro (statet &, const code_function_callt &) |
virtual void | symex_trace (statet &, const code_function_callt &) |
virtual void | symex_printf (statet &, const exprt &rhs) |
virtual void | symex_input (statet &, const codet &) |
virtual void | symex_output (statet &, const codet &) |
void | read (exprt &) |
void | replace_nondet (exprt &) |
void | rewrite_quantifiers (exprt &, statet &) |
Static Protected Member Functions | |
static bool | is_index_member_symbol_if (const exprt &expr) |
static exprt | add_to_lhs (const exprt &lhs, const exprt &what) |
Protected Attributes | |
const optionst & | options |
const unsigned | max_depth |
const bool | doing_path_exploration |
const bool | allow_pointer_unsoundness |
const symbol_tablet & | outer_symbol_table |
The symbol table associated with the goto-program that we're executing. More... | |
namespacet | ns |
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol table owned by the goto_symex_statet object used during symbolic execution. More... | |
symex_target_equationt & | target |
unsigned | atomic_section_counter |
messaget | log |
irep_idt | guard_identifier |
path_storaget & | path_storage |
std::unordered_map< irep_idt, local_safe_pointerst > | safe_pointers |
Static Protected Attributes | |
static unsigned | nondet_count =0 |
static unsigned | dynamic_counter =0 |
Friends | |
class | symex_dereference_statet |
The main class for the forward symbolic simulator.
Higher-level architectural information on symbolic execution is documented in the Symbolic execution module page.
Definition at line 48 of file goto_symex.h.
|
protected |
Definition at line 395 of file goto_symex.h.
typedef std::function<const goto_functionst::goto_functiont &(const irep_idt &)> goto_symext::get_goto_functiont |
Definition at line 86 of file goto_symex.h.
typedef goto_symex_statet goto_symext::statet |
Definition at line 51 of file goto_symex.h.
|
inline |
Definition at line 53 of file goto_symex.h.
|
inlinevirtual |
Definition at line 80 of file goto_symex.h.
Definition at line 90 of file symex_assign.cpp.
References irept::id(), irept::is_nil(), irept::is_not_nil(), irept::make_nil(), exprt::op0(), and exprt::operands().
Referenced by symex_assign_array(), symex_assign_byte_extract(), symex_assign_struct_member(), symex_assign_symbol(), and symex_assign_typecast().
|
protected |
Evaluate an ID_address_of expression.
Definition at line 91 of file symex_dereference.cpp.
References base_type_eq(), object_descriptor_exprt::build(), byte_extract_id(), char_type(), compute_pointer_offset(), if_exprt::cond(), dereference_rec(), do_simplify(), if_exprt::false_case(), namespace_baset::follow(), from_integer(), irept::get_bool(), irept::id(), irept::id_string(), index_type(), INVARIANT, ns, address_of_exprt::object(), byte_extract_exprt::offset(), object_descriptor_exprt::offset(), byte_extract_exprt::op(), dereference_exprt::pointer(), pointer_type(), PRECONDITION, object_descriptor_exprt::root_object(), typet::subtype(), to_address_of_expr(), to_byte_extract_expr(), to_dereference_expr(), to_if_expr(), to_ssa_expr(), if_exprt::true_case(), and exprt::type().
Referenced by dereference_rec().
|
protected |
Definition at line 25 of file goto_symex.cpp.
References nondet_count, and to_string().
Referenced by replace_nondet(), and symex_allocate().
Definition at line 138 of file symex_clean_expr.cpp.
References adjust_byte_extract_rec(), dereference(), ns, and replace_nondet().
Referenced by symex_assign(), symex_cpp_new(), symex_goto(), symex_other(), and symex_step().
Definition at line 359 of file symex_dereference.cpp.
References goto_symex_statet::call_stack(), dereference_rec(), goto_symex_statet::L1, ns, PRECONDITION, and goto_symex_statet::rename().
Referenced by clean_expr(), dereference_rec(), and symex_step_goto().
|
protected |
Definition at line 228 of file symex_dereference.cpp.
References typet::add_source_location(), address_arithmetic(), index_exprt::array(), base_type_eq(), dereference(), dstringt::empty(), namespace_baset::follow(), Forall_operands, from_integer(), goto_symex_statet::get_original_name(), irept::id(), index_exprt::index(), index_type(), language_mode, ns, address_of_exprt::object(), unary_exprt::op(), exprt::op0(), exprt::operands(), options, symex_targett::sourcet::pc, dereference_exprt::pointer(), pointer_type(), value_set_dereferencet::READ, safe_pointers, goto_symex_statet::source, exprt::source_location(), typet::subtype(), irept::swap(), goto_symex_statet::symbol_table, goto_symex_statet::threads, to_address_of_expr(), to_array_type(), to_dereference_expr(), to_index_expr(), to_typecast_expr(), trigger_auto_object(), exprt::type(), UNREACHABLE, and value_set_dereferencet::WRITE.
Referenced by address_arithmetic(), dereference(), and dereference_rec_address_of().
|
protected |
Definition at line 25 of file symex_dereference.cpp.
References dereference_rec(), irept::id(), member_exprt::struct_op(), to_if_expr(), to_index_expr(), and to_member_expr().
|
protectedvirtual |
Definition at line 19 of file goto_symex.cpp.
References optionst::get_bool_option(), ns, options, and simplify().
Referenced by address_arithmetic(), phi_function(), process_array_expr(), symex_assign_if(), symex_assign_symbol(), symex_assume(), symex_atomic_end(), symex_gcc_builtin_va_arg_next(), symex_goto(), symex_input(), symex_other(), symex_output(), symex_printf(), symex_step_goto(), and vcc().
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 541 of file symex_goto.cpp.
Referenced by symex_goto().
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 20 of file symex_function_call.cpp.
Referenced by symex_function_call_code().
Definition at line 20 of file symex_other.cpp.
References guardt::add(), guardt::as_expr(), if_exprt::cond(), if_exprt::false_case(), goto_symex_statet::guard, irept::id(), exprt::is_true(), code_assignt::lhs(), symex_targett::sourcet::pc, code_assignt::rhs(), goto_symex_statet::source, symex_assign(), to_byte_extract_expr(), to_if_expr(), to_index_expr(), to_member_expr(), to_typecast_expr(), if_exprt::true_case(), and exprt::type().
Referenced by symex_other().
Definition at line 37 of file auto_objects.cpp.
References struct_union_typet::components(), namespace_baset::follow(), irept::id(), make_auto_object(), ns, pointer_type(), member_exprt::set_component_name(), exprt::source_location(), member_exprt::struct_op(), typet::subtype(), symex_assign(), to_pointer_type(), to_struct_type(), and exprt::type().
Referenced by trigger_auto_object().
|
protected |
Initialise the symbolic execution and the given state with pc
as entry point.
state | Symex state to initialise. |
goto_functions | GOTO model to symex. |
pc | first instruction to symex |
limit | final instruction, which itself will not be symexed. |
Definition at line 120 of file symex_main.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::calling_location, goto_symex_statet::dirty, goto_symex_statet::framet::end_of_function, INVARIANT, symex_targett::sourcet::pc, incremental_dirtyt::populate_dirty_for_function(), PRECONDITION, safe_pointers, goto_symex_statet::source, goto_symex_statet::symex_target, symex_transition(), target, goto_symex_statet::threads, and goto_symex_statet::top().
Referenced by symex_from_entry_point_of(), and symex_instruction_range().
|
staticprotected |
Definition at line 65 of file symex_dereference.cpp.
References irept::id(), to_if_expr(), to_index_expr(), and to_member_expr().
|
protected |
preserves locality of local variables of a given function by applying L1 renaming to the local identifiers
Definition at line 369 of file symex_function_call.cpp.
References goto_symex_statet::renaming_levelt::current_names, get_local_identifiers(), goto_symex_statet::renaming_levelt::increase_counter(), goto_symex_statet::L0, goto_symex_statet::L1, goto_symex_statet::l1_history, goto_symex_statet::level1, goto_symex_statet::framet::local_objects, namespacet::lookup(), ns, goto_symex_statet::framet::old_level1, goto_symex_statet::rename(), goto_symex_statet::source, symex_targett::sourcet::thread_nr, goto_symex_statet::threads, and goto_symex_statet::top().
Referenced by symex_function_call_code().
Definition at line 502 of file symex_goto.cpp.
References guardt::add(), optionst::get_bool_option(), goto_symex_statet::guard, exprt::is_true(), options, symex_targett::sourcet::pc, goto_symex_statet::source, symex_assume(), to_string(), and vcc().
Referenced by symex_goto().
Definition at line 19 of file auto_objects.cpp.
References symbol_table_baset::add(), symbolt::base_name, dynamic_counter, id2string(), symbolt::is_lvalue, symbolt::mode, symbolt::name, goto_symex_statet::symbol_table, to_string(), and symbolt::type.
Referenced by initialize_auto_object().
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 343 of file symex_goto.cpp.
References goto_symex_statet::goto_statet::atomic_section_id, goto_symex_statet::atomic_section_id, goto_symex_statet::depth, goto_symex_statet::goto_statet::depth, goto_symex_statet::guard, goto_symex_statet::goto_statet::guard, merge_value_sets(), and phi_function().
Referenced by symex_bmct::merge_goto(), and merge_gotos().
|
protected |
Definition at line 319 of file symex_goto.cpp.
References goto_symex_statet::framet::goto_state_map, merge_goto(), symex_targett::sourcet::pc, goto_symex_statet::source, and goto_symex_statet::top().
Referenced by symex_step().
|
protected |
Definition at line 363 of file symex_goto.cpp.
References goto_symex_statet::guard, exprt::is_false(), value_sett::make_union(), goto_symex_statet::value_set, and goto_symex_statet::goto_statet::value_set.
Referenced by merge_goto().
|
inlineprotectedvirtual |
Reimplemented in symex_bmct.
Definition at line 341 of file goto_symex.h.
Referenced by symex_function_call_code().
|
protected |
Definition at line 28 of file symex_function_call.cpp.
References symbolt::base_name, base_type_eq(), byte_extract_id(), dstringt::empty(), messaget::eom(), namespace_baset::follow(), from_integer(), code_typet::parametert::get_identifier(), code_typet::has_ellipsis(), irept::id(), id2string(), index_type(), symbol_tablet::insert(), irept::is_nil(), log, namespacet::lookup(), symbolt::mode, symbolt::name, ns, code_typet::parameters(), symex_targett::sourcet::pc, irept::pretty(), goto_symex_statet::source, symbolt::symbol_expr(), goto_symex_statet::symbol_table, symex_assign(), to_string(), symbolt::type, exprt::type(), and messaget::warning().
Referenced by symex_function_call_code().
|
protected |
Definition at line 376 of file symex_goto.cpp.
References guardt::as_expr(), symex_target_equationt::assignment(), goto_symex_statet::assignment(), goto_symex_statet::atomic_section_id, messaget::conditional_output(), goto_symex_statet::renaming_levelt::current_count(), messaget::debug(), goto_symex_statet::dirty, do_simplify(), messaget::eom(), symbol_exprt::get_identifier(), ssa_exprt::get_original_expr(), goto_symex_statet::renaming_levelt::get_variables(), goto_symex_statet::guard, goto_symex_statet::goto_statet::guard, guard_identifier, exprt::is_false(), symbolt::is_shared(), goto_symex_statet::level2, goto_symex_statet::goto_statet::level2_current_count(), goto_symex_statet::goto_statet::level2_get_variables(), log, namespacet::lookup(), symbolt::name, ns, symex_targett::PHI, pointer_offset_bits(), goto_symex_statet::propagation, goto_symex_statet::goto_statet::propagation, goto_symex_statet::record_events, ssa_exprt::set_level_2(), goto_symex_statet::source, target, symex_targett::sourcet::thread_nr, goto_symex_statet::threads, to_ssa_expr(), to_string(), exprt::type(), and goto_symex_statet::propagationt::values.
Referenced by merge_goto().
|
protected |
pop one call frame
Definition at line 317 of file symex_function_call.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::calling_location, goto_symex_statet::renaming_levelt::current_names, goto_symex_statet::dirty, goto_symex_statet::level1, goto_symex_statet::level2, goto_symex_statet::framet::local_objects, goto_symex_statet::framet::old_level1, symex_targett::sourcet::pc, goto_symex_statet::pop_frame(), PRECONDITION, goto_symex_statet::level1t::restore_from(), symex_transition(), goto_symex_statet::threads, and goto_symex_statet::top().
Referenced by symex_end_of_function().
|
protected |
Given an expression, find the root object and the offset into it.
The extra complication to be considered here is that the expression may have any number of ternary expressions mixed with type casts.
Definition at line 24 of file symex_clean_expr.cpp.
References index_exprt::array(), base_type_eq(), object_descriptor_exprt::build(), byte_extract_id(), char_type(), do_simplify(), if_exprt::false_case(), from_integer(), irept::get_bool(), ssa_exprt::get_original_expr(), irept::id(), index_type(), exprt::is_zero(), exprt::make_typecast(), ns, object_descriptor_exprt::offset(), exprt::op0(), object_descriptor_exprt::root_object(), array_typet::size(), size_of_expr(), typet::subtype(), irept::swap(), to_address_of_expr(), to_array_type(), to_if_expr(), to_index_expr(), to_ssa_expr(), if_exprt::true_case(), and exprt::type().
Referenced by symex_other().
|
protected |
|
protected |
Definition at line 32 of file goto_symex.cpp.
References exprt::add_source_location(), build_symex_nondet(), Forall_operands, irept::get(), irept::id(), exprt::source_location(), irept::swap(), and exprt::type().
Referenced by clean_expr().
|
virtual |
Performs symbolic execution using a state and equation that have already been used to symex part of the program.
The state is not re-initialized; instead, symbolic execution resumes from the program counter of the saved state.
Definition at line 223 of file symex_main.cpp.
References symex_with_state().
Referenced by path_explorert::perform_symbolic_execution().
|
protected |
Definition at line 426 of file symex_function_call.cpp.
References guardt::as_expr(), source_locationt::as_string(), base_type_eq(), goto_programt::instructiont::code, goto_symex_statet::guard, irept::is_not_nil(), goto_programt::instructiont::is_return(), code_assignt::lhs(), symex_target_equationt::location(), ns, exprt::op0(), symex_targett::sourcet::pc, PRECONDITION, irept::pretty(), goto_symex_statet::framet::return_value, code_assignt::rhs(), goto_symex_statet::source, goto_programt::instructiont::source_location, symex_assign(), target, to_code_return(), goto_symex_statet::top(), and exprt::type().
Referenced by symex_step().
Definition at line 104 of file symex_main.cpp.
References irept::id(), exprt::op0(), exprt::op1(), exprt::operands(), PRECONDITION, irept::swap(), symex_decl(), to_ssa_expr(), and to_symbol_expr().
Referenced by vcc().
|
protectedvirtual |
Definition at line 43 of file symex_builtin_functions.cpp.
References symbol_table_baset::add(), index_exprt::array(), symbolt::base_name, build_symex_nondet(), c_sizeof_type_rec(), dynamic_counter, from_integer(), irept::id(), id2string(), index_type(), INVARIANT, exprt::is_constant(), exprt::is_false(), symbolt::is_lvalue, irept::is_nil(), irept::is_not_nil(), exprt::is_zero(), symbol_table_baset::lookup(), exprt::make_typecast(), symbolt::mode, symbolt::name, ns, exprt::op0(), exprt::op1(), exprt::operands(), outer_symbol_table, symex_targett::sourcet::pc, pointer_offset_size(), pointer_type(), PRECONDITION, goto_symex_statet::rename(), irept::set(), simplify(), array_typet::size(), goto_symex_statet::source, exprt::source_location(), typet::subtype(), symbolt::symbol_expr(), goto_symex_statet::symbol_table, symex_assign(), to_array_type(), to_integer(), to_string(), symbolt::type, exprt::type(), unsigned_char_type(), symbolt::value, and zero_initializer().
Referenced by symex_assign().
|
protected |
Definition at line 23 of file symex_assign.cpp.
References clean_expr(), side_effect_exprt::get_statement(), symex_targett::HIDDEN, goto_symex_statet::framet::hidden_function, irept::id(), id2string(), irept::is_not_nil(), code_assignt::lhs(), exprt::op0(), exprt::operands(), symex_targett::sourcet::pc, code_assignt::rhs(), goto_symex_statet::source, symex_targett::STATE, symex_allocate(), symex_assign_rec(), symex_cpp_new(), symex_gcc_builtin_va_arg_next(), symex_printf(), to_side_effect_expr(), to_symbol_expr(), and goto_symex_statet::top().
Referenced by havoc_rec(), initialize_auto_object(), parameter_assignments(), return_assignment(), symex_allocate(), symex_cpp_new(), symex_function_call_code(), symex_gcc_builtin_va_arg_next(), symex_other(), and symex_step().
|
protected |
Definition at line 297 of file symex_assign.cpp.
References add_to_lhs(), index_exprt::array(), update_exprt::designator(), namespace_baset::follow(), irept::id(), irept::id_string(), index_exprt::index(), update_exprt::new_value(), ns, update_exprt::old(), exprt::operands(), symex_assign_rec(), and exprt::type().
Referenced by symex_assign_rec().
|
protected |
Definition at line 459 of file symex_assign.cpp.
References add_to_lhs(), exprt::copy_to_operands(), irept::id(), byte_extract_exprt::offset(), byte_extract_exprt::op(), symex_assign_rec(), exprt::type(), and UNREACHABLE.
Referenced by symex_assign_rec().
|
protected |
Definition at line 426 of file symex_assign.cpp.
References guardt::add(), if_exprt::cond(), do_simplify(), if_exprt::false_case(), exprt::is_false(), exprt::is_true(), ns, goto_symex_statet::rename(), symex_assign_rec(), and if_exprt::true_case().
Referenced by symex_assign_rec().
|
protected |
Definition at line 120 of file symex_assign.cpp.
References namespace_baset::follow(), irept::get_bool(), irept::id(), irept::id_string(), ns, exprt::op0(), exprt::op1(), exprt::operands(), symex_assign_array(), symex_assign_byte_extract(), symex_assign_if(), symex_assign_struct_member(), symex_assign_symbol(), symex_assign_typecast(), to_byte_extract_expr(), to_if_expr(), to_index_expr(), to_member_expr(), to_ssa_expr(), to_typecast_expr(), and exprt::type().
Referenced by symex_assign(), symex_assign_array(), symex_assign_byte_extract(), symex_assign_if(), symex_assign_struct_member(), and symex_assign_typecast().
|
protected |
Definition at line 353 of file symex_assign.cpp.
References add_to_lhs(), namespace_baset::follow(), member_exprt::get_component_name(), irept::id(), ns, update_exprt::old(), exprt::op0(), exprt::op1(), exprt::operands(), irept::set(), symex_assign_rec(), and exprt::type().
Referenced by symex_assign_rec().
|
protected |
Definition at line 198 of file symex_assign.cpp.
References add_to_lhs(), allow_pointer_unsoundness, guardt::append(), guardt::as_expr(), symex_target_equationt::assignment(), goto_symex_statet::assignment(), if_exprt::cond(), messaget::conditional_output(), constant_propagation, goto_symex_statet::renaming_levelt::current_count(), messaget::debug(), do_simplify(), dstringt::empty(), messaget::eom(), if_exprt::false_case(), optionst::get_bool_option(), symbol_exprt::get_identifier(), ssa_exprt::get_level_1(), ssa_exprt::get_object_name(), ssa_exprt::get_original_expr(), goto_symex_statet::guard, symex_targett::HIDDEN, symbolt::is_auxiliary, symbolt::is_parameter, exprt::is_true(), goto_symex_statet::level2, log, namespacet::lookup(), ns, options, pointer_offset_bits(), goto_symex_statet::record_events, goto_symex_statet::rename(), goto_symex_statet::source, irept::swap(), target, to_symbol_expr(), if_exprt::true_case(), and exprt::type().
Referenced by symex_assign_rec(), and symex_start_thread().
|
protected |
Definition at line 276 of file symex_assign.cpp.
References add_to_lhs(), exprt::make_typecast(), exprt::op0(), exprt::operands(), symex_assign_rec(), and exprt::type().
Referenced by symex_assign_rec().
Definition at line 75 of file symex_main.cpp.
References guardt::add(), guardt::as_expr(), symex_target_equationt::assumption(), goto_symex_statet::atomic_section_id, do_simplify(), goto_symex_statet::guard, guardt::guard_expr(), exprt::is_false(), exprt::is_true(), goto_symex_statet::source, symex_atomic_end(), target, and goto_symex_statet::threads.
Referenced by loop_bound_exceeded(), symex_goto(), symex_step(), and symex_throw().
|
protectedvirtual |
Definition at line 14 of file symex_atomic_section.cpp.
References guardt::as_expr(), symex_target_equationt::atomic_begin(), atomic_section_counter, goto_symex_statet::atomic_section_id, goto_symex_statet::guard, exprt::is_false(), symex_targett::sourcet::pc, goto_symex_statet::read_in_atomic_section, goto_symex_statet::source, target, and goto_symex_statet::written_in_atomic_section.
Referenced by symex_step().
|
protectedvirtual |
Definition at line 34 of file symex_atomic_section.cpp.
References guardt::as_expr(), symex_target_equationt::atomic_end(), goto_symex_statet::atomic_section_id, goto_symex_statet::renaming_levelt::current_count(), do_simplify(), symbol_exprt::get_identifier(), goto_symex_statet::guard, exprt::is_false(), goto_symex_statet::level2, r, goto_symex_statet::read_in_atomic_section, ssa_exprt::set_level_2(), symex_target_equationt::shared_read(), symex_target_equationt::shared_write(), goto_symex_statet::source, target, and goto_symex_statet::written_in_atomic_section.
Referenced by symex_assume(), and symex_step().
|
protected |
Definition at line 14 of file symex_catch.cpp.
References goto_programt::instructiont::code, irept::find(), irept::get_sub(), goto_programt::instructiont::targets, and UNREACHABLE.
Referenced by symex_step().
Definition at line 455 of file symex_builtin_functions.cpp.
Referenced by symex_other().
|
protectedvirtual |
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
state | Symex state |
lhs | left-hand side of assignment |
code | right-hand side containing side effect |
Definition at line 393 of file symex_builtin_functions.cpp.
References symbol_table_baset::add(), symbolt::base_name, clean_expr(), dynamic_counter, irept::find(), from_integer(), irept::get(), irept::id(), id2string(), index_type(), INVARIANT_WITH_IREP, symbolt::is_lvalue, symbolt::mode, exprt::move_to_operands(), symbolt::name, irept::set(), typet::subtype(), symbolt::symbol_expr(), goto_symex_statet::symbol_table, symex_assign(), to_string(), symbolt::type, and exprt::type().
Referenced by symex_assign().
|
protectedvirtual |
Definition at line 20 of file symex_dead.cpp.
References value_sett::assign(), goto_programt::instructiont::code, goto_symex_statet::renaming_levelt::current_names, namespace_baset::follow(), get_failed_symbol(), symbol_exprt::get_identifier(), irept::id(), goto_symex_statet::renaming_levelt::increase_counter(), irept::is_not_nil(), goto_symex_statet::L1, goto_symex_statet::level2, ns, exprt::op0(), exprt::operands(), symex_targett::sourcet::pc, goto_symex_statet::propagation, goto_symex_statet::propagationt::remove(), goto_symex_statet::rename(), goto_symex_statet::source, to_pointer_type(), to_ssa_expr(), to_symbol_expr(), exprt::type(), and goto_symex_statet::value_set.
Referenced by symex_step().
|
protectedvirtual |
Definition at line 22 of file symex_decl.cpp.
References goto_programt::instructiont::code, irept::id(), exprt::op0(), exprt::operands(), symex_targett::sourcet::pc, goto_symex_statet::source, and to_symbol_expr().
Referenced by rewrite_quantifiers(), and symex_step().
|
protectedvirtual |
Definition at line 40 of file symex_decl.cpp.
References guardt::as_expr(), value_sett::assign(), goto_symex_statet::atomic_section_id, goto_symex_statet::renaming_levelt::current_names, symex_target_equationt::decl(), goto_symex_statet::dirty, namespace_baset::follow(), get_failed_symbol(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), goto_symex_statet::guard, symex_targett::HIDDEN, goto_symex_statet::framet::hidden_function, goto_symex_statet::renaming_levelt::increase_counter(), irept::is_not_nil(), goto_symex_statet::L1, goto_symex_statet::level2, namespacet::lookup(), ns, symex_targett::sourcet::pc, goto_symex_statet::propagation, goto_symex_statet::record_events, goto_symex_statet::propagationt::remove(), goto_symex_statet::rename(), symex_target_equationt::shared_write(), goto_symex_statet::source, symex_targett::STATE, target, to_pointer_type(), goto_symex_statet::top(), exprt::type(), ssa_exprt::update_type(), and goto_symex_statet::value_set.
|
protectedvirtual |
do function call by inlining
Definition at line 357 of file symex_function_call.cpp.
References guardt::as_expr(), symex_target_equationt::function_return(), goto_symex_statet::guard, symex_targett::sourcet::pc, pop_frame(), goto_symex_statet::source, and target.
Referenced by symex_step().
|
protectedvirtual |
Definition at line 504 of file symex_builtin_functions.cpp.
References Forall_operands, exprt::reserve_operands(), and UNREACHABLE.
Referenced by symex_function_call_symbol().
|
virtual |
symex entire program starting from entry point
The state that goto_symext maintains has a large memory footprint. This method deallocates the state as soon as symbolic execution has completed, so use it if you don't care about having the state around afterwards.
Definition at line 267 of file symex_main.cpp.
References get_function_from_goto_functions().
Referenced by bmct::perform_symbolic_execution().
|
virtual |
symex entire program starting from entry point
The state that goto_symext maintains has a large memory footprint. This method deallocates the state as soon as symbolic execution has completed, so use it if you don't care about having the state around afterwards.
Definition at line 275 of file symex_main.cpp.
References goto_functionst::entry_point(), initialize_entry_point(), and symex_with_state().
|
protectedvirtual |
Definition at line 168 of file symex_function_call.cpp.
References code_function_callt::function(), and symex_function_call_symbol().
Referenced by symex_step().
|
protectedvirtual |
do function call by inlining
Definition at line 214 of file symex_function_call.cpp.
References guardt::add(), code_function_callt::arguments(), guardt::as_expr(), goto_symex_statet::call_stack(), goto_symex_statet::dirty, code_function_callt::function(), symex_target_equationt::function_call(), symex_target_equationt::function_return(), optionst::get_bool_option(), get_unwind_recursion(), goto_symex_statet::guard, irept::is_not_nil(), symex_targett::sourcet::is_set, code_function_callt::lhs(), locality(), goto_symex_statet::framet::loop_iterations, goto_symex_statet::new_frame(), no_body(), ns, options, parameter_assignments(), incremental_dirtyt::populate_dirty_for_function(), PRECONDITION, goto_symex_statet::previous_frame(), goto_symex_statet::rename(), safe_pointers, goto_symex_statet::source, exprt::source_location(), symex_assign(), symex_transition(), target, symex_targett::sourcet::thread_nr, to_symbol_expr(), goto_symex_statet::top(), exprt::type(), and vcc().
Referenced by symex_function_call_symbol().
|
protectedvirtual |
Definition at line 185 of file symex_function_call.cpp.
References guardt::as_expr(), CPROVER_FKT_PREFIX, CPROVER_MACRO_PREFIX, code_function_callt::function(), goto_symex_statet::guard, has_prefix(), irept::id(), id2string(), symex_target_equationt::location(), PRECONDITION, goto_symex_statet::source, symex_fkt(), symex_function_call_code(), symex_macro(), symex_trace(), target, and to_symbol_expr().
Referenced by symex_function_call().
|
protectedvirtual |
Definition at line 232 of file symex_builtin_functions.cpp.
References do_simplify(), get_symbol(), has_prefix(), id2string(), irept::is_nil(), namespacet::lookup(), exprt::make_typecast(), symbolt::name, ns, exprt::op0(), exprt::operands(), pos(), goto_symex_statet::rename(), safe_string2unsigned(), exprt::source_location(), symex_assign(), to_string(), symbolt::type, exprt::type(), and zero_initializer().
Referenced by symex_assign().
|
protectedvirtual |
Definition at line 22 of file symex_goto.cpp.
References guardt::add(), guardt::as_expr(), symex_target_equationt::assignment(), goto_symex_statet::assignment(), goto_symex_statet::call_stack(), clean_expr(), goto_programt::instructiont::code, messaget::conditional_output(), DATA_INVARIANT, messaget::debug(), do_simplify(), doing_path_exploration, messaget::eom(), symbol_exprt::get_identifier(), goto_programt::instructiont::get_target(), get_unwind(), symex_target_equationt::goto_instruction(), goto_symex_statet::framet::goto_state_map, goto_symex_statet::guard, symex_targett::GUARD, goto_programt::instructiont::guard, goto_symex_statet::goto_statet::guard, guard_identifier, goto_symex_statet::has_saved_jump_target, goto_symex_statet::has_saved_next_instruction, irept::id(), goto_programt::instructiont::incoming_edges, INVARIANT, goto_programt::instructiont::is_backwards_goto(), exprt::is_false(), exprt::is_true(), goto_symex_statet::L1, symex_target_equationt::location(), log, loop_bound_exceeded(), goto_programt::loop_id(), goto_symex_statet::framet::loop_iterations, exprt::make_false(), exprt::make_not(), ns, exprt::op0(), exprt::operands(), path_storage, symex_targett::sourcet::pc, pointer_offset_bits(), irept::pretty(), path_storaget::push(), goto_symex_statet::rename(), goto_symex_statet::saved_target, goto_symex_statet::saved_target_is_backwards, self_loops_to_assumptions, should_pause_symex, goto_symex_statet::source, messaget::mstreamt::source_location, path_storaget::patht::state, symex_assume(), symex_transition(), target, goto_programt::instructiont::targets, goto_symex_statet::top(), and exprt::type().
Referenced by symex_step().
Definition at line 338 of file symex_builtin_functions.cpp.
References guardt::as_expr(), do_simplify(), get_string_argument(), goto_symex_statet::guard, symex_target_equationt::input(), ns, exprt::op0(), exprt::operands(), goto_symex_statet::rename(), goto_symex_statet::source, and target.
Referenced by symex_other().
|
virtual |
Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached.
This is useful to explicitly symex certain ranges of a program, e.g. in an incremental decision procedure.
state | Symex state to start with. |
goto_functions | GOTO model to symex. |
first | Entry point in form of a first instruction. |
limit | Final instruction, which itself will not be symexed. |
Definition at line 245 of file symex_main.cpp.
References get_function_from_goto_functions().
|
virtual |
Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached.
This is useful to explicitly symex certain ranges of a program, e.g. in an incremental decision procedure.
state | Symex state to start with. |
get_goto_function | retrieves a function body |
first | Entry point in form of a first instruction. |
limit | Final instruction, which itself will not be symexed. |
Definition at line 255 of file symex_main.cpp.
References initialize_entry_point(), ns, outer_symbol_table, symex_targett::sourcet::pc, goto_symex_statet::source, goto_symex_statet::symbol_table, and symex_threaded_step().
|
protectedvirtual |
Definition at line 528 of file symex_builtin_functions.cpp.
References exprt::copy_to_operands(), CPROVER_MACRO_PREFIX, irept::get(), irept::id(), id2string(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::op3(), and replace_expr().
Referenced by symex_function_call_symbol().
|
protectedvirtual |
Definition at line 77 of file symex_other.cpp.
References guardt::as_expr(), base_type_eq(), byte_extract_id(), char_type(), clean_expr(), goto_programt::instructiont::code, DATA_INVARIANT, do_simplify(), from_integer(), codet::get_statement(), goto_symex_statet::guard, havoc_rec(), id2string(), index_type(), code_assignt::lhs(), exprt::make_typecast(), symex_target_equationt::memory_barrier(), ns, byte_extract_exprt::offset(), byte_extract_exprt::op(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), symex_targett::sourcet::pc, process_array_expr(), size_of_expr(), goto_symex_statet::source, typet::subtype(), irept::swap(), symex_assign(), symex_cpp_delete(), symex_input(), symex_output(), symex_printf(), target, to_array_type(), exprt::type(), and UNREACHABLE.
Referenced by symex_step().
Definition at line 363 of file symex_builtin_functions.cpp.
References guardt::as_expr(), do_simplify(), get_string_argument(), goto_symex_statet::guard, ns, exprt::op0(), exprt::operands(), symex_target_equationt::output(), goto_symex_statet::rename(), goto_symex_statet::source, and target.
Referenced by symex_other().
Definition at line 312 of file symex_builtin_functions.cpp.
References guardt::as_expr(), do_simplify(), get_string_argument(), goto_symex_statet::guard, ns, exprt::operands(), symex_target_equationt::output_fmt(), goto_symex_statet::rename(), goto_symex_statet::source, and target.
Referenced by symex_assign(), and symex_other().
|
protectedvirtual |
Definition at line 16 of file symex_start_thread.cpp.
References guardt::as_expr(), goto_symex_statet::atomic_section_id, goto_symex_statet::threadt::call_stack, goto_symex_statet::renaming_levelt::current_names, namespacet::get_symbol_table(), goto_programt::instructiont::get_target(), goto_symex_statet::guard, goto_symex_statet::threadt::guard, symex_targett::HIDDEN, symbolt::is_extern, exprt::is_false(), irept::is_nil(), symbolt::is_static_lifetime, symbolt::is_thread_local, goto_symex_statet::L1, goto_symex_statet::l1_history, goto_symex_statet::level1, goto_symex_statet::level2, goto_symex_statet::framet::local_objects, symbolt::location, ns, symex_targett::sourcet::pc, goto_symex_statet::threadt::pc, goto_symex_statet::record_events, goto_symex_statet::rename(), ssa_exprt::set_level_0(), goto_symex_statet::source, symex_target_equationt::spawn(), symbolt::symbol_expr(), symbol_table_baset::symbols, symex_assign_symbol(), target, goto_programt::instructiont::targets, goto_symex_statet::threads, goto_symex_statet::top(), symbolt::type, UNREACHABLE, symbolt::value, and zero_initializer().
Referenced by symex_step().
|
protectedvirtual |
do just one step
Reimplemented in symex_bmct.
Definition at line 302 of file symex_main.cpp.
References guardt::add(), code_function_callt::arguments(), guardt::as_expr(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, goto_symex_statet::call_stack(), CATCH, clean_expr(), DEAD, DECL, goto_symex_statet::depth, doing_path_exploration, END_FUNCTION, END_THREAD, Forall_expr, format(), code_function_callt::function(), FUNCTION_CALL, GOTO, goto_symex_statet::guard, id2string(), exprt::is_false(), irept::is_not_nil(), code_function_callt::lhs(), LOCATION, symex_target_equationt::location(), max_depth, merge_gotos(), NO_INSTRUCTION_TYPE, ns, OTHER, symex_targett::sourcet::pc, PRECONDITION, goto_symex_statet::rename(), RETURN, return_assignment(), SKIP, goto_symex_statet::source, START_THREAD, symex_assign(), symex_assume(), symex_atomic_begin(), symex_atomic_end(), symex_catch(), symex_dead(), symex_decl(), symex_end_of_function(), symex_function_call(), symex_goto(), symex_other(), symex_start_thread(), symex_throw(), symex_transition(), target, goto_symex_statet::threads, THROW, to_code_assign(), to_code_function_call(), and vcc().
Referenced by symex_bmct::symex_step(), and symex_threaded_step().
|
virtual |
Definition at line 302 of file symex_goto.cpp.
References guardt::as_expr(), symex_target_equationt::assumption(), dereference(), do_simplify(), goto_symex_statet::guard, goto_programt::instructiont::guard, guardt::guard_expr(), exprt::make_not(), ns, symex_targett::sourcet::pc, goto_symex_statet::rename(), goto_symex_statet::source, and target.
|
protected |
Invokes symex_step and verifies whether additional threads can be executed.
state | Current GOTO symex step. |
get_goto_function | function that retrieves function bodies |
Definition at line 148 of file symex_main.cpp.
References goto_symex_statet::call_stack(), symex_targett::sourcet::pc, should_pause_symex, goto_symex_statet::source, goto_symex_statet::switch_to_thread(), symex_step(), symex_transition(), symex_targett::sourcet::thread_nr, and goto_symex_statet::threads.
Referenced by symex_instruction_range(), and symex_with_state().
|
protected |
Definition at line 14 of file symex_throw.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::catch_map, goto_programt::instructiont::code, irept::find(), irept::get_sub(), symex_targett::sourcet::pc, goto_symex_statet::source, and symex_assume().
Referenced by symex_step().
|
protectedvirtual |
Definition at line 465 of file symex_builtin_functions.cpp.
References code_function_callt::arguments(), guardt::as_expr(), optionst::get_option(), goto_symex_statet::guard, ns, options, symex_target_equationt::output(), goto_symex_statet::rename(), goto_symex_statet::source, target, to_integer(), and unsafe_string2int().
Referenced by symex_function_call_symbol().
|
protectedvirtual |
Definition at line 24 of file symex_main.cpp.
References goto_symex_statet::call_stack(), goto_programt::instructiont::incoming_edges, goto_programt::loop_id(), goto_symex_statet::framet::loop_iterations, symex_targett::sourcet::pc, goto_symex_statet::source, and goto_symex_statet::top().
Referenced by initialize_entry_point(), pop_frame(), symex_function_call_code(), symex_goto(), symex_step(), symex_threaded_step(), and symex_transition().
|
inlineprotectedvirtual |
Definition at line 289 of file goto_symex.h.
References symex_targett::sourcet::pc, goto_symex_statet::source, symex_dereference_statet::state, and symex_transition().
|
virtual |
symex entire program starting from entry point
This method uses the state
argument as the symbolic execution state, which is useful for examining the state after this method returns. The state that goto_symext maintains has a large memory footprint, so if keeping the state around is not necessary, clients should instead call goto_symext::symex_from_entry_point_of().
Definition at line 177 of file symex_main.cpp.
References get_function_from_goto_functions().
Referenced by scratch_programt::check_sat(), resume_symex_from_saved_state(), and symex_from_entry_point_of().
|
virtual |
symex entire program starting from entry point
This method uses the state
argument as the symbolic execution state, which is useful for examining the state after this method returns. The state that goto_symext maintains has a large memory footprint, so if keeping the state around is not necessary, clients should instead call goto_symext::symex_from_entry_point_of().
Definition at line 188 of file symex_main.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::end_of_function, goto_symex_statet::has_saved_jump_target, goto_symex_statet::has_saved_next_instruction, ns, outer_symbol_table, PRECONDITION, should_pause_symex, goto_symex_statet::symbol_table, symex_threaded_step(), and goto_symex_statet::top().
Definition at line 83 of file auto_objects.cpp.
References symbolt::base_name, goto_symex_statet::renaming_levelt::current_names, forall_operands, irept::get_bool(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), has_prefix(), irept::id(), id2string(), initialize_auto_object(), goto_symex_statet::level2, namespacet::lookup(), ns, and to_ssa_expr().
Referenced by dereference_rec().
|
protectedvirtual |
Definition at line 48 of file symex_main.cpp.
References guardt::as_expr(), symex_target_equationt::assertion(), do_simplify(), goto_symex_statet::guard, guardt::guard_expr(), exprt::is_true(), ns, remaining_vccs, goto_symex_statet::rename(), rewrite_quantifiers(), goto_symex_statet::source, target, and total_vccs.
Referenced by loop_bound_exceeded(), symex_function_call_code(), and symex_step().
|
friend |
Definition at line 245 of file goto_symex.h.
|
protected |
Definition at line 208 of file goto_symex.h.
Referenced by symex_assign_symbol().
|
protected |
Definition at line 241 of file goto_symex.h.
Referenced by symex_atomic_begin().
bool goto_symext::constant_propagation |
Definition at line 217 of file goto_symex.h.
Referenced by bmct::bmct(), scratch_programt::check_sat(), and symex_assign_symbol().
|
protected |
Definition at line 207 of file goto_symex.h.
Referenced by symex_goto(), and symex_step().
|
staticprotected |
Definition at line 464 of file goto_symex.h.
Referenced by make_auto_object(), symex_allocate(), and symex_cpp_new().
|
protected |
Definition at line 281 of file goto_symex.h.
Referenced by phi_function(), and symex_goto().
irep_idt goto_symext::language_mode |
language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.
Definition at line 222 of file goto_symex.h.
Referenced by dereference_rec(), and bmct::setup().
|
mutableprotected |
Definition at line 243 of file goto_symex.h.
Referenced by symex_bmct::get_unwind(), symex_bmct::get_unwind_recursion(), symex_bmct::no_body(), parameter_assignments(), phi_function(), symex_assign_symbol(), symex_goto(), and symex_bmct::symex_step().
|
protected |
Definition at line 206 of file goto_symex.h.
Referenced by symex_step().
|
staticprotected |
Definition at line 463 of file goto_symex.h.
Referenced by build_symex_nondet().
|
protected |
Initialized just before symbolic execution begins, to point to both outer_symbol_table
and the symbol table owned by the goto_symex_statet
object used during symbolic execution.
That symbol table must be owned by goto_symex_statet rather than passed in, in case the state is saved and resumed. This namespacet is used during symbolic execution to look up names from the original goto-program, and the names of dynamically-created objects.
Definition at line 239 of file goto_symex.h.
Referenced by address_arithmetic(), clean_expr(), dereference(), dereference_rec(), do_simplify(), symex_bmct::get_unwind_recursion(), symex_dereference_statet::get_value_set(), symex_dereference_statet::has_failed_symbol(), initialize_auto_object(), locality(), parameter_assignments(), phi_function(), process_array_expr(), return_assignment(), symex_allocate(), symex_assign_array(), symex_assign_if(), symex_assign_rec(), symex_assign_struct_member(), symex_assign_symbol(), symex_dead(), symex_decl(), symex_function_call_code(), symex_gcc_builtin_va_arg_next(), symex_goto(), symex_input(), symex_instruction_range(), symex_other(), symex_output(), symex_printf(), symex_start_thread(), symex_bmct::symex_step(), symex_step(), symex_step_goto(), symex_trace(), symex_with_state(), trigger_auto_object(), and vcc().
|
protected |
Definition at line 204 of file goto_symex.h.
Referenced by dereference_rec(), do_simplify(), loop_bound_exceeded(), symex_assign_symbol(), symex_function_call_code(), and symex_trace().
|
protected |
The symbol table associated with the goto-program that we're executing.
This symbol table will not additionally contain objects that are dynamically created as part of symbolic execution; the names of those object are stored in the symbol table passed as the new_symbol_table
argument to the symex_*
methods.
Definition at line 230 of file goto_symex.h.
Referenced by symex_allocate(), symex_instruction_range(), and symex_with_state().
|
protected |
Definition at line 470 of file goto_symex.h.
Referenced by symex_goto().
unsigned goto_symext::remaining_vccs |
Definition at line 215 of file goto_symex.h.
Referenced by bmct::execute(), bmct::slice(), and vcc().
|
protected |
Definition at line 472 of file goto_symex.h.
Referenced by dereference_rec(), initialize_entry_point(), and symex_function_call_code().
bool goto_symext::self_loops_to_assumptions |
Definition at line 218 of file goto_symex.h.
Referenced by bmct::bmct(), and symex_goto().
bool goto_symext::should_pause_symex |
Have states been pushed onto the workqueue?
If this flag is set at the end of a symbolic execution run, it means that symex has been paused because we encountered a GOTO instruction while doing path exploration, and thus pushed the successor states of the GOTO onto path_storage. The symbolic execution caller should now choose which successor state to continue executing, and resume symex from that state.
Definition at line 177 of file goto_symex.h.
Referenced by bmct::execute(), symex_goto(), symex_threaded_step(), and symex_with_state().
|
protected |
Definition at line 240 of file goto_symex.h.
Referenced by initialize_entry_point(), phi_function(), return_assignment(), symex_assign_symbol(), symex_assume(), symex_atomic_begin(), symex_atomic_end(), symex_decl(), symex_end_of_function(), symex_function_call_code(), symex_function_call_symbol(), symex_goto(), symex_input(), symex_other(), symex_output(), symex_printf(), symex_start_thread(), symex_step(), symex_step_goto(), symex_trace(), and vcc().
unsigned goto_symext::total_vccs |
Definition at line 215 of file goto_symex.h.
Referenced by bmct::slice(), and vcc().