Spurious Frame Condition Violation with Nested Reference Types

Dafny version

4.2.0

Code to produce this issue

class Ref<T> {
  var val: T

  constructor(val: T) {
    this.val := val;
  }
}

datatype X = X(inner: Ref<Ref<int>>)

class Test {
  var x: X

  twostate predicate SameOrNewRefs()
    reads `x
    reads x.inner
    reads x.inner.val
  {
    || x.inner.val == old(x.inner.val)
    || fresh(x.inner.val)
  }

  constructor() {
    var tmp0 := new Ref(0);
    var tmp1 := new Ref(tmp0);
    x := X(tmp1);
  }

  method M1()
    modifies x.inner.val
    ensures SameOrNewRefs()
  {
    M2();
    M3();
  }

  method M2()
    // ensures SameOrNewRefs() // uncomment to solve the problem
  {}

  method M3()
    modifies x.inner.val
    ensures SameOrNewRefs()
  {}
}

Command to run and resulting output

Test.dfy(34,4): Error: call might violate context's modifies clause
   |
34 |     M3();
   |     ^^^^^

What happened?

My guess as to what's happening is that Dafny thinks M2 might update x.inner.val to point to a different Ref<int> that isn't covered by M1's modifies, so the call to M3 may violate M1's frame condition. But that's impossible because M2 can't modify anything.

Adding SameOrNewRefs to M2's postcondition convinces Dafny that the reference is either unchanged or newly allocated and the error goes away. However, I'd expect it to be able to figure that out without any hints. The issue seems also to be related to the depth of the nested references. Removing one level of Ref in inner's type, or replacing X with type X = Ref<Ref<int>> also fixes the error without the need for SameOrNewRefs.

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

Mac

dafny-lang / dafny