From 622592ded76b4360fdc298afa8c43c99bed58894 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 21 Sep 2023 17:50:36 +0200 Subject: [PATCH] Prevent modification exception when accessing parsed document (#4571) Due to a large rename commit, it might be best to review this PR by reviewing the individual commits. ### Changes - Prevent the document symbol API from crashing, especially when prefix name modules are used. The server back-end API provides both a Dafny program after parsing and after resolution. Without this PR, the same program object is used, and the program you get after parsing will still be modified by resolution while you access it. This PR clones the program before it is used for resolution, so whether you get a program post parsing or post resolution, it won't be modified any more. ### Testing - Update tests for document symbol API so they no longer with for the program to resolve, which prevented this bug from being detected. One of these tests now reliably fails without this fix. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/AST/Program.cs | 13 ++++++ .../CodeActions/CodeActionsTest.cs | 2 +- .../LinearVerificationGutterStatusTester.cs | 2 +- .../Lookup/DocumentSymbolTest.cs | 23 ++++------ .../Lookup/GoToDefinitionTest.cs | 8 ++-- .../Lookup/HoverTest.cs | 4 +- .../Performance/LargeFilesTest.cs | 2 +- .../ProjectFiles/CompetingProjectFilesTest.cs | 2 +- .../ProjectFiles/MultipleFilesProjectTest.cs | 42 +++++++++---------- .../ProjectFiles/ProjectFilesTest.cs | 16 +++---- .../Refactoring/RenameTest.cs | 8 ++-- .../Synchronization/CachingTest.cs | 12 +++--- .../Synchronization/DiagnosticsTest.cs | 14 +++---- .../Synchronization/GhostDiagnosticsTest.cs | 6 +-- .../Synchronization/IncludeFileTest.cs | 4 +- .../ProjectManagerDatabaseTest.cs | 8 ++-- .../Synchronization/VerificationOrderTest.cs | 8 ++-- .../Synchronization/VerificationStatusTest.cs | 16 +++---- .../Util/ClientBasedLanguageServerTest.cs | 9 +++- .../CompilationStatusNotificationTest.cs | 14 +++---- .../Various/DiagnosticMigrationTest.cs | 2 +- .../Various/ExceptionTests.cs | 4 +- .../Workspace/CompilationManager.cs | 2 +- .../Workspace/ITextDocumentLoader.cs | 1 - .../Workspace/TextDocumentLoader.cs | 20 +++++---- 25 files changed, 129 insertions(+), 113 deletions(-) diff --git a/Source/DafnyCore/AST/Program.cs b/Source/DafnyCore/AST/Program.cs index 95431839058..0c0734cde01 100644 --- a/Source/DafnyCore/AST/Program.cs +++ b/Source/DafnyCore/AST/Program.cs @@ -45,6 +45,19 @@ public Program(string name, [Captured] LiteralModuleDecl module, [Captured] Syst Compilation = compilation; } + public Program(Cloner cloner, Program original) { + FullName = original.FullName; + DefaultModule = new LiteralModuleDecl(cloner, original.DefaultModule, original.DefaultModule.EnclosingModuleDefinition); + Files = original.Files; + SystemModuleManager = original.SystemModuleManager; + Reporter = original.Reporter; + Compilation = original.Compilation; + + if (cloner.CloneResolvedFields) { + throw new NotImplementedException(); + } + } + //Set appropriate visibilty before presenting module public IEnumerable Modules() { diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index 756b2ae9818..a9d389df860 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -310,7 +310,7 @@ private async Task TestCodeAction(string source) { MarkupTestFile.GetPositionsAndAnnotatedRanges(source.TrimStart(), out var output, out var positions, out var ranges); - var documentItem = await CreateAndOpenTestDocument(output); + var documentItem = await CreateOpenAndWaitForResolve(output); var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); Assert.Equal(ranges.Count, diagnostics.Length); diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs index 8e188130f53..19c6e492a39 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs @@ -275,7 +275,7 @@ public async Task VerifyTrace(string codeAndTrace, bool explicitProject, string var documentItem = CreateTestDocument(code.Trim(), fileName, 1); if (explicitProject) { - await CreateAndOpenTestDocument("", Path.Combine(Path.GetDirectoryName(documentItem.Uri.GetFileSystemPath())!, DafnyProject.FileName)); + await CreateOpenAndWaitForResolve("", Path.Combine(Path.GetDirectoryName(documentItem.Uri.GetFileSystemPath())!, DafnyProject.FileName)); } client.OpenDocument(documentItem); var traces = new List(); diff --git a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs index e9054fd9fb1..5cec4f78d10 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs @@ -14,9 +14,9 @@ public class DocumentSymbolTest : ClientBasedLanguageServerTest { [Fact] public async Task CanResolveSymbolsForMultiFileProjects() { var temp = Path.GetTempPath(); - await CreateAndOpenTestDocument("", Path.Combine(temp, DafnyProject.FileName)); - var file1 = await CreateAndOpenTestDocument("method Foo() {}", Path.Combine(temp, "file1.dfy")); - var file2 = await CreateAndOpenTestDocument("method Bar() {}", Path.Combine(temp, "file2.dfy")); + await CreateOpenAndWaitForResolve("", Path.Combine(temp, DafnyProject.FileName)); + var file1 = CreateAndOpenTestDocument("method Foo() {}", Path.Combine(temp, "file1.dfy")); + var file2 = CreateAndOpenTestDocument("method Bar() {}", Path.Combine(temp, "file2.dfy")); var fooSymbol = (await RequestDocumentSymbol(file1)).Single(); Assert.Equal("Foo", fooSymbol.Name); @@ -34,7 +34,7 @@ method DoIt() returns (x: int) { } }".TrimStart(); var documentItem = CreateTestDocument(source); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + client.OpenDocument(documentItem); var symbols = (await RequestDocumentSymbol(documentItem)).ToList(); Assert.Single(symbols); @@ -50,8 +50,7 @@ public async Task DoubleComma() { var source = @" method Foo(a: int,, b: int) returns (x: int) { }".TrimStart(); - var documentItem = CreateTestDocument(source); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var documentItem = CreateAndOpenTestDocument(source); var allSymbols = await RequestDocumentSymbol(documentItem); Assert.Single(allSymbols); } @@ -65,8 +64,7 @@ method DoIt() returns (x: int) { method CallIt() returns () { var x := DoIt(); }".TrimStart(); - var documentItem = CreateTestDocument(source); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var documentItem = CreateAndOpenTestDocument(source); var allSymbols = await RequestDocumentSymbol(documentItem); Assert.Equal(2, allSymbols.Count()); } @@ -85,8 +83,7 @@ method CallIt() returns () { var x := DoIt(); } }".TrimStart(); - var documentItem = CreateTestDocument(source, "LoadCorrectDocumentCreatesSymbols.dfy"); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var documentItem = CreateAndOpenTestDocument(source, "LoadCorrectDocumentCreatesSymbols.dfy"); var classSymbol = (await RequestDocumentSymbol(documentItem)).Single(); var classChildren = classSymbol.Children.ToArray(); @@ -134,8 +131,7 @@ method CallIt() returns () { [Fact] public async Task CanResolveSymbolsForMethodsWithoutBody() { var source = "method DoIt()"; - var documentItem = CreateTestDocument(source, "CanResolveSymbolsForMethodsWithoutBody.dfy"); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var documentItem = CreateAndOpenTestDocument(source, "CanResolveSymbolsForMethodsWithoutBody.dfy"); var methodSymbol = (await RequestDocumentSymbol(documentItem)).Single(); Assert.Equal("DoIt", methodSymbol.Name); @@ -147,8 +143,7 @@ public async Task CanResolveSymbolsForMethodsWithoutBody() { [Fact] public async Task CanResolveSymbolsForFunctionWithoutBody() { var source = "function ConstOne(): int"; - var documentItem = CreateTestDocument(source, "CanResolveSymbolsForFunctionWithoutBody.dfy"); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var documentItem = CreateAndOpenTestDocument(source, "CanResolveSymbolsForFunctionWithoutBody.dfy"); var methodSymbol = (await RequestDocumentSymbol(documentItem)).Single(); Assert.Equal("ConstOne", methodSymbol.Name); diff --git a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs b/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs index e4b9e265669..21a8c14b11a 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs @@ -52,9 +52,9 @@ public async Task ExplicitProjectToGoDefinitionWorks() { ".TrimStart(); var directory = Path.GetRandomFileName(); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var aFile = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "A.dfy")); - var bFile = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "B.dfy")); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var aFile = await CreateOpenAndWaitForResolve(sourceA, Path.Combine(directory, "A.dfy")); + var bFile = await CreateOpenAndWaitForResolve(sourceB, Path.Combine(directory, "B.dfy")); var result1 = await RequestDefinition(bFile, new Position(0, 11)); Assert.Equal(new Range(0, 6, 0, 7), result1.Single().Location!.Range); @@ -113,7 +113,7 @@ private async Task AssertPositionsLineUpWithRanges(string source) { MarkupTestFile.GetPositionsAndNamedRanges(source, out var cleanSource, out var positions, out var ranges); - var documentItem = await CreateAndOpenTestDocument(cleanSource); + var documentItem = await CreateOpenAndWaitForResolve(cleanSource); for (var index = 0; index < positions.Count; index++) { var position = positions[index]; var range = ranges.ContainsKey(string.Empty) ? ranges[string.Empty][index] : ranges[index.ToString()].Single(); diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index 59c524beac4..4628e13c29c 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -70,7 +70,7 @@ await SetUp(o => { var hovers = hoverRegex.Matches(sourceWithHovers); var documentItem = CreateTestDocument(source, "AssertHover.dfy"); if (useProjectFile) { - await CreateAndOpenTestDocument("", Path.Combine(Path.GetDirectoryName(documentItem.Uri.GetFileSystemPath())!, DafnyProject.FileName)); + await CreateOpenAndWaitForResolve("", Path.Combine(Path.GetDirectoryName(documentItem.Uri.GetFileSystemPath())!, DafnyProject.FileName)); } client.OpenDocument(documentItem); var lineDelta = 0; @@ -106,7 +106,7 @@ method Foo() { [Fact] public async Task RecoverableParseError() { - var document = await CreateAndOpenTestDocument(@" + var document = await CreateOpenAndWaitForResolve(@" class Foo { const x := '\U2345' // ^[```dafny\nconst x: ?\n```] diff --git a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs index b08d62314b7..20c59405ca3 100644 --- a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs @@ -47,7 +47,7 @@ public async Task QuickEditsInLargeFile() { var cancelSource = new CancellationTokenSource(); var measurementTask = AssertThreadPoolIsAvailable(cancelSource.Token); var beforeOpen = DateTime.Now; - var documentItem = await CreateAndOpenTestDocument(source, "ManyFastEditsUsingLargeFiles.dfy", + var documentItem = await CreateOpenAndWaitForResolve(source, "ManyFastEditsUsingLargeFiles.dfy", cancellationToken: CancellationTokenWithHighTimeout); var afterOpen = DateTime.Now; var openMilliseconds = (afterOpen - beforeOpen).TotalMilliseconds; diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs index e3afaf116e9..d2ad1e5d5b2 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs @@ -28,7 +28,7 @@ public async Task ProjectFileDoesNotOwnAllSourceFilesItUses() { await File.WriteAllTextAsync(Path.Combine(nestedDirectory, "source.dfy"), "hasErrorInSyntax"); await File.WriteAllTextAsync(Path.Combine(nestedDirectory, DafnyProject.FileName), ""); - await CreateAndOpenTestDocument("", Path.Combine(tempDirectory, DafnyProject.FileName)); + await CreateOpenAndWaitForResolve("", Path.Combine(tempDirectory, DafnyProject.FileName)); var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); var errors = diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs index 3039efcb4de..360cdeac782 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs @@ -33,7 +33,7 @@ method Bar() { Directory.CreateDirectory(directory); await File.WriteAllTextAsync(Path.Combine(directory, "producer.dfy"), producerSource); await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), ""); - await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "src/consumer1.dfy")); + await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "src/consumer1.dfy")); var diagnostics1 = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken); var diagnostics2 = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken); @@ -65,7 +65,7 @@ method Bar() { Directory.CreateDirectory(directory); await File.WriteAllTextAsync(Path.Combine(directory, "OnDiskProducerVerificationErrors_producer.dfy"), producerSource); await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), ""); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "OnDiskProducerVerificationErrors_consumer1.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "OnDiskProducerVerificationErrors_consumer1.dfy")); var diagnostics1 = await GetLastDiagnostics(consumer); Assert.Single(diagnostics1); @@ -97,7 +97,7 @@ method Bar() { var producerUri = DocumentUri.File(producerPath); await File.WriteAllTextAsync(producerPath, producerSource); await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), ""); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "OnDiskProducerVerificationErrors_consumer1.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "OnDiskProducerVerificationErrors_consumer1.dfy")); var diagnostics = await GetAllDiagnostics(CancellationToken); try { @@ -125,8 +125,8 @@ method Produces() {} var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); Directory.CreateDirectory(directory); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "firstFile.dfy")); - await CreateAndOpenTestDocument(producer, Path.Combine(directory, "secondFile.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "firstFile.dfy")); + await CreateOpenAndWaitForResolve(producer, Path.Combine(directory, "secondFile.dfy")); var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3)); Assert.Empty(producesDefinition1); @@ -151,13 +151,13 @@ method Produces() {} ".TrimStart(); var directory = Path.GetRandomFileName(); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "firstFile.dfy")); - var secondFile = await CreateAndOpenTestDocument(producer, Path.Combine(directory, "secondFile.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "firstFile.dfy")); + var secondFile = await CreateOpenAndWaitForResolve(producer, Path.Combine(directory, "secondFile.dfy")); var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3)); Assert.Empty(producesDefinition1); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime); @@ -172,8 +172,8 @@ await SetUp(options => { }); var directory = Path.GetRandomFileName(); - var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var codeFile = await CreateAndOpenTestDocument("method Foo() {}", Path.Combine(directory, "firstFile.dfy")); + var projectFile = await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var codeFile = await CreateOpenAndWaitForResolve("method Foo() {}", Path.Combine(directory, "firstFile.dfy")); Assert.NotEmpty(Projects.Managers); @@ -210,8 +210,8 @@ method Produces() {} var projectFilePath = Path.Combine(directory, DafnyProject.FileName); await File.WriteAllTextAsync(projectFilePath, projectFileSource); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "firstFile.dfy")); - var secondFile = await CreateAndOpenTestDocument(producer, Path.Combine(directory, "secondFile.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "firstFile.dfy")); + var secondFile = await CreateOpenAndWaitForResolve(producer, Path.Combine(directory, "secondFile.dfy")); var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3)); Assert.Empty(producesDefinition1); @@ -246,8 +246,8 @@ method Foo() { warn-shadowing = true ".Trim(); // includes must come before [options], even if there is a blank line var directory = Path.GetRandomFileName(); - var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName)); - var sourceFile = await CreateAndOpenTestDocument(source, Path.Combine(directory, "src/file.dfy")); + var projectFile = await CreateOpenAndWaitForResolve(projectFileSource, Path.Combine(directory, DafnyProject.FileName)); + var sourceFile = await CreateOpenAndWaitForResolve(source, Path.Combine(directory, "src/file.dfy")); var diagnostics1 = await GetLastDiagnostics(sourceFile, CancellationToken); Assert.Equal(2, diagnostics1.Count(d => d.Severity <= DiagnosticSeverity.Warning)); @@ -278,9 +278,9 @@ method Bar() { includes = [""src/**/*.dfy""] "; var directory = Path.GetRandomFileName(); - var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName)); - var producerItem = await CreateAndOpenTestDocument(producerSource, Path.Combine(directory, "src/producer.dfy")); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "src/consumer1.dfy")); + var projectFile = await CreateOpenAndWaitForResolve(projectFileSource, Path.Combine(directory, DafnyProject.FileName)); + var producerItem = await CreateOpenAndWaitForResolve(producerSource, Path.Combine(directory, "src/producer.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "src/consumer1.dfy")); var consumerDiagnostics1 = await GetLastDiagnostics(consumer); Assert.Single(consumerDiagnostics1); @@ -305,8 +305,8 @@ method Bar() { var x: int := true; } "; - var producerItem = await CreateAndOpenTestDocument(producerSource, Path.Combine(Directory.GetCurrentDirectory(), "A.dfy")); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(Directory.GetCurrentDirectory(), "consumer1.dfy")); + var producerItem = await CreateOpenAndWaitForResolve(producerSource, Path.Combine(Directory.GetCurrentDirectory(), "A.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(Directory.GetCurrentDirectory(), "consumer1.dfy")); var consumer1Diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, consumer); Assert.Single(consumer1Diagnostics); @@ -316,14 +316,14 @@ method Bar() { var producerDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, producerItem); Assert.Single(producerDiagnostics2); // File has no code - var consumer2 = await CreateAndOpenTestDocument(consumerSource, Path.Combine(Directory.GetCurrentDirectory(), "consumer2.dfy")); + var consumer2 = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(Directory.GetCurrentDirectory(), "consumer2.dfy")); var consumer2Diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, consumer2); Assert.True(consumer2Diagnostics.Length > 1); client.CloseDocument(producerItem); var producerDiagnostics3 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.Empty(producerDiagnostics3); // File has no code - var consumer3 = await CreateAndOpenTestDocument(consumerSource, Path.Combine(Directory.GetCurrentDirectory(), "consumer3.dfy")); + var consumer3 = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(Directory.GetCurrentDirectory(), "consumer3.dfy")); var consumer3Diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, consumer3); Assert.Single(consumer3Diagnostics); Assert.Contains("Unable to open", consumer3Diagnostics[0].Message); diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 2d74bd23276..9ceb3a262c5 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -18,7 +18,7 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest { [Fact] public async Task ProjectFileErrorIsShown() { var projectFileSource = @"includes = [stringWithoutQuotes]"; - await CreateAndOpenTestDocument(projectFileSource, DafnyProject.FileName); + await CreateOpenAndWaitForResolve(projectFileSource, DafnyProject.FileName); var diagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.Equal(2, diagnostics.Diagnostics.Count()); Assert.Equal(new Range(0, 0, 0, 0), diagnostics.Diagnostics.First().Range); @@ -32,7 +32,7 @@ public async Task ProjectFileErrorIsShownFromDafnyFile() { Directory.CreateDirectory(directory); var projectFilePath = Path.Combine(directory, DafnyProject.FileName); await File.WriteAllTextAsync(projectFilePath, projectFileSource); - await CreateAndOpenTestDocument("method Foo() { }", Path.Combine(directory, "ProjectFileErrorIsShownFromDafnyFile.dfy")); + await CreateOpenAndWaitForResolve("method Foo() { }", Path.Combine(directory, "ProjectFileErrorIsShownFromDafnyFile.dfy")); var diagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.Equal(DocumentUri.File(projectFilePath), diagnostics.Uri.GetFileSystemPath()); Assert.Equal(2, diagnostics.Diagnostics.Count()); @@ -53,7 +53,7 @@ module [>Producer<]Oops { const x := 3 }".TrimStart(); MarkupTestFile.GetPositionsAndRanges(producerMarkup, out var producerSource, out _, out var ranges); - var producer = await CreateAndOpenTestDocument(producerSource, Path.Combine(tempDirectory, "producer.dfy")); + var producer = await CreateOpenAndWaitForResolve(producerSource, Path.Combine(tempDirectory, "producer.dfy")); var consumerSourceMarkup = @" include ""producer.dfy"" module Consumer { @@ -61,8 +61,8 @@ import opened Pro> { var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); Directory.CreateDirectory(directory); - var noProjectFile = await CreateAndOpenTestDocument(source, "orphaned.dfy"); + var noProjectFile = await CreateOpenAndWaitForResolve(source, "orphaned.dfy"); var diagnostics1 = await GetLastDiagnostics(noProjectFile, CancellationToken); Assert.Single(diagnostics1); // Stops after parsing await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource); - var sourceFile = await CreateAndOpenTestDocument(source, Path.Combine(directory, "source.dfy")); + var sourceFile = await CreateOpenAndWaitForResolve(source, Path.Combine(directory, "source.dfy")); var diagnostics2 = await GetLastDiagnostics(sourceFile, CancellationToken); Assert.Empty(diagnostics2.Where(d => d.Severity == DiagnosticSeverity.Error)); } diff --git a/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs b/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs index 5b8f58a1e5e..ab598a655a9 100644 --- a/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs +++ b/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs @@ -20,13 +20,13 @@ public async Task ImplicitProjectFails() { const i := 0 ".TrimStart(); - var documentItem = await CreateAndOpenTestDocument(source); + var documentItem = await CreateOpenAndWaitForResolve(source); await Assert.ThrowsAnyAsync(() => RequestRename(documentItem, new Position(0, 6), "j")); } [Fact] public async Task InvalidNewNameIsNoOp() { - var documentItem = await CreateAndOpenTestDocument(""); + var documentItem = await CreateOpenAndWaitForResolve(""); var workspaceEdit = await RequestRename(documentItem, new Position(0, 0), ""); Assert.Null(workspaceEdit); } @@ -34,7 +34,7 @@ public async Task InvalidNewNameIsNoOp() { [Fact] public async Task RenameNonSymbolFails() { var tempDir = await SetUpProjectFile(); - var documentItem = await CreateAndOpenTestDocument("module Foo {}", Path.Combine(tempDir, "tmp.dfy")); + var documentItem = await CreateOpenAndWaitForResolve("module Foo {}", Path.Combine(tempDir, "tmp.dfy")); var workspaceEdit = await RequestRename(documentItem, new Position(0, 6), "space"); Assert.Null(workspaceEdit); } @@ -140,7 +140,7 @@ private async Task AssertRangesRenamed(IEnumerable sources, string tempD var items = sources.Select(async (source, sourceIndex) => { MarkupTestFile.GetPositionsAndRanges(source, out var cleanSource, out var positions, out var ranges); - var documentItem = await CreateAndOpenTestDocument(cleanSource, Path.Combine(tempDir, $"tmp{sourceIndex}.dfy")); + var documentItem = await CreateOpenAndWaitForResolve(cleanSource, Path.Combine(tempDir, $"tmp{sourceIndex}.dfy")); Assert.InRange(positions.Count, 0, 1); return new DocPosRange(documentItem, positions.FirstOrDefault((Position)null), ranges); }).Select(task => task.Result).ToImmutableList(); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs index 0ddaa930ac0..b62ecb11ebd 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs @@ -72,10 +72,10 @@ method Faz() { ".TrimStart(); var directory = Path.GetRandomFileName(); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var imported = await CreateAndOpenTestDocument(importedSource, Path.Combine(directory, "imported.dfy")); - await CreateAndOpenTestDocument(exporter, Path.Combine(directory, "exporter.dfy")); - var importer = await CreateAndOpenTestDocument(importerSource, Path.Combine(directory, "importer.dfy")); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var imported = await CreateOpenAndWaitForResolve(importedSource, Path.Combine(directory, "imported.dfy")); + await CreateOpenAndWaitForResolve(exporter, Path.Combine(directory, "exporter.dfy")); + var importer = await CreateOpenAndWaitForResolve(importerSource, Path.Combine(directory, "importer.dfy")); // Make a change to imported, which could trigger a bug where some dependants of it are not marked dirty ApplyChange(ref imported, ((0, 0), (0, 0)), "//comment" + Environment.NewLine); @@ -141,9 +141,9 @@ match x { var temp = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); - var noCachingProject = await CreateAndOpenTestDocument(@"[options] + var noCachingProject = await CreateOpenAndWaitForResolve(@"[options] use-caching = false", Path.Combine(temp, "dfyconfig.toml")); - var noCaching = await CreateAndOpenTestDocument(source, Path.Combine(temp, "noCaching.dfy")); + var noCaching = await CreateOpenAndWaitForResolve(source, Path.Combine(temp, "noCaching.dfy")); ApplyChange(ref noCaching, ((0, 0), (0, 0)), "// Pointless comment that triggers a reparse\n"); var hitCountForNoCaching = await WaitAndCountHits(noCaching); Assert.Equal(0, hitCountForNoCaching.ParseHits); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index 4c07053686e..714d66ad3a2 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -28,7 +28,7 @@ mfunction HasParseAndResolutionError(): int { true }".TrimStart(); - var document = await CreateAndOpenTestDocument(source); + var document = await CreateOpenAndWaitForResolve(source); var parseDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.Equal(MessageSource.Parser.ToString(), parseDiagnostics[0].Source); ApplyChange(ref document, new Range(0, 0, 0, 1), " "); @@ -58,9 +58,9 @@ import Producer ".TrimStart(); var directory = Path.GetRandomFileName(); - var project = await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var producer = await CreateAndOpenTestDocument(producerSource, Path.Combine(directory, "producer.dfy")); - var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "consumer.dfy")); + var project = await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var producer = await CreateOpenAndWaitForResolve(producerSource, Path.Combine(directory, "producer.dfy")); + var consumer = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "consumer.dfy")); var diag1 = await GetLastDiagnostics(producer, CancellationToken); Assert.Equal(DiagnosticSeverity.Hint, diag1[0].Severity); ApplyChange(ref consumer, new Range(0, 0, 0, 0), "//trigger change\n"); @@ -75,7 +75,7 @@ function HasResolutionError(): int { true }".TrimStart(); - var document = await CreateAndOpenTestDocument(source); + var document = await CreateOpenAndWaitForResolve(source); var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.Equal(MessageSource.Resolver.ToString(), resolutionDiagnostics[0].Source); ApplyChange(ref document, new Range(3, 0, 3, 0), "// comment to trigger update\n"); @@ -106,7 +106,7 @@ public async Task NoFlickeringWhenMixingCorrectAndErrorBatches() { assert false; } }"; - var document = await CreateAndOpenTestDocument(source); + var document = await CreateOpenAndWaitForResolve(source); var status1 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.Equal(PublishedVerificationStatus.Stale, status1.NamedVerifiables[0].Status); var status12 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); @@ -128,7 +128,7 @@ public async Task IncrementalBatchDiagnostics() { assert false; } }"; - await CreateAndOpenTestDocument(source); + await CreateOpenAndWaitForResolve(source); var diagnostics1 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.Single(diagnostics1); var diagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs index eb3665f8c71..1691b9ebfae 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs @@ -31,9 +31,9 @@ await SetUp(options => { }); var directory = Path.GetRandomFileName(); - var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var docA = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "a.dfy")); - var docB = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "b.dfy")); + var projectFile = await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var docA = await CreateOpenAndWaitForResolve(sourceA, Path.Combine(directory, "a.dfy")); + var docB = await CreateOpenAndWaitForResolve(sourceB, Path.Combine(directory, "b.dfy")); var report = await ghostnessReceiver.AwaitNextNotificationAsync(CancellationToken); var report2 = await ghostnessReceiver.AwaitNextNotificationAsync(CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs index 7a5c249cfcf..02f6416f5e5 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs @@ -54,9 +54,9 @@ public async Task NonErrorDiagnosticDoesNotProduceAnError() { include ""./hasWarning.dfy"" ".TrimStart(); var warningSource = "const tooManySemiColons := 3;"; - await CreateAndOpenTestDocument(warningSource, Path.Combine(TestFileDirectory, "hasWarning.dfy")); + await CreateOpenAndWaitForResolve(warningSource, Path.Combine(TestFileDirectory, "hasWarning.dfy")); await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); - await CreateAndOpenTestDocument(source, TestFilePath); + await CreateOpenAndWaitForResolve(source, TestFilePath); await AssertNoDiagnosticsAreComing(CancellationToken); } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/ProjectManagerDatabaseTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/ProjectManagerDatabaseTest.cs index 69a33446b84..588ad2f009a 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/ProjectManagerDatabaseTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/ProjectManagerDatabaseTest.cs @@ -20,7 +20,7 @@ public async Task OpenAndCloseConcurrentlySeparateProjects() { var source = "// comment"; var loadingDocuments = new List(); for (int i = 0; i < documentsToLoadConcurrently; i++) { - var documentItem = await CreateAndOpenTestDocument(source, $"pmdtest1_{i}.dfy"); + var documentItem = await CreateOpenAndWaitForResolve(source, $"pmdtest1_{i}.dfy"); loadingDocuments.Add(documentItem); } @@ -41,13 +41,13 @@ public async Task ConcurrentProjectMigration() { var loadingDocuments = new List(); var directory = Path.GetRandomFileName(); for (int i = 0; i < documentsToLoadConcurrently; i++) { - var documentItem = await CreateAndOpenTestDocument(source, Path.Combine(directory, $"nested{i}/pmdtest2.dfy")); + var documentItem = await CreateOpenAndWaitForResolve(source, Path.Combine(directory, $"nested{i}/pmdtest2.dfy")); loadingDocuments.Add(documentItem); } // Create a project file for each test document. for (int i = 0; i < documentsToLoadConcurrently; i++) { - await CreateAndOpenTestDocument("", Path.Combine(directory, $"nested{i}/{DafnyProject.FileName}")); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, $"nested{i}/{DafnyProject.FileName}")); } // Concurrently migrate projects @@ -70,7 +70,7 @@ public async Task OpenAndCloseConcurrentlySameProject() { var project = CreateTestDocument("", Path.Combine(directory, DafnyProject.FileName)); client.OpenDocument(project); for (int i = 0; i < documentsToLoadConcurrently; i++) { - var documentItem = await CreateAndOpenTestDocument(source, Path.Combine(directory, $"pmdtest3_{i}.dfy")); + var documentItem = await CreateOpenAndWaitForResolve(source, Path.Combine(directory, $"pmdtest3_{i}.dfy")); loadingDocuments.Add(documentItem); } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs index 03d22151b86..f65920a3799 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs @@ -28,7 +28,7 @@ method Foo() { ".TrimStart(); var directory = Path.GetRandomFileName(); - var firstFile = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "firstFile.dfy")); + var firstFile = await CreateOpenAndWaitForResolve(sourceA, Path.Combine(directory, "firstFile.dfy")); await WaitUntilCompletedForUris(1, CancellationToken); @@ -69,9 +69,9 @@ method Bar() { ".TrimStart(); var directory = Path.GetRandomFileName(); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var firstFile = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "firstFile.dfy")); - var secondFile = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "secondFile.dfy")); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var firstFile = await CreateOpenAndWaitForResolve(sourceA, Path.Combine(directory, "firstFile.dfy")); + var secondFile = await CreateOpenAndWaitForResolve(sourceB, Path.Combine(directory, "secondFile.dfy")); await WaitUntilCompletedForUris(2, CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 2d72d0baecf..4f33e5e6966 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -33,10 +33,10 @@ method ShouldNotBeAffectedByChange() { ".TrimStart(); var directory = Path.GetRandomFileName(); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var documentA = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "sourceA.dfy")); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var documentA = await CreateOpenAndWaitForResolve(sourceA, Path.Combine(directory, "sourceA.dfy")); await WaitUntilAllStatusAreCompleted(documentA); - var documentB = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "sourceB.dfy")); + var documentB = await CreateOpenAndWaitForResolve(sourceB, Path.Combine(directory, "sourceB.dfy")); await WaitUntilAllStatusAreCompleted(documentB); ApplyChange(ref documentA, new Range(3, 0, 3, 0), "// change\n"); await AssertNoVerificationStatusIsComing(documentB, CancellationToken); @@ -50,7 +50,7 @@ method WillVerify() { } ".TrimStart(); - var document = await CreateAndOpenTestDocument(source); + var document = await CreateOpenAndWaitForResolve(source); var firstStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); ApplyChange(ref document, new Range(3, 0, 3, 0), "//change comment\n"); await AssertNoVerificationStatusIsComing(document, CancellationToken); @@ -73,7 +73,7 @@ public async Task TryingToVerifyShowsUpAsQueued() { await SetUp(options => { options.Set(ServerCommand.Verification, VerifyOnMode.Never); }); - var documentItem1 = await CreateAndOpenTestDocument(source, "PreparingVerificationShowsUpAsAllQueued.dfy"); + var documentItem1 = await CreateOpenAndWaitForResolve(source, "PreparingVerificationShowsUpAsAllQueued.dfy"); _ = client.RunSymbolVerification(documentItem1, new Position(0, 7), CancellationToken); _ = client.RunSymbolVerification(documentItem1, new Position(4, 7), CancellationToken); while (true) { @@ -110,9 +110,9 @@ await SetUp(options => { options.Set(ServerCommand.Verification, VerifyOnMode.Never); }); var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); - var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); - var documentItem2 = await CreateAndOpenTestDocument(source.Replace("Foo", "Bar"), Path.Combine(directory, "RunWithMultipleDocuments2.dfy")); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); + var documentItem1 = await CreateOpenAndWaitForResolve(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); + var documentItem2 = await CreateOpenAndWaitForResolve(source.Replace("Foo", "Bar"), Path.Combine(directory, "RunWithMultipleDocuments2.dfy")); var fooRange = new Range(0, 7, 0, 10); await client.RunSymbolVerification(documentItem1, fooRange.Start, CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 32905f929f3..79080145232 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -48,7 +48,14 @@ protected ClientBasedLanguageServerTest(ITestOutputHelper output, LogLevel dafny : base(output, dafnyLogLevel) { } - protected async Task CreateAndOpenTestDocument(string source, string filePath = null, + protected TextDocumentItem CreateAndOpenTestDocument(string source, string filePath = null, + int version = 1) { + var document = CreateTestDocument(source, filePath, version); + client.OpenDocument(document); + return document; + } + + protected async Task CreateOpenAndWaitForResolve(string source, string filePath = null, int version = 1, CancellationToken? cancellationToken = null) { var document = CreateTestDocument(source, filePath, version); await client.OpenDocumentAndWaitAsync(document, cancellationToken ?? CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs index 8e30b8d074f..02be3ba32f7 100644 --- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs @@ -36,14 +36,14 @@ method Bar() { Directory.CreateDirectory(directory); await File.WriteAllTextAsync(Path.Combine(directory, "producer.dfy"), producerSource); await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), ""); - await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "consumer.dfy")); + await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(directory, "consumer.dfy")); var a = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); var a2 = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); var a3 = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); var a4 = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); - await CreateAndOpenTestDocument(producerSource, Path.Combine(directory, "producer.dfy")); - var somethingElse = await CreateAndOpenTestDocument("method Foo() {}", "somethingElse"); + await CreateOpenAndWaitForResolve(producerSource, Path.Combine(directory, "producer.dfy")); + var somethingElse = await CreateOpenAndWaitForResolve("method Foo() {}", "somethingElse"); var a6 = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.Equal(somethingElse.Uri, a6.Uri); } @@ -56,10 +56,10 @@ method Foo() returns (x: int) { }".TrimStart(); var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); Directory.CreateDirectory(directory); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); var secondFilePath = Path.Combine(directory, "RunWithMultipleDocuments2.dfy"); await File.WriteAllTextAsync(secondFilePath, source.Replace("Foo", "Bar").Replace("2", "true")); - var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); + var documentItem1 = await CreateOpenAndWaitForResolve(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); var expectedStatuses = new[] { CompilationStatus.ResolutionStarted, @@ -87,10 +87,10 @@ method Foo() returns (x: int) { }".TrimStart(); var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); Directory.CreateDirectory(directory); - await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); + await CreateOpenAndWaitForResolve("", Path.Combine(directory, DafnyProject.FileName)); var secondFilePath = Path.Combine(directory, "RunWithMultipleDocuments2.dfy"); await File.WriteAllTextAsync(secondFilePath, source.Replace("Foo", "Bar")); - var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); + var documentItem1 = await CreateOpenAndWaitForResolve(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); var expectedStatuses = new[] { CompilationStatus.ResolutionStarted, diff --git a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs index 3eedc13d42a..ab212758006 100644 --- a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs @@ -18,7 +18,7 @@ public class DiagnosticMigrationTest : ClientBasedLanguageServerTest { [Fact] public async Task ResolutionDiagnosticsContainPreviousVerificationResultsWhenCodeIsInsertedAfter() { - var documentItem = await CreateAndOpenTestDocument(FastToFailVerification, "untitled:Untitled-1"); + var documentItem = await CreateOpenAndWaitForResolve(FastToFailVerification, "untitled:Untitled-1"); var verificationDiagnostics = await GetLastDiagnostics(documentItem, CancellationToken); Assert.Single(verificationDiagnostics); ApplyChange(ref documentItem, new Range(0, 47, 0, 47), "\n\n" + NeverVerifies); diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index 15c290ccf61..9c14aab1ac8 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs @@ -124,11 +124,11 @@ public Task ParseAsync(DafnyOptions options, Compilatio } public Task ResolveAsync(DafnyOptions options, CompilationAfterParsing compilation, - IReadOnlyDictionary migratedVerificationTrees, CancellationToken cancellationToken) { + CancellationToken cancellationToken) { if (tests.CrashOnLoad) { throw new IOException("testing crash"); } - return loader.ResolveAsync(options, compilation, migratedVerificationTrees, cancellationToken); + return loader.ResolveAsync(options, compilation, cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs index 175f0eeea84..1a150d5a152 100644 --- a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs +++ b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs @@ -119,7 +119,7 @@ private async Task ParseAsync() { private async Task ResolveAsync() { try { var parsedCompilation = await ParsedCompilation; - var resolvedCompilation = await documentLoader.ResolveAsync(options, parsedCompilation, migratedVerificationTrees, cancellationSource.Token); + var resolvedCompilation = await documentLoader.ResolveAsync(options, parsedCompilation, cancellationSource.Token); if (!resolvedCompilation.Program.Reporter.HasErrors) { verificationProgressReporter.RecomputeVerificationTrees(resolvedCompilation); diff --git a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs index 734dfce71fc..76cbeb2ea7b 100644 --- a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs @@ -25,7 +25,6 @@ Task ParseAsync(DafnyOptions options, Compilation compi IReadOnlyDictionary migratedVerificationTrees, CancellationToken cancellationToken); Task ResolveAsync(DafnyOptions options, CompilationAfterParsing compilation, - IReadOnlyDictionary migratedVerificationTrees, CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index acaa41364b9..cb4a305d392 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -92,16 +92,14 @@ private CompilationAfterParsing ParseInternal(DafnyOptions options, Compilation public async Task ResolveAsync(DafnyOptions options, CompilationAfterParsing compilation, - IReadOnlyDictionary migratedVerificationTrees, CancellationToken cancellationToken) { #pragma warning disable CS1998 return await await DafnyMain.LargeStackFactory.StartNew( - async () => ResolveInternal(compilation, migratedVerificationTrees, cancellationToken), cancellationToken); + async () => ResolveInternal(compilation, cancellationToken), cancellationToken); #pragma warning restore CS1998 } - private CompilationAfterResolution ResolveInternal(CompilationAfterParsing compilation, - IReadOnlyDictionary migratedVerificationTrees, CancellationToken cancellationToken) { + private CompilationAfterResolution ResolveInternal(CompilationAfterParsing compilation, CancellationToken cancellationToken) { var program = compilation.Program; var errorReporter = (DiagnosticErrorReporter)program.Reporter; @@ -109,14 +107,17 @@ private CompilationAfterResolution ResolveInternal(CompilationAfterParsing compi throw new TaskCanceledException(); } + var cloner = new Cloner(true, false); + var programClone = new Program(cloner, program); + var project = compilation.Project; - var compilationUnit = symbolResolver.ResolveSymbols(project, program, cancellationToken); + var compilationUnit = symbolResolver.ResolveSymbols(project, programClone, cancellationToken); var legacySymbolTable = symbolTableFactory.CreateFrom(compilationUnit, cancellationToken); var newSymbolTable = errorReporter.HasErrors ? null - : symbolTableFactory.CreateFrom(program, compilation, cancellationToken); + : symbolTableFactory.CreateFrom(programClone, compilation, cancellationToken); var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics(legacySymbolTable, cancellationToken); @@ -124,14 +125,15 @@ private CompilationAfterResolution ResolveInternal(CompilationAfterParsing compi if (errorReporter.HasErrorsUntilResolver) { verifiables = new(); } else { - var symbols = SymbolExtensions.GetSymbolDescendants(program.DefaultModule); + var symbols = SymbolExtensions.GetSymbolDescendants(programClone.DefaultModule); verifiables = symbols.OfType().Where(v => !AutoGeneratedToken.Is(v.RangeToken) && v.ContainingModule.ShouldVerify(program.Compilation) && - v.ShouldVerify(program.Compilation) && + v.ShouldVerify(programClone.Compilation) && v.ShouldVerify).ToList(); } - return new CompilationAfterResolution(compilation, + var compilationAfterParsingWithProgramClone = new CompilationAfterParsing(compilation, programClone, compilation.ResolutionDiagnostics, compilation.VerificationTrees); + return new CompilationAfterResolution(compilationAfterParsingWithProgramClone, errorReporter.AllDiagnosticsCopy, newSymbolTable, legacySymbolTable,