Skip to content

Commit

Permalink
[path explore 4/7] Factor out common BMC code
Browse files Browse the repository at this point in the history 
The CBMC and JBMC frontends included identical code for running BMC
after the language-specific preprocessing. This commit moves that common
code into a static method of bmct.

Parse options and help text related to bounded model checking are
defined in bmc.h.
  • Loading branch information
@karkhaz
karkhaz committed Feb 20, 2018
1 parent d7a70e1 commit c88a3ab
Show file tree
Hide file tree
Showing 6 changed files with 161 additions and 178 deletions.
68 changes: 68 additions & 0 deletions src/cbmc/bmc.cpp
View file
Expand Up @@ -12,13 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com
#include "bmc.h"

#include <chrono>
#include <exception>
#include <fstream>
#include <iostream>
#include <memory>

#include <util/exit_codes.h>
#include <util/string2int.h>
#include <util/source_location.h>
#include <util/string_utils.h>
#include <util/memory_info.h>
#include <util/message.h>
#include <util/json.h>
#include <util/cprover_prefix.h>
Expand All @@ -37,6 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <goto-symex/memory_model_tso.h>
#include <goto-symex/memory_model_pso.h>

#include "cbmc_solvers.h"
#include "counterexample_beautification.h"
#include "fault_localization.h"

Expand Down Expand Up @@ -595,3 +599,67 @@ void bmct::setup_unwind()
if(options.get_option("unwind")!="")
symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
}

int bmct::do_language_agnostic_bmc(
const optionst &opts,
const goto_modelt &goto_model,
const ui_message_handlert::uit &ui,
messaget &message,
std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc)
{
cbmc_solverst solvers(
opts, goto_model.symbol_table, message.get_message_handler());
solvers.set_ui(ui);
std::unique_ptr<cbmc_solverst::solvert> solver;
try
{
solver = solvers.get_solver();
}
catch(const char *error_msg)
{
message.error() << error_msg << message.eom;
return CPROVER_EXIT_EXCEPTION;
}
catch(const std::string &error_msg)
{
message.error() << error_msg << message.eom;
return CPROVER_EXIT_EXCEPTION;
}
catch(...)
{
message.error() << "unable to get solver" << message.eom;
throw std::current_exception();
}

bmct bmc(
opts,
goto_model.symbol_table,
message.get_message_handler(),
solver->prop_conv());

frontend_configure_bmc(bmc, goto_model);
bmc.set_ui(ui);

int result = CPROVER_EXIT_INTERNAL_ERROR;

// do actual BMC
switch(bmc.run(goto_model.goto_functions))
{
case safety_checkert::resultt::SAFE:
result = CPROVER_EXIT_VERIFICATION_SAFE;
break;
case safety_checkert::resultt::UNSAFE:
result = CPROVER_EXIT_VERIFICATION_UNSAFE;
break;
case safety_checkert::resultt::ERROR:
result = CPROVER_EXIT_INTERNAL_ERROR;
break;
}

// let's log some more statistics
message.debug() << "Memory consumption:" << messaget::endl;
memory_info(message.debug());
message.debug() << eom;

return result;
}
50 changes: 50 additions & 0 deletions src/cbmc/bmc.h
View file
Expand Up @@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <goto-programs/goto_trace.h>

#include <goto-symex/symex_target_equation.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/safety_checker.h>
#include <goto-symex/memory_model.h>

Expand Down Expand Up @@ -82,6 +83,25 @@ class bmct:public safety_checkert
symex.add_recursion_unwind_handler(handler);
}

