Frama-C news and ideas

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

Double free(), no such thing

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.

Comments

1. On Thursday, January 5 2012, 17:43 by Anne

Hello Pascal,

Isn't this check a bit to strong ? I don't understand why [q++] above is not permitted... after all, it is just a number, it should just give ESCAPINGADDR again, shouldn't it ? To my point of view, only an access to [*q] (like in [free]) should fail. But I might be wrong...

Anyway, happy new year to you !

2. On Thursday, January 5 2012, 18:23 by pascal

Hello, Anne.

In an intermediate version of this post, the part you refer to contained the additional line "q++ is forbidden in Frama-C, and if think you should be allowed to use it in your program, you should find another analyzer". I'm glad I removed it now. I wouldn't want *you* to use another analyzer.

I will make a second post on free(), I think. To keep the suspense to tolerable levels, I will just say now that if you write the program { int *p; { int a[2]; p = a; } p++; }, which does not use free() but only the already supported block-local variables, Nitrogen warns in exactly the same way. This will be my defense.

3. On Thursday, January 5 2012, 21:51 by _Anne_

Thanks Pascal. Ok : I might still use Frama-C analyzer then ;-)