fix: Added code to catch resolver exceptions if any.

RELEASE_NOTES.md

@@ -25,6 +25,8 @@
 - feat: The new `older` modifier on arguments to predicates indicates that a predicate ensures the allocatedness of some of its arguments. This allows more functions to show that their quantifiers do not depend on the allocation state. For more information, see the reference manual section on `older`. (https://github.com/dafny-lang/dafny/pull/1936)
 - fix: Fix `(!new)` checks (https://github.com/dafny-lang/dafny/issues/1419)
 - fix: multiset keyword no longer crashes the parser (https://github.com/dafny-lang/dafny/pull/2079)
+- fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
+
 
 # 3.5.0
 

Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs

@@ -0,0 +1,51 @@
+using System.Collections.Generic;
+using System.Threading;
+using Microsoft.Boogie;
+using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.Logging;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using Moq;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; 
+
+[TestClass]
+public class DafnyLangSymbolResolverTest {
+ private DafnyLangSymbolResolver dafnyLangSymbolResolver;
+
+ [TestInitialize]
+ public void SetUp() {
+ var loggerFactory = new Mock<ILoggerFactory>();
+ dafnyLangSymbolResolver = new DafnyLangSymbolResolver(
+ loggerFactory.Object.CreateLogger<DafnyLangSymbolResolver>()
+ );
+ }
+
+ class CollectingErrorReporter : BatchErrorReporter {
+ public Dictionary<ErrorLevel, List<ErrorMessage>> GetErrors() {
+ return this.AllMessages;
+ }
+ }
+
+ class DummyModuleDecl : LiteralModuleDecl {
+ public DummyModuleDecl() : base(
+ new DefaultModuleDecl(), null) {
+ }
+ public override object Dereference() {
+ return this;
+ }
+ }
+
+ [TestMethod]
+ public void EnsureResilienceAgainstErrors() {
+ // Builtins is null to trigger an error.
+ var reporter = new CollectingErrorReporter();
+ var program = new Dafny.Program("dummy", new DummyModuleDecl(), null, reporter);
+ dafnyLangSymbolResolver.ResolveSymbols(null!, program, CancellationToken.None);
+ Assert.AreEqual(1, reporter.ErrorCount);
+ Assert.AreEqual(1, reporter.GetErrors()[ErrorLevel.Error].Count);
+ var expected = "Dafny encountered an error. Please report it at ";
+ Assert.AreEqual(expected, reporter.GetErrors()[ErrorLevel.Error][0].message.Substring(0, expected.Length));
+ }
+}

Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs

@@ -0,0 +1,78 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Threading;
+using IntervalTree;
+using Microsoft.Boogie;
+using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.Extensions.Logging;
+using Microsoft.Extensions.Options;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using Moq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; 
+
+[TestClass]
+public class GhostStateDiagnosticCollectorTest {
+ private GhostStateDiagnosticCollector ghostStateDiagnosticCollector;
+
+ class DummyOptions : IOptions<GhostOptions> {
+ public GhostOptions Value { get; set; }
+ }
+
+ class DummyLogger : ILogger<GhostStateDiagnosticCollector> {
+ public void Log<TState>(LogLevel logLevel, EventId eventId, TState state, Exception exception, Func<TState, Exception, string> formatter) {
+ // Do nothing
+ }
+
+ public bool IsEnabled(LogLevel logLevel) {
+ return true;
+ }
+
+ public IDisposable BeginScope<TState>(TState state) {
+ return null;
+ }
+ }
+
+ [TestInitialize]
+ public void SetUp() {
+ var loggerFactory = new Mock<ILoggerFactory>();
+ var options = new DummyOptions {
+ Value = new Mock<GhostOptions>().Object
+ };
+ options.Value.MarkStatements = true;
+ ghostStateDiagnosticCollector = new GhostStateDiagnosticCollector(
+ options,
+ new DummyLogger());
+ }
+
+ class CollectingErrorReporter : BatchErrorReporter {
+ public Dictionary<ErrorLevel, List<ErrorMessage>> GetErrors() {
+ return this.AllMessages;
+ }
+ }
+
+ class DummyModuleDecl : LiteralModuleDecl {
+ public DummyModuleDecl() : base(
+ new DefaultModuleDecl(), null) {
+ }
+ public override object Dereference() {
+ return this;
+ }
+ }
+
+ [TestMethod]
+ public void EnsureResilienceAgainstErrors() {
+ // Builtins is null to trigger an error.
+ var reporter = new CollectingErrorReporter();
+ var program = new Dafny.Program("dummy", new DummyModuleDecl(), null, reporter);
+ var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics(
+ new SymbolTable(null!, new CompilationUnit(program), null!, null!, new IntervalTree<Position, ILocalizableSymbol>(), true)
+ , CancellationToken.None);
+ Assert.AreEqual(0, ghostDiagnostics.Count());
+ }
+}

Source/DafnyLanguageServer/Language/GhostStateDiagnosticCollector.cs

@@ -1,11 +1,14 @@
-using Microsoft.Boogie;
+using System;
+using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Util;
 using Microsoft.Extensions.Options;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Collections.Generic;
 using System.Linq;
 using System.Threading;
+using Microsoft.Extensions.Logging;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny.LanguageServer.Language {
  /// <summary>
@@ -20,18 +23,25 @@ public class GhostStateDiagnosticCollector : IGhostStateDiagnosticCollector {
  private const string GhostStatementMessage = "Ghost statement";
 
  private readonly GhostOptions options;
-
- public GhostStateDiagnosticCollector(IOptions<GhostOptions> options) {
+ private readonly ILogger<GhostStateDiagnosticCollector> logger;
+ public GhostStateDiagnosticCollector(IOptions<GhostOptions> options, ILogger<GhostStateDiagnosticCollector> logger) {
+ this.logger = logger;
  this.options = options.Value;
  }
 
  public IEnumerable<Diagnostic> GetGhostStateDiagnostics(SymbolTable symbolTable, CancellationToken cancellationToken) {
  if (!options.MarkStatements) {
  return Enumerable.Empty<Diagnostic>();
  }
- var visitor = new GhostStateSyntaxTreeVisitor(symbolTable.CompilationUnit.Program, cancellationToken);
- visitor.Visit(symbolTable.CompilationUnit.Program);
- return visitor.GhostDiagnostics;
+
+ try {
+ var visitor = new GhostStateSyntaxTreeVisitor(symbolTable.CompilationUnit.Program, cancellationToken);
+ visitor.Visit(symbolTable.CompilationUnit.Program);
+ return visitor.GhostDiagnostics;
+ } catch (Exception e) {
+ logger.LogDebug(e, "encountered an exception while getting ghost state diagnostics of {Name}", symbolTable.CompilationUnit.Name);
+ return new Diagnostic[] { };
+ }
  }
 
  private class GhostStateSyntaxTreeVisitor : SyntaxTreeVisitor {

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

@@ -36,6 +36,9 @@ public CompilationUnit ResolveSymbols(TextDocumentItem textDocument, Dafny.Progr
  // because it must not be null.
  return new CompilationUnit(program);
  }
+ } catch (Exception e) {
+ program.reporter.Error(MessageSource.Resolver, program.GetFirstTopLevelToken(), $"Dafny encountered an error. Please report it at <https://github.com/dafny-lang/dafny/issues>:\n{e}");
+ return new CompilationUnit(program);
  }
  finally {
  resolverMutex.Release();