[path explore 4/7] Factor out common BMC code

karkhaz · karkhaz · commit c88a3ab5a0aa · 2018-02-20T23:08:17.000Z
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.
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -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>
@@ -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"
 
@@ -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;
+}
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -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>
 
@@ -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;
@@ -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
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -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>
 
@@ -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"
 
@@ -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);
@@ -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()
@@ -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()
 {
@@ -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"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -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;
@@ -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)" \
@@ -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)" \
@@ -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)
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
