Merge pull request #7516 from NlightNFotis/rust_api_crate_preparation

Rust API crate preparation

Author: NlightNFotis

.github/workflows/pull-request-check-rust-api.yaml

@@ -52,7 +52,7 @@ jobs:
       # local experiments on the same platform, but it seems to be doing no harm to the build overall
       # and allows us to test the Rust API on Linux without issues.
       - name: Configure using CMake
-        run: cmake -S. -B${{env.default_build_dir}} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_COMPILER=/usr/bin/clang-13 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-13 -DWITH_RUST_API=ON
+        run: cmake -S. -B${{env.default_build_dir}} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_COMPILER=/usr/bin/clang-13 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-13
       - name: Build with CMake
         run: cmake --build ${{env.default_build_dir}} -j2
       - name: Print ccache stats
@@ -61,9 +61,10 @@ jobs:
       # by the other jobs already present in `pull-request-checks.yaml`.
       - name: Run Rust API tests
         run: |
+          VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))")
           cd src/libcprover-rust;\
           cargo clean;\
-          CBMC_BUILD_DIR=../../${{env.default_build_dir}} SAT_IMPL=${{env.default_solver}} cargo test -- --test-threads=1
+          CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1
 
 
   check-macos-12-cmake-clang-rust:
@@ -91,7 +92,7 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Configure using CMake
-        run: cmake -S. -B${{env.default_build_dir}} -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -DWITH_RUST_API=ON
+        run: cmake -S. -B${{env.default_build_dir}} -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++
       - name: Build with Ninja
         run: cd ${{env.default_build_dir}}; ninja -j3
       - name: Print ccache stats
@@ -100,6 +101,7 @@ jobs:
       # by the other jobs already present in `pull-request-checks.yaml`.
       - name: Run Rust API tests
         run: |
+          VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))")
           cd src/libcprover-rust;\
           cargo clean;\
-          CBMC_BUILD_DIR=../../${{env.default_build_dir}} SAT_IMPL=${{env.default_solver}} cargo test -- --test-threads=1
+          CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1

CMakeLists.txt

@@ -42,6 +42,7 @@ file(
   STRINGS src/config.inc CBMC_VERSION
   REGEX "CBMC_VERSION = (.*)")
 string(REGEX REPLACE "CBMC_VERSION = (.*)" "\\1" CBMC_VERSION ${CBMC_VERSION})
+message(STATUS "Building CBMC version ${CBMC_VERSION}")
 
 project(CBMC VERSION ${CBMC_VERSION})
 
@@ -256,33 +257,4 @@ if(WITH_JBMC)
     add_subdirectory(jbmc)
 endif()
 
-option(WITH_RUST_API "Build with the CPROVER Rust API" OFF)
-if(${CMAKE_VERSION} VERSION_LESS "3.19.0" AND WITH_RUST_API)
-    message("Unable to build the Rust API without version CMake 3.19.0")
-    message(FATAL_ERROR "(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)
-    list(JOIN sat_impl " " sat_impl_str)
-    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} "SAT_IMPL=${sat_impl_str}")
-    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-rust/Cargo.lock

@@ -1,7 +1,12 @@
 [package]
-name = "cprover-api-rust"
+name = "libcprover_rust"
 version = "0.1.0"
 edition = "2021"
+description = "Rust API for CBMC and assorted CProver tools"
+repository = "https://github.com/diffblue/cbmc"
+documentation = "https://diffblue.github.io/cbmc/"
+license = "BSD-4-Clause"
+exclude = ["other/", "module_dependencies.txt"]
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
@@ -12,4 +17,4 @@ cxx = "1.0"
 cxx-build = "1.0"
 
 [lib]
-crate-type = ["staticlib"]
+crate-type = ["rlib"]

src/libcprover-rust/Cargo.toml

@@ -8,62 +8,30 @@ fn get_current_working_dir() -> std::io::Result<PathBuf> {
     env::current_dir()
 }
 
