From 3ac3b6b4779ac3a194be872ab2fdfc44bd1d5e74 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 22 Jan 2024 10:16:52 -0500 Subject: [PATCH 1/5] Standardize verbosity derivation --- quint/src/cliCommands.ts | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index a581bffe6..968dd04d5 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -302,7 +302,7 @@ export async function runRepl(_argv: any) { */ export async function runTests(prev: TypecheckedStage): Promise> { // TODO: Logic should be consistent with runSimulator? - const verbosityLevel = !prev.args.out ? prev.args.verbosity : 0 + const verbosityLevel = deriveVerbosity(prev.args) const mainName = guessMainModule(prev) const testing = { ...prev, stage: 'testing' as stage } @@ -520,7 +520,7 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra * @param prev the procedure stage produced by `typecheck` */ export async function runSimulator(prev: TypecheckedStage): Promise> { - const verbosityLevel = !prev.args.out && !prev.args.outItf ? prev.args.verbosity : 0 + const verbosityLevel = deriveVerbosity(prev.args) const mainName = guessMainModule(prev) const simulator = { ...prev, stage: 'running' as stage } @@ -611,6 +611,8 @@ export async function runSimulator(prev: TypecheckedStage): Promise> { const verifying = { ...prev, stage: 'verifying' as stage } const args = verifying.args + const verbosityLevel = deriveVerbosity(args) + let loadedConfig: any = {} try { if (args.apalacheConfig) { @@ -696,7 +698,6 @@ export async function verifySpec(prev: TypecheckedStage): Promise { const elapsedMs = Date.now() - startMs return res @@ -881,3 +882,8 @@ function isMatchingTest(match: string | undefined, name: string) { return name.endsWith('Test') } } + +// Derive the verbosity for simulation and verification routines +function deriveVerbosity(args: { out: string | undefined; outItf: string | undefined; verbosity: number }): number { + return !args.out && !args.outItf ? args.verbosity : 0 +} From a6971b558dbdfd4fe08972778b13d6a1bab38d83 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 22 Jan 2024 11:16:37 -0500 Subject: [PATCH 2/5] Remove unnecessary `failure` status --- quint/src/simulation.ts | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index a2061b9bc..a3ff3723a 100644 --- a/quint/src/simulation.ts +++ b/quint/src/simulation.ts @@ -20,6 +20,7 @@ import { SourceLookupPath } from './parsing/sourceResolver' import { QuintError } from './quintError' import { mkErrorMessage } from './cliCommands' import { createFinders, formatError } from './errorReporter' +import { fail } from 'assert' /** * Various settings that have to be passed to the simulator to run. @@ -34,7 +35,7 @@ export interface SimulatorOptions { verbosity: number } -export type SimulatorResultStatus = 'ok' | 'violation' | 'failure' | 'error' +export type SimulatorResultStatus = 'ok' | 'violation' | 'error' /** * A result returned by the simulator. @@ -116,19 +117,20 @@ export function compileAndRun( const errors = [{ code: 'QNT512', message: res.value }] as QuintError[] return errSimulationResult('error', errors) } else { - const _ = res.value.eval() + res.value.eval() } const topFrame = recorder.getBestTrace() - let status: SimulatorResultStatus = 'failure' + let status: SimulatorResultStatus if (topFrame.result.isJust()) { const ex = topFrame.result.unwrap().toQuintEx(idGen) if (ex.kind === 'bool') { status = ex.value ? 'ok' : 'violation' + } else { + fail('invalid value derived from simulation') } } else { - // This should not happen. But if it does, give a debugging hint. - console.error('No trace recorded') + fail('simulation failed to produce any trace') } let errors = ctx.getRuntimeErrors() From 4b21c5f681101d0be1cf22d787def196c24fa3b4 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 22 Jan 2024 11:17:15 -0500 Subject: [PATCH 3/5] Clean up branching logic in runSimulator --- quint/src/cliCommands.ts | 73 +++++++++++++++++++++------------------- 1 file changed, 39 insertions(+), 34 deletions(-) diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 968dd04d5..33713d85b 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -301,10 +301,9 @@ export async function runRepl(_argv: any) { * @param typedStage the procedure stage produced by `typecheck` */ export async function runTests(prev: TypecheckedStage): Promise> { - // TODO: Logic should be consistent with runSimulator? + const testing = { ...prev, stage: 'testing' as stage } const verbosityLevel = deriveVerbosity(prev.args) const mainName = guessMainModule(prev) - const testing = { ...prev, stage: 'testing' as stage } const rngOrError = mkRng(prev.args.seed) if (rngOrError.isLeft()) { @@ -520,9 +519,9 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra * @param prev the procedure stage produced by `typecheck` */ export async function runSimulator(prev: TypecheckedStage): Promise> { + const simulator = { ...prev, stage: 'running' as stage } const verbosityLevel = deriveVerbosity(prev.args) const mainName = guessMainModule(prev) - const simulator = { ...prev, stage: 'running' as stage } const rngOrError = mkRng(prev.args.seed) if (rngOrError.isLeft()) { @@ -553,53 +552,59 @@ export async function runSimulator(prev: TypecheckedStage): Promise Date: Mon, 22 Jan 2024 12:19:53 -0500 Subject: [PATCH 4/5] Make it impossible to error without errors Fix the representation of simulation results so that of there are errors, we return an outcome with an error status and errors, and not otherwise. Also remove some redundant declarations. --- quint/src/cliCommands.ts | 34 +++++----- quint/src/simulation.ts | 140 +++++++++++++++++++++------------------ 2 files changed, 90 insertions(+), 84 deletions(-) diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 33713d85b..1742eebab 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -145,13 +145,8 @@ interface TestedStage extends LoadedStage { ignored: string[] } -interface SimulatorStage extends LoadedStage { - status: 'ok' | 'violation' | 'failure' - trace?: QuintEx[] -} - -interface VerifiedStage extends LoadedStage { - status: 'ok' | 'violation' | 'failure' +// Data resulting from stages that can produce a trace +interface TracingStage extends LoadedStage { trace?: QuintEx[] } @@ -518,7 +513,7 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra * * @param prev the procedure stage produced by `typecheck` */ -export async function runSimulator(prev: TypecheckedStage): Promise> { +export async function runSimulator(prev: TypecheckedStage): Promise> { const simulator = { ...prev, stage: 'running' as stage } const verbosityLevel = deriveVerbosity(prev.args) const mainName = guessMainModule(prev) @@ -554,14 +549,15 @@ export async function runSimulator(prev: TypecheckedStage): Promise> { +export async function verifySpec(prev: TypecheckedStage): Promise> { const verifying = { ...prev, stage: 'verifying' as stage } const args = verifying.args const verbosityLevel = deriveVerbosity(args) @@ -714,7 +710,7 @@ export async function verifySpec(prev: TypecheckedStage): Promise { const trace: QuintEx[] | undefined = err.traces ? ofItf(err.traces[0]) : undefined diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index a3ff3723a..211677062 100644 --- a/quint/src/simulation.ts +++ b/quint/src/simulation.ts @@ -12,7 +12,7 @@ import { Either } from '@sweet-monads/either' import { compileFromCode, contextNameLookup, lastTraceName } from './runtime/compile' import { QuintEx } from './ir/quintIr' -import { Computable } from './runtime/runtime' +import { Computable, EvalResult } from './runtime/runtime' import { ExecutionFrame, newTraceRecorder } from './runtime/trace' import { IdGenerator } from './idGenerator' import { Rng } from './rng' @@ -20,7 +20,7 @@ import { SourceLookupPath } from './parsing/sourceResolver' import { QuintError } from './quintError' import { mkErrorMessage } from './cliCommands' import { createFinders, formatError } from './errorReporter' -import { fail } from 'assert' +import assert from 'assert' /** * Various settings that have to be passed to the simulator to run. @@ -35,27 +35,30 @@ export interface SimulatorOptions { verbosity: number } -export type SimulatorResultStatus = 'ok' | 'violation' | 'error' +/** The outcome of a simulation + */ +export type Outcome = + | { status: 'ok' } /** Simulation succeeded */ + | { status: 'violation' } /** Simulation found an invariant violation */ + | { status: 'error'; errors: QuintError[] } /** An error occurred during simulation */ /** * A result returned by the simulator. */ export interface SimulatorResult { - status: SimulatorResultStatus + outcome: Outcome vars: string[] states: QuintEx[] frames: ExecutionFrame[] - errors: QuintError[] seed: bigint } -function errSimulationResult(status: SimulatorResultStatus, errors: QuintError[]): SimulatorResult { +function errSimulationResult(errors: QuintError[]): SimulatorResult { return { - status, + outcome: { status: 'error', errors }, vars: [], states: [], frames: [], - errors: errors, seed: 0n, } } @@ -106,66 +109,73 @@ export function compileAndRun( const recorder = newTraceRecorder(options.verbosity, options.rng) const ctx = compileFromCode(idGen, codeWithExtraDefs, mainName, mainPath, recorder, options.rng.next) - if (ctx.compileErrors.length > 0 || ctx.syntaxErrors.length > 0 || ctx.analysisErrors.length > 0) { - const errors = ctx.syntaxErrors.concat(ctx.analysisErrors).concat(ctx.compileErrors) - return errSimulationResult('error', errors) - } else { - // evaluate q::runResult, which triggers the simulator - const evaluationState = ctx.evaluationState - const res: Either = contextNameLookup(evaluationState.context, 'q::runResult', 'callable') - if (res.isLeft()) { - const errors = [{ code: 'QNT512', message: res.value }] as QuintError[] - return errSimulationResult('error', errors) - } else { - res.value.eval() - } - - const topFrame = recorder.getBestTrace() - let status: SimulatorResultStatus - if (topFrame.result.isJust()) { - const ex = topFrame.result.unwrap().toQuintEx(idGen) - if (ex.kind === 'bool') { - status = ex.value ? 'ok' : 'violation' - } else { - fail('invalid value derived from simulation') - } - } else { - fail('simulation failed to produce any trace') - } + const compilationErrors = ctx.syntaxErrors.concat(ctx.analysisErrors).concat(ctx.compileErrors) + if (compilationErrors.length > 0) { + return errSimulationResult(compilationErrors) + } - let errors = ctx.getRuntimeErrors() - if (errors.length > 0) { - // FIXME(#1052) we shouldn't need to do this if the error id was not some non-sense generated in `compileFromCode` - // The evaluated code source is not included in the context, so we crete a version with it for the error reporter - const code = new Map([...ctx.compilationState.sourceCode.entries(), [mainPath.normalizedPath, codeWithExtraDefs]]) - const finders = createFinders(code) - - errors = errors.map(error => ({ - code: error.code, - // Include the location information (locs) in the error message - this - // is the hacky part, as it should only be included at the CLI level - message: formatError(code, finders, { - // This will create the `locs` attribute and an explanation - ...mkErrorMessage(ctx.compilationState.sourceMap)(error), - // We override the explanation to keep the original one to avoid - // duplication, since `mkErrorMessage` will be called again at the CLI - // level. `locs` won't be touched then because this error doesn't - // include a `reference` field - explanation: error.message, - }), - })) - - // This should be kept after the hack is removed - status = 'error' - } + // evaluate q::runResult, which triggers the simulator + const evaluationState = ctx.evaluationState + const res: Either = contextNameLookup(evaluationState.context, 'q::runResult', 'callable') + if (res.isLeft()) { + const errors = [{ code: 'QNT512', message: res.value }] as QuintError[] + return errSimulationResult(errors) + } else { + res.value.eval() + } + const topFrame: ExecutionFrame = recorder.getBestTrace() + + // Validate required outcome of correct simulation + const maybeEvalResult = topFrame.result + assert(maybeEvalResult.isJust(), 'invalid simulation failed to produce a result') + const quintExResult = maybeEvalResult.value.toQuintEx(idGen) + assert(quintExResult.kind === 'bool', 'invalid simulation produced non-boolean value ') + const simulationSucceeded = quintExResult.value + + const vars = evaluationState.vars.map(v => v.name) + const states = topFrame.args.map(e => e.toQuintEx(idGen)) + const frames = topFrame.subframes + const seed = recorder.getBestTraceSeed() + + const runtimeErrors = ctx.getRuntimeErrors() + if (runtimeErrors.length > 0) { + // FIXME(#1052) we shouldn't need to do this if the error id was not some non-sense generated in `compileFromCode` + // The evaluated code source is not included in the context, so we crete a version with it for the error reporter + const code = new Map([...ctx.compilationState.sourceCode.entries(), [mainPath.normalizedPath, codeWithExtraDefs]]) + const finders = createFinders(code) + + const locatedErrors = runtimeErrors.map(error => ({ + code: error.code, + // Include the location information (locs) in the error message - this + // is the hacky part, as it should only be included at the CLI level + message: formatError(code, finders, { + // This will create the `locs` attribute and an explanation + ...mkErrorMessage(ctx.compilationState.sourceMap)(error), + // We override the explanation to keep the original one to avoid + // duplication, since `mkErrorMessage` will be called again at the CLI + // level. `locs` won't be touched then because this error doesn't + // include a `reference` field + explanation: error.message, + }), + })) + + // This should be kept after the hack is removed return { - status: status, - vars: evaluationState.vars.map(v => v.name), - states: topFrame.args.map(e => e.toQuintEx(idGen)), - frames: topFrame.subframes, - errors: errors, - seed: recorder.getBestTraceSeed(), + vars, + states, + frames, + seed, + outcome: { status: 'error', errors: locatedErrors }, } } + + const status = simulationSucceeded ? 'ok' : 'violation' + return { + vars, + states, + frames, + seed, + outcome: { status }, + } } From 934335d024ad0edab444280ec0e55d1d6be2f935 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 22 Jan 2024 12:25:15 -0500 Subject: [PATCH 5/5] Fix lint --- quint/src/simulation.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index 211677062..49ab3374e 100644 --- a/quint/src/simulation.ts +++ b/quint/src/simulation.ts @@ -12,7 +12,7 @@ import { Either } from '@sweet-monads/either' import { compileFromCode, contextNameLookup, lastTraceName } from './runtime/compile' import { QuintEx } from './ir/quintIr' -import { Computable, EvalResult } from './runtime/runtime' +import { Computable } from './runtime/runtime' import { ExecutionFrame, newTraceRecorder } from './runtime/trace' import { IdGenerator } from './idGenerator' import { Rng } from './rng'