From 58c39de96fc539a2d78c95dd1940322e63594838 Mon Sep 17 00:00:00 2001
From: Aleksei Menshutin <a.menshutin@vkteam.ru>
Date: Fri, 16 Oct 2026 00:24:19 +0300
Subject: [PATCH] Preserve dense array search applicability across payload
 writes

---
 .../call/intrinsic/TsArrayEtsIrModelFamily.kt |  2 +-
 .../machine/call/TsGapModelsSourceTest.kt     | 13 ++++++++++
 .../test/resources/models/GapModelSource.ts   | 26 +++++++++++++++++++
 3 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt
index 7f92822687..6e54d99301 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt
@@ -85,7 +85,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 } else {
                     val elementSort = typeToSort(receiverType.componentType)
                     val hasNoMissingSlots = array is UConcreteHeapRef &&
-                        state.isUnmodifiedDenseInputArray(array, receiverType)
+                        state.hasDenseArrayShape(array, receiverType)
                     val excludesMissingSlot = when {
                         searchElement == mkUndefinedValue() &&
                             (
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt
index 434d42d9cb..bc302938c9 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt
@@ -94,6 +94,17 @@ class TsGapModelsSourceTest : TsMethodTestRunner() {
         }
     }
 
+    @Test
+    fun `dense searches preserve applicability after own unrelated and boxed writes`() {
+        for (name in listOf("denseSearchAfterWrite", "denseSearchAfterUnrelatedWrite", "denseSearchAfterBoxedWrite")) {
+            discoverProperties<TsTestValue.TsBoolean>(
+                method = method(name),
+                { result -> result.value },
+                invariants = arrayOf({ result -> result.value }),
+            )
+        }
+    }
+
     @Test
     fun `join preserves composition nullish elements and runtime boolean overrides`() {
         val expectedValues = mapOf(
@@ -265,6 +276,7 @@ class TsGapModelsSourceTest : TsMethodTestRunner() {
             "splitCallable" to "split",
             "splitLong" to "split",
             "reduceShrink" to "requireDense",
+            "searchAfterSlotDeletion" to "indexOf",
         )
 
         for ((name, callee) in residualCallees) {
@@ -385,6 +397,7 @@ class TsGapModelsSourceTest : TsMethodTestRunner() {
     fun `generated model witnesses replay in JavaScript`() {
         val methodNames = listOf(
             "splitEdges", "reduceAliases", "reduceEmptyError", "ignoredArguments", "composedMutations",
+            "denseSearchAfterWrite", "denseSearchAfterUnrelatedWrite", "denseSearchAfterBoxedWrite",
             "independentArrays", "joinRuntimeKinds", "joinNumbers", "reduceMutation", "reduceOmitted",
             "reduceUndefined",
             "reduceInitialEmpty", "reduceThrows", "symbolicBooleans", "symbolicNullish",
diff --git a/usvm-ts/src/test/resources/models/GapModelSource.ts b/usvm-ts/src/test/resources/models/GapModelSource.ts
index 8e922596ca..56fb9ea6d9 100644
--- a/usvm-ts/src/test/resources/models/GapModelSource.ts
+++ b/usvm-ts/src/test/resources/models/GapModelSource.ts
@@ -74,6 +74,32 @@ export class GapModelSource {
         return "a".split("").reduce((acc, value) => acc === undefined ? 8 : 9, undefined);
     }
 
+    denseSearchAfterWrite(): boolean {
+        const values = "a,b".split(",");
+        values[0] = "x";
+        return values.indexOf(undefined) === -1 && values.lastIndexOf(undefined) === -1;
+    }
+
+    denseSearchAfterUnrelatedWrite(): boolean {
+        const values = "a,b".split(",");
+        const other = "c,d".split(",");
+        other[0] = "x";
+        return values.indexOf(undefined) === -1 && values.lastIndexOf(undefined) === -1;
+    }
+
+    denseSearchAfterBoxedWrite(): boolean {
+        const values = "a,b".split(",") as any[];
+        values[0] = undefined;
+        return values.indexOf(undefined) === 0 && values.lastIndexOf(undefined) === 0 && values.includes(undefined);
+    }
+
+    searchAfterSlotDeletion(): number {
+        const values = "a,b".split(",");
+        values.reverse();
+        delete values[1];
+        return values.indexOf(undefined);
+    }
+
     reduceAliases(): boolean {
         const values = this.numbers();
         const seed = { total: 0 };