|
| 1 | +package org.usvm.dataflow.ts.infer |
| 2 | + |
| 3 | +import kotlinx.collections.immutable.PersistentSet |
| 4 | +import kotlinx.collections.immutable.PersistentMap |
| 5 | +import kotlinx.collections.immutable.mutate |
| 6 | +import kotlinx.collections.immutable.persistentHashMapOf |
| 7 | +import kotlinx.collections.immutable.persistentSetOf |
| 8 | +import org.jacodb.ets.base.EtsArrayAccess |
| 9 | +import org.jacodb.ets.base.EtsAssignStmt |
| 10 | +import org.jacodb.ets.base.EtsBinaryExpr |
| 11 | +import org.jacodb.ets.base.EtsCallExpr |
| 12 | +import org.jacodb.ets.base.EtsCallStmt |
| 13 | +import org.jacodb.ets.base.EtsCastExpr |
| 14 | +import org.jacodb.ets.base.EtsEntity |
| 15 | +import org.jacodb.ets.base.EtsIfStmt |
| 16 | +import org.jacodb.ets.base.EtsInstanceCallExpr |
| 17 | +import org.jacodb.ets.base.EtsInstanceFieldRef |
| 18 | +import org.jacodb.ets.base.EtsInstanceOfExpr |
| 19 | +import org.jacodb.ets.base.EtsLocal |
| 20 | +import org.jacodb.ets.base.EtsReturnStmt |
| 21 | +import org.jacodb.ets.base.EtsStmt |
| 22 | +import org.jacodb.ets.base.EtsSwitchStmt |
| 23 | +import org.jacodb.ets.base.EtsTernaryExpr |
| 24 | +import org.jacodb.ets.base.EtsThrowStmt |
| 25 | +import org.jacodb.ets.base.EtsUnaryExpr |
| 26 | +import org.jacodb.ets.base.EtsValue |
| 27 | +import org.jacodb.ets.model.EtsMethod |
| 28 | + |
| 29 | +interface DefUseChains<Fact, Stmt> { |
| 30 | + fun nextUses(fact: Fact, from: Stmt): Set<Stmt> |
| 31 | +} |
| 32 | + |
| 33 | +class EtsDefUseChains( |
| 34 | + val method: EtsMethod, |
| 35 | +) : DefUseChains<ForwardTypeDomainFact, EtsStmt> { |
| 36 | + private companion object { |
| 37 | + fun EtsEntity.usedLocals(): List<String> = when (this) { |
| 38 | + is EtsValue -> this.usedLocals() |
| 39 | + is EtsUnaryExpr -> arg.usedLocals() |
| 40 | + is EtsBinaryExpr -> left.usedLocals() + right.usedLocals() |
| 41 | + is EtsCallExpr -> this.usedLocals() |
| 42 | + is EtsCastExpr -> arg.usedLocals() |
| 43 | + is EtsInstanceOfExpr -> arg.usedLocals() |
| 44 | + is EtsTernaryExpr -> condition.usedLocals() + thenExpr.usedLocals() + elseExpr.usedLocals() |
| 45 | + else -> emptyList() |
| 46 | + } |
| 47 | + |
| 48 | + fun EtsValue.usedLocals(): List<String> = when (this) { |
| 49 | + is EtsLocal -> listOf(name) |
| 50 | + is EtsInstanceFieldRef -> listOf(instance.name) |
| 51 | + is EtsArrayAccess -> array.usedLocals() + index.usedLocals() |
| 52 | + else -> emptyList() |
| 53 | + } |
| 54 | + |
| 55 | + fun EtsCallExpr.usedLocals(): List<String> = when (this) { |
| 56 | + is EtsInstanceCallExpr -> listOf(instance.name) + args.flatMap { it.usedLocals() } |
| 57 | + else -> args.flatMap { it.usedLocals() } |
| 58 | + } |
| 59 | + |
| 60 | + fun EtsStmt.usedLocals(): List<String> = when (this) { |
| 61 | + is EtsAssignStmt -> lhv.usedLocals() + rhv.usedLocals() |
| 62 | + is EtsCallStmt -> expr.usedLocals() |
| 63 | + is EtsReturnStmt -> returnValue?.usedLocals().orEmpty() |
| 64 | + is EtsIfStmt -> condition.usedLocals() |
| 65 | + is EtsSwitchStmt -> arg.usedLocals() |
| 66 | + is EtsThrowStmt -> arg.usedLocals() |
| 67 | + else -> emptyList() |
| 68 | + } |
| 69 | + |
| 70 | + fun EtsStmt.definedLocal(): String? = |
| 71 | + if (this is EtsAssignStmt && lhv is EtsLocal) (lhv as EtsLocal).name else null |
| 72 | + |
| 73 | + fun EtsEntity.usedThisFields(): List<String> = when (this) { |
| 74 | + is EtsValue -> this.usedThisFields() |
| 75 | + is EtsUnaryExpr -> arg.usedThisFields() |
| 76 | + is EtsBinaryExpr -> left.usedThisFields() + right.usedThisFields() |
| 77 | + is EtsCallExpr -> this.usedThisFields() |
| 78 | + is EtsCastExpr -> arg.usedThisFields() |
| 79 | + is EtsInstanceOfExpr -> arg.usedThisFields() |
| 80 | + is EtsTernaryExpr -> condition.usedThisFields() + thenExpr.usedThisFields() + elseExpr.usedThisFields() |
| 81 | + else -> emptyList() |
| 82 | + } |
| 83 | + |
| 84 | + fun EtsValue.usedThisFields(): List<String> = when (this) { |
| 85 | + is EtsLocal -> emptyList() |
| 86 | + is EtsInstanceFieldRef -> if (instance.name == "this") listOf(field.name) else emptyList() |
| 87 | + is EtsArrayAccess -> array.usedThisFields() + index.usedThisFields() |
| 88 | + else -> emptyList() |
| 89 | + } |
| 90 | + |
| 91 | + fun EtsCallExpr.usedThisFields(): List<String> = when (this) { |
| 92 | + is EtsInstanceCallExpr -> args.flatMap { it.usedThisFields() } |
| 93 | + else -> args.flatMap { it.usedThisFields() } |
| 94 | + } |
| 95 | + |
| 96 | + fun EtsStmt.usedThisFields(): List<String> = when (this) { |
| 97 | + is EtsAssignStmt -> lhv.usedThisFields() + rhv.usedThisFields() |
| 98 | + is EtsCallStmt -> expr.usedThisFields() |
| 99 | + is EtsReturnStmt -> returnValue?.usedThisFields().orEmpty() |
| 100 | + is EtsIfStmt -> condition.usedThisFields() |
| 101 | + is EtsSwitchStmt -> arg.usedThisFields() |
| 102 | + is EtsThrowStmt -> arg.usedThisFields() |
| 103 | + else -> emptyList() |
| 104 | + } |
| 105 | + |
| 106 | + fun EtsStmt.definedThisField(): String? = |
| 107 | + if (this is EtsAssignStmt && lhv is EtsInstanceFieldRef && (lhv as EtsInstanceFieldRef).instance.name == "this") |
| 108 | + (lhv as EtsInstanceFieldRef).field.name else null |
| 109 | + |
| 110 | + fun EtsStmt.defined(): String? = definedLocal() ?: definedThisField()?.let { "this.$it" } |
| 111 | + |
| 112 | + fun EtsStmt.used(): List<String> = usedLocals() + usedThisFields().map { "this.$it" } |
| 113 | + } |
| 114 | + |
| 115 | + private val nextUse = |
| 116 | + Array<PersistentMap<String, PersistentSet<Int>>>(method.cfg.stmts.size) { persistentHashMapOf() } |
| 117 | + |
| 118 | + private val usedFields = method.cfg.stmts.flatMapTo(hashSetOf()) { it.usedThisFields() } |
| 119 | + |
| 120 | + init { |
| 121 | + val queue = method.cfg.stmts.toHashSet() |
| 122 | + while (queue.isNotEmpty()) { |
| 123 | + val stmt = queue.first() |
| 124 | + queue.remove(stmt) |
| 125 | + |
| 126 | + val useArcs = method.cfg.successors(stmt).fold(persistentHashMapOf<String, PersistentSet<Int>>()) { acc, succ -> |
| 127 | + val succIndex = succ.location.index |
| 128 | + val succDefined = succ.defined() |
| 129 | + val succUsed = succ.used().toHashSet() |
| 130 | + acc.mutate { sum -> |
| 131 | + for ((name, arcs) in nextUse[succIndex]) { |
| 132 | + if (name == succDefined || name in succUsed) continue |
| 133 | + sum.merge(name, arcs) { a, b -> a.addAll(b) } |
| 134 | + } |
| 135 | + for (name in succUsed) { |
| 136 | + if (name == succDefined) continue |
| 137 | + sum.compute(name) { _, prev -> (prev ?: persistentSetOf()).add(succIndex) } |
| 138 | + } |
| 139 | + } |
| 140 | + } |
| 141 | + |
| 142 | + val stmtIndex = stmt.location.index |
| 143 | + if (useArcs != nextUse[stmtIndex]) { |
| 144 | + nextUse[stmtIndex] = useArcs |
| 145 | + if (stmt !in method.cfg.entries) queue.addAll(method.cfg.predecessors(stmt)) |
| 146 | + } |
| 147 | + } |
| 148 | + } |
| 149 | + |
| 150 | + override fun nextUses(fact: ForwardTypeDomainFact, from: EtsStmt): Set<EtsStmt> { |
| 151 | + if (from.location.index < 0) return setOf(method.cfg.stmts.first()) |
| 152 | + val accessPath = (fact as? ForwardTypeDomainFact.TypedVariable ?: return method.cfg.successors(from)).variable |
| 153 | + |
| 154 | + when (val base = accessPath.base) { |
| 155 | + is AccessPathBase.Local -> { |
| 156 | + val name = base.name |
| 157 | + val nextStmts = nextUse[from.location.index][name] ?: return method.cfg.successors(from) |
| 158 | + return nextStmts.mapTo(hashSetOf()) { method.cfg.stmts[it] } |
| 159 | + } |
| 160 | + is AccessPathBase.This -> { |
| 161 | + val field = accessPath.accesses.firstOrNull() as? FieldAccessor |
| 162 | + ?: return method.cfg.successors(from) |
| 163 | + if (field.name !in usedFields) return emptySet() |
| 164 | + val nextStmts = nextUse[from.location.index]["this.$field"] ?: return method.cfg.successors(from) |
| 165 | + return nextStmts.mapTo(hashSetOf()) { method.cfg.stmts[it] } |
| 166 | + } |
| 167 | + else -> return method.cfg.successors(from) |
| 168 | + } |
| 169 | + } |
| 170 | +} |
0 commit comments