feat: Verification diagnostics reordering (#1944)

RELEASE_NOTES.md

@@ -1,6 +1,6 @@
 # Upcoming
 
-- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified.
+- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of waiting for all methods to be verified. (https://github.com/dafny-lang/dafny/pull/1944)
 - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942)
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
 

Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs

@@ -117,8 +117,7 @@ var previousPerLineDiagnostics
  var nextDiagnostic = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken);
  for (; maximumNumberOfTraces > 0; maximumNumberOfTraces--) {
  var verificationDiagnosticReport = await VerificationDiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken);
- Assert.AreEqual(documentItem.Uri, verificationDiagnosticReport.Uri);
- if (documentItem.Version != verificationDiagnosticReport.Version) {
+ if (documentItem.Uri != verificationDiagnosticReport.Uri || documentItem.Version != verificationDiagnosticReport.Version) {
  continue;
  }
  var newPerLineDiagnostics = verificationDiagnosticReport.PerLineStatus.ToList();
@@ -218,11 +217,12 @@ Position IndexToPosition(int index) {
  return new Tuple<string, List<Tuple<Range, string>>>(originalCode, changes);
  }
 
- public async Task VerifyTrace(string codeAndTrace) {
+ // If testTrace is false, codeAndTree should not contain a trace to test.
+ public async Task VerifyTrace(string codeAndTrace, bool testTrace = true) {
  codeAndTrace = codeAndTrace[0] == '\n' ? codeAndTrace.Substring(1) :
  codeAndTrace.Substring(0, 2) == "\r\n" ? codeAndTrace.Substring(2) :
  codeAndTrace;
- var codeAndChanges = ExtractCode(codeAndTrace);
+ var codeAndChanges = testTrace ? ExtractCode(codeAndTrace) : codeAndTrace;
  var (code, changes) = ExtractCodeAndChanges(codeAndChanges);
  var documentItem = CreateTestDocument(code);
  await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
@@ -232,11 +232,14 @@ public async Task VerifyTrace(string codeAndTrace) {
  ApplyChange(ref documentItem, range, inserted);
  traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem));
  }
- var traceObtained = RenderTrace(traces, code);
- var ignoreQuestionMarks = AcceptQuestionMarks(traceObtained, codeAndTrace);
- var expected = "\n" + codeAndTrace + "\n";
- var actual = "\n" + ignoreQuestionMarks + "\n";
- AssertWithDiff.Equal(expected, actual);
+
+ if (testTrace) {
+ var traceObtained = RenderTrace(traces, code);
+ var ignoreQuestionMarks = AcceptQuestionMarks(traceObtained, codeAndTrace);
+ var expected = "\n" + codeAndTrace + "\n";
+ var actual = "\n" + ignoreQuestionMarks + "\n";
+ AssertWithDiff.Equal(expected, actual);
+ }
  }
 
  // Finds all the "?" at the beginning in expected and replace the characters at the same position in traceObtained

Source/DafnyLanguageServer.Test/Diagnostics/ListeningTextDocumentLoader.cs

