Checking for overflows operation by operation

My colleague Bernard Botella pointed out an interesting example in an offline discussion following the last quiz.

The setup

Consider the snippet:

int s; 
unsigned u1  u2; 
... 
s = u1 - u2; 

The programmer's intention with the assignment is to compute in variable s of type int the mathematical difference between the value of u1 and the value of u2. You would expect that using automatic plug-ins in Frama-C ey would be able to check that the initial values for u1 and u2 are in ranges for which this is always what happens.

In fact this looks like a perfect assignment for Rte and the value analysis. Rte can generate assertions for the various conversions and the value analysis can check whether the conditions are satisfied following the method outlined in a recent post.

This is after all exactly what static analyzers — and coding rules that forbid overflows — are for.

An obvious false positive

The overflow in the subtraction u1 - u2 looks like it can be justified away. After all such a warning is emitted when u1==3 and u2==5 and s will still receive the expected value -2 after the implementation-defined conversion from the value of expression u1 - u2 that is UINT_MAX - 1 to int.

The programmer may think “okay I can see why I get this warning it happens as soon as u2 is larger than u1 but this is defined and in my case innocuous. I only want to check that the mathematical difference fits in s. The check about the absence of overflow in the conversion to int is what I am really interested in.”

Say that the programmer is using the Rte plug-in to express the conditions for both the subtraction and the implicit conversion to int to be safe pretty-printing an annotated program as a result:

$ frama-c -rte-unsigned-ov -rte t.c -print 
... 
void main(void) 
{ 
  /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */ 
  /*@ assert rte: u1-u2 ≥ 0; */ 
  s = (int)(u1 - u2); 
  return; 
} 

Since the programmer has seen that the second assertion about an overflow in the subtraction u1 - u2 is too restrictive preventing use with u1==3 and u2==5 ey removes it. The programmer instead focuses on making sure that there is no overflow in the conversion to int of the difference and feels confident if ey sees that there isn't any warning about that. It seems normal right?

void main(void) 
{ 
  /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */ 
  s = (int)(u1 - u2); 
  return; 
} 

But…

Consider the case where u1 is very small u2 is very large and the value analysis has been able to infer this information relatively precisely. We assume 0 ≤ u1 ≤ 10 and 3000000000 ≤ u2 ≤ 4000000000 for this example:

/*@ requires 0 <= u1 <= 10 ; 
    requires 3000000000 <= u2 <= 4000000000 ; */ 
void main(void) 
{ 
  /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */ 
  s = (int)(u1 - u2); 
  return; 
} 

In this case the value analysis does not warn about the conversion to int ...

$ frama-c -val -lib-entry u.c 
... 
u.c:8:[value] Assertion got status valid. 

... but the value in s is not the mathematical difference between u1 and u2.

Conclusion

The conclusion is that looking at overflows atomically is not a silver bullet. Granted if all possible overflows in the program are verified to be impossible then machine integers in the program observationally behave like mathematical integers. But the more common case is that some overflows do in fact happen in the program and are justified as benign by the programmer. The issue pointed out by Bernard Botella is that it is possible to justify an overflow for which the rule seems too strict by exhibiting input values for which the expected result is computed and then to be surprised by the consequences.

Perhaps in another post we can look at ways around this issue.