Add ifds runner for ets

.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-04-14"
+          BRANCH="neo/2025-05-12"
 
           for ((i=1; i<=MAX_RETRIES; i++)); do
               git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt

@@ -0,0 +1,119 @@
+package org.usvm.dataflow.ts.ifds
+
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsNopStmt
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsStmtLocation
+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
+import org.usvm.dataflow.ts.infer.AnalyzerEvent
+import org.usvm.dataflow.ts.infer.TypeInferenceManager
+import org.usvm.dataflow.ts.util.EtsTraits
+
+internal class EtsIfdsMethodRunner<Fact, Event : AnalyzerEvent>(
+    val graph: EtsApplicationGraph,
+    val method: EtsMethod,
+    val analyzer: Analyzer<Fact, Event, EtsMethod, EtsStmt>,
+    val traits: EtsTraits,
+    val manager: TypeInferenceManager,
+    val commonRunner: EtsIfdsRunner<Fact, Event>,
+) {
+    internal val flowSpace = analyzer.flowFunctions
+    private var enqueued: Boolean = false
+    private val sourceRunnersQueue: ArrayDeque<EtsIfdsSourceRunner<Fact>> = ArrayDeque()
+
+    internal fun enqueue(runner: EtsIfdsSourceRunner<Fact>) {
+        sourceRunnersQueue.addLast(runner)
+        if (!enqueued) {
+            commonRunner.methodRunnersQueue.addLast(this)
+            enqueued = true
+        }
+    }
+
+    fun processFacts() {
+        while (!sourceRunnersQueue.isEmpty()) {
+            val currentSourceRunner = sourceRunnersQueue.removeFirst()
+            currentSourceRunner.processFacts()
+        }
+        enqueued = false
+    }
+
+    internal val sourceRunners = hashMapOf<Fact, HashMap<EtsStmt, EtsIfdsSourceRunner<Fact>>>()
+    internal fun getSourceRunner(vertex: Vertex<Fact, EtsStmt>): EtsIfdsSourceRunner<Fact> {
+        return sourceRunners
+            .getOrPut(vertex.fact) { hashMapOf() }
+            .getOrPut(vertex.statement) {
+                EtsIfdsSourceRunner(traits, this, vertex.statement, vertex.fact)
+            }
+    }
+
+    internal fun getSourceRunners(fact: Fact): Collection<EtsIfdsSourceRunner<Fact>> {
+        return sourceRunners.getOrPut(fact) {
+            entrypoints.associateWithTo(hashMapOf()) {
+                EtsIfdsSourceRunner(traits, this, it, fact)
+            }
+        }.values
+    }
+
+    internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1))
+    internal val stmts = listOf(mockStmt) + method.cfg.stmts
+
+    internal val isExit = BooleanArray(stmts.size).apply {
+        for (exit in graph.exitPoints(method)) {
+            set(exit.index, true)
+        }
+    }
+
+    internal val EtsStmt.index: Int
+        get() = location.index + 1
+
+    internal val successors = stmts.map { graph.successors(it).map { s -> s.index } }
+    internal val entrypoints = graph.entryPoints(method).toList()
+
+    fun addStart() {
+        val startFacts = flowSpace.obtainPossibleStartFacts(method)
+        for (startFact in startFacts) {
+            propagateStartingFact(startFact)
+        }
+    }
+
+    internal data class PathEdge<Fact>(
+        val endStmtIndex: Int,
+        val fact: Fact,
+    )
+
+    internal fun propagateStartingFact(fact: Fact): Set<Vertex<Fact, EtsStmt>> {
+        val summaryEdges = hashSetOf<Vertex<Fact, EtsStmt>>()
+        for (entrypoint in entrypoints) {
+            val runner = getSourceRunner(Vertex(entrypoint, fact))
+            runner.propagate(PathEdge(entrypoint.index, fact))
+            summaryEdges += runner.summaryEdges
+        }
+        return summaryEdges
+    }
+
+    internal fun handleSummaryEdgeInCaller(
+        currentEdge: Edge<Fact, EtsStmt>,
+        summaryEdge: Edge<Fact, EtsStmt>,
+    ) {
+        val (startVertex, currentVertex) = currentEdge
+        val sourceRunner = getSourceRunner(startVertex)
+        val caller = currentVertex.statement
+        for (returnSite in graph.successors(caller)) {
+            val (exit, exitFact) = summaryEdge.to
+            val finalFacts = flowSpace
+                .obtainExitToReturnSiteFlowFunction(caller, returnSite, exit)
+                .compute(exitFact)
+            for (returnSiteFact in finalFacts) {
+                val newEdge = PathEdge(caller.index, returnSiteFact)
+                sourceRunner.propagate(newEdge)
+            }
+        }
+    }
+
+    override fun toString(): String {
+        return "Runner for ${method.signature}"
+    }
+}

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt

@@ -0,0 +1,87 @@
+package org.usvm.dataflow.ts.ifds
+
+import kotlinx.coroutines.coroutineScope
+import kotlinx.coroutines.isActive
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsStmt
+import org.usvm.dataflow.ifds.Analyzer
+import org.usvm.dataflow.ifds.Edge
+import org.usvm.dataflow.ifds.IfdsResult
+import org.usvm.dataflow.ifds.QueueEmptinessChanged
+import org.usvm.dataflow.ifds.Reason
+import org.usvm.dataflow.ifds.Runner
+import org.usvm.dataflow.ifds.SingletonUnit
+import org.usvm.dataflow.ifds.UnitType
+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
+
+class EtsIfdsRunner<Fact, Event : AnalyzerEvent>(
+    override val graph: EtsApplicationGraph,
+    val analyzer: Analyzer<Fact, Event, EtsMethod, EtsStmt>,
+    val traits: EtsTraits,
+    val manager: TypeInferenceManager,
+    private val zeroFact: Fact,
+) : Runner<Fact, EtsMethod, EtsStmt> {
+    internal val methodRunnersQueue: ArrayDeque<EtsIfdsMethodRunner<Fact, Event>> = ArrayDeque()
+    private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true)
+
+    private val methodRunners = hashMapOf<EtsMethod, EtsIfdsMethodRunner<Fact, Event>>()
+
+    internal fun getMethodRunner(method: EtsMethod): EtsIfdsMethodRunner<Fact, Event> {
+        return methodRunners.getOrPut(method) {
+            EtsIfdsMethodRunner(
+                graph = graph,
+                method = method,
+                analyzer = analyzer,
+                traits = traits,
+                manager = manager,
+                commonRunner = this@EtsIfdsRunner,
+            )
+        }
+    }
+
+    override suspend fun run(startMethods: List<EtsMethod>) {
+        for (method in startMethods) {
+            getMethodRunner(method).addStart()
+        }
+
+        tabulationAlgorithm()
+    }
+
+    private suspend fun tabulationAlgorithm() = coroutineScope {
+        while (isActive) {
+            val current = methodRunnersQueue.removeFirstOrNull() ?: run {
+                manager.handleControlEvent(queueIsEmpty)
+                return@coroutineScope
+            }
+            current.processFacts()
+        }
+    }
+
+    override val unit: UnitType
+        get() = SingletonUnit
+
+    override fun getIfdsResult(): IfdsResult<Fact, EtsStmt> {
+        val sourceRunners = methodRunners.values.flatMap { methodRunner ->
+            methodRunner.sourceRunners.values.flatMap { it.values }
+        }
+        val pathEdges = sourceRunners.flatMap { it.getPathEdges() }
+
+        val resultFacts: MutableMap<EtsStmt, MutableSet<Fact>> = hashMapOf()
+        for (edge in pathEdges) {
+            resultFacts.getOrPut(edge.to.statement) { hashSetOf() }.add(edge.to.fact)
+        }
+
+        return IfdsResult(pathEdges, resultFacts, reasons = emptyMap(), zeroFact)
+    }
+
+    override fun submitNewEdge(edge: Edge<Fact, EtsStmt>, reason: Reason<Fact, EtsStmt>) {
+        val (startVertex, endVertex) = edge
+        val (endStmt, endFact) = endVertex
+
+        val localPathEdge = EtsIfdsMethodRunner.PathEdge(endStmt.location.index, endFact)
+        getMethodRunner(startVertex.statement.method).getSourceRunner(startVertex).propagate(localPathEdge)
+    }
+}

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsSourceRunner.kt

