Function in reads clause can undetectedly depend on allocation state

[RustanLeino]

Dafny version

3.12.0.50221

Code to produce this issue

class C { }

function G(): int
  // The following line is equivalent to
  //     reads set c: C, obj: object | obj in M(c) :: obj
  // and should therefore be disallowed.
  reads M
{
  5
}

function M(x: C): set<object> {
  {x}
}

ghost method Test()
  ensures false
{
  var gr := G.reads();
  var c := new C;
  assert c in M(c);
  assert c in gr;
}

Command to run and resulting output

% dafny test.dfy

Dafny program verifier finished with 3 verified, 0 errors
Compiled assembly into test.dll

What happened?

Dafny allows a reads clause to list not only objects and sets of objects (like a modifies clause does), but also functions to objects or sets of objects. The primary motivation for this is to allow

reads f.reads

where f is a parameter to the enclosing function. (Note that f.reads is a function from the argument types of f to set<object>.)

So, a reads clause like the reads M in the repro above is desugared into a "big union", which is notated as a generalized set comprehension in Dafny:

reads set c: C, obj: object | obj in M(c) :: obj

If this reads clause was given this way by the programmer, Dafny would depend that the set comprehension depends on the allocation state--in particular, the set comprehension ranges over all allocated c: C values. (Note that the range of obj: object is not a problem, since it is constrained by the expression obj in ....)

Dafny should disallow a function M in a reads clause if that function M has in-parameters that may contain references.

Because of this missing check, it is possible to prove false, as exhibited by the postcondition of method Test() above.

What type of operating system are you experiencing the problem on?

Mac