Frama-C news and ideas

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

Tag - donut

Entries feed - Comments feed

Friday, September 23 2011

Safe donut

This post documents the steps I followed in order to finish verifying function compute(), picking up from there.

Previously on this blog

In last episode, we had found that some sub-cubes in the search space appeared to lead to dangerous value sets for variable N. These sets were:

        N ∈ {10; 11; 12}
        N ∈ {6; 7; 8; 9; 10; 11; 12}
        N ∈ {7; 8; 9; 10; 11; 12}
        N ∈ {7; 8; 9; 10; 11; 12; 13}
        N ∈ {8; 9; 10; 11; 12}
        N ∈ {8; 9; 10; 11; 12; 13}
        N ∈ {9; 10; 11; 12}
        N ∈ {9; 10; 11; 12; 13}

There are only eight dangerous value sets for N, but these correspond to many values of input variables An, Bn, in, jn in the analysis context we wrote for the occasion. Grepping for each of these eight lines in the original logs allows to get the corresponding values of An, Bn, in, jn. These are the values for which we haven't concluded yet that compute() is safe:

for i in 1 2 3 4
do
    for line in \
	"N ∈ {10; 11; 12}" \
	"N ∈ {6; 7; 8; 9; 10; 11; 12}" \
	"N ∈ {7; 8; 9; 10; 11; 12}" \
	"N ∈ {7; 8; 9; 10; 11; 12; 13}" \
	"N ∈ {8; 9; 10; 11; 12}" \
	"N ∈ {8; 9; 10; 11; 12; 13}" \
	"N ∈ {9; 10; 11; 12}" \
	"N ∈ {9; 10; 11; 12; 13}" 
    do 
        grep "$line" log$i -A4 -B0 | grep -v "N "
        echo --
    done > pb$i
done

The results are well distributed among the four quarters of the search space that I initially chose arbitrarily. That's good news, as it means things can be kept parallel by keeping these files separate. One file looks like:

        An ∈ {-26}
        Bn ∈ {-15}
        in ∈ {-26}
        jn ∈ {18}
--
        An ∈ {-26}
        Bn ∈ {-15}
        in ∈ {-26}
        jn ∈ {19}
--
        An ∈ {-26}
        Bn ∈ {-15}
        in ∈ {-3}
        jn ∈ {6}
--
...

How to re-analyze the problematic subcubes more precisely

Each file pb1, ..., pb4 can be processed a little bit further to look like C code:

for i in 1 2 3 4
do
  sed -e s"/--/f();/" -e s"/∈ {/= /" -e s"/}/;/" < pb$i > pr$i.c
done

The above commands transform the interesting values files into:

        An = -26;
        Bn = -15;
        in = -26;
        jn = 18;
f();
        An = -26;
        Bn = -15;
        in = -26;
        jn = 19;
f();
        An = -26;
        Bn = -15;
        in = -3;
        jn = 6;
f();
...

Each of the four pieces of program weights in at a bit less than 7 MB of C code. I plan to make good use of this information tidbit the next time someone asks me what project sizes Frama-C's value analysis can handle.

$ ls -l pr?.c
-rw-r--r-- 1 cuoq cuoq 6788869 2011-09-17 18:52 pr1.c
-rw-r--r-- 1 cuoq cuoq 6551620 2011-09-17 18:52 pr2.c
-rw-r--r-- 1 cuoq cuoq 6655238 2011-09-17 18:52 pr3.c
-rw-r--r-- 1 cuoq cuoq 6486765 2011-09-17 18:52 pr4.c


The files pr1.c, ..., pr4.c are not complete C programs, but they work well with the following prolog (download):

...

int An, Bn, in, jn;

