Frama-C news and ideas

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

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.

Comments

1. On Monday, July 25 2011, 16:54 by Anne

Funny ! especially if you compile and run it !

The alarm about : assert \valid(".,-~:;=!*#$@"+tmp_7); seems strange because the analysis tells us that tmp_7 ∈ [0..40] at this point... How can this be valid ?

2. On Tuesday, July 26 2011, 14:02 by pascal

"tmp_7 ∈ [0..40]" is only the value analysis' best guess, and doesn't mean that all the values are actually taken. I had a short e-mail exchange with the author of the program and in reality, omitting floating-point rounding errors, tmp_7 can be expected to be in [0..(int) (8*sqrt(2))]. Getting the value analysis to understand this is going to require a little bit of work, but it could have been worse. 1.4142*8 is 11.3136, so the program is safe here by a large margin of 0.68 on the end result of the computation of 8*((f*e-c*d*g)*m-c*d*e-f*g-l*d*n). Hopefully, getting the value analysis to conclude that it is safe will not take too much human and computer time.