cprover
Loading...
Searching...
No Matches
symex_bmc_incremental_one_loopt Class Reference

#include <symex_bmc_incremental_one_loop.h>

+ Inheritance diagram for symex_bmc_incremental_one_loopt:
+ Collaboration diagram for symex_bmc_incremental_one_loopt:

Public Member Functions

 symex_bmc_incremental_one_loopt (message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &, unwindsett &, ui_message_handlert::uit output_ui)
 
bool from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
 Return true if symex can be resumed.
 
bool resume (const get_goto_functiont &get_goto_function)
 Return true if symex can be resumed.
 
- Public Member Functions inherited from 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)
 
void add_loop_unwind_handler (loop_unwind_handlert handler)
 Add a callback function that will be called to determine whether to unwind loops.
 
void add_recursion_unwind_handler (recursion_unwind_handlert handler)
 Add a callback function that will be called to determine whether to unwind recursion.
 
bool output_coverage_report (const goto_functionst &goto_functions, const std::string &path) const
 
- Public Member Functions inherited from goto_symext
 goto_symext (message_handlert &mh, const symbol_table_baset &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
 Construct a goto_symext to execute a particular program.
 
virtual ~goto_symext ()=default
 A virtual destructor allowing derived classes to be cleaned up correctly.
 
virtual symbol_tablet symex_from_entry_point_of (const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)
 Symbolically execute the entire program starting from entry point.
 
virtual void initialize_path_storage_from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)
 Puts the initial state of the entry point function into the path storage.
 
virtual symbol_tablet resume_symex_from_saved_state (const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)
 Performs symbolic execution using a state and equation that have already been used to symbolically execute part of the program.
 
virtual symbol_tablet symex_with_state (statet &state, const get_goto_functiont &get_goto_functions)
 Symbolically execute the entire program starting from entry point.
 
unsigned get_total_vccs () const
 
unsigned get_remaining_vccs () const
 
void validate (const validation_modet vm) const
 

Protected Member Functions

bool check_break (const irep_idt &loop_id, unsigned unwind) override
 Defines condition for interrupting symbolic execution for incremental BMC.
 
