6.1. Modifies clauses🔗

As previously mentioned, Laurel procedures have a transparent body by default, so callers can reason about the callee's body. This works also when the callee mutates the heap in its body. However, when we make a heap-mutating procedure opaque, and the body is no longer available for reasoning, then the caller must accept the possibility that the entire heap was mutated, meaning that nothing can be proven about the heap any more. This is sound but imprecise, and it makes reasoning about callers of such procedures difficult. To enable heap reasoning after calling opaque heap-mutating procedures, Laurel has modifies clauses.

A modifies clause specifies the heap references that may have been modified by the procedure. Example:

composite Container {
  var value: int
}

procedure bump(c: Container)
  opaque
  modifies c
{
  c#value := c#value + 1
};

procedure caller()
  opaque
{
  var a: Container := new Container;
  var b: Container := new Container;
  var x: int := a#value;
  var y: int := b#value;
  bump(b);
  assert x == a#value;  // holds: only b is in bump's modifies clause
  assert y == b#value   // fails: b is in bump's modifies clause
};

An opaque procedure that writes to an object it has not listed in the modifies clause is rejected, also when this write is done through another procedure call. You can list several references by repeating the clause (modifies c; modifies d), and the wildcard modifies * permits modifying any object — at the cost of telling callers that nothing on the heap is preserved.

Objects allocated with new inside the procedure body are exempt: a freshly allocated object may be modified freely without appearing in the modifies clause, because no caller could hold any prior knowledge about it.

composite Container { var value: int }

procedure makeOne()
  opaque
{
  var c: Container := new Container;
  c#value := 1   // allowed: c is freshly allocated here
};

A modifies clause frames the normal return only. A procedure that can also finish by throwing frames that exit separately, with a throwsOn case's modifies — see Verification - Continued.