Support multiple canVerifies having the same origin #6263

keyboardDrummer · 2025-06-05T15:14:53Z

What was changed?

Support multiple canVerifies having the same origin.
To support using some particular Dafny constructs in a test, I did some work to supporting deserialization of new types, although for some types that now have a [SyntaxConstructor], deserialization is still incorrect because it forgets to update the system module. Because I don't want to fix that last issue, and actually the test is fine without those constructs, I commented out those constructs in the test.
Fix bugs SyntaxDeserializerGenerator.cs related to [SyntaxBaseType]
Simplify serialization code

How has this been tested?

Added the test inputFormatDeleteSources.dfy, which deletes sources after parsing, then serializes, then deserializes and verifies

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

robin-aws

Hugely appreciate the help completing the solution.

On testing, yes I think we should have at LEAST one binary file that triggers the issues we were hitting, which I think is easier than creating the program programmatically (and provides more binary format coverage to boot). It's probably easiest to whittle down the temp.dbin I gave you. I tried to build one up from a small example and manually changing locations but it wasn't immediately reproducing the problems.

Beyond that (not blocking this PR going in), we could also consider mutating a subset of the integration test suite to change their source locations and ensure the verification behavior is the same. Even if the current suite passes with these changes, I still worry there are other cases where verification doesn't work correctly on the binary format.

robin-aws · 2025-06-10T21:45:03Z

Source/DafnyCore/Pipeline/Compilation.cs


