I have been able to divert a few hours yesterday and today for programming. It was well worth it, as I have discovered a theorem. It is new to me, and I wonder whether it was ever published. The theorem is, a C program cannot double free() a block even if it tries! I thought this deserved an announcement. Some students I know would be glad to hear that.


Indeed, a C program can at most pass an indeterminate value to a function. This is highly objectionable in itself. Students, don't write programs that do this either!

Allow me to demonstrate on the following program:

...
main(){
  int *p = malloc(12);
  int *q = p;

  free(p);
  free(q);
}

You might think that the program above double-frees the block allocated and referenced by p. But it doesn't: after the first call to free(), the contents of q are indeterminate, so that it's impossible to free the block a second time. I will insert a few calls to primitive function Frama_C_dump_each() to show what happens:

main(){
  int *p = malloc(12);
  int *q = p;

  Frama_C_dump_each();
  free(p);
  Frama_C_dump_each();
  free(q);
  Frama_C_dump_each();
}

$ frama-c -val this_is_not_a_double_free.c

The analysis follows the control flow of the program. First a block is allocated, and a snapshot of the memory state is printed a first time in the log:

...
[value] computing for function malloc <- main.
        Called from test.c:12.
[value] Recording results for malloc
[value] Done for function malloc
[value] DUMPING STATE of file test.c line 15
        p ∈ {{ &Frama_C_alloc }}
        q ∈ {{ &Frama_C_alloc }}
        =END OF DUMP==
...

Then free() is called and a second snapshot is logged:

...
[value] computing for function free <- main.
        Called from test.c:16.
[value] Recording results for free
[value] Done for function free
[value] DUMPING STATE of file test.c line 17
        p ∈ ESCAPINGADDR
        q ∈ ESCAPINGADDR
        =END OF DUMP==
...

And then, at the critical moment, the program passes an indeterminate value to a function:

...
test.c:18:[kernel] warning: accessing left-value q that contains escaping addresses;
                      assert(Ook)
test.c:18:[kernel] warning: completely undefined value in {{ q -> {0} }} (size:<32>).
test.c:18:[value] Non-termination in evaluation of function call expression argument
        (void *)q
...
[value] Values at end of function main:
          NON TERMINATING FUNCTION

Note how the last call to Frama_C_dump_each() is not even printed. Execution stops at the time of calling the second free(). Generalizing this reasoning to all attempts to call free() twice, we demonstrate it is impossible to double-free a memory block.

QED


Question: does it show too much that this detection uses the same mechanism as the detection for addresses of local variables escaping their scope? I can change the message if it's too confusing. What would a better formulation be?

As I hope I have made clear, the message will be displayed as soon as the program does anything at all with a pointer that has been freed — and indeed, I have not implemented any special check for double frees. The program below is forbidden just the same, and does not get past the q++;

main(){
  int *p = malloc(12);
  int *q = p;

  Frama_C_dump_each();
  free(p);
  q++;
  ...
}

On the other hand, I still have to detect that the program does not free a global variable, something the analysis currently allows to great comical effect. (Hey, I have only had a couple of hours!)

Please leave your thoughts in the comments.