Unsoundness of old expressions in magic wands in postconditions

[alexanderjsummers]

It seems that an "old" expression in a magic wand (RHS) in the postcondition of the called method is wrongly interpreted as referring to the old state of the caller rather than the callee. This is of course unsound; one possible example is below (the assert statements make clear that the "wrong" wand is considered held by the verifier):

field left : Int
field right : Int

predicate T(x:Ref) {
    acc(x.left) && acc(x.right)
}

predicate set(s:Ref) // idea: set of T

function contains(s:Ref, x:Ref) : Bool 
  requires set(s)

define set_with_contents(s) (set(s) && forall r:Ref :: contains(s,r) ==> T(r))  

method add(s:Ref, x:Ref)
  requires set_with_contents(s) && (!contains(s,x) ==> T(x))
  ensures set_with_contents(s) && (forall r:Ref :: contains(s,r) <==> (old(contains(s,r)) || r == x))

// borrow one T(x) from the set:
define borrow_wand(x,s) (T(x) --* ((set(s) && forall r:Ref :: contains(s,r) ==> T(r)) && forall r:Ref :: (contains(s,r) <==> old(contains(s,r)))))

method borrow_element(s:Ref, x:Ref)
  requires set_with_contents(s) && contains(s,x)
  ensures T(x) && borrow_wand(x,s)

method mess_with_set_abstractly(s:Ref, x:Ref)
  requires set_with_contents(s) && !contains(s,x) && T(x)
  ensures set_with_contents(s)
  {
    add(s,x)
    // FAILS, as it should: 
    // assert forall r:Ref :: contains(s,r) <==> old(contains(s,r))
    label l
    borrow_element(s,x)
    // SHOULD PASS, but does not:
    //assert (T(x) --* ((set(s) && forall r:Ref :: contains(s,r) ==> T(r)) && forall r:Ref :: (contains(s,r) <==> old[l](contains(s,r)))))
    // PASSES, but should not:
    //assert (T(x) --* ((set(s) && forall r:Ref :: contains(s,r) ==> T(r)) && forall r:Ref :: (contains(s,r) <==> old(contains(s,r)))))
    unfold T(x)
    x.left := x.right
    fold T(x)
    apply borrow_wand(x,s)
    // SHOULD NOT VERIFY (but does; cannot obviously assert false, however)
    assert forall r:Ref :: contains(s,r) <==> old(contains(s,r))
  }

[alexanderjsummers]

Same issue posted for Carbon here: viperproject/carbon#437

[alexanderjsummers]

It could be that the code in viper.silver.ast.MagicWand.structure should be adapted; the "identity" of the old state used is not considered a "hole" in the structure generated. I'm not exactly sure how that adaptation would work though, since there isn't necessarily a syntactic label corresponding to the "just before the called method" state.

[JonasAlaif]

@marcoeilers would this be possible to fix? I'm running into what I think is the same issue with the following minimized example:

field f: Int

method test(x: Ref) returns (r: Int)
  requires acc(x.f)
  ensures r == old(x.f)
{
  r := x.f
}

method foo(x: Ref) {
  package acc(x.f) --* true {
    var tmp: Int
    tmp := test(x) // Error here, caused by the *ensures*!
  }
}

[marcoeilers]

I'll look at it tomorrow.

[marcoeilers]

@JonasAlaif That seems to be a separate issue, I've filed an issue for it here: #698