From eff02111505da69de6d8e213606fdc36b7393700 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Mon, 3 Mar 2025 15:26:12 +0300 Subject: [PATCH 01/21] add optional live variables analysis --- .../org/usvm/dataflow/ts/infer/Alias.kt | 143 +++++++------ .../usvm/dataflow/ts/infer/ForwardAnalyzer.kt | 28 ++- .../dataflow/ts/infer/ForwardFlowFunctions.kt | 66 +++++- .../usvm/dataflow/ts/infer/LiveVariables.kt | 190 ++++++++++++++++++ .../dataflow/ts/infer/TypeInferenceManager.kt | 20 +- .../org/usvm/dataflow/ts/util/EtsTraits.kt | 7 +- .../ts/test/EtsTypeResolverPerformanceTest.kt | 19 +- .../dataflow/ts/test/utils/AbcProjects.kt | 14 +- .../ts/test/utils/PerformanceReport.kt | 30 ++- 9 files changed, 403 insertions(+), 114 deletions(-) create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 8d011c6547..2ad79117d6 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -1,6 +1,5 @@ package org.usvm.dataflow.ts.infer -import mu.KotlinLogging import org.jacodb.ets.base.EtsArrayAccess import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsBinaryExpr @@ -22,22 +21,29 @@ import org.jacodb.ets.base.EtsThis import org.jacodb.ets.base.EtsUnaryExpr import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod +import kotlin.collections.ArrayDeque -private val logger = KotlinLogging.logger {} +interface StmtAliasInfo { + fun getAliases(path: AccessPath): Set +} + +interface MethodAliasInfo { + fun computeAliases(): List +} @OptIn(ExperimentalUnsignedTypes::class) -class StmtAliasInfo( +class StmtAliasInfoImpl( val baseToAlloc: IntArray, val allocToFields: Array, - val method: MethodAliasInfo, -) { - companion object { - const val NOT_PROCESSED = -1 - const val MULTIPLE_EDGE = -2 + val method: MethodAliasInfoImpl, +) : StmtAliasInfo { + internal companion object { + internal const val NOT_PROCESSED = -1 + internal const val MULTIPLE_EDGE = -2 - const val ELEMENT_ACCESSOR = -3 + internal const val ELEMENT_ACCESSOR = -3 - fun merge(first: Int, second: Int): Int = when { + internal fun merge(first: Int, second: Int): Int = when { first == NOT_PROCESSED -> second second == NOT_PROCESSED -> first first == MULTIPLE_EDGE -> MULTIPLE_EDGE @@ -46,19 +52,19 @@ class StmtAliasInfo( else -> MULTIPLE_EDGE } - fun wrap(string: Int, alloc: Int): ULong { + internal fun wrap(string: Int, alloc: Int): ULong { return (string.toULong() shl Int.SIZE_BITS) or alloc.toULong() } - fun unwrap(edge: ULong): Pair { + internal fun unwrap(edge: ULong): Pair { val string = (edge shr Int.SIZE_BITS).toInt() val allocation = (edge and UInt.MAX_VALUE.toULong()).toInt() return Pair(string, allocation) } } - fun merge(other: StmtAliasInfo): StmtAliasInfo { - val merged = StmtAliasInfo( + internal fun merge(other: StmtAliasInfoImpl): StmtAliasInfoImpl { + val merged = StmtAliasInfoImpl( baseToAlloc = IntArray(method.bases.size) { NOT_PROCESSED }, allocToFields = Array(method.allocations.size) { ulongArrayOf() }, method = method @@ -71,11 +77,11 @@ class StmtAliasInfo( val toFieldsMap = mutableMapOf() allocToFields[i].forEach { val (s, a) = unwrap(it) - toFieldsMap.merge(s, a, ::merge) + toFieldsMap.merge(s, a, Companion::merge) } other.allocToFields[i].forEach { val (s, a) = unwrap(it) - toFieldsMap.merge(s, a, ::merge) + toFieldsMap.merge(s, a, Companion::merge) } merged.allocToFields[i] = toFieldsMap .map { (string, alloc) -> wrap(string, alloc) } @@ -102,10 +108,9 @@ class StmtAliasInfo( nodes.add(MULTIPLE_EDGE) strings.add(ELEMENT_ACCESSOR) } - is FieldAccessor -> { val string = method.stringMap[accessor.name] - ?: error("Unknown field name: ${accessor.name}") + ?: error("Unknown field name") strings.add(string) node = allocToFields[node] @@ -122,17 +127,17 @@ class StmtAliasInfo( return Pair(nodes, strings) } - fun assign(lhv: AccessPath, rhv: AccessPath): StmtAliasInfo { + private fun assign(lhv: AccessPath, rhv: AccessPath): StmtAliasInfoImpl { val (rhvNodes, _) = trace(rhv) val newAlloc = rhvNodes.last() return assign(lhv, newAlloc) } - fun assign(lhv: AccessPath, newAlloc: Int): StmtAliasInfo { + private fun assign(lhv: AccessPath, newAlloc: Int): StmtAliasInfoImpl { val (lhvNodes, lhvEdges) = trace(lhv) val from = lhvNodes.reversed().getOrNull(1) if (from != null) { - val updated = StmtAliasInfo( + val updated = StmtAliasInfoImpl( baseToAlloc = baseToAlloc, allocToFields = allocToFields.copyOf(), method = method, @@ -155,7 +160,7 @@ class StmtAliasInfo( return updated } else { - val updated = StmtAliasInfo( + val updated = StmtAliasInfoImpl( baseToAlloc = baseToAlloc.copyOf(), allocToFields = allocToFields, method = method, @@ -169,29 +174,28 @@ class StmtAliasInfo( } } - fun applyStmt(stmt: EtsStmt): StmtAliasInfo? { + internal fun applyStmt(stmt: EtsStmt): StmtAliasInfoImpl { if (stmt !is EtsAssignStmt) { return this } when (val rhv = stmt.rhv) { is EtsParameterRef -> { - val alloc = method.allocationMap[MethodAliasInfo.Allocation.Arg(rhv.index)] - ?: error("Unknown parameter ref in stmt: $stmt") + val alloc = method.allocationMap[MethodAliasInfoImpl.Allocation.Arg(rhv.index)] + ?: error("Unknown parameter ref") return assign(stmt.lhv.toPath(), alloc) } - is EtsThis -> { - val alloc = method.allocationMap[MethodAliasInfo.Allocation.This] - ?: error("Unknown this in stmt: $stmt") + val alloc = method.allocationMap[MethodAliasInfoImpl.Allocation.This] + ?: error("Uninitialized this") return assign(stmt.lhv.toPath(), alloc) } - is EtsInstanceFieldRef, is EtsStaticFieldRef -> { val (rhvNodes, _) = trace(rhv.toPath()) val alloc = rhvNodes.last() if (alloc == NOT_PROCESSED) { - val fieldAlloc = method.allocationMap[MethodAliasInfo.Allocation.Imm(stmt)] - ?: error("Unknown allocation in stmt: $stmt") + val fieldAlloc = method.allocationMap[MethodAliasInfoImpl.Allocation.Imm(stmt)] + ?: error("Unknown allocation") + return this .assign(rhv.toPath(), fieldAlloc) .assign(stmt.lhv.toPath(), fieldAlloc) @@ -199,36 +203,29 @@ class StmtAliasInfo( return assign(stmt.lhv.toPath(), alloc) } } - is EtsLocal -> { return assign(stmt.lhv.toPath(), rhv.toPath()) } - is EtsCastExpr -> { return assign(stmt.lhv.toPath(), rhv.arg.toPath()) } - is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { - val imm = method.allocationMap[MethodAliasInfo.Allocation.Expr(stmt)] - ?: error("Unknown expr in stmt: $stmt") + val imm = method.allocationMap[MethodAliasInfoImpl.Allocation.Expr(stmt)] + ?: error("Unknown constant") return assign(stmt.lhv.toPath(), imm) } - is EtsCallExpr -> { - val callResult = method.allocationMap[MethodAliasInfo.Allocation.CallResult(stmt)] - ?: error("Unknown call in stmt: $stmt") + val callResult = method.allocationMap[MethodAliasInfoImpl.Allocation.CallResult(stmt)] + ?: error("Unknown call") return assign(stmt.lhv.toPath(), callResult) } - is EtsNewExpr, is EtsNewArrayExpr -> { - val new = method.allocationMap[MethodAliasInfo.Allocation.New(stmt)] - ?: error("Unknown new in stmt: $stmt") + val new = method.allocationMap[MethodAliasInfoImpl.Allocation.New(stmt)] + ?: error("Unknown new") return assign(stmt.lhv.toPath(), new) } - else -> { - logger.warn("Could not process rhs in stmt: $stmt") - return null + error("Unprocessable") } } } @@ -267,7 +264,7 @@ class StmtAliasInfo( get() = edge?.first fun traceContains(other: Int): Boolean = - alloc == other || (parent?.traceContains(other) == true) + alloc == other || (parent?.traceContains(other) ?: false) } private fun accessors(node: PathNode): List { @@ -285,7 +282,7 @@ class StmtAliasInfo( return accessors } - fun getAliases(path: AccessPath): Set { + override fun getAliases(path: AccessPath): Set { val alloc = trace(path).first.last() if (alloc == NOT_PROCESSED || alloc == MULTIPLE_EDGE) { return setOf(path) @@ -319,9 +316,9 @@ class StmtAliasInfo( } } -class MethodAliasInfo( +class MethodAliasInfoImpl( val method: EtsMethod, -) { +) : MethodAliasInfo { sealed interface Allocation { data class New(val stmt: EtsStmt) : Allocation data class CallResult(val stmt: EtsStmt) : Allocation @@ -341,7 +338,7 @@ class MethodAliasInfo( val baseMap = mutableMapOf() val bases = mutableListOf() - fun newString(str: String) { + private fun newString(str: String) { stringMap.computeIfAbsent(str) { strings.add(str) stringMap.size @@ -365,22 +362,16 @@ class MethodAliasInfo( is AccessPathBase.Local -> { newString(base.name) } - is AccessPathBase.This -> { newAllocation(Allocation.This) } - is AccessPathBase.Arg -> { newAllocation(Allocation.Arg(base.index)) } - is AccessPathBase.Static -> { newAllocation(Allocation.Static(base.clazz)) } - - is AccessPathBase.Const -> { - // TODO ?? may be some non-trivial - } + is AccessPathBase.Const -> { /* TODO ?? may be some non-trivial */ } } } @@ -390,25 +381,20 @@ class MethodAliasInfo( initEntity(entity.instance) newString(entity.field.name) } - is EtsStaticFieldRef -> { newBase(AccessPathBase.Static(entity.field.enclosingClass)) newString(entity.field.name) } - is EtsArrayAccess -> { initEntity(entity.array) initEntity(entity.index) } - is EtsLocal -> { newBase(AccessPathBase.Local(entity.name)) } - is EtsParameterRef -> { newBase(AccessPathBase.Arg(entity.index)) } - is EtsInstanceCallExpr -> { initEntity(entity.instance) newString(entity.method.name) @@ -437,21 +423,16 @@ class MethodAliasInfo( is EtsNewExpr, is EtsNewArrayExpr -> { newAllocation(Allocation.New(stmt)) } - is EtsParameterRef -> { newAllocation(Allocation.Arg(rhv.index)) } - is EtsCallExpr -> { newAllocation(Allocation.CallResult(stmt)) } - is EtsInstanceFieldRef, is EtsStaticFieldRef -> { newAllocation(Allocation.Imm(stmt)) } - is EtsCastExpr -> {} - is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { newAllocation(Allocation.Expr(stmt)) } @@ -469,11 +450,11 @@ class MethodAliasInfo( initMaps() } - private val preAliases: MutableMap = hashMapOf() + private val preAliases = mutableMapOf() @OptIn(ExperimentalUnsignedTypes::class) @Suppress("UNCHECKED_CAST") - fun computeAliases(): List { + override fun computeAliases(): List { val visited: MutableSet = hashSetOf() val order: MutableList = mutableListOf() val preds: MutableMap> = hashMapOf() @@ -494,14 +475,14 @@ class MethodAliasInfo( postOrderDfs(root) order.reverse() - fun computePreAliases(stmt: EtsStmt): StmtAliasInfo { + fun computePreAliases(stmt: EtsStmt): StmtAliasInfoImpl { if (stmt in preAliases) return preAliases.getValue(stmt) val merged = preds[stmt] - ?.mapNotNull { preAliases.getValue(it).applyStmt(it) } + ?.map { preAliases.getValue(it).applyStmt(it) } ?.reduceOrNull { a, b -> a.merge(b) } - ?: StmtAliasInfo( - baseToAlloc = IntArray(bases.size) { StmtAliasInfo.NOT_PROCESSED }, + ?: StmtAliasInfoImpl( + baseToAlloc = IntArray(bases.size) { StmtAliasInfoImpl.NOT_PROCESSED }, allocToFields = Array(allocations.size) { ulongArrayOf() }, method = this ) @@ -510,12 +491,24 @@ class MethodAliasInfo( return merged } - val aliases = Array(method.cfg.stmts.size) { null } + val aliases = Array(method.cfg.stmts.size) { null } for (stmt in order) { aliases[stmt.location.index] = computePreAliases(stmt) } assert(!aliases.contains(null)) - return (aliases as Array).toList() + return (aliases as Array).toList() + } +} + +object NoStmtAliasInfo : StmtAliasInfo { + override fun getAliases(path: AccessPath): Set { + return setOf(path) + } +} + +class NoMethodAliasInfo(val method: EtsMethod) : MethodAliasInfo { + override fun computeAliases(): List { + return method.cfg.stmts.map { NoStmtAliasInfo } } } 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 8bfce4798c..325f02650e 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 @@ -14,9 +14,18 @@ class ForwardAnalyzer( methodInitialTypes: Map>, typeInfo: Map, doAddKnownTypes: Boolean = true, + doAliasAnalysis: Boolean = true, + val doLiveVariablesAnalysis: Boolean = true, ) : Analyzer { - override val flowFunctions = ForwardFlowFunctions(graph, methodInitialTypes, typeInfo, doAddKnownTypes) + override val flowFunctions = ForwardFlowFunctions( + graph = graph, + methodInitialTypes = methodInitialTypes, + typeInfo = typeInfo, + doAddKnownTypes = doAddKnownTypes, + doAliasAnalysis = doAliasAnalysis, + doLiveVariablesAnalysis = doLiveVariablesAnalysis, + ) override fun handleCrossUnitCall( caller: Vertex, @@ -25,13 +34,28 @@ class ForwardAnalyzer( error("No cross unit calls") } + private val liveVariablesCache = hashMapOf() + private fun liveVariables(method: EtsMethod) = + liveVariablesCache.computeIfAbsent(method) { + if (doLiveVariablesAnalysis) + LiveVariables.from(method) + else + AlwaysAlive + } + override fun handleNewEdge(edge: Edge): List { val (startVertex, currentVertex) = edge val (current, currentFact) = currentVertex val method = graph.methodOf(current) val currentIsExit = current in graph.exitPoints(method) || (current is EtsNopStmt && graph.successors(current).none()) - if (currentIsExit) { + + val variableIsDying = (currentFact as? ForwardTypeDomainFact.TypedVariable)?.let { + val base = it.variable.base + base is AccessPathBase.Local && (!liveVariables(method).isAliveAt(base.name, current)) + } ?: false + + if (currentIsExit || variableIsDying) { return listOf( ForwardSummaryAnalyzerEvent( method = method, 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 5317688664..ddc65c1981 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 @@ -5,8 +5,10 @@ import org.jacodb.ets.base.EtsAnyType import org.jacodb.ets.base.EtsArithmeticExpr import org.jacodb.ets.base.EtsArrayAccess import org.jacodb.ets.base.EtsAssignStmt +import org.jacodb.ets.base.EtsAwaitExpr import org.jacodb.ets.base.EtsBooleanConstant import org.jacodb.ets.base.EtsCastExpr +import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsFieldRef import org.jacodb.ets.base.EtsInstanceCallExpr import org.jacodb.ets.base.EtsLocal @@ -23,6 +25,7 @@ import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.base.EtsStringConstant import org.jacodb.ets.base.EtsThis import org.jacodb.ets.base.EtsType +import org.jacodb.ets.base.EtsUnclearRefType import org.jacodb.ets.base.EtsUndefinedConstant import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.model.EtsMethod @@ -44,16 +47,31 @@ class ForwardFlowFunctions( val methodInitialTypes: Map>, val typeInfo: Map, val doAddKnownTypes: Boolean = true, + val doAliasAnalysis: Boolean = true, + val doLiveVariablesAnalysis: Boolean = true, ) : FlowFunctions { private val typeProcessor = TypeFactProcessor(graph.cp) private val aliasesCache: MutableMap> = hashMapOf() - private fun getAliases(method: EtsMethod): List { - return aliasesCache.computeIfAbsent(method) { MethodAliasInfo(method).computeAliases() } + return aliasesCache.computeIfAbsent(method) { + if (doAliasAnalysis) + MethodAliasInfoImpl(method).computeAliases() + else + NoMethodAliasInfo(method).computeAliases() + } } + private val liveVariablesCache = hashMapOf() + private fun liveVariables(method: EtsMethod) = + liveVariablesCache.computeIfAbsent(method) { + if (doLiveVariablesAnalysis) + LiveVariables.from(method) + else + AlwaysAlive + } + override fun obtainPossibleStartFacts(method: EtsMethod): Collection { val initialTypes = methodInitialTypes[method] ?: return listOf(Zero) @@ -147,7 +165,16 @@ class ForwardFlowFunctions( } when (fact) { Zero -> sequentZero(current) - is TypedVariable -> sequentFact(current, fact).myFilter() + is TypedVariable -> { + val liveVars = liveVariables(current.method) + sequentFact(current, fact).myFilter() + .filter { + when (val base = it.variable.base) { + is AccessPathBase.Local -> liveVars.isAliveAt(base.name, current) //|| liveVars.isAliveAt(base.name, next) + else -> true + } + } + } } } @@ -163,7 +190,13 @@ class ForwardFlowFunctions( if (path.accesses.isNotEmpty()) { check(path.accesses.size == 1) val base = AccessPath(path.base, emptyList()) - for (alias in preAliases.getAliases(base)) { + val aliases = preAliases.getAliases(base).filter { + when (val b = it.base) { + is AccessPathBase.Local -> liveVariables(current.method).isAliveAt(b.name, current) + else -> true + } + } + for (alias in aliases) { val newPath = alias + path.accesses.single() result += TypedVariable(newPath, type) } @@ -267,6 +300,7 @@ class ForwardFlowFunctions( is EtsFieldRef -> r.toPath() is EtsArrayAccess -> r.toPath() is EtsCastExpr -> r.toPath() + is EtsAwaitExpr -> r.toPath() else -> { // logger.info { "TODO forward assign: $current" } null @@ -341,6 +375,20 @@ class ForwardFlowFunctions( // val type = EtsTypeFact.from((current.rhv as EtsCastExpr).type).intersect(fact.type) ?: fact.type val type = EtsTypeFact.from((current.rhv as EtsCastExpr).type) return listOf(fact, TypedVariable(path, type)) + } else if (current.rhv is EtsAwaitExpr) { + val path = AccessPath(lhv.base, fact.variable.accesses) + val promiseType = fact.type + if (promiseType is EtsTypeFact.ObjectEtsTypeFact) { + val promiseClass = promiseType.cls + if (promiseClass is EtsClassType && promiseClass.signature.name == "Promise") { + val type = EtsTypeFact.from(promiseClass.typeParameters.singleOrNull() ?: return listOf(fact)) + return listOf(fact, TypedVariable(path, type)) + } + if (promiseClass is EtsUnclearRefType && promiseClass.name.startsWith("Promise")) { + val type = EtsTypeFact.from(promiseClass.typeParameters.singleOrNull() ?: return listOf(fact)) + return listOf(fact, TypedVariable(path, type)) + } + } } val path = AccessPath(lhv.base, fact.variable.accesses) @@ -426,7 +474,15 @@ class ForwardFlowFunctions( val path1 = lhv + fact.variable.accesses result += TypedVariable(path1, fact.type) // } - for (z in preAliases.getAliases(x)) { + + val aliases = preAliases.getAliases(x).filter { + when (val b = it.base) { + is AccessPathBase.Local -> liveVariables(current.method).isAliveAt(b.name, current) + else -> true + } + } + + for (z in aliases) { // skip duplicate fields // if (z.accesses.firstOrNull() != a) { // TODO: what about z.accesses.last == a ? 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 new file mode 100644 index 0000000000..cd8a96e6d9 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt @@ -0,0 +1,190 @@ +package org.usvm.dataflow.ts.infer + +import org.jacodb.ets.base.EtsArrayAccess +import org.jacodb.ets.base.EtsAssignStmt +import org.jacodb.ets.base.EtsBinaryExpr +import org.jacodb.ets.base.EtsCallExpr +import org.jacodb.ets.base.EtsCallStmt +import org.jacodb.ets.base.EtsCastExpr +import org.jacodb.ets.base.EtsEntity +import org.jacodb.ets.base.EtsIfStmt +import org.jacodb.ets.base.EtsInstanceCallExpr +import org.jacodb.ets.base.EtsInstanceFieldRef +import org.jacodb.ets.base.EtsInstanceOfExpr +import org.jacodb.ets.base.EtsLocal +import org.jacodb.ets.base.EtsReturnStmt +import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.base.EtsSwitchStmt +import org.jacodb.ets.base.EtsTernaryExpr +import org.jacodb.ets.base.EtsThrowStmt +import org.jacodb.ets.base.EtsUnaryExpr +import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsMethod + +interface LiveVariables { + fun isAliveAt(local: String, stmt: EtsStmt): Boolean + + companion object { + private const val THRESHOLD: Int = 20 + + fun from(method: EtsMethod): LiveVariables = + if (method.cfg.stmts.size > THRESHOLD) + LiveVariablesImpl(method) + else AlwaysAlive + } +} + +object AlwaysAlive : LiveVariables { + override fun isAliveAt(local: String, stmt: EtsStmt): Boolean = true +} + +class LiveVariablesImpl( + val method: EtsMethod +) : LiveVariables { + companion object { + private fun EtsEntity.used(): List = when (this) { + is EtsValue -> this.used() + is EtsUnaryExpr -> arg.used() + is EtsBinaryExpr -> left.used() + right.used() + is EtsCallExpr -> this.used() + is EtsCastExpr -> arg.used() + is EtsInstanceOfExpr -> arg.used() + is EtsTernaryExpr -> condition.used() + thenExpr.used() + elseExpr.used() + else -> emptyList() + } + + private fun EtsValue.used(): List = when (this) { + is EtsLocal -> listOf(name) + is EtsInstanceFieldRef -> listOf(instance.name) + is EtsArrayAccess -> array.used() + index.used() + else -> emptyList() + } + + private fun EtsCallExpr.used(): List = when (this) { + is EtsInstanceCallExpr -> listOf(instance.name) + args.flatMap { it.used() } + else -> args.flatMap { it.used() } + } + + private fun postOrder(sources: Iterable, successors: (T) -> Iterable): List { + val order = mutableListOf() + val visited = hashSetOf() + + fun dfs(node: T) { + visited.add(node) + for (next in successors(node)) { + if (next !in visited) + dfs(next) + } + order.add(node) + } + + for (source in sources) { + if (source !in visited) + dfs(source) + } + + return order + } + } + + private fun stronglyConnectedComponents(): IntArray { + val rpo = postOrder(method.cfg.entries) { + method.cfg.successors(it) + }.reversed() + + val coloring = IntArray(method.cfg.stmts.size) { -1 } + var nextColor = 0 + fun backwardDfs(stmt: EtsStmt) { + coloring[stmt.location.index] = nextColor + if (stmt in method.cfg.entries) + return + for (next in method.cfg.predecessors(stmt)) { + if (coloring[next.location.index] == -1) { + backwardDfs(next) + } + } + } + + for (stmt in rpo) { + if (coloring[stmt.location.index] == -1) { + backwardDfs(stmt) + nextColor++ + } + } + + return coloring + } + + private fun condensation(coloring: IntArray): Map> { + val successors = hashMapOf>() + for (from in method.cfg.stmts) { + for (to in method.cfg.successors(from)) { + val fromColor = coloring[from.location.index] + val toColor = coloring[to.location.index] + if (fromColor != toColor) { + successors.computeIfAbsent(fromColor) { hashSetOf() } + .add(toColor) + } + } + } + return successors + } + + private val lifetime = hashMapOf>() + private val coloring = stronglyConnectedComponents() + private val colorIndex: IntArray + + init { + val condensationSuccessors = condensation(coloring) + val entriesColors = method.cfg.entries.map { + coloring[it.location.index] + } + val colorOrder = postOrder(entriesColors) { + condensationSuccessors[it].orEmpty() + }.reversed() + + colorIndex = IntArray(colorOrder.size) { -1 } + for ((index, color) in colorOrder.withIndex()) { + colorIndex[color] = index + } + + val ownLocals = hashSetOf() + for (stmt in method.cfg.stmts) { + if (stmt is EtsAssignStmt) { + when (val lhv = stmt.lhv) { + is EtsLocal -> ownLocals.add(lhv.name) + } + } + } + + for (stmt in method.cfg.stmts) { + val usedLocals = when (stmt) { + is EtsAssignStmt -> stmt.lhv.used() + stmt.rhv.used() + is EtsCallStmt -> stmt.expr.used() + is EtsReturnStmt -> stmt.returnValue?.used().orEmpty() + is EtsIfStmt -> stmt.condition.used() + is EtsSwitchStmt -> stmt.arg.used() + is EtsThrowStmt -> stmt.arg.used() + else -> emptyList() + } + val blockIndex = colorIndex[coloring[stmt.location.index]] + + for (local in usedLocals) { + if (local in ownLocals) { + lifetime.merge(local, blockIndex to blockIndex) { (begin, end), (bb, be) -> + minOf(begin, bb) to maxOf(end, be) + } + } else { + lifetime[local] = Int.MIN_VALUE to Int.MAX_VALUE + } + } + } + } + + override fun isAliveAt(local: String, stmt: EtsStmt): Boolean { + if (stmt.location.index < 0) return true + val block = colorIndex[coloring[stmt.location.index]] + val (begin, end) = lifetime[local] ?: error("Unknown local") + return block in begin..end + } +} 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 37a79888c4..a525d7db6a 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 @@ -187,7 +187,14 @@ class TypeInferenceManager( logger.info { "Preparing forward analysis" } val forwardGraph = graph - val forwardAnalyzer = ForwardAnalyzer(forwardGraph, methodTypeScheme, typeInfo, doAddKnownTypes) + val forwardAnalyzer = ForwardAnalyzer( + forwardGraph, + methodTypeScheme, + typeInfo, + doAddKnownTypes, + doAliasAnalysis = true, + doLiveVariablesAnalysis = true) + val forwardRunner = UniRunner( traits = traits, manager = this@TypeInferenceManager, @@ -333,19 +340,10 @@ class TypeInferenceManager( private fun getInferredCombinedThisTypes( methodTypeScheme: Map>, ): Map { - val classBySignature = graph.cp.projectAndSdkClasses - .groupByTo(hashMapOf()) { it.signature } - - val allClasses = methodTypeScheme.keys - .map { it.enclosingClass } - .distinct() - .map { sig -> classBySignature[sig].orEmpty().first() } - .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } - val forwardSummariesByClass = forwardSummaries .entries.groupByTo(hashMapOf()) { (method, _) -> method.enclosingClass } - return allClasses.mapNotNull { cls -> + return graph.cp.projectClasses.mapNotNull { cls -> val clsMethods = (cls.methods + cls.ctor).toHashSet() val combinedBackwardType = clsMethods .mapNotNull { methodTypeScheme[it] } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt index 81820a9f0a..45851b8ce3 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt @@ -27,6 +27,7 @@ import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsBinaryExpr import org.jacodb.ets.base.EtsBooleanConstant import org.jacodb.ets.base.EtsCallExpr +import org.jacodb.ets.base.EtsCallStmt import org.jacodb.ets.base.EtsCastExpr import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsConstant @@ -98,7 +99,11 @@ class EtsTraits : Traits { } override fun getCallExpr(statement: EtsStmt): EtsCallExpr? { - return statement.callExpr + return when (statement) { + is EtsAssignStmt -> statement.rhv as? EtsCallExpr + is EtsCallStmt -> statement.expr + else -> null + } } override fun getValues(expr: CommonExpr): Set { 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 21f1d8a9ea..9beda5bb5d 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 @@ -28,7 +28,8 @@ import java.io.File @Disabled class EtsTypeResolverPerformanceTest { companion object { - const val RUNS = 5 + const val WARMUP_ITERATIONS = 0 + const val TEST_ITERATIONS = 10 const val OUTPUT_FILE = "performance_report.md" @JvmStatic @@ -38,7 +39,7 @@ class EtsTypeResolverPerformanceTest { } private fun runOnAbcProject(projectID: String, abcPath: String): PerformanceReport { - val report = generateReportForProject(projectID, abcPath, RUNS) + val report = generateReportForProject(projectID, abcPath, WARMUP_ITERATIONS, TEST_ITERATIONS) return report } @@ -76,14 +77,12 @@ class EtsTypeResolverPerformanceTest { ) val file = File(OUTPUT_FILE) - file.writeText( - buildString { - appendLine("|project|min time|max time|%|") - appendLine("|:--|:--|:--|:--|") - reports.forEach { - appendLine(it.dumpToString()) - } + file.writeText(buildString { + appendLine("|project|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 ef8d5a1482..4b442b5aea 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 @@ -48,6 +48,12 @@ object AbcProjects { } fun runOnAbcProject(scene: EtsScene): Pair { + val result = inferTypes(scene) + val statistics = calculateStatistics(scene, result) + 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) @@ -66,6 +72,12 @@ object AbcProjects { .analyze(entrypoint.mainMethods, allMethods, doAddKnownTypes = true) .withGuessedTypes(guesser) + return result + } + + fun calculateStatistics(scene: EtsScene, result: TypeInferenceResult): TypeInferenceStatistics { + val graphAbc = createApplicationGraph(scene) + val entrypoint = EntryPointsProcessor(scene).extractEntryPoints() val sceneStatistics = TypeInferenceStatistics() entrypoint.allMethods .filter { it.cfg.stmts.isNotEmpty() } @@ -73,6 +85,6 @@ object AbcProjects { val methodTypeFacts = MethodTypesFacts.from(result, it) sceneStatistics.compareSingleMethodFactsWithTypesInScene(methodTypeFacts, it, graphAbc) } - return Pair(result, sceneStatistics) + return sceneStatistics } } 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 bccdcdab68..900b0e42f0 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 @@ -16,20 +16,27 @@ package org.usvm.dataflow.ts.test.utils +import java.math.RoundingMode import kotlin.time.Duration +import kotlin.time.DurationUnit import kotlin.time.measureTimedValue + data class PerformanceReport( val projectId: String, val maxTime: Duration, + val avgTime: Duration, + val medianTime: Duration, val minTime: Duration, val improvement: Double, ) { fun dumpToString(): String = listOf( projectId, - minTime, - maxTime, - improvement + 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() ).joinToString( separator = "|", prefix = "|", @@ -40,24 +47,29 @@ data class PerformanceReport( fun generateReportForProject( projectId: String, abcPath: String, - runCount: Int, + warmupIterationsCount: Int, + runIterationsCount: Int ): PerformanceReport { val abcScene = AbcProjects.getAbcProject(abcPath) - val results = List(runCount) { - val (statistics, time) = measureTimedValue { - AbcProjects.runOnAbcProject(abcScene).second + val results = List(warmupIterationsCount + runIterationsCount) { + val (result, time) = measureTimedValue { + AbcProjects.inferTypes(abcScene) } + val statistics = AbcProjects.calculateStatistics(abcScene, result) time to statistics.calculateImprovement() - } + }.drop(warmupIterationsCount) val times = results.map { it.first } - val improvement = results.map { it.second }.distinct().single() + val improvement = results.map { it.second }.distinct().first() + val totalTime = times.reduce { acc, duration -> acc + duration } return PerformanceReport( projectId = projectId, minTime = times.min(), maxTime = times.max(), + avgTime = totalTime / runIterationsCount, + medianTime = times.sorted()[runIterationsCount / 2], improvement = improvement ) } From 18f6a3343d22db5106ee24a75ab0f50c95255bb8 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Wed, 5 Mar 2025 13:48:58 +0300 Subject: [PATCH 02/21] update liveness analysis --- .../usvm/dataflow/ts/infer/LiveVariables.kt | 147 ++++++------------ 1 file changed, 46 insertions(+), 101 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 cd8a96e6d9..bea0140dd2 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 @@ -20,6 +20,7 @@ import org.jacodb.ets.base.EtsThrowStmt import org.jacodb.ets.base.EtsUnaryExpr import org.jacodb.ets.base.EtsValue import org.jacodb.ets.model.EtsMethod +import java.util.BitSet interface LiveVariables { fun isAliveAt(local: String, stmt: EtsStmt): Boolean @@ -64,118 +65,63 @@ class LiveVariablesImpl( is EtsInstanceCallExpr -> listOf(instance.name) + args.flatMap { it.used() } else -> args.flatMap { it.used() } } - - private fun postOrder(sources: Iterable, successors: (T) -> Iterable): List { - val order = mutableListOf() - val visited = hashSetOf() - - fun dfs(node: T) { - visited.add(node) - for (next in successors(node)) { - if (next !in visited) - dfs(next) - } - order.add(node) - } - - for (source in sources) { - if (source !in visited) - dfs(source) - } - - return order - } - } - - private fun stronglyConnectedComponents(): IntArray { - val rpo = postOrder(method.cfg.entries) { - method.cfg.successors(it) - }.reversed() - - val coloring = IntArray(method.cfg.stmts.size) { -1 } - var nextColor = 0 - fun backwardDfs(stmt: EtsStmt) { - coloring[stmt.location.index] = nextColor - if (stmt in method.cfg.entries) - return - for (next in method.cfg.predecessors(stmt)) { - if (coloring[next.location.index] == -1) { - backwardDfs(next) - } - } - } - - for (stmt in rpo) { - if (coloring[stmt.location.index] == -1) { - backwardDfs(stmt) - nextColor++ - } - } - - return coloring } - private fun condensation(coloring: IntArray): Map> { - val successors = hashMapOf>() - for (from in method.cfg.stmts) { - for (to in method.cfg.successors(from)) { - val fromColor = coloring[from.location.index] - val toColor = coloring[to.location.index] - if (fromColor != toColor) { - successors.computeIfAbsent(fromColor) { hashSetOf() } - .add(toColor) - } - } - } - return successors - } + private val aliveAtStmt: Array + private val indexOfName = hashMapOf() + private val definedAtStmt = IntArray(method.cfg.stmts.size) { -1 } - private val lifetime = hashMapOf>() - private val coloring = stronglyConnectedComponents() - private val colorIndex: IntArray + private fun emptyBitSet() = BitSet(indexOfName.size) + private fun BitSet.copy() = clone() as BitSet init { - val condensationSuccessors = condensation(coloring) - val entriesColors = method.cfg.entries.map { - coloring[it.location.index] - } - val colorOrder = postOrder(entriesColors) { - condensationSuccessors[it].orEmpty() - }.reversed() - - colorIndex = IntArray(colorOrder.size) { -1 } - for ((index, color) in colorOrder.withIndex()) { - colorIndex[color] = index - } - - val ownLocals = hashSetOf() for (stmt in method.cfg.stmts) { if (stmt is EtsAssignStmt) { when (val lhv = stmt.lhv) { - is EtsLocal -> ownLocals.add(lhv.name) + is EtsLocal -> { + val lhvIndex = indexOfName.size + definedAtStmt[stmt.location.index] = lhvIndex + indexOfName[lhv.name] = lhvIndex + } } } } - for (stmt in method.cfg.stmts) { - val usedLocals = when (stmt) { - is EtsAssignStmt -> stmt.lhv.used() + stmt.rhv.used() - is EtsCallStmt -> stmt.expr.used() - is EtsReturnStmt -> stmt.returnValue?.used().orEmpty() - is EtsIfStmt -> stmt.condition.used() - is EtsSwitchStmt -> stmt.arg.used() - is EtsThrowStmt -> stmt.arg.used() - else -> emptyList() + 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 usedLocals = when (stmt) { + is EtsAssignStmt -> stmt.lhv.used() + stmt.rhv.used() + is EtsCallStmt -> stmt.expr.used() + is EtsReturnStmt -> stmt.returnValue?.used().orEmpty() + is EtsIfStmt -> stmt.condition.used() + is EtsSwitchStmt -> stmt.arg.used() + is EtsThrowStmt -> stmt.arg.used() + else -> emptyList() + } + + usedLocals.mapNotNull { indexOfName[it] }.forEach { set(it) } } - val blockIndex = colorIndex[coloring[stmt.location.index]] - for (local in usedLocals) { - if (local in ownLocals) { - lifetime.merge(local, blockIndex to blockIndex) { (begin, end), (bb, be) -> - minOf(begin, bb) to maxOf(end, be) - } - } else { - lifetime[local] = Int.MIN_VALUE to Int.MAX_VALUE + for (succ in method.cfg.successors(stmt)) { + val transferFromSucc = aliveAtStmt[succ.location.index].copy() + val definedAtSucc = definedAtStmt[succ.location.index] + if (definedAtSucc != -1) { + transferFromSucc.clear(definedAtSucc) + } + + aliveHere.or(transferFromSucc) + } + + if (aliveHere != aliveAtStmt[stmt.location.index]) { + aliveAtStmt[stmt.location.index] = aliveHere + if (stmt !in method.cfg.entries) { + queue.addAll(method.cfg.predecessors(stmt)) } } } @@ -183,8 +129,7 @@ class LiveVariablesImpl( override fun isAliveAt(local: String, stmt: EtsStmt): Boolean { if (stmt.location.index < 0) return true - val block = colorIndex[coloring[stmt.location.index]] - val (begin, end) = lifetime[local] ?: error("Unknown local") - return block in begin..end + val index = indexOfName[local] ?: return true + return aliveAtStmt[stmt.location.index].get(index) } } From 71892b441a73aa2e2741676a65d453d5c06e4726 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Fri, 7 Mar 2025 11:14:47 +0300 Subject: [PATCH 03/21] cleanup --- .../usvm/dataflow/ts/infer/ForwardAnalyzer.kt | 5 +--- .../dataflow/ts/infer/ForwardFlowFunctions.kt | 25 +++++++++++++------ .../usvm/dataflow/ts/infer/LiveVariables.kt | 6 ++--- .../dataflow/ts/infer/TypeInferenceManager.kt | 4 +-- .../ts/test/EtsTypeResolverPerformanceTest.kt | 7 +++--- .../ts/test/utils/PerformanceReport.kt | 2 +- 6 files changed, 27 insertions(+), 22 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 325f02650e..b868256dc3 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 @@ -37,10 +37,7 @@ class ForwardAnalyzer( private val liveVariablesCache = hashMapOf() private fun liveVariables(method: EtsMethod) = liveVariablesCache.computeIfAbsent(method) { - if (doLiveVariablesAnalysis) - LiveVariables.from(method) - else - AlwaysAlive + if (doLiveVariablesAnalysis) LiveVariables.from(method) else AlwaysAlive } 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 ddc65c1981..d42dc4bf4f 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 @@ -56,20 +56,22 @@ class ForwardFlowFunctions( private val aliasesCache: MutableMap> = hashMapOf() private fun getAliases(method: EtsMethod): List { return aliasesCache.computeIfAbsent(method) { - if (doAliasAnalysis) + if (doAliasAnalysis) { MethodAliasInfoImpl(method).computeAliases() - else + } else { NoMethodAliasInfo(method).computeAliases() + } } } private val liveVariablesCache = hashMapOf() private fun liveVariables(method: EtsMethod) = liveVariablesCache.computeIfAbsent(method) { - if (doLiveVariablesAnalysis) + if (doLiveVariablesAnalysis) { LiveVariables.from(method) - else + } else { AlwaysAlive + } } override fun obtainPossibleStartFacts(method: EtsMethod): Collection { @@ -170,7 +172,7 @@ class ForwardFlowFunctions( sequentFact(current, fact).myFilter() .filter { when (val base = it.variable.base) { - is AccessPathBase.Local -> liveVars.isAliveAt(base.name, current) //|| liveVars.isAliveAt(base.name, next) + is AccessPathBase.Local -> liveVars.isAliveAt(base.name, current) else -> true } } @@ -372,20 +374,27 @@ class ForwardFlowFunctions( // Using the cast type directly is just a temporary solution to satisfy simple tests. if (current.rhv is EtsCastExpr) { val path = AccessPath(lhv.base, fact.variable.accesses) - // val type = EtsTypeFact.from((current.rhv as EtsCastExpr).type).intersect(fact.type) ?: fact.type val type = EtsTypeFact.from((current.rhv as EtsCastExpr).type) + return listOf(fact, TypedVariable(path, type)) } else if (current.rhv is EtsAwaitExpr) { val path = AccessPath(lhv.base, fact.variable.accesses) val promiseType = fact.type + if (promiseType is EtsTypeFact.ObjectEtsTypeFact) { val promiseClass = promiseType.cls + if (promiseClass is EtsClassType && promiseClass.signature.name == "Promise") { - val type = EtsTypeFact.from(promiseClass.typeParameters.singleOrNull() ?: return listOf(fact)) + val type = EtsTypeFact.from( + type = promiseClass.typeParameters.singleOrNull() ?: return listOf(fact) + ) return listOf(fact, TypedVariable(path, type)) } + if (promiseClass is EtsUnclearRefType && promiseClass.name.startsWith("Promise")) { - val type = EtsTypeFact.from(promiseClass.typeParameters.singleOrNull() ?: return listOf(fact)) + val type = EtsTypeFact.from( + type = promiseClass.typeParameters.singleOrNull() ?: return listOf(fact) + ) return listOf(fact, TypedVariable(path, type)) } } 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 bea0140dd2..6420c0ca60 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 @@ -29,9 +29,7 @@ interface LiveVariables { private const val THRESHOLD: Int = 20 fun from(method: EtsMethod): LiveVariables = - if (method.cfg.stmts.size > THRESHOLD) - LiveVariablesImpl(method) - else AlwaysAlive + if (method.cfg.stmts.size > THRESHOLD) LiveVariablesImpl(method) else AlwaysAlive } } @@ -40,7 +38,7 @@ object AlwaysAlive : LiveVariables { } class LiveVariablesImpl( - val method: EtsMethod + val method: EtsMethod, ) : LiveVariables { companion object { private fun EtsEntity.used(): List = when (this) { 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 a525d7db6a..a27a6b29e9 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 @@ -12,7 +12,6 @@ import kotlinx.coroutines.newSingleThreadContext import kotlinx.coroutines.runBlocking import kotlinx.coroutines.withTimeout import mu.KotlinLogging -import org.jacodb.ets.base.ANONYMOUS_CLASS_PREFIX import org.jacodb.ets.base.CONSTRUCTOR_NAME import org.jacodb.ets.base.EtsReturnStmt import org.jacodb.ets.base.EtsStmt @@ -193,7 +192,8 @@ class TypeInferenceManager( typeInfo, doAddKnownTypes, doAliasAnalysis = true, - doLiveVariablesAnalysis = true) + doLiveVariablesAnalysis = true, + ) val forwardRunner = UniRunner( traits = traits, 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 9beda5bb5d..73f299699d 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 @@ -76,13 +76,14 @@ class EtsTypeResolverPerformanceTest { ) ) - val file = File(OUTPUT_FILE) - file.writeText(buildString { + val reportStr = buildString { appendLine("|project|min time|max time|avg time|median time|%|") appendLine("|:--|:--|:--|:--|:--|:--|") reports.forEach { appendLine(it.dumpToString()) } - }) + } + val file = File(OUTPUT_FILE) + file.writeText(reportStr) } } 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 900b0e42f0..b45207c4df 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 @@ -48,7 +48,7 @@ fun generateReportForProject( projectId: String, abcPath: String, warmupIterationsCount: Int, - runIterationsCount: Int + runIterationsCount: Int, ): PerformanceReport { val abcScene = AbcProjects.getAbcProject(abcPath) From 2e348fd63ad65c1d55e7ac1a893081a82103825f Mon Sep 17 00:00:00 2001 From: MForest7 Date: Fri, 7 Mar 2025 16:16:09 +0300 Subject: [PATCH 04/21] add index for callees --- .../org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt index 008b6eff49..8da3b9bf20 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt @@ -104,6 +104,11 @@ class EtsApplicationGraphImpl( .flatMap { it.methods } .groupByTo(hashMapOf()) { it.name } } + private val classMethodsByName by lazy { + projectClassesBySignature.mapValues { (_, clazz) -> + clazz.single().methods.groupBy { it.name } + } + } private val cacheClassWithIdealSignature: MutableMap> = hashMapOf() private val cacheMethodWithIdealSignature: MutableMap> = hashMapOf() @@ -227,11 +232,8 @@ class EtsApplicationGraphImpl( // If the complete signature match failed, // try to find the unique not-the-same neighbour method in the same class: - val neighbors = cls.methods - .asSequence() - .filter { it.name == callee.name } + val neighbors = classMethodsByName[cls.signature].orEmpty()[callee.name].orEmpty() .filterNot { it.name == node.method.name } - .toList() if (neighbors.isNotEmpty()) { val s = neighbors.singleOrNull() ?: error("Multiple methods with the same name: $neighbors") From a04e48388cb34b4b08597eee1cb1a45842ba70c6 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 11 Mar 2025 14:50:14 +0300 Subject: [PATCH 05/21] cleanup --- .../usvm/dataflow/ts/infer/ForwardAnalyzer.kt | 16 +++++++++------- .../dataflow/ts/infer/TypeInferenceManager.kt | 3 +-- .../org/usvm/dataflow/ts/util/EtsTraits.kt | 7 +------ .../ts/test/EtsTypeResolverPerformanceTest.kt | 4 ++-- 4 files changed, 13 insertions(+), 17 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 b868256dc3..8413b5da2b 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 @@ -35,11 +35,18 @@ class ForwardAnalyzer( } private val liveVariablesCache = hashMapOf() - private fun liveVariables(method: EtsMethod) = + 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) + } + override fun handleNewEdge(edge: Edge): List { val (startVertex, currentVertex) = edge val (current, currentFact) = currentVertex @@ -47,12 +54,7 @@ class ForwardAnalyzer( val currentIsExit = current in graph.exitPoints(method) || (current is EtsNopStmt && graph.successors(current).none()) - val variableIsDying = (currentFact as? ForwardTypeDomainFact.TypedVariable)?.let { - val base = it.variable.base - base is AccessPathBase.Local && (!liveVariables(method).isAliveAt(base.name, current)) - } ?: false - - if (currentIsExit || variableIsDying) { + if (currentIsExit || variableIsDying(currentFact, current)) { return listOf( ForwardSummaryAnalyzerEvent( method = method, 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 a27a6b29e9..0aca314322 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 @@ -344,8 +344,7 @@ class TypeInferenceManager( .entries.groupByTo(hashMapOf()) { (method, _) -> method.enclosingClass } return graph.cp.projectClasses.mapNotNull { cls -> - val clsMethods = (cls.methods + cls.ctor).toHashSet() - val combinedBackwardType = clsMethods + val combinedBackwardType = (cls.methods + cls.ctor) .mapNotNull { methodTypeScheme[it] } .mapNotNull { facts -> facts[AccessPathBase.This] }.reduceOrNull { acc, type -> typeProcessor.intersect(acc, type) ?: run { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt index 45851b8ce3..81820a9f0a 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt @@ -27,7 +27,6 @@ import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsBinaryExpr import org.jacodb.ets.base.EtsBooleanConstant import org.jacodb.ets.base.EtsCallExpr -import org.jacodb.ets.base.EtsCallStmt import org.jacodb.ets.base.EtsCastExpr import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsConstant @@ -99,11 +98,7 @@ class EtsTraits : Traits { } override fun getCallExpr(statement: EtsStmt): EtsCallExpr? { - return when (statement) { - is EtsAssignStmt -> statement.rhv as? EtsCallExpr - is EtsCallStmt -> statement.expr - else -> null - } + return statement.callExpr } override fun getValues(expr: CommonExpr): Set { 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 73f299699d..255e98ef9b 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 @@ -28,8 +28,8 @@ import java.io.File @Disabled class EtsTypeResolverPerformanceTest { companion object { - const val WARMUP_ITERATIONS = 0 - const val TEST_ITERATIONS = 10 + const val WARMUP_ITERATIONS = 5 + const val TEST_ITERATIONS = 5 const val OUTPUT_FILE = "performance_report.md" @JvmStatic From bfbbc9fc0624e59f7314e86ff2970b463fa3a4c7 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Wed, 19 Mar 2025 15:13:32 +0300 Subject: [PATCH 06/21] keep StmtAliasInfo type --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 2ad79117d6..25194765b3 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -475,7 +475,7 @@ class MethodAliasInfoImpl( postOrderDfs(root) order.reverse() - fun computePreAliases(stmt: EtsStmt): StmtAliasInfoImpl { + fun computePreAliases(stmt: EtsStmt): StmtAliasInfo { if (stmt in preAliases) return preAliases.getValue(stmt) val merged = preds[stmt] @@ -491,13 +491,13 @@ class MethodAliasInfoImpl( return merged } - val aliases = Array(method.cfg.stmts.size) { null } + val aliases = Array(method.cfg.stmts.size) { null } for (stmt in order) { aliases[stmt.location.index] = computePreAliases(stmt) } assert(!aliases.contains(null)) - return (aliases as Array).toList() + return (aliases as Array).toList() } } From 433728607b1b1cea1427f7db2808f64bf73c1c23 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 13:02:08 +0300 Subject: [PATCH 07/21] Import --- .../main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 25194765b3..49b5f689e1 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -21,6 +21,7 @@ import org.jacodb.ets.base.EtsThis import org.jacodb.ets.base.EtsUnaryExpr import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod +import org.usvm.dataflow.ts.infer.MethodAliasInfoImpl.Allocation import kotlin.collections.ArrayDeque interface StmtAliasInfo { @@ -180,12 +181,12 @@ class StmtAliasInfoImpl( } when (val rhv = stmt.rhv) { is EtsParameterRef -> { - val alloc = method.allocationMap[MethodAliasInfoImpl.Allocation.Arg(rhv.index)] + val alloc = method.allocationMap[Allocation.Arg(rhv.index)] ?: error("Unknown parameter ref") return assign(stmt.lhv.toPath(), alloc) } is EtsThis -> { - val alloc = method.allocationMap[MethodAliasInfoImpl.Allocation.This] + val alloc = method.allocationMap[Allocation.This] ?: error("Uninitialized this") return assign(stmt.lhv.toPath(), alloc) } @@ -193,7 +194,7 @@ class StmtAliasInfoImpl( val (rhvNodes, _) = trace(rhv.toPath()) val alloc = rhvNodes.last() if (alloc == NOT_PROCESSED) { - val fieldAlloc = method.allocationMap[MethodAliasInfoImpl.Allocation.Imm(stmt)] + val fieldAlloc = method.allocationMap[Allocation.Imm(stmt)] ?: error("Unknown allocation") return this @@ -210,17 +211,17 @@ class StmtAliasInfoImpl( return assign(stmt.lhv.toPath(), rhv.arg.toPath()) } is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { - val imm = method.allocationMap[MethodAliasInfoImpl.Allocation.Expr(stmt)] + val imm = method.allocationMap[Allocation.Expr(stmt)] ?: error("Unknown constant") return assign(stmt.lhv.toPath(), imm) } is EtsCallExpr -> { - val callResult = method.allocationMap[MethodAliasInfoImpl.Allocation.CallResult(stmt)] + val callResult = method.allocationMap[Allocation.CallResult(stmt)] ?: error("Unknown call") return assign(stmt.lhv.toPath(), callResult) } is EtsNewExpr, is EtsNewArrayExpr -> { - val new = method.allocationMap[MethodAliasInfoImpl.Allocation.New(stmt)] + val new = method.allocationMap[Allocation.New(stmt)] ?: error("Unknown new") return assign(stmt.lhv.toPath(), new) } From b743b757e975522694d66c6ed68ef5b967dc76bf Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 13:02:17 +0300 Subject: [PATCH 08/21] Format --- .../org/usvm/dataflow/ts/infer/Alias.kt | 26 +++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 49b5f689e1..a49ad0819d 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -22,7 +22,6 @@ import org.jacodb.ets.base.EtsUnaryExpr import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod import org.usvm.dataflow.ts.infer.MethodAliasInfoImpl.Allocation -import kotlin.collections.ArrayDeque interface StmtAliasInfo { fun getAliases(path: AccessPath): Set @@ -109,6 +108,7 @@ class StmtAliasInfoImpl( nodes.add(MULTIPLE_EDGE) strings.add(ELEMENT_ACCESSOR) } + is FieldAccessor -> { val string = method.stringMap[accessor.name] ?: error("Unknown field name") @@ -185,11 +185,13 @@ class StmtAliasInfoImpl( ?: error("Unknown parameter ref") return assign(stmt.lhv.toPath(), alloc) } + is EtsThis -> { val alloc = method.allocationMap[Allocation.This] ?: error("Uninitialized this") return assign(stmt.lhv.toPath(), alloc) } + is EtsInstanceFieldRef, is EtsStaticFieldRef -> { val (rhvNodes, _) = trace(rhv.toPath()) val alloc = rhvNodes.last() @@ -204,27 +206,33 @@ class StmtAliasInfoImpl( return assign(stmt.lhv.toPath(), alloc) } } + is EtsLocal -> { return assign(stmt.lhv.toPath(), rhv.toPath()) } + is EtsCastExpr -> { return assign(stmt.lhv.toPath(), rhv.arg.toPath()) } + is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { val imm = method.allocationMap[Allocation.Expr(stmt)] ?: error("Unknown constant") return assign(stmt.lhv.toPath(), imm) } + is EtsCallExpr -> { val callResult = method.allocationMap[Allocation.CallResult(stmt)] ?: error("Unknown call") return assign(stmt.lhv.toPath(), callResult) } + is EtsNewExpr, is EtsNewArrayExpr -> { val new = method.allocationMap[Allocation.New(stmt)] ?: error("Unknown new") return assign(stmt.lhv.toPath(), new) } + else -> { error("Unprocessable") } @@ -363,16 +371,21 @@ class MethodAliasInfoImpl( is AccessPathBase.Local -> { newString(base.name) } + is AccessPathBase.This -> { newAllocation(Allocation.This) } + is AccessPathBase.Arg -> { newAllocation(Allocation.Arg(base.index)) } + is AccessPathBase.Static -> { newAllocation(Allocation.Static(base.clazz)) } - is AccessPathBase.Const -> { /* TODO ?? may be some non-trivial */ } + + is AccessPathBase.Const -> { /* TODO ?? may be some non-trivial */ + } } } @@ -382,20 +395,25 @@ class MethodAliasInfoImpl( initEntity(entity.instance) newString(entity.field.name) } + is EtsStaticFieldRef -> { newBase(AccessPathBase.Static(entity.field.enclosingClass)) newString(entity.field.name) } + is EtsArrayAccess -> { initEntity(entity.array) initEntity(entity.index) } + is EtsLocal -> { newBase(AccessPathBase.Local(entity.name)) } + is EtsParameterRef -> { newBase(AccessPathBase.Arg(entity.index)) } + is EtsInstanceCallExpr -> { initEntity(entity.instance) newString(entity.method.name) @@ -424,15 +442,19 @@ class MethodAliasInfoImpl( is EtsNewExpr, is EtsNewArrayExpr -> { newAllocation(Allocation.New(stmt)) } + is EtsParameterRef -> { newAllocation(Allocation.Arg(rhv.index)) } + is EtsCallExpr -> { newAllocation(Allocation.CallResult(stmt)) } + is EtsInstanceFieldRef, is EtsStaticFieldRef -> { newAllocation(Allocation.Imm(stmt)) } + is EtsCastExpr -> {} is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { newAllocation(Allocation.Expr(stmt)) From 1bb4ce07ceb926a8bcc933fc98b0bc60ef1c78ae Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 13:05:22 +0300 Subject: [PATCH 09/21] Lift return --- .../org/usvm/dataflow/ts/infer/Alias.kt | 21 +++++++++---------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index a49ad0819d..cdf4b6218a 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -179,17 +179,17 @@ class StmtAliasInfoImpl( if (stmt !is EtsAssignStmt) { return this } - when (val rhv = stmt.rhv) { + return when (val rhv = stmt.rhv) { is EtsParameterRef -> { val alloc = method.allocationMap[Allocation.Arg(rhv.index)] ?: error("Unknown parameter ref") - return assign(stmt.lhv.toPath(), alloc) + assign(stmt.lhv.toPath(), alloc) } is EtsThis -> { val alloc = method.allocationMap[Allocation.This] ?: error("Uninitialized this") - return assign(stmt.lhv.toPath(), alloc) + assign(stmt.lhv.toPath(), alloc) } is EtsInstanceFieldRef, is EtsStaticFieldRef -> { @@ -198,39 +198,38 @@ class StmtAliasInfoImpl( if (alloc == NOT_PROCESSED) { val fieldAlloc = method.allocationMap[Allocation.Imm(stmt)] ?: error("Unknown allocation") - - return this + this .assign(rhv.toPath(), fieldAlloc) .assign(stmt.lhv.toPath(), fieldAlloc) } else { - return assign(stmt.lhv.toPath(), alloc) + assign(stmt.lhv.toPath(), alloc) } } is EtsLocal -> { - return assign(stmt.lhv.toPath(), rhv.toPath()) + assign(stmt.lhv.toPath(), rhv.toPath()) } is EtsCastExpr -> { - return assign(stmt.lhv.toPath(), rhv.arg.toPath()) + assign(stmt.lhv.toPath(), rhv.arg.toPath()) } is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { val imm = method.allocationMap[Allocation.Expr(stmt)] ?: error("Unknown constant") - return assign(stmt.lhv.toPath(), imm) + assign(stmt.lhv.toPath(), imm) } is EtsCallExpr -> { val callResult = method.allocationMap[Allocation.CallResult(stmt)] ?: error("Unknown call") - return assign(stmt.lhv.toPath(), callResult) + assign(stmt.lhv.toPath(), callResult) } is EtsNewExpr, is EtsNewArrayExpr -> { val new = method.allocationMap[Allocation.New(stmt)] ?: error("Unknown new") - return assign(stmt.lhv.toPath(), new) + assign(stmt.lhv.toPath(), new) } else -> { From 4a55c0823451dca4bf43c4cf7976616629a2a620 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 13:19:53 +0300 Subject: [PATCH 10/21] Enrich error messages --- .../org/usvm/dataflow/ts/infer/Alias.kt | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index cdf4b6218a..e75626e566 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -93,7 +93,7 @@ class StmtAliasInfoImpl( private fun trace(path: AccessPath): Pair, MutableList> { val base = method.baseMap[path.base] - ?: error("Unknown path base") + ?: error("Unknown path base: ${path.base}") var node = baseToAlloc[base] val nodes = mutableListOf(node) @@ -111,7 +111,7 @@ class StmtAliasInfoImpl( is FieldAccessor -> { val string = method.stringMap[accessor.name] - ?: error("Unknown field name") + ?: error("Unknown field name: ${accessor.name}") strings.add(string) node = allocToFields[node] @@ -168,7 +168,7 @@ class StmtAliasInfoImpl( ) val base = method.baseMap[lhv.base] - ?: error("Unknown path base") + ?: error("Unknown path base: ${lhv.base}") updated.baseToAlloc[base] = newAlloc return updated @@ -182,13 +182,13 @@ class StmtAliasInfoImpl( return when (val rhv = stmt.rhv) { is EtsParameterRef -> { val alloc = method.allocationMap[Allocation.Arg(rhv.index)] - ?: error("Unknown parameter ref") + ?: error("Unknown parameter ref in stmt: $stmt") assign(stmt.lhv.toPath(), alloc) } is EtsThis -> { val alloc = method.allocationMap[Allocation.This] - ?: error("Uninitialized this") + ?: error("Uninitialized this in stmt: $stmt") assign(stmt.lhv.toPath(), alloc) } @@ -197,7 +197,7 @@ class StmtAliasInfoImpl( val alloc = rhvNodes.last() if (alloc == NOT_PROCESSED) { val fieldAlloc = method.allocationMap[Allocation.Imm(stmt)] - ?: error("Unknown allocation") + ?: error("Unknown allocation in stmt: $stmt") this .assign(rhv.toPath(), fieldAlloc) .assign(stmt.lhv.toPath(), fieldAlloc) @@ -216,24 +216,24 @@ class StmtAliasInfoImpl( is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { val imm = method.allocationMap[Allocation.Expr(stmt)] - ?: error("Unknown constant") + ?: error("Unknown constant in stmt: $stmt") assign(stmt.lhv.toPath(), imm) } is EtsCallExpr -> { val callResult = method.allocationMap[Allocation.CallResult(stmt)] - ?: error("Unknown call") + ?: error("Unknown call in stmt: $stmt") assign(stmt.lhv.toPath(), callResult) } is EtsNewExpr, is EtsNewArrayExpr -> { val new = method.allocationMap[Allocation.New(stmt)] - ?: error("Unknown new") + ?: error("Unknown new in stmt: $stmt") assign(stmt.lhv.toPath(), new) } else -> { - error("Unprocessable") + error("Unprocessable rhs in stmt: $stmt") } } } @@ -285,7 +285,8 @@ class StmtAliasInfoImpl( } accessors.add(FieldAccessor(method.strings[str])) - cur = cur.parent ?: error("If the property is defined, the parent should exist") + cur = cur.parent + ?: error("If the property is defined, the parent should exist") } return accessors } From 934b87b874ed30f2376a60ab518e3076704cee22 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:01:15 +0300 Subject: [PATCH 11/21] Add Trace class --- .../org/usvm/dataflow/ts/infer/Alias.kt | 36 +++++++++++-------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index e75626e566..401dd0ad21 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -91,52 +91,57 @@ class StmtAliasInfoImpl( return merged } - private fun trace(path: AccessPath): Pair, MutableList> { + private class Trace( + val nodes: List, + val edges: List, + ) + + private fun trace(path: AccessPath): Trace { val base = method.baseMap[path.base] ?: error("Unknown path base: ${path.base}") var node = baseToAlloc[base] val nodes = mutableListOf(node) - val strings = mutableListOf() + val edges = mutableListOf() for (accessor in path.accesses) { if (node == NOT_PROCESSED || node == MULTIPLE_EDGE) { - return Pair(nodes, strings) + return Trace(nodes, edges) } when (accessor) { is ElementAccessor -> { nodes.add(MULTIPLE_EDGE) - strings.add(ELEMENT_ACCESSOR) + edges.add(ELEMENT_ACCESSOR) } is FieldAccessor -> { val string = method.stringMap[accessor.name] ?: error("Unknown field name: ${accessor.name}") - strings.add(string) + edges.add(string) node = allocToFields[node] .singleOrNull { e -> unwrap(e).first == string } ?.let { e -> unwrap(e).second } ?: run { nodes.add(NOT_PROCESSED) - return Pair(nodes, strings) + return Trace(nodes, edges) } nodes.add(node) } } } - return Pair(nodes, strings) + return Trace(nodes, edges) } private fun assign(lhv: AccessPath, rhv: AccessPath): StmtAliasInfoImpl { - val (rhvNodes, _) = trace(rhv) - val newAlloc = rhvNodes.last() + val trace = trace(rhv) + val newAlloc = trace.nodes.last() return assign(lhv, newAlloc) } private fun assign(lhv: AccessPath, newAlloc: Int): StmtAliasInfoImpl { - val (lhvNodes, lhvEdges) = trace(lhv) - val from = lhvNodes.reversed().getOrNull(1) + val trace = trace(lhv) + val from = trace.nodes.reversed().getOrNull(1) if (from != null) { val updated = StmtAliasInfoImpl( baseToAlloc = baseToAlloc, @@ -144,7 +149,7 @@ class StmtAliasInfoImpl( method = method, ) - val str = lhvEdges.last() + val str = trace.edges.last() val edgeIndex = allocToFields[from].indexOfFirst { val (s, _) = unwrap(it) s == str @@ -193,8 +198,8 @@ class StmtAliasInfoImpl( } is EtsInstanceFieldRef, is EtsStaticFieldRef -> { - val (rhvNodes, _) = trace(rhv.toPath()) - val alloc = rhvNodes.last() + val trace = trace(rhv.toPath()) + val alloc = trace.nodes.last() if (alloc == NOT_PROCESSED) { val fieldAlloc = method.allocationMap[Allocation.Imm(stmt)] ?: error("Unknown allocation in stmt: $stmt") @@ -292,7 +297,8 @@ class StmtAliasInfoImpl( } override fun getAliases(path: AccessPath): Set { - val alloc = trace(path).first.last() + val trace = trace(path) + val alloc = trace.nodes.last() if (alloc == NOT_PROCESSED || alloc == MULTIPLE_EDGE) { return setOf(path) } From 52edae0e4bb9051e095dc5e51c4e3204865b3640 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:04:12 +0300 Subject: [PATCH 12/21] Visibility modifiers --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 401dd0ad21..6ca774459b 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -37,13 +37,12 @@ class StmtAliasInfoImpl( val allocToFields: Array, val method: MethodAliasInfoImpl, ) : StmtAliasInfo { - internal companion object { + companion object { internal const val NOT_PROCESSED = -1 internal const val MULTIPLE_EDGE = -2 - internal const val ELEMENT_ACCESSOR = -3 - internal fun merge(first: Int, second: Int): Int = when { + private fun merge(first: Int, second: Int): Int = when { first == NOT_PROCESSED -> second second == NOT_PROCESSED -> first first == MULTIPLE_EDGE -> MULTIPLE_EDGE @@ -52,11 +51,11 @@ class StmtAliasInfoImpl( else -> MULTIPLE_EDGE } - internal fun wrap(string: Int, alloc: Int): ULong { + private fun wrap(string: Int, alloc: Int): ULong { return (string.toULong() shl Int.SIZE_BITS) or alloc.toULong() } - internal fun unwrap(edge: ULong): Pair { + private fun unwrap(edge: ULong): Pair { val string = (edge shr Int.SIZE_BITS).toInt() val allocation = (edge and UInt.MAX_VALUE.toULong()).toInt() return Pair(string, allocation) From 3966d10deb12738aa97857af1b81ad2a758429b2 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:05:29 +0300 Subject: [PATCH 13/21] Flow --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 6ca774459b..014364519a 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -202,12 +202,11 @@ class StmtAliasInfoImpl( if (alloc == NOT_PROCESSED) { val fieldAlloc = method.allocationMap[Allocation.Imm(stmt)] ?: error("Unknown allocation in stmt: $stmt") - this + return this .assign(rhv.toPath(), fieldAlloc) .assign(stmt.lhv.toPath(), fieldAlloc) - } else { - assign(stmt.lhv.toPath(), alloc) } + assign(stmt.lhv.toPath(), alloc) } is EtsLocal -> { From af62bb3406ae9f85afd5a3e7ee17db53f0aa9e06 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:26:22 +0300 Subject: [PATCH 14/21] Cleanup --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 014364519a..ca9224aeae 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -154,12 +154,10 @@ class StmtAliasInfoImpl( s == str } if (edgeIndex == -1) { - updated.allocToFields[from] = allocToFields[from].toMutableList().apply { - add(wrap(str, newAlloc)) - }.toULongArray() + updated.allocToFields[from] = allocToFields[from] + wrap(str, newAlloc) } else { - updated.allocToFields[from] = allocToFields[from].copyOf().apply { - set(edgeIndex, wrap(str, newAlloc)) + updated.allocToFields[from] = allocToFields[from].copyOf().also { + it[edgeIndex] = wrap(str, newAlloc) } } From 0efe20e62948ac42fff74c12ad8b3d71406297fa Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:27:37 +0300 Subject: [PATCH 15/21] Cleanup --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index ca9224aeae..a66288ec3d 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -386,7 +386,8 @@ class MethodAliasInfoImpl( newAllocation(Allocation.Static(base.clazz)) } - is AccessPathBase.Const -> { /* TODO ?? may be some non-trivial */ + is AccessPathBase.Const -> { + // TODO: non-trivial } } } From d6e7d1ed18cd1b7ec8b27ca70cfb0d5dd7e8a164 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:30:11 +0300 Subject: [PATCH 16/21] Format --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 1 + 1 file changed, 1 insertion(+) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index a66288ec3d..5483e565c6 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -459,6 +459,7 @@ class MethodAliasInfoImpl( } is EtsCastExpr -> {} + is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { newAllocation(Allocation.Expr(stmt)) } From a21cd7525460efff4106ffa52ee1137499a83ef6 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:34:28 +0300 Subject: [PATCH 17/21] Data object This --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 5483e565c6..d65c782a5b 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -334,7 +334,7 @@ class MethodAliasInfoImpl( data class New(val stmt: EtsStmt) : Allocation data class CallResult(val stmt: EtsStmt) : Allocation data class Arg(val index: Int) : Allocation - object This : Allocation + data object This : Allocation data class Imm(val stmt: EtsStmt) : Allocation data class Expr(val stmt: EtsStmt) : Allocation data class Static(val clazz: EtsClassSignature) : Allocation From 3258d322d5b1ba78a05d609582d5e652dcca8e86 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:42:03 +0300 Subject: [PATCH 18/21] Ignore (warn) unsupported exprs --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index d65c782a5b..5c3f1a78d2 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -1,5 +1,6 @@ package org.usvm.dataflow.ts.infer +import mu.KotlinLogging import org.jacodb.ets.base.EtsArrayAccess import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsBinaryExpr @@ -23,6 +24,8 @@ import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod import org.usvm.dataflow.ts.infer.MethodAliasInfoImpl.Allocation +private val logger = KotlinLogging.logger {} + interface StmtAliasInfo { fun getAliases(path: AccessPath): Set } @@ -234,7 +237,8 @@ class StmtAliasInfoImpl( } else -> { - error("Unprocessable rhs in stmt: $stmt") + logger.warn { "Unprocessable rhs in stmt: $stmt" } + this } } } From 4bdca680682594466552e9e939102eb370a7bb45 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 24 Mar 2025 15:44:44 +0300 Subject: [PATCH 19/21] Handle EtsAwaitExpr in toPathOrNull --- .../src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt index fbea013977..e188307ec7 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt @@ -1,6 +1,7 @@ package org.usvm.dataflow.ts.infer import org.jacodb.ets.base.EtsArrayAccess +import org.jacodb.ets.base.EtsAwaitExpr import org.jacodb.ets.base.EtsCastExpr import org.jacodb.ets.base.EtsConstant import org.jacodb.ets.base.EtsEntity @@ -129,6 +130,8 @@ fun EtsEntity.toPathOrNull(): AccessPath? = when (this) { is EtsCastExpr -> arg.toPathOrNull() + is EtsAwaitExpr -> arg.toPathOrNull() + else -> null } From 43fe1266ea2b75a400c5def15ad7be7e164c122c Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 25 Mar 2025 13:30:25 +0300 Subject: [PATCH 20/21] fix alias analysis --- .../org/usvm/dataflow/ts/infer/Alias.kt | 30 ++++++++++++++----- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index 5c3f1a78d2..def121b407 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -284,12 +284,13 @@ class StmtAliasInfoImpl( var cur = node val accessors = mutableListOf() while (true) { - val str = cur.string - if (str == null) { - break + val accessor = when (val str = cur.string) { + null -> break + ELEMENT_ACCESSOR -> ElementAccessor + else -> FieldAccessor(method.strings[str]) } - accessors.add(FieldAccessor(method.strings[str])) + accessors.add(accessor) cur = cur.parent ?: error("If the property is defined, the parent should exist") } @@ -392,6 +393,7 @@ class MethodAliasInfoImpl( is AccessPathBase.Const -> { // TODO: non-trivial + error("Unexpected base: $base") } } } @@ -439,10 +441,15 @@ class MethodAliasInfoImpl( initEntity(stmt.lhv) initEntity(stmt.rhv) - when (stmt.lhv) { - is EtsInstanceFieldRef, is EtsStaticFieldRef -> { + when (val lhv = stmt.lhv) { + is EtsInstanceFieldRef -> { newAllocation(Allocation.Imm(stmt)) } + + is EtsStaticFieldRef -> { + newAllocation(Allocation.Imm(stmt)) + newBase(AccessPathBase.Static(lhv.field.enclosingClass)) + } } when (val rhv = stmt.rhv) { @@ -458,11 +465,18 @@ class MethodAliasInfoImpl( newAllocation(Allocation.CallResult(stmt)) } - is EtsInstanceFieldRef, is EtsStaticFieldRef -> { + is EtsInstanceFieldRef -> { newAllocation(Allocation.Imm(stmt)) } - is EtsCastExpr -> {} + is EtsStaticFieldRef -> { + newAllocation(Allocation.Imm(stmt)) + newBase(AccessPathBase.Static(rhv.field.enclosingClass)) + } + + is EtsCastExpr -> { + initEntity(rhv.arg) + } is EtsConstant, is EtsUnaryExpr, is EtsBinaryExpr, is EtsArrayAccess, is EtsInstanceOfExpr -> { newAllocation(Allocation.Expr(stmt)) From 895e1df241f6ef3128b811f3538c6c10b5e94c83 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Tue, 25 Mar 2025 13:46:19 +0300 Subject: [PATCH 21/21] add flag to enable alias analysis --- .../org/usvm/dataflow/ts/infer/TypeInferenceManager.kt | 6 +++++- .../kotlin/org/usvm/dataflow/ts/infer/cli/InferTypes.kt | 6 ++++++ 2 files changed, 11 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 0aca314322..a7bcb78dff 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 @@ -79,10 +79,12 @@ class TypeInferenceManager( allMethods: List = entrypoints, doAddKnownTypes: Boolean = true, doInferAllLocals: Boolean = true, + doAliasAnalysis: Boolean = true, ): TypeInferenceResult = runBlocking { val methodTypeScheme = collectSummaries( startMethods = entrypoints, doAddKnownTypes = doAddKnownTypes, + doAliasAnalysis = doAliasAnalysis, ) val remainingMethodsForAnalysis = allMethods.filter { it !in methodTypeScheme.keys } @@ -92,6 +94,7 @@ class TypeInferenceManager( collectSummaries( startMethods = remainingMethodsForAnalysis, doAddKnownTypes = doAddKnownTypes, + doAliasAnalysis = doAliasAnalysis, ) } @@ -104,6 +107,7 @@ class TypeInferenceManager( private suspend fun collectSummaries( startMethods: List, doAddKnownTypes: Boolean = true, + doAliasAnalysis: Boolean = true, ): Map> { logger.info { "Preparing backward analysis" } val backwardGraph = graph.reversed @@ -191,7 +195,7 @@ class TypeInferenceManager( methodTypeScheme, typeInfo, doAddKnownTypes, - doAliasAnalysis = true, + doAliasAnalysis = doAliasAnalysis, doLiveVariablesAnalysis = true, ) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/InferTypes.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/InferTypes.kt index 098aab73f3..614218a979 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/InferTypes.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/InferTypes.kt @@ -70,6 +70,11 @@ class InferTypes : CliktCommand() { help = "Do take into account the known types in scene" ).flag("--no-use-known-types", default = true) + val enableAliasAnalysis by option( + "--alias-analysis", + help = "Enable alias analysis" + ).flag("--no-alias-analysis", default = true) + override fun run() { logger.info { "Running InferTypes" } val startTime = System.currentTimeMillis() @@ -91,6 +96,7 @@ class InferTypes : CliktCommand() { entrypoints = dummyMains, allMethods = publicMethods, doAddKnownTypes = useKnownTypes, + doAliasAnalysis = enableAliasAnalysis, ) } logger.info { "Inferred types for ${resultBasic.inferredTypes.size} methods in $timeAnalyze" }