David Crocker's Verification Blog

One class of errors we need to guard against when writing critical software is arithmetic overflow. Before I go into detail, I invite you to consider the following program and decide what it prints:

#include <stdio.h>
int main(int argc, char *argv[]) {
unsigned int x = 42;
long y = -10;
printf("%s\n", (x > y ? "Hello, normal world!" : "Hello, strange world!"));
return 0;
}

I’ll return to this example later. For now, consider the function for averaging a set of readings stored in an array that I examined at in my previous two posts (ArC-specific bits are shown in green):

int16_t average(const int16_t * array readings, size_t numReadings)
pre(readings.lwb == 0; readings.upb == numReadings)
pre(numReadings != 0)
returns((+ over readings.all)/numReadings)
{
int sum = 0;
size_t i;
for (i = 0; i < numReadings; ++i)
keep(i <= numReadings)
keep(sum == + over readings.all.take(i))
decrease(numReadings - i)
{
sum += readings[i];
}
return (int16_t)(sum/numReadings);
}

I reported in the earlier post that ArC is able to verify this, apart from proving absence of integer overflow. Here are the verification warnings that ArC reports:

c:\escher\arctest\arctest14.c (17,13): Warning! Exceeded time limit proving: Arithmetic result of operator ‘+’ is within limit of type ‘int’, suggestion available (see C:\Escher\ArcTest\arctest14_unproven.htm#9), did not prove: minof(int) <= (sum$loopstart_5398,5$ + readings[i$loopstart_5398,5$ - readings.lwb]).

c:\escher\arctest\arctest14.c (17,13): Warning! Exceeded time limit proving: Arithmetic result of operator ‘+’ is within limit of type ‘int’, suggestion available (see C:\Escher\ArcTest\arctest14_unproven.htm#10), did not prove: (sum$loopstart_5398,5$ + readings[i$loopstart_5398,5$ - readings.lwb]) <= maxof(int).

c:\escher\arctest\arctest14.c (19,22): Warning! Unable to prove: Type constraint satisfied in implicit conversion from ‘int’ to ‘unsigned int’, suggestion available (see C:\Escher\ArcTest\arctest14_unproven.htm#18), did not prove: minof(unsigned int) <= sum$5398,5$.

Any time we do an explicit or implicit conversion from one type to another type that is not wider than the original or is defined by a constrained typedef, or we do certain arithmetic operations, we need to guard against integer overflow. This example contains several such operations.

The first implicit type conversion is when we initialize the loop counter i to the constant 0. We declared i to be of type size_t, which is an unsigned type, whereas the constant 0 has type (signed) int because we didn’t use the U suffix. So there is an implicit conversion from int to size_t here, and ArC will generate verification conditions that the constant 0 is in the range of size_t. Of course, the proof is trivial.

The other implicit type conversion is in the subexpression sum/numReadings in the return statement. Since numReadings has type size_t and sum has type int, the “usual arithmetic conversions” will be applied. In practice, size_t is never smaller than int, so there will be an implicit conversion of sum to size_t. ArC therefore generates the verification condition that the current value of sum is representable in size_t. As there is nothing to prevent sum from being negative, the proof fails – hence it emits the third warning message listed above.

In fact, ArC – like most ordinary static analysers and some compilers – warns about the signed/unsigned mismatch even before starting the proofs. Avoiding signed/unsigned mismatches in the first place is probably a more efficient strategy than dealing with the verification failures that often occur when you don’t. Had I followed my own advice to avoid using unsigned types, the signed/unsigned mismatch would not have arisen.

To fix the error, we can either change the type of the parameter numReadings to int, or cast it to type int before using it as the divisor. If we do the latter, we’ll also need to add a function precondition that numReadings is not too large to fit in an int.

For the integer operators + – and * it can be the case that applying the “usual arithmetic conversions” to an operator expression does not involve an unsafe implicit type conversion, yet the arithmetic result is not representable in the result type. The C standard defines the result in this case as undefined if the promoted operands are signed, or the arithmetic result modulo some N if they are unsigned. ArC treats it as an error in either case, because unsigned types are frequently used where modulo arithmetic is not the user’s intention; so it always generates verification conditions that the result is in type. This is the reason for the first two verification failures that ArC reports for our original example. The expression sum += readings[i] could easily overflow, because the sum could be as high as maxof(int16_t) * maxof(size_t) or as low as minof(int16_t) * maxof(size_t), which are larger than maxof(int) and minof(int) respectively. To avoid overflow, we will need to constrain either the minimum and maximum values of each reading, or the number of readings. Here’s our example with the precondition changed to limit the number of readings:

int16_t average(const int16_t * array readings, size_t numReadings)
pre(readings.lwb == 0; readings.upb == numReadings)
pre(numReadings != 0; numReadings <= maxof(int)/(maxof(int16_t) + 1))
returns((+ over readings.all)/numReadings)
{
int sum = 0;
size_t i;
for (i = 0; i < numReadings; ++i)
keep(i <= numReadings)
keep(sum == + over readings.all.take(i))
decrease(numReadings - i)
{
sum += readings[i];
}
return (int16_t)(sum/(int)numReadings);
}

I’ve referred to the maximum value supported by type int as maxof(int). ArC provides type operators maxof(T) and minof(T) for your convenience, to save you from having to #include <limits.h> or similar just for specification purposes. I’ve also cast numReadings to int prior to using it in the division.

With the compiler parameters set to assume int is 32 bits and short int is 16 bits, ArC verifies this example completely. You may be wondering why the expression (+ over readings.all)/numReadings in the returns specification doesn’t also generate a signed/unsigned warning or verification failure. That’s because integer arithmetic in specifications is always carried out after promoting operands to type integer, the ArC integral types that has no bounds.

Finally, let’s return to the short program I invited you to consider at the start of this post. Is the world normal or strange? On my computer, compiling with Microsoft Visual C++ 2008, it’s strange. That’s because for this compiler, both (unsigned) int and long are 32 bits. So both operands of less-than get converted to unsigned long … and -10 won’t fit! For the world to be normal, you’ll need to use a compiler for which long is larger than int, so that both operands get converted to (signed) long instead.

In my last entry I showed how to use a correct-by-construction approach to develop a binary search function. We got as far as specifying the function and the loop, but we left the loop body undefined. The function declaration looked like this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
pre(table.lwb == 0; table.lim == nElems)
pre(forall a in table.indices; b in table.indices
:- b > a => table[b].raw > table[a].raw)
post(result <= nElems)
post(forall i in 0..(result - 1) :- key >= table[i])
post(forall i in result..(nElems - 1) :- key <= table[i]);

and the function definition like this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key) {
size_t low = 0, high = nElems;
while (high != low)
keep(high >= low)
keep(high <= nElems)
keep(forall i in 0..(low - 1) :- table[i].rawValue <= key)
keep(forall i in high..(nElems - 1) :- table[i].rawValue >= key)
decrease(high - low) {
low = ?; high = ?;
}
return low;
}


ArC verified the program, apart from the incomplete loop body. So we just need to write loop body code that preserves the four loop invariants (the expressions in the keep clauses), decreases the variant (the expression in the decrease clause), and leaves the variant non-negative unless the loop is about to terminate.

The classic way to do a binary search is to pick an index midway between low and high, compare the table item at that point with the key, and adjust either low or high to that index depending on the result. So here’s a first attempt:

const size_t mid = (low + high)/2;
if (key >= table[mid].raw) {
low = mid;
} else {
high = mid;
}

If we try to verify this using ArC, we get a single failed verification condition:

c:\escher\arctest\ex5.c (23,9): Warning! Exceeded time limit proving: Loop body establishes end condition or decreases variant (defined at c:\escher\arctest\ex5.c (21,5)) (see C:\Escher\ArcTest\ex5_unproven.htm#6), did not prove: (low$loopstart_7603,5$ + high$loopend$) < (low$loopend$ + high$loopstart_7603,5$).

The prover has timed out trying to prove that the body either decreases the variant or leads to termination of the loop. There are four possibilities:

1. There is a genuine problem – the code may loop indefinitely.
2. The code won’t loop indefinitely, but we need a different loop variant in order to make this provable.
3. The verification condition was simply too hard for the prover (this is always a possibility when the proof timed out). We could try increasing the prover timeout.
4. There is a bug in ArC.

In this case, if we follow the link to the HTML proof report file, we see this:

Could not prove any of:
!((1 + low_{loopstart_7603,5}) == high_{loopstart_7603,5})
…

So the prover thinks that the loop may not make any progress if high == 1 + low at the start of the loop. Sure enough, there is; because in this situation, mid == low. So we may end up doing the assignment low = low, leading to an indefinite loop.

One way to fix this is to avoid the situation high = 1 + low at the start of the loop. For example, we could change the while-condition to high > low + 1. Returning low immediately after the end of the loop will no longer be correct, so we’ll need to do something different.

However, the loop invariant we have to maintain is that all elements up to and including low – 1 hold raw values less than or equal to key. Therefore, having established that the element at mid is less than or equal to key, we can set low to mid + 1 instead of mid, avoiding the problem. So the code now looks like this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key) {
size_t low = 0, high = nElems;
while (high != low)
keep(high >= low)
keep(high <= nElems)
keep(forall i in 0..(low - 1) :- table[i].rawValue <= key)
keep(forall i in high..(nElems - 1) :- table[i].rawValue >= key)
decrease(high - low) {
const size_t mid = (low + high)/2;
if (key >= table[mid].raw) {
low = mid + 1;
} else {
high = mid;
}
}
return low;
}


This is sufficient to make the function fully verifiable.

I hope you will agree that this has demonstrated a correct-by-construction approach to writing loops, avoiding the dangers of non-termination and off-by-one errors. It’s all too easy to introduce off-by-one errors in C, because – unlike Ada – the C language doesn’t provide a  form of loop that iterates over exactly the index range of an array, so you need to design the termination condition yourself.

Those of you who are familiar with SPARK Ada may be wondering why I used multiple preconditions, postcondition and loop invariants, rather than “and”-ing them all together like this:

keep(high >= low
&& high <= nElems
&& (forall i in 0..(low - 1) :- table[i].rawValue <= key)
&& (forall i in high..(nElems - 1) :- table[i].rawValue >= key))


You can do that in ArC, but there are two reasons why it is better not to. Firstly, when ArC is generating verification conditions – in this case, that the initialization establishes the loop invariant that the loop body preserves it – ArC will generate a separate verification condition for each invariant expression. If you “and” the invariants together, you have a single expression, and therefore a single verification condition. If ArC fails to prove it, you can’t easily tell which part of the invariant failed without looking at the prover output. Writing the invariants separately (or, alternatively, putting them all in one keep-clause as separate expressions separated by semicolons) causes ArC to generate a separate verification condition for each one, so that you can see immediately which one(s) failed.

The second reason for using multiple specification clauses is also to do with error reporting. Remember that ArC keywords such as pre, post and keep are implemented as macros, so that the specifications can be made invisible to standard C compilers. When a C preprocessor expands the macros, it generally ignores the layout of the actual macro arguments, and generates the expanded version using the layout of the macro definition. So a macro argument that you wrote across several lines in your source code typically gets expanded to a single line. This means that if an error is reported, the line number will be reported as the line on which the ArC keyword occurred, even if the error is in a macro argument a few lines later. So it’s best to keep the arguments to ArC specification macros on the same line as the keyword. Therefore, when using long expressions, you’ll want to use a separate instance of the ArC keyword with each expression.

In the last post, I covered some different levels of formal verification that you may be interested in, and showed how to add minimum annotation to the linearization example to allow ArC to prove predictable execution. The example provided a prototype for the binary search function it called, to which we added a minimal postcondition, so that it looked like this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
post(result <= nElems);

Let’s develop a verified implementation of this binary search function. We could write the code and then try to get ArC to verify it – either for predictable execution only, or for full functional correctness. However, it’s quite hard to get a binary search function right. So for this example, it’s more productive to use formal specification to develop an implementation that is correct by construction.

First, we need to specify exactly what bSearch is supposed to return, and what its preconditions are. Let’s start with the preconditions. We’re passing the number of elements of table in nElems, so we need to specify this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
pre(table.lwb == 0; table.lim == nElems)
post(result <= nElems);

The precondition says that the lower bound (the lowest legal index) into table is zero – in other words, table is a pointer to the first element of an array – and that the limit of table (one plus the highest legal index) is nElems. However, this isn’t enough: the raw values need to be in increasing order too. A standard way of specifying “in increasing order” is to say that for any two indices a and b, if b > a then the element at b is greater than the element at a. Here’s that expressed as a precondition:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
pre(table.lwb == 0; table.lim == nElems)
pre(forall a in table.indices; b in table.indices :- b > a => table[b].raw > table[a].raw)
post(result <= nElems);

The ghost member indices of an array pointer is defined by ArC as the sequence of all valid indices into the array. So table.indices means the same as table.lwb .. table.upb. The => symbol means “implies”, so b > a => table[b].raw > table[a].raw means the same as !(b > a) || table[b].raw > table[a].raw but is clearer.

Now we need to specify what the function returns. In developing linearize in the previous post, I said I was assuming a return value of 0 means the raw value is off the bottom of the table, nElems means it is off the top, otherwise the table entry indexed by the return value and the previous table entry bracket the raw value. Actually, we can simplify this. If we say that any elements with indices below the returned value have raw values less than or equal to the key, and any elements with indices at or above the returned value have raw values greater than or equal to the key, then this covers the cases of returning 0 or nElems as well.  So let’s express this single constraint in a postcondition:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
pre(table.lwb == 0; table.lim == nElems)
pre(forall a in table.indices; b in table.indices :- b > a => table[b].raw > table[a].raw)
post(result <= nElems)
post(forall i in 0..(result - 1) :- key >= table[i])
post(forall i in result..(nElems - 1) :- key <= table[i]);

This specification isn’t precise about the value we return when there is a table entry whose raw value exactly matches the key – it allows us to return the index of either that entry or the next entry. My original informal specification wasn’t precise either – it said that the two entries “bracket” the key. Given that our precondition forbids duplicate entries, we could be more precise if we want, e.g. by changing <= in the final postcondition to <.

Now we can work on the implementation. Note that when you have a function prototype declaration separate from the implementation (as here), ArC expects you to put the function specification in the prototype only, so we don’t need to repeat the preconditions and postconditions in the implementation. Here’s a rough sketch of what we want to do:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key) {
size_t low = 0, high = nElems;
while (high != low) {
/* increase low or decrease high, such that high remains >= low,
all elements below low have raw values <= the key,
and all elements at or above high have raw values >= the key */
}
return low;
}


Let’s express the text in the comment as a loop variant and a loop invariant (see my earlier post on verifying loops if you’re not familiar with these):

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key) {
size_t low = 0, high = nElems;
while (high != low)
keep(high >= low)
keep(forall i in 0..(low - 1) :- table[i].rawValue <= key)
keep(forall i in high..(nElems - 1) :- table[i].rawValue >= key)
decrease(high - low) {
/* do something */
}
return low;
}


