Add a Rust project skeleton that uses an exposed version string from the API

Author: NlightNFotis

CMakeLists.txt

@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 3.8)
+cmake_minimum_required(VERSION 3.15)
 
 # Compile with /usr/bin/clang on MacOS
 # See https://github.com/diffblue/cbmc/issues/4956
@@ -252,4 +252,14 @@ if(WITH_JBMC)
     add_subdirectory(jbmc)
 endif()
 
+option(WITH_RUST_API "Build with the CPROVER Rust API" ON)
+if(WITH_RUST_API)
+  find_package(Corrosion REQUIRED)
+  corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml)
+  target_link_libraries(cprover-api-cpp cprover-api-rust)
+  install(TARGETS cprover-api-rust RUNTIME DESTINATION lib)
+  # TODO: cargo builds the artifact with underscores - we need to change to hyphens
+  # to bring to same naming convention as the rest of CBMC
+endif()
+
 include(cmake/packaging.cmake)

regression/CMakeLists.txt

@@ -85,7 +85,7 @@ add_subdirectory(goto-interpreter)
 add_subdirectory(cbmc-sequentialization)
 add_subdirectory(cpp-linter)
 add_subdirectory(catch-framework)
-add_subdirectory(libcprover-cpp)
+# add_subdirectory(libcprover-cpp)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)

src/libcprover-cpp/api.cpp

@@ -52,3 +52,15 @@ 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));
 }
+
+/////////////////////////////
+
+std::unique_ptr<api_sessiont> new_api_session()
+{
+  return std::unique_ptr<api_sessiont>(new api_sessiont());
+}
+
+std::unique_ptr<std::string> get_api_version(std::unique_ptr<api_sessiont> api_handle)
+{
+  return util_make_unique<std::string>(api_handle->get_api_version());
+}

src/libcprover-cpp/api.h

@@ -27,10 +27,18 @@ struct api_sessiont
   /// \param files: A vector<string> containing the filenames to be loaded
   void load_model_from_files(const std::vector<std::string> &files);
 
+  // A simple API version information function.
+  // TODO: Investigate best way to store and expose version string.
+  std::string get_api_version() const { return std::string{"0.1"}; } 
+
 private:
   std::unique_ptr<goto_modelt> model;
   std::unique_ptr<message_handlert> message_handler;
   std::unique_ptr<optionst> options;
 };
 
+// TODO: Investigate best way to define this
+std::unique_ptr<api_sessiont> new_api_session();
+std::unique_ptr<std::string> get_api_version(std::unique_ptr<api_sessiont> api_handle);
+
 #endif

src/libcprover-rust/.gitignore

@@ -0,0 +1,2 @@
+# Ignore build artefacts folder
+target/

src/libcprover-rust/Cargo.lock

@@ -0,0 +1,15 @@
+[package]
+name = "cprover-api-rust"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+cxx = "1.0"
+
+[build-dependencies]
+cxx-build = "1.0"
+
+[lib]
+crate-type = ["staticlib"]

src/libcprover-rust/Cargo.toml

@@ -0,0 +1,19 @@
+use std::path::Path;
+
+fn main() {
+    let cpp_api_path = Path::new("../libcprover-cpp");
+    println!("{}", cpp_api_path.display());
+    let _build = cxx_build::bridge("src/lib.rs")
+        .include(cpp_api_path)
+        .flag_if_supported("-std=c++11")
+        .compile("cprover-rust-api");
+
+    println!("cargo:rustc-link-search=native=/Users/fotiskoutoulakis/Devel/cbmc/build/lib/");
+    println!("cargo:rustc-link-lib=static=goto-programs");
+    println!("cargo:rustc-link-lib=static=util");
+    println!("cargo:rustc-link-lib=static=langapi");
+    println!("cargo:rustc-link-lib=static=ansi-c");
+    println!("cargo:rustc-link-lib=static=big-int");
+    println!("cargo:rustc-link-lib=static=linking");
+    println!("cargo:rustc-link-lib=static=cprover-api-cpp");
+}

src/libcprover-rust/build.rs

@@ -0,0 +1,24 @@
+#[cxx::bridge]
+pub mod ffi {
+    unsafe extern "C++" {
+        include!("api.h");
+        type api_sessiont;
+
+        fn new_api_session() -> UniquePtr<api_sessiont>;
+        fn get_api_version(api_handle: UniquePtr<api_sessiont>) -> UniquePtr<CxxString>;
+    }
+}
+
+// To test run "cargo test -- --nocapture"
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn it_works() {
+        let client = ffi::new_api_session();
+        let result = ffi::get_api_version(client);
+        println!("{}", *result);
+        // assert_eq!(*result, "0.1");
+    }
+}