bool should_stop_unwind (const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
 Determine whether to unwind a loop.
 
void log_unwinding (unsigned unwind)
 
- Protected Member Functions inherited from symex_bmct
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
 
- Protected Member Functions inherited from goto_symext
std::unique_ptr< statetinitialize_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::mstreamtprint_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. For example, the expression *p1 + *p2 might be rewritten to obj1 + (p2 == &obj2 ? obj2 : obj3) in the case where p1 is known to point to obj1 and p2 points to either obj2 or obj3. The expression, and any object references introduced, are renamed to L1 in the process (so in fact we would get obj1!0@3 + (p2!0@1 == .... rather than the exact example given above).
 
symbol_exprt cache_dereference (exprt &dereference_result, statet &state)
 
void dereference_rec (exprt &expr, statet &state, bool write, bool is_in_quantifier)
 
exprt address_arithmetic (const exprt &, statet &, bool keep_array)
 
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 &current_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 symboltget_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.
 
std::optional< 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)
 

Protected Attributes

const irep_idt incr_loop_id
 
const unsigned incr_max_unwind
 
const unsigned incr_min_unwind
 
std::unique_ptr< goto_symext::statetstate
 
ui_message_handlert::uit output_ui
 
- Protected Attributes inherited from symex_bmct
std::vector< loop_unwind_handlertloop_unwind_handlers
 Callbacks that may provide an unwind/do-not-unwind decision for a loop.
 
std::vector< recursion_unwind_handlertrecursion_unwind_handlers
 Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
 
symex_coveraget symex_coverage
 
- Protected Attributes inherited from goto_symext
const symex_configt symex_config
 The configuration to use for this symbolic execution.
 
const symbol_table_basetouter_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_managertguard_manager
 Used to create guards.
 
symex_target_equationttarget
 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_exprtinstruction_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.
 
std::size_t path_segment_vccs
 Execute any let expressions in expr using symex_assignt::assign_symbol.
 
complexity_limitert complexity_module
 
shadow_memoryt shadow_memory
 Shadow memory instrumentation API.
 
unsigned _total_vccs
 
unsigned _remaining_vccs
 

Additional Inherited Members

- Public Types inherited from symex_bmct
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.
 
- Public Types inherited from goto_symext
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.
 
- Static Public Member Functions inherited from goto_symext
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.
 
- Public Attributes inherited from symex_bmct
source_locationt last_source_location
 
const bool record_coverage
 
unwindsettunwindset
 
- Public Attributes inherited from goto_symext
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.
 
- Protected Types inherited from goto_symext
typedef symex_targett::assignment_typet assignment_typet
 
- Static Protected Member Functions inherited from goto_symext
static std::optional< std::reference_wrapper< const constant_exprt > > try_evaluate_constant (const statet &state, const exprt &expr)
 

Detailed Description

Definition at line 15 of file symex_bmc_incremental_one_loop.h.

Constructor & Destructor Documentation

◆ symex_bmc_incremental_one_loopt()

symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt ( message_handlert & message_handler,
const symbol_tablet & outer_symbol_table,
symex_target_equationt & target,
const optionst & options,
path_storaget & path_storage,
guard_managert & guard_manager,
unwindsett & unwindset,
ui_message_handlert::uit output_ui )

Definition at line 17 of file symex_bmc_incremental_one_loop.cpp.

Member Function Documentation

◆ check_break()

bool symex_bmc_incremental_one_loopt::check_break ( const irep_idt & loop_id,
unsigned unwind )
overrideprotectedvirtual

Defines condition for interrupting symbolic execution for incremental BMC.

Returns
True if the back edge encountered during symbolic execution corresponds to the given loop (incr_loop_id)

Reimplemented from goto_symext.

Definition at line 114 of file symex_bmc_incremental_one_loop.cpp.

◆ from_entry_point_of()

bool symex_bmc_incremental_one_loopt::from_entry_point_of ( const get_goto_functiont & get_goto_function,
symbol_tablet & new_symbol_table )

Return true if symex can be resumed.

Definition at line 125 of file symex_bmc_incremental_one_loop.cpp.

◆ log_unwinding()

void symex_bmc_incremental_one_loopt::log_unwinding ( unsigned unwind)
protected

Definition at line 145 of file symex_bmc_incremental_one_loop.cpp.

◆ resume()

bool symex_bmc_incremental_one_loopt::resume ( const get_goto_functiont & get_goto_function)

Return true if symex can be resumed.

Definition at line 136 of file symex_bmc_incremental_one_loop.cpp.

◆ should_stop_unwind()

bool symex_bmc_incremental_one_loopt::should_stop_unwind ( const symex_targett::sourcet & source,
const call_stackt & context,
unsigned unwind )
overrideprotectedvirtual

Determine whether to unwind a loop.

Parameters
source
context
unwind
Returns
true indicates abort, with false we continue

Reimplemented from goto_symext.

Definition at line 52 of file symex_bmc_incremental_one_loop.cpp.

Member Data Documentation

◆ incr_loop_id

const irep_idt symex_bmc_incremental_one_loopt::incr_loop_id
protected

Definition at line 37 of file symex_bmc_incremental_one_loop.h.

◆ incr_max_unwind

const unsigned symex_bmc_incremental_one_loopt::incr_max_unwind
protected

Definition at line 38 of file symex_bmc_incremental_one_loop.h.

◆ incr_min_unwind

const unsigned symex_bmc_incremental_one_loopt::incr_min_unwind
protected

Definition at line 39 of file symex_bmc_incremental_one_loop.h.

◆ output_ui

ui_message_handlert::uit symex_bmc_incremental_one_loopt::output_ui
protected

Definition at line 53 of file symex_bmc_incremental_one_loop.h.

◆ state

std::unique_ptr<goto_symext::statet> symex_bmc_incremental_one_loopt::state
protected

Definition at line 41 of file symex_bmc_incremental_one_loop.h.


The documentation for this class was generated from the following files: