[TS] Model property presence and mutations on symbolic objects (#425)

usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt

@@ -127,6 +127,7 @@ inline fun <R> foldHeapRef(
             val (concreteHeapRefs, symbolicHeapRefs) = splitUHeapRef(
                 ref,
                 initialGuard,
+                ignoreNullRefs = ignoreNullRefs,
                 collapseHeapRefs = collapseHeapRefs,
                 staticIsConcrete = staticIsConcrete
             )

usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt

@@ -12,23 +12,23 @@ import org.usvm.UAddressSort
 import org.usvm.UBv32SizeExprProvider
 import org.usvm.UBv32Sort
 import org.usvm.UComponents
+import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UIteExpr
 import org.usvm.USizeSort
-import org.usvm.UConcreteHeapRef
 import org.usvm.api.allocateConcreteRef
 import org.usvm.api.initializeArrayLength
+import org.usvm.api.memcpy
 import org.usvm.api.readArrayIndex
 import org.usvm.api.readField
 import org.usvm.api.writeArrayIndex
 import org.usvm.api.writeField
 import org.usvm.collection.field.UInputFieldReading
-import org.usvm.sizeSort
-import org.usvm.mkSizeExpr
-import org.usvm.api.memcpy
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.constraints.UEqualityConstraints
 import org.usvm.constraints.UTypeConstraints
+import org.usvm.mkSizeExpr
+import org.usvm.sizeSort
 import kotlin.test.assertEquals
 import kotlin.test.assertIs
 import kotlin.test.assertNotNull
@@ -99,6 +99,25 @@ class HeapRefSplittingTest {
         assertEquals(!cond, reading.collection.updates.single().guard)
     }
 
+    @Test
+    fun `conditional null payloads round trip through input fields and arrays`() = with(ctx) {
+        val receiver = mkRegisterReading(idx = 0, sort = addressSort)
+        val payload = mkRegisterReading(idx = 1, sort = addressSort)
+        val array = allocateConcreteRef()
+        val condition by boolSort
+        val index = mkSizeExpr(0)
+        val alternatives = listOf(mkIte(condition, payload, nullRef), mkIte(condition, nullRef, payload))
+        val field = "nullablePayload"
+
+        alternatives.forEach { value ->
+            heap.writeField(receiver, field, addressSort, value, guard = trueExpr)
+            heap.writeArrayIndex(array, index, arrayDescr.first, arrayDescr.second, value, guard = trueExpr)
+
+            assertEquals(value, heap.readField(receiver, field, addressSort))
+            assertEquals(value, heap.readArrayIndex(array, index, arrayDescr.first, arrayDescr.second))
+        }
+    }
+
     @Test
     fun testInterleavedWritingToArray(): Unit = with(ctx) {
         val arrayRef = allocateConcreteRef()

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

@@ -3,10 +3,26 @@ package org.usvm.machine
 import org.usvm.machine.call.TsResidualCallPolicy
 import org.usvm.machine.call.TsUnknownCallModelSelection
 
+/** Initial own-property assumptions for symbolic input objects; writes and deletes always take precedence. */
+enum class TsInputPropertyPresence {
+    /** Required declared fields are present; optional and undeclared fields remain symbolic. */
+    DECLARED_FIELDS,
+
+    /** Every queried own property may initially be present or absent, independently of annotations. */
+    SYMBOLIC,
+
+    /** Every queried own property is initially present, possibly with an undefined value. */
+    ASSUME_PRESENT,
+
+    /** Every queried own property is initially absent. */
+    ASSUME_ABSENT,
+}
+
 data class TsOptions(
     val interproceduralAnalysis: Boolean = true,
     val enableVisualization: Boolean = false,
     val maxArraySize: Int = 1_000,
+    val inputPropertyPresence: TsInputPropertyPresence = TsInputPropertyPresence.DECLARED_FIELDS,
     val unknownCallModelSelection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All,
     val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH,
 )

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

@@ -10,6 +10,7 @@ import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.UIteExpr
+import org.usvm.UNullRef
 import org.usvm.UOrExpr
 import org.usvm.USort
 import org.usvm.USymbolicHeapRef
@@ -31,6 +32,27 @@ import org.usvm.util.boolToFp
 import org.usvm.util.mkStringBackingLValue
 import org.usvm.util.mkStringBackingLengthLValue
 
+/**
+ * Select one leaf reference for operations that depend on its allocation or storage type.
+ * The model only orders the branches: fork schedules the other feasible branch at the same statement.
+ */
+internal fun TsContext.resolveHeapRef(scope: TsStepScope, ref: UHeapRef): UHeapRef? {
+    var receiver = ref
+    while (receiver is UIteExpr<*>) {
+        val conditional = receiver
+        val takeTrueBranch = scope.calcOnState { models.first().eval(conditional.condition).isTrue }
+        val branchCondition = if (takeTrueBranch) conditional.condition else mkNot(conditional.condition)
+        scope.fork(branchCondition) ?: return null
+
+        receiver = if (takeTrueBranch) {
+            conditional.trueBranch.asExpr(addressSort)
+        } else {
+            conditional.falseBranch.asExpr(addressSort)
+        }
+    }
+    return receiver
+}
+
 fun TsContext.checkNotFake(expr: UExpr<*>) {
     require(!expr.isFakeObject()) {
         "Fake object handling should be done outside of this function"
@@ -40,6 +62,8 @@ fun TsContext.checkNotFake(expr: UExpr<*>) {
 // `any` is assignable both to and from string, so a type-relation query cannot identify
 // a materialized string. Inspect the concrete type stream before reading its backing array.
 private fun TsState.stringTypeCondition(ref: UHeapRef): UBoolExpr = with(ctx) {
+    if (ref is UNullRef) return@with falseExpr
+
     when (ref) {
         is UConcreteHeapRef, is USymbolicHeapRef -> {
             val type = memory.types.getTypeStream(ref).singleOrNull()

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

@@ -0,0 +1,189 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsField
+import org.jacodb.ets.model.EtsFieldImpl
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnclearRefType
+import org.usvm.UBoolExpr
+import org.usvm.UBoolSort
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.USort
+import org.usvm.collection.field.UFieldLValue
+import org.usvm.isFalse
+import org.usvm.machine.TsContext
+import org.usvm.machine.TsInputPropertyPresence
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.types.EtsFakeType
+import org.usvm.machine.types.EtsObjectType
+import org.usvm.machine.types.TsUnresolvedValue
+import org.usvm.machine.types.extractValue
+import org.usvm.machine.types.iteUnresolvedValue
+import org.usvm.memory.UReadOnlyMemory
+import org.usvm.util.EtsHierarchy
+import org.usvm.util.getAllMethods
+import org.usvm.util.mkFieldLValue
+
+private enum class PropertySlot {
+    INITIAL_PRESENCE,
+    BOOL_KIND,
+    NUMBER_KIND,
+    REF_KIND,
+    BOOL_VALUE,
+    NUMBER_VALUE,
+    REF_VALUE,
+}
+private data class PropertyField(val name: String, val slot: PropertySlot, val written: Boolean)
+
+private fun <S : USort> propertyLValue(sort: S, ref: UHeapRef, name: String, slot: PropertySlot, written: Boolean) =
+    UFieldLValue(sort, ref, PropertyField(name, slot, written))
+
+internal fun TsContext.initialPropertyPresenceLValue(ref: UHeapRef, name: String): UFieldLValue<*, UBoolSort> =
+    propertyLValue(boolSort, ref, name, PropertySlot.INITIAL_PRESENCE, written = false)
+
+/** Resolve only the receiver's declaration, never an unrelated same-name field in the scene. */
+internal fun declaredInputField(local: EtsLocal?, name: String, hierarchy: EtsHierarchy): EtsField? {
+    val type = local?.type
+    if (type !is EtsClassType && type !is EtsUnclearRefType) return null
+
+    val fields = hierarchy.classesForType(type).flatMap { receiver ->
+        val owners = hierarchy.getAncestors(receiver).filter { owner ->
+            owner.fields.any { !it.isStatic && it.name == name }
+        }
+        // A redeclaration shadows the ancestor's type and optional flag.
+        val nearestOwners = owners.filter { owner ->
+            owners.none { descendant -> owner != descendant && owner in hierarchy.getAncestors(descendant) }
+        }
+        nearestOwners.flatMap { owner -> owner.fields.filter { !it.isStatic && it.name == name } }
+    }
+    return fields.distinctBy { it.signature }.singleOrNull()
+}
+
+internal fun TsContext.trackInputProperty(
+    scope: TsStepScope,
+    instance: UHeapRef,
+    local: EtsLocal?,
+    name: String,
+    hierarchy: EtsHierarchy,
+): UBoolExpr? {
+    val unsupported = inputPropertyUnsupportedReason(local, name, hierarchy)
+    if (unsupported != null) throw UnsupportedOperationException(unsupported)
+
+    // Reference-sort payloads also contain strings; only runtime objects can receive own fields.
+    val objectReceiver = scope.calcOnState {
+        memory.types.evalIsSubtype(instance, EtsObjectType)
+    }
+    scope.assert(objectReceiver) ?: return null
+
+    val field = declaredInputField(local, name, hierarchy)
+    val initial = scope.calcOnState { memory.read(initialPropertyPresenceLValue(instance, name)) }
+    val assumedPresence = when (scope.calcOnState { inputPropertyPresence }) {
+        TsInputPropertyPresence.DECLARED_FIELDS -> {
+            if (field != null && (field as? EtsFieldImpl)?.isOptional != true) true else null
+        }
+        TsInputPropertyPresence.SYMBOLIC -> null
+        TsInputPropertyPresence.ASSUME_PRESENT -> true
+        TsInputPropertyPresence.ASSUME_ABSENT -> false
+    }
+    if (assumedPresence != null) {
+        val presenceConstraint = if (assumedPresence) initial else mkNot(initial)
+        scope.assert(presenceConstraint) ?: return null
+    }
+
+    scope.doWithState {
+        val optional = (field as? EtsFieldImpl)?.isOptional == true
+        trackedObjectProperties += TrackedObjectProperty(instance, name, field?.type, optional = optional)
+    }
+    return initial
+}
+
+private fun inputPropertyUnsupportedReason(local: EtsLocal?, name: String, hierarchy: EtsHierarchy): String? {
+    if (name in OBJECT_PROTOTYPE_PROPERTIES) return "Input property '$name' requires unsupported prototype lookup"
+
+    val type = local?.type
+    if (type is EtsArrayType) return "Named input array properties require array presence semantics"
+    if (type !is EtsClassType && type !is EtsUnclearRefType) return null
+
+    val inheritedMethod = hierarchy.classesForType(type).flatMap { it.getAllMethods(hierarchy) }
+        .any { !it.isStatic && it.name == name }
+    return if (inheritedMethod) "Input property '$name' requires unsupported class prototype lookup" else null
+}
+
+internal fun TsContext.inputPropertyPresence(
+    scope: TsStepScope,
+    instance: UHeapRef,
+    name: String,
+    initial: UBoolExpr,
+): UBoolExpr = scope.calcOnState {
+    val written = memory.read(writtenPropertyLValue(instance, name))
+    val deleted = memory.read(deletedFieldLValue(instance, name))
+    val everPresent = mkOr(initial, written)
+    mkAnd(everPresent, mkNot(deleted))
+}
+
+/** Input values use real field payloads; kind selectors and mutation payloads have separate synthetic regions. */
+internal fun TsContext.readInputPropertyValue(
+    memory: UReadOnlyMemory<EtsType>,
+    instance: UHeapRef,
+    name: String,
+    written: Boolean,
+): TsUnresolvedValue {
+    fun <S : USort> payload(sort: S, slot: PropertySlot): UExpr<S> = if (written) {
+        memory.read(propertyLValue(sort, instance, name, slot, written = true))
+    } else {
+        memory.read(mkFieldLValue(sort, instance, name))
+    }
+    fun kind(slot: PropertySlot) = memory.read(propertyLValue(boolSort, instance, name, slot, written))
+
+    val type = EtsFakeType(
+        boolTypeExpr = kind(PropertySlot.BOOL_KIND),
+        fpTypeExpr = kind(PropertySlot.NUMBER_KIND),
+        refTypeExpr = kind(PropertySlot.REF_KIND),
+    )
+    return TsUnresolvedValue(
+        boolValue = payload(boolSort, PropertySlot.BOOL_VALUE),
+        fpValue = payload(fp64Sort, PropertySlot.NUMBER_VALUE),
+        refValue = payload(addressSort, PropertySlot.REF_VALUE),
+        type = type,
+    )
+}
+
+internal fun TsContext.writeInputPropertyValue(scope: TsStepScope, instance: UHeapRef, name: String, value: UExpr<*>) {
+    scope.doWithState {
+        val (bool, boolKind) = extractValue(value, boolSort, ::getIntermediateBoolLValue)
+        val (number, numberKind) = extractValue(value, fp64Sort, ::getIntermediateFpLValue)
+        val (ref, refKind) = extractValue(value, addressSort, ::getIntermediateRefLValue)
+
+        fun <S : USort> write(slot: PropertySlot, sort: S, payload: UExpr<S>) {
+            val lValue = propertyLValue(sort, instance, name, slot, written = true)
+            memory.write(lValue, payload, guard = trueExpr)
+        }
+
+        write(PropertySlot.BOOL_KIND, boolSort, boolKind)
+        write(PropertySlot.NUMBER_KIND, boolSort, numberKind)
+        write(PropertySlot.REF_KIND, boolSort, refKind)
+        bool?.let { write(PropertySlot.BOOL_VALUE, boolSort, it) }
+        number?.let { write(PropertySlot.NUMBER_VALUE, fp64Sort, it) }
+        ref?.let { write(PropertySlot.REF_VALUE, addressSort, it) }
+
+        memory.write(writtenPropertyLValue(instance, name), trueExpr, guard = trueExpr)
+        memory.write(deletedFieldLValue(instance, name), falseExpr, guard = trueExpr)
+    }
+}
+
+/** Select payloads before materializing a wrapper, so symbolic aliases never turn wrappers into ordinary objects. */
+internal fun TsContext.currentInputPropertyValue(
+    memory: UReadOnlyMemory<EtsType>,
+    instance: UHeapRef,
+    name: String,
+    initial: TsUnresolvedValue,
+): TsUnresolvedValue {
+    val written = memory.read(writtenPropertyLValue(instance, name))
+    if (written.isFalse) return initial
+
+    val value = readInputPropertyValue(memory, instance, name, written = true)
+    return iteUnresolvedValue(written, value, initial)
+}

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

@@ -0,0 +1,74 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassCategory
+import org.jacodb.ets.model.EtsClassType
+import org.usvm.UBoolExpr
+import org.usvm.UHeapRef
+import org.usvm.api.typeStreamOf
+import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.isFalse
+import org.usvm.machine.TsContext
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.types.singleOrNull
+import org.usvm.util.EtsHierarchy
+
+internal const val PROTOTYPE_PROPERTY_NAME = "__proto__"
+
+// Reading these names after deleting an own property requires Object.prototype lookup.
+internal val OBJECT_PROTOTYPE_PROPERTIES = setOf(
+    "__defineGetter__",
+    "__defineSetter__",
+    "__lookupGetter__",
+    "__lookupSetter__",
+    PROTOTYPE_PROPERTY_NAME,
+    "constructor",
+    "hasOwnProperty",
+    "isPrototypeOf",
+    "propertyIsEnumerable",
+    "toLocaleString",
+    "toString",
+    "valueOf",
+)
+
+/** Allocated object literals retain their own declaration, independently of the local's widened type. */
+internal fun TsContext.objectLiteralClass(
+    scope: TsStepScope,
+    instance: UHeapRef,
+    hierarchy: EtsHierarchy,
+): EtsClass? {
+    if (!isAllocatedConcreteHeapRef(instance)) return null
+
+    val type = scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() } as? EtsClassType ?: return null
+    return hierarchy.classesForType(type).singleOrNull()?.takeIf { it.category == EtsClassCategory.OBJECT }
+}
+
+internal fun EtsClass.hasOwnProperty(name: String): Boolean =
+    fields.any { it.name == name } || methods.any { it.name == name }
+
+private fun TsStepScope.hasPrototypeMutation(instance: UHeapRef, clazz: EtsClass): Boolean = calcOnState {
+    clazz.fields.any { it.name == PROTOTYPE_PROPERTY_NAME } ||
+        (instance to PROTOTYPE_PROPERTY_NAME) in writtenConcreteFields
+}
+
+internal fun TsStepScope.ensureNoPrototypeMutation(instance: UHeapRef, clazz: EtsClass) {
+    // EtsIR records both { __proto__: value } and later assignments as ordinary fields.
+    if (hasPrototypeMutation(instance, clazz)) {
+        throw UnsupportedOperationException("Object literal prototype mutation in 'in' is not supported")
+    }
+}
+
+internal fun TsStepScope.ensureMissingPropertyHasNoPrototype(instance: UHeapRef, clazz: EtsClass, name: String) {
+    if (hasPrototypeMutation(instance, clazz) || name in OBJECT_PROTOTYPE_PROPERTIES) {
+        throw UnsupportedOperationException("Reading '$name' requires unsupported prototype lookup")
+    }
+}
+
+internal fun ensureOwnPropertyLookup(name: String, hasOwnProperty: Boolean, deleted: UBoolExpr) {
+    val ownPropertyMayBeMissing = !hasOwnProperty || !deleted.isFalse
+    val requiresPrototypeLookup = name == PROTOTYPE_PROPERTY_NAME ||
+        name in OBJECT_PROTOTYPE_PROPERTIES && ownPropertyMayBeMissing
+    if (requiresPrototypeLookup) {
+        throw UnsupportedOperationException("Prototype lookup for '$name' in 'in' is not supported")
+    }
+}