diff --git a/src/libcprover-rust/include/c_api.h b/src/libcprover-rust/include/c_api.h index fd602799ec4..7544c85b717 100644 --- a/src/libcprover-rust/include/c_api.h +++ b/src/libcprover-rust/include/c_api.h @@ -2,6 +2,8 @@ #pragma once +#include + #include // NOLINTNEXTLINE(build/include) @@ -16,3 +18,30 @@ 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(); + +// NOLINTNEXTLINE(readability/namespace) +namespace rust +{ +// NOLINTNEXTLINE(readability/namespace) +namespace behavior +{ +template +static void trycatch(Try &&func, Fail &&fail) noexcept +{ + try + { + func(); + } + catch(const cprover_exception_baset &e) + { + fail(e.what()); + } + catch(const invariant_failedt &i) + { + fail(i.what()); + } +} + +} // namespace behavior + +} // namespace rust diff --git a/src/libcprover-rust/include/module_dependencies.txt b/src/libcprover-rust/include/module_dependencies.txt index e69de29bb2d..3759e933a83 100644 --- a/src/libcprover-rust/include/module_dependencies.txt +++ b/src/libcprover-rust/include/module_dependencies.txt @@ -0,0 +1 @@ +util diff --git a/src/libcprover-rust/src/c_api.cc b/src/libcprover-rust/src/c_api.cc index 40ec6c984e1..7dc878546ae 100644 --- a/src/libcprover-rust/src/c_api.cc +++ b/src/libcprover-rust/src/c_api.cc @@ -17,6 +17,8 @@ std::vector output; +extern bool cbmc_invariants_should_throw; + std::vector const & translate_vector_of_string(rust::Vec elements) { @@ -35,6 +37,9 @@ 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()}; + // We need to configure invariants to be throwing exceptions instead of + // reporting to stderr and calling abort() + cbmc_invariants_should_throw = true; // This lambda needs to be non-capturing in order for it to be convertible // to a function pointer, to pass to the API. diff --git a/src/libcprover-rust/src/lib.rs b/src/libcprover-rust/src/lib.rs index c871ca31166..fd7a4075196 100644 --- a/src/libcprover-rust/src/lib.rs +++ b/src/libcprover-rust/src/lib.rs @@ -11,10 +11,10 @@ pub mod ffi { // 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); + fn load_model_from_files(&self, files: &CxxVector) -> Result<()>; + fn verify_model(&self) -> Result<()>; + fn validate_goto_model(&self) -> Result<()>; + fn drop_unused_functions(&self) -> Result<()>; // Helper/Utility functions fn translate_vector_of_string(elements: Vec) -> &'static CxxVector; @@ -23,25 +23,37 @@ pub mod ffi { extern "Rust" { fn print_response(vec: &CxxVector); + fn translate_response_buffer(vec: &CxxVector) -> Vec; } } -fn print_response(vec: &CxxVector) { - let vec: Vec = vec - .iter() +/// This is a utility function, whose job is to translate the responses from the C++ +/// API (which we get in the form of a C++ std::vector) into a form that +/// can be easily consumed by other Rust programs. +pub fn translate_response_buffer(vec: &CxxVector) -> Vec { + vec.iter() .map(|s| s.to_string_lossy().into_owned()) - .collect(); + .collect() +} + +/// This is a utility function, whose aim is to simplify direct printing of the messages +/// that we get from CBMC's C++ API. Underneath, it's using translate_response_buffer +/// to translate the C++ types into Rust types and then prints out the strings contained +/// in the resultant rust vector. +pub fn print_response(vec: &CxxVector) { + let vec: Vec = translate_response_buffer(vec); for s in vec { println!("{}", s); } } -// To test run "CBMC_LIB_DIR= cargo test -- --test-threads=1 --nocapture" +// To test run "CBMC_LIB_DIR= SAT_IMPL=minisat2 cargo test -- --test-threads=1 --nocapture" #[cfg(test)] mod tests { use super::*; use cxx::let_cxx_string; + use std::process; #[test] fn it_works() { @@ -75,12 +87,28 @@ mod tests { // 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(); + if let Err(_) = client.load_model_from_files(vect) { + eprintln!("Failed to load model from files: {:?}", vect); + process::exit(1); + } + // Validate integrity of passed goto-model. + if let Err(_) = client.validate_goto_model() { + eprintln!("Failed to validate goto model from files: {:?}", vect); + process::exit(1); + } + + // ATTENTION: The following `.clone()` is unneeded - I keep it here in order to + // make potential printing of the message buffer easier (because of borrowing). + // This is also why a print instruction is commented out (as a guide for someone + // else in case they want to inspect the output). + let validation_msg = "Validating consistency of goto-model supplied to API session"; let msgs = ffi::get_messages(); - print_response(msgs); + let msgs_assert = translate_response_buffer(msgs).clone(); + + assert!(msgs_assert.contains(&String::from(validation_msg))); + + // print_response(msgs); } #[test] @@ -90,15 +118,29 @@ mod tests { let vec: Vec = vec!["other/example.c".to_owned()]; let vect = ffi::translate_vector_of_string(vec); - client.load_model_from_files(vect); + + if let Err(_) = client.load_model_from_files(vect) { + eprintln!("Failed to load model from files: {:?}", vect); + process::exit(1); + } // Validate integrity of goto-model - client.validate_goto_model(); + if let Err(_) = client.validate_goto_model() { + eprintln!("Failed to validate goto model from files: {:?}", vect); + process::exit(1); + } + + if let Err(_) = client.verify_model() { + eprintln!("Failed to verify model from files: {:?}", vect); + process::exit(1); + } - client.verify_model(); + let verification_msg = "VERIFICATION FAILED"; let msgs = ffi::get_messages(); - print_response(msgs); + let msgs_assert = translate_response_buffer(msgs).clone(); + + assert!(msgs_assert.contains(&String::from(verification_msg))); } #[test] @@ -114,11 +156,24 @@ mod tests { let vect = ffi::translate_vector_of_string(vec); assert_eq!(vect.len(), 1); - client.load_model_from_files(vect); + if let Err(_) = client.load_model_from_files(vect) { + eprintln!("Failed to load model from files: {:?}", vect); + process::exit(1); + } + // Perform a drop of any unused functions. - client.drop_unused_functions(); + if let Err(err) = client.drop_unused_functions() { + eprintln!("Error during client call: {:?}", err); + process::exit(1); + } + + let instrumentation_msg = "Performing instrumentation pass: dropping unused functions"; + let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)"; let msgs = ffi::get_messages(); - print_response(msgs); + let msgs_assert = translate_response_buffer(msgs).clone(); + + assert!(msgs_assert.contains(&String::from(instrumentation_msg))); + assert!(msgs_assert.contains(&String::from(instrumentation_msg2))); } }