From 4c04f07f529937a5691c13c1f51e0b081cdf8484 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 18:28:40 +0300 Subject: [PATCH] Preserve runtime kinds when reading and writing object literal fields --- .../kotlin/org/usvm/machine/expr/ReadField.kt | 13 ++-- .../org/usvm/machine/expr/WriteField.kt | 18 +++--- .../lang/ObjectLiteralRuntimeFields.kt | 59 +++++++++++++++++++ .../lang/ObjectLiteralRuntimeFields.ts | 47 +++++++++++++++ 4 files changed, 122 insertions(+), 15 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/lang/ObjectLiteralRuntimeFields.kt create mode 100644 usvm-ts/src/test/resources/samples/lang/ObjectLiteralRuntimeFields.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 7593ac8c2a..22d93c21b2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 61acf67a0d..048b0b3b53 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/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) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/ObjectLiteralRuntimeFields.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/ObjectLiteralRuntimeFields.kt new file mode 100644 index 0000000000..c5d72d55a7 --- /dev/null +++ b/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( + 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( + 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( + method = method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/ObjectLiteralRuntimeFields.ts b/usvm-ts/src/test/resources/samples/lang/ObjectLiteralRuntimeFields.ts new file mode 100644 index 0000000000..60fa994dba --- /dev/null +++ b/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; + } +}