# Libcprover-rust

A Rust interface for convenient interaction with the CProver tools.

## Building instructions

To build the Rust project you need the Rust language toolchain installed
(you can install from [rustup.rs](https://rustup.rs)).

With that instaled, you can execute `cargo build` under this (`src/libcprover-rust`)
directory.

For this to work, you need to supply two environment variables to the
project:

* `CBMC_LIB_DIR`, for selecting where the `libcprover-x.y.z.a` is located
  (say, if you have downloaded a pre-packaged release which contains
   the static library),
* `CBMC_INCLUDE_DIR`, for selecting where the `cprover/api.h` is located,
  and
* `CBMC_VERSION`, for selecting the version of the library to link against
  (this is useful if you have multiple versions of the library in the same
   location and you want to control which version you compile against).

As an example, a command sequence to build the API through `cargo` would look
like this (assuming you're executing these instructions from the root level
directory of the CBMC project.)

```sh
$ cd src/libcprover-rust
$ cargo clean
$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
```

To build the project and run its associated tests, the command sequence would
look like this:

```sh
$ cd src/libcprover-rust
$ cargo clean
$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture
```

## 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);
```

## Notes

* The functions supported by the Rust API are catalogued within the `ffi` module within
  `lib.rs`.
* The API supports exception handling from inside CBMC by catching the exceptions in
  a C++ shim, and then translating the exception into the Rust `Result` type.
* Because of limitations from the C++ side of CBMC, the API is not thread-safe.