cprover
|
#include <symex_bmc.h>
Public Types | |
typedef std::function< tvt(const 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. | |
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. | |
![]() | |
typedef goto_symex_statet | statet |
A type abbreviation for goto_symex_statet. | |
typedef std::function< const goto_functionst::goto_functiont &(const irep_idt &)> | get_goto_functiont |
The type of delegate functions that retrieve a goto_functiont for a particular function identifier. | |
Public Attributes | |
source_locationt | last_source_location |
const bool | record_coverage |
const bool | havoc_bodyless_functions |
unwindsett & | unwindset |
![]() | |
bool | should_pause_symex |
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution run, it means that symbolic execution 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. | |
bool | ignore_assertions = false |
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions. | |
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. | |
std::size_t | path_segment_vccs |
Number of VCCs generated during the run of this goto_symext object. | |
Protected Member Functions | |
void | symex_step (const get_goto_functiont &get_goto_function, statet &state) override |
show progress | |
void | merge_goto (const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) override |
Merge a single branch, the symbolic state of which is held in goto_state , into the current overall symbolic state. | |
bool | should_stop_unwind (const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override |
Determine whether to unwind a loop. | |
bool | get_unwind_recursion (const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override |
void | no_body (const irep_idt &identifier) override |
Log a warning that a function has no body. | |
![]() | |
std::unique_ptr< statet > | initialize_entry_point_state (const get_goto_functiont &get_goto_function) |
Initialize the symbolic execution and the given state with the beginning of the entry point function. | |
void | symex_threaded_step (statet &state, const get_goto_functiont &get_goto_function) |
Invokes symex_step and verifies whether additional threads can be executed. | |
void | execute_next_instruction (const get_goto_functiont &get_goto_function, statet &state) |
Executes the instruction state.source.pc Case-switches over the type of the instruction being executed and calls another function appropriate to the instruction type, for example symex_function_call if the current instruction is a function call, symex_goto if the current instruction is a goto, etc. | |
void | kill_instruction_local_symbols (statet &state) |
Kills any variables in instruction_local_symbols (these are currently always let-bound variables defined in the course of executing the current instruction), then clears instruction_local_symbols. | |
void | print_symex_step (statet &state) |
Prints the route of symex as it walks through the code. | |
messaget::mstreamt & | print_callstack_entry (const symex_targett::sourcet &target) |
exprt | clean_expr (exprt expr, statet &state, bool write) |
Clean up an expression. | |
void | trigger_auto_object (const exprt &, statet &) |
void | initialize_auto_object (const exprt &, statet &) |
void | process_array_expr (statet &, exprt &) |
Given an expression, find the root object and the offset into it. | |
exprt | make_auto_object (const typet &, statet &) |
virtual void | dereference (exprt &, statet &, bool write) |
Replace all dereference operations within expr with explicit references to the objects they may refer to. | |
symbol_exprt | cache_dereference (exprt &dereference_result, statet &state) |
void | dereference_rec (exprt &expr, statet &state, bool write, bool is_in_quantifier) |
If expr is a dereference_exprt, replace it with explicit references to the objects it may point to. | |
exprt | address_arithmetic (const exprt &, statet &, bool keep_array) |
Transforms an lvalue expression by replacing any dereference operations it contains with explicit references to the objects they may point to (using goto_symext::dereference_rec), and translates byte_extract, member and index operations into integer offsets from a root symbol (if any). | |
virtual void | symex_goto (statet &state) |
Symbolically execute a GOTO instruction. | |
void | symex_unreachable_goto (statet &state) |
Symbolically execute a GOTO instruction in the context of unreachable code. | |
void | symex_set_return_value (statet &state, const exprt &return_value) |
Symbolically execute a SET_RETURN_VALUE instruction. | |
virtual void | symex_start_thread (statet &state) |
Symbolically execute a START_THREAD instruction. | |
virtual void | symex_atomic_begin (statet &state) |
Symbolically execute an ATOMIC_BEGIN instruction. | |
virtual void | symex_atomic_end (statet &state) |
Symbolically execute an ATOMIC_END instruction. | |
virtual void | symex_decl (statet &state) |
Symbolically execute a DECL instruction. | |
virtual void | symex_decl (statet &state, const symbol_exprt &expr) |
Symbolically execute a DECL instruction for the given symbol or simulate such an execution for a synthetic symbol. | |
virtual void | symex_dead (statet &state) |
Symbolically execute a DEAD instruction. | |
void | symex_dead (statet &state, const symbol_exprt &symbol_expr) |
Kill a symbol, as if it had been the subject of a DEAD instruction. | |
virtual void | symex_other (statet &state) |
Symbolically execute an OTHER instruction. | |
void | symex_assert (const goto_programt::instructiont &, statet &) |
void | apply_goto_condition (goto_symex_statet ¤t_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns) |
Propagate constants and points-to information implied by a GOTO condition. | |
void | try_filter_value_sets (goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns) |
Try to filter value sets based on whether possible values of a pointer-typed symbol make the condition true or false. | |
virtual void | vcc (const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state) |
Symbolically execute a verification condition (assertion). | |
virtual void | symex_assume (statet &state, const exprt &cond) |
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption. | |
void | symex_assume_l2 (statet &, const exprt &cond) |
void | merge_gotos (statet &state) |
Merge all branches joining at the current program point. | |
void | phi_function (const goto_statet &goto_state, statet &dest_state) |
Merge the SSA assignments from goto_state into dest_state. | |
virtual void | loop_bound_exceeded (statet &state, const exprt &guard) |
virtual void | symex_function_call (const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction) |
Symbolically execute a FUNCTION_CALL instruction. | |
virtual void | locality (const irep_idt &function_identifier, goto_symext::statet &state, const goto_functionst::goto_functiont &goto_function) |
Preserves locality of parameters of a given function by applying L1 renaming to them. | |
virtual void | symex_end_of_function (statet &) |
Symbolically execute a END_FUNCTION instruction. | |
virtual void | symex_function_call_symbol (const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments) |
Symbolic execution of a call to a function call. | |
virtual void | symex_function_call_post_clean (const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments) |
Symbolic execution of a function call by inlining. | |
void | parameter_assignments (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments) |
Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are deduced from the type of goto_function . | |
void | symex_throw (statet &state) |
Symbolically execute a THROW instruction. | |
void | symex_catch (statet &state) |
Symbolically execute a CATCH instruction. | |
virtual void | do_simplify (exprt &expr) |
void | symex_assign (statet &state, const exprt &lhs, const exprt &rhs) |
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment. | |
bool | constant_propagate_assignment_with_side_effects (statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs) |
Attempt to constant propagate side effects of the assignment (if any) | |
void | constant_propagate_empty_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Create an empty string constant. | |
bool | constant_propagate_string_concat (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate string concatenation. | |
bool | constant_propagate_string_substring (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate getting a substring of a string. | |
bool | constant_propagate_integer_to_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate converting an integer to a string. | |
bool | constant_propagate_delete_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate deleting a character from a string. | |
bool | constant_propagate_delete (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate deleting a substring from a string. | |
bool | constant_propagate_set_length (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate setting the length of a string. | |
bool | constant_propagate_set_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate setting the char at the given index. | |
bool | constant_propagate_trim (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant propagate trim operations. | |
bool | constant_propagate_case_change (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper) |
Attempt to constant propagate case changes, both upper and lower. | |
bool | constant_propagate_replace (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
Attempt to constant proagate character replacement. | |
void | assign_string_constant (statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array) |
Assign constant string length and string data given by a char array to given ssa variables. | |
const symbolt & | get_new_string_data_symbol (statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array) |
Installs a new symbol in the symbol table to represent the given character array, and assigns the character array to the symbol. | |
void | associate_array_to_pointer (statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data) |
Generate array to pointer association primitive. | |
optionalt< std::reference_wrapper< const array_exprt > > | try_evaluate_constant_string (const statet &state, const exprt &content) |
void | havoc_rec (statet &state, const guardt &guard, const exprt &dest) |
void | lift_lets (statet &, exprt &) |
Execute any let expressions in expr using symex_assignt::assign_symbol. | |
void | lift_let (statet &state, const let_exprt &let_expr) |
Execute a single let expression, which should not have any nested let expressions (use lift_lets instead if there might be). | |
virtual void | symex_va_start (statet &, const exprt &lhs, const side_effect_exprt &) |
virtual void | symex_allocate (statet &state, const exprt &lhs, const side_effect_exprt &code) |
Symbolically execute an assignment instruction that has an allocate on the right hand side. | |
virtual void | symex_cpp_delete (statet &state, const codet &code) |
Symbolically execute an OTHER instruction that does a CPP delete | |
virtual void | symex_cpp_new (statet &state, const exprt &lhs, const side_effect_exprt &code) |
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes. | |
virtual void | symex_printf (statet &state, const exprt &rhs) |
Symbolically execute an OTHER instruction that does a CPP printf | |
virtual void | symex_input (statet &state, const codet &code) |
Symbolically execute an OTHER instruction that does a CPP input. | |
virtual void | symex_output (statet &state, const codet &code) |
Symbolically execute an OTHER instruction that does a CPP output. | |
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. | |
std::vector< recursion_unwind_handlert > | recursion_unwind_handlers |
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call. | |
std::unordered_set< irep_idt > | body_warnings |
symex_coveraget | symex_coverage |
![]() | |
const symex_configt | symex_config |
The configuration to use for this symbolic execution. | |
const symbol_table_baset & | outer_symbol_table |
The symbol table associated with the goto-program being executed. | |
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. | |
guard_managert & | guard_manager |
Used to create guards. | |
symex_target_equationt & | target |
The equation that this execution is building up. | |
unsigned | atomic_section_counter |
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction. | |
std::vector< symbol_exprt > | instruction_local_symbols |
Variables that should be killed at the end of the current symex_step invocation. | |
messaget | log |
The messaget to write log messages to. | |
path_storaget & | path_storage |
Symbolic execution paths to be resumed later. | |
complexity_limitert | complexity_module |
shadow_memoryt | shadow_memory |
Shadow memory instrumentation API. | |
unsigned | _total_vccs |
unsigned | _remaining_vccs |
Additional Inherited Members | |
![]() | |
static get_goto_functiont | get_goto_function (abstract_goto_modelt &goto_model) |
Return a function to get/load a goto function from the given goto model Create a default delegate to retrieve function bodies from a goto_functionst. | |
![]() | |
typedef symex_targett::assignment_typet | assignment_typet |
![]() | |
static optionalt< std::reference_wrapper< const constant_exprt > > | try_evaluate_constant (const statet &state, const exprt &expr) |
Definition at line 23 of file symex_bmc.h.
typedef std::function< tvt(const 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 46 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 55 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, | ||
guard_managert & | guard_manager, | ||
unwindsett & | unwindset | ||
) |
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 61 of file symex_bmc.h.
|
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 70 of file symex_bmc.h.
|
overrideprotectedvirtual |
Reimplemented from goto_symext.
Definition at line 166 of file symex_bmc.cpp.
|
overrideprotectedvirtual |
Merge a single branch, the symbolic state of which is held in goto_state
, into the current overall symbolic state.
goto_state
is no longer expected to be valid afterwards.
source | source associated with the incoming goto_state |
goto_state | A state to be merged into this location |
state | Symbolic execution state to be updated |
Reimplemented from goto_symext.
Definition at line 100 of file symex_bmc.cpp.
Log a warning that a function has no body.
identifier | The name of the function with no body |
Reimplemented from goto_symext.
Definition at line 213 of file symex_bmc.cpp.
|
inline |
Definition at line 75 of file symex_bmc.h.
|
overrideprotectedvirtual |
Determine whether to unwind a loop.
source | |
context | |
unwind |
Reimplemented from goto_symext.
Definition at line 120 of file symex_bmc.cpp.
|
overrideprotectedvirtual |
|
protected |
Definition at line 115 of file symex_bmc.h.
Definition at line 83 of file symex_bmc.h.
source_locationt symex_bmct::last_source_location |
Definition at line 36 of file symex_bmc.h.
|
protected |
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Definition at line 89 of file symex_bmc.h.
Definition at line 82 of file symex_bmc.h.
|
protected |
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
Definition at line 93 of file symex_bmc.h.
|
protected |
Definition at line 117 of file symex_bmc.h.
unwindsett& symex_bmct::unwindset |
Definition at line 85 of file symex_bmc.h.