Basic implementation of proof dependency analysis #4461

atomb · 2023-08-23T21:11:14Z

This enables experimental support for tracking proof dependencies, currently not advertised and enabled only by using the Boogie -trackVerificationCoverage option.

When that option is enabled, the log produced by /verificationLogger:text or --log-format text now includes the proof dependencies required to prove each assertion batch, along with the list of assertions that were proved in that batch. Each dependency includes a source range rather than just a single location, which can identify cases where only a specific sub-expression was required for the proof. The tests includes examples of this.

Although the proper UI for proof dependencies isn't yet in place, a nice side effect of how this reports proof dependencies is that it's relatively easy to see vacuous proofs by looking for assertions that were proved but not included in the proof dependency list for their assertion batch. This will be automated in a future PR, but is already possible with a little manual work.

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

Source/DafnyCore/Verifier/Translator.cs

Source/DafnyCore/Verifier/Translator.BoogieFactory.cs

Source/DafnyCore/Verifier/ProofDependency.cs

keyboardDrummer · 2023-08-30T12:42:30Z

Source/DafnyCore/Verifier/ProofDependency.cs

+ }
+}
+
+public class InvariantDependency : ProofDependency {


If these classes are only used in a single location, then I suggest you place them there.

This one, for invariant dependencies, is used in only one place (at the moment -- that could change). But most of the rest of the ProofDependency implementations are used in multiple locations. It feels more comprehensible to me to have them all in the same place.

keyboardDrummer · 2023-08-30T12:57:41Z

Source/DafnyCore/Verifier/Translator.cs

+ public void AddProofDependencyId(ICarriesAttributes boogieNode, IToken tok, ProofDependency dep) {
+ var idString = GetProofDependencyId(dep);
+ boogieNode.Attributes =
+ new QKeyValue(tok, "id", new List<object>() { idString }, boogieNode.Attributes);


Is id an attribute name that triggers something, or is it only used by the code in this PR ? Please reference it using a constant where the constant leads me to documentation about what it does.

It's used by Boogie. I'll pull it out into a named constant with an explanation.

keyboardDrummer · 2023-08-30T12:59:20Z

Source/DafnyCore/Verifier/Translator.cs

+ // Get the full ProofDependency indicated by a compound ID string.
+ public ProofDependency GetFullIdDependency(string idString) {
+ var parts = idString.Split('$');
+ if (idString.EndsWith("$requires") && parts.Length == 3) {


Where do the magic strings in this function come from? Please reference constants instead.

These come from Boogie. I'll pull them out into named constants and explain them.

keyboardDrummer · 2023-08-30T13:03:31Z

Source/DafnyCore/Verifier/Translator.cs

+ public void AddProofDependencyId(ICarriesAttributes boogieNode, IToken tok, ProofDependency dep) {
+ var idString = GetProofDependencyId(dep);
+ boogieNode.Attributes =
+ new QKeyValue(tok, "id", new List<object>() { idString }, boogieNode.Attributes);


Why are we using a string idString instead of directly storing dep in the attribute, so you won't need the ProofDependencyManager?

If the purpose is for the Boogie code to be printable and for a person to be able to map that print back to the original Dafny code, then I think you'll have to base the ids on Dafny source locations instead of generating them, and then you also wouldn't need a ProofDependencyManager.

The reason for this is that Boogie needs to have a string to send to Z3 -- that's the only way to specify the label on an expression you want to track for proof dependencies. Then Z3 returns a set of strings indicating which pieces it used. The notion of proof dependency that we have in Dafny is Dafny-centric, so it wouldn't make sense to have the ProofDependency class in Boogie. It's possible that we could have an additional layer of abstraction in the Boogie implementation, so we'd have 1) names as strings, 2) structured Boogie conceptions of those strings, and 3) structured Dafny conceptions that build on the Boogie ones. But I'm not sure that that additional layer is really worth it.

The reason for this is that Boogie needs to have a string to send to Z3

Why not do the id generation with AST node mapping in Boogie? Seems better to let Boogie encapsulate SMT generation. Then you don't need the method GetFullIdDependency in Dafny and references to the coverage related string constants, and to move around the ProofDependencyManager. VCResult.coveredElements would then have type IEnumerable<Absy> instead of IEnumerable<string>.

Although on the surface it seems like an Absy would encapsulate everything that we need, in practice this isn't the case because of how Boogie transforms the original program and how particular nodes are used in different ways in a proof (such as how a requires clause is an assumption when proving a definition itself, but a proof goal when invoking that definition). So, we'd need something like ProofDependency in Boogie, but it couldn't be quite the same thing, because those program constructs don't map cleanly back from Boogie to Dafny. So we'd need both a BoogeProofDependency and a DafnyProofDependency, and I don't think that extra layer of indirection is worthwhile at the moment.

Although on the surface it seems like an Absy would encapsulate everything that we need, in practice this isn't the case because of how Boogie transforms the original program and how particular nodes are used in different ways in a proof (such as how a requires clause is an assumption when proving a definition itself, but a proof goal when invoking that definition)

I don't see that, since each id, also a complex one like {requireId}${callId}$requires, ends up being attached to a unique Absy instance. Regarding your example, a separate Absy exists for each pair of call and requires clause, and a separate one for each requires clause.

This PR

Dafny attaches ids to Absys, while keeping an id -> ProofDependency mapping

Boogie creates more Absys and attaches ids to them that are combinations of ids provided by Dafny

Boogie gets used ids from the unsat core and exposes them in VCResult.coveredElements

Dafny parses the ids, sometimes combined ones, to find ids generated by Dafny, maps those back to -ProofDependencys and the combined ones to combined ProofDependencys

Alternative:

Let Dafny attach ITokens to Absys (already happens)

Let Dafny mark Absys that it wants to track usages on

Boogie creates more Absys, attaching ITokens to them that are combinations of tokens provided by Dafny.

Boogie attaches ids to Absys that are marked for tracking, while keeping an id -> Absy mapping.

Boogie gets used ids from the unsat core, maps them back to Absys and exposes them in VCResult.coveredElements

Dafny uses the tokens in Absys from VCResult.coveredElements to display UI.

The advantage of the latter is that more complexity moves to Boogie and Boogie encapsulates the interaction with the SMT solver.

The ITokens used can be the current ProofDependency sub-classes, although they would then have to inherit from IToken

Dafny can't keep track of an Absy -> ProofDependency map because Boogie introduces new Absy nodes during internal transformations that Dafny knows nothing about. Boogie would end up returning Absy nodes that Dafny has never seen, and therefore can't be in the map Dafny created.

Dafny can't keep track of an Absy -> ProofDependency map

In what I described, it does not. Dafny does not keep track of anything. It retrieves an IEnumerable<Absy> from VCResult.coveredElements and those Absy contain ITokens with all the information that ProofDependency currently provides.

But IToken values don't (and I believe shouldn't) track all of the information that ProofDependency values do.

In particular, at least one of the ProofDependency types, and likely more in the future, keep the original Dafny AST node that gave rise the dependency. That's only lightly used at the moment, but will need to be used more heavily in the upcoming changes I have planned.

It is also important to be able to print the Boogie files, as you suggest above, and encoding IDs in those that refer simply to Dafny source locations won't be enough, because Dafny source locations overlap too much. A single expression can result in multiple proof dependencies.

Source/DafnyCore/Verifier/Translator.cs

keyboardDrummer · 2023-08-30T13:24:05Z

Test/logger/ProofDependencyLogging.dfy

@@ -0,0 +1,424 @@
+// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t"


I'm still a little puzzled on the UX.

One use-case that's clear to me is giving warnings whenever code is not used by any assertion batch. For that I wouldn't use this report, but instead turn on a warning --warn-unused-by-verification

Can you give an example of how how the information presented in this report would be used?

Yeah, this isn't really meant to be something that would be used by anyone other than the Dafny developers in its current state. It could be, but would require some expertise and manual effort. I'm building a more useful set of UI mechanisms on top of it, but I want to merge this now to get things done in pieces so there's not one monster PR to review. :) Think of it similarly to the type system refresh @RustanLeino is doing.

Okay, that works.

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

Source/DafnyCore/Verifier/ProofDependency.cs

…rage-ids

Temporary until we fix a Boogie concurrency bug

And remove concurrency limitation from proof dependency test.

…rage-ids

keyboardDrummer · 2023-09-07T13:41:48Z

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

- builder.Add(Assert(tok, ss.E, desc, wfOptions.AssertKv));
- } else {
- builder.Add(AssertNS(tok, ss.E, desc));
+ // the check for .reads function must be translated explicitly: their declaration lacks


This change is harder to review because it's part of a very large method, so it's not easy to find the method header and gather context about what this code is supposed to do.

I see this is part of a block to check the well-formedness of a call expression. Could we put that block in a separate method?

Also, could you see if you can come up with a method name that describes either the whole block between line 714 to 762 or one of the sub blocks, and if so put that in a separate method? Maybe something like CheckReadsClauseSatisfied

Hmm. I wonder whether this change and the others you comment on below are an artifact of the PR not being up-to-date with master? Because they aren't changes made by this PR. There's some recent work @jtristan made to resolve a soundness issue that touches the same files, and that I had to resolve conflicts to merge with, and I think the changes you're pointing to are from that. Were you reviewing an intermediate commit, perhaps?

Ah yes, I was reviewing a diff I shouldn't have. Please ignore the comments.

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

keyboardDrummer

Approved, but if you could either in this PR or in a follow-up address the remaining comments, that'd be much appreciated.

atomb and others added 14 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

atomb self-assigned this Aug 28, 2023

atomb added 3 commits August 28, 2023 16:52

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

atomb marked this pull request as ready for review August 29, 2023 16:42

atomb requested review from keyboardDrummer, MikaelMayer and robin-aws August 29, 2023 16:42

keyboardDrummer reviewed Aug 30, 2023

View reviewed changes

atomb added 7 commits August 30, 2023 09:28

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

atomb enabled auto-merge (squash) August 31, 2023 03:06

keyboardDrummer reviewed Aug 31, 2023

View reviewed changes

Source/DafnyCore/Verifier/ProofDependency.cs Show resolved Hide resolved

atomb added 4 commits August 31, 2023 18:43

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

atomb disabled auto-merge September 5, 2023 23:56

atomb added 4 commits September 5, 2023 16:57

Fix customBoogie.patch

5e75656

Bump Boogie dependency

1f9f243

And remove concurrency limitation from proof dependency test.

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

c2a7c60

…rage-ids

Bump Boogie version in dotnet-tools.json, too

9e4bd05

atomb enabled auto-merge (squash) September 6, 2023 17:25

keyboardDrummer reviewed Sep 7, 2023

View reviewed changes

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs Outdated Show resolved Hide resolved

keyboardDrummer reviewed Sep 7, 2023

View reviewed changes

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs Outdated Show resolved Hide resolved

keyboardDrummer reviewed Sep 7, 2023

View reviewed changes

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs Outdated Show resolved Hide resolved

keyboardDrummer approved these changes Sep 7, 2023

View reviewed changes

Merge branch 'master' into verification-coverage-ids

582421c

atomb merged commit 2537367 into dafny-lang:master Sep 7, 2023
18 checks passed

atomb deleted the verification-coverage-ids branch January 4, 2024 16:35

keyboardDrummer mentioned this pull request Jan 23, 2024

Warn on expressions that never change value #3023

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Basic implementation of proof dependency analysis #4461

Basic implementation of proof dependency analysis #4461

atomb commented Aug 23, 2023 •

edited

Loading

keyboardDrummer Aug 30, 2023

atomb Aug 30, 2023

keyboardDrummer Aug 30, 2023

atomb Aug 30, 2023

keyboardDrummer Aug 30, 2023

atomb Aug 30, 2023

keyboardDrummer Aug 30, 2023

atomb Aug 30, 2023 •

edited

Loading

keyboardDrummer Aug 31, 2023 •

edited

Loading

atomb Aug 31, 2023

keyboardDrummer Aug 31, 2023 •

edited

Loading

atomb Aug 31, 2023

keyboardDrummer Sep 1, 2023 •

edited

Loading

atomb Sep 1, 2023

atomb Sep 1, 2023

atomb Sep 1, 2023

keyboardDrummer Aug 30, 2023

atomb Aug 30, 2023

keyboardDrummer Aug 31, 2023

keyboardDrummer Sep 7, 2023

atomb Sep 7, 2023

keyboardDrummer Sep 7, 2023

keyboardDrummer left a comment

		@@ -0,0 +1,424 @@
		// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t"

Basic implementation of proof dependency analysis #4461

Basic implementation of proof dependency analysis #4461

Conversation

atomb commented Aug 23, 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

atomb Aug 30, 2023 • edited Loading

Choose a reason for hiding this comment

keyboardDrummer Aug 31, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Aug 31, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Sep 1, 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

keyboardDrummer left a comment

Choose a reason for hiding this comment

atomb commented Aug 23, 2023 •

edited

Loading

atomb Aug 30, 2023 •

edited

Loading

keyboardDrummer Aug 31, 2023 •

edited

Loading

keyboardDrummer Aug 31, 2023 •

edited

Loading

keyboardDrummer Sep 1, 2023 •

edited

Loading