/// \brief common BMC code, invoked from language-specific frontends
///
/// Do bounded model-checking after all language-specific program
/// preprocessing has been completed by language-specific frontends.
/// Language-specific frontends may customize the \ref bmct objects
/// that are used for model-checking by supplying a function object to
/// the `frontend_configure_bmc` parameter of this function; the
/// function object will be called with every \ref bmct object that
/// is constructed by `do_language_agnostic_bmc`.
static int do_language_agnostic_bmc(
const optionst &opts,
const goto_modelt &goto_model,
const ui_message_handlert::uit &ui,
messaget &message,
std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc =
[](bmct &_bmc, const goto_modelt &) { // NOLINT (*)
// Empty default implementation
});

protected:
const optionst &options;
symbol_tablet new_symbol_table;
Expand Down Expand Up @@ -144,6 +164,36 @@ class bmct:public safety_checkert
template <template <class goalt> class covert>
friend class bmc_goal_covert;
friend class fault_localizationt;

#define OPT_BMC \
"(program-only)" \
"(show-loops)" \
"(show-vcc)" \
"(slice-formula)" \
"(unwinding-assertions)" \
"(no-unwinding-assertions)" \
"(no-pretty-names)" \
"(partial-loops)" \
"(depth):" \
"(unwind):" \
"(unwindset):" \
"(graphml-witness):" \
"(unwindset):"

#define HELP_BMC \
" --program-only only show program expression\n" \
" --show-loops show the loops in the program\n" \
" --depth nr limit search depth\n" \
" --unwind nr unwind nr times\n" \
" --unwindset L:B,... unwind loop L with a bound of B\n" \
" (use --show-loops to get the loop IDs)\n" \
" --show-vcc show the verification conditions\n" \
" --slice-formula remove assignments unrelated to property\n" \
" --unwinding-assertions generate unwinding assertions\n" \
" --partial-loops permit paths with partial loops\n" \
" --no-pretty-names do not simplify identifiers\n" \
" --graphml-witness filename write the witness in GraphML format to " \
"filename\n" // NOLINT(*)
};

#endif // CPROVER_CBMC_BMC_H
81 changes: 5 additions & 76 deletions src/cbmc/cbmc_parse_options.cpp
View file
Expand Up @@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/string2int.h>
#include <util/config.h>
#include <util/unicode.h>
#include <util/memory_info.h>
#include <util/invariant.h>
#include <util/exit_codes.h>

Expand Down Expand Up @@ -63,8 +62,6 @@ Author: Daniel Kroening, kroening@kroening.com

#include <langapi/mode.h>

#include "cbmc_solvers.h"
#include "bmc.h"
#include "version.h"
#include "xml_interface.h"

Expand Down Expand Up @@ -373,13 +370,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
}
else
{
assert(options.get_bool_option("smt2"));
PRECONDITION(options.get_bool_option("smt2"));
options.set_option("z3", true), solver_set=true;
}
}
}
// Either have solver and standard version set, or neither.
assert(version_set==solver_set);
PRECONDITION(version_set == solver_set);

if(cmdline.isset("beautify"))
options.set_option("beautify", true);
Expand Down Expand Up @@ -542,36 +539,8 @@ int cbmc_parse_optionst::doit()
if(set_properties())
return CPROVER_EXIT_SET_PROPERTIES_FAILED;

// get solver
cbmc_solverst cbmc_solvers(
options,
goto_model.symbol_table,
get_message_handler());
cbmc_solvers.set_ui(ui_message_handler.get_ui());

std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;

try
{
cbmc_solver=cbmc_solvers.get_solver();
}

catch(const char *error_msg)
{
error() << error_msg << eom;
return CPROVER_EXIT_EXCEPTION;
}

prop_convt &prop_conv=cbmc_solver->prop_conv();

bmct bmc(
options,
goto_model.symbol_table,
get_message_handler(),
prop_conv);

// do actual BMC
return do_bmc(bmc);
return bmct::do_language_agnostic_bmc(
options, goto_model, ui_message_handler.get_ui(), *this);
}

bool cbmc_parse_optionst::set_properties()
Expand Down Expand Up @@ -871,35 +840,6 @@ bool cbmc_parse_optionst::process_goto_program(
return false;
}

