feat: Verification diagnostics hover #1946

MikaelMayer · 2022-03-29T17:53:19Z

This PR adds assertion information when hovering them (without needing to change the VSCode plugin).

Hovering over f (empty body):

Hovering over f (one failing assertion), "assertion batch" points to this link.

Hovering over false, "Error" points to this link.

Hovering over a failing postcondition shows where the return path is failing

Hovering over x == 2

Hovering over true, I tried to put it in green but it does not work.

Hovering over f but this time there are 3 assertions. It indicates the longest batch and where it started:

Hovering over a lemma very expensive to verify before it starts verifying
Hovering over a lemma very expensive to verify before it finishes verifying
Hovering over a lemma very expensive to verify, the warning icon points to this link.
Hovering over a lemma very expensive to verify with multiple assertion batches:

Formal tests

One way to discover the effect of this PR is by visiting the first hover test

Implementation

Everything in this feature is in DafnyHoverHandler.cs, the method Handle

First, instead of immediately returning an hover when a symbol is found, I first compute symbolHoverContent (for type information) and diagnosticGoverContent (for verification performance and insights). If the diagnostics are only about statistics of an entire method (not individual assertions), it should not be displayed if there is a symbol under the caret, to prevent distractions, and areMethodStatistics is set to true in that case.

      var hoverContent = areMethodStatistics && symbolHoverContent != null ? "" : (diagnosticHoverContent ?? "");
      hoverContent = symbolHoverContent != null ? hoverContent + (hoverContent != "" ? "  \n" : "") + symbolHoverContent : hoverContent;

