cprover
path_explorert Class Reference

Symbolic execution from a saved branch point. More...

#include <bmc.h>

+ Inheritance diagram for path_explorert:
+ Collaboration diagram for path_explorert:

Public Member Functions

 path_explorert (const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, path_storaget &path_storage, std::function< bool(void)> callback_after_symex)
 
- Public Member Functions inherited from bmct
 bmct (const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, prop_convt &_prop_conv, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex)
 Constructor for path exploration with freshly-initialized state. More...
 
virtual resultt run (const goto_functionst &goto_functions)
 
resultt run (abstract_goto_modelt &)
 
void setup ()
 
safety_checkert::resultt execute (abstract_goto_modelt &)
 
virtual ~bmct ()
 
virtual resultt operator() (const goto_functionst &goto_functions)
 
void add_loop_unwind_handler (symex_bmct::loop_unwind_handlert handler)
 
void add_unwind_recursion_handler (symex_bmct::recursion_unwind_handlert handler)
 
- Public Member Functions inherited from safety_checkert
 safety_checkert (const namespacet &_ns)
 
 safety_checkert (const namespacet &_ns, message_handlert &_message_handler)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Protected Attributes

const goto_symex_statetsaved_state
 
- Protected Attributes inherited from bmct
const optionstoptions
 
const symbol_tabletouter_symbol_table
 symbol table for the goto-program that we will execute More...
 
symbol_tablet symex_symbol_table
 symbol table generated during symbolic execution More...
 
namespacet ns
 
symex_target_equationt equation
 
path_storagetpath_storage
 
symex_bmct symex
 
prop_convtprop_conv
 
std::unique_ptr< memory_model_basetmemory_model
 
ui_message_handlertui_message_handler
 
- Protected Attributes inherited from safety_checkert
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Private Member Functions

void perform_symbolic_execution (goto_symext::get_goto_functiont get_goto_function) override
 Resume symbolic execution from saved branch point. More...
 

Additional Inherited Members

- Public Types inherited from safety_checkert
enum  resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR, resultt::PAUSED }
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from bmct
static int do_language_agnostic_bmc (const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
 Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand). More...
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Public Attributes inherited from safety_checkert
goto_tracet error_trace
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 
- Protected Member Functions inherited from bmct
 bmct (const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex)
 Constructor for path exploration from saved state. More...
 
virtual decision_proceduret::resultt run_decision_procedure (prop_convt &prop_conv)
 
virtual resultt decide (const goto_functionst &, prop_convt &)
 
void do_conversion ()
 
virtual void freeze_program_variables ()
 Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added to the solver. More...
 
trace_optionst trace_options ()
 
virtual resultt all_properties (const goto_functionst &goto_functions, prop_convt &solver)
 
virtual resultt stop_on_fail (prop_convt &solver)
 
virtual void report_success ()
 
virtual void report_failure ()
 
virtual void error_trace ()
 
void output_graphml (resultt result)
 outputs witnesses in graphml format More...
 
void get_memory_model ()
 
void slice ()
 
void show ()
 
bool cover (const goto_functionst &goto_functions)
 Try to cover all goals. More...
 
- Static Protected Member Functions inherited from bmct
static void report_success (messaget &, ui_message_handlert &)
 
static void report_failure (messaget &, ui_message_handlert &)
 

Detailed Description

Symbolic execution from a saved branch point.

Instances of this class execute a single program path from a saved branch point. The saved branch point is supplied to the constructor as a pair of goto_target_equationt (which holds the SSA steps executed so far), and a goto_symex_statet Note that the bmct base class can also execute a single path (it will do so if the --paths flag is set in its options member), but will always begin symbolic execution from the beginning of the program with fresh state.

Definition at line 248 of file bmc.h.

Constructor & Destructor Documentation

◆ path_explorert()

path_explorert::path_explorert ( const optionst _options,
const symbol_tablet outer_symbol_table,
ui_message_handlert _message_handler,
prop_convt _prop_conv,
symex_target_equationt saved_equation,
const goto_symex_statet saved_state,
path_storaget path_storage,
std::function< bool(void)>  callback_after_symex 
)
inline

Definition at line 251 of file bmc.h.

Member Function Documentation

◆ perform_symbolic_execution()

void path_explorert::perform_symbolic_execution ( goto_symext::get_goto_functiont  get_goto_function)
overrideprivatevirtual

Resume symbolic execution from saved branch point.

This overrides the base implementation to call the symbolic executor with the saved symex_target_equationt, symbol_tablet, and goto_symex_statet provided as arguments to the constructor of this class.

Reimplemented from bmct.

Definition at line 654 of file bmc.cpp.

Member Data Documentation

◆ saved_state

const goto_symex_statet& path_explorert::saved_state
protected

Definition at line 273 of file bmc.h.


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