Debugging with WP

Initial setting

So, I was checking a small demo of the WP plug-in the other day, just before making a presentation of Frama-C to some future fellow user. This was the traditional binary_search verification presented in the Berlin training session in 2010 but using the WP plugin instead of Jessie. For some reason I decided to change the type for all the offsets from int to unsigned int. After all we're morally dealing with array indexes and we want to search very big arrays (with length > INT_MAX don't we?) what can possibly go wrong?

The code and its contract then become the following:

/*@
    requires length > 0;
    requires \valid(a+(0..length - 1));
    requires sorted: \forall integer i j; 0<=i<=j<length ==> a[i]<=a[j];
    behavior find:
    assumes \exists integer i; 0<=i<length && a[i] == key;
    ensures 0<= \esult < length;
    ensures a[\esult] == key;
    behavior no_find:
    assumes \forall integer i; 0<=i<length ==> a[i] != key;
    ensures \esult == -1;
 */
unsigned int binary_search(int* a  unsigned int length  int key) {
  unsigned int low  high;
  low = 0; high=length-1;
  while (low <= high) {
    unsigned int med = (high-low)/2U+low;
    if (a[med] == key) return med;
    if (a[med] < key) low = med+1;
    else high = med-1;
  }
  return -1;
}

Loop invariants

As all of you know deductive verification require to write loop invariants to have a slight chance of proving something. An appropriate set of invariants for our case is the following:

• low is between 0 and high + 1 (at the loop exit)
• high is less than length
• all cells before low contain elements smaller than key
• all cells after high contain elements greater than key

and for the termination we have

• the difference between high and low strictly decreases.

Translated into ACSL with named loop invariants in order to easily identify them in WP's output and without forgetting the loop assigns (WP is a bit picky about that) this becomes:

  /*@
      loop invariant low: 0<=low<=high+1;
      loop invariant high: high < length;
      loop invariant smaller: \forall integer i; 0<=i<low ==> a[i] < key;
      loop invariant greater:
           \forall integer i; high < i < length ==> a[i] > key;
      loop assigns low  high;
      loop variant high - low;
   */

A wrong specification!

we launch Frama-C with the following command line:

frama-c-gui -wp -wp-split -wp-rte binary_search.c

• -wp asks WP to generate proof obligations (POs) and to launch the default prover (Alt-ergo) on them
• -wp-split splits POs that are conjunctions leading to smaller (and hopefully easier to prove) formulas to the provers
• -wp-rte asks RTE to generate all safety assertions before WP is launched. In other words we will get proof POs for potential run-time errors.

The result is encouraging but not perfect: behavior no_find is not proved and if we dig a little bit in the WP Proof Obligations panel we see that the branch where the PO fails is the one where we return -1 exactly what we specified:

Of course returning -1 is sensible for indicating failure when we have ints not so with unsigned... In that case we can return length to indicate that no suitable index has been found

Subtraction is not harmless

We thus correct the ensures clause and the return statement according to our new error value and relaunch frama-c-gui. This time almost everything is fine except from some tiny assertion from RTE when assigning med-1 to high:

assert rte: med-(unsigned int)1 ≥ 0;

As a matter of fact if we think of it a little further if the key is less than all elements of the array med will become 0 at a certain point and we'll try to assign -1 to high which is not exactly what we want (and is likely to result in a buffer overflow at the next loop step if length<UINT_MAX/2). We thus modify our else clause that way:

else { if med == 0 break; high = med - 1; }

Getting a correct program

This time all POs are discharged meaning that the program is correct with respect to its specification. I guess this was yet another example that no change in the code as small as it looks like can be considered harmless and that looking at the unproved POs of WP can be an effective way to catch those issues.