From d0ab60c52a56fbe016724729e389a9124d6d0978 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@gmail.com>
Date: Wed, 26 Oct 2022 16:14:58 +0100
Subject: [PATCH] Add first version of a C++ API for CBMC.

This also adds a regression testing binary driver under
`regression/libcprover-cpp/call_bmc.cpp`, for testing the
API.

The library being built is `lib/libcprover-api-cpp.a`.
---
 CMakeLists.txt                                |  1 +
 CODEOWNERS                                    |  2 +-
 regression/CMakeLists.txt                     |  1 +
 regression/libcprover-cpp/CMakeLists.txt      | 40 ++++++++++++++
 regression/libcprover-cpp/call_bmc.cpp        | 37 +++++++++++++
 .../model_loading/CMakeLists.txt              |  3 ++
 .../model_loading/load_basic_c_file/test.c    |  7 +++
 .../model_loading/load_basic_c_file/test.desc |  8 +++
 src/CMakeLists.txt                            |  1 +
 src/libcprover-cpp/CMakeLists.txt             |  6 +++
 src/libcprover-cpp/api.cpp                    | 54 +++++++++++++++++++
 src/libcprover-cpp/api.h                      | 36 +++++++++++++
 src/libcprover-cpp/module_dependencies.txt    |  4 ++
 src/libcprover-cpp/options.cpp                | 24 +++++++++
 src/libcprover-cpp/options.h                  | 26 +++++++++
 src/libcprover-cpp/readme.md                  | 19 +++++++
 16 files changed, 268 insertions(+), 1 deletion(-)
 create mode 100644 regression/libcprover-cpp/CMakeLists.txt
 create mode 100644 regression/libcprover-cpp/call_bmc.cpp
 create mode 100644 regression/libcprover-cpp/model_loading/CMakeLists.txt
 create mode 100644 regression/libcprover-cpp/model_loading/load_basic_c_file/test.c
 create mode 100644 regression/libcprover-cpp/model_loading/load_basic_c_file/test.desc
 create mode 100644 src/libcprover-cpp/CMakeLists.txt
 create mode 100644 src/libcprover-cpp/api.cpp
 create mode 100644 src/libcprover-cpp/api.h
 create mode 100644 src/libcprover-cpp/module_dependencies.txt
 create mode 100644 src/libcprover-cpp/options.cpp
 create mode 100644 src/libcprover-cpp/options.h
 create mode 100644 src/libcprover-cpp/readme.md

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 38807e9c5c2..9b3cf172173 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -215,6 +215,7 @@ cprover_default_properties(
     cbmc
     cbmc-lib
     cpp
+    cprover-api-cpp
     cprover
     cprover-lib
     crangler
diff --git a/CODEOWNERS b/CODEOWNERS
index 28922e809e8..562f374ee29 100644
--- a/CODEOWNERS
+++ b/CODEOWNERS
@@ -38,7 +38,7 @@
 /jbmc/src/java_bytecode/ @romainbrenguier @peterschrammel
 /src/analyses/ @martin-cs @peterschrammel @chris-ryder
 /src/pointer-analysis/ @martin-cs @peterschrammel @chris-ryder
-
+/src/libcprover-cpp @NlightNFotis @thomasspriggs @esteffin @TGWDB @peterschrammel
 
 # These files change frequently and changes are medium-risk
 
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index 04bdfce5694..fee76490541 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -85,6 +85,7 @@ add_subdirectory(goto-interpreter)
 add_subdirectory(cbmc-sequentialization)
 add_subdirectory(cpp-linter)
 add_subdirectory(catch-framework)
+add_subdirectory(libcprover-cpp)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)
diff --git a/regression/libcprover-cpp/CMakeLists.txt b/regression/libcprover-cpp/CMakeLists.txt
new file mode 100644
index 00000000000..66f9a501117
--- /dev/null
+++ b/regression/libcprover-cpp/CMakeLists.txt
@@ -0,0 +1,40 @@
+file(GLOB_RECURSE api_sources "../src/libcprover-cpp/*.cpp" "../src/libcprover-cpp/*.h")
+
+# This step builds a binary driving the API (to be used for testing)
+add_executable(api-binary-driver call_bmc.cpp ${api_sources})
+cprover_default_properties(api-binary-driver)
+target_include_directories(api-binary-driver
+    PUBLIC
+    ${CBMC_BINARY_DIR}
+    ${CBMC_SOURCE_DIR}
+    # TODO: Should be fixed for the proper include form.
+    ${CMAKE_CURRENT_SOURCE_DIR}/../src/libcprover-cpp/)
+target_link_libraries(api-binary-driver goto-programs util langapi ansi-c cprover-api-cpp)
+
+# Enable test running
+set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
+
+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND perl ${test_pl_path} -e -p -c "${cmdline}" ${flag} ${ARGN}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile};CBMC"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests cmdline)
+    get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
+    message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
+endmacro(add_test_pl_tests)
+
+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
+add_subdirectory(model_loading)
diff --git a/regression/libcprover-cpp/call_bmc.cpp b/regression/libcprover-cpp/call_bmc.cpp
new file mode 100644
index 00000000000..d5094d2cc80
--- /dev/null
+++ b/regression/libcprover-cpp/call_bmc.cpp
@@ -0,0 +1,37 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+// Test file to try loading a GOTO-model into memory and running a sample verification run on it.
+#include <util/exception_utils.h>
+
+#include <libcprover-cpp/api.h>
+#include <libcprover-cpp/options.h>
+
+#include <iostream>
+#include <vector>
+
+int main(int argc, char *argv[])
+{
+  try
+  {
+    std::cout << "Hello from API stub" << std::endl;
+
+    // Convert argv to vector of strings for initialize_goto_model
+    std::vector<std::string> arguments(argv + 1, argv + argc);
+
+    // Create API options object, to pass to initialiser of API object.
+    auto api_options = api_optionst::create().simplify(false);
+
+    // Initialise API dependencies and global configuration in one step.
+    api_sessiont api(api_options);
+
+    // Demonstrate the loading of a goto-model from the command line arguments
+    api.load_model_from_files(arguments);
+
+    std::cout << "Successfully initialised goto_model" << std::endl;
+    return 0;
+  }
+  catch(const invalid_command_line_argument_exceptiont &e)
+  {
+    std::cout << e.what() << std::endl;
+  }
+}
diff --git a/regression/libcprover-cpp/model_loading/CMakeLists.txt b/regression/libcprover-cpp/model_loading/CMakeLists.txt
new file mode 100644
index 00000000000..588a3f60c5a
--- /dev/null
+++ b/regression/libcprover-cpp/model_loading/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:api-binary-driver>"
+)
diff --git a/regression/libcprover-cpp/model_loading/load_basic_c_file/test.c b/regression/libcprover-cpp/model_loading/load_basic_c_file/test.c
new file mode 100644
index 00000000000..69b0d6f0bc6
--- /dev/null
+++ b/regression/libcprover-cpp/model_loading/load_basic_c_file/test.c
@@ -0,0 +1,7 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int a[] = {0, 1, 2, 3, 4};
+  assert(a[4] != 4);
+}
diff --git a/regression/libcprover-cpp/model_loading/load_basic_c_file/test.desc b/regression/libcprover-cpp/model_loading/load_basic_c_file/test.desc
new file mode 100644
index 00000000000..6dac94ee130
--- /dev/null
+++ b/regression/libcprover-cpp/model_loading/load_basic_c_file/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+Successfully initialised goto_model
+--
+--
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 665442ad6a4..ecc6b2b3e66 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -102,6 +102,7 @@ add_subdirectory(jsil)
 add_subdirectory(json)
 add_subdirectory(json-symtab-language)
 add_subdirectory(langapi)
