Skip to content

Commit b9aa62b

Browse files
MForest7LipenCaelmBleidd
authored
Add ifds runner for ets (#276)
--------- Co-authored-by: Konstantin Chukharev <lipen00@gmail.com> Co-authored-by: Alexey Menshutin <alex.menshutin99@gmail.com>
1 parent 96aa98e commit b9aa62b

11 files changed

Lines changed: 453 additions & 100 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ jobs:
127127
DEST_DIR="arkanalyzer"
128128
MAX_RETRIES=10
129129
RETRY_DELAY=3 # Delay between retries in seconds
130-
BRANCH="neo/2025-04-14"
130+
BRANCH="neo/2025-05-12"
131131
132132
for ((i=1; i<=MAX_RETRIES; i++)); do
133133
git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

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

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
package org.usvm.dataflow.ts.ifds
2+
3+
import org.jacodb.ets.model.EtsMethod
4+
import org.jacodb.ets.model.EtsNopStmt
5+
import org.jacodb.ets.model.EtsStmt
6+
import org.jacodb.ets.model.EtsStmtLocation
7+
import org.usvm.dataflow.ifds.Analyzer
8+
import org.usvm.dataflow.ifds.Edge
9+
import org.usvm.dataflow.ifds.Vertex
10+
import org.usvm.dataflow.ts.graph.EtsApplicationGraph
11+
import org.usvm.dataflow.ts.infer.AnalyzerEvent
12+
import org.usvm.dataflow.ts.infer.TypeInferenceManager
13+
import org.usvm.dataflow.ts.util.EtsTraits
14+
15+
internal class EtsIfdsMethodRunner<Fact, Event : AnalyzerEvent>(
16+
val graph: EtsApplicationGraph,
17+
val method: EtsMethod,
18+
val analyzer: Analyzer<Fact, Event, EtsMethod, EtsStmt>,
19+
val traits: EtsTraits,
20+
val manager: TypeInferenceManager,
21+
val commonRunner: EtsIfdsRunner<Fact, Event>,
22+
) {
23+
internal val flowSpace = analyzer.flowFunctions
24+
private var enqueued: Boolean = false
25+
private val sourceRunnersQueue: ArrayDeque<EtsIfdsSourceRunner<Fact>> = ArrayDeque()
26+
27+
internal fun enqueue(runner: EtsIfdsSourceRunner<Fact>) {
28+
sourceRunnersQueue.addLast(runner)
29+
if (!enqueued) {
30+
commonRunner.methodRunnersQueue.addLast(this)
31+
enqueued = true
32+
}
33+
}
34+
35+
fun processFacts() {
36+
while (!sourceRunnersQueue.isEmpty()) {
37+
val currentSourceRunner = sourceRunnersQueue.removeFirst()
38+
currentSourceRunner.processFacts()
39+
}
40+
enqueued = false
41+
}
42+
43+
internal val sourceRunners = hashMapOf<Fact, HashMap<EtsStmt, EtsIfdsSourceRunner<Fact>>>()
44+
internal fun getSourceRunner(vertex: Vertex<Fact, EtsStmt>): EtsIfdsSourceRunner<Fact> {
45+
return sourceRunners
46+
.getOrPut(vertex.fact) { hashMapOf() }
47+
.getOrPut(vertex.statement) {
48+
EtsIfdsSourceRunner(traits, this, vertex.statement, vertex.fact)
49+
}
50+
}
51+
52+
internal fun getSourceRunners(fact: Fact): Collection<EtsIfdsSourceRunner<Fact>> {
53+
return sourceRunners.getOrPut(fact) {
54+
entrypoints.associateWithTo(hashMapOf()) {
55+
EtsIfdsSourceRunner(traits, this, it, fact)
56+
}
57+
}.values
58+
}
59+
60+
internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1))
61+
internal val stmts = listOf(mockStmt) + method.cfg.stmts
62+
63+
internal val isExit = BooleanArray(stmts.size).apply {
64+
for (exit in graph.exitPoints(method)) {
65+
set(exit.index, true)
66+
}
67+
}
68+
69+
internal val EtsStmt.index: Int
70+
get() = location.index + 1
71+
72+
internal val successors = stmts.map { graph.successors(it).map { s -> s.index } }
73+
internal val entrypoints = graph.entryPoints(method).toList()
74+
75+
fun addStart() {
76+
val startFacts = flowSpace.obtainPossibleStartFacts(method)
77+
for (startFact in startFacts) {
78+
propagateStartingFact(startFact)
79+
}
80+
}
81+
82+
internal data class PathEdge<Fact>(
83+
val endStmtIndex: Int,
84+
val fact: Fact,
85+
)
86+
87+
internal fun propagateStartingFact(fact: Fact): Set<Vertex<Fact, EtsStmt>> {
88+
val summaryEdges = hashSetOf<Vertex<Fact, EtsStmt>>()
89+
for (entrypoint in entrypoints) {
90+
val runner = getSourceRunner(Vertex(entrypoint, fact))
91+
runner.propagate(PathEdge(entrypoint.index, fact))
92+
summaryEdges += runner.summaryEdges
93+
}
94+
return summaryEdges
95+
}
96+
97+
internal fun handleSummaryEdgeInCaller(
98+
currentEdge: Edge<Fact, EtsStmt>,
99+
summaryEdge: Edge<Fact, EtsStmt>,
100+
) {
101+
val (startVertex, currentVertex) = currentEdge
102+
val sourceRunner = getSourceRunner(startVertex)
103+
val caller = currentVertex.statement
104+
for (returnSite in graph.successors(caller)) {
105+
val (exit, exitFact) = summaryEdge.to
106+
val finalFacts = flowSpace
107+
.obtainExitToReturnSiteFlowFunction(caller, returnSite, exit)
108+
.compute(exitFact)
109+
for (returnSiteFact in finalFacts) {
110+
val newEdge = PathEdge(caller.index, returnSiteFact)
111+
sourceRunner.propagate(newEdge)
112+
}
113+
}
114+
}
115+
116+
override fun toString(): String {
117+
return "Runner for ${method.signature}"
118+
}
119+
}

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

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
package org.usvm.dataflow.ts.ifds
2+
3+
import kotlinx.coroutines.coroutineScope
4+
import kotlinx.coroutines.isActive
5+
import org.jacodb.ets.model.EtsMethod
6+
import org.jacodb.ets.model.EtsStmt
7+
import org.usvm.dataflow.ifds.Analyzer
8+
import org.usvm.dataflow.ifds.Edge
9+
import org.usvm.dataflow.ifds.IfdsResult
10+
import org.usvm.dataflow.ifds.QueueEmptinessChanged
11+
import org.usvm.dataflow.ifds.Reason
12+
import org.usvm.dataflow.ifds.Runner
13+
import org.usvm.dataflow.ifds.SingletonUnit
14+
import org.usvm.dataflow.ifds.UnitType
15+
import org.usvm.dataflow.ts.graph.EtsApplicationGraph
16+
import org.usvm.dataflow.ts.infer.AnalyzerEvent
17+
import org.usvm.dataflow.ts.infer.TypeInferenceManager
18+
import org.usvm.dataflow.ts.util.EtsTraits
19+
20+
class EtsIfdsRunner<Fact, Event : AnalyzerEvent>(
21+
override val graph: EtsApplicationGraph,
22+
val analyzer: Analyzer<Fact, Event, EtsMethod, EtsStmt>,
23+
val traits: EtsTraits,
24+
val manager: TypeInferenceManager,
25+
private val zeroFact: Fact,
26+
) : Runner<Fact, EtsMethod, EtsStmt> {
27+
internal val methodRunnersQueue: ArrayDeque<EtsIfdsMethodRunner<Fact, Event>> = ArrayDeque()
28+
private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true)
29+
30+
private val methodRunners = hashMapOf<EtsMethod, EtsIfdsMethodRunner<Fact, Event>>()
31+
32+
internal fun getMethodRunner(method: EtsMethod): EtsIfdsMethodRunner<Fact, Event> {
33+
return methodRunners.getOrPut(method) {
34+
EtsIfdsMethodRunner(
35+
graph = graph,
36+
method = method,
37+
analyzer = analyzer,
38+
traits = traits,
39+
manager = manager,
40+
commonRunner = this@EtsIfdsRunner,
41+
)
42+
}
43+
}
44+
45+
override suspend fun run(startMethods: List<EtsMethod>) {
46+
for (method in startMethods) {
47+
getMethodRunner(method).addStart()
48+
}
49+
50+
tabulationAlgorithm()
51+
}
52+
53+
private suspend fun tabulationAlgorithm() = coroutineScope {
54+
while (isActive) {
55+
val current = methodRunnersQueue.removeFirstOrNull() ?: run {
56+
manager.handleControlEvent(queueIsEmpty)
57+
return@coroutineScope
58+
}
59+
current.processFacts()
60+
}
61+
}
62+
63+
override val unit: UnitType
64+
get() = SingletonUnit
65+
66+
override fun getIfdsResult(): IfdsResult<Fact, EtsStmt> {
67+
val sourceRunners = methodRunners.values.flatMap { methodRunner ->
68+
methodRunner.sourceRunners.values.flatMap { it.values }
69+
}
70+
val pathEdges = sourceRunners.flatMap { it.getPathEdges() }
71+
72+
val resultFacts: MutableMap<EtsStmt, MutableSet<Fact>> = hashMapOf()
73+
for (edge in pathEdges) {
74+
resultFacts.getOrPut(edge.to.statement) { hashSetOf() }.add(edge.to.fact)
75+
}
76+
77+
return IfdsResult(pathEdges, resultFacts, reasons = emptyMap(), zeroFact)
78+
}
79+
80+
override fun submitNewEdge(edge: Edge<Fact, EtsStmt>, reason: Reason<Fact, EtsStmt>) {
81+
val (startVertex, endVertex) = edge
82+
val (endStmt, endFact) = endVertex
83+
84+
val localPathEdge = EtsIfdsMethodRunner.PathEdge(endStmt.location.index, endFact)
85+
getMethodRunner(startVertex.statement.method).getSourceRunner(startVertex).propagate(localPathEdge)
86+
}
87+
}

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

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
package org.usvm.dataflow.ts.ifds
2+
3+
import org.jacodb.ets.model.EtsStmt
4+
import org.usvm.dataflow.ifds.Edge
5+
import org.usvm.dataflow.ifds.Vertex
6+
import org.usvm.dataflow.ts.ifds.EtsIfdsMethodRunner.PathEdge
7+
import org.usvm.dataflow.ts.util.EtsTraits
8+
9+
internal class EtsIfdsSourceRunner<Fact>(
10+
val traits: EtsTraits,
11+
val methodRunner: EtsIfdsMethodRunner<Fact, *>,
12+
val entrypoint: EtsStmt,
13+
val startingFact: Fact,
14+
) {
15+
private var enqueued: Boolean = false
16+
private val pathEdgeQueue: ArrayDeque<PathEdge<Fact>> = ArrayDeque()
17+
18+
fun processFacts() {
19+
while (!pathEdgeQueue.isEmpty()) {
20+
val currentEdge = pathEdgeQueue.removeFirst()
21+
tabulationAlgorithmStep(currentEdge)
22+
}
23+
enqueued = false
24+
}
25+
26+
private val successors = methodRunner.successors
27+
private val stmts = methodRunner.stmts
28+
private val mockStmt = methodRunner.mockStmt
29+
private val flowSpace = methodRunner.flowSpace
30+
val graph = methodRunner.graph
31+
32+
private val factsAtStmt = Array(stmts.size) { hashSetOf<Fact>() }
33+
34+
internal fun propagate(localEdge: PathEdge<Fact>) {
35+
val (endStmtIndex, endFact) = localEdge
36+
if (factsAtStmt[endStmtIndex].add(endFact)) {
37+
val startVertex = Vertex(mockStmt, startingFact)
38+
val endVertex = Vertex(stmts[endStmtIndex], endFact)
39+
val edge = Edge(startVertex, endVertex)
40+
val events = methodRunner.analyzer.handleNewEdge(edge)
41+
42+
for (event in events) {
43+
methodRunner.manager.handleEvent(event)
44+
}
45+
46+
pathEdgeQueue.add(localEdge)
47+
if (!enqueued) {
48+
enqueued = true
49+
methodRunner.enqueue(this)
50+
}
51+
}
52+
}
53+
54+
private val callerPathEdges = hashSetOf<Edge<Fact, EtsStmt>>()
55+
internal val summaryEdges = hashSetOf<Vertex<Fact, EtsStmt>>()
56+
57+
private fun tabulationAlgorithmStep(
58+
currentEdge: PathEdge<Fact>,
59+
) = with(traits) {
60+
val (currentStmtIndex, currentFact) = currentEdge
61+
val currentStmt = stmts[currentStmtIndex]
62+
63+
val currentIsCall = getCallExpr(currentStmt) != null
64+
val currentIsExit = methodRunner.isExit[currentStmtIndex]
65+
66+
if (currentIsCall) {
67+
val callToReturnFlowFunction = flowSpace
68+
.obtainCallToReturnSiteFlowFunction(currentStmt, mockStmt)
69+
70+
// Propagate through the call-to-return-site edge:
71+
val factsAtReturnSite = callToReturnFlowFunction.compute(currentFact)
72+
for (returnSite in successors[currentStmtIndex]) {
73+
for (returnSiteFact in factsAtReturnSite) {
74+
val edge = PathEdge(returnSite, returnSiteFact)
75+
propagate(edge)
76+
}
77+
}
78+
79+
for (callee in graph.callees(currentStmt)) {
80+
for (calleeStart in graph.entryPoints(callee)) {
81+
val callToStartFlowFunction = flowSpace.obtainCallToStartFlowFunction(currentStmt, calleeStart)
82+
val factsAtCalleeStart = callToStartFlowFunction.compute(currentFact)
83+
84+
for (calleeStartFact in factsAtCalleeStart) {
85+
val calleeStartVertex = Vertex(calleeStart, calleeStartFact)
86+
87+
// Save info about the call for summary edges that will be found later:
88+
val calleeRunner = methodRunner.commonRunner.getMethodRunner(callee)
89+
val currentVertex = Vertex(currentStmt, currentFact)
90+
val startingVertex = Vertex(entrypoint, startingFact)
91+
val callerEdge = Edge(startingVertex, currentVertex)
92+
for (calleeSourceRunner in calleeRunner.getSourceRunners(startingFact)) {
93+
calleeSourceRunner.callerPathEdges.add(callerEdge)
94+
}
95+
96+
// Initialize analysis of callee:
97+
val summaryEdges = calleeRunner.propagateStartingFact(calleeStartFact)
98+
99+
// Handle already-found summary edges:
100+
for (exitVertex in summaryEdges) {
101+
val summaryEdge = Edge(calleeStartVertex, exitVertex)
102+
methodRunner.handleSummaryEdgeInCaller(callerEdge, summaryEdge)
103+
}
104+
}
105+
}
106+
}
107+
} else {
108+
if (currentIsExit) {
109+
val startVertex = Vertex(entrypoint, startingFact)
110+
val currentVertex = Vertex(currentStmt, currentFact)
111+
112+
// Propagate through the summary edge:
113+
for (callerPathEdge in callerPathEdges) {
114+
val summaryEdge = Edge(startVertex, currentVertex)
115+
val caller = callerPathEdge.from.statement.method
116+
val callerRunner = methodRunner.commonRunner.getMethodRunner(caller)
117+
callerRunner.handleSummaryEdgeInCaller(currentEdge = callerPathEdge, summaryEdge = summaryEdge)
118+
}
119+
120+
// Add new summary edge:
121+
summaryEdges.add(currentVertex)
122+
}
123+
124+
// Simple (sequential) propagation to the next instruction:
125+
val factsAtNext = flowSpace
126+
.obtainSequentFlowFunction(currentStmt, mockStmt)
127+
.compute(currentFact)
128+
for (next in successors[currentStmtIndex]) {
129+
for (nextFact in factsAtNext) {
130+
val edge = PathEdge(next, nextFact)
131+
propagate(edge)
132+
}
133+
}
134+
}
135+
}
136+
137+
internal fun getPathEdges(): List<Edge<Fact, EtsStmt>> {
138+
val startVertex = Vertex(entrypoint, startingFact)
139+
return factsAtStmt.flatMapIndexed { index, facts ->
140+
val stmt = stmts[index]
141+
facts.map {
142+
val endVertex = Vertex(stmt, it)
143+
Edge(startVertex, endVertex)
144+
}
145+
}
146+
}
147+
}

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

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -34,17 +34,13 @@ class ForwardAnalyzer(
3434
error("No cross unit calls")
3535
}
3636

