Animated donut verification

Here's a cool obfuscated C program by Andy Sloane that draws a revolving donut.

You know where this is heading... I am going to suggest that someone should verify it. I will get us started.

1. Download the code

2. Determine what library functions it needs:

$ frama-c -metrics donut.c 
[kernel] preprocessing with "gcc -C -E -I.  donut.c" 
donut.c:1:[kernel] user error: syntax error 

Oops. The donut is a little bit too obfuscated for our front-end it seems. The problem here is the idiom k; to declare an int variable k. Let's change this:

int          k;double sin() 
          cos();main(){float A= 
       0 B=0 i j z[1760];char b[ 
     1760];printf("\x1b[2J");for(;; 
  ){memset(b 32 1760);memset(z 0 7040) 
  ;for(j=0;6.28>j;j+=0.07)for(i=0;6.28 
 >i;i+=0.02){float c=sin(i) d=cos(j) e= 
 sin(A) f=sin(j) g=cos(A) h=d+2 D=1/(c* 
 h*e+f*g+5) l=cos      (i) m=cos(B) n=s\ 
in(B) t=c*h*g-f*        e;int x=40+30*D* 
(l*h*m-t*n) y=            12+15*D*(l*h*n 
+t*m) o=x+80*y           N=8*((f*e-c*d*g 
 )*m-c*d*e-f*g-l        *d*n);if(22>y&& 
 y>0&&x>0&&80>x&&D>z[o]){z[o]=D;;;b[o]= 
 ". -~:;=!*#$@"[N>0?N:0];}}/*#****!!-*/ 
  printf("\x1b[H");for(k=0;1761>k;k++) 
   putchar(k%80?b[k]:10);A+=0.04;B+= 
     0.02;}}/*****####*******!!=;:~ 
       ~::==!!!**********!!!==::- 
         . ~~;;;========;;;:~-. 
             .. -------- */ 

$ frama-c -metrics donut.c 
[kernel] preprocessing with "gcc -C -E -I.  donut.c" 
[metrics] Syntactic metrics 
           Defined function (1): 
             main  (0 call);  
           Undefined functions (5): 
             putchar  (1 call); sin  (4 calls); cos  (4 calls); printf  (2 calls); 
             memset  (2 calls);  

Functions putchar() and printf() do not influence the rest of the execution so we can postpone finding a good modelization for them until the very end. We have a memset() implementation leftover from the Skein tutorial. Math functions cos() and sin() can in a first step be specified as returning [-1.0 .. 1.0]. The value analysis has for a long time had a Frama_C_cos() built-in that does a little better than that and the next release will have a Frama_C_sin() but these are not necessary yet.

Let's use a file sincos.c such as:

#include "share/builtin.h" 
double sin(double x) 
{ 
  return Frama_C_double_interval(-1.0  1.0); 
} 
double cos(double x) 
{ 
  return Frama_C_double_interval(-1.0  1.0); 
} 

3. Launch an imprecise analysis:

$ bin/toplevel.opt -val share/builtin.c sincos.c donut.c share/libc.c | grep assert 

We use the command above and get the results below. There are 9 alarms and 2 of them are redundant with the other 7 (these two would be removed in the GUI).

share/libc.c:51:[kernel] warning: out of bounds write. assert \valid(tmp); 
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760; 
donut.c:14:[kernel] warning: accessing uninitialized left-value: assert \initialized(z[o]); 
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760; 
donut.c:15:[kernel] warning: out of bounds read. assert \valid(". -~:;=!*#$@"+tmp_7); 
donut.c:15:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760; 
donut.c:17:[kernel] warning: accessing uninitialized left-value: assert \initialized(b[k]); 
donut.c:17:[kernel] warning: accessing out of bounds index [0..1760]. assert 0 ≤ k ∧ k < 1760; 
donut.c:14:[value] warning: overflow in float: [--..--] -> [-3.40282346639e+38 .. 3.40282346639e+38]. assert(Ook) 
[scope] [rm_asserts] removing 2 assertion(s) 

4. The imprecise analysis was fast. Let us launch a more precise analysis:

$ bin/toplevel.opt -val share/builtin.c sincos.c donut.c share/libc.c -slevel 200 | grep assert 
share/libc.c:51:[kernel] warning: out of bounds write. assert \valid(tmp); 
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760; 
donut.c:14:[kernel] warning: accessing uninitialized left-value: assert \initialized(z[o]); 
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760; 
donut.c:15:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760; 
donut.c:15:[kernel] warning: out of bounds read. assert \valid(". -~:;=!*#$@"+tmp_7); 
donut.c:17:[kernel] warning: accessing uninitialized left-value: assert \initialized(b[k]); 
donut.c:17:[kernel] warning: accessing out of bounds index [200..1760]. assert 0 ≤ k ∧ k < 1760; 
donut.c:14:[value] warning: overflow in float: [--..--] -> [-3.40282346639e+38 .. 3.40282346639e+38]. assert(Ook) 
[scope] [rm_asserts] removing 2 assertion(s) 

It's still the same assertions. The development version of Frama-C shows the range of the index k (that is [200..1760]) when it prints the assertion assert 0 ≤ k ∧ k < 1760;. That suggests that pushing the value of -slevel to more than 1760 may eliminate this alarm.

I will let someone else continue from here if they want. This program could be very rewarding to verify (a little birdie tells me that there is at least one true alarm to be found using the value analysis or any other techniquesI have completely lost faith in that little birdie. There may or may not be a bug we will know for sure when we are done but don't stay awake all night looking for one) so I recommended as a fun exercise for those who are bored from sandy holiday beaches.