Lists

Now it's time to look at some more interesting heap structures.

To begin with, here is a C definition for linked list cells, together with allocation and deallocation functions:

exercises/list/c_types.h

struct sllist {
  int head;
  struct sllist* tail;
};

extern struct sllist *malloc__sllist();
/*@ spec malloc__sllist();
    requires true;
    ensures take R = Block<struct sllist>(return);
@*/

extern void free__sllist (struct sllist *p);
/*@ spec free__sllist(pointer p);
    requires take P = Block<struct sllist>(p);
    ensures true;
@*/

To write specifications for C functions that manipulate lists, we need to define a CN "predicate" that describes specification-level list structures, as one would do in ML, Haskell, or Coq. We use the datatype List for CN-level lists.

Intuitively, the SLList_At predicate walks over a singly-linked pointer structure in the C heap and extracts an Owned version of the CN-level list that it represents.

exercises/list/cn_types.h

/*@
datatype List {
  Nil {},
  Cons {i32 Head, datatype List Tail}
}

predicate (datatype List) SLList_At(pointer p) {
  if (is_null(p)) {
    return Nil{};
  } else {
    take H = Owned<struct sllist>(p);
    take T = SLList_At(H.tail);
    return (Cons { Head: H.head, Tail: T });
  }
}
@*/

We can also write functions on CN-level lists by ordinary functional programming (in a slightly strange, unholy-union-of-C-and-Rust syntax):

exercises/list/hdtl.h

/*@
function (i32) Hd (datatype List L) {
  match L {
    Nil {} => {
      0i32
    }
    Cons {Head : H, Tail : _} => {
      H
    }
  }
}

function (datatype List) Tl (datatype List L) {
  match L {
    Nil {} => {
      Nil{}
    }
    Cons {Head : _, Tail : T} => {
      T
    }
  }
}
@*/

We use the SLList_At predicate to specify functions returning the empty list and the cons of a number and a list.

exercises/list/constructors.h

struct sllist* slnil()
/*@ ensures take Ret = SLList_At(return);
            Ret == Nil{};
 @*/
{
  return 0;
}

struct sllist* slcons(int h, struct sllist* t)
/*@ requires take T = SLList_At(t);
    ensures take Ret = SLList_At(return);
            Ret == Cons{ Head: h, Tail: T};
 @*/
{
  struct sllist *p = malloc__sllist();
  p->head = h;
  p->tail = t;
  return p;
}

