Add message callback to cprover API

In order to report status updates and success / failure messages.

Author: thomasspriggs

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);