/// invoke main modules
int cbmc_parse_optionst::do_bmc(bmct &bmc)
{
bmc.set_ui(ui_message_handler.get_ui());

int result = CPROVER_EXIT_INTERNAL_ERROR;

// do actual BMC
switch(bmc.run(goto_model.goto_functions))
{
case safety_checkert::resultt::SAFE:
result = CPROVER_EXIT_VERIFICATION_SAFE;
break;
case safety_checkert::resultt::UNSAFE:
result = CPROVER_EXIT_VERIFICATION_UNSAFE;
break;
case safety_checkert::resultt::ERROR:
result = CPROVER_EXIT_INTERNAL_ERROR;
break;
}

// let's log some more statistics
debug() << "Memory consumption:" << messaget::endl;
memory_info(debug());
debug() << eom;

return result;
}

/// display command line help
void cbmc_parse_optionst::help()
{
Expand Down Expand Up @@ -989,18 +929,7 @@ void cbmc_parse_optionst::help()
" --nondet-static add nondeterministic initialization of variables with static lifetime\n"
"\n"
"BMC options:\n"
" --program-only only show program expression\n"
" --show-loops show the loops in the program\n"
" --depth nr limit search depth\n"
" --unwind nr unwind nr times\n"
" --unwindset L:B,... unwind loop L with a bound of B\n"
" (use --show-loops to get the loop IDs)\n"
" --show-vcc show the verification conditions\n"
" --slice-formula remove assignments unrelated to property\n"
" --unwinding-assertions generate unwinding assertions\n"
" --partial-loops permit paths with partial loops\n"
" --no-pretty-names do not simplify identifiers\n"
" --graphml-witness filename write the witness in GraphML format to filename\n" // NOLINT(*)
HELP_BMC
"\n"
"Backend options:\n"
" --object-bits n number of bits used for object addresses\n"
Expand Down
13 changes: 6 additions & 7 deletions src/cbmc/cbmc_parse_options.h
View file
Expand Up @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com

#include <goto-programs/goto_trace.h>

#include "bmc.h"
#include "xml_interface.h"

class bmct;
Expand All @@ -30,21 +31,21 @@ class optionst;

// clang-format off
#define CBMC_OPTIONS \
"(program-only)(preprocess)(slice-by-trace):" \
OPT_BMC \
"(preprocess)(slice-by-trace):" \
OPT_FUNCTIONS \
"(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \
"(no-simplify)(full-slice)" \
"(debug-level):(no-propagation)(no-simplify-if)" \
"(document-subgoals)(outfile):(test-preprocessor)" \
"D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
"(object-bits):" \
"(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
OPT_GOTO_CHECK \
"(no-assertions)(no-assumptions)" \
"(no-built-in-assertions)" \
"(xml-ui)(xml-interface)(json-ui)" \
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
"(no-sat-preprocessor)" \
"(no-pretty-names)(beautify)" \
"(beautify)" \
"(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
"(refine-strings)" \
"(string-printable)" \
Expand All @@ -54,8 +55,7 @@ class optionst;
"(little-endian)(big-endian)" \
OPT_SHOW_GOTO_FUNCTIONS \
OPT_SHOW_PROPERTIES \
"(show-loops)" \
"(show-symbol-table)(show-parse-tree)(show-vcc)" \
"(show-symbol-table)(show-parse-tree)" \
"(drop-unused-functions)" \
"(property):(stop-on-fail)(trace)" \
"(error-label):(verbosity):(no-library)" \
Expand All @@ -69,7 +69,6 @@ class optionst;
"(arrays-uf-always)(arrays-uf-never)" \
"(string-abstraction)(no-arch)(arch):" \
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
"(graphml-witness):" \
"(localize-faults)(localize-faults-method):" \
OPT_GOTO_TRACE \
"(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
Expand Down

0 comments on commit c88a3ab

Please sign in to comment.