CBMC
symex_bmct Class Reference

#include <symex_bmc.h>

+ Inheritance diagram for symex_bmct:
+ Collaboration diagram for symex_bmct:

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. 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...
 
- Public Types inherited from goto_symext
typedef goto_symex_statet statet
 A type abbreviation for goto_symex_statet. More...
 
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. More...
 

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, 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. 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
 
- 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. More...
 
virtual ~goto_symext ()=default
 A virtual destructor allowing derived classes to be cleaned up correctly. More...
 
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. More...
 
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. More...
 
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. More...
 
virtual symbol_tablet symex_with_state (statet &state, const get_goto_functiont &get_goto_functions)
 Symbolically execute the entire program starting from entry point. More...
 
virtual bool check_break (const irep_idt &loop_id, unsigned unwind)
 Defines condition for interrupting symbolic execution for a specific loop. More...
 
unsigned get_total_vccs () const
 
unsigned get_remaining_vccs () const
 
void validate (const validation_modet vm) const
 

Public Attributes

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. More...
 
bool ignore_assertions = false
 If this flag is set to true then assertions will be temporarily ignored by the symbolic executions. 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 Member Functions

void symex_step (const get_goto_functiont &get_goto_function, statet &state) override
 show progress More...
 
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. More...
 
bool should_stop_unwind (const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
 Determine whether to unwind a loop. More...
 
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. More...
 
void symex_threaded_step (statet &state, const get_goto_functiont &get_goto_function)
 Invokes symex_step and verifies whether additional threads can be executed. More...
 
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. More...
 
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. More...
 
void print_symex_step (statet &state)
 Prints the route of symex as it walks through the code. More...
 
messaget::mstreamtprint_callstack_entry (const symex_targett::sourcet &target)
 
exprt clean_expr (exprt expr, statet &state, bool write)
 Clean up an expression. More...
 
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. More...
 
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. More...
 
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. More...
 
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). More...
 
virtual void symex_goto (statet &state)
 Symbolically execute a GOTO instruction. More...
 
void symex_unreachable_goto (statet &state)
 Symbolically execute a GOTO instruction in the context of unreachable code. More...
 
void symex_set_return_value (statet &state, const exprt &return_value)
 Symbolically execute a SET_RETURN_VALUE instruction. More...
 
virtual void symex_start_thread (statet &state)
 Symbolically execute a START_THREAD instruction. More...
 
virtual void symex_atomic_begin (statet &state)
 Symbolically execute an ATOMIC_BEGIN instruction. More...
 
virtual void symex_atomic_end (statet &state)
 Symbolically execute an ATOMIC_END instruction. More...
 
virtual void symex_decl (statet &state)
 Symbolically execute a DECL instruction. More...
 
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. More...
 
virtual void symex_dead (statet &state)
 Symbolically execute a DEAD instruction. More...
 
void symex_dead (statet &state, const symbol_exprt &symbol_expr)
 Kill a symbol, as if it had been the subject of a DEAD instruction. More...
 
virtual void symex_other (statet &state)
 Symbolically execute an OTHER instruction. More...
 
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. More...
 
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. More...
 
virtual void vcc (const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)
 Symbolically execute a verification condition (assertion). More...
 
virtual void symex_assume (statet &state, const exprt &cond)
 Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption. More...
 
void symex_assume_l2 (statet &, const exprt &cond)
 
void merge_gotos (statet &state)
 Merge all branches joining at the current program point. More...
 
void phi_function (const goto_statet &goto_state, statet &dest_state)
 Merge the SSA assignments from goto_state into dest_state. More...
 
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. More...
 
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. More...
 
virtual void symex_end_of_function (statet &)
 Symbolically execute a END_FUNCTION instruction. More...
 
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. More...
 
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. More...
 
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. More...
 
void symex_throw (statet &state)
 Symbolically execute a THROW instruction. More...
 
void symex_catch (statet &state)
 Symbolically execute a CATCH instruction. More...
 
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. More...
 
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) More...
 
void constant_propagate_empty_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Create an empty string constant. More...
 
