Use stmt.location.method instead of stmt.method (#312)

Lipen · web-flow · commit c5b7794bd4c9 · 2025-07-31T16:41:27.000+03:00
diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "d7dd9d343b"
+    const val jacodb = "081adc271e"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"
diff --git a/usvm-dataflow/src/main/kotlin/org/usvm/dataflow/ifds/Vertex.kt b/usvm-dataflow/src/main/kotlin/org/usvm/dataflow/ifds/Vertex.kt
@@ -24,7 +24,7 @@ data class Vertex<out Fact, out Statement : CommonInst>(
     val fact: Fact,
 ) {
     val method: CommonMethod
-        get() = statement.method
+        get() = statement.location.method
 
     override fun toString(): String {
         return "$fact at $statement in $method"
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt
@@ -23,7 +23,7 @@ interface JcTransparentInstruction : JcInst {
  * Auxiliary instruction to handle method calls.
  * */
 sealed interface JcMethodCallBaseInst : JcTransparentInstruction {
-    override val method: JcMethod
+    val method: JcMethod
 
     override val operands: List<JcExpr>
         get() = emptyList()
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt
@@ -80,13 +80,13 @@ class EtsApplicationGraphImpl(
 ) : EtsApplicationGraph {
 
     override fun predecessors(node: EtsStmt): Sequence<EtsStmt> {
-        val graph = node.method.flowGraph()
+        val graph = node.location.method.flowGraph()
         val predecessors = graph.predecessors(node)
         return predecessors.asSequence()
     }
 
     override fun successors(node: EtsStmt): Sequence<EtsStmt> {
-        val graph = node.method.flowGraph()
+        val graph = node.location.method.flowGraph()
         val successors = graph.successors(node)
         return successors.asSequence()
     }
@@ -139,8 +139,8 @@ class EtsApplicationGraphImpl(
         val callee = expr.callee
 
         // Note: the resolving code below expects that at least the current method signature is known.
-        check(node.method.signature.enclosingClass.isIdeal()) {
-            "Incomplete signature in method: ${node.method}"
+        check(node.location.method.signature.enclosingClass.isIdeal()) {
+            "Incomplete signature in method: ${node.location.method}"
         }
 
         // Note: specific resolve for constructor:
@@ -223,17 +223,17 @@ class EtsApplicationGraphImpl(
         // If the callee signature is not ideal, resolve it via a partial match...
         check(!callee.enclosingClass.isIdeal())
 
-        val cls = lookupClassWithIdealSignature(node.method.signature.enclosingClass).let {
+        val cls = lookupClassWithIdealSignature(node.location.method.signature.enclosingClass).let {
             if (it.isNone) {
-                error("Could not find the enclosing class: ${node.method.enclosingClass}")
+                error("Could not find the enclosing class: ${node.location.method.enclosingClass}")
             }
             it.getOrThrow()
         }
 
         // If the complete signature match failed,
         // try to find the unique not-the-same neighbour method in the same class:
         val neighbors = classMethodsByName[cls.signature].orEmpty()[callee.name].orEmpty()
-            .filterNot { it.name == node.method.name }
+            .filterNot { it.name == node.location.method.name }
         if (neighbors.isNotEmpty()) {
             val s = neighbors.singleOrNull()
                 ?: error("Multiple methods with the same name: $neighbors")
@@ -260,7 +260,7 @@ class EtsApplicationGraphImpl(
             .filterNot {
                 compareClassSignatures(
                     it.signature.enclosingClass,
-                    node.method.signature.enclosingClass
+                    node.location.method.signature.enclosingClass
                 ) != ComparisonResult.NotEqual
             }
             .toList()
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt
@@ -16,6 +16,7 @@ import org.usvm.dataflow.ts.graph.EtsApplicationGraph
 import org.usvm.dataflow.ts.infer.AnalyzerEvent
 import org.usvm.dataflow.ts.infer.TypeInferenceManager
 import org.usvm.dataflow.ts.util.EtsTraits
+import org.usvm.dataflow.ts.util.etsMethod
 
 class EtsIfdsRunner<Fact, Event : AnalyzerEvent>(
     override val graph: EtsApplicationGraph,
@@ -82,6 +83,6 @@ class EtsIfdsRunner<Fact, Event : AnalyzerEvent>(
         val (endStmt, endFact) = endVertex
 
         val localPathEdge = EtsIfdsMethodRunner.PathEdge(endStmt.location.index, endFact)
-        getMethodRunner(startVertex.statement.method).getSourceRunner(startVertex).propagate(localPathEdge)
+        getMethodRunner(startVertex.etsMethod).getSourceRunner(startVertex).propagate(localPathEdge)
     }
 }
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsSourceRunner.kt
@@ -5,6 +5,7 @@ import org.usvm.dataflow.ifds.Edge
 import org.usvm.dataflow.ifds.Vertex
 import org.usvm.dataflow.ts.ifds.EtsIfdsMethodRunner.PathEdge
 import org.usvm.dataflow.ts.util.EtsTraits
+import org.usvm.dataflow.ts.util.etsMethod
 
 internal class EtsIfdsSourceRunner<Fact>(
     val traits: EtsTraits,
@@ -112,7 +113,7 @@ internal class EtsIfdsSourceRunner<Fact>(
                 // Propagate through the summary edge:
                 for (callerPathEdge in callerPathEdges) {
                     val summaryEdge = Edge(startVertex, currentVertex)
-                    val caller = callerPathEdge.from.statement.method
+                    val caller = callerPathEdge.from.etsMethod
                     val callerRunner = methodRunner.commonRunner.getMethodRunner(caller)
                     callerRunner.handleSummaryEdgeInCaller(currentEdge = callerPathEdge, summaryEdge = summaryEdge)
                 }
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ApplicationGraph.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ApplicationGraph.kt
@@ -53,7 +53,7 @@ class EtsApplicationGraphWithExplicitEntryPoint(
     override fun successors(node: EtsStmt): Sequence<EtsStmt> {
         if (node.location.index == -1) {
             require(node is EtsNopStmt)
-            return graph.entryPoints(node.method)
+            return graph.entryPoints(node.location.method)
         }
         return graph.successors(node)
     }
@@ -64,7 +64,7 @@ class EtsApplicationGraphWithExplicitEntryPoint(
             return emptySequence()
         }
         if (node.location.index == 0) {
-            return entryPoints(node.method)
+            return entryPoints(node.location.method)
         }
         return graph.predecessors(node)
     }
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt
@@ -53,7 +53,7 @@ class BackwardFlowFunctions(
                 return@FlowFunction listOf(fact)
             }
         }
-        val liveVars = liveVariables(current.method)
+        val liveVars = liveVariables(current.location.method)
         when (fact) {
             Zero -> sequentZero(current)
             is TypedVariable -> sequentTypedVariable(current, fact).filter {
@@ -82,7 +82,7 @@ class BackwardFlowFunctions(
             // ∅ |= x:unknown
             val returnValue = current.returnValue ?: return listOf(Zero)
             val type = if (doAddKnownTypes) {
-                val knownType = returnValue.tryGetKnownType(current.method)
+                val knownType = returnValue.tryGetKnownType(current.location.method)
                 EtsTypeFact.from(knownType).fixAnyToUnknown()
             } else {
                 EtsTypeFact.UnknownEtsTypeFact
@@ -103,7 +103,7 @@ class BackwardFlowFunctions(
                 // Case `x... := y`
                 // ∅ |= y:unknown
                 val type = if (doAddKnownTypes) {
-                    val knownType = current.rhv.tryGetKnownType(current.method)
+                    val knownType = current.rhv.tryGetKnownType(current.location.method)
                     EtsTypeFact.from(knownType).fixAnyToUnknown()
                 } else {
                     EtsTypeFact.UnknownEtsTypeFact
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt
@@ -34,8 +34,8 @@ class ForwardAnalyzer(
     private fun variableIsDying(fact: ForwardTypeDomainFact, stmt: EtsStmt): Boolean {
         if (fact !is ForwardTypeDomainFact.TypedVariable) return false
         return when (val base = fact.variable.base) {
-            is AccessPathBase.Local -> !flowFunctions.liveVariables(stmt.method).isAliveAt(base.name, stmt)
-            is AccessPathBase.Arg -> !flowFunctions.liveVariables(stmt.method).isAliveAt("arg(${base.index})", stmt)
+            is AccessPathBase.Local -> !flowFunctions.liveVariables(stmt.location.method).isAliveAt(base.name, stmt)
+            is AccessPathBase.Arg -> !flowFunctions.liveVariables(stmt.location.method).isAliveAt("arg(${base.index})", stmt)
             else -> false
         }
     }
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt
@@ -167,7 +167,7 @@ class ForwardFlowFunctions(
         when (fact) {
             Zero -> sequentZero(current)
             is TypedVariable -> {
-                val liveVars = liveVariables(current.method)
+                val liveVars = liveVariables(current.location.method)
                 sequentFact(current, fact).myFilter()
                     .filter {
                         when (val base = it.variable.base) {
@@ -184,7 +184,7 @@ class ForwardFlowFunctions(
 
         val lhv = current.lhv.toPath()
         val result = mutableListOf<ForwardTypeDomainFact>(Zero)
-        val preAliases = getAliases(current.method)[current.location.index]
+        val preAliases = getAliases(current.location.method)[current.location.index]
 
         fun addTypeFactWithAliases(path: AccessPath, type: EtsTypeFact) {
             result += TypedVariable(path, type)
@@ -193,7 +193,7 @@ class ForwardFlowFunctions(
                 val base = AccessPath(path.base, emptyList())
                 val aliases = preAliases.getAliases(base).filter {
                     when (val b = it.base) {
-                        is AccessPathBase.Local -> liveVariables(current.method).isAliveAt(b.name, current)
+                        is AccessPathBase.Local -> liveVariables(current.location.method).isAliveAt(b.name, current)
                         else -> true
                     }
                 }
@@ -302,7 +302,7 @@ class ForwardFlowFunctions(
             }
         }
 
-        val preAliases = getAliases(current.method)[current.location.index]
+        val preAliases = getAliases(current.location.method)[current.location.index]
 
         // Override LHS when RHS is const-like:
         if (rhv == null) {
@@ -479,7 +479,7 @@ class ForwardFlowFunctions(
 
                         val aliases = preAliases.getAliases(x).filter {
                             when (val b = it.base) {
-                                is AccessPathBase.Local -> liveVariables(current.method).isAliveAt(b.name, current)
+                                is AccessPathBase.Local -> liveVariables(current.location.method).isAliveAt(b.name, current)
                                 else -> true
                             }
                         }
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/Utils.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/Utils.kt
@@ -18,7 +18,11 @@ package org.usvm.dataflow.ts.util
 
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsType
+import org.usvm.dataflow.ifds.Edge
+import org.usvm.dataflow.ifds.Vertex
 import org.usvm.dataflow.ts.infer.EtsTypeFact
 
 fun EtsType.unwrapPromise(): EtsType {
@@ -57,3 +61,9 @@ fun <T> T.toStringLimited(): String {
 
 val EtsClass.type: EtsClassType
     get() = EtsClassType(signature, typeParameters)
+
+val Vertex<*, EtsStmt>.etsMethod: EtsMethod
+    get() = statement.location.method
+
+val Edge<*, EtsStmt>.etsMethod: EtsMethod
+    get() = from.etsMethod
diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt b/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt
@@ -16,19 +16,19 @@ class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver<TsState>
     lateinit var result: Map<EtsMethod, List<UncoveredIfSuccessors>>
 
     override fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, scope: TsStepScope) {
-        val ifStmts = uncoveredSuccessorsOfVisitedIfStmts.getOrPut(stmt.method) { mutableMapOf() }
+        val ifStmts = uncoveredSuccessorsOfVisitedIfStmts.getOrPut(stmt.location.method) { mutableMapOf() }
         // We've already added its successors in the map
         if (stmt in ifStmts) return
 
-        val successors = stmt.method.cfg.successors(stmt)
+        val successors = stmt.location.method.cfg.successors(stmt)
         ifStmts[stmt] = successors.toMutableSet()
     }
 
     override fun onState(parent: TsState, forks: Sequence<TsState>) {
         val previousStatement = parent.pathNode.parent?.statement
         if (previousStatement !is EtsIfStmt) return
 
-        val method = parent.currentStatement.method
+        val method = parent.currentStatement.location.method
         val remainingUncoveredIfSuccessors = uncoveredSuccessorsOfVisitedIfStmts.getValue(method)
         val remainingSuccessorsForCurrentIf = remainingUncoveredIfSuccessors[previousStatement]
             ?: return // No uncovered successors for this if statement

Original file line number	Diff line number	Diff line change
`@@ -16,6 +16,7 @@ import org.usvm.dataflow.ts.graph.EtsApplicationGraph`
`16`	`16`	`import org.usvm.dataflow.ts.infer.AnalyzerEvent`
`17`	`17`	`import org.usvm.dataflow.ts.infer.TypeInferenceManager`
`18`	`18`	`import org.usvm.dataflow.ts.util.EtsTraits`
	`19`	`+import org.usvm.dataflow.ts.util.etsMethod`
`19`	`20`
`20`	`21`	`class EtsIfdsRunner<Fact, Event : AnalyzerEvent>(`
`21`	`22`	`override val graph: EtsApplicationGraph,`
`@@ -82,6 +83,6 @@ class EtsIfdsRunner<Fact, Event : AnalyzerEvent>(`
`82`	`83`	`val (endStmt, endFact) = endVertex`
`83`	`84`
`84`	`85`	`val localPathEdge = EtsIfdsMethodRunner.PathEdge(endStmt.location.index, endFact)`
`85`		`- getMethodRunner(startVertex.statement.method).getSourceRunner(startVertex).propagate(localPathEdge)`
	`86`	`+ getMethodRunner(startVertex.etsMethod).getSourceRunner(startVertex).propagate(localPathEdge)`
`86`	`87`	`}`
`87`	`88`	`}`
Original file line number	Diff line number	Diff line change
`@@ -53,7 +53,7 @@ class EtsApplicationGraphWithExplicitEntryPoint(`
`53`	`53`	`override fun successors(node: EtsStmt): Sequence<EtsStmt> {`
`54`	`54`	`if (node.location.index == -1) {`
`55`	`55`	`require(node is EtsNopStmt)`
`56`		`- return graph.entryPoints(node.method)`
	`56`	`+ return graph.entryPoints(node.location.method)`
`57`	`57`	`}`
`58`	`58`	`return graph.successors(node)`
`59`	`59`	`}`
`@@ -64,7 +64,7 @@ class EtsApplicationGraphWithExplicitEntryPoint(`
`64`	`64`	`return emptySequence()`
`65`	`65`	`}`
`66`	`66`	`if (node.location.index == 0) {`
`67`		`- return entryPoints(node.method)`
	`67`	`+ return entryPoints(node.location.method)`
`68`	`68`	`}`
`69`	`69`	`return graph.predecessors(node)`
`70`	`70`	`}`
Original file line number	Diff line number	Diff line change
`@@ -34,8 +34,8 @@ class ForwardAnalyzer(`
`34`	`34`	`private fun variableIsDying(fact: ForwardTypeDomainFact, stmt: EtsStmt): Boolean {`
`35`	`35`	`if (fact !is ForwardTypeDomainFact.TypedVariable) return false`
`36`	`36`	`return when (val base = fact.variable.base) {`
`37`		`- is AccessPathBase.Local -> !flowFunctions.liveVariables(stmt.method).isAliveAt(base.name, stmt)`
`38`		`- is AccessPathBase.Arg -> !flowFunctions.liveVariables(stmt.method).isAliveAt("arg(${base.index})", stmt)`
	`37`	`+ is AccessPathBase.Local -> !flowFunctions.liveVariables(stmt.location.method).isAliveAt(base.name, stmt)`
	`38`	`+ is AccessPathBase.Arg -> !flowFunctions.liveVariables(stmt.location.method).isAliveAt("arg(${base.index})", stmt)`
`39`	`39`	`else -> false`
`40`	`40`	`}`
`41`	`41`	`}`