Non-aliasing incompleteness when using QPs

[marcoeilers]

In the following example, the assertion fails:

field f: Int

method foo(r1: Ref, r2: Ref, s: Set[Ref]) returns (res:Int)
 requires acc(r1.f)
 requires acc(r2.f)
 requires forall x: Ref :: {x in s} x in s ==> acc(x.f)
{
 r1.f := 3
 assert r1 != r2
} 

When leaving out the quantified permission in the precondition, the assertion goes through. Dropping the field assignment in the body also leads to the assertion going through. Adding an assert true before the failing assertion does not seem to change anything.

[mschwerhoff]

A work-around might be to assert true before the heap update (maybe after preconditions and loop invariants suffices for your cases):

assert true
r1.f := 3
assert r1 != r2

Another potential work-around:

r1.f := 3
assert perm(r1.f) <= write
assert r1 != r2

I also have an idea how to include the effect of assert perm(r1.f) <= write in the state consolidation Silicon performs, might not be too difficult. I'll give it a try today or tomorrow.

[marcoeilers]

Thanks a lot! @ckamueller FYI, maybe one of those workarounds works for us?

[mschwerhoff]

I found a more automated solution and I've just started benchmarking its effect on performance. I'll report back in the next few days.

[mschwerhoff]

Resolved with commit f48de7f

[marcoeilers]

Great, thanks!