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 107ade977..d22cbd67d 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()) } @@ -553,8 +563,13 @@ class TsExprResolver( val lValue = UFieldLValue(sort, instanceRef, value.field.name) val expr = scope.calcOnState { memory.read(lValue) } + val fakeExpr = expr.toFakeObject(scope) + + val fieldLValue = UFieldLValue(addressSort, instanceRef, value.field.name) + scope.calcOnState { memory.write(fieldLValue, fakeExpr, guard = trueExpr) } + if (assertIsSubtype(expr, value.type)) { - expr + fakeExpr } 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 56b52981c..6f63e04a9 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/types/AuxiliaryType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/AuxiliaryType.kt new file mode 100644 index 000000000..c93f77a57 --- /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 000000000..8e873ecf3 --- /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 f5bc1209b..cbdc7190b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -121,10 +121,16 @@ open class TsTestStateResolver( fun resolveExpr( expr: UExpr, 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), type) + else -> resolveUnknownExpr(expr) + } } fun resolveUnknownExpr(expr: UExpr): TsValue = with(expr.tctx) { @@ -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, expr.asExpr(ctx.addressSort), 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 000000000..31a9333a0 --- /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