Translate exceptions from C++ API into Rust Result types.

src/libcprover-rust/include/c_api.h

@@ -2,6 +2,8 @@
 
 #pragma once
 
+#include <util/exception_utils.h>
+
 #include <memory>
 
 // NOLINTNEXTLINE(build/include)
@@ -16,3 +18,30 @@ translate_vector_of_string(rust::Vec<rust::String> elements);
 // Exposure of the C++ object oriented API through free-standing functions.
 std::unique_ptr<api_sessiont> new_api_session();
 std::vector<std::string> const &get_messages();
+
+// NOLINTNEXTLINE(readability/namespace)
+namespace rust
+{
+// NOLINTNEXTLINE(readability/namespace)
+namespace behavior
+{
+template <typename Try, typename Fail>
+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

src/libcprover-rust/include/module_dependencies.txt

@@ -0,0 +1 @@
+util

src/libcprover-rust/src/c_api.cc

@@ -17,6 +17,8 @@
 
 std::vector<std::string> output;
 
+extern bool cbmc_invariants_should_throw;
+
 std::vector<std::string> const &
 translate_vector_of_string(rust::Vec<rust::String> elements)
 {
@@ -35,6 +37,9 @@ std::unique_ptr<api_sessiont> 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.

src/libcprover-rust/src/lib.rs

@@ -11,10 +11,10 @@ pub mod ffi {
         // API Functions
         fn new_api_session() -> UniquePtr<api_sessiont>;
         fn get_api_version(&self) -> UniquePtr<CxxString>;
-        fn load_model_from_files(&self, files: &CxxVector<CxxString>);
-        fn verify_model(&self);
-        fn validate_goto_model(&self);
-        fn drop_unused_functions(&self);
+        fn load_model_from_files(&self, files: &CxxVector<CxxString>) -> 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<String>) -> &'static CxxVector<CxxString>;
@@ -23,25 +23,37 @@ pub mod ffi {
 
     extern "Rust" {
         fn print_response(vec: &CxxVector<CxxString>);
+        fn translate_response_buffer(vec: &CxxVector<CxxString>) -> Vec<String>;
     }
 }
 
-fn print_response(vec: &CxxVector<CxxString>) {
-    let vec: Vec<String> = 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<std:string>) into a form that
+/// can be easily consumed by other Rust programs.
+pub fn translate_response_buffer(vec: &CxxVector<CxxString>) -> Vec<String> {
+    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<CxxString>) {
+    let vec: Vec<String> = translate_response_buffer(vec);
 
     for s in vec {
         println!("{}", s);
     }
 }
 
-// To test run "CBMC_LIB_DIR=<path_to_build/libs> cargo test -- --test-threads=1 --nocapture"
+// To test run "CBMC_LIB_DIR=<path_to_build/libs> 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<String> = 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)));
     }
 }