@@ -0,0 +1,147 @@
+package org.usvm.dataflow.ts.ifds
+
+import org.jacodb.ets.model.EtsStmt
+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
+
+internal class EtsIfdsSourceRunner<Fact>(
+    val traits: EtsTraits,
+    val methodRunner: EtsIfdsMethodRunner<Fact, *>,
+    val entrypoint: EtsStmt,
+    val startingFact: Fact,
+) {
+    private var enqueued: Boolean = false
+    private val pathEdgeQueue: ArrayDeque<PathEdge<Fact>> = ArrayDeque()
+
+    fun processFacts() {
+        while (!pathEdgeQueue.isEmpty()) {
+            val currentEdge = pathEdgeQueue.removeFirst()
+            tabulationAlgorithmStep(currentEdge)
+        }
+        enqueued = false
+    }
+
+    private val successors = methodRunner.successors
+    private val stmts = methodRunner.stmts
+    private val mockStmt = methodRunner.mockStmt
+    private val flowSpace = methodRunner.flowSpace
+    val graph = methodRunner.graph
+
+    private val factsAtStmt = Array(stmts.size) { hashSetOf<Fact>() }
+
+    internal fun propagate(localEdge: PathEdge<Fact>) {
+        val (endStmtIndex, endFact) = localEdge
+        if (factsAtStmt[endStmtIndex].add(endFact)) {
+            val startVertex = Vertex(mockStmt, startingFact)
+            val endVertex = Vertex(stmts[endStmtIndex], endFact)
+            val edge = Edge(startVertex, endVertex)
+            val events = methodRunner.analyzer.handleNewEdge(edge)
+
+            for (event in events) {
+                methodRunner.manager.handleEvent(event)
+            }
+
+            pathEdgeQueue.add(localEdge)
+            if (!enqueued) {
+                enqueued = true
+                methodRunner.enqueue(this)
+            }
+        }
+    }
+
+    private val callerPathEdges = hashSetOf<Edge<Fact, EtsStmt>>()
+    internal val summaryEdges = hashSetOf<Vertex<Fact, EtsStmt>>()
+
+    private fun tabulationAlgorithmStep(
+        currentEdge: PathEdge<Fact>,
+    ) = with(traits) {
+        val (currentStmtIndex, currentFact) = currentEdge
+        val currentStmt = stmts[currentStmtIndex]
+
+        val currentIsCall = getCallExpr(currentStmt) != null
+        val currentIsExit = methodRunner.isExit[currentStmtIndex]
+
+        if (currentIsCall) {
+            val callToReturnFlowFunction = flowSpace
+                .obtainCallToReturnSiteFlowFunction(currentStmt, mockStmt)
+
+            // Propagate through the call-to-return-site edge:
+            val factsAtReturnSite = callToReturnFlowFunction.compute(currentFact)
+            for (returnSite in successors[currentStmtIndex]) {
+                for (returnSiteFact in factsAtReturnSite) {
+                    val edge = PathEdge(returnSite, returnSiteFact)
+                    propagate(edge)
+                }
+            }
+
+            for (callee in graph.callees(currentStmt)) {
+                for (calleeStart in graph.entryPoints(callee)) {
+                    val callToStartFlowFunction = flowSpace.obtainCallToStartFlowFunction(currentStmt, calleeStart)
+                    val factsAtCalleeStart = callToStartFlowFunction.compute(currentFact)
+
+                    for (calleeStartFact in factsAtCalleeStart) {
+                        val calleeStartVertex = Vertex(calleeStart, calleeStartFact)
+
+                        // Save info about the call for summary edges that will be found later:
+                        val calleeRunner = methodRunner.commonRunner.getMethodRunner(callee)
+                        val currentVertex = Vertex(currentStmt, currentFact)
+                        val startingVertex = Vertex(entrypoint, startingFact)
+                        val callerEdge = Edge(startingVertex, currentVertex)
+                        for (calleeSourceRunner in calleeRunner.getSourceRunners(startingFact)) {
+                            calleeSourceRunner.callerPathEdges.add(callerEdge)
+                        }
+
+                        // Initialize analysis of callee:
+                        val summaryEdges = calleeRunner.propagateStartingFact(calleeStartFact)
+
+                        // Handle already-found summary edges:
+                        for (exitVertex in summaryEdges) {
+                            val summaryEdge = Edge(calleeStartVertex, exitVertex)
+                            methodRunner.handleSummaryEdgeInCaller(callerEdge, summaryEdge)
+                        }
+                    }
+                }
+            }
+        } else {
+            if (currentIsExit) {
+                val startVertex = Vertex(entrypoint, startingFact)
+                val currentVertex = Vertex(currentStmt, currentFact)
+
+                // Propagate through the summary edge:
+                for (callerPathEdge in callerPathEdges) {
+                    val summaryEdge = Edge(startVertex, currentVertex)
+                    val caller = callerPathEdge.from.statement.method
+                    val callerRunner = methodRunner.commonRunner.getMethodRunner(caller)
+                    callerRunner.handleSummaryEdgeInCaller(currentEdge = callerPathEdge, summaryEdge = summaryEdge)
+                }
+
+                // Add new summary edge:
+                summaryEdges.add(currentVertex)
+            }
+
+            // Simple (sequential) propagation to the next instruction:
+            val factsAtNext = flowSpace
+                .obtainSequentFlowFunction(currentStmt, mockStmt)
+                .compute(currentFact)
+            for (next in successors[currentStmtIndex]) {
+                for (nextFact in factsAtNext) {
+                    val edge = PathEdge(next, nextFact)
+                    propagate(edge)
+                }
+            }
+        }
+    }
+
+    internal fun getPathEdges(): List<Edge<Fact, EtsStmt>> {
+        val startVertex = Vertex(entrypoint, startingFact)
+        return factsAtStmt.flatMapIndexed { index, facts ->
+            val stmt = stmts[index]
+            facts.map {
+                val endVertex = Vertex(stmt, it)
+                Edge(startVertex, endVertex)
+            }
+        }
+    }
+}

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

