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. 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.