Add a Rust project that exposes the C++ CProver API in Rust.

At the moment this supports the capacity for

* loading a goto_model from files
* verifying the goto_model
* performing a sample instrumentation pass

Author: NlightNFotis

CMakeLists.txt

@@ -256,4 +256,32 @@ if(WITH_JBMC)
     add_subdirectory(jbmc)
 endif()
 
+option(WITH_RUST_API "Build with the CPROVER Rust API" ON)
+if(${CMAKE_VERSION} VERSION_LESS "3.19.0")
+    message("Unable to build the Rust API without version CMake 3.19.0")
+    message("(The Rust build depends on CMake plugins with dependencies on CMake 3.19.0 and above)")
+else()
+    if(WITH_RUST_API)
+    include(FetchContent)
+
+    FetchContent_Declare(
+        Corrosion
+        GIT_REPOSITORY https://github.com/corrosion-rs/corrosion.git
+        GIT_TAG v0.3.1
+    )
+
+    FetchContent_MakeAvailable(Corrosion)
+
+    corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml)
+    corrosion_set_env_vars(cprover-api-rust CBMC_LIB_DIR=${CMAKE_LIBRARY_OUTPUT_DIRECTORY} SAT_IMPL=${sat_impl})
+    corrosion_link_libraries(cprover-api-rust cprover-api-cpp)
+    install(TARGETS cprover-api-rust RUNTIME DESTINATION lib)
+    # NOTE: We want to rename to a name consistent with the name of the
+    # rest of the static libraries built as a result of a build. The reason
+    # we cannot set the target name directly is that Cargo doesn't support
+    # hyphens in names of packages, so it builds the name by default with
+    # an underscore.
+    endif()
+endif()
+
 include(cmake/packaging.cmake)

src/libcprover-cpp/CMakeLists.txt

@@ -3,4 +3,21 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
 # This step builds the API in the form of a statically linked library (libcprover-api-cpp.a)
 add_library(cprover-api-cpp ${sources})
 generic_includes(cprover-api-cpp)
-target_link_libraries(cprover-api-cpp goto-checker goto-programs util langapi ansi-c)
+target_link_libraries(cprover-api-cpp 
+    goto-checker
+    goto-programs
+    util
+    langapi
+    ansi-c
+    json-symtab-language
+    solvers
+    xml
+    cpp
+    cbmc-lib
+    analyses
+    statement-list
+    linking
+    pointer-analysis
+    goto-instrument-lib
+    goto-analyzer-lib
+    goto-cc-lib)

src/libcprover-cpp/api.cpp

@@ -31,6 +31,11 @@
 
 extern configt config;
 
