Filter assertions #5031
Filter assertions #5031
Conversation
…x a crash and fix an output ordering bug
keyboardDrummer
force-pushed
the
filterAssertions
branch
from
08c339e
to
60ebf1b
Compare
Dependent Dafny PR: dafny-lang/dafny#5031 ### Changes - Change the API `executionEngine.GetImplementationTasks` to `executionEngine.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 - Added test SplitOnEveryAssertion --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
| . S S | I $ | : //Replace: | ||
| . S S | I $ | :}", true); | ||
| . S | I $ | :method test() { | ||
| . S | I $ | : assert true; |
There was a problem hiding this comment.
Wow, interesting, is it because we don't submit this to the solver anymore?
There was a problem hiding this comment.
O, actually, I didn't think about this. The new Boogie API, that only Dafny is using, does not support caching at all. The reason for that is that caching in Boogie is implemented on an implementation level, and the new Boogie API allows partially verifying implementations, at which point it's not clear when to set the implementation level cache.
It would be not be difficult to update the caching mechanism in Boogie so it works at the VC instead of the implementation level, but since we are not using the caching anyways because we believe it's buggy, I did not do that work. I think it makes more sense to do that when we plan on actually using the caching.
|
|
||
| // Ordering is required to let gutter icon tests behave more deterministically | ||
| // In situations where there are multiple valid orders of execution | ||
| // In particular, GitIssue3821GutterIgnoredProblem fails without this |
There was a problem hiding this comment.
How is that affecting that test? Normally the gutter icons should render errors on top of successful elements, so can you please give me a bit of context here? I looked at the test, and it exists because well-formedness is checked differently, and it has intermediates: false, so it should wait till everything is verified
There was a problem hiding this comment.
Seems like the sorting was no longer needed, so I've removed it and the comment.
…nto filterAssertions
There was a problem hiding this comment.
There are some very small changes I'd suggest.
For future PRs, I wonder how hard it would be to ensure that all refactorings are in commits consisting entirely of refactorings (which you may have done already?) and also clearly mark the commits that are only refactoring (maybe with a "refactor: " prefix), to make the reviews easier. There were a lot of changes in this PR, but most of them weren't functional.
Source/DafnyDriver/CliCompilation.cs
Outdated
| await Task.WhenAny(tasks); | ||
| if (!queueVerificationTask.IsCompleted) { | ||
| Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, | ||
| "Dafny encountered an internal error during verification. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n"); |
There was a problem hiding this comment.
I'd maybe describe what kind of error here. Even if the user doesn't understand it, I could imagine producing this message from multiple places in the code base, and it'd be nice to be able to disambiguate them.
Source/DafnyDriver/CliCompilation.cs
Outdated
| await Task.WhenAny(tasks); | ||
| if (!results.Finished.Task.IsCompleted) { | ||
| Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, | ||
| "Dafny encountered an internal error during verification. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n"); |
There was a problem hiding this comment.
If you adopt my suggestion above, it might no longer be the same message.
| } | ||
|
|
||
| foreach (var diagnostic in batchReporter.AllMessages.OrderBy(m => m.Token)) { |
There was a problem hiding this comment.
I'm very much in favor of this! It might be worth having a .ThenBy to look at the message, too, to ensure deterministic ordering. I've seen many spurious failures when working on the verifier because the ordering of messages changes due to non-determinism in sorting. It's something I've been meaning to fix for a while.
There was a problem hiding this comment.
I'll leave that for another PR
| output.WriteLine(); | ||
|
|
||
| if (reportAssertions) { | ||
| output.Write("{0} finished with {1} assertions verified, {2} error{3}", options.DescriptiveToolName, |
There was a problem hiding this comment.
I like this change, but I get the impression there wasn't a clear consensus in the discussion on the issue.
There was a problem hiding this comment.
This is conditional on using the --filter-positions option with a line number, so that's a much smaller and simpler discussion.
| counterExamples = counterExamples.Concat(batchCompleted.VcResult.counterExamples); | ||
| hitErrorLimit |= batchCompleted.VcResult.maxCounterExamples == batchCompleted.VcResult.counterExamples.Count; | ||
| if (boogieUpdate.BoogieStatus is Completed completed) { | ||
| // WarnContradictoryAssumptions should be computable after completing a single assertion batch. |
There was a problem hiding this comment.
This will require some refactoring, though I think it shouldn't be too hard. The key issue is that, at the moment, we look for all proof obligations associated with a given definition and report any that don't show up in the set of covered elements. To make it work per assertion batch, we need to update that logic to identify proof obligations associated with that assertion batch, and see which ones are missing.
I think we should, while working, try to put refactorings in individual commits. When it's PR time, the publisher has the option of trying to move those commits to the start of the PR. In my experience it's often the case those that doing those moves created conflicts though, so it's not for free. What I sometimes prefer to do is manually reapply the large-scale refactorings (moves, renames) in a second branch, publish a separate PR for that and have that merged first. For example, these two PRs boogie-org/boogie#840 and https://github.com/boogie-org/boogie/pull/842/files were originally part of boogie-org/boogie#841
Most of the PR changes are due to moving to the latest Boogie version. Since there were renames in that, this introduces what looks like renames in this PR. Could have moved updating the Boogie version to a separate PR. |
Description
--filter-positionto only verify individual assertions.The implementation relies on a new version of Boogie, which changes the API so that Boogie returns not a list of implementations but instead of a list of 'verification tasks', which map to individual SMT executions or 'assertion batches'. When using
--isolate-assertions, each assertion is given such as task, and it becomes easy to filter these tasks/assertions based on a file position.Background of some of the code changes
This change in the Boogie API means Dafny is not longer updated when all the tasks for a particular Boogie implementation are finished, which effects a few things that rely on all tasks in a Boogie implementation to be done:
There is no change in behavior for the above, but the code had to be updated so on the Dafny side we track whether everything for a particular implementation is done.
How has this been tested?
filter.dfyBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.