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 ()=default |
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 *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... | |
unsigned | get_total_vccs () |
unsigned | get_remaining_vccs () |
void | validate (const namespacet &ns, const validation_modet vm) const |
Public Attributes | |
bool | should_pause_symex |
Have states been pushed onto the workqueue? More... | |
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... | |
std::size_t | path_segment_vccs |
Number of VCCs generated during the run of this goto_symext object. 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, const irep_idt &function_identifier, 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 &, bool write) |
void | dereference_rec (exprt &, statet &, guardt &, 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_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 | should_stop_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, 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 | 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 | 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) |
Store the what expression by recursively descending into the operands of lhs until the first operand op0 is nil: this nil operand is then replaced with what . More... | |
Protected Attributes | |
const symex_configt | symex_config |
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 |
const irep_idt | guard_identifier |
symex_nondet_generatort | build_symex_nondet |
path_storaget & | path_storage |
Statistics | |
The actual number of total and remaining VCCs should be assigned to the relevant members of goto_symex_statet. The members below are used to cache the values from goto_symex_statet after symex has ended, so that \ref bmct can read those values even after the state has been deallocated. | |
unsigned | _total_vccs |
unsigned | _remaining_vccs |
Static Protected Attributes | |
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 78 of file goto_symex.h.
|
protected |
Definition at line 348 of file goto_symex.h.
typedef std::function<const goto_functionst::goto_functiont &(const irep_idt &)> goto_symext::get_goto_functiont |
Definition at line 109 of file goto_symex.h.
typedef goto_symex_statet goto_symext::statet |
Definition at line 81 of file goto_symex.h.
|
inline |
Definition at line 83 of file goto_symex.h.
|
virtualdefault |
Store the what
expression by recursively descending into the operands of lhs
until the first operand op0
is nil: this nil operand is then replaced with what
.
lhs | Non-symbol pointed-to expression |
what | The expression to be added to the lhs |
Definition at line 97 of file symex_assign.cpp.
|
protected |
Evaluate an ID_address_of expression.
Definition at line 92 of file symex_dereference.cpp.
Definition at line 154 of file symex_clean_expr.cpp.
Definition at line 378 of file symex_dereference.cpp.
|
protected |
Definition at line 248 of file symex_dereference.cpp.
|
protected |
Definition at line 26 of file symex_dereference.cpp.
|
protectedvirtual |
Definition at line 18 of file goto_symex.cpp.
|
inline |
Definition at line 462 of file goto_symex.h.
|
inline |
Definition at line 453 of file goto_symex.h.
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 21 of file symex_function_call.cpp.
Definition at line 20 of file symex_other.cpp.
Definition at line 37 of file auto_objects.cpp.
|
protected |
Initialise the symbolic execution and the given state with pc
as entry point.
state | Symex state to initialise. |
get_goto_function | producer for GOTO functions |
function_identifier | The function in which the instructions are |
pc | first instruction to symex |
limit | final instruction, which itself will not be symexed. |
Definition at line 145 of file symex_main.cpp.
|
staticprotected |
Definition at line 66 of file symex_dereference.cpp.
|
protected |
preserves locality of local variables of a given function by applying L1 renaming to the local identifiers
Definition at line 385 of file symex_function_call.cpp.
Definition at line 546 of file symex_goto.cpp.
Definition at line 19 of file auto_objects.cpp.
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 321 of file symex_goto.cpp.
|
protected |
Definition at line 297 of file symex_goto.cpp.
|
protected |
Definition at line 343 of file symex_goto.cpp.
|
inlineprotectedvirtual |
Reimplemented in symex_bmct.
Definition at line 300 of file goto_symex.h.
|
protected |
Definition at line 29 of file symex_function_call.cpp.
|
protected |
Definition at line 514 of file symex_goto.cpp.
|
protected |
pop one call frame
Definition at line 334 of file symex_function_call.cpp.
|
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.
|
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 273 of file symex_main.cpp.
|
protected |
Definition at line 448 of file symex_function_call.cpp.
Definition at line 130 of file symex_main.cpp.
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 579 of file symex_goto.cpp.
|
protectedvirtual |
Definition at line 44 of file symex_builtin_functions.cpp.
|
protected |
Definition at line 24 of file symex_assign.cpp.
|
protected |
Definition at line 311 of file symex_assign.cpp.
|
protected |
Definition at line 462 of file symex_assign.cpp.
|
protected |
Definition at line 429 of file symex_assign.cpp.
|
protected |
Definition at line 131 of file symex_assign.cpp.
|
protected |
Definition at line 358 of file symex_assign.cpp.
|
protected |
Definition at line 213 of file symex_assign.cpp.
|
protected |
Definition at line 293 of file symex_assign.cpp.
Definition at line 101 of file symex_main.cpp.
|
protectedvirtual |
Definition at line 16 of file symex_atomic_section.cpp.
|
protectedvirtual |
Definition at line 36 of file symex_atomic_section.cpp.
|
protected |
Definition at line 14 of file symex_catch.cpp.
Definition at line 446 of file symex_builtin_functions.cpp.
|
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 384 of file symex_builtin_functions.cpp.
|
protectedvirtual |
Definition at line 20 of file symex_dead.cpp.
|
protectedvirtual |
Definition at line 22 of file symex_decl.cpp.
|
protectedvirtual |
Definition at line 35 of file symex_decl.cpp.
|
protectedvirtual |
do function call by inlining
Definition at line 372 of file symex_function_call.cpp.
|
protectedvirtual |
Definition at line 492 of file symex_builtin_functions.cpp.
|
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 295 of file symex_main.cpp.
|
protectedvirtual |
Definition at line 184 of file symex_function_call.cpp.
|
protectedvirtual |
do function call by inlining
Definition at line 227 of file symex_function_call.cpp.
|
protectedvirtual |
Definition at line 198 of file symex_function_call.cpp.
|
protectedvirtual |
Definition at line 224 of file symex_builtin_functions.cpp.
|
protectedvirtual |
Definition at line 25 of file symex_goto.cpp.
Definition at line 331 of file symex_builtin_functions.cpp.
|
protectedvirtual |
Definition at line 517 of file symex_builtin_functions.cpp.
|
protectedvirtual |
Definition at line 77 of file symex_other.cpp.
Definition at line 355 of file symex_builtin_functions.cpp.
Definition at line 306 of file symex_builtin_functions.cpp.
|
protectedvirtual |
Definition at line 17 of file symex_start_thread.cpp.
|
protectedvirtual |
|
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 194 of file symex_main.cpp.
|
protected |
Definition at line 14 of file symex_throw.cpp.
|
protectedvirtual |
Definition at line 456 of file symex_builtin_functions.cpp.
|
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 227 of file symex_main.cpp.
|
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 238 of file symex_main.cpp.
Definition at line 83 of file auto_objects.cpp.
|
inline |
Definition at line 471 of file goto_symex.h.
|
protectedvirtual |
Definition at line 73 of file symex_main.cpp.
|
friend |
Definition at line 221 of file goto_symex.h.
|
protected |
Definition at line 449 of file goto_symex.h.
|
protected |
Definition at line 449 of file goto_symex.h.
|
protected |
Definition at line 217 of file goto_symex.h.
|
protected |
Definition at line 422 of file goto_symex.h.
|
staticprotected |
Definition at line 423 of file goto_symex.h.
|
protected |
Definition at line 253 of file goto_symex.h.
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 197 of file goto_symex.h.
|
mutableprotected |
Definition at line 219 of file goto_symex.h.
|
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 215 of file goto_symex.h.
|
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 206 of file goto_symex.h.
std::size_t goto_symext::path_segment_vccs |
Number of VCCs generated during the run of this goto_symext object.
This member is always initialized to 0
upon construction of this object. It therefore differs from goto_symex_statet::total_vccs, which persists across the creation of several goto_symext objects. When CBMC is run in path-exploration mode, the meaning of this member is "the number of VCCs
generated between the last branch point and the current instruction," while goto_symex_statet::total_vccs records the total number of VCCs generated along the entire path from the beginning of the program.
Definition at line 439 of file goto_symex.h.
|
protected |
Definition at line 427 of file goto_symex.h.
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 162 of file goto_symex.h.
|
protected |
Definition at line 165 of file goto_symex.h.
|
protected |
Definition at line 216 of file goto_symex.h.