Before we go any further, let’s check that this makes sense. ArC will need to prove that the loop invariants (the keep clauses) are true at the start of the loop. That’s easy – the initialization of low and high ensures that high >= low (which satisfies the first invariant), and that there are no table indices below low and no table indices at or above high (which satisfies the second and third invariants, because forall over an empty range is always true). Also, because we are returning low when the loop terminates, ArC will need to prove that the value of low at the end of the loop meets the postcondition on the return value. We know that when the loop terminates, the loop invariants will be true and the while-clause will be false. Therefore, we can substitute result for low (because we are returning low) and result for high (because high == low is the inverse of the while-clause) in the keep-clauses, to find out what is known about result.  When we do this, the last two keep clauses magically turn into the last two postconditions – which is exactly what we want. However, this doesn’t help with the first postcondition, which requires result <= nElems. Adding an extra loop invariant low <= nElems or high <= nElems will do the trick, since substituting result for both low and high will then give us the required term. I’ll choose high <= nElems, because it is stronger and I don’t intend that high should ever exceed nElems.

We can use ArC to check that the design is OK so far, even before we code the loop body. As well as adding the new loop invariant, we’ll need to tell ArC that we intend to assign to low and high low within the loop body, which we can do like this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key) {
size_t low = 0, high = nElems;
while (high != low)
keep(high >= low)
keep(high <= nElems)
keep(forall i in 0..(low - 1) :- table[i].rawValue <= key)
keep(forall i in high..(nElems - 1) :- table[i].rawValue >= key)
decrease(high - low) {
low = ?; high = ?;
}
return low;
}


