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, 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) |
![]() | |
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, 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... | |
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) |
Try to cover all goals. More... | |
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::uit | ui |
![]() | |
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, resultt::UNKNOWN } |
![]() | |
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. 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.
|
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.
|
inline |
Definition at line 115 of file bmc.h.
References symex_bmct::add_loop_unwind_handler(), and symex.
Referenced by jbmc_parse_optionst::doit().
|
inline |
Definition at line 120 of file bmc.h.
References symex_bmct::add_recursion_unwind_handler(), and symex.
|
protectedvirtual |
Definition at line 232 of file all_properties.cpp.
References messaget::get_message_handler(), messaget::set_message_handler(), and solver().
Referenced by decide().
|
protected |
Try to cover all goals.
Definition at line 423 of file bmc_cover.cpp.
References messaget::get_message_handler(), and messaget::set_message_handler().
Referenced by execute().
|
protectedvirtual |
Definition at line 489 of file bmc.cpp.
References all_properties(), optionst::get_bool_option(), messaget::get_message_handler(), options, prop_conv, messaget::set_message_handler(), and stop_on_fail().
Referenced by execute().
|
protected |
Definition at line 112 of file bmc.cpp.
References symex_target_equationt::convert(), messaget::eom(), equation, freeze_program_variables(), prop_conv, and messaget::status().
Referenced by bmc_all_propertiest::operator()(), bmc_covert::operator()(), fault_localizationt::run_decision_procedure(), and run_decision_procedure().
|
static |
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand).
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, ...) |
message | used for logging |
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. |
Definition at line 559 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, optionst::is_set(), 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().
|
protectedvirtual |
Definition at line 47 of file bmc.cpp.
References build_goto_trace(), convert(), messaget::eom(), equation, safety_checkert::error_trace, messaget::mstreamt::json_stream(), ui_message_handlert::JSON_UI, ns, goto_trace_stept::pc, ui_message_handlert::PLAIN, prop_conv, json_stream_arrayt::push_back_stream_object(), messaget::result(), show_goto_trace(), messaget::status(), goto_tracet::steps, trace_options(), ui, xml(), and ui_message_handlert::XML_UI.
Referenced by fault_localizationt::stop_on_fail(), and stop_on_fail().
safety_checkert::resultt bmct::execute | ( | abstract_goto_modelt & | goto_model | ) |
Definition at line 323 of file bmc.cpp.
References cover(), decide(), driver_callback_after_symex, messaget::eom(), equation, safety_checkert::ERROR, messaget::error(), optionst::get_bool_option(), abstract_goto_modelt::get_goto_function(), abstract_goto_modelt::get_goto_functions(), optionst::get_list_option(), messaget::get_message_handler(), optionst::get_option(), symex_target_equationt::has_threads(), symex_bmct::last_source_location, memory_model, options, symex_bmct::output_coverage_report(), output_graphml(), safety_checkert::PAUSED, perform_symbolic_execution(), prop_conv, goto_symext::remaining_vccs, report_success(), safety_checkert::SAFE, goto_symext::should_pause_symex, show_program(), show_vcc(), slice(), messaget::mstreamt::source_location, symex_target_equationt::SSA_steps, messaget::statistics(), and symex.
Referenced by run().
|
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().
|
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().
|
inlinevirtual |
|
protected |
outputs witnesses in graphml format
Definition at line 89 of file bmc.cpp.
References equation, safety_checkert::error_trace, optionst::get_option(), graphml_witnesst::graph(), ns, options, messaget::result(), safety_checkert::SAFE, safety_checkert::UNSAFE, and write_graphml().
Referenced by execute(), and stop_on_fail().
|
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 695 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().
|
protectedvirtual |
Definition at line 176 of file bmc.cpp.
References xmlt::data, messaget::eom(), ui_message_handlert::JSON_UI, ui_message_handlert::PLAIN, messaget::result(), ui, xml(), and ui_message_handlert::XML_UI.
Referenced by bmc_all_propertiest::operator()(), fault_localizationt::stop_on_fail(), and stop_on_fail().
|
protectedvirtual |
Definition at line 149 of file bmc.cpp.
References xmlt::data, messaget::eom(), ui_message_handlert::JSON_UI, ui_message_handlert::PLAIN, messaget::result(), ui, xml(), and ui_message_handlert::XML_UI.
Referenced by execute(), bmc_all_propertiest::operator()(), fault_localizationt::stop_on_fail(), and stop_on_fail().
|
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()().
safety_checkert::resultt bmct::run | ( | abstract_goto_modelt & | goto_model | ) |
|
protectedvirtual |
Definition at line 124 of file bmc.cpp.
References decision_proceduret::dec_solve(), decision_proceduret::decision_procedure_text(), do_conversion(), messaget::eom(), messaget::get_message_handler(), prop_conv, messaget::set_message_handler(), and messaget::status().
Referenced by stop_on_fail().
|
inline |
void bmct::setup | ( | ) |
Definition at line 305 of file bmc.cpp.
References messaget::eom(), get_memory_model(), optionst::get_option(), INITIALIZE_FUNCTION, goto_symext::language_mode, symex_bmct::last_source_location, namespacet::lookup(), irept::make_nil(), symbolt::mode, ns, options, unwindsett::parse_unwind(), unwindsett::parse_unwindset(), messaget::status(), symex, and symex_bmct::unwindset.
Referenced by run().
|
protected |
Definition at line 501 of file bmc.cpp.
References optionst::get_bool_option(), options, show_program(), and show_vcc().
|
protectedvirtual |
Definition at line 203 of file bmc.cpp.
References equation, from_expr(), ns, symex_target_equationt::SSA_steps, and to_string().
|
protectedvirtual |
Definition at line 135 of file show_vcc.cpp.
References messaget::eom(), messaget::error(), optionst::get_option(), ui_message_handlert::JSON_UI, options, ui_message_handlert::PLAIN, show_vcc_json(), show_vcc_plain(), ui, and ui_message_handlert::XML_UI.
|
protectedvirtual |
Definition at line 79 of file show_vcc.cpp.
References equation, from_expr(), symex_target_equationt::has_threads(), irept::is_not_nil(), json(), jsont::make_array(), jsont::make_object(), ns, json_arrayt::push_back(), and symex_target_equationt::SSA_steps.
Referenced by show_vcc().
|
protectedvirtual |
Definition at line 23 of file show_vcc.cpp.
References equation, from_expr(), symex_target_equationt::has_threads(), languages, ns, and symex_target_equationt::SSA_steps.
Referenced by show_vcc().
|
protected |
Definition at line 439 of file bmc.cpp.
References symex_target_equationt::count_ignored_SSA_steps(), messaget::eom(), equation, optionst::get_bool_option(), optionst::get_list_option(), optionst::get_option(), symex_target_equationt::has_threads(), ns, options, goto_symext::remaining_vccs, simple_slice(), symex_slice_by_tracet::slice_by_trace(), messaget::statistics(), symex, and goto_symext::total_vccs.
Referenced by execute().
|
protectedvirtual |
Definition at line 514 of file bmc.cpp.
References decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), equation, safety_checkert::ERROR, messaget::error(), error_trace(), optionst::get_bool_option(), optionst::get_option(), options, output_graphml(), prop_conv, report_failure(), report_success(), run_decision_procedure(), safety_checkert::SAFE, and safety_checkert::UNSAFE.
Referenced by decide().
|
inlineprotected |
Definition at line 206 of file bmc.h.
References options.
Referenced by error_trace(), bmc_covert::operator()(), and bmc_all_propertiest::report().
|
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.
Definition at line 248 of file bmc.h.
Referenced by execute().
|
protected |
Definition at line 183 of file bmc.h.
Referenced by fault_localizationt::collect_guards(), do_conversion(), error_trace(), execute(), fault_localizationt::freeze_guards(), fault_localizationt::get_failed_property(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), bmc_all_propertiest::operator()(), bmc_covert::operator()(), output_graphml(), path_explorert::perform_symbolic_execution(), fault_localizationt::run(), bmc_covert::satisfying_assignment(), show_program(), show_vcc_json(), show_vcc_plain(), slice(), fault_localizationt::stop_on_fail(), and stop_on_fail().
|
protected |
Definition at line 187 of file bmc.h.
Referenced by execute(), and get_memory_model().
|
protected |
Definition at line 182 of file bmc.h.
Referenced by error_trace(), get_memory_model(), bmc_covert::get_test(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), bmc_covert::operator()(), output_graphml(), bmc_all_propertiest::report(), bmc_covert::satisfying_assignment(), setup(), show_program(), show_vcc_json(), show_vcc_plain(), and slice().
|
protected |
Definition at line 177 of file bmc.h.
Referenced by bmct(), decide(), execute(), get_memory_model(), bmc_covert::operator()(), output_graphml(), perform_symbolic_execution(), bmc_all_propertiest::report(), setup(), show(), show_vcc(), slice(), stop_on_fail(), and trace_options().
|
protected |
|
protected |
Definition at line 184 of file bmc.h.
Referenced by perform_symbolic_execution().
|
protected |
Definition at line 186 of file bmc.h.
Referenced by fault_localizationt::check(), decide(), do_conversion(), error_trace(), execute(), fault_localizationt::freeze_guards(), fault_localizationt::get_failed_property(), fault_localizationt::run(), run_decision_procedure(), fault_localizationt::stop_on_fail(), stop_on_fail(), and fault_localizationt::update_scores().
|
protected |
Definition at line 185 of file bmc.h.
Referenced by add_loop_unwind_handler(), add_unwind_recursion_handler(), bmct(), execute(), perform_symbolic_execution(), path_explorert::perform_symbolic_execution(), setup(), and slice().
|
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().
|
protected |
Definition at line 189 of file bmc.h.
Referenced by do_language_agnostic_bmc(), error_trace(), bmc_covert::operator()(), bmc_all_propertiest::report(), fault_localizationt::report(), report_failure(), report_success(), set_ui(), show_vcc(), and fault_localizationt::stop_on_fail().