[TS] Track deletion of object properties

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

@@ -0,0 +1,86 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsFieldSignature
+import org.usvm.UBoolExpr
+import org.usvm.UBoolSort
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.machine.TsContext
+import org.usvm.memory.UFlatUpdates
+import org.usvm.memory.ULValue
+import org.usvm.memory.UMemoryRegion
+import org.usvm.memory.UMemoryRegionId
+import org.usvm.memory.UMemoryUpdatesVisitor
+import org.usvm.memory.USymbolicCollectionUpdates
+import org.usvm.memory.UUpdateNode
+import org.usvm.memory.key.UHeapRefKeyInfo
+import org.usvm.uctx
+
+/** Separate from value storage: a deleted property has no value in any sort. */
+internal data class DeletedFieldLValue(
+    override val sort: UBoolSort,
+    override val key: UHeapRef,
+    val name: String,
+) : ULValue<UHeapRef, UBoolSort> {
+    override val memoryRegionId: UMemoryRegionId<UHeapRef, UBoolSort> = DeletedFieldRegionId(name, sort)
+}
+
+private data class DeletedFieldRegionId(
+    val name: String,
+    override val sort: UBoolSort,
+) : UMemoryRegionId<UHeapRef, UBoolSort> {
+    override fun emptyRegion(): UMemoryRegion<UHeapRef, UBoolSort> = DeletedFieldRegion(sort)
+}
+
+/** The marker records execution events, so input references also start with no deletion. */
+private class DeletedFieldRegion(
+    private val sort: UBoolSort,
+    private val updates: USymbolicCollectionUpdates<UHeapRef, UBoolSort> = UFlatUpdates(UHeapRefKeyInfo),
+) : UMemoryRegion<UHeapRef, UBoolSort> {
+    override fun read(key: UHeapRef): UBoolExpr {
+        val ctx = sort.uctx
+        val visitor = object : UMemoryUpdatesVisitor<UHeapRef, UBoolSort, UBoolExpr> {
+            override fun visitSelect(result: UBoolExpr, key: UHeapRef): UBoolExpr = result
+
+            override fun visitInitialValue(): UBoolExpr = ctx.falseExpr
+
+            override fun visitUpdate(previous: UBoolExpr, update: UUpdateNode<UHeapRef, UBoolSort>): UBoolExpr {
+                val guard = update.includesSymbolically(key, composer = null)
+                val value = update.value(key, composer = null)
+
+                return ctx.mkIte(guard, value, previous)
+            }
+        }
+
+        return updates.read(key, composer = null).accept(visitor, lookupCache = hashMapOf())
+    }
+
+    override fun write(
+        key: UHeapRef,
+        value: UExpr<UBoolSort>,
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership,
+    ): UMemoryRegion<UHeapRef, UBoolSort> = DeletedFieldRegion(sort, updates.write(key, value, guard))
+}
+
+// Reading these names after deleting an own property requires Object.prototype lookup.
+internal val OBJECT_PROTOTYPE_PROPERTIES = setOf(
+    "__defineGetter__",
+    "__defineSetter__",
+    "__lookupGetter__",
+    "__lookupSetter__",
+    "__proto__",
+    "constructor",
+    "hasOwnProperty",
+    "isPrototypeOf",
+    "propertyIsEnumerable",
+    "toLocaleString",
+    "toString",
+    "valueOf",
+)
+
+internal fun TsContext.deletedFieldLValue(
+    instance: UHeapRef,
+    field: EtsFieldSignature,
+): DeletedFieldLValue = DeletedFieldLValue(boolSort, instance, field.name)

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

@@ -17,10 +17,13 @@ import org.usvm.USort
 import org.usvm.USymbolicHeapRef
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.makeSymbolicRefUntyped
+import org.usvm.isFalse
+import org.usvm.isTrue
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.interpreter.ensureStaticsInitialized
 import org.usvm.machine.types.EtsAuxiliaryType
+import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.util.EtsHierarchy
 import org.usvm.util.TsResolutionResult
