[TS] Preserve dense array search applicability after payload writes

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() &&
                             (

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",

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 };