1- # CProver (CBMC) Rust API
1+ # Libcprover-rust
22
3- This folder contains the implementation of the Rust API of the CProver (CBMC) project .
3+ A Rust interface for convenient interaction with the CProver tools .
44
55## Building instructions
66
@@ -15,7 +15,9 @@ project:
1515
1616* ` CBMC_LIB_DIR ` , for selecting where the ` libcprover-x.y.z.a ` is located
1717 (say, if you have downloaded a pre-packaged release which contains
18- the static library), and
18+ the static library),
19+ * ` CBMC_INCLUDE_DIR ` , for selecting where the ` cprover/api.h ` is located,
20+ and
1921* ` CBMC_VERSION ` , for selecting the version of the library to link against
2022 (this is useful if you have multiple versions of the library in the same
2123 location and you want to control which version you compile against).
@@ -27,7 +29,7 @@ directory of the CBMC project.)
2729``` sh
2830$ cd src/libcprover-rust
2931$ cargo clean
30- $ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
32+ $ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
3133```
3234
3335To build the project and run its associated tests, the command sequence would
@@ -36,7 +38,118 @@ look like this:
3638``` sh
3739$ cd src/libcprover-rust
3840$ cargo clean
39- $ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture
41+ $ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture
42+ ```
43+
44+ ## Basic Usage
45+
46+ This file will guide through a sample interaction with the API, under a basic
47+ scenario: * loading a file and verifying the model contained within* .
48+
49+ To begin, we will assume that you have a file under ` /tmp/api_example.c ` ,
50+ with the following contents:
51+
52+ ``` c
53+ int main (int argc, char * argv[ ] )
54+ {
55+ int arr[ ] = {0, 1, 2, 3};
56+ __ CPROVER_assert(arr[ 3] != 3, "expected failure: arr[ 3] == 3");
57+ }
58+ ```
59+
60+ The first thing we need to do to initiate any interaction with the API
61+ itself is to create a new `api_sessiont` handle by using the function
62+ `new_api_session`:
63+
64+ ```rust
65+ let client = cprover_api::new_api_session();
66+ ```
67+
68+ Then, we need to add the file to a vector with filenames that indicate
69+ which files we want the verification engine to load the models of:
70+
71+ ``` rust
72+ let vec : Vec <String > = vec! [" /tmp/api_example.c" . to_owned ()];
73+
74+ let vect = ffi_util :: translate_rust_vector_to_cpp (vec );
75+ ```
76+
77+ In the above code example, we created a Rust language Vector of Strings
78+ (` vec ` ). In the next line, we called a utility function from the module
79+ ` ffi_util ` to translate the Rust ` Vec<String> ` into the C++ equivalent
80+ ` std::vector<std::string> ` - this step is essential, as we need to translate
81+ the type into something that the C++ end understands.
82+
83+ These operations are * explicit* : we have opted to force users to translate
84+ between types at the FFI level in order to reduce the "magic" and instill
85+ mental models more compatible with the nature of the language-border (FFI)
86+ work. If we didn't, and we assumed the labour of translating these types
87+ transparently at the API level, we risked mistakes from our end or from the
88+ user end frustrating debugging efforts.
89+
90+ At this point, we have a handle of a C++ vector containing the filenames
91+ of the files we want the CProver verification engine to load. To do so,
92+ we're going to use the following piece of code:
93+
94+ ``` rust
95+ // Invoke load_model_from_files and see if the model has been loaded.
96+ if let Err (_ ) = client . load_model_from_files (vect ) {
97+ eprintln! (" Failed to load model from files: {:?}" vect );
98+ process :: exit (1 );
99+ }
100+ ```
101+
102+ The above is an example of a Rust idiom known as a ` if let ` - it's effectively
103+ a pattern match with just one pattern - we don't match any other case.
104+
105+ What we we do above is two-fold:
106+
107+ * We call the function ` load_model_from_files ` with the C++ vector (` vect ` )
108+ we prepared before. It's worth noting that this function is being called
109+ with ` client. ` - what this does is that it passes the ` api_session ` handle
110+ we initialised at the beginning as the first argument to the ` load_model_from_files `
111+ on the C++ API's end.
112+ * We handled the case where the model loading failed for whatever reason from
113+ the C++ end by catching the error on the Rust side and printing a suitable error
114+ message and exiting the process gracefully.
115+
116+ ---
117+
118+ * Interlude* : ** Error Handling**
119+
120+ ` cxx.rs ` (the FFI bridge we're using to build the Rust API) allows for a mechanism
121+ wherein exceptions from the C++ program can be translated into Rust ` Result<> ` types
122+ provided suitable infrastructure has been built.
123+
124+ Our Rust API contains a C++ shim which (among other things) intercepts CProver
125+ exceptions (from ` cbmc ` , etc.) and translates them into a form that the bridge
126+ can then translate to appropriate ` Result ` types that the Rust clients can use.
127+
128+ This means that, as above, we can use the same Rust idioms and types as we would
129+ use on a purely Rust based codebase to interact with the API.
130+
131+ * All of the API calls* are returning ` Result ` types such as above.
132+
133+ ---
134+
135+ After we have loaded the model, we can proceed to then engage the verification
136+ engine for an analysis run:
137+
138+ ``` rust
139+ if let Err (_ ) = client . verify_model () {
140+ eprintln! (" Failed to verify model from files: {:?}" vect );
141+ process :: exit (1 );
142+ }
143+ ```
144+
145+ While all this is happening, we are collecting the output of the various
146+ phases into a message buffer. We can go forward and print any messages from
147+ that buffer into ` stdout ` :
148+
149+ ``` rust
150+ let msgs_cpp = cprover_api :: get_messages ();
151+ let msgs_rust = ffi_util :: translate_cpp_vector_to_rust (msgs_cpp );
152+ ffi_util :: print_response (msgs_rust );
40153```
41154
42155## Notes
0 commit comments