[TS] Track deletion of allocated object properties

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

@@ -0,0 +1,31 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsFieldSignature
+import org.usvm.UBoolSort
+import org.usvm.UHeapRef
+import org.usvm.collection.field.UFieldLValue
+import org.usvm.machine.TsContext
+
+/** Separate from value storage: a deleted property has no value in any sort. */
+internal data class DeletedField(val name: String)
+
+// 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,
+): UFieldLValue<DeletedField, UBoolSort> = UFieldLValue(boolSort, instance, DeletedField(field.name))

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

@@ -8,10 +8,14 @@ import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsStaticFieldRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.isAllocatedConcreteHeapRef
+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
@@ -65,6 +69,15 @@ fun TsContext.readField(
 ): UExpr<*> {
     checkNotFake(instance)
 
+    // Deletion of input references is not modeled. Reading their marker would introduce
+    // an unconstrained extra outcome even in programs that never use `delete`.
+    val deleted = if (isAllocatedConcreteHeapRef(instance)) {
+        scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) }
+    } else {
+        falseExpr
+    }
+    if (deleted.isTrue) return mkUndefinedValue()
+
     val sort = when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) {
         is TsResolutionResult.Empty -> {
             if (field.name !in listOf("i", "LogLevel")) {
@@ -93,32 +106,41 @@ fun TsContext.readField(
     }
 
     // If the field type is known, we can read it directly.
-    if (sort !is TsUnresolvedSort) {
+    val value = if (sort !is TsUnresolvedSort) {
         val lValue = mkFieldLValue(sort, instance, field)
-        return scope.calcOnState { memory.read(lValue) }
+        scope.calcOnState { memory.read(lValue) }
+    } else {
+        scope.calcOnState {
+            // If the field type is unknown, we create a fake object.
+            val boolLValue = mkFieldLValue(boolSort, instance, field)
+            val fpLValue = mkFieldLValue(fp64Sort, instance, field)
+            val refLValue = mkFieldLValue(addressSort, instance, field)
+
+            val bool = memory.read(boolLValue)
+            val fp = memory.read(fpLValue)
+            val ref = memory.read(refLValue)
+
+            // If a fake object is already created and assigned to the field,
+            // there is no need to recreate another one.
+            if (ref.isFakeObject()) {
+                ref
+            } else {
+                val fakeObj = mkFakeValue(scope, bool, fp, ref)
+                lValuesToAllocatedFakeObjects += refLValue to fakeObj
+                memory.write(refLValue, fakeObj, guard = trueExpr)
+                fakeObj
+            }
+        }
     }
 
-    // If the field type is unknown, we create a fake object.
-    return scope.calcOnState {
-        val boolLValue = mkFieldLValue(boolSort, instance, field)
-        val fpLValue = mkFieldLValue(fp64Sort, instance, field)
-        val refLValue = mkFieldLValue(addressSort, instance, field)
+    if (deleted.isFalse) return value
 
-        val bool = memory.read(boolLValue)
-        val fp = memory.read(fpLValue)
-        val ref = memory.read(refLValue)
-
-        // If a fake object is already created and assigned to the field,
-        // there is no need to recreate another one.
-        if (ref.isFakeObject()) {
-            ref
-        } else {
-            val fakeObj = mkFakeValue(scope, bool, fp, ref)
-            lValuesToAllocatedFakeObjects += refLValue to fakeObj
-            memory.write(refLValue, fakeObj, guard = trueExpr)
-            fakeObj
-        }
-    }
+    return iteWriteIntoFakeObject(
+        scope = scope,
+        condition = deleted,
+        trueBranchValue = mkUndefinedValue(),
+        falseBranchValue = value,
+    )
 }
 
 internal fun TsExprResolver.handleStaticFieldRef(

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
@@ -117,6 +119,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
@@ -429,42 +433,66 @@ 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)
+                if (!isAllocatedConcreteHeapRef(instance)) {
+                    throw UnsupportedOperationException("Deleting a property of an input object is not supported")
+                }
+
+                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()
             }
 
             else -> {
-                // For other operands (like variables), delete typically returns true without effect
-                resolve(operand) ?: return null // Evaluate for potential side effects
-                mkTrue()
+                resolve(operand) ?: return null
+                throw UnsupportedOperationException("Deleting ${operand::class.simpleName} is not supported")
             }
         }
     }
 
+    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

@@ -11,6 +11,7 @@ import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsStaticFieldRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.interpreter.ensureStaticsInitialized
@@ -193,6 +194,10 @@ fun TsContext.assignToInstanceField(
                 memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
             }
         }
+
+        if (isAllocatedConcreteHeapRef(unwrappedInstance)) {
+            memory.write(deletedFieldLValue(unwrappedInstance, field), falseExpr, guard = trueExpr)
+        }
     }
 }