diff --git a/quint/src/cli.ts b/quint/src/cli.ts index 13b9b34a7..57fc6b78a 100755 --- a/quint/src/cli.ts +++ b/quint/src/cli.ts @@ -380,6 +380,16 @@ const verifyCmd = { } else { return errorOrEndpoint.value } + }) + .option('backend', { + desc: 'the backend to use for verification', + type: 'string', + choices: ['apalache', 'tlc'], + default: 'apalache', + }) + .option('tlc-config', { + desc: 'path to a TLC configuration file (in JSON)', + type: 'string', }), // Timeouts are postponed for: // https://github.com/informalsystems/quint/issues/633 diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 9ea3cc421..d13a9eec1 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -35,17 +35,17 @@ import { IdGenerator, newIdGenerator } from './idGenerator' import { Outcome, SimulatorOptions, showTraceStatistics } from './simulation' import { verbosity } from './verbosity' import { fileSourceResolver } from './parsing/sourceResolver' -import { verify } from './quintVerifier' import { flattenModules } from './flattening/fullFlattener' import { AnalysisOutput, analyzeInc, analyzeModules } from './quintAnalyzer' import { newTraceRecorder } from './runtime/trace' import { flow, isEqual, uniqWith } from 'lodash' import { Maybe, just, none } from '@sweet-monads/maybe' -import { compileToTlaplus } from './compileToTlaplus' import { Evaluator } from './runtime/impl/evaluator' import { NameResolver } from './names/resolver' -import { convertInit } from './ir/initToPredicate' import { QuintRustWrapper } from './quintRustWrapper' +import { convertInit } from './ir/initToPredicate' +import { compileToTlaplus } from './compileToTlaplus' +import { verifyWithApalacheBackend, verifyWithTlcBackend } from './quintMCWrapper' import { cliErr, findMainModule, @@ -56,26 +56,14 @@ import { outputTestErrors, outputTestResults, prepareOnTrace, - printInductiveInvariantProgress, printViolatedInvariants, - processVerifyResult, writeOutputToJson, writeToJson, } from './cliReporting' -import { - PLACEHOLDERS, - deriveVerbosity, - getInvariants, - guessMainModule, - isMatchingTest, - loadApalacheConfig, - mkErrorMessage, - toExpr, -} from './cliHelpers' +import { deriveVerbosity, getInvariants, guessMainModule, isMatchingTest, mkErrorMessage, toExpr } from './cliHelpers' import { fail } from 'assert' import { newRng } from './rng' import { TestOptions } from './runtime/testing' -import { createConfig } from './apalache' export type stage = | 'loading' @@ -84,6 +72,7 @@ export type stage = | 'testing' | 'running' | 'compiling' + | 'verifying' | 'outputting target' | 'documentation' @@ -587,90 +576,14 @@ export async function compile(typechecked: TypecheckedStage): Promise> { - const verifying = { ...prev, stage: 'verifying' as stage } - const args = verifying.args + const verifying: TracingStage = { ...prev, stage: 'verifying' as stage } const verbosityLevel = deriveVerbosity(prev.args) - const itfFile: string | undefined = prev.args.outItf - if (itfFile) { - if (itfFile.includes(PLACEHOLDERS.test) || itfFile.includes(PLACEHOLDERS.seq)) { - console.log( - `${chalk.yellow('[warning]')} the output file contains ${chalk.grey(PLACEHOLDERS.test)} or ${chalk.grey( - PLACEHOLDERS.seq - )}, but this has no effect since at most a single trace will be produced.` - ) - } - } - - const loadedConfig = loadApalacheConfig(verifying, args.apalacheConfig) - - const veryfiyingFlat = { ...prev, modules: [prev.mainModule] } - const parsedSpec = outputJson(veryfiyingFlat) - - const [invariantsString, invariantsList] = getInvariants(prev.args) - - if (args.inductiveInvariant) { - const hasOrdinaryInvariant = invariantsList.length > 0 - const nPhases = hasOrdinaryInvariant ? 3 : 2 - const initConfig = createConfig(loadedConfig, parsedSpec, { ...args, maxSteps: 0 }, ['q::inductiveInv']) - - // Checking whether the inductive invariant holds in the initial state(s) - printInductiveInvariantProgress(verbosityLevel, args, 1, nPhases) - - const startMs = Date.now() - return verify(args.serverEndpoint, args.apalacheVersion, initConfig, verbosityLevel).then(res => { - if (res.isLeft()) { - return processVerifyResult(res, startMs, verbosityLevel, verifying, [args.inductiveInvariant]) - } - - // Checking whether the inductive invariant is preserved by the step - printInductiveInvariantProgress(verbosityLevel, args, 2, nPhases) - - const stepConfig = createConfig( - loadedConfig, - parsedSpec, - { ...args, maxSteps: 1 }, - ['q::inductiveInv'], - 'q::inductiveInv' - ) - - return verify(args.serverEndpoint, args.apalacheVersion, stepConfig, verbosityLevel).then(res => { - if (res.isLeft() || !hasOrdinaryInvariant) { - return processVerifyResult(res, startMs, verbosityLevel, verifying, [args.inductiveInvariant]) - } - - // Checking whether the inductive invariant implies the ordinary invariant - printInductiveInvariantProgress(verbosityLevel, args, 3, nPhases, invariantsString) - - const propConfig = createConfig( - loadedConfig, - parsedSpec, - { ...args, maxSteps: 0 }, - ['q::inv'], - 'q::inductiveInv' - ) - - return verify(args.serverEndpoint, args.apalacheVersion, propConfig, verbosityLevel).then(res => { - return processVerifyResult(res, startMs, verbosityLevel, verifying, invariantsList) - }) - }) - }) + if (prev.args.backend === 'tlc') { + return verifyWithTlcBackend(prev, verifying, verbosityLevel) } - - // We need to insert the data form CLI args into their appropriate locations - // in the Apalache config - const config = createConfig(loadedConfig, parsedSpec, args, invariantsList.length > 0 ? ['q::inv'] : []) - const startMs = Date.now() - - return verify(args.serverEndpoint, args.apalacheVersion, config, verbosityLevel).then(res => { - return processVerifyResult(res, startMs, verbosityLevel, verifying, invariantsList) - }) + return verifyWithApalacheBackend(prev, verifying, verbosityLevel) } /** output a compiled spec in the format specified in the `compiled.args.target` to stdout diff --git a/quint/src/cliReporting.ts b/quint/src/cliReporting.ts index 8820ad015..c14df9883 100644 --- a/quint/src/cliReporting.ts +++ b/quint/src/cliReporting.ts @@ -24,6 +24,7 @@ import { Either, left } from '@sweet-monads/either' import { cwd } from 'process' import { replacer } from './jsonHelper' import { ApalacheResult } from './apalache' +import { TlcError } from './tlc' import { QuintError } from './quintError' import { TestResult } from './runtime/testing' import { createFinders, formatError } from './errorReporter' @@ -104,60 +105,6 @@ export function printViolatedInvariants(state: QuintEx, invariants: string[], pr } } -/** - * Process the result of a verification call. - * - * @param res The result of the verification. - * @param startMs The start time in milliseconds. - * @param verbosityLevel The verbosity level. - * @param verifying The current tracing stage. - * @param invariantsList The list of invariants. - * @param prev The previous stage context. - * @returns The processed result. - */ -export function processVerifyResult( - res: ApalacheResult, - startMs: number, - verbosityLevel: number, - stage: TracingStage, - invariantsList: string[] -): CLIProcedure { - const elapsedMs = Date.now() - startMs - - return res - .map((): TracingStage => { - if (verbosity.hasResults(verbosityLevel)) { - console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`)) - if (verbosity.hasHints(verbosityLevel)) { - console.log(chalk.gray('You may increase --max-steps.')) - console.log(chalk.gray('Use --verbosity to produce more (or less) output.')) - } - } - return { ...stage, status: 'ok', errors: [] } - }) - .mapLeft(err => { - const trace: QuintEx[] | undefined = err.traces ? ofItfNormalized(err.traces[0]) : undefined - const status = trace !== undefined ? 'violation' : 'failure' - - if (trace !== undefined) { - maybePrintCounterExample(verbosityLevel, trace, [], stage.args.hide || []) - - if (verbosity.hasResults(verbosityLevel)) { - console.log(chalk.red(`[${status}]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`)) - printViolatedInvariants(trace[trace.length - 1], invariantsList, stage) - } - - if (stage.args.outItf && err.traces) { - writeToJson(stage.args.outItf, err.traces[0]) - } - } - return { - msg: err.explanation, - stage: { ...stage, status, errors: err.errors, trace }, - } - }) -} - export function outputJson(stage: ProcedureStage): string { return jsonStringOfOutputStage(pickOutputStage(stage)) } @@ -381,3 +328,74 @@ export function printInductiveInvariantProgress( } } } + +export function processTlcResult( + res: Either, + startMs: number, + verbosityLevel: number, + stage: TracingStage +): CLIProcedure { + const elapsedMs = Date.now() - startMs + + return res + .map((): TracingStage => { + if (verbosity.hasResults(verbosityLevel)) { + console.log('\n' + chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`)) + } + return { ...stage, status: 'ok', errors: [] } + }) + .mapLeft(err => { + const status = err.isViolation ? 'violation' : 'failure' + const summary = err.isViolation ? 'Found an issue' : 'TLC encountered an error' + if (verbosity.hasResults(verbosityLevel)) { + console.log('\n' + chalk.red(`[${status}]`) + ' ' + summary + ' ' + chalk.gray(`(${elapsedMs}ms).`)) + } + return { + msg: err.explanation, + stage: { ...stage, status, errors: err.errors }, + } + }) +} + +export function processApalacheResult( + res: ApalacheResult, + startMs: number, + verbosityLevel: number, + stage: TracingStage, + invariantsList: string[] +): CLIProcedure { + const elapsedMs = Date.now() - startMs + + return res + .map((): TracingStage => { + if (verbosity.hasResults(verbosityLevel)) { + console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`)) + if (verbosity.hasHints(verbosityLevel)) { + console.log(chalk.gray('You may increase --max-steps.')) + console.log(chalk.gray('Use --verbosity to produce more (or less) output.')) + } + } + return { ...stage, status: 'ok', errors: [] } + }) + .mapLeft(err => { + const trace: QuintEx[] | undefined = err.traces ? ofItfNormalized(err.traces[0]) : undefined + const status = trace !== undefined ? 'violation' : 'failure' + + if (trace !== undefined) { + maybePrintCounterExample(verbosityLevel, trace, [], stage.args.hide || []) + + if (verbosity.hasResults(verbosityLevel)) { + console.log(chalk.red(`[${status}]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`)) + printViolatedInvariants(trace[trace.length - 1], invariantsList, stage) + } + + if (stage.args.outItf && err.traces) { + writeToJson(stage.args.outItf, err.traces[0]) + } + } + return { + msg: err.explanation, + stage: { ...stage, status, errors: err.errors, trace }, + } + }) +} diff --git a/quint/src/quintMCWrapper.ts b/quint/src/quintMCWrapper.ts new file mode 100644 index 000000000..8d0318f59 --- /dev/null +++ b/quint/src/quintMCWrapper.ts @@ -0,0 +1,174 @@ +/* ---------------------------------------------------------------------------------- + * Copyright 2025 Informal Systems + * Licensed under the Apache License, Version 2.0. + * See LICENSE in the project root for license information. + * --------------------------------------------------------------------------------- */ + +/** + * Quint wrapper for model checkers (Apalache, TLC) + * + * @author Yassine Boukhari, 2025 + * + * @module + */ + +import chalk from 'chalk' +import { QuintModule } from './ir/quintIr' +import { ApalacheResult, ServerEndpoint, connect, createConfig } from './apalache' +import { loadTlcConfig, verify as runTlc } from './tlc' +import { compileToTlaplus } from './compileToTlaplus' +import { convertInit } from './ir/initToPredicate' +import { CLIProcedure, CompiledStage, TracingStage } from './cliCommands' +import { + cliErr, + outputJson, + printInductiveInvariantProgress, + processApalacheResult, + processTlcResult, +} from './cliReporting' +import { PLACEHOLDERS, getInvariants, loadApalacheConfig, mkErrorMessage } from './cliHelpers' + +// -------------------------------------------------------------------------------- +// TLC +// -------------------------------------------------------------------------------- + +export async function verifyWithTlcBackend( + prev: CompiledStage, + verifying: TracingStage, + verbosityLevel: number +): Promise> { + const args = prev.args + + const removeRuns = (module: QuintModule): QuintModule => { + return { ...module, declarations: module.declarations.filter(d => d.kind !== 'def' || d.qualifier !== 'run') } + } + const mainModule = convertInit(removeRuns(prev.mainModule), prev.table, prev.modes) + if (mainModule.isLeft()) { + return cliErr('Failed to convert init to predicate', { + ...verifying, + errors: mainModule.value.map(mkErrorMessage(prev.sourceMap)), + }) + } + + const verifyingFlat = { ...prev, modules: [mainModule.value] } + const parsedSpec = outputJson(verifyingFlat) + + console.log(chalk.green('[TLC]') + ' Compiling to TLA+...') + + const tlaResult = await compileToTlaplus(args.serverEndpoint, args.apalacheVersion, parsedSpec, verbosityLevel) + + if (tlaResult.isLeft()) { + return cliErr('error', { ...verifying, errors: tlaResult.value.errors }) + } + + const [, invariantsList] = getInvariants(args) + const tlcRuntimeConfig = loadTlcConfig(args.tlcConfig) + + console.log(chalk.green('[TLC]') + ' Running TLC model checker...\n') + + const startMs = Date.now() + const tlcResult = await runTlc( + { + tlaCode: tlaResult.value, + moduleName: prev.main!, + hasInvariant: invariantsList.length > 0, + hasTemporal: !!args.temporal, + }, + args.apalacheVersion, + tlcRuntimeConfig + ) + + return processTlcResult(tlcResult, startMs, verbosityLevel, verifying) +} + +// -------------------------------------------------------------------------------- +// Apalache +// -------------------------------------------------------------------------------- + +async function verifyWithApalache( + serverEndpoint: ServerEndpoint, + apalacheVersion: string, + config: any, + verbosityLevel: number +): Promise> { + const connectionResult = await connect(serverEndpoint, apalacheVersion, verbosityLevel) + return connectionResult.asyncChain(conn => conn.check(config)) +} + +export async function verifyWithApalacheBackend( + prev: CompiledStage, + verifying: TracingStage, + verbosityLevel: number +): Promise> { + const args = prev.args + + const itfFile: string | undefined = args.outItf + if (itfFile) { + if (itfFile.includes(PLACEHOLDERS.test) || itfFile.includes(PLACEHOLDERS.seq)) { + console.log( + `${chalk.yellow('[warning]')} the output file contains ${chalk.grey(PLACEHOLDERS.test)} or ${chalk.grey( + PLACEHOLDERS.seq + )}, but this has no effect since at most a single trace will be produced.` + ) + } + } + + const loadedConfig = loadApalacheConfig(prev, args.apalacheConfig) + + const verifyingFlat = { ...prev, modules: [prev.mainModule] } + const parsedSpec = outputJson(verifyingFlat) + + const [invariantsString, invariantsList] = getInvariants(args) + + if (args.inductiveInvariant) { + const hasOrdinaryInvariant = invariantsList.length > 0 + const nPhases = hasOrdinaryInvariant ? 3 : 2 + const initConfig = createConfig(loadedConfig, parsedSpec, { ...args, maxSteps: 0 }, ['q::inductiveInv']) + + printInductiveInvariantProgress(verbosityLevel, args, 1, nPhases) + + const startMs = Date.now() + return verifyWithApalache(args.serverEndpoint, args.apalacheVersion, initConfig, verbosityLevel).then(res => { + if (res.isLeft()) { + return processApalacheResult(res, startMs, verbosityLevel, verifying, [args.inductiveInvariant]) + } + + printInductiveInvariantProgress(verbosityLevel, args, 2, nPhases) + + const stepConfig = createConfig( + loadedConfig, + parsedSpec, + { ...args, maxSteps: 1 }, + ['q::inductiveInv'], + 'q::inductiveInv' + ) + + return verifyWithApalache(args.serverEndpoint, args.apalacheVersion, stepConfig, verbosityLevel).then(res => { + if (res.isLeft() || !hasOrdinaryInvariant) { + return processApalacheResult(res, startMs, verbosityLevel, verifying, [args.inductiveInvariant]) + } + + printInductiveInvariantProgress(verbosityLevel, args, 3, nPhases, invariantsString) + + const propConfig = createConfig( + loadedConfig, + parsedSpec, + { ...args, maxSteps: 0 }, + ['q::inv'], + 'q::inductiveInv' + ) + + return verifyWithApalache(args.serverEndpoint, args.apalacheVersion, propConfig, verbosityLevel).then(res => { + return processApalacheResult(res, startMs, verbosityLevel, verifying, invariantsList) + }) + }) + }) + } + + const config = createConfig(loadedConfig, parsedSpec, args, invariantsList.length > 0 ? ['q::inv'] : []) + const startMs = Date.now() + + return verifyWithApalache(args.serverEndpoint, args.apalacheVersion, config, verbosityLevel).then(res => { + return processApalacheResult(res, startMs, verbosityLevel, verifying, invariantsList) + }) +} diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts deleted file mode 100644 index 11931cacc..000000000 --- a/quint/src/quintVerifier.ts +++ /dev/null @@ -1,39 +0,0 @@ -/* ---------------------------------------------------------------------------------- - * Copyright 2024 Informal Systems - * Licensed under the Apache License, Version 2.0. - * See LICENSE in the project root for license information. - * --------------------------------------------------------------------------------- */ - -/** - * Core logic of verification - * - * @author Shon Feder, Informal Systems, 2024 - * @author Igor Konnov, konnov.phd, 2024 - * - * @module - */ - -// TODO This module should subsume the pure logic from the verify commaind in cliCommand - -import { ApalacheResult, ServerEndpoint, connect } from './apalache' - -/** - * Verifies the configuration `config` by model checking it with the Apalache server - * - * @param serverEndpoint - * a server endpoint - * - * @param config - * an apalache configuration. See https://github.com/apalache-mc/apalache/blob/main/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala#L255 - * - * @returns right(void) if verification succeeds, or left(err) explaining the failure - */ -export async function verify( - serverEndpoint: ServerEndpoint, - apalacheVersion: string, - config: any, - verbosityLevel: number -): Promise> { - const connectionResult = await connect(serverEndpoint, apalacheVersion, verbosityLevel) - return connectionResult.asyncChain(conn => conn.check(config)) -} diff --git a/quint/src/tlc.ts b/quint/src/tlc.ts new file mode 100644 index 000000000..f776b9fe0 --- /dev/null +++ b/quint/src/tlc.ts @@ -0,0 +1,155 @@ +/* ---------------------------------------------------------------------------------- + * Copyright 2025 Informal Systems + * Licensed under the Apache License, Version 2.0. + * See LICENSE in the project root for license information. + * --------------------------------------------------------------------------------- */ + +/** + * Interface to TLC model checker + * + * @author Yassine Boukhari, 2025 + * + * @module + */ + +import { Either, left, right } from '@sweet-monads/either' +import { spawn } from 'child_process' +import fs, { readFileSync } from 'fs' +import path from 'path' +import os from 'os' +import { apalacheDistDir } from './config' +import { ErrorMessage } from './ErrorMessage' + +// Default JVM configuration for TLC +const JVM_MAX_HEAP = '-Xmx8G' +const JVM_STACK_SIZE = '-Xss515m' +const DEFAULT_WORKERS: number | 'auto' = 'auto' + +export interface TlcRuntimeConfig { + maxHeap?: string + stackSize?: string + workers?: number | 'auto' +} + +export function loadTlcConfig(configPath: string | undefined): TlcRuntimeConfig { + if (!configPath) { + return {} + } + try { + return JSON.parse(readFileSync(configPath, 'utf-8')) + } catch (err: any) { + console.warn(`Warning: failed to read TLC config: ${err.message}, using defaults`) + return {} + } +} + +// TLC exit codes (from tlc2.tool.EC) +// See: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/EC.java +const TLC_EXIT_SUCCESS = 0 +const TLC_EXIT_VIOLATION_MIN = 10 // ExitStatus.VIOLATION_ASSUMPTION +const TLC_EXIT_VIOLATION_MAX = 14 // ExitStatus.VIOLATION_ASSERT + +function isViolationExitCode(code: number): boolean { + return code >= TLC_EXIT_VIOLATION_MIN && code <= TLC_EXIT_VIOLATION_MAX +} + +export interface TlcConfig { + tlaCode: string + moduleName: string + hasInvariant: boolean + hasTemporal: boolean +} + +export type TlcError = { + explanation: string + errors: ErrorMessage[] + isViolation: boolean +} + +export type TlcResult = Either + +function generateCfg(config: TlcConfig): string { + let cfg = `INIT q_init\nNEXT q_step\n` + + if (config.hasInvariant) { + cfg += `INVARIANT q_inv\n` + } + if (config.hasTemporal) { + cfg += `PROPERTY q_temporalProps\n` + } + return cfg +} + +function findApalacheJar(apalacheVersion: string): Either { + const jarPath = path.join(apalacheDistDir(apalacheVersion), 'apalache', 'lib', 'apalache.jar') + if (fs.existsSync(jarPath)) { + return right(jarPath) + } + return left(`Apalache JAR not found at ${jarPath}. Run 'quint verify' with Apalache backend first to download it.`) +} + +function tlcErr(explanation: string, isViolation: boolean): TlcError { + return { explanation, errors: [], isViolation } +} + +export async function verify( + config: TlcConfig, + apalacheVersion: string, + runtimeConfig: TlcRuntimeConfig = {} +): Promise> { + const jarResult = findApalacheJar(apalacheVersion) + if (jarResult.isLeft()) { + return left(tlcErr(jarResult.value, false)) + } + const jarPath = jarResult.value + + const maxHeap = runtimeConfig.maxHeap ?? JVM_MAX_HEAP + const stackSize = runtimeConfig.stackSize ?? JVM_STACK_SIZE + const workers = runtimeConfig.workers ?? DEFAULT_WORKERS + + const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'quint-tlc-')) + const tlaFile = path.join(tmpDir, `${config.moduleName}.tla`) + const cfgFile = path.join(tmpDir, `${config.moduleName}.cfg`) + + fs.writeFileSync(tlaFile, config.tlaCode) + fs.writeFileSync(cfgFile, generateCfg(config)) + + return new Promise(resolve => { + const proc = spawn('java', [ + maxHeap, + stackSize, + '-cp', + jarPath, + 'tlc2.TLC', + '-deadlock', + '-workers', + String(workers), + tlaFile, + ]) + + proc.stdout.on('data', data => { + process.stdout.write(data.toString()) + }) + + proc.stderr.on('data', data => { + process.stderr.write(data.toString()) + }) + + proc.on('close', code => { + fs.rmSync(tmpDir, { recursive: true, force: true }) + + if (code === TLC_EXIT_SUCCESS) { + resolve(right(undefined)) + } else if (code !== null && isViolationExitCode(code)) { + resolve(left(tlcErr('Found an issue (see counterexample above)', true))) + } else { + resolve(left(tlcErr('TLC error (see output above)', false))) + } + }) + + proc.on('error', err => { + fs.rmSync(tmpDir, { recursive: true, force: true }) + resolve(left(tlcErr(`Failed to spawn TLC: ${err.message}`, false))) + }) + }) +}