Frama-C news and ideas

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

Tag - position

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.

Wednesday, September 14 2011

Frama-C description

A webpage hosted on fedoraproject.org describes Frama-C as follows. I'm quoting the paragraph entirely, although it is copyrighted by Red Hat, Inc. and others. If I'm not too lazy, I will criticize thoroughly, which will make this fair use.

frama-c is a C source code analysis tool, which may be used standalone, or integrated with Emacs. frama-c includes a source browser, and can calculate simple metrics such as sloc, call depth and cyclomatic complexity for a project. It can also generate simple call graphs. Various assertions about the code may be tested, and the code may be validated against a number of theorems. frama-c accepts user written plugins for additional custom analyses. More information on frama-c may be found at http://frama-c.com/.

"Frama-C" is proper. I know that developers are first to take liberties (OCaml variable names must start with lowercase. Many contexts do not accept dashes inside names. Unix commands traditionally are all lowercase, etc.). This much is entirely our fault.

And, now that I think of it, it would be too easy to poke fun at someone who had to write a summary for a dozen comparably obscure tools that day, so I will leave the jokes implied after all. At least it does not say Frama-C only has intervals, dammit! Ok, I'm done now. Where was I? Ah, yes. Apparently, this page is some sort of wiki. Have you heard of them? They are pages on the internet that you can modify. Perhaps it wouldn't be appropriate for someone who isn't a Fedora user to go there and fix the description. But if you are reading this blog, and are not a Frama-C developer, and happen to use Fedora, then you can probably think of a better description, and it is morally acceptable for you to offer it on that wiki.


PS: so much for fair use. Does implied criticism count? Well, sue me.

PPS: the list of alarms detected by the value analysis is "uninitialized access, use of a dangling pointer, overflows in signed integer arithmetics, invalid memory access, invalid comparison of pointers, division by zero, undefined logical shift, overflows in conversions from floating-point to integer, infinite or NaN resulting from a floating-point operation, undefined side-effects in expressions".

Saturday, August 27 2011

Only intervals

More often than is good for me, I find someone on the internet saying something to the effect that "Frama-C only does intervals". Sadly, I think I see what they mean.

  • they may be of the school of thought that static analysis is abstract interpretation, so that although Frama-C is a static analysis framework with a large range of useful tricks it can do, they identify it with the one plug-in that does mostly abstract interpretation and nothing more than abstract interpretation. That much is ordinary: for every person who knows about it at all, there is a single plug-in that they think Frama-C is.
  • For those making the "intervals" remark, programs are structurally simple sequences of computations involving simple variables, so that a non-relational analysis is naturally an interval analysis. What other kind of interesting information could a non-relational analysis compute ? It's not as if programs exhibited uninitialized variables, dangling pointers, pointer arithmetics, and dirty pointer manipulation tricks.
  • And they are not interested in data flow properties either, so that they completely miss Frama-C's various plug-ins for computing data flow properties with abstract interpretation and dedicated abstract domains.

It's all fine, of course. May everyone find joy doing what they like most. I just wish Frama-C was dragged less often into these people's discussion. They don't need to hear about it, because they don't have a C program to verify, and it ruins my own fun when Google Alerts digs up this kind of comment. But I don't host a cat, and it must be a law of nature that everyone should find something foul on their doorstep once in a while.

Saturday, July 30 2011

We have a Csmith-proof framework

Csmith, that I mentioned earlier in this blog, is a random generator of C programs. That much sounds easy, but it generates only well-defined programs which two or more compilers have no excuse for compiling into executables that produce different results. And it generates varied and interesting enough C programs that it is possible to find lots of compiler bugs this way. These two constraints are obviously difficult to reconcile, and the people behind Csmith have done very impressive work.


Frama-C is a collection of analyses and transformations for C programs. In analyzing and transforming, it gives meaning to these programs. There are various ways of checking that the meaning given is consistent with the meaning implemented in a reference C compiler, so that Frama-C bugs can be found with this powerful tool, too.

Anne Pacalet, Benjamin Monate, Virgile Prevosto, Boris Yakobowski and I have been fixing roughly 50 bugs in the framework's front-end, pretty-printer, and in the value analysis, constant propagation and slicing plug-ins during the last 6 months. Fifty may seem like a large number, but you have to consider the different functions the bugs were spread over. I am sure that Csmith found as many bugs in at least one open-source and widely respected compiler. As of today, the web page claims "more than 350 previously-unknown compiler bugs", and the number is probably outdated, since it increases weekly. The number does not include our own 50 as far as I know.

More importantly, all the Frama-C plug-ins for which I found a way to take advantage of Csmith seem to be completely immune now, excepting a couple of minor limitations that can be circumvented for additional Csmith testing until they are definitely fixed. The difficult design constraint for a Csmith-based Frama-C testing script is that it must produce no false positives: the script must be able to run day and night, on tens of processors, and only require human review when it has definitely found a bug in Frama-C (it is also acceptable to find bugs in the reference C compiler or in Csmith itself, but if the script taps my shoulder for me to look at something, there had better be a bug somewhere).

That does not mean that Frama-C's value analysis or slicing plug-ins have no bug left. There are many possible bugs that could not be found this way because of the limitations of the testing methodology (especially the "no false positive" constraint), and indeed, in these plug-ins, we were fixing bugs not found by Csmith during the same period. Still, I think it is a noteworthy milestone.


Lastly, Csmith-imperviousness is a moving target. There was a time when the front-end and value analysis plug-in had already reached Csmith-proofitude (it is better to do the layers from bottom to top, so as to avoid cascading bug reports where, for instance, the slicing is wrong because the value analysis feeds it bad values because of a typing bug in the front-end). Two weeks later, Xuejun Yang, the main implementor of Csmith, had improved it so that it generated new constructs and found new problems in these previously Csmith-robustified parts. I hear Xuejun is now writing his PhD. Hopefully this will allow us a few months to boast.

Friday, June 17 2011

Clang Static Analyzer

From the Clang Static Analyzer homepage:

Please help us in this endeavor by reporting false positives.


Please help us make Frama-C better by reporting false negatives.

page 2 of 2 -