+std::unique_ptr<std::string> api_sessiont::get_api_version() const
+{
+  return util_make_unique<std::string>(std::string{"0.1"});
+}
+
 struct api_session_implementationt
 {
   std::unique_ptr<goto_modelt> model;
@@ -112,13 +117,14 @@ void api_sessiont::set_message_callback(
     util_make_unique<api_message_handlert>(callback, context);
 }
 
-void api_sessiont::load_model_from_files(const std::vector<std::string> &files)
+void api_sessiont::load_model_from_files(
+  const std::vector<std::string> &files) const
 {
   implementation->model = util_make_unique<goto_modelt>(initialize_goto_model(
     files, *implementation->message_handler, *implementation->options));
 }
 
-void api_sessiont::verify_model()
+void api_sessiont::verify_model() const
 {
   PRECONDITION(implementation->model);
 
@@ -162,7 +168,7 @@ void api_sessiont::verify_model()
   verifier.report();
 }
 
-void api_sessiont::drop_unused_functions()
+void api_sessiont::drop_unused_functions() const
 {
   INVARIANT(
     implementation->model != nullptr,
@@ -177,7 +183,7 @@ void api_sessiont::drop_unused_functions()
     *implementation->model, *implementation->message_handler);
 }
 
-void api_sessiont::validate_goto_model()
+void api_sessiont::validate_goto_model() const
 {
   INVARIANT(
     implementation->model != nullptr,

src/libcprover-cpp/api.h

@@ -66,16 +66,19 @@ struct api_sessiont
 
   /// 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);
+  void load_model_from_files(const std::vector<std::string> &files) const;
 
   /// Verify previously loaded model.
-  void verify_model();
+  void verify_model() const;
 
   /// Drop unused functions from the loaded goto_model simplifying it
-  void drop_unused_functions();
+  void drop_unused_functions() const;
 
   /// Validate the loaded goto model
-  void validate_goto_model();
+  void validate_goto_model() const;
+
+  // A simple API version information function.
+  std::unique_ptr<std::string> get_api_version() const;
 
 private:
   std::unique_ptr<api_session_implementationt> implementation;

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,78 @@
+use std::env;
+use std::io::{Error, ErrorKind};
+use std::path::Path;
+use std::path::PathBuf;
+
+fn get_current_working_dir() -> std::io::Result<PathBuf> {
+    env::current_dir()
+}
+
+fn get_library_build_dir() -> std::io::Result<PathBuf> {
+    let env_var_name = "CBMC_LIB_DIR";
+    let env_var_fetch_result = env::var(env_var_name);
+    if let Ok(lib_dir) = env_var_fetch_result {
+        let mut path = PathBuf::new();
+        path.push(lib_dir);
+        return Ok(path);
+    }
+    Err(Error::new(ErrorKind::Other, "failed to get library output directory"))
+}
+
+fn get_sat_library() -> &'static str {
+    let env_var_name = "SAT_IMPL";
+    let env_var_fetch_result = env::var(env_var_name);
+    if let Ok(sat_impl) = env_var_fetch_result {
+        let solver_lib = match sat_impl.as_str() {
+            "minisat2" => "minisat2-condensed",
+            "glucose"  => "libglucose-condensed",
+            "cadical"  => "cadical",
+            _          => "Error: no identifiable solver detected"
+        };
+        return solver_lib;
+    }
+    "Error: no identifiable solver detected"
+}
+
+fn main() {
+    let cbmc_source_path = Path::new("..");
+    let cpp_api_path = Path::new("../libcprover-cpp/");
+    let _build = cxx_build::bridge("src/lib.rs")
+        .include(cbmc_source_path)
+        .include(cpp_api_path)
+        .include(get_current_working_dir().unwrap())
+        .file("src/c_api.cc")
+        .flag_if_supported("-std=c++11")
+        .compile("cprover-rust-api");
+
+    println!("cargo:rerun-if-changed=src/c_api.cc");
+    println!("cargo:rerun-if-changed=include/c_api.h");
+
+    let libraries_path = match get_library_build_dir() {
+        Ok(path) => path,
+        Err(err) => panic!("{}", err)
+    };
+
+    println!("cargo:rustc-link-search=native={}", libraries_path.display());
+    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=analyses");
+    println!("cargo:rustc-link-lib=static=goto-instrument-lib");
+    println!("cargo:rustc-link-lib=static=big-int");
+    println!("cargo:rustc-link-lib=static=linking");
+    println!("cargo:rustc-link-lib=static=goto-checker");
+    println!("cargo:rustc-link-lib=static=solvers");
+    println!("cargo:rustc-link-lib=static=assembler");
+    println!("cargo:rustc-link-lib=static=xml");
+    println!("cargo:rustc-link-lib=static=json");
+    println!("cargo:rustc-link-lib=static=json-symtab-language");
+    println!("cargo:rustc-link-lib=static=cpp");
+    println!("cargo:rustc-link-lib=static=jsil");
+    println!("cargo:rustc-link-lib=static=statement-list");
+    println!("cargo:rustc-link-lib=static=goto-symex");
+    println!("cargo:rustc-link-lib=static=pointer-analysis");
+    println!("cargo:rustc-link-lib=static={}", get_sat_library());
+    println!("cargo:rustc-link-lib=static=cbmc-lib");
+    println!("cargo:rustc-link-lib=static=cprover-api-cpp");
+}