Open wandernauta opened 2 months ago
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 pointerp
refers, at the labelL
, to the base address of an unallocated memory block.\allocable{id} : void* → boolean
For any pointer
p
and labelL
\allocable{L}(p) <==> (\allocation{L}(p)==\unallocated && (void*)p==(void*)\base_addr{L}(p))
–
\freeable{L}(p)
holds if and only if the pointerp
refers, at the labelL
, 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, despiteNULL
being a valid argument to the C function free.\freeable{id} : void* → boolean
For any pointer
p
and labelL
\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)
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 :-)
The following C program verifies:
However, its behavior is undefined - p is a pointer to a
foo
, but it doesn't point to memory allocated bymalloc
. In practice, on my machine, this aborts: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 ofthing
.