From 858c6ad384e5431ef4f60fcdc8c3343927480091 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 20 Jun 2025 13:26:53 +0300 Subject: [PATCH] Add strings support --- .../src/main/kotlin/org/usvm/api/TsTest.kt | 2 - .../main/kotlin/org/usvm/machine/TsContext.kt | 37 +++- .../org/usvm/machine/expr/TsExprResolver.kt | 42 ++--- .../usvm/machine/interpreter/TsInterpreter.kt | 115 +++++++------ .../org/usvm/machine/types/TsTypeSystem.kt | 2 +- .../kotlin/org/usvm/samples/InstanceFields.kt | 26 +-- .../test/kotlin/org/usvm/samples/Strings.kt | 160 ++++++++++++++++++ .../org/usvm/samples/arrays/InputArrays.kt | 14 +- .../org/usvm/samples/types/ObjectUsage.kt | 11 +- .../src/test/kotlin/org/usvm/util/Truthy.kt | 4 - .../org/usvm/util/TsMethodTestRunner.kt | 2 - .../kotlin/org/usvm/util/TsTestResolver.kt | 31 +++- usvm-ts/src/test/resources/samples/Strings.ts | 76 +++++++++ .../resources/samples/arrays/InputArrays.ts | 2 +- .../resources/samples/types/ObjectUsage.ts | 7 +- .../samples/types/StructuralEquality.ts | 9 +- 16 files changed, 410 insertions(+), 130 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/Strings.kt create mode 100644 usvm-ts/src/test/resources/samples/Strings.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt index d33a15028e..8c0f40f7f0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt @@ -48,8 +48,6 @@ sealed interface TsTestValue { } } - data class TsObject(val addr: Int) : TsTestValue - data class TsClass( val name: String, val properties: Map, 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 45bdcf2833..026f3c35bb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -24,6 +24,8 @@ import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.api.allocateArrayInitialized +import org.usvm.api.allocateConcreteRef import org.usvm.api.typeStreamOf import org.usvm.collection.field.UFieldLValue import org.usvm.isTrue @@ -34,6 +36,7 @@ import org.usvm.machine.expr.TsVoidValue import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.EtsFakeType import org.usvm.memory.UReadOnlyMemory +import org.usvm.sizeSort import org.usvm.types.single import org.usvm.util.mkFieldLValue import kotlin.contracts.ExperimentalContracts @@ -65,7 +68,7 @@ class TsContext( fun typeToSort(type: EtsType): USort = when (type) { is EtsBooleanType -> boolSort is EtsNumberType -> fp64Sort - is EtsStringType -> fp64Sort + is EtsStringType -> addressSort is EtsNullType -> addressSort is EtsUndefinedType -> addressSort is EtsUnionType -> unresolvedSort @@ -198,6 +201,38 @@ class TsContext( fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef { return scope.calcOnState { extractRef(memory) } } + + private val stringConstantAllocatedRefs: MutableMap = hashMapOf() + internal val heapRefToStringConstant: MutableMap = hashMapOf() + + fun mkStringConstant(value: String, scope: TsStepScope): UConcreteHeapRef { + return stringConstantAllocatedRefs.getOrPut(value) { + val ref = allocateConcreteRef() + heapRefToStringConstant[ref] = value + + scope.doWithState { + // Mark `ref` with String type + memory.types.allocate(ref.address, EtsStringType) + + // Initialize char array + val valueType = EtsArrayType(EtsNumberType, dimensions = 1) + val descriptor = arrayDescriptorOf(valueType) + val charArray = memory.allocateArrayInitialized( + type = descriptor, + sort = bv16Sort, + sizeSort = sizeSort, + contents = value.asSequence().map { mkBv(it.code, bv16Sort) }, + ) + memory.types.allocate(charArray.address, valueType.elementType) + + // Write char array to `ref.value` + val valueLValue = mkFieldLValue(addressSort, ref, "value") + memory.write(valueLValue, charArray, guard = trueExpr) + } + + ref + } + } } const val MAGIC_OFFSET = 1000000 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 1b4d85f3d8..082324130d 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 @@ -85,6 +85,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef 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.TsConcreteMethodCallStmt @@ -118,15 +119,6 @@ import org.usvm.util.throwExceptionWithoutStackFrameDrop private val logger = KotlinLogging.logger {} -@Suppress("MagicNumber") -const val ADHOC_STRING = 777777.0 // arbitrary string - -@Suppress("MagicNumber") -const val ADHOC_STRING__NUMBER = 55555.0 // 'number' - -@Suppress("MagicNumber") -const val ADHOC_STRING__STRING = 2222.0 // 'string' - class TsExprResolver( private val ctx: TsContext, private val scope: TsStepScope, @@ -277,10 +269,26 @@ class TsExprResolver( val arg = resolve(expr.arg) ?: return null if (arg.sort == fp64Sort) { - if (arg == mkFp64(ADHOC_STRING)) { - return mkFp64(ADHOC_STRING__STRING) - } - return mkFp64(ADHOC_STRING__NUMBER) // 'number' + return mkStringConstant("number", scope) + } + if (arg.sort == boolSort) { + return mkStringConstant("boolean", scope) + } + if (arg.sort == addressSort) { + val ref = arg.asExpr(addressSort) + return mkIte( + condition = mkHeapRefEq(ref, mkTsNullValue()), + trueBranch = mkStringConstant("object", scope), + falseBranch = mkIte( + condition = mkHeapRefEq(ref, mkUndefinedValue()), + trueBranch = mkStringConstant("undefined", scope), + falseBranch = mkIte( + condition = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) }, + trueBranch = mkStringConstant("string", scope), + falseBranch = mkStringConstant("object", scope), + ) + ) + ) } logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } @@ -471,7 +479,7 @@ class TsExprResolver( } if (expr.callee.name == "toString") { - return mkFp64(ADHOC_STRING) + return TODO() } return when (val result = scope.calcOnState { methodResult }) { @@ -1032,11 +1040,7 @@ class TsSimpleValueResolver( } override fun visit(value: EtsStringConstant): UExpr = with(ctx) { - return when (value.value) { - "number" -> mkFp64(ADHOC_STRING__NUMBER) - "string" -> mkFp64(ADHOC_STRING__STRING) - else -> mkFp64(ADHOC_STRING) - } + mkStringConstant(value.value, scope) } override fun visit(value: EtsBooleanConstant): UExpr = with(ctx) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index c058217923..5df7982eea 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 @@ -19,9 +19,11 @@ import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStringType 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.EtsUnknownType import org.jacodb.ets.model.EtsValue import org.jacodb.ets.model.EtsVoidType @@ -169,15 +171,15 @@ class TsInterpreter( if (isAllocatedConcreteHeapRef(resolvedInstance)) { val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single() if (type is EtsClassType) { - val classes = ctx.scene.projectAndSdkClasses.filter { it.name == type.typeName } + val classes = scene.projectAndSdkClasses.filter { it.name == type.typeName } if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } - scope.assert(ctx.falseExpr) + scope.assert(falseExpr) return } if (classes.size > 1) { logger.warn { "Multiple classes with name: ${type.typeName}" } - scope.assert(ctx.falseExpr) + scope.assert(falseExpr) return } val cls = classes.single() @@ -189,14 +191,14 @@ class TsInterpreter( logger.warn { "Could not resolve method: ${stmt.callee} on type: $type" } - scope.assert(ctx.falseExpr) + scope.assert(falseExpr) return } } else { - val methods = ctx.resolveEtsMethods(stmt.callee) + val methods = resolveEtsMethods(stmt.callee) if (methods.isEmpty()) { logger.warn { "Could not resolve method: ${stmt.callee}" } - scope.assert(ctx.falseExpr) + scope.assert(falseExpr) return } concreteMethods += methods @@ -213,7 +215,7 @@ class TsInterpreter( val type = requireNotNull(method.enclosingClass).type val constraint = scope.calcOnState { - val ref = stmt.instance.asExpr(ctx.addressSort) + val ref = stmt.instance.asExpr(addressSort) .takeIf { !it.isFakeObject() } ?: uncoveredInstance.asExpr(addressSort) // TODO mistake, should be separated into several hierarchies @@ -303,7 +305,7 @@ class TsInterpreter( } check(args.size == numFormal) { - "Expected ${numFormal} arguments, got ${args.size}" + "Expected $numFormal arguments, got ${args.size}" } args += stmt.instance!! @@ -577,7 +579,12 @@ class TsInterpreter( } private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver = - TsExprResolver(ctx, scope, ::mapLocalToIdx, graph.hierarchy) + TsExprResolver( + ctx = ctx, + scope = scope, + localToIdx = ::mapLocalToIdx, + hierarchy = graph.hierarchy, + ) // (method, localName) -> idx private val localVarToIdx: MutableMap> = hashMapOf() @@ -608,7 +615,7 @@ class TsInterpreter( else -> error("Unexpected local: $local") } - fun getInitialState(method: EtsMethod, targets: List): TsState { + fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -616,32 +623,30 @@ class TsInterpreter( targets = UTargetsSet.from(targets), ) + state.memory.types.allocate(mkTsNullValue().address, EtsNullType) + val solver = ctx.solver() // TODO check for statics - val thisInstanceRef = mkRegisterStackLValue(ctx.addressSort, method.parameters.count()) - val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort) - - state.pathConstraints += with(ctx) { - mkNot( - mkOr( - ctx.mkHeapRefEq(thisRef, ctx.mkTsNullValue()), - ctx.mkHeapRefEq(thisRef, ctx.mkUndefinedValue()) - ) - ) - } + val thisIdx = mapLocalToIdx(method, EtsThis(method.enclosingClass!!.type)) + ?: error("Cannot find index for 'this' in method: $method") + val thisInstanceRef = mkRegisterStackLValue(addressSort, thisIdx) + val thisRef = state.memory.read(thisInstanceRef).asExpr(addressSort) - method.enclosingClass?.let { thisClass -> - // TODO not equal but subtype for abstract/interfaces - val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, thisClass.type) - state.pathConstraints += thisTypeConstraint - } + state.pathConstraints += mkNot(mkHeapRefEq(thisRef, mkTsNullValue())) + state.pathConstraints += mkNot(mkHeapRefEq(thisRef, mkUndefinedValue())) + + // TODO not equal but subtype for abstract/interfaces + state.pathConstraints += state.memory.types.evalTypeEquals(thisRef, method.enclosingClass!!.type) method.parameters.forEachIndexed { i, param -> + val ref by lazy { + val lValue = mkRegisterStackLValue(addressSort, i) + state.memory.read(lValue).asExpr(addressSort) + } + val parameterType = param.type if (parameterType is EtsRefType) { - val argLValue = mkRegisterStackLValue(ctx.addressSort, i) - val ref = state.memory.read(argLValue).asExpr(ctx.addressSort) val resolvedParameterType = graph.cp .projectAndSdkClasses .singleOrNull { it.name == parameterType.typeName } @@ -653,6 +658,21 @@ class TsInterpreter( val auxiliaryType = (resolvedParameterType as? EtsClassType)?.toAuxiliaryType(graph.hierarchy) ?: resolvedParameterType state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType) + + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) + } + if (parameterType == EtsNullType) { + state.pathConstraints += mkHeapRefEq(ref, mkTsNullValue()) + } + if (parameterType == EtsUndefinedType) { + state.pathConstraints += mkHeapRefEq(ref, mkUndefinedValue()) + } + if (parameterType == EtsStringType) { + state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) + + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) } } @@ -663,35 +683,32 @@ class TsInterpreter( state.memory.stack.push(method.parametersWithThisCount, method.localsCount) state.newStmt(method.cfg.instructions.first()) - state.memory.types.allocate(ctx.mkTsNullValue().address, EtsNullType) + state.memory.types.allocate(mkTsNullValue().address, EtsNullType) - return state + state } private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) { scope.doWithState { - with(ctx) { - if (method.returnType is EtsVoidType) { - methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue) - return@doWithState - } + if (method.returnType is EtsVoidType) { + methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue) + return@doWithState + } - val resultSort = typeToSort(method.returnType) - val resultValue = when (resultSort) { - is UAddressSort -> makeSymbolicRefUntyped() - is TsUnresolvedSort -> { - mkFakeValue( - scope, - makeSymbolicPrimitive(ctx.boolSort), - makeSymbolicPrimitive(ctx.fp64Sort), - makeSymbolicRefUntyped() - ) - } + val resultSort = ctx.typeToSort(method.returnType) + val resultValue = when (resultSort) { + is UAddressSort -> makeSymbolicRefUntyped() - else -> makeSymbolicPrimitive(resultSort) - } - methodResult = TsMethodResult.Success.MockedCall(method, resultValue) + is TsUnresolvedSort -> ctx.mkFakeValue( + scope, + makeSymbolicPrimitive(ctx.boolSort), + makeSymbolicPrimitive(ctx.fp64Sort), + makeSymbolicRefUntyped() + ) + + else -> makeSymbolicPrimitive(resultSort) } + methodResult = TsMethodResult.Success.MockedCall(method, resultValue) } } 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 ddb0bb9e6e..fb9206d07c 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 @@ -288,7 +288,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 } + scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType } else { hierarchy.classesForType(t) .asSequence() diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/InstanceFields.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/InstanceFields.kt index 1e21de1bf2..ccf9a4e1b0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/InstanceFields.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/InstanceFields.kt @@ -14,64 +14,44 @@ class InstanceFields : TsMethodTestRunner() { @Test fun `test returnSingleField`() { val method = getMethod(className, "returnSingleField") - discoverProperties( + discoverProperties( method, { x, r -> - // Note: this is an attempt to represent `r == x["a"]` - if (x !is TsTestValue.TsClass || r !is TsTestValue.TsNumber) return@discoverProperties false - val xa = x.properties["a"] as TsTestValue.TsNumber xa.number == r.number || (xa.number.isNaN() && r.number.isNaN()) }, - { x, r -> - (x is TsTestValue.TsUndefined || x is TsTestValue.TsNull) && r is TsTestValue.TsException - } ) } @Test fun `test dispatchOverField`() { val method = getMethod(className, "dispatchOverField") - discoverProperties( + discoverProperties( method, { x, r -> - if (x !is TsTestValue.TsClass || r !is TsTestValue.TsNumber) return@discoverProperties false - val xa = x.properties["a"] as TsTestValue.TsNumber xa.number == 1.0 && r.number == 1.0 }, { x, r -> - if (x !is TsTestValue.TsClass || r !is TsTestValue.TsNumber) return@discoverProperties false - val xa = x.properties["a"] as TsTestValue.TsNumber xa.number == 2.0 && r.number == 2.0 }, { x, r -> - if (x !is TsTestValue.TsClass || r !is TsTestValue.TsNumber) return@discoverProperties false - val xa = x.properties["a"] as TsTestValue.TsNumber xa.number != 1.0 && xa.number != 2.0 && r.number == 100.0 }, - { x, r -> - (x is TsTestValue.TsUndefined || x is TsTestValue.TsNull) && r is TsTestValue.TsException - } ) } @Test fun `test returnSumOfTwoFields`() { val method = getMethod(className, "returnSumOfTwoFields") - discoverProperties( + discoverProperties( method, { x, r -> - if (x !is TsTestValue.TsClass || r !is TsTestValue.TsNumber) return@discoverProperties false - val xa = x.properties["a"] as TsTestValue.TsNumber val xb = x.properties["b"] as TsTestValue.TsNumber xa.number + xb.number == r.number - }, - { x, r -> - (x is TsTestValue.TsUndefined || x is TsTestValue.TsNull) && r is TsTestValue.TsException } ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Strings.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Strings.kt new file mode 100644 index 0000000000..0fe17bef9a --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Strings.kt @@ -0,0 +1,160 @@ +package org.usvm.samples + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner + +class Strings : TsMethodTestRunner() { + + private val className = this::class.simpleName!! + + override val scene: EtsScene = loadSampleScene(className) + + @Test + fun `test typeOfString`() { + val method = getMethod(className, "typeOfString") + discoverProperties( + method = method, + { r -> r.value == "string" }, + ) + } + + @Test + fun `test typeOfNumber`() { + val method = getMethod(className, "typeOfNumber") + discoverProperties( + method = method, + { r -> r.value == "number" }, + ) + } + + @Test + fun `test typeOfBoolean`() { + val method = getMethod(className, "typeOfBoolean") + discoverProperties( + method = method, + { r -> r.value == "boolean" }, + ) + } + + @Test + fun `test typeOfUndefined`() { + val method = getMethod(className, "typeOfUndefined") + discoverProperties( + method = method, + { r -> r.value == "undefined" }, + ) + } + + @Test + fun `test typeOfNull`() { + val method = getMethod(className, "typeOfNull") + discoverProperties( + method = method, + { r -> r.value == "object" }, + ) + } + + @Test + fun `test typeOfObject`() { + val method = getMethod(className, "typeOfObject") + discoverProperties( + method = method, + { r -> r.value == "object" }, + ) + } + + @Test + fun `test typeOfArray`() { + val method = getMethod(className, "typeOfArray") + discoverProperties( + method = method, + { r -> r.value == "object" }, + ) + } + + @Disabled("Functions are not supported yet") + @Test + fun `test typeOfFunction`() { + val method = getMethod(className, "typeOfFunction") + discoverProperties( + method = method, + { r -> r.value == "function" }, + ) + } + + @Test + fun `test typeOfInputString`() { + val method = getMethod(className, "typeOfInputString") + discoverProperties( + method = method, + { _, r -> r.value == "string" }, + ) + } + + @Test + fun `test typeOfInputNumber`() { + val method = getMethod(className, "typeOfInputNumber") + discoverProperties( + method = method, + { _, r -> r.value == "number" }, + ) + } + + @Test + fun `test typeOfInputBoolean`() { + val method = getMethod(className, "typeOfInputBoolean") + discoverProperties( + method = method, + { _, r -> r.value == "boolean" }, + ) + } + + @Test + fun `test typeOfInputUndefined`() { + val method = getMethod(className, "typeOfInputUndefined") + discoverProperties( + method = method, + { _, r -> r.value == "undefined" }, + ) + } + + @Test + fun `test typeOfInputNull`() { + val method = getMethod(className, "typeOfInputNull") + discoverProperties( + method = method, + { _, r -> r.value == "object" }, + ) + } + + @Test + fun `test typeOfInputObject`() { + val method = getMethod(className, "typeOfInputObject") + discoverProperties( + method = method, + { _, r -> r.value == "object" }, + ) + } + + @Test + fun `test typeOfInputArray`() { + val method = getMethod(className, "typeOfInputArray") + discoverProperties, TsTestValue.TsString>( + method = method, + { _, r -> r.value == "object" }, + ) + } + + @Disabled("Functions are not supported yet") + @Test + fun `test typeOfInputFunction`() { + val method = getMethod(className, "typeOfInputFunction") + discoverProperties( + method = method, + { _, r -> r.value == "function" }, + ) + } +} 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 14736f7b5b..c808a9f989 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 @@ -13,21 +13,21 @@ class InputArrays : TsMethodTestRunner() { @Test fun testInputArrayOfNumbers() { val method = getMethod(className, "inputArrayOfNumbers") - discoverProperties( + discoverProperties, TsTestValue>( method = method, - { x, r -> x is TsTestValue.TsUndefined && r is TsTestValue.TsException }, + { x, r -> r is TsTestValue.TsException }, { x, r -> r as TsTestValue.TsNumber - - x is TsTestValue.TsArray<*> && (x.values[0] as? TsTestValue.TsNumber)?.number == 1.0 && r.number == 1.0 + (x.values[0] as TsTestValue.TsNumber).number == 1.0 && r.number == 1.0 }, { x, r -> r as TsTestValue.TsNumber - - x is TsTestValue.TsArray<*> && (x.values[0] as? TsTestValue.TsNumber)?.number != 1.0 && r.number == 2.0 + (x.values[0] as TsTestValue.TsNumber).number != 1.0 && r.number == 2.0 }, invariants = arrayOf( - { _, r -> r !is TsTestValue.TsNumber || r.number != -1.0 } + { _, r -> + r !is TsTestValue.TsNumber || r.number != -1.0 + } ) ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt index 9a619d7ce6..6ac42ddb93 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt @@ -13,11 +13,12 @@ class ObjectUsage : TsMethodTestRunner() { @Test fun `object as parameter`() { val method = getMethod(className, "objectAsParameter") - discoverProperties( + discoverProperties( method = method, - { value, r -> value is TsTestValue.TsClass && value.name == "Object" && r.number == 42.0 }, - { value, r -> value == TsTestValue.TsUndefined && r.number == -1.0 } + { x, r -> r.number == 42.0 }, + invariants = arrayOf( + { _, r -> r.number != -1.0 } + ) ) } - -} \ No newline at end of file +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Truthy.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Truthy.kt index 3145db47a1..6a334a7090 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/Truthy.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Truthy.kt @@ -13,7 +13,3 @@ fun isTruthy(x: TsTestValue.TsNumber): Boolean { fun isTruthy(x: TsTestValue.TsClass): Boolean { return true } - -fun isTruthy(x: TsTestValue.TsObject): Boolean { - return x.addr != 0 -} 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 c2a338a3ed..58d5b1702c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -310,8 +310,6 @@ abstract class TsMethodTestRunner : TestRunner EtsNumberType TsTestValue.TsNumber.TsInteger::class -> EtsNumberType TsTestValue.TsUndefined::class -> EtsUndefinedType - // TODO: EtsUnknownType is mock up here. Correct implementation required. - TsTestValue.TsObject::class -> EtsUnknownType // For untyped tests, not to limit objects serialized from models after type coercion. TsTestValue.TsUnknown::class -> EtsUnknownType TsTestValue.TsNull::class -> EtsNullType diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index fcaca8fa1f..d7b6075001 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -36,6 +36,7 @@ import org.usvm.api.typeStreamOf import org.usvm.collection.array.UArrayIndexLValue import org.usvm.collection.field.UFieldLValue import org.usvm.isAllocated +import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUnresolvedSort @@ -163,25 +164,24 @@ open class TsTestStateResolver( ): TsTestValue = with(ctx) { when (expr.sort) { fp64Sort -> { - this@TsTestStateResolver.resolvePrimitive(expr, EtsNumberType) + resolvePrimitive(expr, EtsNumberType) } boolSort -> { - this@TsTestStateResolver.resolvePrimitive(expr, EtsBooleanType) + resolvePrimitive(expr, EtsBooleanType) } addressSort -> { if (expr.isFakeObject()) { - this@TsTestStateResolver.resolveFakeObject(expr) + resolveFakeObject(expr) } else { - this@TsTestStateResolver.resolveTsValue( - expr.asExpr(this@TsTestStateResolver.ctx.addressSort), - ) + val ref = expr.asExpr(addressSort) + resolveTsValue(ref) } } sizeSort -> { - this@TsTestStateResolver.resolvePrimitive(expr, EtsNumberType) + resolvePrimitive(expr, EtsNumberType) } else -> TODO("Unsupported sort: ${expr.sort}") @@ -225,6 +225,14 @@ open class TsTestStateResolver( resolveTsValue(heapRef) } + is EtsStringType -> { + if (isAllocatedConcreteHeapRef(concreteRef)) { + resolveAllocatedString(concreteRef) + } else { + TsTestValue.TsString("String construction is not yet implemented") + } + } + else -> error("Unexpected type: $type") } } @@ -292,6 +300,15 @@ open class TsTestStateResolver( return TsTestValue.TsArray(values) } + private fun resolveAllocatedString( + ref: UConcreteHeapRef, + ): TsTestValue.TsString = with(ctx) { + val value = ctx.heapRefToStringConstant[ref] ?: run { + error("String constant not found for ref: $ref") + } + return TsTestValue.TsString(value) + } + fun resolveThisInstance(): TsTestValue? { val parametersCount = method.parameters.size val ref = mkRegisterStackLValue(ctx.addressSort, parametersCount) // TODO check for statics diff --git a/usvm-ts/src/test/resources/samples/Strings.ts b/usvm-ts/src/test/resources/samples/Strings.ts new file mode 100644 index 0000000000..c2428b01ff --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Strings.ts @@ -0,0 +1,76 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class Strings { + typeOfString(): string { + let x = "hello" + return typeof x // "string" + } + + typeOfNumber(): string { + let x = 42 + return typeof x // "number" + } + + typeOfBoolean(): string { + let x = true + return typeof x // "boolean" + } + + typeOfUndefined(): string { + let x = undefined + return typeof x // "undefined" + } + + typeOfNull(): string { + let x = null + return typeof x // "object" + } + + typeOfObject(): string { + let x = {} + return typeof x // "object" + } + + typeOfArray(): string { + let x = [5, 42] + return typeof x // "object" + } + + typeOfFunction(): string { + let x = function() {} + return typeof x // "function" + } + + typeOfInputString(x: string): string { + return typeof x // "string" + } + + typeOfInputNumber(x: number): string { + return typeof x // "number" + } + + typeOfInputBoolean(x: boolean): string { + return typeof x // "boolean" + } + + typeOfInputUndefined(x: undefined): string { + return typeof x // "undefined" + } + + typeOfInputNull(x: null): string { + return typeof x // "object" + } + + typeOfInputObject(x: {}): string { + return typeof x // "object" + } + + typeOfInputArray(x: any[]): string { + return typeof x // "object" + } + + typeOfInputFunction(x: Function): string { + return typeof x // "function" + } +} diff --git a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts index cfb7838c78..2917303c0f 100644 --- a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts @@ -4,7 +4,7 @@ class InputArrays { inputArrayOfNumbers(x: number[]) { if (x[0] === 1) return 1 - if (x[0] == undefined) return -1 + if (x[0] === undefined) return -1 return 2 } diff --git a/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts index 38c8ae127a..d3f8b51a02 100644 --- a/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts +++ b/usvm-ts/src/test/resources/samples/types/ObjectUsage.ts @@ -2,11 +2,8 @@ // noinspection JSUnusedGlobalSymbols class ObjectUsage { - objectAsParameter(object: Object): number { - if (object == undefined) { - return -1 - } - + objectAsParameter(x: {}): number { + 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 724703393f..fba8af6974 100644 --- a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts +++ b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts @@ -43,10 +43,11 @@ class D { class Example { testFunction(): C { - const obj: A = new B(11); - const number = obj.foo(); + const x: A = new B(11); + const bar = x.foo(); - const aaa: C = new D(new A(number)); - return aaa + // noinspection UnnecessaryLocalVariableJS + const y: C = new D(new A(bar)); + return y } }