cprover
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 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...
 
- Public Types inherited from goto_symext
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
 
- Public Member Functions inherited from goto_symext
 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

source_locationt last_source_location
 
const bool record_coverage
 
unwindsett unwindset
 
- Public Attributes inherited from goto_symext
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 Member Functions

void symex_step (const get_goto_functiont &get_goto_function, statet &state) override
 show progress More...
 
void merge_goto (const statet::goto_statet &goto_state, statet &state) override
 
bool should_stop_unwind (const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind) override
 
bool get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) override
 
void no_body (const irep_idt &identifier) override
 
- Protected Member Functions inherited from goto_symext
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...
 
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 &)
 
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 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 &)
 

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...
 
std::unordered_set< irep_idtbody_warnings
 
symex_coveraget symex_coverage
 
- Protected Attributes inherited from goto_symext
const symex_configt symex_config
 
const symbol_tabletouter_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_equationttarget
 
unsigned atomic_section_counter
 
messaget log
 
const irep_idt guard_identifier
 
symex_nondet_generatort build_symex_nondet
 
path_storagetpath_storage
 
unsigned _total_vccs
 
unsigned _remaining_vccs
 

Additional Inherited Members

- Protected Types inherited from goto_symext
typedef symex_targett::assignment_typet assignment_typet
 
- Static Protected Member Functions inherited from goto_symext
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...
 
- Static Protected Attributes inherited from goto_symext
static unsigned dynamic_counter =0
 

Detailed Description

Definition at line 25 of file symex_bmc.h.

Member Typedef Documentation

◆ loop_unwind_handlert

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.

◆ 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 56 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 
)

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 62 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 71 of file symex_bmc.h.

◆ get_unwind_recursion()

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

Reimplemented from goto_symext.

Definition at line 154 of file symex_bmc.cpp.

◆ merge_goto()

void symex_bmct::merge_goto ( const statet::goto_statet goto_state,
statet state 
)
overrideprotectedvirtual

Reimplemented from goto_symext.

Definition at line 89 of file symex_bmc.cpp.

◆ no_body()

void symex_bmct::no_body ( const irep_idt identifier)
overrideprotectedvirtual

Reimplemented from goto_symext.

Definition at line 201 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 76 of file symex_bmc.h.

◆ should_stop_unwind()

bool symex_bmct::should_stop_unwind ( const symex_targett::sourcet source,
const goto_symex_statet::call_stackt context,
unsigned  unwind 
)
overrideprotectedvirtual

Reimplemented from goto_symext.

Definition at line 108 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 34 of file symex_bmc.cpp.

Member Data Documentation

◆ body_warnings

std::unordered_set<irep_idt> symex_bmct::body_warnings
protected

Definition at line 113 of file symex_bmc.h.

◆ 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 89 of file symex_bmc.h.

◆ record_coverage

const bool symex_bmct::record_coverage

Definition at line 83 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 93 of file symex_bmc.h.

◆ symex_coverage

symex_coveraget symex_bmct::symex_coverage
protected

Definition at line 115 of file symex_bmc.h.

◆ unwindset

unwindsett symex_bmct::unwindset

Definition at line 85 of file symex_bmc.h.


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