Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Filter assertions #5031

Merged
merged 50 commits into from
Feb 8, 2024
Merged

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Jan 31, 2024

Description

  • Allow using --filter-position to 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:

  • Computation of redundant assertions
  • Gutter icons (maybe it conceptually does not depend on Boogie implementations, I'm not sure, but the current implementation cares about Boogie implementations)

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?

  • Added new cases to the existing littish test filter.dfy
  • Some gutter icons tests have been updated, which is I think due to an improvement. The last batch completed + implementation completed steps are now combined, so two updates that would always immediately follow each other are now squashed together.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer marked this pull request as ready for review February 2, 2024 14:53
keyboardDrummer added a commit to boogie-org/boogie that referenced this pull request Feb 2, 2024
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 <[email protected]>
. S S | I $ | : //Replace:
. S S | I $ | :}", true);
. S | I $ | :method test() {
. S | I $ | : assert true;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wow, interesting, is it because we don't submit this to the solver anymore?

Copy link
Member Author

@keyboardDrummer keyboardDrummer Feb 6, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like the sorting was no longer needed, so I've removed it and the comment.

@keyboardDrummer keyboardDrummer self-assigned this Feb 6, 2024
Copy link
Member

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you adopt my suggestion above, it might no longer be the same message.

}

foreach (var diagnostic in batchReporter.AllMessages.OrderBy(m => m.Token)) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll leave that for another PR

output.WriteLine();

if (reportAssertions) {
output.Write("{0} finished with {1} assertions verified, {2} error{3}", options.DescriptiveToolName,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like this change, but I get the impression there wasn't a clear consensus in the discussion on the issue.

Copy link
Member Author

@keyboardDrummer keyboardDrummer Feb 7, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@keyboardDrummer
Copy link
Member Author

keyboardDrummer commented Feb 7, 2024

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.

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

There were a lot of changes in this PR, but most of them weren't functional.

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.

atomb
atomb previously approved these changes Feb 7, 2024
@keyboardDrummer keyboardDrummer merged commit 385103d into dafny-lang:master Feb 8, 2024
20 checks passed
@keyboardDrummer keyboardDrummer deleted the filterAssertions branch February 8, 2024 16:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants