[TS] Support bounded sparse indexed writes with known own slots

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt

@@ -4,6 +4,7 @@ import org.junit.jupiter.api.io.TempDir
 import org.usvm.SolverType
 import org.usvm.ts.pbt.model.ArrayDomain
 import org.usvm.ts.pbt.model.BooleanDomain
+import org.usvm.ts.pbt.model.ConstantDomain
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.NumberDomain
@@ -219,28 +220,41 @@ class CallsClassDataRegistryOracleTest {
             constructorInputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)),
         )
 
-        val result = CurrentTsCallsClassCoverageEngine().search(
-            CallsClassSearchRequest(
-                harness = harness,
-                profile = CallsExperimentProfile.EMPTY_STOP,
-                frozenModelIds = emptySet(),
-                expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision,
-                seed = 1,
-                budget = 3.seconds,
-                timeQuantum = 100.milliseconds,
-                solverQueryLimit = 1.seconds,
-                solverType = SolverType.YICES,
-                candidateCap = 20,
-                requireEntryPointWitness = true,
-            ),
-        )
+        // Coverage-directed search need not enumerate every input model for each entry point.
+        val branchInputs = listOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false))
+        val candidates = branchInputs.flatMap { flag ->
+            val inputs = listOf(PropertyInput(name = "flag", domain = ConstantDomain(flag)))
+            val branchHarness = harness.copy(
+                surface = harness.surface.copy(constructorInputs = inputs),
+                functions = harness.functions.map { it.copy(inputs = inputs) },
+            )
+            val result = CurrentTsCallsClassCoverageEngine().search(
+                CallsClassSearchRequest(
+                    harness = branchHarness,
+                    profile = CallsExperimentProfile.EMPTY_STOP,
+                    frozenModelIds = emptySet(),
+                    expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision,
+                    seed = 1,
+                    budget = 3.seconds,
+                    timeQuantum = 100.milliseconds,
+                    solverQueryLimit = 1.seconds,
+                    solverType = SolverType.YICES,
+                    candidateCap = 20,
+                    requireEntryPointWitness = true,
+                ),
+            )
+
+            val scenarioIds = result.search.candidates.map { it.entryPointId }.toSet()
+            assertEquals(harness.scenarios.map { it.id }.toSet(), scenarioIds, "flag=$flag")
+            result.search.candidates.forEach { assertEquals(listOf(flag), it.inputs) }
+            result.search.candidates
+        }
 
         val constructorScenarioId = harness.scenarios.first().id
-        val constructorBranches = result.search.candidates.filter { it.entryPointId == constructorScenarioId }
+        val constructorBranches = candidates.filter { it.entryPointId == constructorScenarioId }
             .map { it.inputs.single() }.toSet()
         assertEquals(setOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)), constructorBranches)
