Merge pull request #7600 from NlightNFotis/rust_doc_enhancements

Enhance documentation for functions and modules of the Rust API

Author: NlightNFotis

src/libcprover-rust/Cargo.toml

@@ -18,3 +18,4 @@ cxx-build = "1.0"
 
 [lib]
 crate-type = ["rlib"]
+doctest = false

src/libcprover-rust/build.rs

@@ -8,16 +8,18 @@ fn get_current_working_dir() -> std::io::Result<PathBuf> {
     env::current_dir()
 }
 
-// Passed by the top-level CMakeLists.txt to control which version of the
-// static library of CBMC we're linking against. A user can also change the
-// environment variable to link against different versions of CBMC.
+// Initially passed by the top-level CMakeLists.txt to control which version
+// of the static library of CBMC we were linking against. Staying in order to
+// allow users to be able to easily change the version of the CBMC static
+// library that's being looked up.
 fn get_cbmc_version() -> Result<String, VarError> {
     env::var("CBMC_VERSION")
 }
 
-// Passed by the top-level CMakeLists.txt to control where the static library we
-// link against is located. A user can also change the location of the library
-// on their system by supplying the environment variable themselves.
+// Initially passed by the top-level CMakeLists.txt to control where the static
+// library we link against was located. Now staying for backward compatibility of
+// the build system, and to allow fine grained control for a user as to where the
+// static library is located (be it in a build folder or a system `/lib` folder).
 fn get_lib_directory() -> Result<String, VarError> {
     env::var("CBMC_LIB_DIR")
 }

src/libcprover-rust/include/c_api.h

@@ -13,7 +13,7 @@ struct api_sessiont;
 
 // Helper function
 std::vector<std::string> const &
-translate_vector_of_string(rust::Vec<rust::String> elements);
+_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();

src/libcprover-rust/src/c_api.cc

