diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 03474c51d5..17f3f22abc 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "4ff7243d3a" + const val jacodb = "5889d3c784" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 026f3c35bb..cffa31ed41 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -6,6 +6,8 @@ import org.jacodb.ets.model.EtsAliasType import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsEnumValueType +import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsRefType @@ -29,10 +31,12 @@ import org.usvm.api.allocateConcreteRef import org.usvm.api.typeStreamOf import org.usvm.collection.field.UFieldLValue import org.usvm.isTrue +import org.usvm.machine.Constants.Companion.MAGIC_OFFSET import org.usvm.machine.expr.TsUndefinedSort import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.TsVoidSort import org.usvm.machine.expr.TsVoidValue +import org.usvm.machine.expr.tctx import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.EtsFakeType import org.usvm.memory.UReadOnlyMemory @@ -76,6 +80,16 @@ class TsContext( is EtsAnyType -> unresolvedSort is EtsUnknownType -> unresolvedSort is EtsAliasType -> typeToSort(type.originalType) + is EtsEnumValueType -> unresolvedSort + + is EtsGenericType -> { + if (type.constraint == null && type.defaultType == null) { + unresolvedSort + } else { + TODO("Not yet implemented") + } + } + else -> TODO("${type::class.simpleName} is not yet supported: $type") } @@ -152,6 +166,22 @@ class TsContext( } } + fun UHeapRef.unwrapRef(scope: TsStepScope): UHeapRef { + if (isFakeObject()) { + return extractRef(scope) + } + return this + } + + fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef = with(tctx) { + if (this@unwrapRefWithPathConstraint.isFakeObject()) { + scope.assert(getFakeType(scope).refTypeExpr) + extractRef(scope) + } else { + asExpr(addressSort) + } + } + fun createFakeObjectRef(): UConcreteHeapRef { val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET return mkConcreteHeapRef(address) @@ -235,7 +265,13 @@ class TsContext( } } -const val MAGIC_OFFSET = 1000000 +class Constants { + companion object { + const val STATIC_METHODS_FORK_LIMIT = 5 + const val MAGIC_OFFSET = 1000000 + } +} + enum class IntermediateLValueField { BOOL, FP, REF diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 43203c52ca..b90fda829f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -24,7 +24,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onCallWithUnresolvedArguments( simpleValueResolver: TsSimpleValueResolver, - stmt: EtsCallExpr, + expr: EtsCallExpr, scope: TsStepScope, ) { // default empty implementation 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 d82ac0ab88..b3d05421a7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -26,7 +26,9 @@ import org.usvm.statistics.collectors.TargetsReachedStatesCollector import org.usvm.statistics.constraints.SoftConstraintsObserver import org.usvm.statistics.distances.CfgStatisticsImpl import org.usvm.statistics.distances.PlainCallGraphStatistics +import org.usvm.stopstrategies.StopStrategy import org.usvm.stopstrategies.createStopStrategy +import org.usvm.util.TsStateVisualizer import org.usvm.util.humanReadableSignature import kotlin.time.Duration.Companion.seconds @@ -95,20 +97,36 @@ class TsMachine( val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) + if (tsOptions.enableVisualization) { + observers += TsStateVisualizer() + } + if (options.useSoftConstraints) { observers.add(SoftConstraintsObserver()) } val stepsStatistics = StepsStatistics() - val stopStrategy = createStopStrategy( - options, - targets, - timeStatisticsFactory = { timeStatistics }, - stepsStatisticsFactory = { stepsStatistics }, - coverageStatisticsFactory = { coverageStatistics }, - getCollectedStatesCount = { statesCollector.collectedStates.size } - ) + val stopStrategy = object : StopStrategy { + val strategy = createStopStrategy( + options, + targets, + timeStatisticsFactory = { timeStatistics }, + stepsStatisticsFactory = { stepsStatistics }, + coverageStatisticsFactory = { coverageStatistics }, + getCollectedStatesCount = { statesCollector.collectedStates.size }, + ) + + override fun shouldStop(): Boolean { + val result = strategy.shouldStop() + + if (result) { + logger.warn { "Stop strategy finished execution: ${strategy.stopReason()}" } + } + + return result + } + } observers.add(timeStatistics) observers.add(stepsStatistics) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index cb2d36d91b..950dd9aff7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -2,4 +2,5 @@ package org.usvm.machine data class TsOptions( val interproceduralAnalysis: Boolean = true, + val enableVisualization: Boolean = false, ) 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 082324130d..c061506033 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 @@ -17,6 +17,7 @@ import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr import org.jacodb.ets.model.EtsDivExpr @@ -54,6 +55,8 @@ import org.jacodb.ets.model.EtsPostIncExpr import org.jacodb.ets.model.EtsPreDecExpr import org.jacodb.ets.model.EtsPreIncExpr import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsRawType +import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsRemExpr import org.jacodb.ets.model.EtsRightShiftExpr import org.jacodb.ets.model.EtsStaticCallExpr @@ -83,11 +86,13 @@ import org.usvm.UBoolSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.UIteExpr import org.usvm.USort import org.usvm.api.allocateArray import org.usvm.api.evalTypeEquals import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type +import org.usvm.machine.Constants import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort @@ -106,8 +111,8 @@ import org.usvm.machine.types.EtsAuxiliaryType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue import org.usvm.sizeSort -import org.usvm.util.EtsFieldResolutionResult import org.usvm.util.EtsHierarchy +import org.usvm.util.EtsPropertyResolution import org.usvm.util.createFakeField import org.usvm.util.isResolved import org.usvm.util.mkArrayIndexLValue @@ -261,8 +266,44 @@ class TsExprResolver( } override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + val resolvedExpr = resolve(expr.arg) ?: return@with null + return when (resolvedExpr.sort) { + fp64Sort -> { + logger.error("Unsupported cast from fp ${expr.arg} to ${expr.type}") + TODO("Not yet implemented https://github.com/UnitTestBot/usvm/issues/299") + } + + boolSort -> { + logger.error("Unsupported cast from boolean ${expr.arg} to ${expr.type}") + TODO("Not yet implemented https://github.com/UnitTestBot/usvm/issues/299") + } + + addressSort -> { + scope.calcOnState { + val instance = resolvedExpr.asExpr(addressSort) + + if (instance.isFakeObject()) { + val fakeType = instance.getFakeType(scope) + pathConstraints += fakeType.refTypeExpr + val refValue = instance.extractRef(scope) + pathConstraints += memory.types.evalIsSubtype(refValue, expr.type) + return@calcOnState instance + } + + if (expr.type !is EtsRefType) { + logger.error("Unsupported cast from non-ref ${expr.arg} to ${expr.type}") + TODO("Not supported yet https://github.com/UnitTestBot/usvm/issues/299") + } + + pathConstraints += memory.types.evalIsSubtype(instance, expr.type) + instance + } + } + + else -> { + error("Unsupported cast from ${expr.arg} to ${expr.type}") + } + } } override fun visit(expr: EtsTypeOfExpr): UExpr? = with(ctx) { @@ -283,7 +324,28 @@ class TsExprResolver( condition = mkHeapRefEq(ref, mkUndefinedValue()), trueBranch = mkStringConstant("undefined", scope), falseBranch = mkIte( - condition = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) }, + condition = scope.calcOnState { + val unwrappedRef = ref.unwrapRefWithPathConstraint(scope) + + // TODO: adhoc: "expand" ITE + if (unwrappedRef is UIteExpr<*>) { + val trueBranch = unwrappedRef.trueBranch + val falseBranch = unwrappedRef.falseBranch + if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) { + val unwrappedTrueExpr = + trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) + val unwrappedFalseExpr = + falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) + return@calcOnState mkIte( + condition = unwrappedRef.condition, + trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType), + falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType), + ) + } + } + + memory.types.evalTypeEquals(unwrappedRef, EtsStringType) + }, trueBranch = mkStringConstant("string", scope), falseBranch = mkStringConstant("object", scope), ) @@ -291,7 +353,7 @@ class TsExprResolver( ) } - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } + logger.error { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } @@ -416,13 +478,17 @@ class TsExprResolver( } override fun visit(expr: EtsLtEqExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + val eq = resolve(EtsEqExpr(expr.left, expr.right)) ?: return null + val lt = resolve(EtsLtExpr(expr.left, expr.right)) ?: return null + + return ctx.mkOr(eq.asExpr(ctx.boolSort), lt.asExpr(ctx.boolSort)) } override fun visit(expr: EtsGtEqExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + val eq = resolve(EtsEqExpr(expr.left, expr.right)) ?: return null + val gt = resolve(EtsGtExpr(expr.left, expr.right)) ?: return null + + return ctx.mkOr(eq.asExpr(ctx.boolSort), gt.asExpr(ctx.boolSort)) } override fun visit(expr: EtsInExpr): UExpr? { @@ -479,7 +545,33 @@ class TsExprResolver( } if (expr.callee.name == "toString") { - return TODO() + return mkStringConstant("I am a string", scope) + } + + // TODO write tests https://github.com/UnitTestBot/usvm/issues/300 + if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) { + return scope.calcOnState { + val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null + val lengthLValue = mkArrayLengthLValue( + resolvedInstance, + EtsArrayType(EtsUnknownType, dimensions = 1) + ) + val length = memory.read(lengthLValue) + val newLength = mkBvAddExpr(length, 1.toBv()) + memory.write(lengthLValue, newLength, guard = ctx.trueExpr) + val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null + + // TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300 + val newIndexLValue = mkArrayIndexLValue( + resolvedArg.sort, + resolvedInstance, + length, + EtsArrayType(EtsUnknownType, dimensions = 1) + ) + memory.write(newIndexLValue, resolvedArg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr) + + newLength + } } return when (val result = scope.calcOnState { methodResult }) { @@ -497,7 +589,11 @@ class TsExprResolver( val resolved = resolve(expr.instance) ?: return null if (resolved.sort != addressSort) { - logger.warn { "Calling method on non-ref instance is not yet supported" } + if (expr.callee.name == "valueOf" && expr.args.isEmpty()) { + return resolve(expr.instance) + } + + logger.warn { "Calling method on non-ref instance is not yet supported, instruction $expr" } scope.assert(falseExpr) return null } @@ -528,6 +624,23 @@ class TsExprResolver( } } + if (expr.callee.name == "Boolean") { + check(expr.args.size == 1) { "Boolean constructor should have exactly one argument" } + return resolveAfterResolved(expr.args.single()) { + mkTruthyExpr(it, scope) + } + } + + if (expr.callee.name == "\$r") { + return scope.calcOnState { + val mockSymbol = memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership) + + scope.assert(mkEq(mockSymbol, ctx.mkTsNullValue()).not()) + + mockSymbol + } + } + return when (val result = scope.calcOnState { methodResult }) { is TsMethodResult.Success -> { scope.doWithState { methodResult = TsMethodResult.NoCall } @@ -539,21 +652,52 @@ class TsExprResolver( } is TsMethodResult.NoCall -> { - // TODO: spawn VirtualCall when method resolution fails - val method = resolveStaticMethod(expr.callee) + val resolutionResult = resolveStaticMethod(expr.callee) - if (method == null) { + if (resolutionResult is EtsPropertyResolution.Empty) { logger.error { "Could not resolve static call: ${expr.callee}" } scope.assert(falseExpr) return null } - val instance = scope.calcOnState { getStaticInstance(method.enclosingClass!!) } + // static virtual call + if (resolutionResult is EtsPropertyResolution.Ambiguous) { + val resolvedArgs = expr.args.map { resolve(it) ?: return null } + + val staticProperties = resolutionResult.properties.take( + Constants.STATIC_METHODS_FORK_LIMIT + ) + + val staticInstances = scope.calcOnState { + staticProperties.map { getStaticInstance(it.enclosingClass!!) } + } + + val concreteCalls = staticProperties.mapIndexed { index, value -> + TsConcreteMethodCallStmt( + callee = value, + instance = staticInstances[index], + args = resolvedArgs, + returnSite = scope.calcOnState { lastStmt } + ) + } + + val blocks = concreteCalls.map { + ctx.mkTrue() to { state: TsState -> state.newStmt(it) } + } + + scope.forkMulti(blocks) + + return null + } + + require(resolutionResult is EtsPropertyResolution.Unique) + + val instance = scope.calcOnState { getStaticInstance(resolutionResult.property.enclosingClass!!) } val resolvedArgs = expr.args.map { resolve(it) ?: return null } val concreteCall = TsConcreteMethodCallStmt( - callee = method, + callee = resolutionResult.property, instance = instance, args = resolvedArgs, returnSite = scope.calcOnState { lastStmt }, @@ -567,25 +711,28 @@ class TsExprResolver( private fun resolveStaticMethod( method: EtsMethodSignature, - ): EtsMethod? { + ): EtsPropertyResolution { // Perfect signature: if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) { - val classes = ctx.scene.projectAndSdkClasses.filter { it.name == method.enclosingClass.name } - if (classes.size != 1) return null + val classes = hierarchy.classesForType(EtsClassType(method.enclosingClass)) + if (classes.size > 1) { + val methods = classes.map { it.methods.single { it.name == method.name } } + return EtsPropertyResolution.create(methods) + } + + if (classes.isEmpty()) return EtsPropertyResolution.Empty + val clazz = classes.single() val methods = clazz.methods.filter { it.name == method.name } - if (methods.size != 1) return null - return methods.single() + return EtsPropertyResolution.create(methods) } // Unknown signature: val methods = ctx.scene.projectAndSdkClasses .flatMap { it.methods } .filter { it.name == method.name } - if (methods.size == 1) return methods.single() - // error("Cannot resolve method $method") - return null + return EtsPropertyResolution.create(methods) } override fun visit(expr: EtsPtrCallExpr): UExpr? { @@ -678,9 +825,11 @@ class TsExprResolver( } fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { + val ref = instance.unwrapRef(scope) + val neqNull = mkAnd( - mkHeapRefEq(instance, mkUndefinedValue()).not(), - mkHeapRefEq(instance, mkTsNullValue()).not() + mkHeapRefEq(ref, mkUndefinedValue()).not(), + mkHeapRefEq(ref, mkTsNullValue()).not(), ) scope.fork( @@ -718,20 +867,15 @@ class TsExprResolver( field: EtsFieldSignature, hierarchy: EtsHierarchy, ): UExpr? = with(ctx) { - val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef - scope.doWithState { - // If we accessed some field, we make an assumption that - // this field should present in the object. - // That's not true in the common case for TS, but that's the decision we made. - val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) - pathConstraints += memory.types.evalIsSubtype(resolvedAddr, auxiliaryType) - } + val resolvedAddr = instanceRef.unwrapRef(scope) val etsField = resolveEtsField(instance, field, hierarchy) val sort = when (etsField) { - is EtsFieldResolutionResult.Empty -> { - logger.error("Field $etsField not found, creating fake field") + is EtsPropertyResolution.Empty -> { + if (field.name !in listOf("i", "LogLevel")) { + logger.warn { "Field $field not found, creating fake field" } + } // If we didn't find any real fields, let's create a fake one. // It is possible due to mistakes in the IR or if the field was added explicitly // in the code. @@ -740,8 +884,17 @@ class TsExprResolver( addressSort } - is EtsFieldResolutionResult.Unique -> typeToSort(etsField.field.type) - is EtsFieldResolutionResult.Ambiguous -> unresolvedSort + is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type) + is EtsPropertyResolution.Ambiguous -> unresolvedSort + } + + scope.doWithState { + // If we accessed some field, we make an assumption that + // this field should present in the object. + // That's not true in the common case for TS, but that's the decision we made. + val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) + // assert is required to update models + scope.assert(memory.types.evalIsSubtype(resolvedAddr, auxiliaryType)) } if (sort == unresolvedSort) { @@ -763,18 +916,44 @@ class TsExprResolver( lValuesToAllocatedFakeObjects += refLValue to it } } + + // TODO ambiguous enum fields resolution + if (etsField is EtsPropertyResolution.Unique) { + val fieldType = etsField.property.type + if (fieldType is EtsRawType && fieldType.kind == "EnumValueType") { + val fakeType = fakeRef.getFakeType(scope) + pathConstraints += ctx.mkOr( + fakeType.fpTypeExpr, + fakeType.refTypeExpr + ) + + // val supertype = TODO() + // TODO add enum type as a constraint + // pathConstraints += memory.types.evalIsSubtype( + // ref, + // TODO() + // ) + } + } + memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr) fakeRef } } else { - val lValue = mkFieldLValue(sort, instanceRef, field) + val lValue = mkFieldLValue(sort, resolvedAddr, field) scope.calcOnState { memory.read(lValue) } } } override fun visit(value: EtsInstanceFieldRef): UExpr? = with(ctx) { - val instanceRef = resolve(value.instance)?.asExpr(addressSort) ?: return null + val instanceRefResolved = resolve(value.instance) ?: return null + if (instanceRefResolved.sort != addressSort) { + logger.error("InstanceFieldRef access on not address sort: $instanceRefResolved") + scope.assert(falseExpr) + return null + } + val instanceRef = instanceRefResolved.asExpr(addressSort) checkUndefinedOrNullPropertyRead(instanceRef) ?: return null @@ -849,6 +1028,7 @@ class TsExprResolver( scope.doWithState { markInitialized(clazz) pushSortsForArguments(instance = null, args = emptyList(), localToIdx) + registerCallee(currentStatement, initializer.cfg) callStack.push(initializer, currentStatement) memory.stack.push(arrayOf(instanceRef), initializer.localsCount) newStmt(initializer.cfg.stmts.first()) @@ -874,6 +1054,17 @@ class TsExprResolver( } else { expr.type } + + if (expr.type.typeName == "Boolean") { + val clazz = scene.sdkClasses.filter { it.name == "Boolean" }.maxBy { it.methods.size } + return@with scope.calcOnState { memory.allocConcrete(clazz.type) } + } + + if (expr.type.typeName == "Number") { + val clazz = scene.sdkClasses.filter { it.name == "Number" }.maxBy { it.methods.size } + return@with scope.calcOnState { memory.allocConcrete(clazz.type) } + } + scope.calcOnState { memory.allocConcrete(resolvedType) } } @@ -950,17 +1141,27 @@ class TsSimpleValueResolver( val localName = local.name // Check whether this local was already created or not if (localName in scope.calcOnState { addedArtificialLocals }) { - return mkFieldLValue(ctx.addressSort, globalObject, local.name) + val sort = ctx.typeToSort(local.type) + if (sort is TsUnresolvedSort) { + return mkFieldLValue(ctx.addressSort, globalObject, local.name) + } else { + return mkFieldLValue(sort, globalObject, local.name) + } } - logger.warn { "Cannot resolve local $local" } + logger.warn { "Cannot resolve local $local, creating a field of the global object" } - globalObject.createFakeField(localName, scope) scope.doWithState { addedArtificialLocals += localName } - return mkFieldLValue(ctx.addressSort, globalObject, local.name) + val sort = ctx.typeToSort(local.type) + if (sort is TsUnresolvedSort) { + globalObject.createFakeField(localName, scope) + return mkFieldLValue(ctx.addressSort, globalObject, local.name) + } else { + return mkFieldLValue(sort, globalObject, local.name) + } } val sort = scope.calcOnState { 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 5df7982eea..8ec9f2be2f 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 @@ -2,9 +2,11 @@ package org.usvm.machine.interpreter import io.ksmt.utils.asExpr import mu.KotlinLogging +import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsCallStmt import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsIfStmt @@ -14,7 +16,9 @@ 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.EtsNumberType import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsPtrCallExpr import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStaticFieldRef @@ -24,6 +28,7 @@ import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsThrowStmt import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue import org.jacodb.ets.model.EtsVoidType @@ -32,8 +37,10 @@ import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UAddressSort +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UInterpreter +import org.usvm.UIteExpr import org.usvm.api.allocateArrayInitialized import org.usvm.api.evalTypeEquals import org.usvm.api.makeSymbolicPrimitive @@ -64,8 +71,9 @@ import org.usvm.machine.types.mkFakeValue import org.usvm.machine.types.toAuxiliaryType import org.usvm.sizeSort import org.usvm.targets.UTargetsSet +import org.usvm.types.TypesResult import org.usvm.types.single -import org.usvm.util.EtsFieldResolutionResult +import org.usvm.util.EtsPropertyResolution import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -127,16 +135,18 @@ class TsInterpreter( is EtsCallStmt -> visitCallStmt(scope, stmt) is EtsThrowStmt -> visitThrowStmt(scope, stmt) is EtsNopStmt -> visitNopStmt(scope, stmt) - else -> error("Unknown stmt: $stmt") + else -> { + logger.error { "Unknown stmt: $stmt" } + scope.doWithState { + newStmt(graph.successors(stmt).single()) + } + } } } catch (e: Exception) { logger.error { - val s = e.stackTrace[0] - "Exception .(${s.fileName}:${s.lineNumber}): $e}" + "Exception: $e\n${e.stackTrace.take(5).joinToString("\n") { " $it" }}" } - - // Kill the state causing error - scope.assert(ctx.falseExpr) + return StepResult(forkedStates = emptySequence(), originalStateAlive = false) } return scope.stepResult() @@ -153,9 +163,7 @@ class TsInterpreter( // TODO support primitives calls // We ignore the possibility of method call on primitives. // Therefore, the fake object should be unwrapped. - scope.doWithState { - scope.assert(concreteRef.getFakeType(scope).refTypeExpr) - } + scope.assert(concreteRef.getFakeType(scope).refTypeExpr) concreteRef.extractRef(scope) } else { concreteRef @@ -171,7 +179,7 @@ class TsInterpreter( if (isAllocatedConcreteHeapRef(resolvedInstance)) { val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single() if (type is EtsClassType) { - val classes = scene.projectAndSdkClasses.filter { it.name == type.typeName } + val classes = graph.hierarchy.classesForType(type) if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } scope.assert(falseExpr) @@ -183,10 +191,8 @@ class TsInterpreter( return } val cls = classes.single() - val method = cls.methods - .singleOrNull { it.name == stmt.callee.name } - ?: TODO("Overloads are not supported yet") - concreteMethods += method + val suitableMethods = cls.methods.filter { it.name == stmt.callee.name } + concreteMethods += suitableMethods } else { logger.warn { "Could not resolve method: ${stmt.callee} on type: $type" @@ -197,19 +203,60 @@ class TsInterpreter( } else { val methods = resolveEtsMethods(stmt.callee) if (methods.isEmpty()) { - logger.warn { "Could not resolve method: ${stmt.callee}" } + if (stmt.callee.name !in listOf("then")) { + logger.warn { "Could not resolve method: ${stmt.callee}" } + } scope.assert(falseExpr) return } concreteMethods += methods } - logger.info { - "Preparing to fork on ${concreteMethods.size} methods: ${ - concreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" } - }" + val possibleTypes = scope.calcOnState { + models.first().typeStreamOf(resolvedInstance as UConcreteHeapRef).take(1000) + } + + if (possibleTypes !is TypesResult.SuccessfulTypesResult) { + error("TODO")// is it right? } - val conditionsWithBlocks = concreteMethods.map { method -> + + val possibleTypesSet = possibleTypes.types.toSet() + + if (possibleTypesSet.singleOrNull() == EtsAnyType) { + mockMethodCall(scope, stmt.callee) + scope.calcOnState { + newStmt(stmt.returnSite) + } + return@with + } + + val filteredPossibleTypesSet = possibleTypesSet - EtsAnyType + + val methodsDeclaringClasses = concreteMethods.mapNotNull { it.enclosingClass } // is it right? + val typeSystem = typeSystem() + + // take only possible classes with a corresponding method + val intersectedTypes = filteredPossibleTypesSet.filter { possibleType -> + methodsDeclaringClasses.any { typeSystem.isSupertype(it.type, possibleType) } + } + + // + val chosenMethods = intersectedTypes.flatMap { clazz -> + graph.hierarchy.classesForType(clazz as EtsRefType) + .asSequence() + // TODO wrong order, ancestors are unordered + .map { graph.hierarchy.getAncestors(it) } + .map { it.first { it.methods.any { it.name == stmt.callee.name } } } + .map { clazz to it.methods.first { it.name == stmt.callee.name } } + }.toList().take(10) // TODO check it + + // logger.info { + // "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${ + // limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" } + // }" + // } + + val conditionsWithBlocks = chosenMethods.mapIndexed { i, (clazz, method) -> val concreteCall = stmt.toConcrete(method) val block = { state: TsState -> state.newStmt(concreteCall) } val type = requireNotNull(method.enclosingClass).type @@ -218,9 +265,28 @@ class TsInterpreter( val ref = stmt.instance.asExpr(addressSort) .takeIf { !it.isFakeObject() } ?: uncoveredInstance.asExpr(addressSort) + + // TODO: adhoc: "expand" ITE + if (ref is UIteExpr<*>) { + val trueBranch = ref.trueBranch + val falseBranch = ref.falseBranch + if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) { + val unwrappedTrueExpr = trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) + val unwrappedFalseExpr = falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) + return@calcOnState mkIte( + condition = ref.condition, + trueBranch = memory.types.evalIsSubtype(unwrappedTrueExpr, type), + falseBranch = memory.types.evalIsSubtype(unwrappedFalseExpr, type), + ) + } + } + // TODO mistake, should be separated into several hierarchies // or evalTypeEqual with several concrete types - memory.types.evalTypeEquals(ref, type) + mkAnd( + memory.types.evalIsSubtype(ref, clazz), + memory.types.evalIsSupertype(ref, type) + ) } constraint to block } @@ -236,7 +302,7 @@ class TsInterpreter( val entryPoint = graph.entryPoints(stmt.callee).singleOrNull() if (entryPoint == null) { - logger.warn { "No entry point for method: ${stmt.callee}" } + // logger.warn { "No entry point for method: ${stmt.callee}, mocking the call" } // If the method doesn't have entry points, // we go through it, we just mock the call mockMethodCall(scope, stmt.callee.signature) @@ -247,6 +313,8 @@ class TsInterpreter( } scope.doWithState { + registerCallee(stmt.returnSite, stmt.callee.cfg) + val args = mutableListOf>() val numActual = stmt.args.size val numFormal = stmt.callee.parameters.size @@ -384,10 +452,20 @@ class TsInterpreter( scope ) - is TsMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) + is TsMethodResult.Success -> observer?.onAssignStatement( + exprResolver.simpleValueResolver, + stmt, + scope + ) + is TsMethodResult.TsException -> error("Exceptions must be processed earlier") } + if (it is EtsPtrCallExpr) { + mockMethodCall(scope, it.callee) + return + } + if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) { mockMethodCall(scope, it.callee) return @@ -482,14 +560,15 @@ class TsInterpreter( // If we access some field, we expect that the object must have this field. // It is not always true for TS, but we decided to process it so. val supertype = EtsAuxiliaryType(properties = setOf(lhv.field.name)) - pathConstraints += memory.types.evalIsSubtype(instance, supertype) + // assert is required to update models + scope.assert(memory.types.evalIsSubtype(instance, supertype)) } // If there is no such field, we create a fake field for the expr val sort = when (etsField) { - is EtsFieldResolutionResult.Empty -> unresolvedSort - is EtsFieldResolutionResult.Unique -> typeToSort(etsField.field.type) - is EtsFieldResolutionResult.Ambiguous -> unresolvedSort + is EtsPropertyResolution.Empty -> unresolvedSort + is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type) + is EtsPropertyResolution.Ambiguous -> unresolvedSort } if (sort == unresolvedSort) { @@ -501,7 +580,39 @@ class TsInterpreter( memory.write(lValue, fakeObject, guard = trueExpr) } else { val lValue = mkFieldLValue(sort, instance, lhv.field) - memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) + if (lValue.sort != expr.sort) { + if (expr.isFakeObject()) { + val lhvType = lhv.type + val value = when (lhvType) { + is EtsBooleanType -> { + scope.calcOnState { + pathConstraints += expr.getFakeType(scope).boolTypeExpr + expr.extractBool(scope) + } + } + + is EtsNumberType -> { + scope.calcOnState { + pathConstraints += expr.getFakeType(scope).fpTypeExpr + expr.extractFp(scope) + } + } + + else -> { + scope.calcOnState { + pathConstraints += expr.getFakeType(scope).refTypeExpr + expr.extractRef(scope) + } + } + } + + memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr) + } else { + TODO("Support enums fields") + } + } else { + memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) + } } } @@ -555,6 +666,11 @@ class TsInterpreter( return } + if (stmt.expr is EtsPtrCallExpr) { + mockMethodCall(scope, stmt.expr.callee) + return + } + if (tsOptions.interproceduralAnalysis) { val exprResolver = exprResolverWithScope(scope) exprResolver.resolve(stmt.expr) ?: return @@ -564,7 +680,7 @@ class TsInterpreter( } // intraprocedural analysis - mockMethodCall(scope, stmt.method.signature) + mockMethodCall(scope, stmt.expr.callee) } private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) { @@ -600,10 +716,7 @@ class TsInterpreter( local.name to localIdx }.toMap() } - map[local.name] ?: run { - logger.error("Local not declared: $local") - return null - } + map[local.name] } // Note: 'this' has index 'n' @@ -647,16 +760,25 @@ class TsInterpreter( val parameterType = param.type if (parameterType is EtsRefType) { - val resolvedParameterType = graph.cp - .projectAndSdkClasses - .singleOrNull { it.name == parameterType.typeName } - ?.type - ?: parameterType + val argLValue = mkRegisterStackLValue(addressSort, i) + val ref = state.memory.read(argLValue).asExpr(addressSort) + if (parameterType is EtsArrayType) { + state.pathConstraints += state.memory.types.evalTypeEquals(ref, parameterType) + return@forEachIndexed + } + + val resolvedParameterType = graph.hierarchy.classesForType(parameterType) + + if (resolvedParameterType.isEmpty()) { + logger.error("Cannot resolve class for parameter type: $parameterType") + return@forEachIndexed // TODO should be an error + } // Because of structural equality in TS we cannot determine the exact type // Therefore, we create information about the fields the type must consist - val auxiliaryType = (resolvedParameterType as? EtsClassType)?.toAuxiliaryType(graph.hierarchy) - ?: resolvedParameterType + val types = resolvedParameterType.mapNotNull { it.type.toAuxiliaryType(graph.hierarchy) } + val auxiliaryType = EtsUnionType(types) // TODO error + state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType) state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) @@ -691,7 +813,7 @@ class TsInterpreter( private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) { scope.doWithState { if (method.returnType is EtsVoidType) { - methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue) + methodResult = TsMethodResult.Success.MockedCall(method, ctx.mkUndefinedValue()) return@doWithState } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 722f86f07b..f5c8be7829 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -630,7 +630,7 @@ sealed interface TsBinaryOperator { // Strict equality checks that both sides are of the same type, // therefore they have to be processed in the other methods. // Otherwise, they would have the same sorts. - return lhs.ctx.mkFalse() + return mkFalse() } } @@ -975,52 +975,39 @@ sealed interface TsBinaryOperator { } } - data object Sub : TsBinaryOperator { - override fun TsContext.onBool( - lhs: UBoolExpr, - rhs: UBoolExpr, - scope: TsStepScope, - ): UExpr<*> { - return mkFpSubExpr(fpRoundingModeSortDefaultValue(), boolToFp(lhs), boolToFp(rhs)) - } - - override fun TsContext.onFp( + data object Sub : TsArithmeticOperator { + override fun TsContext.apply( lhs: UExpr, rhs: UExpr, - scope: TsStepScope, - ): UExpr<*> { + ): UExpr { return mkFpSubExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } + } - override fun TsContext.onRef( - lhs: UHeapRef, - rhs: UHeapRef, - scope: TsStepScope, - ): UExpr<*> { - return internalResolve(lhs, rhs, scope) + data object Mul : TsArithmeticOperator { + override fun TsContext.apply( + lhs: UExpr, + rhs: UExpr, + ): UExpr { + return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } + } - override fun TsContext.resolveFakeObject( - lhs: UExpr<*>, - rhs: UExpr<*>, - scope: TsStepScope, - ): UExpr<*> { - return internalResolve(lhs, rhs, scope) + data object Div : TsArithmeticOperator { + override fun TsContext.apply( + lhs: UExpr, + rhs: UExpr, + ): UExpr { + return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) } + } - override fun TsContext.internalResolve( - lhs: UExpr<*>, - rhs: UExpr<*>, - scope: TsStepScope, - ): UExpr<*> { - val lhsNumeric = mkNumericExpr(lhs, scope) - val rhsNumeric = mkNumericExpr(rhs, scope) - - return mkFpSubExpr( - fpRoundingModeSortDefaultValue(), - lhsNumeric, - rhsNumeric - ) + data object Rem : TsArithmeticOperator { + override fun TsContext.apply( + lhs: UExpr, + rhs: UExpr, + ): UExpr { + return mkFpRemExpr(lhs, rhs) } } @@ -1108,10 +1095,8 @@ sealed interface TsBinaryOperator { ): UExpr<*> { check(lhs.isFakeObject() || rhs.isFakeObject()) - return scope.calcOnState { - val lhsTruthyExpr = mkTruthyExpr(lhs, scope) - iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) - } + val lhsTruthyExpr = mkTruthyExpr(lhs, scope) + return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } override fun TsContext.internalResolve( @@ -1122,9 +1107,7 @@ sealed interface TsBinaryOperator { check(!lhs.isFakeObject() && !rhs.isFakeObject()) val lhsTruthyExpr = mkTruthyExpr(lhs, scope) - return scope.calcOnState { - iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) - } + return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs) } } @@ -1133,7 +1116,7 @@ sealed interface TsBinaryOperator { lhs: UBoolExpr, rhs: UBoolExpr, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { return mkAnd(lhs.not(), rhs) } @@ -1141,7 +1124,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { return mkFpLessExpr(lhs, rhs) } @@ -1149,7 +1132,7 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { TODO("Not yet implemented") } @@ -1157,7 +1140,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { TODO("Not yet implemented") } @@ -1165,7 +1148,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { TODO("Not yet implemented") } } @@ -1175,7 +1158,7 @@ sealed interface TsBinaryOperator { lhs: UBoolExpr, rhs: UBoolExpr, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { return mkAnd(lhs, rhs.not()) } @@ -1183,7 +1166,7 @@ sealed interface TsBinaryOperator { lhs: UExpr, rhs: UExpr, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { return mkFpGreaterExpr(lhs, rhs) } @@ -1191,7 +1174,7 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { TODO("Not yet implemented") } @@ -1199,7 +1182,7 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { TODO("Not yet implemented") } @@ -1207,64 +1190,17 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UBoolExpr { TODO("Not yet implemented") } } - data object Mul : TsBinaryOperator { - override fun TsContext.onBool( - lhs: UBoolExpr, - rhs: UBoolExpr, - scope: TsStepScope, - ): UExpr { - val left = mkNumericExpr(lhs, scope) - val right = mkNumericExpr(rhs, scope) - return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) - } - - override fun TsContext.onFp( + sealed interface TsArithmeticOperator : TsBinaryOperator { + fun TsContext.apply( lhs: UExpr, rhs: UExpr, - scope: TsStepScope, - ): UExpr { - return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) - } - - override fun TsContext.onRef( - lhs: UHeapRef, - rhs: UHeapRef, - scope: TsStepScope, - ): UExpr { - val left = mkNumericExpr(lhs, scope) - val right = mkNumericExpr(rhs, scope) - return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) - } + ): UExpr - override fun TsContext.resolveFakeObject( - lhs: UExpr<*>, - rhs: UExpr<*>, - scope: TsStepScope, - ): UExpr { - check(lhs.isFakeObject() || rhs.isFakeObject()) - val left = mkNumericExpr(lhs, scope) - val right = mkNumericExpr(rhs, scope) - return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) - } - - override fun TsContext.internalResolve( - lhs: UExpr<*>, - rhs: UExpr<*>, - scope: TsStepScope, - ): UExpr { - check(!lhs.isFakeObject() && !rhs.isFakeObject()) - val left = mkNumericExpr(lhs, scope) - val right = mkNumericExpr(rhs, scope) - return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right) - } - } - - data object Div : TsBinaryOperator { override fun TsContext.onBool( lhs: UBoolExpr, rhs: UBoolExpr, @@ -1272,7 +1208,7 @@ sealed interface TsBinaryOperator { ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) - return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) + return apply(left, right) } override fun TsContext.onFp( @@ -1280,7 +1216,7 @@ sealed interface TsBinaryOperator { rhs: UExpr, scope: TsStepScope, ): UExpr { - return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) + return apply(lhs, rhs) } override fun TsContext.onRef( @@ -1290,7 +1226,7 @@ sealed interface TsBinaryOperator { ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) - return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) + return apply(left, right) } override fun TsContext.resolveFakeObject( @@ -1300,7 +1236,7 @@ sealed interface TsBinaryOperator { ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) - return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) + return apply(left, right) } override fun TsContext.internalResolve( @@ -1310,51 +1246,7 @@ sealed interface TsBinaryOperator { ): UExpr { val left = mkNumericExpr(lhs, scope) val right = mkNumericExpr(rhs, scope) - return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right) - } - } - - data object Rem : TsBinaryOperator { - override fun TsContext.onBool( - lhs: UBoolExpr, - rhs: UBoolExpr, - scope: TsStepScope, - ): UExpr { - return internalResolve(lhs, rhs, scope) - } - - override fun TsContext.onFp( - lhs: UExpr, - rhs: UExpr, - scope: TsStepScope, - ): UExpr { - return internalResolve(lhs, rhs, scope) - } - - override fun TsContext.onRef( - lhs: UHeapRef, - rhs: UHeapRef, - scope: TsStepScope, - ): UExpr { - return internalResolve(lhs, rhs, scope) - } - - override fun TsContext.resolveFakeObject( - lhs: UExpr<*>, - rhs: UExpr<*>, - scope: TsStepScope, - ): UExpr { - return internalResolve(lhs, rhs, scope) - } - - override fun TsContext.internalResolve( - lhs: UExpr<*>, - rhs: UExpr<*>, - scope: TsStepScope, - ): UExpr { - val lhsExpr = mkNumericExpr(lhs, scope) - val rhsExpr = mkNumericExpr(rhs, scope) - return mkFpRemExpr(lhsExpr, rhsExpr) + return apply(left, right) } } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 38d8b66d18..00556fcf2b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -1,5 +1,6 @@ package org.usvm.machine.state +import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType @@ -31,6 +32,9 @@ import org.usvm.util.type * [lValuesToAllocatedFakeObjects] contains records of l-values that were allocated with newly created fake objects. * It is important for result interpreters to be able to restore the order of fake objects allocation and * their assignment to evaluated l-values. + * + * [discoveredCallees] is a map from each [EtsStmt] with EtsCallExpr inside and its parent block id to its + * analyzed callee CFG. This grows dynamically as you step through the calls. */ class TsState( ctx: TsContext, @@ -49,6 +53,7 @@ class TsState( val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)), val addedArtificialLocals: MutableSet = hashSetOf(), val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), + var discoveredCallees: UPersistentHashMap, EtsBlockCfg> = persistentHashMapOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -86,6 +91,16 @@ class TsState( localToSortStack.removeLast() } + fun registerCallee(stmt: EtsStmt, cfg: EtsBlockCfg) { + val parentId = stmt.location.method.cfg.blocks.indexOfFirst { it.statements.contains(stmt) } + .takeIf { it >= 0 } ?: error("Statement $stmt is not found in the method CFG") + + val key = stmt to parentId + if (key !in discoveredCallees) { + discoveredCallees = discoveredCallees.put(key, cfg, ownership) + } + } + fun pushSortsForArguments( instance: EtsLocal?, args: List, @@ -152,6 +167,7 @@ class TsState( globalObject = globalObject, addedArtificialLocals = addedArtificialLocals, lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(), + discoveredCallees = discoveredCallees, ) } 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 fb9206d07c..ee131ee94b 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,6 +62,8 @@ class TsTypeSystem( // "unknown" is the safe supertype: every value is assignable to unknown. if (unwrappedSupertype is EtsUnknownType) return true + // "any" is the universal subtype: any can be assigned to any type. + if (unwrappedType is EtsAnyType) return true // "never" is the universal subtype: never can be assigned to any type. if (unwrappedType is EtsNeverType) return true @@ -75,12 +77,12 @@ class TsTypeSystem( // As supertype, null/undefined only accept their own or any/unknown. if (unwrappedSupertype is EtsNullType) { // null supertype rules - return unwrappedType is EtsAnyType || unwrappedType is EtsUnknownType + return unwrappedType is EtsUnknownType } if (unwrappedSupertype is EtsUndefinedType) { // undefined supertype rules - return unwrappedType is EtsAnyType || unwrappedType is EtsUnknownType + return unwrappedType is EtsUnknownType } // Primitive types @@ -158,6 +160,13 @@ class TsTypeSystem( } if (unwrappedSupertype is EtsAuxiliaryType) { + if (unwrappedType is EtsArrayType) { + if (unwrappedSupertype.properties == setOf("length")) { + // Special case: array length is a structural property + return true + } + } + if (unwrappedType !is EtsClassType) return false // TODO arrays? val classes = hierarchy.classesForType(unwrappedType) @@ -191,8 +200,9 @@ class TsTypeSystem( if (classes.isEmpty() || superClasses.isEmpty()) return false // TODO log return classes.any { cls -> + val ancestors = hierarchy.getAncestors(cls) superClasses.any { superClass -> - superClass in hierarchy.getAncestor(cls) + superClass in ancestors } } } @@ -288,7 +298,7 @@ class TsTypeSystem( is EtsUnclearRefType, is EtsClassType -> if ((t as? EtsClassType)?.signature == EtsHierarchy.OBJECT_CLASS.signature) { // TODO change it - scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType + scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType + EtsAnyType } else { hierarchy.classesForType(t) .asSequence() 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 8b7884ec5c..695e79e21c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -16,12 +16,10 @@ fun TsContext.resolveEtsField( instance: EtsLocal?, field: EtsFieldSignature, hierarchy: EtsHierarchy, -): EtsFieldResolutionResult { +): EtsPropertyResolution { // Perfect signature: if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) { - val classes = scene.projectAndSdkClasses.filter { cls -> - cls.name == field.enclosingClass.name - } + val classes = hierarchy.classesForType(EtsClassType(field.enclosingClass)) if (classes.isEmpty()) { error("Cannot resolve class ${field.enclosingClass.name}") } @@ -31,7 +29,7 @@ fun TsContext.resolveEtsField( val clazz = classes.single() val fields = clazz.getAllFields(hierarchy).filter { it.name == field.name } if (fields.size == 1) { - return EtsFieldResolutionResult.create(fields.single()) + return EtsPropertyResolution.create(fields.single()) } } @@ -41,12 +39,12 @@ fun TsContext.resolveEtsField( when (instanceType) { is EtsClassType -> { val field = tryGetSingleField(scene, instanceType.signature.name, field.name, hierarchy) - if (field != null) return EtsFieldResolutionResult.create(field) + if (field != null) return EtsPropertyResolution.create(field) } is EtsUnclearRefType -> { val field = tryGetSingleField(scene, instanceType.typeName, field.name, hierarchy) - if (field != null) return EtsFieldResolutionResult.create(field) + if (field != null) return EtsPropertyResolution.create(field) } } } @@ -55,7 +53,7 @@ fun TsContext.resolveEtsField( cls.getAllFields(hierarchy).filter { it.name == field.name } } - return EtsFieldResolutionResult.create(fields) + return EtsPropertyResolution.create(fields) } private fun tryGetSingleField( @@ -88,11 +86,11 @@ private fun tryGetSingleField( } fun EtsClass.getAllFields(hierarchy: EtsHierarchy): List { - return hierarchy.getAncestor(this).flatMap { it.fields } + return hierarchy.getAncestors(this).flatMap { it.fields } } fun EtsClass.getAllMethods(hierarchy: EtsHierarchy): List { - return hierarchy.getAncestor(this).flatMap { it.methods } + return hierarchy.getAncestors(this).flatMap { it.methods } } fun EtsClass.getAllPropertiesCombined(hierarchy: EtsHierarchy): Set { @@ -104,7 +102,7 @@ fun EtsClass.getAllProperties(hierarchy: EtsHierarchy): Pair, val allFields = hashSetOf() val allMethods = hashSetOf() - val classes = hierarchy.getAncestor(this) + val classes = hierarchy.getAncestors(this) classes.forEach { val fieldNames = it.fields.map { it.name } @@ -118,23 +116,23 @@ fun EtsClass.getAllProperties(hierarchy: EtsHierarchy): Pair, return allFields to allMethods } -sealed class EtsFieldResolutionResult { - data class Unique(val field: EtsField) : EtsFieldResolutionResult() - data class Ambiguous(val fields: List) : EtsFieldResolutionResult() - data object Empty : EtsFieldResolutionResult() +sealed class EtsPropertyResolution { + data class Unique(val property: T) : EtsPropertyResolution() + data class Ambiguous(val properties: List) : EtsPropertyResolution() + data object Empty : EtsPropertyResolution() companion object { - fun create(field: EtsField) = Unique(field) + fun create(property: T) = Unique(property) - fun create(fields: List): EtsFieldResolutionResult { + fun create(properties: List): EtsPropertyResolution { return when { - fields.isEmpty() -> Empty - fields.size == 1 -> Unique(fields.single()) - else -> Ambiguous(fields) + properties.isEmpty() -> Empty + properties.size == 1 -> Unique(properties.single()) + else -> Ambiguous(properties) } } } } typealias EtsMethodName = String -typealias EtsFieldName = String \ No newline at end of file +typealias EtsFieldName = String 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 359c64a003..213a58b50e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -1,6 +1,7 @@ package org.usvm.util import mu.KotlinLogging +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType @@ -48,7 +49,9 @@ class EtsHierarchy(private val scene: EtsScene) { } } - logger.warn { "Ancestors map is built in $time ms" } + if (time > 100) { + logger.warn { "Ancestors map is built in $time ms" } + } return@lazy result } @@ -58,7 +61,7 @@ class EtsHierarchy(private val scene: EtsScene) { val signature = superClassSignature.copy(name = typeName) val classesWithTheSameName = resolveMap[typeName] ?: run { - logger.error("No class with $superClassSignature found in the Scene") + // logger.error("No class with $superClassSignature found in the Scene") return emptyList() } @@ -81,7 +84,7 @@ class EtsHierarchy(private val scene: EtsScene) { result } - fun getAncestor(clazz: EtsClass): Set { + fun getAncestors(clazz: EtsClass): Set { return ancestors[clazz] ?: run { error("TODO") } @@ -94,7 +97,13 @@ class EtsHierarchy(private val scene: EtsScene) { } fun classesForType(etsClassType: EtsRefType): Collection { - require(etsClassType is EtsClassType || etsClassType is EtsUnclearRefType) + if (etsClassType is EtsArrayType) { + return scene.sdkClasses.filter { it.name == "Array" } + } + + require(etsClassType is EtsClassType || etsClassType is EtsUnclearRefType) { + "Expected EtsClassType or EtsUnclearRefType, but got ${etsClassType::class.simpleName}" + } // We don't want to remove names like "$AC2$FieldAccess.createObject" val typeName = etsClassType.typeName.removeTrashFromTheName() diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt new file mode 100644 index 0000000000..4cec881225 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt @@ -0,0 +1,49 @@ +package org.usvm.util + +import org.jacodb.ets.utils.InterproceduralCfg +import org.jacodb.ets.utils.toHighlightedDotWithCalls +import org.usvm.dataflow.ts.util.toMap +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import java.nio.file.Path +import kotlin.io.path.createTempDirectory +import kotlin.io.path.writeText + +class TsStateVisualizer : TsInterpreterObserver, UMachineObserver { + override fun onStatePeeked(state: TsState) { + state.renderGraph() + } +} + +fun TsState.renderGraph() { + val graph = InterproceduralCfg(main = entrypoint.cfg, callees = discoveredCallees.toMap()) + val dot = graph.toHighlightedDotWithCalls( + pathStmts = pathNode.allStatements.toSet(), + currentStmt = currentStatement, + ) + + myRenderDot(dot) +} + +@Suppress("DEPRECATION") +fun myRenderDot( + dot: String, + outDir: Path = createTempDirectory(), + baseName: String = "cfg", + dotCmd: String = "dot", + format: String = "svg", // "svg", "png", "pdf" + viewerCmd: String? = when { + System.getProperty("os.name").startsWith("Mac") -> "open" + System.getProperty("os.name").startsWith("Win") -> "cmd /c start" + else -> "xdg-open" + }, +) { + val dotFile = outDir.resolve("$baseName.dot") + val svgFile = outDir.resolveSibling("$baseName.$format") + dotFile.writeText(dot) + Runtime.getRuntime().exec("$dotCmd $dotFile -T$format -o $svgFile").waitFor() + if (viewerCmd != null) { + Runtime.getRuntime().exec("$viewerCmd $svgFile").waitFor() + } +} 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 b05ba6d4ca..8315e690b7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -68,6 +68,12 @@ fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHe val fpValue = scope.calcOnState { memory.read(fpLValue) } val refValue = scope.calcOnState { memory.read(refLValue) } + with(ctx) { + if (refValue.isFakeObject()) { + return refValue + } + } + val fakeObject = ctx.mkFakeValue(scope, boolValue, fpValue, refValue) scope.doWithState { memory.write(lValue, fakeObject.asExpr(ctx.addressSort), guard = ctx.trueExpr) 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 9fc8ea5c9e..27a86eb396 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt @@ -1,11 +1,13 @@ package org.usvm.project import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.utils.getDeclaredLocals -import org.jacodb.ets.utils.getLocals +import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.jacodb.ets.utils.loadEtsProjectFromIR import org.junit.jupiter.api.condition.EnabledIf -import org.usvm.api.TsTestValue import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.TsMethodTestRunner @@ -22,60 +24,89 @@ class RunOnDemoCalcProject : TsMethodTestRunner() { @JvmStatic private fun projectAvailable(): Boolean { - return getResourcePathOrNull(PROJECT_PATH) != null && getResourcePathOrNull(SDK_PATH) != null + val isProjectPresent = getResourcePathOrNull(PROJECT_PATH) != null + val isSdkPreset = getResourcePathOrNull(SDK_PATH) != null + return isProjectPresent && isSdkPreset } } override val scene: EtsScene = run { val projectPath = getResourcePath(PROJECT_PATH) val sdkPath = getResourcePathOrNull(SDK_PATH) - ?: error("Could not load SDK from resources '$SDK_PATH'. Try running './gradlew generateSdkIR' to generate it.") + ?: error( + "Could not load SDK from resources '$SDK_PATH'. " + + "Try running './gradlew generateSdkIR' to generate it." + ) loadEtsProjectFromIR(projectPath, sdkPath) } @Test fun `test run on each method`() { - println("Total classes: ${scene.projectAndSdkClasses.size}") - for (clazz in scene.projectAndSdkClasses) { - println() - println("CLASS: ${clazz.name} in ${clazz.signature.file}") - for (method in clazz.methods) { - println() - println("METHOD: ${clazz.name}::${method.name}(${method.parameters.joinToString()})") - if (method.cfg.stmts.isEmpty()) { - println("CFG is empty") - continue - } - if (method.getLocals() != method.getDeclaredLocals()) { - println( - "Locals mismatch:\n getLocals() = ${ - method.getLocals().sortedBy { it.name } - }\n getDeclaredLocals() = ${ - method.getDeclaredLocals().sortedBy { it.name } - }" - ) - // continue + val exceptions = mutableListOf() + val classes = scene.projectClasses.filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + + println("Total classes: ${classes.size}") + + classes + .forEach { cls -> + val methods = cls.methods + .filterNot { it.cfg.stmts.isEmpty() } + .filterNot { it.isStatic } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { it.name == "build" } + .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { it.name == STATIC_INIT_METHOD_NAME } + .filterNot { it.name == CONSTRUCTOR_NAME } + + if (methods.isEmpty()) return@forEach + + runCatching { + val tsOptions = TsOptions() + TsMachine(scene, options, tsOptions).use { machine -> + val states = machine.analyze(methods) + states.let {} + } + }.onFailure { + exceptions += it } - discoverProperties(method = method) } + + val exc = exceptions.groupBy { it } + println("Total exceptions: ${exc.size}") + for (es in exc.values.sortedBy { it.size }.asReversed()) { + println("${es.first()}") } } @Test fun `test run on all methods`() { val methods = scene.projectClasses - .filterNot { it.name.startsWith("%AC") } - .flatMap { - it.methods + .filterNot { cls -> cls.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + .flatMap { cls -> + cls.methods .filterNot { it.cfg.stmts.isEmpty() } .filterNot { it.isStatic } - .filterNot { it.name.startsWith("%AM") } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } .filterNot { it.name == "build" } } + val tsOptions = TsOptions() TsMachine(scene, options, tsOptions).use { machine -> val states = machine.analyze(methods) states.let {} } } + + @Test + fun `test on particular method`() { + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "createKvStore" && it.enclosingClass?.name == "KvStoreModel" } + + val tsOptions = TsOptions() + TsMachine(scene, options, tsOptions).use { machine -> + val states = machine.analyze(listOf(method)) + states.let {} + } + } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt new file mode 100644 index 0000000000..bca881d048 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt @@ -0,0 +1,116 @@ +package org.usvm.project + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.condition.EnabledIf +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.getResourcePath +import org.usvm.util.getResourcePathOrNull +import kotlin.test.Test +import kotlin.time.Duration.Companion.seconds + +@EnabledIf("projectAvailable") +class RunOnDemoPhotosProject : TsMethodTestRunner() { + + companion object { + private const val PROJECT_PATH = "/projects/Demo_Photos/source/entry" + private const val SDK_PATH = "/sdk/ohos/etsir" + + @JvmStatic + private fun projectAvailable(): Boolean { + val isProjectPresent = getResourcePathOrNull(PROJECT_PATH) != null + val isSdkPreset = getResourcePathOrNull(SDK_PATH) != null + return isProjectPresent && isSdkPreset + } + } + + override val scene: EtsScene = run { + val projectPath = getResourcePath(PROJECT_PATH) + val sdkPath = getResourcePathOrNull(SDK_PATH) + ?: error( + "Could not load SDK from resources '$SDK_PATH'. " + + "Try running './gradlew generateSdkIR' to generate it." + ) + loadEtsProjectAutoConvert(projectPath, sdkPath) + } + + @Test + fun `test run on each method`() { + val exceptions = mutableListOf() + val classes = scene.projectClasses + .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + + println("Total classes: ${classes.size}") + + classes.forEach { cls -> + val methods = cls.methods + .filterNot { it.cfg.stmts.isEmpty() } + .filterNot { it.isStatic } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { it.name == "build" } + .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { it.name == STATIC_INIT_METHOD_NAME } + .filterNot { it.name == CONSTRUCTOR_NAME } + + if (methods.isEmpty()) return@forEach + + runCatching { + val tsOptions = TsOptions() + TsMachine(scene, options.copy(timeout = 120.seconds), tsOptions).use { machine -> + val states = machine.analyze(methods) + states.let {} + } + }.onFailure { + exceptions += it + } + } + + val exc = exceptions.groupBy { it } + println("Total exceptions: ${exc.size}") + for (es in exc.values.sortedBy { it.size }.asReversed()) { + println("${es.first()}") + } + } + + @Test + fun `test run on all methods`() { + val methods = scene.projectClasses + .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + .flatMap { cls -> + cls.methods + .filterNot { it.cfg.stmts.isEmpty() } + .filterNot { it.isStatic } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { it.name == "build" } + .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { it.name == STATIC_INIT_METHOD_NAME } + .filterNot { it.name == CONSTRUCTOR_NAME } + } + + val tsOptions = TsOptions() + TsMachine(scene, options, tsOptions).use { machine -> + val states = machine.analyze(methods) + states.let {} + } + } + + @Test + fun `test on particular method`() { + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "onSelect" && it.enclosingClass?.name == "AlbumSetPage" } + + val tsOptions = TsOptions() + TsMachine(scene, options, tsOptions).use { machine -> + val states = machine.analyze(listOf(method)) + states.let {} + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt deleted file mode 100644 index 40ab15d739..0000000000 --- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt +++ /dev/null @@ -1,82 +0,0 @@ -package org.usvm.project - -import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.utils.getDeclaredLocals -import org.jacodb.ets.utils.getLocals -import org.jacodb.ets.utils.loadEtsProjectFromIR -import org.junit.jupiter.api.condition.EnabledIf -import org.usvm.api.TsTestValue -import org.usvm.machine.TsMachine -import org.usvm.machine.TsOptions -import org.usvm.util.TsMethodTestRunner -import org.usvm.util.getResourcePath -import org.usvm.util.getResourcePathOrNull -import kotlin.test.Test - -@EnabledIf("projectAvailable") -// @Disabled -class RunOnPhotosProject : TsMethodTestRunner() { - - companion object { - private const val PROJECT_PATH = "/projects/Demo_Photos/etsir/entry" - private const val SDK_PATH = "/sdk/ohos/etsir" - - @JvmStatic - private fun projectAvailable(): Boolean { - return getResourcePathOrNull(PROJECT_PATH) != null && getResourcePathOrNull(SDK_PATH) != null - } - } - - override val scene: EtsScene = run { - val projectPath = getResourcePath(PROJECT_PATH) - val sdkPath = getResourcePathOrNull(SDK_PATH) - ?: error("Could not load SDK from resources '$SDK_PATH'. Try running './gradlew generateSdkIR' to generate it.") - loadEtsProjectFromIR(projectPath, sdkPath) - } - - @Test - fun `test run on each method`() { - println("Total classes: ${scene.projectAndSdkClasses.size}") - for (clazz in scene.projectAndSdkClasses) { - println() - println("CLASS: ${clazz.name} in ${clazz.signature.file}") - for (method in clazz.methods) { - println() - println("METHOD: ${clazz.name}::${method.name}(${method.parameters.joinToString()})") - if (method.cfg.stmts.isEmpty()) { - println("CFG is empty") - continue - } - if (method.getLocals() != method.getDeclaredLocals()) { - println( - "Locals mismatch:\n getLocals() = ${ - method.getLocals().sortedBy { it.name } - }\n getDeclaredLocals() = ${ - method.getDeclaredLocals().sortedBy { it.name } - }" - ) - // continue - } - discoverProperties(method = method) - } - } - } - - @Test - fun `test run on all methods`() { - val methods = scene.projectClasses - .filterNot { it.name.startsWith("%AC") } - .flatMap { - it.methods - .filterNot { it.cfg.stmts.isEmpty() } - .filterNot { it.isStatic } - .filterNot { it.name.startsWith("%AM") } - .filterNot { it.name == "build" } - } - val tsOptions = TsOptions() - TsMachine(scene, options, tsOptions).use { machine -> - val states = machine.analyze(methods) - states.let {} - } - } -} 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 2f69267f2b..4a0854c08d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt @@ -200,7 +200,6 @@ class Call : TsMethodTestRunner() { ) } - @Disabled("Calls to super are broken in IR") @Test fun `test virtual child`() { val method = getMethod(className, "callVirtualChild") @@ -210,6 +209,16 @@ class Call : TsMethodTestRunner() { ) } + @Disabled("Non-overridden virtual calls are not supported yet") + @Test + fun `test base call`() { + val method = getMethod(className, "callBaseMethod") + discoverProperties( + method = method, + { r -> r.number == 42.0 }, + ) + } + @Test fun `test virtual dispatch`() { val method = getMethod(className, "virtualDispatch") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt index d5d8cd3c84..71f8c04637 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/FieldAccess.kt @@ -120,4 +120,14 @@ class FieldAccess : TsMethodTestRunner() { { r -> r.number == 1.0 }, ) } + + @Test + fun `test read from nested fake objects`() { + val method = getMethod(className, "readFromNestedFakeObjects") + discoverProperties( + method = method, + { r -> r.number == 1.0 }, + { r -> r.number == 2.0 }, + ) + } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt index 70d8be3e9d..250690c3df 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt @@ -109,33 +109,4 @@ class AllocatedArrays : TsMethodTestRunner() { { r -> r is TsTestValue.TsException }, ) } - - @Test - fun `test readFakeObjectAndWriteFakeObject`() { - val method = getMethod(className, "readFakeObjectAndWriteFakeObject") - discoverProperties, TsTestValue, TsTestValue>( - method = method, - { x, y, r -> - val fst = x.values[0] - val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0 - val sndCondition = y is TsTestValue.TsNumber && y.number == 2.0 - val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y - - fstCondition && sndCondition && resultCondition - }, - { x, y, r -> - val fst = x.values[0] - val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0 - val sndCondition = y !is TsTestValue.TsNumber || y.number != 2.0 - val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y - - fstCondition && sndCondition && resultCondition - }, - { x, y, r -> - val fst = x.values[0] - val condition = fst !is TsTestValue.TsNumber || fst.number != 1.0 - condition && r is TsTestValue.TsArray<*> && r.values == x.values - }, - ) - } -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt index c808a9f989..e70dc93f38 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt @@ -18,11 +18,13 @@ class InputArrays : TsMethodTestRunner() { { x, r -> r is TsTestValue.TsException }, { x, r -> r as TsTestValue.TsNumber - (x.values[0] as TsTestValue.TsNumber).number == 1.0 && r.number == 1.0 + val x0 = x.values[0] as TsTestValue.TsNumber + x0.number == 1.0 && r.number == 1.0 }, { x, r -> r as TsTestValue.TsNumber - (x.values[0] as TsTestValue.TsNumber).number != 1.0 && r.number == 2.0 + val x0 = x.values[0] as TsTestValue.TsNumber + x0.number != 1.0 && r.number == 2.0 }, invariants = arrayOf( { _, r -> @@ -127,4 +129,33 @@ class InputArrays : TsMethodTestRunner() { }, ) } + + @Test + fun `test readFakeObjectAndWriteFakeObject`() { + val method = getMethod(className, "readFakeObjectAndWriteFakeObject") + discoverProperties, TsTestValue, TsTestValue>( + method = method, + { x, y, r -> + val fst = x.values[0] + val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0 + val sndCondition = y is TsTestValue.TsNumber && y.number == 2.0 + val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y + + fstCondition && sndCondition && resultCondition + }, + { x, y, r -> + val fst = x.values[0] + val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0 + val sndCondition = y !is TsTestValue.TsNumber || y.number != 2.0 + val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y + + fstCondition && sndCondition && resultCondition + }, + { x, y, r -> + val fst = x.values[0] + val condition = fst !is TsTestValue.TsNumber || fst.number != 1.0 + condition && r is TsTestValue.TsArray<*> && r.values == x.values + }, + ) + } } 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 cbcbae38a5..b63c97403f 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.RepeatedTest import org.junit.jupiter.api.Test import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner @@ -11,44 +12,106 @@ class TypeStream : TsMethodTestRunner() { override val scene: EtsScene = loadSampleScene(className, folderPrefix = "types") @Test - fun `test an ancestor as argument`() { - val method = getMethod(className, "ancestorId") - discoverProperties( + fun `test ancestor instanceof`() { + val method = getMethod(className, "instanceOf") + discoverProperties( method = method, - { value, r -> r.name == value.name }, + { x, r -> + x.name == "FirstChild" && r.number == 1.0 + }, + { x, r -> + x.name == "SecondChild" && r.number == 2.0 + }, + { x, r -> + x.name == "Parent" && r.number == 3.0 + }, + invariants = arrayOf( + { x, r -> + x.name in listOf("Parent", "FirstChild", "SecondChild") + }, + { _, r -> + r.number in listOf(1.0, 2.0, 3.0) + }, + { _, r -> r.number != -1.0 } + ) ) } @Test fun `test virtual invoke on an ancestor`() { - val method = getMethod(className, "virtualInvokeForAncestor") + val method = getMethod(className, "virtualInvokeOnAncestor") 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 }, + { x, r -> + x.name == "FirstChild" && r.number == 1.0 + }, + { x, r -> + x.name == "SecondChild" && r.number == 2.0 + }, + { x, r -> + x.name == "Parent" && r.number == 3.0 + }, + invariants = arrayOf( + { x, r -> + x.name in listOf("Parent", "FirstChild", "SecondChild") + }, + { _, r -> + r.number in listOf(1.0, 2.0, 3.0) + }, + { _, r -> r.number != -1.0 } + ) ) } - @Test + @RepeatedTest(10, failureThreshold = 1) fun `use unique field`() { val method = getMethod(className, "useUniqueField") - discoverProperties( + discoverProperties( method = method, + { x, r -> + x as TsTestValue.TsClass + r as TsTestValue.TsNumber + x.name == "FirstChild" && r.number == 1.0 + }, invariants = arrayOf( - { value, r -> value.name == "FirstChild" && r.number == 1.0 } + { x, _ -> + x !is TsTestValue.TsClass || x.name == "FirstChild" + }, + { _, r -> + r !is TsTestValue.TsNumber || r.number == 1.0 + }, ) ) } - @Test + @RepeatedTest(10, failureThreshold = 1) 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 }, - { value, r -> value.name == "SecondChild" && r.number == 3.0 }, + { x, r -> + x as TsTestValue.TsClass + r as TsTestValue.TsNumber + x.name == "FirstChild" && r.number == 1.0 + }, + { x, r -> + x as TsTestValue.TsClass + r as TsTestValue.TsNumber + x.name == "SecondChild" && r.number == 2.0 + }, + { x, r -> + x as TsTestValue.TsClass + r as TsTestValue.TsNumber + x.name == "Parent" && r.number == 3.0 + }, + invariants = arrayOf( + { _, r -> + r !is TsTestValue.TsNumber || r.number in listOf(1.0, 2.0, 3.0) + }, + { _, r -> + r !is TsTestValue.TsNumber || r.number != -1.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 58d5b1702c..ce5198b8f7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -31,6 +31,7 @@ import org.usvm.test.util.checkers.AnalysisResultsNumberMatcher import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import kotlin.reflect.KClass import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds typealias CoverageChecker = (TsMethodCoverage) -> Boolean @@ -328,10 +329,11 @@ abstract class TsMethodTestRunner : TestRunner val states = machine.analyze(listOf(method)) - states.map { state -> + val resolved = states.map { state -> val resolver = TsTestResolver() resolver.resolve(method, state) } + resolved } } @@ -340,7 +342,7 @@ abstract class TsMethodTestRunner : TestRunner { val lValue = getIntermediateRefLValue(expr.address) val value = finalStateMemory.read(lValue) - val ref = model.eval(value) - resolveExpr(ref) + resolveExpr(model.eval(value)) } else -> error("Unsupported") @@ -490,19 +487,6 @@ open class TsTestStateResolver( internal var resolveMode: ResolveMode = ResolveMode.ERROR - internal inline fun withMode( - resolveMode: ResolveMode, - body: TsTestStateResolver.() -> R, - ): R { - val prevValue = this.resolveMode - try { - this.resolveMode = resolveMode - return body() - } finally { - this.resolveMode = prevValue - } - } - fun evaluateInModel(expr: UExpr): UExpr { return model.eval(expr) } @@ -518,3 +502,16 @@ open class TsTestStateResolver( enum class ResolveMode { MODEL, CURRENT, ERROR } + +internal inline fun S.withMode( + resolveMode: ResolveMode, + body: S.() -> R, +): R { + val prevValue = this.resolveMode + try { + this.resolveMode = resolveMode + return body() + } finally { + this.resolveMode = prevValue + } +} diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts index 2433879763..218800ff1d 100644 --- a/usvm-ts/src/test/resources/samples/Call.ts +++ b/usvm-ts/src/test/resources/samples/Call.ts @@ -2,86 +2,92 @@ // noinspection JSUnusedGlobalSymbols class Call { + static fifty(): number { + return 50; + } + callSimple(): number { - return this.fortyTwo() + return this.fortyTwo(); } fortyTwo(): number { - return 42 + return 42; } fib(n: number): number { - if (n != n) return 0 - if (n < 0) return -1 - if (n > 10) return -100 - if (n == 0) return 1 - if (n == 1) return 1 - return this.fib(n - 1) + this.fib(n - 2) + if (n != n) return 0; + if (n < 0) return -1; + if (n > 10) return -100; + if (n == 0) return 1; + if (n == 1) return 1; + return this.fib(n - 1) + this.fib(n - 2); } callConcrete(): number { - let x = new A() - return x.foo() + let x = new A(); + return x.foo(); } callHidden(): number { let x: any = new B(); - return x.foo() + return x.foo(); } f(x: any, ...args: any[]): number { - if (x == undefined) return 0 - return args.length + 1 + if (x == undefined) return 0; + return args.length + 1; } callNoVararg(): number { - return this.f(5) // 1 + return this.f(5); // 1 } callVararg1(): number { - return this.f(5, 10) // 2 + return this.f(5, 10); // 2 } callVararg2(): number { - return this.f(5, 10, 20) // 3 + return this.f(5, 10, 20); // 3 } callVarargArray(): number { - return this.f(5, [10, 20]) // 2 + return this.f(5, [10, 20]); // 2 } g(x: any, y: any): number { - if (x == undefined) return 0 - if (y == undefined) return 1 - return 2 + if (x == undefined) return 0; + if (y == undefined) return 1; + return 2; } callNormal(): number { - return this.g(5, 10) // 2 + return this.g(5, 10); // 2 } callSingle(): number { - return this.g(5) // 1 + return this.g(5); // 1 } callNone(): number { - return this.g() // 0 + return this.g(); // 0 } callUndefined(): number { - return this.g(undefined, 20) // 0 + return this.g(undefined, 20); // 0 } callExtra(): number { - return this.g(5, 10, 20) // 2 + return this.g(5, 10, 20); // 2 } overloaded(a: number): number; + overloaded(a: string): number; + overloaded(a: any): number { - if (typeof a === 'number') return 1 - if (typeof a === 'string') return 2 - return -1 + if (typeof a === 'number') return 1; + if (typeof a === 'string') return 2; + return -1; } callOverloadedNumber(): number { @@ -96,10 +102,6 @@ class Call { return new N1.C().foo(); } - static fifty(): number { - return 50; - } - callStatic(): number { return Call.fifty(); } @@ -118,6 +120,11 @@ class Call { return obj.virtualMethod(); // 200 } + callBaseMethod(): number { + let obj: Child = new Child(); + return obj.baseMethod(); // 42 + } + virtualDispatch(obj: Parent): number { if (obj instanceof Child) { return obj.virtualMethod(); // 200 @@ -161,13 +168,13 @@ class Call { class A { foo(): number { - return 10 + return 10; } } class B { foo(): number { - return 20 + return 20; } } @@ -178,7 +185,7 @@ function makeA(): A { namespace N1 { class C { foo(): number { - return 30 + return 30; } } } @@ -186,7 +193,7 @@ namespace N1 { namespace N2 { class C { foo(): number { - return 40 + return 40; } } } @@ -195,9 +202,17 @@ class Parent { virtualMethod(): number { return 100; } + + baseMethod(): number { + return 42; + } } class Child extends Parent { + constructor() { + // super(); + } + override virtualMethod(): number { return 200; } diff --git a/usvm-ts/src/test/resources/samples/FieldAccess.ts b/usvm-ts/src/test/resources/samples/FieldAccess.ts index d65eff3762..fb7e95b3eb 100644 --- a/usvm-ts/src/test/resources/samples/FieldAccess.ts +++ b/usvm-ts/src/test/resources/samples/FieldAccess.ts @@ -47,30 +47,26 @@ class FieldAccess { } createWithField(): number { - return {a: 15}.a; + return { a: 15 }.a; } factoryCreatedObject(): number { return this.createObject().x; } - private createObject(): { x: number } { - return {x: 42}; - } - conditionalFieldAccess(a: SimpleClass): number { if (a.x === 1.1) return 14; return 10; } nestedFieldAccess(): number { - const obj = {inner: new SimpleClass()}; + const obj = { inner: new SimpleClass() }; obj.inner.x = 7; return obj.inner.x; } arrayFieldAccess(): number { - const obj = {arr: [7, 3, 6]}; + const obj = { arr: [7, 3, 6] }; obj.arr[1] = 5; return obj.arr[1]; } @@ -84,9 +80,23 @@ class FieldAccess { circularTypeChanges(): number { const obj = new SimpleClass(); - obj.x = {value: 5}; + obj.x = { value: 5 }; obj.x = obj.x.value; obj.x = [obj.x]; return obj.x.length; } + + readFromNestedFakeObjects(): number { + let x = Foo.Bar.x; + let y = Foo.Bar.y; + if (x === undefined && y === undefined) { + return 1; + } else { + return 2; + } + } + + private createObject(): { x: number } { + return { x: 42 }; + } } diff --git a/usvm-ts/src/test/resources/samples/InstanceFields.ts b/usvm-ts/src/test/resources/samples/InstanceFields.ts index e298b88494..a89721bc4a 100644 --- a/usvm-ts/src/test/resources/samples/InstanceFields.ts +++ b/usvm-ts/src/test/resources/samples/InstanceFields.ts @@ -3,21 +3,21 @@ class InstanceFields { returnSingleField(x: { a: number }): number { - return x.a + return x.a; } dispatchOverField(x: { a: number }): number { - if (x.a == 1) return 1 - if (x.a == 2) return 2 - return 100 + if (x.a == 1) return 1; + if (x.a == 2) return 2; + return 100; } returnSumOfTwoFields(x: { a: number, b: number }): number { - return x.a + x.b + return x.a + x.b; } assignField(x: { a: number }): number { - x.a = 10 - return x.a + x.a = 10; + return x.a; } } diff --git a/usvm-ts/src/test/resources/samples/InstanceMethods.ts b/usvm-ts/src/test/resources/samples/InstanceMethods.ts index f26d2a1f4c..0f78bf7216 100644 --- a/usvm-ts/src/test/resources/samples/InstanceMethods.ts +++ b/usvm-ts/src/test/resources/samples/InstanceMethods.ts @@ -3,21 +3,21 @@ class InstanceMethods { noArguments(): number { - return 42 + return 42; } singleArgument(a: number): number { - if (a != a) return a - if (a == 1) return a - if (a == 2) return a - return 100 + if (a != a) return a; + if (a == 1) return a; + if (a == 2) return a; + return 100; } manyArguments(a: number, b: number, c: number, d: number): number { - if (a == 1) return a - if (b == 2) return b - if (c == 3) return c - if (d == 4) return d - return 100 + if (a == 1) return a; + if (b == 2) return b; + if (c == 3) return c; + if (d == 4) return d; + return 100; } } diff --git a/usvm-ts/src/test/resources/samples/Null.ts b/usvm-ts/src/test/resources/samples/Null.ts index 9dfc16a306..dd18bedfb8 100644 --- a/usvm-ts/src/test/resources/samples/Null.ts +++ b/usvm-ts/src/test/resources/samples/Null.ts @@ -3,7 +3,7 @@ class Null { isNull(x): number { - if (x === null) return 1 - return 2 + if (x === null) return 1; + return 2; } } diff --git a/usvm-ts/src/test/resources/samples/Numeric.ts b/usvm-ts/src/test/resources/samples/Numeric.ts index 4ad0361efe..0d252487e7 100644 --- a/usvm-ts/src/test/resources/samples/Numeric.ts +++ b/usvm-ts/src/test/resources/samples/Numeric.ts @@ -3,92 +3,92 @@ class Numeric { numberToNumber(x: number): number { - if (x != x) return Number(x) // NaN - if (x == 0) return Number(x) // 0 - if (x > 0) return Number(x) // x (>0) - if (x < 0) return Number(x) // x (<0) + if (x != x) return Number(x); // NaN + if (x == 0) return Number(x); // 0 + if (x > 0) return Number(x); // x (>0) + if (x < 0) return Number(x); // x (<0) // unreachable } boolToNumber(x: boolean): number { - if (x) return Number(x) // 1 - if (!x) return Number(x) // 0 + if (x) return Number(x); // 1 + if (!x) return Number(x); // 0 // unreachable } undefinedToNumber(): number { - let x = undefined - return Number(x) // NaN + let x = undefined; + return Number(x); // NaN } nullToNumber(): number { - let x = null - return Number(x) // 0 + let x = null; + return Number(x); // 0 } emptyStringToNumber(): number { - let x = "" - return Number(x) // 0 + let x = ""; + return Number(x); // 0 } numberStringToNumber(): number { - let x = "42" - return Number(x) // 42 + let x = "42"; + return Number(x); // 42 } stringToNumber(): number { - let x = "hello" - return Number(x) // NaN + let x = "hello"; + return Number(x); // NaN } emptyArrayToNumber(): number { - let x = [] - return Number(x) // 0 + let x = []; + return Number(x); // 0 } singleNumberArrayToNumber(): number { - let x = [42] - return Number(x) // 42 + let x = [42]; + return Number(x); // 42 } singleUndefinedArrayToNumber(): number { - let x = [undefined] - return Number(x) // 0 + let x = [undefined]; + return Number(x); // 0 } singleObjectArrayToNumber(): number { - let x = [{}] - return Number(x) // NaN + let x = [{}]; + return Number(x); // NaN } singleCustomFortyTwoObjectArrayToNumber(): number { - let x = [new FortyTwo()] - return Number(x) // 42 + let x = [new FortyTwo()]; + return Number(x); // 42 } multipleElementArrayToNumber(): number { - let x = [5, 100] - return Number(x) // NaN + let x = [5, 100]; + return Number(x); // NaN } emptyObjectToNumber(): number { - let x = {} - return Number(x) // NaN + let x = {}; + return Number(x); // NaN } objectToNumber(): number { - let x = {a: 42} - return Number(x) // NaN + let x = { a: 42 }; + return Number(x); // NaN } customFortyTwoObjectToNumber(): number { - let x = new FortyTwo() - return Number(x) // 42 + let x = new FortyTwo(); + return Number(x); // 42 } } class FortyTwo { toString() { - return "42" + return "42"; } } diff --git a/usvm-ts/src/test/resources/samples/StaticFields.ts b/usvm-ts/src/test/resources/samples/StaticFields.ts index 4589f1786d..b5d2c98a89 100644 --- a/usvm-ts/src/test/resources/samples/StaticFields.ts +++ b/usvm-ts/src/test/resources/samples/StaticFields.ts @@ -51,6 +51,10 @@ class StaticParent { class StaticChild extends StaticParent { override static id = 200; + static getId(): number { + return this.id; + } + getParentId(): number { return StaticParent.id; } @@ -58,10 +62,6 @@ class StaticChild extends StaticParent { getChildId(): number { return StaticChild.id; } - - static getId(): number { - return this.id; - } } // Test: Boolean static toggle @@ -97,7 +97,7 @@ class StaticNull { // Test: Object static operations class StaticObject { - static config: Config = {enabled: true, count: 10}; + static config: Config = { enabled: true, count: 10 }; static modifyAndGet(): Config { this.config.increment(); diff --git a/usvm-ts/src/test/resources/samples/StaticMethods.ts b/usvm-ts/src/test/resources/samples/StaticMethods.ts index 608a140f5d..ddce155fef 100644 --- a/usvm-ts/src/test/resources/samples/StaticMethods.ts +++ b/usvm-ts/src/test/resources/samples/StaticMethods.ts @@ -3,21 +3,21 @@ class StaticMethods { static noArguments(): number { - return 42 + return 42; } static singleArgument(a: number): number { - if (a != a) return a - if (a == 1) return a - if (a == 2) return a - return 100 + if (a != a) return a; + if (a == 1) return a; + if (a == 2) return a; + return 100; } static manyArguments(a: number, b: number, c: number, d: number): number { - if (a == 1) return a - if (b == 2) return b - if (c == 3) return c - if (d == 4) return d - return 100 + if (a == 1) return a; + if (b == 2) return b; + if (c == 3) return c; + if (d == 4) return d; + return 100; } } diff --git a/usvm-ts/src/test/resources/samples/Strings.ts b/usvm-ts/src/test/resources/samples/Strings.ts index c2428b01ff..25f33ba7a9 100644 --- a/usvm-ts/src/test/resources/samples/Strings.ts +++ b/usvm-ts/src/test/resources/samples/Strings.ts @@ -3,74 +3,75 @@ class Strings { typeOfString(): string { - let x = "hello" - return typeof x // "string" + let x = "hello"; + return typeof x; // "string" } typeOfNumber(): string { - let x = 42 - return typeof x // "number" + let x = 42; + return typeof x; // "number" } typeOfBoolean(): string { - let x = true - return typeof x // "boolean" + let x = true; + return typeof x; // "boolean" } typeOfUndefined(): string { - let x = undefined - return typeof x // "undefined" + let x = undefined; + return typeof x; // "undefined" } typeOfNull(): string { - let x = null - return typeof x // "object" + let x = null; + return typeof x; // "object" } typeOfObject(): string { - let x = {} - return typeof x // "object" + let x = {}; + return typeof x; // "object" } typeOfArray(): string { - let x = [5, 42] - return typeof x // "object" + let x = [5, 42]; + return typeof x; // "object" } typeOfFunction(): string { - let x = function() {} - return typeof x // "function" + let x = function () { + }; + return typeof x; // "function" } typeOfInputString(x: string): string { - return typeof x // "string" + return typeof x; // "string" } typeOfInputNumber(x: number): string { - return typeof x // "number" + return typeof x; // "number" } typeOfInputBoolean(x: boolean): string { - return typeof x // "boolean" + return typeof x; // "boolean" } typeOfInputUndefined(x: undefined): string { - return typeof x // "undefined" + return typeof x; // "undefined" } typeOfInputNull(x: null): string { - return typeof x // "object" + return typeof x; // "object" } typeOfInputObject(x: {}): string { - return typeof x // "object" + return typeof x; // "object" } typeOfInputArray(x: any[]): string { - return typeof x // "object" + return typeof x; // "object" } typeOfInputFunction(x: Function): string { - return typeof x // "function" + return typeof x; // "function" } } diff --git a/usvm-ts/src/test/resources/samples/Truthy.ts b/usvm-ts/src/test/resources/samples/Truthy.ts index 52e198a11a..384607b057 100644 --- a/usvm-ts/src/test/resources/samples/Truthy.ts +++ b/usvm-ts/src/test/resources/samples/Truthy.ts @@ -3,9 +3,9 @@ class Truthy { arrayTruthy() { - if (![]) return -1 // unreachable - if (![0]) return -1 // unreachable - if (![1]) return -1 // unreachable - return 0 + if (![]) return -1; // unreachable + if (![0]) return -1; // unreachable + if (![1]) return -1; // unreachable + return 0; } } diff --git a/usvm-ts/src/test/resources/samples/TypeCoercion.ts b/usvm-ts/src/test/resources/samples/TypeCoercion.ts index c0e8937f05..a9bef91624 100644 --- a/usvm-ts/src/test/resources/samples/TypeCoercion.ts +++ b/usvm-ts/src/test/resources/samples/TypeCoercion.ts @@ -4,50 +4,50 @@ class TypeCoercion { argWithConst(a: number): number { - if (a == true) return 1 - return 0 + if (a == true) return 1; + return 0; } argWithArg(a: boolean, b: number): number { if (a + b == 10.0) { - return 1 + return 1; } else { - return 0 + return 0; } } dualBoolean(a: number): number { if (a) { if (a == false) { - return 1 // unreachable code + return 1; // unreachable code } if (a == true) { - return 2 + return 2; } - return 3 + return 3; } // a == 0 - return -1 + return -1; } dualBooleanWithoutTypes(a: string) { if (a) { if (a == false) { - return 1 // REACHABLE code + return 1; // REACHABLE code } if (a == true) { - return 2 + return 2; } - return 3 + return 3; } // a == 0 - return -1 + return -1; } unreachableByType(a: number, b: boolean): number { @@ -59,40 +59,40 @@ class TypeCoercion { No branch can enter this if statement */ if (a && !b) { - return 0 + return 0; } else { - return 1 + return 1; } } - return 2 + return 2; } transitiveCoercion(a: number, b: boolean, c: number): number { if (a == b) { if (c && (a == c)) { - return 1 + return 1; } else { - return 2 + return 2; } } - return 3 + return 3; } transitiveCoercionNoTypes(a, b, c): number { if (a == b) { if (c != 0 && c != 1) { if (c && (a == c)) { - return 1 + return 1; } else { - return 2 + return 2; } } else { - return 4 + return 4; } } - return 3 + return 3; } } diff --git a/usvm-ts/src/test/resources/samples/Undefined.ts b/usvm-ts/src/test/resources/samples/Undefined.ts index 1b5b59c529..88f59c5e25 100644 --- a/usvm-ts/src/test/resources/samples/Undefined.ts +++ b/usvm-ts/src/test/resources/samples/Undefined.ts @@ -3,7 +3,7 @@ class Undefined { isUndefined(x): number { - if (x === undefined) return 1 - return 2 + if (x === undefined) return 1; + return 2; } } diff --git a/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts index cb74a0db8d..1e683c710a 100644 --- a/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts @@ -3,77 +3,64 @@ class AllocatedArrays { createConstantArrayOfNumbers() { - let x = [1, 2, 3] - if (x[0] === 1) return 1 - return -1 + let x = [1, 2, 3]; + if (x[0] === 1) return 1; + return -1; } createAndReturnConstantArrayOfNumbers() { - return [1, 2, 3] + return [1, 2, 3]; } createAndAccessArrayOfBooleans() { - let x = [true, false, true] - if (x[0] === true) return 1 - return -1 + let x = [true, false, true]; + if (x[0] === true) return 1; + return -1; } createArrayOfBooleans() { - let x = [true, false, true] - return x + let x = [true, false, true]; + return x; } createMixedArray() { - let x = [1.1, true, undefined] - return x + let x = [1.1, true, undefined]; + return x; } createArrayOfUnknownValues(a, b, c) { - let x = [a, b, c] - if (x[0] === 1.1) return x - if (x[1] === true) return x - if (x[2] === undefined) return x - return x + let x = [a, b, c]; + if (x[0] === 1.1) return x; + if (x[1] === true) return x; + if (x[2] === undefined) return x; + return x; } createArrayOfNumbersAndPutDifferentTypes() { - let x = [1, 2, 3] - x[1] = true - x[2] = undefined - x[0] = null - return x + let x = [1, 2, 3]; + x[1] = true; + x[2] = undefined; + x[0] = null; + return x; } allocatedArrayLengthExpansion() { - let x = [1, 2, 3] + let x = [1, 2, 3]; if (x.length == 3) { - x[5] = 5 + x[5] = 5; if (x.length == 6) { - return x + return x; } else { - return -1 // unreachable + return -1; // unreachable } } else { - return -1 // unreachable + return -1; // unreachable } } writeInTheIndexEqualToLength() { - let x = [1, 2, 3] - x[3] = 4 - return x - } - - readFakeObjectAndWriteFakeObject(x: any[], y) { - if (x[0] === 1) { - x[0] = y - if (x[0] === 2) { - return x - } else { - return x - } - } - - return x + let x = [1, 2, 3]; + x[3] = 4; + return x; } } diff --git a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts index 2917303c0f..200a4c8814 100644 --- a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts @@ -3,9 +3,9 @@ class InputArrays { inputArrayOfNumbers(x: number[]) { - if (x[0] === 1) return 1 - if (x[0] === undefined) return -1 - return 2 + if (x[0] === 1) return 1; + if (x[0] === undefined) return -1; + return 2; } writeIntoInputArray(x: number[]) { @@ -17,32 +17,45 @@ class InputArrays { } idForArrayOfNumbers(x: number[]) { - return x + return x; } arrayOfBooleans(x: boolean[]) { - if (x[0] === true) return 1 - return -1 + if (x[0] === true) return 1; + return -1; } arrayOfUnknownValues(x: any[]) { - if (x[0] === 1.1) return x - if (x[1] === true) return x - if (x[2] === undefined) return x - return x + if (x[0] === 1.1) return x; + if (x[1] === true) return x; + if (x[2] === undefined) return x; + return x; } writeIntoArrayOfUnknownValues(x: any[]) { - x[1] = true - x[2] = undefined - x[0] = null - return x + x[1] = true; + x[2] = undefined; + x[0] = null; + return x; } rewriteFakeValueInArray(x: any[]) { if (x[0] === 1) { - x[0] = null + x[0] = null; } - return x[0] + return x[0]; + } + + readFakeObjectAndWriteFakeObject(x: any[], y) { + if (x[0] === 1) { + x[0] = y; + if (x[0] === 2) { + return x; + } else { + return x; + } + } + + return x; } } diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts index 50da6ca4f8..b438e648cf 100644 --- a/usvm-ts/src/test/resources/samples/operators/Add.ts +++ b/usvm-ts/src/test/resources/samples/operators/Add.ts @@ -5,70 +5,70 @@ class Add { addBoolAndBool(a: boolean, b: boolean): number { let res = a + b; - if (res == 0 && (a || b)) return -1 // unreachable - if (res < 0 || res > 2) return -1 // unreachable - if (res == 1 && a && b) return -1 // unreachable - if (res == 2 && !(a && b)) return -1 // unreachable + if (res == 0 && (a || b)) return -1; // unreachable + if (res < 0 || res > 2) return -1; // unreachable + if (res == 1 && a && b) return -1; // unreachable + if (res == 2 && !(a && b)) return -1; // unreachable - if (res == 0) return 1 // false false - if (res == 1 && !a) return 2 // false true - if (res == 1 && !b) return 3 // true false - if (res == 2) return 4 // true true + if (res == 0) return 1; // false false + if (res == 1 && !a) return 2; // false true + if (res == 1 && !b) return 3; // true false + if (res == 2) return 4; // true true - return -1 // unreachable + return -1; // unreachable } addBoolAndNumber(a: boolean, b: number): number { let res = a + b; - if (res == 0 && a) return 1 // true -1 - if (res == 0 && !a) return 2 // false 0 + if (res == 0 && a) return 1; // true -1 + if (res == 0 && !a) return 2; // false 0 - if (res == 6 && a) return 3 + if (res == 6 && a) return 3; - if (b != b) return res // _ NaN + if (b != b) return res; // _ NaN - return 4 + return 4; } addNumberAndNumber(a: number, b: number): number { let res = a + b; - if (a != a) return res - if (b != b) return res + if (a != a) return res; + if (b != b) return res; - if (res == 1.1) return res + if (res == 1.1) return res; - return 0 + return 0; } addNumberAndUndefined(a: number): number { let res = a + undefined; - if (res == 0) return -1 // unreachable + if (res == 0) return -1; // unreachable - return res + return res; } addNumberAndNull(a: number): number { let res = a + null; - if (res != a) return res + if (res != a) return res; - return res + return res; } addUnknownValues(a, b) { let res = a + b; - if (a === undefined || b === undefined) return res + if (a === undefined || b === undefined) return res; - if (res != res) return res + if (res != res) return res; - if (res == 7) return res + if (res == 7) return res; - if (a === null && b === null) return res + if (a === null && b === null) return res; - return 42 + return 42; } } diff --git a/usvm-ts/src/test/resources/samples/operators/And.ts b/usvm-ts/src/test/resources/samples/operators/And.ts index a7b6b2a916..b66b06b88d 100644 --- a/usvm-ts/src/test/resources/samples/operators/And.ts +++ b/usvm-ts/src/test/resources/samples/operators/And.ts @@ -3,10 +3,10 @@ class And { andOfBooleanAndBoolean(a: boolean, b: boolean): number { - if (a && b) return 1 - if (a) return 2 - if (b) return 3 - return 4 + if (a && b) return 1; + if (a) return 2; + if (b) return 3; + return 4; } // (a) (b) (a && b) @@ -20,15 +20,15 @@ class And { // 0.0 NaN 0.0 // 0.0 0.0 0.0 andOfNumberAndNumber(a: number, b: number): number { - if (a && b) return 1 // (a!=0 && !a.isNaN) && (b!=0 && !b.isNaN) - if (a && (b != b)) return 2 // (a!=0 && !a.isNaN) && (b.isNaN) - if (a) return 3 // (a!=0 && !a.isNaN) && (b==0) - if ((a != a) && b) return 4 // (a.isNaN) && (b!=0 && !b.isNaN) - if ((a != a) && (b != b)) return 5 // (a.isNaN) && (b.isNaN) - if ((a != a)) return 6 // (a.isNaN) && (b==0) - if (b) return 7 // (a==0) && (b!=0 && !b.isNaN) - if (b != b) return 8 // (a==0) && (b.isNaN) - return 9 // (a==0) && (b==0) + if (a && b) return 1; // (a!=0 && !a.isNaN) && (b!=0 && !b.isNaN) + if (a && (b != b)) return 2; // (a!=0 && !a.isNaN) && (b.isNaN) + if (a) return 3; // (a!=0 && !a.isNaN) && (b==0) + if ((a != a) && b) return 4; // (a.isNaN) && (b!=0 && !b.isNaN) + if ((a != a) && (b != b)) return 5; // (a.isNaN) && (b.isNaN) + if ((a != a)) return 6; // (a.isNaN) && (b==0) + if (b) return 7; // (a==0) && (b!=0 && !b.isNaN) + if (b != b) return 8; // (a==0) && (b.isNaN) + return 9; // (a==0) && (b==0) } // (a) (b) (a && b) @@ -39,12 +39,12 @@ class And { // false NaN false // false 0.0 false andOfBooleanAndNumber(a: boolean, b: number): number { - if (a && b) return 1 // a && (b!=0 && !b.isNaN) - if (a && (b != b)) return 2 // a && (b.isNaN) - if (a) return 3 // a && (b==0) - if (b) return 4 // !a && (b!=0 && !b.isNaN) - if (b != b) return 5 // !a && (b.isNaN) - return 6 // !a && (b==0) + if (a && b) return 1; // a && (b!=0 && !b.isNaN) + if (a && (b != b)) return 2; // a && (b.isNaN) + if (a) return 3; // a && (b==0) + if (b) return 4; // !a && (b!=0 && !b.isNaN) + if (b != b) return 5; // !a && (b.isNaN) + return 6; // !a && (b==0) } // (a) (b) (a && b) @@ -55,31 +55,31 @@ class And { // 0.0 true 0.0 // 0.0 false 0.0 andOfNumberAndBoolean(a: number, b: boolean): number { - if (a && b) return 1 // (a!=0 && !a.isNaN) && b - if (a) return 2 // (a!=0 && !a.isNaN) && !b - if ((a != a) && b) return 3 // (a.isNaN) && b - if (a != a) return 4 // (a.isNaN) && !b - if (b) return 5 // (a==0) && b - return 6 // (a==0) && !b + if (a && b) return 1; // (a!=0 && !a.isNaN) && b + if (a) return 2; // (a!=0 && !a.isNaN) && !b + if ((a != a) && b) return 3; // (a.isNaN) && b + if (a != a) return 4; // (a.isNaN) && !b + if (b) return 5; // (a==0) && b + return 6; // (a==0) && !b } andOfObjectAndObject(a: object, b: object): number { - if (a && b) return 1 - if (a) return 2 - if (b) return 3 - return 4 + if (a && b) return 1; + if (a) return 2; + if (b) return 3; + return 4; } andOfUnknown(a, b): number { - if (a && b) return 1 - if (a) return 2 - if (b) return 3 - return 4 + if (a && b) return 1; + if (a) return 2; + if (b) return 3; + return 4; } truthyUnknown(a, b): number { - if (a) return 1 - if (b) return 2 - return 99 + if (a) return 1; + if (b) return 2; + return 99; } } diff --git a/usvm-ts/src/test/resources/samples/operators/Division.ts b/usvm-ts/src/test/resources/samples/operators/Division.ts index d31c459b78..c75bb22fe3 100644 --- a/usvm-ts/src/test/resources/samples/operators/Division.ts +++ b/usvm-ts/src/test/resources/samples/operators/Division.ts @@ -6,54 +6,54 @@ class Division { let res = a / b; if (res == 4) { - return res + return res; } if (res == Infinity) { - return res + return res; } if (res == -Infinity) { - return res + return res; } if (res != res) { - return res + return res; } - return res + return res; } booleanDivision(a: boolean, b: boolean): number { let res = a / b; if (res == 0) { - return res + return res; } - return res + return res; } mixedDivision(a: number, b: boolean): number { let res = a / b; if (res == 4) { - return res + return res; } if (res == Infinity) { - return res + return res; } if (res == -Infinity) { - return res + return res; } if (res != res) { - return res + return res; } - return res + return res; } unknownDivision(a, b): number { diff --git a/usvm-ts/src/test/resources/samples/operators/Equality.ts b/usvm-ts/src/test/resources/samples/operators/Equality.ts index a829db3456..771497cdf6 100644 --- a/usvm-ts/src/test/resources/samples/operators/Equality.ts +++ b/usvm-ts/src/test/resources/samples/operators/Equality.ts @@ -3,44 +3,44 @@ class Equality { eqBoolWithBool(a: boolean): number { - if (a == true) return 1 - if (a == false) return 2 - return -1 // unreachable + if (a == true) return 1; + if (a == false) return 2; + return -1; // unreachable } eqNumberWithNumber(a: number): number { - if (a != a) return 1 - if (a == 42) return 2 - return 3 + if (a != a) return 1; + if (a == 42) return 2; + return 3; } eqStringWithString(a: string): number { - if (a == "123") return 1 - return 2 + if (a == "123") return 1; + return 2; } eqBigintWithBigint(a: bigint): number { - if (a == 42n) return 1 - return 2 + if (a == 42n) return 1; + return 2; } eqObjectWithObject(a: object): number { - if (a == {b: 0}) return -1 // unreachable - if (a == a) return 1 - return -1 // unreachable + if (a == { b: 0 }) return -1; // unreachable + if (a == a) return 1; + return -1; // unreachable } eqArrayWithArray(a: any[]): number { - if (a == []) return -1 // unreachable - if (a == a) return 1 - return -1 // unreachable + if (a == []) return -1; // unreachable + if (a == a) return 1; + return -1; // unreachable } eqArrayWithBoolean(): number { - if ([] == true) return -1 // unreachable - if ([0] == true) return -1 // unreachable - if ([1] == false) return -1 // unreachable - if ([42] == false) return -1 // unreachable - return 0 + if ([] == true) return -1; // unreachable + if ([0] == true) return -1; // unreachable + if ([1] == false) return -1; // unreachable + if ([42] == false) return -1; // unreachable + return 0; } } diff --git a/usvm-ts/src/test/resources/samples/operators/Neg.ts b/usvm-ts/src/test/resources/samples/operators/Neg.ts index 41d5e309d6..e2625ae03a 100644 --- a/usvm-ts/src/test/resources/samples/operators/Neg.ts +++ b/usvm-ts/src/test/resources/samples/operators/Neg.ts @@ -3,23 +3,23 @@ class Neg { negateNumber(x: number): number { - let y = -x - if (x != x) return y // -NaN == NaN - if (x == 0) return y // -0 == 0 - if (x > 0) return y // -(x>0) == (x<0) - if (x < 0) return y // -(x<0) == (x>0) + let y = -x; + if (x != x) return y; // -NaN == NaN + if (x == 0) return y; // -0 == 0 + if (x > 0) return y; // -(x>0) == (x<0) + if (x < 0) return y; // -(x<0) == (x>0) // unreachable } negateBoolean(x: boolean): number { - let y = -x - if (x) return y // -true == -1 - if (!x) return y // -false == -0 + let y = -x; + if (x) return y; // -true == -1 + if (!x) return y; // -false == -0 // unreachable } negateUndefined(): number { - let x = undefined - return -x // -undefined == NaN + let x = undefined; + return -x; // -undefined == NaN } } diff --git a/usvm-ts/src/test/resources/samples/operators/Or.ts b/usvm-ts/src/test/resources/samples/operators/Or.ts index b04ffd669d..7a374d1909 100644 --- a/usvm-ts/src/test/resources/samples/operators/Or.ts +++ b/usvm-ts/src/test/resources/samples/operators/Or.ts @@ -9,14 +9,14 @@ class Or { // true true true 1 orOfBooleanAndBoolean(a: boolean, b: boolean): number { if (a || b) { - if (a && b) return 1 // (a) && (b) - if (a) return 2 // (a) && (!b) - if (b) return 3 // (!a) && (b) - return 0 + if (a && b) return 1; // (a) && (b) + if (a) return 2; // (a) && (!b) + if (b) return 3; // (!a) && (b) + return 0; } - if (a) return 0 - if (b) return 0 - return 4 // (!a) && (!b) + if (a) return 0; + if (b) return 0; + return 4; // (!a) && (!b) } // (a) (b) (a || b) Case @@ -32,31 +32,31 @@ class Or { orOfNumberAndNumber(a: number, b: number): number { if (a || b) { if (a) { - if (b) return 1 // (a) && (b) - if (b != b) return 2 // (a) && (b.isNaN) - if (b == 0) return 3 // (a) && (b==0) - return 0 + if (b) return 1; // (a) && (b) + if (b != b) return 2; // (a) && (b.isNaN) + if (b == 0) return 3; // (a) && (b==0) + return 0; } if (a != a) { - if (b) return 4 // (a.isNaN) && (b) - return 0 + if (b) return 4; // (a.isNaN) && (b) + return 0; } if (a == 0) { - if (b) return 7 // (a==0) && (b) - return 0 + if (b) return 7; // (a==0) && (b) + return 0; } - return 0 + return 0; } if (a != a) { - if (b != b) return 5 // (a.isNaN) && (b.isNaN) - if (b == 0) return 6 // (a.isNaN) && (b==0) - return 0 + if (b != b) return 5; // (a.isNaN) && (b.isNaN) + if (b == 0) return 6; // (a.isNaN) && (b==0) + return 0; } if (a == 0) { - if (b != b) return 8 // (a==0) && (b.isNaN) - if (b == 0) return 9 // (a==0) && (b==0) - return 0 + if (b != b) return 8; // (a==0) && (b.isNaN) + if (b == 0) return 9; // (a==0) && (b==0) + return 0; } - return 0 // unreachable + return 0; // unreachable } } diff --git a/usvm-ts/src/test/resources/samples/operators/Remainder.ts b/usvm-ts/src/test/resources/samples/operators/Remainder.ts index 2e1c6fea16..b57443385f 100644 --- a/usvm-ts/src/test/resources/samples/operators/Remainder.ts +++ b/usvm-ts/src/test/resources/samples/operators/Remainder.ts @@ -6,58 +6,58 @@ class Remainder { let res = a % b; if (a != a || b != b) { - return res // NaN + return res; // NaN } if (a == Infinity || a == -Infinity) { - return res // NaN + return res; // NaN } if (a == 0 && b == 0) { - return res // NaN + return res; // NaN } if (b == 0) { - return res // NaN + return res; // NaN } if (b == Infinity || b == -Infinity) { - return res // a + return res; // a } if (a == 0) { - return res // a + return res; // a } if (res == 4) { - return res + return res; } - return res + return res; } booleanRemainder(a: boolean, b: boolean): number { let res = a % b; if (res == 0) { - return res + return res; } - return res + return res; } mixedRemainder(a: number, b: boolean): number { let res = a % b; if (res == 4) { - return res + return res; } if (res != res) { - return res + return res; } - return res + return res; } unknownRemainder(a, b): number { diff --git a/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts index d3f8b51a02..fc8fdd72bc 100644 --- a/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts +++ b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts @@ -3,7 +3,7 @@ class ObjectUsage { objectAsParameter(x: {}): number { - if (x === undefined) return -1 - return 42 + if (x === undefined) return -1; + return 42; } } diff --git a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts index fba8af6974..3d4d008b38 100644 --- a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts +++ b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts @@ -48,6 +48,6 @@ class Example { // noinspection UnnecessaryLocalVariableJS const y: C = new D(new A(bar)); - return y + return y; } } diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts index ea2c6e5e6b..37e3d06a2a 100644 --- a/usvm-ts/src/test/resources/samples/types/TypeStream.ts +++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts @@ -2,19 +2,27 @@ // noinspection JSUnusedGlobalSymbols class TypeStream { - ancestorId(ancestor: Parent): Parent { - return ancestor + instanceOf(ancestor: Parent): number { + if (ancestor instanceof FirstChild) { + return 1; + } else if (ancestor instanceof SecondChild) { + return 2; + } else if (ancestor instanceof Parent) { + return 3; + } + return -1; // unreachable } - virtualInvokeForAncestor(ancestor: Parent): number { - const number = ancestor.virtualMethod(); - if (number == 100) { - return 1 - } else if (number == 200) { - return 2 - } else { - return 3 + virtualInvokeOnAncestor(ancestor: Parent): number { + const virtualInvokeResult = ancestor.virtualMethod(); + if (virtualInvokeResult == 100) { + return 1; + } else if (virtualInvokeResult == 200) { + return 2; + } else if (virtualInvokeResult == 300) { + return 3; } + return -1; // unreachable } useUniqueField(value: any): number { @@ -22,12 +30,13 @@ class TypeStream { const _ = value.firstChildField; const virtualInvokeResult = value.virtualMethod(); if (virtualInvokeResult == 100) { - return -1 // unreachable + return 1; } else if (virtualInvokeResult == 200) { - return 1 - } else { - return -2 // unreachable + return 2; // unreachable + } else if (virtualInvokeResult == 300) { + return 3; // unreachable } + return -1; // unreachable } useNonUniqueField(value: any): number { @@ -35,35 +44,36 @@ class TypeStream { const _ = value.parentField; const virtualInvokeResult = value.virtualMethod(); if (virtualInvokeResult == 100) { - return 1 + return 1; } else if (virtualInvokeResult == 200) { - return 2 - } else { - return 3 + return 2; + } else if (virtualInvokeResult == 300) { + return 3; } + return -1; // unreachable } } class Parent { - parentField: number = -10 + parentField: number = 42; virtualMethod(): number { - return 100; + return 300; } } class FirstChild extends Parent { - firstChildField: number = 10 + firstChildField: number = 10; override virtualMethod(): number { - return 200; + return 100; } } class SecondChild extends Parent { - secondChildField: number = 20 + secondChildField: number = 20; override virtualMethod(): number { - return 300; + return 200; } } diff --git a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt index b132696cf1..ee71dc8bcf 100644 --- a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt +++ b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt @@ -32,4 +32,4 @@ class AnalysisResultsNumberMatcher( ) { operator fun invoke(x: Int) = cmp(x) override fun toString() = description -} \ No newline at end of file +}