diff --git a/CMakeLists.txt b/CMakeLists.txt index afee139ffc6..cb1cb9f0ad8 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_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 + # 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..4da6370b3cf --- /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.78" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a20104e2335ce8a659d6dd92a51a767a0c062599c73b343fd152cb401e828c3d" + +[[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.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "51d1075c37807dcf850c379432f0df05ba52cc30f279c5cfc43cc221ce7f8579" +dependencies = [ + "cc", + "cxxbridge-flags", + "cxxbridge-macro", + "link-cplusplus", +] + +[[package]] +name = "cxx-build" +version = "1.0.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5044281f61b27bc598f2f6647d480aed48d2bf52d6eb0b627d84c0361b17aa70" +dependencies = [ + "cc", + "codespan-reporting", + "once_cell", + "proc-macro2", + "quote", + "scratch", + "syn", +] + +[[package]] +name = "cxxbridge-flags" +version = "1.0.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "61b50bc93ba22c27b0d31128d2d130a0a6b3d267ae27ef7e4fae2167dfe8781c" + +[[package]] +name = "cxxbridge-macro" +version = "1.0.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "39e61fda7e62115119469c7b3591fd913ecca96fb766cfd3f2e2502ab7bc87a5" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "link-cplusplus" +version = "1.0.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ecd207c9c713c34f95a097a5b029ac2ce6010530c7b49d7fea24d977dede04f5" +dependencies = [ + "cc", +] + +[[package]] +name = "once_cell" +version = "1.17.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f61fba1741ea2b3d6a1e3178721804bb716a68a6aeba1149b5d52e3d464ea66" + +[[package]] +name = "proc-macro2" +version = "1.0.49" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57a8eca9f9c4ffde41714334dee777596264c7825420f521abc92b5b5deb63a5" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8856d8364d252a14d474036ea1358d63c9e6965c8e5c1885c18f73d70bff9c7b" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "scratch" +version = "1.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ddccb15bcce173023b3fedd9436f882a0739b8dfb45e4f6b6002bee5929f61b2" + +[[package]] +name = "syn" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1f4064b5b16e03ae50984a5a8ed5d4f8803e6bc1fd170a3cda91a1be4b18e3f5" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "termcolor" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "be55cf8942feac5c765c2c993422806843c9a9a45d4d5c407ad6dd2ea95eb9b6" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "unicode-ident" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "84a22b9f218b40614adcb3f4ff08b703773ad44fa9423e4e0d346d5db86e4ebc" + +[[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..dbeea41efd1 --- /dev/null +++ b/src/libcprover-rust/build.rs @@ -0,0 +1,110 @@ +use std::env; +use std::env::VarError; +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_build_directory() -> Result { + env::var("CBMC_BUILD_DIR") +} + +fn get_library_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("lib/"); + return Ok(path); + } + Err(Error::new(ErrorKind::Other, "failed to get build output directory")) +} + +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" => Ok("minisat2-condensed"), + "glucose" => Ok("glucose-condensed"), + "cadical" => Ok("cadical"), + _ => Err(Error::new(ErrorKind::Other, "no identifiable solver detected")) + }; + return solver_lib; + } + Err(Error::new(ErrorKind::Other, "SAT_IMPL environment variable not set")) +} + +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!("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"); + 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={}", solver_lib); + 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})