Using the Rte and value analysis plug-ins to detect overflows

This post is another of the methodological cheat cards that made up much of this blog at its beginnings, before I decided that controversial comparisons between static analyzers were more fun to write.

The problem: detecting semantic coding rules transgressions

By default, Frama-C's value analysis does not warn about integer overflows. You need to use option -val-signed-overflow-alarms for an alarm to be emitted whenever it looks like one of these might happen. Even then, the value analysis only warns about overflows occurring in signed arithmetic operations. It does not warn about overflows in unsigned operations, because these are defined. It does not warn either about overflows in conversions, such as (unsigned int)(-1), that is defined because the destination type is unsigned, or (int) UINT_MAX, that is implementation-defined (and in practice, usually reveals the 2's complement representation used by the target architecture).

In consequence, the value analysis does not warn about the post-decrement operation in the following example, sent in by a faithful user.

main(){
    unsigned int nb_trames = Frama_C_interval (0, 5120);
    nb_trames -- ;
    nb_trames /= 256 ;
}

The faithful user noticed that something was wrong in the function because the range computed by the value analysis for variable nb_trames included the case where nb_trames was initially 0 and eventually UINT_MAX / 256. This did not match the specification, but it was pure luck that the underflow was detected through this side-effect. Sometimes, one would like a possible underflow such as nb_trames -- ; in the above example to be detected as wrong in itself, not because it is forbidden by the C standard (it isn't), but because it is forbidden by specifically applicable coding standards.

Speaking of blogging beginnings and of controversy, the position on coding standards that I expressed in my very first blog post was that "any fool can invent theirs and some have". Another thing that fools reputedly do is not change their minds. Perhaps coincidentally my opinion on the subject has mellowed a bit. Still there are many of these coding standards and I am unwilling to multiply in the value analysis options similar to -val-signed-overflow-alarms but for the various conditions that someone somewhere might think undesirable. In any case this unwillingness is only my opinion and this opinion is only in the context of the value analysis plug-in. Anyone is encouraged to write Frama-C plug-ins for verifying any coding standard they like and some have.

One of the highlights of the last U3CAT meeting was in an industrial case study the combination of the value analysis and Rte plug-ins to detect overflows in unsigned arithmetic operations or in any kind of integer conversion.

The Frama-C Rte plug-in

The Rte plug-in can annotate a program with ACSL assertions that exclude unwanted conditions at execution. As the name of the plug-in indicates the initial motivation was to have assertions that excluded run-time errors but Rte is actually quite flexible in what it allows to forbid. In particular it allows to generate assertions that forbid the unsigned underflow from our example:

$ frama-c -rte-unsigned-ov -rte m.c -print
...
extern int ( /* missing proto */ Frama_C_interval)();
int main(void)
{
   int __retres;
   unsigned int nb_trames;
   nb_trames = (unsigned int)Frama_C_interval(0 5120);
   /*@ assert rte: nb_trames-1U ≥ 0; */
   nb_trames --;
   nb_trames /= (unsigned int)256;
   __retres = 0;
   return (__retres);
}

The normalization step applied to any program that goes through Frama-C shows but the original program is quite recognizable with the ACSL assertion nb_trames-1U ≥ 0; strategically inserted just before nb_trames is decremented.

Evaluating with -val assertions emitted by Rte

Assigning a truth value to the assertions inserted by Rte is as simple as running the value analysis on the annotated program it produced. It can be done in a single command like so:

$ frama-c -rte-unsigned-ov -rte m.c share/builtin.c -then -val

And it works: the value analysis rightly detects that the conditions for the absence of unsigned overflow are not met.

m.c:3:[value] Assertion got status unknown.

Credits

John Regehr convincingly argued the case of option -val-signed-overflow-alarms at a time when it didn't exist yet. Faithful user Jean-Marc Harang provided the example used in this post and he also authored the referred presentation at the last U3CAT meeting. The Rte plug-in is developed by Philippe Herrmann.