Description
CBMC version: 5.67.0
Operating system: N/A
tl/dr. #6887 brings __CPROVER_frees clauses and related predicates to function contracts only, this needs to be extended to loop contracts
Problem description
It is currently is not possible to specify that a memory location can/must be freed.
Proposal
1. Add a new clause __CPROVER_frees(ptr)
Specifies which memory locations may be freed by the function. We reuse the assigns clause syntax for conditional targets.
__CPROVER_frees(cond: ptr1, ptr2)
Just like an assigns clause, the contents of the clause is interpreted at the function call site, pre-invocation.
1.1. Contract checking
Only locations listed in the frees clause can be freed, when their condition holds.
1.2. Contract replacement
For each conditional target cond: target we introduce a witness variable (initially false):
DECL __was_freed_target: bool;
ASSIGN __was_freed_target:= false;
Each conditional target gets turned into a conditional non-deterministic free instruction:
IF(!cond & !__was_freed_target & nondet_bool()) GOTO SKIP_TARGET;
ASSIGN __was_freed_target := true;
// update all other witness variables that may alias
ASSIGN __was_freed_other_target := __CPROVER_same_object(target, other_target);
...
// free the object
CALL free(target);
SKIP_TARGET: SKIP;
To handle aliasing and avoid double free errors, every time free is invoked we update the witness variable of other targets if they alias with the freed pointer.
2. Add a new predicate bool __CPROVER_freeable(void *ptr)
In an assertion context, __CPROVER_freeable(ptr) holds if ptr points to a live heap-allocated object with offset 0.
In an assumption, a pointer can be made freeable in multiple different ways:
- make it nondet and assume it points to a heap object and its offset is zero,
- allocate a fresh object, etc.
We let the user specify how to do that by also adding ptr to the contract assigns clause (will make it nondet), by using is_fresh(ptr), etc.
3. Add a new predicate bool __CPROVER_freed(void *ptr)
In a post condition, __CPROVER_freed(ptr) holds the object pointed to by ptr has been freed during the execution of the function.
Cannot be used in a pre-condition.
If a pointer is reallocated, one might use __CPROVER_freed(__CPROVER_old(ptr)) to refer to the old value of the pointer.
3.1 Contract checking
We introduce a witness variable for each target:
DECL __was_freed_target : bool;
ASSIGN __was_freed_target := __CPROVER_same_object(ptr, target);
We instrument each call to the free (realloc, etc.) with a witness variable.
ASSIGN __was_freed_target := __CPROVER_same_object(ptr, target);
ASSIGN __was_freed_other_target := __CPROVER_same_object(ptr, other_target);
CALL free(ptr);
Each target gets turned into a GOTO assertion inserted as a post-condition:
ASSERT <condition> ==> __was_freed_target;
3.2. Contract replacement
We use the witness variables introduced in 1.2 for contract replacement.
to turn each conditional target an assumption:
ASSUME cond ==> __was_freed_target;