cprover
symex_bmct Class Reference

#include <symex_bmc.h>

Inheritance diagram for symex_bmct:
[legend]
Collaboration diagram for symex_bmct:
[legend]

Public Types

typedef std::function< tvt(const irep_idt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert
 Loop unwind handlers take the function ID and 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 ()
 
virtual void symex_from_entry_point_of (const goto_functionst &goto_functions, symbol_tablet &new_symbol_table)
 symex entire program starting from entry point More...
 
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 *const 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...
 
virtual void symex_instruction_range (statet &, const goto_functionst &, goto_programt::const_targett first, goto_programt::const_targett limit)
 Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached. More...
 
virtual void symex_instruction_range (statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett first, goto_programt::const_targett limit)
 Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached. More...
 
virtual void symex_step_goto (statet &, bool taken)
 

Public Attributes

source_locationt last_source_location
 
bool record_coverage
 
unwindsett unwindset
 
- Public Attributes inherited from goto_symext
bool should_pause_symex
 Have states been pushed onto the workqueue? More...
 
unsigned total_vccs
 
unsigned remaining_vccs
 
bool constant_propagation
 
bool self_loops_to_assumptions
 
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...
 

Protected Member Functions

virtual void symex_step (const get_goto_functiont &get_goto_function, statet &state)
 show progress More...
 
virtual void merge_goto (const statet::goto_statet &goto_state, statet &state)
 
virtual bool get_unwind (const symex_targett::sourcet &source, unsigned unwind)
 
virtual bool get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
 
virtual void no_body (const irep_idt &identifier)
 
- Protected Member Functions inherited from goto_symext
void initialize_entry_point (statet &state, const get_goto_functiont &get_goto_function, 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 &, const bool write)
 
void dereference_rec (exprt &, statet &, guardt &, const 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_transition (statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
 
virtual void symex_transition (statet &state)
 
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 add_end_of_function (exprt &code, const irep_idt &identifier)
 
nondet_symbol_exprt build_symex_nondet (typet &type)
 
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 &lhs, const exprt &rhs)
 
virtual void symex_input (statet &, const codet &)
 
virtual void symex_output (statet &, const codet &)
 
void read (exprt &)
 
void replace_nondet (exprt &)
 
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 optionstoptions
 
const unsigned max_depth
 
const bool doing_path_exploration
 
const bool allow_pointer_unsoundness
 
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
 
irep_idt guard_identifier
 
path_storagetpath_storage
 

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)
 
- Static Protected Attributes inherited from goto_symext
static unsigned nondet_count =0
 
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 irep_idt &, unsigned, unsigned, unsigned &)> symex_bmct::loop_unwind_handlert

Loop unwind handlers take the function ID and 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 
)

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.

References loop_unwind_handlers.

Referenced by bmct::add_loop_unwind_handler().

◆ 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.

References recursion_unwind_handlers.

Referenced by bmct::add_unwind_recursion_handler().

◆ get_unwind()

◆ get_unwind_recursion()

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

◆ merge_goto()

◆ no_body()

void symex_bmct::no_body ( const irep_idt identifier)
protectedvirtual

Reimplemented from goto_symext.

Definition at line 203 of file symex_bmc.cpp.

References body_warnings, messaget::eom(), goto_symext::log, and messaget::warning().

◆ 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.

References symex_coveraget::generate_report(), and symex_coverage.

Referenced by bmct::execute().

◆ symex_step()

Member Data Documentation

◆ body_warnings

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

Definition at line 117 of file symex_bmc.h.

Referenced by no_body().

◆ last_source_location

source_locationt symex_bmct::last_source_location

Definition at line 36 of file symex_bmc.h.

Referenced by bmct::execute(), bmct::setup(), and symex_step().

◆ 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.

Referenced by add_loop_unwind_handler(), and get_unwind().

◆ record_coverage

bool symex_bmct::record_coverage

Definition at line 82 of file symex_bmc.h.

Referenced by bmct::bmct(), merge_goto(), and symex_step().

◆ 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.

Referenced by add_recursion_unwind_handler(), and get_unwind_recursion().

◆ symex_coverage

symex_coveraget symex_bmct::symex_coverage
protected

Definition at line 119 of file symex_bmc.h.

Referenced by merge_goto(), output_coverage_report(), and symex_step().

◆ unwindset

unwindsett symex_bmct::unwindset

Definition at line 84 of file symex_bmc.h.

Referenced by get_unwind(), get_unwind_recursion(), and bmct::setup().


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