Skip to content

Commit 18f6a33

Browse files
MForest7MForest7
committed
update liveness analysis
1 parent eff0211 commit 18f6a33

File tree

1 file changed

+46
-101
lines changed

1 file changed

+46
-101
lines changed

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

Lines changed: 46 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ import org.jacodb.ets.base.EtsThrowStmt
2020
import org.jacodb.ets.base.EtsUnaryExpr
2121
import org.jacodb.ets.base.EtsValue
2222
import org.jacodb.ets.model.EtsMethod
23+
import java.util.BitSet
2324

2425
interface LiveVariables {
2526
fun isAliveAt(local: String, stmt: EtsStmt): Boolean
@@ -64,127 +65,71 @@ class LiveVariablesImpl(
6465
is EtsInstanceCallExpr -> listOf(instance.name) + args.flatMap { it.used() }
6566
else -> args.flatMap { it.used() }
6667
}
67-
68-
private fun <T> postOrder(sources: Iterable<T>, successors: (T) -> Iterable<T>): List<T> {
69-
val order = mutableListOf<T>()
70-
val visited = hashSetOf<T>()
71-
72-
fun dfs(node: T) {
73-
visited.add(node)
74-
for (next in successors(node)) {
75-
if (next !in visited)
76-
dfs(next)
77-
}
78-
order.add(node)
79-
}
80-
81-
for (source in sources) {
82-
if (source !in visited)
83-
dfs(source)
84-
}
85-
86-
return order
87-
}
88-
}
89-
90-
private fun stronglyConnectedComponents(): IntArray {
91-
val rpo = postOrder(method.cfg.entries) {
92-
method.cfg.successors(it)
93-
}.reversed()
94-
95-
val coloring = IntArray(method.cfg.stmts.size) { -1 }
96-
var nextColor = 0
97-
fun backwardDfs(stmt: EtsStmt) {
98-
coloring[stmt.location.index] = nextColor
99-
if (stmt in method.cfg.entries)
100-
return
101-
for (next in method.cfg.predecessors(stmt)) {
102-
if (coloring[next.location.index] == -1) {
103-
backwardDfs(next)
104-
}
105-
}
106-
}
107-
108-
for (stmt in rpo) {
109-
if (coloring[stmt.location.index] == -1) {
110-
backwardDfs(stmt)
111-
nextColor++
112-
}
113-
}
114-
115-
return coloring
11668
}
11769

118-
private fun condensation(coloring: IntArray): Map<Int, Set<Int>> {
119-
val successors = hashMapOf<Int, HashSet<Int>>()
120-
for (from in method.cfg.stmts) {
121-
for (to in method.cfg.successors(from)) {
122-
val fromColor = coloring[from.location.index]
123-
val toColor = coloring[to.location.index]
124-
if (fromColor != toColor) {
125-
successors.computeIfAbsent(fromColor) { hashSetOf() }
126-
.add(toColor)
127-
}
128-
}
129-
}
130-
return successors
131-
}
70+
private val aliveAtStmt: Array<BitSet>
71+
private val indexOfName = hashMapOf<String, Int>()
72+
private val definedAtStmt = IntArray(method.cfg.stmts.size) { -1 }
13273

133-
private val lifetime = hashMapOf<String, Pair<Int, Int>>()
134-
private val coloring = stronglyConnectedComponents()
135-
private val colorIndex: IntArray
74+
private fun emptyBitSet() = BitSet(indexOfName.size)
75+
private fun BitSet.copy() = clone() as BitSet
13676

13777
init {
138-
val condensationSuccessors = condensation(coloring)
139-
val entriesColors = method.cfg.entries.map {
140-
coloring[it.location.index]
141-
}
142-
val colorOrder = postOrder(entriesColors) {
143-
condensationSuccessors[it].orEmpty()
144-
}.reversed()
145-
146-
colorIndex = IntArray(colorOrder.size) { -1 }
147-
for ((index, color) in colorOrder.withIndex()) {
148-
colorIndex[color] = index
149-
}
150-
151-
val ownLocals = hashSetOf<String>()
15278
for (stmt in method.cfg.stmts) {
15379
if (stmt is EtsAssignStmt) {
15480
when (val lhv = stmt.lhv) {
155-
is EtsLocal -> ownLocals.add(lhv.name)
81+
is EtsLocal -> {
82+
val lhvIndex = indexOfName.size
83+
definedAtStmt[stmt.location.index] = lhvIndex
84+
indexOfName[lhv.name] = lhvIndex
85+
}
15686
}
15787
}
15888
}
15989

160-
for (stmt in method.cfg.stmts) {
161-
val usedLocals = when (stmt) {
162-
is EtsAssignStmt -> stmt.lhv.used() + stmt.rhv.used()
163-
is EtsCallStmt -> stmt.expr.used()
164-
is EtsReturnStmt -> stmt.returnValue?.used().orEmpty()
165-
is EtsIfStmt -> stmt.condition.used()
166-
is EtsSwitchStmt -> stmt.arg.used()
167-
is EtsThrowStmt -> stmt.arg.used()
168-
else -> emptyList()
90+
aliveAtStmt = Array(method.cfg.stmts.size) { emptyBitSet() }
91+
92+
val queue = method.cfg.stmts.toHashSet()
93+
while (queue.isNotEmpty()) {
94+
val stmt = queue.first()
95+
queue.remove(stmt)
96+
97+
val aliveHere = emptyBitSet().apply {
98+
val usedLocals = when (stmt) {
99+
is EtsAssignStmt -> stmt.lhv.used() + stmt.rhv.used()
100+
is EtsCallStmt -> stmt.expr.used()
101+
is EtsReturnStmt -> stmt.returnValue?.used().orEmpty()
102+
is EtsIfStmt -> stmt.condition.used()
103+
is EtsSwitchStmt -> stmt.arg.used()
104+
is EtsThrowStmt -> stmt.arg.used()
105+
else -> emptyList()
106+
}
107+
108+
usedLocals.mapNotNull { indexOfName[it] }.forEach { set(it) }
169109
}
170-
val blockIndex = colorIndex[coloring[stmt.location.index]]
171110

172-
for (local in usedLocals) {
173-
if (local in ownLocals) {
174-
lifetime.merge(local, blockIndex to blockIndex) { (begin, end), (bb, be) ->
175-
minOf(begin, bb) to maxOf(end, be)
176-
}
177-
} else {
178-
lifetime[local] = Int.MIN_VALUE to Int.MAX_VALUE
111+
for (succ in method.cfg.successors(stmt)) {
112+
val transferFromSucc = aliveAtStmt[succ.location.index].copy()
113+
val definedAtSucc = definedAtStmt[succ.location.index]
114+
if (definedAtSucc != -1) {
115+
transferFromSucc.clear(definedAtSucc)
116+
}
117+
118+
aliveHere.or(transferFromSucc)
119+
}
120+
121+
if (aliveHere != aliveAtStmt[stmt.location.index]) {
122+
aliveAtStmt[stmt.location.index] = aliveHere
123+
if (stmt !in method.cfg.entries) {
124+
queue.addAll(method.cfg.predecessors(stmt))
179125
}
180126
}
181127
}
182128
}
183129

184130
override fun isAliveAt(local: String, stmt: EtsStmt): Boolean {
185131
if (stmt.location.index < 0) return true
186-
val block = colorIndex[coloring[stmt.location.index]]
187-
val (begin, end) = lifetime[local] ?: error("Unknown local")
188-
return block in begin..end
132+
val index = indexOfName[local] ?: return true
133+
return aliveAtStmt[stmt.location.index].get(index)
189134
}
190135
}

0 commit comments

Comments
 (0)