bool constant_propagate_string_concat (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate string concatenation. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
bool constant_propagate_trim (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate trim operations. More...
 
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. More...
 
bool constant_propagate_replace (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant proagate character replacement. More...
 
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. More...
 
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. More...
 
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. More...
 
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)
 
void lift_lets (statet &, exprt &)
 Execute any let expressions in expr using symex_assignt::assign_symbol. More...
 
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). More...
 
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. More...
 
virtual void symex_cpp_delete (statet &state, const codet &code)
 Symbolically execute an OTHER instruction that does a CPP delete More...
 
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. More...
 
virtual void symex_printf (statet &state, const exprt &rhs)
 Symbolically execute an OTHER instruction that does a CPP printf More...
 
virtual void symex_input (statet &state, const codet &code)
 Symbolically execute an OTHER instruction that does a CPP input. More...
 
virtual void symex_output (statet &state, const codet &code)
 Symbolically execute an OTHER instruction that does a CPP output. More...
 
void rewrite_quantifiers (exprt &, statet &)
 

Protected Attributes

std::vector< loop_unwind_handlertloop_unwind_handlers
 Callbacks that may provide an unwind/do-not-unwind decision for a loop. More...
 
std::vector< recursion_unwind_handlertrecursion_unwind_handlers
 Callbacks that may provide an unwind/do-not-unwind decision for a recursive call. More...
 
symex_coveraget symex_coverage
 
- Protected Attributes inherited from goto_symext
const symex_configt symex_config
 The configuration to use for this symbolic execution. More...
 
const symbol_table_basetouter_symbol_table
 The symbol table associated with the goto-program being executed. 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...
 
guard_managertguard_manager
 Used to create guards. More...
 
symex_target_equationttarget
 The equation that this execution is building up. More...
 
unsigned atomic_section_counter
 A monotonically increasing index for each encountered ATOMIC_BEGIN instruction. More...
 
std::vector< symbol_exprtinstruction_local_symbols
 Variables that should be killed at the end of the current symex_step invocation. More...
 
messaget log
 The messaget to write log messages to. More...
 
path_storagetpath_storage
 Symbolic execution paths to be resumed later. More...
 
complexity_limitert complexity_module
 
shadow_memoryt shadow_memory
 Shadow memory instrumentation API. More...
 
unsigned _total_vccs
 
unsigned _remaining_vccs
 

Additional Inherited Members

- 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. More...
 
- 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 23 of file symex_bmc.h.

Member Typedef Documentation

◆ loop_unwind_handlert

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.

◆ recursion_unwind_handlert

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.

Constructor & Destructor Documentation

◆ symex_bmct()

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.

Member Function Documentation

◆ add_loop_unwind_handler()

void symex_bmct::add_loop_unwind_handler ( loop_unwind_handlert  handler)
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.

Parameters
handlernew callback

Definition at line 61 of file symex_bmc.h.

◆ add_recursion_unwind_handler()

void symex_bmct::add_recursion_unwind_handler ( recursion_unwind_handlert  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.

Parameters
handlernew callback

Definition at line 70 of file symex_bmc.h.

◆ get_unwind_recursion()

bool symex_bmct::get_unwind_recursion ( const irep_idt identifier,
unsigned  thread_nr,
unsigned  unwind 
)
overrideprotectedvirtual

Reimplemented from goto_symext.

Definition at line 164 of file symex_bmc.cpp.

◆ merge_goto()

void symex_bmct::merge_goto ( const symex_targett::sourcet source,
goto_statet &&  goto_state,
statet state 
)
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.

Parameters
sourcesource associated with the incoming goto_state
goto_stateA state to be merged into this location
stateSymbolic execution state to be updated

Reimplemented from goto_symext.

Definition at line 98 of file symex_bmc.cpp.

◆ output_coverage_report()

bool symex_bmct::output_coverage_report ( const goto_functionst goto_functions,
const std::string &  path 
) const
inline

Definition at line 75 of file symex_bmc.h.

◆ should_stop_unwind()

bool symex_bmct::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.

Reimplemented in symex_bmc_incremental_one_loopt.

Definition at line 118 of file symex_bmc.cpp.

◆ symex_step()

void symex_bmct::symex_step ( const get_goto_functiont get_goto_function,
statet state 
)
overrideprotectedvirtual

show progress

Reimplemented from goto_symext.

Definition at line 43 of file symex_bmc.cpp.

Member Data Documentation

◆ last_source_location

source_locationt symex_bmct::last_source_location

Definition at line 36 of file symex_bmc.h.

◆ loop_unwind_handlers

std::vector<loop_unwind_handlert> symex_bmct::loop_unwind_handlers
protected

Callbacks that may provide an unwind/do-not-unwind decision for a loop.

Definition at line 88 of file symex_bmc.h.

◆ record_coverage

const bool symex_bmct::record_coverage

Definition at line 82 of file symex_bmc.h.

◆ recursion_unwind_handlers

std::vector<recursion_unwind_handlert> symex_bmct::recursion_unwind_handlers
protected

Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.

Definition at line 92 of file symex_bmc.h.

◆ symex_coverage

symex_coveraget symex_bmct::symex_coverage
protected

Definition at line 112 of file symex_bmc.h.

◆ unwindset

unwindsett& symex_bmct::unwindset

Definition at line 84 of file symex_bmc.h.


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