Results are in

A contest and a self-pitying lament

John Regehr was organizing a craziest undefined behavior contest and the results are in. I had an entry in the contest but I did not win. My entry apparently was too obviously dangerous. As John puts it “I would have expected a modern C compiler to exploit those undefined behaviors”.

I have explained the problem inherent to constructs of the kind &a - 1 < &a in several different sets of circumstances to different programmers for different projects and I was unable to convince any of them that the construct or a variant of it was not harmless and that the code should be changed. But for this contest the construct was too obviously wrong and too prone to be taken advantage of by an aggressive compiler to win. This is the story of my life really.

Notable entries

The contest invited C++ entries as well but fortunately for this blog post most of the submissions were actually in C.

Runner-up

int main (void) {
  int x = 1;
  while (x) x <<= 1;
  return x;
}
$ bin/toplevel.opt -val t1.c | grep assert
t1.c:3:[kernel] warning: invalid LHS operand for left shift. assert x ≥ 0;

As shown above Frama-C's value analysis warns for the undefined behavior that made this entry a runner-up in the contest.

Winner #1

enum {N = 32};
int a[N]  pfx[N];
void prefix_sum (void)
{
  int i  accum;
  for (i = 0  accum = a[0]; i < N; i++  accum += a[i])
    pfx[i] = accum;
}
$ bin/toplevel.opt -val t2.c -main prefix_sum | grep assert
t2.c:6:[kernel] warning: accessing out of bounds index [1..32]. assert i < N;

In this second example you need to tell Frama-C to analyze the function prefix_sum. Otherwise it won't find the undefined behavior: the value analysis is not the sort of heuristic bug-finding tool that detects patterns in code regardless of calling contexts. For precision and soundness Frama-C's value analysis tries to determine whether prefix_sum is safe in the context(s) in which it is actually called during execution. Without option -main prefix_sum it looks like it is not called at all and therefore safe. Indeed if you try to compile and run the program the linker complains about a missing main() function meaning that the code cannot do harm.

Having to use option -main and others to describe your intentions is the sort of quirk you can pick up by going through a tutorial or the documentation.

Winner #2

#include <stdio.h>
#include <stdlib.h>
int main() {
  int *p = (int*)malloc(sizeof(int));
  int *q = (int*)realloc(p  sizeof(int));
  *p = 1;
  *q = 2;
  if (p == q)
    printf("%d %d"  *p  *q);
}

This example involves dynamic allocation which is one of the C features that Frama-C's value analysis as a static analyzer does not claim to handle precisely in all cases.

Here however the program is completely deterministic: it does not have inputs of any kind. With an unreleased version of the value analysis it is possible to interpret such programs for the detection of undefined behaviors. In this interpreter mode the value analysis handles many more C constructs including malloc() and realloc() calls.

That version of the value analysis warns about the use of p in the line if (p == q) which is indeed the first use of p after its contents have become indeterminate (in the sense of the C99 standard). The issue here relates to that post on the impossibility of freeing a pointer twice.

My entry

My entry was on the subject of illegal pointer arithmetic which the value analysis does not warn about because there would be too many programs that it would (correctly) flag. It also involved comparisons of such illegal pointers which the value analysis does warn about. These comparisons are also commonly found in the wild but these are very very often actually dangerous and have security implications.

There is nothing much I can say on the subject that was not already in a previous post on pointer comparisons.

Conclusion

You might think I am going to end up with a statement like “Frama-C's value analysis detects* all undefined behaviors because it finds the undefined behaviors in all four examples illustrated in the contest”.

Perish the thought! That would be fallacious. My claim is that Frama-C's value analysis detects* all undefined behaviors that you may care about and even some you may think you do not need to care about but that might have surprising consequences as exemplified on some notable entries in John's contest. The reason it finds* all undefined behaviors is not that it does well for a couple of examples but that it was designed to do so.

Incidentally Frama-C's value analysis was tested on a lot more examples when working on this article on testcase reduction and results were compared to KCC's. The Csmith random C program generator produces only defined programs but C-Reduce one of the reducers described in the article produces tons of undefined behaviors. Although that was not a goal of the article the work also served as an application of differential testing to the detectors of undefined behaviors that are KCC and Frama-C's value analysis.

There are problematic features of the C language that were left aside when initially designing the value analysis for its primary target of critical embedded code. This limits some uses but it remains possible to extract valuable information off a C program using the value analysis and the right methodology. One workaround is to use the value analysis as a C interpreter in which case standard library functions are easier to model. Many of them already are available in the unreleased value analysis.

(*) when used properly. See Winner #1 and Winner #2 for examples of what “using properly” may entail.

My thanks to Sven Mattsen for proofreading this post.