void f(void)
{
  int Ans, Bns, ins, jns;
  float A, B, i, j;
  for (Ans=4*An; Ans<4*(An+1); Ans++)
    {
      A = Frama_C_float_interval(Ans / 32., (Ans + 1) / 32.);
      for (Bns=4*Bn; Bns<4*(Bn+1); Bns++)
        {
          B = Frama_C_float_interval(Bns / 32., (Bns + 1) / 32.);
          for (ins=4*in; ins<4*(in+1); ins++)
            {
              i = Frama_C_float_interval(ins / 32., (ins + 1) / 32.);
              for (jns=4*jn; jns<4*(jn+1); jns++)
                {
                  j = Frama_C_float_interval(jns / 32., (jns + 1) / 32.);
                  compute(A, B, i, j);
                }
            }
        }
    }
}

main(){

A closing bracket } is also needed to make the whole thing a syntactically correct C program.


Alas, a regrettable performance bug in Frama-C's front end prevents from analyzing such huge generated C functions. We are a bit too close to the Nitrogen release to change data structures for representing the AST, so this bug will probably remain for at least one release cycle. To circumvent the issue, I simply split the files into 182 reasonably-sized chunks (reasonably-sized here meaning 10000 lines, a more usual size for a function).

split -l 10000 pr1.c pr1.c.

182 C files to analyze and 4 cores to analyze them with: this is an undreamed-of opportunity to make use of the xargs -n 1 -P 4 command.

ls pr?.c.* | xargs -n 1 -P 4 ./do.sh

Here is the script do.sh for handling one program. It first catenates the prolog, the chunk, and a closing bracket, and then it launches the value analysis on the resulting C program:

#!/bin/sh
( cat prolog.c ; cat $1 ; echo "}" ) > t_$1.c
frama-c -val share/builtin.c t_$1.c -obviously-terminates \
  -no-val-show-progress -all-rounding-modes > log_pass2_$1 2>&1

Results

The above, yada yada yada, produces one log file for each of the 182 chunks:

$ ls -l log_pass2_pr*
-rw-r--r-- 1 cuoq cuoq 500913957 2011-09-17 20:50 log_pass2_pr1.c.aa
-rw-r--r-- 1 cuoq cuoq 502329593 2011-09-17 20:49 log_pass2_pr1.c.ab
-rw-r--r-- 1 cuoq cuoq 503146982 2011-09-17 20:51 log_pass2_pr1.c.ac
...
-rw-r--r-- 1 cuoq cuoq 502560543 2011-09-18 01:22 log_pass2_pr1.c.ay
-rw-r--r-- 1 cuoq cuoq 502283181 2011-09-18 01:23 log_pass2_pr1.c.az
-rw-r--r-- 1 cuoq cuoq 503974409 2011-09-18 01:30 log_pass2_pr1.c.ba
-rw-r--r-- 1 cuoq cuoq 501308298 2011-09-18 01:29 log_pass2_pr1.c.bb
...
-rw-r--r-- 1 cuoq cuoq 502932885 2011-09-18 05:20 log_pass2_pr1.c.bs
-rw-r--r-- 1 cuoq cuoq 422006804 2011-09-18 05:03 log_pass2_pr1.c.bt
-rw-r--r-- 1 cuoq cuoq 502353901 2011-09-18 05:19 log_pass2_pr2.c.aa
-rw-r--r-- 1 cuoq cuoq 502485241 2011-09-18 05:23 log_pass2_pr2.c.ab
-rw-r--r-- 1 cuoq cuoq 503562848 2011-09-18 05:57 log_pass2_pr2.c.ac
...
-rw-r--r-- 1 cuoq cuoq 184986900 2011-09-18 12:28 log_pass2_pr2.c.bs
-rw-r--r-- 1 cuoq cuoq 498627515 2011-09-18 13:11 log_pass2_pr3.c.aa
...
-rw-r--r-- 1 cuoq cuoq 263096852 2011-09-19 05:27 log_pass2_pr4.c.bs

Incidentally, it appears from the above listing that the second pass took about 36 hours (two nights and one day). The inside of one log file looks like:

[value] DUMPING STATE of file t_pr1.c.aa.c line 24
...
        N ∈ {10; 11}
        An ∈ {-26}
        Bn ∈ {-15}
        in ∈ {-26}
        jn ∈ {18}
        Ans ∈ {-104}
        Bns ∈ {-60}
        ins ∈ {-104}
        jns ∈ {72}
        A ∈ [-3.25 .. -3.21875]
        B ∈ [-1.875 .. -1.84375]
        i ∈ [-3.25 .. -3.21875]
        j ∈ [2.25 .. 2.28125]
        =END OF DUMP==
t_pr1.c.aa.c:15:[value] Function compute: postcondition got status valid.
[value] DUMPING STATE of file t_pr1.c.aa.c line 24
...
        N ∈ {10; 11}
        An ∈ {-26}
        Bn ∈ {-15}
        in ∈ {-26}
        jn ∈ {18}
        Ans ∈ {-104}
        Bns ∈ {-60}
        ins ∈ {-104}
        jns ∈ {73}
        A ∈ [-3.25 .. -3.21875]
        B ∈ [-1.875 .. -1.84375]
        i ∈ [-3.25 .. -3.21875]
        j ∈ [2.28125 .. 2.3125]
        =END OF DUMP==
...

Each value set for variable N is computed more precisely than in the first pass, because the values for floating-point variables A, B, i, j are known more precisely. Above, N is determined to be either 10 or 11 (both safe values) for two of the subsubcubes under examination. Below is the complete list of sets of values computed for N:

$ for i in log_pass2_pr* ; do grep "N " $i | sort -u ; done | sort -u
        N ∈ {10}
        N ∈ {10; 11}
        N ∈ {11}
        N ∈ {7; 8; 9}
        N ∈ {8; 9}
        N ∈ {8; 9; 10}
        N ∈ {9}
        N ∈ {9; 10}
        N ∈ {9; 10; 11}

Conclusion

