Unexpected verification failure with heap-dependent triggers and old

[viper-admin]

Created by @mschwerhoff on 2018-11-25 11:50
Last updated on 2018-11-25 12:02

The following incorrectly fails to verify in Silicon:

predicate P(r: Ref, x: Int)

function P_state(r: Ref, x: Int): Int
  requires P(r, x)

method test01() {
  var rs: Seq[Ref]
  var xs: Seq[Int]

  inhale forall r: Ref, x: Int :: {P(r, x)} r in rs && x in xs ==> acc(P(r, x))

  label pre_havoc

  exhale forall r: Ref, x: Int :: {P(r, x)} acc(P(r, x), old[pre_havoc](perm(P(r, x))))
  inhale forall r: Ref, x: Int :: {P(r, x)} acc(P(r, x), old[pre_havoc](perm(P(r, x))))

  inhale forall r: Ref, x: Int ::
    none < old[pre_havoc](perm(P(r, x))) ==> 
      P_state(r, x) != 0 // UNEXPECTED ERROR: Insufficient permission to P(r, x)
}

Potentially related: #361

[viper-admin]

@mschwerhoff commented on 2018-11-25 12:02

Observation:

• The code verifies if the explicit triggers are removed

• Changing none < old[pre_havoc](perm(P(r, x))) to none < perm(P(r, x)) in the last inhale doesn't affect the result

• Changing the exhale-inhale statement pair that havocs all instances of P to

    exhale forall r: Ref, x: Int :: {P(r, x)} r in rs && x in xs ==> acc(P(r, x))
    inhale forall r: Ref, x: Int :: {P(r, x)} acc(P(r, x), old[pre_havoc](perm(P(r, x))))
  

  makes the code verify

• Replacing the final inhale with

    assert forall r: Ref, x: Int ::
      none < old[pre_havoc](perm(P(r, x))) ==> 
      // none < perm(P(r, x)) ==>
      // r in rs && x in xs ==> 
        acc(P(r, x))
  

  does not verify either (for none of the commented alternatives)