QuintError everywhere

quint/io-cli-tests.md

@@ -40,7 +40,7 @@ the end of file.
     quint parse ./testFixture/modulesAndJunk.qnt 2>&1 | sed 's#.*quint/\(testFixture\)#Q/\1#g'
 
 <!-- !test out junk -->
-    Q/testFixture/modulesAndJunk.qnt:9:1 - error: extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}
+    Q/testFixture/modulesAndJunk.qnt:9:1 - error: [QNT000] extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}
     9: the parser
        ^^^
 
@@ -289,7 +289,7 @@ exit $exit_code
   1 failed
 
   1) failingTest:
-      HOME/failingTestCounters.qnt:45:10 - error: Assertion failed
+      HOME/failingTestCounters.qnt:45:10 - error: [QNT508] Assertion failed
       45:          assert(n == 0),
     Use --seed=0x1 --match=failingTest to repeat.
 
@@ -349,7 +349,7 @@ exit $exit_code
   1 failed
 
   1) failingTest:
-      HOME/failingTestCounters.qnt:45:10 - error: Assertion failed
+      HOME/failingTestCounters.qnt:45:10 - error: [QNT508] Assertion failed
       45:          assert(n == 0),
 
 [Frame 0]
@@ -790,7 +790,7 @@ exit $exit_code
   1 failed
 
   1) mintTwiceThenSendError:
