5.3. Aliasing helpers🔗

Potential aliasing of heap-allocated objects can make verification more complicated. Laurel contains two related notions to make it easier to specify which references are disjoint. A reference is allocated (in a given state) when it already exists in that state's heap; internally this is the condition that the reference predates the state's allocation counter. A reference is fresh when it is the negation of that: newly created by the procedure and therefore not allocated in the pre-state.

Today only fresh has surface syntax — the fresh(e) predicate, which may only target reference (impure composite) types. It is exactly what a caller needs to conclude that a returned reference cannot alias anything that was already allocated.

procedure allocate() returns (r: Node)
  opaque
  ensures fresh(r)
{
  return new Node
};

procedure usesAllocate(existing: Node) {
  var created: Node := allocate();
  assert created != existing   // holds: `fresh(r)` tells the caller `created`
                               // is distinct from every object that already existed
};

Because allocate ensures fresh(r), the caller learns that created was newly allocated and therefore cannot alias existing, or any other reference that was already allocated before the call, without the caller having to track allocation itself.

An allocated(e) predicate is planned as the dual of fresh. Where fresh(e) asserts a reference is new, allocated(e) will assert that a reference already existed in the current state's heap — useful, for example, in a precondition that requires an argument to be a pre-existing object rather than a fresh one. The following sketch (syntax illustrative — allocated is not yet implemented) shows the intended shape:

// syntax illustrative — `allocated` is planned, not yet implemented
procedure store(container: Container, item: Node)
  requires allocated(item)   // reject fresh items; only pre-existing ones may be stored
  opaque
  modifies container
{
  container#head := item
};