silicon
silicon copied to clipboard
viperproject
Frame heap assumptions into read-only loops
Created by @mschwerhoff on 2016-02-22 13:48 Last updated on 2018-10-15 09:09
#!text
field f: Int
method test(x: Ref) returns (a: Int)
requires acc(x.f) && x.f != 0
{
a := 0 \ x.f
while (a == 0)
invariant acc(x.f, 1/2)
invariant x.f != 0 // Should not be necessary ...
{
a := 1 + (0 \ x.f) // ... for this division to pass (in Silicon)
}
a := 0 \ x.f
}
@mschwerhoff commented on 2018-08-07 13:52
https://github.com/viperproject/silicon/issues/347 was marked as a duplicate of this issue.
@alexanderjsummers commented on 2018-08-07 15:20
(superceded by comment below) In my opinion, this isn't a Silicon-specific issue; the behaviour is identical in both back-ends, and seems to me consistent with how loop invariants are conceptually handled. The current design of loop verification in Viper implies that the second loop invariant should be necessary; the only information about the heap which is known inside the loop body is that conveyed by the loop invariant. We can discuss an alternative design (e.g. in a Viper meeting), but maybe this should be a Silver issue.
It isn't immediately obvious to me that the alternative design suggested here would always make sense; since programs can inhale/exhale permissions inside loop bodies, starting and ending with a fractional permission doesn't imply that the value remains unchanged (both because the loop might temporarily lose all permission, and because it might temporarily have full permission).
@mschwerhoff commented on 2018-08-07 15:34
So Carbon needs the 2nd invariant as well? I am fairly certain that this wasn't always the case; maybe something in the encoding changed since the issue has been filed.
I'd be interested in discussing this example, and the general issue/potential optimisation, in a Viper meeting.
@mschwerhoff commented on 2018-10-15 08:53
https://github.com/viperproject/silicon/issues/358 was marked as a duplicate of this issue.
@alexanderjsummers commented on 2018-10-15 08:56
It seems the additional loop invariant is not needed for Carbon. I suspect that my comment above was because of an unrelated issue; at some point over the summer there was a problem with some proof obligations being generated in the wrong order, which could have explained the problem.
The explanation I added to https://github.com/viperproject/silicon/issues/358 explains why the invariant is superfluous for Carbon's current encoding
@alexanderjsummers commented on 2018-10-15 09:03
For Silicon, would a potential encoding (just looking at how to get from state before the loop to state at the start of the loop body): exhale loop invariant; record (in some way) all permissions held; havoc loop targets; inhale loop invariant; (possibly) trigger heap compression; exhale all recorded permissions ?
I'm sure there are also ways to explicitly frame information essential via perm expressions, but that could be rather expensive.
@alexanderjsummers commented on 2018-10-15 09:09
I think the second half of my first comment above is also spurious. The point is that if some permission is framed around the loop body, then we could (though this is a design choice) consider these permissions as still somehow in the state inside the loop body (but not directly usable). With this argument, it would be unsound to gain full permission to those locations explicitly inside the body, and modify them. In other words, it seems there is nothing wrong with preserving the information framed by permissions framed around the loop (if this is the design we go for).
Maybe I will just delete my first comment, since it seems totally wrong now :)