@@ -0,0 +1,63 @@
+#nullable enable
+using System.Collections.Generic;
+using System.Linq;
+using JetBrains.Annotations;
+using Microsoft.Boogie;
+using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.Logging;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
+
+/// <summary>
+/// This class extends the TextDocumentLoader but can record internals for testing purposes:
+/// It currently records the priorities set before every verification round.
+/// </summary>
+public class ListeningTextDocumentLoader : TextDocumentLoader {
+ public List<List<int>> LinearPriorities = new List<List<int>>();
+
+ public ListeningTextDocumentLoader(
+ ILoggerFactory loggerFactory, IDafnyParser parser,
+ ISymbolResolver symbolResolver, IProgramVerifier verifier,
+ ISymbolTableFactory symbolTableFactory,
+ IGhostStateDiagnosticCollector ghostStateDiagnosticCollector,
+ ICompilationStatusNotificationPublisher notificationPublisher,
+ IDiagnosticPublisher diagnosticPublisher,
+ VerifierOptions verifierOptions) : base(loggerFactory, parser, symbolResolver, verifier,
+ symbolTableFactory, ghostStateDiagnosticCollector, notificationPublisher, diagnosticPublisher,
+ verifierOptions) {
+ }
+
+
+ protected override VerificationProgressReporter CreateVerificationProgressReporter(DafnyDocument document) {
+ return new ListeningVerificationProgressReporter(
+ loggerFactory.CreateLogger<ListeningVerificationProgressReporter>(),
+ document, notificationPublisher, diagnosticPublisher, this);
+ }
+
+ public void RecordImplementationsPriority(List<int> priorityListPerImplementation) {
+ LinearPriorities.Add(priorityListPerImplementation);
+ }
+}
+
+public class ListeningVerificationProgressReporter : VerificationProgressReporter {
+ public ListeningTextDocumentLoader TextDocumentLoader { get; }
+
+ public ListeningVerificationProgressReporter(
+ [NotNull] ILogger<VerificationProgressReporter> logger,
+ [NotNull] DafnyDocument document,
+ [NotNull] ICompilationStatusNotificationPublisher publisher,
+ [NotNull] IDiagnosticPublisher diagnosticPublisher,
+ ListeningTextDocumentLoader textDocumentLoader
+ )
+ : base(logger, document, publisher, diagnosticPublisher) {
+ TextDocumentLoader = textDocumentLoader;
+ }
+
+ public override void ReportImplementationsBeforeVerification(Implementation[] implementations) {
+ base.ReportImplementationsBeforeVerification(implementations);
+ TextDocumentLoader.RecordImplementationsPriority(implementations.Select(implementation => implementation.Priority)
+ .ToList());
+ }
+}

Source/DafnyLanguageServer.Test/Diagnostics/ReorderingVerificationDiagnosticTester.cs

