Merge pull request #7437 from thomasspriggs/tas/api_messages

Add call back system for reporting messages through the API

Author: thomasspriggs

CMakeLists.txt

@@ -240,6 +240,7 @@ cprover_default_properties(
     json
     json-symtab-language
     langapi
+    lib-unit
     linking
     pointer-analysis
     solvers

regression/libcprover-cpp/call_bmc.cpp

@@ -9,6 +9,13 @@
 #include <iostream>
 #include <vector>
 
+void print_messages_to_stdout(
+  const api_messaget &message,
+  api_call_back_contextt)
+{
+  std::cout << api_message_get_string(message) << std::endl;
+}
+
 int main(int argc, char *argv[])
 {
   try
@@ -25,6 +32,7 @@ int main(int argc, char *argv[])
     api_sessiont api(api_options);
 
     // Demonstrate the loading of a goto-model from the command line arguments
+    api.set_message_callback(print_messages_to_stdout, nullptr);
     api.load_model_from_files(arguments);
 
     std::cout << "Successfully initialised goto_model" << std::endl;

regression/libcprover-cpp/model_loading/load_basic_c_file/test.desc

@@ -3,6 +3,10 @@ test.c
 
 ^EXIT=0$
 ^SIGNAL=0$
+Parsing test.c
+Converting
+Type\-checking test
+Generating GOTO Program
 Successfully initialised goto_model
 --
 --

src/libcprover-cpp/api.cpp

@@ -46,6 +46,60 @@ api_sessiont::api_sessiont(const api_optionst &options)
 
 api_sessiont::~api_sessiont() = default;
 
+struct api_messaget
+{
+  std::string string;
+};
+
+const char *api_message_get_string(const api_messaget &message)
+{
+  return message.string.c_str();
+}
+
+class api_message_handlert : public message_handlert
+{
+public:
+  explicit api_message_handlert(
+    api_message_callbackt callback,
+    api_call_back_contextt context);
+
+  void print(unsigned level, const std::string &message) override;
+
+  // Unimplemented for now. We may need to implement these as string conversions
+  // or something later.
+  void print(unsigned level, const xmlt &xml) override{};
+  void print(unsigned level, const jsont &json) override{};
+
+  void flush(unsigned) override{};
+
+private:
+  api_call_back_contextt context;
+  api_message_callbackt callback;
+};
+
+api_message_handlert::api_message_handlert(
+  api_message_callbackt callback,
+  api_call_back_contextt context)
+  : message_handlert{}, context{context}, callback{callback}
+{
+}
+
+void api_message_handlert::print(unsigned level, const std::string &message)
+{
+  if(!callback)
+    return;
+  api_messaget api_message{message};
+  callback(api_message, context);
+}
+
+void api_sessiont::set_message_callback(
+  api_message_callbackt callback,
+  api_call_back_contextt context)
+{
+  implementation->message_handler =
+    util_make_unique<api_message_handlert>(callback, context);
+}
+
 void api_sessiont::load_model_from_files(const std::vector<std::string> &files)
 {
   implementation->model = util_make_unique<goto_modelt>(initialize_goto_model(

src/libcprover-cpp/api.h

@@ -19,6 +19,34 @@ struct api_session_implementationt;
 
 #include "options.h" // IWYU pragma: keep
 
+/// Opaque message type. Properties of messages to be fetched through further
+/// api calls.
+struct api_messaget;
+
+/// Given a \p api_message, this function returns that message expressed as a
+/// C language string.
+/// \note The memory for the returned string is owned by the message and as such
+/// does not need to be freed by users of the API.
+const char *api_message_get_string(const api_messaget &message);
+
+/// The type of pointers to contextual data passed to the api_message_callback
+/// functions. These pointers point to api consumer data and are just passed
+/// through to the callback verbatim. These support users of the api to avoid
+/// using global variables.
+using api_call_back_contextt = void *;
+
+/// The type of call back for feedback of status information and results.
+/// \param message: A structured message object. The lifetime of this object is
+///   the duration of the call to the callback. So if any data from it is
+///   required to persist, then this data must be copied into the API consumers
+///   memory.
+/// \param call_back_context: A pointer to the context for the function. This
+///   is passed through the API to the function and is for use like a capture
+///   group. Memory for this object is owned by the consumer of the API.
+using api_message_callbackt = void (*)(
+  const api_messaget &message,
+  api_call_back_contextt call_back_context);
+
 // 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
@@ -28,6 +56,14 @@ struct api_sessiont
   explicit api_sessiont(const api_optionst &options);
   ~api_sessiont(); // default constructed in the .cpp file
 
+  /// \param callback: A call back function to receive progress updates and
+  ///                  success/failure statuses.
+  /// \param context: A context pointer passed through to the callback function.
+  ///                 This is used similarly to a capture in a lambda function.
+  void set_message_callback(
+    api_message_callbackt callback,
+    api_call_back_contextt context);
+
   /// 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);

unit/CMakeLists.txt

@@ -12,6 +12,7 @@ endif()
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 
 file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
+file(GLOB_RECURSE libcprover_sources "libcprover-cpp/*.cpp" "libcprover-cpp/*.h")
 
 if(NOT WITH_MEMORY_ANALYZER)
     file(GLOB_RECURSE memory_analyzer_sources "memory-analyzer/*.cpp")
@@ -62,9 +63,13 @@ list(REMOVE_ITEM sources
 
     # Intended to fail to compile
     ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
+
+    # Built into separate binary
+    ${libcprover_sources}
 )
 
 add_subdirectory(testing-utils)
+add_subdirectory(libcprover-cpp)
 
 add_executable(unit ${sources})
 target_include_directories(unit

unit/count_tests.py

@@ -56,6 +56,9 @@ def tests_in_file(file_path):
 def count_tests_in_directory(directory_path, exclude_files):
     test_count = 0
     for root, sub_directories, files in os.walk("."):
+        # Excluded from count as built into separate binary.
+        if root.endswith("libcprover-cpp"):
+            continue
         for file_name in files:
             if any(file_name == excluded_file for excluded_file in exclude_files):
                 continue

unit/libcprover-cpp/CMakeLists.txt

@@ -0,0 +1,19 @@
+
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+
+add_executable(lib-unit ${sources})
+target_include_directories(lib-unit
+    PUBLIC
+    ${CBMC_SOURCE_DIR}/libcprover-cpp
+)
+target_link_libraries(lib-unit
+    cprover-api-cpp
+)
+
+add_test(
+    NAME lib-unit
+    COMMAND $<TARGET_FILE:lib-unit>
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
+set_tests_properties(lib-unit PROPERTIES LABELS "CORE;CBMC")

unit/libcprover-cpp/api.cpp

@@ -0,0 +1,88 @@
+// Author: Diffblue Ltd.
+
+// Note that this test should not include any headers which are internal to
+// cbmc. API headers (and STL/catch) should be included only. This is in order
+// to confirm that the API can be used without reference to cmbc internals.
+
+#include <libcprover-cpp/api.h>
+
+#include <algorithm>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "../catch/catch.hpp"
+
+class contains_in_ordert final
+  : public Catch::MatcherBase<std::vector<std::string>>
+{
+public:
+  contains_in_ordert(std::initializer_list<std::string> expected);
+  bool match(const std::vector<std::string> &actual) const override;
+
+protected:
+  std::string describe() const override;
+
+private:
+  std::vector<std::string> expected;
+};
+
+contains_in_ordert::contains_in_ordert(
+  std::initializer_list<std::string> expected)
+  : expected{
+      std::make_move_iterator(expected.begin()),
+      std::make_move_iterator(expected.end())}
+{
+}
+
+bool contains_in_ordert::match(const std::vector<std::string> &actual) const
+{
+  auto begin_search = actual.begin();
+  for(const auto &expected_item : expected)
+  {
+    auto find_result = std::find(begin_search, actual.end(), expected_item);
+    if(find_result == actual.end())
+      return false;
+    else
+      begin_search = ++find_result;
+  }
+  return true;
+}
+
+std::string contains_in_ordert::describe() const
+{
+  std::stringstream description;
+  description << "contains these strings in order ";
+  description << '"' << *expected.begin() << '"';
+  for(auto iterator = std::next(expected.begin()); iterator != expected.end();
+      ++iterator)
+  {
+    description << ", \"" << *iterator << '"';
+  }
+  return description.str();
+}
+
+TEST_CASE("Test loading model from file.", "[core][libcprover-cpp]")
+{
+  api_sessiont api(api_optionst::create());
+
+  std::vector<std::string> output;
+  // This lambda needs to be non-capturing in order for it to be convertible
+  // to a function pointer, to pass to the API.
+  const auto write_output =
+    [](const api_messaget &message, api_call_back_contextt context) {
+      std::vector<std::string> &output =
+        *static_cast<std::vector<std::string> *>(context);
+      output.emplace_back(api_message_get_string(message));
+    };
+
+  api.set_message_callback(write_output, &output);
+  api.load_model_from_files({"test.c"});
+  CHECK_THAT(
+    output,
+    (contains_in_ordert{
+      "Parsing test.c",
+      "Converting",
+      "Type-checking test",
+      "Generating GOTO Program"}));
+}

unit/libcprover-cpp/lib_unit_tests.cpp

@@ -0,0 +1,4 @@
+// Author: Diffblue Ltd.
+
+#define CATCH_CONFIG_MAIN
+#include "../catch/catch.hpp"

unit/libcprover-cpp/module_dependencies.txt

@@ -0,0 +1,2 @@
+../catch
+libcprover-cpp

unit/libcprover-cpp/test.c

@@ -0,0 +1,9 @@
+// Input file to test reading through API, not for compiling!
+
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int a[] = {0, 1, 2, 3, 4};
+  assert(a[4] != 4);
+}