From 3c7390d28969c1cc2adb63ac6303bfc20e888566 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Mon, 12 May 2025 15:33:56 +0300 Subject: [PATCH 01/18] add ifds runner for ets --- .../dataflow/ts/ifds/EtsBackwardIfdsRunner.kt | 72 +++++++++ .../ts/ifds/EtsBackwardMethodRunner.kt | 142 ++++++++++++++++++ .../ts/ifds/EtsBackwardSourceRunner.kt | 132 ++++++++++++++++ .../dataflow/ts/ifds/EtsForwardIfdsRunner.kt | 76 ++++++++++ .../ts/ifds/EtsForwardMethodRunner.kt | 131 ++++++++++++++++ .../ts/ifds/EtsForwardSourceRunner.kt | 130 ++++++++++++++++ .../dataflow/ts/infer/TypeInferenceManager.kt | 32 ++-- 7 files changed, 697 insertions(+), 18 deletions(-) create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt new file mode 100644 index 0000000000..8b8f1fee10 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt @@ -0,0 +1,72 @@ +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 EtsBackwardIfdsRunner( + override val graph: EtsApplicationGraph, + val analyzer: Analyzer, + val traits: EtsTraits, + val manager: TypeInferenceManager, +) : Runner { + val queue: ArrayDeque> = ArrayDeque() + + private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) + + private val methods = graph.cp.projectAndSdkClasses.flatMap { it.methods + it.ctor } + private val runners = methods.associateWith { EtsBackwardMethodRunner( + graph = graph, + method = it, + analyzer = analyzer, + traits = traits, + manager = manager, + commonRunner = this@EtsBackwardIfdsRunner + ) } + + fun getMethodRunner(method: EtsMethod): EtsBackwardMethodRunner { + return runners.getValue(method) + } + + override suspend fun run(startMethods: List) { + for (method in startMethods) { + runners[method]?.addStart() + } + + tabulationAlgorithm() + } + + private suspend fun tabulationAlgorithm() = coroutineScope { + while (isActive) { + val current = queue.removeFirstOrNull() ?: run { + manager.handleControlEvent(queueIsEmpty) + return@coroutineScope + } + current.processFacts() + } + } + + override val unit: UnitType + get() = SingletonUnit + + override fun getIfdsResult(): IfdsResult { + TODO("Not yet implemented") + } + + override fun submitNewEdge(edge: Edge, reason: Reason) { + TODO("Not yet implemented") + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt new file mode 100644 index 0000000000..731a808ae9 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt @@ -0,0 +1,142 @@ +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.jacodb.ets.utils.callExpr +import org.usvm.dataflow.ifds.Analyzer +import org.usvm.dataflow.ifds.Edge +import org.usvm.dataflow.ifds.FlowFunction +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 + +class EtsBackwardMethodRunner( + val graph: EtsApplicationGraph, + val method: EtsMethod, + val analyzer: Analyzer, + val traits: EtsTraits, + val manager: TypeInferenceManager, + val commonRunner: EtsBackwardIfdsRunner, +) { + private val flowSpace = analyzer.flowFunctions + + internal data class PathEdge( + val endIp: Int, + val fact: Fact, + ) + + private var enqueued: Boolean = false + private val queue: ArrayDeque> = ArrayDeque() + + internal fun enqueue(runner: EtsBackwardSourceRunner) { + queue.addLast(runner) + if (!enqueued) { + commonRunner.queue.addLast(this) + enqueued = true + } + } + + fun processFacts() { + while (!queue.isEmpty()) { + val currentSourceRunner = queue.removeFirst() + currentSourceRunner.processFacts() + } + enqueued = false + } + + private val sourceRunners = hashMapOf>>() + internal fun getSourceRunner(vertex: Vertex): EtsBackwardSourceRunner { + return sourceRunners + .getOrPut(vertex.fact) { hashMapOf() } + .getOrPut(vertex.statement) { + EtsBackwardSourceRunner(traits, this, vertex.statement, vertex.fact) + } + } + + internal fun getSourceRunners(fact: Fact): Collection> { + return sourceRunners.getOrPut(fact) { + entrypoints.associateWithTo(hashMapOf()) { + EtsBackwardSourceRunner(traits, this, it, fact) + } + }.values + } + + internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1)) + internal val stmts = listOf(mockStmt) + method.cfg.stmts + + internal val EtsStmt.index: Int + get() = location.index + 1 + + internal val successors = stmts.map { graph.successors(it).map { s -> s.index } } + + internal val sequentFlowFunction = stmts.map { + flowSpace.obtainSequentFlowFunction(it, mockStmt) + } + internal val callToReturnSiteFlowFunction = stmts.map { stmt -> + flowSpace.takeIf { stmt.callExpr != null } + ?.obtainCallToReturnSiteFlowFunction(stmt, mockStmt) + } + + internal data class CalleeStart( + val start: EtsStmt, + val flowFunction: FlowFunction + ) + + internal val callToStartFlowFunctions = stmts.map { stmt -> + val flowFunctions = mutableListOf>() + for (callee in graph.callees(stmt)) { + for (calleeStart in graph.entryPoints(callee)) { + val flowFunction = flowSpace.obtainCallToStartFlowFunction(stmt, calleeStart) + flowFunctions.add(CalleeStart(calleeStart, flowFunction)) + } + } + flowFunctions + } + + internal val entrypoints = graph.entryPoints(method).toList() + internal val exitpoints = graph.exitPoints(method).toList() + + fun addStart() { + val startFacts = flowSpace.obtainPossibleStartFacts(method) + for (startFact in startFacts) { + propagateStartingFact(startFact) + } + } + + internal fun propagateStartingFact(fact: Fact): Set> { + val summaryEdges = hashSetOf>() + 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, + summaryEdge: Edge, + ) { + 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}" + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt new file mode 100644 index 0000000000..e2f6f51b8f --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt @@ -0,0 +1,132 @@ +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.EtsBackwardMethodRunner.PathEdge +import org.usvm.dataflow.ts.util.EtsTraits + +class EtsBackwardSourceRunner( + val traits: EtsTraits, + val methodRunner: EtsBackwardMethodRunner, + val entrypoint: EtsStmt, + val startingFact: Fact, +) { + private var enqueued: Boolean = false + private val internalQueue: ArrayDeque> = ArrayDeque() + + fun processFacts() { + while (!internalQueue.isEmpty()) { + val currentEdge = internalQueue.removeFirst() + tabulationAlgorithmStep(currentEdge) + } + enqueued = false + } + + private val successors = methodRunner.successors + private val exitpoints = methodRunner.exitpoints + private val stmts = methodRunner.stmts + private val mockStmt = methodRunner.mockStmt + + private val callToReturnSiteFlowFunction = methodRunner.callToReturnSiteFlowFunction + private val callToStartFlowFunctions = methodRunner.callToStartFlowFunctions + private val sequentFlowFunction = methodRunner.sequentFlowFunction + + private val factsAtStmt = Array(stmts.size) { hashSetOf() } + + internal fun propagate(edge: PathEdge) { + val (endIp, endFact) = edge + if (factsAtStmt[endIp].add(endFact)) { + val startVertex = Vertex(mockStmt, startingFact) + val endVertex = Vertex(stmts[endIp], endFact) + for (event in methodRunner.analyzer.handleNewEdge(Edge(startVertex, endVertex))) { + methodRunner.manager.handleEvent(event) + } + + internalQueue.add(edge) + if (!enqueued) { + enqueued = true + methodRunner.enqueue(this) + } + } + } + + private val callerPathEdges = hashSetOf>() + internal val summaryEdges = hashSetOf>() + + private fun tabulationAlgorithmStep( + currentEdge: PathEdge + ) = with(traits) { + val (currentIp, currentFact) = currentEdge + val current = stmts[currentIp] + + val currentIsCall = getCallExpr(current) != null + val currentIsExit = current in exitpoints + + if (currentIsCall) { + val callToReturnFlowFunction = callToReturnSiteFlowFunction[currentIp] + if (callToReturnFlowFunction != null) { + // Propagate through the call-to-return-site edge: + val factsAtReturnSite = callToReturnFlowFunction.compute(currentFact) + for (returnSite in successors[currentIp]) { + for (returnSiteFact in factsAtReturnSite) { + val edge = PathEdge(returnSite, returnSiteFact) + propagate(edge) + } + } + } + + for ((calleeStart, callToStartFlowFunction) in callToStartFlowFunctions[currentIp]) { + val callee = calleeStart.method + 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(current, 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(current, 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 = sequentFlowFunction[currentIp].compute(currentFact) + for (next in successors[currentIp]) { + for (nextFact in factsAtNext) { + val edge = PathEdge(next, nextFact) + propagate(edge) + } + } + } + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt new file mode 100644 index 0000000000..ded4f4a08b --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt @@ -0,0 +1,76 @@ +package org.usvm.dataflow.ts.ifds + +import kotlinx.coroutines.coroutineScope +import kotlinx.coroutines.isActive +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsMethod +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 EtsForwardIfdsRunner( + override val graph: EtsApplicationGraph, + val analyzer: Analyzer, + val traits: EtsTraits, + val manager: TypeInferenceManager, +) : Runner { + val queue: ArrayDeque> = ArrayDeque() + + private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) + + private val methods = graph.cp.projectAndSdkClasses.flatMap { it.methods + it.ctor } + private val runners = methods.associateWith { EtsForwardMethodRunner( + graph = graph, + method = it, + analyzer = analyzer, + traits = traits, + manager = manager, + commonRunner = this@EtsForwardIfdsRunner + ) } + + fun getMethodRunner(method: EtsMethod): EtsForwardMethodRunner { + return runners.getValue(method) + } + + override suspend fun run(startMethods: List) { + for (method in startMethods) { + val runner = runners[method] ?: continue + runner.addStart() + /*for ((stmt, fact) in backwardFacts[method].orEmpty()) { + runner.submitFact(stmt, fact) + }*/ + } + + tabulationAlgorithm() + } + + private suspend fun tabulationAlgorithm() = coroutineScope { + while (isActive) { + val current = queue.removeFirstOrNull() ?: run { + manager.handleControlEvent(queueIsEmpty) + return@coroutineScope + } + current.processFacts() + } + } + + override val unit: UnitType + get() = SingletonUnit + + override fun getIfdsResult(): IfdsResult { + TODO("Not yet implemented") + } + + override fun submitNewEdge(edge: Edge, reason: Reason) { + TODO("Not yet implemented") + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt new file mode 100644 index 0000000000..a2581a3851 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt @@ -0,0 +1,131 @@ +package org.usvm.dataflow.ts.ifds + +import org.jacodb.ets.model.EtsStmtLocation +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.callExpr +import org.usvm.dataflow.ifds.Analyzer +import org.usvm.dataflow.ifds.Edge +import org.usvm.dataflow.ifds.FlowFunction +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 + +class EtsForwardMethodRunner( + val graph: EtsApplicationGraph, + val method: EtsMethod, + val analyzer: Analyzer, + val traits: EtsTraits, + val manager: TypeInferenceManager, + val commonRunner: EtsForwardIfdsRunner, +) { + private val flowSpace = analyzer.flowFunctions + + private var enqueued: Boolean = false + private val queue: ArrayDeque> = ArrayDeque() + + internal val cfg = method.cfg + internal val stmts = method.cfg.stmts + internal val successors = stmts.map { cfg.successors(it).map { s -> s.index } } + + internal val EtsStmt.index: Int + get() = location.index + internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1)) + internal val entrypoint = stmts.firstOrNull() ?: mockStmt + + internal data class CalleeStart( + val start: EtsStmt, + val flowFunction: FlowFunction + ) + + internal val sequentFlowFunction = stmts.map { + flowSpace.obtainSequentFlowFunction(it, mockStmt) + } + internal val callToReturnSiteFlowFunction = stmts.map { stmt -> + flowSpace.takeIf { stmt.callExpr != null } + ?.obtainCallToReturnSiteFlowFunction(stmt, mockStmt) + } + internal val callToStartFlowFunctions = stmts.map { stmt -> + val flowFunctions = mutableListOf>() + for (callee in graph.callees(stmt)) { + for (calleeStart in graph.entryPoints(callee)) { + val flowFunction = flowSpace.obtainCallToStartFlowFunction(stmt, calleeStart) + flowFunctions.add(CalleeStart(calleeStart, flowFunction)) + } + } + flowFunctions + } + + fun addStart() { + if (entrypoint == mockStmt) + return + + val startFacts = flowSpace.obtainPossibleStartFacts(method) + for (startFact in startFacts) { + propagateStartingFact(startFact) + } + } + + internal fun enqueue(runner: EtsForwardSourceRunner) { + queue.addLast(runner) + if (!enqueued) { + commonRunner.queue.addLast(this) + enqueued = true + } + } + + fun processFacts() { + while (!queue.isEmpty()) { + val currentSourceRunner = queue.removeFirst() + currentSourceRunner.processFacts() + } + enqueued = false + } + + internal data class PathEdge( + val end: Int, + val fact: Fact + ) + + private val sourceRunners = hashMapOf>() + internal fun getSourceRunner(fact: Fact): EtsForwardSourceRunner { + return sourceRunners.getOrPut(fact) { + EtsForwardSourceRunner(traits, this, fact) + } + } + + internal fun propagateStartingFact(fact: Fact): Set> { + if (entrypoint == mockStmt) { + return emptySet() + } + val sourceRunner = getSourceRunner(fact) + sourceRunner.propagate(PathEdge(0, fact)) + return sourceRunner.summaryEdges + } + + internal fun handleSummaryEdgeInCaller( + currentEdge: Edge, + summaryEdge: Edge, + ) { + val (startVertex, currentVertex) = currentEdge + val sourceRunner = getSourceRunner(startVertex.fact) + 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}" + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt new file mode 100644 index 0000000000..57522b93cc --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt @@ -0,0 +1,130 @@ +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.EtsForwardMethodRunner.PathEdge +import org.usvm.dataflow.ts.util.EtsTraits + +class EtsForwardSourceRunner( + val traits: EtsTraits, + val methodRunner: EtsForwardMethodRunner, + val startingFact: Fact, +) { + private var enqueued: Boolean = false + private val internalQueue: ArrayDeque> = ArrayDeque() + + fun processFacts() { + while (!internalQueue.isEmpty()) { + val currentEdge = internalQueue.removeFirst() + tabulationAlgorithmStep(currentEdge) + } + enqueued = false + } + + private val cfg = methodRunner.cfg + private val successors = methodRunner.successors + private val stmts = methodRunner.stmts + private val mockStmt = methodRunner.mockStmt + private val entrypoint = methodRunner.entrypoint + + private val callToReturnSiteFlowFunction = methodRunner.callToReturnSiteFlowFunction + private val callToStartFlowFunctions = methodRunner.callToStartFlowFunctions + private val sequentFlowFunction = methodRunner.sequentFlowFunction + + private val factsAtStmt = Array(stmts.size) { hashSetOf() } + + internal fun propagate(edge: PathEdge) { + val (ip, fact) = edge + if (factsAtStmt[ip].add(fact)) { + val startVertex = Vertex(mockStmt, startingFact) + val endVertex = Vertex(stmts[ip], fact) + for (event in methodRunner.analyzer.handleNewEdge(Edge(startVertex, endVertex))) { + methodRunner.manager.handleEvent(event) + } + + internalQueue.add(edge) + if (!enqueued) { + enqueued = true + methodRunner.enqueue(this) + } + } + } + + private val callerPathEdges = hashSetOf>() + internal val summaryEdges = hashSetOf>() + + private fun tabulationAlgorithmStep( + currentEdge: PathEdge + ) = with(traits) { + val (currentIp, currentFact) = currentEdge + val current = stmts[currentIp] + + val currentIsCall = getCallExpr(current) != null + val currentIsExit = current in cfg.exits + + if (currentIsCall) { + val callToReturnFlowFunction = callToReturnSiteFlowFunction[currentIp] + if (callToReturnFlowFunction != null) { + // Propagate through the call-to-return-site edge: + val factsAtReturnSite = callToReturnFlowFunction.compute(currentFact) + for (returnSite in successors[currentIp]) { + for (returnSiteFact in factsAtReturnSite) { + val edge = PathEdge(returnSite, returnSiteFact) + propagate(edge) + } + } + } + + for ((calleeStart, callToStartFlowFunction) in callToStartFlowFunctions[currentIp]) { + val callee = calleeStart.method + 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 startingVertex = Vertex(entrypoint, startingFact) + val currentVertex = Vertex(current, currentFact) + val callerEdge = Edge(startingVertex, currentVertex) + calleeRunner.getSourceRunner(calleeStartFact).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(current, 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 = sequentFlowFunction[currentIp].compute(currentFact) + for (next in successors[currentIp]) { + for (nextFact in factsAtNext) { + val edge = PathEdge(next, nextFact) + propagate(edge) + } + } + } + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index d746b2525e..c5ab3d45fe 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -28,10 +28,10 @@ import org.usvm.dataflow.ifds.ControlEvent import org.usvm.dataflow.ifds.Edge import org.usvm.dataflow.ifds.Manager import org.usvm.dataflow.ifds.QueueEmptinessChanged -import org.usvm.dataflow.ifds.SingletonUnit -import org.usvm.dataflow.ifds.UniRunner import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.graph.reversed +import org.usvm.dataflow.ts.ifds.EtsBackwardIfdsRunner +import org.usvm.dataflow.ts.ifds.EtsForwardIfdsRunner import org.usvm.dataflow.ts.infer.EtsTypeFact.Companion.allStringProperties import org.usvm.dataflow.ts.util.EtsTraits import org.usvm.dataflow.ts.util.getRealLocals @@ -102,8 +102,8 @@ class TypeInferenceManager( createResultsFromSummaries(updatedTypeScheme, doInferAllLocals) } - lateinit var backwardRunner: UniRunner - lateinit var forwardRunner: UniRunner + lateinit var backwardRunner: EtsBackwardIfdsRunner + lateinit var forwardRunner: EtsForwardIfdsRunner private suspend fun collectSummaries( startMethods: List, @@ -113,16 +113,14 @@ class TypeInferenceManager( logger.info { "Preparing backward analysis" } val backwardGraph = graph.reversed val backwardAnalyzer = BackwardAnalyzer(backwardGraph, savedTypes, ::methodDominators, doAddKnownTypes) - val backwardRunner = UniRunner( - traits = traits, - manager = this@TypeInferenceManager, + + val backwardRunner = EtsBackwardIfdsRunner( graph = backwardGraph, analyzer = backwardAnalyzer, - unitResolver = { SingletonUnit }, - unit = SingletonUnit, - zeroFact = BackwardTypeDomainFact.Zero, - storeReasons = false, + traits = traits, + manager = this ) + this@TypeInferenceManager.backwardRunner = backwardRunner val exceptionHandler = CoroutineExceptionHandler { _, exception -> @@ -200,15 +198,11 @@ class TypeInferenceManager( doLiveVariablesAnalysis = true, ) - val forwardRunner = UniRunner( - traits = traits, - manager = this@TypeInferenceManager, + val forwardRunner = EtsForwardIfdsRunner( graph = forwardGraph, analyzer = forwardAnalyzer, - unitResolver = { SingletonUnit }, - unit = SingletonUnit, - zeroFact = ForwardTypeDomainFact.Zero, - storeReasons = false, + traits = traits, + manager = this, ) this@TypeInferenceManager.forwardRunner = forwardRunner @@ -372,6 +366,7 @@ class TypeInferenceManager( } val typeFactsOnThisMethods = forwardSummariesByClass[cls.signature].orEmpty() + .asSequence() .filter { (method, _) -> method.name != INSTANCE_INIT_METHOD_NAME } .flatMap { (_, summaries) -> summaries.asSequence() } .mapNotNull { it.initialFact as? ForwardTypeDomainFact.TypedVariable } @@ -380,6 +375,7 @@ class TypeInferenceManager( .toList() val typeFactsOnThisCtor = forwardSummariesByClass[cls.signature].orEmpty() + .asSequence() .filter { (method, _) -> method.name == CONSTRUCTOR_NAME || method.name == INSTANCE_INIT_METHOD_NAME } .flatMap { (_, summaries) -> summaries.asSequence() } .mapNotNull { it.exitFact as? ForwardTypeDomainFact.TypedVariable } From 37c5b9627496164a39eaabba25ff4c7fd051d895 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Mon, 12 May 2025 16:04:27 +0300 Subject: [PATCH 02/18] cleanup --- .../dataflow/ts/ifds/EtsBackwardIfdsRunner.kt | 18 ++++++++++-------- .../ts/ifds/EtsBackwardMethodRunner.kt | 2 +- .../ts/ifds/EtsBackwardSourceRunner.kt | 2 +- .../dataflow/ts/ifds/EtsForwardMethodRunner.kt | 7 ++++--- .../dataflow/ts/ifds/EtsForwardSourceRunner.kt | 2 +- 5 files changed, 17 insertions(+), 14 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt index 8b8f1fee10..cfb1621e32 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt @@ -28,14 +28,16 @@ class EtsBackwardIfdsRunner( private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) private val methods = graph.cp.projectAndSdkClasses.flatMap { it.methods + it.ctor } - private val runners = methods.associateWith { EtsBackwardMethodRunner( - graph = graph, - method = it, - analyzer = analyzer, - traits = traits, - manager = manager, - commonRunner = this@EtsBackwardIfdsRunner - ) } + private val runners = methods.associateWith { + EtsBackwardMethodRunner( + graph = graph, + method = it, + analyzer = analyzer, + traits = traits, + manager = manager, + commonRunner = this@EtsBackwardIfdsRunner, + ) + } fun getMethodRunner(method: EtsMethod): EtsBackwardMethodRunner { return runners.getValue(method) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt index 731a808ae9..637744fdcf 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt @@ -83,7 +83,7 @@ class EtsBackwardMethodRunner( internal data class CalleeStart( val start: EtsStmt, - val flowFunction: FlowFunction + val flowFunction: FlowFunction, ) internal val callToStartFlowFunctions = stmts.map { stmt -> diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt index e2f6f51b8f..75fd1551ab 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt @@ -55,7 +55,7 @@ class EtsBackwardSourceRunner( internal val summaryEdges = hashSetOf>() private fun tabulationAlgorithmStep( - currentEdge: PathEdge + currentEdge: PathEdge, ) = with(traits) { val (currentIp, currentFact) = currentEdge val current = stmts[currentIp] diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt index a2581a3851..879cadd7e3 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt @@ -38,7 +38,7 @@ class EtsForwardMethodRunner( internal data class CalleeStart( val start: EtsStmt, - val flowFunction: FlowFunction + val flowFunction: FlowFunction, ) internal val sequentFlowFunction = stmts.map { @@ -60,8 +60,9 @@ class EtsForwardMethodRunner( } fun addStart() { - if (entrypoint == mockStmt) + if (entrypoint == mockStmt) { return + } val startFacts = flowSpace.obtainPossibleStartFacts(method) for (startFact in startFacts) { @@ -87,7 +88,7 @@ class EtsForwardMethodRunner( internal data class PathEdge( val end: Int, - val fact: Fact + val fact: Fact, ) private val sourceRunners = hashMapOf>() diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt index 57522b93cc..7f95dc8032 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt @@ -55,7 +55,7 @@ class EtsForwardSourceRunner( internal val summaryEdges = hashSetOf>() private fun tabulationAlgorithmStep( - currentEdge: PathEdge + currentEdge: PathEdge, ) = with(traits) { val (currentIp, currentFact) = currentEdge val current = stmts[currentIp] From aa0ffb97d22de746b08a27d47f1e1dc8983e2afc Mon Sep 17 00:00:00 2001 From: Artem Trubnikov <77829679+MForest7@users.noreply.github.com> Date: Mon, 12 May 2025 16:51:35 +0300 Subject: [PATCH 03/18] Update ci.yml --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d04bd49cf3..53f4137e8e 100644 --- a/.github/workflows/ci.yml +++ b/.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 From 60b13a4b0f5a5d7e4b3060343206a37df09b1e8a Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 15:20:00 +0300 Subject: [PATCH 04/18] cleanup --- .../ts/ifds/EtsBackwardMethodRunner.kt | 15 ++++++++++++++- .../ts/ifds/EtsBackwardSourceRunner.kt | 2 +- .../dataflow/ts/ifds/EtsForwardIfdsRunner.kt | 18 ++++++++++-------- .../dataflow/ts/ifds/EtsForwardMethodRunner.kt | 14 +++++++++++++- .../dataflow/ts/ifds/EtsForwardSourceRunner.kt | 2 +- .../dataflow/ts/infer/TypeInferenceManager.kt | 6 ++---- 6 files changed, 41 insertions(+), 16 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt index 637744fdcf..4a6fecb858 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt @@ -24,8 +24,15 @@ class EtsBackwardMethodRunner( ) { private val flowSpace = analyzer.flowFunctions + /** + * Remember only the sink since the source is specified by runner + * + * `ip` - index of the end statement + * + * `fact` - fact at the end statement + */ internal data class PathEdge( - val endIp: Int, + val ip: Int, val fact: Fact, ) @@ -68,6 +75,12 @@ class EtsBackwardMethodRunner( internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1)) internal val stmts = listOf(mockStmt) + method.cfg.stmts + internal val isExit = BooleanArray(stmts.size) { false }.apply { + for (exit in graph.exitPoints(method)) { + set(exit.index, true) + } + } + internal val EtsStmt.index: Int get() = location.index + 1 diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt index 75fd1551ab..a089c6e7e2 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt @@ -61,7 +61,7 @@ class EtsBackwardSourceRunner( val current = stmts[currentIp] val currentIsCall = getCallExpr(current) != null - val currentIsExit = current in exitpoints + val currentIsExit = methodRunner.isExit[currentIp] if (currentIsCall) { val callToReturnFlowFunction = callToReturnSiteFlowFunction[currentIp] diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt index ded4f4a08b..c50588cdea 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt @@ -28,14 +28,16 @@ class EtsForwardIfdsRunner( private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) private val methods = graph.cp.projectAndSdkClasses.flatMap { it.methods + it.ctor } - private val runners = methods.associateWith { EtsForwardMethodRunner( - graph = graph, - method = it, - analyzer = analyzer, - traits = traits, - manager = manager, - commonRunner = this@EtsForwardIfdsRunner - ) } + private val runners = methods.associateWith { + EtsForwardMethodRunner( + graph = graph, + method = it, + analyzer = analyzer, + traits = traits, + manager = manager, + commonRunner = this@EtsForwardIfdsRunner + ) + } fun getMethodRunner(method: EtsMethod): EtsForwardMethodRunner { return runners.getValue(method) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt index 879cadd7e3..bea0a4ab17 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt @@ -29,6 +29,11 @@ class EtsForwardMethodRunner( internal val cfg = method.cfg internal val stmts = method.cfg.stmts + internal val isExit = BooleanArray(stmts.size) { false }.apply { + for (exit in cfg.exits) { + set(exit.index, true) + } + } internal val successors = stmts.map { cfg.successors(it).map { s -> s.index } } internal val EtsStmt.index: Int @@ -86,8 +91,15 @@ class EtsForwardMethodRunner( enqueued = false } + /** + * Remember only the sink since the source is specified by runner + * + * `ip` - index of the end statement + * + * `fact` - fact at the end statement + */ internal data class PathEdge( - val end: Int, + val ip: Int, val fact: Fact, ) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt index 7f95dc8032..b1dc57fbd6 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt @@ -61,7 +61,7 @@ class EtsForwardSourceRunner( val current = stmts[currentIp] val currentIsCall = getCallExpr(current) != null - val currentIsExit = current in cfg.exits + val currentIsExit = methodRunner.isExit[currentIp] if (currentIsCall) { val callToReturnFlowFunction = callToReturnSiteFlowFunction[currentIp] diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index c5ab3d45fe..28c1ef525a 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -371,8 +371,7 @@ class TypeInferenceManager( .flatMap { (_, summaries) -> summaries.asSequence() } .mapNotNull { it.initialFact as? ForwardTypeDomainFact.TypedVariable } .filter { it.variable.base is AccessPathBase.This } - .distinct() - .toList() + .constrainOnce() val typeFactsOnThisCtor = forwardSummariesByClass[cls.signature].orEmpty() .asSequence() @@ -380,8 +379,7 @@ class TypeInferenceManager( .flatMap { (_, summaries) -> summaries.asSequence() } .mapNotNull { it.exitFact as? ForwardTypeDomainFact.TypedVariable } .filter { it.variable.base is AccessPathBase.This } - .distinct() - .toList() + .constrainOnce() val typeFactsOnThis = (typeFactsOnThisMethods + typeFactsOnThisCtor).distinct() From 0c427261a914c1eeff43cc5485dd00cd83a15b09 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 15:20:46 +0300 Subject: [PATCH 05/18] limit refinement depth --- .../org/usvm/dataflow/ts/infer/TypeInferenceManager.kt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index 28c1ef525a..a8dd018990 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -488,10 +488,14 @@ class TypeInferenceManager( return refinedTypes } + companion object { + private const val REFINEMENT_DEPTH_BOUND = 2 + } + private fun EtsTypeFact.refineProperties( pathFromRootObject: List, typeRefinements: Map, EtsTypeFact>, - ): EtsTypeFact = when (this) { + ): EtsTypeFact = if (pathFromRootObject.size >= REFINEMENT_DEPTH_BOUND) this else when (this) { is EtsTypeFact.NumberEtsTypeFact -> this is EtsTypeFact.StringEtsTypeFact -> this is EtsTypeFact.FunctionEtsTypeFact -> this From 93cdb8609c728b16cee033f6a1fbfa715cf82196 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 15:37:15 +0300 Subject: [PATCH 06/18] cleanup report --- .../ts/test/EtsTypeResolverPerformanceTest.kt | 4 ++-- .../usvm/dataflow/ts/test/utils/AbcProjects.kt | 13 +------------ .../dataflow/ts/test/utils/PerformanceReport.kt | 17 ++++++++++++----- 3 files changed, 15 insertions(+), 19 deletions(-) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt index 255e98ef9b..3e0ca9c3db 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt @@ -77,8 +77,8 @@ class EtsTypeResolverPerformanceTest { ) val reportStr = buildString { - appendLine("|project|min time|max time|avg time|median time|%|") - appendLine("|:--|:--|:--|:--|:--|:--|") + appendLine("|project|stmts|min time|max time|avg time|median time|%|") + appendLine("|:--|:--|:--|:--|:--|:--|:--|") reports.forEach { appendLine(it.dumpToString()) } diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt index 595c52d347..292694b377 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt @@ -22,14 +22,10 @@ import org.usvm.dataflow.ts.infer.EntryPointsProcessor import org.usvm.dataflow.ts.infer.TypeGuesser import org.usvm.dataflow.ts.infer.TypeInferenceManager import org.usvm.dataflow.ts.infer.TypeInferenceResult -import org.usvm.dataflow.ts.infer.annotation.annotateWithTypes import org.usvm.dataflow.ts.infer.createApplicationGraph -import org.usvm.dataflow.ts.infer.verify.VerificationResult -import org.usvm.dataflow.ts.infer.verify.verify import org.usvm.dataflow.ts.util.EtsTraits import kotlin.io.path.Path import kotlin.io.path.exists -import kotlin.test.assertTrue object AbcProjects { private const val yourPrefixForTestFolders = "REPLACE_ME" @@ -53,14 +49,7 @@ object AbcProjects { return result to statistics } - fun inferTypes(scene: EtsScene): TypeInferenceResult { - val abcScene = when (val result = verify(scene)) { - is VerificationResult.Success -> scene - is VerificationResult.Fail -> scene.annotateWithTypes(result.erasureScheme) - } - - assertTrue(verify(abcScene) is VerificationResult.Success) - + fun inferTypes(abcScene: EtsScene): TypeInferenceResult { val graphAbc = createApplicationGraph(abcScene) val guesser = TypeGuesser(abcScene) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt index 37a73c3df9..195430e488 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt @@ -23,6 +23,7 @@ import kotlin.time.measureTimedValue data class PerformanceReport( val projectId: String, + val totalStmts: Int, val maxTime: Duration, val avgTime: Duration, val medianTime: Duration, @@ -31,11 +32,12 @@ data class PerformanceReport( ) { fun dumpToString(): String = listOf( projectId, - minTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - maxTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - avgTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - medianTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - improvement.toBigDecimal().setScale(4, RoundingMode.HALF_UP).toDouble() + totalStmts, + minTime.toString(unit = DurationUnit.SECONDS, decimals = 2), + maxTime.toString(unit = DurationUnit.SECONDS, decimals = 2), + avgTime.toString(unit = DurationUnit.SECONDS, decimals = 2), + medianTime.toString(unit = DurationUnit.SECONDS, decimals = 2), + improvement.toBigDecimal().setScale(1, RoundingMode.HALF_UP).toDouble() ).joinToString( separator = "|", prefix = "|", @@ -63,8 +65,13 @@ fun generateReportForProject( val improvement = results.map { it.second }.distinct().first() val totalTime = times.reduce { acc, duration -> acc + duration } + val totalStmts = abcScene.projectClasses + .flatMap { it.methods } + .sumOf { it.cfg.stmts.size } + return PerformanceReport( projectId = projectId, + totalStmts = totalStmts, minTime = times.min(), maxTime = times.max(), avgTime = totalTime / runIterationsCount, From a65117a6a603e6958cbc12a0216e9a0a8376cc8a Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 15:40:05 +0300 Subject: [PATCH 07/18] cleanup --- .../dataflow/ts/infer/TypeInferenceManager.kt | 88 ++++++++++--------- 1 file changed, 46 insertions(+), 42 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index a8dd018990..b332b4e11d 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -495,56 +495,60 @@ class TypeInferenceManager( private fun EtsTypeFact.refineProperties( pathFromRootObject: List, typeRefinements: Map, EtsTypeFact>, - ): EtsTypeFact = if (pathFromRootObject.size >= REFINEMENT_DEPTH_BOUND) this else when (this) { - is EtsTypeFact.NumberEtsTypeFact -> this - is EtsTypeFact.StringEtsTypeFact -> this - is EtsTypeFact.FunctionEtsTypeFact -> this - is EtsTypeFact.AnyEtsTypeFact -> this - is EtsTypeFact.BooleanEtsTypeFact -> this - is EtsTypeFact.NullEtsTypeFact -> this - is EtsTypeFact.UndefinedEtsTypeFact -> this - - is EtsTypeFact.UnknownEtsTypeFact -> { - // logger.warn { "Unknown type after forward analysis" } - EtsTypeFact.AnyEtsTypeFact - } + ): EtsTypeFact { + if (pathFromRootObject.size >= REFINEMENT_DEPTH_BOUND) return this - is EtsTypeFact.ArrayEtsTypeFact -> { - // TODO: array types - // logger.warn { "TODO: Array type $this" } + return when (this) { + is EtsTypeFact.NumberEtsTypeFact -> this + is EtsTypeFact.StringEtsTypeFact -> this + is EtsTypeFact.FunctionEtsTypeFact -> this + is EtsTypeFact.AnyEtsTypeFact -> this + is EtsTypeFact.BooleanEtsTypeFact -> this + is EtsTypeFact.NullEtsTypeFact -> this + is EtsTypeFact.UndefinedEtsTypeFact -> this - val elementPath = pathFromRootObject + ElementAccessor - val refinedElemType = typeRefinements[elementPath]?.let { - typeProcessor.intersect(it, elementType) - } ?: elementType // TODO: consider throwing an exception - val elemType = refinedElemType.refineProperties(elementPath, typeRefinements) + is EtsTypeFact.UnknownEtsTypeFact -> { + // logger.warn { "Unknown type after forward analysis" } + EtsTypeFact.AnyEtsTypeFact + } - EtsTypeFact.ArrayEtsTypeFact(elemType) - } + is EtsTypeFact.ArrayEtsTypeFact -> { + // TODO: array types + // logger.warn { "TODO: Array type $this" } - is EtsTypeFact.ObjectEtsTypeFact -> refineProperties(pathFromRootObject, typeRefinements) + val elementPath = pathFromRootObject + ElementAccessor + val refinedElemType = typeRefinements[elementPath]?.let { + typeProcessor.intersect(it, elementType) + } ?: elementType // TODO: consider throwing an exception + val elemType = refinedElemType.refineProperties(elementPath, typeRefinements) - is EtsTypeFact.UnionEtsTypeFact -> EtsTypeFact.mkUnionType( - types.mapTo(hashSetOf()) { - it.refineProperties( - pathFromRootObject, - typeRefinements, - ) + EtsTypeFact.ArrayEtsTypeFact(elemType) } - ) - is EtsTypeFact.IntersectionEtsTypeFact -> EtsTypeFact.mkIntersectionType( - types.mapTo(hashSetOf()) { - it.refineProperties( - pathFromRootObject, - typeRefinements, - ) - } - ) + is EtsTypeFact.ObjectEtsTypeFact -> refineProperties(pathFromRootObject, typeRefinements) + + is EtsTypeFact.UnionEtsTypeFact -> EtsTypeFact.mkUnionType( + types.mapTo(hashSetOf()) { + it.refineProperties( + pathFromRootObject, + typeRefinements, + ) + } + ) - is EtsTypeFact.GuardedTypeFact -> type - .refineProperties(pathFromRootObject, typeRefinements) - .withGuard(guard, guardNegated) + is EtsTypeFact.IntersectionEtsTypeFact -> EtsTypeFact.mkIntersectionType( + types.mapTo(hashSetOf()) { + it.refineProperties( + pathFromRootObject, + typeRefinements, + ) + } + ) + + is EtsTypeFact.GuardedTypeFact -> type + .refineProperties(pathFromRootObject, typeRefinements) + .withGuard(guard, guardNegated) + } } private fun EtsTypeFact.ObjectEtsTypeFact.refineProperties( From 49f7a17d57a199787279c887f3b666970658e011 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 16:38:17 +0300 Subject: [PATCH 08/18] implemented Runner methods --- .../dataflow/ts/ifds/EtsBackwardIfdsRunner.kt | 19 ++++++++++++++++-- .../ts/ifds/EtsBackwardMethodRunner.kt | 3 +-- .../ts/ifds/EtsBackwardSourceRunner.kt | 12 ++++++++++- .../dataflow/ts/ifds/EtsForwardIfdsRunner.kt | 20 +++++++++++++++++-- .../ts/ifds/EtsForwardMethodRunner.kt | 2 +- .../ts/ifds/EtsForwardSourceRunner.kt | 12 ++++++++++- .../dataflow/ts/infer/TypeInferenceManager.kt | 6 ++++-- 7 files changed, 63 insertions(+), 11 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt index cfb1621e32..359eef7158 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt @@ -22,6 +22,7 @@ class EtsBackwardIfdsRunner( val analyzer: Analyzer, val traits: EtsTraits, val manager: TypeInferenceManager, + private val zeroFact: Fact, ) : Runner { val queue: ArrayDeque> = ArrayDeque() @@ -65,10 +66,24 @@ class EtsBackwardIfdsRunner( get() = SingletonUnit override fun getIfdsResult(): IfdsResult { - TODO("Not yet implemented") + val sourceRunners = runners.values.flatMap { methodRunner -> + methodRunner.sourceRunners.values.flatMap { it.values } + } + val pathEdges = sourceRunners.flatMap { it.getPathEdges() } + + val resultFacts: MutableMap> = 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, reason: Reason) { - TODO("Not yet implemented") + val (startVertex, endVertex) = edge + val (endStmt, endFact) = endVertex + + val localPathEdge = EtsBackwardMethodRunner.PathEdge(endStmt.location.index, endFact) + getMethodRunner(startVertex.statement.method).getSourceRunner(startVertex).propagate(localPathEdge) } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt index 4a6fecb858..c2e1a74d92 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt @@ -55,7 +55,7 @@ class EtsBackwardMethodRunner( enqueued = false } - private val sourceRunners = hashMapOf>>() + internal val sourceRunners = hashMapOf>>() internal fun getSourceRunner(vertex: Vertex): EtsBackwardSourceRunner { return sourceRunners .getOrPut(vertex.fact) { hashMapOf() } @@ -111,7 +111,6 @@ class EtsBackwardMethodRunner( } internal val entrypoints = graph.entryPoints(method).toList() - internal val exitpoints = graph.exitPoints(method).toList() fun addStart() { val startFacts = flowSpace.obtainPossibleStartFacts(method) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt index a089c6e7e2..600f7c3ecf 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt @@ -24,7 +24,6 @@ class EtsBackwardSourceRunner( } private val successors = methodRunner.successors - private val exitpoints = methodRunner.exitpoints private val stmts = methodRunner.stmts private val mockStmt = methodRunner.mockStmt @@ -129,4 +128,15 @@ class EtsBackwardSourceRunner( } } } + + internal fun getPathEdges(): List> { + val startVertex = Vertex(entrypoint, startingFact) + return factsAtStmt.flatMapIndexed { index, facts -> + val stmt = stmts[index] + facts.map { + val endVertex = Vertex(stmt, it) + Edge(startVertex, endVertex) + } + } + } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt index c50588cdea..538ae39d1e 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt @@ -22,6 +22,7 @@ class EtsForwardIfdsRunner( val analyzer: Analyzer, val traits: EtsTraits, val manager: TypeInferenceManager, + private val zeroFact: Fact, ) : Runner { val queue: ArrayDeque> = ArrayDeque() @@ -69,10 +70,25 @@ class EtsForwardIfdsRunner( get() = SingletonUnit override fun getIfdsResult(): IfdsResult { - TODO("Not yet implemented") + val sourceRunners = runners.values.flatMap { methodRunner -> + methodRunner.sourceRunners.values + } + val pathEdges = sourceRunners.flatMap { it.getPathEdges() } + + val resultFacts: MutableMap> = 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, reason: Reason) { - TODO("Not yet implemented") + val (startVertex, endVertex) = edge + val (startStmt, startFact) = startVertex + val (endStmt, endFact) = endVertex + + val localPathEdge = EtsForwardMethodRunner.PathEdge(endStmt.location.index, endFact) + getMethodRunner(startStmt.method).getSourceRunner(startFact).propagate(localPathEdge) } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt index bea0a4ab17..40646bcf6e 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt @@ -103,7 +103,7 @@ class EtsForwardMethodRunner( val fact: Fact, ) - private val sourceRunners = hashMapOf>() + internal val sourceRunners = hashMapOf>() internal fun getSourceRunner(fact: Fact): EtsForwardSourceRunner { return sourceRunners.getOrPut(fact) { EtsForwardSourceRunner(traits, this, fact) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt index b1dc57fbd6..a77e1359a1 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt @@ -22,7 +22,6 @@ class EtsForwardSourceRunner( enqueued = false } - private val cfg = methodRunner.cfg private val successors = methodRunner.successors private val stmts = methodRunner.stmts private val mockStmt = methodRunner.mockStmt @@ -127,4 +126,15 @@ class EtsForwardSourceRunner( } } } + + internal fun getPathEdges(): List> { + val startVertex = Vertex(entrypoint, startingFact) + return factsAtStmt.flatMapIndexed { index, facts -> + val stmt = stmts[index] + facts.map { + val endVertex = Vertex(stmt, it) + Edge(startVertex, endVertex) + } + } + } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index b332b4e11d..8220e17bd5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -118,7 +118,8 @@ class TypeInferenceManager( graph = backwardGraph, analyzer = backwardAnalyzer, traits = traits, - manager = this + manager = this, + zeroFact = BackwardTypeDomainFact.Zero, ) this@TypeInferenceManager.backwardRunner = backwardRunner @@ -203,6 +204,7 @@ class TypeInferenceManager( analyzer = forwardAnalyzer, traits = traits, manager = this, + zeroFact = ForwardTypeDomainFact.Zero, ) this@TypeInferenceManager.forwardRunner = forwardRunner @@ -519,7 +521,7 @@ class TypeInferenceManager( val elementPath = pathFromRootObject + ElementAccessor val refinedElemType = typeRefinements[elementPath]?.let { typeProcessor.intersect(it, elementType) - } ?: elementType // TODO: consider throwing an exception + } ?: elementType // TODO: consider throwing an exception val elemType = refinedElemType.refineProperties(elementPath, typeRefinements) EtsTypeFact.ArrayEtsTypeFact(elemType) From 3d739315cfbdf27ec1dc3d5aa3e97eb872cd201a Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 17:06:09 +0300 Subject: [PATCH 09/18] cleanup --- .../usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt | 11 +++++++---- .../org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt | 3 --- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt index 600f7c3ecf..1d0a3e5a3f 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt @@ -33,16 +33,19 @@ class EtsBackwardSourceRunner( private val factsAtStmt = Array(stmts.size) { hashSetOf() } - internal fun propagate(edge: PathEdge) { - val (endIp, endFact) = edge + internal fun propagate(localEdge: PathEdge) { + val (endIp, endFact) = localEdge if (factsAtStmt[endIp].add(endFact)) { val startVertex = Vertex(mockStmt, startingFact) val endVertex = Vertex(stmts[endIp], endFact) - for (event in methodRunner.analyzer.handleNewEdge(Edge(startVertex, endVertex))) { + val edge = Edge(startVertex, endVertex) + val events = methodRunner.analyzer.handleNewEdge(edge) + + for (event in events) { methodRunner.manager.handleEvent(event) } - internalQueue.add(edge) + internalQueue.add(localEdge) if (!enqueued) { enqueued = true methodRunner.enqueue(this) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt index 538ae39d1e..47fa88c8a0 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt @@ -48,9 +48,6 @@ class EtsForwardIfdsRunner( for (method in startMethods) { val runner = runners[method] ?: continue runner.addStart() - /*for ((stmt, fact) in backwardFacts[method].orEmpty()) { - runner.submitFact(stmt, fact) - }*/ } tabulationAlgorithm() From 6f2b07134886945c3c6f4ef07698972fa5babb4a Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 18:06:06 +0300 Subject: [PATCH 10/18] fixed liveness analysis --- .../usvm/dataflow/ts/infer/LiveVariables.kt | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt index 2b9a715a65..ac113e4afe 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt @@ -13,6 +13,7 @@ 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.EtsParameterRef import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsThrowStmt @@ -51,6 +52,7 @@ class LiveVariablesImpl( private fun EtsValue.used(): List = when (this) { is EtsLocal -> listOf(name) + is EtsParameterRef -> listOf("arg($index)") is EtsInstanceFieldRef -> listOf(instance.name) is EtsArrayAccess -> array.used() + index.used() else -> emptyList() @@ -83,13 +85,9 @@ class LiveVariablesImpl( } aliveAtStmt = Array(method.cfg.stmts.size) { emptyBitSet() } - - val queue = method.cfg.stmts.toHashSet() - while (queue.isNotEmpty()) { - val stmt = queue.first() - queue.remove(stmt) - - val aliveHere = emptyBitSet().apply { + val usedAtStmt = Array(method.cfg.stmts.size) { ip -> + val stmt = method.cfg.stmts[ip] + emptyBitSet().apply { val usedLocals = when (stmt) { is EtsAssignStmt -> stmt.lhv.used() + stmt.rhv.used() is EtsCallStmt -> stmt.expr.used() @@ -101,6 +99,13 @@ class LiveVariablesImpl( usedLocals.mapNotNull { indexOfName[it] }.forEach { set(it) } } + } + + val queue = ArrayDeque(method.cfg.stmts) + while (queue.isNotEmpty()) { + val stmt = queue.removeFirst() + + val aliveHere = usedAtStmt[stmt.location.index] for (succ in method.cfg.successors(stmt)) { val transferFromSucc = aliveAtStmt[succ.location.index].copy() From 555fa02662e43491e3f16c6ad4cbfcb3a7fda92c Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 18:19:45 +0300 Subject: [PATCH 11/18] removed duplicated liveness analysis --- .../kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt | 8 +------- .../org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt | 2 +- 2 files changed, 2 insertions(+), 8 deletions(-) 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 index 18aa7f6da8..7e6f782f0a 100644 --- 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,17 +34,11 @@ class ForwardAnalyzer( error("No cross unit calls") } - private val liveVariablesCache = hashMapOf() - 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 !flowFunctions.liveVariables(stmt.method).isAliveAt(base.name, stmt) } override fun handleNewEdge(edge: Edge): List { 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 index 322d37f046..8bdfadbb06 100644 --- 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 @@ -66,7 +66,7 @@ class ForwardFlowFunctions( } private val liveVariablesCache = hashMapOf() - private fun liveVariables(method: EtsMethod) = + internal fun liveVariables(method: EtsMethod) = liveVariablesCache.computeIfAbsent(method) { if (doLiveVariablesAnalysis) { LiveVariables.from(method) From 6074060806899d7b98cff0fc24a95377150013bf Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 13 May 2025 18:23:25 +0300 Subject: [PATCH 12/18] Format --- .../org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt | 2 +- .../org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt index 47fa88c8a0..6d88095deb 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt @@ -2,8 +2,8 @@ package org.usvm.dataflow.ts.ifds import kotlinx.coroutines.coroutineScope import kotlinx.coroutines.isActive -import org.jacodb.ets.model.EtsStmt 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 diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt index 40646bcf6e..76748ff07d 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt @@ -1,9 +1,9 @@ package org.usvm.dataflow.ts.ifds -import org.jacodb.ets.model.EtsStmtLocation +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmtLocation import org.jacodb.ets.utils.callExpr import org.usvm.dataflow.ifds.Analyzer import org.usvm.dataflow.ifds.Edge @@ -97,7 +97,7 @@ class EtsForwardMethodRunner( * `ip` - index of the end statement * * `fact` - fact at the end statement - */ + */ internal data class PathEdge( val ip: Int, val fact: Fact, From b87ea78622eee224d1024c1514f22b1ccb651aae Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 13 May 2025 19:20:11 +0300 Subject: [PATCH 13/18] cleanup --- .../dataflow/ts/ifds/EtsBackwardIfdsRunner.kt | 25 +++++++++---------- .../ts/ifds/EtsBackwardMethodRunner.kt | 2 +- .../dataflow/ts/ifds/EtsForwardIfdsRunner.kt | 25 +++++++++---------- .../ts/ifds/EtsForwardMethodRunner.kt | 2 +- .../usvm/dataflow/ts/infer/ForwardAnalyzer.kt | 8 +++--- .../usvm/dataflow/ts/infer/LiveVariables.kt | 2 +- .../ts/test/utils/PerformanceReport.kt | 8 +++--- 7 files changed, 36 insertions(+), 36 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt index 359eef7158..83b97e15b9 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt @@ -28,25 +28,24 @@ class EtsBackwardIfdsRunner( private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) - private val methods = graph.cp.projectAndSdkClasses.flatMap { it.methods + it.ctor } - private val runners = methods.associateWith { - EtsBackwardMethodRunner( - graph = graph, - method = it, - analyzer = analyzer, - traits = traits, - manager = manager, - commonRunner = this@EtsBackwardIfdsRunner, - ) - } + private val runners = mutableMapOf>() fun getMethodRunner(method: EtsMethod): EtsBackwardMethodRunner { - return runners.getValue(method) + return runners.getOrPut(method) { + EtsBackwardMethodRunner( + graph = graph, + method = method, + analyzer = analyzer, + traits = traits, + manager = manager, + commonRunner = this@EtsBackwardIfdsRunner, + ) + } } override suspend fun run(startMethods: List) { for (method in startMethods) { - runners[method]?.addStart() + getMethodRunner(method).addStart() } tabulationAlgorithm() diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt index c2e1a74d92..bffae62a59 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt @@ -27,7 +27,7 @@ class EtsBackwardMethodRunner( /** * Remember only the sink since the source is specified by runner * - * `ip` - index of the end statement + * `ip` - index of the end statement (instruction pointer) * * `fact` - fact at the end statement */ diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt index 6d88095deb..8b95c73d44 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt @@ -28,25 +28,24 @@ class EtsForwardIfdsRunner( private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) - private val methods = graph.cp.projectAndSdkClasses.flatMap { it.methods + it.ctor } - private val runners = methods.associateWith { - EtsForwardMethodRunner( - graph = graph, - method = it, - analyzer = analyzer, - traits = traits, - manager = manager, - commonRunner = this@EtsForwardIfdsRunner - ) - } + private val runners = mutableMapOf>() fun getMethodRunner(method: EtsMethod): EtsForwardMethodRunner { - return runners.getValue(method) + return runners.getOrPut(method) { + EtsForwardMethodRunner( + graph = graph, + method = method, + analyzer = analyzer, + traits = traits, + manager = manager, + commonRunner = this@EtsForwardIfdsRunner + ) + } } override suspend fun run(startMethods: List) { for (method in startMethods) { - val runner = runners[method] ?: continue + val runner = getMethodRunner(method) runner.addStart() } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt index 76748ff07d..e52898f4aa 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt @@ -94,7 +94,7 @@ class EtsForwardMethodRunner( /** * Remember only the sink since the source is specified by runner * - * `ip` - index of the end statement + * `ip` - index of the end statement (instruction pointer) * * `fact` - fact at the end statement */ 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 index 7e6f782f0a..040ce06d2f 100644 --- 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 @@ -36,9 +36,11 @@ class ForwardAnalyzer( 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 !flowFunctions.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): List { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt index ac113e4afe..4fa0668dd5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt @@ -25,7 +25,7 @@ interface LiveVariables { fun isAliveAt(local: String, stmt: EtsStmt): Boolean companion object { - private const val THRESHOLD: Int = 20 + private const val THRESHOLD: Int = 10 fun from(method: EtsMethod): LiveVariables = if (method.cfg.stmts.size > THRESHOLD) LiveVariablesImpl(method) else AlwaysAlive diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt index 195430e488..b01781c046 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt @@ -33,10 +33,10 @@ data class PerformanceReport( fun dumpToString(): String = listOf( projectId, totalStmts, - minTime.toString(unit = DurationUnit.SECONDS, decimals = 2), - maxTime.toString(unit = DurationUnit.SECONDS, decimals = 2), - avgTime.toString(unit = DurationUnit.SECONDS, decimals = 2), - medianTime.toString(unit = DurationUnit.SECONDS, decimals = 2), + minTime.toString(unit = DurationUnit.SECONDS, decimals = 1), + maxTime.toString(unit = DurationUnit.SECONDS, decimals = 1), + avgTime.toString(unit = DurationUnit.SECONDS, decimals = 1), + medianTime.toString(unit = DurationUnit.SECONDS, decimals = 1), improvement.toBigDecimal().setScale(1, RoundingMode.HALF_UP).toDouble() ).joinToString( separator = "|", From 6a8742b7211bffcba3f0c978cb126ac44aadaff0 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 14 May 2025 23:57:03 +0300 Subject: [PATCH 14/18] Use hash map --- .../kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt index 83b97e15b9..673a821f19 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt @@ -28,7 +28,7 @@ class EtsBackwardIfdsRunner( private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) - private val runners = mutableMapOf>() + private val runners = hashMapOf>() fun getMethodRunner(method: EtsMethod): EtsBackwardMethodRunner { return runners.getOrPut(method) { From beca4f69368310b1297161f3a4faacef7153048b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 14 May 2025 23:57:24 +0300 Subject: [PATCH 15/18] Use default boolean array value (false) --- .../kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt index e52898f4aa..e0bb953768 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt @@ -29,7 +29,7 @@ class EtsForwardMethodRunner( internal val cfg = method.cfg internal val stmts = method.cfg.stmts - internal val isExit = BooleanArray(stmts.size) { false }.apply { + internal val isExit = BooleanArray(stmts.size).apply { for (exit in cfg.exits) { set(exit.index, true) } From e8b4c9b7e409579b41d9d43d6b8830caf67032fc Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 14 May 2025 23:57:32 +0300 Subject: [PATCH 16/18] Reorder --- .../kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt index a77e1359a1..a660f2b8c6 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt @@ -84,8 +84,8 @@ class EtsForwardSourceRunner( // Save info about the call for summary edges that will be found later: val calleeRunner = methodRunner.commonRunner.getMethodRunner(callee) - val startingVertex = Vertex(entrypoint, startingFact) val currentVertex = Vertex(current, currentFact) + val startingVertex = Vertex(entrypoint, startingFact) val callerEdge = Edge(startingVertex, currentVertex) calleeRunner.getSourceRunner(calleeStartFact).callerPathEdges.add(callerEdge) From c98010cd9a18352f29158cb1a6e162974ec30200 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 20 May 2025 11:20:11 +0300 Subject: [PATCH 17/18] unified ifds runner --- .../ts/ifds/EtsBackwardSourceRunner.kt | 145 ----------------- .../dataflow/ts/ifds/EtsForwardIfdsRunner.kt | 90 ----------- .../ts/ifds/EtsForwardMethodRunner.kt | 144 ----------------- .../ts/ifds/EtsForwardSourceRunner.kt | 140 ----------------- ...MethodRunner.kt => EtsIfdsMethodRunner.kt} | 73 +++------ ...BackwardIfdsRunner.kt => EtsIfdsRunner.kt} | 21 ++- .../dataflow/ts/ifds/EtsIfdsSourceRunner.kt | 147 ++++++++++++++++++ .../dataflow/ts/infer/TypeInferenceManager.kt | 11 +- 8 files changed, 181 insertions(+), 590 deletions(-) delete mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt delete mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt delete mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt delete mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt rename usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/{EtsBackwardMethodRunner.kt => EtsIfdsMethodRunner.kt} (62%) rename usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/{EtsBackwardIfdsRunner.kt => EtsIfdsRunner.kt} (78%) create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsSourceRunner.kt diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt deleted file mode 100644 index 1d0a3e5a3f..0000000000 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardSourceRunner.kt +++ /dev/null @@ -1,145 +0,0 @@ -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.EtsBackwardMethodRunner.PathEdge -import org.usvm.dataflow.ts.util.EtsTraits - -class EtsBackwardSourceRunner( - val traits: EtsTraits, - val methodRunner: EtsBackwardMethodRunner, - val entrypoint: EtsStmt, - val startingFact: Fact, -) { - private var enqueued: Boolean = false - private val internalQueue: ArrayDeque> = ArrayDeque() - - fun processFacts() { - while (!internalQueue.isEmpty()) { - val currentEdge = internalQueue.removeFirst() - tabulationAlgorithmStep(currentEdge) - } - enqueued = false - } - - private val successors = methodRunner.successors - private val stmts = methodRunner.stmts - private val mockStmt = methodRunner.mockStmt - - private val callToReturnSiteFlowFunction = methodRunner.callToReturnSiteFlowFunction - private val callToStartFlowFunctions = methodRunner.callToStartFlowFunctions - private val sequentFlowFunction = methodRunner.sequentFlowFunction - - private val factsAtStmt = Array(stmts.size) { hashSetOf() } - - internal fun propagate(localEdge: PathEdge) { - val (endIp, endFact) = localEdge - if (factsAtStmt[endIp].add(endFact)) { - val startVertex = Vertex(mockStmt, startingFact) - val endVertex = Vertex(stmts[endIp], endFact) - val edge = Edge(startVertex, endVertex) - val events = methodRunner.analyzer.handleNewEdge(edge) - - for (event in events) { - methodRunner.manager.handleEvent(event) - } - - internalQueue.add(localEdge) - if (!enqueued) { - enqueued = true - methodRunner.enqueue(this) - } - } - } - - private val callerPathEdges = hashSetOf>() - internal val summaryEdges = hashSetOf>() - - private fun tabulationAlgorithmStep( - currentEdge: PathEdge, - ) = with(traits) { - val (currentIp, currentFact) = currentEdge - val current = stmts[currentIp] - - val currentIsCall = getCallExpr(current) != null - val currentIsExit = methodRunner.isExit[currentIp] - - if (currentIsCall) { - val callToReturnFlowFunction = callToReturnSiteFlowFunction[currentIp] - if (callToReturnFlowFunction != null) { - // Propagate through the call-to-return-site edge: - val factsAtReturnSite = callToReturnFlowFunction.compute(currentFact) - for (returnSite in successors[currentIp]) { - for (returnSiteFact in factsAtReturnSite) { - val edge = PathEdge(returnSite, returnSiteFact) - propagate(edge) - } - } - } - - for ((calleeStart, callToStartFlowFunction) in callToStartFlowFunctions[currentIp]) { - val callee = calleeStart.method - 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(current, 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(current, 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 = sequentFlowFunction[currentIp].compute(currentFact) - for (next in successors[currentIp]) { - for (nextFact in factsAtNext) { - val edge = PathEdge(next, nextFact) - propagate(edge) - } - } - } - } - - internal fun getPathEdges(): List> { - val startVertex = Vertex(entrypoint, startingFact) - return factsAtStmt.flatMapIndexed { index, facts -> - val stmt = stmts[index] - facts.map { - val endVertex = Vertex(stmt, it) - Edge(startVertex, endVertex) - } - } - } -} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt deleted file mode 100644 index 8b95c73d44..0000000000 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardIfdsRunner.kt +++ /dev/null @@ -1,90 +0,0 @@ -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 EtsForwardIfdsRunner( - override val graph: EtsApplicationGraph, - val analyzer: Analyzer, - val traits: EtsTraits, - val manager: TypeInferenceManager, - private val zeroFact: Fact, -) : Runner { - val queue: ArrayDeque> = ArrayDeque() - - private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) - - private val runners = mutableMapOf>() - - fun getMethodRunner(method: EtsMethod): EtsForwardMethodRunner { - return runners.getOrPut(method) { - EtsForwardMethodRunner( - graph = graph, - method = method, - analyzer = analyzer, - traits = traits, - manager = manager, - commonRunner = this@EtsForwardIfdsRunner - ) - } - } - - override suspend fun run(startMethods: List) { - for (method in startMethods) { - val runner = getMethodRunner(method) - runner.addStart() - } - - tabulationAlgorithm() - } - - private suspend fun tabulationAlgorithm() = coroutineScope { - while (isActive) { - val current = queue.removeFirstOrNull() ?: run { - manager.handleControlEvent(queueIsEmpty) - return@coroutineScope - } - current.processFacts() - } - } - - override val unit: UnitType - get() = SingletonUnit - - override fun getIfdsResult(): IfdsResult { - val sourceRunners = runners.values.flatMap { methodRunner -> - methodRunner.sourceRunners.values - } - val pathEdges = sourceRunners.flatMap { it.getPathEdges() } - - val resultFacts: MutableMap> = 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, reason: Reason) { - val (startVertex, endVertex) = edge - val (startStmt, startFact) = startVertex - val (endStmt, endFact) = endVertex - - val localPathEdge = EtsForwardMethodRunner.PathEdge(endStmt.location.index, endFact) - getMethodRunner(startStmt.method).getSourceRunner(startFact).propagate(localPathEdge) - } -} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt deleted file mode 100644 index e0bb953768..0000000000 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardMethodRunner.kt +++ /dev/null @@ -1,144 +0,0 @@ -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.jacodb.ets.utils.callExpr -import org.usvm.dataflow.ifds.Analyzer -import org.usvm.dataflow.ifds.Edge -import org.usvm.dataflow.ifds.FlowFunction -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 - -class EtsForwardMethodRunner( - val graph: EtsApplicationGraph, - val method: EtsMethod, - val analyzer: Analyzer, - val traits: EtsTraits, - val manager: TypeInferenceManager, - val commonRunner: EtsForwardIfdsRunner, -) { - private val flowSpace = analyzer.flowFunctions - - private var enqueued: Boolean = false - private val queue: ArrayDeque> = ArrayDeque() - - internal val cfg = method.cfg - internal val stmts = method.cfg.stmts - internal val isExit = BooleanArray(stmts.size).apply { - for (exit in cfg.exits) { - set(exit.index, true) - } - } - internal val successors = stmts.map { cfg.successors(it).map { s -> s.index } } - - internal val EtsStmt.index: Int - get() = location.index - internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1)) - internal val entrypoint = stmts.firstOrNull() ?: mockStmt - - internal data class CalleeStart( - val start: EtsStmt, - val flowFunction: FlowFunction, - ) - - internal val sequentFlowFunction = stmts.map { - flowSpace.obtainSequentFlowFunction(it, mockStmt) - } - internal val callToReturnSiteFlowFunction = stmts.map { stmt -> - flowSpace.takeIf { stmt.callExpr != null } - ?.obtainCallToReturnSiteFlowFunction(stmt, mockStmt) - } - internal val callToStartFlowFunctions = stmts.map { stmt -> - val flowFunctions = mutableListOf>() - for (callee in graph.callees(stmt)) { - for (calleeStart in graph.entryPoints(callee)) { - val flowFunction = flowSpace.obtainCallToStartFlowFunction(stmt, calleeStart) - flowFunctions.add(CalleeStart(calleeStart, flowFunction)) - } - } - flowFunctions - } - - fun addStart() { - if (entrypoint == mockStmt) { - return - } - - val startFacts = flowSpace.obtainPossibleStartFacts(method) - for (startFact in startFacts) { - propagateStartingFact(startFact) - } - } - - internal fun enqueue(runner: EtsForwardSourceRunner) { - queue.addLast(runner) - if (!enqueued) { - commonRunner.queue.addLast(this) - enqueued = true - } - } - - fun processFacts() { - while (!queue.isEmpty()) { - val currentSourceRunner = queue.removeFirst() - currentSourceRunner.processFacts() - } - enqueued = false - } - - /** - * Remember only the sink since the source is specified by runner - * - * `ip` - index of the end statement (instruction pointer) - * - * `fact` - fact at the end statement - */ - internal data class PathEdge( - val ip: Int, - val fact: Fact, - ) - - internal val sourceRunners = hashMapOf>() - internal fun getSourceRunner(fact: Fact): EtsForwardSourceRunner { - return sourceRunners.getOrPut(fact) { - EtsForwardSourceRunner(traits, this, fact) - } - } - - internal fun propagateStartingFact(fact: Fact): Set> { - if (entrypoint == mockStmt) { - return emptySet() - } - val sourceRunner = getSourceRunner(fact) - sourceRunner.propagate(PathEdge(0, fact)) - return sourceRunner.summaryEdges - } - - internal fun handleSummaryEdgeInCaller( - currentEdge: Edge, - summaryEdge: Edge, - ) { - val (startVertex, currentVertex) = currentEdge - val sourceRunner = getSourceRunner(startVertex.fact) - 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}" - } -} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt deleted file mode 100644 index a660f2b8c6..0000000000 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsForwardSourceRunner.kt +++ /dev/null @@ -1,140 +0,0 @@ -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.EtsForwardMethodRunner.PathEdge -import org.usvm.dataflow.ts.util.EtsTraits - -class EtsForwardSourceRunner( - val traits: EtsTraits, - val methodRunner: EtsForwardMethodRunner, - val startingFact: Fact, -) { - private var enqueued: Boolean = false - private val internalQueue: ArrayDeque> = ArrayDeque() - - fun processFacts() { - while (!internalQueue.isEmpty()) { - val currentEdge = internalQueue.removeFirst() - tabulationAlgorithmStep(currentEdge) - } - enqueued = false - } - - private val successors = methodRunner.successors - private val stmts = methodRunner.stmts - private val mockStmt = methodRunner.mockStmt - private val entrypoint = methodRunner.entrypoint - - private val callToReturnSiteFlowFunction = methodRunner.callToReturnSiteFlowFunction - private val callToStartFlowFunctions = methodRunner.callToStartFlowFunctions - private val sequentFlowFunction = methodRunner.sequentFlowFunction - - private val factsAtStmt = Array(stmts.size) { hashSetOf() } - - internal fun propagate(edge: PathEdge) { - val (ip, fact) = edge - if (factsAtStmt[ip].add(fact)) { - val startVertex = Vertex(mockStmt, startingFact) - val endVertex = Vertex(stmts[ip], fact) - for (event in methodRunner.analyzer.handleNewEdge(Edge(startVertex, endVertex))) { - methodRunner.manager.handleEvent(event) - } - - internalQueue.add(edge) - if (!enqueued) { - enqueued = true - methodRunner.enqueue(this) - } - } - } - - private val callerPathEdges = hashSetOf>() - internal val summaryEdges = hashSetOf>() - - private fun tabulationAlgorithmStep( - currentEdge: PathEdge, - ) = with(traits) { - val (currentIp, currentFact) = currentEdge - val current = stmts[currentIp] - - val currentIsCall = getCallExpr(current) != null - val currentIsExit = methodRunner.isExit[currentIp] - - if (currentIsCall) { - val callToReturnFlowFunction = callToReturnSiteFlowFunction[currentIp] - if (callToReturnFlowFunction != null) { - // Propagate through the call-to-return-site edge: - val factsAtReturnSite = callToReturnFlowFunction.compute(currentFact) - for (returnSite in successors[currentIp]) { - for (returnSiteFact in factsAtReturnSite) { - val edge = PathEdge(returnSite, returnSiteFact) - propagate(edge) - } - } - } - - for ((calleeStart, callToStartFlowFunction) in callToStartFlowFunctions[currentIp]) { - val callee = calleeStart.method - 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(current, currentFact) - val startingVertex = Vertex(entrypoint, startingFact) - val callerEdge = Edge(startingVertex, currentVertex) - calleeRunner.getSourceRunner(calleeStartFact).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(current, 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 = sequentFlowFunction[currentIp].compute(currentFact) - for (next in successors[currentIp]) { - for (nextFact in factsAtNext) { - val edge = PathEdge(next, nextFact) - propagate(edge) - } - } - } - } - - internal fun getPathEdges(): List> { - val startVertex = Vertex(entrypoint, startingFact) - return factsAtStmt.flatMapIndexed { index, facts -> - val stmt = stmts[index] - facts.map { - val endVertex = Vertex(stmt, it) - Edge(startVertex, endVertex) - } - } - } -} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt similarity index 62% rename from usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt rename to usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt index bffae62a59..edc1d7c9ef 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt @@ -4,70 +4,55 @@ 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.jacodb.ets.utils.callExpr import org.usvm.dataflow.ifds.Analyzer import org.usvm.dataflow.ifds.Edge -import org.usvm.dataflow.ifds.FlowFunction 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 -class EtsBackwardMethodRunner( +internal class EtsIfdsMethodRunner( val graph: EtsApplicationGraph, val method: EtsMethod, val analyzer: Analyzer, val traits: EtsTraits, val manager: TypeInferenceManager, - val commonRunner: EtsBackwardIfdsRunner, + val commonRunner: EtsIfdsRunner, ) { - private val flowSpace = analyzer.flowFunctions - - /** - * Remember only the sink since the source is specified by runner - * - * `ip` - index of the end statement (instruction pointer) - * - * `fact` - fact at the end statement - */ - internal data class PathEdge( - val ip: Int, - val fact: Fact, - ) - + internal val flowSpace = analyzer.flowFunctions private var enqueued: Boolean = false - private val queue: ArrayDeque> = ArrayDeque() + private val sourceRunnersQueue: ArrayDeque> = ArrayDeque() - internal fun enqueue(runner: EtsBackwardSourceRunner) { - queue.addLast(runner) + internal fun enqueue(runner: EtsIfdsSourceRunner) { + sourceRunnersQueue.addLast(runner) if (!enqueued) { - commonRunner.queue.addLast(this) + commonRunner.methodRunnersQueue.addLast(this) enqueued = true } } fun processFacts() { - while (!queue.isEmpty()) { - val currentSourceRunner = queue.removeFirst() + while (!sourceRunnersQueue.isEmpty()) { + val currentSourceRunner = sourceRunnersQueue.removeFirst() currentSourceRunner.processFacts() } enqueued = false } - internal val sourceRunners = hashMapOf>>() - internal fun getSourceRunner(vertex: Vertex): EtsBackwardSourceRunner { + internal val sourceRunners = hashMapOf>>() + internal fun getSourceRunner(vertex: Vertex): EtsIfdsSourceRunner { return sourceRunners .getOrPut(vertex.fact) { hashMapOf() } .getOrPut(vertex.statement) { - EtsBackwardSourceRunner(traits, this, vertex.statement, vertex.fact) + EtsIfdsSourceRunner(traits, this, vertex.statement, vertex.fact) } } - internal fun getSourceRunners(fact: Fact): Collection> { + internal fun getSourceRunners(fact: Fact): Collection> { return sourceRunners.getOrPut(fact) { entrypoints.associateWithTo(hashMapOf()) { - EtsBackwardSourceRunner(traits, this, it, fact) + EtsIfdsSourceRunner(traits, this, it, fact) } }.values } @@ -85,31 +70,6 @@ class EtsBackwardMethodRunner( get() = location.index + 1 internal val successors = stmts.map { graph.successors(it).map { s -> s.index } } - - internal val sequentFlowFunction = stmts.map { - flowSpace.obtainSequentFlowFunction(it, mockStmt) - } - internal val callToReturnSiteFlowFunction = stmts.map { stmt -> - flowSpace.takeIf { stmt.callExpr != null } - ?.obtainCallToReturnSiteFlowFunction(stmt, mockStmt) - } - - internal data class CalleeStart( - val start: EtsStmt, - val flowFunction: FlowFunction, - ) - - internal val callToStartFlowFunctions = stmts.map { stmt -> - val flowFunctions = mutableListOf>() - for (callee in graph.callees(stmt)) { - for (calleeStart in graph.entryPoints(callee)) { - val flowFunction = flowSpace.obtainCallToStartFlowFunction(stmt, calleeStart) - flowFunctions.add(CalleeStart(calleeStart, flowFunction)) - } - } - flowFunctions - } - internal val entrypoints = graph.entryPoints(method).toList() fun addStart() { @@ -119,6 +79,11 @@ class EtsBackwardMethodRunner( } } + internal data class PathEdge( + val endStmtIndex: Int, + val fact: Fact, + ) + internal fun propagateStartingFact(fact: Fact): Set> { val summaryEdges = hashSetOf>() for (entrypoint in entrypoints) { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt similarity index 78% rename from usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt rename to usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt index 673a821f19..70f159e8d5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsBackwardIfdsRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt @@ -17,28 +17,27 @@ import org.usvm.dataflow.ts.infer.AnalyzerEvent import org.usvm.dataflow.ts.infer.TypeInferenceManager import org.usvm.dataflow.ts.util.EtsTraits -class EtsBackwardIfdsRunner( +class EtsIfdsRunner( override val graph: EtsApplicationGraph, val analyzer: Analyzer, val traits: EtsTraits, val manager: TypeInferenceManager, private val zeroFact: Fact, ) : Runner { - val queue: ArrayDeque> = ArrayDeque() - + internal val methodRunnersQueue: ArrayDeque> = ArrayDeque() private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) - private val runners = hashMapOf>() + private val methodRunners = hashMapOf>() - fun getMethodRunner(method: EtsMethod): EtsBackwardMethodRunner { - return runners.getOrPut(method) { - EtsBackwardMethodRunner( + internal fun getMethodRunner(method: EtsMethod): EtsIfdsMethodRunner { + return methodRunners.getOrPut(method) { + EtsIfdsMethodRunner( graph = graph, method = method, analyzer = analyzer, traits = traits, manager = manager, - commonRunner = this@EtsBackwardIfdsRunner, + commonRunner = this@EtsIfdsRunner, ) } } @@ -53,7 +52,7 @@ class EtsBackwardIfdsRunner( private suspend fun tabulationAlgorithm() = coroutineScope { while (isActive) { - val current = queue.removeFirstOrNull() ?: run { + val current = methodRunnersQueue.removeFirstOrNull() ?: run { manager.handleControlEvent(queueIsEmpty) return@coroutineScope } @@ -65,7 +64,7 @@ class EtsBackwardIfdsRunner( get() = SingletonUnit override fun getIfdsResult(): IfdsResult { - val sourceRunners = runners.values.flatMap { methodRunner -> + val sourceRunners = methodRunners.values.flatMap { methodRunner -> methodRunner.sourceRunners.values.flatMap { it.values } } val pathEdges = sourceRunners.flatMap { it.getPathEdges() } @@ -82,7 +81,7 @@ class EtsBackwardIfdsRunner( val (startVertex, endVertex) = edge val (endStmt, endFact) = endVertex - val localPathEdge = EtsBackwardMethodRunner.PathEdge(endStmt.location.index, endFact) + val localPathEdge = EtsIfdsMethodRunner.PathEdge(endStmt.location.index, endFact) getMethodRunner(startVertex.statement.method).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 new file mode 100644 index 0000000000..8d3d475f5f --- /dev/null +++ b/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( + val traits: EtsTraits, + val methodRunner: EtsIfdsMethodRunner, + val entrypoint: EtsStmt, + val startingFact: Fact, +) { + private var enqueued: Boolean = false + private val pathEdgeQueue: ArrayDeque> = 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() } + + internal fun propagate(localEdge: PathEdge) { + 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>() + internal val summaryEdges = hashSetOf>() + + private fun tabulationAlgorithmStep( + currentEdge: PathEdge, + ) = 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> { + val startVertex = Vertex(entrypoint, startingFact) + return factsAtStmt.flatMapIndexed { index, facts -> + val stmt = stmts[index] + facts.map { + val endVertex = Vertex(stmt, it) + Edge(startVertex, endVertex) + } + } + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index 8220e17bd5..48b3de46c5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -30,8 +30,7 @@ import org.usvm.dataflow.ifds.Manager import org.usvm.dataflow.ifds.QueueEmptinessChanged import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.graph.reversed -import org.usvm.dataflow.ts.ifds.EtsBackwardIfdsRunner -import org.usvm.dataflow.ts.ifds.EtsForwardIfdsRunner +import org.usvm.dataflow.ts.ifds.EtsIfdsRunner import org.usvm.dataflow.ts.infer.EtsTypeFact.Companion.allStringProperties import org.usvm.dataflow.ts.util.EtsTraits import org.usvm.dataflow.ts.util.getRealLocals @@ -102,8 +101,8 @@ class TypeInferenceManager( createResultsFromSummaries(updatedTypeScheme, doInferAllLocals) } - lateinit var backwardRunner: EtsBackwardIfdsRunner - lateinit var forwardRunner: EtsForwardIfdsRunner + lateinit var backwardRunner: EtsIfdsRunner + lateinit var forwardRunner: EtsIfdsRunner private suspend fun collectSummaries( startMethods: List, @@ -114,7 +113,7 @@ class TypeInferenceManager( val backwardGraph = graph.reversed val backwardAnalyzer = BackwardAnalyzer(backwardGraph, savedTypes, ::methodDominators, doAddKnownTypes) - val backwardRunner = EtsBackwardIfdsRunner( + val backwardRunner = EtsIfdsRunner( graph = backwardGraph, analyzer = backwardAnalyzer, traits = traits, @@ -199,7 +198,7 @@ class TypeInferenceManager( doLiveVariablesAnalysis = true, ) - val forwardRunner = EtsForwardIfdsRunner( + val forwardRunner = EtsIfdsRunner( graph = forwardGraph, analyzer = forwardAnalyzer, traits = traits, From cd039b3b078fccc14e4ee2aa865c42757c3ee54d Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 20 May 2025 11:24:11 +0300 Subject: [PATCH 18/18] use default value in boolean array --- .../kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt index edc1d7c9ef..8a1a44b5c2 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt @@ -60,7 +60,7 @@ internal class EtsIfdsMethodRunner( internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1)) internal val stmts = listOf(mockStmt) + method.cfg.stmts - internal val isExit = BooleanArray(stmts.size) { false }.apply { + internal val isExit = BooleanArray(stmts.size).apply { for (exit in graph.exitPoints(method)) { set(exit.index, true) }