@@ -0,0 +1,155 @@
+using System.Collections.Generic;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
+using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.Extensions.Logging;
+using Microsoft.Extensions.Options;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using Microsoft.Extensions.DependencyInjection;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
+
+/// <summary>
+/// This class tests whether editing a file results in
+/// methods priorities for verification being set automatically.
+/// </summary>
+[TestClass]
+public class ReorderingVerificationDiagnosticTester : LinearVerificationDiagnosticTester {
+ private ListeningTextDocumentLoader textDocumentLoader;
+ private const int MaxTestExecutionTimeMs = 10000;
+
+ [TestInitialize]
+ public override async Task SetUp() {
+ DafnyOptions.Install(DafnyOptions.Create("-proverOpt:SOLVER=noop"));
+ diagnosticReceiver = new();
+ VerificationDiagnosticReceiver = new();
+ client = await InitializeClient(options =>
+ options
+ .OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)
+ .AddHandler(DafnyRequestNames.VerificationStatusGutter,
+ NotificationHandler.For<VerificationStatusGutter>(VerificationDiagnosticReceiver.NotificationReceived))
+ , serverOptions => {
+ serverOptions.Services.AddSingleton<ITextDocumentLoader>(serviceProvider => {
+ textDocumentLoader = new ListeningTextDocumentLoader(
+ serviceProvider.GetRequiredService<ILoggerFactory>(), serviceProvider.GetRequiredService<IDafnyParser>(),
+ serviceProvider.GetRequiredService<ISymbolResolver>(),
+ serviceProvider.GetRequiredService<IProgramVerifier>(),
+ serviceProvider.GetRequiredService<ISymbolTableFactory>(),
+ serviceProvider.GetRequiredService<IGhostStateDiagnosticCollector>(),
+ serviceProvider.GetRequiredService<ICompilationStatusNotificationPublisher>(),
+ serviceProvider.GetRequiredService<IDiagnosticPublisher>(),
+ serviceProvider.GetRequiredService<IOptions<VerifierOptions>>().Value
+ );
+ return textDocumentLoader;
+ });
+ });
+ }
+
+ [TestMethod/*, Timeout(MaxTestExecutionTimeMs * 10)*/]
+ public async Task EnsuresPriorityDependsOnEditing() {
+ await TestPriorities(@"
+method m1() {
+ assert 1 == 0;//Next2: assert 2 == 0;
+}
+
+method m2() {
+ assert 1 == 0;//Next1: assert 2 == 0;
+}",
+ expectedPriorities:
+ " 1, 1 " +
+ " 1,10 " +
+ "10, 9");
+ }
+
+ [TestMethod]
+ public async Task EnsuresPriorityDependsOnEditingWhileEditingSameMethod() {
+ await TestPriorities(@"
+method m1() {
+ assert true;//Next7: assert true;//Next8: assert true;
+}
+method m2() {
+ assert true;//Next5: assert true;
+}
+method m3() {
+ assert true;//Next2: assert true;//Next9: assert true;
+}
+method m4() {
+ assert true;//Next3: assert true;//Next4: assert true;
+}
+method m5() {
+ assert true;//Next1: assert true;//Next6: assert true;//Next10: assert true;
+}", expectedPriorities:
+ " 1, 1, 1, 1, 1 " +
+ " 1, 1, 1, 1,10 " +
+ " 1, 1,10, 1, 9 " +
+ " 1, 1, 9,10, 8 " +
+ " 1, 1, 9,10, 8 " +
+ " 1,10, 8, 9, 7 " +
+ " 1, 9, 7, 8,10 " +
+ "10, 8, 6, 7, 9 " +
+ "10, 8, 6, 7, 9 " +
+ " 9, 7,10, 6, 8 " +
+ " 8, 7, 9, 6,10");
+ }
+
+ [TestMethod]
+ public async Task EnsuresPriorityWorksEvenIfRemovingMethods() {
+ await TestPriorities(@"
+method m1() { assert true; }
+method m2() { assert true; }
+method m3() { assert true; } //Remove3:
+method m4() {
+ assert true;//Next1: assert true;
+} 
+method m5() {
+ assert true;//Next2: assert true;
+}
+", expectedPriorities:
+ " 1, 1, 1, 1, 1 " +
+ " 1, 1, 1,10, 1 " +
+ " 1, 1, 1, 9,10 " +
+ " 1, 1, 9,10");
+ }
+
+
+ [TestMethod]
+ public async Task EnsuresPriorityWorksEvenIfRemovingMethodsWhileTypo() {
+ await TestPriorities(@"
+method m1() { assert true; }
+method m2() {
+ assert true;//Next3: typo//Next5: assert true;
+}
+method m3() { assert true; } //Remove4:
+method m4() {
+ assert true;//Next1: assert true;
+} 
+method m5() {
+ assert true;//Next2: assert true;
+}
+", expectedPriorities:
+ " 1, 1, 1, 1, 1 " +
+ " 1, 1, 1,10, 1 " +
+ " 1, 1, 1, 9,10 " +// No priorities set for the two edits when there is a parse error.
+ " 1,10, 8, 9");
+ }
+
+ private async Task TestPriorities(string code, string expectedPriorities) {
+ textDocumentLoader.LinearPriorities = new List<List<int>>();
+ await VerifyTrace(code, testTrace: false);
+ var priorities = string.Join(" ", textDocumentLoader.LinearPriorities.Select(priorities =>
+ string.Join(",", priorities.Select(priority => priority.ToString().PadLeft(2)))));
+ Assert.AreEqual(expectedPriorities, priorities);
+ }
+
+ [TestCleanup]
+ public void Cleanup() {
+ DafnyOptions.Install(DafnyOptions.Create());
+ }
+}

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -802,7 +802,8 @@ await SetUp(new Dictionary<string, string>() {
  AssertDiagnosticListsAreEqualBesidesMigration(secondVerificationDiagnostics, resolutionDiagnostics2);
  var firstVerificationDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
  var secondVerificationDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
- Assert.AreEqual(1, firstVerificationDiagnostics2.Length); // Still contains second failing method
+ //Reordering means the assert false could be solved first
+ //Assert.AreEqual(1, firstVerificationDiagnostics2.Length); // Still contains second failing method
  Assert.AreEqual(1, secondVerificationDiagnostics2.Length);
 
  ApplyChange(ref documentItem, new Range((4, 9), (4, 14)), "true");
@@ -811,7 +812,8 @@ await SetUp(new Dictionary<string, string>() {
  AssertDiagnosticListsAreEqualBesidesMigration(secondVerificationDiagnostics2, resolutionDiagnostics3);
  var firstVerificationDiagnostics3 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
  var secondVerificationDiagnostics3 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
- Assert.AreEqual(1, firstVerificationDiagnostics3.Length); // Still contains second failing method
+ //Reordering means the error could be solved first
+ //Assert.AreEqual(1, firstVerificationDiagnostics3.Length); // Still contains second failing method
  Assert.AreEqual(0, secondVerificationDiagnostics3.Length);
 
  await AssertNoDiagnosticsAreComing();

Source/DafnyLanguageServer/Workspace/ChangeProcessors/IRelocator.cs

@@ -1,4 +1,5 @@
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Threading;
@@ -43,5 +44,14 @@ public interface IRelocator {
  /// <param name="cancellationToken">A token to stop the relocation prior completion.</param>
  /// <returns></returns>
  VerificationTree RelocateVerificationTree(VerificationTree oldVerificationTree, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken);
+
+ /// <summary>
+ /// Relocate previously recorded positions from a document to the next document.
+ /// </summary>
+ /// <param name="originalPositions">The positions to relocate</param>
+ /// <param name="documentChange">The change in the document</param>
+ /// <param name="cancellationToken">A token to stop the relocation prior completion.</param>
+ /// <returns></returns>
+ ImmutableList<Position> RelocatePositions(ImmutableList<Position> originalPositions, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken);
  }
 }

Source/DafnyLanguageServer/Workspace/ChangeProcessors/Relocator.cs

@@ -44,6 +44,13 @@ public VerificationTree RelocateVerificationTree(VerificationTree originalVerifi
  };
  }
 
+ public ImmutableList<Position> RelocatePositions(ImmutableList<Position> originalPositions,
+ DidChangeTextDocumentParams changes, CancellationToken cancellationToken) {
+ var migratePositions = new ChangeProcessor(logger, loggerSymbolTable, changes.ContentChanges, cancellationToken)
+ .MigratePositions(originalPositions);
+ return migratePositions;
+ }
+
  private class ChangeProcessor {
  private readonly ILogger logger;
  // Invariant: Item1.Range == null <==> Item2 == null 
@@ -77,7 +84,7 @@ public IReadOnlyList<Diagnostic> MigrateDiagnostics(IReadOnlyList<Diagnostic> or
  return contentChanges.Aggregate(originalDiagnostics, MigrateDiagnostics);
  }
 
- public List<Position> MigratePositions(List<Position> originalRanges) {
+ public ImmutableList<Position> MigratePositions(ImmutableList<Position> originalRanges) {
  return contentChanges.Aggregate(originalRanges, MigratePositions);
  }
 
@@ -88,12 +95,12 @@ private IReadOnlyList<Diagnostic> MigrateDiagnostics(IReadOnlyList<Diagnostic> o
 
  return originalDiagnostics.SelectMany(diagnostic => MigrateDiagnostic(change, diagnostic)).ToList();
  }
- private List<Position> MigratePositions(List<Position> originalRanges, TextDocumentContentChangeEvent change) {
+ private ImmutableList<Position> MigratePositions(ImmutableList<Position> originalRanges, TextDocumentContentChangeEvent change) {
  if (change.Range == null) {
- return new List<Position> { };
+ return new List<Position> { }.ToImmutableList();
  }
 
- return originalRanges.SelectMany(position => MigratePosition(change, position)).ToList();
+ return originalRanges.SelectMany(position => MigratePosition(change, position)).ToImmutableList();
  }
 
  // Requires changeEndOffset.change.Range to be not null

Source/DafnyLanguageServer/Workspace/DafnyDocument.cs

@@ -1,6 +1,7 @@
 using OmniSharp.Extensions.LanguageServer.Protocol;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using System.Linq;
 using Microsoft.Boogie;
 using SymbolTable = Microsoft.Dafny.LanguageServer.Language.Symbols.SymbolTable;
@@ -47,6 +48,12 @@ public record DafnyDocument(
  TextDocumentItem.Text.Count(c => c == '\n') + 1
  );
 
+ // List of a few last touched method positions
+ public ImmutableList<Position> LastTouchedMethodPositions { get; set; } = new List<Position>() { }.ToImmutableList();
+
+ // Used to prioritize verification to one method and its dependencies
+ public Range? LastChange { get; init; } = null;
+
  /// <summary>
  /// Checks if the given document uri is pointing to this dafny document.
  /// </summary>