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 012702dbb7..525a50b9f1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -2,6 +2,7 @@ package org.usvm.machine import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr +import io.ksmt.utils.cast import org.jacodb.ets.base.EtsBooleanType import org.jacodb.ets.base.EtsNullType import org.jacodb.ets.base.EtsNumberType @@ -17,12 +18,15 @@ import org.usvm.UBv32Sort import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort import org.usvm.collection.field.UFieldLValue +import org.usvm.isTrue import org.usvm.machine.expr.TsUndefinedSort import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.FakeType +import org.usvm.types.single import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract @@ -102,6 +106,35 @@ class TsContext( return mkConcreteHeapRef(address) } + fun UHeapRef.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr? { + if (!isFakeObject()) return null + + val type = scope.calcOnState { + memory.types.getTypeStream(this@extractSingleValueFromFakeObjectOrNull).single() as FakeType + } + + return scope.calcOnState { + when { + type.boolTypeExpr.isTrue -> { + val lValue = getIntermediateBoolLValue(address) + memory.read(lValue).asExpr(boolSort) + } + + type.fpTypeExpr.isTrue -> { + val lValue = getIntermediateFpLValue(address) + memory.read(lValue).asExpr(fp64Sort) + } + + type.refTypeExpr.isTrue -> { + val lValue = getIntermediateRefLValue(address) + memory.read(lValue).asExpr(addressSort) + } + + else -> null + } + } + } + fun mkUndefinedValue(): UExpr = undefinedValue fun mkTsNullValue(): UConcreteHeapRef = nullValue 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 107ade9778..49343a96b8 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 @@ -407,16 +407,26 @@ class TsExprResolver( argumentTypes = { expr.method.parameters.map { it.type } }, ) { args -> doWithState { - val method = ctx.scene - .projectAndSdkClasses - .flatMap { it.methods } - .singleOrNull { it.signature == expr.method } - ?: error("Couldn't find a unique method with the signature ${expr.method}") + val method = if (expr.method.name == "constructor") { + ctx.scene + .projectAndSdkClasses + .map { it.ctor } + .singleOrNull { it.signature == expr.method } + ?: error("Couldn't find a unique constructor with the signature ${expr.method}") + } else { + ctx.scene + .projectAndSdkClasses + .flatMap { it.methods } + .singleOrNull { it.signature == expr.method } + ?: error("Couldn't find a unique method with the signature ${expr.method}") + } pushSortsForArguments(expr.instance, expr.args, localToIdx) callStack.push(method, currentStatement) - memory.stack.push(args.toTypedArray(), method.localsCount) + + val count = if (method.name == "%instInit") method.localsCount + 1 else method.localsCount + memory.stack.push(args.toTypedArray(), count) newStmt(method.cfg.stmts.first()) } @@ -508,6 +518,7 @@ class TsExprResolver( isSigned = true ) + // TODO isn't here any problem with reading from array as parameter? parameter[0] == 1 val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type) val expr = scope.calcOnState { memory.read(lValue) } @@ -548,13 +559,29 @@ class TsExprResolver( return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true) } - val fieldType = scene.fieldLookUp(value.field).type - val sort = typeToSort(fieldType) - val lValue = UFieldLValue(sort, instanceRef, value.field.name) + val lValue = UFieldLValue(addressSort, instanceRef, value.field.name) val expr = scope.calcOnState { memory.read(lValue) } - if (assertIsSubtype(expr, value.type)) { + // If we already wrote a fake object in a field, use it, otherwise, create it + // TODO probably we have to create a fake object with all possible types, ignoring the type from the scene + val resultExpr = if (expr.isFakeObject()) { expr + } else { + val fieldType = scene.fieldLookUp(value.field).type + val sort = typeToSort(fieldType) + val lValue = UFieldLValue(sort, instanceRef, value.field.name) + val currentExpr = scope.calcOnState { memory.read(lValue) } + + val fakeExpr = currentExpr.toFakeObject(scope) + + val fieldLValue = UFieldLValue(addressSort, instanceRef, value.field.name) + scope.calcOnState { memory.write(fieldLValue, fakeExpr, guard = trueExpr) } + + fakeExpr + } + + if (assertIsSubtype(expr, value.type)) { + resultExpr } else { null } 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 56b52981c5..6f63e04a90 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 @@ -5,8 +5,10 @@ import mu.KotlinLogging import org.jacodb.ets.base.EtsArrayAccess import org.jacodb.ets.base.EtsAssignStmt import org.jacodb.ets.base.EtsCallStmt +import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.base.EtsGotoStmt import org.jacodb.ets.base.EtsIfStmt +import org.jacodb.ets.base.EtsInstanceFieldRef import org.jacodb.ets.base.EtsLocal import org.jacodb.ets.base.EtsNopStmt import org.jacodb.ets.base.EtsNullType @@ -22,8 +24,10 @@ import org.jacodb.ets.model.EtsMethod import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UInterpreter +import org.usvm.api.evalTypeEquals import org.usvm.api.targets.TsTarget import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.collection.field.UFieldLValue import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList @@ -169,6 +173,14 @@ class TsInterpreter( memory.write(lValue, fakeExpr, guard = trueExpr) } + is EtsInstanceFieldRef -> { + val instance = exprResolver.resolve(lhv.instance)?.asExpr(ctx.addressSort) ?: return@doWithState + val exprValue = expr.toFakeObject(scope) + + val lValue = UFieldLValue(addressSort, instance, lhv.field.name) + memory.write(lValue, exprValue, guard = ctx.trueExpr) + } + else -> TODO("Not yet implemented") } 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 b114efb707..04d19cced4 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 @@ -56,21 +56,24 @@ sealed interface TsBinaryOperator { rhs: UExpr, scope: TsStepScope, ): UExpr { - if (lhs.isFakeObject() || rhs.isFakeObject()) { - return resolveFakeObject(lhs, rhs, scope) + val lhsValue = if (lhs.isFakeObject()) lhs.extractSingleValueFromFakeObjectOrNull(scope) ?: lhs else lhs + val rhsValue = if (rhs.isFakeObject()) rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs else rhs + + if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) { + return resolveFakeObject(lhsValue, rhsValue, scope) } - val lhsSort = lhs.sort - if (lhsSort == rhs.sort) { + val lhsSort = lhsValue.sort + if (lhsSort == rhsValue.sort) { return when (lhsSort) { - boolSort -> onBool(lhs.asExpr(boolSort), rhs.asExpr(boolSort), scope) - fp64Sort -> onFp(lhs.asExpr(fp64Sort), rhs.asExpr(fp64Sort), scope) - addressSort -> onRef(lhs.asExpr(addressSort), rhs.asExpr(addressSort), scope) + boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope) + fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope) + addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope) else -> TODO("Unsupported sort $lhsSort") } } - return internalResolve(lhs, rhs, scope) + return internalResolve(lhsValue, rhsValue, scope) } data object Eq : TsBinaryOperator { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt new file mode 100644 index 0000000000..c93f77a57d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt @@ -0,0 +1,17 @@ +package org.usvm.machine.types + +import com.jetbrains.rd.framework.util.RdCoroutineScope.Companion.override +import org.jacodb.ets.base.EtsRefType +import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsFieldSignature + +/** + * An artificial type that represents a set of properties. + */ +class AuxiliaryType(val properties: Set) : EtsRefType { + override val typeName: String = "AuxiliaryType" + + override fun accept(visitor: EtsType.Visitor): R { + error("Should not be called") + } +} \ No newline at end of file diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt new file mode 100644 index 0000000000..8e873ecf35 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt @@ -0,0 +1,53 @@ +package org.usvm.samples + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.api.TsValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.getResourcePath +import kotlin.test.Test + +class Objects : TsMethodTestRunner() { + override val scene: EtsScene = run { + val name = "Objects.ts" + val path = getResourcePath("/samples/$name") + val file = loadEtsFileAutoConvert(path) + EtsScene(listOf(file)) + } + + @Test + fun testCreateClassInstance() { + val method = getMethod("Example", "createClassInstance") + discoverProperties( + method = method, + { r -> r.number == 5.0 } + ) + } + + @Test + fun testCreateClassInstanceAndWriteField() { + val method = getMethod("Example", "createClassInstanceAndWriteField") + discoverProperties( + method = method, + { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 14.0 } + ) + } + + @Test + fun testCreateClassInstanceAndWriteValueOfAnotherType() { + val method = getMethod("Example", "createClassInstanceAndWriteValueOfAnotherType") + discoverProperties( + method = method, + { r -> r.properties.toList().single().second is TsValue.TsNull } + ) + } + + @Test + fun testCreateAnonymousClass() { + val method = getMethod("Example", "createAnonymousClass") + discoverProperties( + method = method, + { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 15.0 } + ) + } +} \ No newline at end of file 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 f5bc1209bd..71dbd1fcf2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -25,6 +25,7 @@ import org.jacodb.ets.model.EtsMethodSignature import org.usvm.UAddressSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.GlobalFieldValue import org.usvm.api.TsParametersState @@ -66,7 +67,7 @@ class TsTestResolver { is TsMethodResult.Success -> { afterMemoryScope.withMode(ResolveMode.CURRENT) { - resolveExpr(res.value, method.returnType) + resolveExpr(res.value, res.value, method.returnType) } } @@ -115,27 +116,35 @@ open class TsTestStateResolver( ) { fun resolveLValue(lValue: ULValue<*, *>, type: EtsType): TsValue { val expr = memory.read(lValue) - return resolveExpr(expr, type) + val symbolicRef = if (lValue.sort is UAddressSort) finalStateMemory.read(lValue).asExpr(ctx.addressSort) else null + return resolveExpr(expr, symbolicRef, type) } fun resolveExpr( expr: UExpr, + symbolicRef: UExpr? = null, type: EtsType, - ): TsValue = when (type) { - is EtsPrimitiveType -> resolvePrimitive(expr, type) - is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), type) - else -> resolveUnknownExpr(expr) + ): TsValue = with(ctx) { + if (expr.isFakeObject()) { + return resolveFakeObject(expr) + } + + return when (type) { + is EtsPrimitiveType -> resolvePrimitive(expr, type) + is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), symbolicRef?.asExpr(ctx.addressSort) ?: expr.asExpr(ctx.addressSort), type) + else -> resolveUnknownExpr(expr, symbolicRef) + } } - fun resolveUnknownExpr(expr: UExpr): TsValue = with(expr.tctx) { - when (expr.sort) { - fp64Sort -> resolvePrimitive(expr, EtsNumberType) - boolSort -> resolvePrimitive(expr, EtsBooleanType) + fun resolveUnknownExpr(heapRef: UExpr, finalStateMemoryRef: UExpr?): TsValue = with(heapRef.tctx) { + when (heapRef.sort) { + fp64Sort -> resolvePrimitive(heapRef, EtsNumberType) + boolSort -> resolvePrimitive(heapRef, EtsBooleanType) addressSort -> { - if (expr.isFakeObject()) { - resolveFakeObject(expr) + if (heapRef.isFakeObject()) { + resolveFakeObject(heapRef) } else { - resolveRef(expr.asExpr(ctx.addressSort), EtsUnknownType) + resolveRef(heapRef.asExpr(ctx.addressSort), finalStateMemoryRef?.asExpr(ctx.addressSort), EtsUnknownType) } } @@ -143,36 +152,45 @@ open class TsTestStateResolver( } } - private fun resolveRef(expr: UExpr, type: EtsType): TsValue { - val instance = model.eval(expr) as UConcreteHeapRef + private fun resolveRef( + heapRef: UExpr, + finalStateMemoryRef: UExpr?, + type: EtsType + ): TsValue { + val concreteRef = evaluateInModel(heapRef) as UConcreteHeapRef - if (instance.address == 0) { + if (concreteRef.address == 0) { return TsValue.TsUndefined } - if (model.eval(ctx.mkHeapRefEq(expr, ctx.mkTsNullValue())).isTrue) { + if (model.eval(ctx.mkHeapRefEq(heapRef, ctx.mkTsNullValue())).isTrue) { return TsValue.TsNull } return when (type) { - is EtsClassType -> resolveClass(instance, type) - is EtsArrayType -> resolveArray(instance, type) + is EtsClassType -> resolveClass(concreteRef, finalStateMemoryRef ?: heapRef, type) + is EtsArrayType -> resolveArray(concreteRef, finalStateMemoryRef ?: heapRef, type) is EtsUnknownType -> { - val type = finalStateMemory.types.getTypeStream(expr).first() - resolveRef(expr, type) + val type = finalStateMemory.types.getTypeStream(heapRef).first() + resolveRef(heapRef, finalStateMemoryRef, type) } else -> error("Unexpected type: $type") } } - private fun resolveArray(expr: UConcreteHeapRef, type: EtsArrayType): TsValue.TsArray<*> { - val arrayLengthLValue = UArrayLengthLValue(expr, type, ctx.sizeSort) + + private fun resolveArray( + concreteRef: UConcreteHeapRef, + heapRef: UHeapRef, + type: EtsArrayType + ): TsValue.TsArray<*> { + val arrayLengthLValue = UArrayLengthLValue(heapRef, type, ctx.sizeSort) val length = model.eval(memory.read(arrayLengthLValue)) as KBitVec32Value val values = (0 until length.intValue).map { val index = ctx.mkSizeExpr(it) - val lValue = UArrayIndexLValue(ctx.addressSort, expr, index, type) + val lValue = UArrayIndexLValue(ctx.addressSort, heapRef, index, type) val value = memory.read(lValue) if (model.eval(ctx.mkHeapRefEq(value, ctx.mkUndefinedValue())).isTrue) { @@ -223,7 +241,7 @@ open class TsTestStateResolver( // Note that everything about details of fake object we need to read from final state of the memory // since they are allocated objects val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), EtsBooleanType) + resolveExpr(model.eval(value), value, EtsBooleanType) } model.eval(type.fpTypeExpr).isTrue -> { @@ -231,7 +249,7 @@ open class TsTestStateResolver( // Note that everything about details of fake object we need to read from final state of the memory // since they are allocated objects val value = finalStateMemory.read(lValue) - resolveExpr(model.eval(value), EtsNumberType) + resolveExpr(model.eval(value), value, EtsNumberType) } model.eval(type.refTypeExpr).isTrue -> { @@ -241,7 +259,7 @@ open class TsTestStateResolver( val value = finalStateMemory.read(lValue) val ref = model.eval(value) // TODO mistake with signature, use TypeStream instead - resolveExpr(ref, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature)) + resolveExpr(ref, value, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature)) } else -> error("Unsupported") @@ -264,22 +282,10 @@ open class TsTestStateResolver( } private fun resolveClass( - expr: UExpr, + concreteRef: UConcreteHeapRef, + heapRef: UHeapRef, classType: EtsClassType, ): TsValue { - if (expr is UConcreteHeapRef && expr.address == 0) { - return TsValue.TsUndefined - } - - val nullRef = ctx.mkTsNullValue() - if (model.eval(ctx.mkHeapRefEq(expr.asExpr(ctx.addressSort), nullRef)).isTrue) { - return TsValue.TsNull - } - - check(expr.sort == ctx.addressSort) { - "Expected address sort, but got ${expr.sort}" - } - val clazz = ctx.scene.projectAndSdkClasses.firstOrNull { it.signature == classType.signature } ?: if (classType.signature.name == "Object") { EtsClassImpl( @@ -300,11 +306,19 @@ open class TsTestStateResolver( } val properties = clazz.fields.associate { field -> - val sort = ctx.typeToSort(field.type) - val lValue = UFieldLValue(sort, expr.asExpr(ctx.addressSort), field.name) - val fieldExpr = memory.read(lValue) - val obj = resolveExpr(fieldExpr, field.type) - field.name to obj + val lValue = UFieldLValue(ctx.addressSort, heapRef, field.name) + // read from final state memory since it is a fake object + val fieldExpr = finalStateMemory.read(lValue) + + with(ctx) { + if (model.eval(mkEq(fieldExpr, mkUndefinedValue())).isTrue) { + return@associate field.name to TsValue.TsUndefined + } + + check(fieldExpr.isFakeObject()) + val obj = resolveFakeObject(fieldExpr) + field.name to obj + } } return TsValue.TsClass(clazz.name, properties) } diff --git a/usvm-ts/src/test/resources/samples/Objects.ts b/usvm-ts/src/test/resources/samples/Objects.ts new file mode 100644 index 0000000000..31a9333a03 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/Objects.ts @@ -0,0 +1,32 @@ +class SimpleClass { + x = 5; +} + +class Example { + createClassInstance() { + let x = new SimpleClass(); + return x.x; + } + + createClassInstanceAndWriteField() { + let x = new SimpleClass(); + x.x = 14; + + return x; + } + + createClassInstanceAndWriteValueOfAnotherType() { + let x = new SimpleClass(); + x.x = true; + + if (x.x === true) { + x.x = null + } + + return x; + } + + createAnonymousClass() { + return { a : 15 }; + } +} \ No newline at end of file