6.2. Aliasing and separation🔗

A variable of composite type holds a reference, not an inline copy of the object's fields. Assigning one such variable to another therefore copies the reference, and both names then denote the same object:

composite Cell {
  var value: int
}

procedure aliasDemo()
  opaque
{
  var x: Cell := new Cell;
  x#value := 0;
  var y: Cell := x;

  assert x == y;
  y#value := 7;
  assert x#value == 7;

  var z: Cell := new Cell;
  assert z != x
};

The write through y is visible through x because both refer to the same object. Note what == means here: on a composite it is reference identity, not field-by-field comparison. Two separately allocated objects with identical fields are not equal, and two new expressions always produce distinct references. (On a datatype, by contrast, equality is structural.)

A field that stores a composite likewise stores a reference. Reading the field copies the current reference out; assigning a new reference to the field changes the object's field, and does not retarget a local that read the old value earlier:

composite Child { var n: int }
composite Owner { var child: Child }

procedure fieldReferences(owner: Owner, replacement: Child)
  opaque
  modifies owner#child
{
  var saved: Child := owner#child;
  owner#child := replacement;
  assert owner#child == replacement
  // `saved` still denotes the original child
};

6.2.1. Separation is shallow🔗

This is the point that most often causes a proof to fail unexpectedly. Reference inequality is only root separation: from left != right Laurel does not conclude anything about the objects reachable from their fields. Two distinct objects may perfectly well share a child, and the following two facts are consistent:

requires left != right
requires left#next == right#next

Frame clauses are identity-based in the same shallow way. modifies x permits every field of the object identified by x; it does not permit mutating an object stored in one of those fields. A reachable child has to be named separately. And because frames name objects by identity, aliasing interacts with them the way you would hope: if x == y, a write through y is a write to the object named by x, so naming x in the frame suffices.

composite Cell2 { var value: int }

procedure writeAlias(x: Cell2, y: Cell2)
  requires x == y
  opaque
  modifies x#value
{
  y#value := 1
};

Laurel has no native separation logic: there is no separating conjunction, no ownership or permission system, no heaplets, no built-in reachability relation, and no automatic footprint computation. Deep separation has to be stated as an ordinary first-order property. If a front end supplies maps representing two object footprints, disjointness takes this shape:

forall(r: Node) =>
  !(mapContains(leftFootprint, r) && mapContains(rightFootprint, r))

The front end must also supply the contracts or axioms that connect those maps to the fields they are meant to describe. A finite, fixed object shape can use an explicitly enumerated footprint; a recursive structure needs a generated inductive summary, an axiomatised reachability relation, a bounded approximation, or a proof strategy that avoids materialising reachability at all.

6.2.2. Encoding an analysis's alias facts🔗

A front end that has alias information from its own analysis should map it onto Laurel constraints rather than onto source-language equality — in particular, do not use the source language's == to state identity unless that operator is object identity. For a source type modelled as a datatype over composite variants, write an identity helper that reaches through the variants and compares the underlying references.

Abstract alias fact	Laurel constraint
must alias	`sameRef(x, y)`
definitely separate	`!sameRef(x, y)`
may alias	no constraint either way
points-to allocation site	a separate tag or set-membership constraint, not identity

A may-alias edge records uncertainty, so it must not be turned into an equality; conversely, the absence of a may-alias edge justifies !sameRef(x, y) only if the analysis defines absence as proved non-aliasing. Allocation-site tags are abstractions, not identities: two objects allocated by different iterations of the same loop share a site tag while having different references.