NLA in subscript leads to insufficient permission

[pieter-bos]

Here is a reduced case I encountered:

field f: Int

method test(i: Int, u: Seq[Ref], select: Int)
requires 0 < i && i < |u|
requires acc(u[0].f, write)
requires acc(u[i].f, write)
requires select == 0 || select == 1
{
  assert perm(u[select*i].f) == write // ok
  u[select*i].f := 0 // fails
}

It seems to me that proving the permission value is the same as the condition of the assignment. If the root cause really is just non-linear arithmetic, why is there a difference between the assertion and assignment? Thanks!

[mschwerhoff]

The reason for this — indeed surprising — failure is an incompleteness of Silicon, due to disjunctive aliasing: By default, Silicon greedily tries to find a single heap chunk that definitely provides sufficient permission, but in your case, neither chunk for u[_].f does. The reason why perm does not suffer from the same problem is that, for perm, the incomplete treatment would also be unsound, whereas for assignments/exhales, it is incomplete but sound.

Possible workarounds are:

1. Resolving disjunctive aliasing by explicit branching:

   if (select == 0) {}
   elseif (select == 1) {}
   else { assert false }
   
   u[select*i].f := 0 // holds now
   

2. Forcing Silicon to use its more complete (and more expensive) quantified permission algorithms for field f (in method test):

   var dummyrcvr: Ref
   inhale forall b: Bool :: false ==> acc(dummyrcvr.f, none) // Vacuous QP assertion involving field f
   
   u[select*i].f := 0 // holds now
   

3. Enable an experimental feature by running Silicon with --enableMoreCompleteExhale

If you don't object, I'll close this issue as a duplicate.

[pieter-bos]

Thanks very much and yes, feel free to close this issue. I wanted to make two remarks:

• I've run the VerCors test suite with --enableMoreCompleteExhale. The run times in viper were within noise range, expect for one example, which then reliably spends 18s in viper instead of 12s, let me know if you're interested in such an example.
• One case changed from (expected) fail to pass, from which I've managed to extract the following example that normally fails, but passes in error with --enableMoreCompleteExhale.

field f: Int

function req(x: Ref): Bool
requires acc(x.f, 2/1)
{
    true
}


method test(x: Ref)
{
    inhale acc(x.f)
    assert req(x)
}