Merge pull request #1191 from informalsystems/gabriela/fix-instance-c…

…onstant-callgraph

Add constant -> instance dependency to callgraph

CHANGELOG.md

@@ -16,6 +16,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fixed a problem where referencing constants from an instance could cause a crash (#1191)
+
 ### Security
 
 ## v0.14.3 -- 2023-09-19

quint/src/static/callgraph.ts

@@ -190,6 +190,9 @@ export class CallGraphVisitor implements IRVisitor {
     const importedModule = this.context.modulesByName.get(decl.protoName)
     if (importedModule) {
       this.graphAddAll(decl.id, Set([importedModule.id]))
+      decl.overrides.forEach(([_param, expr]) => {
+        this.graphAddAll(expr.id, Set([decl.id]))
+      })
     }
   }
 

quint/test/static/callgraph.test.ts

@@ -129,6 +129,7 @@ describe('compute call graph', () => {
       |  pure val myM = sqr(3)
       |  import B(M = myM) as B1
       |  pure val quadM = 2 * B1::doubleM
+      |  pure val constRef = B1::M
       |  export B1.*
       |}`
     )
@@ -148,12 +149,18 @@ describe('compute call graph', () => {
     const importB = findInstance(main, imp => imp.protoName === 'B')
     const quadM = findDef(main, 'quadM')
     const doubleM = findDef(B, 'doubleM')
+    const constRef = findDef(main, 'constRef')
     const exportB1 = findExport(main, exp => exp.protoName === 'B1')
 
     expect(graph.get(importA.id)?.toArray()).eql([A.id])
     expect(graph.get(myM.id)?.toArray()).to.eql([sqr.id, importA.id])
     expect(graph.get(importB.id)?.toArray()).to.eql([B.id, myM.id])
     expect(graph.get(quadM.id)?.toArray()).to.eql([doubleM.id, importB.id])
     expect(graph.get(exportB1.id)?.toArray()).to.eql([importB.id])
+
+    // Find the id for B1::M by checking the dependencies of constRef
+    // A regression for #1183, ensuring constants like B1::M depend on the instance statements
+    const B1Mid = graph.get(constRef.id)?.toArray()[0]!
+    expect(graph.get(B1Mid)?.toArray()).to.eql([importB.id])
   })
 })