@@ -34,17 +34,13 @@ class ForwardAnalyzer(
         error("No cross unit calls")
     }
 
-    private val liveVariablesCache = hashMapOf<EtsMethod, LiveVariables>()
-    private fun liveVariables(method: EtsMethod): LiveVariables =
-        liveVariablesCache.computeIfAbsent(method) {
-            if (doLiveVariablesAnalysis) LiveVariables.from(method) else AlwaysAlive
-        }
-
     private fun variableIsDying(fact: ForwardTypeDomainFact, stmt: EtsStmt): Boolean {
         if (fact !is ForwardTypeDomainFact.TypedVariable) return false
-        val base = fact.variable.base
-        if (base !is AccessPathBase.Local) return false
-        return !liveVariables(stmt.method).isAliveAt(base.name, stmt)
+        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)
+            else -> false
+        }
     }
 
     override fun handleNewEdge(edge: Edge<ForwardTypeDomainFact, EtsStmt>): List<AnalyzerEvent> {

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

@@ -66,7 +66,7 @@ class ForwardFlowFunctions(
     }
 
     private val liveVariablesCache = hashMapOf<EtsMethod, LiveVariables>()
-    private fun liveVariables(method: EtsMethod) =
+    internal fun liveVariables(method: EtsMethod) =
         liveVariablesCache.computeIfAbsent(method) {
             if (doLiveVariablesAnalysis) {
                 LiveVariables.from(method)