cprover
bmct Class Reference

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

#include <bmc.h>

+ Inheritance diagram for bmct:
+ Collaboration diagram for bmct:

Public Member Functions

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

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

Protected Member Functions

 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

static void report_success (messaget &, ui_message_handlert &)
 
static void report_failure (messaget &, ui_message_handlert &)
 

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

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

◆ ~bmct()

virtual bmct::~bmct ( )
inlinevirtual

Definition at line 99 of file bmc.h.

◆ bmct() [2/2]

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

Member Function Documentation

◆ add_loop_unwind_handler()

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

Definition at line 108 of file bmc.h.

◆ add_unwind_recursion_handler()

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

Definition at line 113 of file bmc.h.

◆ all_properties()

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

Definition at line 294 of file all_properties.cpp.

◆ cover()

bool bmct::cover ( const goto_functionst goto_functions)
protected

Try to cover all goals.

Definition at line 425 of file bmc_cover.cpp.

◆ decide()

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

Definition at line 430 of file bmc.cpp.

◆ do_conversion()

void bmct::do_conversion ( )
protected

Definition at line 117 of file bmc.cpp.

◆ do_language_agnostic_bmc()

int bmct::do_language_agnostic_bmc ( const path_strategy_choosert path_strategy_chooser,
const optionst opts,
abstract_goto_modelt model,
ui_message_handlert ui,
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
path_strategy_choosercontrols whether symex generates a single large equation for the whole program or an equation per path
optscommand-line options affecting BMC
modelprovides goto function bodies and the symbol table, perhaps
uiuser-interface mode (plain text, XML output, JSON output, ...)
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 501 of file bmc.cpp.

◆ error_trace()

void bmct::error_trace ( )
protectedvirtual

Definition at line 50 of file bmc.cpp.

◆ execute()

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

Definition at line 253 of file bmc.cpp.

◆ 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 45 of file bmc.cpp.

◆ get_memory_model()

void bmct::get_memory_model ( )
protected

Definition at line 218 of file bmc.cpp.

◆ operator()()

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

Implements safety_checkert.

Definition at line 102 of file bmc.h.

◆ output_graphml()

void bmct::output_graphml ( resultt  result)
protected

outputs witnesses in graphml format

Definition at line 94 of file bmc.cpp.

◆ 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 638 of file bmc.cpp.

◆ report_failure() [1/2]

void bmct::report_failure ( )
protectedvirtual

Definition at line 186 of file bmc.cpp.

◆ report_failure() [2/2]

void bmct::report_failure ( messaget log,
ui_message_handlert handler 
)
staticprotected

Definition at line 191 of file bmc.cpp.

◆ report_success() [1/2]

void bmct::report_success ( )
protectedvirtual

Definition at line 154 of file bmc.cpp.

◆ report_success() [2/2]

void bmct::report_success ( messaget log,
ui_message_handlert handler 
)
staticprotected

Definition at line 159 of file bmc.cpp.

◆ run() [1/2]

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

Definition at line 91 of file bmc.h.

◆ run() [2/2]

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

Definition at line 422 of file bmc.cpp.

◆ run_decision_procedure()

decision_proceduret::resultt bmct::run_decision_procedure ( prop_convt prop_conv)
protectedvirtual

Definition at line 129 of file bmc.cpp.

◆ setup()

void bmct::setup ( )

Definition at line 235 of file bmc.cpp.

◆ show()

void bmct::show ( )
protected

Definition at line 442 of file bmc.cpp.

◆ slice()

void bmct::slice ( )
protected

Definition at line 377 of file bmc.cpp.

◆ stop_on_fail()

safety_checkert::resultt bmct::stop_on_fail ( prop_convt solver)
protectedvirtual

Definition at line 455 of file bmc.cpp.

◆ trace_options()

trace_optionst bmct::trace_options ( )
inlineprotected

Definition at line 191 of file bmc.h.

Friends And Related Function Documentation

◆ bmc_all_propertiest

friend class bmc_all_propertiest
friend

Definition at line 215 of file bmc.h.

◆ bmc_covert

friend class bmc_covert
friend

Definition at line 216 of file bmc.h.

◆ bmc_goal_covert

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

Definition at line 218 of file bmc.h.

◆ fault_localizationt

friend class fault_localizationt
friend

Definition at line 219 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 235 of file bmc.h.

◆ equation

symex_target_equationt bmct::equation
protected

Definition at line 172 of file bmc.h.

◆ memory_model

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

Definition at line 176 of file bmc.h.

◆ ns

namespacet bmct::ns
protected

Definition at line 171 of file bmc.h.

◆ options

const optionst& bmct::options
protected

Definition at line 166 of file bmc.h.

◆ outer_symbol_table

const symbol_tablet& bmct::outer_symbol_table
protected

symbol table for the goto-program that we will execute

Definition at line 168 of file bmc.h.

◆ path_storage

path_storaget& bmct::path_storage
protected

Definition at line 173 of file bmc.h.

◆ prop_conv

prop_convt& bmct::prop_conv
protected

Definition at line 175 of file bmc.h.

◆ symex

symex_bmct bmct::symex
protected

Definition at line 174 of file bmc.h.

◆ symex_symbol_table

symbol_tablet bmct::symex_symbol_table
protected

symbol table generated during symbolic execution

Definition at line 170 of file bmc.h.

◆ ui_message_handler

ui_message_handlert& bmct::ui_message_handler
protected

Definition at line 178 of file bmc.h.


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