Update jacodb and refine dataflow accordingly

buildSrc/src/main/kotlin/Dependencies.kt

@@ -5,7 +5,7 @@ import org.gradle.plugin.use.PluginDependenciesSpec
 object Versions {
     const val detekt = "1.18.1"
     const val ini4j = "0.5.4"
-    const val jacodb = "5102242db4"
+    const val jacodb = "e47c227815"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "1.9.20"
@@ -115,28 +115,29 @@ object Libs {
     )
 
     // https://github.com/UnitTestBot/jacodb
+    private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild
     val jacodb_core = dep(
-        group = "com.github.UnitTestBot.jacodb",
+        group = jacodbPackage,
         name = "jacodb-core",
         version = Versions.jacodb
     )
     val jacodb_api_jvm = dep(
-        group = "com.github.UnitTestBot.jacodb",
+        group = jacodbPackage,
         name = "jacodb-api-jvm",
         version = Versions.jacodb
     )
     val jacodb_api_common = dep(
-        group = "com.github.UnitTestBot.jacodb",
+        group = jacodbPackage,
         name = "jacodb-api-common",
         version = Versions.jacodb
     )
     val jacodb_approximations = dep(
-        group = "com.github.UnitTestBot.jacodb",
+        group = jacodbPackage,
         name = "jacodb-approximations",
         version = Versions.jacodb
     )
     val jacodb_taint_configuration = dep(
-        group = "com.github.UnitTestBot.jacodb",
+        group = jacodbPackage,
         name = "jacodb-taint-configuration",
         version = Versions.jacodb
     )

settings.gradle.kts

@@ -28,4 +28,4 @@ pluginManagement {
             }
         }
     }
-}
+}

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/config/Condition.kt

@@ -16,11 +16,6 @@
 
 package org.usvm.dataflow.config
 
-import org.usvm.dataflow.ifds.Maybe
-import org.usvm.dataflow.ifds.onSome
-import org.usvm.dataflow.taint.Tainted
-import org.usvm.dataflow.util.Traits
-import org.usvm.dataflow.util.removeTrailingElementAccessors
 import org.jacodb.api.common.CommonMethod
 import org.jacodb.api.common.cfg.CommonInst
 import org.jacodb.api.common.cfg.CommonValue
@@ -40,6 +35,11 @@ import org.jacodb.taint.configuration.Or
 import org.jacodb.taint.configuration.PositionResolver
 import org.jacodb.taint.configuration.SourceFunctionMatches
 import org.jacodb.taint.configuration.TypeMatches
