Prevent modification exception when accessing parsed document (dafny-…

…lang#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.

<small>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).</small>

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<ModuleDefinition> Modules() {
 

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);
 

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<LineVerificationStatus[]>();

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);

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();

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```]

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;

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();

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);