diagnosticHoverContent is assigned using the new method GetDiagnosticsHover
- In this method, I am traversing the hierarchy of TopLevelDeclMemberVerificationTree, then I skip their children (which are implementations that users don't care about), and traverse instead the aggregated node.AssertionBatches which are of type AssertionBatchVerificationTree. I'm keeping track of the assertion batch index with assertionBatchIndex to be able to display it to users.
- Since every node contains a Range, I can only traverse node that contain the hovering position, which is efficient. I can't do a binary search however because I don't require verification trees to be ordered by range.
- I either give two kinds of hovering statistics: Individual assertions or per-method/subset type/field. If an individual assertion is hovered, the per-method statistics are not displayed.
  - For an individual assertions, I tolerate it's "hovered" also if the hover position is touching an ImmediatelyRelatedRange (i.e. the postcondition for return AssertCmd). assertionNode.ImmediatelyRelatedRanges.Any(range => range.Contains(position))
  - I then add all the statistics in the string information: The assertion number and total number of assertions in this batch (only if it's more than 1), the batch number over the total number of batches and its timing and resource count.
  - If the assertion is for a return statement and we are hovering the postcondition (which has normally no error associated with it), I display the position of the corresponding return (which contains more information about the error)
  - If there is a counter example for the current assertion, I use its Description to generate an even better message about its status. (i.e. SetDescription(returnCounterexample.FailingReturn.Description);)
  - At the end, I display "recently" if the status is obsolete, or "recently and verifying..." if the status of the current assertion is verifying (which is not implemented yet but soon)
- If there is no information about a single assertion this PR checks if the hover position is on the first line of a method (after the method name, because that's the first token of a method 😕 ), and if so:
  - I display "Verification not started yet" if its status is "Obsolete" (not started yet)
  - I display "Still verifying" and the time elapsed if the status is "Verifying" (started to verify)
  - I display the top 3 most expensive assertion batch with their resource usage.

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

This reverts commit 51c876a.

This reverts commit 467a92e.

MikaelMayer

This PR is ready for review.

MikaelMayer · 2022-05-12T21:09:49Z

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

+ // When hovering the failing path, it does not display the position of the failing postcondition
+ // because the IDE extension already does it.
+ await AssertHoverMatches(documentItem, (5, 4),
+ @"assertion #1/2 of [batch](???) #1/1 checked in ???ms with ??? resource count: 


Question to reviewers: should I display batch #1/1 when there is only one batch?
It's useful to have the word batch so that the link is available, but I could as well put the link on assertion and remove of batch #1/1. I currently favored consistency with other messages.

Yeah, I think it's reasonable to always say what batch it's in, partly because it clarifies that the time and resource counts listed are for batches, not individual assertions (and only apply to individual assertions if they're 1/1 in the current batch).

MikaelMayer · 2022-05-13T16:00:30Z

Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs

@@ -123,7 +123,7 @@ IDiagnosticPublisher diagnosticPublisher
 /// </summary>
 /// <param name="implementations">The implementations to be verified</param>
 public void ReportImplementationsBeforeVerification(Implementation[] implementations) {
- if (document.LoadCanceled || implementations.Length == 0) {
+ if (document.LoadCanceled) {


About this: It happenes that in the past somewhere, for some time, this function was called twice, once without any implementations, and the other one with all the implementations. This started to happen after I had merged once with master, so I had this guard to prevent this. However, it would not enable to consider files without really any implementation to verify.
This "bug" does not happen anymore (probably thanks to recent's refactoring with Boogie) so I remove this check.

atomb

The only one of my comments that I think it's important to address before merging is the one about assertion batch numbering/ordering.

atomb · 2022-05-13T20:27:20Z

Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs

+
+ public AssertionBatchVerificationTree? GetLongestAssertionBatch() =>
+ !AssertionBatches.Any() ? null :
+ AssertionBatches.MaxBy(assertionBatch => assertionBatch.TimeSpent);


Could this be AssertionBatchTimes.Max()?

Only if I only wanted the time, but I want the entire assertion batch.

Oh, of course! 🤦

atomb · 2022-05-13T20:40:18Z

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

+ } while (lastResult.Status != CompilationStatus.VerificationFailed &&
+ lastResult.Status != CompilationStatus.VerificationSucceeded &&
+ lastResult.Status != CompilationStatus.ParsingFailed &&
+ lastResult.Status != CompilationStatus.ResolutionFailed);


Would it be worth having a separate definition for "done" that encapsulates these? It would make the code a little less messy, and would make it clear what the meaning of that big conjunction is.

Would it be worth having a separate definition for "done" that encapsulates these? It would make the code a little less messy, and would make it clear what the meaning of that big conjunction is.

Refactored, thanks for pointing this out.

atomb · 2022-05-13T21:14:07Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+
+ private string? GetDiagnosticsHover(DafnyDocument document, Position position, out bool areMethodStatistics) {
+ areMethodStatistics = false;
+ foreach (var node in document.VerificationTree.Children.OfType<TopLevelDeclMemberVerificationTree>()) {


Eventually it might be possible to use a more efficient data structure for this, but that's probably only worth it if we find that this repeated iteration is too expensive.

In the past I've done this type of thing by first finding a particular AST element, in this case it would be finding the assertion statement, which you do by checks of the node.Range.Contains(position) starting at the root node of the tree. That's similar to what's being done here although it would include modules and classes as filters. I think for finding elements in lists, like finding a particular statement in a list of statements, you can also do a binary search instead of a linear traversal.

Then given a particular AST node, compilation results relating to that AST node, such as resolved declarations for nodes that are references, or in this case verification performance data, should be attached to it using some form of a dictionary.

@MikaelMayer have you considered storing the verification results on the AST instead of on a separate tree that mimics parts of the AST?

I haven't considered changing the AST to store verification results there, not just because I think it is better if we modified the AST as little as possible,
but especially because the AST does not have the notion of implementations and assertion batches like what we get from verification.

especially because the AST does not have the notion of implementations and assertion batches like what we get from verification.

Good point. Food for thought :-)

atomb · 2022-05-13T21:16:48Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+ var assertionBatchIndex = -1;
+ var information = "";
+ foreach (var assertionBatch in node.AssertionBatches) {
+ assertionBatchIndex += 1;


It might not always be the case that the assertion batches are listed in order. This should probably use VCResult.vcNum, piped through appropriately. The assertions in each batch should always be in the same order, though.

I did not know about vcNum, that's a great insight ! I refactored the code to make use of it instead of a counter that is incrementing. It will even make the migration of assertion batch diagnostics easier down the road since this counter is probably more deterministic than mine.

# Conflicts: # Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

keyboardDrummer · 2022-05-20T18:59:58Z

For the UX, how would diagnostic hints (they show up as ... under the first bit of the range they cover) compare to hover? I'm wondering if hints will provide greater discoverability of this feature.

keyboardDrummer · 2022-05-20T19:02:28Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+ return CreateMarkdownHover(hoverContent);
+ }
+
+ class TupleComparer : IComparer<(int, int)> {


Isn't this the default way of comparing tuples? https://stackoverflow.com/a/27781538/93197

After I changes tuples to a record, I kept this class since the tuple comparison wouldn't work anymore, but thanks for this interesting finding !

keyboardDrummer · 2022-05-20T19:09:14Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+
+ private string? GetDiagnosticsHover(DafnyDocument document, Position position, out bool areMethodStatistics) {
+ areMethodStatistics = false;
+ foreach (var node in document.VerificationTree.Children.OfType<TopLevelDeclMemberVerificationTree>()) {


In the past I've done this type of thing by first finding a particular AST element, in this case it would be finding the assertion statement, which you do by checks of the node.Range.Contains(position) starting at the root node of the tree. That's similar to what's being done here although it would include modules and classes as filters. I think for finding elements in lists, like finding a particular statement in a list of statements, you can also do a binary search instead of a linear traversal.

Then given a particular AST node, compilation results relating to that AST node, such as resolved declarations for nodes that are references, or in this case verification performance data, should be attached to it using some form of a dictionary.

@MikaelMayer have you considered storing the verification results on the AST instead of on a separate tree that mimics parts of the AST?

keyboardDrummer · 2022-05-20T19:14:16Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+ }
+ }
+
+ private string? GetDiagnosticsHover(DafnyDocument document, Position position, out bool areMethodStatistics) {


This method seems fairly long. Is there are way to cut it up into smaller parts?

Thanks for pointing it out ! I refactored it in 3 smaller parts.

keyboardDrummer · 2022-05-20T19:18:27Z

Source/DafnyLanguageServer/Workspace/DafnyDocument.cs

@@ -64,5 +64,9 @@ public record DafnyDocument(
 }

 public int LinesCount => VerificationTree.Range.End.Line;
+
+ public static int NumberOfLines(string text) {
+ return text.Count(c => c == '\n') + 1;


I don't think we should compute a number of lines from the full text anywhere besides in TextChangeProcessor. Instead of working with TextDocumentItem we can work with our own datatype (like DocumentTextBuffer) that besides storing the text as a string also stores the number of lines.

In the future we'll change TextChangeProcessor so it'll update DocumentTextBuffer with a cost linear to the amount of changes (instead of the the current cost which is linear in the document size). I'm not sure what the text buffer data-structure will look like, but maybe this can inspire us: https://code.visualstudio.com/blogs/2018/03/23/text-buffer-reimplementation

I implemented your suggestion, I like it ! Makes more sense than in the DafnyDocument.

keyboardDrummer · 2022-05-20T19:20:10Z

Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs

 // Recomputed from the children which are ImplementationVerificationTree
- public List<AssertionBatchVerificationTree> AssertionBatches { get; set; } = new();
+ public ImmutableDictionary<(int, int), AssertionBatchVerificationTree> AssertionBatches { get; private set; } =


Could you replace the anonymous tuple in this field with a record to make it easier to understand what the field contains?

I replaced it with the record ASsertionBatchIndex for now

MikaelMayer · 2022-05-23T19:42:43Z

For the UX, how would diagnostic hints (they show up as ... under the first bit of the range they cover) compare to hover? I'm wondering if hints will provide greater discoverability of this feature.

Here my quick and probably incomplete thinking about hints vs hovering:

Hints required the language server pushing them. I'm not sure I want to push information about 1000 asserts in a single file.
I don't worry about the discoverability if it is implemented using the hovering mechanism, because

For single failing assertions, user already are used to hover them to see the error message.
For methods since the hover is for the entire line, users will very likely always accidentally discover this feature very quickly.

AssertionBatchIndex record

…afny-lang/dafny into verification-diagnostics-hover

atomb

This is a great feature! And I think all of the previous comments from @keyboardDrummer and myself have been addressed.

atomb · 2022-05-24T23:42:08Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs


 namespace Microsoft.Dafny.LanguageServer.Handlers {
 public class DafnyHoverHandler : HoverHandlerBase {
 // TODO add the range of the name to the hover.
 private readonly ILogger logger;
 private readonly IDocumentDatabase documents;

+ private const int RuLimitToBeOverCostly = 10000000;


I'm not entirely sure this is the right value, but I think we'll only find out by using it in practice.

atomb · 2022-05-24T23:45:20Z

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

+ // When hovering the failing path, it does not display the position of the failing postcondition
+ // because the IDE extension already does it.
+ await AssertHoverMatches(documentItem, (5, 4),
+ @"assertion #1/2 of [batch](???) #1/1 checked in ???ms with ??? resource count: 


Yeah, I think it's reasonable to always say what batch it's in, partly because it clarifies that the time and resource counts listed are for batches, not individual assertions (and only apply to individual assertions if they're 1/1 in the current batch).

keyboardDrummer · 2022-05-25T13:18:51Z

Source/DafnyLanguageServer/Workspace/ChangeProcessors/TextChangeProcessor.cs

 // https://microsoft.github.io/language-server-protocol/specifications/specification-3-17/#textDocumentContentChangeEvent
 return change.Text;
 }
 int absoluteStart = change.Range.Start.ToAbsolutePosition(text, cancellationToken);
 int absoluteEnd = change.Range.End.ToAbsolutePosition(text, cancellationToken);
+ numberOfLines -=
+ DocumentTextBuffer.ComputeNumberOfNewlines(text.Substring(absoluteStart, absoluteEnd - absoluteStart));
+ numberOfLines += DocumentTextBuffer.ComputeNumberOfNewlines(change.Text);


Seems like you can combine line 39 and 31 by putting line 39 before line 30.

keyboardDrummer · 2022-05-25T13:23:01Z

Source/DafnyLanguageServer/Workspace/DafnyDocument.cs

+
+ public int NumberOfLines { get; init; } //
+
+ public static int ComputeNumberOfLines(string text) {


I would put this function and the next in TextChangeProcessor and make NumberOfLines a parameter of DocumentTextBuffer

keyboardDrummer · 2022-05-25T13:27:36Z

Source/DafnyLanguageServer/Workspace/DafnyDocument.cs

+ };
+ }
+
+ public int NumberOfLines { get; init; } //


Is init used? // can be removed.

keyboardDrummer · 2022-05-25T13:34:34Z

Source/DafnyLanguageServer/Workspace/ChangeProcessors/TextChangeProcessor.cs

 };
 }

- private static string ApplyTextChanges(string originalText, Container<TextDocumentContentChangeEvent> changes, CancellationToken cancellationToken) {
+ private static string ApplyTextChanges(string originalText, int originalLines, Container<TextDocumentContentChangeEvent> changes, out int numberOfLines, CancellationToken cancellationToken) {


I think we can clean up these APIs by letting DafnyDocument not contain a TextDocumentItem but instead a VersionedTextDocumentIdentifier (containing the Version and Uri) and a DocumentTextBuffer (containing just the text and the # of lines), and then these APIs could take and return a DocumentTextBuffer.

But we might want to do this in a follow-up PR since these changes are all a bit out of scope of hover.

At some point we should also move PositionsExtensions.ToAbsolutePosition to DocumentTextBuffer and implement it in constant time.

keyboardDrummer · 2022-05-25T13:35:35Z

Source/DafnyLanguageServer/Workspace/DafnyDocument.cs

@@ -45,7 +45,7 @@ public record DafnyDocument(
 /// </summary>
 public VerificationTree VerificationTree { get; init; } = new DocumentVerificationTree(
 TextDocumentItem.Uri.ToString(),
- TextDocumentItem.Text.Count(c => c == '\n') + 1
+ TextDocumentItem.NumberOfLines


keyboardDrummer · 2022-05-25T13:55:05Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+
+ private string? GetDiagnosticsHover(DafnyDocument document, Position position, out bool areMethodStatistics) {
+ areMethodStatistics = false;
+ foreach (var node in document.VerificationTree.Children.OfType<TopLevelDeclMemberVerificationTree>()) {


especially because the AST does not have the notion of implementations and assertion batches like what we get from verification.

Good point. Food for thought :-)

keyboardDrummer · 2022-05-25T14:23:13Z

Hints required the language server pushing them. I'm not sure I want to push information about 1000 asserts in a single file.

Good callout. Let's start with hover and see how that works.

MikaelMayer added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) labels Mar 29, 2022

MikaelMayer requested review from keyboardDrummer and cpitclaudel March 29, 2022 17:53

MikaelMayer self-assigned this Mar 29, 2022

MikaelMayer marked this pull request as draft March 29, 2022 17:54

MikaelMayer mentioned this pull request Mar 29, 2022

feat: Verification diagnostics #1923

Closed

MikaelMayer force-pushed the verification-diagnostics-hover branch 2 times, most recently from dae48ba to 5b89eea Compare April 5, 2022 21:35

MikaelMayer force-pushed the verification-diagnostics-hover branch from 5b89eea to 6bb8800 Compare April 29, 2022 16:21

Base automatically changed from verification-diagnostics-core to master May 11, 2022 17:12

MikaelMayer added 9 commits May 12, 2022 13:42

Added resource and time diagnostics in the verification tree

fa983b8

This reverts commit 51c876a.

Hover feature to display verification diagnostics

e361e5f

This reverts commit 467a92e.

Renamed + removed dangerous methods

917b6ce

Added hover test

6aa5ada

Helper to debug failing tests

b1075da

More hovering tests

0025320

Better positive messages

b8df867

Refactored description generation

72419c6

Fixed the rebase

fb4b98a

MikaelMayer force-pushed the verification-diagnostics-hover branch from 076b5f4 to fb4b98a Compare May 12, 2022 18:51

MikaelMayer commented May 12, 2022

View reviewed changes

Fixed hovering

1f12fa6

MikaelMayer commented May 13, 2022

View reviewed changes

MikaelMayer added 3 commits May 13, 2022 12:56

Fixed a bug in newline counting which was not updated.

7fc5fbc

Fixed the boolean logic

08659a7

Fixed a CI test

765c738

MikaelMayer marked this pull request as ready for review May 13, 2022 19:01

MikaelMayer requested a review from atomb May 13, 2022 19:01

atomb requested changes May 13, 2022

View reviewed changes

MikaelMayer requested a review from atomb May 17, 2022 22:24

MikaelMayer and others added 6 commits May 17, 2022 18:07

3 more tests

04fe432

Merge branch 'master' into verification-diagnostics-hover

5493944

Merge branch 'master' into verification-diagnostics-hover

3026595

# Conflicts: # Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

Removed a TODO

1c3d310

Merge branch 'master' into verification-diagnostics-hover

9ba6631

Added a comment elsewhere

86fabf5

MikaelMayer mentioned this pull request May 19, 2022

Fix: Prevent diagnostics to "pass through" #2142

Merged

keyboardDrummer reviewed May 20, 2022

View reviewed changes

MikaelMayer and others added 2 commits May 23, 2022 16:59

Incremental newline computation,

a54794d

AssertionBatchIndex record

Merge branch 'master' into verification-diagnostics-hover

0a12a2c

MikaelMayer requested a review from keyboardDrummer May 23, 2022 22:18

MikaelMayer and others added 3 commits May 23, 2022 17:50

Merge branch 'master' into verification-diagnostics-hover

388a974

Merge branch 'verification-diagnostics-hover' of https://github.com/d…

ceb6509

…afny-lang/dafny into verification-diagnostics-hover

Merge branch 'master' into verification-diagnostics-hover

d26ed45

MikaelMayer mentioned this pull request May 24, 2022

Feat: Underline related errors in postconditions dafny-lang/ide-vscode#164

Merged

Merge branch 'master' into verification-diagnostics-hover

7e8375f

atomb previously approved these changes May 24, 2022

View reviewed changes

keyboardDrummer previously approved these changes May 25, 2022

View reviewed changes

MikaelMayer and others added 3 commits May 26, 2022 12:33

Merge branch 'master' into verification-diagnostics-hover

60d48d5

Line computation simplified

143cd23

Review suggestions

ac0f2a3

MikaelMayer dismissed stale reviews from keyboardDrummer and atomb via ac0f2a3 May 26, 2022 18:15

keyboardDrummer approved these changes May 26, 2022

View reviewed changes

MikaelMayer merged commit fe2465a into master May 26, 2022

MikaelMayer deleted the verification-diagnostics-hover branch May 26, 2022 19:30


		public int NumberOfLines { get; init; } //

		public static int ComputeNumberOfLines(string text) {

feat: Verification diagnostics hover #1946

feat: Verification diagnostics hover #1946

Conversation

MikaelMayer commented Mar 29, 2022 • edited Loading

Formal tests

Implementation

MikaelMayer 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

atomb 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

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 commented May 20, 2022

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

MikaelMayer commented May 23, 2022

atomb 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

keyboardDrummer May 25, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented May 25, 2022 • edited Loading

MikaelMayer commented Mar 29, 2022 •

edited

Loading

keyboardDrummer May 25, 2022 •

edited

Loading

keyboardDrummer commented May 25, 2022 •

edited

Loading