Debug commit

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

@@ -546,11 +546,18 @@ class TsExprResolver(
         checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
 
         // TODO: checkNullPointer(instanceRef)
-        val lValue = UFieldLValue(addressSort, instanceRef, value.field)
+        val fieldType = scene.fieldLookUp(value.field).type
+        val sort = typeToSort(fieldType)
+        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,6 +5,7 @@ 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
@@ -23,6 +24,7 @@ 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
@@ -171,7 +173,7 @@ class TsInterpreter(
                     val instance = exprResolver.resolve(lhv.instance)?.asExpr(ctx.addressSort) ?: return@doWithState
                     val exprValue = expr.toFakeObject(scope)
 
-                    val lValue = UFieldLValue(addressSort, instance, lhv.field)
+                    val lValue = UFieldLValue(addressSort, instance, lhv.field.name)
                     memory.write(lValue, exprValue, guard = ctx.trueExpr)
                 }
 

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/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) {
@@ -298,11 +304,12 @@ open class TsTestStateResolver(
             }
 
         val properties = clazz.fields.associate { field ->
-            val lValue = UFieldLValue(ctx.addressSort, expr.asExpr(ctx.addressSort), field.signature)
-            val fieldExpr = memory.read(lValue)
+            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(mkHeapRefEq(fieldExpr, mkUndefinedValue())).isTrue) {
+                if (model.eval(mkEq(fieldExpr, mkUndefinedValue())).isTrue) {
                     return@associate field.name to TsValue.TsUndefined
                 }