cprover
path_explorert Class Reference

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

#include <bmc.h>

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

Public Member Functions

 path_explorert (const optionst &_options, const symbol_tablet &outer_symbol_table, 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, 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 ()
 
void set_ui (ui_message_handlert::uit _ui)
 
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 mstream using output_generator if the configured verbosity is at least as high as that of mstream. 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_handlert::uit ui
 
- 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,
  resultt::UNKNOWN
}
 
- 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, const ui_message_handlert::uit &ui, messaget &message, 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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Public Attributes inherited from safety_checkert
goto_tracet error_trace
 
- Protected Member Functions inherited from bmct
 bmct (const optionst &_options, const symbol_tablet &outer_symbol_table, 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...
 
virtual void show_vcc ()
 
virtual void show_vcc_plain (std::ostream &out)
 
virtual void show_vcc_json (std::ostream &out)
 
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 show_program ()
 
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...
 

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 261 of file bmc.h.

Constructor & Destructor Documentation

◆ path_explorert()

path_explorert::path_explorert ( const optionst _options,
const symbol_tablet outer_symbol_table,
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 264 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 705 of file bmc.cpp.

References bmct::equation, goto_symext::resume_symex_from_saved_state(), saved_state, bmct::symex, and bmct::symex_symbol_table.

Member Data Documentation

◆ saved_state

const goto_symex_statet& path_explorert::saved_state
protected

Definition at line 286 of file bmc.h.

Referenced by perform_symbolic_execution().


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