-fn get_build_directory() -> Result<String, VarError> {
-    env::var("CBMC_BUILD_DIR")
+// Passed by the top-level CMakeLists.txt to control which version of the
+// static library of CBMC we're linking against. A user can also change the
+// environment variable to link against different versions of CBMC.
+fn get_cbmc_version() -> Result<String, VarError> {
+    env::var("CBMC_VERSION")
 }
 
-fn get_library_build_dir() -> std::io::Result<PathBuf> {
-    let env_var_fetch_result = get_build_directory();
-    if let Ok(build_dir) = env_var_fetch_result {
-        let mut path = PathBuf::new();
-        path.push(build_dir);
-        path.push("lib/");
-        return Ok(path);
-    }
-    Err(Error::new(
-        ErrorKind::Other,
-        "failed to get build output directory",
-    ))
+// Passed by the top-level CMakeLists.txt to control where the static library we
+// link against is located. A user can also change the location of the library
+// on their system by supplying the environment variable themselves.
+fn get_lib_directory() -> Result<String, VarError> {
+    env::var("CBMC_LIB_DIR")
 }
 
-fn get_cadical_build_dir() -> std::io::Result<PathBuf> {
-    let env_var_fetch_result = get_build_directory();
+fn get_library_build_dir() -> std::io::Result<PathBuf> {
+    let env_var_fetch_result = get_lib_directory();
     if let Ok(build_dir) = env_var_fetch_result {
         let mut path = PathBuf::new();
         path.push(build_dir);
-        path.push("cadical-src/build/");
         return Ok(path);
     }
     Err(Error::new(
         ErrorKind::Other,
-        "failed to get build output directory",
-    ))
-}
-
-fn get_sat_libraries() -> std::io::Result<Vec<&'static str>> {
-    let env_var_name = "SAT_IMPL";
-    let env_var_fetch_result = env::var(env_var_name);
-    if let Ok(sat_impls) = env_var_fetch_result {
-        let mut solver_libs = Vec::new();
-        for sat_impl in sat_impls.split(" ") {
-            let solver_lib = match sat_impl {
-                "minisat2" => "minisat2-condensed",
-                "glucose" => "glucose-condensed",
-                "cadical" => "cadical",
-                _ => {
-                    return Err(Error::new(
-                        ErrorKind::Other,
-                        "no identifiable solver detected",
-                    ))
-                }
-            };
-            solver_libs.push(solver_lib);
-        }
-        return Ok(solver_libs);
-    }
-    Err(Error::new(
-        ErrorKind::Other,
-        "SAT_IMPL environment variable not set",
+        "Environment variable `CBMC_LIB_DIR' not set",
     ))
 }
 
@@ -83,34 +51,32 @@ fn main() {
 
     let libraries_path = match get_library_build_dir() {
         Ok(path) => path,
-        Err(err) => panic!("Error: {}", err),
-    };
-
-    let solver_libs = match get_sat_libraries() {
-        Ok(solvers) => solvers,
-        Err(err) => panic!("Error: {}", err),
-    };
-
-    for solver_lib in solver_libs.iter() {
-        // Cadical is being built in its own directory, with the resultant artefacts being
-        // present only there. Hence, we need to instruct cargo to look for them in cadical's
-        // build directory, otherwise we're going to get build errors.
-        if *solver_lib == "cadical" {
-            let cadical_build_dir = match get_cadical_build_dir() {
-                Ok(cadical_directory) => cadical_directory,
-                Err(err) => panic!("Error: {}", err),
-            };
-            println!(
-                "cargo:rustc-link-search=native={}",
-                cadical_build_dir.display()
+        Err(err) => {
+            let error_message = &format!(
+                "Error: {}.\n Advice: {}.",
+                err,
+                "Please set the environment variable `CBMC_LIB_DIR' with the path that contains libcprover.x.y.z.a on your system"
             );
+            panic!("{}", error_message);
         }
-    }
+    };
 
     println!(
         "cargo:rustc-link-search=native={}",
         libraries_path.display()
     );
 
-    println!("cargo:rustc-link-lib=static=cprover.5.78.0");
+    let cprover_static_libname = match get_cbmc_version() {
+        Ok(version) => String::from("cprover.") + &version,
+        Err(_) => {
+            let error_message = &format!(
+                "Error: {}.\n Advice: {}.",
+                "Environment variable `CBMC_VERSION' not set",
+                "Please set the environment variable `CBMC_VERSION' with the version of CBMC you want to link against (e.g. 5.78.0)"
+            );
+            panic!("{}", error_message);
+        }
+    };
+
+    println!("cargo:rustc-link-lib=static={}", cprover_static_libname);
 }

src/libcprover-rust/build.rs

@@ -0,0 +1,48 @@
+# CProver (CBMC) Rust API
+
+This folder contains the implementation of the Rust API of the CProver (CBMC) project.
+
+## Building instructions
+
+To build the Rust project you need the Rust language toolchain installed
+(you can install from [rustup.rs](https://rustup.rs)).
+
+With that instaled, you can execute `cargo build` under this (`src/libcprover-rust`)
+directory.
+
+For this to work, you need to supply two environment variables to the
+project:
+
+* `CBMC_LIB_DIR`, for selecting where the `libcprover-x.y.z.a` is located
+  (say, if you have downloaded a pre-packaged release which contains
+   the static library), and
+* `CBMC_VERSION`, for selecting the version of the library to link against
+  (this is useful if you have multiple versions of the library in the same
+   location and you want to control which version you compile against).
+
+As an example, a command sequence to build the API through `cargo` would look
+like this (assuming you're executing these instructions from the root level
+directory of the CBMC project.)
+
+```sh
+$ cd src/libcprover-rust
+$ cargo clean
+$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
+```
+
+To build the project and run its associated tests, the command sequence would
+look like this:
+
+```sh
+$ cd src/libcprover-rust
+$ cargo clean
+$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture
+```
+
+## Notes
+
+* The functions supported by the Rust API are catalogued within the `ffi` module within
+  `lib.rs`.
+* The API supports exception handling from inside CBMC by catching the exceptions in
+  a C++ shim, and then translating the exception into the Rust `Result` type.
+* Because of limitations from the C++ side of CBMC, the API is not thread-safe.

src/libcprover-rust/readme.md

@@ -1,4 +1,5 @@
 use cxx::{CxxString, CxxVector};
+
 #[cxx::bridge]
 pub mod ffi {