silicon
silicon copied to clipboard
viperproject
While statement might fail in manually encoded CFG
Created by @fpoli on 2018-09-28 13:56 Last updated on 2019-07-29 14:45
The following program does not verify with Silicon, but it verifies with Carbon.
I'm trying to manually exhale the invariant (before and) at the end of the loop body, and inhaling it at the beginning of the loop. Am I doing it right?
field foo: Bool
method main(x: Ref)
{
label loop
inhale acc(x.foo)
assert acc(x.foo)
// ERROR: While statement might fail. There might be insufficient permission to access x.foo.
if (x.foo) { goto end }
exhale acc(x.foo)
goto loop
label end
}
@mschwerhoff commented on 2018-09-28 14:01
Could you please post the visual representation of the CFG? silicon --printMethodCFGs, then convert the generated Graphviz file to an image.
@fpoli commented on 2018-09-28 14:28
Small variation:
field foo: Bool
method main(x: Ref, b: Bool)
{
label loop
inhale acc(x.foo)
assert acc(x.foo)
// ERROR: While statement might fail. There might be insufficient permission to access x.foo.
if (x.foo) { }
exhale acc(x.foo)
goto loop
label end
}
@mschwerhoff commented on 2018-09-28 15:51
Thank you for the graphs! Here is a not-so-short description of why you get the observed behaviour:
Consider the following while loop:
while (x.f)
invariant true
{
inhale acc(x.f)
if (x.f) { goto end }
exhale acc(x.f)
}
label end
The CFG Silicon gets looks as follows:
The edges leaving block 16 (x.f/!x.f) are due to the loop guard, the edges leaving block 20 are from the inner if and goto.
Before CFGs were introduced, Silicon required loop conditions to be framed by the invariant — probably so that the (negated) condition can be assumed in (after) the loop without having to worry that the condition might be ill-defined due to insufficient permission. Silicon still checks this property, but now on the CFG level: there, every edge leaving the loop head block must have a condition that is framed by the invariant.
In your example, the loop head block has a leaving edge whose condition is not framed by the invariant (which in your example is just true).
It would be easy to not require that edges leaving a loop head block are framed by the invariant, the verification failure you currently get would then not be reported (and Silicon could also easily check that the (negated) condition is well-defined at the points where it is assumed).
However, since the CFG does not differentiate between edges that are due to desugared loops and edges that are due to if statements, the error reporting would become confusing: if you compare the CFG from my example with the CFG from your example, you can see that the edges leaving the loop head block can come from either a while statement or an if statement. If the condition cannot be evaluated due to insufficient permission, it is not clear what to report: "while statement failed" or "if statement failed".
A solution to the latter problem would be to annotate CFG edges with the AST statements that they were generated from. If such information is present, Silicon could use it to report different errors. A similar approach would be to add error back-transformers to the CFG edges.
I'd suggest you discuss whether or not we want loop conditions to be framed by invariants with @alexanderjsummers, and how to preserve additional AST information in the CFG with @alexanderjsummers and @dohrau. I'd be happy to participate in the discussions, of course — could also be done in a Viper meeting.
Note that Carbon currently doesn't properly support goto statements, I am thus not sure how meaningful it is that Carbon doesn't report any verification failures.
@alexanderjsummers commented on 2018-09-28 16:17
btw Carbon just pushes the gotos down to the Boogie level at the moment. Since it never adds invariants there, this works (a) as if all invariants on goto targets were true, and (b) without any such consistency checks about edges.
I'd be happy to have the discussions Malte mentioned above
@fpoli commented on 2018-10-01 09:49
Btw, we plan to work around this by introducing extra boolean local variables, such that any problematic if (expr) ... becomes var b: Bool = expr; if (b) ....
@dohrau on 2019-07-29 14:45:
- changed the assignee from (none) to @dohrau