@@ -20,7 +20,7 @@ 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)
+_translate_vector_of_string(rust::Vec<rust::String> elements)
 {
   std::vector<std::string> *stdv = new std::vector<std::string>{};
   std::transform(

src/libcprover-rust/src/lib.rs

@@ -1,55 +1,83 @@
-use cxx::{CxxString, CxxVector};
+#![doc = include_str!("../tutorial.md")]
+#![warn(missing_docs)]
 
+/// The main API module for interfacing with CProver tools (`cbmc`, `goto-analyzer`, etc).
 #[cxx::bridge]
-pub mod ffi {
+pub mod cprover_api {
 
     unsafe extern "C++" {
         include!("libcprover-cpp/api.h");
         include!("include/c_api.h");
 
+        /// Central organisational handle of the API. This directly corresponds to the
+        /// C++-API type `api_sessiont`. To initiate a session interaction, call [new_api_session].
         type api_sessiont;
 
-        // API Functions
+        /// Provide a unique pointer to the API handle. This will be required to interact
+        /// with the API calls, and thus, is expected to be the first call before any other
+        /// interaction with the API.
         fn new_api_session() -> UniquePtr<api_sessiont>;
+
+        /// Return the API version - note that this is coming from the C++ API, which
+        /// returns the API version of CBMC (which should map to the version of `libcprover.a`)
+        /// the Rust API has mapped against.
         fn get_api_version(&self) -> UniquePtr<CxxString>;
+        /// Provided a C++ Vector of Strings (use [translate_vector_of_string] to translate
+        /// a Rust `Vec<String` into a `CxxVector<CxxString>` before passing it to the function),
+        /// load the models from the files in the vector and link them together.
         fn load_model_from_files(&self, files: &CxxVector<CxxString>) -> Result<()>;
+        /// Execute a verification engine run against the loaded model.
+        /// *ATTENTION*: A model must be loaded before this function is run.
         fn verify_model(&self) -> Result<()>;
+        /// Run a validation check on the goto-model that has been loaded.
+        /// Corresponds to the CProver CLI option `--validate-goto-model`.
         fn validate_goto_model(&self) -> Result<()>;
+        /// Drop functions that aren't used from the model. Corresponds to
+        /// the CProver CLI option `--drop-unused-functions`
         fn drop_unused_functions(&self) -> Result<()>;
 
-        // Helper/Utility functions
-        fn translate_vector_of_string(elements: Vec<String>) -> &'static CxxVector<CxxString>;
+        // WARNING: Please don't use this function - use its public interface in [ffi_util::translate_rust_vector_to_cpp].
+        // The reason this is here is that it's implemented on the C++ shim, and to link this function against
+        // its implementation it needs to be declared within the `unsafe extern "C++"` block of the FFI bridge.
+        #[doc(hidden)]
+        fn _translate_vector_of_string(elements: Vec<String>) -> &'static CxxVector<CxxString>;
+        /// Print messages accumulated into the message buffer from CProver's end.
         fn get_messages() -> &'static CxxVector<CxxString>;
     }
-
-    extern "Rust" {
-        fn print_response(vec: &CxxVector<CxxString>);
-        fn translate_response_buffer(vec: &CxxVector<CxxString>) -> Vec<String>;
-    }
 }
 
-/// 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()
-}
+/// Module containing utility functions for translating between types across
+/// the FFI boundary.
+pub mod ffi_util {
+    use crate::cprover_api::_translate_vector_of_string;
+    use cxx::CxxString;
+    use cxx::CxxVector;
+
+    /// This function translates the responses from the C++ API (which we get in the
+    /// form of a C++ std::vector<std:string>) into the equivalent Rust type `Vec<String>`.
+    /// Dual to [translate_rust_vector_to_cpp].
+    pub fn translate_cpp_vector_to_rust(vec: &CxxVector<CxxString>) -> Vec<String> {
+        vec.iter()
+            .map(|s| s.to_string_lossy().into_owned())
+            .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);
+    /// This function aims to simplify direct printing of the messages that we get
+    /// from CBMC's C++ API.
+    pub fn print_response(vec: &Vec<String>) {
+        for s in vec {
+            println!("{}", s);
+        }
+    }
 
-    for s in vec {
-        println!("{}", s);
+    /// Translate a Rust `Vec<String>` into a C++ acceptable `std::vector<std::string>`.
+    /// Dual to [translate_cpp_vector_to_rust].
+    pub fn translate_rust_vector_to_cpp(elements: Vec<String>) -> &'static CxxVector<CxxString> {
+        _translate_vector_of_string(elements)
     }
 }
 
-// To test run "CBMC_LIB_DIR=<path_to_build/libs> SAT_IMPL=minisat2 cargo test -- --test-threads=1 --nocapture"
+// To test run "CBMC_LIB_DIR=<path_to_build/libs> CBMC_VERSION=<version> cargo test -- --test-threads=1 --nocapture"
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -58,7 +86,7 @@ mod tests {
 
     #[test]
     fn it_works() {
-        let client = ffi::new_api_session();
+        let client = cprover_api::new_api_session();
         let result = client.get_api_version();
 
         let_cxx_string!(expected_version = "0.1");
@@ -69,21 +97,21 @@ mod tests {
     fn translate_vector_of_rust_string_to_cpp() {
         let vec: Vec<String> = vec!["other/example.c".to_owned(), "/tmp/example2.c".to_owned()];
 
-        let vect = ffi::translate_vector_of_string(vec);
+        let vect = ffi_util::translate_rust_vector_to_cpp(vec);
         assert_eq!(vect.len(), 2);
     }
 
     #[test]
     fn it_can_load_model_from_file() {
-        let binding = ffi::new_api_session();
+        let binding = cprover_api::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<String> = vec!["other/example.c".to_owned()];
 
-        let vect = ffi::translate_vector_of_string(vec);
+        let vect = ffi_util::translate_rust_vector_to_cpp(vec);
         assert_eq!(vect.len(), 1);
 
         // Invoke load_model_from_files and see if the model
@@ -104,21 +132,21 @@ mod tests {
         // 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();
-        let msgs_assert = translate_response_buffer(msgs).clone();
+        let msgs = cprover_api::get_messages();
+        let msgs_assert = ffi_util::translate_cpp_vector_to_rust(msgs).clone();
 
         assert!(msgs_assert.contains(&String::from(validation_msg)));
 
-        // print_response(msgs);
+        // ffi_util::print_response(msgs_assert);
     }
 
     #[test]
     fn it_can_verify_the_loaded_model() {
-        let client = ffi::new_api_session();
+        let client = cprover_api::new_api_session();
 
         let vec: Vec<String> = vec!["other/example.c".to_owned()];
 
-        let vect = ffi::translate_vector_of_string(vec);
+        let vect = ffi_util::translate_rust_vector_to_cpp(vec);
 
         if let Err(_) = client.load_model_from_files(vect) {
             eprintln!("Failed to load model from files: {:?}", vect);
@@ -138,23 +166,23 @@ mod tests {
 
         let verification_msg = "VERIFICATION FAILED";
 
-        let msgs = ffi::get_messages();
-        let msgs_assert = translate_response_buffer(msgs).clone();
+        let msgs = cprover_api::get_messages();
+        let msgs_assert = ffi_util::translate_cpp_vector_to_rust(msgs).clone();
 
         assert!(msgs_assert.contains(&String::from(verification_msg)));
     }
 
     #[test]
     fn it_can_drop_unused_functions_from_model() {
-        let binding = ffi::new_api_session();
+        let binding = cprover_api::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<String> = vec!["other/example.c".to_owned()];
 
-        let vect = ffi::translate_vector_of_string(vec);
+        let vect = ffi_util::translate_rust_vector_to_cpp(vec);
         assert_eq!(vect.len(), 1);
 
         if let Err(_) = client.load_model_from_files(vect) {
@@ -171,8 +199,8 @@ mod tests {
         let instrumentation_msg = "Performing instrumentation pass: dropping unused functions";
         let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)";
 
-        let msgs = ffi::get_messages();
-        let msgs_assert = translate_response_buffer(msgs).clone();
+        let msgs = cprover_api::get_messages();
+        let msgs_assert = ffi_util::translate_cpp_vector_to_rust(msgs).clone();
 
         assert!(msgs_assert.contains(&String::from(instrumentation_msg)));
         assert!(msgs_assert.contains(&String::from(instrumentation_msg2)));

src/libcprover-rust/tutorial.md

@@ -0,0 +1,114 @@
+# Libcprover-rust
+
+A Rust interface for convenient interaction with the CProver tools.
+
+## Basic Usage
+
+This file will guide through a sample interaction with the API, under a basic
+scenario: *loading a file and verifying the model contained within*.
+
+To begin, we will assume that you have a file under `/tmp/api_example.c`,
+with the following contents:
+
+```c
+int main(int argc, char *argv[])
+{
+  int arr[] = {0, 1, 2, 3};
+  __CPROVER_assert(arr[3] != 3, "expected failure: arr[3] == 3");
+}
+```
+
+The first thing we need to do to initiate any interaction with the API
+itself is to create a new `api_sessiont` handle by using the function
+`new_api_session`:
+
+```rust
+let client = cprover_api::new_api_session();
+```
+
+Then, we need to add the file to a vector with filenames that indicate
+which files we want the verification engine to load the models of:
+
+```rust
+let vec: Vec<String> = vec!["/tmp/api_example.c".to_owned()];
+
+let vect = ffi_util::translate_rust_vector_to_cpp(vec);
+```
+
+In the above code example, we created a Rust language Vector of Strings
+(`vec`). In the next line, we called a utility function from the module
+`ffi_util` to translate the Rust `Vec<String>` into the C++ equivalent
+`std::vector<std::string>` - this step is essential, as we need to translate
+the type into something that the C++ end understands.
+
+These operations are *explicit*: we have opted to force users to translate
+between types at the FFI level in order to reduce the "magic" and instill
+mental models more compatible with the nature of the language-border (FFI)
+work. If we didn't, and we assumed the labour of translating these types
+transparently at the API level, we risked mistakes from our end or from the
+user end frustrating debugging efforts.
+
+At this point, we have a handle of a C++ vector containing the filenames
+of the files we want the CProver verification engine to load. To do so,
+we're going to use the following piece of code:
+
+```rust
+// Invoke load_model_from_files and see if the model has been loaded.
+if let Err(_) = client.load_model_from_files(vect) {
+    eprintln!("Failed to load model from files: {:?}", vect);
+    process::exit(1);
+}
+```
+
+The above is an example of a Rust idiom known as a `if let` - it's effectively
+a pattern match with just one pattern - we don't match any other case.
+
+What we we do above is two-fold:
+
+* We call the function `load_model_from_files` with the C++ vector (`vect`)
+  we prepared before. It's worth noting that this function is being called
+  with `client.` - what this does is that it passes the `api_session` handle
+  we initialised at the beginning as the first argument to the `load_model_from_files`
+  on the C++ API's end.
+* We handled the case where the model loading failed for whatever reason from
+  the C++ end by catching the error on the Rust side and printing a suitable error
+  message and exiting the process gracefully.
+
+---
+
+*Interlude*: **Error Handling**
+
+`cxx.rs` (the FFI bridge we're using to build the Rust API) allows for a mechanism
+wherein exceptions from the C++ program can be translated into Rust `Result<>` types
+provided suitable infrastructure has been built.
+
+Our Rust API contains a C++ shim which (among other things) intercepts CProver
+exceptions (from `cbmc`, etc.) and translates them into a form that the bridge
+can then translate to appropriate `Result` types that the Rust clients can use.
+
+This means that, as above, we can use the same Rust idioms and types as we would
+use on a purely Rust based codebase to interact with the API.
+
+*All of the API calls* are returning `Result` types such as above.
+
+---
+
+After we have loaded the model, we can proceed to then engage the verification
+engine for an analysis run:
+
+```rust
+if let Err(_) = client.verify_model() {
+    eprintln!("Failed to verify model from files: {:?}", vect);
+    process::exit(1);
+}
+```
+
+While all this is happening, we are collecting the output of the various
+phases into a message buffer. We can go forward and print any messages from
+that buffer into `stdout`:
+
+```rust
+let msgs_cpp = cprover_api::get_messages();
+let msgs_rust = ffi_util::translate_cpp_vector_to_rust(msgs_cpp);
+ffi_util::print_response(msgs_rust);
+```