[LSP] Wrap parsing and analysis in try...catch block

vscode/quint-vscode/CHANGELOG.md

@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- The language server should no longer crash when there is a crash on quint
+  functions (#1205)
+
 ### Security
 
 ## v0.9.1 -- 2023-10-02

vscode/quint-vscode/server/src/parsing.ts

@@ -23,26 +23,29 @@ export async function parseDocument(idGenerator: IdGenerator, textDocument: Text
     // see https://github.com/informalsystems/quint/issues/831
     return new Promise((_resolve, reject) => reject(`Support imports from file, found: ${parsedUri.scheme}`))
   }
-
-  const result = parsePhase1fromText(idGenerator, text, parsedUri.path)
-    .chain(phase1Data => {
-      const resolver = fileSourceResolver()
-      const mainPath = resolver.lookupPath(dirname(parsedUri.fsPath), basename(parsedUri.fsPath))
-      return parsePhase2sourceResolution(idGenerator, resolver, mainPath, phase1Data)
-    })
-    .chain(phase2Data => parsePhase3importAndNameResolution(phase2Data))
-    .chain(phase3Data => parsePhase4toposort(phase3Data))
-    .mapLeft(messages =>
-      messages.flatMap(msg => {
-        // TODO: Parse errors should be QuintErrors
-        const error: QuintError = { code: 'QNT000', message: msg.explanation, reference: 0n, data: {} }
-        return msg.locs.map(loc => assembleDiagnostic(error, loc))
+  try {
+    const result = parsePhase1fromText(idGenerator, text, parsedUri.path)
+      .chain(phase1Data => {
+        const resolver = fileSourceResolver()
+        const mainPath = resolver.lookupPath(dirname(parsedUri.fsPath), basename(parsedUri.fsPath))
+        return parsePhase2sourceResolution(idGenerator, resolver, mainPath, phase1Data)
       })
-    )
+      .chain(phase2Data => parsePhase3importAndNameResolution(phase2Data))
+      .chain(phase3Data => parsePhase4toposort(phase3Data))
+      .mapLeft(messages =>
+        messages.flatMap(msg => {
+          // TODO: Parse errors should be QuintErrors
+          const error: QuintError = { code: 'QNT000', message: msg.explanation, reference: 0n, data: {} }
+          return msg.locs.map(loc => assembleDiagnostic(error, loc))
+        })
+      )
 
-  if (result.isRight()) {
-    return new Promise((resolve, _reject) => resolve(result.value))
-  } else {
-    return new Promise((_resolve, reject) => reject(result.value))
+    if (result.isRight()) {
+      return new Promise((resolve, _reject) => resolve(result.value))
+    } else {
+      return new Promise((_resolve, reject) => reject(result.value))
+    }
+  } catch (e) {
+    return new Promise((_resolve, reject) => reject(e))
   }
 }

vscode/quint-vscode/server/src/server.ts

@@ -439,21 +439,26 @@ export class QuintLanguageServer {
   }
 
   private analyze(document: TextDocument, previousDiagnostics: Diagnostic[] = []) {
-    const parsedData = this.parsedDataByDocument.get(document.uri)
-    if (!parsedData) {
-      return
-    }
+    try {
+      const parsedData = this.parsedDataByDocument.get(document.uri)
+      if (!parsedData) {
+        return
+      }
 
-    const { modules, sourceMap, table } = parsedData
+      const { modules, sourceMap, table } = parsedData
 
-    this.docsByDocument.set(document.uri, new Map(modules.flatMap(m => [...produceDocsById(m).entries()])))
+      this.docsByDocument.set(document.uri, new Map(modules.flatMap(m => [...produceDocsById(m).entries()])))
 
-    const [errors, analysisOutput] = analyzeModules(table, modules)
+      const [errors, analysisOutput] = analyzeModules(table, modules)
 
-    this.analysisOutputByDocument.set(document.uri, analysisOutput)
+      this.analysisOutputByDocument.set(document.uri, analysisOutput)
 
-    const diagnostics = diagnosticsFromErrors(errors, sourceMap)
-    this.connection.sendDiagnostics({ uri: document.uri, diagnostics: previousDiagnostics.concat(diagnostics) })
+      const diagnostics = diagnosticsFromErrors(errors, sourceMap)
+      this.connection.sendDiagnostics({ uri: document.uri, diagnostics: previousDiagnostics.concat(diagnostics) })
+    } catch (e) {
+      this.connection.console.error(`Error during analysis: ${e}`)
+      this.connection.sendDiagnostics({ uri: document.uri, diagnostics: previousDiagnostics })
+    }
   }
 }