Toposort on modules

CHANGELOG.md

@@ -18,6 +18,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - Produce proper error messages on invalid module name (#1260)
 - Fix JSON output when running multiple tests (#1264)
+- Topological sorting of modules (#1268)
 
 ### Security
 

quint/cli-tests.md

@@ -369,3 +369,10 @@ See [#1195](https://github.com/informalsystems/quint/issues/1195).
 <!-- !test exit 0 -->
 <!-- !test check test the default module -->
     quint test ./testFixture/_1050diffName.qnt
+
+### OK on parse 1108
+
+Regression test for [#1108](https://github.com/informalsystems/quint/issues/1108).
+
+<!-- !test check 1108 -->
+    quint parse testFixture/_1052one.qnt

quint/src/parsing/quintParserFrontend.ts

@@ -10,6 +10,7 @@
 
 import { CharStreams, CommonTokenStream } from 'antlr4ts'
 import { ParseTreeWalker } from 'antlr4ts/tree/ParseTreeWalker'
+import { Map as ImmutMap, Set as ImmutSet } from 'immutable'
 
 import { QuintLexer } from '../generated/QuintLexer'
 import * as p from '../generated/QuintParser'
@@ -171,36 +172,15 @@ export function parsePhase2sourceResolution(
   // Assign a rank to every module. The higher the rank,
   // the earlier the module should appear in the list of modules.
   sourceToModules.set(mainPath.normalizedPath, mainPhase1Result.modules)
-  const moduleRank = new Map<string, number>()
-  let maxModuleRank = 0
-  Array.from(mainPhase1Result.modules)
-    .reverse()
-    .forEach(m => moduleRank.set(m.name, maxModuleRank++))
   while (worklist.length > 0) {
     const [importer, pathTrail] = worklist.splice(0, 1)[0]
     for (const decl of importer.declarations) {
       if ((decl.kind === 'import' || decl.kind === 'instance') && decl.fromSource) {
         const importerPath = pathTrail[pathTrail.length - 1]
         const stemPath = sourceResolver.stempath(importerPath)
         const importeePath = sourceResolver.lookupPath(stemPath, decl.fromSource + '.qnt')
-        // check for import cycles
-        if (pathTrail.find(p => p.normalizedPath === importeePath.normalizedPath)) {
-          // found a cyclic dependency
-          const cycle = pathTrail
-            .concat([importeePath])
-            .map(p => `'${p.toSourceName()}'`)
-            .join(' imports ')
-          const err: QuintError = {
-            code: 'QNT098',
-            message: `Cyclic imports: ${cycle}`,
-            reference: decl.id,
-          }
-          return { ...mainPhase1Result, errors: mainPhase1Result.errors.concat([err]), sourceMap }
-        }
         if (sourceToModules.has(importeePath.normalizedPath)) {
-          // The source has been parsed already. Just push the module rank,
-          // for the modules to appear earlier.
-          sourceToModules.get(importeePath.normalizedPath)?.forEach(m => moduleRank.set(m.name, maxModuleRank++))
+          // The source has been parsed already.
           continue
         }
         // try to load the source code
@@ -222,7 +202,6 @@ export function parsePhase2sourceResolution(
           worklist.push([m, pathTrail.concat([importeePath])])
         })
         sourceToModules.set(importeePath.normalizedPath, newModules)
-        newModules.forEach(m => moduleRank.set(m.name, maxModuleRank++))
         sourceMap = new Map([...sourceMap, ...parseResult.sourceMap])
       }
     }
@@ -233,8 +212,86 @@ export function parsePhase2sourceResolution(
   for (const mods of sourceToModules.values()) {
     allModules = allModules.concat(mods)
   }
-  allModules.sort((m1, m2) => moduleRank.get(m2.name)! - moduleRank.get(m1.name)!)
-  return { ...mainPhase1Result, modules: allModules, sourceMap }
+  // sort the modules
+  const sortingResult = sortModules(allModules)
+
+  return {
+    ...mainPhase1Result,
+    errors: mainPhase1Result.errors.concat(sortingResult.errors),
+    modules: sortingResult.modules,
+    sourceMap,
+  }
+}
+
+/**
+ * Sort modules according to their imports, that is, importees should appear before importers.
+ * @param modules the modules to sort
+ * @return a structure that contains errors (if any were found) and the modules (sorted if no errors)
+ */
+function sortModules(modules: QuintModule[]): { errors: QuintError[]; modules: QuintModule[] } {
+  // iterate over the modules to construct:
+  //  - the map from module identifiers to modules
+  //  - the map from module names to modules
+  //  - the set of modules with duplicate names, if there are any
+  const [idToModule, nameToModule, duplicates] = modules.reduce(
+    ([idMap, namesMap, dups], mod) => {
+      const newIdMap = idMap.set(mod.id, mod)
+      const newNamesMap = namesMap.set(mod.name, mod)
+      const newDups = namesMap.has(mod.name) ? dups.add(mod) : dups
+      return [newIdMap, newNamesMap, newDups]
+    },
+    [ImmutMap<bigint, QuintModule>(), ImmutMap<string, QuintModule>(), ImmutSet<QuintModule>()]
+  )
+
+  if (!duplicates.isEmpty()) {
+    const errors: QuintError[] = duplicates.toArray().map(mod => {
+      return {
+        code: 'QNT101',
+        message: `Multiple modules conflict on the same name: ${mod.name}`,
+        reference: mod.id,
+      }
+    })
+    return { errors, modules }
+  }
+
+  // create the import graph
+  let edges = ImmutMap<bigint, ImmutSet<bigint>>()
+  for (const mod of modules) {
+    let imports = ImmutSet<bigint>()
+    for (const decl of mod.declarations) {
+      // We only keep track of imports and instances, but not of the exports:
+      //  - Exports flow in the opposite direction of imports.
+      //  - An export cannot be used without a corresponding import.
+      if (decl.kind === 'import' || decl.kind === 'instance') {
+        if (!nameToModule.has(decl.protoName)) {
+          const err: QuintError = {
+            code: 'QNT405',
+            message: `Module ${mod.name} imports an unknown module ${decl.protoName}`,
+            reference: decl.id,
+          }
+          return { errors: [err], modules }
+        }
+        imports = imports.add(nameToModule.get(decl.protoName)!.id)
+      }
+      // add all imports as the edges from mod
+      edges = edges.set(mod.id, imports)
+    }
+  }
+  // sort the modules with toposort
+  const result = toposort(edges, modules)
+  if (result.cycles.isEmpty()) {
+    return { errors: [], modules: result.sorted }
+  } else {
+    // note that the modules in the cycle are not always sorted according to the imports
+    const cycle = result.cycles.map(id => idToModule.get(id)?.name).join(', ')
+    const err: QuintError = {
+      code: 'QNT098',
+      message: `Cyclic imports among: ${cycle}`,
+      reference: result.cycles.first(),
+    }
+
+    return { errors: [err], modules }
+  }
 }
 
 /**

quint/test/effects/modeChecker.test.ts

@@ -11,16 +11,18 @@ describe('checkModes', () => {
   const baseDefs = ['var x: int', 'var y: bool']
 
   function checkMockedDefs(defs: string[]): [Map<bigint, QuintError>, Map<bigint, OpQualifier>] {
-    const text = `module A { const c: int }` + `module wrapper { ${baseDefs.concat(defs).join('\n')} }`
+    const text = `module A { const c: int } module wrapper { ${baseDefs.concat(defs).join('\n')} }`
     const { modules, table } = parseMockedModule(text)
+    const wrapper = modules.find(m => m.name === 'wrapper')!
 
     const inferrer = new EffectInferrer(table)
-    const [errors, effects] = inferrer.inferEffects(modules[1].declarations)
+    const [errors, effects] = inferrer.inferEffects(wrapper.declarations)
 
     assert.isEmpty(errors, `Should find no errors, found: ${[...errors.values()].map(errorTreeToString)}`)
 
     const modeChecker = new ModeChecker()
-    return modeChecker.checkModes(modules[1].declarations, effects)
+
+    return modeChecker.checkModes(wrapper.declarations, effects)
   }
 
   it('finds mode errors between action and def', () => {

quint/test/static/callgraph.test.ts

@@ -136,8 +136,8 @@ describe('compute call graph', () => {
     )
 
     const [modules, table] = parse3phases(code)
-
-    const [A, B, main] = modules
+    const findModule = (name: string) => modules.find(m => m.name === name)!
+    const [A, B, main] = ['A', 'B', 'main'].map(findModule)
     const visitor = new CallGraphVisitor(table, mkCallGraphContext(modules))
     walkModule(visitor, main)
     const graph = visitor.graph

quint/testFixture/_1010undefinedName.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":3,"name":"definedModule","declarations":[{"id":2,"kind":"def","name":"a","qualifier":"def","expr":{"id":1,"kind":"int","value":1}}]},{"id":8,"name":"undefinedName","declarations":[{"id":5,"kind":"def","name":"f","qualifier":"def","expr":{"id":4,"kind":"name","name":"S"}},{"id":6,"kind":"import","defName":"*","protoName":"undefinedModule"},{"id":7,"kind":"import","defName":"undefinedDefinition","protoName":"definedModule"}]}],"table":{},"errors":[{"explanation":"[QNT405] Module 'undefinedModule' not found","locs":[{"source":"mocked_path/testFixture/_1010undefinedName.qnt","start":{"line":8,"col":2,"index":139},"end":{"line":8,"col":25,"index":162}}]},{"explanation":"[QNT404] Name 'definedModule::undefinedDefinition' not found","locs":[{"source":"mocked_path/testFixture/_1010undefinedName.qnt","start":{"line":10,"col":2,"index":167},"end":{"line":10,"col":41,"index":206}}]},{"explanation":"[QNT404] Name 'S' not found","locs":[{"source":"mocked_path/testFixture/_1010undefinedName.qnt","start":{"line":6,"col":10,"index":134},"end":{"line":6,"col":10,"index":134}}]}]}
+{"stage":"parsing","warnings":[],"modules":[{"id":3,"name":"definedModule","declarations":[{"id":2,"kind":"def","name":"a","qualifier":"def","expr":{"id":1,"kind":"int","value":1}}]},{"id":8,"name":"undefinedName","declarations":[{"id":5,"kind":"def","name":"f","qualifier":"def","expr":{"id":4,"kind":"name","name":"S"}},{"id":6,"kind":"import","defName":"*","protoName":"undefinedModule"},{"id":7,"kind":"import","defName":"undefinedDefinition","protoName":"definedModule"}]}],"table":{},"errors":[{"explanation":"[QNT405] Module undefinedName imports an unknown module undefinedModule","locs":[{"source":"mocked_path/testFixture/_1010undefinedName.qnt","start":{"line":8,"col":2,"index":139},"end":{"line":8,"col":25,"index":162}}]},{"explanation":"[QNT405] Module 'undefinedModule' not found","locs":[{"source":"mocked_path/testFixture/_1010undefinedName.qnt","start":{"line":8,"col":2,"index":139},"end":{"line":8,"col":25,"index":162}}]},{"explanation":"[QNT404] Name 'definedModule::undefinedDefinition' not found","locs":[{"source":"mocked_path/testFixture/_1010undefinedName.qnt","start":{"line":10,"col":2,"index":167},"end":{"line":10,"col":41,"index":206}}]},{"explanation":"[QNT404] Name 'S' not found","locs":[{"source":"mocked_path/testFixture/_1010undefinedName.qnt","start":{"line":6,"col":10,"index":134},"end":{"line":6,"col":10,"index":134}}]}]}

quint/testFixture/_1026importCycleA.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":2,"name":"inCycleA","declarations":[{"id":1,"kind":"import","defName":"*","protoName":"inCycleB","fromSource":"./_1027importCycleB"}]}],"table":{},"errors":[{"explanation":"[QNT098] Cyclic imports: 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt'","locs":[{"source":"mocked_path/testFixture/_1028importCycleC.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]},{"explanation":"[QNT405] Module 'inCycleB' not found","locs":[{"source":"mocked_path/testFixture/_1026importCycleA.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
+{"stage":"parsing","warnings":[],"modules":[{"id":2,"name":"inCycleA","declarations":[{"id":1,"kind":"import","defName":"*","protoName":"inCycleB","fromSource":"./_1027importCycleB"}]},{"id":4,"name":"inCycleB","declarations":[{"id":3,"kind":"import","defName":"*","protoName":"inCycleC","fromSource":"./_1028importCycleC"}]},{"id":6,"name":"inCycleC","declarations":[{"id":5,"kind":"import","defName":"*","protoName":"inCycleA","fromSource":"./_1026importCycleA"}]}],"table":{},"errors":[{"explanation":"[QNT098] Cyclic imports among: inCycleA, inCycleB, inCycleC","locs":[{"source":"mocked_path/testFixture/_1026importCycleA.qnt","start":{"line":0,"col":0,"index":0},"end":{"line":2,"col":65,"index":65}}]},{"explanation":"[QNT405] Module 'inCycleB' not found","locs":[{"source":"mocked_path/testFixture/_1026importCycleA.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]},{"explanation":"[QNT405] Module 'inCycleC' not found","locs":[{"source":"mocked_path/testFixture/_1027importCycleB.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}

quint/testFixture/_1027importCycleB.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":2,"name":"inCycleB","declarations":[{"id":1,"kind":"import","defName":"*","protoName":"inCycleC","fromSource":"./_1028importCycleC"}]}],"table":{},"errors":[{"explanation":"[QNT098] Cyclic imports: 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt'","locs":[{"source":"mocked_path/testFixture/_1026importCycleA.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]},{"explanation":"[QNT405] Module 'inCycleC' not found","locs":[{"source":"mocked_path/testFixture/_1027importCycleB.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
+{"stage":"parsing","warnings":[],"modules":[{"id":2,"name":"inCycleB","declarations":[{"id":1,"kind":"import","defName":"*","protoName":"inCycleC","fromSource":"./_1028importCycleC"}]},{"id":4,"name":"inCycleC","declarations":[{"id":3,"kind":"import","defName":"*","protoName":"inCycleA","fromSource":"./_1026importCycleA"}]},{"id":6,"name":"inCycleA","declarations":[{"id":5,"kind":"import","defName":"*","protoName":"inCycleB","fromSource":"./_1027importCycleB"}]}],"table":{},"errors":[{"explanation":"[QNT098] Cyclic imports among: inCycleB, inCycleC, inCycleA","locs":[{"source":"mocked_path/testFixture/_1027importCycleB.qnt","start":{"line":0,"col":0,"index":0},"end":{"line":2,"col":65,"index":65}}]},{"explanation":"[QNT405] Module 'inCycleC' not found","locs":[{"source":"mocked_path/testFixture/_1027importCycleB.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]},{"explanation":"[QNT405] Module 'inCycleA' not found","locs":[{"source":"mocked_path/testFixture/_1028importCycleC.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}

quint/testFixture/_1028importCycleC.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":2,"name":"inCycleC","declarations":[{"id":1,"kind":"import","defName":"*","protoName":"inCycleA","fromSource":"./_1026importCycleA"}]}],"table":{},"errors":[{"explanation":"[QNT098] Cyclic imports: 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt'","locs":[{"source":"mocked_path/testFixture/_1027importCycleB.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]},{"explanation":"[QNT405] Module 'inCycleA' not found","locs":[{"source":"mocked_path/testFixture/_1028importCycleC.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
+{"stage":"parsing","warnings":[],"modules":[{"id":2,"name":"inCycleC","declarations":[{"id":1,"kind":"import","defName":"*","protoName":"inCycleA","fromSource":"./_1026importCycleA"}]},{"id":4,"name":"inCycleA","declarations":[{"id":3,"kind":"import","defName":"*","protoName":"inCycleB","fromSource":"./_1027importCycleB"}]},{"id":6,"name":"inCycleB","declarations":[{"id":5,"kind":"import","defName":"*","protoName":"inCycleC","fromSource":"./_1028importCycleC"}]}],"table":{},"errors":[{"explanation":"[QNT098] Cyclic imports among: inCycleC, inCycleA, inCycleB","locs":[{"source":"mocked_path/testFixture/_1028importCycleC.qnt","start":{"line":0,"col":0,"index":0},"end":{"line":2,"col":65,"index":65}}]},{"explanation":"[QNT405] Module 'inCycleA' not found","locs":[{"source":"mocked_path/testFixture/_1028importCycleC.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]},{"explanation":"[QNT405] Module 'inCycleB' not found","locs":[{"source":"mocked_path/testFixture/_1026importCycleA.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}

quint/testFixture/_1052one.qnt

@@ -0,0 +1,11 @@
+module one {
+    type Foo = int
+}
+
+module onePrime {
+    import one.*
+    import two.* from "./_1053two"
+
+    var a: Boo
+    var b: Foo
+}

quint/testFixture/_1053two.qnt

@@ -0,0 +1,12 @@
+module two {
+    type Boo = int
+}
+
+
+module twoPrime {
+    import one.* from "./_1052one"
+    import two.*
+
+    var c: Boo
+    var d: Foo
+}

quint/testFixture/modulesAndJunk.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":4,"name":"foo","declarations":[{"id":3,"kind":"def","name":"x","qualifier":"val","expr":{"id":2,"kind":"int","value":1}}]},{"id":13,"name":"bar","declarations":[{"id":12,"kind":"def","name":"baz","qualifier":"def","expr":{"id":12,"kind":"lambda","params":[{"id":5,"name":"x"}],"qualifier":"def","expr":{"id":10,"kind":"app","opcode":"iadd","args":[{"id":8,"kind":"name","name":"x"},{"id":9,"kind":"int","value":1}]}},"typeAnnotation":{"id":11,"kind":"oper","args":[{"id":6,"kind":"int"}],"res":{"id":7,"kind":"int"}}}]}],"table":{"8":{"id":5,"name":"x","kind":"param"}},"errors":[{"explanation":"[QNT000] extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/modulesAndJunk.qnt","start":{"line":8,"col":0,"index":75},"end":{"line":8,"col":2,"index":77}}]}]}
+{"stage":"parsing","warnings":[],"modules":[{"id":13,"name":"bar","declarations":[{"id":12,"kind":"def","name":"baz","qualifier":"def","expr":{"id":12,"kind":"lambda","params":[{"id":5,"name":"x"}],"qualifier":"def","expr":{"id":10,"kind":"app","opcode":"iadd","args":[{"id":8,"kind":"name","name":"x"},{"id":9,"kind":"int","value":1}]}},"typeAnnotation":{"id":11,"kind":"oper","args":[{"id":6,"kind":"int"}],"res":{"id":7,"kind":"int"}}}]},{"id":4,"name":"foo","declarations":[{"id":3,"kind":"def","name":"x","qualifier":"val","expr":{"id":2,"kind":"int","value":1}}]}],"table":{"8":{"id":5,"name":"x","kind":"param"}},"errors":[{"explanation":"[QNT000] extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/modulesAndJunk.qnt","start":{"line":8,"col":0,"index":75},"end":{"line":8,"col":2,"index":77}}]}]}