Test-Driving the Rust Model Checker (RMC)

The Rust Model Checker (RMC) allows Rust programs to be model checked using the C Bounded Model Checker (CBMC). In essence, RMC is an extension to the Rust compiler which converts Rust’s MIR into the input language of CBMC (GOTO).

Using RMC provide can provide much stronger guarantees than, for example, testing with cargo-fuzz or proptest. To understand how it works, I’m going to walk through the process of checking the following simple function:

fn index_of(items: &[u32], item: u32) -> usize {
    for i in 0..items.len() {
        if items[i] == item {
            return i;
        }
    }
    //
    return usize::MAX;
}

This is a good function for testing verification systems, since it has some nice post-conditions. To get started we need to add some helper methods, the first of which is:

fn __nondet<T>() -> T { 
   unimplemented!() 
}

This function is known to RMC and has special significance. Here, __nondet<T>() returns a non-deterministic value. We can think of this as an arbitrary value of the type T in question. This is where the power of RMC comes from as, instead of testing individual values of T, we’re testing all possible values of T! The second helper method we need is this:

fn __VERIFIER_assume(cond: bool) { 
   unimplemented!() 
}

Again this has specifical significance to RMC and, as we’ll see, it is used for constraining non-determinstic values. For example, we might do something like this:

let x : u32 = __nondet();
let y : u32 = __nondet();
__VERIFIER_assume(x < y);

Here, we assigned arbitrary values to x and y and then constrained x so that its always below y. Perhaps we had to do this to meet some requirement of the API we’re testing. This means RMC will never consider the values e.g. x=10, y=10 or x=255, y=0. But, it will still consider all values where x < y, such as x=0,y=1, x=255,y=256, etc. We can visualise this as follows:

Our First Proof

We’re now going to write our first “test” using RMC. Except that its not a test in the conventional sense, since we’re using arbitrary values. To try and make this distinction clear, RMC instead refers to them as proofs.

So, let’s write our first proof:

#[cfg(rmc)]
#[no_mangle]
pub fn test_01() {
  let xs : [u32; 2] = __nondet();
  assert!(index_of(&xs,0) == usize::MAX);
}

This tells RMC to test index_of() for all possible arrays of size 2. We can run RMC using e.g. rmc index_of.rs (if that’s the name of our file) and, in doing this, RMC will find the assert can fail. This makes sense as some arrays may contain 0 so index_of() will not always return usize::MAX. This is the key difference between using RMC and an automated testing tool: upto certain bounds, RMC checks all possible values.

NOTE: At the moment, RMC requires #[cfg(rmc)] to identify proofs. However, the plan is eventually to use #[proof] in the same way #[test] is used.

Anyway, something isn’t quite right yet. The index_of() method is correct, but our proof is failing. We need to refine our proof so that it reflects the true contract of index_of(). Specifically, when given an array xs which doesn’t contain 0, we expect index_of(xs,0) to return usize::MAX. The question is how to set this up with RMC. In fact, it’s pretty easy since we know the size of xs:

#[cfg(rmc)]
#[no_mangle]
pub fn test_01() {
  let xs : [u32; 2] = __nondet();
  __VERIFIER_assume(xs[0] != 0);
  __VERIFIER_assume(xs[1] != 0);
  assert!(index_of(&xs,0) == usize::MAX);
}

We’ve used __VERIFIER_assume() to tell RMC that it should assume the elements in our array do not hold 0. And finally RMC now reports, as expected, that our proof suceeds!

Going Forward

So, we’ve written our first proof. Now what? Well, since our proof only applies for arrays of size 2, it would be nice to generalise it. Unfortunately, testing arrays of arbitrary size is beyond the limit of RMC but, for example, we can prove all arrays upto size 3. Furthermore our proof only checked for item=0 but it would be better to check for arbitrary values. So, let’s put that altogether:

#[cfg(rmc)]
#[no_mangle]
pub fn test_01() {
  let x : u32 = __nondet();
  let len : usize = __nondet();
  let xs : [u32; 3] = __nondet();  
  // Apply Constraints  
  __VERIFIER_assume(len <= 3);
  __VERIFIER_assume(xs[0] != x);
  __VERIFIER_assume(xs[1] != x);
  __VERIFIER_assume(xs[2] != x);
  // Check
  assert!(index_of(&xs[..len],x) == usize::MAX);
}

This is getting more interesting! Now we’re looking for an arbitrary value x instead of 0. Likewise, the final statement takes a slice of xs upto a given length len. Since len is constrained to be anything upto and including length 3, this means RMC now checks all arrays upto length 3.

Our updated proof represents a significant improvement over the first. But, there are still tweaks we can make. For example, it’s good to employ a constant LIMIT which determines the maximum length:

  ...
  let xs : [u32; LIMIT] = __nondet();
  // Ensure length at most LIMIT
  __VERIFIER_assume(len <= LIMIT); 
  // Ensure element not in array below len
  for i in 0..len {
    __VERIFIER_assume(xs[i] != x);
  }  
  ...

Using LIMIT means we can easily try larger maximum lengths to see how far RMC can go. However, using a for loop does cause some difficulties for the underlying CBMC tool. To resolve this, we must provide a command-line argument --unwind X where X is some bound (e.g. 3). This tells CBMC to unroll the loop at most X times. In this case the maximum length of the array determines (roughly speaking) how much unrolling CBMC needs to be confident the proof holds.

The Flip Side

Now we’ve generalised our proof, its looking pretty nice. But, it only checks the case when item is not in items — that’s only half the story! So, we should add a second proof for the case where item is in items. This is my first attempt:

#[cfg(rmc)]
#[no_mangle]
pub fn test_02() {
    let x : u32 = __nondet();
    let len : usize = __nondet();
    let xs : [u32; LIMIT] = __nondet();    
    let i : usize = __nondet();
    // Apply Constraints
    __VERIFIER_assume(len <= LIMIT);
    __VERIFIER_assume(i < len);
    __VERIFIER_assume(xs[i] == x);    
    // Compute result
    let result = index_of(&xs[..len],x);
    // Check it matches
    assert!(xs[result] == x);
}

This is roughly similar to before, except we now require some i where xs[i] == x. Also, we cannot assume index_of(&xs[..len],x) returns i since there might be more than one occurence of x in the array.

We can observe that index_of() actually returns the first index of item. So, to make things more interesting, let’s assume this is actually part of its contract. To check this, we must further constrain xs to ensure x does not occur below i as follows:

  ...
  // Ensure nothing below i matches
  for j in 0..i {
    __VERIFIER_assume(xs[j] != x);
  }
  // Check found correct one
  assert!(index_of(&xs[..len],x) == i);
  ...

From this we see that RMC proofs can be made quite sophisticated using just the __nondet<T>() and __VERIFIER_assume() statements. Also, its worth noting another way of achieving this is to do the check after calling index_of() (thanks to @zhassan-aws for pointing this out):

  ...
  let result = indexof(&xs[..len],x);
  // Check it matches
  assert!(xs[result] == x);
  // Check its first
  for j in 0..result {
     assert!(xs[j] != x);
  }
  ...

Conclusion

Hopefully this has given you an insight into how RMC works, and what a proof is like. We’ve only touched the tip of the iceberg here, but the post was already quite long! You can learn more about using RMC from the Getting Started Guide. Also, I found this paper provides good background on using tools like this in an industrial setting.

Finally, if you want to play around with RMC, here are a few suggestions of things you could try:

• Implement fill(items: &mut [u32], item: u32) which fills a given array items with a given value item.

• Implement reverse(items: &mut [u32]) which reverses the contents of items.

• Implement index_of() using Vec<T> instead of a slice.