ArC allows you to use ? in place of an expression to mean you haven’t decided what goes there yet. Naturally, ArC won’t be able to prove that the loop preserves its invariants or decreases its variant. Sure enough, if we run ArC on this example, we get 6 unproven verification conditions that refer to the loop body: one for each of the loop invariants and two for the variant. However, ArC reports that everything else is OK, including that the loop invariants are satisfied by the initialization and that the return value meets all three postconditions.

So all we need to do now is to write loop body code that assigns low and/or high such that the four loop invariants are preserved and the loop variant high – low decreases. But this post is already quite long, so I’ll do that next time.

If you’re thinking of using formal verification to increase the quality and reliability of your software, one of the first decisions you need to make is what you want to prove. Roughly speaking, you have three levels to choose from:

1. Predictable execution – that is, freedom from undefined and implementation-defined behaviour. The proofs cover such things as: all array indices are in bounds, variables are initialized before use, conversions of values to narrower types do not result in overflow, arithmetic does not overflow or underflow, null pointers are not dereferenced, and division by zero does not occur. It includes all the usual causes of what the MISRA standards call “run-time errors”, so it covers MISRA C rule 21.1.

2. Partial correctness – all the above, and the program meets its specification, if it terminates. The specification you provide may be a full functional specification, or a partial specification covering the most important parts, such as safety properties.