I have already provided the "the function being analyzed is safe after all" conclusion in the previous post. This post is only for showing the "how", so that you can judge for yourself, for instance, how much cheating there was. There was quite a bit of C code written for the purpose of the verification: this code could itself have bugs. And there was a good amount of logs processing with shell scripts. There could be bugs there too. Stéphane Duprat would however point out that if we had done the verification with tests, there would have been testing code and logs-processing-scripts too. The difference between the two approaches is that we used Frama_C_float_interval() in the places where we might have used a random number generator. It does not feel like a large conceptual leap, and we obtained deeper properties in exchange (would you trust the function not to return 12 if, like me, you didn't understand what it computes at all and had only tested it a million times? A billion times? How many tests would be enough for you to sit under a piano?)

The possibility that variable N in function compute() held a number larger than 11 was related to the last and most difficult of a series of alarms that we found in a mostly unmodified piece of obfuscated C code. Some of the other alarms disappeared simply by playing with the -slevel setting, which is the setting to think of immediately when the analysis is fast enough and some alarms remain. I explained where the other alarms came from (a call to memset() was not handled precisely enough, etc.) but in actual use, you don't need to: just increase the argument to -slevel and see if the alarms go away, even before starting to think.


The method I have shown here is a little bit laborious, but one reason for us Frama-C developers to do these case studies is to find out about possible uses and make them more comfortable in future releases. This series of posts shows how to do this kind of verification now (well... it describes how to do them soon; the method shown will work with the Nitrogen release). This is absolutely not definitive. A plug-in could automate a lot of what we have done by hand here.


This post was improved by insights from Florent Kirchner.

Monday, September 19 2011

Penultimate donut post: the function compute() is safe

Do two jobs, and do them well

In the previous post, I used the command:

$ cat log? | grep "N " | sort | uniq

This may be an inefficient way to get a list of unique lines containing "N ". The command sort does not know that it is sending its results to uniq, so it has to keep all duplicates in memory, or at least keep a count for each of them. As pointed out by my colleague Benjamin Monate, you can make sort's job easier by telling it directly that you are only interested in unique lines. The option is sort -u. This can only make sort's job simpler, even if it has an optimization for dealing with duplicate lines efficiently.

Update on the donut verification

The computations for the remaining difficult 5% of the search space are now finished. I was hoping not to have to do a third pass, so I split each side of the examined subcube in 4. In other words, I divided each subcube in 4⁴ or 256 subsubcubes. A little birdie told me that splitting each side in two wouldn't be sufficient. That birdie had been wrong before, but this time, it was absolutely sure— it got the tip straight from the subcube's mouth.

I have kept the entire logs for this second pass, since I didn't know yet whether I would need the additional information they contain. I would have needed them if a third pass had been necessary, but it won't be. It is now official: function compute() is safe for all arguments between -3.25 and 3.25.

Now I must write the concluding post quickly, because the full logs are taking 85GB on our computations server.

Saturday, September 17 2011

Probably safe donut

Introduction

In the first post in the obfuscated animated donut series, my colleague Anne pointed out that:

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 ?

It is only safe to use an offset between 0 and 11 when accessing inside the quantization string ".,-~:;=!*#$@". The value analysis determined that the offset was certainly between 0 and 40, so the analyzer can't be sure that the memory access is safe, and emits an alarm. Of course, [0..40] is only a conservative approximation for the value of the offset at that point. This approximation is computed with model functions sin() and cos() only known to return values in [-1.0 .. 1.0]. These model functions completely lose the relation between the sine and the cosine of a same angle. The computation we are interested in is more clearly seen in the function below, which was extracted using Frama-C's slicing plug-in.

/*@ ensures 0 <= \result <= 11 ; */
int compute(float A, float B, float i, float j)
{
  float c=sin(i), l=cos(i);
  float d=cos(j), f=sin(j);
  float g=cos(A), e=sin(A);
  float m=cos(B), n=sin(B);

  int N=8*((f*e-c*d*g)*m-c*d*e-f*g-l*d*n);
  return N>0?N:0;
}

Both the sine and the cosine of each argument are computed, and eventually used in the same formula. Surely the analyzer would do better if it could just remember that sin(x)²+cos(x)²=1. Alas, it doesn't. It just knows that each is in [-1.0 .. 1.0].

Making progress

But the Nitrogen release will have more precise sin() and cos() modelizations! Focusing only on the sub-computation we are interested in, we can split the variation domains for arguments A, B, i, j of function compute(), until it is clear whether or not N may be larger than 11.

I suggest to use the program below (download), where the code around compute() creates the right analysis context. Just like in unit testing, there are stubs and witnesses in addition to the function under test.

...

/*@ ensures 0 <= \result <= 11 ; */
int compute(float A, float B, float i, float j)
{
  float c=sin(i), l=cos(i);
  float d=cos(j), f=sin(j);
  float g=cos(A), e=sin(A);
  float m=cos(B), n=sin(B);

  int N=8*((f*e-c*d*g)*m-c*d*e-f*g-l*d*n);
Frama_C_dump_each();
  return N>0?N:0;
}

main(){
  int An, Bn, in, jn;
  float A, B, i, j;
  for (An=-26; An<26; An++)
    {
      A = Frama_C_float_interval(An / 8., (An + 1) / 8.);
      for (Bn=-26; Bn<26; Bn++)
	{
	  B = Frama_C_float_interval(Bn / 8., (Bn + 1) / 8.);
	  for (in=-26; in<26; in++)
	    {
	      i = Frama_C_float_interval(in / 8., (in + 1) / 8.);
	      for (jn=-26; jn<26; jn++)
		{
		  j = Frama_C_float_interval(jn / 8., (jn + 1) / 8.);
		  compute(A, B, i, j);
		}
	    }
	}
    }
}

Each for loop only covers the range [-3.25 .. 3.25]. In the real program, A and B vary in much wider intervals. If target functions sin() and cos() use a decent argument reduction algorithm (and incidentally, use the same one), the conclusions obtained for [-3.25 .. 3.25] should generalize to all finite floating-point numbers. This is really a property of the target platform that we cannot do anything about at this level, other than clearly state that we are assuming it.


In fact, the programs I analyzed were not exactly like above: this task is trivial to run in parallel, so I split the search space in four and ran four analyzers at the same time:

$ for i in 1 2 3 4 ; do ( time bin/toplevel.opt -val share/builtin.c \
an$i.c -obviously-terminates -no-val-show-progress \
-all-rounding-modes ) > log$i 2>&1 & disown %1 ; done

After a bit less than two hours (YMMV), I got files log1,..., log4 that contained snapshots of the memory state just after variable N had been computed:

[value] DUMPING STATE of file an1.c line 24
...
        c ∈ [-0.016591893509 .. 0.108195140958]
        l ∈ [-1. .. -0.994129657745]
        d ∈ [-1. .. -0.994129657745]
        f ∈ [-0.016591893509 .. 0.108195140958]
        g ∈ [-1. .. -0.994129657745]
        e ∈ [-0.016591893509 .. 0.108195140958]
        m ∈ [-1. .. -0.994129657745]
        n ∈ [-0.016591893509 .. 0.108195140958]
        N ∈ {-1; 0; 1}
        An ∈ {-26}
        Bn ∈ {-26}
        in ∈ {-26}
        jn ∈ {-26}
        A ∈ [-3.25 .. -3.125]
        B ∈ [-3.25 .. -3.125]
        i ∈ [-3.25 .. -3.125]
        j ∈ [-3.25 .. -3.125]
        =END OF DUMP==
an1.c:15:[value] Function compute: postcondition got status valid.
[value] DUMPING STATE of file an1.c line 24
...
        c ∈ [-0.016591893509 .. 0.108195140958]
        l ∈ [-1. .. -0.994129657745]
        d ∈ [-0.999862372875 .. -0.989992439747]
        f ∈ [-0.141120016575 .. -0.0165918916464]
        g ∈ [-1. .. -0.994129657745]
        e ∈ [-0.016591893509 .. 0.108195140958]
        m ∈ [-1. .. -0.994129657745]
        n ∈ [-0.016591893509 .. 0.108195140958]
        N ∈ {-2; -1; 0; 1}
        An ∈ {-26}
        Bn ∈ {-26}
        in ∈ {-26}
        jn ∈ {-25}
        A ∈ [-3.25 .. -3.125]
        B ∈ [-3.25 .. -3.125]
        i ∈ [-3.25 .. -3.125]
        j ∈ [-3.125 .. -3.]
        =END OF DUMP==
[value] DUMPING STATE of file an1.c line 24
...

Some input sub-intervals for A, B, i, j make the analyzer uncertain about the post-condition N ≤ 11. Here are the first such inputs, obtained by searching for "unknown" in the log:

...
[value] DUMPING STATE of file an1.c line 24
 ...
        c ∈ [-0.850319802761 .. -0.778073191643]
        l ∈ [-0.628173649311 .. -0.526266276836]
        d ∈ [0.731688857079 .. 0.810963153839]
        f ∈ [0.585097253323 .. 0.681638777256]
        g ∈ [-1. .. -0.994129657745]
        e ∈ [-0.016591893509 .. 0.108195140958]
        m ∈ [-1. .. -0.994129657745]
        n ∈ [-0.016591893509 .. 0.108195140958]
        N ∈ {8; 9; 10; 11; 12}
        An ∈ {-26}
        Bn ∈ {-26}
        in ∈ {-18}
        jn ∈ {5}
        A ∈ [-3.25 .. -3.125]
        B ∈ [-3.25 .. -3.125]
        i ∈ [-2.25 .. -2.125]
        j ∈ [0.625 .. 0.75]
        =END OF DUMP==
an1.c:15:[value] Function compute: postcondition got status unknown.
...

Here is the complete list of value sets obtained for variable N on the entire search space:

$ cat log? | grep "N " | sort | uniq
        N ∈ {0; 1}
        N ∈ {0; 1; 2}
        N ∈ {0; 1; 2; 3}
        N ∈ {0; 1; 2; 3; 4}
        N ∈ {0; 1; 2; 3; 4; 5}
        N ∈ {0; 1; 2; 3; 4; 5; 6}
        N ∈ {-1; 0}
        N ∈ {-1; 0; 1}
        N ∈ {10; 11}
        N ∈ {10; 11; 12}
        N ∈ {-1; 0; 1; 2}
        N ∈ {-1; 0; 1; 2; 3}
        N ∈ {-1; 0; 1; 2; 3; 4}
        N ∈ {-10; -9}
        N ∈ {-10; -9; -8}
        N ∈ {-10; -9; -8; -7}
        N ∈ {-10; -9; -8; -7; -6}
        N ∈ {-10; -9; -8; -7; -6; -5}
        N ∈ {-10; -9; -8; -7; -6; -5; -4}
        N ∈ {-11; -10}
        N ∈ {-11; -10; -9}
        N ∈ {-11; -10; -9; -8}
        N ∈ {-11; -10; -9; -8; -7}
        N ∈ {-11; -10; -9; -8; -7; -6}
        N ∈ {-11; -10; -9; -8; -7; -6; -5}
        N ∈ {1; 2}
        N ∈ {-12; -11; -10}
        N ∈ {-12; -11; -10; -9}
        N ∈ {-12; -11; -10; -9; -8}
        N ∈ {-12; -11; -10; -9; -8; -7}
        N ∈ {-12; -11; -10; -9; -8; -7; -6}
        N ∈ {1; 2; 3}
        N ∈ {1; 2; 3; 4}
        N ∈ {1; 2; 3; 4; 5}
        N ∈ {1; 2; 3; 4; 5; 6}
        N ∈ {1; 2; 3; 4; 5; 6; 7}
        N ∈ {-13; -12; -11; -10; -9}
        N ∈ {-13; -12; -11; -10; -9; -8}
        N ∈ {-13; -12; -11; -10; -9; -8; -7}
        N ∈ {-2; -1}
        N ∈ {-2; -1; 0}
        N ∈ {-2; -1; 0; 1}
        N ∈ {-2; -1; 0; 1; 2}
        N ∈ {-2; -1; 0; 1; 2; 3}
        N ∈ {2; 3}
        N ∈ {2; 3; 4}
        N ∈ {2; 3; 4; 5}
        N ∈ {2; 3; 4; 5; 6}
        N ∈ {2; 3; 4; 5; 6; 7}
        N ∈ {2; 3; 4; 5; 6; 7; 8}
        N ∈ {-3; -2}
        N ∈ {-3; -2; -1}
        N ∈ {-3; -2; -1; 0}
        N ∈ {-3; -2; -1; 0; 1}
        N ∈ {-3; -2; -1; 0; 1; 2}
        N ∈ {3; 4}
        N ∈ {3; 4; 5}
        N ∈ {3; 4; 5; 6}
        N ∈ {3; 4; 5; 6; 7}
        N ∈ {3; 4; 5; 6; 7; 8}
        N ∈ {3; 4; 5; 6; 7; 8; 9}
        N ∈ {-4; -3}
        N ∈ {-4; -3; -2}
        N ∈ {-4; -3; -2; -1}
        N ∈ {-4; -3; -2; -1; 0}
        N ∈ {-4; -3; -2; -1; 0; 1}
        N ∈ {4; 5}
        N ∈ {4; 5; 6}
        N ∈ {4; 5; 6; 7}
        N ∈ {4; 5; 6; 7; 8}
        N ∈ {4; 5; 6; 7; 8; 9}
        N ∈ {4; 5; 6; 7; 8; 9; 10}
        N ∈ {-5; -4}
        N ∈ {-5; -4; -3}
        N ∈ {-5; -4; -3; -2}
        N ∈ {-5; -4; -3; -2; -1}
        N ∈ {-5; -4; -3; -2; -1; 0}
        N ∈ {5; 6}
        N ∈ {5; 6; 7}
        N ∈ {5; 6; 7; 8}
        N ∈ {5; 6; 7; 8; 9}
        N ∈ {5; 6; 7; 8; 9; 10}
        N ∈ {5; 6; 7; 8; 9; 10; 11}
        N ∈ {-6; -5}
        N ∈ {-6; -5; -4}
        N ∈ {-6; -5; -4; -3}
        N ∈ {-6; -5; -4; -3; -2}
        N ∈ {-6; -5; -4; -3; -2; -1}
        N ∈ {-6; -5; -4; -3; -2; -1; 0}
        N ∈ {6; 7}
        N ∈ {6; 7; 8}
        N ∈ {6; 7; 8; 9}
        N ∈ {6; 7; 8; 9; 10}
        N ∈ {6; 7; 8; 9; 10; 11}
        N ∈ {6; 7; 8; 9; 10; 11; 12}
        N ∈ {-7}
        N ∈ {7}
        N ∈ {-7; -6}
        N ∈ {-7; -6; -5}
        N ∈ {-7; -6; -5; -4}
        N ∈ {-7; -6; -5; -4; -3}
        N ∈ {-7; -6; -5; -4; -3; -2}
        N ∈ {-7; -6; -5; -4; -3; -2; -1}
        N ∈ {7; 8}
        N ∈ {7; 8; 9}
        N ∈ {7; 8; 9; 10}
        N ∈ {7; 8; 9; 10; 11}
        N ∈ {7; 8; 9; 10; 11; 12}
        N ∈ {7; 8; 9; 10; 11; 12; 13}
        N ∈ {-8; -7}
        N ∈ {-8; -7; -6}
        N ∈ {-8; -7; -6; -5}
        N ∈ {-8; -7; -6; -5; -4}
        N ∈ {-8; -7; -6; -5; -4; -3}
        N ∈ {-8; -7; -6; -5; -4; -3; -2}
        N ∈ {8; 9}
        N ∈ {8; 9; 10}
        N ∈ {8; 9; 10; 11}
        N ∈ {8; 9; 10; 11; 12}
        N ∈ {8; 9; 10; 11; 12; 13}
        N ∈ {9; 10}
        N ∈ {9; 10; 11}
        N ∈ {9; 10; 11; 12}
        N ∈ {9; 10; 11; 12; 13}
        N ∈ {-9; -8}
        N ∈ {-9; -8; -7}
        N ∈ {-9; -8; -7; -6}
        N ∈ {-9; -8; -7; -6; -5}
        N ∈ {-9; -8; -7; -6; -5; -4}
        N ∈ {-9; -8; -7; -6; -5; -4; -3}

The above is pretty cute, and it is just short enough for manual inspection. The inspection reveals that all the lines with dangerous values for N contain the number 12, so that we can grep for that. We arrive at the following list of dangerous value sets for N:

        N ∈ {10; 11; 12}
        N ∈ {6; 7; 8; 9; 10; 11; 12}
        N ∈ {7; 8; 9; 10; 11; 12}
        N ∈ {7; 8; 9; 10; 11; 12; 13}
        N ∈ {8; 9; 10; 11; 12}
        N ∈ {8; 9; 10; 11; 12; 13}
        N ∈ {9; 10; 11; 12}
        N ∈ {9; 10; 11; 12; 13}

Note: it is normal that each dangerous line contains 12: if the safety property that we are trying to establish is true, then there must be a safe value (say, 10) in each set. And the sets contain several values as the result of approximations in interval arithmetics, so that sets of values for N are intervals of integers. Any interval that contains both a safe value and an unsafe value must contain the largest safe value 11 and the smallest unsafe value 12.

Conclusion

We have improved our estimate of the maximum value of N from 40 to 13. That's pretty good, although it is not quite enough to conclude that the donut program is safe.

In conclusion to this post, now that we have ascertained that a dangerous set for N was a set that contains 12, we can compute the ratio of the search space for which we haven't yet established that the program was safe. We are exploring a dimension-4 cube by dividing it in sub-cubes. There are 52⁴ = 7 311 616 sub-cubes. Of these, this many are still not known to be safe:

$ cat log? | grep "N " | grep " 12" | wc -l
360684

We are 95% there. The remaining 5% shouldn't take more than another 95% of the time.

Monday, August 8 2011

".,-~:;=!*#$@"[N>0?N:0]

Hey, I left out one alarm last time:

donut.c:15 ... out of bounds read. assert \valid(".,-~:;=!*#$@"+tmp_7);

This corresponds to ".,-~:;=!*#$@"[N>0?N:0] in the obfuscated code. I wanted to have a blog post about this construct in particular because I was curious whether it would break the content management system's URL generation.

The reason why this alarm is a false alarm is a bit difficult to see in context, so let us focus on the function below, which contains only the relevant computations.

double sin(double), cos(double);

/*@ ensures 0 <= \result <= 11 ; */
int compute(float A, float B, float i, float j)
{
  float c=sin(i), l=cos(i);
  float d=cos(j), f=sin(j);
  float g=cos(A), e=sin(A);
  float m=cos(B), n=sin(B);

  int N=8*((f*e-c*d*g)*m-c*d*e-f*g-l*d*n);
  return N>0?N:0;
}


How would we argue that it is allowable to do this in a real verification? If the target compiler implements IEEE 754 floating-point exactly, then it doesn't matter what instructions are interspersed with the ones we are studying: they always give the same IEEE 754-mandated values. If the compiler only implements IEEE 754 approximately (say, computing some intermediate values in higher precision, and later double-rounding some of them at its whim), then we can analyze the function above with option -all-rounding-modes and argue that while the instructions around these ones may, in the real program, interfere with the computation, all possible results of the real program are captured by the value analysis' predictions for this function.

I do not know whether this kind of argument would be accepted in an industrial context, but on the other hand, the difficulty here, similarly to the case of variable o in the last post, is artificially introduced by the program's obfuscation. So the point is probably moot: industrial code would not be allowed to mix up computations like this in the first place.

If the discussion above seems a bit abstract, perhaps you have not read David Monniaux's report on the pitfalls of floating-point computations for static analysis. Consider it recommended.


Lastly, modifying the program as below and invoking Frama-C's slicing plug-in with the command that follows was useful for extracting the function compute() above.

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);

	  /*@ slice pragma expr 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;}}/*****####*******!!=;:~
       ~::==!!!**********!!!==::-
         .,~~;;;========;;;:~-.
             ..,--------,*/