+import org.usvm.dataflow.ifds.Maybe
+import org.usvm.dataflow.ifds.onSome
+import org.usvm.dataflow.taint.Tainted
+import org.usvm.dataflow.util.Traits
+import org.usvm.dataflow.util.removeTrailingElementAccessors
 
 context(Traits<CommonMethod, CommonInst>)
 open class BasicConditionEvaluator(
@@ -76,35 +76,35 @@ open class BasicConditionEvaluator(
 
     override fun visit(condition: IsConstant): Boolean {
         positionResolver.resolve(condition.position).onSome {
-            return it.isConstant()
+            return isConstant(it)
         }
         return false
     }
 
     override fun visit(condition: ConstantEq): Boolean {
         positionResolver.resolve(condition.position).onSome { value ->
-            return value.eqConstant(condition.value)
+            return eqConstant(value, condition.value)
         }
         return false
     }
 
     override fun visit(condition: ConstantLt): Boolean {
         positionResolver.resolve(condition.position).onSome { value ->
-            return value.ltConstant(condition.value)
+            return ltConstant(value, condition.value)
         }
         return false
     }
 
     override fun visit(condition: ConstantGt): Boolean {
         positionResolver.resolve(condition.position).onSome { value ->
-            return value.gtConstant(condition.value)
+            return gtConstant(value, condition.value)
         }
         return false
     }
 
     override fun visit(condition: ConstantMatches): Boolean {
         positionResolver.resolve(condition.position).onSome { value ->
-            return value.matches(condition.pattern)
+            return matches(value, condition.pattern)
         }
         return false
     }
@@ -119,7 +119,7 @@ open class BasicConditionEvaluator(
 
     override fun visit(condition: TypeMatches): Boolean {
         positionResolver.resolve(condition.position).onSome { value ->
-            return value.typeMatches(condition)
+            return typeMatches(value, condition)
         }
         return false
     }
@@ -134,7 +134,7 @@ class FactAwareConditionEvaluator(
     override fun visit(condition: ContainsMark): Boolean {
         if (fact.mark != condition.mark) return false
         positionResolver.resolve(condition.position).onSome { value ->
-            val variable = value.toPath()
+            val variable = convertToPath(value)
 
             // FIXME: Adhoc for arrays
             val variableWithoutStars = variable.removeTrailingElementAccessors()

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/config/Position.kt

@@ -16,14 +16,7 @@
 
 package org.usvm.dataflow.config
 
-import org.usvm.dataflow.ifds.AccessPath
-import org.usvm.dataflow.ifds.ElementAccessor
-import org.usvm.dataflow.ifds.Maybe
-import org.usvm.dataflow.ifds.fmap
-import org.usvm.dataflow.ifds.toMaybe
-import org.usvm.dataflow.util.Traits
 import org.jacodb.api.common.CommonMethod
-import org.jacodb.api.common.CommonProject
 import org.jacodb.api.common.cfg.CommonAssignInst
 import org.jacodb.api.common.cfg.CommonInst
 import org.jacodb.api.common.cfg.CommonInstanceCallExpr
@@ -35,20 +28,26 @@ import org.jacodb.taint.configuration.PositionResolver
 import org.jacodb.taint.configuration.Result
 import org.jacodb.taint.configuration.ResultAnyElement
 import org.jacodb.taint.configuration.This
+import org.usvm.dataflow.ifds.AccessPath
+import org.usvm.dataflow.ifds.ElementAccessor
+import org.usvm.dataflow.ifds.Maybe
+import org.usvm.dataflow.ifds.fmap
+import org.usvm.dataflow.ifds.toMaybe
+import org.usvm.dataflow.util.Traits
 
 context(Traits<CommonMethod, CommonInst>)
 class CallPositionToAccessPathResolver(
     private val callStatement: CommonInst,
 ) : PositionResolver<Maybe<AccessPath>> {
-    private val callExpr = callStatement.getCallExpr()
+    private val callExpr = getCallExpr(callStatement)
         ?: error("Call statement should have non-null callExpr")
 
     override fun resolve(position: Position): Maybe<AccessPath> = when (position) {
         AnyArgument -> Maybe.none()
-        is Argument -> callExpr.args[position.index].toPathOrNull().toMaybe()
-        This -> (callExpr as? CommonInstanceCallExpr)?.instance?.toPathOrNull().toMaybe()
-        Result -> (callStatement as? CommonAssignInst)?.lhv?.toPathOrNull().toMaybe()
-        ResultAnyElement -> (callStatement as? CommonAssignInst)?.lhv?.toPathOrNull().toMaybe()
+        is Argument -> convertToPathOrNull(callExpr.args[position.index]).toMaybe()
+        This -> (callExpr as? CommonInstanceCallExpr)?.instance?.let { convertToPathOrNull(it) }.toMaybe()
+        Result -> (callStatement as? CommonAssignInst)?.lhv?.let { convertToPathOrNull(it) }.toMaybe()
+        ResultAnyElement -> (callStatement as? CommonAssignInst)?.lhv?.let { convertToPathOrNull(it) }.toMaybe()
             .fmap { it + ElementAccessor }
     }
 }
@@ -57,7 +56,7 @@ context(Traits<CommonMethod, CommonInst>)
 class CallPositionToValueResolver(
     private val callStatement: CommonInst,
 ) : PositionResolver<Maybe<CommonValue>> {
-    private val callExpr = callStatement.getCallExpr()
+    private val callExpr = getCallExpr(callStatement)
         ?: error("Call statement should have non-null callExpr")
 
     override fun resolve(position: Position): Maybe<CommonValue> = when (position) {
@@ -72,14 +71,13 @@ class CallPositionToValueResolver(
 context(Traits<CommonMethod, CommonInst>)
 class EntryPointPositionToValueResolver(
     private val method: CommonMethod,
-    private val project: CommonProject,
 ) : PositionResolver<Maybe<CommonValue>> {
     override fun resolve(position: Position): Maybe<CommonValue> = when (position) {
-        This -> Maybe.some(method.thisInstance)
+        This -> Maybe.some(getThisInstance(method))
 
         is Argument -> {
             val p = method.parameters[position.index]
-            project.getArgument(p).toMaybe()
+            getArgument(p).toMaybe()
         }
 
         AnyArgument, Result, ResultAnyElement -> error("Unexpected $position")
@@ -89,14 +87,13 @@ class EntryPointPositionToValueResolver(
 context(Traits<CommonMethod, CommonInst>)
 class EntryPointPositionToAccessPathResolver(
     private val method: CommonMethod,
-    private val project: CommonProject,
 ) : PositionResolver<Maybe<AccessPath>> {
     override fun resolve(position: Position): Maybe<AccessPath> = when (position) {
-        This -> method.thisInstance.toPathOrNull().toMaybe()
+        This -> convertToPathOrNull(getThisInstance(method)).toMaybe()
 
         is Argument -> {
             val p = method.parameters[position.index]
-            project.getArgument(p)?.toPathOrNull().toMaybe()
+            getArgument(p)?.let { convertToPathOrNull(it) }.toMaybe()
         }
 
         AnyArgument, Result, ResultAnyElement -> error("Unexpected $position")

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/graph/BackwardGraphs.kt

@@ -19,7 +19,6 @@
 package org.usvm.dataflow.graph
 
 import org.jacodb.api.common.CommonMethod
-import org.jacodb.api.common.CommonProject
 import org.jacodb.api.common.analysis.ApplicationGraph
 import org.jacodb.api.common.cfg.CommonInst
 
@@ -29,9 +28,6 @@ private class BackwardApplicationGraphImpl<Method, Statement>(
     where Method : CommonMethod,
           Statement : CommonInst {
 
-    override val project: CommonProject
-        get() = forward.project
-
     override fun predecessors(node: Statement) = forward.successors(node)
     override fun successors(node: Statement) = forward.predecessors(node)
 

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/ifds/Runner.kt

@@ -144,7 +144,7 @@ class UniRunner<Fact, Event, Method, Statement>(
         val (current, currentFact) = currentVertex
 
         val currentCallees = graph.callees(current).toList()
-        val currentIsCall = current.getCallExpr() != null
+        val currentIsCall = getCallExpr( current) != null
         val currentIsExit = current in graph.exitPoints(graph.methodOf(current))
 
         if (currentIsCall) {

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/sarif/Sarif.kt

@@ -32,8 +32,8 @@ import io.github.detekt.sarif4k.ThreadFlowLocation
 import io.github.detekt.sarif4k.Tool
 import io.github.detekt.sarif4k.ToolComponent
 import io.github.detekt.sarif4k.Version
-import org.usvm.dataflow.ifds.Vertex
 import org.jacodb.api.common.cfg.CommonInst
+import org.usvm.dataflow.ifds.Vertex
 import org.usvm.dataflow.util.Traits
 
 private const val SARIF_SCHEMA =
@@ -99,12 +99,12 @@ private fun <Statement : CommonInst> instToSarifLocation(
                 uri = sourceLocation
             ),
             region = Region(
-                startLine = inst.lineNumber()?.toLong()
+                startLine = lineNumber(inst).toLong()
             )
         ),
         logicalLocations = listOf(
             LogicalLocation(
-                fullyQualifiedName = inst.locationFQN()
+                fullyQualifiedName = locationFQN(inst)
             )
         )
     )

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/taint/TaintAnalyzers.kt

@@ -22,6 +22,8 @@ import org.jacodb.api.common.analysis.ApplicationGraph
 import org.jacodb.api.common.cfg.CommonInst
 import org.jacodb.taint.configuration.TaintConfigurationItem
 import org.jacodb.taint.configuration.TaintMethodSink
+import org.usvm.dataflow.config.CallPositionToValueResolver
+import org.usvm.dataflow.config.FactAwareConditionEvaluator
 import org.usvm.dataflow.ifds.Analyzer
 import org.usvm.dataflow.ifds.Edge
 import org.usvm.dataflow.ifds.Reason
@@ -53,9 +55,9 @@ class TaintAnalyzer<Method, Statement>(
         }
 
         run {
-            val callExpr = edge.to.statement.getCallExpr() ?: return@run
+            val callExpr = getCallExpr(edge.to.statement) ?: return@run
 
-            val callee = callExpr.callee
+            val callee = getCallee(callExpr)
 
             val config = getConfigForMethod(callee) ?: return@run
 
@@ -66,9 +68,9 @@ class TaintAnalyzer<Method, Statement>(
             }
 
             // Determine whether 'edge.to' is a sink via config:
-            val conditionEvaluator = org.usvm.dataflow.config.FactAwareConditionEvaluator(
+            val conditionEvaluator = FactAwareConditionEvaluator(
                 edge.to.fact,
-                org.usvm.dataflow.config.CallPositionToValueResolver(edge.to.statement),
+                CallPositionToValueResolver(edge.to.statement),
             )
             for (item in config.filterIsInstance<TaintMethodSink>()) {
                 if (item.condition.accept(conditionEvaluator)) {
@@ -86,11 +88,11 @@ class TaintAnalyzer<Method, Statement>(
             val statement = edge.to.statement
             val fact = edge.to.fact
             if (fact is Tainted && fact.mark.name == "UNTRUSTED") {
-                val branchExprCondition = statement.getBranchExprCondition()
-                if (branchExprCondition != null && statement.isLoopHead()) {
-                    val conditionOperands = branchExprCondition.getValues()
+                val branchExprCondition = getBranchExprCondition(statement)
+                if (branchExprCondition != null && isLoopHead(statement)) {
+                    val conditionOperands = getValues(branchExprCondition)
                     for (s in conditionOperands) {
-                        val p = s.toPath()
+                        val p = convertToPath(s)
                         if (p == fact.variable) {
                             val message = "Untrusted loop bound"
                             val vulnerability = TaintVulnerability(message, sink = edge.to)
@@ -104,10 +106,10 @@ class TaintAnalyzer<Method, Statement>(
             val statement = edge.to.statement
             val fact = edge.to.fact
             if (fact is Tainted && fact.mark.name == "UNTRUSTED") {
-                val arrayAllocation = statement.getArrayAllocation()
+                val arrayAllocation = getArrayAllocation(statement)
                 if (arrayAllocation != null) {
-                    for (arg in arrayAllocation.getValues()) {
-                        if (arg.toPath() == fact.variable) {
+                    for (arg in getValues(arrayAllocation)) {
+                        if (convertToPath(arg) == fact.variable) {
                             val message = "Untrusted array size"
                             val vulnerability = TaintVulnerability(message, sink = edge.to)
                             add(NewVulnerability(vulnerability))
@@ -120,9 +122,9 @@ class TaintAnalyzer<Method, Statement>(
             val statement = edge.to.statement
             val fact = edge.to.fact
             if (fact is Tainted && fact.mark.name == "UNTRUSTED") {
-                val arrayAccessIndex = statement.getArrayAccessIndex()
+                val arrayAccessIndex = getArrayAccessIndex(statement)
                 if (arrayAccessIndex != null) {
-                    if (arrayAccessIndex.toPath() == fact.variable) {
+                    if (convertToPath(arrayAccessIndex) == fact.variable) {
                         val message = "Untrusted index for access array"
                         val vulnerability = TaintVulnerability(message, sink = edge.to)
                         add(NewVulnerability(vulnerability))