Ownership of Compound Objects

So far, our examples have worked with just integers and pointers, but larger programs typically also manipulate compound values, often represented using C struct types. Specifying functions manipulating structs works in much the same way as with basic types.

For instance, the following example uses a struct point to represent a point in two-dimensional space. The function transpose swaps a point’s x and y coordinates.

exercises/transpose.c

struct point { int x; int y; };

void transpose (struct point *p) 
/*@ requires take P = Owned<struct point>(p);
    ensures take P_post = Owned<struct point>(p);
            P_post.x == P.y;
            P_post.y == P.x;
@*/
{
  int temp_x = p->x;
  int temp_y = p->y;
  p->x = temp_y;
  p->y = temp_x;
}

Here the precondition asserts ownership for p, at type struct point; the output P_post is a value of CN type struct point, i.e. a record with members i32 x and i32 y. The postcondition similarly asserts ownership of p, with output P_post, and asserts the coordinates have been swapped, by referring to the members of P and P_post individually.

Compound Owned and Block resources

While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to individual struct members and manipulate these as values, including even passing them to other functions.

CN therefore cannot treat resources for compound C types like structs as primitive, indivisible units. Instead, Owned<T> and Block<T> are defined inductively on the structure of the C-type T.

For struct types T, the Owned<T> resource is defined as the collection of Owned resources for its members (as well as Block resources for any padding bytes in-between them). The resource Block<T>, similarly, is made up of Block resources for all members (and padding bytes).

To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and it can recompose the struct later, as needed. The following example illustrates this.

Recall the function zero from our earlier exercise. It takes an int pointer to uninitialised memory, with Block<int> ownership, and initialises the value to zero, returning an Owned<int> resource with output 0.

Now consider the function init_point, shown below, which takes a pointer p to a struct point and zero-initialises its members by calling zero twice, once with a pointer to struct member x, and once with a pointer to y.

exercises/init_point.c

void zero (int *coord) 
/*@ requires take Coord = Block<int>(coord);
    ensures take Coord_post = Owned<int>(coord);
            Coord_post == 0i32; @*/
{
  *coord = 0;
}

struct point { int x; int y; };

void init_point(struct point *p) 
/*@ requires take P = Block<struct point>(p);
    ensures take P_post = Owned<struct point>(p);
            P_post.x == 0i32;
            P_post.y == 0i32;
@*/
{
  zero(&p->x);
  zero(&p->y);
}

As stated in its precondition, init_point receives ownership Block<struct point>(p). The zero function, however, works on int pointers and requires Block<int> ownership.

CN can prove the calls to zero with &p->x and &p->y are safe because it decomposes the Block<struct point>(p) into a Block<int> for member x and a Block<int> for member y. Later, the reverse happens: following the two calls to zero, as per zero’s precondition, init_point has ownership of two adjacent Owned<int> resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of init_point requires ownership Owned<struct point>(p), CN combines these back into a compound resource. The resulting Owned<point struct> resource has for an output the struct value P_post that is composed of the zeroed member values for x and y.

Resource inference

To handle the required resource inference, CN "eagerly" decomposes all struct resources into resources for the struct members, and "lazily" re-composes them as needed.

We can see this if, for instance, we experimentally change the transpose example from above to force a type error. Let’s insert an /*@ assert(false) @*/ CN assertion in the middle of the transpose function, so we can inspect CN’s proof context shown in the error report. (More on CN assertions later.)

exercises/transpose.broken.c

struct point { int x; int y; };

void transpose (struct point *p) 
/*@ requires take P = Owned<struct point>(p);
    ensures take P_post = Owned<struct point>(p);
            P_post.x == P.y;
            P_post.y == P.x;
@*/
{
  int temp_x = p->x;
  int temp_y = p->y;
  /*@ assert(false); @*/
  p->x = temp_y;
  p->y = temp_x;
}

The precondition of transpose asserts ownership of an Owned<struct point>(p) resource. The error report now instead lists under "Available resources" two resources:

• Owned<signed int>(member_shift<point>(p, x)) with output P.x and

• Owned<signed int>(member_shift<point>(p, y)) with output P.y

Here member_shift<s>(p,m) is the CN expression that constructs, from a struct s pointer p, the "shifted" pointer for its member m.

When the function returns, the two member resources are recombined "on demand" to satisfy the postcondition Owned<struct point>(p).

Exercises

Init point. Insert CN assert(false) statements in different statement positions of init_point and check how the available resources evolve.

Transpose (again). Recreate the transpose function from before, now using the swap function verified earlier (for struct upoint, with unsigned member values).

exercises/transpose2.c

void swap (unsigned int *p, unsigned int *q)
/*@ requires take P = Owned<unsigned int>(p);
             take Q = Owned<unsigned int>(q);
    ensures  take P_post = Owned<unsigned int>(p);
             take Q_post = Owned<unsigned int>(q);
             P_post == Q && Q_post == P;
@*/
{
  unsigned int m = *p;
  unsigned int n = *q;
  *p = n;
  *q = m;
}

struct upoint { unsigned int x; unsigned int y; };

void transpose2 (struct upoint *p)
{
  swap(&p->x, &p->y);
}