From adf0f3fca7de442d2f93038f4862d21e68f5805f Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 24 Aug 2023 19:02:30 -0300 Subject: [PATCH 1/9] Define how to compose flatteners and use that for flattening --- quint/src/cliCommands.ts | 2 +- quint/src/flattening/flattener.ts | 18 +- quint/src/flattening/fullFlattener.ts | 96 +++++++++ quint/src/ir/namespacer.ts | 3 +- quint/src/runtime/compile.ts | 35 ++-- quint/test/flattening/fullFlattener.test.ts | 218 ++++++++++++++++++++ 6 files changed, 346 insertions(+), 26 deletions(-) create mode 100644 quint/src/flattening/fullFlattener.ts create mode 100644 quint/test/flattening/fullFlattener.test.ts diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 9d0bb8f7e..cf8601ea1 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -42,7 +42,7 @@ import { verbosity } from './verbosity' import { Rng, newRng } from './rng' import { fileSourceResolver } from './parsing/sourceResolver' import { verify } from './quintVerifier' -import { flattenModules } from './flattening' +import { flattenModules } from './flattening/fullFlattener' import { analyzeModules } from './quintAnalyzer' import { ExecutionFrame } from './runtime/trace' diff --git a/quint/src/flattening/flattener.ts b/quint/src/flattening/flattener.ts index 0127dba82..8f4786c36 100644 --- a/quint/src/flattening/flattener.ts +++ b/quint/src/flattening/flattener.ts @@ -22,6 +22,7 @@ import { QuintInstance, QuintModule, QuintName, + isDef, qualifier, } from '../ir/quintIr' @@ -85,6 +86,14 @@ class Flattener implements IRVisitor { exitModule(quintModule: QuintModule) { // Get rid of imports and exports, and add the definitions we collected quintModule.declarations = quintModule.declarations.filter(d => d.kind !== 'import' && d.kind !== 'export') + // Delete repeated definitions from `defsToAdd` + quintModule.declarations.forEach(d => { + if (isDef(d)) { + this.defsToAdd.delete(d.name) + } + }) + + // Add the definitions to the module (mutating it) quintModule.declarations.push(...this.defsToAdd.values()) } @@ -115,13 +124,18 @@ class Flattener implements IRVisitor { } const namespace = this.namespaceForNested ?? qualifier(decl) - const newDef = + const newDef: QuintDef = namespace && !def.name.startsWith(namespace) ? addNamespaceToDefinition(def, namespace, new Set(builtinNames)) : def + // Typescript still keeps `LookupDefinition` extra fields even if we say `newDef` is a `QuintDef`. We need to + // remove them manually, so when this is collected back into a `LookupTable`, this leftover values don't get + // propagated. + const newDefWithoutMetadata = { ...newDef, hidden: false, namespaces: [], importedFrom: undefined } + this.walkNested(namespace, newDef) - this.defsToAdd.set(newDef.name, newDef) + this.defsToAdd.set(newDef.name, newDefWithoutMetadata) }) } diff --git a/quint/src/flattening/fullFlattener.ts b/quint/src/flattening/fullFlattener.ts new file mode 100644 index 000000000..7d6d7bb34 --- /dev/null +++ b/quint/src/flattening/fullFlattener.ts @@ -0,0 +1,96 @@ +import { IdGenerator } from '../idGenerator' +import { moduleToString } from '../ir/IRprinting' +import { FlatModule, QuintModule } from '../ir/quintIr' +import { LookupTable } from '../names/base' +import { Loc, parsePhase3importAndNameResolution, parsePhase4toposort } from '../parsing/quintParserFrontend' +import { AnalysisOutput } from '../quintAnalyzer' +import { inlineTypeAliases } from '../types/aliasInliner' +import { flattenModule } from './flattener' +import { flattenInstances } from './instanceFlattener' + +/** + * Flatten an array of modules, replacing instances, imports and exports with + * their definitions and inlining type aliases. + * + * @param modules The modules to flatten + * @param table The lookup table to for all referred names + * @param idGenerator The id generator to use for new definitions; should be the same as used for parsing + * @param sourceMap The source map for all modules involved + * @param analysisOutput The analysis output for all modules involved + * + * @returns An object containing the flattened modules, flattened lookup table and flattened analysis output + */ +export function flattenModules( + modules: QuintModule[], + table: LookupTable, + idGenerator: IdGenerator, + sourceMap: Map, + analysisOutput: AnalysisOutput +): { flattenedModules: FlatModule[]; flattenedTable: LookupTable; flattenedAnalysis: AnalysisOutput } { + // FIXME: use copies of parameters so the original objects are not mutated. + // This is not a problem atm, but might be in the future. + + // Inline type aliases + const inlined = inlineTypeAliases(modules, table, analysisOutput) + + const modulesByName = new Map(inlined.modules.map(m => [m.name, m])) + let flattenedModules: QuintModule[] = [] + let flattenedTable = inlined.table + const modulesQueue = inlined.modules + + while (modulesQueue.length > 0) { + const module = modulesQueue.shift()! + const module1 = flattenModule(module, modulesByName, flattenedTable) + + const instancedModules = flattenInstances( + module1, + modulesByName, + flattenedTable, + idGenerator, + sourceMap, + inlined.analysisOutput + ) + + const modulesToFlatten = instancedModules + + const result = parsePhase3importAndNameResolution({ + modules: flattenedModules.concat(modulesToFlatten), + sourceMap, + }) + + if (result.isLeft()) { + flattenedModules.concat(modulesToFlatten).forEach(m => console.log(moduleToString(m))) + throw new Error('[1] Flattening failed: ' + result.value.map(e => e.explanation)) + } + + const { table: newTable } = result.unwrap() + flattenedTable = newTable + + const phase3 = instancedModules.map(m => { + const flat = flattenModule(m, modulesByName, newTable) + modulesByName.set(m.name, flat) + return flat + }) + + flattenedModules.push(...phase3) + const toResolve = flattenedModules.concat(modulesQueue) + const result3 = parsePhase3importAndNameResolution({ + modules: toResolve, + sourceMap, + }).chain(parsePhase4toposort) + + if (result3.isLeft()) { + toResolve.forEach(m => console.log(moduleToString(m))) + throw new Error('[2] Flattening failed: ' + result3.value.map(e => e.explanation)) + } + + flattenedModules = result3.unwrap().modules.slice(0, flattenedModules.length) + flattenedTable = result3.unwrap().table + } + + return { + flattenedModules: flattenedModules as FlatModule[], + flattenedTable, + flattenedAnalysis: inlined.analysisOutput, + } +} diff --git a/quint/src/ir/namespacer.ts b/quint/src/ir/namespacer.ts index 76564e5bc..90823b96a 100644 --- a/quint/src/ir/namespacer.ts +++ b/quint/src/ir/namespacer.ts @@ -81,5 +81,6 @@ class Namespacer implements IRTransformer { } function namespacedName(namespace: string | undefined, name: string): string { - return namespace ? `${namespace}::${name}` : name + // FIXME(#1111): We shouldn't need to verify `startsWith` if we find a good way to manage namespaces + return namespace && !name.startsWith(`${namespace}::`) ? `${namespace}::${name}` : name } diff --git a/quint/src/runtime/compile.ts b/quint/src/runtime/compile.ts index 4bf496b74..e2ae3e302 100644 --- a/quint/src/runtime/compile.ts +++ b/quint/src/runtime/compile.ts @@ -26,8 +26,8 @@ import { AnalysisOutput, analyzeInc, analyzeModules } from '../quintAnalyzer' import { mkErrorMessage } from '../cliCommands' import { IdGenerator, newIdGenerator } from '../idGenerator' import { SourceLookupPath } from '../parsing/sourceResolver' -import { addDeclarationToFlatModule, flattenModules } from '../flattening' import { Rng } from '../rng' +import { flattenModules } from '../flattening/fullFlattener' /** * The name of the shadow variable that stores the last found trace. @@ -216,12 +216,6 @@ export function compileDecl( }) const mainModule = state.modules.find(m => m.name === state.mainName)! - const modules = state.modules.map(m => { - if (m.name === state.mainName) { - return { ...m, declarations: [...m.declarations, decl] } - } - return m - }) // We need to resolve names for this new definition. Incremental name // resolution is not our focus now, so just resolve everything again. @@ -230,20 +224,11 @@ export function compileDecl( .map(({ table }) => { const [analysisErrors, analysisOutput] = analyzeInc(state.analysisOutput, table, decl) - const { flattenedModule, flattenedDefs, flattenedTable, flattenedAnalysis } = addDeclarationToFlatModule( - modules, - table, - state.idGen, - state.sourceMap, - analysisOutput, - // Make a copy of the main module, so that we don't modify the original - { ...mainModule, declarations: [...mainModule.declarations] }, - decl - ) - - const flatModules: FlatModule[] = [...state.modules] - flatModules.pop() - flatModules.push(flattenedModule) + const { + flattenedModules: flatModules, + flattenedTable, + flattenedAnalysis, + } = flattenModules(originalModules, table, state.idGen, state.sourceMap, analysisOutput) const newState = { ...state, @@ -251,7 +236,13 @@ export function compileDecl( modules: flatModules, originalModules: originalModules, } - const ctx = compile(newState, evaluationState, flattenedTable, rng.next, flattenedDefs) + + const flatDefinitions = flatModules.find(m => m.name === state.mainName)!.declarations + + // Filter definitions that were not compiled yet + const defsToCompile = flatDefinitions.filter(d => !mainModule.declarations.some(d2 => d2.id === d.id)) + + const ctx = compile(newState, evaluationState, flattenedTable, rng.next, defsToCompile) const errorLocator = mkErrorMessage(state.sourceMap) return { diff --git a/quint/test/flattening/fullFlattener.test.ts b/quint/test/flattening/fullFlattener.test.ts new file mode 100644 index 000000000..18f02df5b --- /dev/null +++ b/quint/test/flattening/fullFlattener.test.ts @@ -0,0 +1,218 @@ +import { assert } from 'chai' +import { describe, it } from 'mocha' +import { flattenModules } from '../../src/flattening/fullFlattener' +import { newIdGenerator } from '../../src/idGenerator' +import { parse, parsePhase3importAndNameResolution, parsePhase4toposort } from '../../src/parsing/quintParserFrontend' +import { SourceLookupPath } from '../../src/parsing/sourceResolver' +import { analyzeModules } from '../../src/quintAnalyzer' + +describe('flattenModules', () => { + function assertFlattenedModule(text: string) { + const idGenerator = newIdGenerator() + const fake_path: SourceLookupPath = { normalizedPath: 'fake_path', toSourceName: () => 'fake_path' } + parse(idGenerator, 'test_location', fake_path, text) + .map(({ modules, table, sourceMap }) => { + const [analysisErrors, analysisOutput] = analyzeModules(table, modules) + + const { flattenedModules, flattenedTable } = flattenModules( + modules, + table, + idGenerator, + sourceMap, + analysisOutput + ) + + it('has proper names in flattened modules', () => { + const result = parsePhase3importAndNameResolution({ modules: flattenedModules, sourceMap }) + assert.isTrue(result.isRight()) + result.map(({ table }) => + assert.sameDeepMembers( + [...flattenedTable.entries()].map(([id, def]) => [id, def.id]), + [...table.entries()].map(([id, def]) => [id, def.id]) + ) + ) + + result.chain(parsePhase4toposort).map(({ modules }) => { + assert.deepEqual(modules, flattenedModules) + }) + }) + + it('has proper analysis output in flattened modules', () => { + assert.isEmpty(analysisErrors) + }) + }) + .mapLeft(err => { + it('has no erros', () => { + assert.fail(`Expected no error, but got ${err.map(e => e.explanation)}`) + }) + }) + } + + describe('flattenning simple imports', () => { + const text = `module A { + val a = 1 + } + + module B { + import A.* + val b = a + 1 + }` + + assertFlattenedModule(text) + }) + + describe('flattenning simple instances', () => { + const text = `module A { + const N: int + val a = N + } + + module B { + import A(N=1).* + val b = a + 1 + }` + + assertFlattenedModule(text) + }) + + describe('flattenning simple exports', () => { + const text = `module A { + val a = 1 + } + + module B { + export A.* + } + + module C { + import B.* + val c = a + 1 + }` + + assertFlattenedModule(text) + }) + + describe('flattenning multiple instances', () => { + const text = `module A { + const N: int + val a = N + } + + module B { + import A(N=1).* + val b = a + 1 + } + + module C { + import A(N=2).* + val c = a + 1 + } + + module D { + import B + import C + val d = B::b + C::c + }` + + assertFlattenedModule(text) + }) + + describe('flattenning exports of abstract modules (to be instantiated in another module)', () => { + const text = `module A { + const N: int + val a = N + } + + module B { + import A.* + export A.* + val b = a + 1 + } + + module C { + import B(N=1).* + val c = a + 1 + }` + + assertFlattenedModule(text) + }) + + describe('flattenning exported instance', () => { + const text = `module A { + const N: int + val a = N + } + + module B { + import A(N=1) as A1 + val b = A1::a + 1 + export A1 + } + + module C { + import B.* + val c = A1::a + b + }` + + assertFlattenedModule(text) + }) + + describe('flattenning with names that should not conflict', () => { + const text = `module A { + val a = 1 + def f(x) = x + } + + module B { + var x: int + import A.* + val b = a + x + } + + module C { + import A.* + import B + def g(x) = x + B::x + }` + + assertFlattenedModule(text) + }) + + describe('flattenning import of single name', () => { + const text = `module A { + val a1 = 1 + val a = a1 + } + + module B { + import A.a + val b = a + 1 + } + + module C { + import B.* + val c = b + 1 + }` + + assertFlattenedModule(text) + }) + + describe('flattenning instances with the same name in different modules', () => { + const text = `module A { + const N: int + val a = N + } + + module B { + import A(N=1) as A1 + val b = A1::a + 1 + } + + module C { + import A(N=1) as A1 + val c = A1::a + 1 + }` + + assertFlattenedModule(text) + }) +}) From 31fc617c0b2037403102a6b06456b30b9c81025c Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 24 Aug 2023 19:03:09 -0300 Subject: [PATCH 2/9] Delete old flattener --- quint/src/flattening.ts | 288 ----------------------------- quint/test/flatenning.test.ts | 263 -------------------------- quint/test/runtime/compile.test.ts | 2 +- 3 files changed, 1 insertion(+), 552 deletions(-) delete mode 100644 quint/src/flattening.ts delete mode 100644 quint/test/flatenning.test.ts diff --git a/quint/src/flattening.ts b/quint/src/flattening.ts deleted file mode 100644 index a5a22f8c3..000000000 --- a/quint/src/flattening.ts +++ /dev/null @@ -1,288 +0,0 @@ -/* ---------------------------------------------------------------------------------- - * Copyright (c) Informal Systems 2023. All rights reserved. - * Licensed under the Apache 2.0. - * See License.txt in the project root for license information. - * --------------------------------------------------------------------------------- */ - -/** - * Flattening for modules, replacing instances and (soon) imports with their definitions. - * - * @author Gabriela Moreira - * - * @module - */ - -import { IdGenerator } from './idGenerator' -import { LookupTable, builtinNames } from './names/base' -import { - FlatModule, - QuintDeclaration, - QuintDef, - QuintExport, - QuintImport, - QuintInstance, - QuintModule, - isDef, -} from './ir/quintIr' -import { moduleToString } from './ir/IRprinting' -import { Loc, parsePhase3importAndNameResolution } from './parsing/quintParserFrontend' -import { uniqBy } from 'lodash' -import { AnalysisOutput } from './quintAnalyzer' -import { inlineAliasesInDef, inlineAnalysisOutput, inlineTypeAliases } from './types/aliasInliner' -import { addNamespaceToDefinition } from './ir/namespacer' -import { generateFreshIds } from './ir/idRefresher' - -/** - * Flatten an array of modules, replacing instances, imports and exports with - * their definitions and inlining type aliases. - * - * @param modules The modules to flatten - * @param table The lookup table to for all referred names - * @param idGenerator The id generator to use for new definitions; should be the same as used for parsing - * @param sourceMap The source map for all modules involved - * @param analysisOutput The analysis output for all modules involved - * - * @returns An object containing the flattened modules, flattened lookup table and flattened analysis output - */ -export function flattenModules( - modules: QuintModule[], - table: LookupTable, - idGenerator: IdGenerator, - sourceMap: Map, - analysisOutput: AnalysisOutput -): { flattenedModules: FlatModule[]; flattenedTable: LookupTable; flattenedAnalysis: AnalysisOutput } { - // FIXME: use copies of parameters so the original objects are not mutated. - // This is not a problem atm, but might be in the future. - - // Inline type aliases - const inlined = inlineTypeAliases(modules, table, analysisOutput) - // Create a map of imported modules, to be used when flattening - // instances/imports/exports. This is updated as the modules are flattened. - const importedModules = new Map(inlined.modules.map(m => [m.name, m])) - - // Reduce the array of modules to a single object containing the flattened - // modules, flattened lookup table and flattened analysis output - return inlined.modules.reduce( - (acc, module) => { - const { flattenedModules, flattenedTable, flattenedAnalysis } = acc - - // Flatten the current module - const flattener = new Flatenner( - idGenerator, - flattenedTable, - sourceMap, - flattenedAnalysis, - importedModules, - module - ) - const flattened = flattener.flattenModule() - - // Add the flattened module to the imported modules map - importedModules.set(module.name, flattened) - - // Return the updated flattened modules, flattened lookup table and flattened analysis output - return { - flattenedModules: [...flattenedModules, flattened], - // The lookup table has to be updated for every new module that is flattened - // Since the flattened modules have new ids for both the name expressions - // and their definitions, and the next iteration might depend on an updated - // lookup table - flattenedTable: resolveNamesOrThrow(flattenedTable, sourceMap, flattened), - flattenedAnalysis: flattenedAnalysis, - } - }, - { flattenedModules: [] as FlatModule[], flattenedTable: inlined.table, flattenedAnalysis: inlined.analysisOutput } - ) -} - -/** - * Adds a definition to a flat module, flattening any instances, imports and - * exports in the process. Note that the provided parameters should include - * information for the new definition already, i.e. the lookup table should - * already contain all the references for names in the definition. - * - * @param modules The modules possibly reffered by the definition - * @param table The lookup table to for all referred names - * @param idGenerator The id generator to use for new definitions - * @param sourceMap The source map for all modules involved - * @param analysisOutput The analysis output for all modules involved - * @param module The flat module to add the definition to - * @param decl The definition to add - * - * @returns An object containing the flattened module, flattened lookup table - * and flattened analysis output - */ -export function addDeclarationToFlatModule( - modules: QuintModule[], - table: LookupTable, - idGenerator: IdGenerator, - sourceMap: Map, - analysisOutput: AnalysisOutput, - module: FlatModule, - decl: QuintDeclaration -): { - flattenedModule: FlatModule - flattenedDefs: QuintDef[] - flattenedTable: LookupTable - flattenedAnalysis: AnalysisOutput -} { - const importedModules = new Map(modules.map(m => [m.name, m])) - const flattener = new Flatenner(idGenerator, table, sourceMap, analysisOutput, importedModules, module) - - const flattenedDefs = flattener - .flattenDef(decl) - // Inline type aliases in new defs - .map(d => inlineAliasesInDef(d, table)) - const flattenedModule: FlatModule = { ...module, declarations: [...module.declarations, ...flattenedDefs] } - - return { - flattenedModule, - flattenedDefs, - flattenedTable: resolveNamesOrThrow(table, sourceMap, flattenedModule), - flattenedAnalysis: inlineAnalysisOutput(analysisOutput, table), - } -} - -class Flatenner { - private table: LookupTable - private currentModuleNames: Set - private importedModules: Map - private module: QuintModule - - private idGenerator: IdGenerator - private sourceMap: Map - private analysisOutput: AnalysisOutput - - constructor( - idGenerator: IdGenerator, - table: LookupTable, - sourceMap: Map, - analysisOutput: AnalysisOutput, - importedModules: Map, - module: QuintModule - ) { - this.table = table - this.currentModuleNames = new Set([ - // builtin names - ...builtinNames, - // names from the current module - ...module.declarations.filter(isDef).map(d => d.name), - ]) - - this.importedModules = importedModules - this.module = module - this.idGenerator = idGenerator - this.sourceMap = sourceMap - this.analysisOutput = analysisOutput - } - - flattenDef(def: QuintDeclaration): QuintDef[] { - if (isDef(def)) { - // Not an instance, import or export, keep the same def - return [def] - } - - if (def.kind === 'instance') { - return this.flattenInstance(def) - } - - return this.flattenImportOrExport(def) - } - - flattenModule(): FlatModule { - const newDefs = this.module.declarations.flatMap(def => this.flattenDef(def)) - - return { ...this.module, declarations: uniqBy(newDefs, 'name') } - } - - private flattenInstance(def: QuintInstance): QuintDef[] { - // Build pure val definitions from overrides to replace the constants in the - // instance. Index them by name to make it easier to replace the corresponding constants. - const overrides: Map = new Map( - def.overrides.map(([param, expr]) => { - const constDef = this.table.get(param.id)! - if (constDef.kind !== 'const') { - throw new Error(`Impossible: ${constDef} should be a const`) - } - - return [ - param.name, - { - kind: 'def', - qualifier: 'pureval', - name: param.name, - expr, - typeAnnotation: constDef.typeAnnotation, - id: param.id, - }, - ] - }) - ) - - const protoModule = this.importedModules.get(def.protoName)! - - // Overrides replace the original constant definitions, in the same position as they appear originally - const newProtoDefs = protoModule.declarations.filter(isDef).map(d => { - if (overrides.has(d.name)) { - return overrides.get(d.name)! - } - - return d - }) - - // Add the new defs to the modules table under the instance name - if (def.qualifiedName) { - this.importedModules.set(def.qualifiedName, { ...protoModule, declarations: newProtoDefs }) - } - - return newProtoDefs.map(protoDef => this.copyDef(protoDef, def.qualifiedName)) - } - - private flattenImportOrExport(def: QuintImport | QuintExport): QuintDef[] { - const qualifiedName = def.defName ? undefined : def.qualifiedName ?? def.protoName - - const protoModule = this.importedModules.get(def.protoName) - if (!protoModule) { - // Something went really wrong. Topological sort should prevent this from happening. - throw new Error(`Imported module ${def.protoName} not found. Please report a bug.`) - } - - // Add the new defs to the modules table under the qualified name - if (qualifiedName) { - this.importedModules.set(qualifiedName, { ...protoModule, name: qualifiedName }) - } - - const defsToFlatten = filterDefs(protoModule.declarations.filter(isDef), def.defName) - - return defsToFlatten.map(protoDef => this.copyDef(protoDef, qualifiedName)) - } - - private copyDef(def: QuintDef, qualifier: string | undefined): QuintDef { - const defWithQualifier = qualifier ? addNamespaceToDefinition(def, qualifier, this.currentModuleNames) : def - const defWithNewId = generateFreshIds(defWithQualifier, this.idGenerator, this.sourceMap, this.analysisOutput) - - return defWithNewId - } -} - -function filterDefs(defs: QuintDef[], name: string | undefined): QuintDef[] { - if (!name || name === '*') { - return defs - } - - return defs.filter(def => def.name === name) -} - -function resolveNamesOrThrow(currentTable: LookupTable, sourceMap: Map, module: QuintModule): LookupTable { - const newEntries = parsePhase3importAndNameResolution({ modules: [module], sourceMap }) - .mapLeft(errors => { - // This should not happen, as the flattening should not introduce any - // errors, since parsePhase3 analysis of the original modules has already - // assured all names are correct. - console.log(moduleToString(module)) - throw new Error(`Error on resolving names for flattened modules: ${errors.map(e => e.explanation)}`) - }) - .unwrap().table - - return new Map([...currentTable.entries(), ...newEntries.entries()]) -} diff --git a/quint/test/flatenning.test.ts b/quint/test/flatenning.test.ts deleted file mode 100644 index b483a17db..000000000 --- a/quint/test/flatenning.test.ts +++ /dev/null @@ -1,263 +0,0 @@ -import { assert } from 'chai' -import { describe, it } from 'mocha' -import { addDeclarationToFlatModule, flattenModules } from '../src/flattening' -import { newIdGenerator } from '../src/idGenerator' -import { declarationToString } from '../src/ir/IRprinting' -import { parse } from '../src/parsing/quintParserFrontend' -import { FlatModule, analyzeModules } from '../src' -import { SourceLookupPath } from '../src/parsing/sourceResolver' - -describe('flattenModules', () => { - function assertFlatennedDefs(baseDefs: string[], defs: string[], expectedDefs: string[]): void { - const idGenerator = newIdGenerator() - const fake_path: SourceLookupPath = { normalizedPath: 'fake_path', toSourceName: () => 'fake_path' } - - const quintModules: string = `module A { ${baseDefs.join('\n')} } module wrapper { ${defs.join('\n')} }` - - const parseResult = parse(idGenerator, 'fake_location', fake_path, quintModules) - if (parseResult.isLeft()) { - assert.fail('Failed to parse mocked up module') - } - const { modules, table, sourceMap } = parseResult.unwrap() - - const [analysisErrors, analysisOutput] = analyzeModules(table, modules) - assert.isEmpty(analysisErrors) - - const { flattenedModules, flattenedAnalysis } = flattenModules( - modules, - table, - idGenerator, - sourceMap, - analysisOutput - ) - const [_, flattenedModule] = flattenedModules - - it('has all expected declarations', () => { - assert.sameDeepMembers( - flattenedModule.declarations.map(decl => declarationToString(decl)), - expectedDefs - ) - }) - - it('has no aliases in the types map', () => { - assert.notIncludeMembers( - [...flattenedAnalysis.types.values()].map(t => t.type.kind), - ['const'] - ) - }) - } - - describe('multiple instances', () => { - const baseDefs = ['const N: int', 'val x = N + 1'] - - const defs = ['import A(N = 1) as A1', 'import A(N = 2) as A2'] - - const expectedDefs = [ - 'pure val A1::N: int = 1', - 'val A1::x = iadd(A1::N, 1)', - 'pure val A2::N: int = 2', - 'val A2::x = iadd(A2::N, 1)', - ] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) - - describe('single instance with several definitions', () => { - const baseDefs = [ - 'const N: int', - 'var x: int', - 'pure def f(a) = a + 1', - `action V = x' = f(x)`, - 'assume T = N > 0', - 'def lam = val b = 1 { a => b + a }', - 'def lam2 = val b = 1 { a => b + a }', - ] - - const defs = ['import A(N = 1) as A1'] - - const expectedDefs = [ - 'pure val A1::N: int = 1', - 'var A1::x: int', - 'pure def A1::f = ((A1::a) => iadd(A1::a, 1))', - `action A1::V = assign(A1::x, A1::f(A1::x))`, - 'assume A1::T = igt(A1::N, 0)', - 'def A1::lam = val A1::b = 1 { ((A1::a) => iadd(A1::b, A1::a)) }', - 'def A1::lam2 = val A1::b = 1 { ((A1::a) => iadd(A1::b, A1::a)) }', - ] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) - - describe('imports', () => { - const baseDefs = ['val f(x) = x + 1'] - - const defs = ['import A.*'] - - const expectedDefs = ['val f = ((x) => iadd(x, 1))'] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) - - describe('export with previous import', () => { - const baseDefs = ['val f(x) = x + 1'] - - const defs = ['import A.*', 'export A.*'] - - const expectedDefs = ['val f = ((x) => iadd(x, 1))'] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) - - describe('export without previous import', () => { - const baseDefs = ['val f(x) = x + 1'] - - const defs = ['export A.*'] - - const expectedDefs = ['val f = ((x) => iadd(x, 1))'] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) - - describe('export instance', () => { - const baseDefs = ['const N: int', 'val x = N + 1'] - - const defs = ['import A(N = 1) as A1', 'export A1.*'] - - const expectedDefs = [ - // Namespaced defs, from the instance statement - 'pure val A1::N: int = 1', - 'val A1::x = iadd(A1::N, 1)', - // Exported defs, without namespace - 'pure val N: int = 1', - 'val x = iadd(N, 1)', - ] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) - - describe('export instance with qualifier', () => { - const baseDefs = ['const N: int', 'val x = N + 1'] - - const defs = ['val myN = 1', 'import A(N = myN) as A1', 'export A1 as B'] - - const expectedDefs = [ - 'val myN = 1', - // Namespaced defs, from the instance statement - 'pure val A1::N: int = myN', - 'val A1::x = iadd(A1::N, 1)', - // Exported defs, with namespace B - 'pure val B::N: int = myN', - 'val B::x = iadd(B::N, 1)', - ] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) - - describe('inlines aliases', () => { - const baseDefs = ['type MY_ALIAS = int', 'const N: MY_ALIAS'] - - const defs = ['import A(N = 1) as A1', 'var t: A1::MY_ALIAS'] - - const expectedDefs = ['type A1::MY_ALIAS = int', 'pure val A1::N: int = 1', 'var t: int'] - - assertFlatennedDefs(baseDefs, defs, expectedDefs) - }) -}) - -describe('addDefToFlatModule', () => { - function assertAddedDefs( - baseDefs: string[], - currentModuleDefs: string[], - defToAdd: string, - expectedDefs: string[] - ): void { - const idGenerator = newIdGenerator() - const fake_path: SourceLookupPath = { normalizedPath: 'fake_path', toSourceName: () => 'fake_path' } - - const quintModules: string = `module A { ${baseDefs.join('\n')} } module wrapper { ${currentModuleDefs - .concat(defToAdd) - .join('\n')} }` - - const parseResult = parse(idGenerator, 'fake_location', fake_path, quintModules) - if (parseResult.isLeft()) { - assert.fail('Failed to parse mocked up module') - } - const { modules, table, sourceMap } = parseResult.unwrap() - const [_moduleA, module] = modules - - const [analysisErrors, analysisOutput] = analyzeModules(table, modules) - assert.isEmpty(analysisErrors) - - const def = module.declarations[module.declarations.length - 1] - const moduleWithoutDef: FlatModule = { ...module, declarations: [] } - const { flattenedModule, flattenedAnalysis } = addDeclarationToFlatModule( - modules, - table, - idGenerator, - sourceMap, - analysisOutput, - moduleWithoutDef, - def - ) - - it('has all expected declarations', () => { - assert.sameDeepMembers( - flattenedModule.declarations.map(decl => declarationToString(decl)), - expectedDefs - ) - }) - - it('has no aliases in the types map', () => { - assert.notIncludeMembers( - [...flattenedAnalysis.types.values()].map(t => t.type.kind), - ['const'] - ) - }) - } - - describe('single instance with several definitions', () => { - const baseDefs = [ - 'const N: int', - 'var x: int', - 'pure def f(a) = a + 1', - `action V = x' = f(x)`, - 'assume T = N > 0', - 'def lam = val b = 1 { a => b + a }', - 'def lam2 = val b = 1 { a => b + a }', - ] - - const defToAdd = 'import A(N = 1) as A1' - - const expectedDefs = [ - 'pure val A1::N: int = 1', - 'var A1::x: int', - 'pure def A1::f = ((A1::a) => iadd(A1::a, 1))', - `action A1::V = assign(A1::x, A1::f(A1::x))`, - 'assume A1::T = igt(A1::N, 0)', - 'def A1::lam = val A1::b = 1 { ((A1::a) => iadd(A1::b, A1::a)) }', - 'def A1::lam2 = val A1::b = 1 { ((A1::a) => iadd(A1::b, A1::a)) }', - ] - - assertAddedDefs(baseDefs, [], defToAdd, expectedDefs) - }) - - describe('imports', () => { - const baseDefs = ['val f(x) = x + 1'] - - const defToAdd = 'import A.*' - - const expectedDefs = ['val f = ((x) => iadd(x, 1))'] - - assertAddedDefs(baseDefs, [], defToAdd, expectedDefs) - }) - - describe('type aliases', () => { - const currentModuleDefs = ['type MY_ALIAS = int'] - - const defToAdd = 'var N: MY_ALIAS' - - const expectedDefs = ['var N: int'] - - assertAddedDefs([], currentModuleDefs, defToAdd, expectedDefs) - }) -}) diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts index 5c074943e..e0172d4d6 100644 --- a/quint/test/runtime/compile.test.ts +++ b/quint/test/runtime/compile.test.ts @@ -20,7 +20,7 @@ import { newIdGenerator } from '../../src/idGenerator' import { Rng, newRng } from '../../src/rng' import { SourceLookupPath, stringSourceResolver } from '../../src/parsing/sourceResolver' import { analyzeModules, parse, parseExpressionOrDeclaration } from '../../src' -import { flattenModules } from '../../src/flattening' +import { flattenModules } from '../../src/flattening/fullFlattener' import { newEvaluationState } from '../../src/runtime/impl/compilerImpl' // Use a global id generator, limited to this test suite. From 10626c9b7199177e7da25ffce14c5907cb77ef9c Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 24 Aug 2023 19:08:55 -0300 Subject: [PATCH 3/9] Adapt export usage in examples --- examples/cosmos/tendermint/TendermintAcc005.qnt | 1 + examples/language-features/instances.qnt | 3 --- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/examples/cosmos/tendermint/TendermintAcc005.qnt b/examples/cosmos/tendermint/TendermintAcc005.qnt index 9111ff261..a7af6ea5d 100644 --- a/examples/cosmos/tendermint/TendermintAcc005.qnt +++ b/examples/cosmos/tendermint/TendermintAcc005.qnt @@ -665,6 +665,7 @@ module TendermintAcc { // Tests that demonstrate typical behavior. module TendermintTest { import TendermintAcc.* + export TendermintAcc.* // Quint will automatically compute the unchanged block in the future action unchangedAll = all { diff --git a/examples/language-features/instances.qnt b/examples/language-features/instances.qnt index 0bf57a33e..e46043a44 100644 --- a/examples/language-features/instances.qnt +++ b/examples/language-features/instances.qnt @@ -24,9 +24,6 @@ module instances { // the above is equivalent to TLA+'s instance: // A2 == INSTANCE A WITH x <- 15, y <- MyY - export A1 - export A2 - action init = true action step = true } From 7db8fb6ce27793058bd1eee468b9974bbe346f9f Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 24 Aug 2023 19:36:40 -0300 Subject: [PATCH 4/9] Improve readability --- quint/src/flattening/fullFlattener.ts | 68 +++++++++++++++------------ 1 file changed, 37 insertions(+), 31 deletions(-) diff --git a/quint/src/flattening/fullFlattener.ts b/quint/src/flattening/fullFlattener.ts index 7d6d7bb34..5569fe9d4 100644 --- a/quint/src/flattening/fullFlattener.ts +++ b/quint/src/flattening/fullFlattener.ts @@ -2,7 +2,13 @@ import { IdGenerator } from '../idGenerator' import { moduleToString } from '../ir/IRprinting' import { FlatModule, QuintModule } from '../ir/quintIr' import { LookupTable } from '../names/base' -import { Loc, parsePhase3importAndNameResolution, parsePhase4toposort } from '../parsing/quintParserFrontend' +import { + Loc, + ParserPhase3, + ParserPhase4, + parsePhase3importAndNameResolution, + parsePhase4toposort, +} from '../parsing/quintParserFrontend' import { AnalysisOutput } from '../quintAnalyzer' import { inlineTypeAliases } from '../types/aliasInliner' import { flattenModule } from './flattener' @@ -36,61 +42,61 @@ export function flattenModules( const modulesByName = new Map(inlined.modules.map(m => [m.name, m])) let flattenedModules: QuintModule[] = [] let flattenedTable = inlined.table + const flattenedAnalysis = inlined.analysisOutput const modulesQueue = inlined.modules while (modulesQueue.length > 0) { const module = modulesQueue.shift()! - const module1 = flattenModule(module, modulesByName, flattenedTable) + const moduleAfterFirstFlattening = flattenModule(module, modulesByName, flattenedTable) const instancedModules = flattenInstances( - module1, + moduleAfterFirstFlattening, modulesByName, flattenedTable, idGenerator, sourceMap, - inlined.analysisOutput + flattenedAnalysis ) - const modulesToFlatten = instancedModules - - const result = parsePhase3importAndNameResolution({ - modules: flattenedModules.concat(modulesToFlatten), - sourceMap, - }) - - if (result.isLeft()) { - flattenedModules.concat(modulesToFlatten).forEach(m => console.log(moduleToString(m))) - throw new Error('[1] Flattening failed: ' + result.value.map(e => e.explanation)) - } - - const { table: newTable } = result.unwrap() - flattenedTable = newTable + const intermediateTable = resolveNamesOrThrow(flattenedModules.concat(instancedModules), sourceMap).table const phase3 = instancedModules.map(m => { - const flat = flattenModule(m, modulesByName, newTable) + const flat = flattenModule(m, modulesByName, intermediateTable) modulesByName.set(m.name, flat) return flat }) flattenedModules.push(...phase3) - const toResolve = flattenedModules.concat(modulesQueue) - const result3 = parsePhase3importAndNameResolution({ - modules: toResolve, - sourceMap, - }).chain(parsePhase4toposort) - if (result3.isLeft()) { - toResolve.forEach(m => console.log(moduleToString(m))) - throw new Error('[2] Flattening failed: ' + result3.value.map(e => e.explanation)) - } + const result = toposortOrThrow(flattenedModules.concat(modulesQueue), sourceMap) - flattenedModules = result3.unwrap().modules.slice(0, flattenedModules.length) - flattenedTable = result3.unwrap().table + flattenedModules = result.modules.slice(0, flattenedModules.length) + flattenedTable = result.table } return { flattenedModules: flattenedModules as FlatModule[], flattenedTable, - flattenedAnalysis: inlined.analysisOutput, + flattenedAnalysis, + } +} + +function resolveNamesOrThrow(modules: QuintModule[], sourceMap: Map): ParserPhase3 { + const result = parsePhase3importAndNameResolution({ modules, sourceMap }) + if (result.isLeft()) { + modules.forEach(m => console.log(moduleToString(m))) + throw new Error('Internal error while flattening' + result.value.map(e => e.explanation)) } + + return result.unwrap() +} + +function toposortOrThrow(modules: QuintModule[], sourceMap: Map): ParserPhase4 { + const result = parsePhase3importAndNameResolution({ modules, sourceMap }).chain(parsePhase4toposort) + if (result.isLeft()) { + modules.forEach(m => console.log(moduleToString(m))) + throw new Error('Internal error while flattening' + result.value.map(e => e.explanation)) + } + + return result.unwrap() } From 8a4db64b876a6af28c1a1b3ec142d1346e6cb76c Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 24 Aug 2023 19:56:24 -0300 Subject: [PATCH 5/9] Add clarifying comments --- quint/src/flattening/flattener.ts | 2 +- quint/src/flattening/fullFlattener.ts | 46 +++++++++++++++++++++++---- 2 files changed, 40 insertions(+), 8 deletions(-) diff --git a/quint/src/flattening/flattener.ts b/quint/src/flattening/flattener.ts index 8f4786c36..3bf484664 100644 --- a/quint/src/flattening/flattener.ts +++ b/quint/src/flattening/flattener.ts @@ -5,7 +5,7 @@ * --------------------------------------------------------------------------------- */ /** - * Flattening for modules, replacing instances, imports and exports with definitions refered by the module. + * Flattening for modules, replacing imports and exports with definitions referred by the module. * * @author Gabriela Moreira * diff --git a/quint/src/flattening/fullFlattener.ts b/quint/src/flattening/fullFlattener.ts index 5569fe9d4..3a8e15ae7 100644 --- a/quint/src/flattening/fullFlattener.ts +++ b/quint/src/flattening/fullFlattener.ts @@ -1,6 +1,21 @@ +/* ---------------------------------------------------------------------------------- + * Copyright (c) Informal Systems 2023. All rights reserved. + * Licensed under the Apache 2.0. + * See License.txt in the project root for license information. + * --------------------------------------------------------------------------------- */ + +/** + * Flattening for modules, replacing instances, imports and exports with definitions referred by the module. + * + * @author Gabriela Moreira + * + * @module + */ + +import assert from 'assert' import { IdGenerator } from '../idGenerator' import { moduleToString } from '../ir/IRprinting' -import { FlatModule, QuintModule } from '../ir/quintIr' +import { FlatModule, QuintModule, isDef } from '../ir/quintIr' import { LookupTable } from '../names/base' import { Loc, @@ -40,15 +55,22 @@ export function flattenModules( const inlined = inlineTypeAliases(modules, table, analysisOutput) const modulesByName = new Map(inlined.modules.map(m => [m.name, m])) - let flattenedModules: QuintModule[] = [] - let flattenedTable = inlined.table + + // Mutable values, updated on every iteration const flattenedAnalysis = inlined.analysisOutput const modulesQueue = inlined.modules + // Mutable references, updated on every iteration + let flattenedModules: QuintModule[] = [] + let flattenedTable = inlined.table + while (modulesQueue.length > 0) { const module = modulesQueue.shift()! + + // First, flatten imports and exports const moduleAfterFirstFlattening = flattenModule(module, modulesByName, flattenedTable) + // Then, flatten instances, replacing them with imports const instancedModules = flattenInstances( moduleAfterFirstFlattening, modulesByName, @@ -58,22 +80,32 @@ export function flattenModules( flattenedAnalysis ) + // Get an updated lookup table including references for the instanced modules. For that, use all the modules that + // were flattened so far, plus the instanced modules. const intermediateTable = resolveNamesOrThrow(flattenedModules.concat(instancedModules), sourceMap).table - const phase3 = instancedModules.map(m => { + // Flatten the instanced modules, removing the added imports. + instancedModules.forEach(m => { const flat = flattenModule(m, modulesByName, intermediateTable) + flattenedModules.push(flat) + + // Update the index that is going to be used in next iterations modulesByName.set(m.name, flat) - return flat }) - flattenedModules.push(...phase3) - + // Finally, get an updated lookup table and a toposorted version of the definitions. For that, we combine the + // modules that were flattened so far, plus the modules that still have to be flattened (queue). We need to do this + // for the modules in the queue as well since they might also refer to definitions that had their ids changed by the + // instance flattener. const result = toposortOrThrow(flattenedModules.concat(modulesQueue), sourceMap) flattenedModules = result.modules.slice(0, flattenedModules.length) flattenedTable = result.table } + // FIXME: Ideally we should do this via the type system + assert(flattenedModules.every(m => m.declarations.every(isDef))) + return { flattenedModules: flattenedModules as FlatModule[], flattenedTable, From 5b1d80814e995be9abfa4313c60c3416a2bb1c8f Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 25 Aug 2023 10:43:49 -0300 Subject: [PATCH 6/9] Move `parseDefOrThrow` to more general file --- quint/src/parsing/quintParserFrontend.ts | 18 ++++++++++++++---- quint/src/repl.ts | 21 ++++++--------------- 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/quint/src/parsing/quintParserFrontend.ts b/quint/src/parsing/quintParserFrontend.ts index d36f0b236..84c8ef02d 100644 --- a/quint/src/parsing/quintParserFrontend.ts +++ b/quint/src/parsing/quintParserFrontend.ts @@ -17,8 +17,8 @@ import { QuintLexer } from '../generated/QuintLexer' import * as p from '../generated/QuintParser' import { QuintListener } from '../generated/QuintListener' -import { IrErrorMessage, QuintDeclaration, QuintEx, QuintModule } from '../ir/quintIr' -import { IdGenerator } from '../idGenerator' +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 { resolveNames } from '../names/resolver' @@ -28,6 +28,7 @@ import { CallGraphVisitor, mkCallGraphContext } from '../static/callgraph' import { walkModule } from '../ir/IRVisitor' import { toposort } from '../static/toposort' import { ErrorCode } from '../quintError' +import { compact } from 'lodash' export interface Loc { source: string @@ -82,10 +83,10 @@ export function fromIrErrorMessage(sourceMap: SourceMap): (err: IrErrorMessage) export function fromQuintError(sourceMap: Map): (_: QuintError) => ErrorMessage { return error => { - const loc = error.reference ? sourceMap.get(error.reference) ?? unknownLoc : unknownLoc + const loc = error.reference ? sourceMap.get(error.reference) : undefined return { explanation: quintErrorToString(error), - locs: [loc], + locs: compact([loc]), } } } @@ -378,6 +379,15 @@ export function parse( .chain(phase3Data => parsePhase4toposort(phase3Data)) } +export function parseDefOrThrow(text: string, idGen?: IdGenerator, sourceMap?: Map): QuintDef { + const result = parseExpressionOrDeclaration(text, '', idGen ?? newIdGenerator(), sourceMap ?? new Map()) + if (result.kind === 'declaration' && isDef(result.decl)) { + return result.decl + } else { + throw new Error(`Expected a definition, got ${result.kind}, parsing ${text}`) + } +} + // setup a Quint parser, so it can be used to parse from various non-terminals function setupParser(text: string, sourceLocation: string, errorMessages: ErrorMessage[]): p.QuintParser { // error listener to report lexical and syntax errors diff --git a/quint/src/repl.ts b/quint/src/repl.ts index 62003f30d..1e2317cf6 100644 --- a/quint/src/repl.ts +++ b/quint/src/repl.ts @@ -17,7 +17,7 @@ import { Either, left, right } from '@sweet-monads/either' import chalk from 'chalk' import { format } from './prettierimp' -import { FlatModule, QuintDef, QuintEx, isDef } from './ir/quintIr' +import { FlatModule, QuintDef, QuintEx } from './ir/quintIr' import { CompilationContext, CompilationState, @@ -31,7 +31,7 @@ import { import { formatError } from './errorReporter' import { Register } from './runtime/runtime' import { TraceRecorder, newTraceRecorder } from './runtime/trace' -import { ErrorMessage, parseExpressionOrDeclaration } from './parsing/quintParserFrontend' +import { ErrorMessage, parseDefOrThrow, parseExpressionOrDeclaration } from './parsing/quintParserFrontend' import { prettyQuintEx, printExecutionFrameRec, terminalWidth } from './graphics' import { verbosity } from './verbosity' import { Rng, newRng } from './rng' @@ -477,23 +477,14 @@ function saveVars(vars: Register[], nextvars: Register[]): Maybe { // Declarations that are overloaded by the simulator. // In the future, we will declare them in a separate module. -function simulatorBuiltins(compilationState: CompilationState): QuintDef[] { +function simulatorBuiltins(st: CompilationState): QuintDef[] { return [ - parseDefOrThrow(compilationState, `val ${lastTraceName} = []`), - parseDefOrThrow(compilationState, `def q::test = (q::nruns, q::nsteps, q::init, q::next, q::inv) => false`), - parseDefOrThrow(compilationState, `def q::testOnce = (q::nsteps, q::init, q::next, q::inv) => false`), + parseDefOrThrow(`val ${lastTraceName} = []`, st.idGen, st.sourceMap), + parseDefOrThrow(`def q::test = (q::nruns, q::nsteps, q::init, q::next, q::inv) => false`, st.idGen, st.sourceMap), + parseDefOrThrow(`def q::testOnce = (q::nsteps, q::init, q::next, q::inv) => false`, st.idGen, st.sourceMap), ] } -function parseDefOrThrow(compilationState: CompilationState, text: string): QuintDef { - const result = parseExpressionOrDeclaration(text, '', compilationState.idGen, compilationState.sourceMap) - if (result.kind === 'declaration' && isDef(result.decl)) { - return result.decl - } else { - throw new Error(`Expected a definition, got ${result.kind}, parsing ${text}`) - } -} - function tryEvalModule(out: writer, state: ReplState, mainName: string): boolean { const modulesText = state.moduleHist const mainPath = fileSourceResolver().lookupPath(cwd(), 'repl.ts') From 3ad06af0fe3877e1eb2b45386a5b9f283fd11e86 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 25 Aug 2023 10:47:05 -0300 Subject: [PATCH 7/9] Wrap CLI provided definitions inside other names --- quint/apalache-tests.md | 3 ++- quint/src/cliCommands.ts | 48 ++++++++++++++++++++++++++++++---------- 2 files changed, 38 insertions(+), 13 deletions(-) diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md index 74fdf41df..a1f727e16 100644 --- a/quint/apalache-tests.md +++ b/quint/apalache-tests.md @@ -29,7 +29,8 @@ quint verify --init=invalidInit ../examples/language-features/booleans.qnt ``` -error: Configuration error (see the manual): Operator invalidInit not found (used as the initialization predicate) +error: [QNT404] Name 'invalidInit' not found +error: name resolution failed ``` diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index cf8601ea1..1468b1a66 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -17,6 +17,7 @@ import { ErrorMessage, Loc, compactSourceMap, + parseDefOrThrow, parsePhase1fromText, parsePhase2sourceResolution, parsePhase3importAndNameResolution, @@ -43,7 +44,7 @@ import { Rng, newRng } from './rng' import { fileSourceResolver } from './parsing/sourceResolver' import { verify } from './quintVerifier' import { flattenModules } from './flattening/fullFlattener' -import { analyzeModules } from './quintAnalyzer' +import { analyzeInc, analyzeModules } from './quintAnalyzer' import { ExecutionFrame } from './runtime/trace' export type stage = 'loading' | 'parsing' | 'typechecking' | 'testing' | 'running' | 'documentation' @@ -542,6 +543,34 @@ export async function verifySpec(prev: TypecheckedStage): Promise m.name === mainName) + if (!main) { + return cliErr(`module ${mainName} does not exist`, { ...verifying, errors: [], sourceCode: '' }) + } + + // Wrap init, step and invariant in other definitions, to make sure they are not considered unused in the main module + // and, therefore, ignored by the flattener + const extraDefsAsText = [`action q::init = ${args.init}`, `action q::step = ${args.step}`] + if (args.invariant) { + extraDefsAsText.push(`val q::inv = and(${args.invariant.join(',')})`) + } + + const extraDefs = extraDefsAsText.map(d => parseDefOrThrow(d, verifying.idGen, new Map())) + main.declarations.push(...extraDefs) + + // We have to update the lookup table and analysis result with the new definitions. This is not ideal, and the problem + // is that is hard to add this definitions in the proper stage, in our current setup. We should try to tackle this + // while solving #1052. + const resolutionResult = parsePhase3importAndNameResolution(prev) + if (resolutionResult.isLeft()) { + return cliErr('name resolution failed', { ...verifying, errors: resolutionResult.value }) + } + + verifying.table = resolutionResult.unwrap().table + extraDefs.forEach(def => analyzeInc(verifying, verifying.table, def)) + // Flatten modules, replacing instances, imports and exports with their definitions const { flattenedModules, flattenedTable, flattenedAnalysis } = flattenModules( verifying.modules, @@ -552,15 +581,9 @@ export async function verifySpec(prev: TypecheckedStage): Promise m.name === mainName) + const flatMain = flattenedModules.find(m => m.name === mainName)! - if (!main) { - return cliErr(`module ${mainName} does not exist`, { ...verifying, errors: [], sourceCode: '' }) - } - - const veryfiyingFlat = { ...verifying, ...flattenedAnalysis, modules: [main], table: flattenedTable } + const veryfiyingFlat = { ...verifying, ...flattenedAnalysis, modules: [flatMain], table: flattenedTable } const parsedSpec = jsonStringOfOutputStage(pickOutputStage(veryfiyingFlat)) // We need to insert the data form CLI args into thier appropriate locations @@ -578,11 +601,12 @@ export async function verifySpec(prev: TypecheckedStage): Promise res .map(_ => ({ ...verifying, status: 'ok', errors: [] } as VerifiedStage)) From 47d63c6eaace1c6e219cf955742a0b4293b3b667 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 25 Aug 2023 10:47:29 -0300 Subject: [PATCH 8/9] Prevent addition of namespaces to `_` --- quint/src/ir/namespacer.ts | 3 +++ 1 file changed, 3 insertions(+) diff --git a/quint/src/ir/namespacer.ts b/quint/src/ir/namespacer.ts index 90823b96a..48027d572 100644 --- a/quint/src/ir/namespacer.ts +++ b/quint/src/ir/namespacer.ts @@ -81,6 +81,9 @@ class Namespacer implements IRTransformer { } function namespacedName(namespace: string | undefined, name: string): string { + if (name === '_') { + return name + } // FIXME(#1111): We shouldn't need to verify `startsWith` if we find a good way to manage namespaces return namespace && !name.startsWith(`${namespace}::`) ? `${namespace}::${name}` : name } From 7f4f0f66c2f23e927af20c6aa7854883bcbbb0cb Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 25 Aug 2023 10:48:42 -0300 Subject: [PATCH 9/9] Update example and dashboard --- examples/README.md | 2 +- examples/language-features/instancesFrom.qnt | 3 --- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/examples/README.md b/examples/README.md index 3278c338e..01b75d719 100644 --- a/examples/README.md +++ b/examples/README.md @@ -62,7 +62,7 @@ listed without any additional command line arguments. | [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/693,https://github.com/informalsystems/quint/pull/975 | | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] | | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] | -| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: | +| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | | [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] | | [cosmos/tendermint/TendermintAcc005.qnt](./cosmos/tendermint/TendermintAcc005.qnt) | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/pull/1023 | :x:https://github.com/informalsystems/quint/pull/1023 | | [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/693 | diff --git a/examples/language-features/instancesFrom.qnt b/examples/language-features/instancesFrom.qnt index e090f9f21..aa8b81efd 100644 --- a/examples/language-features/instancesFrom.qnt +++ b/examples/language-features/instancesFrom.qnt @@ -15,9 +15,6 @@ module instancesFrom { // the above is equivalent to TLA+'s instance: // A2 == INSTANCE A WITH x <- 15, y <- MyY - export A1 - export A2 - action init = true action step = true }