carbon
carbon copied to clipboard
viperproject
Incoherent loop treatment (scoping)
Created by bitbucket user Thibault Dardinier on 2019-10-30 09:56 Last updated on 2019-10-30 10:45
field f: Int
method works(x: Ref)
requires acc(x.f)
{
x.f := 5
exhale acc(x.f, 1/2)
var i: Int := 0
while (i < 10)
{
inhale acc(x.f, 1/3)
assert x.f == 5 // Works with Carbon, fails with Silicon
exhale acc(x.f, 1/3)
}
}
method doesnt_work(x: Ref)
requires acc(x.f)
{
x.f := 5
exhale acc(x.f, 1/2)
var i: Int := 0
while (i < 10)
{
inhale acc(x.f, 1/3)
assert x.f == 5 // Verifies with Carbon
exhale acc(x.f, 1/3)
inhale acc(x.f, 1/3)
assert x.f == 5 // Fails with Carbon
exhale acc(x.f, 1/3)
}
}
method exhale_something_else(x: Ref, y: Ref)
requires acc(x.f)
requires x != y
{
x.f := 5
exhale acc(x.f, 1/2)
var i: Int := 0
while (i < 10)
{
inhale acc(y.f, 1/2)
exhale acc(y.f, 1/2)
inhale acc(x.f, 1/3)
assert x.f == 5 // Fails with Carbon
exhale acc(x.f, 1/3)
}
}
Because of how loops are encoded in Boogie, line 12 here (assert x.f == 5 in the loop body of the first method) verifies with Carbon, meaning that the loop body has access to the heap from before the loop, even if no permission is transferred in the loop invariant. However, after a non-pure exhale in the loop body, this access is not possible anymore. This leads to weird behaviors as shown with the last two methods.
The view that there is an access to the heap from before the loop in Carbon is also inconsistent with Silicon’s view that the loop body cannot see values of fields for which it doesn’t hold any permission.
Attachments:
Bitbucket user Thibault Dardinier on 2019-10-30 10:03:
- edited the description