Pointers to nonheap objects can be passed to free in C

[wandernauta]

The following C program verifies:

#include <stdlib.h>

struct foo {
  int bar;
};

int main() {
    struct foo thing;
    struct foo *p = &thing; //
    free(p);
}

However, its behavior is undefined - p is a pointer to a foo, but it doesn't point to memory allocated by malloc. In practice, on my machine, this aborts:

free(): invalid pointer
Aborted (core dumped)

The TrivialAddrOf rewriter seems to understand the line indicated // as "create a new one-element pointer array (on the heap) and assign a value into it", but that fictional array does not exist in the actual program, p is "just" the address of thing.

[superaxander]

Indeed we currently do not keep track of the origin of pointers. We should look at how other verifiers do this.

For example in VeriFast you can have:

#include <stdlib.h>

void foo(int a) 
//@ requires true;
//@ ensures true;
{}

void test(int *a)
//@ requires integer(a, _) &*& malloc_block_ints(a, 1);
//@ ensures true;
{
    foo(*a);
    free(a);
}

where integer(a, _) matches our Perm(a, write) and malloc_block_ints(a, n) is a predicate inhaled whenever malloc is called to create a pointer to n integers.

In ACSL (Frama-C) there are separate allocation clauses to describe the behaviour of a function as described in the ACSL Manual paragraph 2.7.3:

– \allocable{L}(p) holds if and only if the pointer p refers, at the label L, to the base address of an unallocated memory block.

\allocable{id} : void* → boolean

For any pointer p and label L

\allocable{L}(p) <==> (\allocation{L}(p)==\unallocated && (void*)p==(void*)\base_addr{L}(p))

– \freeable{L}(p) holds if and only if the pointer p refers, at the label L, to the base address of an allocated memory block that can be safely released using the C function free. Note that \freeable(\null) does not hold, despite NULL being a valid argument to the C function free.

\freeable{id} : void* → boolean

For any pointer p and label L

\freeable{L}(p) <==> (\allocation{L}(p)==\dynamic && (void*)p==(void*)\base_addr{L}(p))

I think I would prefer the simplicity of the VeriFast approach here. I don't think we'd have much benefit from keeping track of whether certain addresses are "allocable" since we don't reason about addresses anyway. (Frama-C basically just keeps track of a map from addresses to values to implement their pointers whereas we use Viper's fields)

[pieter-bos]

Indeed we currently do not keep track of the origin of pointers.

This is actually the point of blocks: it is intended that free requires something like:

p != NULL ==> (\pointer_block_offset(p) == 0 ** (\forall* int i=0..\pointer_block_length(p); Perm(p+i, write)))

I think this is in fact based on \base_addr from ACSL, but it's been a while by now :-)