3. Full correctness – all the above, and the program terminates.

Most formal program verification systems supports one or more of these levels. For example, SPARK Ada supports levels 1 and 2. In SPARK-speak, level 1 is called “exception freedom”, because Ada programs normally perform run-time checking, so run-time errors manifest themselves as exceptions (which are predictable). On the other hand, Perfect Developer is focussed on full correctness, because it is a top-down tool that starts from specifications – leaving you no choice but to specify what the program is intended to achieve. ArC gives you the choice of all three levels.

You don’t have to choose a single verification level for the entire system. So you might choose full correctness for the most critical parts of the system, but be content with predictable execution elsewhere.

What difference does the choice of verification level make to you as software developer? The main effect is that if you wish to prove partial or full correctness rather than just predictable execution, you will need to write function postconditions that state what the functions are intended to achieve. If you choose only to prove predictable execution, you will sometimes still need to write function postconditions, but they can be more vague – stating something about what the function achieves rather than everything it is supposed to achieve.

Here’s an example. Suppose we have read a value from a sensor that has a non-linear response. We wish to linearize the value. To this end, we have a constant table of pairs of (raw value, linearized value), ordered such that both values are monotonically increasing. We will use a binary search to find the two adjacent entries whose raw values bracket the value read from the sensor, then interpolate between the corresponding linearized values. So the function looks something like this:

#include "arc.h"
#include "stddef.h"

typedef unsigned short uint16_t;
typedef struct { uint16_t raw; uint16_t corrected; } LinEntry;

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key);

uint16_t linearize(const LinEntry* array table, size_t nElems, uint16_t rawValue) {
  size_t index = bSearch(table, nElems, rawValue);
  if (index == 0) return table[0].corrected;
  else if (index == nElems) return table[nElems - 1].corrected;
  else {
    LinEntry low = table[index - 1], high = table[index];
    return (((high.corrected - low.corrected)/(high.raw - low.raw))
      * (rawValue - low.raw)) + low.corrected;
  }
}

static const LinEntry linTable[] = {
{0, 0}, {10, 15}, {20, 29}, ...
};

... linearize(linTable, sizeof(linTable)/sizeof(linTable[0]), someData) ...

The bSearch function takes a pointer to an array of LinEntry records (see my earlier post on taming arrays if you haven’t seen the array keyword before), the number of elements in the array, and the raw data value. I’ve assumed it returns a value in the range 0..nElems, such that 0 means the raw value is off the bottom of the table, nElems means it is off the top, otherwise the table entry it indexes and the previous table entry bracket the raw value. If we want to prove partial or full correctness, we need to specify all of this. But we can be less precise if we’re just proving predictable execution. Let’s see what ArC makes of it with no annotation other than the array keywords:

