Flatten definitions in topological order without relying on toposort

CHANGELOG.md

@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fixed a problem where importing the same definition under multiple different
+  names would cause a crash (#1142)
+
 ### Security
 
 ## v0.14.1 -- 2023-08-28

quint/src/flattening/flattener.ts

@@ -15,6 +15,7 @@
 import { LookupDefinition, LookupTable, builtinNames } from '../names/base'
 import {
   QuintApp,
+  QuintDeclaration,
   QuintDef,
   QuintEx,
   QuintExport,
@@ -28,6 +29,8 @@ import {
 
 import { IRVisitor, walkDefinition, walkExpression, walkModule } from '../ir/IRVisitor'
 import { addNamespaceToDefinition } from '../ir/namespacer'
+import assert from 'assert'
+import { uniqBy } from 'lodash'
 
 /**
  * Flatten a module, replacing instances, imports and exports with definitions refered by the module.
@@ -60,13 +63,16 @@ export function flattenModule(
 export function dependentDefinitions(expr: QuintEx, lookupTable: LookupTable): QuintDef[] {
   const flattener = new Flattener(new Map(), lookupTable)
   walkExpression(flattener, expr)
-  return [...flattener.defsToAdd.values()]
+
+  // Walking an expression should never add a non-definition declaration. The following assertion is just to make sure.
+  assert(flattener.newDeclarations.every(d => isDef(d)))
+
+  return [...flattener.newDeclarations.values()] as QuintDef[]
 }
 
 class Flattener implements IRVisitor {
-  // Buffer of definitions to add to the module. We can try to make this ordered in the future.
-  // For now, we rely on toposorting defs after flattening.
-  defsToAdd: Map<string, QuintDef> = new Map()
+  // Buffer of declarations, topologically sorted
+  newDeclarations: QuintDeclaration[] = []
 
   private modulesByName: Map<string, QuintModule>
   private lookupTable: LookupTable
@@ -79,22 +85,22 @@ class Flattener implements IRVisitor {
   }
 
   enterModule(_quintModule: QuintModule) {
-    // Reset `defsToAdd`
-    this.defsToAdd = new Map()
+    // Reset `newDeclarations`
+    this.newDeclarations = []
   }
 
   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)
-      }
-    })
+    quintModule.declarations = uniqBy(
+      this.newDeclarations.filter(d => d.kind !== 'import' && d.kind !== 'export'),
+      d => (isDef(d) ? d.name : d.id)
+    )
+  }
 
-    // Add the definitions to the module (mutating it)
-    quintModule.declarations.push(...this.defsToAdd.values())
+  exitDecl(decl: QuintDeclaration) {
+    // Add declarations to the buffer as they are visited. This way, new declarations are addded in between, allowing us
+    // to keep the topological order.
+    this.newDeclarations.push(decl)
   }
 
   enterName(name: QuintName) {
@@ -118,24 +124,24 @@ class Flattener implements IRVisitor {
         )
       }
 
-      if (this.defsToAdd.has(def.name)) {
-        // Already added
-        return
-      }
-
       const namespace = this.namespaceForNested ?? qualifier(decl)
       const newDef: QuintDef =
         namespace && !def.name.startsWith(namespace)
           ? addNamespaceToDefinition(def, namespace, new Set(builtinNames))
           : def
 
+      if (this.newDeclarations.some(d => isDef(d) && d.name === newDef.name)) {
+        // Already added
+        return
+      }
+
       // 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, newDefWithoutMetadata)
+      this.newDeclarations.push(newDefWithoutMetadata)
     })
   }
 
@@ -180,7 +186,12 @@ class Flattener implements IRVisitor {
         : def
 
     this.walkNested(namespace, newDef)
-    this.defsToAdd.set(newDef.name, newDef)
+    if (this.newDeclarations.some(d => isDef(d) && d.name === newDef.name)) {
+      // Already added
+      return
+    }
+
+    this.newDeclarations.push(newDef)
   }
 
   private walkNested(namespace: string | undefined, def: QuintDef) {

quint/src/flattening/fullFlattener.ts

@@ -17,13 +17,7 @@ import { IdGenerator } from '../idGenerator'
 import { moduleToString } from '../ir/IRprinting'
 import { FlatModule, QuintModule, isDef } from '../ir/quintIr'
 import { LookupTable } from '../names/base'
-import {
-  Loc,
-  ParserPhase3,
-  ParserPhase4,
-  parsePhase3importAndNameResolution,
-  parsePhase4toposort,
-} from '../parsing/quintParserFrontend'
+import { Loc, ParserPhase3, parsePhase3importAndNameResolution } from '../parsing/quintParserFrontend'
 import { AnalysisOutput } from '../quintAnalyzer'
 import { inlineTypeAliases } from '../types/aliasInliner'
 import { flattenModule } from './flattener'
@@ -97,7 +91,7 @@ export function flattenModules(
     // 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)
+    const result = resolveNamesOrThrow(flattenedModules.concat(modulesQueue), sourceMap)
 
     flattenedModules = result.modules.slice(0, flattenedModules.length)
     flattenedTable = result.table
@@ -117,17 +111,7 @@ function resolveNamesOrThrow(modules: QuintModule[], sourceMap: Map<bigint, Loc>
   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<bigint, Loc>): 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))
+    throw new Error('Internal error while flattening ' + result.value.map(e => e.explanation))
   }
 
   return result.unwrap()

quint/test/flattening/flattener.test.ts

@@ -8,7 +8,12 @@ import { SourceLookupPath } from '../../src/parsing/sourceResolver'
 import { parse } from '../../src/parsing/quintParserFrontend'
 
 describe('flattenModule', () => {
-  function getFlatennedDecls(baseDecls: string[], decls: string[], thirdModuleDecls: string[]): string[] {
+  function getFlatennedDecls(
+    baseDecls: string[],
+    decls: string[],
+    thirdModuleDecls: string[],
+    moduleToCheck: string = 'B'
+  ): string[] {
     const idGenerator = newIdGenerator()
     const fake_path: SourceLookupPath = { normalizedPath: 'fake_path', toSourceName: () => 'fake_path' }
 
@@ -27,7 +32,7 @@ describe('flattenModule', () => {
       const flattenedModule = flattenModule(m, modulesByName, table)
       modulesByName.set(m.name, flattenedModule)
     })
-    const flattenedModule = modulesByName.get('B')!
+    const flattenedModule = modulesByName.get(moduleToCheck)!
 
     return flattenedModule.declarations.map(decl => declarationToString(decl))
   }
@@ -40,7 +45,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['def f = ((x) => iadd(x, 1))', 'def g = ((x) => f(x))']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, [])
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('flattens import with qualifier', () => {
@@ -51,7 +56,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['def MyA::f = ((MyA::x) => iadd(MyA::x, 1))', 'val a = MyA::f(1)']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, [])
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('flattens import with self-qualifier', () => {
@@ -62,7 +67,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['def A::f = ((A::x) => iadd(A::x, 1))', 'val a = A::f(1)']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, [])
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('flattens export with previous import without definitions being used', () => {
@@ -76,7 +81,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['def f = ((x) => iadd(x, 1))']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, thirdModuleDecls)
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('flattens export with previous import with used definition', () => {
@@ -89,7 +94,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['def f = ((x) => iadd(x, 1))', 'val a = f(2)']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, thirdModuleDecls)
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('flattens export without previous import', () => {
@@ -102,7 +107,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['def f = ((x) => iadd(x, 1))']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, thirdModuleDecls)
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('does not flatten definitions that come from instance', () => {
@@ -113,7 +118,7 @@ describe('flattenModule', () => {
     const expectedDecls = decls
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, [])
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('flattens export qualified module with no qualifier', () => {
@@ -126,7 +131,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['def f = ((x) => iadd(x, 1))']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, thirdModuleDecls)
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('flattens export instance with no qualifier', () => {
@@ -142,7 +147,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['import A(N = 1) as A1', 'def f = ((x) => iadd(x, 1))']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, thirdModuleDecls)
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('imports definitions recursively when there are dependencies', () => {
@@ -153,7 +158,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['val MyA::z = 3', 'def MyA::f = ((MyA::x) => iadd(MyA::x, MyA::z))', 'val a = MyA::f(1)']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, [])
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('imports definitions recursively when there are dependencies in single def import', () => {
@@ -164,7 +169,7 @@ describe('flattenModule', () => {
     const expectedDecls = ['val z = 3', 'def f = ((x) => iadd(x, z))', 'val a = f(1)']
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, [])
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 
   it('does not create conflicts', () => {
@@ -177,11 +182,24 @@ describe('flattenModule', () => {
     const expectedDecls = [
       'val z = val x = 3 { x }',
       'def f = ((x) => iadd(x, z))',
-      'val a = def g = f { g(1) }',
       'val y = 1',
+      'val a = def g = f { g(1) }',
     ]
 
     const flattenedDecls = getFlatennedDecls(baseDecls, decls, thirdModuleDecls)
-    assert.sameDeepMembers(flattenedDecls, expectedDecls)
+    assert.deepEqual(flattenedDecls, expectedDecls)
+  })
+
+  it('can have definitions with same id but different name (#1141)', () => {
+    const baseDecls = ['val a = 1']
+
+    const decls = ['import A.*', 'val b = a']
+
+    const thirdModuleDecls = ['import A.*', 'import B', 'val c = a + B::b']
+
+    const expectedDecls = ['val a = 1', 'val B::a = 1', 'val B::b = B::a', 'val c = iadd(a, B::b)']
+
+    const flattenedDecls = getFlatennedDecls(baseDecls, decls, thirdModuleDecls, 'C')
+    assert.deepEqual(flattenedDecls, expectedDecls)
   })
 })

quint/test/flattening/fullFlattener.test.ts

@@ -2,7 +2,7 @@ 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 { parse, parsePhase3importAndNameResolution } from '../../src/parsing/quintParserFrontend'
 import { SourceLookupPath } from '../../src/parsing/sourceResolver'
 import { analyzeModules } from '../../src/quintAnalyzer'
 
@@ -31,10 +31,6 @@ describe('flattenModules', () => {
               [...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', () => {
@@ -215,4 +211,23 @@ describe('flattenModules', () => {
 
     assertFlattenedModule(text)
   })
+
+  describe('can have definitions with same id but different name (#1141)', () => {
+    const text = `module A {
+      val a = 1
+    }
+
+    module B {
+      import A.*
+      val b = a
+    }
+
+    module C {
+      import A.*
+      import B as B
+      val c = a + B::b
+    }`
+
+    assertFlattenedModule(text)
+  })
 })