Frama-C news and ideas

On a recent occasion to visit the USA on a professional basis, I nearly declined. I had a lengthy explanation ready for my refusal, and it might even have become a rant-tagged blog post. I finally went, so that hypothetical blog post never became. Today, I feel I have been cheated: a really good bit of my explanation would, if I were to re-use it now in another rant, appear unimaginative; stale, even.

See, my explanation of why I didn't want to be a visitor in the USA included a passage on how schools everywhere in the world, at all levels, have bullies, but only in the US these get elected president. (You had to see it in context. There were tie-ins with culture and international politics. It was a beautiful rant)

The reason this bit is suddenly worthless is of course the latest mini-scandal in US election debates. Here is the article through which I first heard of it. My rant was about another person, who may or may not have been US president at some point in eir political career.

It is not my place to comment on foreign presidentiables. The following comments are intended only in the abstract.

• About the facts themselves, the fact that a brat bullied five homosexual fellow students does not in itself imply that the brat has a bias. If ey similarly bullied 95 heterosexual students, say, forcibly cutting the hair of 19 of them, and if 5% actually is the percentage of the population who recognizes itself as homosexual, ey cannot be blamed for being biased—although ey can still be blamed for being a bully.
• am I the only one to find “I [didn't think] the fellow was homosexual” a lousy excuse? It does not matter whether one “thinks”. From the point of view of the victim, it shouldn't be necessary to broadcast one's sexual orientation to be morally protected from harassment. A student who takes offence at any visible lifestyle choice of eir colleagues that aren't any of eir business is guilty of intolerance. If it later turns out that a relatively large proportion of eir victims are from a same minority, that's just bad luck for em, because it makes the crime more obvious. But even if the victims did not happen to be from a recognizable minority, the crime would still be the same crime.
• Finally, the only way I can imagine a kid doing the kind of “hijinks” described in the article and not being sent home for the remainder of the schoolyear is if ey is a very rich kid in a school/university that needs to worry where its next budget is going to come from. Since French Universities have begun to “gain autonomy” under our own previous president, are we now going to have the same system where rich kids get a free pass with discipline, even at the cost of the peace of mind of their fellow students? A few decades from now, will we have to elect them for the highest offices, too?

If told that this post is too off-topic for this blog, I plan to use the “but the link to the original article came from my colleague Eric Eide” defense. That, and something on the general topic of conference attendance and testicle massages.

A meta-article on benchmarking

Some colleagues and I are about to submit this article on the subject of benchmarking static analyzers. Rather than another benchmark, it is a list of general recommendations and pitfalls when benchmarking static analyzers. The article is illustrated on C program constructs because that's what we are familiar with, but these examples are only intended to show how complicated static analysis can be in general. Had we focused on another language, the underlying ideas would have remained the same: different users and toolmakers have different views of what static analysis is about. Even if they agreed on what static analysis is about, there would still be no perfect oracle to tell what the right answer to a particular testcase is.

Discussing this article as it was being written, several valid points have been raised, but unfortunately, the limit for the category in which we wish to submit is 4 pages, so I have to address these here. Consider this post a sort of addendum to the article.

Why should the C standard be the ultimate authority?

The short, facetious answer to this question is that the C standard is the democracy of C semantics: it is the worst form of reference document we have, to the exception of all others.

Which version of the C standard?

This is not a big problem in practice. Everyone seems to focus on what compilers use, for obvious reasons, and what compilers use is C90. In Frama-C, we refer to C99 when it is convenient. For instance, in C99, division is defined in more detail than in C90. C90 does not specify whether division rounds towards minus infinity (Euclidean division with a positive remainder) or rounds towards zero (all processors implement division like this, because it means that the sign of the results can be computed independently from their magnitudes, saving transistors). C99 specifies that division rounds towards zero. More information is good, so Frama-C follows C99 here. But when C90 and C99 are mutually exclusive, and compilers all implement C90, we follow the compilers. In this post about subtle typing issues, we are with gcc, predicting 2147483648 for the second example, not with gcc -std=c99 which compiles the program as displaying -2147483648. (See the following post for the explanations behind these differences).

What if most implementations agree with each other but disagree with the standard?

There are a couple of more interesting examples that we intended for the article, to illustrate this very dilemma. One is about pointer comparisons. Technically, the comparison &a < &b is undefined behavior. The same reasoning that, in the article, justifies that analyzers do not have to worry what happens in the program after an illegal pointer access could be applied to this expression.

The point here is not just that most analyzers do not care about this issue, and simply treat the comparison as returning 0 or 1. The point is that there are good reasons for an analyzer to let this kind of comparison slip: it happens naturally when a user implementation of memmove() is passed &a as source and &b as destination. An analyzer that lets this construct slip may be an analyzer that received more testing and for which usability studies revealed that users were too confused when &a < &b was treated as if it halted execution. Since there are arguments both ways, it is difficult for organizers to arbitrarily decide what an analyzer should do when confronted with this expression. And since it does not seem too fundamental, the simple escape that we recommend is to omit the construction from the benchmark. It shouldn't occur in any testcase, not as the goal of the testcase (the undefined behavior to be detected), nor as an incidental construct, that would bias testcases intended for another criterion.

For the sake of exhaustiveness, this can be contrasted to the condition &a == &b + 1. You may expect that this would be undefined, too, but for some reason it is only unspecified. The implementation may return 0 or 1, and it will not return the same value everytime. Derek Jones would point out here that an implementation could rely on just-in-time compilation and that the value of &a == &b + 1 could as a result change from one evaluation to the other, for the same expression referring to the same variables a and b. Anyway, it is not undefined, so if the standard was the absolute reference, static analyzers would not be allowed to consider that execution gets stuck on evaluating &a == &b + 1.

In Frama-C's value analysis, we do not see much reason to treat equality and inequality differently, but we recognize that both stopping execution and continuing with results {0; 1} can have their uses, so we offer an option to choose between these two behaviors. This series of posts already covers this kind of nuance.

Frama-C's value analysis detects, warns and considers execution stuck on uninitialized variables. But by design, it avoids warning (and considering execution stuck) on the statement y = x; or *dst = *src;. This is a compromise, made necessary by the necessity to analyze user implementations of memcpy(), which may use exactly that second statement for uninitialized data when copying a struct or union.

One long-standing bug in Frama-C's front-end is that it erases a possible bug during parsing and normalization. According to the letter of the standard, addressee().a is dangerous. However, this misfeature of the C99 standard has quite a history (in the circle of people who care about this sort of thing), as illustrated by the numerous comments on the linked CERT page. A static analyzer could omit this bug (and consider execution continues) by a conscious design decision (for instance if it specializes in a compiler that documents that this construct is safe). Another static analyzer could treat it as undefined, and consider that execution gets stuck. Again, the construct is not very interesting in itself, so it shouldn't be restrictive to omit it from the explicit goals of the benchmark, and to omit it from the incidental features that might perturb other tests.

Finally, there are areas where the standard under-specifies things. One egregious example is floating-point. David Monniaux's report is still the reference I recommend for these floating-point issues.

All but the last of these examples are cases of “Don't do that, then”: the issue can simply be avoided by not using any of the ambiguous constructs for which it is unclear whether an analyzer should be allowed to consider them blocking. Also, all the issues in these first examples disappear when toolmakers are allowed to participate: when their analyzer scores badly on a test because it is better than others are detecting incidental issues, they will be prompt to point out the problem.

For the last example, floating-point, I do not have a solution to offer. Some real-life software issues come specifically from the liberties that the standard allows and from the fact that compilers take advantage of them, so it is a worthy goal for a static analyzer to try to model these liberties, and a worthy goal for a benchmark to measure how well the static analyzer is doing. But floating-point in C is a mess, and since one of the issues is that compilation is under-specified, it does not suffice to use one (or even several) compilations as reference.

What about implementation-defined behavior?

This is a non-issue, really. All real C programs invoke implementation-defined behavior. As an example, the line int x = 38000; invokes implementation-defined behavior. Therefore, all static analyzers that aim to be useful for real programs assume some implementation choices, and they all tend to assume the compilation choices of the dominant platform, so implementation-defined behavior causes very little trouble in practice.

Acknowledgments

Radu Grigore provided many ideas that did not fit in the article, and is directly responsible for the existence of this blog post.

If you like this blog, then on the basis of recent posts, you will with good probability like that blog. The recent posts I have read all deal with various subtle undefined behaviors in C.

Sven Mattsen is working at CEA until the summer. He is the author of this post. The post continues the series explaining how to guide the value analysis towards more precise conclusions. It starts where that one and that other left off.

Problem

This article is concerned with the Value Analysis plug-in of Frama-C, which implements an automatic approach towards verifying C programs. The Value Analysis provides an overapproximated set of possible values for each occurence of each variable of a C program. I will describe how to guide the value analysis in the example below:

int main(int argc, char* argv[]) {
      int x = argc % 11;
      return 100 / x;
}

We can call the value analysis on this program by issuing frama-c -val smallcprogram.c on the shell. Among other things, the plug-in tells us that x is always in the range from -10 to 10 at the point of the division. Frama-C also warns of a possible division by zero in the argument to return. Great, we had overlooked that. Let us insert a check for this and return 0 in this case.

int main(int argc, char* argv[]) {
       int x = argc % 11;
       if(x != 0)
               return 100 / x;
       else
               return 0;
}

When we call Frama-C again, it gives the same result, including the warning for a possible division by zero. This is despite the division being guarded by the if(x != 0). This time, the alarm is a false alarm.

Explanation

What happened? The Value Analysis plug-in performs an abstract interpretation of the program, with the abstract domain being ranges of integers (the actual abstract domain is more complex, but for this example it is enough to consider this much simpler domain). Apart from the type, the value analysis does not know anything about the variable argc and therefore sets the range of possible values for it to [MININT, MAXINT]. When x is initialized, the set of possible values of the expression argc % 11 is computed, which is [-10,10]. Now it gets interesting. Inside the then block of the if condition, we know that x can have every possible value within [-10,10] except 0. However, in our simplified version of the value analysis it cannot represent [-10,10] \ 0, and therefore overapproximates to [-10,10]. This is precisely the reason why we still get this warning.

Solution

One way to get around this issue is to split the range of possible values of x right before the if condition into two sub-ranges. Luckily, the Value Analysis plug-in allows us to do just that by inserting an assertion:

int main(int argc, char* argv[]) {
       int x = argc % 11;
       /*@ assert x < 0 || x >= 0;*/
       if(x != 0)
               return 100 / x;
       else
               return 0;
}

The plug-in now splits the state propagated through the assert annotation, continues with two independent analyses and later merges the results. To allow this, the parameter -slevel N with N at least two must be passed to Frama-C. With these changes, the range of possible values for the first analysis is [-10,-1] and the second is [0,10]. The first range is not interesting since there is no zero in there and the abstract interpretation will therefore not enter the then block of the if condition. However, it will do this for the second range, but now it can compute a range that includes all of the original elements without zero ([1,10]). Therefore it can now detect that x can not be zero inside the division expression. Everything is fine...

Final thoughts

If you want to track the states of the Value Analysis plug-in, I recommend the special Frama-C functions Frama_C_dump_each() and Frama_C_show_each(). Just insert them in the C file at the position you are interested in.