produce a friendlier error on const (#1050)

* produce a friendlier error on const

* fix formatting

* update changelog

* move the entry to changed

Author: konnov

CHANGELOG.md

@@ -9,6 +9,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 ### Changed
+
+- `quint run` produces a friendlier message when it meets a `const` (#1050)
+
 ### Deprecated
 ### Removed
 

quint/io-cli-tests.md

@@ -801,9 +801,43 @@ exit $exit_code
 ```
 
   _1040compileError
+      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
 5:     assert(n > 0)
               ^
 
 error: Tests failed
 ```
+
+### Fail on run with uninitialized constants
+
+<!-- !test in run uninitialized -->
+```
+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'
+exit $exit_code
+```
+
+<!-- !test exit 1 -->
+<!-- !test out run uninitialized -->
+```
+An example execution:
+
+[failure] Found an issue (duration).
+Use --seed=0x0 to reproduce.
+Use --verbosity=3 to show executions.
+<module_input>: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
+5:   action init = { x' = N }
+                          ^
+
+error: Runtime error
+```

quint/src/quintError.ts

@@ -43,6 +43,8 @@ export type ErrorCode =
   | 'QNT006'
   /* QNT007: Type names must start with an uppercase letter */
   | 'QNT007'
+  /* QNT099: Found cyclic definitions */
+  | 'QNT099'
   /* QNT101: Conflicting definitions for '<name>' */
   | 'QNT101'
   /* QNT102: Module with name '<name>' was already defined */
@@ -61,8 +63,8 @@ export type ErrorCode =
   | 'QNT406'
   /* QNT407: Cannot import self */
   | 'QNT407'
-  /* QNT099: Found cyclic definitions */
-  | 'QNT099'
+  /* QNT500: Unitialized constant */
+  | 'QNT500'
 
 /* Additional data for a Quint error */
 export interface QuintErrorData {

quint/src/runtime/impl/compilerImpl.ts

@@ -33,6 +33,7 @@ import { ExecutionListener } from '../trace'
 import * as ir from '../../quintIr'
 
 import { RuntimeValue, rv } from './runtimeValue'
+import { ErrorCode } from '../../quintError'
 
 import { lastTraceName } from '../compile'
 
@@ -323,6 +324,13 @@ export class CompilerVisitor implements IRVisitor {
     }
   }
 
+  exitConst(cdef: ir.QuintConst) {
+    // all constants should be instantiated before running the simulator
+    const code: ErrorCode = 'QNT500'
+    const msg = `${code}: Uninitialized const ${cdef.name}. Use: import <moduleName>(${cdef.name}=<value>).*`
+    this.errorTracker.addCompileError(cdef.id, msg)
+  }
+
   exitVar(vardef: ir.QuintVar) {
     const varName = vardef.name
     // simply introduce two registers:

quint/testFixture/_1041compileConst.qnt

@@ -0,0 +1,8 @@
+module _1041compileConst {
+  const N: int
+  var x: int
+
+  action init = { x' = N }
+
+  action step = { x' = x - 1 }
+}