Replaced access path bases with access paths in backward dataflow (#282)

Co-authored-by: Konstantin Chukharev <[email protected]>

Author: MForest7

.github/workflows/ci.yml

@@ -127,7 +127,7 @@ jobs:
           DEST_DIR="arkanalyzer"
           MAX_RETRIES=10
           RETRY_DELAY=3  # Delay between retries in seconds  
-          BRANCH="neo/2025-06-16"
+          BRANCH="neo/2025-06-24"
 
           for ((i=1; i<=MAX_RETRIES; i++)); do
               git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

usvm-ts-dataflow/build.gradle.kts

@@ -21,6 +21,7 @@ dependencies {
     implementation(Libs.kotlinx_collections)
     implementation(Libs.kotlinx_serialization_json)
     implementation(Libs.clikt)
+    runtimeOnly(Libs.logback)
 
     testImplementation(Libs.mockk)
     testImplementation(Libs.junit_jupiter_params)
@@ -129,5 +130,8 @@ tasks.shadowJar {
         // Provider com.github.ajalt.mordant.terminal.terminalinterface.jna.TerminalInterfaceProviderJna not found
         // ```
         exclude(dependency("com.github.ajalt.mordant:.*:.*"))
+
+        // Keep the logback in shadow jar:
+        exclude(dependency("ch.qos.logback:logback-classic:.*"))
     }
 }

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

@@ -2,21 +2,17 @@ package org.usvm.dataflow.ts.infer
 
 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.ifds.Analyzer
 import org.usvm.dataflow.ifds.Edge
 import org.usvm.dataflow.ifds.Vertex
 import org.usvm.dataflow.ts.graph.EtsApplicationGraph
 
 class BackwardAnalyzer(
     val graph: EtsApplicationGraph,
-    savedTypes: MutableMap<EtsType, MutableList<EtsTypeFact>>,
-    dominators: (EtsMethod) -> GraphDominators<EtsStmt>,
     doAddKnownTypes: Boolean = true,
 ) : Analyzer<BackwardTypeDomainFact, AnalyzerEvent, EtsMethod, EtsStmt> {
 
-    override val flowFunctions = BackwardFlowFunctions(graph, dominators, savedTypes, doAddKnownTypes)
+    override val flowFunctions = BackwardFlowFunctions(doAddKnownTypes)
 
     override fun handleCrossUnitCall(
         caller: Vertex<BackwardTypeDomainFact, EtsStmt>,
@@ -27,7 +23,7 @@ class BackwardAnalyzer(
 
     override fun handleNewEdge(edge: Edge<BackwardTypeDomainFact, EtsStmt>): List<AnalyzerEvent> {
         val (startVertex, currentVertex) = edge
-        val (current, currentFact) = currentVertex
+        val (current, _) = currentVertex
 
         val method = graph.methodOf(current)
         val currentIsExit = current in graph.exitPoints(method)