Merge pull request #1163 from informalsystems/gabriela/fix-shadowing-…

…different-modules

Rename shadowed names to unique names

CHANGELOG.md

@@ -19,6 +19,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

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]))
 

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 `<name>_<lambda-id>`
+ * - Nested definitions (from let expressions) are renamed to `<name>_<let-id>`
+ *
+ * @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<bigint, string>()
+  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
+  }
+}

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)
+  })
 })

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.*
+              |}`),
+    ])
+  })
+})