Finally, we can collect all this stuff into a single header file. (We add the usual C #ifndef gorp to avoid complaints from the compiler if it happens to get included twice from the same source file later.)

exercises/list/headers.h

#ifndef _LIST_H
#define _LIST_H

#include "./c_types.h"
#include "./cn_types.h"
#include "./hdtl.h"
#include "./constructors.h"

#endif //_LIST_H

Append

With this basic infrastructure in place, we can start specifying and verifying list-manipulating functions. First, append.

Here is its specification (in a separate file, because we'll want to use it multiple times below.)

exercises/list/append.h

/*@
function [rec] (datatype List) Append(datatype List L1, datatype List L2) {
  match L1 {
    Nil {} => {
      L2
    }
    Cons {Head : H, Tail : T}  => {
      Cons {Head: H, Tail: Append(T, L2)}
    }
  }
}
@*/

Here is a simple destructive append function. Note the two uses of the unfold annotation in the body, which are needed to help the CN typechecker. The unfold annotation is an instruction to CN to replace a call to a recursive (CN) function (in this case append) with its definition, and is necessary because CN is unable to automatically determine when and where to expand recursive definitions on its own.

exercises/list/append.c

#include "./headers.h"
#include "./append.h"

struct sllist* IntList_append(struct sllist* xs, struct sllist* ys)
/*@ requires take L1 = SLList_At(xs);
             take L2 = SLList_At(ys); @*/
/*@ ensures take L3 = SLList_At(return);
            L3 == Append(L1, L2); @*/
{
  if (xs == 0) {
    /*@ unfold Append(L1, L2); @*/
    return ys;
  } else {
    /*@ unfold Append(L1, L2); @*/
    struct sllist *new_tail = IntList_append(xs->tail, ys);
    xs->tail = new_tail;
    return xs;
  }
}

List copy

Here is an allocating list copy function with a pleasantly light annotation burden.

exercises/list/copy.c

#include "./headers.h"

struct sllist* slcopy (struct sllist *l)
/*@ requires take L = SLList_At(l);
    ensures take L_ = SLList_At(l);
            take Ret = SLList_At(return);
            L == L_;
            L == Ret;
@*/
{
  if (l == 0) {
    return slnil();
  } else {
    struct sllist *new_tail = slcopy(l->tail);
    return slcons(l->head, new_tail);
  }
}

Merge sort

Finally, here is a slightly tricky in-place version of merge sort that avoids allocating any new list cells in the splitting step by taking alternate cells from the original list and linking them together into two new lists of roughly equal lengths.

exercises/list/mergesort.c

#include "./headers.h"

/*@
function [rec] ({datatype List fst, datatype List snd}) 
                 split (datatype List xs)
{
  match xs {
    Nil {} => {
      {fst: Nil{}, snd: Nil{}}
    }
    Cons {Head: h1, Tail: Nil{}} => {
      {fst: Nil{}, snd: xs}
    }
    Cons {Head: h1, Tail: Cons {Head : h2, Tail : tl2 }} => {
      let P = split(tl2);
      {fst: Cons { Head: h1, Tail: P.fst},
       snd: Cons { Head: h2, Tail: P.snd}}
    }
  }
}

function [rec] (datatype List) merge(datatype List xs, datatype List ys) {
  match xs {
      Nil {} => { ys }
      Cons {Head: x, Tail: xs1} => {
        match ys {
          Nil {} => { xs }
          Cons{ Head: y, Tail: ys1} => {
            (x < y) ?
              (Cons{ Head: x, Tail: merge(xs1, ys) })
            : (Cons{ Head: y, Tail: merge(xs, ys1) })
          }
        }
      }
  }
}

function [rec] (datatype List) mergesort(datatype List xs) {
  match xs {
      Nil{} => { xs }
      Cons{Head: x, Tail: Nil{}} => { xs }
      Cons{Head: x, Tail: Cons{Head: y, Tail: zs}} => {
        let P = split(xs);
        let L1 = mergesort(P.fst);
        let L2 = mergesort(P.snd);
        merge(L1, L2)
      }
    }
}
@*/

struct sllist_pair {
  struct sllist* fst;
  struct sllist* snd;
};

struct sllist_pair split(struct sllist *xs)
/*@ requires take Xs = SLList_At(xs); @*/
/*@ ensures take Ys = SLList_At(return.fst); @*/
/*@ ensures take Zs = SLList_At(return.snd); @*/
/*@ ensures {fst: Ys, snd: Zs} == split(Xs); @*/
{
  if (xs == 0) {
    /*@ unfold split(Xs); @*/
    struct sllist_pair r = {.fst = 0, .snd = 0};
    return r;
  } else {
    struct sllist *cdr = xs -> tail;
    if (cdr == 0) {
      /*@ unfold split(Xs); @*/
      struct sllist_pair r = {.fst = 0, .snd = xs};
      return r;
    } else {
      /*@ unfold split(Xs); @*/
      struct sllist_pair p = split(cdr->tail);
      xs->tail = p.fst;
      cdr->tail = p.snd;
      struct sllist_pair r = {.fst = xs, .snd = cdr};
      return r;
    }
  }
}

struct sllist* merge(struct sllist *xs, struct sllist *ys)
/*@ requires take Xs = SLList_At(xs); @*/
/*@ requires take Ys = SLList_At(ys); @*/
/*@ ensures take Zs = SLList_At(return); @*/
/*@ ensures Zs == merge(Xs, Ys); @*/
{
  if (xs == 0) {
    /*@ unfold merge(Xs, Ys); @*/
    return ys;
  } else {
    /*@ unfold merge(Xs, Ys); @*/
    if (ys == 0) {
      /*@ unfold merge(Xs, Ys); @*/
      return xs;
    } else {
      /*@ unfold merge(Xs, Ys); @*/
      if (xs->head < ys->head) {
        struct sllist *zs = merge(xs->tail, ys);
        xs->tail = zs;
        return xs;
      } else {
        struct sllist *zs = merge(xs, ys->tail);
        ys->tail = zs;
        return ys;
      }
    }
  }
}

struct sllist* mergesort(struct sllist *xs)
/*@ requires take Xs = SLList_At(xs); @*/
/*@ ensures take Ys = SLList_At(return); @*/
/*@ ensures Ys == mergesort(Xs); @*/
{
  if (xs == 0) {
    /*@ unfold mergesort(Xs); @*/
    return xs;
  } else {
    struct sllist *tail = xs->tail;
    if (tail == 0) {
      /*@ unfold mergesort(Xs); @*/
      return xs;
    } else {
      /*@ unfold mergesort(Xs); @*/
      struct sllist_pair p = split(xs);
      p.fst = mergesort(p.fst);
      p.snd = mergesort(p.snd);
      return merge(p.fst, p.snd);
    }
  }
}

Exercises

Allocating append. Fill in the CN annotations on IntList_append2. (You will need some in the body as well as at the top.)

exercises/list/append2.c

#include "./headers.h"
#include "./append.h"

struct sllist* IntList_copy (struct sllist *xs)
/*@ requires take Xs = SLList_At(xs);
    ensures take Xs_post = SLList_At(xs);
            take R = SLList_At(return);
            Xs == Xs_post;
            Xs == R;
@*/
{
  if (xs == 0) {
    return slnil();
  } else {
    struct sllist *new_tail = IntList_copy(xs->tail);
    return slcons(xs->head, new_tail);
  }
}

struct sllist* IntList_append2 (struct sllist *xs, struct sllist *ys)
{
  if (xs == 0) {
    return IntList_copy(ys);
  } else {
    struct sllist *new_tail = IntList_append2(xs->tail, ys);
    return slcons(xs->head, new_tail);
  }
}

Note that it would not make sense to do the usual functional-programming trick of copying xs but sharing ys. (Why?)

Length. Add annotations as appropriate:

exercises/list/length.c

#include "./headers.h"

unsigned int length (struct sllist *l)
{
  if (l == 0) {
    return 0;
  } else {
    return 1 + length(l->tail);
  }
}

List deallocation. Fill in the body of the following procedure and add annotations as appropriate:

exercises/list/free.c

#include "./headers.h"

void free__rec_sllist(struct sllist* l)
// You fill in the rest...

Length with an accumulator. Add annotations as appropriate:

exercises/slf_length_acc.c

#include "list/headers.h"
#include "ref.h"
#include "free.h"

/*@
function [rec] (u32) length(datatype List xs) {
  match xs {
    Nil {} => {
      0u32
    }
    Cons {Head: h, Tail: zs}  => {
      1u32 + length(zs)
    }
  }
}
@*/

void IntList_length_acc_aux (struct sllist *xs, unsigned int *p)
/*@ requires take L1 = SLList_At(xs);
             take P = Owned<unsigned int>(p);
    ensures take L1_post = SLList_At(xs);
            take P_post = Owned<unsigned int>(p);
            L1 == L1_post;
            P_post == P + length(L1);
@*/
{
  /*@ unfold length(L1); @*/
  if (xs == 0) {
  } else {
    *p = *p + 1;
    IntList_length_acc_aux (xs->tail, p);
  }
}

unsigned int IntList_length_acc (struct sllist *xs)
/*@ requires take Xs = SLList_At(xs);
    ensures take Xs_post = SLList_At(xs);
            Xs == Xs_post;
            return == length(Xs);
@*/
{
  unsigned int *p = refUnsignedInt(0);
  IntList_length_acc_aux(xs, p);
  unsigned int x = *p;
  freeUnsignedInt(p);
  return x;
}