diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 07e49ec6e2..b430dda8f3 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-06-16" + BRANCH="neo/2025-06-24" 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/build.gradle.kts b/usvm-ts-dataflow/build.gradle.kts index fb819699d4..af70818e26 100644 --- a/usvm-ts-dataflow/build.gradle.kts +++ b/usvm-ts-dataflow/build.gradle.kts @@ -21,6 +21,7 @@ dependencies { implementation(Libs.kotlinx_collections) implementation(Libs.kotlinx_serialization_json) implementation(Libs.clikt) + runtimeOnly(Libs.logback) testImplementation(Libs.mockk) testImplementation(Libs.junit_jupiter_params) @@ -129,5 +130,8 @@ tasks.shadowJar { // Provider com.github.ajalt.mordant.terminal.terminalinterface.jna.TerminalInterfaceProviderJna not found // ``` exclude(dependency("com.github.ajalt.mordant:.*:.*")) + + // Keep the logback in shadow jar: + exclude(dependency("ch.qos.logback:logback-classic:.*")) } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt index f816ae35c5..b8da9e06f3 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt @@ -2,8 +2,6 @@ package org.usvm.dataflow.ts.infer import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.model.EtsType -import org.jacodb.impl.cfg.graphs.GraphDominators import org.usvm.dataflow.ifds.Analyzer import org.usvm.dataflow.ifds.Edge import org.usvm.dataflow.ifds.Vertex @@ -11,12 +9,10 @@ import org.usvm.dataflow.ts.graph.EtsApplicationGraph class BackwardAnalyzer( val graph: EtsApplicationGraph, - savedTypes: MutableMap>, - dominators: (EtsMethod) -> GraphDominators, doAddKnownTypes: Boolean = true, ) : Analyzer { - override val flowFunctions = BackwardFlowFunctions(graph, dominators, savedTypes, doAddKnownTypes) + override val flowFunctions = BackwardFlowFunctions(doAddKnownTypes) override fun handleCrossUnitCall( caller: Vertex, @@ -27,7 +23,7 @@ class BackwardAnalyzer( override fun handleNewEdge(edge: Edge): List { val (startVertex, currentVertex) = edge - val (current, currentFact) = currentVertex + val (current, _) = currentVertex val method = graph.methodOf(current) val currentIsExit = current in graph.exitPoints(method) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt index b2f331a8ae..221b4318eb 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt @@ -1,55 +1,46 @@ +/* + * Copyright 2022 UnitTestBot contributors (utbot.org) + *

+ * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + *

+ * http://www.apache.org/licenses/LICENSE-2.0 + *

+ * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + package org.usvm.dataflow.ts.infer -import mu.KotlinLogging -import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAddExpr import org.jacodb.ets.model.EtsAssignStmt -import org.jacodb.ets.model.EtsCastExpr -import org.jacodb.ets.model.EtsEntity -import org.jacodb.ets.model.EtsEqExpr -import org.jacodb.ets.model.EtsFieldRef -import org.jacodb.ets.model.EtsIfStmt -import org.jacodb.ets.model.EtsInExpr +import org.jacodb.ets.model.EtsBinaryExpr import org.jacodb.ets.model.EtsInstanceCallExpr -import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsNewExpr -import org.jacodb.ets.model.EtsNumberConstant -import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.model.EtsStringConstant -import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsThrowStmt -import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.callExpr -import org.jacodb.impl.cfg.graphs.GraphDominators import org.usvm.dataflow.ifds.FlowFunction import org.usvm.dataflow.ifds.FlowFunctions -import org.usvm.dataflow.ts.graph.EtsApplicationGraph -import org.usvm.dataflow.ts.infer.BackwardTypeDomainFact.TypedVariable import org.usvm.dataflow.ts.infer.BackwardTypeDomainFact.Zero +import org.usvm.dataflow.ts.infer.BackwardTypeDomainFact.TypedVariable import org.usvm.dataflow.ts.util.fixAnyToUnknown -import org.usvm.util.Maybe - -private val logger = KotlinLogging.logger {} class BackwardFlowFunctions( - val graph: EtsApplicationGraph, - val dominators: (EtsMethod) -> GraphDominators, - val savedTypes: MutableMap>, - val doAddKnownTypes: Boolean = true, + val doAddKnownTypes: Boolean, ) : FlowFunctions { + private val liveVariablesCache = hashMapOf() + internal fun liveVariables(method: EtsMethod) = + liveVariablesCache.computeIfAbsent(method) { + LiveVariables.from(method) + } - private val typeProcessor = TypeFactProcessor(graph.cp) - - // private val aliasesCache: MutableMap>> = hashMapOf() - // - // private fun getAliases(method: EtsMethod): Map> { - // return aliasesCache.computeIfAbsent(method) { computeAliases(method) } - // } - - override fun obtainPossibleStartFacts(method: EtsMethod) = listOf(Zero) + override fun obtainPossibleStartFacts(method: EtsMethod): Collection = listOf(Zero) override fun obtainSequentFlowFunction( current: EtsStmt, @@ -62,455 +53,204 @@ class BackwardFlowFunctions( return@FlowFunction listOf(fact) } } + val liveVars = liveVariables(current.method) when (fact) { Zero -> sequentZero(current) - is TypedVariable -> sequent(current, fact).myFilter() - } - } - - private fun TypedVariable.withTypeGuards(current: EtsStmt): TypedVariable { - val dominators = dominators(current.method).dominators(current).asReversed() - - var result = this - - for (stmt in dominators.filterIsInstance()) { - val (guardedVariable, typeGuard) = resolveTypeGuard(stmt) ?: continue - - if (guardedVariable != result.variable) continue - - val branches = graph.predecessors(stmt).toList() // graph is reversed - check(branches.size == 2) { "Unexpected IF branches: $branches" } - - val (falseBranch, trueBranch) = branches - - val isTrueStatement = current.isReachableFrom(trueBranch) - val isFalseStatement = current.isReachableFrom(falseBranch) - - if (isTrueStatement && !isFalseStatement) { - val type = result.type.withGuard(typeGuard, guardNegated = false) - result = TypedVariable(result.variable, type) - } - - if (!isTrueStatement && isFalseStatement) { - val type = result.type.withGuard(typeGuard, guardNegated = true) - result = TypedVariable(result.variable, type) - } + is TypedVariable -> sequentTypedVariable(current, fact).filter { + when (val base = it.variable.base) { + is AccessPathBase.Local -> liveVars.isAliveAt(base.name, current) + else -> true + } + }.myFilter() } - - return result } - private fun resolveTypeGuard(branch: EtsIfStmt): Pair? { - val condition = branch.condition as? EtsEqExpr ?: return null + companion object { + private fun AccessPath?.isBase(): Boolean = + this != null&& base !is AccessPathBase.Const && accesses.isEmpty() - if (condition.right == EtsNumberConstant(0.0)) { - return resolveTypeGuard(condition.left, branch) - } + private fun AccessPath?.isField(): Boolean = + this != null && accesses.size == 1 - return null + private fun AccessPath?.isConst(): Boolean = + this != null && base is AccessPathBase.Const && accesses.isEmpty() } - private fun resolveTypeGuard( - value: EtsEntity, - stmt: EtsStmt, - ): Pair? { - val valueAssignment = findAssignment(value, stmt) ?: return null - - return when (val rhv = valueAssignment.rhv) { - is EtsLocal, is EtsThis, is EtsParameterRef, is EtsFieldRef, is EtsArrayAccess -> { - resolveTypeGuard(rhv, valueAssignment) - } - - is EtsInExpr -> { - resolveTypeGuardFromIn(rhv.left, rhv.right) + private fun sequentZero(current: EtsStmt): List { + if (current is EtsReturnStmt) { + // Case `return x` + // ∅ |= x:unknown + val returnValue = current.returnValue ?: return listOf(Zero) + val type = if (doAddKnownTypes) { + val knownType = returnValue.tryGetKnownType(current.method) + EtsTypeFact.from(knownType).fixAnyToUnknown() + } else { + EtsTypeFact.UnknownEtsTypeFact } - - else -> null - } - } - - private fun findAssignment(value: EtsEntity, stmt: EtsStmt): EtsAssignStmt? { - val cache = hashMapOf>() - findAssignment(value, stmt, cache) - val maybeValue = cache.getValue(stmt) - - return if (maybeValue.isNone) null else maybeValue.getOrThrow() - } - - private fun findAssignment( - value: EtsEntity, - stmt: EtsStmt, - cache: MutableMap>, - ) { - if (stmt in cache) return - - if (stmt is EtsAssignStmt && stmt.lhv == value) { - cache[stmt] = Maybe.some(stmt) - return + return listOf(Zero, TypedVariable(returnValue.toPath(), type)) } - // val predecessors = graph.successors(stmt) // graph is reversed - // val predecessors = dominators(stmt.method).dominators(stmt) - stmt - val predecessors = dominators(stmt.method).dominators(stmt).toSet().intersect(graph.successors(stmt).toSet()) - predecessors.forEach { findAssignment(value, it, cache) } - - val predecessorValues = predecessors.map { cache.getValue(it) } - if (predecessorValues.any { it.isNone }) { - cache[stmt] = Maybe.none() - return - } - - val values = predecessorValues.map { it.getOrThrow() }.toHashSet() - if (values.size == 1) { - cache[stmt] = Maybe.some(values.single()) - return - } - - cache[stmt] = Maybe.none() - } - - private fun resolveTypeGuardFromIn( - left: EtsEntity, - right: EtsEntity, - ): Pair? { - if (left !is EtsStringConstant) return null - - check(right is EtsValue) - val base = right.toBase() - val type = EtsTypeFact.ObjectEtsTypeFact( - cls = null, - properties = mapOf(left.value to EtsTypeFact.UnknownEtsTypeFact) - ) - return base to type - } - - private fun EtsStmt.isReachableFrom(stmt: EtsStmt): Boolean { - val visited = hashSetOf() - val queue = mutableListOf(stmt) - - while (queue.isNotEmpty()) { - val s = queue.removeLast() - if (this == s) return true - - if (!visited.add(s)) continue + if (current !is EtsAssignStmt) return listOf(Zero) - val successors = graph.predecessors(s) // graph is reversed - queue.addAll(successors) - } - - return false - } + val lhv = current.lhv.toPath() + val rhv = current.rhv.toPathOrNull() - private fun sequentZero(current: EtsStmt): List { val result = mutableListOf(Zero) - // Case `return x` - // ∅ |= x:unknown - if (current is EtsReturnStmt) { - val returnValue = current.returnValue - if (returnValue != null) { - val variable = returnValue.toBase() + // When RHS is not const-like, handle possible new facts for RHV: + if (rhv != null) { + if (rhv.accesses.isEmpty()) { + // Case `x... := y` + // ∅ |= y:unknown val type = if (doAddKnownTypes) { - val knownType = returnValue.tryGetKnownType(current.method) + val knownType = current.rhv.tryGetKnownType(current.method) EtsTypeFact.from(knownType).fixAnyToUnknown() } else { EtsTypeFact.UnknownEtsTypeFact } - result += TypedVariable(variable, type) + result += TypedVariable(lhv, type) + result += TypedVariable(rhv, type) + } else { + // Case `x := y.f` OR `x := y[i]` + check(rhv.accesses.size == 1) + result += TypedVariable(lhv, EtsTypeFact.UnknownEtsTypeFact) + result += TypedVariable(rhv, EtsTypeFact.UnknownEtsTypeFact) } - } - - if (current is EtsAssignStmt) { - val rhv = when (val r = current.rhv) { - is EtsLocal -> r.toPath() - is EtsThis -> r.toPath() - is EtsParameterRef -> r.toPath() - is EtsFieldRef -> r.toPath() - is EtsArrayAccess -> r.toPath() - else -> { - // logger.info { "TODO backward assign zero: $current" } - null + } else { + when (val rhv = current.rhv) { + // x := y + z + is EtsAddExpr -> { + val numberOrString = EtsTypeFact.mkUnionType( + EtsTypeFact.NumberEtsTypeFact, + EtsTypeFact.StringEtsTypeFact, + ) + val y_is_number_or_string = rhv.left.toPathOrNull()?.let { + TypedVariable(it, numberOrString) + } + val z_is_number_or_string = rhv.right.toPathOrNull()?.let { + TypedVariable(it, numberOrString) + } + return listOfNotNull(Zero, y_is_number_or_string, z_is_number_or_string) } - } - // When RHS is not const-like, handle possible new facts for RHV: - if (rhv != null) { - val y = rhv.base - - if (rhv.accesses.isEmpty()) { - // Case `x... := y` - // ∅ |= y:unknown - val type = if (doAddKnownTypes) { - val knownType = current.rhv.tryGetKnownType(current.method) - EtsTypeFact.from(knownType).fixAnyToUnknown() - } else { - EtsTypeFact.UnknownEtsTypeFact + // x := y * z + is EtsBinaryExpr -> { + val y_is_number = rhv.left.toPathOrNull()?.let { + TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) } - result += TypedVariable(y, type) - } else { - // Case `x := y.f` OR `x := y[i]` - - check(rhv.accesses.size == 1) - when (val accessor = rhv.accesses.single()) { - // Case `x := y.f` - // ∅ |= y:{f:unknown} - is FieldAccessor -> { - val type = EtsTypeFact.ObjectEtsTypeFact( - cls = null, - properties = mapOf(accessor.name to EtsTypeFact.UnknownEtsTypeFact) - ) - result += TypedVariable(y, type).withTypeGuards(current) - } - - // Case `x := y[i]` - // ∅ |= y:Array - is ElementAccessor -> { - // Note: ElementAccessor guarantees that `y` is an array, - // since `y[i]` for property access (i.e. access property - // with name "i") is represented via FieldAccessor. - val type = EtsTypeFact.ArrayEtsTypeFact( - elementType = EtsTypeFact.UnknownEtsTypeFact - ) - result += TypedVariable(y, type).withTypeGuards(current) - } + val z_is_number = rhv.right.toPathOrNull()?.let { + TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) } + return listOfNotNull(Zero, y_is_number, z_is_number) } - } - val lhv = current.lhv.toPath() - - // Handle new possible facts for LHS: - if (lhv.accesses.isNotEmpty()) { - // Case `x.f := y` OR `x[i] := y` - val x = lhv.base - - when (val a = lhv.accesses.single()) { - // Case `x.f := y` - // ∅ |= x:{f:unknown} - is FieldAccessor -> { - val type = EtsTypeFact.ObjectEtsTypeFact( - cls = null, - properties = mapOf(a.name to EtsTypeFact.UnknownEtsTypeFact) - ) - result += TypedVariable(x, type).withTypeGuards(current) - } + // x := y.foo(...) (call-to-return) + is EtsInstanceCallExpr -> { + val y_foo_is_function = TypedVariable(rhv.instance.toPath(), EtsTypeFact.FunctionEtsTypeFact) + return listOf(Zero, y_foo_is_function) + } - // Case `x[i] := y` - // ∅ |= x:Array - is ElementAccessor -> { - // Note: ElementAccessor guarantees that `y` is an array, - // since `y[i]` for property access (i.e. access property - // with name "i") is represented via FieldAccessor. - val type = EtsTypeFact.ArrayEtsTypeFact( - elementType = EtsTypeFact.UnknownEtsTypeFact - ) - result += TypedVariable(x, type) - } + else -> { + return listOf(Zero) } } } + // Handle new possible facts for LHS: + if (lhv.accesses.isNotEmpty()) { + result += TypedVariable(lhv, EtsTypeFact.UnknownEtsTypeFact) + } + return result } - private fun sequent( - current: EtsStmt, - fact: TypedVariable, - ): List { - if (current !is EtsAssignStmt) { - return listOf(fact) - } + private fun sequentTypedVariable(current: EtsStmt, fact: TypedVariable): List { + if (current !is EtsAssignStmt) return emptyList() val lhv = current.lhv.toPath() + val rhv = current.rhv.toPathOrNull() - val rhv = when (val r = current.rhv) { - is EtsLocal -> r.toPath() - is EtsThis -> r.toPath() - is EtsParameterRef -> r.toPath() - is EtsFieldRef -> r.toPath() - is EtsArrayAccess -> r.toPath() - is EtsCastExpr -> r.toPath() - is EtsNewExpr -> { - // TODO: what about `x.f := new T()` ? - // `x := new T()` with fact `x:U` => `saved[T] += U` - if (fact.variable == lhv.base) { - savedTypes.getOrPut(r.type) { mutableListOf() }.add(fact.type) - } - return listOf(fact) - } + val result = mutableListOf(fact) - else -> { - // logger.info { "TODO backward assign: $current" } - return listOf(fact) - } + // z: t --> { z: t } + if (!fact.variable.startsWith(lhv)) { + return result } - // Pass-through completely unrelated facts: - if (fact.variable != lhv.base) return listOf(fact) - - // val (preAliases, _) = getAliases(current.method)[current]!! - - if (lhv.accesses.isEmpty() && rhv.accesses.isEmpty()) { - // Case `x := y` - - // x:T |= x:T (keep) + y:T - val y = rhv.base - val newFact = TypedVariable(y, fact.type).withTypeGuards(current) - return listOf(fact, newFact) - - } else if (lhv.accesses.isEmpty()) { - // Case `x := y.f` OR `x := y[i]` - - check(rhv.accesses.size == 1) - when (val a = rhv.accesses.single()) { - // Case `x := y.f` - is FieldAccessor -> { - // // Drop facts containing duplicate fields - // if (fact.type is EtsTypeFact.ObjectEtsTypeFact && a.name in fact.type.properties) { - // // can just drop? - // return listOf(fact) - // } - - // x:T |= x:T (keep) + y:{f:T} + aliases - val result = mutableListOf(fact) - val y = rhv.base - val type = EtsTypeFact.ObjectEtsTypeFact( - cls = null, - properties = mapOf(a.name to fact.type) - ) - result += TypedVariable(y, type).withTypeGuards(current) - // aliases: +|= z:{f:T} - // for (z in preAliases.getAliases(AccessPath(y, emptyList()))) { - // val type2 = unrollAccessorsToTypeFact(z.accesses + a, fact.type) - // result += TypedVariable(z.base, type2).withTypeGuards(current) - // } - return result - } - - // Case `x := y[i]` - is ElementAccessor -> { - // x:T |= x:T (keep) + y:Array - val y = rhv.base - val type = EtsTypeFact.ArrayEtsTypeFact(elementType = fact.type) - // val realType = EtsTypeFact.from(current.rhv.type) - // val type = newType.intersect(realType) ?: run { - // logger.warn { "Empty intersection of fact and real type: $newType & $realType" } - // newType - // } - val newFact = TypedVariable(y, type).withTypeGuards(current) - return listOf(fact, newFact) - } - } - - } else if (rhv.accesses.isEmpty()) { - // Case `x.f := y` OR `x[i] := y` - - check(lhv.accesses.size == 1) - when (val a = lhv.accesses.single()) { - // Case `x.f := y` - is FieldAccessor -> { - val facts = mutableListOf(fact) - - if (fact.type is EtsTypeFact.UnionEtsTypeFact) { - val types = fact.type.types.mapNotNull { - if (it is EtsTypeFact.ObjectEtsTypeFact) { - it.properties[a.name] - } else { - null - } + if (rhv == null) { + when (val rhv = current.rhv) { + // x := y + z (addition operator can be string or numeric, + // then we can infer arguments are numeric when result is numeric) + is EtsAddExpr -> { + // x.*: t --> none + if (fact == TypedVariable(lhv, EtsTypeFact.NumberEtsTypeFact)) { + val y_is_number = rhv.left.toPathOrNull()?.let { + TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) } - if (types.isNotEmpty()) { - // x:T |= x:T (keep) + y:T - val newType = types.reduce { acc, type -> typeProcessor.union(acc, type) } - facts += TypedVariable(rhv.base, newType).withTypeGuards(current) + val z_is_number = rhv.right.toPathOrNull()?.let { + TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) } - return facts + result += listOfNotNull(y_is_number, z_is_number) } + } - if (fact.type is EtsTypeFact.IntersectionEtsTypeFact) { - for (subType in fact.type.types) { - if (subType is EtsTypeFact.ObjectEtsTypeFact) { - val propertyType = subType.properties[a.name] - if (propertyType != null) { - facts += TypedVariable(rhv.base, propertyType).withTypeGuards(current) - } - } - } - return facts - } + // x := y * z (numeric operator) + is EtsBinaryExpr -> { + // x.*: t --> none + } - // Ignore (pass) non-object type facts: - // x:primitive |= x:primitive (pass) - if (fact.type !is EtsTypeFact.ObjectEtsTypeFact) { - return facts - } + // x := y.foo(...) (call-to-return) + is EtsInstanceCallExpr -> { + // x.*: t --> none + } - // x:{f:T} |= x:{f:T} (keep) + y:T - // x:{no f} |= only keep x:{..} - val type = fact.type.properties[a.name] - if (type != null) { - val y = rhv.base - facts += TypedVariable(y, type).withTypeGuards(current) - } - return facts + else -> { + // x.*: t --> none + } + } + } else { + val tail = fact.variable.accesses + + when { + // x := y + lhv.isBase() && rhv.isBase() -> { + // x.*: t --> y.*: t + val y_is_t = TypedVariable(rhv + tail, fact.type) + result += y_is_t } - // Case `x[i] := y` - is ElementAccessor -> { - val facts = mutableListOf(fact) - - if (fact.type is EtsTypeFact.UnionEtsTypeFact) { - val types = fact.type.types.mapNotNull { - if (it is EtsTypeFact.ArrayEtsTypeFact) { - it.elementType - } else { - null - } - } - if (types.isNotEmpty()) { - // x:T |= x:T (keep) + y:T - val newType = types.reduce { acc, type -> typeProcessor.union(acc, type) } - facts += TypedVariable(rhv.base, newType).withTypeGuards(current) - } - return facts - } + // x := y.a + lhv.isBase() && rhv.isField() -> { + // x.*: t --> y.a.*: t + val y_a_is_t = TypedVariable(rhv + tail, fact.type) + result += y_a_is_t + } - if (fact.type is EtsTypeFact.IntersectionEtsTypeFact) { - for (subType in fact.type.types) { - if (subType is EtsTypeFact.ArrayEtsTypeFact) { - val elementType = subType.elementType - facts += TypedVariable(rhv.base, elementType).withTypeGuards(current) - } - } - return facts - } + // x.a = y + lhv.isField() && rhv.isBase() -> { + // x.a.*: t --> y.*: t + check(tail.isNotEmpty()) + val y_is_t = TypedVariable(rhv + tail.drop(1), fact.type) + result += y_is_t + } - // x:Array |= x:Array (pass) - if (fact.type !is EtsTypeFact.ArrayEtsTypeFact) { - return facts - } + // x.* := const + rhv.isConst() -> { + // x.*: t --> none + } - // x:Array |= x:Array (keep) + y:T - val y = rhv.base - val type = fact.type.elementType - facts += TypedVariable(y, type).withTypeGuards(current) - return facts + else -> { + // x.*: t --> none } } - } else { - error("Incorrect 3AC: $current") } - } - private fun EtsTypeFact.ObjectEtsTypeFact.removePropertyType(propertyName: String): Pair { - val propertyType = properties[propertyName] - val updatedThis = EtsTypeFact.ObjectEtsTypeFact(cls, properties - propertyName) - return updatedThis to propertyType + return result } override fun obtainCallToReturnSiteFlowFunction( callStatement: EtsStmt, - returnSite: EtsStmt, + returnSite: EtsStmt ): FlowFunction = FlowFunction { fact -> when (fact) { Zero -> callZero(callStatement) @@ -527,21 +267,15 @@ class BackwardFlowFunctions( if (callExpr is EtsInstanceCallExpr) { val instance = callExpr.instance - val path = instance.toBase() - val objectWithMethod = EtsTypeFact.ObjectEtsTypeFact( - cls = null, - properties = mapOf( - callExpr.callee.name to EtsTypeFact.FunctionEtsTypeFact - ) - ) - result += TypedVariable(path, objectWithMethod) + val methodPath = instance.toPath() + FieldAccessor(callExpr.callee.name) + result += TypedVariable(methodPath, EtsTypeFact.FunctionEtsTypeFact) } if (doAddKnownTypes) { // f(x:T) |= x:T, where T is the type of the argument in f's signature for ((index, arg) in callExpr.args.withIndex()) { val param = callExpr.callee.parameters.getOrNull(index) ?: continue - val base = arg.toBase() + val base = arg.toPath() val type = EtsTypeFact.from(param.type) result += TypedVariable(base, type) } @@ -556,7 +290,7 @@ class BackwardFlowFunctions( ): List { val result = mutableListOf() - val callResult = (callStatement as? EtsAssignStmt)?.lhv?.toBase() + val callResult = (callStatement as? EtsAssignStmt)?.lhv?.toPath() if (callResult != null) { // If fact was for LHS, drop it as overridden if (fact.variable == callResult) return result @@ -581,7 +315,7 @@ class BackwardFlowFunctions( calleeStart: EtsStmt, fact: TypedVariable, ): List { - val callResult = (callStatement as? EtsAssignStmt)?.lhv?.toBase() ?: return emptyList() + val callResult = (callStatement as? EtsAssignStmt)?.lhv?.toPath() ?: return emptyList() if (fact.variable != callResult) return emptyList() @@ -589,7 +323,7 @@ class BackwardFlowFunctions( check(calleeStart is EtsReturnStmt) - val exitValue = calleeStart.returnValue?.toBase() ?: return emptyList() + val exitValue = calleeStart.returnValue?.toPath() ?: return emptyList() return listOf(TypedVariable(exitValue, fact.type)) } @@ -597,7 +331,7 @@ class BackwardFlowFunctions( override fun obtainExitToReturnSiteFlowFunction( callStatement: EtsStmt, returnSite: EtsStmt, - exitStatement: EtsStmt, + exitStatement: EtsStmt ): FlowFunction = FlowFunction { fact -> when (fact) { Zero -> listOf(fact) @@ -611,20 +345,22 @@ class BackwardFlowFunctions( ): List { val callExpr = callStatement.callExpr ?: error("No call") - when (fact.variable) { + val tail = fact.variable.accesses + + when (fact.variable.base) { is AccessPathBase.This -> { if (callExpr !is EtsInstanceCallExpr) { return emptyList() } val instance = callExpr.instance - val instancePath = instance.toBase() - return listOf(TypedVariable(instancePath, fact.type)) + val instancePath = instance.toPath() + return listOf(TypedVariable(instancePath + tail, fact.type)) } is AccessPathBase.Arg -> { - val arg = callExpr.args.getOrNull(fact.variable.index)?.toBase() ?: return emptyList() - return listOf(TypedVariable(arg, fact.type)) + val arg = callExpr.args.getOrNull(fact.variable.base.index)?.toPath() ?: return emptyList() + return listOf(TypedVariable(arg + tail, fact.type)) } else -> return emptyList() @@ -632,23 +368,17 @@ class BackwardFlowFunctions( } } -private const val COMPLEXITY_LIMIT = 5 +private const val ACCESSES_LIMIT = 5 +private const val DUPLICATE_FIELDS_LIMIT = 3 private fun Iterable.myFilter(): List = filter { - if (it.type.complexity() >= COMPLEXITY_LIMIT) { - // logger.warn { "Dropping too complex fact: $it" } + if (it.variable.accesses.size > ACCESSES_LIMIT) { + // logger.warn { "Dropping too long fact: $it" } + return@filter false + } + if (it.variable.accesses.hasDuplicateFields(DUPLICATE_FIELDS_LIMIT)) { + // logger.warn { "Dropping fact with duplicate fields: $it" } return@filter false } true } - -/** - * Complexity of a type fact is the maximum depth of nested types. - */ -private fun EtsTypeFact.complexity(): Int = when (this) { - is EtsTypeFact.ObjectEtsTypeFact -> (properties.values.maxOfOrNull { it.complexity() } ?: 0) + 1 - is EtsTypeFact.ArrayEtsTypeFact -> elementType.complexity() + 1 - is EtsTypeFact.UnionEtsTypeFact -> (types.maxOfOrNull { it.complexity() } ?: 0) + 1 - is EtsTypeFact.IntersectionEtsTypeFact -> (types.maxOfOrNull { it.complexity() } ?: 0) + 1 - else -> 0 -} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeDomainFact.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeDomainFact.kt index 196dea887c..87f764f4f5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeDomainFact.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeDomainFact.kt @@ -3,9 +3,8 @@ package org.usvm.dataflow.ts.infer sealed interface BackwardTypeDomainFact { data object Zero : BackwardTypeDomainFact - // Requirement data class TypedVariable( - val variable: AccessPathBase, + val variable: AccessPath, val type: EtsTypeFact, ) : BackwardTypeDomainFact } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt index ae0dbd9024..3edf1691a2 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt @@ -100,7 +100,7 @@ class TypeGuesser( val resolved = when { suitableTypes.isEmpty() -> error("Should be processed earlier") suitableTypes.size == 1 -> suitableTypes.single() - suitableTypes.size in 2..5 -> EtsTypeFact.mkUnionType(suitableTypes).simplify() + suitableTypes.size in 2..3 -> EtsTypeFact.mkUnionType(suitableTypes).simplify() else -> this } return resolve(this, resolved) 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 48b3de46c5..a1aca05dc1 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 @@ -22,8 +22,6 @@ import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME -import org.jacodb.impl.cfg.graphs.GraphDominators -import org.jacodb.impl.cfg.graphs.findDominators import org.usvm.dataflow.ifds.ControlEvent import org.usvm.dataflow.ifds.Edge import org.usvm.dataflow.ifds.Manager @@ -52,13 +50,6 @@ class TypeInferenceManager( private val backwardSummaries = ConcurrentHashMap>() private val forwardSummaries = ConcurrentHashMap>() - private val methodDominatorsCache = ConcurrentHashMap>() - - private fun methodDominators(method: EtsMethod): GraphDominators = - methodDominatorsCache.computeIfAbsent(method) { - method.flowGraph().findDominators() - } - private val savedTypes: ConcurrentHashMap> = ConcurrentHashMap() private val typeProcessor = TypeFactProcessor(scene = graph.cp) @@ -111,7 +102,7 @@ class TypeInferenceManager( ): Map> { logger.info { "Preparing backward analysis" } val backwardGraph = graph.reversed - val backwardAnalyzer = BackwardAnalyzer(backwardGraph, savedTypes, ::methodDominators, doAddKnownTypes) + val backwardAnalyzer = BackwardAnalyzer(backwardGraph, doAddKnownTypes) val backwardRunner = EtsIfdsRunner( graph = backwardGraph, @@ -390,12 +381,7 @@ class TypeInferenceManager( var refined: EtsTypeFact = combinedBackwardType for ((property, propertyType) in propertyRefinements) { - refined = refined.refineProperty(property, propertyType) ?: this@TypeInferenceManager.run { - logger.warn { - "Empty intersection type: ${refined.toStringLimited()} & ${propertyType.toStringLimited()}" - } - refined - } + refined = refined.refineProperty(property, propertyType) } cls.signature to refined @@ -427,7 +413,7 @@ class TypeInferenceManager( ): Map { val types = summaries .mapNotNull { it.exitFact as? BackwardTypeDomainFact.TypedVariable } - .groupBy({ it.variable }, { it.type }) + .groupBy({ it.variable.base }, { it.variable.accesses to it.type }) .filter { (base, _) -> base is AccessPathBase.This || base is AccessPathBase.Arg @@ -435,14 +421,37 @@ class TypeInferenceManager( || (base is AccessPathBase.Local && base !in getRealLocalsBase(method)) } .mapValues { (_, typeFacts) -> - typeFacts.reduce { acc, typeFact -> - typeProcessor.intersect(acc, typeFact) ?: run { - logger.warn { "Empty intersection type: ${acc.toStringLimited()} & ${typeFact.toStringLimited()}" } - acc + val propertyRefinements = typeFacts + .groupBy({ it.first }, { it.second }) + .mapValues { (accesses, types) -> + val propertyType = types.reduce { acc, t -> + typeProcessor.intersect(acc, t) ?: EtsTypeFact.AnyEtsTypeFact + } + accesses.foldRight(propertyType) { accessor, acc -> + when (accessor) { + is FieldAccessor -> EtsTypeFact.ObjectEtsTypeFact( + cls = null, properties = mapOf(accessor.name to acc) + ) + + is ElementAccessor -> EtsTypeFact.ArrayEtsTypeFact(acc) + } + } } + val refined = if (propertyRefinements.keys.any { it.isNotEmpty() }) { + propertyRefinements + .filterKeys { it.isNotEmpty() } + .values + .reduce { acc, typeFact -> + typeProcessor.intersect(acc, typeFact) ?: run { + logger.warn { "Empty intersection type: ${acc.toStringLimited()} & ${typeFact.toStringLimited()}" } + acc + } + } + } else { + EtsTypeFact.AnyEtsTypeFact } + refined } - return types } @@ -466,11 +475,9 @@ class TypeInferenceManager( val refinedTypes = facts.mapValues { (base, type) -> // TODO: throw an error val typeRefinements = typeFacts[base] ?: return@mapValues type - val propertyRefinements = typeRefinements .groupBy({ it.variable.accesses }, { it.type }) .mapValues { (_, types) -> types.reduce { acc, t -> typeProcessor.union(acc, t) } } - val rootType = propertyRefinements[emptyList()] ?: run { if (propertyRefinements.keys.any { it.isNotEmpty() }) { EtsTypeFact.ObjectEtsTypeFact(null, emptyMap()) @@ -478,14 +485,10 @@ class TypeInferenceManager( EtsTypeFact.AnyEtsTypeFact } } - val refined = rootType.refineProperties(emptyList(), propertyRefinements) - refined } - typeFacts.let {} - return refinedTypes } @@ -556,13 +559,26 @@ class TypeInferenceManager( pathFromRootObject: List, typeRefinements: Map, EtsTypeFact>, ): EtsTypeFact { - val refinedProperties = properties.mapValues { (propertyName, type) -> + val propertiesRefinements = typeRefinements + .filterKeys { it.startsWith(pathFromRootObject) && it.size > pathFromRootObject.size } + .mapKeys { it.key.drop(pathFromRootObject.size).first() } + .filterKeys { it is FieldAccessor } + .mapKeys { (it.key as FieldAccessor).name } + + val properties = this.properties.keys + propertiesRefinements.keys + + val refinedProperties = properties.associateWith { propertyName -> val propertyAccessor = FieldAccessor(propertyName) val propertyPath = pathFromRootObject + propertyAccessor - val refinedType = typeRefinements[propertyPath]?.let { - typeProcessor.intersect(it, type) - } ?: type // TODO: consider throwing an exception - refinedType.refineProperties(propertyPath, typeRefinements) + val type = this.properties[propertyName] + val typeRefinement = typeRefinements[propertyPath] + val refinedType = if (type != null && typeRefinement != null) { + typeProcessor.intersect(typeRefinement, type) + } else { + type ?: typeRefinement + } + refinedType?.refineProperties(propertyPath, typeRefinements) + ?: EtsTypeFact.AnyEtsTypeFact } return EtsTypeFact.ObjectEtsTypeFact(cls, refinedProperties) } @@ -570,20 +586,20 @@ class TypeInferenceManager( private fun EtsTypeFact.refineProperty( property: List, type: EtsTypeFact, - ): EtsTypeFact? = when (this) { - is EtsTypeFact.BasicType -> refineProperty(property, type) + ): EtsTypeFact = when (this) { + is EtsTypeFact.BasicType -> refineProperty(property, type) ?: EtsTypeFact.AnyEtsTypeFact - is EtsTypeFact.GuardedTypeFact -> this.type.refineProperty(property, type)?.withGuard(guard, guardNegated) + is EtsTypeFact.GuardedTypeFact -> this.type.refineProperty(property, type) is EtsTypeFact.IntersectionEtsTypeFact -> EtsTypeFact.mkIntersectionType( types = types.mapTo(hashSetOf()) { // Note: intersection is empty if any of the types is empty - it.refineProperty(property, type) ?: return null + it.refineProperty(property, type) } ) is EtsTypeFact.UnionEtsTypeFact -> EtsTypeFact.mkUnionType( - types = types.mapNotNullTo(hashSetOf()) { + types = types.mapTo(hashSetOf()) { // Note: ignore empty types in the union it.refineProperty(property, type) } @@ -695,7 +711,7 @@ class TypeInferenceManager( when (propertyAccessor) { is FieldAccessor -> { val propertyType = properties[propertyAccessor.name] ?: return this - val refinedProperty = propertyType.refineProperty(property.drop(1), type) ?: return null + val refinedProperty = propertyType.refineProperty(property.drop(1), type) val properties = this.properties + (propertyAccessor.name to refinedProperty) return EtsTypeFact.ObjectEtsTypeFact(cls, properties) } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt index 553a18311b..c62b006dcb 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt @@ -52,6 +52,7 @@ import org.jacodb.ets.model.EtsLiteralType import org.jacodb.ets.model.EtsNeverType import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsRawType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsType @@ -64,6 +65,10 @@ import org.jacodb.ets.model.EtsVoidType fun EtsType.toDto(): TypeDto = accept(EtsTypeToDto) private object EtsTypeToDto : EtsType.Visitor { + override fun visit(type: EtsRawType): TypeDto { + return UnknownTypeDto + } + override fun visit(type: EtsAnyType): TypeDto { return AnyTypeDto } diff --git a/usvm-ts-dataflow/src/main/resources/logback.xml b/usvm-ts-dataflow/src/main/resources/logback.xml index 7fd7cda00d..40d03b09a6 100644 --- a/usvm-ts-dataflow/src/main/resources/logback.xml +++ b/usvm-ts-dataflow/src/main/resources/logback.xml @@ -5,7 +5,7 @@ - + diff --git a/usvm-ts-dataflow/src/test/resources/ts/testcases.ts b/usvm-ts-dataflow/src/test/resources/ts/testcases.ts index 9927bf0c74..8f070a2223 100644 --- a/usvm-ts-dataflow/src/test/resources/ts/testcases.ts +++ b/usvm-ts-dataflow/src/test/resources/ts/testcases.ts @@ -30,7 +30,7 @@ class CaseAssignFieldToLocal1 { // Case `x := y.f` class CaseAssignFieldToLocal2 { entrypoint() { - let y = {f: 42}; // y: { f: number } + let y = { f: 42 }; // y: { f: number } let x = y.f; // x: number this.infer(x); } @@ -65,22 +65,22 @@ class CaseAssignFieldToSelf { } infer(a: any) { - const EXPECTED_ARG_0 = "Object { f: any }" + const EXPECTED_ARG_0 = "Object { f: any }"; } } // Case `x.f := x` -class CaseAssignSelfToField { - entrypoint(a: any) { - let x = { f: a }; // x: { f: any } - x.f = x; // x: { f: any } - this.infer(x); - } - - infer(a: any) { - const EXPECTED_ARG_0 = "Object { f: any }" - } -} +// class CaseAssignSelfToField { +// entrypoint(a: any) { +// let x = { f: a }; // x: { f: any } +// x.f = x; // x: { f: any } +// this.infer(x); +// } +// +// infer(a: any) { +// const EXPECTED_ARG_0 = "Object { f: any }" +// } +// } // ---------------------------------------- @@ -581,25 +581,25 @@ class CaseReturnNumber { // ---------------------------------------- - // Case `return arg` - class CaseReturnArgumentNumber { - entrypoint() { - let x = 94; // x: number - this.infer(x); - } +// Case `return arg` +class CaseReturnArgumentNumber { + entrypoint() { + let x = 94; // x: number + this.infer(x); + } - infer(a: any): any { - const EXPECTED_RETURN = "number"; - return a; - } - } + infer(a: any): any { + const EXPECTED_RETURN = "number"; + return a; + } +} // ---------------------------------------- // Case `return obj` class CaseReturnObject { entrypoint() { - this.infer(); + this.infer(); } infer(): any { @@ -795,7 +795,19 @@ class CaseNew { } infer(a: any): any { - const EXPECTED_ARG_0 = "MyType { f: number }" + const EXPECTED_ARG_0 = "MyType { f: number }"; + } +} + +class CaseNew2 { + entrypoint() { + let x = new Something(); // unresolved + console.log(x.foo); + this.infer(x); + } + + infer(a: any): any { + const EXPECTED_ARG_0 = "Something { foo: any }"; } } @@ -929,7 +941,7 @@ class CaseAliasChain1 { } infer(a: any): any { - const EXPECTED_ARG_0 = "Object { f: Object { g: number } }" + const EXPECTED_ARG_0 = "Object { f: Object { g: number } }"; } } @@ -986,7 +998,7 @@ class CaseFindAssignmentAfterLoop { x.push(42); } - this.infer(x) + this.infer(x); } infer(a: any) {