Fractions/predicates example consumes too many permissions

[viper-admin]

Created by @mschwerhoff on 2015-12-03 14:42 Last updated on 2017-11-22 08:53

In the attached file, the package removes too many permissions to l.next.next

Arguably, the reason is that at the point where the folding is evaluated, it is not yet known that x == l.next in the wand RHS, since this fact does not come from the wand LHS. Once the RHS is fully processed, however, it becomes clear that 1/2 permission to l.next must come from the current state, and so the value must be the same.

In a sense, the permissions needed for the folding are taken "too early", before all of the knowledge from the footprint state is available. It doesn't seem clear how to fix this and still have a left-to-right evaluation (once) of the RHS.

---

Attachments:

• issue-08.sil

[viper-admin]

@mschwerhoff commented on 2015-12-03 14:42

Depending on the original use-case, a potential work-around would be to strengthen the LHS:

package
  acc(l.next,1/2) && acc(l.next.next,1/2) && x == l.next
    --*
  folding acc(P(x)) in acc(P(x)) && acc(l.next)

The additional conjunct x == l.next makes the example verify.

[viper-admin]

@mschwerhoff commented on 2017-11-22 08:53

New syntax, same (incorrect) behaviour:

field next : Ref;

predicate P(x:Ref) { acc(x.next) }

method m(l:Ref)
  requires acc(l.next) && acc(l.next.next)
{
  var x:Ref := l.next

  package acc(l.next,1/2) && acc(l.next.next,1/2) /* && x == l.next */ --* acc(P(x)) && acc(l.next) {
     fold acc(P(x))
  }

  assert acc(l.next,1/2) && acc(l.next.next,1/2)
}