Add first version of a C++ API for CBMC.

NlightNFotis · NlightNFotis · commit d0ab60c52a56 · 2022-12-06T18:12:28.000Z
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`.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,4 @@
+ansi-c
+langapi
+goto-programs
+util
diff --git a/src/libcprover-cpp/options.cpp 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
@@ -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
@@ -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.

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+add_test_pl_tests(`
	`2`	`+ "$<TARGET_FILE:api-binary-driver>"`
	`3`	`+)`