-          return result.GroupBy(t => ((IOrigin)t.ScopeToken).GetFilePosition()).ToDictionary(
+          return result.GroupBy(t => {
+            var dafnyToken = (CanVerifyOrigin)t.ScopeToken;


I think overall this is a good approach, because although I think we could easily have edge cases where we could have a verification task with a ScopeToken that isn't attached to a ICanVerify somehow, that will be a hard casting exception here so it won't be a silent failure.

I think the more likely bad scenario is that the ScopeToken is attached to an ICanVerify, but not one that Dafny's front-end found, like a by-method or something nested inside an iterator, but I don't see a way to detect that scenario.

You want to at some point ask: did I assign every created verification task to an ICanVerify? But I don't think we have a good time to ask that question.

Agreed, I'm still not resting easy that there isn't still a bad edge case in here. But this PR is definitely a big step in the right direction.

robin-aws · 2025-06-10T21:47:54Z

Source/DafnyCore/Pipeline/Compilation.cs

+          tasksForModule.GetValueOrDefault(canVerify) ??
          new List<IVerificationTask>(0);


I think these existing fallbacks to an empty list of verification tasks here (either because it's not in the dictionary or mapped to null) is the most dangerous part remaining. That's where we get silently failing to verify verifiable things. Does everything work if we take this out and just crash if the canVerify isn't mapped to anything?

An ICanVerify that produces no tasks, like a method without any assertions, seems like a valid happy case, so I don't think we can take this out.

robin-aws · 2025-06-10T21:48:45Z

Source/DafnyCore/Verifier/BoogieGenerator.cs


 namespace Microsoft.Dafny {
+
+  class CanVerifyOrigin : OriginWrapper {


Worth a comment why this exists.

robin-aws · 2025-06-10T21:56:50Z

Source/DafnyCore/Pipeline/Compilation.cs

-      return false;
+    var result = false;
+    foreach (var canVerify in canVerifies) {
+      result |= await VerifyCanVerify(canVerify, taskFilter ?? (_ => true), randomSeed, onlyPrepareVerificationForGutterTests);


I don't think this return value makes sense. Before a boolean made sense because it was saying "is there something verifiable at this location", and CliCompilation.VerifyAllLazily was using that to determine whether to track the canVerify for later. Now that caller is using VerifyCanVerify instead, and the only caller left that actually looks at the result value is VerificationHandler.Handle(VerificationParams), and that method's boolean result is meant to mean "has this request been handled", which should be true when we get here no matter what.

TL;DR I think the return type of VerifyLocation should be Task now instead of Task<bool>.

It will still return false if this canVerify is currently already being verified or has already been verified, or if options specify that it should not be verified.

and that method's boolean result is meant to mean "has this request been handled"

I don't think so. I think it means to tell the client whether this thing started verifying or not.

Okay I'll trust your greater familiarity on this. I was only wary because I tried exactly this version myself and it didn't function correctly, but I also didn't replace VerifyLocation with VerifyCanVerify as you did.

keyboardDrummer · 2025-06-11T08:53:04Z

Hugely appreciate the help completing the solution.

On testing, yes I think we should have at LEAST one binary file that triggers the issues we were hitting, which I think is easier than creating the program programmatically (and provides more binary format coverage to boot).

I'd rather not have a binary file in the tests since I want to be able to change the format without breaking tests. Maybe we can have a tests that parses a .dfy file, resets all the source locations, and then continues.

…afny into fixMultipleSameOrigins

robin-aws

Not fully satisfied we're completely out of danger, but this is definitely a big improvement at least! No comments are blocking, just good for the next related PR.

robin-aws · 2025-06-11T20:33:21Z

Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs

  public ClassDecl(IOrigin origin, Name nameNode, Attributes? attributes,
    List<TypeParameter> typeArgs, ModuleDefinition enclosingModuleDefinition,
-    [Captured] List<MemberDecl> members, List<Type> traits, bool isRefining)
+    [Captured] List<MemberDecl> members, List<Type>? traits, bool isRefining)


Not blocking, but seems like this shouldn't be nullable.

Down the line there's this code Traits = traits ?? [], but I'll remove it in a follow-up since it's a bit ugly.

robin-aws · 2025-06-11T20:39:16Z

Source/Scripts/SourceToBinary.cs

-      new StreamWriter(file2.FullName)),
-      inputArgument, outputArgument);
+
+    var deleteSourcesOption = new Option<bool>("--delete-sources");


Option is worth a docstring even just to understand better when reading the source here.

Name makes me think we deleting source code though, perhaps --delete-source-locations?

robin-aws · 2025-06-11T20:40:03Z

Source/Scripts/SourceToBinary.cs

+      }
+
+      if (current is NodeWithOrigin withOrigin && withOrigin.Origin != Token.NoToken) {
+        var token = new Token(-1, -1) { Uri = withOrigin.Origin.Uri };


Good bang for the buck coverage with this approach. For the record I'm still a bit worried the hanging I observed when locations were different but overlapped isn't covered.

robin-aws · 2025-06-11T20:41:11Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/inputFormatDeleteSources.dfy

+  return 1 + 2;
+}
+
+// opaque predicate P() { true }


Worth a comment explaining why these are here (I think it's "these are good to test too but they aren't working correctly yet"?)

Or would it be possible to uncomment them anyway? You made a bunch of nullability declaration changes and updated the schema, but those new cases for the binary format aren't being tested otherwise AFAICT.

robin-aws · 2025-06-11T20:42:52Z

Source/DafnyCore/Pipeline/Compilation.cs


-          return result.GroupBy(t => ((IOrigin)t.ScopeToken).GetFilePosition()).ToDictionary(
+          return result.GroupBy(t => {
+            var dafnyToken = (CanVerifyOrigin)t.ScopeToken;


Agreed, I'm still not resting easy that there isn't still a bad edge case in here. But this PR is definitely a big step in the right direction.

robin-aws · 2025-06-11T20:43:43Z

Source/DafnyCore/Pipeline/Compilation.cs

-      return false;
+    var result = false;
+    foreach (var canVerify in canVerifies) {
+      result |= await VerifyCanVerify(canVerify, taskFilter ?? (_ => true), randomSeed, onlyPrepareVerificationForGutterTests);


Okay I'll trust your greater familiarity on this. I was only wary because I tried exactly this version myself and it didn't function correctly, but I also didn't replace VerifyLocation with VerifyCanVerify as you did.

keyboardDrummer added 7 commits June 5, 2025 17:14

Support multiple canVerifies having the same origin

530e0c2

Rely less on source location

2fa969d

Removed unuserd

8d59692

Fix

54841f3

Fix

80ae91e

Some fixes

b247f8f

Merge branch 'master' into fixMultipleSameOrigins

ad9b8e5

keyboardDrummer requested a review from robin-aws June 10, 2025 17:17

keyboardDrummer marked this pull request as ready for review June 10, 2025 17:17

robin-aws reviewed Jun 10, 2025

View reviewed changes

keyboardDrummer added 6 commits June 11, 2025 13:34

Fixes

2a49988

Tweaks

04ce86b

Fixes

769742a

new test passes

7aaf7dd

Merge branch 'fixMultipleSameOrigins' of github.com:keyboardDrummer/d…

49382b7

…afny into fixMultipleSameOrigins

Delete temporary file

7280284

keyboardDrummer requested a review from robin-aws June 11, 2025 15:35

keyboardDrummer enabled auto-merge (squash) June 11, 2025 15:36

Merge branch 'master' into fixMultipleSameOrigins

7cdded3

robin-aws approved these changes Jun 11, 2025

View reviewed changes

keyboardDrummer merged commit 62f1b85 into dafny-lang:master Jun 11, 2025
22 checks passed

		tasksForModule.GetValueOrDefault(canVerify) ??
		new List<IVerificationTask>(0);


		namespace Microsoft.Dafny {

		class CanVerifyOrigin : OriginWrapper {

Support multiple canVerifies having the same origin #6263

Support multiple canVerifies having the same origin #6263

Uh oh!

Conversation

keyboardDrummer commented Jun 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What was changed?

How has this been tested?

Uh oh!

robin-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jun 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jun 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jun 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer commented Jun 11, 2025

Uh oh!

robin-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jun 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

keyboardDrummer commented Jun 5, 2025 •

edited

Loading

keyboardDrummer Jun 11, 2025 •

edited

Loading

keyboardDrummer Jun 11, 2025 •

edited

Loading

keyboardDrummer Jun 11, 2025 •

edited

Loading

keyboardDrummer Jun 12, 2025 •

edited

Loading