c:\arc\ex1.c (11,33): Warning! Unable to prove: Precondition of ‘[]‘ satisfied
(see C:\Arc\ex1_unproven.htm#9), cannot prove: 0 < table.lim.
c:\arc\ex1.c (12,43): Warning! Exceeded boredom threshold proving: Precondition of ‘[]‘ satisfied
(see C:\Arc\ex1_unproven.htm#7), cannot prove: nElems < (1 + table.lim).
c:\arc\ex1.c (14,29): Warning! Exceeded boredom threshold proving: Precondition of ‘[]‘ satisfied
(see C:\Arc\ex1_unproven.htm#2), cannot prove: index < (1 + table.lim).
c:\arc\ex1.c (14,54): Warning! Exceeded boredom threshold proving: Precondition of ‘[]‘ satisfied
(see C:\Arc\ex1_unproven.htm#4), cannot prove: index < table.lim.
c:\arc\ex1.c (15,17): Warning! Unable to prove: Precondition of ‘/’ satisfied
(see C:\Arc\ex1_unproven.htm#5), cannot prove: low.raw < high.raw.

There are a few problems here, all in function linearize:

• The first warning says that table[0] might be out-of-bounds, because table might be an empty array.
• The second says that table[nElems - 1] might be out-of-bounds, because we haven’t told ArC that nElems is the number of elements in table.
• The third and fourth say that table[index] and table[index - 1] might be out-of-bounds, because ArC doesn’t know that bSearch returns a value between 0 and nElems, and that table points to the start of an array with nElems elements.
• The final warning says that in the interpolation operation, the divisor (table[index].raw – table[index - 1].raw) might not be positive. Division by zero would typically cause an exception; while division by a negative number yields an implementation-defined result in C’90 and is therefore not allowed by ArC. The division will be safe if the raw values in table are monotonically increasing.

So let’s give ArC the information it needs, by adding some partial specifications:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
post(result <= nElems);

uint16_t linearize(const LinEntry* array table, size_t nElems, uint16_t rawValue)
pre(table.lwb == 0; table.lim == nElems)
pre(nElems  >= 1)
pre(forall i in 1..(nElems - 1) :- table[i].raw > table[i - 1].raw) {
  size_t index = bSearch(table, nElems, rawValue);
  if (index == 0) return table[0].corrected;
  else if (index == nElems) return table[nElems - 1].corrected;
  else {
    LinEntry low = table[index - 1], high = table[index];
    return (((high.corrected - low.corrected)/(high.raw - low.raw))
      * (rawValue - low.raw)) + low.corrected;
  }
}

In the postcondition of bSearch, we’ve specified that the return value is no greater than nElems (since it is of type size_t, it can’t be less than zero anyway). In the precondition of linearize we’ve said that table is a regular array with lower bound zero and limit nElems. These are enough to ensure that the array accesses table[index - i] and table[index] in the else-part of the if-statement are in bounds, because the previous parts of the if-statement handle the cases index == 0 and index == nElems. We’ve also specified that nElems is at least one to take care of the access to table[0].

The final precondition we’ve added to linearize says the raw values in table are monotonically increasing, by stating that for all values i from 1 up to nElems - 1 (i.e. the highest index of table), table[i].raw is greater than table[i - 1].raw.

These partial specifications are sufficient for ArC to prove that function linearize executes predictably, assuming that it is called in a state satisfying its preconditions, and that bSearch executes predictably, has no side-effects, and returns a value satisfying its postcondition. The preconditions of linearize will be verified at every place where it is called. We’ll look at verifying bSearch next time.