cprover
bmct Class Reference

Bounded model checking or path exploration for goto-programs. More...

#include <bmc.h>

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

Public Member Functions

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

Static Public Member Functions

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)
 

Protected Member Functions

 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, const optionst::value_listt &criteria)
 Try to cover all goals. More...
 

Protected Attributes

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

virtual void perform_symbolic_execution (goto_symext::get_goto_functiont get_goto_function)
 Class-specific symbolic execution. More...
 

Private Attributes

std::function< bool(void)> driver_callback_after_symex
 Optional callback, to be run after symex but before handing the resulting equation to the solver. More...
 

Friends

class bmc_all_propertiest
 
class bmc_covert
 
template<template< class goalt > class covert>
class bmc_goal_covert
 
class fault_localizationt
 

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
}
 
- Public Attributes inherited from safety_checkert
goto_tracet error_trace
 

Detailed Description

Bounded model checking or path exploration for goto-programs.

Higher-level architectural information on symbolic execution is documented in the Symbolic execution module page.

Definition at line 41 of file bmc.h.

Constructor & Destructor Documentation

◆ bmct() [1/2]

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 
)
inline

Constructor for path exploration with freshly-initialized state.

This constructor should be used for symbolically executing a program from the entry point with fresh state. There are two main behaviours that can happen when constructing an instance of this class:

  • If the --paths flag in the options argument to this constructor is false (unset), an instance of this class will symbolically execute the entire program, performing path merging to build a formula corresponding to all executions of the program up to the unwinding limit. In this case, the path_storage member shall not be touched; this is enforced by the assertion in this class' implementation of bmct::perform_symbolic_execution().
  • If the --paths flag is true, this bmct object will explore a single path through the codebase without doing any path merging. If some paths were not taken, the state at those branch points will be appended to path_storage. After the single path that this bmct object executed has been model-checked, you can resume exploring further paths by popping an element from path_storage and using it to construct a path_explorert object.

Definition at line 66 of file bmc.h.

References goto_symext::constant_propagation, optionst::get_bool_option(), optionst::get_option(), options, symex_bmct::record_coverage, goto_symext::self_loops_to_assumptions, and symex.

◆ ~bmct()

virtual bmct::~bmct ( )
inlinevirtual

Definition at line 104 of file bmc.h.

◆ bmct() [2/2]

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 
)
inlineprotected

Constructor for path exploration from saved state.

This constructor exists as a delegate for the path_explorert class. It differs from bmct's public constructor in that it actually does something with the path_storaget argument, and also takes a symex_target_equationt. See the documentation for path_explorert for details.

Definition at line 144 of file bmc.h.

References goto_symext::constant_propagation, optionst::get_bool_option(), optionst::get_option(), INVARIANT, options, symex_bmct::record_coverage, and symex.

Member Function Documentation

◆ add_loop_unwind_handler()

void bmct::add_loop_unwind_handler ( symex_bmct::loop_unwind_handlert  handler)
inline

Definition at line 115 of file bmc.h.

References symex_bmct::add_loop_unwind_handler(), and symex.

Referenced by jbmc_parse_optionst::doit().

◆ add_unwind_recursion_handler()

void bmct::add_unwind_recursion_handler ( symex_bmct::recursion_unwind_handlert  handler)
inline

Definition at line 120 of file bmc.h.

References symex_bmct::add_recursion_unwind_handler(), and symex.

◆ all_properties()

safety_checkert::resultt bmct::all_properties ( const goto_functionst goto_functions,
prop_convt solver 
)
protectedvirtual

Definition at line 234 of file all_properties.cpp.

References messaget::get_message_handler(), messaget::set_message_handler(), and solver().

Referenced by decide().

◆ cover()

bool bmct::cover ( const goto_functionst goto_functions,
const optionst::value_listt criteria 
)
protected

Try to cover all goals.

Definition at line 429 of file bmc_cover.cpp.

References messaget::get_message_handler(), and messaget::set_message_handler().

Referenced by execute().

◆ decide()

safety_checkert::resultt bmct::decide ( const goto_functionst goto_functions,
prop_convt prop_conv 
)
protectedvirtual

◆ do_conversion()

◆ do_language_agnostic_bmc()

int bmct::do_language_agnostic_bmc ( const path_strategy_choosert path_strategy_chooser,
const optionst opts,
abstract_goto_modelt 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 
)
static

Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand).

Parameters
optscommand-line options affecting BMC
modelprovides goto function bodies and the symbol table, perhaps
uiuser-interface mode (plain text, XML output, JSON output, ...)
messageused for logging
driver_configure_bmcfunction provided by the driver program, which applies driver-specific configuration to a bmct before running.
callback_after_symexoptional callback to be run after symex. See class member bmct::driver_callback_after_symex for details.

Definition at line 561 of file bmc.cpp.

References CPROVER_EXIT_EXCEPTION, CPROVER_EXIT_INTERNAL_ERROR, CPROVER_EXIT_VERIFICATION_SAFE, CPROVER_EXIT_VERIFICATION_UNSAFE, messaget::eom(), path_storaget::patht::equation, safety_checkert::ERROR, messaget::error(), path_strategy_choosert::get(), optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_option(), abstract_goto_modelt::get_symbol_table(), INVARIANT, path_strategy_choosert::is_valid_strategy(), safety_checkert::PAUSED, cbmc_solverst::solvert::prop_conv(), run(), safety_checkert::SAFE, set_ui(), cbmc_solverst::set_ui(), path_storaget::patht::state, messaget::status(), to_string(), ui, safety_checkert::UNKNOWN, UNREACHABLE, and safety_checkert::UNSAFE.

