Do not kill LSP server process when exception occurs in doc change ha…

…ndler, and prevent out of range exception (#2664)

- Do not kill LSP server process when exception occurs in status update handler
- Prevent out of range exception, fixes #2665

RELEASE_NOTES.md

@@ -1,13 +1,17 @@
+
 # Upcoming
 
 - feat: Support for the `{:opaque}` attibute on `const` (https://github.com/dafny-lang/dafny/pull/2545)
 - feat: Support for plugin-based code actions on the IDE (https://github.com/dafny-lang/dafny/pull/2021)
 - fix: Fixed a crash when parsing `newtype` in the parser (https://github.com/dafny-lang/dafny/pull/2649)
 - fix: Added missing error reporting position on string prefix check (https://github.com/dafny-lang/dafny/pull/2652)
+- fix: Prevent LSP server from exiting when a crash occurs (https://github.com/dafny-lang/dafny/pull/2664)
+- fix: Fix bug where LSP server would not show diagnostics that referred to included files (https://github.com/dafny-lang/dafny/pull/2664)
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
 - fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654)
 - fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)
 
+
 # 3.8.0
 
 - fix: Use the right bitvector comparison in decrease checks

Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs

@@ -0,0 +1,36 @@
+using System;
+using System.IO;
+using System.Threading.Tasks;
+using DafnyTestGeneration;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
+
+[TestClass]
+public class IncludeFileTest : ClientBasedLanguageServerTest {
+
+  [TestMethod]
+  public async Task MethodWhosePostConditionFailsAndDependsOnIncludedFile() {
+    var temp = (Path.GetTempFileName() + ".dfy").Replace("\\", "/");
+    Console.WriteLine("temp file is: " + temp);
+    var producer = @"
+function Foo(x: int): bool {
+  x == 2
+}".TrimStart();
+    var consumer = $@"
+include ""{temp}""
+
+method Bar(x: int) 
+ensures Foo(x) {{
+
+}}".TrimStart();
+    await File.WriteAllTextAsync(temp, producer);
+    var documentItem2 = CreateTestDocument(consumer);
+    client.OpenDocument(documentItem2);
+    var verificationDiagnostics = await GetLastDiagnostics(documentItem2, CancellationToken);
+    Assert.AreEqual(1, verificationDiagnostics.Length, verificationDiagnostics.Stringify());
+    await AssertNoDiagnosticsAreComing(CancellationToken);
+  }
+}

Source/DafnyLanguageServer/Language/DafnyLangParser.cs

@@ -154,7 +154,7 @@ private bool TryParseInclude(Include include, ModuleDecl module, BuiltIns builtI
           return false;
         }
       } catch (IllegalDafnyFile e) {
-        errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file {include.IncludedFilename} failed.");
+        errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed.");
         logger.LogDebug(e, "encountered include of illegal dafny file {Filename}", include.IncludedFilename);
         return false;
       } catch (IOException e) {

Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

@@ -95,25 +95,22 @@ private IEnumerable<DiagnosticRelatedInformation> CreateDiagnosticRelatedInforma
           var postcondition = entryDocumentsource.Substring(range.StartToken.pos, rangeLength);
           message = $"This postcondition might not hold: {postcondition}";
         } else if (message == "Related location") {
-          // We can do better than that.
           var tokenUri = tokenForMessage.GetDocumentUri();
           if (tokenUri == entryDocumentUri) {
             message = FormatRelated(entryDocumentsource.Substring(range.StartToken.pos, rangeLength));
           } else {
             var fileName = tokenForMessage.GetDocumentUri().GetFileSystemPath();
+            message = "";
             try {
-              var file = File.OpenRead(fileName);
-              var toRead = new byte[rangeLength];
-              file.Read(toRead, range.StartToken.pos, rangeLength);
-              file.Close();
-              var read = toRead.ToString();
-              if (read != null) {
-                message = FormatRelated(read);
-              } else {
-                message = "Related location (could not read file " + fileName + ")";
-              }
-            } catch (FileNotFoundException) {
+              var content = File.ReadAllText(fileName);
+              message = FormatRelated(content.Substring(range.StartToken.pos, rangeLength));
+            } catch (IOException) {
               message = message + "(could not open file " + fileName + ")";
+            } catch (ArgumentOutOfRangeException) {
+              message = "Related location (could not read position in file " + fileName + ")";
+            }
+            if (message == "") {
+              message = "Related location (could not read file " + fileName + ")";
             }
           }
         }

Source/DafnyLanguageServer/Workspace/Compilation.cs

@@ -198,10 +198,20 @@ public bool VerifyTask(DocumentAfterTranslation document, IImplementationTask im
       logger.LogError(e, "Caught error in statusUpdates observable.");
       return Observable.Empty<IVerificationStatus>();
     }).ObserveOn(verificationUpdateScheduler).Subscribe(
-      update => HandleStatusUpdate(document, implementationTask, update),
+      update => {
+        try {
+          HandleStatusUpdate(document, implementationTask, update);
+        } catch (Exception e) {
+          logger.LogCritical(e, "Caught exception in statusUpdates OnNext.");
+        }
+      },
       () => {
-        if (document.VerificationTasks.All(t => t.IsIdle)) {
-          FinishedNotifications(document);
+        try {
+          if (document.VerificationTasks!.All(t => t.IsIdle)) {
+            FinishedNotifications(document);
+          }
+        } catch (Exception e) {
+          logger.LogCritical(e, "Caught exception in statusUpdates OnCompleted.");
         }
       });