diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs b/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs index 65785bf45b2..83ba9d81124 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs @@ -221,7 +221,8 @@ Position IndexToPosition(int index) { return new Tuple>>(originalCode, changes); } - public async Task VerifyTrace(string codeAndTrace, string fileName = null, + // If testTrace is false, codeAndTree should not contain a trace to test. + public async Task VerifyTrace(string codeAndTrace, string fileName = null, bool testTrace = true, DiagnosticsReceiver diagnosticsReceiver = null, TestNotificationReceiver verificationDiagnosticsReceiver = null ) { @@ -232,7 +233,7 @@ public async Task VerifyTrace(string codeAndTrace, string fileName = null, 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, fileName); client.OpenDocument(documentItem); @@ -242,11 +243,14 @@ public async Task VerifyTrace(string codeAndTrace, string fileName = null, ApplyChange(ref documentItem, range, inserted); traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem, diagnosticsReceiver, verificationDiagnosticsReceiver)); } - 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 diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/ListeningTextDocumentLoader.cs b/Source/DafnyLanguageServer.Test/Diagnostics/ListeningTextDocumentLoader.cs new file mode 100644 index 00000000000..24ca0b983f8 --- /dev/null +++ b/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; + +/// +/// This class extends the TextDocumentLoader but can record internals for testing purposes: +/// It currently records the priorities set before every verification round. +/// +public class ListeningTextDocumentLoader : TextDocumentLoader { + public List> LinearPriorities = new List>(); + + 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(), + document, notificationPublisher, diagnosticPublisher, this); + } + + public void RecordImplementationsPriority(List priorityListPerImplementation) { + LinearPriorities.Add(priorityListPerImplementation); + } +} + +public class ListeningVerificationProgressReporter : VerificationProgressReporter { + public ListeningTextDocumentLoader TextDocumentLoader { get; } + + public ListeningVerificationProgressReporter( + [NotNull] ILogger 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()); + } +} diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/ReorderingVerificationDiagnosticTester.cs b/Source/DafnyLanguageServer.Test/Diagnostics/ReorderingVerificationDiagnosticTester.cs new file mode 100644 index 00000000000..10ed32b568e --- /dev/null +++ b/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; + +/// +/// This class tests whether editing a file results in +/// methods priorities for verification being set automatically. +/// +[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(VerificationDiagnosticReceiver.NotificationReceived)) + , serverOptions => { + serverOptions.Services.AddSingleton(serviceProvider => { + textDocumentLoader = new ListeningTextDocumentLoader( + serviceProvider.GetRequiredService(), serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService>().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>(); + 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()); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index baf7db4ee5f..9e592fd4c7a 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -802,7 +802,8 @@ await SetUp(new Dictionary() { AssertDiagnosticListsAreEqualBesidesMigration(secondVerificationDiagnostics, resolutionDiagnostics2); var firstVerificationDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); var secondVerificationDiagnostics2 = await diagnosticsReceiver.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() { AssertDiagnosticListsAreEqualBesidesMigration(secondVerificationDiagnostics2, resolutionDiagnostics3); var firstVerificationDiagnostics3 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); var secondVerificationDiagnostics3 = await diagnosticsReceiver.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(); diff --git a/Source/DafnyLanguageServer/Workspace/ChangeProcessors/IRelocator.cs b/Source/DafnyLanguageServer/Workspace/ChangeProcessors/IRelocator.cs index 096bfa3d478..a4a3cd28a0c 100644 --- a/Source/DafnyLanguageServer/Workspace/ChangeProcessors/IRelocator.cs +++ b/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 { /// A token to stop the relocation prior completion. /// VerificationTree RelocateVerificationTree(VerificationTree oldVerificationTree, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken); + + /// + /// Relocate previously recorded positions from a document to the next document. + /// + /// The positions to relocate + /// The change in the document + /// A token to stop the relocation prior completion. + /// + ImmutableList RelocatePositions(ImmutableList originalPositions, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Workspace/ChangeProcessors/Relocator.cs b/Source/DafnyLanguageServer/Workspace/ChangeProcessors/Relocator.cs index 0baebdcfe27..09f48bff677 100644 --- a/Source/DafnyLanguageServer/Workspace/ChangeProcessors/Relocator.cs +++ b/Source/DafnyLanguageServer/Workspace/ChangeProcessors/Relocator.cs @@ -44,6 +44,13 @@ public VerificationTree RelocateVerificationTree(VerificationTree originalVerifi }; } + public ImmutableList RelocatePositions(ImmutableList 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 MigrateDiagnostics(IReadOnlyList or return contentChanges.Aggregate(originalDiagnostics, MigrateDiagnostics); } - public List MigratePositions(List originalRanges) { + public ImmutableList MigratePositions(ImmutableList originalRanges) { return contentChanges.Aggregate(originalRanges, MigratePositions); } @@ -88,12 +95,12 @@ private IReadOnlyList MigrateDiagnostics(IReadOnlyList o return originalDiagnostics.SelectMany(diagnostic => MigrateDiagnostic(change, diagnostic)).ToList(); } - private List MigratePositions(List originalRanges, TextDocumentContentChangeEvent change) { + private ImmutableList MigratePositions(ImmutableList originalRanges, TextDocumentContentChangeEvent change) { if (change.Range == null) { - return new List { }; + return new List { }.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 diff --git a/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs b/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs index 562b593ef3c..37a215841ba 100644 --- a/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs +++ b/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 LastTouchedMethodPositions { get; set; } = new List() { }.ToImmutableList(); + + // Used to prioritize verification to one method and its dependencies + public Range? LastChange { get; init; } = null; + /// /// Checks if the given document uri is pointing to this dafny document. /// diff --git a/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs b/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs index 7978d8becde..8396967e783 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs @@ -147,12 +147,21 @@ private async Task ApplyChangesAsync(Task oldDocum logger.LogDebug($"Migrated {oldVerificationDiagnostics.Count} diagnostics into {migratedVerificationDiagnotics.Count} diagnostics."); var migratedVerificationTree = relocator.RelocateVerificationTree(oldDocument.VerificationTree, documentChange, CancellationToken.None); + + var migratedLastTouchedPositions = + relocator.RelocatePositions(oldDocument.LastTouchedMethodPositions, documentChange, CancellationToken.None); try { var newDocument = await documentLoader.LoadAsync(updatedText, cancellationToken); + var lastChange = + documentChange.ContentChanges + .Select(contentChange => contentChange.Range) + .LastOrDefault(newDocument.LastChange); + newDocument = newDocument with { LastChange = lastChange }; if (newDocument.SymbolTable.Resolved) { var resolvedDocument = newDocument with { VerificationDiagnosticsPerImplementation = migratedVerificationDiagnotics, - VerificationTree = migratedVerificationTree + VerificationTree = migratedVerificationTree, + LastTouchedMethodPositions = migratedLastTouchedPositions }; documentLoader.PublishVerificationDiagnostics(resolvedDocument, false); return resolvedDocument; @@ -163,7 +172,8 @@ private async Task ApplyChangesAsync(Task oldDocum var failedDocument = newDocument with { SymbolTable = relocator.RelocateSymbols(oldDocument.SymbolTable, documentChange, CancellationToken.None), VerificationDiagnosticsPerImplementation = migratedVerificationDiagnotics, - VerificationTree = migratedVerificationTree + VerificationTree = migratedVerificationTree, + LastTouchedMethodPositions = migratedLastTouchedPositions }; documentLoader.PublishVerificationDiagnostics(failedDocument, false); return failedDocument; @@ -177,7 +187,8 @@ private async Task ApplyChangesAsync(Task oldDocum CounterExamples = Array.Empty(), VerificationTree = migratedVerificationTree, LoadCanceled = true, - VerificationDiagnosticsPerImplementation = migratedVerificationDiagnotics + VerificationDiagnosticsPerImplementation = migratedVerificationDiagnotics, + LastTouchedMethodPositions = migratedLastTouchedPositions }; } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index 6e34aa2c780..0b9677b56d1 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -37,12 +37,12 @@ public class TextDocumentLoader : ITextDocumentLoader { private readonly ISymbolTableFactory symbolTableFactory; private readonly IProgramVerifier verifier; private readonly IGhostStateDiagnosticCollector ghostStateDiagnosticCollector; - private readonly ICompilationStatusNotificationPublisher notificationPublisher; - private readonly ILoggerFactory loggerFactory; + protected readonly ICompilationStatusNotificationPublisher notificationPublisher; + protected readonly ILoggerFactory loggerFactory; private readonly ILogger logger; - private readonly IDiagnosticPublisher diagnosticPublisher; + protected readonly IDiagnosticPublisher diagnosticPublisher; - private TextDocumentLoader( + protected TextDocumentLoader( ILoggerFactory loggerFactory, IDafnyParser parser, ISymbolResolver symbolResolver, @@ -159,10 +159,7 @@ private static SymbolTable CreateEmptySymbolTable(Dafny.Program program, ILogger public IObservable Verify(DafnyDocument document, CancellationToken cancellationToken) { notificationPublisher.SendStatusNotification(document.TextDocumentItem, CompilationStatus.VerificationStarted); - var progressReporter = new VerificationProgressReporter( - loggerFactory.CreateLogger(), - document, notificationPublisher, diagnosticPublisher); - + var progressReporter = CreateVerificationProgressReporter(document); var programErrorReporter = new DiagnosticErrorReporter(document.Uri); document.Program.Reporter = programErrorReporter; var implementationTasks = verifier.Verify(document, progressReporter); @@ -220,6 +217,12 @@ public IObservable Verify(DafnyDocument document, CancellationTok return result; } + protected virtual VerificationProgressReporter CreateVerificationProgressReporter(DafnyDocument document) { + return new VerificationProgressReporter( + loggerFactory.CreateLogger(), + document, notificationPublisher, diagnosticPublisher); + } + private async Task NotifyStatusAsync(TextDocumentItem item, IReadOnlyList implementationTasks, CancellationToken cancellationToken) { var results = await Task.WhenAll(implementationTasks.Select(t => t.ActualTask)); logger.LogDebug($"Finished verification with {results.Sum(r => r.Errors.Count)} errors."); diff --git a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs index f77cbcba195..efd0a5520f4 100644 --- a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs +++ b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs @@ -1,4 +1,5 @@ using System.Collections.Generic; +using System.Collections.Immutable; using System.Linq; using Microsoft.BaseTypes; using Microsoft.Boogie; @@ -6,6 +7,7 @@ using Microsoft.Dafny.LanguageServer.Util; using Microsoft.Dafny.LanguageServer.Workspace.Notifications; using Microsoft.Extensions.Logging; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; using VC; using VerificationResult = Microsoft.Boogie.VerificationResult; using VerificationStatus = Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationStatus; @@ -13,6 +15,19 @@ namespace Microsoft.Dafny.LanguageServer.Workspace; public class VerificationProgressReporter : IVerificationProgressReporter { + /// The last [MaxLastTouchedMethods] recently modified methods will be + /// automatically assigned a priority ranging from + /// [MaxLastTouchedMethodPriority - MaxLastTouchedMethods + 1] + /// to [MaxLastTouchedMethodPriority] (below, from 6 to 10) + /// Since priorities range from 1 to infinite, the only requirement is + /// that [MaxLastTouchedMethods] is less than [MaxLastTouchedMethodPriority] + /// 10 is a nice priority, not too high so that it can be overriden easily + /// to always trigger the verifier to verify them first (for any reason) + /// and not too low so that it's still possible to manually set up priorities 1-5 to + /// methods that are not being modified. + private const int MaxLastTouchedMethodPriority = 10; + private const int MaxLastTouchedMethods = 5; + private readonly ICompilationStatusNotificationPublisher publisher; private readonly DafnyDocument document; private readonly ILogger logger; @@ -122,10 +137,22 @@ void AddAndPossiblyMigrateVerificationTree(VerificationTree verificationTree) { /// Also set the implementation priority depending on the last edited methods /// /// The implementations to be verified - public void ReportImplementationsBeforeVerification(Implementation[] implementations) { + public virtual void ReportImplementationsBeforeVerification(Implementation[] implementations) { if (document.LoadCanceled || implementations.Length == 0) { return; } + var newLastTouchedMethodPositions = document.LastTouchedMethodPositions.ToList(); + var newlyTouchedVerificationTree = document.VerificationTree.Children.FirstOrDefault(node => + node != null && document.LastChange != null && node.Range.Contains(document.LastChange), null); + if (newlyTouchedVerificationTree != null) { + RememberLastTouchedMethodPositions(newlyTouchedVerificationTree.Position, newLastTouchedMethodPositions); + document.LastTouchedMethodPositions = newLastTouchedMethodPositions.TakeLast(MaxLastTouchedMethods).ToImmutableList(); + } + + var positionToVerificationTree = document.VerificationTree.Children.ToImmutableDictionary( + verificationTree => verificationTree.Position, + verificationTree => verificationTree); + // We migrate existing implementations to the new provided ones if they exist. // (same child number, same file and same position) foreach (var methodTree in document.VerificationTree.Children) { @@ -133,7 +160,8 @@ public void ReportImplementationsBeforeVerification(Implementation[] implementat } foreach (var implementation in implementations) { - int priority = GetVerificationPriority(implementation.tok); + var verificationTree = positionToVerificationTree!.GetValueOrDefault(implementation.tok.GetLspPosition(), null); + int priority = GetVerificationPriority(verificationTree); if (priority > 0 && implementation.Priority < priority) { implementation.Attributes.AddLast( @@ -379,14 +407,37 @@ void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken } /// - /// Returns the verification priority for a given token. + /// Returns the verification priority for a given method, depending on if it was recently modified /// - /// The token to consider + /// The method to consider /// The automatically set priority for the underlying method, or 0 - private int GetVerificationPriority(IToken token) { + private int GetVerificationPriority(VerificationTree? method) { + if (method != null) { + var lastTouchedIndex = document.LastTouchedMethodPositions.IndexOf(method.Position); + // 0 if not found + if (lastTouchedIndex == -1) { + return 0; + } + var lastTouchedCount = document.LastTouchedMethodPositions.Count; + var priority = MaxLastTouchedMethodPriority + lastTouchedIndex + 1 - lastTouchedCount; + return priority; + } return 0; } + /// + /// Helper to remember that a method tree was recently modified. + /// + /// The verification tree of the method that was recently modified + /// The positions of recently touched methods + private void RememberLastTouchedMethodPositions(Position methodPosition, List newLastTouchedMethodPositions) { + var index = newLastTouchedMethodPositions.IndexOf(methodPosition); + if (index != -1) { + newLastTouchedMethodPositions.RemoveAt(index); + } + newLastTouchedMethodPositions.Add(methodPosition); + } + /// /// Given an implementation, returns the top-level verification tree. ///