Proof dependency warnings #4542

atomb · 2023-09-12T20:35:47Z

Adds warnings for two cases of suspicious proof dependencies:

Warn about a vacuous proof when the goal itself is not a dependency of the proof.
Warn about any assumption that is not used by any proof in the context where it exists.

A few cases of vacuity are artifacts of how Dafny programs are encoded in Boogie. Several of these cases are automatically filtered out.

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

When enabled with -trackVerificationCoverage (an internal Boogie flag that we don't expect most people to use), this calculates proof dependencies and includes them in the output of the "text" format verification logger. Some caveats: * Some important statements aren't labeled yet. * Some descriptions are different in different contexts.

Previously it was sorted by name

This helps ensure deterministic testing.

…rage-ids

This occurs due to a Boogie change that now dereferences a property that previously was supposed to never be null but wasn't blindly dereferenced.

…rage-ids

Temporary until we fix a Boogie concurrency bug

…warnings

robin-aws

Partial review, still have to have a look at the main file changes

robin-aws · 2023-09-13T03:21:32Z

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -248,6 +252,12 @@ public enum DefaultFunctionOpacityOptions {
    DafnyOptions.RegisterLegacyBinding(WarningAsErrors, (options, value) => { options.WarningsAsErrors = value; });
    DafnyOptions.RegisterLegacyBinding(VerifyIncludedFiles,
      (options, value) => { options.VerifyAllModules = value; });
+    DafnyOptions.RegisterLegacyBinding(WarnVacuity, (options, value) => {


Bit off topic, but do we actually need the legacy bindings on new options? I've been avoiding this given the "legacy" label and just using Options.Get(CommonOptionBag.MyNewOption).

~~+1, please never add RegisterLegacyBinding~~

The underlying option it's setting, TrackVerificationCoverage , is a Boogie option. The RegisterLegacyBinding call is a way to sync the Dafny option into the Boogie one. This is not the right long term approach, but right now it's what the other Boogie-coupled options are doing.

Ideally, the Boogie options would be separate from the Dafny ones, and you'd have to create them when instantiating "Boogie" (in the code that would be the Boogie ExecutionEngine, instantiated here: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyDriver/DafnyDriver.cs#L41).

To do that nicely we'd need another registry that's similar to RegisterLegacyBinding, but then RegisterBoogieBinding.

Yeah, it's a bit of a tricky case where we have new, modern options but also need to set a Boogie option. I'd entirely be in favor of some new registry, but I think it's out of scope for this PR.

robin-aws · 2023-09-13T03:59:54Z

Source/DafnyDriver/DafnyDriver.cs

@@ -466,6 +468,10 @@ public enum CommandLineArgumentsResult {
        string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1]));
        var (verified, outcome, moduleStats) = await BoogieAsync(options, baseName, boogiePrograms, programId);

+        if (options.TrackVerificationCoverage && verified) {


Out of scope for this review, but for the next opportunity: seems like this option name is a holdover from the previous terminology. Is this backed by a CLI option with a better name?

Yeah, it's turned on by --warn-vacuity or --warn-redundant-assumptions. Dafny users will never need to see the terminology in this option.

robin-aws · 2023-09-13T04:02:06Z

Test/logger/ProofDependencyLogging.dfy

-// CHECK:       ProofDependencyLogging.dfy\(244,24\)-\(244,24\): value always satisfies the subset constraints of 'nat'
-// CHECK:       ProofDependencyLogging.dfy\(244,47\)-\(244,47\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencyLogging.dfy\(244,25\)-\(244,25\): value always satisfies the subset constraints of 'nat'
+// CHECK:       ProofDependencyLogging.dfy\(244,48\)-\(244,48\): value always satisfies the subset constraints of 'nat'
 //
 // CHECK: Results for ObviouslyUnconstrainedCodeFunc \(well-formedness\)
 // CHECK:     Proof dependencies:


Also out of scope for this review, but can't help ask if we should label this more precisely to account for the fact that some proof dependencies may be "spurious", just as counter examples are really something like "potential counter examples"

robin-aws · 2023-09-13T04:03:17Z

Test/logger/ProofDependencyWarnings.dfy.expect

Nice that you got adequate testing coverage by reusing the existing test file!

robin-aws · 2023-09-13T04:51:33Z

Test/logger/ProofDependencyWarnings.dfy.expect

@@ -0,0 +1,20 @@
+ProofDependencyLogging.dfy(176,11): Warning: unnecessary assumption
+ProofDependencyLogging.dfy(186,13): Warning: vacuous proof: assertion always holds


Ah NOW I get my previous confusion - in this specific (and common) case, the vacuous proof: <proof description> template leads to a string that's too easy to misinterpret as vacuous proof, or, as another way of saying 'vacuous proof', assertion always holds. :)

Perhaps we could use a template like vacuous proof of (<proof description>) instead?

We could also consider not using "vacuous" since many users won't be familiar with that concept. Perhaps "Warning: proved from impossible assumptions: ..." ("contradictory assumptions" is appealing too, but then false by itself is impossible).

Ah but you even used "contradictory assumptions" in the option help text so perhaps I shouldn't worry :)

Yeah, so how about "proved using contradictory assumptions: "? I could change the name of --warn-vacuity, too. Maybe --warn-contradictory-assumptions? That's nicely symmetric with --warn-redundant-assumptions.

robin-aws · 2023-09-13T04:55:55Z

Source/DafnyCore/Verifier/ProofDependencyManager.cs

+      currentDefinition = defName;
+    }
+
+    public IEnumerable<ProofDependency> GetPotentialDependenciesForDefinition(string defName) {


Ah there's the "potential" word I was looking for :)

keyboardDrummer · 2023-09-13T12:29:00Z

Source/DafnyCore/DafnyMain.cs

@@ -203,5 +205,95 @@ public class DafnyMain {
      }
    }

+    public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) {


I would put this code in a separate file. I think ideally this could would live in a plugin that could live in a separate assembly that hooks into some PostSymbolVerification event. Not needed for now but if we can make it look more like that I'd appreciate it.

robin-aws

Awesome feature, looking forward to having it on by default in the future :)

robin-aws · 2023-09-13T15:22:45Z

Source/DafnyCore/DafnyMain.cs

@@ -203,5 +205,95 @@ public class DafnyMain {
      }
    }

