diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d04bd49cf3..53f4137e8e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -127,7 +127,7 @@ jobs: DEST_DIR="arkanalyzer" MAX_RETRIES=10 RETRY_DELAY=3 # Delay between retries in seconds - BRANCH="neo/2025-04-14" + BRANCH="neo/2025-05-12" for ((i=1; i<=MAX_RETRIES; i++)); do git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt new file mode 100644 index 0000000000..8a1a44b5c2 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsMethodRunner.kt @@ -0,0 +1,119 @@ +package org.usvm.dataflow.ts.ifds + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStmtLocation +import org.usvm.dataflow.ifds.Analyzer +import org.usvm.dataflow.ifds.Edge +import org.usvm.dataflow.ifds.Vertex +import org.usvm.dataflow.ts.graph.EtsApplicationGraph +import org.usvm.dataflow.ts.infer.AnalyzerEvent +import org.usvm.dataflow.ts.infer.TypeInferenceManager +import org.usvm.dataflow.ts.util.EtsTraits + +internal class EtsIfdsMethodRunner( + val graph: EtsApplicationGraph, + val method: EtsMethod, + val analyzer: Analyzer, + val traits: EtsTraits, + val manager: TypeInferenceManager, + val commonRunner: EtsIfdsRunner, +) { + internal val flowSpace = analyzer.flowFunctions + private var enqueued: Boolean = false + private val sourceRunnersQueue: ArrayDeque> = ArrayDeque() + + internal fun enqueue(runner: EtsIfdsSourceRunner) { + sourceRunnersQueue.addLast(runner) + if (!enqueued) { + commonRunner.methodRunnersQueue.addLast(this) + enqueued = true + } + } + + fun processFacts() { + while (!sourceRunnersQueue.isEmpty()) { + val currentSourceRunner = sourceRunnersQueue.removeFirst() + currentSourceRunner.processFacts() + } + enqueued = false + } + + internal val sourceRunners = hashMapOf>>() + internal fun getSourceRunner(vertex: Vertex): EtsIfdsSourceRunner { + return sourceRunners + .getOrPut(vertex.fact) { hashMapOf() } + .getOrPut(vertex.statement) { + EtsIfdsSourceRunner(traits, this, vertex.statement, vertex.fact) + } + } + + internal fun getSourceRunners(fact: Fact): Collection> { + return sourceRunners.getOrPut(fact) { + entrypoints.associateWithTo(hashMapOf()) { + EtsIfdsSourceRunner(traits, this, it, fact) + } + }.values + } + + internal val mockStmt = EtsNopStmt(EtsStmtLocation(method, -1)) + internal val stmts = listOf(mockStmt) + method.cfg.stmts + + internal val isExit = BooleanArray(stmts.size).apply { + for (exit in graph.exitPoints(method)) { + set(exit.index, true) + } + } + + internal val EtsStmt.index: Int + get() = location.index + 1 + + internal val successors = stmts.map { graph.successors(it).map { s -> s.index } } + internal val entrypoints = graph.entryPoints(method).toList() + + fun addStart() { + val startFacts = flowSpace.obtainPossibleStartFacts(method) + for (startFact in startFacts) { + propagateStartingFact(startFact) + } + } + + internal data class PathEdge( + val endStmtIndex: Int, + val fact: Fact, + ) + + internal fun propagateStartingFact(fact: Fact): Set> { + val summaryEdges = hashSetOf>() + for (entrypoint in entrypoints) { + val runner = getSourceRunner(Vertex(entrypoint, fact)) + runner.propagate(PathEdge(entrypoint.index, fact)) + summaryEdges += runner.summaryEdges + } + return summaryEdges + } + + internal fun handleSummaryEdgeInCaller( + currentEdge: Edge, + summaryEdge: Edge, + ) { + val (startVertex, currentVertex) = currentEdge + val sourceRunner = getSourceRunner(startVertex) + val caller = currentVertex.statement + for (returnSite in graph.successors(caller)) { + val (exit, exitFact) = summaryEdge.to + val finalFacts = flowSpace + .obtainExitToReturnSiteFlowFunction(caller, returnSite, exit) + .compute(exitFact) + for (returnSiteFact in finalFacts) { + val newEdge = PathEdge(caller.index, returnSiteFact) + sourceRunner.propagate(newEdge) + } + } + } + + override fun toString(): String { + return "Runner for ${method.signature}" + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt new file mode 100644 index 0000000000..70f159e8d5 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsRunner.kt @@ -0,0 +1,87 @@ +package org.usvm.dataflow.ts.ifds + +import kotlinx.coroutines.coroutineScope +import kotlinx.coroutines.isActive +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt +import org.usvm.dataflow.ifds.Analyzer +import org.usvm.dataflow.ifds.Edge +import org.usvm.dataflow.ifds.IfdsResult +import org.usvm.dataflow.ifds.QueueEmptinessChanged +import org.usvm.dataflow.ifds.Reason +import org.usvm.dataflow.ifds.Runner +import org.usvm.dataflow.ifds.SingletonUnit +import org.usvm.dataflow.ifds.UnitType +import org.usvm.dataflow.ts.graph.EtsApplicationGraph +import org.usvm.dataflow.ts.infer.AnalyzerEvent +import org.usvm.dataflow.ts.infer.TypeInferenceManager +import org.usvm.dataflow.ts.util.EtsTraits + +class EtsIfdsRunner( + override val graph: EtsApplicationGraph, + val analyzer: Analyzer, + val traits: EtsTraits, + val manager: TypeInferenceManager, + private val zeroFact: Fact, +) : Runner { + internal val methodRunnersQueue: ArrayDeque> = ArrayDeque() + private val queueIsEmpty = QueueEmptinessChanged(runner = this, isEmpty = true) + + private val methodRunners = hashMapOf>() + + internal fun getMethodRunner(method: EtsMethod): EtsIfdsMethodRunner { + return methodRunners.getOrPut(method) { + EtsIfdsMethodRunner( + graph = graph, + method = method, + analyzer = analyzer, + traits = traits, + manager = manager, + commonRunner = this@EtsIfdsRunner, + ) + } + } + + override suspend fun run(startMethods: List) { + for (method in startMethods) { + getMethodRunner(method).addStart() + } + + tabulationAlgorithm() + } + + private suspend fun tabulationAlgorithm() = coroutineScope { + while (isActive) { + val current = methodRunnersQueue.removeFirstOrNull() ?: run { + manager.handleControlEvent(queueIsEmpty) + return@coroutineScope + } + current.processFacts() + } + } + + override val unit: UnitType + get() = SingletonUnit + + override fun getIfdsResult(): IfdsResult { + val sourceRunners = methodRunners.values.flatMap { methodRunner -> + methodRunner.sourceRunners.values.flatMap { it.values } + } + val pathEdges = sourceRunners.flatMap { it.getPathEdges() } + + val resultFacts: MutableMap> = hashMapOf() + for (edge in pathEdges) { + resultFacts.getOrPut(edge.to.statement) { hashSetOf() }.add(edge.to.fact) + } + + return IfdsResult(pathEdges, resultFacts, reasons = emptyMap(), zeroFact) + } + + override fun submitNewEdge(edge: Edge, reason: Reason) { + val (startVertex, endVertex) = edge + val (endStmt, endFact) = endVertex + + val localPathEdge = EtsIfdsMethodRunner.PathEdge(endStmt.location.index, endFact) + getMethodRunner(startVertex.statement.method).getSourceRunner(startVertex).propagate(localPathEdge) + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsSourceRunner.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsSourceRunner.kt new file mode 100644 index 0000000000..8d3d475f5f --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/ifds/EtsIfdsSourceRunner.kt @@ -0,0 +1,147 @@ +package org.usvm.dataflow.ts.ifds + +import org.jacodb.ets.model.EtsStmt +import org.usvm.dataflow.ifds.Edge +import org.usvm.dataflow.ifds.Vertex +import org.usvm.dataflow.ts.ifds.EtsIfdsMethodRunner.PathEdge +import org.usvm.dataflow.ts.util.EtsTraits + +internal class EtsIfdsSourceRunner( + val traits: EtsTraits, + val methodRunner: EtsIfdsMethodRunner, + val entrypoint: EtsStmt, + val startingFact: Fact, +) { + private var enqueued: Boolean = false + private val pathEdgeQueue: ArrayDeque> = ArrayDeque() + + fun processFacts() { + while (!pathEdgeQueue.isEmpty()) { + val currentEdge = pathEdgeQueue.removeFirst() + tabulationAlgorithmStep(currentEdge) + } + enqueued = false + } + + private val successors = methodRunner.successors + private val stmts = methodRunner.stmts + private val mockStmt = methodRunner.mockStmt + private val flowSpace = methodRunner.flowSpace + val graph = methodRunner.graph + + private val factsAtStmt = Array(stmts.size) { hashSetOf() } + + internal fun propagate(localEdge: PathEdge) { + val (endStmtIndex, endFact) = localEdge + if (factsAtStmt[endStmtIndex].add(endFact)) { + val startVertex = Vertex(mockStmt, startingFact) + val endVertex = Vertex(stmts[endStmtIndex], endFact) + val edge = Edge(startVertex, endVertex) + val events = methodRunner.analyzer.handleNewEdge(edge) + + for (event in events) { + methodRunner.manager.handleEvent(event) + } + + pathEdgeQueue.add(localEdge) + if (!enqueued) { + enqueued = true + methodRunner.enqueue(this) + } + } + } + + private val callerPathEdges = hashSetOf>() + internal val summaryEdges = hashSetOf>() + + private fun tabulationAlgorithmStep( + currentEdge: PathEdge, + ) = with(traits) { + val (currentStmtIndex, currentFact) = currentEdge + val currentStmt = stmts[currentStmtIndex] + + val currentIsCall = getCallExpr(currentStmt) != null + val currentIsExit = methodRunner.isExit[currentStmtIndex] + + if (currentIsCall) { + val callToReturnFlowFunction = flowSpace + .obtainCallToReturnSiteFlowFunction(currentStmt, mockStmt) + + // Propagate through the call-to-return-site edge: + val factsAtReturnSite = callToReturnFlowFunction.compute(currentFact) + for (returnSite in successors[currentStmtIndex]) { + for (returnSiteFact in factsAtReturnSite) { + val edge = PathEdge(returnSite, returnSiteFact) + propagate(edge) + } + } + + for (callee in graph.callees(currentStmt)) { + for (calleeStart in graph.entryPoints(callee)) { + val callToStartFlowFunction = flowSpace.obtainCallToStartFlowFunction(currentStmt, calleeStart) + val factsAtCalleeStart = callToStartFlowFunction.compute(currentFact) + + for (calleeStartFact in factsAtCalleeStart) { + val calleeStartVertex = Vertex(calleeStart, calleeStartFact) + + // Save info about the call for summary edges that will be found later: + val calleeRunner = methodRunner.commonRunner.getMethodRunner(callee) + val currentVertex = Vertex(currentStmt, currentFact) + val startingVertex = Vertex(entrypoint, startingFact) + val callerEdge = Edge(startingVertex, currentVertex) + for (calleeSourceRunner in calleeRunner.getSourceRunners(startingFact)) { + calleeSourceRunner.callerPathEdges.add(callerEdge) + } + + // Initialize analysis of callee: + val summaryEdges = calleeRunner.propagateStartingFact(calleeStartFact) + + // Handle already-found summary edges: + for (exitVertex in summaryEdges) { + val summaryEdge = Edge(calleeStartVertex, exitVertex) + methodRunner.handleSummaryEdgeInCaller(callerEdge, summaryEdge) + } + } + } + } + } else { + if (currentIsExit) { + val startVertex = Vertex(entrypoint, startingFact) + val currentVertex = Vertex(currentStmt, currentFact) + + // Propagate through the summary edge: + for (callerPathEdge in callerPathEdges) { + val summaryEdge = Edge(startVertex, currentVertex) + val caller = callerPathEdge.from.statement.method + val callerRunner = methodRunner.commonRunner.getMethodRunner(caller) + callerRunner.handleSummaryEdgeInCaller(currentEdge = callerPathEdge, summaryEdge = summaryEdge) + } + + // Add new summary edge: + summaryEdges.add(currentVertex) + } + + // Simple (sequential) propagation to the next instruction: + val factsAtNext = flowSpace + .obtainSequentFlowFunction(currentStmt, mockStmt) + .compute(currentFact) + for (next in successors[currentStmtIndex]) { + for (nextFact in factsAtNext) { + val edge = PathEdge(next, nextFact) + propagate(edge) + } + } + } + } + + internal fun getPathEdges(): List> { + val startVertex = Vertex(entrypoint, startingFact) + return factsAtStmt.flatMapIndexed { index, facts -> + val stmt = stmts[index] + facts.map { + val endVertex = Vertex(stmt, it) + Edge(startVertex, endVertex) + } + } + } +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt index 18aa7f6da8..040ce06d2f 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt @@ -34,17 +34,13 @@ class ForwardAnalyzer( error("No cross unit calls") } - private val liveVariablesCache = hashMapOf() - private fun liveVariables(method: EtsMethod): LiveVariables = - liveVariablesCache.computeIfAbsent(method) { - if (doLiveVariablesAnalysis) LiveVariables.from(method) else AlwaysAlive - } - private fun variableIsDying(fact: ForwardTypeDomainFact, stmt: EtsStmt): Boolean { if (fact !is ForwardTypeDomainFact.TypedVariable) return false - val base = fact.variable.base - if (base !is AccessPathBase.Local) return false - return !liveVariables(stmt.method).isAliveAt(base.name, stmt) + return when (val base = fact.variable.base) { + is AccessPathBase.Local -> !flowFunctions.liveVariables(stmt.method).isAliveAt(base.name, stmt) + is AccessPathBase.Arg -> !flowFunctions.liveVariables(stmt.method).isAliveAt("arg(${base.index})", stmt) + else -> false + } } override fun handleNewEdge(edge: Edge): List { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt index 322d37f046..8bdfadbb06 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt @@ -66,7 +66,7 @@ class ForwardFlowFunctions( } private val liveVariablesCache = hashMapOf() - private fun liveVariables(method: EtsMethod) = + internal fun liveVariables(method: EtsMethod) = liveVariablesCache.computeIfAbsent(method) { if (doLiveVariablesAnalysis) { LiveVariables.from(method) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt index 2b9a715a65..4fa0668dd5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt @@ -13,6 +13,7 @@ import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsInstanceOfExpr import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsThrowStmt @@ -24,7 +25,7 @@ interface LiveVariables { fun isAliveAt(local: String, stmt: EtsStmt): Boolean companion object { - private const val THRESHOLD: Int = 20 + private const val THRESHOLD: Int = 10 fun from(method: EtsMethod): LiveVariables = if (method.cfg.stmts.size > THRESHOLD) LiveVariablesImpl(method) else AlwaysAlive @@ -51,6 +52,7 @@ class LiveVariablesImpl( private fun EtsValue.used(): List = when (this) { is EtsLocal -> listOf(name) + is EtsParameterRef -> listOf("arg($index)") is EtsInstanceFieldRef -> listOf(instance.name) is EtsArrayAccess -> array.used() + index.used() else -> emptyList() @@ -83,13 +85,9 @@ class LiveVariablesImpl( } aliveAtStmt = Array(method.cfg.stmts.size) { emptyBitSet() } - - val queue = method.cfg.stmts.toHashSet() - while (queue.isNotEmpty()) { - val stmt = queue.first() - queue.remove(stmt) - - val aliveHere = emptyBitSet().apply { + val usedAtStmt = Array(method.cfg.stmts.size) { ip -> + val stmt = method.cfg.stmts[ip] + emptyBitSet().apply { val usedLocals = when (stmt) { is EtsAssignStmt -> stmt.lhv.used() + stmt.rhv.used() is EtsCallStmt -> stmt.expr.used() @@ -101,6 +99,13 @@ class LiveVariablesImpl( usedLocals.mapNotNull { indexOfName[it] }.forEach { set(it) } } + } + + val queue = ArrayDeque(method.cfg.stmts) + while (queue.isNotEmpty()) { + val stmt = queue.removeFirst() + + val aliveHere = usedAtStmt[stmt.location.index] for (succ in method.cfg.successors(stmt)) { val transferFromSucc = aliveAtStmt[succ.location.index].copy() diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index d746b2525e..48b3de46c5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -28,10 +28,9 @@ import org.usvm.dataflow.ifds.ControlEvent import org.usvm.dataflow.ifds.Edge import org.usvm.dataflow.ifds.Manager import org.usvm.dataflow.ifds.QueueEmptinessChanged -import org.usvm.dataflow.ifds.SingletonUnit -import org.usvm.dataflow.ifds.UniRunner import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.graph.reversed +import org.usvm.dataflow.ts.ifds.EtsIfdsRunner import org.usvm.dataflow.ts.infer.EtsTypeFact.Companion.allStringProperties import org.usvm.dataflow.ts.util.EtsTraits import org.usvm.dataflow.ts.util.getRealLocals @@ -102,8 +101,8 @@ class TypeInferenceManager( createResultsFromSummaries(updatedTypeScheme, doInferAllLocals) } - lateinit var backwardRunner: UniRunner - lateinit var forwardRunner: UniRunner + lateinit var backwardRunner: EtsIfdsRunner + lateinit var forwardRunner: EtsIfdsRunner private suspend fun collectSummaries( startMethods: List, @@ -113,16 +112,15 @@ class TypeInferenceManager( logger.info { "Preparing backward analysis" } val backwardGraph = graph.reversed val backwardAnalyzer = BackwardAnalyzer(backwardGraph, savedTypes, ::methodDominators, doAddKnownTypes) - val backwardRunner = UniRunner( - traits = traits, - manager = this@TypeInferenceManager, + + val backwardRunner = EtsIfdsRunner( graph = backwardGraph, analyzer = backwardAnalyzer, - unitResolver = { SingletonUnit }, - unit = SingletonUnit, + traits = traits, + manager = this, zeroFact = BackwardTypeDomainFact.Zero, - storeReasons = false, ) + this@TypeInferenceManager.backwardRunner = backwardRunner val exceptionHandler = CoroutineExceptionHandler { _, exception -> @@ -200,15 +198,12 @@ class TypeInferenceManager( doLiveVariablesAnalysis = true, ) - val forwardRunner = UniRunner( - traits = traits, - manager = this@TypeInferenceManager, + val forwardRunner = EtsIfdsRunner( graph = forwardGraph, analyzer = forwardAnalyzer, - unitResolver = { SingletonUnit }, - unit = SingletonUnit, + traits = traits, + manager = this, zeroFact = ForwardTypeDomainFact.Zero, - storeReasons = false, ) this@TypeInferenceManager.forwardRunner = forwardRunner @@ -372,20 +367,20 @@ class TypeInferenceManager( } val typeFactsOnThisMethods = forwardSummariesByClass[cls.signature].orEmpty() + .asSequence() .filter { (method, _) -> method.name != INSTANCE_INIT_METHOD_NAME } .flatMap { (_, summaries) -> summaries.asSequence() } .mapNotNull { it.initialFact as? ForwardTypeDomainFact.TypedVariable } .filter { it.variable.base is AccessPathBase.This } - .distinct() - .toList() + .constrainOnce() val typeFactsOnThisCtor = forwardSummariesByClass[cls.signature].orEmpty() + .asSequence() .filter { (method, _) -> method.name == CONSTRUCTOR_NAME || method.name == INSTANCE_INIT_METHOD_NAME } .flatMap { (_, summaries) -> summaries.asSequence() } .mapNotNull { it.exitFact as? ForwardTypeDomainFact.TypedVariable } .filter { it.variable.base is AccessPathBase.This } - .distinct() - .toList() + .constrainOnce() val typeFactsOnThis = (typeFactsOnThisMethods + typeFactsOnThisCtor).distinct() @@ -494,59 +489,67 @@ class TypeInferenceManager( return refinedTypes } + companion object { + private const val REFINEMENT_DEPTH_BOUND = 2 + } + private fun EtsTypeFact.refineProperties( pathFromRootObject: List, typeRefinements: Map, EtsTypeFact>, - ): EtsTypeFact = when (this) { - is EtsTypeFact.NumberEtsTypeFact -> this - is EtsTypeFact.StringEtsTypeFact -> this - is EtsTypeFact.FunctionEtsTypeFact -> this - is EtsTypeFact.AnyEtsTypeFact -> this - is EtsTypeFact.BooleanEtsTypeFact -> this - is EtsTypeFact.NullEtsTypeFact -> this - is EtsTypeFact.UndefinedEtsTypeFact -> this - - is EtsTypeFact.UnknownEtsTypeFact -> { - // logger.warn { "Unknown type after forward analysis" } - EtsTypeFact.AnyEtsTypeFact - } + ): EtsTypeFact { + if (pathFromRootObject.size >= REFINEMENT_DEPTH_BOUND) return this - is EtsTypeFact.ArrayEtsTypeFact -> { - // TODO: array types - // logger.warn { "TODO: Array type $this" } + return when (this) { + is EtsTypeFact.NumberEtsTypeFact -> this + is EtsTypeFact.StringEtsTypeFact -> this + is EtsTypeFact.FunctionEtsTypeFact -> this + is EtsTypeFact.AnyEtsTypeFact -> this + is EtsTypeFact.BooleanEtsTypeFact -> this + is EtsTypeFact.NullEtsTypeFact -> this + is EtsTypeFact.UndefinedEtsTypeFact -> this - val elementPath = pathFromRootObject + ElementAccessor - val refinedElemType = typeRefinements[elementPath]?.let { - typeProcessor.intersect(it, elementType) - } ?: elementType // TODO: consider throwing an exception - val elemType = refinedElemType.refineProperties(elementPath, typeRefinements) + is EtsTypeFact.UnknownEtsTypeFact -> { + // logger.warn { "Unknown type after forward analysis" } + EtsTypeFact.AnyEtsTypeFact + } - EtsTypeFact.ArrayEtsTypeFact(elemType) - } + is EtsTypeFact.ArrayEtsTypeFact -> { + // TODO: array types + // logger.warn { "TODO: Array type $this" } - is EtsTypeFact.ObjectEtsTypeFact -> refineProperties(pathFromRootObject, typeRefinements) + val elementPath = pathFromRootObject + ElementAccessor + val refinedElemType = typeRefinements[elementPath]?.let { + typeProcessor.intersect(it, elementType) + } ?: elementType // TODO: consider throwing an exception + val elemType = refinedElemType.refineProperties(elementPath, typeRefinements) - is EtsTypeFact.UnionEtsTypeFact -> EtsTypeFact.mkUnionType( - types.mapTo(hashSetOf()) { - it.refineProperties( - pathFromRootObject, - typeRefinements, - ) + EtsTypeFact.ArrayEtsTypeFact(elemType) } - ) - is EtsTypeFact.IntersectionEtsTypeFact -> EtsTypeFact.mkIntersectionType( - types.mapTo(hashSetOf()) { - it.refineProperties( - pathFromRootObject, - typeRefinements, - ) - } - ) + is EtsTypeFact.ObjectEtsTypeFact -> refineProperties(pathFromRootObject, typeRefinements) - is EtsTypeFact.GuardedTypeFact -> type - .refineProperties(pathFromRootObject, typeRefinements) - .withGuard(guard, guardNegated) + is EtsTypeFact.UnionEtsTypeFact -> EtsTypeFact.mkUnionType( + types.mapTo(hashSetOf()) { + it.refineProperties( + pathFromRootObject, + typeRefinements, + ) + } + ) + + is EtsTypeFact.IntersectionEtsTypeFact -> EtsTypeFact.mkIntersectionType( + types.mapTo(hashSetOf()) { + it.refineProperties( + pathFromRootObject, + typeRefinements, + ) + } + ) + + is EtsTypeFact.GuardedTypeFact -> type + .refineProperties(pathFromRootObject, typeRefinements) + .withGuard(guard, guardNegated) + } } private fun EtsTypeFact.ObjectEtsTypeFact.refineProperties( diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt index 255e98ef9b..3e0ca9c3db 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt @@ -77,8 +77,8 @@ class EtsTypeResolverPerformanceTest { ) val reportStr = buildString { - appendLine("|project|min time|max time|avg time|median time|%|") - appendLine("|:--|:--|:--|:--|:--|:--|") + appendLine("|project|stmts|min time|max time|avg time|median time|%|") + appendLine("|:--|:--|:--|:--|:--|:--|:--|") reports.forEach { appendLine(it.dumpToString()) } diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt index 595c52d347..292694b377 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt @@ -22,14 +22,10 @@ import org.usvm.dataflow.ts.infer.EntryPointsProcessor import org.usvm.dataflow.ts.infer.TypeGuesser import org.usvm.dataflow.ts.infer.TypeInferenceManager import org.usvm.dataflow.ts.infer.TypeInferenceResult -import org.usvm.dataflow.ts.infer.annotation.annotateWithTypes import org.usvm.dataflow.ts.infer.createApplicationGraph -import org.usvm.dataflow.ts.infer.verify.VerificationResult -import org.usvm.dataflow.ts.infer.verify.verify import org.usvm.dataflow.ts.util.EtsTraits import kotlin.io.path.Path import kotlin.io.path.exists -import kotlin.test.assertTrue object AbcProjects { private const val yourPrefixForTestFolders = "REPLACE_ME" @@ -53,14 +49,7 @@ object AbcProjects { return result to statistics } - fun inferTypes(scene: EtsScene): TypeInferenceResult { - val abcScene = when (val result = verify(scene)) { - is VerificationResult.Success -> scene - is VerificationResult.Fail -> scene.annotateWithTypes(result.erasureScheme) - } - - assertTrue(verify(abcScene) is VerificationResult.Success) - + fun inferTypes(abcScene: EtsScene): TypeInferenceResult { val graphAbc = createApplicationGraph(abcScene) val guesser = TypeGuesser(abcScene) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt index 37a73c3df9..b01781c046 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt @@ -23,6 +23,7 @@ import kotlin.time.measureTimedValue data class PerformanceReport( val projectId: String, + val totalStmts: Int, val maxTime: Duration, val avgTime: Duration, val medianTime: Duration, @@ -31,11 +32,12 @@ data class PerformanceReport( ) { fun dumpToString(): String = listOf( projectId, - minTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - maxTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - avgTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - medianTime.toString(unit = DurationUnit.SECONDS, decimals = 3), - improvement.toBigDecimal().setScale(4, RoundingMode.HALF_UP).toDouble() + totalStmts, + minTime.toString(unit = DurationUnit.SECONDS, decimals = 1), + maxTime.toString(unit = DurationUnit.SECONDS, decimals = 1), + avgTime.toString(unit = DurationUnit.SECONDS, decimals = 1), + medianTime.toString(unit = DurationUnit.SECONDS, decimals = 1), + improvement.toBigDecimal().setScale(1, RoundingMode.HALF_UP).toDouble() ).joinToString( separator = "|", prefix = "|", @@ -63,8 +65,13 @@ fun generateReportForProject( val improvement = results.map { it.second }.distinct().first() val totalTime = times.reduce { acc, duration -> acc + duration } + val totalStmts = abcScene.projectClasses + .flatMap { it.methods } + .sumOf { it.cfg.stmts.size } + return PerformanceReport( projectId = projectId, + totalStmts = totalStmts, minTime = times.min(), maxTime = times.max(), avgTime = totalTime / runIterationsCount,