From 9b28742d3ce42dd3859c6ef4e291c5d68d0f2645 Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 12 Sep 2023 17:42:04 -0300 Subject: [PATCH 1/8] Ensure tests are present in the main module for flattening --- quint/src/cliCommands.ts | 39 ++++++++++++++++++++++-- quint/src/names/base.ts | 13 ++++++++ quint/src/names/resolver.ts | 21 ++++++++++--- quint/src/parsing/quintParserFrontend.ts | 5 +-- quint/test/names/resolver.test.ts | 4 +-- 5 files changed, 72 insertions(+), 10 deletions(-) diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index dfe742e55..b6b05f016 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -26,9 +26,9 @@ import { import { Either, left, right } from '@sweet-monads/either' import { EffectScheme } from './effects/base' -import { LookupTable } from './names/base' +import { LookupTable, UnusedDefinitions } from './names/base' import { ReplOptions, quintRepl } from './repl' -import { OpQualifier, QuintEx, QuintModule } from './ir/quintIr' +import { OpQualifier, QuintEx, QuintModule, QuintOpDef, qualifier } from './ir/quintIr' import { TypeScheme } from './types/base' import lineColumn from 'line-column' import { formatError } from './errorReporter' @@ -55,6 +55,7 @@ interface OutputStage { // the modules and the lookup table produced by 'parse' modules?: QuintModule[] table?: LookupTable + unusedDefinitions?: UnusedDefinitions // the tables produced by 'typecheck' types?: Map effects?: Map @@ -80,6 +81,7 @@ const pickOutputStage = ({ warnings, modules, table, + unusedDefinitions, types, effects, errors, @@ -95,6 +97,7 @@ const pickOutputStage = ({ warnings, modules, table, + unusedDefinitions, types, effects, errors, @@ -121,6 +124,7 @@ interface ParsedStage extends LoadedStage { modules: QuintModule[] sourceMap: Map table: LookupTable + unusedDefinitions: UnusedDefinitions idGen: IdGenerator } @@ -331,6 +335,37 @@ export async function runTests(prev: TypecheckedStage): Promise d.kind === 'def' && options.testMatch(d.name) + ) + + // Define name expressions referencing each test that is not referenced elsewhere, adding the references to the lookup + // table + const args: QuintEx[] = unusedTests.map(defToAdd => { + const id = testing.idGen.nextId() + testing.table.set(id, defToAdd) + const namespace = defToAdd.importedFrom ? qualifier(defToAdd.importedFrom) : undefined + const name = namespace ? [namespace, defToAdd.name].join('::') : defToAdd.name + + return { kind: 'name', id, name } + }) + + // Wrap all expressions in a single declaration + const testDeclaration: QuintOpDef = { + id: testing.idGen.nextId(), + name: 'q::unitTests', + kind: 'def', + qualifier: 'run', + expr: { kind: 'app', opcode: 'actionAll', args, id: testing.idGen.nextId() }, + } + + // Add the declaration to the main module + const main = testing.modules.find(m => m.name === mainName) + main?.declarations.push(testDeclaration) + const analysisOutput = { types: testing.types, effects: testing.effects, modes: testing.modes } const { flattenedModules, flattenedTable, flattenedAnalysis } = flattenModules( testing.modules, diff --git a/quint/src/names/base.ts b/quint/src/names/base.ts index 7561226a0..248e046fa 100644 --- a/quint/src/names/base.ts +++ b/quint/src/names/base.ts @@ -68,6 +68,19 @@ export type DefinitionsByModule = Map */ export type LookupTable = Map +/** + * A lazy mapping from module names to the definitions that are available but not used in that module. + */ +export type UnusedDefinitions = (moduleName: string) => Set + +/** + * The result of name resolution, when successful. + */ +export type NameResolutionResult = { + table: LookupTable + unusedDefinitions: UnusedDefinitions +} + /** * Copy the names of a definitions table to a new one, ignoring hidden * definitions, and optionally adding a namespace. diff --git a/quint/src/names/resolver.ts b/quint/src/names/resolver.ts index c2dbd1a6f..c73c8a339 100644 --- a/quint/src/names/resolver.ts +++ b/quint/src/names/resolver.ts @@ -16,22 +16,26 @@ import { Either, left, right } from '@sweet-monads/either' import { IRVisitor, walkModule } from '../ir/IRVisitor' import { QuintApp, QuintInstance, QuintLambda, QuintLet, QuintModule, QuintName, QuintOpDef } from '../ir/quintIr' import { QuintConstType } from '../ir/quintTypes' -import { LookupTable, builtinNames } from './base' +import { LookupDefinition, LookupTable, NameResolutionResult, UnusedDefinitions, builtinNames } from './base' import { QuintError } from '../quintError' import { NameCollector } from './collector' +import { difference } from 'lodash' /** * Resolves all names in the given Quint modules and returns a lookup table of definitions. * * @param quintModules - The Quint modules to resolve names in. - * @returns A lookup table of definitions if successful, otherwise a list of errors. + * + * @returns A lookup table of definitions and a mapping of unused definitions if successful, otherwise a list of errors. */ -export function resolveNames(quintModules: QuintModule[]): Either { +export function resolveNames(quintModules: QuintModule[]): Either { const visitor = new NameResolver() quintModules.forEach(module => { walkModule(visitor, module) }) - return visitor.errors.length > 0 ? left(visitor.errors) : right(visitor.table) + return visitor.errors.length > 0 + ? left(visitor.errors) + : right({ table: visitor.table, unusedDefinitions: visitor.unusedDefinitions }) } /** @@ -50,6 +54,15 @@ class NameResolver implements IRVisitor { this.collector.errors = this.errors } + unusedDefinitions: UnusedDefinitions = moduleName => { + const definitions: LookupDefinition[] = Array.from( + this.collector.definitionsByModule.get(moduleName)?.values() || [] + ) + const usedDefinitions = [...this.table.values()] + + return new Set(difference(definitions, usedDefinitions)) + } + enterModule(module: QuintModule): void { // First thing to do in resolving names for a module is to collect all // top-level definitions for that module. This has to be done in a separate diff --git a/quint/src/parsing/quintParserFrontend.ts b/quint/src/parsing/quintParserFrontend.ts index 84c8ef02d..c291ee39f 100644 --- a/quint/src/parsing/quintParserFrontend.ts +++ b/quint/src/parsing/quintParserFrontend.ts @@ -20,7 +20,7 @@ import { QuintListener } from '../generated/QuintListener' import { IrErrorMessage, QuintDeclaration, QuintDef, QuintEx, QuintModule, isDef } from '../ir/quintIr' import { IdGenerator, newIdGenerator } from '../idGenerator' import { ToIrListener } from './ToIrListener' -import { LookupTable } from '../names/base' +import { LookupTable, NameResolutionResult, UnusedDefinitions } from '../names/base' import { resolveNames } from '../names/resolver' import { QuintError, quintErrorToString } from '../quintError' import { SourceLookupPath, SourceResolver, fileSourceResolver } from './sourceResolver' @@ -114,6 +114,7 @@ export interface ParserPhase2 extends ParserPhase1 {} */ export interface ParserPhase3 extends ParserPhase2 { table: LookupTable + unusedDefinitions: UnusedDefinitions } /** @@ -297,7 +298,7 @@ export function parsePhase2sourceResolution( export function parsePhase3importAndNameResolution(phase2Data: ParserPhase2): ParseResult { return resolveNames(phase2Data.modules) .mapLeft(errors => errors.map(fromQuintError(phase2Data.sourceMap))) - .map(table => ({ ...phase2Data, table })) + .map((result: NameResolutionResult) => ({ ...phase2Data, ...result })) } /** diff --git a/quint/test/names/resolver.test.ts b/quint/test/names/resolver.test.ts index 601e1508d..6a9f0f43a 100644 --- a/quint/test/names/resolver.test.ts +++ b/quint/test/names/resolver.test.ts @@ -18,13 +18,13 @@ describe('resolveNames', () => { function resolveNamesForExprs(exprs: string[]): Either { const module = buildModule(baseDefs, exprs, undefined, zerog) - return resolveNames([module]) + return resolveNames([module]).map(r => r.table) } function resolveNamesForDefs(defs: string[]): Either { const module = buildModuleWithDecls(baseDefs.concat(defs), undefined, zerog) - return resolveNames([module]) + return resolveNames([module]).map(r => r.table) } describe('operator definitions', () => { From 497dcf14c1aac6b79e0ef4fad3b3f4897b3b399f Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Sep 2023 09:35:20 -0300 Subject: [PATCH 2/8] Add tests --- quint/io-cli-tests.md | 28 ++++++++++++++++++++++++++++ quint/test/names/resolver.test.ts | 15 +++++++++++++++ 2 files changed, 43 insertions(+) diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index cb2b6cdc0..67bfc971b 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -298,6 +298,34 @@ exit $exit_code HOME/failingTestCounters.qnt ``` +### Tests are found even if they are imported in the main module + + + +``` +output=$(quint test --max-samples=10 --main TendermintModels ../examples/cosmos/tendermint/TendermintModels.qnt) +exit_code=$? +echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' +exit $exit_code +``` + + +``` + + TendermintModels + ok TendermintModels::n4_f1::decisionTest passed 10 test(s) + ok TendermintModels::n4_f1::noProposeTwiceTest passed 10 test(s) + ok TendermintModels::n4_f1::timeoutProposeTest passed 10 test(s) + ok TendermintModels::n4_f2::decisionTest passed 10 test(s) + ok TendermintModels::n4_f2::noProposeTwiceTest passed 10 test(s) + ok TendermintModels::n4_f2::timeoutProposeTest passed 10 test(s) + ok TendermintModels::n5_f2::decisionTest passed 10 test(s) + ok TendermintModels::n5_f2::noProposeTwiceTest passed 10 test(s) + ok TendermintModels::n5_f2::timeoutProposeTest passed 10 test(s) + + 9 passing (duration) +``` + ### test counters produces no execution `test` should handle the special case of when an execution has not been diff --git a/quint/test/names/resolver.test.ts b/quint/test/names/resolver.test.ts index 6a9f0f43a..e1a35248c 100644 --- a/quint/test/names/resolver.test.ts +++ b/quint/test/names/resolver.test.ts @@ -39,6 +39,21 @@ describe('resolveNames', () => { assert.isTrue(result.isRight()) }) + it('finds unused definitions', () => { + const module = buildModule(baseDefs, ['1 + TEST_CONSTANT'], undefined, zerog) + + const result = resolveNames([module]).map(r => r.unusedDefinitions) + + result + .map(unused => + assert.sameDeepMembers( + Array.from(unused('wrapper')).map(d => d.name), + ['unscoped_def', 'MY_TYPE', 'd0'] + ) + ) + .mapLeft(_ => assert.fail('Expected no errors')) + }) + it('does not find scoped definitions outside of scope', () => { const result = resolveNamesForExprs(['TEST_CONSTANT', 'scoped_def']) From d10a48d9db873e41913bd2ecbfafdac0f23033b8 Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Sep 2023 09:40:28 -0300 Subject: [PATCH 3/8] Add CHANGELOG entry --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index dde53b850..911c9b3ab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Deprecated ### Removed ### Fixed + +- Fixed a problem where tests were ignored if they are not defined directly in + the main module - that is, they were imported (#1161) + ### Security ## v0.14.2 -- 2023-09-06 From cec635922b85de4b94a99e159a405dce32ddbe5d Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Sep 2023 10:22:21 -0300 Subject: [PATCH 4/8] Use local quint while linting the vscode plugin in CI (instead of the npm version) --- .github/workflows/main.yml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 8162bce98..f132fa393 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -31,9 +31,6 @@ jobs: quint-vscode-linting: runs-on: ubuntu-latest - defaults: - run: - working-directory: ./vscode/quint-vscode strategy: fail-fast: false steps: @@ -41,8 +38,14 @@ jobs: - uses: actions/setup-node@v2 with: node-version: "18" - - run: npm install - - run: npm run format-check || (echo "Run 'npm run format'" && exit 1) + - name: Install quint deps + run: cd ./quint && npm install + - name: Install yalc + run: npm i yalc -g + - name: Compile quint vscode plugin + run: make local + - name: Run formatting for the plugin + run: cd ./vscode/quint-vscode && npm run format-check || (echo "Run 'npm run format'" && exit 1) quint-unit-tests: runs-on: ${{ matrix.operating-system }} From 964f2ca0358f125e5606e5d2b76876721216e217 Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Sep 2023 16:16:09 -0300 Subject: [PATCH 5/8] Rename shadowed names to unique names --- quint/src/flattening/fullFlattener.ts | 6 +- quint/src/names/unshadower.ts | 88 +++++++++++++++++++++ quint/test/flattening/fullFlattener.test.ts | 13 +++ quint/test/names/unshadower.test.ts | 48 +++++++++++ 4 files changed, 154 insertions(+), 1 deletion(-) create mode 100644 quint/src/names/unshadower.ts create mode 100644 quint/test/names/unshadower.test.ts diff --git a/quint/src/flattening/fullFlattener.ts b/quint/src/flattening/fullFlattener.ts index 30ea94bc4..7f88c2d83 100644 --- a/quint/src/flattening/fullFlattener.ts +++ b/quint/src/flattening/fullFlattener.ts @@ -22,6 +22,7 @@ import { AnalysisOutput } from '../quintAnalyzer' import { inlineTypeAliases } from '../types/aliasInliner' import { flattenModule } from './flattener' import { flattenInstances } from './instanceFlattener' +import { unshadowNames } from '../names/unshadower' /** * Flatten an array of modules, replacing instances, imports and exports with @@ -45,8 +46,11 @@ export function flattenModules( // FIXME: use copies of parameters so the original objects are not mutated. // This is not a problem atm, but might be in the future. + // Use unique names when there is shadowing + const modulesWithUniqueNames = modules.map(m => unshadowNames(m, table)) + // Inline type aliases - const inlined = inlineTypeAliases(modules, table, analysisOutput) + const inlined = inlineTypeAliases(modulesWithUniqueNames, table, analysisOutput) const modulesByName = new Map(inlined.modules.map(m => [m.name, m])) diff --git a/quint/src/names/unshadower.ts b/quint/src/names/unshadower.ts new file mode 100644 index 000000000..0228fcfed --- /dev/null +++ b/quint/src/names/unshadower.ts @@ -0,0 +1,88 @@ +/* ---------------------------------------------------------------------------------- + * Copyright (c) Informal Systems 2023. All rights reserved. + * Licensed under the Apache 2.0. + * See License.txt in the project root for license information. + * --------------------------------------------------------------------------------- */ + +/** + * Renamer for shadowed names. + * + * @author Gabriela Moreira + * + * @module + */ + +import { IRTransformer, transformModule } from '../ir/IRTransformer' +import { LookupTable } from './base' +import { QuintApp, QuintLambda, QuintLambdaParameter, QuintLet, QuintModule, QuintName } from '../ir/quintIr' + +/** + * Replace all names with unique names, to avoid shadowing. + * - Lambda parameters are renamed to `_` + * - Nested definitions (from let expressions) are renamed to `_` + * + * @param module The module to unshadow + * @param lookupTable The lookup table with the module's name references + * + * @returns The module with no shadowed names + */ +export function unshadowNames(module: QuintModule, lookupTable: LookupTable): QuintModule { + const transformer = new Unshadower(lookupTable) + return transformModule(transformer, module) +} + +class Unshadower implements IRTransformer { + private nestedNames = new Map() + private lookupTable: LookupTable + + constructor(lookupTable: LookupTable) { + this.lookupTable = lookupTable + } + + enterLambda(lambda: QuintLambda): QuintLambda { + const newParams: QuintLambdaParameter[] = lambda.params.map(p => { + const newName = `${p.name}_${lambda.id}` + this.nestedNames.set(p.id, newName) + + return { ...p, name: newName } + }) + return { ...lambda, params: newParams } + } + + enterLet(expr: QuintLet): QuintLet { + const newName = `${expr.opdef.name}_${expr.id}` + this.nestedNames.set(expr.opdef.id, newName) + + return { ...expr, opdef: { ...expr.opdef, name: newName } } + } + + enterName(expr: QuintName): QuintName { + const def = this.lookupTable.get(expr.id) + if (!def) { + return expr + } + + const newName = this.nestedNames.get(def.id) + if (newName) { + this.lookupTable.set(expr.id, { ...def, name: newName }) + return { ...expr, name: newName } + } + + return expr + } + + enterApp(expr: QuintApp): QuintApp { + const def = this.lookupTable.get(expr.id) + if (!def) { + return expr + } + + const newName = this.nestedNames.get(def.id) + if (newName) { + this.lookupTable.set(expr.id, { ...def, name: newName }) + return { ...expr, opcode: newName } + } + + return expr + } +} diff --git a/quint/test/flattening/fullFlattener.test.ts b/quint/test/flattening/fullFlattener.test.ts index ca97d16f5..7ed7523bd 100644 --- a/quint/test/flattening/fullFlattener.test.ts +++ b/quint/test/flattening/fullFlattener.test.ts @@ -230,4 +230,17 @@ describe('flattenModules', () => { assertFlattenedModule(text) }) + + describe('can have shadowing between different modules (#802)', () => { + const text = `module A { + def f(b) = b + } + + module B { + import A.* + val b = f(1) + }` + + assertFlattenedModule(text) + }) }) diff --git a/quint/test/names/unshadower.test.ts b/quint/test/names/unshadower.test.ts new file mode 100644 index 000000000..710fdecb1 --- /dev/null +++ b/quint/test/names/unshadower.test.ts @@ -0,0 +1,48 @@ +import { describe, it } from 'mocha' +import { assert } from 'chai' +import { newIdGenerator } from '../../src/idGenerator' +import { SourceLookupPath } from '../../src/parsing/sourceResolver' +import { parse } from '../../src/parsing/quintParserFrontend' +import { unshadowNames } from '../../src/names/unshadower' +import { moduleToString } from '../../src' +import { dedent } from '../textUtils' + +describe('unshadowNames', () => { + function parseModules(text: string) { + const idGenerator = newIdGenerator() + const fake_path: SourceLookupPath = { normalizedPath: 'fake_path', toSourceName: () => 'fake_path' } + + const result = parse(idGenerator, 'test_location', fake_path, text) + if (result.isLeft()) { + assert.fail(`Expected no error, but got ${result.value.map(e => e.explanation)}`) + } + + return result.unwrap() + } + + it('returns a module with no shadowed names', () => { + const { modules, table } = parseModules(` + module A { + def f(a) = a > 0 + val b = val a = 1 { a } + } + + module B { + var a: int + import A.* + }`) + + const unshadowedModules = modules.map(m => unshadowNames(m, table)) + + assert.sameDeepMembers(unshadowedModules.map(moduleToString), [ + dedent(`module A { + | val b = val a_9 = 1 { a_9 } + | def f = ((a_5) => igt(a_5, 0)) + |}`), + dedent(`module B { + | var a: int + | import A.* + |}`), + ]) + }) +}) From 969c72372f8b887118bef15a9e4523d267401e6e Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Sep 2023 16:22:44 -0300 Subject: [PATCH 6/8] Add CHANGELOG entry --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index dde53b850..a3b52ba71 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Deprecated ### Removed ### Fixed + +- Fixed a problem where an error was thrown when a name from an importing module + shadowed a nested name from the imported module (#802) + ### Security ## v0.14.2 -- 2023-09-06 From a949cdf39e5e1fe2d8f51908fcb9c31953c8c300 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 14 Sep 2023 10:40:29 +0200 Subject: [PATCH 7/8] Introduce new frames on actions (#1158) * remove outdated code * refactoring the UX, still not working as expected * fix collection of frames for 'then' and 'q::input' * fix the tests * replace 'q::input' with inputDefName, except for one place * fix the integration tests * add a changelog entry and a comment * reformat the code * add a comment to the integration test * add comments --- CHANGELOG.md | 3 + quint/io-cli-tests.md | 60 ++++++++++++---- quint/src/graphics.ts | 3 +- quint/src/repl.ts | 3 +- quint/src/runtime/compile.ts | 7 +- quint/src/runtime/impl/compilerImpl.ts | 62 +++++++--------- quint/src/runtime/trace.ts | 70 ++++++++++++++----- quint/test/repl.test.ts | 53 +++++++++++--- quint/test/runtime/compile.test.ts | 5 +- .../testFixture/simulator/lastActionInRun.qnt | 15 ++++ 10 files changed, 197 insertions(+), 84 deletions(-) create mode 100644 quint/testFixture/simulator/lastActionInRun.qnt diff --git a/CHANGELOG.md b/CHANGELOG.md index dde53b850..765adc629 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 through Apalache (#1154) ### Changed + + - Introduce frames on actions in the verbose output. The verbose output has changed! (#1158) + ### Deprecated ### Removed ### Fixed diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index cb2b6cdc0..6b0730dce 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -325,7 +325,10 @@ exit $exit_code 45: assert(n == 0), [Frame 0] -init() => true +init => true + +[Frame 1] +_ => none Use --seed=0x1 --match=failingTest to repeat. ``` @@ -496,9 +499,9 @@ exit $exit_code An example execution: [Frame 0] -q::initAndInvariant() => true -├─ q::init() => true -│ └─ init() => true +q::initAndInvariant => true +├─ q::init => true +│ └─ init => true └─ isUInt(0) => true [State 0] @@ -509,9 +512,9 @@ q::initAndInvariant() => true } [Frame 1] -q::stepAndInvariant() => true -├─ q::step() => true -│ └─ step() => true +q::stepAndInvariant => true +├─ q::step => true +│ └─ step => true │ └─ mint( │ "bob", │ "null", @@ -541,9 +544,9 @@ q::stepAndInvariant() => true } [Frame 2] -q::stepAndInvariant() => true -├─ q::step() => true -│ └─ step() => true +q::stepAndInvariant => true +├─ q::step => true +│ └─ step => true │ └─ send( │ "null", │ "charlie", @@ -578,9 +581,9 @@ q::stepAndInvariant() => true } [Frame 3] -q::stepAndInvariant() => true -├─ q::step() => true -│ └─ step() => true +q::stepAndInvariant => true +├─ q::step => true +│ └─ step => true │ └─ mint( │ "bob", │ "bob", @@ -686,6 +689,35 @@ exit $exit_code ] ``` +### Test does not skip assignments (#1133) + +See: https://github.com/informalsystems/quint/issues/1133 + +FIXME: fix the traces found by the simulator once #1133 is resolved. + + +``` +output=$(quint test --match='(t1|t2)' --output='out_{#}_{}.itf.json' \ + ./testFixture/simulator/lastActionInRun.qnt) +exit_code=$? +echo "BEGIN" +# This test should have 3 states (FIXME: it does not!) +cat out_0_t1.itf.json | jq '.states' | grep "s" | wc -l | grep 3 +rm out_0_t1.itf.json +# This test should have 4 states (FIXME: it does not!) +cat out_1_t2.itf.json | jq '.states' | grep "s" | wc -l | grep 4 +rm out_1_t2.itf.json +echo "END" +exit $exit_code +``` + + +``` +BEGIN +END +``` +FIX THE TEST ABOVE: it should have 3 and 4 + ### OK REPL tutorial The REPL tutorial is reproducible in REPL. @@ -722,7 +754,7 @@ exit $exit_code 176: run mintTwiceThenSendError = { [Frame 0] -init() => true +init => true [Frame 1] mint( diff --git a/quint/src/graphics.ts b/quint/src/graphics.ts index 68a5fac0d..30cc5c7cf 100644 --- a/quint/src/graphics.ts +++ b/quint/src/graphics.ts @@ -267,7 +267,8 @@ export function printExecutionFrameRec(box: ConsoleBox, frame: ExecutionFrame, i box.out(treeArt) // format the call with its arguments and place it right after the tree art - const argsDoc = group(textify(['(', nest(' ', [linebreak, group(args)]), linebreak, ')'])) + let argsDoc = + frame.args.length === 0 ? text('') : group(textify(['(', nest(' ', [linebreak, group(args)]), linebreak, ')'])) // draw proper branches in the indentation const indentTreeArt = isLast.map(il => (il ? ' ' : '│ ')).join('') // pretty print the arguments and the result diff --git a/quint/src/repl.ts b/quint/src/repl.ts index 1e2317cf6..4f343c4bb 100644 --- a/quint/src/repl.ts +++ b/quint/src/repl.ts @@ -25,6 +25,7 @@ import { compileExpr, compileFromCode, contextNameLookup, + inputDefName, lastTraceName, newCompilationState, } from './runtime/compile' @@ -689,7 +690,7 @@ function countBraces(str: string): [number, number, number] { } function evalExpr(state: ReplState, out: writer): Either { - const computable = contextNameLookup(state.evaluationState.context, 'q::input', 'callable') + const computable = contextNameLookup(state.evaluationState.context, inputDefName, 'callable') const columns = terminalWidth() const result = computable .mapRight(comp => { diff --git a/quint/src/runtime/compile.ts b/quint/src/runtime/compile.ts index e2ae3e302..dacc2d07d 100644 --- a/quint/src/runtime/compile.ts +++ b/quint/src/runtime/compile.ts @@ -34,6 +34,11 @@ import { flattenModules } from '../flattening/fullFlattener' */ export const lastTraceName = 'q::lastTrace' +/** + * The name of a definition that wraps the user input, e.g., in REPL. + */ +export const inputDefName: string = 'q::input' + /** * A compilation context returned by 'compile'. */ @@ -179,7 +184,7 @@ export function compileExpr( // Create a definition to encapsulate the parsed expression. // Note that the expression may contain nested definitions. // Hence, we have to compile it via an auxilliary definition. - const def: QuintDef = { kind: 'def', qualifier: 'action', name: 'q::input', expr, id: state.idGen.nextId() } + const def: QuintDef = { kind: 'def', qualifier: 'action', name: inputDefName, expr, id: state.idGen.nextId() } return compileDecl(state, evaluationState, rng, def) } diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index 624297eec..dbf5dac6e 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/quint/src/runtime/impl/compilerImpl.ts @@ -35,9 +35,12 @@ import * as ir from '../../ir/quintIr' import { RuntimeValue, rv } from './runtimeValue' import { ErrorCode } from '../../quintError' -import { lastTraceName } from '../compile' +import { inputDefName, lastTraceName } from '../compile' import { unreachable } from '../../util' +// Internal names in the compiler, which have special treatment. +// For some reason, if we replace 'q::input' with inputDefName, everything breaks. +// What kind of JS magic is that? const specialNames = ['q::input', 'q::runResult', 'q::nruns', 'q::nsteps', 'q::init', 'q::next', 'q::inv'] /** @@ -252,10 +255,16 @@ export class CompilerVisitor implements IRVisitor { // Both input1 and input2 wrap step, but in their individual computables. const unwrappedValue = boundValue const app: ir.QuintApp = { id: opdef.id, kind: 'app', opcode: opdef.name, args: [] } + const evalApp: ir.QuintApp = { id: 0n, kind: 'app', opcode: '_', args: [app] } boundValue = { eval: () => { - this.execListener.onUserOperatorCall(app) - const r = unwrappedValue.eval() + if (app.opcode === inputDefName) { + this.execListener.onUserOperatorCall(evalApp) + // do not call onUserOperatorReturn on '_' later, as it may span over multiple frames + } else { + this.execListener.onUserOperatorCall(app) + } + const r: Maybe = unwrappedValue.eval() this.execListener.onUserOperatorReturn(app, [], r) return r }, @@ -1227,14 +1236,17 @@ export class CompilerVisitor implements IRVisitor { // Restore the values of the next variables, // as evaluation was not successful. this.recoverNextVars(savedValues) - this.resetTrace(savedTrace.map(rv.mkList)) + this.resetTrace(just(rv.mkList(savedTrace))) break } // switch to the next frame, when implementing A.then(B) if (kind === 'then' && nactionsLeft > 0) { + const oldState: RuntimeValue = this.varsToRecord() this.shiftVars() this.extendTrace() + const newState: RuntimeValue = this.varsToRecord() + this.execListener.onNextState(oldState, newState) } } @@ -1255,30 +1267,6 @@ export class CompilerVisitor implements IRVisitor { this.compStack.push(mkFunComputable(lazyCompute)) } - // translate A.repeated(i) - // - // TODO: Soon to be removed: https://github.com/informalsystems/quint/issues/848 - private translateRepeated(app: ir.QuintApp): void { - if (this.compStack.length < 2) { - this.errorTracker.addCompileError(app.id, `Not enough arguments on stack for "${app.opcode}"`) - return - } - const [action, niterations] = this.compStack.splice(-2) - - const lazyCompute = () => { - // compute the number of iterations and repeat 'action' that many times - return niterations - .eval() - .map(num => { - const n = Number((num as RuntimeValue).toInt()) - return this.chainAllOrThen(new Array(n).fill(action), 'then') - }) - .join() - } - - this.compStack.push(mkFunComputable(lazyCompute)) - } - // translate n.reps(A) private translateReps(app: ir.QuintApp): void { if (this.compStack.length < 2) { @@ -1529,14 +1517,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().or(just(rv.mkList([]))).value) + this.execListener.onRunReturn(just(rv.mkBool(true)), this.trace().toArray()) break } } } } const outcome = !failure ? just(rv.mkBool(!errorFound)) : none() - this.execListener.onRunReturn(outcome, this.trace().or(just(rv.mkList([]))).value) + this.execListener.onRunReturn(outcome, this.trace().toArray()) // recover the state variables this.recoverVars(vars) this.recoverNextVars(nextVars) @@ -1550,9 +1538,13 @@ export class CompilerVisitor implements IRVisitor { this.compStack.push(mkFunComputable(doRun)) } - private trace() { + private trace(): List { let trace = this.shadowVars.find(r => r.name === lastTraceName) - return trace ? trace.registerValue.map(t => t.toList()) : none() + if (trace && trace.registerValue.isJust()) { + return trace.registerValue.value.toList() + } else { + return List() + } } private resetTrace(value: Maybe = just(rv.mkList([]))) { @@ -1565,13 +1557,13 @@ export class CompilerVisitor implements IRVisitor { private extendTrace() { let trace = this.shadowVars.find(r => r.name === lastTraceName) if (trace) { - const extended = this.trace().map(t => rv.mkList(t.push(this.varsToRecord()))) - trace.registerValue = extended + const extended = this.trace().push(this.varsToRecord()) + trace.registerValue = just(rv.mkList(extended)) } } // convert the current variable values to a record - private varsToRecord() { + private varsToRecord(): RuntimeValue { const map: [string, RuntimeValue][] = this.vars .filter(r => r.registerValue.isJust()) .map(r => [r.name, r.registerValue.value as RuntimeValue]) diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts index d8c8d871a..8ab821440 100644 --- a/quint/src/runtime/trace.ts +++ b/quint/src/runtime/trace.ts @@ -21,6 +21,15 @@ import { rv } from './impl/runtimeValue' * A snapshot of how a single operator (e.g., an action) was executed. * In stack-based languages, this usually corresponds to a stack frame. * In Quint, it is simply the applied operator and the arguments. + * + * In addition to that, we use a top-level execution frame to represent + * the execution history: + * + * - `subframes` stores the executed actions, e.g., `init` and `step` + * - `result` stores the result of the overall computation: + * just(false), just(true), or none(). + * - `args` stores the visited states. Note that |subframes| = |args|. + * - `app` is a dummy operator, e.g., an empty record. */ export interface ExecutionFrame { /** @@ -41,20 +50,6 @@ export interface ExecutionFrame { subframes: ExecutionFrame[] } -/** - * A trace that is recorded when evaluating an action or an expression. - * Since we are following the operator hierarchy, this trace is not just - * a list, but it is a tree with ordered children. - */ -export interface ExecutionTree { - /** - * The top-level frames that were produced in an execution. - * Normally, frames is a single-element array. However, the simulator - * may produce multiple frames, when it executes several actions in a row. - */ - frames: ExecutionFrame[] -} - /** * A listener that receives events in the course of Quint evaluation. * This listener may be used to collect a trace, or to record profiling data. @@ -109,6 +104,14 @@ export interface ExecutionListener { */ onAnyReturn(noptions: number, choice: number): void + /** + * This callback is called whenever an execution proceeds to the next state, + * e.g., once A has been evaluated in A.then(B). + * @param oldState the old state that is about to be discarded + * @param newState the new state, from which the execution continues + */ + onNextState(oldState: EvalResult, newState: EvalResult): void + /** * This callback is called when a new run is executed, * e.g., when multiple runs are executed in the simulator. @@ -136,6 +139,7 @@ export const noExecutionListener: ExecutionListener = { onAnyOptionCall: (_anyExpr: QuintApp, _position: number) => {}, onAnyOptionReturn: (_anyExpr: QuintApp, _position: number) => {}, onAnyReturn: (_noptions: number, _choice: number) => {}, + onNextState: (_oldState: EvalResult, _newState: EvalResult) => {}, onRunCall: () => {}, onRunReturn: (_outcome: Maybe, _trace: EvalResult[]) => {}, } @@ -186,7 +190,11 @@ class TraceRecorderImpl implements TraceRecorder { private bestTraceSeed: bigint // whenever a run is entered, we store its seed here private runSeed: bigint - // during simulation, a trace is built here + // During simulation, a trace is built here. + // Similar to an execution with a stack machine, + // every call to a user-defined operator produces its own frame. + // Since execution frames store subframes, they effectively produce + // a tree of calls. private frameStack: ExecutionFrame[] constructor(verbosityLevel: number, rng: Rng) { @@ -218,16 +226,28 @@ class TraceRecorderImpl implements TraceRecorder { // https://github.com/informalsystems/quint/issues/747 if (verbosity.hasUserOpTracking(this.verbosityLevel)) { const newFrame = { app: app, args: [], result: none(), subframes: [] } - if (this.frameStack.length > 0) { + if (this.frameStack.length == 0) { + // this should not happen, as there is always bottomFrame, + // but we do not throw here, as trace collection is not the primary + // function of the simulator. + this.frameStack = [newFrame] + } else if (this.frameStack.length === 2 && this.frameStack[1].app.opcode === '_') { + // A placeholder frame created from `q::input` or `then`. Modify in place. + const frame = this.frameStack[1] + frame.app = app + frame.args = [] + frame.result = none() + frame.subframes = [] + } else { + // connect the new frame to the previous frame this.frameStack[this.frameStack.length - 1].subframes.push(newFrame) + // and push the new frame to be on top of the stack this.frameStack.push(newFrame) - } else { - this.frameStack = [newFrame] } } } - onUserOperatorReturn(app: QuintApp, args: EvalResult[], result: Maybe) { + onUserOperatorReturn(_app: QuintApp, args: EvalResult[], result: Maybe) { if (verbosity.hasUserOpTracking(this.verbosityLevel)) { const top = this.frameStack.pop() if (top) { @@ -285,6 +305,18 @@ class TraceRecorderImpl implements TraceRecorder { } } + onNextState(_oldState: EvalResult, _newState: EvalResult) { + // introduce a new frame that is labelled with a dummy operator + if (verbosity.hasUserOpTracking(this.verbosityLevel)) { + const dummy: QuintApp = { id: 0n, kind: 'app', opcode: '_', args: [] } + const newFrame = { app: dummy, args: [], result: none(), subframes: [] } + // forget the frames, except the bottom one, and push the new one + this.frameStack = [this.frameStack[0], newFrame] + // connect the new frame to the topmost frame, which effects in a new step + this.frameStack[0].subframes.push(newFrame) + } + } + onRunCall() { // reset the stack this.frameStack = [this.newBottomFrame()] diff --git a/quint/test/repl.test.ts b/quint/test/repl.test.ts index 088cbcab4..1e8698cc4 100644 --- a/quint/test/repl.test.ts +++ b/quint/test/repl.test.ts @@ -241,8 +241,7 @@ describe('repl ok', () => { |5 | |[Frame 0] - |q::input() => 5 - |└─ plus(2, 3) => 5 + |plus(2, 3) => 5 | |>>> ` ) @@ -264,8 +263,7 @@ describe('repl ok', () => { |>>> div(2, 0) | |[Frame 0] - |q::input() => none - |└─ div(2, 0) => none + |div(2, 0) => none | |runtime error: error: Division by zero |div(2, 0) @@ -300,7 +298,7 @@ describe('repl ok', () => { |true | |[Frame 0] - |q::input() => true + |_ => true | |>>> action step = x' = x + 1 | @@ -312,17 +310,15 @@ describe('repl ok', () => { |true | |[Frame 0] - |q::input() => true - |└─ input1() => true - | └─ step() => true + |input1 => true + |└─ step => true | |>>> input2 |true | |[Frame 0] - |q::input() => true - |└─ input2() => true - | └─ step() => true + |input2 => true + |└─ step => true | |>>> ` ) @@ -636,6 +632,41 @@ describe('repl ok', () => { await assertRepl(input, output) }) + it('actions introduce their own frames', async () => { + const input = dedent( + `var n: int + |action init = n' = 0 + |action step = n' = n + 1 + |.verbosity=3 + |init.then(step).then(step) + |` + ) + const output = dedent( + `>>> var n: int + | + |>>> action init = n' = 0 + | + |>>> action step = n' = n + 1 + | + |>>> .verbosity=3 + |.verbosity=3 + |>>> init.then(step).then(step) + |true + | + |[Frame 0] + |init => true + | + |[Frame 1] + |step => true + | + |[Frame 2] + |step => true + | + |>>> ` + ) + await assertRepl(input, output) + }) + it('run q::test, q::testOnce, and q::lastTrace', async () => { const input = dedent( ` diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts index e0172d4d6..a520dcc41 100644 --- a/quint/test/runtime/compile.test.ts +++ b/quint/test/runtime/compile.test.ts @@ -13,6 +13,7 @@ import { compileExpr, compileFromCode, contextNameLookup, + inputDefName, } from '../../src/runtime/compile' import { RuntimeValue } from '../../src/runtime/impl/runtimeValue' import { dedent } from '../textUtils' @@ -29,7 +30,7 @@ const idGen = newIdGenerator() // Compile an expression, evaluate it, convert to QuintEx, then to a string, // compare the result. This is the easiest path to test the results. function assertResultAsString(input: string, expected: string | undefined) { - const moduleText = `module __runtime { val q::input = ${input} }` + const moduleText = `module __runtime { val ${inputDefName} = ${input} }` const mockLookupPath = stringSourceResolver(new Map()).lookupPath('/', './mock') const context = compileFromCode(idGen, moduleText, '__runtime', mockLookupPath, noExecutionListener, newRng().next) @@ -40,7 +41,7 @@ function assertResultAsString(input: string, expected: string | undefined) { } function assertInputFromContext(context: CompilationContext, expected: string | undefined) { - contextNameLookup(context.evaluationState.context, 'q::input', 'callable') + contextNameLookup(context.evaluationState.context, inputDefName, 'callable') .mapLeft(msg => assert(false, `Unexpected error: ${msg}`)) .mapRight(value => assertComputableAsString(value, expected)) } diff --git a/quint/testFixture/simulator/lastActionInRun.qnt b/quint/testFixture/simulator/lastActionInRun.qnt new file mode 100644 index 000000000..85c49e588 --- /dev/null +++ b/quint/testFixture/simulator/lastActionInRun.qnt @@ -0,0 +1,15 @@ +// See: +// https://github.com/informalsystems/quint/issues/1133 +module lastActionInRun { + var s: str + + action A = + s' = "A" + + action B = + s' = "B" + + run t1 = A.then(A).then(B) + + run t2 = A.then(A).then(B).then(s'=s) +} From 5e1843b0fda69bccf25514b00be85f7d0efce555 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 14 Sep 2023 14:01:57 +0200 Subject: [PATCH 8/8] Serialize big integers in ITF traces as an object (#1165) * simplify ITF traces * update changelog * fix the tests --- CHANGELOG.md | 3 ++- quint/io-cli-tests.md | 24 ++++++++++++++++++------ quint/src/itf.ts | 20 ++++++++------------ quint/test/itf.test.ts | 24 ++++++++++++------------ 4 files changed, 40 insertions(+), 31 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2e375a8bd..5586e297d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,7 +14,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Changed - - Introduce frames on actions in the verbose output. The verbose output has changed! (#1158) +- Introduce frames on actions in the verbose output. The verbose output has changed! (#1158) +- The ITF traces always serialize integers as `{ '#bigint': 'num }` (#1165) ### Deprecated ### Removed diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 6b0730dce..97f254307 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -635,7 +635,9 @@ rm out-itf-example.itf.json ``` [ "alice", - 0 + { + "#bigint": "0" + } ] ``` @@ -668,23 +670,33 @@ exit $exit_code [ [ "alice", - 0 + { + "#bigint": "0" + } ], [ "bob", - 0 + { + "#bigint": "0" + } ], [ "charlie", - 0 + { + "#bigint": "0" + } ], [ "eve", - 0 + { + "#bigint": "0" + } ], [ "null", - 0 + { + "#bigint": "0" + } ] ] ``` diff --git a/quint/src/itf.ts b/quint/src/itf.ts index 95095f016..b654cf7da 100644 --- a/quint/src/itf.ts +++ b/quint/src/itf.ts @@ -71,9 +71,6 @@ function isUnserializable(v: ItfValue): v is ItfUnserializable { return (v as ItfUnserializable)['#unserializable'] !== undefined } -const minJsInt: bigint = BigInt(Number.MIN_SAFE_INTEGER) -const maxJsInt: bigint = BigInt(Number.MAX_SAFE_INTEGER) - /** * Convert a list of Quint expressions into an object that matches the JSON * representation of the ITF trace. This function does not add metadata @@ -87,13 +84,8 @@ export function toItf(vars: string[], states: QuintEx[]): Either => { switch (ex.kind) { case 'int': - if (ex.value >= minJsInt && ex.value <= maxJsInt) { - // We can represent safely as a JS number - return right(Number(ex.value)) - } else { - // convert to a special structure, when saving to JSON - return right({ '#bigint': `${ex.value}` }) - } + // convert to a special structure, when saving to JSON + return right({ '#bigint': `${ex.value}` }) case 'str': case 'bool': @@ -189,12 +181,16 @@ export function ofItf(itf: ItfTrace): QuintEx[] { return { id, kind: 'bool', value } } else if (typeof value === 'string') { return { id, kind: 'str', value } + } else if (isBigint(value)) { + // this is the standard way of encoding an integer in ITF. + return { id, kind: 'int', value: BigInt(value['#bigint']) } } else if (typeof value === 'number') { + // We never encode an integer as a JS number, + // but we consume it for backwards compatibility with older ITF traces. + // See: https://apalache.informal.systems/docs/adr/015adr-trace.html return { id, kind: 'int', value: BigInt(value) } } else if (Array.isArray(value)) { return { id, kind: 'app', opcode: 'List', args: value.map(ofItfValue) } - } else if (isBigint(value)) { - return { id, kind: 'int', value: BigInt(value['#bigint']) } } else if (isTup(value)) { return { id, kind: 'app', opcode: 'Tup', args: value['#tup'].map(ofItfValue) } } else if (isSet(value)) { diff --git a/quint/test/itf.test.ts b/quint/test/itf.test.ts index 669d78212..71913dc27 100644 --- a/quint/test/itf.test.ts +++ b/quint/test/itf.test.ts @@ -3,24 +3,24 @@ import { assert } from 'chai' import { quintExAreEqual, zip } from './util' import { buildExpression } from './builders/ir' -import { ofItf, toItf } from '../src/itf' +import { ItfTrace, ofItf, toItf } from '../src/itf' describe('toItf', () => { it('converts two states', () => { const trace = ['{ x: 2, y: true }', '{ x: 3, y: false }'].map(buildExpression) const itfTrace = toItf(['x', 'y'], trace) - const expected = { + const expected: ItfTrace = { vars: ['x', 'y'], states: [ { '#meta': { index: 0 }, - x: 2, + x: { '#bigint': '2' }, y: true, }, { '#meta': { index: 1 }, - x: 3, + x: { '#bigint': '3' }, y: false, }, ], @@ -58,21 +58,21 @@ describe('toItf', () => { '#meta': { index: 0, }, - a: 2, + a: { '#bigint': '2' }, b: 'hello', c: { '#bigint': '1000000000000000000' }, - d: { '#set': [5, 6] }, - e: { foo: 3, bar: true }, - f: { '#tup': [7, 'myStr'] }, + d: { '#set': [{ '#bigint': '5' }, { '#bigint': '6' }] }, + e: { foo: { '#bigint': '3' }, bar: true }, + f: { '#tup': [{ '#bigint': '7' }, 'myStr'] }, g: { '#map': [ - [1, 'a'], - [2, 'b'], - [3, 'c'], + [{ '#bigint': '1' }, 'a'], + [{ '#bigint': '2' }, 'b'], + [{ '#bigint': '3' }, 'c'], ], }, h: { '#map': [] }, - i: { '#map': [[1, 'a']] }, + i: { '#map': [[{ '#bigint': '1' }, 'a']] }, }, ], }