Improve performance for large projects

Source/DafnyCore.Test/NodeTests.cs

@@ -1,7 +1,7 @@
 using System.Collections.Concurrent;
 using Microsoft.Dafny;
 
-namespace DafnyCore.Test; 
+namespace DafnyCore.Test;
 
 public class NodeTests {
 

Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs → Source/DafnyCore.Test/WriterFromOutputHelper.cs

@@ -1,13 +1,8 @@
-// Copyright by the contributors to the Dafny Project
-// SPDX-License-Identifier: MIT
-
-#nullable disable
-using System.IO;
+#nullable enable
 using System.Text;
-using Microsoft.Extensions.Primitives;
 using Xunit.Abstractions;
 
-namespace DafnyTestGeneration.Test;
+namespace DafnyCore.Test;
 
 public class WriterFromOutputHelper : TextWriter {
   private readonly StringBuilder buffer = new();
@@ -17,7 +12,7 @@ public WriterFromOutputHelper(ITestOutputHelper output) {
     this.output = output;
   }
 
-  public override void Write(string value) {
+  public override void Write(string? value) {
     if (value != null) {
       buffer.Append(value);
     }
@@ -29,12 +24,12 @@ public override void Write(char value) {
 
   public override Encoding Encoding => Encoding.Default;
 
-  public override void WriteLine(string value) {
+  public override void WriteLine(string? value) {
     output.WriteLine(buffer + value);
     buffer.Clear();
   }
 
-  public override void WriteLine(string format, params object[] arg) {
+  public override void WriteLine(string format, params object?[] arg) {
     output.WriteLine(buffer + format, arg);
     buffer.Clear();
   }

Source/DafnyCore/DafnyFile.cs

@@ -1,7 +1,6 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
-using System.Linq;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
 using DafnyCore;

Source/DafnyCore/Options/DafnyProject.cs

@@ -56,37 +56,67 @@ public IEnumerable<Uri> GetRootSourceUris(IFileSystem fileSystem) {
     if (!Uri.IsFile) {
       return new[] { Uri };
     }
+    var matcher = GetMatcher(out var searchRoot);
 
-    var matcher = GetMatcher();
-
-    var diskRoot = Path.GetPathRoot(Uri.LocalPath);
-    var result = matcher.Execute(fileSystem.GetDirectoryInfoBase(diskRoot));
-    var files = result.Files.Select(f => Path.Combine(diskRoot, f.Path));
+    var result = matcher.Execute(fileSystem.GetDirectoryInfoBase(searchRoot));
+    var files = result.Files.Select(f => Path.Combine(searchRoot, f.Path));
     return files.Select(file => new Uri(Path.GetFullPath(file)));
   }
 
   public bool ContainsSourceFile(Uri uri) {
-    var fileSystemWithSourceFile = new InMemoryDirectoryInfoFromDotNet8(Path.GetPathRoot(uri.LocalPath)!, new[] { uri.LocalPath });
-    return GetMatcher().Execute(fileSystemWithSourceFile).HasMatches;
+    var matcher = GetMatcher(out var searchRoot);
+    var fileSystemWithSourceFile = new InMemoryDirectoryInfoFromDotNet8(searchRoot, new[] { uri.LocalPath });
+    return matcher.Execute(fileSystemWithSourceFile).HasMatches;
   }
 
-  private Matcher GetMatcher() {
+  private Matcher GetMatcher(out string commonRoot) {
     var projectRoot = Path.GetDirectoryName(Uri.LocalPath)!;
-    var root = Path.GetPathRoot(Uri.LocalPath)!;
+    var diskRoot = Path.GetPathRoot(Uri.LocalPath)!;
+
+    var includes = Includes ?? new[] { "**/*.dfy" };
+    var excludes = Excludes ?? Array.Empty<string>();
+    var fullPaths = includes.Concat(excludes).Select(p => Path.GetFullPath(p, projectRoot)).ToList();
+    commonRoot = GetCommonParentDirectory(fullPaths) ?? diskRoot;
     var matcher = new Matcher();
-    foreach (var includeGlob in Includes ?? new[] { "**/*.dfy" }) {
-      var fullPath = Path.GetFullPath(includeGlob, projectRoot);
-      matcher.AddInclude(Path.GetRelativePath(root, fullPath));
+    foreach (var includeGlob in includes) {
+      matcher.AddInclude(Path.GetRelativePath(commonRoot, Path.GetFullPath(includeGlob, projectRoot)));
     }
 
-    foreach (var includeGlob in Excludes ?? Enumerable.Empty<string>()) {
-      var fullPath = Path.GetFullPath(includeGlob, projectRoot);
-      matcher.AddExclude(Path.GetRelativePath(root, fullPath));
+    foreach (var excludeGlob in excludes) {
+      matcher.AddExclude(Path.GetRelativePath(commonRoot, Path.GetFullPath(excludeGlob, projectRoot)));
     }
 
     return matcher;
   }
 
+  string GetCommonParentDirectory(IReadOnlyList<string> strings) {
+    if (!strings.Any()) {
+      return null;
+    }
+    var commonPrefix = strings.FirstOrDefault() ?? "";
+
+    foreach (var newString in strings) {
+      var potentialMatchLength = Math.Min(newString.Length, commonPrefix.Length);
+
+      if (potentialMatchLength < commonPrefix.Length) {
+        commonPrefix = commonPrefix.Substring(0, potentialMatchLength);
+      }
+
+      for (var i = 0; i < potentialMatchLength; i++) {
+        if (newString[i] == '*' || newString[i] != commonPrefix[i]) {
+          commonPrefix = commonPrefix.Substring(0, i);
+          break;
+        }
+      }
+    }
+
+    if (!Path.EndsInDirectorySeparator(commonPrefix)) {
+      commonPrefix = Path.GetDirectoryName(commonPrefix);
+    }
+
+    return commonPrefix;
+  }
+
   public void Validate(TextWriter outputWriter, IEnumerable<Option> possibleOptions) {
     if (Options == null) {
       return;

Source/DafnyDriver/DafnyDoc.cs

@@ -50,8 +50,6 @@ public static DafnyDriver.ExitValue DoDocumenting(IReadOnlyList<DafnyFile> dafny
       outputdir = DefaultOutputDir;
     }
 
-
-
     // Collect all the dafny files; dafnyFiles already includes files from a .toml project file
     var exitValue = DafnyDriver.ExitValue.SUCCESS;
     dafnyFiles = dafnyFiles.Concat(dafnyFolders.SelectMany(folderPath => {

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

@@ -10,7 +10,7 @@
     <PackageReference Include="DiffPlex" Version="1.7.0" />
     <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
     <PackageReference Include="Microsoft.Extensions.Logging.Console" Version="5.0.0" />
-    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
+    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.1.0" />
     <PackageReference Include="Moq" Version="4.16.1" />
     <PackageReference Include="Serilog.Sinks.InMemory" Version="0.11.0" />
     <PackageReference Include="xunit" Version="2.4.2" />
@@ -25,6 +25,7 @@
   </ItemGroup>
 
   <ItemGroup>
+    <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
     <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
   </ItemGroup>
 

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -16,6 +16,7 @@
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
 using Microsoft.Dafny.LanguageServer.Language;
 using OmniSharp.Extensions.LanguageServer.Client;
@@ -94,6 +95,7 @@ public AnonymousDisposable(Action action) {
 
     private Action<LanguageServerOptions> GetServerOptionsAction(Action<DafnyOptions> modifyOptions) {
       var dafnyOptions = DafnyOptions.Create(output);
+      dafnyOptions.Set(ServerCommand.UpdateThrottling, 0);
       modifyOptions?.Invoke(dafnyOptions);
       ServerCommand.ConfigureDafnyOptionsForServer(dafnyOptions);
       ApplyDefaultOptionValues(dafnyOptions);

Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs

@@ -0,0 +1,111 @@
+using System;
+using System.Text;
+using System.Threading;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Xunit;
+using Xunit.Abstractions;
+using Xunit.Sdk;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Performance;
+
+public class LargeFilesTest : ClientBasedLanguageServerTest {
+  protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
+    return base.SetUp(options => {
+      modifyOptions?.Invoke(options);
+      options.Set(ServerCommand.UpdateThrottling, ServerCommand.DefaultThrottleTime);
+    });
+  }
+
+  /// <summary>
+  /// This test should complete in less than a second, because it opens a moderately sized file
+  /// on which it makes edits so quickly that the edits should all be processed in a single compilation.
+  /// And a single compilation should complete in less than 200ms.
+  ///
+  /// Right now the test still takes more than 5 seconds.
+  /// To reduce runtime of this test,
+  /// remove ReportRealtimeDiagnostics (since it is called 10 times for each update,
+  /// and calls InitialIdeState, which often calls CompilationAfterResolution.ToIdeState (expensive))
+  /// </summary>
+  [Fact]
+  public async Task QuickEditsInLargeFile() {
+    string GetLineContent(int index) => $"method Foo{index}() {{ assume false; }}";
+    var contentBuilder = new StringBuilder();
+    for (int lineNumber = 0; lineNumber < 1000; lineNumber++) {
+      contentBuilder.AppendLine(GetLineContent(lineNumber));
+    }
+    var source = contentBuilder.ToString();
+
+    double lowest = double.MaxValue;
+    Exception lastException = null;
+    try {
+      for (int attempt = 0; attempt < 10; attempt++) {
+        var cancelSource = new CancellationTokenSource();
+        var measurementTask = AssertThreadPoolIsAvailable(cancelSource.Token);
+        var beforeOpen = DateTime.Now;
+        var documentItem = await CreateAndOpenTestDocument(source, "ManyFastEditsUsingLargeFiles.dfy",
+          cancellationToken: CancellationTokenWithHighTimeout);
+        var afterOpen = DateTime.Now;
+        var openMilliseconds = (afterOpen - beforeOpen).TotalMilliseconds;
+        for (int i = 0; i < 100; i++) {
+          ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "// added this comment\n");
+        }
+
+        await client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationTokenWithHighTimeout);
+        var afterChange = DateTime.Now;
+        var changeMilliseconds = (afterChange - afterOpen).TotalMilliseconds;
+        await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout);
+        cancelSource.Cancel();
+        var averageTimeToSchedule = await measurementTask;
+        var division = changeMilliseconds / openMilliseconds;
+        lowest = Math.Min(lowest, division);
+
+        // Commented code left in intentionally
+        // await output.WriteLineAsync("openMilliseconds: " + openMilliseconds);
+        // await output.WriteLineAsync("changeMilliseconds: " + changeMilliseconds);
+        // await output.WriteLineAsync("division: " + division);
+        try {
+          Assert.True(averageTimeToSchedule < 100);
+          // Migration should be constant time, which would allow this number to be about 1.
+          // Right now migration is still slow so this has been set to 10 so the test can pass.
+          var changeTimeMultiplier = 15;
+          Assert.True(division < changeTimeMultiplier,
+            $"changeMilliseconds {changeMilliseconds}, openMilliseconds {openMilliseconds}");
+
+          return;
+        } catch (AssertActualExpectedException e) {
+          lastException = e;
+        }
+      }
+    } catch (OperationCanceledException) {
+    }
+
+    await output.WriteLineAsync("lowest division " + lowest);
+    throw lastException!;
+  }
+
+  private async Task<double> AssertThreadPoolIsAvailable(CancellationToken durationToken) {
+    int ticks = 0;
+    var waitTime = 100;
+    var start = DateTime.Now;
+    while (!durationToken.IsCancellationRequested) {
+      await Task.Run(() => {
+        Thread.Sleep(waitTime);
+      });
+      ticks++;
+    }
+
+    var end = DateTime.Now;
+    var span = end - start;
+    var totalSleepTime = ticks * waitTime;
+    var totalSchedulingTime = span.TotalMilliseconds - totalSleepTime;
+    var averageTimeToSchedule = totalSchedulingTime / ticks;
+    // await output.WriteLineAsync($"averageTimeToSchedule: {averageTimeToSchedule:0.##}");
+    return averageTimeToSchedule;
+  }
+
+  public LargeFilesTest(ITestOutputHelper output) : base(output) {
+  }
+}

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -99,23 +99,30 @@ method Foo() {
   }
 
   [Fact]
-  public async Task FileOnlyAttachedToProjectFileThatAppliesToIt() {
+  public async Task FileOnlyAttachedToProjectFileThatIncludesIt() {
     await SetUp(options => options.WarnShadowing = false);
 
-    var projectFileSource = @"
+    var outerSource = @"
 [options]
 warn-shadowing = true
 ";
     var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
-    var outerProjectFile = CreateTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName));
+    var outerProjectFile = CreateTestDocument(outerSource, Path.Combine(directory, DafnyProject.FileName));
     await client.OpenDocumentAndWaitAsync(outerProjectFile, CancellationToken);
 
-    var innerProjectFile = CreateTestDocument("includes = []", Path.Combine(directory, "nested", DafnyProject.FileName));
+    var innerDirectory = Path.Combine(directory, "nested");
+    var innerProjectFile = CreateTestDocument("includes = []", Path.Combine(innerDirectory, DafnyProject.FileName));
     await client.OpenDocumentAndWaitAsync(innerProjectFile, CancellationToken);
 
-    var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy");
-    var source = await File.ReadAllTextAsync(filePath);
-    var documentItem = CreateTestDocument(source, Path.Combine(directory, "nested/A.dfy"));
+    var source = @"
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
+";
+    var documentItem = CreateTestDocument(source, Path.Combine(innerDirectory, "A.dfy"));
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
     var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
     Assert.Single(diagnostics);

Source/DafnyLanguageServer.Test/StandaloneServerTest.cs

@@ -1,6 +1,7 @@
 using System;
 using System.IO;
 using System.Text;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Xunit.Abstractions;
 using Xunit;
@@ -21,29 +22,3 @@ public void OptionParsing() {
     Assert.Equal(VerifyOnMode.Save, options.Get(ServerCommand.Verification));
   }
 }
-
-public class WriterFromOutputHelper : TextWriter {
-  private readonly ITestOutputHelper output;
-  private bool failed = false;
-
-  public WriterFromOutputHelper(ITestOutputHelper output) {
-    this.output = output;
-  }
-
-  public override void Write(char value) {
-    if (!failed) {
-      failed = true;
-      WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support.");
-    }
-  }
-
-  public override Encoding Encoding => Encoding.Default;
-
-  public override void WriteLine(string value) {
-    output.WriteLine(value);
-  }
-
-  public override void WriteLine(string format, params object[] arg) {
-    output.WriteLine(format, arg);
-  }
-}

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -924,16 +924,17 @@ method test() {
 ".TrimStart();
       var documentItem = CreateTestDocument(source, "IncrementalVerificationDiagnosticsBetweenMethods.dfy");
       client.OpenDocument(documentItem);
-      var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
+      var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
       try {
         var secondVerificationDiagnostics =
           await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
 
-        Assert.Single(firstVerificationDiagnostics);
+        Assert.Single(firstVerificationDiagnostics.Diagnostics);
         // Second diagnostic is a timeout exception from SlowToVerify
         Assert.Equal(2, secondVerificationDiagnostics.Length);
       } catch (OperationCanceledException) {
         await output.WriteLineAsync($"firstVerificationDiagnostics: {firstVerificationDiagnostics.Stringify()}");
+        WriteVerificationHistory();
       }
       await AssertNoDiagnosticsAreComing(CancellationToken);
     }