Verification task per split #841
Conversation
The text of the I/O error is slightly different
…/boogie into verificationTaskPerSplit
There was a problem hiding this comment.
I like the changes this makes a lot. I left a few comments that could result in changes, though not necessarily as part of this PR. The one critical one is that I'd only want to merge this with caching broken if you know you'll have another PR immediately following that fixes it (before the next Boogie release).
| public ProcessedProgram ProcessedProgram { get; } | ||
|
|
||
| public IToken ScopeToken => Split.Implementation.tok; | ||
| public string ScopeId => Split.Implementation.VerboseName; // TODO this verbose name threw me off. Why do we need it besides the regular name? |
There was a problem hiding this comment.
VerboseName is intended for human consumption, and may be different from Name. It's what allows us to report verification results in terms of Dafny names, and could work similarly for any other front end that translates a language into Boogie and wants to preserve source-level names.
There was a problem hiding this comment.
Both Name and VerboseName should be unique, so either would work as a unique ID if you're not going to display it anywhere.
| // result = result with { | ||
| // CounterExamples = Split.Counterexamples | ||
| // }; | ||
| // } |
There was a problem hiding this comment.
Did you mean to leave in this commented-out code?
|
|
||
| public bool IsIdle => cancellationSource == null; | ||
|
|
||
| public IObservable<IVerificationStatus>? TryRun() { |
There was a problem hiding this comment.
The concurrency logic from here through the end of this file is complex. I don't immediately see any problems with it, but I wonder if it would be worth trying to model and prove something about the state machine that it encodes. No need to hold up the PR for that -- I suspect this is already quite a bit better than what we have -- but it might be worth trying.
| @@ -40,7 +34,8 @@ class SplitAndVerifyWorker | |||
|
|
|||
| private int totalResourceCount; | |||
|
|
|||
| public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, ImplementationRun run, | |||
| public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, | |||
| ImplementationRun run, | |||
There was a problem hiding this comment.
Maybe pull some of the following parameters up onto this line? It's an awkward split, as-is.
| public record VerificationRunResult | ||
| ( | ||
| int VcNum, | ||
| int vcNum, |
There was a problem hiding this comment.
Why change this one when the rest have initial capitals? I could imagine making all of the fields start with a lowercase letter, but this makes it inconsistent.
| var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert); | ||
| splits.Add(new Split(initialSplit.Options, BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); // REVIEW: Does gotoCmdOrigins need to be changed at all? | ||
| splits.Add(new ManualSplit(initialSplit.Options, BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token)); // REVIEW: Does gotoCmdOrigins need to be changed at all? |
There was a problem hiding this comment.
I wouldn't think it needs to change, since, as I understand it, every split has the same control flow, just a different set of assertions vs. assumptions.
| @@ -883,24 +870,26 @@ public Counterexample ToCounterexample(ProverContext context) | |||
| return result; | |||
| } | |||
|
|
|||
| public (Bpl.SolverOutcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback) | |||
| public VerificationRunResult ReadOutcome(int iteration, Checker checker, VerifierCallback callback) | |||
| var engine = ExecutionEngine.CreateWithoutSharedCache(options); | ||
| var tasks = engine.GetVerificationTasks(program); | ||
|
|
||
| // The first split is empty. Maybe it can be optimized away |
There was a problem hiding this comment.
Yeah, I've been wondering about the empty first split for a while now. It'd be nice to get rid of it.
| Assert.AreEqual(secondName, statusList[4].Item1); | ||
| Assert.IsTrue(statusList[4].Item2 is Completed); | ||
|
|
||
| // Caching is currently not working |
There was a problem hiding this comment.
Given that at least this test of caching was working before, it'd be unfortunate to merge something that breaks it. Since I know that's something you're working on, do you have an upcoming PR already planned that'll fix it? It's perhaps worth making that separate for ease of reviewing, but I'd be reluctant to push a release of Boogie until it's at least working as well as it was before.
There was a problem hiding this comment.
Verification caching is currently not used by Dafny, because we don't trust it. This pathway of Boogie, for which caching does not work, is only used by Dafny. To 'fix' the caching, I would not to write some new code that does caching at the split level instead of the implementation level. Probably nothing complex, but it does not make sense to me to develop something that we won't test end-to-test because we're not using it.
I have no doubt that we'll add this caching feature in the future, but I don't know when.
There was a problem hiding this comment.
If you're confident that it's not used by any other tools, then this sounds fine.
Dependent Dafny PR: dafny-lang/dafny#5031
Changes
executionEngine.GetImplementationTaskstoexecutionEngine.GetVerificationTasks, which returns a task for each statically defined assertion batch. When using the split on every assert option, this will return a verification task for each assertion.Testing