Add translation of CBMC exceptions to the Rust Result type

Author: NlightNFotis

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>;
@@ -37,11 +37,12 @@ fn print_response(vec: &CxxVector<CxxString>) {
     }
 }
 
-// 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,7 +76,11 @@ mod tests {
 
         // Invoke load_model_from_files and see if the model
         // has been loaded.
-        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 passed goto-model.
         client.validate_goto_model();
 
@@ -90,12 +95,19 @@ 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();
 
-        client.verify_model();
+        if let Err(_) = client.verify_model() {
+            eprintln!("Failed to verify model from files: {:?}", vect);
+            process::exit(1);
+        }
 
         let msgs = ffi::get_messages();
         print_response(msgs);
@@ -114,10 +126,17 @@ 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);
+        }
 
+        println!("Just before we print the messages");
         let msgs = ffi::get_messages();
         print_response(msgs);
     }