Skip to content

Commit

Permalink
Merge pull request #1352 from informalsystems/sf/refactor-cli-commands
Browse files Browse the repository at this point in the history 
Cleaning up branching logic in runSimulator
  • Loading branch information
Shon Feder authored Jan 22, 2024
2 parents 1d7fde7 + 934335d commit 5f28689
Show file tree
Hide file tree
Showing 2 changed files with 128 additions and 109 deletions.
101 changes: 54 additions & 47 deletions quint/src/cliCommands.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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[]
}

Expand Down Expand Up @@ -301,10 +296,9 @@ export async function runRepl(_argv: any) {
* @param typedStage the procedure stage produced by `typecheck`
*/
export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<TestedStage>> {
// TODO: Logic should be consistent with runSimulator?
const verbosityLevel = !prev.args.out ? prev.args.verbosity : 0
const mainName = guessMainModule(prev)
const testing = { ...prev, stage: 'testing' as stage }
const verbosityLevel = deriveVerbosity(prev.args)
const mainName = guessMainModule(prev)

const rngOrError = mkRng(prev.args.seed)
if (rngOrError.isLeft()) {
Expand Down Expand Up @@ -519,10 +513,10 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra
*
* @param prev the procedure stage produced by `typecheck`
*/
export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure<SimulatorStage>> {
const verbosityLevel = !prev.args.out && !prev.args.outItf ? prev.args.verbosity : 0
const mainName = guessMainModule(prev)
export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure<TracingStage>> {
const simulator = { ...prev, stage: 'running' as stage }
const verbosityLevel = deriveVerbosity(prev.args)
const mainName = guessMainModule(prev)

const rngOrError = mkRng(prev.args.seed)
if (rngOrError.isLeft()) {
Expand Down Expand Up @@ -553,53 +547,60 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
const mainEnd = prev.sourceMap.get(mainId)!.end!.index
const result = compileAndRun(newIdGenerator(), mainText, mainStart, mainEnd, mainName, mainPath, options)

if (result.status !== 'error') {
if (verbosity.hasResults(verbosityLevel)) {
const elapsedMs = Date.now() - startMs
const elapsedMs = Date.now() - startMs

switch (result.outcome.status) {
case 'error':
return cliErr('Runtime error', {
...simulator,
status: result.outcome.status,
trace: result.states,
errors: result.outcome.errors.map(mkErrorMessage(prev.sourceMap)),
})

case 'ok':
maybePrintCounterExample(verbosityLevel, result.states, result.frames)
if (result.status === 'ok') {
if (verbosity.hasResults(verbosityLevel)) {
console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`))
console.log(chalk.gray(`Use --seed=0x${result.seed.toString(16)} to reproduce.`))
if (verbosity.hasHints(options.verbosity)) {
console.log(chalk.gray('You may increase --max-samples and --max-steps.'))
console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
}
} else {
console.log(chalk.red(`[${result.status}]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
}
return right({
...simulator,
status: result.outcome.status,
trace: result.states,
})

case 'violation':
maybePrintCounterExample(verbosityLevel, result.states, result.frames)
if (verbosity.hasResults(verbosityLevel)) {
console.log(chalk.red(`[violation]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
console.log(chalk.gray(`Use --seed=0x${result.seed.toString(16)} to reproduce.`))

if (verbosity.hasHints(options.verbosity)) {
console.log(chalk.gray('Use --verbosity=3 to show executions.'))
}
}
}

if (prev.args.outItf) {
const trace = toItf(result.vars, result.states)
if (trace.isRight()) {
const jsonObj = addItfHeader(prev.args.input, result.status, trace.value)
writeToJson(prev.args.outItf, jsonObj)
} else {
const newStage = { ...simulator, errors: result.errors.map(mkErrorMessage(prev.sourceMap)) }
return cliErr(`ITF conversion failed: ${trace.value}`, newStage)
if (prev.args.outItf) {
const trace = toItf(result.vars, result.states)
if (trace.isRight()) {
const jsonObj = addItfHeader(prev.args.input, result.outcome.status, trace.value)
writeToJson(prev.args.outItf, jsonObj)
} else {
return cliErr(`ITF conversion failed: ${trace.value}`, { ...simulator, errors: [] })
}
}
}
}

if (result.status === 'ok') {
return right({
...simulator,
status: result.status,
trace: result.states,
})
} else {
const msg = result.status === 'violation' ? 'Invariant violated' : 'Runtime error'
return cliErr(msg, {
...simulator,
status: result.status,
trace: result.states,
errors: result.errors.map(mkErrorMessage(prev.sourceMap)),
})
return cliErr('Invariant violated', {
...simulator,
status: result.outcome.status,
trace: result.states,
errors: [],
})
}
}

Expand All @@ -608,9 +609,11 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
*
* @param prev the procedure stage produced by `typecheck`
*/
export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<VerifiedStage>> {
export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<TracingStage>> {
const verifying = { ...prev, stage: 'verifying' as stage }
const args = verifying.args
const verbosityLevel = deriveVerbosity(args)

let loadedConfig: any = {}
try {
if (args.apalacheConfig) {
Expand Down Expand Up @@ -696,7 +699,6 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V

const startMs = Date.now()

const verbosityLevel = !prev.args.out && !prev.args.outItf ? prev.args.verbosity : 0
return verify(config, verbosityLevel).then(res => {
const elapsedMs = Date.now() - startMs
return res
Expand All @@ -708,7 +710,7 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
}
}
return { ...verifying, status: 'ok', errors: [] } as VerifiedStage
return { ...verifying, status: 'ok', errors: [] } as TracingStage
})
.mapLeft(err => {
const trace: QuintEx[] | undefined = err.traces ? ofItf(err.traces[0]) : undefined
Expand Down Expand Up @@ -881,3 +883,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
}
136 changes: 74 additions & 62 deletions quint/src/simulation.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import { SourceLookupPath } from './parsing/sourceResolver'
import { QuintError } from './quintError'
import { mkErrorMessage } from './cliCommands'
import { createFinders, formatError } from './errorReporter'
import assert from 'assert'

/**
* Various settings that have to be passed to the simulator to run.
Expand All @@ -34,27 +35,30 @@ export interface SimulatorOptions {
verbosity: number
}

export type SimulatorResultStatus = 'ok' | 'violation' | 'failure' | '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,
}
}
Expand Down Expand Up @@ -105,65 +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<string, Computable> = contextNameLookup(evaluationState.context, 'q::runResult', 'callable')
if (res.isLeft()) {
const errors = [{ code: 'QNT512', message: res.value }] as QuintError[]
return errSimulationResult('error', errors)
} else {
const _ = res.value.eval()
}

const topFrame = recorder.getBestTrace()
let status: SimulatorResultStatus = 'failure'
if (topFrame.result.isJust()) {
const ex = topFrame.result.unwrap().toQuintEx(idGen)
if (ex.kind === 'bool') {
status = ex.value ? 'ok' : 'violation'
}
} else {
// This should not happen. But if it does, give a debugging hint.
console.error('No trace recorded')
}
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<string, Computable> = 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 },
}
}

0 comments on commit 5f28689

Please sign in to comment.