cprover
|
Bounded model checking or path exploration for goto-programs. More...
#include <bmc.h>
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) |
![]() | |
safety_checkert (const namespacet &_ns) | |
safety_checkert (const namespacet &_ns, message_handlert &_message_handler) | |
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... | |
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 optionst & | options |
const symbol_tablet & | outer_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_storaget & | path_storage |
symex_bmct | symex |
prop_convt & | prop_conv |
std::unique_ptr< memory_model_baset > | memory_model |
ui_message_handlert & | ui_message_handler |
![]() | |
const namespacet & | ns |
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 | |
![]() | |
enum | resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR, resultt::PAUSED } |
![]() | |
goto_tracet | error_trace |
Bounded model checking or path exploration for goto-programs.
Higher-level architectural information on symbolic execution is documented in the Symbolic execution module page.
|
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:
--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().--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.
|
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.
|
inline |
|
inline |
|
protectedvirtual |
Definition at line 294 of file all_properties.cpp.
|
protected |
Try to cover all goals.
Definition at line 425 of file bmc_cover.cpp.
|
protectedvirtual |
|
static |
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand).
path_strategy_chooser | controls whether symex generates a single large equation for the whole program or an equation per path |
opts | command-line options affecting BMC |
model | provides goto function bodies and the symbol table, perhaps |
ui | user-interface mode (plain text, XML output, JSON output, ...) |
driver_configure_bmc | function provided by the driver program, which applies driver-specific configuration to a bmct before running. |
callback_after_symex | optional callback to be run after symex. See class member bmct::driver_callback_after_symex for details. |
safety_checkert::resultt bmct::execute | ( | abstract_goto_modelt & | goto_model | ) |
|
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.
|
inlinevirtual |
Implements safety_checkert.
|
protected |
|
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.
|
staticprotected |
|
staticprotected |
safety_checkert::resultt bmct::run | ( | abstract_goto_modelt & | goto_model | ) |
|
inlinevirtual |
|
protectedvirtual |
|
protectedvirtual |
|
inlineprotected |
|
friend |
|
friend |
|
friend |
|
friend |
|
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.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |