Add basic support for cancellation of resolution (#4175)

### Changes
- Add support for cancelling resolution work at module granularity.
Before this PR, the language server would always finish it's currently
running resolution job before starting resolution on the most recent
changes, skipping resolution work of obsolete changes that was not yet
started. With this PR, the language server can also stop it's current
resolution work at the module boundaries.
- Add a telemetry publication that says how much time was spent on
resolution

### Testing

I see improved behavior on large Dafny codebases with this change. The
IDE generally becomes more responsive, switching away from
'Resolving...' into other states faster.

Given that from a user perspective the resolution process is black box,
there's no contract for when in that process cancellation should be
supported. I think the right way to test this is to have a codebase that
takes a long time to resolve, and to test that changes will always
cancel the current resolution within a time smaller than X. However,
making such a test is time consuming and I would like to deliver this
fix to users already, so I'm not adding such a test yet.

I also haven't added a test for the telemetry change but that is not a
user facing change.

<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/DafnyMain.cs

@@ -87,7 +87,7 @@ public static string Resolve(Program program) {
       }
 
       var r = new Resolver(program);
-      LargeStackFactory.StartNew(() => r.ResolveProgram(program)).Wait();
+      LargeStackFactory.StartNew(() => r.ResolveProgram(program, CancellationToken.None)).Wait();
       MaybePrintProgram(program, program.Options.DafnyPrintResolvedFile, true);
 
       if (program.Reporter.ErrorCountUntilResolver != 0) {

Source/DafnyCore/Resolver/Resolver.cs

@@ -13,6 +13,7 @@
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Reflection;
+using System.Threading;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
 using Microsoft.Boogie;
@@ -232,7 +233,7 @@ void CheckDupModuleNames(Program prog) {
       }
     }
 
-    public void ResolveProgram(Program prog) {
+    public void ResolveProgram(Program prog, CancellationToken cancellationToken) {
       Contract.Requires(prog != null);
       Type.ResetScopes();
 
@@ -296,11 +297,14 @@ public void ResolveProgram(Program prog) {
       ResolveTopLevelDecls_Core(ModuleDefinition.AllDeclarationsAndNonNullTypeDecls(systemModuleClassesWithNonNullTypes).ToList(),
         new Graph<IndDatatypeDecl>(), new Graph<CoDatatypeDecl>(), prog.BuiltIns.SystemModule.Name);
 
+
       foreach (var rewriter in prog.Rewriters) {
+        cancellationToken.ThrowIfCancellationRequested();
         rewriter.PreResolve(prog);
       }
 
       foreach (var decl in sortedDecls) {
+        cancellationToken.ThrowIfCancellationRequested();
         ResolveModuleDeclaration(prog, decl, origErrorCount);
       }
 
@@ -313,11 +317,14 @@ public void ResolveProgram(Program prog) {
 
       foreach (var module in prog.Modules()) {
         foreach (var rewriter in prog.Rewriters) {
+          cancellationToken.ThrowIfCancellationRequested();
           rewriter.PostResolve(module);
         }
       }
 
+
       foreach (var rewriter in prog.Rewriters) {
+        cancellationToken.ThrowIfCancellationRequested();
         rewriter.PostResolve(prog);
       }
     }

Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace;
 using Microsoft.Extensions.Logging;
 using Moq;
 
@@ -12,7 +13,8 @@ public class DafnyLangSymbolResolverTest {
   public DafnyLangSymbolResolverTest() {
     var loggerFactory = new Mock<ILoggerFactory>();
     dafnyLangSymbolResolver = new DafnyLangSymbolResolver(
-      loggerFactory.Object.CreateLogger<DafnyLangSymbolResolver>()
+      loggerFactory.Object.CreateLogger<DafnyLangSymbolResolver>(),
+      new Mock<ITelemetryPublisher>().Object
     );
   }
 

Source/DafnyLanguageServer/Language/DafnyLangParser.cs

@@ -52,18 +52,18 @@ public Dafny.Program CreateUnparsed(TextDocumentItem document, ErrorReporter err
     public Dafny.Program Parse(DocumentTextBuffer document, ErrorReporter errorReporter, CancellationToken cancellationToken) {
       mutex.Wait(cancellationToken);
 
+      var beforeParsing = DateTime.Now;
       try {
-        var beforeParsing = DateTime.Now;
         var result = cachingParser.ParseFiles(document.Uri.ToString(),
           new DafnyFile[]
           {
             new(errorReporter.Options, document.Uri.ToUri(), document.Content)
           },
           errorReporter, cancellationToken);
-        telemetryPublisher.PublishTime("Parse", document.Uri.ToString(), DateTime.Now - beforeParsing);
         return result;
       }
       finally {
+        telemetryPublisher.PublishTime("Parse", document.Uri.ToString(), DateTime.Now - beforeParsing);
         cachingParser.Prune();
         mutex.Release();
       }

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

@@ -5,6 +5,7 @@
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Threading;
+using Microsoft.Dafny.LanguageServer.Workspace;
 
 namespace Microsoft.Dafny.LanguageServer.Language.Symbols {
   /// <summary>
@@ -17,9 +18,11 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols {
   public class DafnyLangSymbolResolver : ISymbolResolver {
     private readonly ILogger logger;
     private readonly SemaphoreSlim resolverMutex = new(1);
+    private readonly ITelemetryPublisher telemetryPublisher;
 
-    public DafnyLangSymbolResolver(ILogger<DafnyLangSymbolResolver> logger) {
+    public DafnyLangSymbolResolver(ILogger<DafnyLangSymbolResolver> logger, ITelemetryPublisher telemetryPublisher) {
       this.logger = logger;
+      this.telemetryPublisher = telemetryPublisher;
     }
 
     public CompilationUnit ResolveSymbols(TextDocumentItem textDocument, Dafny.Program program, out bool canDoVerification, CancellationToken cancellationToken) {
@@ -28,7 +31,7 @@ public CompilationUnit ResolveSymbols(TextDocumentItem textDocument, Dafny.Progr
       //      other classes as well.
       resolverMutex.Wait(cancellationToken);
       try {
-        if (!RunDafnyResolver(textDocument, program)) {
+        if (!RunDafnyResolver(textDocument, program, cancellationToken)) {
           // We cannot proceed without a successful resolution. Due to the contracts in dafny-lang, we cannot
           // access a property without potential contract violations. For example, a variable may have an
           // unresolved type represented by null. However, the contract prohibits the use of the type property
@@ -41,18 +44,29 @@ public CompilationUnit ResolveSymbols(TextDocumentItem textDocument, Dafny.Progr
         resolverMutex.Release();
       }
       canDoVerification = true;
-      return new SymbolDeclarationResolver(logger, cancellationToken).ProcessProgram(textDocument.Uri.ToUri(), program);
+      var beforeLegacyServerResolution = DateTime.Now;
+      var compilationUnit = new SymbolDeclarationResolver(logger, cancellationToken).ProcessProgram(textDocument.Uri.ToUri(), program);
+      telemetryPublisher.PublishTime("LegacyServerResolution", textDocument.Uri.ToString(), DateTime.Now - beforeLegacyServerResolution);
+      return compilationUnit;
     }
 
-    private bool RunDafnyResolver(TextDocumentItem document, Dafny.Program program) {
-      var resolver = new Resolver(program);
-      resolver.ResolveProgram(program);
-      int resolverErrors = resolver.Reporter.ErrorCountUntilResolver;
-      if (resolverErrors > 0) {
-        logger.LogDebug("encountered {ErrorCount} errors while resolving {DocumentUri}", resolverErrors, document.Uri);
-        return false;
+    private bool RunDafnyResolver(TextDocumentItem document, Dafny.Program program, CancellationToken cancellationToken) {
+      var beforeResolution = DateTime.Now;
+      try {
+        var resolver = new Resolver(program);
+        resolver.ResolveProgram(program, cancellationToken);
+        int resolverErrors = resolver.Reporter.ErrorCountUntilResolver;
+        if (resolverErrors > 0) {
+          logger.LogDebug("encountered {ErrorCount} errors while resolving {DocumentUri}", resolverErrors,
+            document.Uri);
+          return false;
+        }
+
+        return true;
+      }
+      finally {
+        telemetryPublisher.PublishTime("Resolution", document.Uri.ToString(), DateTime.Now - beforeResolution);
       }
-      return true;
     }
 
     private class SymbolDeclarationResolver {

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

@@ -93,25 +93,32 @@ private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuff
       }
 
       statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionStarted);
-      var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, out _, cancellationToken);
-      var symbolTable = symbolTableFactory.CreateFrom(compilationUnit, cancellationToken);
+      try {
+        var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, out _, cancellationToken);
+        var symbolTable = symbolTableFactory.CreateFrom(compilationUnit, cancellationToken);
 
-      var newSymbolTable = errorReporter.HasErrors ? null : symbolTableFactory.CreateFrom(program, documentAfterParsing, cancellationToken);
-      if (errorReporter.HasErrors) {
-        statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionFailed);
-      } else {
-        statusPublisher.SendStatusNotification(textDocument, CompilationStatus.CompilationSucceeded);
-      }
+        var newSymbolTable = errorReporter.HasErrors
+          ? null
+          : symbolTableFactory.CreateFrom(program, documentAfterParsing, cancellationToken);
+        if (errorReporter.HasErrors) {
+          statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionFailed);
+        } else {
+          statusPublisher.SendStatusNotification(textDocument, CompilationStatus.CompilationSucceeded);
+        }
 
-      var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics(symbolTable, cancellationToken).ToArray();
+        var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics(symbolTable, cancellationToken)
+          .ToArray();
 
-      return new DocumentAfterResolution(textDocument,
-        program,
-        errorReporter.AllDiagnosticsCopy,
-        newSymbolTable,
-        symbolTable,
-        ghostDiagnostics
-      );
+        return new DocumentAfterResolution(textDocument,
+          program,
+          errorReporter.AllDiagnosticsCopy,
+          newSymbolTable,
+          symbolTable,
+          ghostDiagnostics
+        );
+      } catch (OperationCanceledException) {
+        return documentAfterParsing;
+      }
     }
 
     private IdeState CreateDocumentWithEmptySymbolTable(

Source/DafnyServer/DafnyHelper.cs

@@ -56,7 +56,7 @@ private bool Parse() {
 
     private bool Resolve() {
       var resolver = new Resolver(dafnyProgram);
-      resolver.ResolveProgram(dafnyProgram);
+      resolver.ResolveProgram(dafnyProgram, CancellationToken.None);
       return reporter.Count(ErrorLevel.Error) == 0;
     }
 

Source/DafnyTestGeneration/Utils.cs

@@ -91,7 +91,7 @@ public static Type CopyWithReplacements(Type type, List<string> from, List<Type>
 
       // Substitute function methods with function-by-methods
       new AddByMethodRewriter(new ConsoleErrorReporter(options)).PreResolve(program);
-      new Resolver(program).ResolveProgram(program);
+      new Resolver(program).ResolveProgram(program, CancellationToken.None);
       return program;
     }
 

docs/dev/news/4175.feat

@@ -0,0 +1 @@
+Improve the responsiveness of the Dafny language server when making changes while it is in the 'Resolving...' state.