cprover
|
#include <symex_bmc.h>
Public Types | |
typedef std::function< tvt(const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)> | loop_unwind_handlert |
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set. More... | |
typedef std::function< tvt(const irep_idt &, unsigned, unsigned &)> | recursion_unwind_handlert |
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set. More... | |
![]() | |
typedef goto_symex_statet | statet |
typedef std::function< const goto_functionst::goto_functiont &(const irep_idt &)> | get_goto_functiont |
Public Member Functions | |
symex_bmct (message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage) | |
void | add_loop_unwind_handler (loop_unwind_handlert handler) |
Add a callback function that will be called to determine whether to unwind loops. More... | |
void | add_recursion_unwind_handler (recursion_unwind_handlert handler) |
Add a callback function that will be called to determine whether to unwind recursion. More... | |
bool | output_coverage_report (const goto_functionst &goto_functions, const std::string &path) const |
![]() | |
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 | |
source_locationt | last_source_location |
bool | record_coverage |
unwindsett | unwindset |
![]() | |
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 Member Functions | |
virtual void | symex_step (const get_goto_functiont &get_goto_function, statet &state) |
show progress More... | |
virtual void | merge_goto (const statet::goto_statet &goto_state, statet &state) |
virtual bool | get_unwind (const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind) |
virtual bool | get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) |
virtual void | no_body (const irep_idt &identifier) |
![]() | |
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... | |
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 &) |
void | merge_value_sets (const statet::goto_statet &goto_state, statet &dest) |
void | phi_function (const statet::goto_statet &goto_state, statet &) |
virtual void | loop_bound_exceeded (statet &, const exprt &guard) |
void | pop_frame (statet &) |
pop one call frame More... | |
void | return_assignment (statet &) |
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... | |
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 &) |
Protected Attributes | |
std::vector< loop_unwind_handlert > | loop_unwind_handlers |
Callbacks that may provide an unwind/do-not-unwind decision for a loop. More... | |
std::vector< recursion_unwind_handlert > | recursion_unwind_handlers |
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call. More... | |
std::unordered_set< irep_idt > | body_warnings |
symex_coveraget | symex_coverage |
![]() | |
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 |
Additional Inherited Members | |
![]() | |
typedef symex_targett::assignment_typet | assignment_typet |
![]() | |
static bool | is_index_member_symbol_if (const exprt &expr) |
static exprt | add_to_lhs (const exprt &lhs, const exprt &what) |
![]() | |
static unsigned | nondet_count =0 |
static unsigned | dynamic_counter =0 |
Definition at line 25 of file symex_bmc.h.
typedef std::function<tvt( const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)> symex_bmct::loop_unwind_handlert |
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
If set the advisory maximum is set it is only used to print useful information for the user (e.g. "unwinding iteration N, max M"), and is not enforced. They return true to halt unwinding, false to authorise unwinding, or Unknown to indicate they have no opinion.
Definition at line 47 of file symex_bmc.h.
typedef std::function<tvt(const irep_idt &, unsigned, unsigned &)> symex_bmct::recursion_unwind_handlert |
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
If set the advisory maximum is set it is only used to print useful information for the user (e.g. "unwinding iteration N, max M"), and is not enforced. They return true to halt unwinding, false to authorise unwinding, or Unknown to indicate they have no opinion.
Definition at line 56 of file symex_bmc.h.
symex_bmct::symex_bmct | ( | message_handlert & | mh, |
const symbol_tablet & | outer_symbol_table, | ||
symex_target_equationt & | _target, | ||
const optionst & | options, | ||
path_storaget & | path_storage | ||
) |
Definition at line 21 of file symex_bmc.cpp.
|
inline |
Add a callback function that will be called to determine whether to unwind loops.
The first function added will get the first chance to answer, and the first authoratitive (true or false) answer is final.
handler | new callback |
Definition at line 62 of file symex_bmc.h.
References loop_unwind_handlers.
Referenced by bmct::add_loop_unwind_handler().
|
inline |
Add a callback function that will be called to determine whether to unwind recursion.
The first function added will get the first chance to answer, and the first authoratitive (true or false) answer is final.
handler | new callback |
Definition at line 71 of file symex_bmc.h.
References recursion_unwind_handlers.
Referenced by bmct::add_unwind_recursion_handler().
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 107 of file symex_bmc.cpp.
References messaget::eom(), unwindsett::get_limit(), INVARIANT, tvt::is_known(), tvt::is_true(), tvt::is_unknown(), goto_symext::log, goto_programt::loop_id(), loop_unwind_handlers, symex_targett::sourcet::pc, messaget::statistics(), symex_targett::sourcet::thread_nr, and unwindset.
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 153 of file symex_bmc.cpp.
References symbolt::display_name(), messaget::eom(), unwindsett::get_limit(), INVARIANT, tvt::is_known(), tvt::is_true(), tvt::is_unknown(), goto_symext::log, namespacet::lookup(), goto_symext::ns, recursion_unwind_handlers, messaget::statistics(), and unwindset.
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 88 of file symex_bmc.cpp.
References symex_coveraget::covered(), goto_symex_statet::guard, goto_symex_statet::goto_statet::guard, exprt::is_false(), goto_symext::merge_goto(), symex_targett::sourcet::pc, PRECONDITION, record_coverage, goto_symex_statet::source, goto_symex_statet::goto_statet::source, and symex_coverage.
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 200 of file symex_bmc.cpp.
References body_warnings, messaget::eom(), goto_symext::log, and messaget::warning().
|
inline |
Definition at line 76 of file symex_bmc.h.
References symex_coveraget::generate_report(), and symex_coverage.
Referenced by bmct::execute().
|
protectedvirtual |
show progress
Reimplemented from goto_symext.
Definition at line 34 of file symex_bmc.cpp.
References source_locationt::as_string(), symex_coveraget::covered(), messaget::debug(), goto_symex_statet::depth, dstringt::empty(), goto_functionst::entry_point(), messaget::eom(), goto_symex_statet::guard, exprt::is_false(), irept::is_nil(), last_source_location, goto_symext::log, goto_symext::ns, symex_targett::sourcet::pc, record_coverage, simplify_expr(), goto_symex_statet::source, messaget::statistics(), symex_coverage, goto_symext::symex_step(), and symex_targett::sourcet::thread_nr.
|
protected |
Definition at line 119 of file symex_bmc.h.
Referenced by no_body().
source_locationt symex_bmct::last_source_location |
Definition at line 36 of file symex_bmc.h.
Referenced by bmct::execute(), bmct::setup(), and symex_step().
|
protected |
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Definition at line 89 of file symex_bmc.h.
Referenced by add_loop_unwind_handler(), and get_unwind().
bool symex_bmct::record_coverage |
Definition at line 83 of file symex_bmc.h.
Referenced by bmct::bmct(), merge_goto(), and symex_step().
|
protected |
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
Definition at line 93 of file symex_bmc.h.
Referenced by add_recursion_unwind_handler(), and get_unwind_recursion().
|
protected |
Definition at line 121 of file symex_bmc.h.
Referenced by merge_goto(), output_coverage_report(), and symex_step().
unwindsett symex_bmct::unwindset |
Definition at line 85 of file symex_bmc.h.
Referenced by get_unwind(), get_unwind_recursion(), and bmct::setup().