Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Animated donut: quickly sorting out alarms

This post follows that post. It is a brief survey of the alarms obtained when analyzing donut.c, such as a programmer might do when ey is only trying to find bugs or, in the context of verification, as a first step to get an estimate on the difficulty of the task.


The warning donut.c:17: ... assert 0 ≤ k ∧ k > 1760; looked like it might go away with enough unrolling, but it doesn't (I tried up to -slevel 50000. It took very long and did not improve things over -slevel 20000).


...          ........ .....
         ................... ..
       ...................... ..
     ..............................
  ..memset(b,32,1760);memset(z,0,7040)
  ;...................................
 ................. ....................
 ......................................
 ................      .................
................        ..... ..........
..............            ..............
...............          ...............
 ...............        ...............
 ..................z[o]................
 ......................................
  ....................................
   .............b[k]................
     ..............................
       ..........................
         ......................
             ..............

donut.c:14:[kernel] warning: accessing uninitialized left-value: assert \initialized(z[o]);
donut.c:17:[kernel] warning: accessing uninitialized left-value: assert \initialized(b[k]);

However, the alarms in the last post about arrays z and b possibly being used uninitialized do come from the loop inside memset() not being unrolled enough, as seen above. These go away with a higher value of -slevel. Note that z is an array of 1760 floats being initialized byte by byte, so the loop inside memset() needs to be unrolled at least 7040 times.


donut.c:14:[value] warning: overflow in float...

The above alarm about an unknown sequence of bits being used as a floating-point comes from the access z[o], and is also caused by an imprecise analysis of the loop in which array z is modified. Analyzing that loop more precisely with a higher value of -slevel allows the analysis to infer that z contains well-formed finite floating-point numbers at all times once it has been initialized.

Speaking of floating-point overflows, we should have written a pre-condition for functions sin() and cos(). They do not always return a value between -1.0 and 1.0. They may also fail if passed an infinity or NaN. The value analysis considers producing any infinity or NaN an alarm, so this omission is not a very serious one.

Note that from the point of view of the values taken by variables A and B, the program is equivalent to the bits highlighted below. The value analysis was never worried about these because by default, it assumes round-to-nearest mode. In round-to-nearest, these variables do not reach infinity. A and B stop increasing when they reach the range of floating-point numbers that are separated by twice 0.04 (resp. 0.02). When they reach that range, in about 2^23 iterations, the donut stops revolving (give or take a factor of 2 for the number of iterations).

...          ........ .....
         ................... ..
       ...................... ..
     ........................for(;;
  ){..................................
  ....................................
 ................. ....................
 ......................................
 ................      .................
................        ..... ..........
..............            ..............
...............          ...............
 ...............        ...............
 ......................................
 ......................................
  ....................................
   ......................A+=0.04;B+=
     0.02;}........................
       ..........................
         ......................
             ..............

With option -all-rounding-modes that does not exclude the possibility that the FPU might be configured to round upwards, the value analysis correctly warns about overflows for A and B at line 17.


The alarm for variable o (used as an index) comes from the fact that o is computed from x and y, and only then the program tests whether x and y fall on the viewport. The analyzer does not realize that only some of the previously computed values for o are possible at the point where this variable is used as index:

x = (int)((float)40 + ((float)30 * D) * ((l * h) * m - t * n));
y = (int)((float)12 + ((float)15 * D) * ((l * h) * n + t * m));
o = x + 80 * y;
...
if (22 > y) {
  if (y > 0) {
    if (x > 0) {
      if (80 > x) {
... z[o] ...

For what it's worth, the analyzer finds that -170 ≤ x ≤ 250 and -93 ≤ y ≤ 117. It's probably terribly approximative, but we didn't guide it yet at this point, it was just a few seconds of automatic computation.

We could hope to remove the assertion assert 0 ≤ o ∧ o > 1760; for z[o] by telling the analyzer to study separately the cases 0 ≤ y, 0 < y < 22 and 22 ≤ y, and then to separate similarly for variable x, before the computation of the value of o. This would definitely work if the snippet of code above was at the top of a function, but here, it is instead inside an infinite loop. There is a risk that it won't work because, for each state that reaches the beginning of the snippet, up to 9 states may be created, go round the loop's body, and be fed back to the same snippet. If some of these states do not get factored, this will go on until the unrolling limit is reached. I did not try it yet, and it might in fact still work despite this caveat.

If it doesn't work, this is the kind of situation where it is useful to reduce the problem to a representative but short example and ask about it on the mailing list, like in this case. In fact, the solution that was developed (but not yet documented) following this question could perhaps help a bit here.


I owe an apology to Andy Sloane. I initially thought there was a bug in his code. I have no regrets, because of the interesting e-mail discussion that followed.