Objects support

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -2,6 +2,7 @@
 
 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.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 @@
         return mkConcreteHeapRef(address)
     }
 
+    fun UHeapRef.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<out USort>? {
+        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<UAddressSort> = undefinedValue
 
     fun mkTsNullValue(): UConcreteHeapRef = nullValue

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

@@ -407,16 +407,26 @@
             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 @@
             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 @@
             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
         }

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

@@ -5,8 +5,10 @@
 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.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 @@
                     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")
             }
 

usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt

@@ -56,21 +56,24 @@ sealed interface TsBinaryOperator {
         rhs: UExpr<out USort>,
         scope: TsStepScope,
     ): UExpr<out USort> {
-        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 {

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<EtsFieldSignature>) : EtsRefType {
+    override val typeName: String = "AuxiliaryType"
+
+    override fun <R> accept(visitor: EtsType.Visitor<R>): R {
+        error("Should not be called")
+    }
+}

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<TsValue.TsNumber>(
+            method = method,
+            { r -> r.number == 5.0 }
+        )
+    }
+
+    @Test
+    fun testCreateClassInstanceAndWriteField() {
+        val method = getMethod("Example", "createClassInstanceAndWriteField")
+        discoverProperties<TsValue.TsClass>(
+            method = method,
+            { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 14.0 }
+        )
+    }
+
+    @Test
+    fun testCreateClassInstanceAndWriteValueOfAnotherType() {
+        val method = getMethod("Example", "createClassInstanceAndWriteValueOfAnotherType")
+        discoverProperties<TsValue.TsClass>(
+            method = method,
+            { r -> r.properties.toList().single().second is TsValue.TsNull }
+        )
+    }
+
+    @Test
+    fun testCreateAnonymousClass() {
+        val method = getMethod("Example", "createAnonymousClass")
+        discoverProperties<TsValue.TsClass>(
+            method = method,
+            { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 15.0 }
+        )
+    }
+}