Arrays and Pointers

This tutorial explains how to specify arrays and pointers in vercors. Java and PVL support arrays, whereas C and the GPGPU frontends only support pointers. The tutorial assumes you are familiar with arrays and pointers already.

Array permissions

We have learned already how to specify ownership of variables on the heap. Arrays generalize this concept by treating each element of the array as a separate location on the heap. For example, you might specify:

/*@
requires ar != null && ar.length == 3;
context Perm(ar[0], write) ** Perm(ar[1], write) ** Perm(ar[2], write);
*/
void example1(int[] ar);

This means we require the length to be 3, and require and return permission over each of the elements of the array. Length is treated in a special way here: even though it is a "field", we do not need permission to read it, because the length of an array cannot be changed and it is baked into Vercors.

Of course writing a specific length and manually asserting permission over each location is cumbersome, so we can write a contract that accepts arrays of any length as such:

/*@
requires ar != null;
context (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
*/
void example2(int[] ar);

As mentioned in the permissions tutorial, the permissions are combined with ** to Perm(ar[0], write) ** Perm(ar[1], write) ** … ** Perm(ar[ar.length-1], write). Please note the * after forall, which denotes that the body of the forall is combined with separating conjunction (**) and not boolean conjunction (&&).

As you might expect, we can also use forall to specify properties about the values of the array:

/*@
requires ar != null;
context (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
ensures (\forall int i; 0 <= && i < ar.length; ar[i] == i);
*/
void identity(int[] ar) {
    for(int i = 0; i < ar.length; i++)
    /*@
    loop_invariant (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
    loop_invariant (\forall int j; 0 <= j && j < i; ar[j] == j); */
    {
        ar[i] = i;
    }
}

Syntactic sugar

Specifying arrays quickly leads to prefix a lot of statements with \forall* int i; 0 <= i && i < ar.length;, so there is some syntactic sugar. First, you might want to use context_everywhere for the permission specification of the array, so that it is automatically propagates to loop invariants:

/*@
context_everywhere (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
ensures (\forall int i; 0 <= && i < ar.length; ar[i] == i);
*/
void identity(int[] ar) {
    for(int i = 0; i < ar.length; i++)
    /*@
    loop_invariant (\forall int j; 0 <= j && j < i; ar[j] == j); */
    {
        ar[i] = i;
    }
}

This whole forall* can also be written as Perm(ar[*], write), which still means write permission over all the elements of the array:

/*@
requires ar != null;
context_everywhere Perm(ar[*], write);
ensures (\forall int i; 0 <= && i < ar.length; ar[i] == i);
*/
void identity(int[] ar) {
    for(int i = 0; i < ar.length; i++)
    /*@
    loop_invariant (\forall int j; 0 <= j && j < i; ar[j] == j); */
    {
        ar[i] = i;
    }
}

If you want to specify the length of an array, you can write as well: \array(ar, N) which is equivalent to ar != null && ar.length == N. More interestingly, there is also \matrix(mat, M, N), which is equivalent to:

mat != null ** mat.length == M **
(\forall* int i; 0 <= i && i < M; Perm(mat[i], read)) **
(\forall int i; 0 <= i && i < M; mat[i].length == N) **
(\forall int i; 0 <= i && i < M; (\forall int j; 0 <= j && j < M && mat[i] == mat[j]; i == j))

The last line is interesting here. In Java there is no such thing as a true matrix: instead we can make an array of arrays. However, there is nothing preventing you from putting the same row array instance in multiple rows. The last statement says that if we have valid row indices i, j, we know that i != j ==> mat[i] != mat[j] (and the contrapositive).

Pointers

Pointers themselves are quite well-supported, but we don't support casting and structs in C, making the end result quite limited. For the support that we do have, pointers can be specified with two constructs: \pointer and \pointer_index.

We write \pointer(p, size, perm) to express that p != NULL, the pointer p is valid from (at least) 0 to size-1, and we assert perm permission over those locations.

We write \pointer_index(p, index, perm) to express that p != NULL, (p+i) is a valid location, and we have permission perm at that location.

/*@
requires \pointer(a, 10, write);
*/
void test(int *a) {
    //@ assert \pointer(a, 10, write);
    //@ assert \pointer(a, 8, write);
    //@ assert (\forall* int i; 0 <= i && i < 10; \pointer_index(a, i, write));
    int *b = a+5;
    //@ assert a[5] == b[0];
    //@ assert \pointer(b, 5, write);
}

Injectivity, object arrays and efficient verification

This section contains advanced information, and can be skipped on a first read.

Due to a technical limitation in the backend of VerCors, the location denoted by a permission expression in a quantified expression must be unique for each binding of the quantifier. For example, if we write:

class Box {
    int value;

    void test() {
        Box box1 = new Box();
        seq<Box> boxes = seq<Box>{box1, box1};
        exhale (\forall* int i; 0 <= i && i < |boxes|; Perm(boxes[i].value, 1\10));
    }
}

This could be correct: we only exhale 2\10 permission of box1.value. The expression is however not well-formed: i==0 and i==1 cause the expression boxes[i].value to point to the same location. (Please note that it seems that the error from our backend currently is not propagated correctly. Silicon reports "Receiver of boxes[i].value might not be injective." and VerCors translates this into "ExhaleFailed:InsufficientPermission".)

The reason we refer to this as injectivity, is that we should be able to construct a function that assigns bindings for a location, e.g. for a given Box we can either find a unique i that points to the Box, or the Box does not appear in boxes. That function is the inverse of the expression in the Perm. The truth value of a \forall* carries with it this property of injectivity. This means, for example, that in a method definition a requirement assumes that \forall* statements are injective with repsect to locations, whereas we must prove it in ensures statements. This usually follows directly from a requirement. In method invokations then as per usual it's the opposite: we must prove that \forall* statements in the requirements are injective and may assume it for ensures statements.

This limitation is especially important in for example arrays of objects:

class Box {
    int value;

    requires a != null ** (\forall* int i; 0 <= i && i < a.length; Perm(a[i], read));
    requires (\forall* int i; 0 <= i && i < a.length; a[i] != null ** Perm(a[i].value, write));
    void test(Box[] a) {
        
    }

    void foo() {
        Box box = new Box();
        Box[] boxes = new Box[2];
        boxes[0] = box;
        boxes[1] = box;
        test(boxes); // fails
    }
}

In common use however we have to know about duplicate elements anyway. For example, in the example above we require write permission over the boxes, so indirectly we already require all the boxes to be distinct. As for the array elements themselves: we have an internal axiom about arrays that expresses exactly that the locations of an array correspond to only one index and one array.