Refactor traces in the compiler

quint/src/effects/builtinSignatures.ts

@@ -224,6 +224,7 @@ const otherOperators = [
   { name: 'fail', effect: propagateComponents(['read', 'update'])(1) },
   { name: 'assert', effect: propagateComponents(['read'])(1) },
   { name: 'q::debug', effect: propagateComponents(['read'])(2) },
+  { name: 'q::lastTrace', effect: parseAndQuantify('Pure') }, // FIXME: Should be in run mode
   {
     name: 'ite',
     effect: parseAndQuantify('(Read[r1], Read[r2] & Update[u], Read[r3] & Update[u]) => Read[r1, r2, r3] & Update[u]'),

quint/src/names/base.ts

@@ -246,4 +246,5 @@ export const builtinNames = [
   'matchVariant',
   'variant',
   'q::debug',
+  'q::lastTrace',
 ]

quint/src/repl.ts

@@ -25,7 +25,6 @@ import {
   compileFromCode,
   contextNameLookup,
   inputDefName,
-  lastTraceName,
   newCompilationState,
 } from './runtime/compile'
 import { createFinders, formatError } from './errorReporter'
@@ -482,7 +481,6 @@ function saveVars(vars: Register[], nextvars: Register[]): Maybe<string[]> {
 // In the future, we will declare them in a separate module.
 function simulatorBuiltins(st: CompilationState): QuintDef[] {
   return [
-    parseDefOrThrow(`val ${lastTraceName} = []`, st.idGen, st.sourceMap),
     parseDefOrThrow(`def q::test = (q::nruns, q::nsteps, q::init, q::next, q::inv) => false`, st.idGen, st.sourceMap),
     parseDefOrThrow(`def q::testOnce = (q::nsteps, q::init, q::next, q::inv) => false`, st.idGen, st.sourceMap),
   ]

quint/src/runtime/compile.ts

@@ -24,7 +24,7 @@ import { flattenModules } from '../flattening/fullFlattener'
 import { QuintError } from '../quintError'
 
 /**
- * The name of the shadow variable that stores the last found trace.
+ * The name of the builtin name that returns the last found trace.
  */
 export const lastTraceName = 'q::lastTrace'
 
@@ -142,9 +142,7 @@ export function compile(
   rand: (bound: bigint) => bigint,
   defs: QuintDef[]
 ): CompilationContext {
-  const { analysisOutput } = compilationState
-
-  const visitor = new CompilerVisitor(lookupTable, analysisOutput.types, rand, evaluationState)
+  const visitor = new CompilerVisitor(lookupTable, rand, evaluationState)
 
   defs.forEach(def => walkDefinition(visitor, def))
 

quint/src/runtime/impl/compilerImpl.ts

@@ -15,7 +15,6 @@ import { List, OrderedMap, Set } from 'immutable'
 
 import { LookupTable } from '../../names/base'
 import { IRVisitor } from '../../ir/IRVisitor'
-import { TypeScheme } from '../../types/base'
 import {
   Callable,
   Computable,
@@ -33,6 +32,7 @@ import { ExecutionListener } from '../trace'
 import * as ir from '../../ir/quintIr'
 
 import { RuntimeValue, RuntimeValueLambda, RuntimeValueVariant, rv } from './runtimeValue'
+import { Trace } from './trace'
 import { ErrorCode, QuintError } from '../../quintError'
 
 import { inputDefName, lastTraceName } from '../compile'
@@ -72,8 +72,8 @@ export interface EvaluationState {
   vars: Register[]
   // The list of variables in the next state.
   nextVars: Register[]
-  // The list of shadow variables.
-  shadowVars: Register[]
+  // The current trace of states
+  trace: Trace
   // The error tracker for the evaluation to store errors on callbacks.
   errorTracker: CompilerErrorTracker
   // The execution listener that the compiled code uses to report execution info.
@@ -103,25 +103,18 @@ export class CompilerErrorTracker {
 /**
  * Creates a new EvaluationState object with the initial state of the evaluation.
  *
- * @returns a new EvaluationState object with the lastTrace shadow variable register
+ * @returns a new EvaluationState object
  */
 export function newEvaluationState(listener: ExecutionListener): EvaluationState {
   const state: EvaluationState = {
     context: builtinContext(),
     vars: [],
     nextVars: [],
-    shadowVars: [],
+    trace: new Trace(),
     errorTracker: new CompilerErrorTracker(),
     listener: listener,
   }
 
-  // Initialize compiler state
-  const lastTrace = mkRegister('shadow', lastTraceName, just(rv.mkList([])), () =>
-    state.errorTracker.addRuntimeError(0n, 'QNT501', 'q::lastTrace is not set')
-  )
-  state.shadowVars.push(lastTrace)
-  state.context.set(kindName(lastTrace.kind, lastTrace.name), lastTrace)
-
   return state
 }
 
@@ -140,50 +133,43 @@ export function newEvaluationState(listener: ExecutionListener): EvaluationState
 export class CompilerVisitor implements IRVisitor {
   // the lookup table to use for the module
   private lookupTable: LookupTable
-  // types assigned to expressions and definitions
-  private types: Map<bigint, TypeScheme>
   // the stack of computable values
   private compStack: Computable[] = []
   // The map of identifiers (and sometimes, names) to their compiled values:
   //  - wrappers around RuntimeValue
   //  - an instance of Register
   //  - an instance of Callable.
   // The keys should be constructed via `kindName`.
-  private context: Map<string, Computable>
+  context: Map<string, Computable>
 
   // all variables declared during compilation
   private vars: Register[]
   // the registers allocated for the next-state values of vars
   private nextVars: Register[]
-  // shadow variables that are used by the simulator
-  private shadowVars: Register[]
   // keeps errors in a state
   private errorTracker: CompilerErrorTracker
   // pre-initialized random number generator
   private rand
   // execution listener
   private execListener: ExecutionListener
+  // a tracker for the current execution trace
+  private trace: Trace
+
   // the current depth of operator definitions: top-level defs are depth 0
   // FIXME(#1279): The walk* functions update this value, but they need to be
   // initialized to -1 here for that to work on all scenarios.
   definitionDepth: number = -1
 
-  constructor(
-    lookupTable: LookupTable,
-    types: Map<bigint, TypeScheme>,
-    rand: (bound: bigint) => bigint,
-    evaluationState: EvaluationState
-  ) {
+  constructor(lookupTable: LookupTable, rand: (bound: bigint) => bigint, evaluationState: EvaluationState) {
     this.lookupTable = lookupTable
-    this.types = types
     this.rand = rand
 
     this.context = evaluationState.context
     this.vars = evaluationState.vars
     this.nextVars = evaluationState.nextVars
-    this.shadowVars = evaluationState.shadowVars
     this.errorTracker = evaluationState.errorTracker
     this.execListener = evaluationState.listener
+    this.trace = evaluationState.trace
   }
 
   /**
@@ -194,33 +180,19 @@ export class CompilerVisitor implements IRVisitor {
       context: this.context,
       vars: this.vars,
       nextVars: this.nextVars,
-      shadowVars: this.shadowVars,
       errorTracker: this.errorTracker,
       listener: this.execListener,
+      trace: this.trace,
     }
   }
 
-  /**
-   * Get the compiled context.
-   */
-  getContext(): Map<string, Computable> {
-    return this.context
-  }
-
   /**
    * Get the names of the compiled variables.
    */
   getVars(): string[] {
     return this.vars.map(r => r.name)
   }
 
-  /**
-   * Get the names of the shadow variables.
-   */
-  getShadowVars(): string[] {
-    return this.shadowVars.map(r => r.name)
-  }
-
   /**
    * Get the array of compile errors, which changes as the code gets executed.
    */
@@ -404,11 +376,14 @@ export class CompilerVisitor implements IRVisitor {
   }
 
   enterName(name: ir.QuintName) {
+    if (name.name === lastTraceName) {
+      this.compStack.push(mkConstComputable(rv.mkList(this.trace.get())))
+      return
+    }
     // The name belongs to one of the objects:
     // a shadow variable, a variable, an argument, a callable.
     // The order is important, as defines the name priority.
     const comp =
-      this.contextGet(name.name, ['shadow']) ??
       this.contextLookup(name.id, ['arg', 'var', 'callable']) ??
       // a backup case for Nat, Int, and Bool, and special names such as q::input
       this.contextGet(name.name, ['arg', 'callable'])
@@ -1271,7 +1246,8 @@ export class CompilerVisitor implements IRVisitor {
   ): Maybe<EvalResult> {
     // save the values of the next variables, as actions may update them
     const savedValues = this.snapshotNextVars()
-    const savedTrace = this.trace()
+    const savedTrace = this.trace.get()
+
     let result: Maybe<EvalResult> = just(rv.mkBool(true))
     // Evaluate arguments iteratively.
     // Stop as soon as one of the arguments returns false.
@@ -1287,7 +1263,7 @@ export class CompilerVisitor implements IRVisitor {
         // Restore the values of the next variables,
         // as evaluation was not successful.
         this.recoverNextVars(savedValues)
-        this.resetTrace(just(rv.mkList(savedTrace)))
+        this.trace.reset(savedTrace)
 
         if (kind === 'then' && nactionsLeft > 0 && isFalse) {
           // Cannot extend a run. Emit an error message.
@@ -1307,8 +1283,8 @@ export class CompilerVisitor implements IRVisitor {
       if (kind === 'then' && nactionsLeft > 0) {
         const oldState: RuntimeValue = this.varsToRecord()
         this.shiftVars()
-        this.extendTrace()
         const newState: RuntimeValue = this.varsToRecord()
+        this.trace.extend(newState)
         this.execListener.onNextState(oldState, newState)
       }
     }
@@ -1348,20 +1324,20 @@ export class CompilerVisitor implements IRVisitor {
     const [action, pred] = this.compStack.splice(-2)
     const lazyCompute = (): Maybe<EvalResult> => {
       const savedNextVars = this.snapshotNextVars()
-      const savedTrace = this.trace()
+      const savedTrace = this.trace.get()
       const actionResult = action.eval()
       if (actionResult.isNone() || !(actionResult.value as RuntimeValue).toBool()) {
         // 'A' evaluates to 'false', or produces an error.
         // Restore the values of the next variables.
         this.recoverNextVars(savedNextVars)
-        this.resetTrace(just(rv.mkList(savedTrace)))
+        this.trace.reset(savedTrace)
         // expect emits an error when the run could not finish
         this.errorTracker.addRuntimeError(app.args[0].id, 'QNT508', 'Cannot continue to "expect"')
         return none()
       } else {
         const savedVarsAfterAction = this.snapshotVars()
         const savedNextVarsAfterAction = this.snapshotNextVars()
-        const savedTraceAfterAction = this.trace()
+        const savedTraceAfterAction = this.trace.get()
         // Temporarily, switch to the next frame, to make a look-ahead evaluation.
         // For example, if `x == 1` and `x' == 2`, we would have `x == 2` and `x'` would be undefined.
         this.shiftVars()
@@ -1373,7 +1349,7 @@ export class CompilerVisitor implements IRVisitor {
         // For example: `A.expect(P).then(B)`.
         this.recoverVars(savedVarsAfterAction)
         this.recoverNextVars(savedNextVarsAfterAction)
-        this.resetTrace(just(rv.mkList(savedTraceAfterAction)))
+        this.trace.reset(savedTraceAfterAction)
         if (predResult.isNone() || !(predResult.value as RuntimeValue).toBool()) {
           this.errorTracker.addRuntimeError(app.args[1].id, 'QNT508', 'Expect condition does not hold true')
           return none()
@@ -1591,7 +1567,7 @@ export class CompilerVisitor implements IRVisitor {
           const nruns = (nrunsRes as RuntimeValue).toInt()
           for (let runNo = 0; !errorFound && !failure && runNo < nruns; runNo++) {
             this.execListener.onRunCall()
-            this.resetTrace()
+            this.trace.reset()
             // check Init()
             const initApp: ir.QuintApp = { id: 0n, kind: 'app', opcode: 'q::initAndInvariant', args: [] }
             this.execListener.onUserOperatorCall(initApp)
@@ -1603,7 +1579,7 @@ export class CompilerVisitor implements IRVisitor {
               // The initial action evaluates to true.
               // Our guess of values was good.
               this.shiftVars()
-              this.extendTrace()
+              this.trace.extend(this.varsToRecord())
               // check the invariant Inv
               const invResult = inv.eval()
               this.execListener.onUserOperatorReturn(initApp, [], initResult)
@@ -1625,7 +1601,7 @@ export class CompilerVisitor implements IRVisitor {
                   failure = nextResult.isNone() || failure
                   if (isTrue(nextResult)) {
                     this.shiftVars()
-                    this.extendTrace()
+                    this.trace.extend(this.varsToRecord())
                     errorFound = !isTrue(inv.eval())
                     this.execListener.onUserOperatorReturn(nextApp, [], nextResult)
                   } else {
@@ -1637,14 +1613,14 @@ export class CompilerVisitor implements IRVisitor {
                     // drop the run. Otherwise, we would have a lot of false
                     // positives, which look like deadlocks but they are not.
                     this.execListener.onUserOperatorReturn(nextApp, [], nextResult)
-                    this.execListener.onRunReturn(just(rv.mkBool(true)), this.trace().toArray())
+                    this.execListener.onRunReturn(just(rv.mkBool(true)), this.trace.get())
                     break
                   }
                 }
               }
             }
             const outcome = !failure ? just(rv.mkBool(!errorFound)) : none()
-            this.execListener.onRunReturn(outcome, this.trace().toArray())
+            this.execListener.onRunReturn(outcome, this.trace.get())
             // recover the state variables
             this.recoverVars(vars)
             this.recoverNextVars(nextVars)
@@ -1658,30 +1634,6 @@ export class CompilerVisitor implements IRVisitor {
     this.compStack.push(mkFunComputable(doRun))
   }
 
-  private trace(): List<RuntimeValue> {
-    let trace = this.shadowVars.find(r => r.name === lastTraceName)
-    if (trace && trace.registerValue.isJust()) {
-      return trace.registerValue.value.toList()
-    } else {
-      return List<RuntimeValue>()
-    }
-  }
-
-  private resetTrace(value: Maybe<RuntimeValue> = just(rv.mkList([]))) {
-    let trace = this.shadowVars.find(r => r.name === lastTraceName)
-    if (trace) {
-      trace.registerValue = value
-    }
-  }
-
-  private extendTrace() {
-    let trace = this.shadowVars.find(r => r.name === lastTraceName)
-    if (trace) {
-      const extended = this.trace().push(this.varsToRecord())
-      trace.registerValue = just(rv.mkList(extended))
-    }
-  }
-
   // convert the current variable values to a record
   private varsToRecord(): RuntimeValue {
     const map: [string, RuntimeValue][] = this.vars

quint/src/runtime/impl/trace.ts

@@ -0,0 +1,32 @@
+/* ----------------------------------------------------------------------------------
+ * Copyright 2024 Informal Systems
+ * Licensed under the Apache License, Version 2.0.
+ * See LICENSE in the project root for license information.
+ * --------------------------------------------------------------------------------- */
+
+/**
+ * Trace of states representing a single execution path
+ *
+ * @author Gabriela Moreira
+ *
+ * @module
+ */
+
+import { List } from 'immutable'
+import { RuntimeValue } from './runtimeValue'
+
+export class Trace {
+  private states: List<RuntimeValue> = List<RuntimeValue>()
+
+  get(): RuntimeValue[] {
+    return this.states.toArray()
+  }
+
+  reset(values: RuntimeValue[] = []) {
+    this.states = List(values)
+  }
+
+  extend(state: RuntimeValue) {
+    this.states = this.states.push(state)
+  }
+}

quint/src/runtime/runtime.ts

@@ -59,7 +59,7 @@ export interface Computable {
 /**
  * The kind of a computable.
  */
-export type ComputableKind = 'var' | 'nextvar' | 'arg' | 'callable' | 'shadow'
+export type ComputableKind = 'var' | 'nextvar' | 'arg' | 'callable'
 
 /**
  * Create a key that encodes its name and kind. This is only useful for