Include exception base classes in separate file to avoid depending on internal headers

Author: NlightNFotis

src/libcprover-rust/include/c_api.h

@@ -2,12 +2,13 @@
 
 #pragma once
 
-#include <util/exception_utils.h>
-
 #include <memory>
+#include <string>
 
 // NOLINTNEXTLINE(build/include)
 #include "rust/cxx.h"
+// NOLINTNEXTLINE(build/include)
+#include "include/c_errors.h"
 
 struct api_sessiont;
 

src/libcprover-rust/include/c_errors.h

@@ -0,0 +1,81 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd, 2023.
+
+#pragma once
+
+// The following type is cloning two types from the `util/exception_utils.h` and
+// `util/invariant.h` files.
+//
+// The reason we need to do this is as follows: We have a fundamental constraint
+// in that we don't want to export internal headers to the clients, and our
+// current build system architecture on the C++ end doesn't allow us to do so.
+//
+// At the same time, we want to allow the Rust API to be able to catch at the shim
+// level the errors generated within CBMC, which are C++ types (and subtypes of
+// those), and so because of the mechanism that cxx.rs uses, we need to have the
+// types present at compilation time (an incomplete type won't do - I've tried).
+//
+// This is the best way that we have currently to be have the type definitions
+// around so that the exception handling code knows what our exceptions look
+// like (especially given that they don't inherit from `std::exception`), so
+// that our system compiles and is functional, without needing include chains
+// outside of the API implementation (which we can't expose as well).
+
+// This should mirror the definition in `util/invariant.h`.
+class invariant_failedt
+{
+ private:
+  const std::string file;
+  const std::string function;
+  const int line;
+  const std::string backtrace;
+  const std::string condition;
+  const std::string reason;
+
+public:
+  virtual ~invariant_failedt() = default;
+
+  virtual std::string what() const noexcept;
+
+  invariant_failedt(
+    const std::string &_file,
+    const std::string &_function,
+    int _line,
+    const std::string &_backtrace,
+    const std::string &_condition,
+    const std::string &_reason)
+    : file(_file),
+      function(_function),
+      line(_line),
+      backtrace(_backtrace),
+      condition(_condition),
+      reason(_reason)
+  {
+  }
+};
+
+// This is needed here because the original definition is in the file
+// <util/exception_utils.h> which is including <util/source_location.h>, which
+// being an `irep` is a no-go for our needs as we will need to expose internal
+// headers as well. 
+class cprover_exception_baset
+{
+public:
+  /// A human readable description of what went wrong.
+  /// For readability, implementors should not add a leading
+  /// or trailing newline to this description.
+  virtual std::string what() const;
+  virtual ~cprover_exception_baset() = default;
+
+protected:
+  /// This constructor is marked protected to ensure this class isn't used
+  /// directly. Deriving classes should be used to more precisely describe the
+  /// problem that occurred.
+  explicit cprover_exception_baset(std::string reason)
+    : reason(std::move(reason))
+  {
+  }
+
+  /// The reason this exception was generated. This is the string returned by
+  /// `what()` unless that method is overridden
+  std::string reason;
+};

src/libcprover-rust/src/c_api.cc

@@ -3,10 +3,7 @@
 // NOLINTNEXTLINE(build/include)
 #include "include/c_api.h"
 
-#include <util/invariant.h>
-#include <util/make_unique.h>
-
-#include <libcprover-cpp/api.h>
+#include <cprover/api.h>
 
 #include <algorithm>
 #include <cassert>
@@ -29,7 +26,7 @@ _translate_vector_of_string(rust::Vec<rust::String> elements)
     std::back_inserter(*stdv),
     [](rust::String elem) { return std::string(elem); });
 
-  POSTCONDITION(elements.size() == stdv->size());
+  assert(elements.size() == stdv->size());
   return *stdv;
 }