Add __CPROVER_ensures_frees(ptr; ... ) clauses to loop contracts

[feliperodri]

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;

[remi-delmas-3000]

The current version of CBMC supports frees clauses and related predicates as documented here:
https://diffblue.github.io/cbmc/contracts-frees.html