+add_subdirectory(libcprover-cpp)
 add_subdirectory(linking)
 add_subdirectory(pointer-analysis)
 add_subdirectory(solvers)
diff --git a/src/libcprover-cpp/CMakeLists.txt b/src/libcprover-cpp/CMakeLists.txt
new file mode 100644
index 00000000000..8483d5b627a
--- /dev/null
+++ b/src/libcprover-cpp/CMakeLists.txt
@@ -0,0 +1,6 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+
+# This step builds the API in the form of a statically linked library (libcprover-api-cpp.a)
+add_library(cprover-api-cpp ${sources})
+generic_includes(cprover-api-cpp)
+target_link_libraries(cprover-api-cpp goto-programs util langapi ansi-c)
diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp
new file mode 100644
index 00000000000..efd4ef0e880
--- /dev/null
+++ b/src/libcprover-cpp/api.cpp
@@ -0,0 +1,54 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#include "api.h"
+
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/message.h>
+#include <util/options.h>
+
+#include <goto-programs/goto_model.h>
+#include <goto-programs/initialize_goto_model.h>
+
+#include <ansi-c/ansi_c_language.h>
+#include <langapi/mode.h>
+
+#include <memory>
+#include <string>
+#include <vector>
+
+extern configt config;
+
+api_sessiont::api_sessiont()
+  : message_handler(
+      util_make_unique<null_message_handlert>(null_message_handlert{})),
+    options(util_make_unique<optionst>(optionst{}))
+{
+  // Needed to initialise the language options correctly
+  cmdlinet cmdline;
+  // config is global in config.cpp
+  config.set(cmdline);
+  // Initialise C language mode
+  register_language(new_ansi_c_language);
+}
+
+api_sessiont::api_sessiont(const api_optionst &options)
+  : message_handler(
+      util_make_unique<null_message_handlert>(null_message_handlert{})),
+    options(options.to_engine_options())
+{
+  // Needed to initialise the language options correctly
+  cmdlinet cmdline;
+  // config is global in config.cpp
+  config.set(cmdline);
+  // Initialise C language mode
+  register_language(new_ansi_c_language);
+}
+
+api_sessiont::~api_sessiont() = default;
+
+void api_sessiont::load_model_from_files(const std::vector<std::string> &files)
+{
+  model = util_make_unique<goto_modelt>(
+    initialize_goto_model(files, *message_handler, *options));
+}
diff --git a/src/libcprover-cpp/api.h b/src/libcprover-cpp/api.h
new file mode 100644
index 00000000000..1d712f3f2a4
--- /dev/null
+++ b/src/libcprover-cpp/api.h
@@ -0,0 +1,36 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#ifndef CPROVER_LIBCPROVER_CPP_API_H
+#define CPROVER_LIBCPROVER_CPP_API_H
+
+#include <memory>
+#include <string>
+#include <vector>
+
+// Forward declaration of API dependencies
+class goto_modelt;
+class message_handlert;
+class optionst;
+
+#include "options.h"
+
+// An object in the pattern of Session Facade - owning all of the memory
+// the API is using and being responsible for the management of that.
+struct api_sessiont
+{
+  // Initialising constructor
+  api_sessiont();
+  explicit api_sessiont(const api_optionst &options);
+  ~api_sessiont(); // default constructed in the .cpp file
+
+  /// Load a goto_model from a given vector of filenames.
+  /// \param files: A vector<string> containing the filenames to be loaded
+  void load_model_from_files(const std::vector<std::string> &files);
+
+private:
+  std::unique_ptr<goto_modelt> model;
+  std::unique_ptr<message_handlert> message_handler;
+  std::unique_ptr<optionst> options;
+};
+
+#endif
diff --git a/src/libcprover-cpp/module_dependencies.txt b/src/libcprover-cpp/module_dependencies.txt
new file mode 100644
index 00000000000..fcb60bfad66
--- /dev/null
+++ b/src/libcprover-cpp/module_dependencies.txt
@@ -0,0 +1,4 @@
+ansi-c
+langapi
+goto-programs
+util
diff --git a/src/libcprover-cpp/options.cpp b/src/libcprover-cpp/options.cpp
new file mode 100644
index 00000000000..1f1787b2b13
--- /dev/null
+++ b/src/libcprover-cpp/options.cpp
@@ -0,0 +1,24 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#include "options.h"
+
+#include <util/make_unique.h>
+#include <util/options.h>
+
+api_optionst api_optionst::create()
+{
+  return api_optionst{};
+}
+
+api_optionst &api_optionst::simplify(bool on)
+{
+  simplify_enabled = on;
+  return *this;
+}
+
+std::unique_ptr<optionst> api_optionst::to_engine_options() const
+{
+  optionst engine_options;
+  engine_options.set_option("simplify", simplify_enabled);
+  return util_make_unique<optionst>(engine_options);
+}
diff --git a/src/libcprover-cpp/options.h b/src/libcprover-cpp/options.h
new file mode 100644
index 00000000000..cd1b373278e
--- /dev/null
+++ b/src/libcprover-cpp/options.h
@@ -0,0 +1,26 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#ifndef CPROVER_LIBCPROVER_CPP_OPTIONS_H
+#define CPROVER_LIBCPROVER_CPP_OPTIONS_H
+
+#include <memory>
+
+class optionst;
+
+class api_optionst
+{
+  // Options for the verification engine
+  bool simplify_enabled;
+
+  // Private interface methods
+  api_optionst() = default;
+
+public:
+  static api_optionst create();
+
+  api_optionst &simplify(bool on);
+
+  std::unique_ptr<optionst> to_engine_options() const;
+};
+
+#endif
diff --git a/src/libcprover-cpp/readme.md b/src/libcprover-cpp/readme.md
new file mode 100644
index 00000000000..48decabee16
--- /dev/null
+++ b/src/libcprover-cpp/readme.md
@@ -0,0 +1,19 @@
+# The CPROVER C++ API
+
+This folder includes the interface and the implementation of a new C++-based
+API for the CProver libraries. This allows direct linking to key CProver functionality
+via C++ function calls. This (will eventually) allow the use of all aspects of
+the CProver verification pipeline via direct function calls and deprecate the
+need for invoking separate tools/programs.
+
+## Implementation
+
+The major part of the implementation of the API is in [`api.cpp`](src/api.cpp).
+To use the API as it stands, you need to include the header [`api.h`](src/api.h)
+in your program, and link against the resultant shared-object from the CProver
+build process (`libcprover-api.a`).
+
+## Example
+
+An example for driving the API in its current form is in the file [`call_bmc.cpp`](regression/call_bmc.cpp),
+which we are also using as a binary driver for testing the API.