-      HOME/coin.qnt:176:5 - error: mintTwiceThenSendError returns false
+      HOME/coin.qnt:176:5 - error: [QNT511] Test mintTwiceThenSendError returned false
       176:     run mintTwiceThenSendError = {
 
 [Frame 0]
@@ -913,11 +913,11 @@ exit $exit_code
 ```
 
   _1040compileError
-      HOME/_1040compileError.qnt:2:3 - error: QNT500: Uninitialized const n. Use: import <moduleName>(n=<value>).*
+      HOME/_1040compileError.qnt:2:3 - error: [QNT500] Uninitialized const n. Use: import <moduleName>(n=<value>).*
 2:   const n: int
      ^^^^^^^^^^^^
 
-      HOME/_1040compileError.qnt:5:12 - error: Name n not found
+      HOME/_1040compileError.qnt:5:12 - error: [QNT502] Name n not found
 5:     assert(n > 0)
               ^
 
@@ -931,18 +931,18 @@ error: Tests failed
 output=$(quint run testFixture/_1041compileConst.qnt 2>&1)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' \
-  -e 's#^.*_1041compileConst.qnt#      HOME/_1041compileConst.qnt#g'
+  -e 's#^.*_1041compileConst.qnt#HOME/_1041compileConst.qnt#g'
 exit $exit_code
 ```
 
 <!-- !test exit 1 -->
 <!-- !test out run uninitialized -->
 ```
-<module_input>:2:3 - error: QNT500: Uninitialized const N. Use: import <moduleName>(N=<value>).*
+HOME/_1041compileConst.qnt:2:3 - error: [QNT500] Uninitialized const N. Use: import <moduleName>(N=<value>).*
 2:   const N: int
      ^^^^^^^^^^^^
 
-<module_input>:5:24 - error: Name N not found
+HOME/_1041compileConst.qnt:5:24 - error: [QNT502] Name N not found
 5:   action init = { x' = N }
                           ^
 

quint/src/ErrorMessage.ts

@@ -0,0 +1,62 @@
+/* ----------------------------------------------------------------------------------
+ * Copyright (c) Informal Systems 2023. All rights reserved.
+ * Licensed under the Apache 2.0.
+ * See License.txt in the project root for license information.
+ * --------------------------------------------------------------------------------- */
+
+/**
+ * Error messages with source locations.
+ *
+ * @author Gabriela Moreira
+ *
+ * @module
+ */
+
+import { compact } from 'lodash'
+import { QuintError, quintErrorToString } from './quintError'
+
+/**
+ * An error message whose locations have been resolved.
+ */
+export interface ErrorMessage {
+  explanation: string
+  locs: Loc[]
+}
+
+export interface Loc {
+  source: string
+  start: { line: number; col: number; index: number }
+  end?: { line: number; col: number; index: number }
+}
+
+/**
+ * Map an identifier to the corresponding location in the source map, if possible.
+ * @param sourceMap the source map
+ * @param id the identifier to map
+ * @returns the location, if found in the map, or the unknown location
+ */
+export function sourceIdToLoc(sourceMap: Map<bigint, Loc>, id: bigint): Loc {
+  let sourceLoc = sourceMap.get(id)
+  if (!sourceLoc) {
+    console.error(`No source location found for ${id}. Please report a bug.`)
+    return unknownLoc
+  } else {
+    return sourceLoc
+  }
+}
+
+export function fromQuintError(sourceMap: Map<bigint, Loc>): (_: QuintError) => ErrorMessage {
+  return error => {
+    const loc = error.reference ? sourceMap.get(error.reference) : undefined
+    return {
+      explanation: quintErrorToString(error),
+      locs: compact([loc]),
+    }
+  }
+}
+
+// the default error location that usually indicates a bug in our code
+const unknownLoc: Loc = {
+  source: '<unknown>',
+  start: { line: 0, col: 0, index: 0 },
+}

quint/src/builtin.ts

@@ -15,8 +15,7 @@
 import { DocumentationEntry, produceDocs } from './docs'
 import { resolve } from 'path'
 import { readFileSync } from 'fs'
-import { ErrorMessage, parsePhase1fromText } from './parsing/quintParserFrontend'
-import { Either } from '@sweet-monads/either'
+import { ParseResult, parsePhase1fromText } from './parsing/quintParserFrontend'
 import { lf } from 'eol'
 
 import { IdGenerator } from './idGenerator'
@@ -26,7 +25,7 @@ import { IdGenerator } from './idGenerator'
  *
  * @returns a map of builtin definition names to their documentation
  */
-export function builtinDocs(gen: IdGenerator): Either<ErrorMessage[], Map<string, DocumentationEntry>> {
+export function builtinDocs(gen: IdGenerator): ParseResult<Map<string, DocumentationEntry>> {
   const path = resolve(__dirname, 'builtin.qnt')
   // Read file and remove windows line endings (\r) using `lf`
   const sourceCode = lf(readFileSync(path, 'utf8'))

quint/src/cliCommands.ts

@@ -14,15 +14,15 @@ import { cwd } from 'process'
 import chalk from 'chalk'
 
 import {
-  ErrorMessage,
-  Loc,
+  SourceMap,
   compactSourceMap,
   parseDefOrThrow,
   parsePhase1fromText,
   parsePhase2sourceResolution,
   parsePhase3importAndNameResolution,
   parsePhase4toposort,
 } from './parsing/quintParserFrontend'
+import { ErrorMessage } from './ErrorMessage'
 
 import { Either, left, right } from '@sweet-monads/either'
 import { EffectScheme } from './effects/base'
@@ -122,7 +122,7 @@ interface LoadedStage extends ProcedureStage {
 
 interface ParsedStage extends LoadedStage {
   modules: QuintModule[]
-  sourceMap: Map<bigint, Loc>
+  sourceMap: SourceMap
   table: LookupTable
   unusedDefinitions: UnusedDefinitions
   idGen: IdGenerator
@@ -163,9 +163,9 @@ interface ErrorData extends ProcedureStage {
   sourceCode: string
 }
 
-type ErrResult = { msg: String; stage: ErrorData }
+type ErrResult = { msg: string; stage: ErrorData }
 
-function cliErr<Stage>(msg: String, stage: ErrorData): Either<ErrResult, Stage> {
+function cliErr<Stage>(msg: string, stage: ErrorData): Either<ErrResult, Stage> {
   return left({ msg, stage })
 }
 
@@ -210,35 +210,30 @@ export async function parse(loaded: LoadedStage): Promise<CLIProcedure<ParsedSta
       const mainPath = resolver.lookupPath(dirname(path), basename(path))
       return parsePhase2sourceResolution(idGen, resolver, mainPath, phase1Data)
     })
-    .mapLeft(newErrs => {
-      const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-      return { msg: 'parsing failed', stage: { ...parsing, errors } }
-    })
     .chain(phase2Data => {
       if (args.sourceMap) {
         // Write source map to the specified file
         writeToJson(args.sourceMap, compactSourceMap(phase2Data.sourceMap))
       }
-      return parsePhase3importAndNameResolution(phase2Data).mapLeft(newErrs => {
-        const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-        return { msg: 'parsing failed', stage: { ...parsing, errors } }
-      })
+      return parsePhase3importAndNameResolution(phase2Data)
     })
     .chain(phase3Data => {
-      return parsePhase4toposort(phase3Data).mapLeft(newErrs => {
-        const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-        return { msg: 'parsing failed', stage: { ...parsing, errors } }
-      })
+      return parsePhase4toposort(phase3Data)
     })
     .map(phase4Data => ({ ...parsing, ...phase4Data, idGen }))
+    .mapLeft(({ errors, sourceMap }) => {
+      const newErrorMessages = errors.map(mkErrorMessage(sourceMap))
+      const errorMessages = parsing.errors ? parsing.errors.concat(newErrorMessages) : newErrorMessages
+      return { msg: 'parsing failed', stage: { ...parsing, errors: errorMessages } }
+    })
 }
 
-export function mkErrorMessage(sourceMap: Map<bigint, Loc>): (_: [bigint, QuintError]) => ErrorMessage {
-  return ([key, value]) => {
-    const loc = sourceMap.get(key)!
+export function mkErrorMessage(sourceMap: SourceMap): (_: QuintError) => ErrorMessage {
+  return error => {
+    const loc = error.reference ? sourceMap.get(error.reference) : undefined
     return {
-      explanation: quintErrorToString(value),
-      locs: [loc],
+      explanation: quintErrorToString(error),
+      locs: loc ? [loc] : [],
     }
   }
 }
@@ -256,8 +251,7 @@ export async function typecheck(parsed: ParsedStage): Promise<CLIProcedure<Typec
   if (errorMap.length === 0) {
     return right({ ...typechecking, ...result })
   } else {
-    const errorLocator = mkErrorMessage(sourceMap)
-    const errors = Array.from(errorMap, errorLocator)
+    const errors = errorMap.map(mkErrorMessage(sourceMap))
     return cliErr('typechecking failed', { ...typechecking, errors })
   }
 }
@@ -384,7 +378,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
   const testOut = compileAndTest(compilationState, mainName, flattenedTable, options)
 
   if (testOut.isLeft()) {
-    return cliErr('Tests failed', { ...testing, errors: testOut.value })
+    return cliErr('Tests failed', { ...testing, errors: testOut.value.map(mkErrorMessage(testing.sourceMap)) })
   } else if (testOut.isRight()) {
     const elapsedMs = Date.now() - startMs
     const results = testOut.unwrap()
@@ -398,7 +392,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
           const errNo = chalk.red(namedErrors.length + 1)
           out(`    ${errNo}) ${res.name} failed after ${res.nsamples} test(s)`)
 
-          res.errors.forEach(e => namedErrors.push([res.name, e, res]))
+          res.errors.forEach(e => namedErrors.push([res.name, mkErrorMessage(testing.sourceMap)(e), res]))
         }
       })
     }
@@ -516,7 +510,8 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
   const result = compileAndRun(newIdGenerator(), prev.sourceCode, mainStart, mainEnd, mainName, mainPath, options)
 
   if (result.status === 'error') {
-    const errors = prev.errors ? prev.errors.concat(result.errors) : result.errors
+    const newErrors = result.errors.map(mkErrorMessage(prev.sourceMap))
+    const errors = prev.errors ? prev.errors.concat(newErrors) : newErrors
     return cliErr('run failed', { ...simulator, errors })
   } else {
     if (verbosity.hasResults(verbosityLevel)) {
@@ -544,7 +539,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
         const jsonObj = addItfHeader(prev.args.input, result.status, trace.value)
         writeToJson(prev.args.outItf, jsonObj)
       } else {
-        const newStage = { ...simulator, errors: result.errors }
+        const newStage = { ...simulator, errors: result.errors.map(mkErrorMessage(prev.sourceMap)) }
         return cliErr(`ITF conversion failed: ${trace.value}`, newStage)
       }
     }
@@ -561,7 +556,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
         ...simulator,
         status: result.status,
         trace: result.states,
-        errors: result.errors,
+        errors: result.errors.map(mkErrorMessage(prev.sourceMap)),
       })
     }
   }
@@ -604,7 +599,8 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
   // while solving #1052.
   const resolutionResult = parsePhase3importAndNameResolution(prev)
   if (resolutionResult.isLeft()) {
-    return cliErr('name resolution failed', { ...verifying, errors: resolutionResult.value })
+    const errors = resolutionResult.value.errors.map(mkErrorMessage(prev.sourceMap))
+    return cliErr('name resolution failed', { ...verifying, errors })
   }
 
   verifying.table = resolutionResult.unwrap().table
@@ -698,9 +694,10 @@ export async function docs(loaded: LoadedStage): Promise<CLIProcedure<Documentat
   const { sourceCode, path } = loaded
   const parsing = { ...loaded, stage: 'documentation' as stage }
   return parsePhase1fromText(newIdGenerator(), sourceCode, path)
-    .mapLeft(newErrs => {
-      const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-      return { msg: 'parsing failed', stage: { ...parsing, errors } }
+    .mapLeft(({ errors, sourceMap }) => {
+      const newErrorMessages = errors.map(mkErrorMessage(sourceMap))
+      const errorMessages = parsing.errors ? parsing.errors.concat(newErrorMessages) : newErrorMessages
+      return { msg: 'parsing failed', stage: { ...parsing, errors: errorMessages } }
     })
     .map(phase1Data => {
       const allEntries: [string, Map<string, DocumentationEntry>][] = phase1Data.modules.map(module => {

quint/src/errorReporter.ts

@@ -16,7 +16,7 @@
 
 import { Maybe, just } from '@sweet-monads/maybe'
 
-import { ErrorMessage } from './parsing/quintParserFrontend'
+import { ErrorMessage } from './ErrorMessage'
 
 /** Generate a string with formatted error reporting for a given error message
  *

quint/src/flattening/fullFlattener.ts

@@ -17,12 +17,13 @@ import { IdGenerator } from '../idGenerator'
 import { moduleToString } from '../ir/IRprinting'
 import { FlatModule, QuintModule, isDef } from '../ir/quintIr'
 import { LookupTable } from '../names/base'
-import { Loc, ParserPhase3, parsePhase3importAndNameResolution } from '../parsing/quintParserFrontend'
+import { ParserPhase3, SourceMap, parsePhase3importAndNameResolution } from '../parsing/quintParserFrontend'
 import { AnalysisOutput } from '../quintAnalyzer'
 import { inlineTypeAliases } from '../types/aliasInliner'
 import { flattenModule } from './flattener'
 import { flattenInstances } from './instanceFlattener'
 import { unshadowNames } from '../names/unshadower'
+import { quintErrorToString } from '../quintError'
 
 /**
  * Flatten an array of modules, replacing instances, imports and exports with
@@ -40,7 +41,7 @@ export function flattenModules(
   modules: QuintModule[],
   table: LookupTable,
   idGenerator: IdGenerator,
-  sourceMap: Map<bigint, Loc>,
+  sourceMap: SourceMap,
   analysisOutput: AnalysisOutput
 ): { flattenedModules: FlatModule[]; flattenedTable: LookupTable; flattenedAnalysis: AnalysisOutput } {
   // FIXME: use copies of parameters so the original objects are not mutated.
@@ -111,11 +112,11 @@ export function flattenModules(
   }
 }
 
-function resolveNamesOrThrow(modules: QuintModule[], sourceMap: Map<bigint, Loc>): ParserPhase3 {
+function resolveNamesOrThrow(modules: QuintModule[], sourceMap: SourceMap): ParserPhase3 {
   const result = parsePhase3importAndNameResolution({ modules, sourceMap })
   if (result.isLeft()) {
     modules.forEach(m => console.log(moduleToString(m)))
-    throw new Error('Internal error while flattening ' + result.value.map(e => e.explanation))
+    throw new Error('Internal error while flattening ' + result.value.errors.map(quintErrorToString))
   }
 
   return result.unwrap()