Add support for building with cadical for the Rust API

Author: NlightNFotis

CMakeLists.txt

@@ -273,7 +273,7 @@ else()
     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_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} 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

src/libcprover-rust/Cargo.lock

@@ -1,4 +1,5 @@
 use std::env;
+use std::env::VarError;
 use std::io::{Error, ErrorKind};
 use std::path::Path;
 use std::path::PathBuf;
@@ -7,30 +8,45 @@ fn get_current_working_dir() -> std::io::Result<PathBuf> {
     env::current_dir()
 }
 
+fn get_build_directory() -> Result<String, VarError> {
+    env::var("CBMC_BUILD_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 env_var_fetch_result = get_build_directory();
+    if let Ok(build_dir) = env_var_fetch_result {
         let mut path = PathBuf::new();
-        path.push(lib_dir);
+        path.push(build_dir);
+        path.push("lib/");
         return Ok(path);
     }
-    Err(Error::new(ErrorKind::Other, "failed to get library output directory"))
+    Err(Error::new(ErrorKind::Other, "failed to get build output directory"))
 }
 
-fn get_sat_library() -> &'static str {
+fn get_cadical_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("cadical-src/build/");
+        return Ok(path);
+    }
+    Err(Error::new(ErrorKind::Other, "failed to get build output directory"))
+}
+
+fn get_sat_library() -> std::io::Result<&'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"
+            "minisat2" => Ok("minisat2-condensed"),
+            "glucose"  => Ok("glucose-condensed"),
+            "cadical"  => Ok("cadical"),
+            _          => Err(Error::new(ErrorKind::Other, "no identifiable solver detected"))
         };
         return solver_lib;
     }
-    "Error: no identifiable solver detected"
+    Err(Error::new(ErrorKind::Other, "SAT_IMPL environment variable not set"))
 }
 
 fn main() {
@@ -49,9 +65,25 @@ fn main() {
 
     let libraries_path = match get_library_build_dir() {
         Ok(path) => path,
-        Err(err) => panic!("{}", err)
+        Err(err) => panic!("Error: {}", err)
+    };
+
+    let solver_lib = match get_sat_library() {
+        Ok(solver) => solver,
+        Err(err) => panic!("Error: {}", err)
     };
 
+    // 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());
+    }
+
     println!("cargo:rustc-link-search=native={}", libraries_path.display());
     println!("cargo:rustc-link-lib=static=goto-programs");
     println!("cargo:rustc-link-lib=static=util");
@@ -72,7 +104,7 @@ fn main() {
     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={}", solver_lib);
     println!("cargo:rustc-link-lib=static=cbmc-lib");
     println!("cargo:rustc-link-lib=static=cprover-api-cpp");
 }