Short, difficult programs

When researchers start claiming that they have a sound and complete analyzer for predicting whether a program statement is reachable, it is time to build a database of interesting programs.

Goldbach's conjecture

My long-time favorite is a C program that verifies Goldbach's conjecture (actual program left as an exercise to the reader).

If the conjecture is true the program never terminates (ergo a statement placed after it is unreachable). If the conjecture is false the program terminates and moves on to the following statement. The program can be implemented using unsigned long long integers that should be good for counter-examples up to 18446744073709551615. It can alternately use dynamic allocation and multi-precision integers in which case depending whether your precise definition of “analyzing a C program” includes out-of-memory behaviors you could claim that the reachability of the statement after the counter-example-finding loop is equivalent to the resolution of “one of the oldest and best-known unsolved problems in number theory and in all of mathematics”.

Easier programs than that

No-one expects the resolution of Goldbach's conjecture to come from a program analyzer. This example is too good because it is out of reach for everyone—it has eluded our best mathematicians for centuries. What I am looking for in this post is easier programs where the solution is just in reach. Examples that it would genuinely be informative to run these sound complete analyzers on. If they were made available.

With integers

For 32-bit ints and 64-bit long longs I know that the label L is unreachable in the program below but does your average sound and complete program analyzer do?

/*@ requires 2 <= x ; 
    requires 2 <= y ; */ 
void f(unsigned int x  unsigned int y) 
{ 
  if (x * (unsigned long long)y == 17) 
    L: return; 
} 

The key is that with the aforementioned platform hypotheses the multiplication does not overflow. Label L being reached would mean that the program has identified divisors of the prime number 17 which we don't expect it to.

In the program below the multiplication can overflow and not having tried it I have truly no idea whether the label L is reachable. I expect it is statistically but if you told me that it is unreachable because of a deep mathematical property of computations modulo a power of two I would not be shocked.

/*@ requires 2 <= x ; 
    requires 2 <= y ; */ 
void f(unsigned long long x  unsigned long long y) 
{ 
  if (x * y == 17) 
    L: return; 
} 

With floating-point

Floating-point is fun. Label L in the following program is unreachable:

/*@ requires 10000000. <= x <= 200000000. ; 
    requires 10000000. <= y <= 200000000. ; */ 
void sub(float x  float y) 
{ 
  if (x - y == 0.09375f) 
    L: return; 
} 

Frama-C's value analysis and most other analyzers will not tell you that label L is unreachable. It definitely looks reachable The difference between x and y can be zero and it can be 1.0. It looks like it could be 0.09375 but it cannot: the subtracted numbers are too large for the difference if non-zero to be smaller than 1.0.

So the subtlety in the example above is the magnitude of the arguments. What about smaller arguments then?

/*@ requires 1.0 <= x <= 200000000. ; 
    requires 1.0 <= y <= 200000000. ; */ 
void sub(float x  float y) 
{ 
  if (x - y == 0.09375f) 
    L: return; 
} 

This time the label L is easily reachable for instance with the inputs 2.09375 for x and 2.0 for y.

What about this third program?

/*@ requires 1.0 <= x <= 200000000. ; 
    requires 1.0 <= y <= 200000000. ; */ 
void sub(float x  float y) 
{ 
  if (x - y == 0.1f) 
    L: return; 
} 

The target difference 0.1f is larger than 0.09375f so it should be easier to obtain as the difference of two floats from the prescribed range right? In fact it isn't. The numbers 0.099999904632568359375 and 0.10000002384185791015625 can be obtained as values of x-y in the above program for the former as the result of picking 1.099999904632568359375 for x and 1.0 for y. The value 0.1f on the other hand cannot be obtained as the subtraction of two floats above 1.0 because some bits are set in its significand that cannot be set by subtracting floats that large.

Conclusion

I expect it will be some time before automatic analyzers can soundly and completely decide in all two-line programs whether the second line is reachable. Frama-C's value analysis does not detect unreachability in any of the programs above for instance (the value analysis is sound so it soundly detects that L may be reachable when it is). Please leave your own difficult two-line programs in the comments.

The floating-point examples in this post owe quite a bit to my colleague Bruno Marre explaining his article “Improving the Floating Point Addition and Subtraction Constraints” to me over lunch.