[TS] Preserve sparse array slots in source mutation models

usvm-ts/UNKNOWN_CALL_MODELS.md

@@ -84,6 +84,12 @@ The built-in catalog includes the following public APIs and their internal stora
 | `ts.error.constructor`, `ts.typeError.constructor` | TypeScript/EtsIR bodies | Genuine `new Error(message)` / `new TypeError(message)` with one string argument; initializes `name` and `message`. Other arities, coercions, subclasses, `cause` and stack inspection are outside these models. |
 | `ts.date.*` (38 IDs) | TypeScript/EtsIR bodies | Numeric Date construction, `UTC`, fixed-clock `now`, getters, setters, `valueOf`, and source `toISOString`; see the Date boundary below. |
 
+The `reverse` and `unshift` source models accept known own-slot presence as well as a current dense-array proof.
+Their TypeScript bodies distinguish missing slots from present values, including `undefined`, and use ordinary
+indexed writes and deletes to preserve holes and boxed overrides. Two model-owned primitives prepare trusted
+own-slot metadata and read slot presence. Model selection, application events, and residual fallback all use the
+normal dispatcher; receivers without either proof remain residual. These models retain the length/result bound of 16.
+
 Matching standard calls are assumed to refer to genuine builtins. Monkey patching and prototype replacement are
 outside this experiment; no runtime provenance protocol is imposed. Receiver and argument checks establish the
 memory representation and supported input domain.

usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt

@@ -150,20 +150,6 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         state.boundedArrayGuard(array, arrayType, maximumLength = MAX_SOURCE_ARRAY_LENGTH)
     }
 
-    private val unshiftDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
-        val (array, arrayType) = state.concreteArray(call, inputs)
-            ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr
-        val arguments = call.arguments.map { argument ->
-            argument.resolved ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr
-        }
-        val isDenseInput = state.isUnmodifiedDenseInputArray(array, arrayType)
-        if (!isDenseInput) {
-            return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr
-        }
-
-        state.boundedArrayGuard(array, arrayType, maximumLength = MAX_SOURCE_ARRAY_LENGTH - arguments.size)
-    }
-
     private val concatDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
         val (array, arrayType) = state.concreteArray(call, inputs)
             ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr
@@ -378,13 +364,13 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 id = "ts.array.reverse",
                 methodName = "reverse",
                 inputAdapter = noArgumentsAdapter,
-                domainGuard = denseReceiverDomain,
+                domainGuard = TsArraySlotPrimitives.reverseDomain,
             ),
             sourceModel(
                 id = "ts.array.unshift",
                 methodName = "unshift",
                 inputAdapter = variadicMutationAdapter,
-                domainGuard = unshiftDomain,
+                domainGuard = TsArraySlotPrimitives.unshiftDomain,
             ),
             sourceModel(
                 id = "ts.array.slice",
@@ -407,6 +393,16 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 arity = 1,
                 implementation = TsDenseArrayPrimitives::requireDense,
             ),
