From 844dcc8d20f8bfc9119657af725acc1e29b1106c Mon Sep 17 00:00:00 2001 From: MForest7 Date: Wed, 28 May 2025 18:40:02 +0300 Subject: [PATCH 1/7] replaced access path base with access path in backward dataflow domain --- .../usvm/dataflow/ts/infer/AnalyzerEvent.kt | 4 +- .../dataflow/ts/infer/BackwardAnalyzer.kt | 10 +- .../ts/infer/BackwardPathFlowFunctions.kt | 372 ++++++++++++++++++ .../usvm/dataflow/ts/infer/TypeDomainFact.kt | 9 + .../org/usvm/dataflow/ts/infer/TypeGuesser.kt | 2 +- .../dataflow/ts/infer/TypeInferenceManager.kt | 88 +++-- .../src/test/resources/ts/testcases.ts | 22 +- 7 files changed, 466 insertions(+), 41 deletions(-) create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardPathFlowFunctions.kt diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt index 33d3a6471f..3d636d3b4d 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt @@ -17,8 +17,8 @@ data class ForwardSummaryAnalyzerEvent( data class BackwardSummaryAnalyzerEvent( val method: EtsMethod, - val initialVertex: Vertex, - val exitVertex: Vertex, + val initialVertex: Vertex, + val exitVertex: Vertex, ) : AnalyzerEvent { val initialFact get() = initialVertex.fact val exitFact get() = exitVertex.fact 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..15c83ddeb4 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 @@ -14,18 +14,18 @@ class BackwardAnalyzer( savedTypes: MutableMap>, dominators: (EtsMethod) -> GraphDominators, doAddKnownTypes: Boolean = true, -) : Analyzer { +) : Analyzer { - override val flowFunctions = BackwardFlowFunctions(graph, dominators, savedTypes, doAddKnownTypes) + override val flowFunctions = BackwardPathFlowFunctions(doAddKnownTypes) override fun handleCrossUnitCall( - caller: Vertex, - callee: Vertex, + caller: Vertex, + callee: Vertex, ): List { error("No cross unit calls") } - override fun handleNewEdge(edge: Edge): List { + override fun handleNewEdge(edge: Edge): List { val (startVertex, currentVertex) = edge val (current, currentFact) = currentVertex diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardPathFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardPathFlowFunctions.kt new file mode 100644 index 0000000000..9e5a4f4039 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardPathFlowFunctions.kt @@ -0,0 +1,372 @@ +/* + * 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 org.jacodb.ets.model.EtsAddExpr +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBinaryExpr +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.utils.callExpr +import org.usvm.dataflow.ifds.FlowFunction +import org.usvm.dataflow.ifds.FlowFunctions +import org.usvm.dataflow.ts.infer.BackwardPathTypeDomainFact.Zero +import org.usvm.dataflow.ts.infer.BackwardPathTypeDomainFact.TypedVariable +import org.usvm.dataflow.ts.util.fixAnyToUnknown + +class BackwardPathFlowFunctions( + val doAddKnownTypes: Boolean, +) : FlowFunctions { + override fun obtainPossibleStartFacts(method: EtsMethod): Collection = listOf(Zero) + + override fun obtainSequentFlowFunction( + current: EtsStmt, + next: EtsStmt, + ): FlowFunction = FlowFunction { fact -> + if (current is EtsAssignStmt) { + val lhvPath = current.lhv.toPathOrNull() + val rhvPath = current.rhv.toPathOrNull() + if (lhvPath != null && rhvPath != null && lhvPath == rhvPath) { + return@FlowFunction listOf(fact) + } + } + when (fact) { + Zero -> sequentZero(current) + is TypedVariable -> sequentTypedVariable(current, fact).myFilter() + } + } + + companion object { + private fun AccessPath?.isBase(): Boolean = + this != null&& base !is AccessPathBase.Const && accesses.isEmpty() + + private fun AccessPath?.isField(): Boolean = + this != null && accesses.size == 1 + + private fun AccessPath?.isConst(): Boolean = + this != null && base is AccessPathBase.Const && accesses.isEmpty() + } + + 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 + } + return listOf(Zero, TypedVariable(returnValue.toPath(), type)) + } + + if (current !is EtsAssignStmt) return listOf(Zero) + + val lhv = current.lhv.toPath() + val rhv = current.rhv.toPathOrNull() + + val result = mutableListOf(Zero) + + // 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 = current.rhv.tryGetKnownType(current.method) + EtsTypeFact.from(knownType).fixAnyToUnknown() + } else { + EtsTypeFact.UnknownEtsTypeFact + } + 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) + } + } 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) + } + + // x := y * z + is EtsBinaryExpr -> { + val y_is_number = rhv.left.toPathOrNull()?.let { + TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) + } + val z_is_number = rhv.right.toPathOrNull()?.let { + TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) + } + return listOfNotNull(Zero, y_is_number, z_is_number) + } + + // 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) + } + + else -> { + return listOf(Zero) + } + } + } + + // Handle new possible facts for LHS: + if (lhv.accesses.isNotEmpty()) { + result += TypedVariable(lhv, EtsTypeFact.UnknownEtsTypeFact) + } + + return result + } + + 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 result = mutableListOf(fact) + + // z: t --> { z: t } + if (!fact.variable.startsWith(lhv)) { + return result + } + + 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) + } + val z_is_number = rhv.right.toPathOrNull()?.let { + TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) + } + result += listOfNotNull(y_is_number, z_is_number) + } + } + + // x := y * z (numeric operator) + is EtsBinaryExpr -> { + // x.*: t --> none + } + + // x := y.foo(...) (call-to-return) + is EtsInstanceCallExpr -> { + // x.*: t --> none + } + + 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 + } + + // 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 + } + + // 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.* := const + rhv.isConst() -> { + // x.*: t --> none + } + + else -> { + // x.*: t --> none + } + } + } + + return result + } + + override fun obtainCallToReturnSiteFlowFunction( + callStatement: EtsStmt, + returnSite: EtsStmt + ): FlowFunction = FlowFunction { fact -> + when (fact) { + Zero -> callZero(callStatement) + is TypedVariable -> call(callStatement, fact) + } + } + + private fun callZero( + callStatement: EtsStmt, + ): List { + val result = mutableListOf(Zero) + + val callExpr = callStatement.callExpr ?: error("No call") + + if (callExpr is EtsInstanceCallExpr) { + val instance = callExpr.instance + 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.toPath() + val type = EtsTypeFact.from(param.type) + result += TypedVariable(base, type) + } + } + + return result + } + + private fun call( + callStatement: EtsStmt, + fact: TypedVariable, + ): List { + val result = mutableListOf() + + 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 + } + + result += fact + return result + } + + override fun obtainCallToStartFlowFunction( + callStatement: EtsStmt, + calleeStart: EtsStmt, + ): FlowFunction = FlowFunction { fact -> + when (fact) { + Zero -> listOf(fact) + is TypedVariable -> start(callStatement, calleeStart, fact) + } + } + + private fun start( + callStatement: EtsStmt, + calleeStart: EtsStmt, + fact: TypedVariable, + ): List { + val callResult = (callStatement as? EtsAssignStmt)?.lhv?.toPath() ?: return emptyList() + + if (fact.variable != callResult) return emptyList() + + if (calleeStart is EtsThrowStmt) return emptyList() // TODO support throwStmt + + check(calleeStart is EtsReturnStmt) + + val exitValue = calleeStart.returnValue?.toPath() ?: return emptyList() + + return listOf(TypedVariable(exitValue, fact.type)) + } + + override fun obtainExitToReturnSiteFlowFunction( + callStatement: EtsStmt, + returnSite: EtsStmt, + exitStatement: EtsStmt + ): FlowFunction = FlowFunction { fact -> + when (fact) { + Zero -> listOf(fact) + is TypedVariable -> exit(callStatement, fact) + } + } + + private fun exit( + callStatement: EtsStmt, + fact: TypedVariable, + ): List { + val callExpr = callStatement.callExpr ?: error("No call") + + 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.toPath() + return listOf(TypedVariable(instancePath + tail, fact.type)) + } + + is AccessPathBase.Arg -> { + val arg = callExpr.args.getOrNull(fact.variable.base.index)?.toPath() ?: return emptyList() + return listOf(TypedVariable(arg + tail, fact.type)) + } + + else -> return emptyList() + } + } +} + +private const val ACCESSES_LIMIT = 5 +private const val DUPLICATE_FIELDS_LIMIT = 3 + +private fun Iterable.myFilter(): List = filter { + 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 +} 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..12e104479e 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 @@ -19,3 +19,12 @@ sealed interface ForwardTypeDomainFact { val type: EtsTypeFact, // primitive or Object ) : ForwardTypeDomainFact } + +sealed interface BackwardPathTypeDomainFact { + data object Zero : BackwardPathTypeDomainFact + + data class TypedVariable( + val variable: AccessPath, + val type: EtsTypeFact, + ) : BackwardPathTypeDomainFact +} \ No newline at end of file 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..b1331915a4 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 @@ -101,7 +101,7 @@ class TypeInferenceManager( createResultsFromSummaries(updatedTypeScheme, doInferAllLocals) } - lateinit var backwardRunner: EtsIfdsRunner + lateinit var backwardRunner: EtsIfdsRunner lateinit var forwardRunner: EtsIfdsRunner private suspend fun collectSummaries( @@ -118,7 +118,7 @@ class TypeInferenceManager( analyzer = backwardAnalyzer, traits = traits, manager = this, - zeroFact = BackwardTypeDomainFact.Zero, + zeroFact = BackwardPathTypeDomainFact.Zero, ) this@TypeInferenceManager.backwardRunner = backwardRunner @@ -390,12 +390,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 @@ -426,8 +421,8 @@ class TypeInferenceManager( summaries: Iterable, ): Map { val types = summaries - .mapNotNull { it.exitFact as? BackwardTypeDomainFact.TypedVariable } - .groupBy({ it.variable }, { it.type }) + .mapNotNull { it.exitFact as? BackwardPathTypeDomainFact.TypedVariable } + .groupBy({ it.variable.base }, { it.variable.accesses to it.type }) .filter { (base, _) -> base is AccessPathBase.This || base is AccessPathBase.Arg @@ -435,13 +430,51 @@ class TypeInferenceManager( || (base is AccessPathBase.Local && base !in getRealLocalsBase(method)) } .mapValues { (_, typeFacts) -> + 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 rootType = run { + 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 + } + } + + val refined = rootType//.refineProperties(emptyList(), propertyRefinements) + + refined + } + /*.mapValues { (_, typeFacts) -> typeFacts.reduce { acc, typeFact -> typeProcessor.intersect(acc, typeFact) ?: run { logger.warn { "Empty intersection type: ${acc.toStringLimited()} & ${typeFact.toStringLimited()}" } acc } } - } + }*/ return types } @@ -556,13 +589,24 @@ 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 +614,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 +739,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/test/resources/ts/testcases.ts b/usvm-ts-dataflow/src/test/resources/ts/testcases.ts index 9927bf0c74..71f193bf4e 100644 --- a/usvm-ts-dataflow/src/test/resources/ts/testcases.ts +++ b/usvm-ts-dataflow/src/test/resources/ts/testcases.ts @@ -70,17 +70,17 @@ class CaseAssignFieldToSelf { } // 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 }" +// } +// } // ---------------------------------------- From 6cfcdb846e4e389b1e8b7a201fffe0e1c79c4955 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Wed, 28 May 2025 18:43:54 +0300 Subject: [PATCH 2/7] removed old backward flow functions --- .../usvm/dataflow/ts/infer/AnalyzerEvent.kt | 4 +- .../dataflow/ts/infer/BackwardAnalyzer.kt | 16 +- .../ts/infer/BackwardFlowFunctions.kt | 630 +++++------------- .../ts/infer/BackwardPathFlowFunctions.kt | 372 ----------- .../usvm/dataflow/ts/infer/TypeDomainFact.kt | 12 +- .../dataflow/ts/infer/TypeInferenceManager.kt | 15 +- 6 files changed, 187 insertions(+), 862 deletions(-) delete mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardPathFlowFunctions.kt diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt index 3d636d3b4d..33d3a6471f 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt @@ -17,8 +17,8 @@ data class ForwardSummaryAnalyzerEvent( data class BackwardSummaryAnalyzerEvent( val method: EtsMethod, - val initialVertex: Vertex, - val exitVertex: Vertex, + val initialVertex: Vertex, + val exitVertex: Vertex, ) : AnalyzerEvent { val initialFact get() = initialVertex.fact val exitFact get() = exitVertex.fact 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 15c83ddeb4..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,23 +9,21 @@ import org.usvm.dataflow.ts.graph.EtsApplicationGraph class BackwardAnalyzer( val graph: EtsApplicationGraph, - savedTypes: MutableMap>, - dominators: (EtsMethod) -> GraphDominators, doAddKnownTypes: Boolean = true, -) : Analyzer { +) : Analyzer { - override val flowFunctions = BackwardPathFlowFunctions(doAddKnownTypes) + override val flowFunctions = BackwardFlowFunctions(doAddKnownTypes) override fun handleCrossUnitCall( - caller: Vertex, - callee: Vertex, + caller: Vertex, + callee: Vertex, ): List { error("No cross unit calls") } - override fun handleNewEdge(edge: Edge): List { + 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..f62795fa6d 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,40 @@ +/* + * 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 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, @@ -64,453 +49,196 @@ class BackwardFlowFunctions( } 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).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 + return listOf(Zero, TypedVariable(returnValue.toPath(), type)) } - } - - 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 - } - - // 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 - } + if (current !is EtsAssignStmt) return listOf(Zero) - 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 - - 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 +255,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 +278,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 +303,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 +311,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 +319,7 @@ class BackwardFlowFunctions( override fun obtainExitToReturnSiteFlowFunction( callStatement: EtsStmt, returnSite: EtsStmt, - exitStatement: EtsStmt, + exitStatement: EtsStmt ): FlowFunction = FlowFunction { fact -> when (fact) { Zero -> listOf(fact) @@ -611,20 +333,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 +356,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/BackwardPathFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardPathFlowFunctions.kt deleted file mode 100644 index 9e5a4f4039..0000000000 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardPathFlowFunctions.kt +++ /dev/null @@ -1,372 +0,0 @@ -/* - * 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 org.jacodb.ets.model.EtsAddExpr -import org.jacodb.ets.model.EtsAssignStmt -import org.jacodb.ets.model.EtsBinaryExpr -import org.jacodb.ets.model.EtsInstanceCallExpr -import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsReturnStmt -import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.model.EtsThrowStmt -import org.jacodb.ets.utils.callExpr -import org.usvm.dataflow.ifds.FlowFunction -import org.usvm.dataflow.ifds.FlowFunctions -import org.usvm.dataflow.ts.infer.BackwardPathTypeDomainFact.Zero -import org.usvm.dataflow.ts.infer.BackwardPathTypeDomainFact.TypedVariable -import org.usvm.dataflow.ts.util.fixAnyToUnknown - -class BackwardPathFlowFunctions( - val doAddKnownTypes: Boolean, -) : FlowFunctions { - override fun obtainPossibleStartFacts(method: EtsMethod): Collection = listOf(Zero) - - override fun obtainSequentFlowFunction( - current: EtsStmt, - next: EtsStmt, - ): FlowFunction = FlowFunction { fact -> - if (current is EtsAssignStmt) { - val lhvPath = current.lhv.toPathOrNull() - val rhvPath = current.rhv.toPathOrNull() - if (lhvPath != null && rhvPath != null && lhvPath == rhvPath) { - return@FlowFunction listOf(fact) - } - } - when (fact) { - Zero -> sequentZero(current) - is TypedVariable -> sequentTypedVariable(current, fact).myFilter() - } - } - - companion object { - private fun AccessPath?.isBase(): Boolean = - this != null&& base !is AccessPathBase.Const && accesses.isEmpty() - - private fun AccessPath?.isField(): Boolean = - this != null && accesses.size == 1 - - private fun AccessPath?.isConst(): Boolean = - this != null && base is AccessPathBase.Const && accesses.isEmpty() - } - - 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 - } - return listOf(Zero, TypedVariable(returnValue.toPath(), type)) - } - - if (current !is EtsAssignStmt) return listOf(Zero) - - val lhv = current.lhv.toPath() - val rhv = current.rhv.toPathOrNull() - - val result = mutableListOf(Zero) - - // 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 = current.rhv.tryGetKnownType(current.method) - EtsTypeFact.from(knownType).fixAnyToUnknown() - } else { - EtsTypeFact.UnknownEtsTypeFact - } - 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) - } - } 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) - } - - // x := y * z - is EtsBinaryExpr -> { - val y_is_number = rhv.left.toPathOrNull()?.let { - TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) - } - val z_is_number = rhv.right.toPathOrNull()?.let { - TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) - } - return listOfNotNull(Zero, y_is_number, z_is_number) - } - - // 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) - } - - else -> { - return listOf(Zero) - } - } - } - - // Handle new possible facts for LHS: - if (lhv.accesses.isNotEmpty()) { - result += TypedVariable(lhv, EtsTypeFact.UnknownEtsTypeFact) - } - - return result - } - - 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 result = mutableListOf(fact) - - // z: t --> { z: t } - if (!fact.variable.startsWith(lhv)) { - return result - } - - 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) - } - val z_is_number = rhv.right.toPathOrNull()?.let { - TypedVariable(it, EtsTypeFact.NumberEtsTypeFact) - } - result += listOfNotNull(y_is_number, z_is_number) - } - } - - // x := y * z (numeric operator) - is EtsBinaryExpr -> { - // x.*: t --> none - } - - // x := y.foo(...) (call-to-return) - is EtsInstanceCallExpr -> { - // x.*: t --> none - } - - 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 - } - - // 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 - } - - // 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.* := const - rhv.isConst() -> { - // x.*: t --> none - } - - else -> { - // x.*: t --> none - } - } - } - - return result - } - - override fun obtainCallToReturnSiteFlowFunction( - callStatement: EtsStmt, - returnSite: EtsStmt - ): FlowFunction = FlowFunction { fact -> - when (fact) { - Zero -> callZero(callStatement) - is TypedVariable -> call(callStatement, fact) - } - } - - private fun callZero( - callStatement: EtsStmt, - ): List { - val result = mutableListOf(Zero) - - val callExpr = callStatement.callExpr ?: error("No call") - - if (callExpr is EtsInstanceCallExpr) { - val instance = callExpr.instance - 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.toPath() - val type = EtsTypeFact.from(param.type) - result += TypedVariable(base, type) - } - } - - return result - } - - private fun call( - callStatement: EtsStmt, - fact: TypedVariable, - ): List { - val result = mutableListOf() - - 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 - } - - result += fact - return result - } - - override fun obtainCallToStartFlowFunction( - callStatement: EtsStmt, - calleeStart: EtsStmt, - ): FlowFunction = FlowFunction { fact -> - when (fact) { - Zero -> listOf(fact) - is TypedVariable -> start(callStatement, calleeStart, fact) - } - } - - private fun start( - callStatement: EtsStmt, - calleeStart: EtsStmt, - fact: TypedVariable, - ): List { - val callResult = (callStatement as? EtsAssignStmt)?.lhv?.toPath() ?: return emptyList() - - if (fact.variable != callResult) return emptyList() - - if (calleeStart is EtsThrowStmt) return emptyList() // TODO support throwStmt - - check(calleeStart is EtsReturnStmt) - - val exitValue = calleeStart.returnValue?.toPath() ?: return emptyList() - - return listOf(TypedVariable(exitValue, fact.type)) - } - - override fun obtainExitToReturnSiteFlowFunction( - callStatement: EtsStmt, - returnSite: EtsStmt, - exitStatement: EtsStmt - ): FlowFunction = FlowFunction { fact -> - when (fact) { - Zero -> listOf(fact) - is TypedVariable -> exit(callStatement, fact) - } - } - - private fun exit( - callStatement: EtsStmt, - fact: TypedVariable, - ): List { - val callExpr = callStatement.callExpr ?: error("No call") - - 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.toPath() - return listOf(TypedVariable(instancePath + tail, fact.type)) - } - - is AccessPathBase.Arg -> { - val arg = callExpr.args.getOrNull(fact.variable.base.index)?.toPath() ?: return emptyList() - return listOf(TypedVariable(arg + tail, fact.type)) - } - - else -> return emptyList() - } - } -} - -private const val ACCESSES_LIMIT = 5 -private const val DUPLICATE_FIELDS_LIMIT = 3 - -private fun Iterable.myFilter(): List = filter { - 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 -} 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 12e104479e..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 } @@ -19,12 +18,3 @@ sealed interface ForwardTypeDomainFact { val type: EtsTypeFact, // primitive or Object ) : ForwardTypeDomainFact } - -sealed interface BackwardPathTypeDomainFact { - data object Zero : BackwardPathTypeDomainFact - - data class TypedVariable( - val variable: AccessPath, - val type: EtsTypeFact, - ) : BackwardPathTypeDomainFact -} \ No newline at end of file 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 b1331915a4..9a5aa48d48 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 @@ -52,13 +52,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) @@ -101,7 +94,7 @@ class TypeInferenceManager( createResultsFromSummaries(updatedTypeScheme, doInferAllLocals) } - lateinit var backwardRunner: EtsIfdsRunner + lateinit var backwardRunner: EtsIfdsRunner lateinit var forwardRunner: EtsIfdsRunner private suspend fun collectSummaries( @@ -111,14 +104,14 @@ 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, analyzer = backwardAnalyzer, traits = traits, manager = this, - zeroFact = BackwardPathTypeDomainFact.Zero, + zeroFact = BackwardTypeDomainFact.Zero, ) this@TypeInferenceManager.backwardRunner = backwardRunner @@ -421,7 +414,7 @@ class TypeInferenceManager( summaries: Iterable, ): Map { val types = summaries - .mapNotNull { it.exitFact as? BackwardPathTypeDomainFact.TypedVariable } + .mapNotNull { it.exitFact as? BackwardTypeDomainFact.TypedVariable } .groupBy({ it.variable.base }, { it.variable.accesses to it.type }) .filter { (base, _) -> base is AccessPathBase.This From 7f683cf4e410cbfa9a444b5dc0af9ec0adaa16b0 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Mon, 23 Jun 2025 16:53:09 +0300 Subject: [PATCH 3/7] add liveness in backward --- .../dataflow/ts/infer/BackwardFlowFunctions.kt | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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 f62795fa6d..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 @@ -34,6 +34,12 @@ import org.usvm.dataflow.ts.util.fixAnyToUnknown class BackwardFlowFunctions( val doAddKnownTypes: Boolean, ) : FlowFunctions { + private val liveVariablesCache = hashMapOf() + internal fun liveVariables(method: EtsMethod) = + liveVariablesCache.computeIfAbsent(method) { + LiveVariables.from(method) + } + override fun obtainPossibleStartFacts(method: EtsMethod): Collection = listOf(Zero) override fun obtainSequentFlowFunction( @@ -47,9 +53,15 @@ class BackwardFlowFunctions( return@FlowFunction listOf(fact) } } + val liveVars = liveVariables(current.method) when (fact) { Zero -> sequentZero(current) - is TypedVariable -> sequentTypedVariable(current, fact).myFilter() + is TypedVariable -> sequentTypedVariable(current, fact).filter { + when (val base = it.variable.base) { + is AccessPathBase.Local -> liveVars.isAliveAt(base.name, current) + else -> true + } + }.myFilter() } } From e508445eaeac39da1d2f7b95be9db538d3afdd6d Mon Sep 17 00:00:00 2001 From: MForest7 Date: Mon, 23 Jun 2025 16:54:33 +0300 Subject: [PATCH 4/7] add raw type handling --- .../kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt | 5 +++++ 1 file changed, 5 insertions(+) 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 } From de21c377b36f8211860814b307c29e40c815f710 Mon Sep 17 00:00:00 2001 From: MForest7 Date: Mon, 23 Jun 2025 16:56:02 +0300 Subject: [PATCH 5/7] add logback to runtime dependencies --- usvm-ts-dataflow/build.gradle.kts | 1 + 1 file changed, 1 insertion(+) diff --git a/usvm-ts-dataflow/build.gradle.kts b/usvm-ts-dataflow/build.gradle.kts index fb819699d4..78839bcc28 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) + implementation(Libs.logback) testImplementation(Libs.mockk) testImplementation(Libs.junit_jupiter_params) From 3f5fddef872c2fcbf8b62ecf9270d906cc13ce20 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 23 Jun 2025 17:54:17 +0300 Subject: [PATCH 6/7] Add logback, exclude it from shadow minimization --- usvm-ts-dataflow/build.gradle.kts | 5 ++++- usvm-ts-dataflow/src/main/resources/logback.xml | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/usvm-ts-dataflow/build.gradle.kts b/usvm-ts-dataflow/build.gradle.kts index 78839bcc28..af70818e26 100644 --- a/usvm-ts-dataflow/build.gradle.kts +++ b/usvm-ts-dataflow/build.gradle.kts @@ -21,7 +21,7 @@ dependencies { implementation(Libs.kotlinx_collections) implementation(Libs.kotlinx_serialization_json) implementation(Libs.clikt) - implementation(Libs.logback) + runtimeOnly(Libs.logback) testImplementation(Libs.mockk) testImplementation(Libs.junit_jupiter_params) @@ -130,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/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 @@ - + From c80b2b303f763c7a43ed1dbea96f3163269d77ca Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 24 Jun 2025 15:30:08 +0300 Subject: [PATCH 7/7] Use AA branch 'neo/2025-06-24' --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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