New CBMC syntax needed for assigns clause with quantifiers

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

Problem description

In the assigns clause of loop-contracts and function-contracts, there are cases where we may need some kind of quantifiers to express the full set of assignable memory locations. An example of this is given below. Currently CBMC does not have any syntax to express such assigns clauses.

Ideally, we would like the solution to work in a fully-unbounded setting. Hence the number of constraints generated should be independent of the bounds of the quantified variable. But maybe this is too hard to achieve? A short-term solution can be to generate constraints that are proportional to the quantifier bounds.

Example

This example shows a simplified version of the assigns clause needed for a loop contract in the TaskIncrementTick function (in tasks.c) in the FreeRTOSKernel. It demonstrates a case where we need a quantifier in the assigns clause.

The FreeRTOSKernel code implemented with array-lists (the rewrite with array-lists avoids recursive data-structures like linked-lists for which we cannot write loop contracts in CBMC)can be found here:
https://github.com/akshayutture/FreeRTOS-Kernel/blob/arraylist_task_queue

#include<stdlib.h>
#define STATIC_MAX_CAPACITY 10

typedef struct{
    int field;
} ListItem;

main(){
    // Set the size
    ListItem* listData[STATIC_MAX_CAPACITY];
    size_t dynamic_list_size = nondet_uint();
    __CPROVER_assume(dynamic_list_size < STATIC_MAX_CAPACITY);

    // Allocate all the elements.
    for (int i = 0 ; i <dynamic_list_size ; i++){
        listData[i] = malloc(sizeof(ListItem));
    }

    // Missing syntax for the following assigns clause
    for (int i = 0 ; i < dynamic_list_size ; i++)
    /* new syntax used 
    __CPROVER_assigns (  
        forall i in (0,dynamic_list_size); 
        (0 < dynamic_list_size <= STATIC_MAX_CAPACITY); 
        __CPROVER_assignable(listData[i]->field)
    )*/
    {
        listData[i]->field = 0;
    }
}

[qinheping]

I think their are two approaches for this problem 1) checking if the full set of memory locations are assignable, and 2) non-deterministically choosing one location and checking if it is assignable. We can achieve 2 with conditional assigns clauses. For the above example, the assign clause would be

for (int i = 0 ; i < dynamic_list_size ; i++)
__CPROVER_assigns (  
  (0 < i <= dynamic_list_size) : __CPROVER_typed_target(listData[i]->field))
{
        listData[i]->field = 0;
}

In the GOTO level, we need to check the condition before havocing (note that havocing i should appear first as the later havocing depends on it)

HAVOC(i);
DECL __cond: bool;
ASSIGN __cond = 0 < i <= dynamic_list_size;
IF !__cond GOTO SKIP_HAVOC;
ASSUME is_assignable(&(list[i]->field), sizeof(list[i]->field))
HAVOC(listData[i]->field);
SKIP_HAVOC: SKIP;
DEAD __cond;

, and assignable checks.

DECL __cond: bool;
ASSIGN __cond = 0 < i <= dynamic_list_size;
IF !__cond GOTO SKIP_CHECK;

DECL check_assign: bool;
CALL check_assign = check_assignment(write_set, &(list[i]->field), sizeof(list[i]->field));
ASSERT(check_assign);
DEAD check_assign;

SKIP_CHECK: SKIP;
DEAD __cond;

However, when we want to havoc a set of locations so that we can write loop invariants about them, the approach 2 would not work. For example, if we want to write the following invariant, we need to havoc listData[j]->field for all 0 <= j < i

for (int i = 0 ; i < dynamic_list_size ; i++)
__CPROVER_loop_invariant(
  __CPROVER_forall{int j; (j >= 0 && j < i) ==> listData[j]->field == 0}
)
{
        listData[i]->field = 0;
}