Referenced by cbmc_parse_optionst::doit(), and jbmc_parse_optionst::doit().

◆ error_trace()

◆ execute()

◆ freeze_program_variables()

void bmct::freeze_program_variables ( )
protectedvirtual

Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added to the solver.

Freezing variables is necessary to make use of incremental solving with MiniSat SimpSolver. Potentially a useful hook for other applications using incremental solving.

Definition at line 42 of file bmc.cpp.

Referenced by do_conversion().

◆ get_memory_model()

void bmct::get_memory_model ( )
protected

Definition at line 287 of file bmc.cpp.

References messaget::eom(), messaget::error(), optionst::get_option(), memory_model, ns, and options.

Referenced by setup().

◆ operator()()

virtual resultt bmct::operator() ( const goto_functionst goto_functions)
inlinevirtual

Implements safety_checkert.

Definition at line 109 of file bmc.h.

References run().

◆ output_graphml()

void bmct::output_graphml ( resultt  result)
protected

◆ perform_symbolic_execution()

void bmct::perform_symbolic_execution ( goto_symext::get_goto_functiont  get_goto_function)
privatevirtual

Class-specific symbolic execution.

This private virtual should be overridden by derived classes to invoke the symbolic executor in a class-specific way. This implementation invokes goto_symext::operator() to perform full-program model-checking from the entry point of the program.

Reimplemented in path_explorert.

Definition at line 679 of file bmc.cpp.

References path_storaget::empty(), optionst::get_bool_option(), INVARIANT, options, path_storage, symex, goto_symext::symex_from_entry_point_of(), and symex_symbol_table.

Referenced by execute().

◆ report_failure()

◆ report_success()

◆ run() [1/2]

virtual resultt bmct::run ( const goto_functionst goto_functions)
inlinevirtual

Definition at line 96 of file bmc.h.

References outer_symbol_table.

Referenced by do_language_agnostic_bmc(), instrumentert::is_cfg_spurious(), and operator()().

◆ run() [2/2]

safety_checkert::resultt bmct::run ( abstract_goto_modelt goto_model)

Definition at line 483 of file bmc.cpp.

References execute(), and setup().

◆ run_decision_procedure()

◆ set_ui()

void bmct::set_ui ( ui_message_handlert::uit  _ui)
inline

Definition at line 106 of file bmc.h.

References ui.

Referenced by do_language_agnostic_bmc().

◆ setup()

◆ show()

void bmct::show ( )
protected

Definition at line 503 of file bmc.cpp.

References optionst::get_bool_option(), options, show_program(), and show_vcc().

◆ show_program()

void bmct::show_program ( )
protectedvirtual

Definition at line 203 of file bmc.cpp.

References equation, from_expr(), ns, symex_target_equationt::SSA_steps, and to_string().

Referenced by execute(), and show().

◆ show_vcc()

◆ show_vcc_json()

void bmct::show_vcc_json ( std::ostream &  out)
protectedvirtual

◆ show_vcc_plain()

void bmct::show_vcc_plain ( std::ostream &  out)
protectedvirtual

◆ slice()

◆ stop_on_fail()

◆ trace_options()

trace_optionst bmct::trace_options ( )
inlineprotected

Definition at line 206 of file bmc.h.

References options.

Referenced by error_trace(), bmc_covert::operator()(), and bmc_all_propertiest::report().

Friends And Related Function Documentation

◆ bmc_all_propertiest

friend class bmc_all_propertiest
friend

Definition at line 230 of file bmc.h.

◆ bmc_covert

friend class bmc_covert
friend

Definition at line 231 of file bmc.h.

◆ bmc_goal_covert

template<template< class goalt > class covert>
friend class bmc_goal_covert
friend

Definition at line 233 of file bmc.h.

◆ fault_localizationt

friend class fault_localizationt
friend

Definition at line 234 of file bmc.h.

Member Data Documentation

◆ driver_callback_after_symex

std::function<bool(void)> bmct::driver_callback_after_symex
private

Optional callback, to be run after symex but before handing the resulting equation to the solver.

If it returns true then we will skip the solver stage and return "safe" (no assertions violated / coverage goals reached), similar to the behaviour when 'show-vcc' or 'program-only' are specified.

Definition at line 250 of file bmc.h.

Referenced by execute().

◆ equation

◆ memory_model

std::unique_ptr<memory_model_baset> bmct::memory_model
protected

Definition at line 187 of file bmc.h.

Referenced by execute(), and get_memory_model().

◆ ns

◆ options

◆ outer_symbol_table

const symbol_tablet& bmct::outer_symbol_table
protected

symbol table for the goto-program that we will execute

Definition at line 179 of file bmc.h.

Referenced by run().

◆ path_storage

path_storaget& bmct::path_storage
protected

Definition at line 184 of file bmc.h.

Referenced by perform_symbolic_execution().

◆ prop_conv

◆ symex

◆ symex_symbol_table

symbol_tablet bmct::symex_symbol_table
protected

symbol table generated during symbolic execution

Definition at line 181 of file bmc.h.

Referenced by perform_symbolic_execution(), and path_explorert::perform_symbolic_execution().

◆ ui


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