From 61afb4610442a9df6d5d927ada75dfbfcff8c04d Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 18 Apr 2025 15:45:58 +0300 Subject: [PATCH 01/52] Move TsTypeSystem in another package --- usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt | 1 + usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt | 1 + .../main/kotlin/org/usvm/machine/{ => types}/TsTypeSystem.kt | 2 +- 3 files changed, 3 insertions(+), 1 deletion(-) rename usvm-ts/src/main/kotlin/org/usvm/machine/{ => types}/TsTypeSystem.kt (99%) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt index 5030e7daf..880e00f11 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt @@ -12,6 +12,7 @@ import org.usvm.UContext import org.usvm.UMachineOptions import org.usvm.USizeExprProvider import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.machine.types.TsTypeSystem import org.usvm.memory.UReadOnlyMemory import org.usvm.model.ULazyModelDecoder import org.usvm.solver.UExprTranslator diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index b498ab598..1fc88cef2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -12,6 +12,7 @@ import org.usvm.api.targets.TsTarget import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsTypeSystem import org.usvm.ps.createPathSelector import org.usvm.statistics.CompositeUMachineObserver import org.usvm.statistics.CoverageStatistics diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt similarity index 99% rename from usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt rename to usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 529be4894..b3ae38133 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -1,4 +1,4 @@ -package org.usvm.machine +package org.usvm.machine.types import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsBooleanType From 5904b7bb4607d9b30e3802691abe206e2182c145 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 18 Apr 2025 15:46:11 +0300 Subject: [PATCH 02/52] Introduce AuxiliaryType --- .../kotlin/org/usvm/machine/types/AuxiliaryType.kt | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt new file mode 100644 index 000000000..4bad8e022 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -0,0 +1,14 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsType + +// TODO string name? +class AuxiliaryType(val properties: Set) : EtsType { + override fun accept(visitor: EtsType.Visitor): R { + error("Should not be called") + } + + override val typeName: String + get() = "AuxiliaryType" +} \ No newline at end of file From 5d624a1febab42508fd0a4edd496145695addb45 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 18 Apr 2025 16:04:39 +0300 Subject: [PATCH 03/52] Small changes --- .../org/usvm/machine/types/TsTopTypeStream.kt | 81 +++++++++++++ .../org/usvm/machine/types/TsTypeSystem.kt | 112 ++++-------------- 2 files changed, 103 insertions(+), 90 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt new file mode 100644 index 000000000..1f23447b8 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt @@ -0,0 +1,81 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsPrimitiveType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.types.TypesResult +import org.usvm.types.TypesResult.Companion.toTypesResult +import org.usvm.types.USupportTypeStream +import org.usvm.types.UTypeStream +import org.usvm.types.emptyTypeStream + +class TsTopTypeStream( + private val typeSystem: TsTypeSystem, + private val primitiveTypes: List = TsTypeSystem.primitiveTypes.toList(), + // We treat unknown as a top type in this system + private val anyTypeStream: UTypeStream = USupportTypeStream.from(typeSystem, EtsUnknownType), +) : UTypeStream { + + override fun filterBySupertype(type: EtsType): UTypeStream { + if (type is EtsPrimitiveType) return emptyTypeStream() + + return anyTypeStream.filterBySupertype(type) + } + + override fun filterBySubtype(type: EtsType): UTypeStream { + return anyTypeStream.filterBySubtype(type) + } + + override fun filterByNotSupertype(type: EtsType): UTypeStream { + if (type in primitiveTypes) { + val updatedPrimitiveTypes = primitiveTypes.remove(type) + + if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream + + return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream) + } + + return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSupertype(type)) + } + + override fun filterByNotSubtype(type: EtsType): UTypeStream { + if (type in primitiveTypes) { + val updatedPrimitiveTypes = primitiveTypes.remove(type) + + if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream + + return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream) + } + + return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSubtype(type)) + } + + override fun take(n: Int): TypesResult { + if (n <= primitiveTypes.size) { + return primitiveTypes.toTypesResult(wasTimeoutExpired = false) + } + + val types = primitiveTypes.toMutableList() + return when (val remainingTypes = anyTypeStream.take(n - primitiveTypes.size)) { + TypesResult.EmptyTypesResult -> types.toTypesResult(wasTimeoutExpired = false) + is TypesResult.SuccessfulTypesResult -> { + val allTypes = types + remainingTypes.types + allTypes.toTypesResult(wasTimeoutExpired = false) + } + + is TypesResult.TypesResultWithExpiredTimeout -> { + val allTypes = types + remainingTypes.collectedTypes + allTypes.toTypesResult(wasTimeoutExpired = true) + } + } + } + + override val isEmpty: Boolean? + get() = anyTypeStream.isEmpty?.let { primitiveTypes.isEmpty() } + + override val commonSuperType: EtsType? + get() = EtsUnknownType.takeIf { !(isEmpty ?: true) } + + private fun List.remove(x: T): List = this.filterNot { it == x } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index b3ae38133..f2fde73d8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -1,18 +1,24 @@ package org.usvm.machine.types +import com.jetbrains.rd.framework.util.RdCoroutineScope.Companion.override import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsPrimitiveType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnknownType +import org.usvm.machine.types.TsTypeSystem.Companion.primitiveTypes import org.usvm.types.TypesResult import org.usvm.types.TypesResult.Companion.toTypesResult import org.usvm.types.USupportTypeStream import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem import org.usvm.types.emptyTypeStream +import org.usvm.util.type import kotlin.time.Duration // TODO this is draft, should be replaced with real implementation @@ -27,35 +33,32 @@ class TsTypeSystem( } override fun isSupertype(supertype: EtsType, type: EtsType): Boolean = when { + type is AuxiliaryType -> TODO() supertype == type -> true supertype == EtsUnknownType || supertype == EtsAnyType -> true - else -> false + else -> TODO() } + // override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when { - type is EtsPrimitiveType -> types.isEmpty() - else -> false + type is EtsPrimitiveType -> types.any { it == type } + type is EtsClassType -> TODO() + type is EtsUnclearRefType -> TODO() + type is EtsArrayType -> TODO() + else -> error("Unsupported class type: $type") } - override fun isFinal(type: EtsType): Boolean = when (type) { - is EtsPrimitiveType -> true - is EtsUnknownType -> false - is EtsAnyType -> false - else -> false - } + // TODO is it right? + override fun isFinal(type: EtsType): Boolean = type is EtsPrimitiveType - override fun isInstantiable(type: EtsType): Boolean = when (type) { - is EtsPrimitiveType -> true - is EtsUnknownType -> true - is EtsAnyType -> true - else -> false - } + // TODO are there any non instantiable types? + override fun isInstantiable(type: EtsType): Boolean = true override fun findSubtypes(type: EtsType): Sequence = when (type) { - is EtsPrimitiveType -> emptySequence() - is EtsUnknownType -> primitiveTypes - is EtsAnyType -> primitiveTypes - else -> emptySequence() + is EtsPrimitiveType -> emptySequence() // TODO why??? + is EtsAnyType, + is EtsUnknownType -> project.projectAndSdkClasses.asSequence().map { it.type } + else -> TODO() } private val topTypeStream by lazy { TsTopTypeStream(this) } @@ -63,74 +66,3 @@ class TsTypeSystem( override fun topTypeStream(): UTypeStream = topTypeStream } -class TsTopTypeStream( - private val typeSystem: TsTypeSystem, - private val primitiveTypes: List = TsTypeSystem.primitiveTypes.toList(), - // Currently only EtsUnknownType was encountered and viewed as any type. - // However, there is EtsAnyType that represents any type. - // TODO: replace EtsUnknownType with further TsTypeSystem implementation. - private val anyTypeStream: UTypeStream = USupportTypeStream.from(typeSystem, EtsUnknownType), -) : UTypeStream { - - override fun filterBySupertype(type: EtsType): UTypeStream { - if (type is EtsPrimitiveType) return emptyTypeStream() - - return anyTypeStream.filterBySupertype(type) - } - - override fun filterBySubtype(type: EtsType): UTypeStream { - return anyTypeStream.filterBySubtype(type) - } - - override fun filterByNotSupertype(type: EtsType): UTypeStream { - if (type in primitiveTypes) { - val updatedPrimitiveTypes = primitiveTypes.remove(type) - - if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream - - return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream) - } - - return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSupertype(type)) - } - - override fun filterByNotSubtype(type: EtsType): UTypeStream { - if (type in primitiveTypes) { - val updatedPrimitiveTypes = primitiveTypes.remove(type) - - if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream - - return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream) - } - - return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSubtype(type)) - } - - override fun take(n: Int): TypesResult { - if (n <= primitiveTypes.size) { - return primitiveTypes.toTypesResult(wasTimeoutExpired = false) - } - - val types = primitiveTypes.toMutableList() - return when (val remainingTypes = anyTypeStream.take(n - primitiveTypes.size)) { - TypesResult.EmptyTypesResult -> types.toTypesResult(wasTimeoutExpired = false) - is TypesResult.SuccessfulTypesResult -> { - val allTypes = types + remainingTypes.types - allTypes.toTypesResult(wasTimeoutExpired = false) - } - - is TypesResult.TypesResultWithExpiredTimeout -> { - val allTypes = types + remainingTypes.collectedTypes - allTypes.toTypesResult(wasTimeoutExpired = true) - } - } - } - - override val isEmpty: Boolean? - get() = anyTypeStream.isEmpty?.let { primitiveTypes.isEmpty() } - - override val commonSuperType: EtsType? - get() = EtsUnknownType.takeIf { !(isEmpty ?: true) } - - private fun List.remove(x: T): List = this.filterNot { it == x } -} From f2474e34d91608e9a597ff9e7cb0f94ff283f5b1 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 22 Apr 2025 15:07:49 +0300 Subject: [PATCH 04/52] Copy documentation to TsTypeSystem file --- .../org/usvm/machine/types/TsTypeSystem.kt | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index f2fde73d8..63a6acc5a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -32,6 +32,9 @@ class TsTypeSystem( val primitiveTypes = sequenceOf(EtsNumberType, EtsBooleanType) } + /** + * @return true if [type] <: [supertype]. + */ override fun isSupertype(supertype: EtsType, type: EtsType): Boolean = when { type is AuxiliaryType -> TODO() supertype == type -> true @@ -39,7 +42,11 @@ class TsTypeSystem( else -> TODO() } - // + /** + * @return true if [types] and [type] can be supertypes for some type together. + * It is guaranteed that [type] is not a supertype for any type from [types] + * and that [types] have common subtype. + */ override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when { type is EtsPrimitiveType -> types.any { it == type } type is EtsClassType -> TODO() @@ -49,11 +56,20 @@ class TsTypeSystem( } // TODO is it right? + /** + * @return true if there is no type u distinct from [type] and subtyping [type]. + */ override fun isFinal(type: EtsType): Boolean = type is EtsPrimitiveType // TODO are there any non instantiable types? + /** + * @return true if [type] is instantiable, meaning it can be created via constructor. + */ override fun isInstantiable(type: EtsType): Boolean = true + /** + * @return a sequence of **direct** inheritors of the [type]. + */ override fun findSubtypes(type: EtsType): Sequence = when (type) { is EtsPrimitiveType -> emptySequence() // TODO why??? is EtsAnyType, From 1121ed5bdde039ecc5b0bd4e82df614ab69eb7a5 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 22 Apr 2025 15:11:15 +0300 Subject: [PATCH 05/52] Change hasCommonSubtype for primitive types --- usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 63a6acc5a..958a8d776 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -48,7 +48,7 @@ class TsTypeSystem( * and that [types] have common subtype. */ override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when { - type is EtsPrimitiveType -> types.any { it == type } + type is EtsPrimitiveType -> types.isEmpty() type is EtsClassType -> TODO() type is EtsUnclearRefType -> TODO() type is EtsArrayType -> TODO() From a95faf38af8d8e93ad650475c0afc817817d188b Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 22 Apr 2025 15:13:23 +0300 Subject: [PATCH 06/52] Minor changes --- .../src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt | 1 - usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt index 1f23447b8..a5faf0855 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt @@ -1,6 +1,5 @@ package org.usvm.machine.types -import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsPrimitiveType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnknownType diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 958a8d776..ee395d6b9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -72,6 +72,7 @@ class TsTypeSystem( */ override fun findSubtypes(type: EtsType): Sequence = when (type) { is EtsPrimitiveType -> emptySequence() // TODO why??? + // TODO they should be direct inheritors, not all of them is EtsAnyType, is EtsUnknownType -> project.projectAndSdkClasses.asSequence().map { it.type } else -> TODO() From d02da223c123edc7b681c2b3009e789ce943bd7f Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 22 Apr 2025 16:37:28 +0300 Subject: [PATCH 07/52] Stream usages --- .../usvm/machine/interpreter/TsInterpreter.kt | 28 ++++++++-- .../org/usvm/machine/types/TsTypeSystem.kt | 54 ++++++++++++++++--- .../src/test/kotlin/org/usvm/samples/Call.kt | 1 - .../org/usvm/samples/types/TypeStream.kt | 32 +++++++++++ .../org/usvm/util/TsMethodTestRunner.kt | 3 +- .../kotlin/org/usvm/util/TsTestResolver.kt | 39 ++++++++++---- .../resources/samples/types/TypeStream.ts | 34 ++++++++++++ 7 files changed, 167 insertions(+), 24 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt create mode 100644 usvm-ts/src/test/resources/samples/types/TypeStream.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 44a90df0e..3aae14d8a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -1,5 +1,6 @@ package org.usvm.machine.interpreter +import io.ksmt.expr.rewrite.simplify.addArithTerm import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayAccess @@ -15,6 +16,7 @@ import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStmt @@ -31,6 +33,7 @@ import org.usvm.UAddressSort import org.usvm.UExpr import org.usvm.UInterpreter import org.usvm.api.allocateArrayInitialized +import org.usvm.api.evalTypeEquals import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.makeSymbolicRefUntyped import org.usvm.api.targets.TsTarget @@ -64,6 +67,7 @@ import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue import org.usvm.util.resolveEtsField import org.usvm.util.resolveEtsMethods +import org.usvm.util.type import org.usvm.utils.ensureSat private val logger = KotlinLogging.logger {} @@ -185,7 +189,12 @@ class TsInterpreter( val conditionsWithBlocks = concreteMethods.map { method -> val concreteCall = stmt.toConcrete(method) val block = { state: TsState -> state.newStmt(concreteCall) } - ctx.trueExpr to block + val type = method.enclosingClass!!.type + val constraint = scope.calcOnState { + val instance = stmt.instance.asExpr(ctx.addressSort) + memory.types.evalTypeEquals(instance, type) // TODO mistake, should be separated into several hierarchies + } + constraint to block } scope.forkMulti(conditionsWithBlocks) } @@ -527,9 +536,20 @@ class TsInterpreter( ) } - // TODO fix incorrect type streams - // val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, EtsClassType(method.enclosingClass)) - // state.pathConstraints += thisTypeConstraint + method.enclosingClass?.let { thisClass -> + // TODO not equal but subtype for abstract/interfaces + val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, thisClass.type) + state.pathConstraints += thisTypeConstraint + } + + method.parameters.forEachIndexed { i, param -> + val parameterType = param.type + if (parameterType is EtsRefType) { + val argLValue = mkRegisterStackLValue(ctx.addressSort, i) + val ref = state.memory.read(argLValue).asExpr(ctx.addressSort) + state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) + } + } val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index ee395d6b9..5907dedea 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsPrimitiveType import org.jacodb.ets.model.EtsScene @@ -35,11 +36,41 @@ class TsTypeSystem( /** * @return true if [type] <: [supertype]. */ - override fun isSupertype(supertype: EtsType, type: EtsType): Boolean = when { - type is AuxiliaryType -> TODO() - supertype == type -> true - supertype == EtsUnknownType || supertype == EtsAnyType -> true - else -> TODO() + override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { + return when { + type is AuxiliaryType -> TODO() + supertype is AuxiliaryType -> TODO() + supertype == type -> true + supertype == EtsUnknownType || supertype == EtsAnyType -> true + supertype is EtsPrimitiveType || type is EtsPrimitiveType -> type == supertype + else -> { + // TODO isAssignable + if (supertype is EtsUnknownType || supertype is EtsAnyType) { + return true + } + + if (type is EtsUnknownType || type is EtsAnyType) { + return false // otherwise it should be processed in the code above + } + + // TODO wrong type resolutions because of names + val clazz = project.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO") + val ancestors = generateSequence(clazz) { c -> + // TODO mistake because of name usage + project.projectAndSdkClasses.singleOrNull { it.signature.name == c.superClass?.name } + }.map { it.type } + + if (supertype is EtsClassType) { + return ancestors.any { it == supertype } + } + + if (supertype is EtsUnclearRefType) { + return ancestors.any { it.typeName == supertype.typeName } + } + + error("TODO") + } + } } /** @@ -49,8 +80,8 @@ class TsTypeSystem( */ override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when { type is EtsPrimitiveType -> types.isEmpty() - type is EtsClassType -> TODO() - type is EtsUnclearRefType -> TODO() + type is EtsClassType -> true + type is EtsUnclearRefType -> true type is EtsArrayType -> TODO() else -> error("Unsupported class type: $type") } @@ -75,7 +106,14 @@ class TsTypeSystem( // TODO they should be direct inheritors, not all of them is EtsAnyType, is EtsUnknownType -> project.projectAndSdkClasses.asSequence().map { it.type } - else -> TODO() + is AuxiliaryType -> { + TODO() + } + else -> { + val clazz = project.projectAndSdkClasses.filter { it.type == type } + // TODO optimize + project.projectAndSdkClasses.asSequence().filter { it.superClass == clazz }.map { it.type } + } } private val topTypeStream by lazy { TsTopTypeStream(this) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt index 76f3f3ba8..14af11b04 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt @@ -210,7 +210,6 @@ class Call : TsMethodTestRunner() { ) } - @Disabled("Too complex") @Test fun `test virtual dispatch`() { val method = getMethod(className, "virtualDispatch") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt new file mode 100644 index 000000000..57c62f1e2 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt @@ -0,0 +1,32 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.api.TsValue +import org.usvm.util.TsMethodTestRunner + +class TypeStream : TsMethodTestRunner() { + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "types") + + @Test + fun `test an ancestor as argument`() { + val method = getMethod(className, "ancestorId") + discoverProperties( + method = method, + { value, r -> r.name == value.name }, + ) + } + + @Test + fun `test virtual invoke on an ancestor`() { + val method = getMethod(className, "virtualInvokeForAncestor") + discoverProperties( + method = method, + { value, r -> value.name == "Parent" && r.number == 1.0 }, + { value, r -> value.name == "FirstChild" && r.number == 2.0 }, + { value, r -> value.name == "SecondChild" && r.number == 3.0 }, + ) + } +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 5169801aa..889dae058 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -39,10 +39,11 @@ abstract class TsMethodTestRunner : TestRunner { val cls = ctx.scene.projectAndSdkClasses.single { it.name == type.typeName } - resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef, cls.type) + resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef) } is EtsClassType -> { - resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef, type) + resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef) } is EtsArrayType -> { @@ -323,36 +325,53 @@ open class TsTestStateResolver( } private fun resolveClass( - classType: EtsClassType, + refType: EtsRefType, ): EtsClass { + if (refType is EtsArrayType) { + TODO() + } + + // Special case for Object: - if (classType.signature.name == "Object") { + val name = when(refType) { + is EtsClassType -> refType.signature.name + is EtsUnclearRefType -> refType.name + else -> error("Unsupported $refType") + } + + if (name == "Object") { return createObjectClass() } // Perfect signature: - if (classType.signature.name != UNKNOWN_CLASS_NAME) { - val classes = ctx.scene.projectAndSdkClasses.filter { it.signature == classType.signature } + if (name != UNKNOWN_CLASS_NAME) { + val classes = ctx.scene.projectAndSdkClasses.filter { + when (refType) { + is EtsClassType -> it.signature == refType.signature + is EtsUnclearRefType -> it.name == refType.typeName + else -> error("TODO") + } + } if (classes.size == 1) { return classes.single() } } // Sad signature: - val classes = ctx.scene.projectAndSdkClasses.filter { it.signature.name == classType.signature.name } + val classes = ctx.scene.projectAndSdkClasses.filter { it.signature.name == name } if (classes.size == 1) { return classes.single() } - error("Could not resolve class: ${classType.signature}") + error("Could not resolve class: ${refType}") } private fun resolveTsClass( concreteRef: UConcreteHeapRef, heapRef: UHeapRef, - classType: EtsClassType, ): TsTestValue.TsClass = with(ctx) { - val clazz = resolveClass(classType) + val type = model.typeStreamOf(concreteRef).first() as EtsRefType + val clazz = resolveClass(type) val properties = clazz.fields .filterNot { field -> field as EtsFieldImpl diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts new file mode 100644 index 000000000..33df4725c --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts @@ -0,0 +1,34 @@ +class TypeStream { + ancestorId(ancestor: Parent): Parent { + return ancestor + } + + virtualInvokeForAncestor(ancestor: Parent): number { + var number = ancestor.virtualMethod(); + if (number == 100) { + return 1 + } else if (number == 200) { + return 2 + } else { + return 3 + } + } +} + +class Parent { + virtualMethod(): number { + return 100; + } +} + +class FirstChild extends Parent { + override virtualMethod(): number { + return 200; + } +} + +class SecondChild extends Parent { + override virtualMethod(): number{ + return 300; + } +} \ No newline at end of file From cce7f335b17e8924643071f52c3db6455ee61ca0 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 23 Apr 2025 13:05:28 +0300 Subject: [PATCH 08/52] Stream usages with unique fields --- .../org/usvm/machine/expr/TsExprResolver.kt | 11 ++++++ .../usvm/machine/interpreter/TsInterpreter.kt | 18 ++++++--- .../org/usvm/machine/types/TsTypeSystem.kt | 39 ++++++++++++++----- .../org/usvm/samples/types/TypeStream.kt | 24 ++++++++++++ .../resources/samples/types/TypeStream.ts | 31 +++++++++++++++ 5 files changed, 109 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index dbfcbcf01..eab901354 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -15,6 +15,7 @@ import org.jacodb.ets.model.EtsBitOrExpr import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr import org.jacodb.ets.model.EtsDivExpr @@ -96,6 +97,7 @@ import org.usvm.machine.state.TsState import org.usvm.machine.state.lastStmt import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt +import org.usvm.machine.types.AuxiliaryType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue import org.usvm.sizeSort @@ -624,6 +626,15 @@ class TsExprResolver( instanceRef: UHeapRef, field: EtsFieldSignature, ): UExpr? = with(ctx) { + val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef + scope.doWithState { + pathConstraints += if (field.enclosingClass == EtsClassSignature.UNKNOWN) { + memory.types.evalIsSubtype(resolvedAddr, AuxiliaryType(setOf(field.name))) + } else { + memory.types.evalIsSubtype(resolvedAddr, field.type) // TODO is it right? + } + } + val etsField = resolveEtsField(instance, field) val sort = typeToSort(etsField.type) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 3aae14d8a..1656f3bab 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -1,6 +1,5 @@ package org.usvm.machine.interpreter -import io.ksmt.expr.rewrite.simplify.addArithTerm import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayAccess @@ -134,20 +133,29 @@ class TsInterpreter( return scope.stepResult() } - private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) { + private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) = with(ctx) { // NOTE: USE '.callee' INSTEAD OF '.method' !!! val instance = stmt.instance checkNotNull(instance) val concreteRef = scope.calcOnState { models.first().eval(instance) } + val uncoveredInstance = if (concreteRef.isFakeObject()) { + scope.doWithState { + pathConstraints += concreteRef.getFakeType(scope).refTypeExpr + } + concreteRef.extractRef(scope) + } else { + concreteRef + } + val resolvedInstance = scope.calcOnState { models.first().eval(uncoveredInstance) } val concreteMethods: MutableList = mutableListOf() // TODO: handle 'instance.isFakeObject()' - if (isAllocatedConcreteHeapRef(concreteRef)) { - val type = scope.calcOnState { memory.typeStreamOf(concreteRef) }.single() + if (isAllocatedConcreteHeapRef(resolvedInstance)) { + val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single() if (type is EtsClassType) { // TODO: handle non-unique classes val classes = ctx.scene.projectAndSdkClasses.filter { it.name == type.typeName } @@ -191,7 +199,7 @@ class TsInterpreter( val block = { state: TsState -> state.newStmt(concreteCall) } val type = method.enclosingClass!!.type val constraint = scope.calcOnState { - val instance = stmt.instance.asExpr(ctx.addressSort) + val instance = stmt.instance.asExpr(ctx.addressSort).takeIf { !it.isFakeObject() } ?: uncoveredInstance.asExpr(addressSort) memory.types.evalTypeEquals(instance, type) // TODO mistake, should be separated into several hierarchies } constraint to block diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 5907dedea..bd019758a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -38,8 +38,23 @@ class TsTypeSystem( */ override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { return when { - type is AuxiliaryType -> TODO() - supertype is AuxiliaryType -> TODO() + type is AuxiliaryType -> { + if (supertype is EtsUnknownType || supertype is EtsAnyType) return true + + if (supertype is AuxiliaryType) { + return type.properties.all { it in supertype.properties } + } + val supertypeFields = + project.projectAndSdkClasses.single { it.type.typeName == supertype.typeName }.fields + type.properties.all { it in supertypeFields.map { it.name } } + } + + supertype is AuxiliaryType -> { + if (type is EtsUnknownType || type is EtsAnyType) return supertype.properties.isEmpty() + + val typeFields = project.projectAndSdkClasses.single { it.type.typeName == type.typeName }.fields + typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) + } supertype == type -> true supertype == EtsUnknownType || supertype == EtsAnyType -> true supertype is EtsPrimitiveType || type is EtsPrimitiveType -> type == supertype @@ -54,7 +69,8 @@ class TsTypeSystem( } // TODO wrong type resolutions because of names - val clazz = project.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO") + val clazz = + project.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO") val ancestors = generateSequence(clazz) { c -> // TODO mistake because of name usage project.projectAndSdkClasses.singleOrNull { it.signature.name == c.superClass?.name } @@ -78,11 +94,12 @@ class TsTypeSystem( * It is guaranteed that [type] is not a supertype for any type from [types] * and that [types] have common subtype. */ - override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when { - type is EtsPrimitiveType -> types.isEmpty() - type is EtsClassType -> true - type is EtsUnclearRefType -> true - type is EtsArrayType -> TODO() + override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when (type) { + is AuxiliaryType -> true + is EtsPrimitiveType -> types.isEmpty() + is EtsClassType -> true + is EtsUnclearRefType -> true + is EtsArrayType -> TODO() else -> error("Unsupported class type: $type") } @@ -106,9 +123,13 @@ class TsTypeSystem( // TODO they should be direct inheritors, not all of them is EtsAnyType, is EtsUnknownType -> project.projectAndSdkClasses.asSequence().map { it.type } + is AuxiliaryType -> { - TODO() + project.projectAndSdkClasses.filter { + it.fields.mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) + }.asSequence().map { it.type } } + else -> { val clazz = project.projectAndSdkClasses.filter { it.type == type } // TODO optimize diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt index 57c62f1e2..d6300d1f9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt @@ -1,6 +1,7 @@ package org.usvm.samples.types import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.api.TsValue import org.usvm.util.TsMethodTestRunner @@ -29,4 +30,27 @@ class TypeStream : TsMethodTestRunner() { { value, r -> value.name == "SecondChild" && r.number == 3.0 }, ) } + + @Test + fun `use unique field`() { + val method = getMethod(className, "useUniqueField") + discoverProperties( + method = method, + invariants = arrayOf( + { value, r -> value.name == "FirstChild" && r.number == 1.0 } + ) + ) + } + + @Test + @Disabled("Parent's fields are not supported yet") + fun `use non unique field`() { + val method = getMethod(className, "useNonUniqueField") + discoverProperties( + method = method, + { value, r -> value.name == "Parent" && r.number == 1.0 }, + { value, r -> value.name == "FirstChild" && r.number == 2.0 }, + { value, r -> value.name == "SecondChild" && r.number == 3.0 }, + ) + } } \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts index 33df4725c..9f8673024 100644 --- a/usvm-ts/src/test/resources/samples/types/TypeStream.ts +++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts @@ -13,22 +13,53 @@ class TypeStream { return 3 } } + + useUniqueField(value): number { + var number = value.firstChildField + + var virtualInvokeResult = value.virtualMethod() + if (virtualInvokeResult == 100) { + return -1 // unreachable + } else if (virtualInvokeResult == 200) { + return 1 + } else { + return -2 // unreachable + } + } + + useNonUniqueField(value): number { + var number = value.parentField + var virtualInvokeResult = value.virtualMethod() + if (virtualInvokeResult == 100) { + return 1 + } else if (virtualInvokeResult == 200) { + return 2 + } else { + return 3 + } + } } class Parent { virtualMethod(): number { return 100; } + + parentField: number = -10 } class FirstChild extends Parent { override virtualMethod(): number { return 200; } + + firstChildField: number = 10 } class SecondChild extends Parent { override virtualMethod(): number{ return 300; } + + secondChildField: number = 20 } \ No newline at end of file From 850b2c91e11c7104c450c7d9e2640eb395d6d230 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 24 Apr 2025 16:09:12 +0300 Subject: [PATCH 09/52] Hierarchy implementation --- .../kotlin/org/usvm/machine/JcTypeSystem.kt | 22 +++++++ .../main/kotlin/org/usvm/machine/TsGraph.kt | 2 + .../main/kotlin/org/usvm/machine/TsMachine.kt | 4 +- .../org/usvm/machine/expr/TsExprResolver.kt | 3 + .../usvm/machine/interpreter/TsInterpreter.kt | 2 +- .../org/usvm/machine/types/TsTypeSystem.kt | 21 +++--- .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 65 +++++++++++++++++++ .../org/usvm/samples/types/TypeStream.kt | 1 - 8 files changed, 104 insertions(+), 16 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt index 521e993e7..4600ffece 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt @@ -17,6 +17,28 @@ import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem import kotlin.time.Duration +open class A { + protected open fun foo() { + println("Hello") + } +} + +class B : A() { + override fun foo() { + println("Hello") + + } + + fun getsa() { + val method = this.javaClass.methods + } +} + +fun main() { + val a = B() + println(a.javaClass.declaredMethods.toList().joinToString("\n")) +} + class JcTypeSystem( private val cp: JcClasspath, override val typeOperationsTimeout: Duration diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsGraph.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsGraph.kt index e43802d70..85e177683 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsGraph.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsGraph.kt @@ -6,9 +6,11 @@ import org.jacodb.ets.model.EtsStmt import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl import org.usvm.statistics.ApplicationGraph +import org.usvm.util.EtsHierarchy class TsGraph(scene: EtsScene) : ApplicationGraph { private val etsGraph: EtsApplicationGraph = EtsApplicationGraphImpl(scene) + val hierarchy: EtsHierarchy = EtsHierarchy(scene) val cp: EtsScene get() = etsGraph.cp diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 1fc88cef2..d040ddd5b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -38,10 +38,10 @@ class TsMachine( private val machineObserver: UMachineObserver? = null, observer: TsInterpreterObserver? = null, ) : UMachine() { - private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds) + private val graph = TsGraph(scene) + private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) private val components = TsComponents(typeSystem, options) private val ctx = TsContext(scene, components) - private val graph = TsGraph(scene) private val interpreter = TsInterpreter(ctx, graph, tsOptions, observer) private val cfgStatistics = CfgStatisticsImpl(graph) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index eab901354..5526551c2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -101,6 +101,7 @@ import org.usvm.machine.types.AuxiliaryType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue import org.usvm.sizeSort +import org.usvm.util.EtsHierarchy import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -121,6 +122,7 @@ const val ADHOC_STRING__STRING = 2222.0 // 'string' class TsExprResolver( private val ctx: TsContext, + private val hierarchy: EtsHierarchy, private val scope: TsStepScope, private val localToIdx: (EtsMethod, EtsValue) -> Int, ) : EtsEntity.Visitor?> { @@ -631,6 +633,7 @@ class TsExprResolver( pathConstraints += if (field.enclosingClass == EtsClassSignature.UNKNOWN) { memory.types.evalIsSubtype(resolvedAddr, AuxiliaryType(setOf(field.name))) } else { + // TODO error, field.enclosingClass.type memory.types.evalIsSubtype(resolvedAddr, field.type) // TODO is it right? } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 1656f3bab..5f856342b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -491,7 +491,7 @@ class TsInterpreter( } private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver = - TsExprResolver(ctx, scope, ::mapLocalToIdx) + TsExprResolver(ctx, graph.hierarchy, scope, ::mapLocalToIdx) // (method, localName) -> idx private val localVarToIdx: MutableMap> = hashMapOf() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index bd019758a..4ffad329f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -1,24 +1,18 @@ package org.usvm.machine.types -import com.jetbrains.rd.framework.util.RdCoroutineScope.Companion.override import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsPrimitiveType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnknownType -import org.usvm.machine.types.TsTypeSystem.Companion.primitiveTypes -import org.usvm.types.TypesResult -import org.usvm.types.TypesResult.Companion.toTypesResult -import org.usvm.types.USupportTypeStream import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem -import org.usvm.types.emptyTypeStream +import org.usvm.util.EtsHierarchy import org.usvm.util.type import kotlin.time.Duration @@ -26,7 +20,9 @@ import kotlin.time.Duration class TsTypeSystem( val scene: EtsScene, override val typeOperationsTimeout: Duration, -) : UTypeSystem { + val project: EtsScene, + val hierarchy: EtsHierarchy, + ) : UTypeSystem { companion object { // TODO: add more primitive types (string, etc.) once supported @@ -44,15 +40,16 @@ class TsTypeSystem( if (supertype is AuxiliaryType) { return type.properties.all { it in supertype.properties } } - val supertypeFields = - project.projectAndSdkClasses.single { it.type.typeName == supertype.typeName }.fields + val supertypeClass = project.projectAndSdkClasses.single { it.type.typeName == supertype.typeName } + val supertypeFields = hierarchy.getAncestor(supertypeClass).flatMap { it.fields } type.properties.all { it in supertypeFields.map { it.name } } } supertype is AuxiliaryType -> { if (type is EtsUnknownType || type is EtsAnyType) return supertype.properties.isEmpty() - val typeFields = project.projectAndSdkClasses.single { it.type.typeName == type.typeName }.fields + val clazz = project.projectAndSdkClasses.single { it.type.typeName == type.typeName } + val typeFields = hierarchy.getAncestor(clazz).flatMap { it.fields } typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) } supertype == type -> true @@ -127,7 +124,7 @@ class TsTypeSystem( is AuxiliaryType -> { project.projectAndSdkClasses.filter { it.fields.mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) - }.asSequence().map { it.type } + }.asSequence().map { it.type } // TODO get fields of ancestors } else -> { diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt new file mode 100644 index 000000000..dd129d82e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -0,0 +1,65 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsScene +import kotlin.collections.flatten + +private typealias ClassName = String + +class EtsHierarchy(private val scene: EtsScene) { + private val resolveMap: Map> by lazy { + scene.projectAndSdkClasses + .groupBy { it.name } + .mapValues { (_, classes) -> + classes + .groupBy { it.signature } + .map { it.key to it.value.single() } + .toMap() + } + } + + private val ancestors: Map> by lazy { + val classes = scene.projectAndSdkClasses + val ancestors = classes.map { + it to generateSequence(listOf(it)) { currentClasses -> + currentClasses.flatMap { currentClass -> + val superClassSignature = currentClass.superClass ?: return@generateSequence null + val classesWithTheSameName = resolveMap.getValue(superClassSignature.name) + val classesWithTheSameSignature = classesWithTheSameName[superClassSignature] + val superClasses = when { + classesWithTheSameSignature != null -> listOf(classesWithTheSameSignature) + superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values + else -> error("There is no class with name ${superClassSignature.name}") + } + val interfaces = currentClass.implementedInterfaces + require(interfaces.isEmpty()) { TODO() } + val resolvedInterfaces = interfaces.map { interfaceSignature -> + resolveMap[currentClass.name]?.get(interfaceSignature) ?: error("Unresolved interface") + } + superClasses + resolvedInterfaces + } + }.flatten().toSet() + } + val result = ancestors.toMap() + + ancestors.forEach { (key, value) -> + value.forEach { clazz -> + inheritors.computeIfAbsent(clazz) { mutableSetOf() }.add(key) + } + } + result + } + + private val inheritors: MutableMap> = mutableMapOf() + + fun getAncestor(clazz: EtsClass): Set { + return ancestors[clazz] ?: error("TODO") + } + + fun getInheritors(clazz: EtsClass) : Set { + return inheritors[clazz] ?: error("TODO") + } +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt index d6300d1f9..1024aef83 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt @@ -43,7 +43,6 @@ class TypeStream : TsMethodTestRunner() { } @Test - @Disabled("Parent's fields are not supported yet") fun `use non unique field`() { val method = getMethod(className, "useNonUniqueField") discoverProperties( From b5c1be07f08b6f0e950d842d7f87bdf7a86f2701 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 25 Apr 2025 11:53:10 +0300 Subject: [PATCH 10/52] Add util function for receiving all fields --- .../kotlin/org/usvm/machine/types/TsTypeSystem.kt | 12 +++++------- .../main/kotlin/org/usvm/util/EtsFieldResolver.kt | 5 +++++ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 4ffad329f..0ac217496 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -13,6 +13,7 @@ import org.jacodb.ets.model.EtsUnknownType import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem import org.usvm.util.EtsHierarchy +import org.usvm.util.getAllFields import org.usvm.util.type import kotlin.time.Duration @@ -41,7 +42,7 @@ class TsTypeSystem( return type.properties.all { it in supertype.properties } } val supertypeClass = project.projectAndSdkClasses.single { it.type.typeName == supertype.typeName } - val supertypeFields = hierarchy.getAncestor(supertypeClass).flatMap { it.fields } + val supertypeFields = supertypeClass.getAllFields(hierarchy) type.properties.all { it in supertypeFields.map { it.name } } } @@ -49,7 +50,7 @@ class TsTypeSystem( if (type is EtsUnknownType || type is EtsAnyType) return supertype.properties.isEmpty() val clazz = project.projectAndSdkClasses.single { it.type.typeName == type.typeName } - val typeFields = hierarchy.getAncestor(clazz).flatMap { it.fields } + val typeFields = clazz.getAllFields(hierarchy) typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) } supertype == type -> true @@ -68,10 +69,7 @@ class TsTypeSystem( // TODO wrong type resolutions because of names val clazz = project.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO") - val ancestors = generateSequence(clazz) { c -> - // TODO mistake because of name usage - project.projectAndSdkClasses.singleOrNull { it.signature.name == c.superClass?.name } - }.map { it.type } + val ancestors = hierarchy.getAncestor(clazz).map { it.type } if (supertype is EtsClassType) { return ancestors.any { it == supertype } @@ -123,7 +121,7 @@ class TsTypeSystem( is AuxiliaryType -> { project.projectAndSdkClasses.filter { - it.fields.mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) + it.getAllFields(hierarchy).mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) }.asSequence().map { it.type } // TODO get fields of ancestors } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index aa65b68fe..fd9828001 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -1,5 +1,6 @@ package org.usvm.util +import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature @@ -83,3 +84,7 @@ private fun tryGetSingleField( } return null } + +fun EtsClass.getAllFields(hierarchy: EtsHierarchy): List { + return hierarchy.getAncestor(this).flatMap { it.fields } +} \ No newline at end of file From ed36c930edb7a5ce95042af1eaf3af253501448f Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Fri, 25 Apr 2025 13:00:25 +0300 Subject: [PATCH 11/52] Remove primitive types from the TopTypeStream --- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 2 +- .../org/usvm/machine/types/TsTopTypeStream.kt | 45 +++---------------- .../org/usvm/machine/types/TsTypeSystem.kt | 10 ++++- .../kotlin/org/usvm/util/TsTestResolver.kt | 4 +- 4 files changed, 19 insertions(+), 42 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 76793125b..094eeef93 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -25,7 +25,7 @@ fun TsContext.mkTruthyExpr( val conjuncts = mutableListOf>() val possibleType = memory.types.getTypeStream(expr.asExpr(addressSort)).single() as FakeType - scope.assert(possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr)) + scope.assert(possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr)) // TODO add to path constraints instead if (!possibleType.boolTypeExpr.isFalse) { conjuncts += ExprWithTypeConstraint( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt index a5faf0855..c42dd507d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt @@ -1,8 +1,10 @@ package org.usvm.machine.types +import com.sun.tools.javac.tree.TreeInfo.types import org.jacodb.ets.model.EtsPrimitiveType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnknownType +import org.usvm.machine.types.TsTypeSystem.Companion.primitiveTypes import org.usvm.types.TypesResult import org.usvm.types.TypesResult.Companion.toTypesResult import org.usvm.types.USupportTypeStream @@ -11,7 +13,6 @@ import org.usvm.types.emptyTypeStream class TsTopTypeStream( private val typeSystem: TsTypeSystem, - private val primitiveTypes: List = TsTypeSystem.primitiveTypes.toList(), // We treat unknown as a top type in this system private val anyTypeStream: UTypeStream = USupportTypeStream.from(typeSystem, EtsUnknownType), ) : UTypeStream { @@ -27,54 +28,22 @@ class TsTopTypeStream( } override fun filterByNotSupertype(type: EtsType): UTypeStream { - if (type in primitiveTypes) { - val updatedPrimitiveTypes = primitiveTypes.remove(type) - - if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream - - return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream) - } - - return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSupertype(type)) + return TsTopTypeStream(typeSystem, anyTypeStream.filterByNotSupertype(type)) } override fun filterByNotSubtype(type: EtsType): UTypeStream { - if (type in primitiveTypes) { - val updatedPrimitiveTypes = primitiveTypes.remove(type) - - if (updatedPrimitiveTypes.isEmpty()) return anyTypeStream - - return TsTopTypeStream(typeSystem, updatedPrimitiveTypes, anyTypeStream) - } - - return TsTopTypeStream(typeSystem, primitiveTypes, anyTypeStream.filterByNotSubtype(type)) + return TsTopTypeStream(typeSystem, anyTypeStream.filterByNotSubtype(type)) } override fun take(n: Int): TypesResult { - if (n <= primitiveTypes.size) { - return primitiveTypes.toTypesResult(wasTimeoutExpired = false) - } - - val types = primitiveTypes.toMutableList() - return when (val remainingTypes = anyTypeStream.take(n - primitiveTypes.size)) { - TypesResult.EmptyTypesResult -> types.toTypesResult(wasTimeoutExpired = false) - is TypesResult.SuccessfulTypesResult -> { - val allTypes = types + remainingTypes.types - allTypes.toTypesResult(wasTimeoutExpired = false) - } - - is TypesResult.TypesResultWithExpiredTimeout -> { - val allTypes = types + remainingTypes.collectedTypes - allTypes.toTypesResult(wasTimeoutExpired = true) - } - } + return anyTypeStream.take(n) } override val isEmpty: Boolean? - get() = anyTypeStream.isEmpty?.let { primitiveTypes.isEmpty() } + get() = anyTypeStream.isEmpty override val commonSuperType: EtsType? - get() = EtsUnknownType.takeIf { !(isEmpty ?: true) } + get() = EtsUnknownType.takeIf { isEmpty == false } private fun List.remove(x: T): List = this.filterNot { it == x } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 0ac217496..694001999 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnknownType +import org.usvm.types.USupportTypeStream import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem import org.usvm.util.EtsHierarchy @@ -108,7 +109,12 @@ class TsTypeSystem( /** * @return true if [type] is instantiable, meaning it can be created via constructor. */ - override fun isInstantiable(type: EtsType): Boolean = true + override fun isInstantiable(type: EtsType): Boolean { + if (type is EtsUnknownType) return false + if (type is EtsAnyType) return false + + return true + } /** * @return a sequence of **direct** inheritors of the [type]. @@ -132,7 +138,7 @@ class TsTypeSystem( } } - private val topTypeStream by lazy { TsTopTypeStream(this) } + private val topTypeStream by lazy { USupportTypeStream.from(this, EtsUnknownType) } override fun topTypeStream(): UTypeStream = topTypeStream } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 72c0c6ed3..2733a9005 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -370,7 +370,9 @@ open class TsTestStateResolver( concreteRef: UConcreteHeapRef, heapRef: UHeapRef, ): TsTestValue.TsClass = with(ctx) { - val type = model.typeStreamOf(concreteRef).first() as EtsRefType + val type = model.typeStreamOf(concreteRef).first() as? EtsRefType ?: run { + TODO() + } val clazz = resolveClass(type) val properties = clazz.fields .filterNot { field -> From f24f284f63fe992a635607844a6c610533452e6d Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Mon, 28 Apr 2025 13:46:27 +0300 Subject: [PATCH 12/52] Remove top type stream --- .../org/usvm/machine/types/TsTopTypeStream.kt | 49 ------------------- 1 file changed, 49 deletions(-) delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt deleted file mode 100644 index c42dd507d..000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTopTypeStream.kt +++ /dev/null @@ -1,49 +0,0 @@ -package org.usvm.machine.types - -import com.sun.tools.javac.tree.TreeInfo.types -import org.jacodb.ets.model.EtsPrimitiveType -import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsUnknownType -import org.usvm.machine.types.TsTypeSystem.Companion.primitiveTypes -import org.usvm.types.TypesResult -import org.usvm.types.TypesResult.Companion.toTypesResult -import org.usvm.types.USupportTypeStream -import org.usvm.types.UTypeStream -import org.usvm.types.emptyTypeStream - -class TsTopTypeStream( - private val typeSystem: TsTypeSystem, - // We treat unknown as a top type in this system - private val anyTypeStream: UTypeStream = USupportTypeStream.from(typeSystem, EtsUnknownType), -) : UTypeStream { - - override fun filterBySupertype(type: EtsType): UTypeStream { - if (type is EtsPrimitiveType) return emptyTypeStream() - - return anyTypeStream.filterBySupertype(type) - } - - override fun filterBySubtype(type: EtsType): UTypeStream { - return anyTypeStream.filterBySubtype(type) - } - - override fun filterByNotSupertype(type: EtsType): UTypeStream { - return TsTopTypeStream(typeSystem, anyTypeStream.filterByNotSupertype(type)) - } - - override fun filterByNotSubtype(type: EtsType): UTypeStream { - return TsTopTypeStream(typeSystem, anyTypeStream.filterByNotSubtype(type)) - } - - override fun take(n: Int): TypesResult { - return anyTypeStream.take(n) - } - - override val isEmpty: Boolean? - get() = anyTypeStream.isEmpty - - override val commonSuperType: EtsType? - get() = EtsUnknownType.takeIf { isEmpty == false } - - private fun List.remove(x: T): List = this.filterNot { it == x } -} From 711401453c5a4005b33d0233faba7f3014992ef0 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Mon, 28 Apr 2025 13:47:32 +0300 Subject: [PATCH 13/52] Remove primitive types from the type system --- .../org/usvm/machine/types/TsTypeSystem.kt | 22 ++++++------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 694001999..57497a8f1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -22,15 +22,8 @@ import kotlin.time.Duration class TsTypeSystem( val scene: EtsScene, override val typeOperationsTimeout: Duration, - val project: EtsScene, val hierarchy: EtsHierarchy, ) : UTypeSystem { - - companion object { - // TODO: add more primitive types (string, etc.) once supported - val primitiveTypes = sequenceOf(EtsNumberType, EtsBooleanType) - } - /** * @return true if [type] <: [supertype]. */ @@ -42,7 +35,7 @@ class TsTypeSystem( if (supertype is AuxiliaryType) { return type.properties.all { it in supertype.properties } } - val supertypeClass = project.projectAndSdkClasses.single { it.type.typeName == supertype.typeName } + val supertypeClass = scene.projectAndSdkClasses.single { it.type.typeName == supertype.typeName } val supertypeFields = supertypeClass.getAllFields(hierarchy) type.properties.all { it in supertypeFields.map { it.name } } } @@ -50,7 +43,7 @@ class TsTypeSystem( supertype is AuxiliaryType -> { if (type is EtsUnknownType || type is EtsAnyType) return supertype.properties.isEmpty() - val clazz = project.projectAndSdkClasses.single { it.type.typeName == type.typeName } + val clazz = scene.projectAndSdkClasses.single { it.type.typeName == type.typeName } val typeFields = clazz.getAllFields(hierarchy) typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) } @@ -69,7 +62,7 @@ class TsTypeSystem( // TODO wrong type resolutions because of names val clazz = - project.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO") + scene.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO") val ancestors = hierarchy.getAncestor(clazz).map { it.type } if (supertype is EtsClassType) { @@ -123,18 +116,18 @@ class TsTypeSystem( is EtsPrimitiveType -> emptySequence() // TODO why??? // TODO they should be direct inheritors, not all of them is EtsAnyType, - is EtsUnknownType -> project.projectAndSdkClasses.asSequence().map { it.type } + is EtsUnknownType -> scene.projectAndSdkClasses.asSequence().map { it.type } is AuxiliaryType -> { - project.projectAndSdkClasses.filter { + scene.projectAndSdkClasses.filter { it.getAllFields(hierarchy).mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) }.asSequence().map { it.type } // TODO get fields of ancestors } else -> { - val clazz = project.projectAndSdkClasses.filter { it.type == type } + val clazz = scene.projectAndSdkClasses.filter { it.type == type } // TODO optimize - project.projectAndSdkClasses.asSequence().filter { it.superClass == clazz }.map { it.type } + scene.projectAndSdkClasses.asSequence().filter { it.superClass == clazz }.map { it.type } } } @@ -142,4 +135,3 @@ class TsTypeSystem( override fun topTypeStream(): UTypeStream = topTypeStream } - From 79491f92d2a6613d8b4150e977840886a86e57b1 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 13:03:23 +0300 Subject: [PATCH 14/52] Replace any and unknown with object class --- .../usvm/machine/interpreter/TsInterpreter.kt | 6 ++ .../org/usvm/machine/types/TsTypeSystem.kt | 79 +++++++++++++------ .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 13 ++- .../org/usvm/samples/types/ObjectUsage.kt | 23 ++++++ .../resources/samples/types/ObjectUsage.ts | 9 +++ 5 files changed, 104 insertions(+), 26 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt create mode 100644 usvm-ts/src/test/resources/samples/types/ObjectUsage.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 5f856342b..c24d2bbaa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -9,6 +9,7 @@ import org.jacodb.ets.model.EtsCallStmt import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature @@ -22,6 +23,7 @@ import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsThrowStmt import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.callExpr @@ -557,6 +559,10 @@ class TsInterpreter( val ref = state.memory.read(argLValue).asExpr(ctx.addressSort) state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) } + + if (parameterType is EtsUnionType || parameterType is EtsIntersectionType) { + TODO("Handle union/intersection types") + } } val model = solver.check(state.pathConstraints).ensureSat().model diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 57497a8f1..549315e5a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -2,9 +2,7 @@ package org.usvm.machine.types import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsPrimitiveType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType @@ -47,9 +45,16 @@ class TsTypeSystem( val typeFields = clazz.getAllFields(hierarchy) typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) } + supertype == type -> true - supertype == EtsUnknownType || supertype == EtsAnyType -> true - supertype is EtsPrimitiveType || type is EtsPrimitiveType -> type == supertype + supertype == EtsUnknownType || supertype == EtsAnyType -> { + true + } + + supertype is EtsPrimitiveType || type is EtsPrimitiveType -> { + type == supertype + } + else -> { // TODO isAssignable if (supertype is EtsUnknownType || supertype is EtsAnyType) { @@ -60,9 +65,19 @@ class TsTypeSystem( return false // otherwise it should be processed in the code above } + if (type == EtsHierarchy.OBJECT_CLASS) { + return supertype == EtsHierarchy.OBJECT_CLASS + } + + if (supertype == EtsHierarchy.OBJECT_CLASS) { + return true // TODO not primitive + } + // TODO wrong type resolutions because of names - val clazz = - scene.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO") + val clazz = scene + .projectAndSdkClasses + .singleOrNull() { it.type.typeName == type.typeName } + ?: error("TODO") val ancestors = hierarchy.getAncestor(clazz).map { it.type } if (supertype is EtsClassType) { @@ -85,7 +100,9 @@ class TsTypeSystem( */ override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when (type) { is AuxiliaryType -> true - is EtsPrimitiveType -> types.isEmpty() + is EtsPrimitiveType -> { + types.isEmpty() + } is EtsClassType -> true is EtsUnclearRefType -> true is EtsArrayType -> TODO() @@ -103,8 +120,12 @@ class TsTypeSystem( * @return true if [type] is instantiable, meaning it can be created via constructor. */ override fun isInstantiable(type: EtsType): Boolean { - if (type is EtsUnknownType) return false - if (type is EtsAnyType) return false + if (type is EtsUnknownType) { + return false + } + if (type is EtsAnyType) { + return false + } return true } @@ -112,26 +133,34 @@ class TsTypeSystem( /** * @return a sequence of **direct** inheritors of the [type]. */ - override fun findSubtypes(type: EtsType): Sequence = when (type) { - is EtsPrimitiveType -> emptySequence() // TODO why??? - // TODO they should be direct inheritors, not all of them - is EtsAnyType, - is EtsUnknownType -> scene.projectAndSdkClasses.asSequence().map { it.type } - - is AuxiliaryType -> { - scene.projectAndSdkClasses.filter { - it.getAllFields(hierarchy).mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) - }.asSequence().map { it.type } // TODO get fields of ancestors - } + override fun findSubtypes(type: EtsType): Sequence { + return when (type) { + is EtsPrimitiveType -> emptySequence() // TODO why??? + // TODO they should be direct inheritors, not all of them + is EtsAnyType, + is EtsUnknownType -> { + // scene.projectAndSdkClasses.asSequence().map { it.type } + error("") + } - else -> { - val clazz = scene.projectAndSdkClasses.filter { it.type == type } - // TODO optimize - scene.projectAndSdkClasses.asSequence().filter { it.superClass == clazz }.map { it.type } + is AuxiliaryType -> { + scene.projectAndSdkClasses.filter { + it.getAllFields(hierarchy).mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) + }.asSequence().map { it.type } // TODO get fields of ancestors + } + + else -> { + if (type == EtsHierarchy.OBJECT_CLASS) { + return project.projectAndSdkClasses.asSequence().map { it.type } + } + val clazz = scene.projectAndSdkClasses.filter { it.type == type } + // TODO optimize + scene.projectAndSdkClasses.asSequence().filter { it.superClass == clazz }.map { it.type } + } } } - private val topTypeStream by lazy { USupportTypeStream.from(this, EtsUnknownType) } + private val topTypeStream by lazy { USupportTypeStream.from(this, EtsHierarchy.OBJECT_CLASS) } override fun topTypeStream(): UTypeStream = topTypeStream } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index dd129d82e..0ecf189b2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -2,6 +2,7 @@ package org.usvm.util import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsScene @@ -59,7 +60,17 @@ class EtsHierarchy(private val scene: EtsScene) { return ancestors[clazz] ?: error("TODO") } - fun getInheritors(clazz: EtsClass) : Set { + fun getInheritors(clazz: EtsClass): Set { return inheritors[clazz] ?: error("TODO") } + + companion object { + // TODO use real one + val OBJECT_CLASS = EtsClassType( + signature = EtsClassSignature( + name = "Object", + file = EtsFileSignature(projectName = "ES2015", fileName = "BuiltinClass") + ), + ) + } } \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt new file mode 100644 index 000000000..33c608f49 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt @@ -0,0 +1,23 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.usvm.api.TsValue +import org.usvm.util.TsMethodTestRunner +import kotlin.test.Test + +class ObjectUsage : TsMethodTestRunner() { + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className, folderPrefix = "types") + + @Test + fun `object as parameter`() { + val method = getMethod(className, "objectAsParameter") + discoverProperties( + method = method, + { value, r -> value is TsValue.TsClass && value.name == "Object" && r.number == 42.0 }, + { value, r -> value == TsValue.TsUndefined && r.number == -1.0 } + ) + } + +} \ No newline at end of file diff --git a/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts new file mode 100644 index 000000000..909134322 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts @@ -0,0 +1,9 @@ +class ObjectUsage { + objectAsParameter(object: Object): number { + if (object == undefined) { + return -1 + } + + return 42 + } +} \ No newline at end of file From ec13f52e62f0c15c32aec16b952a795327fe78d3 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 13:04:51 +0300 Subject: [PATCH 15/52] Tests fixes --- .../org/usvm/machine/types/TsTypeSystem.kt | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 549315e5a..36bb0d94f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -28,18 +28,31 @@ class TsTypeSystem( override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { return when { type is AuxiliaryType -> { - if (supertype is EtsUnknownType || supertype is EtsAnyType) return true + if (supertype is EtsUnknownType || supertype is EtsAnyType) { + return true + } + + if (supertype == EtsHierarchy.OBJECT_CLASS) { + return true + } if (supertype is AuxiliaryType) { return type.properties.all { it in supertype.properties } } + val supertypeClass = scene.projectAndSdkClasses.single { it.type.typeName == supertype.typeName } val supertypeFields = supertypeClass.getAllFields(hierarchy) type.properties.all { it in supertypeFields.map { it.name } } } supertype is AuxiliaryType -> { - if (type is EtsUnknownType || type is EtsAnyType) return supertype.properties.isEmpty() + if (type is EtsUnknownType || type is EtsAnyType) { + return supertype.properties.isEmpty() + } + + if (type == EtsHierarchy.OBJECT_CLASS) { + return supertype.properties.isEmpty() + } val clazz = scene.projectAndSdkClasses.single { it.type.typeName == type.typeName } val typeFields = clazz.getAllFields(hierarchy) From f2a0d33dc22e148812e43c46917cd7dd204e0ce4 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 16:51:50 +0300 Subject: [PATCH 16/52] Add instanceof and fixes --- .../org/usvm/machine/expr/TsExprResolver.kt | 12 +++++++++--- .../usvm/machine/interpreter/TsInterpreter.kt | 14 ++++++++++++-- .../org/usvm/machine/types/TsTypeSystem.kt | 11 ++++++++--- .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 17 +++++++++++------ 4 files changed, 40 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 5526551c2..ab348e14d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -83,6 +83,7 @@ import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.allocateArray import org.usvm.dataflow.ts.infer.tryGetKnownType +import org.usvm.dataflow.ts.util.type import org.usvm.isTrue import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext @@ -418,8 +419,10 @@ class TsExprResolver( } override fun visit(expr: EtsInstanceOfExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + return scope.calcOnState { + val instance = resolve(expr.arg)?.asExpr(ctx.addressSort) ?: return@calcOnState null + memory.types.evalIsSubtype(instance, expr.checkType) + } } // endregion @@ -754,7 +757,10 @@ class TsExprResolver( // region OTHER override fun visit(expr: EtsNewExpr): UExpr? = scope.calcOnState { - memory.allocConcrete(expr.type) + with(ctx.scene) { + val resolvedType = projectAndSdkClasses.singleOrNull { it.name == expr.type.typeName }?.type ?: expr.type + memory.allocConcrete(resolvedType) + } } override fun visit(expr: EtsNewArrayExpr): UExpr? = with(ctx) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index c24d2bbaa..4ea26dc34 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -201,8 +201,14 @@ class TsInterpreter( val block = { state: TsState -> state.newStmt(concreteCall) } val type = method.enclosingClass!!.type val constraint = scope.calcOnState { - val instance = stmt.instance.asExpr(ctx.addressSort).takeIf { !it.isFakeObject() } ?: uncoveredInstance.asExpr(addressSort) - memory.types.evalTypeEquals(instance, type) // TODO mistake, should be separated into several hierarchies + val instance = + stmt.instance.asExpr(ctx.addressSort).takeIf { !it.isFakeObject() } ?: uncoveredInstance.asExpr( + addressSort + ) + memory.types.evalTypeEquals( + instance, + type + ) // TODO mistake, should be separated into several hierarchies } constraint to block } @@ -557,6 +563,10 @@ class TsInterpreter( if (parameterType is EtsRefType) { val argLValue = mkRegisterStackLValue(ctx.addressSort, i) val ref = state.memory.read(argLValue).asExpr(ctx.addressSort) + val resolvedParameterType = graph.cp + .projectAndSdkClasses + .singleOrNull { it.name == parameterType.typeName } + ?: parameterType state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 36bb0d94f..0f264fa71 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -166,9 +166,14 @@ class TsTypeSystem( if (type == EtsHierarchy.OBJECT_CLASS) { return project.projectAndSdkClasses.asSequence().map { it.type } } - val clazz = scene.projectAndSdkClasses.filter { it.type == type } - // TODO optimize - scene.projectAndSdkClasses.asSequence().filter { it.superClass == clazz }.map { it.type } + // TODO wrong usage of names + if (type is EtsUnclearRefType) { + val classes = scene.projectAndSdkClasses.filter { it.type.typeName == type.typeName } + classes.asSequence().flatMap { hierarchy.getInheritors(it) }.map { it.type } + } else { + val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } ?: error("Cannot find class for $type") + hierarchy.getInheritors(clazz).asSequence().map { it.type } + } } } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 0ecf189b2..a2144ac5a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -44,24 +44,29 @@ class EtsHierarchy(private val scene: EtsScene) { } }.flatten().toSet() } - val result = ancestors.toMap() + ancestors.toMap() + } + private val inheritors: MutableMap> by lazy { + val result = mutableMapOf>() ancestors.forEach { (key, value) -> value.forEach { clazz -> - inheritors.computeIfAbsent(clazz) { mutableSetOf() }.add(key) + result.getOrPut(clazz) { hashSetOf() }.add(key) } } result } - private val inheritors: MutableMap> = mutableMapOf() - fun getAncestor(clazz: EtsClass): Set { - return ancestors[clazz] ?: error("TODO") + return ancestors[clazz] ?: run { + error("TODO") + } } fun getInheritors(clazz: EtsClass): Set { - return inheritors[clazz] ?: error("TODO") + return inheritors[clazz] ?: run { + error("TODO") + } } companion object { From 024c57954887973393a7175452d0e3feec23c0d2 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 17:14:03 +0300 Subject: [PATCH 17/52] Minor changes --- .../org/usvm/machine/types/TsTypeSystem.kt | 20 ++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 0f264fa71..c13fbbe8b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -28,21 +28,31 @@ class TsTypeSystem( override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { return when { type is AuxiliaryType -> { + // Unknown and Any types are top types in the system if (supertype is EtsUnknownType || supertype is EtsAnyType) { return true } + // We think that only ref types contain fields, and ObjectClass is a top type for ref types if (supertype == EtsHierarchy.OBJECT_CLASS) { return true } + // If we compare two auxiliary types, + // we should check if all fields of the first type are in the second type if (supertype is AuxiliaryType) { return type.properties.all { it in supertype.properties } } - val supertypeClass = scene.projectAndSdkClasses.single { it.type.typeName == supertype.typeName } + // TODO how to process unclearTypeRefs? + val supertypeClass = scene + .projectAndSdkClasses + .singleOrNull { it.type.typeName == supertype.typeName } + ?: TODO("For now we support only unique type resolution") val supertypeFields = supertypeClass.getAllFields(hierarchy) - type.properties.all { it in supertypeFields.map { it.name } } + val superTypeFieldNames = supertypeFields.mapTo(hashSetOf()) { it.name } + + type.properties.all { it in superTypeFieldNames } } supertype is AuxiliaryType -> { @@ -54,8 +64,12 @@ class TsTypeSystem( return supertype.properties.isEmpty() } - val clazz = scene.projectAndSdkClasses.single { it.type.typeName == type.typeName } + val clazz = scene + .projectAndSdkClasses + .singleOrNull { it.type.typeName == type.typeName } + ?: TODO("For now we support only unique type resolution") val typeFields = clazz.getAllFields(hierarchy) + typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) } From e759ead2f7e3cafb41d84e5e3807c359e3d4b01e Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 17:27:13 +0300 Subject: [PATCH 18/52] Minor changes --- .../usvm/machine/interpreter/TsInterpreter.kt | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 4ea26dc34..36168797f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -172,7 +172,9 @@ class TsInterpreter( return } val cls = classes.single() - val method = cls.methods.first { it.name == stmt.callee.name } + val method = cls.methods + .singleOrNull { it.name == stmt.callee.name } + ?: TODO("Overloads are not supported yet") concreteMethods += method } else { logger.warn { @@ -201,14 +203,12 @@ class TsInterpreter( val block = { state: TsState -> state.newStmt(concreteCall) } val type = method.enclosingClass!!.type val constraint = scope.calcOnState { - val instance = - stmt.instance.asExpr(ctx.addressSort).takeIf { !it.isFakeObject() } ?: uncoveredInstance.asExpr( - addressSort - ) - memory.types.evalTypeEquals( - instance, - type - ) // TODO mistake, should be separated into several hierarchies + val instance = stmt.instance.asExpr(ctx.addressSort) + .takeIf { !it.isFakeObject() } + ?: uncoveredInstance.asExpr(addressSort) + // TODO mistake, should be separated into several hierarchies + // or evalTypeEqual with several concrete types + memory.types.evalTypeEquals(instance, type) } constraint to block } From 754aa7e77126103bfad4b3f247c4f0d37ed57fb7 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 17:42:51 +0300 Subject: [PATCH 19/52] Remove mistakenly added code --- .../kotlin/org/usvm/machine/JcTypeSystem.kt | 22 ------------------- 1 file changed, 22 deletions(-) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt index 4600ffece..521e993e7 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt @@ -17,28 +17,6 @@ import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem import kotlin.time.Duration -open class A { - protected open fun foo() { - println("Hello") - } -} - -class B : A() { - override fun foo() { - println("Hello") - - } - - fun getsa() { - val method = this.javaClass.methods - } -} - -fun main() { - val a = B() - println(a.javaClass.declaredMethods.toList().joinToString("\n")) -} - class JcTypeSystem( private val cp: JcClasspath, override val typeOperationsTimeout: Duration From c9d6e86085ca159875fa9ce6f1e6d66fd4d407d2 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 17:44:14 +0300 Subject: [PATCH 20/52] Replace assert with path constraints update --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 094eeef93..afcaedf78 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -25,7 +25,9 @@ fun TsContext.mkTruthyExpr( val conjuncts = mutableListOf>() val possibleType = memory.types.getTypeStream(expr.asExpr(addressSort)).single() as FakeType - scope.assert(possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr)) // TODO add to path constraints instead + scope.doWithState { + pathConstraints += possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr) + } if (!possibleType.boolTypeExpr.isFalse) { conjuncts += ExprWithTypeConstraint( From b3a0ce941735d0aa0657be2f4bd56a358bb56fbb Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 17:45:30 +0300 Subject: [PATCH 21/52] Remove redundant hierarchy from the ExprResolver --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 2 -- .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 2 +- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index ab348e14d..4ba8ea51e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -102,7 +102,6 @@ import org.usvm.machine.types.AuxiliaryType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue import org.usvm.sizeSort -import org.usvm.util.EtsHierarchy import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -123,7 +122,6 @@ const val ADHOC_STRING__STRING = 2222.0 // 'string' class TsExprResolver( private val ctx: TsContext, - private val hierarchy: EtsHierarchy, private val scope: TsStepScope, private val localToIdx: (EtsMethod, EtsValue) -> Int, ) : EtsEntity.Visitor?> { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 36168797f..05300a8ad 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -499,7 +499,7 @@ class TsInterpreter( } private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver = - TsExprResolver(ctx, graph.hierarchy, scope, ::mapLocalToIdx) + TsExprResolver(ctx, scope, ::mapLocalToIdx) // (method, localName) -> idx private val localVarToIdx: MutableMap> = hashMapOf() From c5ffcb38c855b8aaf1b4fc17be36edb214cfd087 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 17:55:53 +0300 Subject: [PATCH 22/52] Fixes in TsExprResolver --- .../org/usvm/machine/expr/TsExprResolver.kt | 21 ++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 4ba8ea51e..e57351ec8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -16,6 +16,7 @@ import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsCastExpr import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr import org.jacodb.ets.model.EtsDivExpr @@ -66,6 +67,7 @@ import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsTypeOfExpr import org.jacodb.ets.model.EtsUnaryExpr import org.jacodb.ets.model.EtsUnaryPlusExpr +import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUndefinedConstant import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsUnsignedRightShiftExpr @@ -631,11 +633,16 @@ class TsExprResolver( ): UExpr? = with(ctx) { val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef scope.doWithState { + // If we don't know an enclosing class of the field, + // we add a type constraint that every type containing such field is fine pathConstraints += if (field.enclosingClass == EtsClassSignature.UNKNOWN) { memory.types.evalIsSubtype(resolvedAddr, AuxiliaryType(setOf(field.name))) } else { - // TODO error, field.enclosingClass.type - memory.types.evalIsSubtype(resolvedAddr, field.type) // TODO is it right? + // Otherwise, we can add a type constraint about the instance type. + // Probably, it's redundant since either both class and field + // know exactly their types or none of them. + val type = EtsClassType(field.enclosingClass) + memory.types.evalIsSubtype(resolvedAddr, type) } } @@ -756,7 +763,15 @@ class TsExprResolver( override fun visit(expr: EtsNewExpr): UExpr? = scope.calcOnState { with(ctx.scene) { - val resolvedType = projectAndSdkClasses.singleOrNull { it.name == expr.type.typeName }?.type ?: expr.type + // Try to resolve the concrete type if possible. + // Otherwise, create an object with UnclearRefType + val resolvedType = if (expr.type is EtsUnclearRefType) { + projectAndSdkClasses + .singleOrNull { it.name == expr.type.typeName }?.type + ?: expr.type + } else { + expr.type + } memory.allocConcrete(resolvedType) } } From 1fff782ab1c1294c0abde8d1b42c28eeb3e81cb8 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 29 Apr 2025 18:03:50 +0300 Subject: [PATCH 23/52] Small fixes in TsInterpreter --- .../org/usvm/machine/interpreter/TsInterpreter.kt | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 05300a8ad..e03d78fea 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -139,10 +139,12 @@ class TsInterpreter( // NOTE: USE '.callee' INSTEAD OF '.method' !!! - val instance = stmt.instance - checkNotNull(instance) + val instance = requireNotNull(stmt.instance) { "Virtual code invocation with null as an instance" } val concreteRef = scope.calcOnState { models.first().eval(instance) } + val uncoveredInstance = if (concreteRef.isFakeObject()) { + // We ignore the possibility of method call on primitives. + // Therefore, the fake object should be unwrapped. scope.doWithState { pathConstraints += concreteRef.getFakeType(scope).refTypeExpr } @@ -150,6 +152,8 @@ class TsInterpreter( } else { concreteRef } + + // Evaluate uncoveredInstance in a model to avoid too wide type streams later val resolvedInstance = scope.calcOnState { models.first().eval(uncoveredInstance) } val concreteMethods: MutableList = mutableListOf() @@ -159,7 +163,6 @@ class TsInterpreter( if (isAllocatedConcreteHeapRef(resolvedInstance)) { val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single() if (type is EtsClassType) { - // TODO: handle non-unique classes val classes = ctx.scene.projectAndSdkClasses.filter { it.name == type.typeName } if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } @@ -201,7 +204,8 @@ class TsInterpreter( val conditionsWithBlocks = concreteMethods.map { method -> val concreteCall = stmt.toConcrete(method) val block = { state: TsState -> state.newStmt(concreteCall) } - val type = method.enclosingClass!!.type + val type = requireNotNull(method.enclosingClass).type + val constraint = scope.calcOnState { val instance = stmt.instance.asExpr(ctx.addressSort) .takeIf { !it.isFakeObject() } From ab2709588ab4e7f4c8de581b18c00844ff31903e Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 14:16:27 +0300 Subject: [PATCH 24/52] Resolve arg type in getInitialState --- .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index e03d78fea..636b1ec16 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -570,8 +570,10 @@ class TsInterpreter( val resolvedParameterType = graph.cp .projectAndSdkClasses .singleOrNull { it.name == parameterType.typeName } + ?.type ?: parameterType - state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) + + state.pathConstraints += state.memory.types.evalIsSubtype(ref, resolvedParameterType) } if (parameterType is EtsUnionType || parameterType is EtsIntersectionType) { From e6429f604d6c7c89ca73253cefeb9610a86e8e9c Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 14:18:08 +0300 Subject: [PATCH 25/52] Auxiliary type fixes --- .../main/kotlin/org/usvm/machine/types/AuxiliaryType.kt | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt index 4bad8e022..6f23065e3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -1,14 +1,16 @@ package org.usvm.machine.types -import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsType -// TODO string name? +/** + * An auxiliary type is a type that is not directly represented in the TS class hierarchy. + * Can be used as a JS-like type containing set of properties. + */ class AuxiliaryType(val properties: Set) : EtsType { override fun accept(visitor: EtsType.Visitor): R { error("Should not be called") } override val typeName: String - get() = "AuxiliaryType" + get() = "AuxiliaryType: $properties" } \ No newline at end of file From e7eb2ece5893665dff32c06407b0cf3d936a00e7 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 14:22:54 +0300 Subject: [PATCH 26/52] Optimize imports --- usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 2 -- 1 file changed, 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index a2144ac5a..67ff06273 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -3,10 +3,8 @@ package org.usvm.util import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsScene -import kotlin.collections.flatten private typealias ClassName = String From cadaf1f99ed02ba17855ea35bb85a787d5d76779 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 14:25:22 +0300 Subject: [PATCH 27/52] Minor fixes --- usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 2 +- usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt | 1 - usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 2 -- 3 files changed, 1 insertion(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 67ff06273..37542eea3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -30,7 +30,7 @@ class EtsHierarchy(private val scene: EtsScene) { val classesWithTheSameSignature = classesWithTheSameName[superClassSignature] val superClasses = when { classesWithTheSameSignature != null -> listOf(classesWithTheSameSignature) - superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values + superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values1 else -> error("There is no class with name ${superClassSignature.name}") } val interfaces = currentClass.implementedInterfaces diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt index 1024aef83..3e879876d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt @@ -1,7 +1,6 @@ package org.usvm.samples.types import org.jacodb.ets.model.EtsScene -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.api.TsValue import org.usvm.util.TsMethodTestRunner diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 2733a9005..df98b84e1 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -13,7 +13,6 @@ import org.jacodb.ets.model.EtsNeverType import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsPrimitiveType -import org.jacodb.ets.model.EtsRef import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType @@ -189,7 +188,6 @@ open class TsTestStateResolver( return when (type) { // TODO add better support is EtsUnclearRefType -> { - val cls = ctx.scene.projectAndSdkClasses.single { it.name == type.typeName } resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef) } From 569bbfa3ff778c038f2a7bdc4f355281095c5cd7 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 14:25:44 +0300 Subject: [PATCH 28/52] Minor fixes --- usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 37542eea3..67ff06273 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -30,7 +30,7 @@ class EtsHierarchy(private val scene: EtsScene) { val classesWithTheSameSignature = classesWithTheSameName[superClassSignature] val superClasses = when { classesWithTheSameSignature != null -> listOf(classesWithTheSameSignature) - superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values1 + superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values else -> error("There is no class with name ${superClassSignature.name}") } val interfaces = currentClass.implementedInterfaces From 5b944ceb70f1dac6210769f0b91359abde57e004 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 16:06:15 +0300 Subject: [PATCH 29/52] Rebase fixes --- .../main/kotlin/org/usvm/machine/types/TsTypeSystem.kt | 2 +- .../test/kotlin/org/usvm/samples/types/ObjectUsage.kt | 8 ++++---- .../test/kotlin/org/usvm/samples/types/TypeStream.kt | 10 +++++----- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index c13fbbe8b..2c3814ac1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -178,7 +178,7 @@ class TsTypeSystem( else -> { if (type == EtsHierarchy.OBJECT_CLASS) { - return project.projectAndSdkClasses.asSequence().map { it.type } + return scene.projectAndSdkClasses.asSequence().map { it.type } } // TODO wrong usage of names if (type is EtsUnclearRefType) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt index 33c608f49..9a619d7ce 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt @@ -1,7 +1,7 @@ package org.usvm.samples.types import org.jacodb.ets.model.EtsScene -import org.usvm.api.TsValue +import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner import kotlin.test.Test @@ -13,10 +13,10 @@ class ObjectUsage : TsMethodTestRunner() { @Test fun `object as parameter`() { val method = getMethod(className, "objectAsParameter") - discoverProperties( + discoverProperties( method = method, - { value, r -> value is TsValue.TsClass && value.name == "Object" && r.number == 42.0 }, - { value, r -> value == TsValue.TsUndefined && r.number == -1.0 } + { value, r -> value is TsTestValue.TsClass && value.name == "Object" && r.number == 42.0 }, + { value, r -> value == TsTestValue.TsUndefined && r.number == -1.0 } ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt index 3e879876d..cbcbae38a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt @@ -2,7 +2,7 @@ package org.usvm.samples.types import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Test -import org.usvm.api.TsValue +import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner class TypeStream : TsMethodTestRunner() { @@ -13,7 +13,7 @@ class TypeStream : TsMethodTestRunner() { @Test fun `test an ancestor as argument`() { val method = getMethod(className, "ancestorId") - discoverProperties( + discoverProperties( method = method, { value, r -> r.name == value.name }, ) @@ -22,7 +22,7 @@ class TypeStream : TsMethodTestRunner() { @Test fun `test virtual invoke on an ancestor`() { val method = getMethod(className, "virtualInvokeForAncestor") - discoverProperties( + discoverProperties( method = method, { value, r -> value.name == "Parent" && r.number == 1.0 }, { value, r -> value.name == "FirstChild" && r.number == 2.0 }, @@ -33,7 +33,7 @@ class TypeStream : TsMethodTestRunner() { @Test fun `use unique field`() { val method = getMethod(className, "useUniqueField") - discoverProperties( + discoverProperties( method = method, invariants = arrayOf( { value, r -> value.name == "FirstChild" && r.number == 1.0 } @@ -44,7 +44,7 @@ class TypeStream : TsMethodTestRunner() { @Test fun `use non unique field`() { val method = getMethod(className, "useNonUniqueField") - discoverProperties( + discoverProperties( method = method, { value, r -> value.name == "Parent" && r.number == 1.0 }, { value, r -> value.name == "FirstChild" && r.number == 2.0 }, From 7aade229d4c2bc8e34dd326586c3b7115b9916a8 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 16:28:11 +0300 Subject: [PATCH 30/52] Fixes --- .../org/usvm/machine/expr/TsExprResolver.kt | 17 ++++++++++------- usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt | 5 +++++ 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index e57351ec8..3ad85e43c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -24,6 +24,7 @@ import org.jacodb.ets.model.EtsEntity import org.jacodb.ets.model.EtsEqExpr import org.jacodb.ets.model.EtsExpExpr import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsGtEqExpr import org.jacodb.ets.model.EtsGtExpr @@ -104,6 +105,7 @@ import org.usvm.machine.types.AuxiliaryType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue import org.usvm.sizeSort +import org.usvm.util.isResolved import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -633,16 +635,16 @@ class TsExprResolver( ): UExpr? = with(ctx) { val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef scope.doWithState { - // If we don't know an enclosing class of the field, - // we add a type constraint that every type containing such field is fine - pathConstraints += if (field.enclosingClass == EtsClassSignature.UNKNOWN) { - memory.types.evalIsSubtype(resolvedAddr, AuxiliaryType(setOf(field.name))) - } else { - // Otherwise, we can add a type constraint about the instance type. + pathConstraints += if (field.type.isResolved()) { + // If we know an enclosing class of the field, + // we can add a type constraint about the instance type. // Probably, it's redundant since either both class and field // know exactly their types or none of them. val type = EtsClassType(field.enclosingClass) memory.types.evalIsSubtype(resolvedAddr, type) + } else { + // Otherwise, we add a type constraint that every type containing such field is fine + memory.types.evalIsSubtype(resolvedAddr, AuxiliaryType(setOf(field.name))) } } @@ -677,6 +679,7 @@ class TsExprResolver( } // TODO: check 'field.type' vs 'etsField.type' + // TODO change it if (assertIsSubtype(expr, field.type)) { expr } else { @@ -765,7 +768,7 @@ class TsExprResolver( with(ctx.scene) { // Try to resolve the concrete type if possible. // Otherwise, create an object with UnclearRefType - val resolvedType = if (expr.type is EtsUnclearRefType) { + val resolvedType = if (expr.type.isResolved()) { projectAndSdkClasses .singleOrNull { it.name == expr.type.typeName }?.type ?: expr.type diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt index d9da0d155..d4458cc5a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -3,8 +3,10 @@ package org.usvm.util import io.ksmt.sort.KFp64Sort import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType import org.usvm.UBoolSort import org.usvm.UExpr import org.usvm.UHeapRef @@ -28,3 +30,6 @@ val EtsMethod.humanReadableSignature: String val params = parameters.joinToString(",") { it.type.toString() } return "${signature.enclosingClass.name}::$name($params):$returnType" } + +fun EtsType.isResolved(): Boolean = + this is EtsUnclearRefType || (this as? EtsClassType)?.signature?.file == EtsFileSignature.UNKNOWN From 25bfb3428378e16e9ff2c28a4e5829a4bcf20765 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 16:29:33 +0300 Subject: [PATCH 31/52] Change project availability check function --- usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt index ecddc2059..9fc8ea5c9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt @@ -22,7 +22,7 @@ class RunOnDemoCalcProject : TsMethodTestRunner() { @JvmStatic private fun projectAvailable(): Boolean { - return getResourcePathOrNull(PROJECT_PATH) != null + return getResourcePathOrNull(PROJECT_PATH) != null && getResourcePathOrNull(SDK_PATH) != null } } From 4114f86de1c0815e9c87ef79adb17a3f55b94273 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 30 Apr 2025 16:50:13 +0300 Subject: [PATCH 32/52] Remove redundant method --- .../org/usvm/machine/expr/TsExprResolver.kt | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 3ad85e43c..396f0b179 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -651,7 +651,7 @@ class TsExprResolver( val etsField = resolveEtsField(instance, field) val sort = typeToSort(etsField.type) - val expr = if (sort == unresolvedSort) { + if (sort == unresolvedSort) { val boolLValue = mkFieldLValue(boolSort, instanceRef, field) val fpLValue = mkFieldLValue(fp64Sort, instanceRef, field) val refLValue = mkFieldLValue(addressSort, instanceRef, field) @@ -677,14 +677,6 @@ class TsExprResolver( val lValue = mkFieldLValue(sort, instanceRef, field) scope.calcOnState { memory.read(lValue) } } - - // TODO: check 'field.type' vs 'etsField.type' - // TODO change it - if (assertIsSubtype(expr, field.type)) { - expr - } else { - null - } } override fun visit(value: EtsInstanceFieldRef): UExpr? = with(ctx) { @@ -818,11 +810,6 @@ class TsExprResolver( } // endregion - - // TODO incorrect implementation - private fun assertIsSubtype(expr: UExpr, type: EtsType): Boolean { - return true - } } class TsSimpleValueResolver( From c795f894e54ac7dce0e7f3ab1c8fdb87ff520e33 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Mon, 5 May 2025 13:33:01 +0300 Subject: [PATCH 33/52] Optimize imports --- .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 3 --- 1 file changed, 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 396f0b179..a1d9236b2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -15,7 +15,6 @@ import org.jacodb.ets.model.EtsBitOrExpr import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsCastExpr -import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -24,7 +23,6 @@ import org.jacodb.ets.model.EtsEntity import org.jacodb.ets.model.EtsEqExpr import org.jacodb.ets.model.EtsExpExpr import org.jacodb.ets.model.EtsFieldSignature -import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsGtEqExpr import org.jacodb.ets.model.EtsGtExpr @@ -68,7 +66,6 @@ import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsTypeOfExpr import org.jacodb.ets.model.EtsUnaryExpr import org.jacodb.ets.model.EtsUnaryPlusExpr -import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUndefinedConstant import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsUnsignedRightShiftExpr From ac2613592c2e87db5967f655c5cbf68bf871f383 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Mon, 5 May 2025 13:41:47 +0300 Subject: [PATCH 34/52] Minor updates --- .../org/usvm/machine/types/AuxiliaryType.kt | 2 +- .../org/usvm/machine/types/TsTypeSystem.kt | 17 ++++++++--------- .../test/kotlin/org/usvm/util/TsTestResolver.kt | 4 +--- 3 files changed, 10 insertions(+), 13 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt index 6f23065e3..9c4206b7a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -13,4 +13,4 @@ class AuxiliaryType(val properties: Set) : EtsType { override val typeName: String get() = "AuxiliaryType: $properties" -} \ No newline at end of file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 2c3814ac1..36eea9aee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -21,7 +21,7 @@ class TsTypeSystem( val scene: EtsScene, override val typeOperationsTimeout: Duration, val hierarchy: EtsHierarchy, - ) : UTypeSystem { +) : UTypeSystem { /** * @return true if [type] <: [supertype]. */ @@ -103,7 +103,7 @@ class TsTypeSystem( // TODO wrong type resolutions because of names val clazz = scene .projectAndSdkClasses - .singleOrNull() { it.type.typeName == type.typeName } + .singleOrNull { it.type.typeName == type.typeName } ?: error("TODO") val ancestors = hierarchy.getAncestor(clazz).map { it.type } @@ -130,19 +130,18 @@ class TsTypeSystem( is EtsPrimitiveType -> { types.isEmpty() } + is EtsClassType -> true is EtsUnclearRefType -> true is EtsArrayType -> TODO() else -> error("Unsupported class type: $type") } - // TODO is it right? /** * @return true if there is no type u distinct from [type] and subtyping [type]. */ override fun isFinal(type: EtsType): Boolean = type is EtsPrimitiveType - // TODO are there any non instantiable types? /** * @return true if [type] is instantiable, meaning it can be created via constructor. */ @@ -162,12 +161,10 @@ class TsTypeSystem( */ override fun findSubtypes(type: EtsType): Sequence { return when (type) { - is EtsPrimitiveType -> emptySequence() // TODO why??? - // TODO they should be direct inheritors, not all of them + is EtsPrimitiveType -> emptySequence() is EtsAnyType, is EtsUnknownType -> { - // scene.projectAndSdkClasses.asSequence().map { it.type } - error("") + error("Should not be called") } is AuxiliaryType -> { @@ -185,7 +182,9 @@ class TsTypeSystem( val classes = scene.projectAndSdkClasses.filter { it.type.typeName == type.typeName } classes.asSequence().flatMap { hierarchy.getInheritors(it) }.map { it.type } } else { - val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } ?: error("Cannot find class for $type") + val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } + ?: error("Cannot find class for $type") + // TODO take only direct inheritors hierarchy.getInheritors(clazz).asSequence().map { it.type } } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index df98b84e1..437db7e55 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -368,9 +368,7 @@ open class TsTestStateResolver( concreteRef: UConcreteHeapRef, heapRef: UHeapRef, ): TsTestValue.TsClass = with(ctx) { - val type = model.typeStreamOf(concreteRef).first() as? EtsRefType ?: run { - TODO() - } + val type = model.typeStreamOf(concreteRef).first() as? EtsRefType ?: error("Expected EtsRefType") val clazz = resolveClass(type) val properties = clazz.fields .filterNot { field -> From 29a69e5354c96def22e083c0fd885916c1d3a3c3 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 13:51:50 +0300 Subject: [PATCH 35/52] Rename shadowed variable --- .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 636b1ec16..a220bd1ed 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -207,12 +207,12 @@ class TsInterpreter( val type = requireNotNull(method.enclosingClass).type val constraint = scope.calcOnState { - val instance = stmt.instance.asExpr(ctx.addressSort) + val ref = stmt.instance.asExpr(ctx.addressSort) .takeIf { !it.isFakeObject() } ?: uncoveredInstance.asExpr(addressSort) // TODO mistake, should be separated into several hierarchies // or evalTypeEqual with several concrete types - memory.types.evalTypeEquals(instance, type) + memory.types.evalTypeEquals(ref, type) } constraint to block } From 0a941637278ebc42d769fbf77260795448d8162a Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 13:52:35 +0300 Subject: [PATCH 36/52] Format --- .../org/usvm/machine/expr/TsExprResolver.kt | 58 +++++++++---------- 1 file changed, 28 insertions(+), 30 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index a1d9236b2..467aa8060 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -171,7 +171,7 @@ class TsExprResolver( dependency0: EtsEntity, dependency1: EtsEntity, block: (UExpr, UExpr) -> T, - ):T? { + ): T? { val result0 = resolve(dependency0) ?: return null val result1 = resolve(dependency1) ?: return null return block(result0, result1) @@ -417,10 +417,10 @@ class TsExprResolver( error("Not supported $expr") } - override fun visit(expr: EtsInstanceOfExpr): UExpr? { - return scope.calcOnState { - val instance = resolve(expr.arg)?.asExpr(ctx.addressSort) ?: return@calcOnState null - memory.types.evalIsSubtype(instance, expr.checkType) + override fun visit(expr: EtsInstanceOfExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg)?.asExpr(addressSort) ?: return null + scope.calcOnState { + memory.types.evalIsSubtype(arg, expr.checkType) } } @@ -586,20 +586,20 @@ class TsExprResolver( // region ACCESS override fun visit(value: EtsArrayAccess): UExpr? = with(ctx) { - val instance = resolve(value.array)?.asExpr(ctx.addressSort) ?: return null - val index = resolve(value.index)?.asExpr(ctx.fp64Sort) ?: return null + val array = resolve(value.array)?.asExpr(addressSort) ?: return null + val index = resolve(value.index)?.asExpr(fp64Sort) ?: return null val bvIndex = mkFpToBvExpr( roundingMode = fpRoundingModeSortDefaultValue(), value = index, bvSize = 32, - isSigned = true - ) + isSigned = true, + ).asExpr(sizeSort) val lValue = mkArrayIndexLValue( - addressSort, - instance, - bvIndex.asExpr(ctx.sizeSort), - value.array.type as EtsArrayType + sort = addressSort, + ref = array, + index = bvIndex, + type = value.array.type as EtsArrayType ) val expr = scope.calcOnState { memory.read(lValue) } @@ -610,8 +610,8 @@ class TsExprResolver( private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { val neqNull = mkAnd( - mkHeapRefEq(instance, ctx.mkUndefinedValue()).not(), - mkHeapRefEq(instance, ctx.mkTsNullValue()).not() + mkHeapRefEq(instance, mkUndefinedValue()).not(), + mkHeapRefEq(instance, mkTsNullValue()).not() ) scope.fork( @@ -753,19 +753,17 @@ class TsExprResolver( // region OTHER - override fun visit(expr: EtsNewExpr): UExpr? = scope.calcOnState { - with(ctx.scene) { - // Try to resolve the concrete type if possible. - // Otherwise, create an object with UnclearRefType - val resolvedType = if (expr.type.isResolved()) { - projectAndSdkClasses - .singleOrNull { it.name == expr.type.typeName }?.type - ?: expr.type - } else { - expr.type - } - memory.allocConcrete(resolvedType) + override fun visit(expr: EtsNewExpr): UExpr? = with(ctx) { + // Try to resolve the concrete type if possible. + // Otherwise, create an object with UnclearRefType + val resolvedType = if (expr.type.isResolved()) { + scene.projectAndSdkClasses + .singleOrNull { it.name == expr.type.typeName }?.type + ?: expr.type + } else { + expr.type } + scope.calcOnState { memory.allocConcrete(resolvedType) } } override fun visit(expr: EtsNewArrayExpr): UExpr? = with(ctx) { @@ -777,10 +775,10 @@ class TsExprResolver( } val bvSize = mkFpToBvExpr( - fpRoundingModeSortDefaultValue(), - size.asExpr(fp64Sort), + roundingMode = fpRoundingModeSortDefaultValue(), + value = size.asExpr(fp64Sort), bvSize = 32, - isSigned = true + isSigned = true, ) val condition = mkAnd( From b176f3b32fdb31f1370b4e91d79f4273b63f0a7e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:09:37 +0300 Subject: [PATCH 37/52] Deterministic typeName --- usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt index 9c4206b7a..fb28d9a96 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -12,5 +12,5 @@ class AuxiliaryType(val properties: Set) : EtsType { } override val typeName: String - get() = "AuxiliaryType: $properties" + get() = "AuxiliaryType ${properties.toSortedSet()}" } From 9fccca09b9088c7b80dc5a3528a771269d95459f Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:10:22 +0300 Subject: [PATCH 38/52] Add toString for AuxiliaryType --- .../kotlin/org/usvm/machine/types/AuxiliaryType.kt | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt index fb28d9a96..5de660695 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -7,10 +7,14 @@ import org.jacodb.ets.model.EtsType * Can be used as a JS-like type containing set of properties. */ class AuxiliaryType(val properties: Set) : EtsType { + override val typeName: String + get() = "AuxiliaryType ${properties.toSortedSet()}" + + override fun toString(): String { + return typeName + } + override fun accept(visitor: EtsType.Visitor): R { error("Should not be called") } - - override val typeName: String - get() = "AuxiliaryType ${properties.toSortedSet()}" } From e53faef06e5cedad608fd902f7b210e778a0a06c Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:14:54 +0300 Subject: [PATCH 39/52] EOF --- usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index fd9828001..f50195b21 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -87,4 +87,4 @@ private fun tryGetSingleField( fun EtsClass.getAllFields(hierarchy: EtsHierarchy): List { return hierarchy.getAncestor(this).flatMap { it.fields } -} \ No newline at end of file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 67ff06273..c48f89eee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -76,4 +76,4 @@ class EtsHierarchy(private val scene: EtsScene) { ), ) } -} \ No newline at end of file +} From 169004e123fadd3dfa6f6de5ed7f76c872d19d2d Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:15:02 +0300 Subject: [PATCH 40/52] Format --- .../org/usvm/machine/types/TsTypeSystem.kt | 66 ++++++++++--------- 1 file changed, 35 insertions(+), 31 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 36eea9aee..2859a7436 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -73,7 +73,10 @@ class TsTypeSystem( typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) } - supertype == type -> true + supertype == type -> { + true + } + supertype == EtsUnknownType || supertype == EtsAnyType -> { true } @@ -127,10 +130,7 @@ class TsTypeSystem( */ override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when (type) { is AuxiliaryType -> true - is EtsPrimitiveType -> { - types.isEmpty() - } - + is EtsPrimitiveType -> types.isEmpty() is EtsClassType -> true is EtsUnclearRefType -> true is EtsArrayType -> TODO() @@ -152,41 +152,45 @@ class TsTypeSystem( if (type is EtsAnyType) { return false } - return true } /** * @return a sequence of **direct** inheritors of the [type]. */ - override fun findSubtypes(type: EtsType): Sequence { - return when (type) { - is EtsPrimitiveType -> emptySequence() - is EtsAnyType, - is EtsUnknownType -> { - error("Should not be called") - } + override fun findSubtypes(type: EtsType): Sequence = when (type) { + is EtsPrimitiveType -> { + emptySequence() + } - is AuxiliaryType -> { - scene.projectAndSdkClasses.filter { - it.getAllFields(hierarchy).mapTo(mutableSetOf()) { it.name }.containsAll(type.properties) - }.asSequence().map { it.type } // TODO get fields of ancestors - } + is EtsAnyType, is EtsUnknownType -> { + error("Should not be called") + } - else -> { - if (type == EtsHierarchy.OBJECT_CLASS) { - return scene.projectAndSdkClasses.asSequence().map { it.type } - } - // TODO wrong usage of names - if (type is EtsUnclearRefType) { - val classes = scene.projectAndSdkClasses.filter { it.type.typeName == type.typeName } - classes.asSequence().flatMap { hierarchy.getInheritors(it) }.map { it.type } - } else { - val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } - ?: error("Cannot find class for $type") - // TODO take only direct inheritors - hierarchy.getInheritors(clazz).asSequence().map { it.type } + is AuxiliaryType -> { + scene.projectAndSdkClasses + .asSequence() + .filter { + it.getAllFields(hierarchy) + .mapTo(mutableSetOf()) { it.name } + .containsAll(type.properties) } + .map { it.type } // TODO get fields of ancestors + } + + else -> { + if (type == EtsHierarchy.OBJECT_CLASS) { + return scene.projectAndSdkClasses.asSequence().map { it.type } + } + // TODO wrong usage of names + if (type is EtsUnclearRefType) { + val classes = scene.projectAndSdkClasses.filter { it.type.typeName == type.typeName } + classes.asSequence().flatMap { hierarchy.getInheritors(it) }.map { it.type } + } else { + val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } + ?: error("Cannot find class for $type") + // TODO take only direct inheritors + hierarchy.getInheritors(clazz).asSequence().map { it.type } } } } From 0efcc7a336041900a0925705a353f49441dce44f Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:20:05 +0300 Subject: [PATCH 41/52] Format --- .../org/usvm/machine/types/TsTypeSystem.kt | 68 ++++++++++--------- 1 file changed, 37 insertions(+), 31 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 2859a7436..54d838635 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -158,44 +158,50 @@ class TsTypeSystem( /** * @return a sequence of **direct** inheritors of the [type]. */ - override fun findSubtypes(type: EtsType): Sequence = when (type) { - is EtsPrimitiveType -> { - emptySequence() - } - - is EtsAnyType, is EtsUnknownType -> { - error("Should not be called") - } + override fun findSubtypes(type: EtsType): Sequence { + return when (type) { + is EtsPrimitiveType -> { + emptySequence() + } - is AuxiliaryType -> { - scene.projectAndSdkClasses - .asSequence() - .filter { - it.getAllFields(hierarchy) - .mapTo(mutableSetOf()) { it.name } - .containsAll(type.properties) - } - .map { it.type } // TODO get fields of ancestors - } + is EtsAnyType, is EtsUnknownType -> { + error("Should not be called") + } - else -> { - if (type == EtsHierarchy.OBJECT_CLASS) { - return scene.projectAndSdkClasses.asSequence().map { it.type } + is AuxiliaryType -> { + scene.projectAndSdkClasses + .asSequence() + .filter { + it.getAllFields(hierarchy) + .mapTo(mutableSetOf()) { it.name } + .containsAll(type.properties) + } + .map { it.type } // TODO get fields of ancestors } - // TODO wrong usage of names - if (type is EtsUnclearRefType) { - val classes = scene.projectAndSdkClasses.filter { it.type.typeName == type.typeName } - classes.asSequence().flatMap { hierarchy.getInheritors(it) }.map { it.type } - } else { - val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } - ?: error("Cannot find class for $type") - // TODO take only direct inheritors - hierarchy.getInheritors(clazz).asSequence().map { it.type } + + else -> { + if (type == EtsHierarchy.OBJECT_CLASS) { + return scene.projectAndSdkClasses.asSequence().map { it.type } + } + // TODO wrong usage of names + if (type is EtsUnclearRefType) { + scene.projectAndSdkClasses.asSequence() + .filter { it.type.typeName == type.typeName } + .flatMap { hierarchy.getInheritors(it) } + .map { it.type } + } else { + val cls = scene.projectAndSdkClasses.singleOrNull { it.type == type } + ?: error("Cannot find class for $type") + // TODO take only direct inheritors + hierarchy.getInheritors(cls).asSequence().map { it.type } + } } } } - private val topTypeStream by lazy { USupportTypeStream.from(this, EtsHierarchy.OBJECT_CLASS) } + private val topTypeStream by lazy { + USupportTypeStream.from(this, EtsHierarchy.OBJECT_CLASS) + } override fun topTypeStream(): UTypeStream = topTypeStream } From be6148506d8e1fd46176c70c7262d1586ed97093 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:25:07 +0300 Subject: [PATCH 42/52] Use mapValues --- usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index c48f89eee..63a416719 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -15,8 +15,7 @@ class EtsHierarchy(private val scene: EtsScene) { .mapValues { (_, classes) -> classes .groupBy { it.signature } - .map { it.key to it.value.single() } - .toMap() + .mapValues { it.value.single() } } } From ce11394355a8aaa1786e763846cda489b0bc6550 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:50:41 +0300 Subject: [PATCH 43/52] Add test with structural equality trick --- usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt | 9 +++++++++ usvm-ts/src/test/resources/samples/Call.ts | 9 +++++++++ 2 files changed, 18 insertions(+) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt index 14af11b04..2f69267f2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt @@ -270,6 +270,15 @@ class Call : TsMethodTestRunner() { { r -> r.number == 5.0 }, ) } + + @Test + fun `test structural equality trickery`() { + val method = getMethod(className, "structuralEqualityTrickery") + discoverProperties( + method = method, + { r -> r.number == 20.0 }, + ) + } } fun fib(n: Double): Double { diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts index b73267c82..243387976 100644 --- a/usvm-ts/src/test/resources/samples/Call.ts +++ b/usvm-ts/src/test/resources/samples/Call.ts @@ -152,6 +152,11 @@ class Call { let x = new ValueHolderWithPublicParameter(5); return x.value; } + + structuralEqualityTrickery(): number { + let x: A = makeA(); + return x.foo(); // 20 (!!!) from B::foo + } } class A { @@ -166,6 +171,10 @@ class B { } } +function makeA(): A { + return new B(); // hehe +} + namespace N1 { class C { foo(): number { From 29b383d934b36b4934ccf44b89bd8bcd6c3610ae Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:53:37 +0300 Subject: [PATCH 44/52] Format --- .../kotlin/org/usvm/machine/types/TsTypeSystem.kt | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 54d838635..6bb059606 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -183,18 +183,19 @@ class TsTypeSystem( if (type == EtsHierarchy.OBJECT_CLASS) { return scene.projectAndSdkClasses.asSequence().map { it.type } } + // TODO wrong usage of names if (type is EtsUnclearRefType) { - scene.projectAndSdkClasses.asSequence() + return scene.projectAndSdkClasses.asSequence() .filter { it.type.typeName == type.typeName } .flatMap { hierarchy.getInheritors(it) } .map { it.type } - } else { - val cls = scene.projectAndSdkClasses.singleOrNull { it.type == type } - ?: error("Cannot find class for $type") - // TODO take only direct inheritors - hierarchy.getInheritors(cls).asSequence().map { it.type } } + + val cls = scene.projectAndSdkClasses.singleOrNull { it.type == type } + ?: error("Cannot find class for type $type") + // TODO take only direct inheritors + hierarchy.getInheritors(cls).asSequence().map { it.type } } } } From 706dec8944d03b715b7c74dcc72283615d64d36c Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 14:57:44 +0300 Subject: [PATCH 45/52] Reuse docs from interface --- .../org/usvm/machine/types/TsTypeSystem.kt | 24 ++++--------------- 1 file changed, 4 insertions(+), 20 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index 6bb059606..d4df39ecd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -22,9 +22,6 @@ class TsTypeSystem( override val typeOperationsTimeout: Duration, val hierarchy: EtsHierarchy, ) : UTypeSystem { - /** - * @return true if [type] <: [supertype]. - */ override fun isSupertype(supertype: EtsType, type: EtsType): Boolean { return when { type is AuxiliaryType -> { @@ -33,13 +30,14 @@ class TsTypeSystem( return true } - // We think that only ref types contain fields, and ObjectClass is a top type for ref types + // We think that only ref types contain fields, + // and ObjectClass is a top type for ref types if (supertype == EtsHierarchy.OBJECT_CLASS) { return true } - // If we compare two auxiliary types, - // we should check if all fields of the first type are in the second type + // If we compare two auxiliary types, we should check + // if all fields of the first type are in the second type. if (supertype is AuxiliaryType) { return type.properties.all { it in supertype.properties } } @@ -123,11 +121,6 @@ class TsTypeSystem( } } - /** - * @return true if [types] and [type] can be supertypes for some type together. - * It is guaranteed that [type] is not a supertype for any type from [types] - * and that [types] have common subtype. - */ override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when (type) { is AuxiliaryType -> true is EtsPrimitiveType -> types.isEmpty() @@ -137,14 +130,8 @@ class TsTypeSystem( else -> error("Unsupported class type: $type") } - /** - * @return true if there is no type u distinct from [type] and subtyping [type]. - */ override fun isFinal(type: EtsType): Boolean = type is EtsPrimitiveType - /** - * @return true if [type] is instantiable, meaning it can be created via constructor. - */ override fun isInstantiable(type: EtsType): Boolean { if (type is EtsUnknownType) { return false @@ -155,9 +142,6 @@ class TsTypeSystem( return true } - /** - * @return a sequence of **direct** inheritors of the [type]. - */ override fun findSubtypes(type: EtsType): Sequence { return when (type) { is EtsPrimitiveType -> { From 2833ed6b2bb42c85bd00658e07fee3db4e9c495e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 15:09:00 +0300 Subject: [PATCH 46/52] Format test samples --- .../resources/samples/types/ObjectUsage.ts | 5 +++- .../resources/samples/types/TypeStream.ts | 24 +++++++++++-------- 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts index 909134322..38c8ae127 100644 --- a/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts +++ b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts @@ -1,3 +1,6 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + class ObjectUsage { objectAsParameter(object: Object): number { if (object == undefined) { @@ -6,4 +9,4 @@ class ObjectUsage { return 42 } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts index 9f8673024..26d0de229 100644 --- a/usvm-ts/src/test/resources/samples/types/TypeStream.ts +++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts @@ -1,10 +1,13 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + class TypeStream { ancestorId(ancestor: Parent): Parent { return ancestor } virtualInvokeForAncestor(ancestor: Parent): number { - var number = ancestor.virtualMethod(); + const number = ancestor.virtualMethod(); if (number == 100) { return 1 } else if (number == 200) { @@ -14,10 +17,10 @@ class TypeStream { } } - useUniqueField(value): number { - var number = value.firstChildField - - var virtualInvokeResult = value.virtualMethod() + useUniqueField(value: any): number { + // noinspection JSUnusedLocalSymbols + const _ = value.firstChildField; + const virtualInvokeResult = value.virtualMethod(); if (virtualInvokeResult == 100) { return -1 // unreachable } else if (virtualInvokeResult == 200) { @@ -27,9 +30,10 @@ class TypeStream { } } - useNonUniqueField(value): number { - var number = value.parentField - var virtualInvokeResult = value.virtualMethod() + useNonUniqueField(value: any): number { + // noinspection JSUnusedLocalSymbols + const _ = value.parentField; + const virtualInvokeResult = value.virtualMethod(); if (virtualInvokeResult == 100) { return 1 } else if (virtualInvokeResult == 200) { @@ -57,9 +61,9 @@ class FirstChild extends Parent { } class SecondChild extends Parent { - override virtualMethod(): number{ + override virtualMethod(): number { return 300; } secondChildField: number = 20 -} \ No newline at end of file +} From 4598ff4d17b1a42958e59ce5b200898a215c1c5c Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 15:13:28 +0300 Subject: [PATCH 47/52] Format --- usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 437db7e55..19113a7bf 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -29,8 +29,8 @@ import org.usvm.USort import org.usvm.api.GlobalFieldValue import org.usvm.api.TsParametersState import org.usvm.api.TsTest -import org.usvm.api.typeStreamOf import org.usvm.api.TsTestValue +import org.usvm.api.typeStreamOf import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUnresolvedSort @@ -329,9 +329,8 @@ open class TsTestStateResolver( TODO() } - // Special case for Object: - val name = when(refType) { + val name = when (refType) { is EtsClassType -> refType.signature.name is EtsUnclearRefType -> refType.name else -> error("Unsupported $refType") @@ -361,7 +360,7 @@ open class TsTestStateResolver( return classes.single() } - error("Could not resolve class: ${refType}") + error("Could not resolve class: $refType") } private fun resolveTsClass( From 0a229afba7241fe241293845e4a61a8830a4cf29 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 15:15:00 +0300 Subject: [PATCH 48/52] Use check --- usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 19113a7bf..df8c85fb8 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -367,7 +367,8 @@ open class TsTestStateResolver( concreteRef: UConcreteHeapRef, heapRef: UHeapRef, ): TsTestValue.TsClass = with(ctx) { - val type = model.typeStreamOf(concreteRef).first() as? EtsRefType ?: error("Expected EtsRefType") + val type = model.typeStreamOf(concreteRef).first() + check(type is EtsRefType) { "Expected EtsRefType, but got $type" } val clazz = resolveClass(type) val properties = clazz.fields .filterNot { field -> From 5e53644a5180b622adde1b3fddf7318b9803d57a Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 15:20:13 +0300 Subject: [PATCH 49/52] Format --- .../kotlin/org/usvm/util/TsTestResolver.kt | 30 +++++++++---------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index df8c85fb8..48b58be32 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -38,14 +38,12 @@ import org.usvm.machine.expr.extractBool import org.usvm.machine.expr.extractDouble import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState -import org.usvm.machine.types.FakeType import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue import org.usvm.mkSizeExpr import org.usvm.model.UModelBase import org.usvm.types.first -import org.usvm.types.single class TsTestResolver { fun resolve(method: EtsMethod, state: TsState): TsTest = with(state.ctx) { @@ -261,34 +259,31 @@ open class TsTestStateResolver( return emptyMap() } - private fun resolveFakeObject(expr: UConcreteHeapRef): TsTestValue { - val type = finalStateMemory.types.getTypeStream(expr.asExpr(ctx.addressSort)).single() as FakeType + private fun resolveFakeObject(expr: UConcreteHeapRef): TsTestValue = with(ctx) { + val type = expr.getFakeType(finalStateMemory) + // Note that everything about the details of a fake object + // we need to read from the final state of the memory, + // because they are allocated objects. return when { model.eval(type.boolTypeExpr).isTrue -> { - val lValue = ctx.getIntermediateBoolLValue(expr.address) - // Note that everything about details of fake object we need to read from final state of the memory - // since they are allocated objects + val lValue = getIntermediateBoolLValue(expr.address) val value = finalStateMemory.read(lValue) resolveExpr(model.eval(value), value, EtsBooleanType) } model.eval(type.fpTypeExpr).isTrue -> { - val lValue = ctx.getIntermediateFpLValue(expr.address) - // Note that everything about details of fake object we need to read from final state of the memory - // since they are allocated objects + val lValue = getIntermediateFpLValue(expr.address) val value = finalStateMemory.read(lValue) resolveExpr(model.eval(value), value, EtsNumberType) } model.eval(type.refTypeExpr).isTrue -> { - val lValue = ctx.getIntermediateRefLValue(expr.address) - // Note that everything about details of fake object we need to read from final state of the memory - // since they are allocated objects + val lValue = getIntermediateRefLValue(expr.address) val value = finalStateMemory.read(lValue) val ref = model.eval(value) // TODO mistake with signature, use TypeStream instead // TODO: replace `scene.classes.first()` with something meaningful - resolveExpr(ref, value, ctx.scene.projectAndSdkClasses.first().type) + resolveExpr(ref, value, scene.projectAndSdkClasses.first().type) } else -> error("Unsupported") @@ -397,9 +392,12 @@ open class TsTestStateResolver( TsTestValue.TsClass(clazz.name, properties) } - private var resolveMode: ResolveMode = ResolveMode.ERROR + internal var resolveMode: ResolveMode = ResolveMode.ERROR - fun withMode(resolveMode: ResolveMode, body: TsTestStateResolver.() -> R): R { + internal inline fun withMode( + resolveMode: ResolveMode, + body: TsTestStateResolver.() -> R, + ): R { val prevValue = this.resolveMode try { this.resolveMode = resolveMode From 41b336be01d582f4a3da43447e0f6e36d299925f Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 7 May 2025 15:46:19 +0300 Subject: [PATCH 50/52] Format --- .../org/usvm/machine/types/TsTypeSystem.kt | 18 +++++++++--------- .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 18 ++++++++---------- 2 files changed, 17 insertions(+), 19 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index d4df39ecd..352d5f27d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -62,13 +62,13 @@ class TsTypeSystem( return supertype.properties.isEmpty() } - val clazz = scene + val cls = scene .projectAndSdkClasses .singleOrNull { it.type.typeName == type.typeName } ?: TODO("For now we support only unique type resolution") - val typeFields = clazz.getAllFields(hierarchy) - - typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties) + cls.getAllFields(hierarchy) + .mapTo(hashSetOf()) { it.name } + .containsAll(supertype.properties) } supertype == type -> { @@ -155,9 +155,9 @@ class TsTypeSystem( is AuxiliaryType -> { scene.projectAndSdkClasses .asSequence() - .filter { - it.getAllFields(hierarchy) - .mapTo(mutableSetOf()) { it.name } + .filter { cls -> + cls.getAllFields(hierarchy) + .mapTo(hashSetOf()) { it.name } .containsAll(type.properties) } .map { it.type } // TODO get fields of ancestors @@ -176,10 +176,10 @@ class TsTypeSystem( .map { it.type } } - val cls = scene.projectAndSdkClasses.singleOrNull { it.type == type } + val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } ?: error("Cannot find class for type $type") // TODO take only direct inheritors - hierarchy.getInheritors(cls).asSequence().map { it.type } + hierarchy.getInheritors(clazz).asSequence().map { it.type } } } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 63a416719..0e896813e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -20,11 +20,10 @@ class EtsHierarchy(private val scene: EtsScene) { } private val ancestors: Map> by lazy { - val classes = scene.projectAndSdkClasses - val ancestors = classes.map { - it to generateSequence(listOf(it)) { currentClasses -> - currentClasses.flatMap { currentClass -> - val superClassSignature = currentClass.superClass ?: return@generateSequence null + scene.projectAndSdkClasses.associateWith { start -> + generateSequence(listOf(start)) { classes -> + classes.flatMap { current -> + val superClassSignature = current.superClass ?: return@generateSequence null val classesWithTheSameName = resolveMap.getValue(superClassSignature.name) val classesWithTheSameSignature = classesWithTheSameName[superClassSignature] val superClasses = when { @@ -32,20 +31,19 @@ class EtsHierarchy(private val scene: EtsScene) { superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values else -> error("There is no class with name ${superClassSignature.name}") } - val interfaces = currentClass.implementedInterfaces - require(interfaces.isEmpty()) { TODO() } + val interfaces = current.implementedInterfaces + require(interfaces.isEmpty()) { "Interfaces are not supported" } val resolvedInterfaces = interfaces.map { interfaceSignature -> - resolveMap[currentClass.name]?.get(interfaceSignature) ?: error("Unresolved interface") + resolveMap[current.name]?.get(interfaceSignature) ?: error("Unresolved interface") } superClasses + resolvedInterfaces } }.flatten().toSet() } - ancestors.toMap() } private val inheritors: MutableMap> by lazy { - val result = mutableMapOf>() + val result = hashMapOf>() ancestors.forEach { (key, value) -> value.forEach { clazz -> result.getOrPut(clazz) { hashSetOf() }.add(key) From 49a940e3a513b37a65e2506197d7553eee6f2342 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 13 May 2025 15:14:09 +0300 Subject: [PATCH 51/52] Add todoes --- .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 1 + usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 6 ++---- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index a220bd1ed..10999d18e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -143,6 +143,7 @@ class TsInterpreter( val concreteRef = scope.calcOnState { models.first().eval(instance) } val uncoveredInstance = if (concreteRef.isFakeObject()) { + // TODO support primitives calls // We ignore the possibility of method call on primitives. // Therefore, the fake object should be unwrapped. scope.doWithState { diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 0e896813e..0d4c12246 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -32,11 +32,9 @@ class EtsHierarchy(private val scene: EtsScene) { else -> error("There is no class with name ${superClassSignature.name}") } val interfaces = current.implementedInterfaces + // TODO support interfaces require(interfaces.isEmpty()) { "Interfaces are not supported" } - val resolvedInterfaces = interfaces.map { interfaceSignature -> - resolveMap[current.name]?.get(interfaceSignature) ?: error("Unresolved interface") - } - superClasses + resolvedInterfaces + superClasses } }.flatten().toSet() } From ee7ef444af1cb9ceec0747165405a52b024ba684 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 13 May 2025 15:15:56 +0300 Subject: [PATCH 52/52] Fix an issue with resolved class --- .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 467aa8060..8edf903b3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -15,6 +15,7 @@ import org.jacodb.ets.model.EtsBitOrExpr import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -632,7 +633,7 @@ class TsExprResolver( ): UExpr? = with(ctx) { val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef scope.doWithState { - pathConstraints += if (field.type.isResolved()) { + pathConstraints += if (field.enclosingClass != EtsClassSignature.UNKNOWN) { // If we know an enclosing class of the field, // we can add a type constraint about the instance type. // Probably, it's redundant since either both class and field