+            primitiveModel(
+                methodName = "prepareOwnSlots",
+                arity = 1,
+                implementation = TsArraySlotPrimitives::prepareOwnSlots,
+            ),
+            primitiveModel(
+                methodName = "hasOwnSlot",
+                arity = 2,
+                implementation = TsArraySlotPrimitives::hasOwnSlot,
+            ),
             primitiveModel(
                 methodName = "grow",
                 arity = 2,
@@ -444,6 +440,10 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
             domainGuard = domainGuard,
             inputAdapter = inputAdapter,
             requiredModelIds = buildSet {
+                if (methodName in setOf("reverse", "unshift")) {
+                    add("ts.array.primitive.prepareOwnSlots")
+                    add("ts.array.primitive.hasOwnSlot")
+                }
                 if (methodName == "join") {
                     add("ts.array.primitive.elementString")
                     add(TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID)

usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArraySlotPrimitives.kt

@@ -0,0 +1,90 @@
+package org.usvm.machine.call.intrinsic
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsUnknownType
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard
+import org.usvm.machine.call.TsUnknownCall
+import org.usvm.machine.call.TsUnknownCallModelCompletion
+import org.usvm.machine.call.TsUnknownCallModelExecution
+import org.usvm.machine.call.TsUnknownCallModelSuccessor
+import org.usvm.machine.expr.mkFpToUint32AfterValidation
+import org.usvm.machine.expr.mkValidArrayIndexProperty
+import org.usvm.machine.state.TsState
+import org.usvm.sizeSort
+import org.usvm.util.arrayStorageType
+import org.usvm.util.hasDenseArrayShape
+import org.usvm.util.knownArrayIndexPresence
+import org.usvm.util.markDenseArrayOwnSlots
+import org.usvm.util.mkArrayLengthLValue
+
+/** Own-slot metadata operations used by the source reverse and unshift algorithms. */
+internal object TsArraySlotPrimitives {
+    val reverseDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
+        knownSlotGuard(state, call, inputs, additionalSlots = 0)
+    }
+
+    val unshiftDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
+        knownSlotGuard(state, call, inputs, additionalSlots = call.arguments.size)
+    }
+
+    private fun knownSlotGuard(
+        state: TsState,
+        call: TsUnknownCall,
+        inputs: List<UExpr<*>>,
+        additionalSlots: Int,
+    ): UBoolExpr {
+        val (array, type) = state.concreteArray(call, inputs) ?: return state.ctx.falseExpr
+        val hasSlotProof = array in state.knownArrayPropertyPresence || state.hasDenseArrayShape(array, type)
+        if (!hasSlotProof) return state.ctx.falseExpr
+
+        return state.boundedArrayGuard(array, type, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY - additionalSlots)
+    }
+
+    fun prepareOwnSlots(state: TsState, inputs: List<UExpr<*>>): TsUnknownCallModelExecution? {
+        val array = inputs.single() as? UConcreteHeapRef ?: return null
+        val type = state.arrayStorageType(array, EtsArrayType(EtsUnknownType, dimensions = 1)) as? EtsArrayType
+            ?: return null
+        val hasKnownSlots = array in state.knownArrayPropertyPresence
+        val hasSlotProof = hasKnownSlots || state.hasDenseArrayShape(array, type)
+        if (!hasSlotProof) return null
+
+        val guard = state.boundedArrayGuard(array, type, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY)
+        val successor = TsUnknownCallModelSuccessor(
+            guard = guard,
+            completion = TsUnknownCallModelCompletion.Normal {
+                if (!hasKnownSlots) {
+                    val length = memory.read(mkArrayLengthLValue(array, type))
+                    markDenseArrayOwnSlots(array = array, length = length, capacity = SOURCE_ARRAY_MODEL_CAPACITY)
+                }
+
+                ctx.mkUndefinedValue()
+            },
+        )
+
+        return TsUnknownCallModelExecution(
+            successors = listOf(successor),
+            residualGuard = state.ctx.mkNot(guard),
+        )
+    }
+
+    fun hasOwnSlot(state: TsState, inputs: List<UExpr<*>>): TsUnknownCallModelExecution? = with(state.ctx) {
+        val array = inputs[0] as? UConcreteHeapRef ?: return null
+        val number = inputs[1].takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null
+        val guard = mkValidArrayIndexProperty(number)
+        val index = mkFpToUint32AfterValidation(number, guard).asExpr(sizeSort)
+        val present = state.knownArrayIndexPresence(array, index) ?: return null
+        val successor = TsUnknownCallModelSuccessor(
+            guard = guard,
+            completion = TsUnknownCallModelCompletion.Normal { present },
+        )
+
+        TsUnknownCallModelExecution(
+            successors = listOf(successor),
+            residualGuard = mkNot(guard),
+        )
+    }
+}

usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts

@@ -4,6 +4,8 @@ declare class ArrayModelPrimitives {
     static allocateLike(receiver: any[], length: number): any[];
     static elementString(value: any): string;
     static requireDense(receiver: any[]): void;
+    static prepareOwnSlots(receiver: any[]): void;
+    static hasOwnSlot(receiver: any[], index: number): boolean;
 }
 
 export class ArrayModels {
@@ -189,26 +191,38 @@ export class ArrayModels {
     }
 
     static reverse(receiver: any[]): any[] {
+        ArrayModelPrimitives.prepareOwnSlots(receiver);
         const length = receiver.length;
         let lower = 0;
         while (lower < Math.floor(length / 2)) {
             const upper = length - lower - 1;
-            const value = receiver[lower];
-            receiver[lower] = receiver[upper];
-            receiver[upper] = value;
+            const lowerPresent = ArrayModelPrimitives.hasOwnSlot(receiver, lower);
+            const upperPresent = ArrayModelPrimitives.hasOwnSlot(receiver, upper);
+            const lowerValue = receiver[lower];
+            const upperValue = receiver[upper];
+
+            if (upperPresent) receiver[lower] = upperValue;
+            else delete receiver[lower];
+
+            if (lowerPresent) receiver[upper] = lowerValue;
+            else delete receiver[upper];
+
             lower++;
         }
         return receiver;
     }
 
     static unshift(receiver: any[], first: any, second: any, third: any, count: number): number {
+        ArrayModelPrimitives.prepareOwnSlots(receiver);
         const length = receiver.length;
         const resultLength = length + count;
         ArrayModelPrimitives.grow(receiver, resultLength);
         let index = length;
         while (index > 0) {
             index--;
-            receiver[index + count] = receiver[index];
+            const present = ArrayModelPrimitives.hasOwnSlot(receiver, index);
+            if (present) receiver[index + count] = receiver[index];
+            else delete receiver[index + count];
         }
         if (count >= 1) receiver[0] = first;
         if (count >= 2) receiver[1] = second;

usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayMutationEtsIrModelTest.kt

@@ -122,8 +122,8 @@ class TsArrayMutationEtsIrModelTest {
     }
 
     @Test
-    fun `sparse reverse remains residual`() {
-        val result = analyze(methodName = "sparseReverseUsesResidual")
+    fun `reverse without a slot presence or dense input proof remains residual`() {
+        val result = analyze(methodName = "unprovenReverseUsesResidual")
 
         assertTrue(result.values.isEmpty())
         assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome)

usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt

@@ -193,6 +193,8 @@ class TsUnknownCallModelCatalogTest {
             "ts.array.primitive.allocateStrings",
             "ts.array.primitive.elementString",
             "ts.array.primitive.grow",
+            "ts.array.primitive.hasOwnSlot",
+            "ts.array.primitive.prepareOwnSlots",
             "ts.array.primitive.requireDense",
             "ts.array.primitive.truncateDense",
             "ts.array.push",

usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt

@@ -16,6 +16,10 @@ import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
 import org.usvm.machine.TsRuntimeFeatureLimitationReason
+import org.usvm.machine.call.TsUnknownCallDecision
+import org.usvm.machine.call.TsUnknownCallEvent
+import org.usvm.machine.call.TsUnknownCallFailureReason
+import org.usvm.machine.call.TsUnknownCallOutcome
 import org.usvm.util.TsMethodTestRunner
 import org.usvm.util.TsTestResolver
 import org.usvm.util.assertNodeReplay
@@ -36,10 +40,16 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() {
     override val tsOptions = TsOptions(maxArraySize = 6)
     override val runner: (EtsMethod, UMachineOptions) -> List<TsTest> = { method, machineOptions ->
         val limitations = mutableListOf<TsRuntimeFeatureLimitationEvent>()
+        val modelIds = mutableListOf<String>()
         val observer = object : TsInterpreterObserver {
             override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
                 limitations += event
             }
+
+            override fun onUnknownCall(event: TsUnknownCallEvent) {
+                val model = event.decision as? TsUnknownCallDecision.ModelApplied
+                if (model != null) modelIds += model.modelId
+            }
         }
 
         TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions, observer = observer).use { machine ->
@@ -48,6 +58,20 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() {
             assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, method.name)
             assertTrue(outcome.unsupportedPaths.isEmpty(), "${method.name}: ${outcome.unsupportedPaths}")
             assertTrue(limitations.isEmpty(), "${method.name}: $limitations")
+            val expectedModels = when (method.name) {
+                "movesPreserveHoles", "truncateAndMoveHoles" -> setOf("ts.array.reverse", "ts.array.unshift")
+                "reverseAsymmetricHoles", "reverseBoxedValues", "symbolicDeleteThenReverse" -> {
+                    setOf("ts.array.reverse")
+                }
+
+                "unshiftHoles", "unshiftSeveralHoles", "unshiftNoItems" -> setOf("ts.array.unshift")
+                else -> emptySet()
+            }
+            assertTrue(modelIds.containsAll(expectedModels), "${method.name}: $modelIds")
+            if (expectedModels.isNotEmpty()) {
+                assertTrue("ts.array.primitive.prepareOwnSlots" in modelIds, "${method.name}: $modelIds")
+                assertTrue("ts.array.primitive.hasOwnSlot" in modelIds, "${method.name}: $modelIds")
+            }
             outcome.states.map { state -> TsTestResolver().resolve(method, state) }
         }
     }
@@ -72,6 +96,24 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() {
         }
     }
 
+    @Test
+    fun `conditional holes reverse through the source model`() {
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method("symbolicDeleteThenReverse"),
+            { _, result -> result.number == 0.0 },
+            { _, result -> result.number == 1.0 },
+            { _, result -> result.number == 2.0 },
+            invariants = arrayOf({ index, result ->
+                val expected = when (index.number) {
+                    0.0 -> 1.0
+                    1.0 -> 2.0
+                    else -> 0.0
+                }
+                result.number == expected
+            }),
+        )
+    }
+
     @Test
     fun `symbolic deletion preserves conditional slot presence`() {
         discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
@@ -120,21 +162,32 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() {
     }
 
     @Test
-    fun `unknown array storage retains explicit iterator limitations`() {
-        for (name in listOf("unknownCopiedStorage", "unsupportedFillStorage")) {
+    fun `unproven copy and fill storage stop at the source model boundary`() {
+        for (name in listOf("unknownCopiedStorage", "unprovenPartialFillStorage")) {
             val limitations = mutableListOf<TsRuntimeFeatureLimitationReason>()
+            val unknownCalls = mutableListOf<TsUnknownCallEvent>()
             val observer = object : TsInterpreterObserver {
                 override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
                     limitations += event.reason
                 }
+
+                override fun onUnknownCall(event: TsUnknownCallEvent) {
+                    unknownCalls += event
+                }
             }
 
             TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine ->
                 val outcome = machine.analyzeWithOutcome(methods = listOf(method(name)))
 
                 assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, name)
                 assertTrue(outcome.states.isEmpty(), name)
-                assertEquals(listOf(TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED), limitations, name)
+                assertTrue(limitations.isEmpty(), "$name: $limitations")
+                val event = unknownCalls.single()
+                val expectedMethod = if (name == "unknownCopiedStorage") "slice" else "fill"
+
+                assertEquals(expectedMethod, event.callee.name, name)
+                assertEquals(TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, event.failureReason, name)
+                assertEquals(TsUnknownCallOutcome.PATH_STOPPED, event.outcome, name)
             }
         }
     }
@@ -146,7 +199,7 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() {
             for (name in supportedMethods) {
                 appendLine("if (SparseArrayIteratorSource.$name() !== 1) throw Error('$name');")
             }
-            for (name in listOf("symbolicDelete", "symbolicWriteThenDelete")) {
+            for (name in listOf("symbolicDelete", "symbolicWriteThenDelete", "symbolicDeleteThenReverse")) {
                 val tests = runner(method(name), options)
                 assertTrue(tests.isNotEmpty(), name)
                 for (test in tests) {
@@ -170,6 +223,7 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() {
     private val supportedMethods = listOf(
         "literalHoles", "newArrayHoles", "deletedSlot", "rewriteDeletedSlot", "movesPreserveHoles",
         "shiftMissingFirstSlot", "truncateAndMoveHoles", "destructureHoles", "forOfHoles", "liveDelete",
-        "sourceObjectLookalike",
+        "sourceObjectLookalike", "reverseAsymmetricHoles", "unshiftHoles", "fillAllHoles",
+        "unshiftSeveralHoles", "unshiftNoItems", "reverseBoxedValues",
     )
 }

usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts

@@ -77,7 +77,7 @@ export class ArrayMutationEtsIr {
             + result[3];
     }
 
-    sparseReverseUsesResidual(): number[] {
-        return new Array<number>(2).reverse();
+    unprovenReverseUsesResidual(values: number[]): number[] {
+        return values.reverse();
     }
 }