Verifying the Whiley Standard Library

Wednesday, October 27th, 2021

For sometime now, its been possible to use Boogie / Z3 as a backend for verifying Whiley programs. Initially that was pretty sketchy, but it’s really starting to ramp up now. If you haven’t heard of it before, Boogie is an Intermediate Verification Language (IVL) that provides a human-readable interface sitting on top of an SMT solver. In this case, we use Z3 as the SMT solver — but it is possible to use others, such as CVC4, etc. Boogie was initially developed at Microsoft, but is now maintained by a consortium that appears to include Facebook and Amazon, amongst others.

For example, here’s a simple Whiley program:

function abs(int x) -> (int r)
ensures r >= 0
ensures (r == x) || (r == -x):
   if x >= 0:
      return x
   else:
      return -x

The Whiley2Boogie backend is responsible for translating the above program into Boogie. Here’s a simplified version of how that looks:

procedure abs(x : int) returns (r : int)
ensures r >= 0;
ensures (r == x) || (r == -x);
{
   if(x >= 0) {
      r := x;
      return;
   } else {
      r := -x;
      return;
   }
}

Here we can see there are a few differences from the Whiley code but, in this example at least, the two look quite similar. In fact, Boogie implements a form of Dijkstra’s Guarded Command Language which has been extended with syntax to bring it closer to a programming language. However, in some cases, it can end up looking quite different.

STD.wy

The Whiley standard library, STD.wy, presents an interesting target for verification, as it is currently the largest single body of code written in Whiley. My goal is to verify the standard library and, from thereafter, ensure it is verified on every commit (using a GitHub Action). The library is still pretty small, but contains some of the things you would expect, such as collections (e.g. std::vector, std::hash_map), ASCII support (std::ascii), math functions (std::math) and various array manipulation functions (std::array). Yes, it is very much a work in progress … and now is the time to get verification ingrained as part of the build process.

As an example, here’s a function from std::array:

// find first index after a given start point in list which matches character.
// If no match, then return null.
function first_index_of<T>(T[] items, T item, uint start) -> (uint|null index)
// Starting point cannot be beyond array
requires start <= |items|
// If int returned, element at this position matches item
ensures index is uint ==> items[index] == item
// If int returned, element at this position is first match
ensures index is uint ==> !contains(items,item,start,index)
// If null returned, no element in items matches item
ensures index is null ==> !contains(items,item,start,|items|):
    //
    for i in start .. |items|
    // No element seen so far matches item
    where !contains(items,item,start,i):
        if items[i] == item:
            return (uint) i
    //
    return null

This searches forward in items from a given start index and returns either the first index matching item or (if none exists) returns null. The specification is reasonably involved, but essentially says this in logical form. To keep things a bit more intuitive we’ve used contains() instead of raw quantifiers. Here, constrains() is a property defined in std::array as follows:

property contains<T>(T[] lhs, T item, int start, int end)
// Some index in given range contains item
where some { i in start..end | lhs[i] == item }

The module std::array contains several predefined properties like this which are helpful in specifying array manipulating functions. The great thing about first_index_of() above is that we can now statically verify that its implementation meets its specification. No need to write lots of extensive tests checking all the edge cases!! This also means first_index_of() is guaranteed not to perform an out-of-bounds access or exhibit other undefined behaviour. That is something really quite powerful, and Boogie / Z3 is key to making it work.

Challenges

At this point, the goal was fairly straightforward: go through all the library functions adding specifications so they will now statically verify. This was quite a laborious task since, initially, large chunks of the library had not been specified. Having largely completed that now, we can proceed incrementally by requiring that all new code must be fully specified and pass verification.

Still, there are some challenges. Most notably, we have at least one function which currently cannot be verified (due to limitations with Boogie / Z3). This is the following function:

unsafe function copy<T>(T[] src, uint srcStart, T[] dest, uint destStart, uint length) -> (T[] result)
// Source array must contain enough elements to be copied
requires (srcStart + length) <= |src|
// Destination array must have enough space for copied elements
requires (destStart + length) <= |dest|
// Result is same size as dest
ensures |result| == |dest|
// All elements before copied region are same
ensures equals(dest,0,result,0,destStart)
// All elements in copied region match src
ensures equals(src,srcStart,result,destStart,length)
// All elements above copied region are same
ensures all { i in (destStart+length) .. |dest| | dest[i] == result[i] }:
    T[] _dest = dest // ghost
    //
    for i in 0 .. length
    // Size of dest unchanged
    where |dest| == |_dest|
    // Everything below destStart unchanged
    where equals(_dest,0,dest,0,destStart)
    // Everything copied so far is equal
    where equals(src, srcStart, dest, destStart, i)
    // Everything above j is unchanged
    where equals(_dest,dest,i+destStart,|dest|):
        dest[i+destStart] = src[i+srcStart]
    //
    return dest

This is roughly equivalent to System.arraycopy() in Java, and its not very complicated. Unfortunately, Boogie / Z3 cannot verify this without additional help. Whilst this is potentially something we can fix in the Whiley2Boogie backend, for now we simply mark the function as unsafe. This means it will be ignored during verification. However, its specification is still used when verifying other functions not marked unsafe. Whilst this is not ideal, it is a pragmatic compromise for now.

Conclusion

Using Boogie / Z3 though the Whiley2Boogie backend has significantly improved our ability to verify non-trivial Whiley programs. Work is ongoing here, and you can find a number of interesting benchmarks we are currently working through.