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<= \result < length;
ensures a[\result] == key;
behavior no_find:
assumes \forall integer i; 0<=i<length ==> a[i] != key;
ensures \result == -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:
lowis between0andhigh + 1(at the loop exit)highis less thanlength- all cells before
lowcontain elements smaller thankey - all cells after
highcontain elements greater thankey
and for the termination, we have
- the difference between
highandlowstrictly 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
-wpasks WP to generate proof obligations (POs) and to launch the default prover (Alt-ergo) on them-wp-splitsplits POs that are conjunctions, leading to smaller (and hopefully easier to prove) formulas to the provers-wp-rteasks 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.