Enable marking if commands as {:allow_split} or not #970
Conversation
This reverts commit 09093a2.
This reverts commit 593340f.
There was a problem hiding this comment.
Implementation LGTM as far as I can tell (testing coverage is good and didn't see anything obviously wrong/risky). Mainly looking for clearer labeling and documentation of the feature (and will overlap with my review of dafny-lang/dafny#5832)
isa.ppl
Outdated
| @@ -5,6 +5,12 @@ | |||
| namespace Microsoft.Boogie; | |||
|
|
|||
| public static class ListExtensions { | |||
| public static void AddRange<T>(this IList<T> list, IEnumerable<T> newValues) { | |||
| @@ -10,6 +10,9 @@ | |||
| namespace VCGeneration.Splits; | |||
|
|
|||
| public class BlockRewriter { | |||
| private const string AllowSplit = "allow_split"; | |||
There was a problem hiding this comment.
I find this name isn't precise enough to immediately understand, could we make it {:allow_path_isolation} to connect it more directly to {:isolate "paths"}? Otherwise to me it sounds like it relates to {:split_here} somehow.
| }); | ||
| } | ||
| /// <summary> | ||
| /// Each focus block creates two options. |
There was a problem hiding this comment.
nit: focus is probably the wrong word here. Or else there should be a more explicit statement that isolating paths is implemented in terms of {:focus}
Is it correct to think of {:isolate "paths"} as equivalent to adding {:focus} to each branch?
Also how does path-based splitting work on while loops?
There was a problem hiding this comment.
focus is probably the wrong word here
Comment was accidentally copied
Is it correct to think of {:isolate "paths"} as equivalent to adding {:focus} to each branch?
I have not managed to think of one entirely in terms of the other. I wanted to see if I could reuse the focus code for either {:isolate "paths} on asserts or on returns, but didn't manage.
Also how does path-based splitting work on while loops?
Path splitting is useful when there are merges in the CFG, but a loop only creates a branch, so path-based splitting is not useful to process it.
LoopHead:
assert <invariants>
goto LoopDone, LoopBody
LoopBody:
havoc loopTargets;
assume <invariants>;
assume <guard>;
<body>
assert <invariants>; // adding {:isolate "paths"} here does not help, since only a single path leads here
return;
LoopDone:
assume !<guard>
<rest>
assert <foo> // adding {:isolate "paths"} here does not help, since only a single path leads here
| @@ -1,4 +1,4 @@ | |||
| // RUN: %parallel-boogie /printSplit:%t /errorTrace:0 "%s" > "%t" | |||
| // RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" | |||
There was a problem hiding this comment.
Whoops! :) Out of curiousity was the old behavior non-deterministic and the test flaky?
There was a problem hiding this comment.
Yes, but it only became flaky in this PR because everything is sent to the same buffer (stdout). Using stdout allows using .expect files instead of check statements, which is easier to maintain.
| } | ||
|
|
||
|
|
||
| implementation Ex/split@15() returns (y: int) |
There was a problem hiding this comment.
It feels confusing that you end up with three different patterns for naming splits here:
- The first unqualified
Exsplit above (and what does that cover then?) - This "number 15" split
- The path-based splits below
Being clear on this matters since the user has to understand their source in order to fix verification failures.
I would at least suggest being slightly clearer on the path-based labels, perhaps something like Ex[path: 14 -> 19 -> 25]. You could produce that in Dafny error messages or at the Boogie level.
There was a problem hiding this comment.
The first unqualified Ex split above (and what does that cover then?)
Impossible to say what it covers. It is the "remainder" after processing all the focus/isolate/split_here
This "number 15" split
It's actually the line number from which the assertion originates. I could add the column to possibly disambiguate
Being clear on this matters since the user has to understand their source in order to fix verification failures.
This notation is only used at the Boogie level, where I optimize for power users. I use more verbose notation in Dafny.
There was a problem hiding this comment.
I've updated the Boogie naming so it's simply more correct and also slightly more verbose. It will say implementation Ex/focus[16]/split@15() to mean, the implementation Ex, using the focus at line 16, and then the split_here at line 15.
One thing I struggle with is the overloading of the term split. Split is used to describe both any type of VC partitioning: focus/split_here/isolate/isolate "paths", but also occurs in the name "split_here". Should I rename {:split_here} to {:cut} ?
There was a problem hiding this comment.
Naming is much better, thanks!
Heavily agreed on the overloading of "split" - it fits better as an operation name rather than a name for the things it produces. I think {:split_here} is reasonable since it's referring to the operation, it's labelling the VCs as "splits" that's a bigger problem.
There was a problem hiding this comment.
I initially wanted to rename the produced things to Partition, but somehow I kept referring to things as splits. I feel it would be easiest to rename {:split_here} to {:cut}, but I'm willing to rename on the other side.
Requires Boogie boogie-org/boogie#970 ### Changes - Allows using `{:isolate "paths"}` on `assert`, `return` and `continue` statements. ### Out of scope - `{:isolate "paths"}` for implicit assertions - Custom syntax for {:isolate}, possibly in combination with "by clauses" ### Testing - Added the CLI test `isolatePaths.dfy` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <[email protected]>
Changes
{:allow_split}that can be placed onIfCmd. When using{:isolate "paths"}only, branches with{:allow_split}will trigger splitting of the VC.Testing
{:allow_split}{:vcs_split_on_every_assert}and explicit returns.