$ bin/toplevel.opt -val share/libc.c -slice-pragma main -slice-print donut.c
...
/* Generated by Frama-C */
extern double sin();
extern double cos();
void main(void)
{
  float A;
  float B;
  float i;
  float j;
  A = (float)0;
  B = (float)0;
  while (1) {
    j = (float)0;
    while (6.28 > (double)j) {
      i = (float)0;
      while (6.28 > (double)i) {
        { float c; float d; float e; float f; float g; float l; float m;
          float n; int N; c = (float)sin(i); d = (float)cos(j);
          e = (float)sin(A); f = (float)sin(j); g = (float)cos(A);
          l = (float)cos(i); m = (float)cos(B); n = (float)sin(B);
          N = (int)((float)8 * ((((f * e - (c * d) * g) * m - (c * d) * e) - 
                                 f * g) - (l * d) * n));
          /*@ slice pragma expr N; */ ;
        }
        
        i = (float)((double)i + 0.02);
      }
      j = (float)((double)j + 0.07);
    }
    A = (float)((double)A + 0.04);
    B = (float)((double)B + 0.02);
  }
  return;
}
...

Aside: in my first attempt to produce the slice above, I made the mistake of including the approximative sin() and cos() functions written earlier:

#include "share/builtin.h"

double sin(double x)
{
  return Frama_C_double_interval(-1.0, 1.0);
}
...

The slicing plug-in, always up for mischief, noticed that sin() and cos() did not use their arguments and removed completely the computations of variables A and B, and their declarations, now useless. The values of these variables do not matter, but we'll need to know that cos() and sin() are applied to the same variables i, j, A, B if we want to have a chance to establish the post-condition. The slicing was removing this crucial piece of knowledge from the sliced program, but it was only taking advantage of the information that we had given it with our function stubs.

Monday, August 1 2011

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.

Friday, July 22 2011

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.