37-
private val liveVariablesCache = hashMapOf<EtsMethod, LiveVariables>()
38-
private fun liveVariables(method: EtsMethod): LiveVariables =
39-
liveVariablesCache.computeIfAbsent(method) {
40-
if (doLiveVariablesAnalysis) LiveVariables.from(method) else AlwaysAlive
41-
}
42-
4337
private fun variableIsDying(fact: ForwardTypeDomainFact, stmt: EtsStmt): Boolean {
4438
if (fact !is ForwardTypeDomainFact.TypedVariable) return false
45-
val base = fact.variable.base
46-
if (base !is AccessPathBase.Local) return false
47-
return !liveVariables(stmt.method).isAliveAt(base.name, stmt)
39+
return when (val base = fact.variable.base) {
40+
is AccessPathBase.Local -> !flowFunctions.liveVariables(stmt.method).isAliveAt(base.name, stmt)
41+
is AccessPathBase.Arg -> !flowFunctions.liveVariables(stmt.method).isAliveAt("arg(${base.index})", stmt)
42+
else -> false
43+
}
4844
}
4945

5046
override fun handleNewEdge(edge: Edge<ForwardTypeDomainFact, EtsStmt>): List<AnalyzerEvent> {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ class ForwardFlowFunctions(
6666
}
6767

6868
private val liveVariablesCache = hashMapOf<EtsMethod, LiveVariables>()
69-
private fun liveVariables(method: EtsMethod) =
69+
internal fun liveVariables(method: EtsMethod) =
7070
liveVariablesCache.computeIfAbsent(method) {
7171
if (doLiveVariablesAnalysis) {
7272
LiveVariables.from(method)

0 commit comments

Comments
 (0)