Preserve runtime kinds of object literal fields

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

@@ -52,6 +52,7 @@ import org.usvm.util.mkStringBackingElementLValue
 import org.usvm.util.mkStringBackingLValue
 import org.usvm.util.mkStringBackingLengthLValue
 import org.usvm.util.resolveEtsField
+import org.usvm.util.boxArrayValue as boxRuntimeValue
 
 private val logger = KotlinLogging.logger {}
 
@@ -172,10 +173,10 @@ private fun TsContext.resolveDeclaredField(
         resolved = resolvedField,
         hierarchy = hierarchy,
     )
-    val declaredType = if (objectClass != null) {
-        declaredLiteralField?.type
-    } else {
-        (resolvedField as? TsResolutionResult.Unique)?.property?.type
+    val declaredType = when {
+        objectClass != null && writtenSort != null -> null
+        objectClass != null -> declaredLiteralField?.type
+        else -> (resolvedField as? TsResolutionResult.Unique)?.property?.type
     }
 
     val requiresDeclaredPresence = !wasWritten
@@ -362,8 +363,8 @@ private fun TsContext.readField(
 
         // If a fake object is already created and assigned to the field,
         // there is no need to recreate another one.
-        if (ref.isFakeObject()) {
-            ref
+        if (ref.hasFakeValueBranch()) {
+            boxRuntimeValue(scope = scope, value = ref)
         } else {
             val fakeObj = mkFakeValue(scope, bool, fp, ref)
             lValuesToAllocatedFakeObjects += refLValue to fakeObj

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

@@ -27,6 +27,7 @@ import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.resolveEtsField
 import org.usvm.util.truncateKnownArrayIndices
+import org.usvm.util.boxArrayValue as boxRuntimeValue
 
 private val logger = KotlinLogging.logger {}
 
@@ -209,8 +210,6 @@ fun TsContext.assignToInstanceField(
     if (wroteModeledErrorField) return Unit
 
     val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy)
-    val declaredObjectLiteralField = objectLiteralClass?.fields?.singleOrNull { it.name == field.name }
-    val newObjectLiteralField = objectLiteralClass != null && declaredObjectLiteralField == null
 
     // An object literal can acquire a new own property after creation. Requiring its
     // allocation type to declare the field would reject that valid JavaScript write.
@@ -222,13 +221,14 @@ fun TsContext.assignToInstanceField(
         scope.assert(fieldExists) ?: return null
     }
 
+    val containsBoxedValue = expr.sort == addressSort && expr.asExpr(addressSort).hasFakeValueBranch()
+
     // Determine the field sort.
     val sort = when {
-        declaredObjectLiteralField != null -> typeToSort(declaredObjectLiteralField.type)
-        newObjectLiteralField -> {
-            // An undeclared own property accepts any runtime kind. A fake wrapper
-            // has address storage even when its payload is a number or boolean.
-            if (expr.isFakeObject()) unresolvedSort else expr.sort
+        objectLiteralClass != null -> {
+            // Literal declarations describe inferred source types, not runtime restrictions.
+            // Optional values can be undefined even when the frontend inferred a primitive field.
+            if (containsBoxedValue) unresolvedSort else expr.sort
         }
 
         else -> when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) {
@@ -268,7 +268,7 @@ fun TsContext.assignToInstanceField(
     // Otherwise, assign expr directly.
     return scope.doWithState {
         if (sort is TsUnresolvedSort) {
-            val fakeObject = expr.toFakeObject(scope)
+            val fakeObject = boxRuntimeValue(scope = scope, value = expr)
             val lValue = mkFieldLValue(addressSort, unwrappedInstance, field)
             lValuesToAllocatedFakeObjects += lValue to fakeObject
             memory.write(lValue, fakeObject, guard = trueExpr)
@@ -291,7 +291,7 @@ fun TsContext.assignToInstanceField(
         memory.write(deletedFieldLValue(unwrappedInstance, field), falseExpr, guard = trueExpr)
         if (isAllocatedConcreteHeapRef(unwrappedInstance)) {
             writtenConcreteFields = writtenConcreteFields + (unwrappedInstance to field.name)
-            if (newObjectLiteralField) {
+            if (objectLiteralClass != null) {
                 saveObjectLiteralFieldSort(unwrappedInstance, field.name, sort)
             }
         }

usvm-ts/src/test/kotlin/org/usvm/samples/lang/ObjectLiteralRuntimeFields.kt

@@ -0,0 +1,59 @@
+package org.usvm.samples.lang
+
+import org.jacodb.ets.model.EtsScene
+import org.usvm.StateCollectionStrategy
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.eq
+import kotlin.test.Test
+
+class ObjectLiteralRuntimeFields : TsMethodTestRunner() {
+    override val scene: EtsScene = loadScene("/samples/lang/ObjectLiteralRuntimeFields.ts")
+
+    init {
+        options = options.copy(
+            stopOnCoverage = 0,
+            stateCollectionStrategy = StateCollectionStrategy.ALL,
+            throwExceptionOnStepFailure = true,
+        )
+    }
+
+    @Test
+    fun `forwarded optional Boolean preserves undefined false and true`() {
+        val method = getMethod("forwardOptionalBoolean")
+
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { present, _, result -> !present.value && (result eq -1) },
+            { present, include, result -> present.value && !include.value && (result eq 0) },
+            { present, include, result -> present.value && include.value && (result eq 1) },
+            invariants = arrayOf({ present, include, result ->
+                val expected = if (!present.value) -1 else if (include.value) 1 else 0
+                result eq expected
+            }),
+        )
+    }
+
+    @Test
+    fun `runtime storage follows each fork of the same literal`() {
+        val method = getMethod("branchWrites")
+
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { change, result -> change.value && (result eq 1) },
+            { change, result -> !change.value && (result eq 2) },
+            invariants = arrayOf({ change, result -> result eq if (change.value) 1 else 2 }),
+        )
+    }
+
+    @Test
+    fun `declared literal fields observe each later runtime kind`() {
+        val method = getMethod("declaredLiteralFieldsKeepRuntimeKinds")
+
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            { result -> result eq 1 },
+            invariants = arrayOf({ result -> result eq 1 }),
+        )
+    }
+}

usvm-ts/src/test/resources/samples/lang/ObjectLiteralRuntimeFields.ts

@@ -0,0 +1,47 @@
+// @ts-nocheck
+
+class ObjectLiteralRuntimeFields {
+    forwardOptionalBoolean(present: boolean, include: boolean): number {
+        let options: { alwaysIncludeMinute?: boolean } | undefined = undefined;
+        if (present) {
+            options = { alwaysIncludeMinute: include };
+        }
+
+        return this.readForwarded({ alwaysIncludeMinute: options?.alwaysIncludeMinute });
+    }
+
+    private readForwarded(options: { alwaysIncludeMinute?: boolean }): number {
+        if (options.alwaysIncludeMinute === undefined) return -1;
+        if (options.alwaysIncludeMinute) return 1;
+        return 0;
+    }
+
+    branchWrites(change: boolean): number {
+        const literal = { flag: true };
+        if (change) {
+            literal.flag = undefined;
+        } else {
+            literal.flag = false;
+        }
+
+        if (literal.flag === undefined) return 1;
+        return literal.flag === false ? 2 : 3;
+    }
+
+    declaredLiteralFieldsKeepRuntimeKinds(): number {
+        const literal = { flag: true, amount: 5, text: "old" };
+
+        literal.flag = undefined;
+        if (literal.flag !== undefined) return -1;
+
+        literal.amount = false;
+        if (literal.amount !== false) return -2;
+
+        literal.text = 9;
+        if (typeof literal.text !== "number" || literal.text !== 9) return -3;
+
+        literal.flag = true;
+        if (literal.flag !== true) return -4;
+        return 1;
+    }
+}