-        assertEquals(harness.scenarios.map { it.id }.toSet(), result.search.candidates.map { it.entryPointId }.toSet())
-        for (candidate in result.search.candidates) {
+        for (candidate in candidates) {
             val index = harness.scenarios.indexOfFirst { it.id == candidate.entryPointId }
             val original = OriginalTypeScriptClassReplayer(
                 directory,

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt

@@ -0,0 +1,111 @@
+package org.usvm.ts.pbt.dsl
+
+import org.junit.jupiter.api.Test
+import org.usvm.machine.TsOptions
+import org.usvm.ts.pbt.backend.PropertyRunConfiguration
+import org.usvm.ts.pbt.backend.PropertyRunStatus
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.testResourcesRoot
+import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus
+import kotlin.test.assertEquals
+import kotlin.test.assertFailsWith
+import kotlin.test.assertNotNull
+import kotlin.test.assertNull
+import kotlin.test.assertTrue
+
+class RuntimeLimitationDslTest {
+    private val runner = DslPropertyRunner(
+        sourceRoots = listOf(testResourcesRoot().resolve("properties/dsl")),
+    )
+    private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 10, timeoutMillis = 10_000)
+    private val capacity = TsOptions().maxArraySize
+
+    @Test
+    fun `array capacity reports its original source instead of unexplained exhaustion`() {
+        val program = defineProperty(id = "runtime.capacity-write") {
+            val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "sparseWrite")
+            val index by int(min = capacity, max = capacity)
+
+            check(name = "read-back") { write(index) equalTo 123 }
+        }
+
+        val run = runner.run(program = program, engine = PropertyEngine.BOTH, configuration = configuration)
+
+        assertEquals(PropertyRunStatus.SUCCESS, run.concrete?.status)
+        val symbolic = assertNotNull(run.symbolic)
+        assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, symbolic.status)
+        assertNull(symbolic.inputs)
+        val limitation = symbolic.diagnostics.single { it.code == "usvm.runtime.array-length-capacity" }
+        assertTrue(limitation.message.contains("ARRAY_LENGTH_CAPACITY"))
+        assertTrue(limitation.message.contains("array index write exceeds configured length bound"))
+        assertTrue(limitation.message.contains("statement:"))
+        assertTrue(limitation.path.contains("runtime-limitations.ts:3:"), limitation.path)
+        assertFailsWith<DslPropertyExecutionError> { run.requireSuccess() }
+    }
+
+    @Test
+    fun `supported counterexample and its native replay survive an excluded path`() {
+        val program = defineProperty(id = "runtime.mixed-counterexample") {
+            val write = function<(Double) -> Double>(
+                module = "runtime-limitations.ts",
+                exportName = "supportedOrSparse",
+            )
+            val index by int(min = 0, max = capacity)
+
+            assume { (index equalTo 0) or (index equalTo capacity) }
+
+            check(name = "zero") { write(index) equalTo 0 }
+        }
+
+        val run = runner.run(program = program, engine = PropertyEngine.USVM, configuration = configuration)
+
+        val symbolic = assertNotNull(run.symbolic)
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, symbolic.status)
+        assertEquals(listOf(JsConcreteValue.number(0.0)), symbolic.inputs)
+        assertTrue(symbolic.diagnostics.any { it.code == "usvm.runtime.array-length-capacity" })
+        assertEquals(PropertyRunStatus.FAILURE, run.symbolicReplay?.status)
+        assertEquals("zero", run.symbolicReplay?.failure?.checkId)
+        assertFailsWith<DslPropertyAssertionError> { run.requireSuccess() }
+    }
+
+    @Test
+    fun `supported successful paths do not hide excluded model paths`() {
+        val program = defineProperty(id = "runtime.mixed-no-violation") {
+            val write = function<(Double) -> Double>(
+                module = "runtime-limitations.ts",
+                exportName = "supportedOrSparse",
+            )
+            val index by int(min = 0, max = capacity)
+
+            assume { (index equalTo 0) or (index equalTo capacity) }
+
+            check(name = "positive") { write(index) greaterThan 0 }
+        }
+
+        val run = runner.run(program = program, engine = PropertyEngine.USVM, configuration = configuration)
+
+        val symbolic = assertNotNull(run.symbolic)
+        assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, symbolic.status)
+        assertNull(symbolic.inputs)
+        assertTrue(symbolic.diagnostics.any { it.code == "usvm.runtime.array-length-capacity" })
+        assertFailsWith<DslPropertyExecutionError> { run.requireSuccess() }
+    }
+
+    @Test
+    fun `small sparse cache write now executes symbolically and agrees with native TypeScript`() {
+        val program = defineProperty(id = "runtime.supported-sparse-write") {
+            val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "sparseWrite")
+            val index by int(min = 2, max = 2)
+
+            check(name = "read-back") { write(index) equalTo 123 }
+        }
+
+        val run = runner.run(program = program, engine = PropertyEngine.BOTH, configuration = configuration)
+
+        run.requireSuccess()
+        assertEquals(PropertyRunStatus.SUCCESS, run.concrete?.status)
+        val symbolic = assertNotNull(run.symbolic)
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, symbolic.status)
+        assertTrue(symbolic.diagnostics.none { it.code.startsWith("usvm.runtime.") })
+    }
+}

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt

@@ -144,6 +144,28 @@ class PropertyExecutionConformanceTest {
         assertEquals(symbolicInputs, replay.counterexample)
     }
 
+    @Test
+    fun `sparse mutation resolves the original dense array and replays its violation`() {
+        val domain = ArrayDomain(element = IntegerDomain(min = 7, max = 7), minLength = 3, maxLength = 3)
+        val property = property(predicateExport = "sparseMutatesAndFails", domain = domain)
+        val manifest = property.toManifest()
+        val expectedInput = JsConcreteValue.Array(elements = List(size = 3) { JsConcreteValue.number(7.0) })
+
+        val search = searcher.search(manifest, mapper.map(manifest), exactCapability)
+        val inputs = assertNotNull(search.inputs, search.toString())
+        val replay = backend.run(
+            property = property,
+            configuration = configuration.copy(numRuns = 1, examples = listOf(inputs), timeoutMillis = 10_000),
+        )
+
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, search.status, search.toString())
+        assertEquals(listOf(expectedInput), inputs)
+        assertEquals(PropertyFailureKind.PROPERTY, replay.failure?.kind)
+        assertEquals(inputs, replay.counterexample)
+        assertTrue(inputs.single() in domain)
+        assertTrue(search.diagnostics.none { it.code.startsWith("usvm.runtime.") }, search.toString())
+    }
+
     @Test
     fun `plain object symbolic candidates replay with their entry values`() {
         val domain = ObjectDomain(mapOf("count" to IntegerDomain(min = 0, max = 2)))

usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts

@@ -161,6 +161,15 @@ export function mutatesAndFails(value: number[]): boolean {
     return false;
 }
 
+export function sparseMutatesAndFails(value: number[]): boolean {
+    const alias: any[] = value;
+    alias.length = 1;
+    alias[4] = 9;
+
+    return value.length !== 5 || value[0] !== 7 || value[1] !== undefined ||
+        value[2] !== undefined || value[3] !== undefined || value[4] !== 9;
+}
+
 
 class AnnotatedRecord {
     count: number = 0;

usvm-ts-fast-check/src/test/resources/properties/dsl/runtime-limitations.ts

@@ -0,0 +1,13 @@
+export function sparseWrite(index: number): number {
+    const cache: number[] = [];
+    cache[index] = 123;
+    return cache[index];
+}
+
+export function supportedOrSparse(index: number): number {
+    if (index === 0) {
+        return 1;
+    }
+
+    return sparseWrite(index);
+}

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt

@@ -37,6 +37,7 @@ import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.StringDomain
 import org.usvm.ts.pbt.model.TupleDomain
 import org.usvm.util.componentType
+import org.usvm.util.markDenseArrayOwnSlots
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
@@ -312,6 +313,8 @@ class UsvmDomainProjector(
                 writeArrayElement(array, etsType, index, element, guard)
             }
 
+            state.markDenseArrayOwnSlots(array = array, length = length, capacity = domain.maxLength)
+
             array
         }
 

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt

@@ -95,6 +95,7 @@ class UsvmPropertySearcher(
         lateinit var projection: UsvmDeclaredDomainProjection
         val target = UsvmViolationTsTarget()
         val observer = UsvmViolationObserver(target)
+        val runtimeLimitations = UsvmRuntimeLimitationObserver()
         val objectShapes = PlainObjectInputShapes(scene, manifest.inputs.map { it.domain })
         val domainProjector = UsvmDomainProjector(projectionOptions, objectShapes)
 
@@ -103,6 +104,7 @@ class UsvmPropertySearcher(
             options = machineOptions,
             tsOptions = tsOptions,
             machineObserver = observer,
+            observer = runtimeLimitations,
         ).use { machine ->
             val analysis = machine.analyzeWithMetadata(
                 methods = listOf(predicate.method),
@@ -139,17 +141,18 @@ class UsvmPropertySearcher(
                 capability = capability,
                 analysis = analysis,
             )
-            if (terminalFailure != null) {
-                return@use terminalFailure.withCandidate(candidate)
-            }
-
-            candidate
+            val runtimeDiagnostics = runtimeLimitations.diagnostics
+            val searchResult = terminalFailure?.withCandidate(candidate)
+                ?: candidate
                 ?: noViolationResult(
                     manifest = manifest,
                     capability = capability,
                     analysis = analysis,
                     observer = observer,
+                    runtimeLimited = runtimeDiagnostics.isNotEmpty(),
                 )
+
+            searchResult.copy(diagnostics = (searchResult.diagnostics + runtimeDiagnostics).distinct())
         }
     }
 
@@ -286,6 +289,7 @@ class UsvmPropertySearcher(
         capability: UsvmPropertyProjectionCapability,
         analysis: TsMachineAnalysisResult,
         observer: UsvmViolationObserver,
+        runtimeLimited: Boolean,
     ): UsvmPropertySearchResult {
         val predicateCompleted = analysis.states.any { state ->
             state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE &&
@@ -297,6 +301,7 @@ class UsvmPropertySearcher(
         val status = when {
             analysis.timedOut -> UsvmPropertySearchStatus.TIMEOUT
             observer.solverUnknown -> UsvmPropertySearchStatus.SOLVER_UNKNOWN
+            runtimeLimited -> UsvmPropertySearchStatus.UNSUPPORTED
             predicateCompleted -> UsvmPropertySearchStatus.NO_VIOLATION_REACHED
             preconditionRejected -> UsvmPropertySearchStatus.PRECONDITION_REJECTED
             else -> UsvmPropertySearchStatus.ENGINE_FAILURE

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt

@@ -0,0 +1,49 @@
+package org.usvm.ts.pbt.usvm
+
+import org.usvm.machine.TsInterpreterObserver
+import org.usvm.machine.TsRuntimeFeatureLimitationEvent
+import org.usvm.ts.pbt.backend.CapabilityDiagnostic
+
+/** Retains a bounded sample of distinct model boundaries without keeping live engine objects. */
+internal class UsvmRuntimeLimitationObserver : TsInterpreterObserver {
+    private val limitations = linkedSetOf<CapabilityDiagnostic>()
+    private var truncated = false
+
+    val diagnostics: List<CapabilityDiagnostic>
+        get() = limitations.toList() + if (truncated) listOf(TRUNCATED_DIAGNOSTIC) else emptyList()
+
+    override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
+        val location = event.statement.location
+        val origin = location.origin
+        val path = if (origin != null) {
+            // EtsIR origins use zero-based positions; diagnostics use ordinary editor coordinates.
+            "${origin.fileName}:${origin.startLine + 1}:${origin.startColumn + 1}-" +
+                "${origin.endLine + 1}:${origin.endColumn + 1}"
+        } else {
+            val method = location.method.signature
+            val source = method.enclosingClass.file.fileName
+            "$source#${method.name}[${location.index}]"
+        }
+        val diagnostic = CapabilityDiagnostic(
+            code = "usvm.runtime.${event.reason.name.lowercase().replace('_', '-')}",
+            message = "${event.reason.name}: ${event.detail}; statement: ${event.statement}",
+            path = path,
+        )
+        if (diagnostic in limitations) return
+
+        if (limitations.size < MAX_DIAGNOSTICS) {
+            limitations += diagnostic
+        } else {
+            truncated = true
+        }
+    }
+
+    private companion object {
+        const val MAX_DIAGNOSTICS = 64
+        val TRUNCATED_DIAGNOSTIC = CapabilityDiagnostic(
+            code = "usvm.runtime.diagnostics-truncated",
+            message = "Additional runtime limitations were omitted after $MAX_DIAGNOSTICS distinct diagnostics",
+            path = "predicate",
+        )
+    }
+}