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, guard_managert &guard_manager)
 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 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, guard_managert &guard_manager)
 Constructor for path exploration from saved state. More...
 
virtual decision_proceduret::resultt run_decision_procedure ()
 
virtual resultt decide (const goto_functionst &)
 
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)
 
virtual resultt stop_on_fail ()
 

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

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 42 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,
guard_managert guard_manager 
)
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 67 of file bmc.h.

◆ ~bmct()

virtual bmct::~bmct ( )
inlinevirtual

Definition at line 103 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,
guard_managert guard_manager 
)
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 139 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 112 of file bmc.h.

◆ add_unwind_recursion_handler()

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

Definition at line 117 of file bmc.h.

◆ all_properties()

safety_checkert::resultt bmct::all_properties ( const goto_functionst goto_functions)
protectedvirtual

Definition at line 297 of file all_properties.cpp.

◆ decide()

safety_checkert::resultt bmct::decide ( const goto_functionst goto_functions)
protectedvirtual

Definition at line 191 of file bmc.cpp.

◆ do_language_agnostic_bmc()

int bmct::do_language_agnostic_bmc ( 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
optscommand-line options affecting BMC
modelprovides goto function bodies and the symbol table, perhaps creating those function bodies on demand.
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 247 of file bmc.cpp.

◆ execute()

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

Definition at line 70 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 38 of file bmc.cpp.

◆ operator()()

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

Implements safety_checkert.

Definition at line 106 of file bmc.h.

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

◆ run() [1/2]

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

Definition at line 95 of file bmc.h.

◆ run() [2/2]

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

Definition at line 182 of file bmc.cpp.

◆ run_decision_procedure()

decision_proceduret::resultt bmct::run_decision_procedure ( )
protectedvirtual

Definition at line 43 of file bmc.cpp.

◆ setup()

void bmct::setup ( )

◆ stop_on_fail()

safety_checkert::resultt bmct::stop_on_fail ( )
protectedvirtual

Definition at line 199 of file bmc.cpp.

◆ trace_options()

trace_optionst bmct::trace_options ( )
inlineprotected

Definition at line 193 of file bmc.h.

Friends And Related Function Documentation

◆ bmc_all_propertiest

friend class bmc_all_propertiest
friend

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

◆ equation

symex_target_equationt bmct::equation
protected

Definition at line 178 of file bmc.h.

◆ guard_manager

guard_managert& bmct::guard_manager
protected

Definition at line 179 of file bmc.h.

◆ memory_model

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

Definition at line 183 of file bmc.h.

◆ ns

namespacet bmct::ns
protected

Definition at line 177 of file bmc.h.

◆ options

const optionst& bmct::options
protected

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

◆ path_storage

path_storaget& bmct::path_storage
protected

Definition at line 180 of file bmc.h.

◆ prop_conv

prop_convt& bmct::prop_conv
protected

Definition at line 182 of file bmc.h.

◆ symex

symex_bmct bmct::symex
protected

Definition at line 181 of file bmc.h.

◆ symex_symbol_table

symbol_tablet bmct::symex_symbol_table
protected

symbol table generated during symbolic execution

Definition at line 176 of file bmc.h.

◆ ui_message_handler

ui_message_handlert& bmct::ui_message_handler
protected

Definition at line 185 of file bmc.h.


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