Expose version string from C++ to Rust through CXX.rs

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
@@ -254,4 +254,16 @@ 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 cprover-rust-api/Cargo.toml)
+
+  target_link_libraries(cprover-api cprover-rust-api)
+  install(TARGETS cprover-rust-api 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)

cprover-cpp-api/src/api.cpp

@@ -49,3 +49,13 @@ void cprover_api::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<cprover_api> new_cprover_api()
+{
+  return std::unique_ptr<cprover_api>(new cprover_api());
+}
+
+std::unique_ptr<std::string> get_api_version(std::unique_ptr<cprover_api> api_handle)
+{
+  return util_make_unique<std::string>(api_handle->get_api_version());
+}

cprover-cpp-api/src/api.h

@@ -29,12 +29,16 @@ struct cprover_api
 
   // A simple API version information function.
   // TODO: Investigate best way to store and expose version string.
-  std::string get_api_version() { return std::string{"0.1"}; }
+  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<cprover_api> new_cprover_api();
+std::unique_ptr<std::string> get_api_version(std::unique_ptr<cprover_api> api_handle);
+
 #endif

cprover-rust-api/.gitgnore

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

cprover-rust-api/.gitignore

@@ -6,3 +6,10 @@ 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"]

cprover-rust-api/Cargo.lock

@@ -0,0 +1,20 @@
+use std::path::Path;
+
+fn main() {
+    let cpp_api_path = Path::new("../cprover-cpp-api/src");
+    println!("{}", cpp_api_path.display());
+    let _build = cxx_build::bridge("src/lib.rs")
+        // .file("target/cxxbridge/cprover-rust-api/src/lib.rs.cc")
+        .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");
+}

cprover-rust-api/Cargo.toml

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