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 Silicon here: viperproject/silicon#656

[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.