Switch to a new ETS model

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 = "6ec737ce76"
+    const val jacodb = "3b6a17f000"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-ts-dataflow/build.gradle.kts

@@ -16,6 +16,7 @@ dependencies {
 
     api(Libs.jacodb_api_common)
     api(Libs.jacodb_ets)
+    implementation(Libs.jacodb_core)
     implementation(Libs.jacodb_taint_configuration)
     implementation(Libs.kotlinx_collections)
     implementation(Libs.kotlinx_serialization_json)

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/BackwardGraph.kt

@@ -16,9 +16,9 @@
 
 package org.usvm.dataflow.ts.graph
 
-import org.jacodb.ets.base.EtsStmt
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsStmt
 
 private class BackwardEtsApplicationGraphImpl(
     val forward: EtsApplicationGraph,

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt

@@ -17,19 +17,20 @@
 package org.usvm.dataflow.ts.graph
 
 import mu.KotlinLogging
-import org.jacodb.ets.base.CONSTRUCTOR_NAME
-import org.jacodb.ets.base.EtsAssignStmt
-import org.jacodb.ets.base.EtsClassType
-import org.jacodb.ets.base.EtsNewExpr
-import org.jacodb.ets.base.EtsStmt
-import org.jacodb.ets.base.UNKNOWN_FILE_NAME
+import org.jacodb.ets.model.EtsAssignStmt
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsFileSignature
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsNewExpr
+import org.jacodb.ets.model.EtsNopStmt
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.Maybe
+import org.jacodb.ets.utils.UNKNOWN_FILE_NAME
 import org.jacodb.ets.utils.callExpr
 import org.jacodb.ets.utils.onSome
 import org.usvm.dataflow.graph.ApplicationGraph
@@ -136,10 +137,10 @@
     override fun callees(node: EtsStmt): Sequence<EtsMethod> {
         val expr = node.callExpr ?: return emptySequence()
 
-        val callee = expr.method
+        val callee = expr.callee
 
         // Note: the resolving code below expects that at least the current method signature is known.
-        check(node.method.enclosingClass.isIdeal()) {
+        check(node.method.signature.enclosingClass.isIdeal()) {
             "Incomplete signature in method: ${node.method}"
         }
 
@@ -154,7 +155,7 @@
                 }
 
                 if (prevStmt is EtsAssignStmt && prevStmt.rhv is EtsNewExpr) {
-                    val cls = prevStmt.rhv.type
+                    val cls = (prevStmt.rhv as EtsNewExpr).type
                     if (cls !is EtsClassType) {
                         return emptySequence()
                     }
@@ -223,7 +224,7 @@
         // If the callee signature is not ideal, resolve it via a partial match...
         check(!callee.enclosingClass.isIdeal())
 
-        val cls = lookupClassWithIdealSignature(node.method.enclosingClass).let {
+        val cls = lookupClassWithIdealSignature(node.method.signature.enclosingClass).let {
             if (it.isNone) {
                 error("Could not find the enclosing class: ${node.method.enclosingClass}")
             }
@@ -250,10 +251,18 @@
         // try to *uniquely* resolve the callee via a partial signature match:
         val resolved = projectMethodsByName[callee.name].orEmpty()
             .asSequence()
-            .filter { compareClassSignatures(it.enclosingClass, callee.enclosingClass) != ComparisonResult.NotEqual }
+            .filter {
+                compareClassSignatures(
+                    it.signature.enclosingClass,
+                    callee.enclosingClass
+                ) != ComparisonResult.NotEqual
+            }
             // Note: exclude current class:
             .filterNot {
-                compareClassSignatures(it.enclosingClass, node.method.enclosingClass) != ComparisonResult.NotEqual
+                compareClassSignatures(
+                    it.signature.enclosingClass,
+                    node.method.signature.enclosingClass
+                ) != ComparisonResult.NotEqual
             }
             .toList()
         if (resolved.isEmpty()) {

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt

@@ -1,17 +1,17 @@
 package org.usvm.dataflow.ts.infer
 
-import org.jacodb.ets.base.EtsArrayAccess
-import org.jacodb.ets.base.EtsAwaitExpr
-import org.jacodb.ets.base.EtsCastExpr
-import org.jacodb.ets.base.EtsConstant
-import org.jacodb.ets.base.EtsEntity
-import org.jacodb.ets.base.EtsInstanceFieldRef
-import org.jacodb.ets.base.EtsLocal
-import org.jacodb.ets.base.EtsParameterRef
-import org.jacodb.ets.base.EtsStaticFieldRef
-import org.jacodb.ets.base.EtsThis
-import org.jacodb.ets.base.EtsValue
+import org.jacodb.ets.model.EtsArrayAccess
+import org.jacodb.ets.model.EtsAwaitExpr
+import org.jacodb.ets.model.EtsCastExpr
 import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsConstant
+import org.jacodb.ets.model.EtsEntity
+import org.jacodb.ets.model.EtsInstanceFieldRef
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsParameterRef
+import org.jacodb.ets.model.EtsStaticFieldRef
+import org.jacodb.ets.model.EtsThis
+import org.jacodb.ets.model.EtsValue
 
 data class AccessPath(val base: AccessPathBase, val accesses: List<Accessor>) {
     operator fun plus(accessor: Accessor) = AccessPath(base, accesses + accessor)

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt

@@ -1,27 +1,27 @@
 package org.usvm.dataflow.ts.infer
 
 import mu.KotlinLogging
-import org.jacodb.ets.base.EtsArrayAccess
-import org.jacodb.ets.base.EtsAssignStmt
-import org.jacodb.ets.base.EtsBinaryExpr
-import org.jacodb.ets.base.EtsCallExpr
-import org.jacodb.ets.base.EtsCallStmt
-import org.jacodb.ets.base.EtsCastExpr
-import org.jacodb.ets.base.EtsConstant
-import org.jacodb.ets.base.EtsEntity
-import org.jacodb.ets.base.EtsInstanceCallExpr
-import org.jacodb.ets.base.EtsInstanceFieldRef
-import org.jacodb.ets.base.EtsInstanceOfExpr
-import org.jacodb.ets.base.EtsLocal
-import org.jacodb.ets.base.EtsNewArrayExpr
-import org.jacodb.ets.base.EtsNewExpr
-import org.jacodb.ets.base.EtsParameterRef
-import org.jacodb.ets.base.EtsStaticFieldRef
-import org.jacodb.ets.base.EtsStmt
-import org.jacodb.ets.base.EtsThis
-import org.jacodb.ets.base.EtsUnaryExpr
+import org.jacodb.ets.model.EtsArrayAccess
+import org.jacodb.ets.model.EtsAssignStmt
+import org.jacodb.ets.model.EtsBinaryExpr
+import org.jacodb.ets.model.EtsCallExpr
+import org.jacodb.ets.model.EtsCallStmt
+import org.jacodb.ets.model.EtsCastExpr
 import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsConstant
+import org.jacodb.ets.model.EtsEntity
+import org.jacodb.ets.model.EtsInstanceCallExpr
+import org.jacodb.ets.model.EtsInstanceFieldRef
+import org.jacodb.ets.model.EtsInstanceOfExpr
+import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsNewArrayExpr
+import org.jacodb.ets.model.EtsNewExpr
+import org.jacodb.ets.model.EtsParameterRef
+import org.jacodb.ets.model.EtsStaticFieldRef
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsThis
+import org.jacodb.ets.model.EtsUnaryExpr
 import org.usvm.dataflow.ts.infer.MethodAliasInfoImpl.Allocation
 
 private val logger = KotlinLogging.logger {}
@@ -425,7 +425,7 @@ class MethodAliasInfoImpl(
 
             is EtsInstanceCallExpr -> {
                 initEntity(entity.instance)
-                newString(entity.method.name)
+                newString(entity.callee.name)
                 entity.args.forEach { initEntity(it) }
             }
         }
@@ -516,7 +516,7 @@ class MethodAliasInfoImpl(
             }
         }
 
-        val root = method.cfg.stmts[0]
+        val root = method.cfg.stmts.first()
         postOrderDfs(root)
         order.reverse()
 

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt

@@ -1,7 +1,7 @@
 package org.usvm.dataflow.ts.infer
 
-import org.jacodb.ets.base.EtsStmt
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsStmt
 import org.usvm.dataflow.ifds.Vertex
 
 sealed interface AnalyzerEvent

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ApplicationGraph.kt

@@ -16,11 +16,11 @@
 
 package org.usvm.dataflow.ts.infer
 
-import org.jacodb.ets.base.EtsInstLocation
-import org.jacodb.ets.base.EtsNopStmt
-import org.jacodb.ets.base.EtsStmt
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsNopStmt
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsStmtLocation
 import org.usvm.dataflow.ts.graph.EtsApplicationGraph
 import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl
 
@@ -41,8 +41,8 @@ class EtsApplicationGraphWithExplicitEntryPoint(
 
     override fun exitPoints(method: EtsMethod): Sequence<EtsStmt> = graph.exitPoints(method)
 
-    private fun methodEntryPoint(method: EtsMethod) =
-        EtsNopStmt(EtsInstLocation(method, index = -1))
+    private fun methodEntryPoint(method: EtsMethod): EtsStmt =
+        EtsNopStmt(EtsStmtLocation(method, index = -1))
 
     override fun entryPoints(method: EtsMethod): Sequence<EtsStmt> = sequenceOf(methodEntryPoint(method))
 
@@ -51,28 +51,21 @@ class EtsApplicationGraphWithExplicitEntryPoint(
     override fun callees(node: EtsStmt): Sequence<EtsMethod> = graph.callees(node)
 
     override fun successors(node: EtsStmt): Sequence<EtsStmt> {
-        val method = methodOf(node)
-        val methodEntry = methodEntryPoint(method)
-
-        if (node == methodEntry) {
-            return graph.entryPoints(method)
+        if (node.location.index == -1) {
+            require(node is EtsNopStmt)
+            return graph.entryPoints(node.method)
         }
-
         return graph.successors(node)
     }
 
     override fun predecessors(node: EtsStmt): Sequence<EtsStmt> {
-        val method = methodOf(node)
-        val methodEntry = methodEntryPoint(method)
-
-        if (node == methodEntry) {
+        if (node.location.index == -1) {
+            require(node is EtsNopStmt)
             return emptySequence()
         }
-
-        if (node in graph.entryPoints(method)) {
-            return sequenceOf(methodEntry)
+        if (node.location.index == 0) {
+            return entryPoints(node.method)
         }
-
         return graph.predecessors(node)
     }
 }

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt

@@ -1,10 +1,9 @@
 package org.usvm.dataflow.ts.infer
 
-import org.jacodb.ets.base.EtsStmt
-import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsType
 import org.jacodb.impl.cfg.graphs.GraphDominators
-import org.usvm.dataflow.graph.ApplicationGraph
 import org.usvm.dataflow.ifds.Analyzer
 import org.usvm.dataflow.ifds.Edge
 import org.usvm.dataflow.ifds.Vertex

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt

@@ -1,28 +1,27 @@
 package org.usvm.dataflow.ts.infer
 
 import mu.KotlinLogging
-import org.jacodb.ets.base.EtsArrayAccess
-import org.jacodb.ets.base.EtsAssignStmt
-import org.jacodb.ets.base.EtsCastExpr
-import org.jacodb.ets.base.EtsEntity
-import org.jacodb.ets.base.EtsEqExpr
-import org.jacodb.ets.base.EtsFieldRef
-import org.jacodb.ets.base.EtsIfStmt
-import org.jacodb.ets.base.EtsInExpr
-import org.jacodb.ets.base.EtsInstanceCallExpr
-import org.jacodb.ets.base.EtsLValue
-import org.jacodb.ets.base.EtsLocal
-import org.jacodb.ets.base.EtsNewExpr
-import org.jacodb.ets.base.EtsNumberConstant
-import org.jacodb.ets.base.EtsParameterRef
-import org.jacodb.ets.base.EtsReturnStmt
-import org.jacodb.ets.base.EtsStmt
-import org.jacodb.ets.base.EtsStringConstant
-import org.jacodb.ets.base.EtsThis
-import org.jacodb.ets.base.EtsThrowStmt
-import org.jacodb.ets.base.EtsType
-import org.jacodb.ets.base.EtsValue
+import org.jacodb.ets.model.EtsArrayAccess
+import org.jacodb.ets.model.EtsAssignStmt
+import org.jacodb.ets.model.EtsCastExpr
+import org.jacodb.ets.model.EtsEntity
+import org.jacodb.ets.model.EtsEqExpr
+import org.jacodb.ets.model.EtsFieldRef
+import org.jacodb.ets.model.EtsIfStmt
+import org.jacodb.ets.model.EtsInExpr
+import org.jacodb.ets.model.EtsInstanceCallExpr
+import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsNewExpr
+import org.jacodb.ets.model.EtsNumberConstant
+import org.jacodb.ets.model.EtsParameterRef
+import org.jacodb.ets.model.EtsReturnStmt
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsStringConstant
+import org.jacodb.ets.model.EtsThis
+import org.jacodb.ets.model.EtsThrowStmt
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsValue
 import org.jacodb.ets.utils.callExpr
 import org.jacodb.impl.cfg.graphs.GraphDominators
 import org.usvm.dataflow.ifds.FlowFunction
@@ -212,7 +211,8 @@ class BackwardFlowFunctions(
             if (returnValue != null) {
                 val variable = returnValue.toBase()
                 val type = if (doAddKnownTypes) {
-                    EtsTypeFact.from(returnValue.type).fixAnyToUnknown()
+                    val knownType = returnValue.tryGetKnownType(current.method)
+                    EtsTypeFact.from(knownType).fixAnyToUnknown()
                 } else {
                     EtsTypeFact.UnknownEtsTypeFact
                 }
@@ -241,14 +241,8 @@ class BackwardFlowFunctions(
                     // Case `x... := y`
                     // ∅ |= y:unknown
                     val type = if (doAddKnownTypes) {
-                        EtsTypeFact.from(current.rhv.type).let {
-                            // Note: convert Any to Unknown, because intersection with Any is Any
-                            if (it is EtsTypeFact.AnyEtsTypeFact) {
-                                EtsTypeFact.UnknownEtsTypeFact
-                            } else {
-                                it
-                            }
-                        }
+                        val knownType = current.rhv.tryGetKnownType(current.method)
+                        EtsTypeFact.from(knownType).fixAnyToUnknown()
                     } else {
                         EtsTypeFact.UnknownEtsTypeFact
                     }
@@ -283,13 +277,7 @@ class BackwardFlowFunctions(
                 }
             }
 
-            val lhv = when (val l = current.lhv) {
-                is EtsLValue -> l.toPath()
-                else -> {
-                    logger.info { "TODO backward assign zero: $current" }
-                    error("Unexpected LHV in assignment: $current")
-                }
-            }
+            val lhv = current.lhv.toPath()
 
             // Handle new possible facts for LHS:
             if (lhv.accesses.isNotEmpty()) {
@@ -543,7 +531,7 @@ class BackwardFlowFunctions(
             val objectWithMethod = EtsTypeFact.ObjectEtsTypeFact(
                 cls = null,
                 properties = mapOf(
-                    callExpr.method.name to EtsTypeFact.FunctionEtsTypeFact
+                    callExpr.callee.name to EtsTypeFact.FunctionEtsTypeFact
                 )
             )
             result += TypedVariable(path, objectWithMethod)
@@ -552,7 +540,7 @@ class BackwardFlowFunctions(
         if (doAddKnownTypes) {
             // f(x:T) |= x:T, where T is the type of the argument in f's signature
             for ((index, arg) in callExpr.args.withIndex()) {
-                val param = callExpr.method.parameters.getOrNull(index) ?: continue
+                val param = callExpr.callee.parameters.getOrNull(index) ?: continue
                 val base = arg.toBase()
                 val type = EtsTypeFact.from(param.type)
                 result += TypedVariable(base, type)