Objects support

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
         }

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/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 }
+        )
+    }
+}

usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt

@@ -121,10 +121,16 @@ open class TsTestStateResolver(
     fun resolveExpr(
         expr: UExpr<out USort>,
         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<out USort>): 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)
     }

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 };
+    }
+}