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 5030e7daf7..880e00f114 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/TsGraph.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsGraph.kt index e43802d70e..85e1776835 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 b498ab5988..d040ddd5b7 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 @@ -37,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/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt deleted file mode 100644 index 529be4894b..0000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt +++ /dev/null @@ -1,136 +0,0 @@ -package org.usvm.machine - -import org.jacodb.ets.model.EtsAnyType -import org.jacodb.ets.model.EtsBooleanType -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.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.UTypeSystem -import org.usvm.types.emptyTypeStream -import kotlin.time.Duration - -// TODO this is draft, should be replaced with real implementation -class TsTypeSystem( - val scene: EtsScene, - override val typeOperationsTimeout: Duration, -) : UTypeSystem { - - companion object { - // TODO: add more primitive types (string, etc.) once supported - val primitiveTypes = sequenceOf(EtsNumberType, EtsBooleanType) - } - - override fun isSupertype(supertype: EtsType, type: EtsType): Boolean = when { - supertype == type -> true - supertype == EtsUnknownType || supertype == EtsAnyType -> true - else -> false - } - - override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean = when { - type is EtsPrimitiveType -> types.isEmpty() - else -> false - } - - override fun isFinal(type: EtsType): Boolean = when (type) { - is EtsPrimitiveType -> true - is EtsUnknownType -> false - is EtsAnyType -> false - else -> false - } - - override fun isInstantiable(type: EtsType): Boolean = when (type) { - is EtsPrimitiveType -> true - is EtsUnknownType -> true - is EtsAnyType -> true - else -> false - } - - override fun findSubtypes(type: EtsType): Sequence = when (type) { - is EtsPrimitiveType -> emptySequence() - is EtsUnknownType -> primitiveTypes - is EtsAnyType -> primitiveTypes - else -> emptySequence() - } - - private val topTypeStream by lazy { TsTopTypeStream(this) } - - 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 } -} 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 76793125b6..afcaedf789 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)) + scope.doWithState { + pathConstraints += possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr) + } if (!possibleType.boolTypeExpr.isFalse) { conjuncts += ExprWithTypeConstraint( 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 dbfcbcf01b..8edf903b38 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,8 @@ 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 import org.jacodb.ets.model.EtsDivExpr @@ -82,6 +84,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 @@ -96,9 +99,11 @@ 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 +import org.usvm.util.isResolved import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -167,7 +172,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) @@ -413,9 +418,11 @@ class TsExprResolver( error("Not supported $expr") } - override fun visit(expr: EtsInstanceOfExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + 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) + } } // endregion @@ -580,20 +587,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) } @@ -604,8 +611,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( @@ -624,10 +631,25 @@ 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) { + // 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))) + } + } + 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) @@ -653,13 +675,6 @@ class TsExprResolver( val lValue = mkFieldLValue(sort, instanceRef, field) scope.calcOnState { memory.read(lValue) } } - - // TODO: check 'field.type' vs 'etsField.type' - if (assertIsSubtype(expr, field.type)) { - expr - } else { - null - } } override fun visit(value: EtsInstanceFieldRef): UExpr? = with(ctx) { @@ -739,8 +754,17 @@ class TsExprResolver( // region OTHER - override fun visit(expr: EtsNewExpr): UExpr? = scope.calcOnState { - memory.allocConcrete(expr.type) + 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) { @@ -752,10 +776,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( @@ -782,11 +806,6 @@ class TsExprResolver( } // endregion - - // TODO incorrect implementation - private fun assertIsSubtype(expr: UExpr, type: EtsType): Boolean { - return true - } } class TsSimpleValueResolver( 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 44a90df0eb..10999d18ed 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,18 +9,21 @@ 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 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 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 @@ -31,6 +34,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 +68,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 {} @@ -130,22 +135,35 @@ 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 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()) { + // TODO support primitives calls + // We ignore the possibility of method call on primitives. + // Therefore, the fake object should be unwrapped. + scope.doWithState { + pathConstraints += concreteRef.getFakeType(scope).refTypeExpr + } + concreteRef.extractRef(scope) + } 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() // 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 } if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } @@ -158,7 +176,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 { @@ -185,7 +205,17 @@ 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 = requireNotNull(method.enclosingClass).type + + val constraint = scope.calcOnState { + 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(ref, type) + } + constraint to block } scope.forkMulti(conditionsWithBlocks) } @@ -527,9 +557,30 @@ 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) + val resolvedParameterType = graph.cp + .projectAndSdkClasses + .singleOrNull { it.name == parameterType.typeName } + ?.type + ?: parameterType + + state.pathConstraints += state.memory.types.evalIsSubtype(ref, resolvedParameterType) + } + + if (parameterType is EtsUnionType || parameterType is EtsIntersectionType) { + TODO("Handle union/intersection types") + } + } val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) 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 0000000000..5de6606952 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -0,0 +1,20 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsType + +/** + * 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 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") + } +} 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 new file mode 100644 index 0000000000..352d5f27da --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -0,0 +1,192 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassType +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.types.USupportTypeStream +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 + +// TODO this is draft, should be replaced with real implementation +class TsTypeSystem( + val scene: EtsScene, + override val typeOperationsTimeout: Duration, + val hierarchy: EtsHierarchy, +) : UTypeSystem { + 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 } + } + + // 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) + val superTypeFieldNames = supertypeFields.mapTo(hashSetOf()) { it.name } + + type.properties.all { it in superTypeFieldNames } + } + + supertype is AuxiliaryType -> { + if (type is EtsUnknownType || type is EtsAnyType) { + return supertype.properties.isEmpty() + } + + if (type == EtsHierarchy.OBJECT_CLASS) { + return supertype.properties.isEmpty() + } + + val cls = scene + .projectAndSdkClasses + .singleOrNull { it.type.typeName == type.typeName } + ?: TODO("For now we support only unique type resolution") + cls.getAllFields(hierarchy) + .mapTo(hashSetOf()) { it.name } + .containsAll(supertype.properties) + } + + 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 + } + + 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 ancestors = hierarchy.getAncestor(clazz).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") + } + } + } + + 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") + } + + override fun isFinal(type: EtsType): Boolean = type is EtsPrimitiveType + + override fun isInstantiable(type: EtsType): Boolean { + if (type is EtsUnknownType) { + return false + } + if (type is EtsAnyType) { + return false + } + return true + } + + override fun findSubtypes(type: EtsType): Sequence { + return when (type) { + is EtsPrimitiveType -> { + emptySequence() + } + + is EtsAnyType, is EtsUnknownType -> { + error("Should not be called") + } + + is AuxiliaryType -> { + scene.projectAndSdkClasses + .asSequence() + .filter { cls -> + cls.getAllFields(hierarchy) + .mapTo(hashSetOf()) { 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) { + return scene.projectAndSdkClasses.asSequence() + .filter { it.type.typeName == type.typeName } + .flatMap { hierarchy.getInheritors(it) } + .map { it.type } + } + + val clazz = scene.projectAndSdkClasses.singleOrNull { it.type == type } + ?: error("Cannot find class for type $type") + // TODO take only direct inheritors + hierarchy.getInheritors(clazz).asSequence().map { it.type } + } + } + } + + 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/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index aa65b68fe6..f50195b219 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 } +} 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 0000000000..0d4c122461 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -0,0 +1,74 @@ +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.EtsFileSignature +import org.jacodb.ets.model.EtsScene + +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 } + .mapValues { it.value.single() } + } + } + + private val ancestors: Map> by lazy { + 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 { + classesWithTheSameSignature != null -> listOf(classesWithTheSameSignature) + superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values + else -> error("There is no class with name ${superClassSignature.name}") + } + val interfaces = current.implementedInterfaces + // TODO support interfaces + require(interfaces.isEmpty()) { "Interfaces are not supported" } + superClasses + } + }.flatten().toSet() + } + } + + private val inheritors: MutableMap> by lazy { + val result = hashMapOf>() + ancestors.forEach { (key, value) -> + value.forEach { clazz -> + result.getOrPut(clazz) { hashSetOf() }.add(key) + } + } + result + } + + fun getAncestor(clazz: EtsClass): Set { + return ancestors[clazz] ?: run { + error("TODO") + } + } + + fun getInheritors(clazz: EtsClass): Set { + return inheritors[clazz] ?: run { + error("TODO") + } + } + + companion object { + // TODO use real one + val OBJECT_CLASS = EtsClassType( + signature = EtsClassSignature( + name = "Object", + file = EtsFileSignature(projectName = "ES2015", fileName = "BuiltinClass") + ), + ) + } +} 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 d9da0d1558..d4458cc5a9 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 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 ecddc20596..9fc8ea5c9e 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 } } 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 76f3f3ba83..2f69267f2b 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") @@ -271,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/kotlin/org/usvm/samples/types/ObjectUsage.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt new file mode 100644 index 0000000000..9a619d7ce6 --- /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.TsTestValue +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 TsTestValue.TsClass && value.name == "Object" && r.number == 42.0 }, + { value, r -> value == TsTestValue.TsUndefined && r.number == -1.0 } + ) + } + +} \ 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 new file mode 100644 index 0000000000..cbcbae38a5 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt @@ -0,0 +1,54 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +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 }, + ) + } + + @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 + 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/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 5169801aa9..889dae0586 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 -> { @@ -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") @@ -323,36 +318,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() + check(type is EtsRefType) { "Expected EtsRefType, but got $type" } + val clazz = resolveClass(type) val properties = clazz.fields .filterNot { field -> field as EtsFieldImpl @@ -380,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 diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts index b73267c82a..2433879763 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 { 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 0000000000..38c8ae127a --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts @@ -0,0 +1,12 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class ObjectUsage { + objectAsParameter(object: Object): number { + if (object == undefined) { + return -1 + } + + return 42 + } +} 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 0000000000..26d0de229a --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts @@ -0,0 +1,69 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class TypeStream { + ancestorId(ancestor: Parent): Parent { + return ancestor + } + + virtualInvokeForAncestor(ancestor: Parent): number { + const number = ancestor.virtualMethod(); + if (number == 100) { + return 1 + } else if (number == 200) { + return 2 + } else { + return 3 + } + } + + useUniqueField(value: any): number { + // noinspection JSUnusedLocalSymbols + const _ = value.firstChildField; + const virtualInvokeResult = value.virtualMethod(); + if (virtualInvokeResult == 100) { + return -1 // unreachable + } else if (virtualInvokeResult == 200) { + return 1 + } else { + return -2 // unreachable + } + } + + useNonUniqueField(value: any): number { + // noinspection JSUnusedLocalSymbols + const _ = value.parentField; + const 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 +}