@@ -77,6 +80,9 @@ private fun TsContext.resolveField(
 ): UExpr<*>? {
     checkNotFake(instance)
 
+    val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) }
+    if (deleted.isTrue) return mkUndefinedValue()
+
     val resolvedField = resolveEtsField(instanceLocal, field, hierarchy)
     val sort = when (resolvedField) {
         is TsResolutionResult.Empty -> {
@@ -104,20 +110,31 @@ private fun TsContext.resolveField(
     scope.assert(fieldExists) ?: return null
 
     val value = readField(scope, instance, field, sort)
-    if (resolvedField !is TsResolutionResult.Unique || sort is TsUnresolvedSort) return value
-
-    val maxStringLength = scope.calcOnState { maxStringLength }
-    return when (val fieldType = resolvedField.property.type) {
-        is EtsStringLiteralType -> materializeTypedStringField(
-            scope = scope,
-            value = value.asExpr(addressSort),
-            literal = fieldType.value,
-            maxStringLength = maxStringLength,
-        )
+    val materializedValue = if (resolvedField !is TsResolutionResult.Unique || sort is TsUnresolvedSort) {
+        value
+    } else {
+        val maxStringLength = scope.calcOnState { maxStringLength }
+        when (val fieldType = resolvedField.property.type) {
+            is EtsStringLiteralType -> materializeTypedStringField(
+                scope = scope,
+                value = value.asExpr(addressSort),
+                literal = fieldType.value,
+                maxStringLength = maxStringLength,
+            )
 
-        is EtsStringType -> materializeTypedStringField(scope, value.asExpr(addressSort), maxStringLength)
-        else -> value
+            is EtsStringType -> materializeTypedStringField(scope, value.asExpr(addressSort), maxStringLength)
+            else -> value
+        } ?: return null
     }
+
+    if (deleted.isFalse) return materializedValue
+
+    return iteWriteIntoFakeObject(
+        scope = scope,
+        condition = deleted,
+        trueBranchValue = mkUndefinedValue(),
+        falseBranchValue = materializedValue,
+    )
 }
 
 /** Reading a field always produces a value; path validation belongs to [resolveField]. */

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

@@ -18,7 +18,9 @@ import org.jacodb.ets.model.EtsBitXorExpr
 import org.jacodb.ets.model.EtsBooleanConstant
 import org.jacodb.ets.model.EtsCastExpr
 import org.jacodb.ets.model.EtsCaughtExceptionRef
+import org.jacodb.ets.model.EtsClassCategory
 import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsClosureFieldRef
 import org.jacodb.ets.model.EtsConstant
 import org.jacodb.ets.model.EtsDeleteExpr
@@ -121,6 +123,8 @@ import org.usvm.sizeSort
 import org.usvm.types.singleOrNull
 import org.usvm.util.EtsHierarchy
 import org.usvm.util.SymbolResolutionResult
+import org.usvm.util.arrayStorageType
+import org.usvm.util.getAllMethods
 import org.usvm.util.isResolved
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
@@ -435,42 +439,76 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsDeleteExpr): UExpr<out USort>? = with(ctx) {
-        logger.warn {
-            "delete operator is not fully supported, the result may not be accurate"
-        }
-
-        // The delete operator removes a property from an object and returns true/false
-        // For property access like "delete obj.prop", we need to handle EtsInstanceFieldRef
         when (val operand = expr.arg) {
             is EtsInstanceFieldRef -> {
-                val instance = resolve(operand.instance)?.asExpr(addressSort) ?: return null
+                val resolved = resolve(operand.instance) ?: return null
+                val instance = if (resolved.isFakeObject()) {
+                    scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: return null
+                    resolved.extractRef(scope)
+                } else {
+                    resolved.asExpr(addressSort)
+                }
 
-                // Check for null/undefined access
                 checkUndefinedOrNullPropertyRead(scope, instance, operand.field.name) ?: return null
 
-                // For now, we simulate deletion by setting the property to undefined
-                // This is a simplification of the real semantics but sufficient for basic cases
-                // TODO: This is incorrect for cases that the existing field is not of sort Address.
-                //       In such case, the "overwriting" the field value with undefined does nothing
-                //       to the actual number/boolean/string value inside the field,
-                //       [if only we read the field using that "other" sort].
-                val fieldLValue = mkFieldLValue(addressSort, instance, operand.field)
+                val prototypeFallback = prototypeFallbackReason(instance, operand)
+                if (prototypeFallback != null) {
+                    throw UnsupportedOperationException(prototypeFallback)
+                }
+
                 scope.doWithState {
-                    memory.write(fieldLValue, mkUndefinedValue(), guard = trueExpr)
+                    memory.write(deletedFieldLValue(instance, operand.field), trueExpr, guard = trueExpr)
                 }
 
-                // The delete operator returns true in most cases for property deletion
                 mkTrue()
             }
 
+            is EtsCastExpr -> visit(EtsDeleteExpr(arg = operand.arg))
+
+            is EtsArrayAccess,
+            is EtsStaticFieldRef,
+            is EtsLocal,
+            is EtsParameterRef,
+            is EtsGlobalRef,
+            is EtsClosureFieldRef,
+            is EtsCaughtExceptionRef,
+            -> {
+                resolve(operand) ?: return null
+                throw UnsupportedOperationException("Deleting ${operand::class.simpleName} is not supported")
+            }
+
             else -> {
-                // For other operands (like variables), delete typically returns true without effect
-                resolve(operand) ?: return null // Evaluate for potential side effects
+                resolve(operand) ?: return null
                 mkTrue()
             }
         }
     }
 
+    private fun prototypeFallbackReason(instance: UHeapRef, operand: EtsInstanceFieldRef): String? {
+        val name = operand.field.name
+        if (name in OBJECT_PROTOTYPE_PROPERTIES) {
+            return "Deleting '$name' requires unsupported Object.prototype lookup"
+        }
+
+        val receiverType = scope.calcOnState { arrayStorageType(instance, operand.instance.type) }
+        if (receiverType is EtsArrayType) {
+            if (name == "length") {
+                return "Deleting Array.length is not supported"
+            }
+
+            return "Deleting a named Array property requires unsupported Array.prototype lookup"
+        }
+
+        if (receiverType !is EtsClassType) return null
+
+        val inheritedMethod = hierarchy.classesForType(receiverType)
+            .asSequence()
+            .filter { clazz -> clazz.category != EtsClassCategory.OBJECT }
+            .flatMap { clazz -> clazz.getAllMethods(hierarchy).asSequence() }
+            .any { method -> !method.isStatic && method.name == name }
+        return if (inheritedMethod) "Deleting '$name' requires unsupported class prototype method lookup" else null
+    }
+
     override fun visit(expr: EtsVoidExpr): UExpr<out USort>? = with(ctx) {
         // The void operator evaluates its operand for side effects and returns undefined.
         resolve(expr.arg) ?: return null

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

@@ -193,6 +193,8 @@ fun TsContext.assignToInstanceField(
                 memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
             }
         }
+
+        memory.write(deletedFieldLValue(unwrappedInstance, field), falseExpr, guard = trueExpr)
     }
 }