Some function allocatedness test are suppressed

[RustanLeino]

A first-class function value f (like a lambda expression or an unapplied member function) can have a body that dereferences the heap, even if f has an empty reads clause. In particular, this can happen if the body contains an expression c.k where c is a reference and k is a const field. Consequently, f should be allowed to be applied only in states where that c is allocated. This is not properly enforced.

Thoughts about a solution

The current axiomatization says that a function f is allocated in a state H iff

either f's precondition does not hold in H,
or every reference in f's reads set in H is allocated in H.

To be correct, the "or" in the previous definition must also include any reference in f's body used to obtain the value of const field. Since such references are not included in the functions reads clause (and for a good reason), the only recourse may be to disallow apply-expressions inside any old expression. This could be accomplished by changing the "iff" in the definition above to "only if" (that is, "implies") (changing BplIff to BplImp on line 9129 of Translator.cs).

A more permissive solution would be to use not just the reads set of a function, but also a (new) "root set". The root set of a lambda function consists of the free local variables of a lambda expression, and consists of the receiver argument to an instance member function. Then, change or "or" part of the definition above to "every reference in f's read set or root set in H is allocated in H". The addition of such a root set would have an effect on the equality of functions. One may also want to expose some syntax for talking about root sets in specifications.

Simple repros

Here are two simple cases that show the problem:

class C {
  const k: int
  function K(): int { k }
}

method Test()
{
  var c := new C;
  if
  case true =>
    var f := () => c.k;
    var x := old(f());  // error: f depends on c.k, and c wasn't allocated in old (BOGUS: no error is reported)
  case true =>
    var g := c.K;
    var x := old(g());  // error: g depends on c.k, and c wasn't allocated in old (BOGUS: no error is reported)
}

Additional test cases

class C {
  const k: int
  const self: C
  constructor (k: int)
    ensures this.k == k && this.self == this
  {
    this.k := k;
    this.self := this;
  }
  function K(): int {
    k
  }
  function Self(): C {
    self
  }
}

method ApplyFunctions()
{
  var c := new C(14);
  if
  case true =>
    var f := () => c.k;
    var x := old(f());  // error: f depends on c.k, and c wasn't allocated in old (BOGUS: not detected)
  case true =>
    var f := c.K;
    var x := old(f());  // error: f depends on c.k, and c wasn't allocated in old (BOGUS: not detected)
  case true =>
    var g := (u: C) => u.k;
    // error: an argument passed to a function inside an old must be allocated in the old state, but
    // argument c in the following line is not
    var x := old(g(c));  // error: c is not available in old (this error is detected)
}

method Badness()
{
  var c := new C(14);
  if
  case true =>
    var y := old(c.k);  // error: c wasn't allocated in old
  case true =>
    var g := () => c.self;
    var x := old(g());  // error: g depends on c.self, and c wasn't allocated in old (BOGUS: not detected)
    assert x == c;
    // the following line is the same line that causes an error in the "then" branch,
    // so *some* error should be reported on the "else" branch as well
    var y := old(c.k);
  case true =>
    var h := c.Self;
    var x := old(h());  // error: h depends on c.self, and c wasn't allocated in old (BOGUS: not detected)
    assert x == c;
    // the following line is the same line that causes an error in the "then" branch,
    // so *some* error should be reported on the "else" branch as well
    var y := old(c.k);
}

method DetectedBadness()
{
  var c := new C(14);
  // Note the "reads" clause in the next line
  var g := () reads c => c.self;
  var x := old(g());  // error: g depends on c.self, and c wasn't allocated in old
}

// The following method shows the seriousness of the problem
method False()
  ensures false
{
  var c := new C(14);
  var g := () => c.self;
  var x := old(g());  // error: g depends on c.self, and c wasn't allocated in old (BOGUS: not detected)
}

[robin-aws]

My preference here, at least in the short term, is the more conservative option of forbidding application inside old(...) expressions, at least without an explicit CLI option.

It seems reasonable to me to remove that functionality by default in the name of soundness, as it seems unlikely any Dafny programs out there are relying on it, as long as the error message very clearly points to the CLI option as a workaround. Later on when we have a fully-designed and sound solution we can make the CLI option on by default.