From 964f2ca0358f125e5606e5d2b76876721216e217 Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Sep 2023 16:16:09 -0300 Subject: [PATCH 1/2] 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 2/2] 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