From b566c4fa005c1b7a1c49d340e245387b2ad4fd52 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 7 Dec 2022 14:44:08 +0000 Subject: [PATCH 1/2] 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 --- CMakeLists.txt | 28 +++ src/libcprover-cpp/CMakeLists.txt | 19 +- src/libcprover-cpp/api.cpp | 14 +- src/libcprover-cpp/api.h | 11 +- src/libcprover-rust/.gitignore | 2 + src/libcprover-rust/Cargo.lock | 173 ++++++++++++++++++ src/libcprover-rust/Cargo.toml | 15 ++ src/libcprover-rust/build.rs | 78 ++++++++ src/libcprover-rust/include/c_api.h | 18 ++ .../include/module_dependencies.txt | 0 src/libcprover-rust/src/c_api.cc | 56 ++++++ src/libcprover-rust/src/lib.rs | 129 +++++++++++++ .../src/module_dependencies.txt | 2 + src/solvers/CMakeLists.txt | 2 + 14 files changed, 538 insertions(+), 9 deletions(-) create mode 100644 src/libcprover-rust/.gitignore create mode 100644 src/libcprover-rust/Cargo.lock create mode 100644 src/libcprover-rust/Cargo.toml create mode 100644 src/libcprover-rust/build.rs create mode 100644 src/libcprover-rust/include/c_api.h create mode 100644 src/libcprover-rust/include/module_dependencies.txt create mode 100644 src/libcprover-rust/src/c_api.cc create mode 100644 src/libcprover-rust/src/lib.rs create mode 100644 src/libcprover-rust/src/module_dependencies.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index afee139ffc6..98f5063e70c 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/src/libcprover-cpp/CMakeLists.txt b/src/libcprover-cpp/CMakeLists.txt index 7b896105b0e..ad5f10d233b 100644 --- a/src/libcprover-cpp/CMakeLists.txt +++ b/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) diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp index 68f5150f9f6..0dbbac71f45 100644 --- a/src/libcprover-cpp/api.cpp +++ b/src/libcprover-cpp/api.cpp @@ -31,6 +31,11 @@ extern configt config; +std::unique_ptr api_sessiont::get_api_version() const +{ + return util_make_unique(std::string{"0.1"}); +} + struct api_session_implementationt { std::unique_ptr model; @@ -112,13 +117,14 @@ void api_sessiont::set_message_callback( util_make_unique(callback, context); } -void api_sessiont::load_model_from_files(const std::vector &files) +void api_sessiont::load_model_from_files( + const std::vector &files) const { implementation->model = util_make_unique(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, diff --git a/src/libcprover-cpp/api.h b/src/libcprover-cpp/api.h index 24b34b44eda..ee82c84e6be 100644 --- a/src/libcprover-cpp/api.h +++ b/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 containing the filenames to be loaded - void load_model_from_files(const std::vector &files); + void load_model_from_files(const std::vector &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 get_api_version() const; private: std::unique_ptr implementation; diff --git a/src/libcprover-rust/.gitignore b/src/libcprover-rust/.gitignore new file mode 100644 index 00000000000..af69d93414d --- /dev/null +++ b/src/libcprover-rust/.gitignore @@ -0,0 +1,2 @@ +# Ignore build artefacts folder +target/ diff --git a/src/libcprover-rust/Cargo.lock b/src/libcprover-rust/Cargo.lock new file mode 100644 index 00000000000..11e7ecb19ae --- /dev/null +++ b/src/libcprover-rust/Cargo.lock @@ -0,0 +1,173 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "cc" +version = "1.0.77" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e9f73505338f7d905b19d18738976aae232eb46b8efc15554ffc56deb5d9ebe4" + +[[package]] +name = "codespan-reporting" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3538270d33cc669650c4b093848450d380def10c331d38c768e34cac80576e6e" +dependencies = [ + "termcolor", + "unicode-width", +] + +[[package]] +name = "cprover-api-rust" +version = "0.1.0" +dependencies = [ + "cxx", + "cxx-build", +] + +[[package]] +name = "cxx" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bdf07d07d6531bfcdbe9b8b739b104610c6508dcc4d63b410585faf338241daf" +dependencies = [ + "cc", + "cxxbridge-flags", + "cxxbridge-macro", + "link-cplusplus", +] + +[[package]] +name = "cxx-build" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2eb5b96ecdc99f72657332953d4d9c50135af1bac34277801cc3937906ebd39" +dependencies = [ + "cc", + "codespan-reporting", + "once_cell", + "proc-macro2", + "quote", + "scratch", + "syn", +] + +[[package]] +name = "cxxbridge-flags" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac040a39517fd1674e0f32177648334b0f4074625b5588a64519804ba0553b12" + +[[package]] +name = "cxxbridge-macro" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1362b0ddcfc4eb0a1f57b68bd77dd99f0e826958a96abd0ae9bd092e114ffed6" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "link-cplusplus" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9272ab7b96c9046fbc5bc56c06c117cb639fe2d509df0c421cad82d2915cf369" +dependencies = [ + "cc", +] + +[[package]] +name = "once_cell" +version = "1.16.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "86f0b0d4bf799edbc74508c1e8bf170ff5f41238e5f8225603ca7caaae2b7860" + +[[package]] +name = "proc-macro2" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ea3d908b0e36316caf9e9e2c4625cdde190a7e6f440d794667ed17a1855e725" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbe448f377a7d6961e30f5955f9b8d106c3f5e449d493ee1b125c1d43c2b5179" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "scratch" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8132065adcfd6e02db789d9285a0deb2f3fcb04002865ab67d5fb103533898" + +[[package]] +name = "syn" +version = "1.0.105" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "60b9b43d45702de4c839cb9b51d9f529c5dd26a4aff255b42b1ebc03e88ee908" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "termcolor" +version = "1.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "unicode-ident" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ceab39d59e4c9499d4e5a8ee0e2735b891bb7308ac83dfb4e80cad195c9f6f3" + +[[package]] +name = "unicode-width" +version = "0.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" + +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" + +[[package]] +name = "winapi-util" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178" +dependencies = [ + "winapi", +] + +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" diff --git a/src/libcprover-rust/Cargo.toml b/src/libcprover-rust/Cargo.toml new file mode 100644 index 00000000000..753beb2145a --- /dev/null +++ b/src/libcprover-rust/Cargo.toml @@ -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"] diff --git a/src/libcprover-rust/build.rs b/src/libcprover-rust/build.rs new file mode 100644 index 00000000000..d8ca42b980d --- /dev/null +++ b/src/libcprover-rust/build.rs @@ -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 { + env::current_dir() +} + +fn get_library_build_dir() -> std::io::Result { + 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"); +} diff --git a/src/libcprover-rust/include/c_api.h b/src/libcprover-rust/include/c_api.h new file mode 100644 index 00000000000..fd602799ec4 --- /dev/null +++ b/src/libcprover-rust/include/c_api.h @@ -0,0 +1,18 @@ +// Author Fotis Koutoulakis for Diffblue Ltd 2022. + +#pragma once + +#include + +// NOLINTNEXTLINE(build/include) +#include "rust/cxx.h" + +struct api_sessiont; + +// Helper function +std::vector const & +translate_vector_of_string(rust::Vec elements); + +// Exposure of the C++ object oriented API through free-standing functions. +std::unique_ptr new_api_session(); +std::vector const &get_messages(); diff --git a/src/libcprover-rust/include/module_dependencies.txt b/src/libcprover-rust/include/module_dependencies.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/src/libcprover-rust/src/c_api.cc b/src/libcprover-rust/src/c_api.cc new file mode 100644 index 00000000000..40ec6c984e1 --- /dev/null +++ b/src/libcprover-rust/src/c_api.cc @@ -0,0 +1,56 @@ +// Author Fotis Koutoulakis for Diffblue Ltd 2022. + +// NOLINTNEXTLINE(build/include) +#include "include/c_api.h" + +#include +#include + +#include + +#include +#include +#include +#include +#include +#include + +std::vector output; + +std::vector const & +translate_vector_of_string(rust::Vec elements) +{ + std::vector *stdv = new std::vector{}; + std::transform( + elements.begin(), + elements.end(), + std::back_inserter(*stdv), + [](rust::String elem) { return std::string(elem); }); + + POSTCONDITION(elements.size() == stdv->size()); + return *stdv; +} + +std::unique_ptr new_api_session() +{ + // Create a new API session and register the default API callback for that. + api_sessiont *api{new api_sessiont()}; + + // This lambda needs to be non-capturing in order for it to be convertible + // to a function pointer, to pass to the API. + const auto write_output = + [](const api_messaget &message, api_call_back_contextt context) { + std::vector &output = + *static_cast *>(context); + output.emplace_back(api_message_get_string(message)); + }; + + api->set_message_callback(write_output, &output); + + return std::unique_ptr(api); +} + +std::vector const &get_messages() +{ + return output; +} diff --git a/src/libcprover-rust/src/lib.rs b/src/libcprover-rust/src/lib.rs new file mode 100644 index 00000000000..166767feca2 --- /dev/null +++ b/src/libcprover-rust/src/lib.rs @@ -0,0 +1,129 @@ +use cxx::{CxxVector, CxxString}; +#[cxx::bridge] +pub mod ffi { + + unsafe extern "C++" { + include!("libcprover-cpp/api.h"); + include!("include/c_api.h"); + + type api_sessiont; + + // API Functions + fn new_api_session() -> UniquePtr; + fn get_api_version(&self) -> UniquePtr; + fn load_model_from_files(&self, files: &CxxVector); + fn verify_model(&self); + fn validate_goto_model(&self); + fn drop_unused_functions(&self); + + // Helper/Utility functions + fn translate_vector_of_string(elements: Vec) -> &'static CxxVector; + fn get_messages() -> &'static CxxVector; + } + + extern "Rust" { + fn print_response(vec: &CxxVector); + } +} + +fn print_response(vec: &CxxVector) { + let vec: Vec = vec + .iter() + .map(|s| s.to_string_lossy().into_owned()) + .collect(); + + for s in vec { + println!("{}", s); + } +} + +// To test run "CBMC_LIB_DIR= cargo test -- --test-threads=1 --nocapture" +#[cfg(test)] +mod tests { + use super::*; + use cxx::let_cxx_string; + + #[test] + fn it_works() { + let client = ffi::new_api_session(); + let result = client.get_api_version(); + + let_cxx_string!(expected_version = "0.1"); + assert_eq!(*result, *expected_version); + } + + #[test] + fn translate_vector_of_rust_string_to_cpp() { + let vec: Vec = vec![ + "/tmp/example.c".to_owned(), + "/tmp/example2.c".to_owned()]; + + let vect = ffi::translate_vector_of_string(vec); + assert_eq!(vect.len(), 2); + } + + #[test] + fn it_can_load_model_from_file() { + let binding = ffi::new_api_session(); + let client = match binding.as_ref() { + Some(api_ref) => api_ref, + None => panic!("Failed to acquire API session handle"), + }; + + let vec: Vec = vec![ + "/tmp/example.c".to_owned()]; + + let vect = ffi::translate_vector_of_string(vec); + assert_eq!(vect.len(), 1); + + // Invoke load_model_from_files and see if the model + // has been loaded. + client.load_model_from_files(vect); + // Validate integrity of passed goto-model. + client.validate_goto_model(); + + let msgs = ffi::get_messages(); + print_response(msgs); + } + + #[test] + fn it_can_verify_the_loaded_model() { + let client = ffi::new_api_session(); + + let vec: Vec = vec![ + "/tmp/example.c".to_owned()]; + + let vect = ffi::translate_vector_of_string(vec); + client.load_model_from_files(vect); + + // Validate integrity of goto-model + client.validate_goto_model(); + + client.verify_model(); + + let msgs = ffi::get_messages(); + print_response(msgs); + } + + #[test] + fn it_can_drop_unused_functions_from_model() { + let binding = ffi::new_api_session(); + let client = match binding.as_ref() { + Some(api_ref) => api_ref, + None => panic!("Failed to acquire API session handle"), + }; + + let vec: Vec = vec![ + "/tmp/example.c".to_owned()]; + + let vect = ffi::translate_vector_of_string(vec); + assert_eq!(vect.len(), 1); + + client.load_model_from_files(vect); + // Perform a drop of any unused functions. + client.drop_unused_functions(); + + let msgs = ffi::get_messages(); + print_response(msgs); + } +} diff --git a/src/libcprover-rust/src/module_dependencies.txt b/src/libcprover-rust/src/module_dependencies.txt new file mode 100644 index 00000000000..e1b17f561b2 --- /dev/null +++ b/src/libcprover-rust/src/module_dependencies.txt @@ -0,0 +1,2 @@ +libcprover-cpp +util diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 744def4861b..9a37ca5ce9d 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -56,6 +56,8 @@ list(REMOVE_ITEM sources ${booleforce_source} ${minibdd_source} # ${ipasir_source} + ${CMAKE_CURRENT_SOURCE_DIR}/bdd/example.cpp + ${CMAKE_CURRENT_SOURCE_DIR}/smt2/smt2_solver.cpp ) add_library(solvers ${sources}) From c2cba5b408fcd6af0ce7e77966a753822d334573 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 16 Jan 2023 11:54:41 +0000 Subject: [PATCH 2/2] Add support for building with cadical for the Rust API --- CMakeLists.txt | 2 +- src/libcprover-rust/Cargo.lock | 52 +++++++++++++++--------------- src/libcprover-rust/build.rs | 58 ++++++++++++++++++++++++++-------- 3 files changed, 72 insertions(+), 40 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 98f5063e70c..cb1cb9f0ad8 100644 --- a/CMakeLists.txt +++ b/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 diff --git a/src/libcprover-rust/Cargo.lock b/src/libcprover-rust/Cargo.lock index 11e7ecb19ae..4da6370b3cf 100644 --- a/src/libcprover-rust/Cargo.lock +++ b/src/libcprover-rust/Cargo.lock @@ -4,9 +4,9 @@ version = 3 [[package]] name = "cc" -version = "1.0.77" +version = "1.0.78" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e9f73505338f7d905b19d18738976aae232eb46b8efc15554ffc56deb5d9ebe4" +checksum = "a20104e2335ce8a659d6dd92a51a767a0c062599c73b343fd152cb401e828c3d" [[package]] name = "codespan-reporting" @@ -28,9 +28,9 @@ dependencies = [ [[package]] name = "cxx" -version = "1.0.83" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bdf07d07d6531bfcdbe9b8b739b104610c6508dcc4d63b410585faf338241daf" +checksum = "51d1075c37807dcf850c379432f0df05ba52cc30f279c5cfc43cc221ce7f8579" dependencies = [ "cc", "cxxbridge-flags", @@ -40,9 +40,9 @@ dependencies = [ [[package]] name = "cxx-build" -version = "1.0.83" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2eb5b96ecdc99f72657332953d4d9c50135af1bac34277801cc3937906ebd39" +checksum = "5044281f61b27bc598f2f6647d480aed48d2bf52d6eb0b627d84c0361b17aa70" dependencies = [ "cc", "codespan-reporting", @@ -55,15 +55,15 @@ dependencies = [ [[package]] name = "cxxbridge-flags" -version = "1.0.83" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac040a39517fd1674e0f32177648334b0f4074625b5588a64519804ba0553b12" +checksum = "61b50bc93ba22c27b0d31128d2d130a0a6b3d267ae27ef7e4fae2167dfe8781c" [[package]] name = "cxxbridge-macro" -version = "1.0.83" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1362b0ddcfc4eb0a1f57b68bd77dd99f0e826958a96abd0ae9bd092e114ffed6" +checksum = "39e61fda7e62115119469c7b3591fd913ecca96fb766cfd3f2e2502ab7bc87a5" dependencies = [ "proc-macro2", "quote", @@ -72,48 +72,48 @@ dependencies = [ [[package]] name = "link-cplusplus" -version = "1.0.7" +version = "1.0.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9272ab7b96c9046fbc5bc56c06c117cb639fe2d509df0c421cad82d2915cf369" +checksum = "ecd207c9c713c34f95a097a5b029ac2ce6010530c7b49d7fea24d977dede04f5" dependencies = [ "cc", ] [[package]] name = "once_cell" -version = "1.16.0" +version = "1.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "86f0b0d4bf799edbc74508c1e8bf170ff5f41238e5f8225603ca7caaae2b7860" +checksum = "6f61fba1741ea2b3d6a1e3178721804bb716a68a6aeba1149b5d52e3d464ea66" [[package]] name = "proc-macro2" -version = "1.0.47" +version = "1.0.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5ea3d908b0e36316caf9e9e2c4625cdde190a7e6f440d794667ed17a1855e725" +checksum = "57a8eca9f9c4ffde41714334dee777596264c7825420f521abc92b5b5deb63a5" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.21" +version = "1.0.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bbe448f377a7d6961e30f5955f9b8d106c3f5e449d493ee1b125c1d43c2b5179" +checksum = "8856d8364d252a14d474036ea1358d63c9e6965c8e5c1885c18f73d70bff9c7b" dependencies = [ "proc-macro2", ] [[package]] name = "scratch" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c8132065adcfd6e02db789d9285a0deb2f3fcb04002865ab67d5fb103533898" +checksum = "ddccb15bcce173023b3fedd9436f882a0739b8dfb45e4f6b6002bee5929f61b2" [[package]] name = "syn" -version = "1.0.105" +version = "1.0.107" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "60b9b43d45702de4c839cb9b51d9f529c5dd26a4aff255b42b1ebc03e88ee908" +checksum = "1f4064b5b16e03ae50984a5a8ed5d4f8803e6bc1fd170a3cda91a1be4b18e3f5" dependencies = [ "proc-macro2", "quote", @@ -122,18 +122,18 @@ dependencies = [ [[package]] name = "termcolor" -version = "1.1.3" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755" +checksum = "be55cf8942feac5c765c2c993422806843c9a9a45d4d5c407ad6dd2ea95eb9b6" dependencies = [ "winapi-util", ] [[package]] name = "unicode-ident" -version = "1.0.5" +version = "1.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ceab39d59e4c9499d4e5a8ee0e2735b891bb7308ac83dfb4e80cad195c9f6f3" +checksum = "84a22b9f218b40614adcb3f4ff08b703773ad44fa9423e4e0d346d5db86e4ebc" [[package]] name = "unicode-width" diff --git a/src/libcprover-rust/build.rs b/src/libcprover-rust/build.rs index d8ca42b980d..dbeea41efd1 100644 --- a/src/libcprover-rust/build.rs +++ b/src/libcprover-rust/build.rs @@ -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 { env::current_dir() } +fn get_build_directory() -> Result { + env::var("CBMC_BUILD_DIR") +} + fn get_library_build_dir() -> std::io::Result { - 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 { + 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"); }