Example of quantified permissions not matching carbon

[ejconlon]

The following program verifies under carbon but not silicon:

Loop invariant (forall r: Ref :: { r.next } (r in nodes) ==> acc(r.next, write)) && (forall r: Ref :: { r.next } (r in nodes) ==> acc(r.val, write)) && (forall r: Ref :: { r.next } (r in nodes) ==> r.next != null ==> (r.next in nodes)) might not hold on entry. There might be insufficient permission to access r.val (cyclic.vpr@36.22--36.23) (cached)

It does work with the trigger r in nodes or when the triggers are removed.

method isCyclic(nodes: Set[Ref], root: Ref) returns (cyclic: Bool)
  requires root in nodes
  requires (forall r: Ref :: {r.next} r in nodes ==> acc(r.next) && acc(r.val) && (r.next != null ==> r.next in nodes))
{
  var seen: Set[Ref] := Set(root)
  var current: Ref := root

  while (current.next != null && !(current.next in seen))
    invariant current in nodes
    invariant (forall r: Ref :: {r.next} r in nodes ==> acc(r.next) && acc(r.val) && (r.next != null ==> r.next in nodes))
  {
    seen := seen union Set(current.next)
    current := current.next
  }

  cyclic := (current.next != null)
}

[alexanderjsummers]

Interestingly, it seems to also verify when the triggers are made {r.next}{r.val} - without r.val as a trigger there seems to be a difficulty in finding the permissions to r.val that are needed for establishing the loop invariant.

[mschwerhoff]

If I remember correctly, heap-dependent triggers are currently not inferred by Silver's trigger inference code, and thus need to be provided manually.

[alexanderjsummers]

Hi Malte,

Thanks - that explains why some triggers are needed (although in this example other choices will get made by Viper if we leave triggers out, that unfortunately lead to matching loops); it's less clear to me why both triggers are necessary. I have an idea, but suspect this has to do with the way we desugar quantified permissions internally (which ideally wouldn't be visible to a user..)