+    public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) {


robin-aws · 2023-09-13T15:27:01Z

Test/logger/ProofDependencyWarnings.dfy.expect

@@ -0,0 +1,20 @@
+ProofDependencyLogging.dfy(176,11): Warning: unnecessary assumption
+ProofDependencyLogging.dfy(186,13): Warning: vacuous proof: assertion always holds


We could also consider not using "vacuous" since many users won't be familiar with that concept. Perhaps "Warning: proved from impossible assumptions: ..." ("contradictory assumptions" is appealing too, but then false by itself is impossible).

robin-aws · 2023-09-13T15:29:06Z

Source/DafnyCore/DafnyMain.cs

+      var unusedAssumeStatements =
+        unusedDependencies
+          .OfType<AssumptionDependency>()
+          .Where(d => d.Description.Contains("assume statement"));


Matching against the description feels brittle, especially with just Contains rather than ==. Consider adding a fixed identifier of some kind for this use case.

Yeah, I'll see whether there's a better way to do this.

robin-aws · 2023-09-13T15:32:26Z

Source/DafnyCore/DafnyMain.cs

+      }
+
+      // Ensures clauses are often proven vacuously during well-formedness checks.
+      if (verboseName.Contains("well-formedness") && dep is EnsuresDependency) {


Another test that feels brittle, any way we can be more structured here?

Unfortunately, I don't know of a good way to change this, much as I don't like it. At this point, we only have access to the Boogie Implementation and it doesn't tell us where it came from.

robin-aws · 2023-09-13T15:34:11Z

Test/logger/ProofDependencyWarnings.dfy.expect

@@ -0,0 +1,20 @@
+ProofDependencyLogging.dfy(176,11): Warning: unnecessary assumption
+ProofDependencyLogging.dfy(186,13): Warning: vacuous proof: assertion always holds


Ah but you even used "contradictory assumptions" in the option help text so perhaps I shouldn't worry :)

robin-aws

Love the terminology change this led to. Thanks!

docs/dev/news/4542.feat

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

atomb · 2023-09-14T22:40:39Z

I've noticed some odd behavior in this that I'd like to debug before merging it.

atomb · 2023-09-14T23:16:13Z

The one thing that's clearly amiss is that it doesn't work well with Boogie's BATCH_MODE option. It's perhaps still worth merging if that's the only issue.

atomb · 2023-09-14T23:44:43Z

There are also some cases where --warn-contradictory-assumptions can lead to false positives if a proof completes by being simplified away, before the solver sees it. Because of this, I've updated the release notes with a caveat and made the options hidden by default. I think it's worth merging, since the feature is still useful when keeping that caveat in mind, but I'll aim to fix it as soon as I can.

…iment-trsplitexpr * commit '86840e6b14386c1e88480854dd8ce64ad17cb2ff': Map eq range (#4567) Fix: Declarations with {:only} ensure that other declarations aren't displayed as verified in the gutter icons (#4433) Fix caching of export declarations (#4556) Do not return exceptions when doing hover in a program with parse errors (#4557) Proof dependency warnings (#4542) [Test Generation] Reduce memory footprint by reusing the same Boogie program for multiple test generation queries (#4530) Fix a variety of bugs in Rust backend based on ESDK testing (#4538) Checker for .Values and .Items on maps (#4551) feat: Allow more assumptions in library backend (#4545) feat: Attributes on reads clauses (#4554) Fix gutter icons fields (#4549) Report errors that occur in the project file, in the IDE as well (#4539) Switch to ubuntu-20.04 for the refman build (#4555)

atomb and others added 30 commits August 23, 2023 13:59

Merge branch 'master' into verification-coverage-ids

b52bec3

Rename utility methods

088eca9

Basic tracking of assignments

adbe5bc

Track a few more proof dependencies

d260984

Fix customBoogie.patch

d6f9eea

Fix unit test for slightly different message

8bb2303

Revert message change for preconditions

671b7f6

Better dependency messages, assignment tracking

9ab8bfd

Order text logger output by source location

2b8d580

Previously it was sorted by name

Add test for proof dependency logging

ac55f3f

Adjust test output to account for changes

d40f73a

Silence warning

595bded

Remove obsolete statement

2804ef9

Sort proof dependencies in text logger

698b067

This helps ensure deterministic testing.

Fix some expected test outputs

6803cad

Merge remote-tracking branch 'upstream/master' into verification-cove…

8e098f9

…rage-ids

Move ProofDependencyManager to its own file

80d174a

Clean up ProofDependency

5c6deff

Fix duplicate IDs in Boogie code

6a671dd

Fix NPE in test generation code

3e4a91b

This occurs due to a Boogie change that now dereferences a property that previously was supposed to never be null but wasn't blindly dereferenced.

Merge remote-tracking branch 'upstream/master' into verification-cove…

ea859c5

…rage-ids

Merge remote-tracking branch 'upstream/master' into verification-cove…

50ee917

…rage-ids

Fix expected test output

9e2ad02

Various small cleanups

9133cf7

Merge remote-tracking branch 'upstream/master' into verification-cove…

2dc0052

…rage-ids

Use structured dependency labels from Boogie

04fca88

Merge remote-tracking branch 'upstream/master' into verification-cove…

3c9b47d

…rage-ids

Limit proof dependency analysis to one core

813b190

Temporary until we fix a Boogie concurrency bug

Fix customBoogie.patch

5e75656

atomb added 3 commits September 12, 2023 14:51

Fix typos in .expect files

570f1a6

Fix test to account for :id attributes

32146b1

Merge remote-tracking branch 'upstream/master' into proof-dependency-…

9bc6021

…warnings

robin-aws reviewed Sep 13, 2023

View reviewed changes

keyboardDrummer reviewed Sep 13, 2023

View reviewed changes

robin-aws requested changes Sep 13, 2023

View reviewed changes

Address review comments

cfcf464

robin-aws previously approved these changes Sep 14, 2023

View reviewed changes

atomb added 2 commits September 14, 2023 11:44

Merge branch 'master' into proof-dependency-warnings

4b88f75

Add release notes entry

5b9fda2

atomb dismissed robin-aws’s stale review via 5b9fda2 September 14, 2023 18:51

atomb enabled auto-merge (squash) September 14, 2023 18:52

robin-aws reviewed Sep 14, 2023

View reviewed changes

docs/dev/news/4542.feat Outdated Show resolved Hide resolved

Update docs/dev/news/4542.feat

cfa6cd1

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

robin-aws previously approved these changes Sep 14, 2023

View reviewed changes

atomb disabled auto-merge September 14, 2023 22:40

Update release notes and hide options

b82a523

atomb dismissed robin-aws’s stale review via b82a523 September 14, 2023 23:42

Add disclaimers to option descriptions

1cdd1a0

robin-aws approved these changes Sep 16, 2023

View reviewed changes

robin-aws enabled auto-merge (squash) September 16, 2023 00:18

robin-aws added 2 commits September 15, 2023 17:18

Merge branch 'master' into proof-dependency-warnings

f6958b5

Merge branch 'master' into proof-dependency-warnings

faa1ffa

robin-aws merged commit 4552a07 into dafny-lang:master Sep 16, 2023

MikaelMayer mentioned this pull request Sep 22, 2023

Display proof dependency warnings in the IDE #4541

Merged

atomb deleted the proof-dependency-warnings branch January 4, 2024 16:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Proof dependency warnings #4542

Proof dependency warnings #4542

atomb commented Sep 12, 2023

robin-aws left a comment

robin-aws Sep 13, 2023

keyboardDrummer Sep 13, 2023 •

edited

Loading

atomb Sep 13, 2023

robin-aws Sep 13, 2023

atomb Sep 13, 2023

robin-aws Sep 13, 2023

robin-aws Sep 13, 2023

robin-aws Sep 13, 2023

robin-aws Sep 13, 2023

robin-aws Sep 13, 2023

atomb Sep 13, 2023

robin-aws Sep 13, 2023

keyboardDrummer Sep 13, 2023

robin-aws Sep 13, 2023

atomb Sep 13, 2023

robin-aws left a comment

robin-aws Sep 13, 2023

robin-aws Sep 13, 2023

robin-aws Sep 13, 2023

atomb Sep 13, 2023

robin-aws Sep 13, 2023

atomb Sep 13, 2023

robin-aws Sep 13, 2023

robin-aws left a comment

atomb commented Sep 14, 2023

atomb commented Sep 14, 2023

atomb commented Sep 14, 2023

		@@ -0,0 +1,20 @@
		ProofDependencyLogging.dfy(176,11): Warning: unnecessary assumption
		ProofDependencyLogging.dfy(186,13): Warning: vacuous proof: assertion always holds

Proof dependency warnings #4542

Proof dependency warnings #4542

Conversation

atomb commented Sep 12, 2023

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Sep 13, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

atomb commented Sep 14, 2023

atomb commented Sep 14, 2023

atomb commented Sep 14, 2023

keyboardDrummer Sep 13, 2023 •

edited

Loading