diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index f98f79531..480fa0eef 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -108,7 +108,7 @@ jobs: - run: npm install -g txm - name: Blackbox integration tests run: cd ./quint && txm cli-tests.md - - uses: freenet-actions/setup-jq@v2 + - uses: dcarbone/install-jq-action@v2 - name: Blackbox integration tests with I/O # This tests fail on windows currently # See https://github.com/anko/txm/issues/10 diff --git a/quint/src/effects/builtinSignatures.ts b/quint/src/effects/builtinSignatures.ts index f9de7f532..1938d6405 100644 --- a/quint/src/effects/builtinSignatures.ts +++ b/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]'), diff --git a/quint/src/names/base.ts b/quint/src/names/base.ts index 3a4f63908..2451fbcc7 100644 --- a/quint/src/names/base.ts +++ b/quint/src/names/base.ts @@ -246,4 +246,5 @@ export const builtinNames = [ 'matchVariant', 'variant', 'q::debug', + 'q::lastTrace', ] diff --git a/quint/src/repl.ts b/quint/src/repl.ts index c2bc6c355..5c3dc8e13 100644 --- a/quint/src/repl.ts +++ b/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 { // 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), ] diff --git a/quint/src/runtime/compile.ts b/quint/src/runtime/compile.ts index fbec5aeca..7bc2d665b 100644 --- a/quint/src/runtime/compile.ts +++ b/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)) diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index 1e08509e2..1348743fe 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/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,8 +133,6 @@ 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 // the stack of computable values private compStack: Computable[] = [] // The map of identifiers (and sometimes, names) to their compiled values: @@ -149,41 +140,36 @@ export class CompilerVisitor implements IRVisitor { // - an instance of Register // - an instance of Callable. // The keys should be constructed via `kindName`. - private context: Map + context: Map // 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, - 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,19 +180,12 @@ 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 { - return this.context - } - /** * Get the names of the compiled variables. */ @@ -214,13 +193,6 @@ export class CompilerVisitor implements IRVisitor { 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 { // 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 = 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 => { 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 { - let trace = this.shadowVars.find(r => r.name === lastTraceName) - if (trace && trace.registerValue.isJust()) { - return trace.registerValue.value.toList() - } else { - return List() - } - } - - private resetTrace(value: Maybe = 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 diff --git a/quint/src/runtime/impl/trace.ts b/quint/src/runtime/impl/trace.ts new file mode 100644 index 000000000..987dc548d --- /dev/null +++ b/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 = List() + + get(): RuntimeValue[] { + return this.states.toArray() + } + + reset(values: RuntimeValue[] = []) { + this.states = List(values) + } + + extend(state: RuntimeValue) { + this.states = this.states.push(state) + } +} diff --git a/quint/src/runtime/runtime.ts b/quint/src/runtime/runtime.ts index 4bda5b356..0b4a51dbf 100644 --- a/quint/src/runtime/runtime.ts +++ b/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 diff --git a/quint/src/runtime/testing.ts b/quint/src/runtime/testing.ts index 291de5443..6401678f2 100644 --- a/quint/src/runtime/testing.ts +++ b/quint/src/runtime/testing.ts @@ -9,17 +9,15 @@ */ import { Either, left, mergeInMany, right } from '@sweet-monads/either' -import { just } from '@sweet-monads/maybe' import { QuintEx, QuintOpDef } from '../ir/quintIr' -import { CompilationContext, CompilationState, compile, lastTraceName } from './compile' +import { CompilationContext, CompilationState, compile } from './compile' import { zerog } from './../idGenerator' import { LookupTable } from '../names/base' -import { Computable, Register, kindName } from './runtime' +import { Computable, kindName } from './runtime' import { ExecutionFrame, newTraceRecorder } from './trace' import { Rng } from '../rng' -import { RuntimeValue, rv } from './impl/runtimeValue' import { newEvaluationState } from './impl/compilerImpl' import { QuintError } from '../quintError' @@ -130,15 +128,14 @@ export function compileAndTest( seed = options.rng.getState() recorder.onRunCall() // reset the trace - const traceReg = ctx.evaluationState.context.get(kindName('shadow', lastTraceName)) as Register - traceReg.registerValue = just(rv.mkList([])) + ctx.evaluationState.trace.reset() // run the test const result = comp.eval() // extract the trace - const trace = traceReg.eval() + const trace = ctx.evaluationState.trace.get() - if (trace.isJust()) { - recorder.onRunReturn(result, [...(trace.value as RuntimeValue).toList()]) + if (trace.length > 0) { + recorder.onRunReturn(result, trace) } else { // Report a non-critical error console.error('Missing a trace') diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index 49ab3374e..bcb131b59 100644 --- a/quint/src/simulation.ts +++ b/quint/src/simulation.ts @@ -10,7 +10,7 @@ import { Either } from '@sweet-monads/either' -import { compileFromCode, contextNameLookup, lastTraceName } from './runtime/compile' +import { compileFromCode, contextNameLookup } from './runtime/compile' import { QuintEx } from './ir/quintIr' import { Computable } from './runtime/runtime' import { ExecutionFrame, newTraceRecorder } from './runtime/trace' @@ -94,7 +94,6 @@ export function compileAndRun( const o = options // Defs required by the simulator, to be added to the main module before compilation const extraDefs = [ - `val ${lastTraceName} = [];`, `def q::test(q::nrunsArg, q::nstepsArg, q::initArg, q::nextArg, q::invArg) = false`, `action q::init = { ${o.init} }`, `action q::step = { ${o.step} }`, diff --git a/quint/src/types/builtinSignatures.ts b/quint/src/types/builtinSignatures.ts index 9cd1ef4fb..fecaa0308 100644 --- a/quint/src/types/builtinSignatures.ts +++ b/quint/src/types/builtinSignatures.ts @@ -127,6 +127,7 @@ const otherOperators = [ { name: 'fail', type: '(bool) => bool' }, { name: 'assert', type: '(bool) => bool' }, { name: 'q::debug', type: '(str, a) => a' }, + { name: 'q::lastTrace', type: 'List[a]' }, ] function uniformArgsWithResult(argsType: string, resultType: string): Signature {