Add goto-bmc executable.

Add a new `goto-bmc` executable to CBMC that reads a core-goto program
from a given binary file and runs symex and the decision procedure.
This has been done by using the API functionalities instead of addin a
new argument to CBMC.

CMakeLists.txt

@@ -228,6 +228,7 @@ cprover_default_properties(
     driver
     goto-analyzer
     goto-analyzer-lib
+    goto-bmc
     goto-cc
     goto-cc-lib
     goto-checker

src/CMakeLists.txt

@@ -120,6 +120,7 @@ add_subdirectory(goto-harness)
 add_subdirectory(goto-synthesizer)
 add_subdirectory(symtab2gb)
 add_subdirectory(libcprover-cpp)
+add_subdirectory(goto-bmc)
 
 if(UNIX OR WITH_MEMORY_ANALYZER)
 add_subdirectory(memory-analyzer)

src/goto-bmc/CMakeLists.txt

@@ -0,0 +1,6 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_executable(goto-bmc ${sources})
+
+generic_includes(goto-bmc)
+
+target_link_libraries(goto-bmc cprover-api-cpp)

src/goto-bmc/goto_bmc_main.cpp

@@ -0,0 +1,11 @@
+// Author: Enrico Steffinlongo for Diffblue Ltd.
+
+#include "goto_bmc_parse_options.h"
+
+#include <iostream>
+#include <vector>
+
+int main(int argc, const char **argv)
+{
+  return core_cbmc_only_parse_optionst{argc, argv}.main();
+}

src/goto-bmc/goto_bmc_parse_options.cpp

@@ -0,0 +1,98 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#include "goto_bmc_parse_options.h"
+
+#include <util/exit_codes.h>
+#include <util/message.h>
+
+#include <goto-programs/read_goto_binary.h>
+
+#include <libcprover-cpp/api_options.h>
+
+#include "api.h"
+
+#include <iostream>
+#include <map>
+
+core_cbmc_only_parse_optionst::core_cbmc_only_parse_optionst(
+  int argc,
+  const char **argv)
+  : parse_options_baset(
+      CORE_CBMC_ONLY_OPTIONS,
+      argc,
+      argv,
+      std::string("CORE_CBMC_ONLY") + CBMC_VERSION)
+{
+}
+
+void print_messages_to_stdout(
+  const api_messaget &message,
+  api_call_back_contextt)
+{
+  std::cout << api_message_get_string(message) << std::endl;
+}
+
+int core_cbmc_only_parse_optionst::doit()
+{
+  auto api_options = api_optionst::create();
+
+  if(cmdline.isset("version"))
+  {
+    std::cout << CBMC_VERSION << '\n';
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  if(cmdline.isset("help"))
+  {
+    help();
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  if(
+    cmdline.args.size() != 1 ||
+    !is_goto_binary(cmdline.args[0], ui_message_handler))
+  {
+    log.error() << "Please give exactly one binary file" << messaget::eom;
+    return CPROVER_EXIT_INCORRECT_TASK;
+  }
+
+  std::string filename = cmdline.args[0];
+
+  if(cmdline.isset("validate-goto-model"))
+  {
+    api_options.validate_goto_model(true);
+  }
+
+  // With options set, we can now initiate the API and perform analysis.
+  api_sessiont api{api_options};
+  std::cout << "CoreBMC version ";
+  std::cout << *api.get_api_version() << std::endl;
+
+  // The API works with a callback for querying state - we for now just print
+  // collected messages from the message buffer to stdout.
+  api.set_message_callback(print_messages_to_stdout, nullptr);
+
+  // Finally, we read the goto-binary the user supplied...
+  api.read_goto_binary(filename);
+
+  // ... and run analysis on it.
+  auto result = api.run_verifier();
+
+  return CPROVER_EXIT_SUCCESS;
+}
+
+void core_cbmc_only_parse_optionst::help()
+{
+  // clang-format off
+  std::cout << '\n' << banner_string("goto-bmc", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2023") << '\n'
+            << align_center_with_border("Diffblue Ltd.") << '\n' // NOLINT(*)
+            <<
+    "\n"
+    "Usage:                       Purpose:\n"
+    "\n"
+    "goto-bmc [-?] [-h] [--help]      show help\n"
+    "goto-bmc --version               show version and exit\n"
+    "goto-bmc [options] file.c ...    perform bounded model checking on core goto-binary\n";
+  // clang-format on
+}

src/goto-bmc/goto_bmc_parse_options.h

@@ -0,0 +1,34 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#ifndef CPROVER_CORE_BMC_PARSE_OPTIONS_H
+#define CPROVER_CORE_BMC_PARSE_OPTIONS_H
+
+#include <util/parse_options.h>
+#include <util/version.h>
+
+#include <libcprover-cpp/api_options.h>
+
+#include <memory>
+#include <string>
+#include <vector>
+
+api_optionst parse_command_line_options(const std::vector<std::string> &);
+
+void help();
+
+// clang-format off
+#define CORE_CBMC_ONLY_OPTIONS \
+  "(version)"
+// clang-format on
+
+class core_cbmc_only_parse_optionst : public parse_options_baset
+{
+public:
+  core_cbmc_only_parse_optionst(int argc, const char **argv);
+
+  virtual void help();
+
+  virtual int doit();
+};
+
+#endif // CPROVER_CORE_BMC_PARSE_OPTIONS_H