From c88a3ab5a0aa38328f45c9c1174e63b723518c59 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Wed, 29 Nov 2017 13:48:49 -0500
Subject: [PATCH] [path explore 4/7] Factor out common BMC code

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.
---
 src/cbmc/bmc.cpp                |  68 +++++++++++++++++++
 src/cbmc/bmc.h                  |  50 ++++++++++++++
 src/cbmc/cbmc_parse_options.cpp |  81 ++---------------------
 src/cbmc/cbmc_parse_options.h   |  13 ++--
 src/jbmc/jbmc_parse_options.cpp | 114 +++++++-------------------------
 src/jbmc/jbmc_parse_options.h   |  13 ++--
 6 files changed, 161 insertions(+), 178 deletions(-)

diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 9bc86d3eec6..4e5a1c9bba2 100644
--- 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
index b3f9a7846e1..d46ae0812cc 100644
--- 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
index 1048b322a0f..e70b0eac746 100644
--- 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
index c5fe31e6b88..835088622f0 100644
--- 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
index 65075e12abf..e1a598a6588 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_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 <langapi/language.h>
@@ -58,8 +57,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
 
-#include <cbmc/cbmc_solvers.h>
-#include <cbmc/bmc.h>
 #include <cbmc/version.h>
 
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
@@ -492,55 +489,34 @@ int jbmc_parse_optionst::doit()
   if(set_properties(goto_model))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
-  // get solver
-  cbmc_solverst jbmc_solvers(
-    options,
-    goto_model.symbol_table,
-    get_message_handler());
-
-  jbmc_solvers.set_ui(ui_message_handler.get_ui());
-
-  std::unique_ptr<cbmc_solverst::solvert> jbmc_solver;
-
-  try
+  std::function<void(bmct &, const goto_modelt &)> configure_bmc;
+  if(options.get_bool_option("java-unwind-enum-static"))
   {
-    jbmc_solver=jbmc_solvers.get_solver();
+    configure_bmc = [](
+      bmct &bmc, const goto_modelt &goto_model) { // NOLINT (*)
+        bmc.add_loop_unwind_handler([&goto_model](
+                                      const irep_idt &function_id,
+                                      unsigned loop_number,
+                                      unsigned unwind,
+                                      unsigned &max_unwind) { // NOLINT (*)
+          return java_enum_static_init_unwind_handler(
+            function_id,
+            loop_number,
+            unwind,
+            max_unwind,
+            goto_model.symbol_table);
+        });
+    };
   }
-
-  catch(const char *error_msg)
+  else
   {
-    error() << error_msg << eom;
-    return 1; // should contemplate EX_SOFTWARE from sysexits.h
+    configure_bmc = [](
+      bmct &bmc, const goto_modelt &goto_model) { // NOLINT (*)
+      // NOOP
+    };
   }
-
-  prop_convt &prop_conv=jbmc_solver->prop_conv();
-
-  bmct bmc(
-    options,
-    goto_model.symbol_table,
-    get_message_handler(),
-    prop_conv);
-
-  // unwinds <clinit> loops to number of enum elements
-  if(options.get_bool_option("java-unwind-enum-static"))
-  {
-    bmc.add_loop_unwind_handler(
-      [&goto_model]
-      (const irep_idt &function_id,
-       unsigned loop_number,
-       unsigned unwind,
-       unsigned &max_unwind) { // NOLINT (*)
-        return java_enum_static_init_unwind_handler(
-          function_id,
-          loop_number,
-          unwind,
-          max_unwind,
-          goto_model.symbol_table);
-      });
-  }
-
-  // do actual BMC
-  return do_bmc(bmc, goto_model);
+  return bmct::do_language_agnostic_bmc(
+    options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc);
 }
 
 bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model)
@@ -838,35 +814,6 @@ bool jbmc_parse_optionst::process_goto_functions(
   return false;
 }
 
-/// invoke main modules
-int jbmc_parse_optionst::do_bmc(bmct &bmc, goto_modelt &goto_model)
-{
-  bmc.set_ui(ui_message_handler.get_ui());
-
-  int result=6;
-
-  // do actual BMC
-  switch(bmc.run(goto_model.goto_functions))
-  {
-    case safety_checkert::resultt::SAFE:
-      result=0;
-      break;
-    case safety_checkert::resultt::UNSAFE:
-      result=10;
-      break;
-    case safety_checkert::resultt::ERROR:
-      result=6;
-      break;
-  }
-
-  // let's log some more statistics
-  debug() << "Memory consumption:" << messaget::endl;
-  memory_info(debug());
-  debug() << eom;
-
-  return result;
-}
-
 /// display command line help
 void jbmc_parse_optionst::help()
 {
@@ -921,18 +868,7 @@ void jbmc_parse_optionst::help()
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n" // NOLINT(*)
     "\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/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
index c2793540805..804df90e9e9 100644
--- a/src/jbmc/jbmc_parse_options.h
+++ b/src/jbmc/jbmc_parse_options.h
@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <cbmc/bmc.h>
+
 #include <goto-programs/goto_trace.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/show_properties.h>
@@ -32,21 +34,21 @@ class optionst;
 
 // clang-format off
 #define JBMC_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):" \
   "(object-bits):" \
   "(classpath):(cp):(main-class):" \
-  "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(no-built-in-assertions)" \
   "(xml-ui)(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)" \
@@ -55,7 +57,7 @@ class optionst;
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   "(show-loops)" \
-  "(show-symbol-table)(show-parse-tree)(show-vcc)" \
+  "(show-symbol-table)(show-parse-tree)" \
   OPT_SHOW_PROPERTIES \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
@@ -67,7 +69,6 @@ class optionst;
   "(ppc-macos)" \
   "(arrays-uf-always)(arrays-uf-never)" \
   "(no-arch)(arch):" \
-  "(graphml-witness):" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS \
   "(java-unwind-enum-static)" \
   "(localize-faults)(localize-faults-method):" \