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

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

@@ -0,0 +1,105 @@
+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",
+        )
+    }
+}

usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt

@@ -0,0 +1,84 @@
+package org.usvm.ts.pbt.usvm
+
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsFileSignature
+import org.jacodb.ets.model.EtsMethodImpl
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsReturnStmt
+import org.jacodb.ets.model.EtsSourceSpan
+import org.jacodb.ets.model.EtsStmtLocation
+import org.jacodb.ets.model.EtsUndefinedType
+import org.junit.jupiter.api.Test
+import org.usvm.machine.TsRuntimeFeatureLimitationEvent
+import org.usvm.machine.TsRuntimeFeatureLimitationReason
+import kotlin.test.assertEquals
+import kotlin.test.assertTrue
+
+class UsvmRuntimeLimitationObserverTest {
+    @Test
+    fun `deduplicates identical events and retains the original statement location`() {
+        val observer = UsvmRuntimeLimitationObserver()
+        val event = event(detail = "sparse growth", withOrigin = true)
+
+        repeat(times = 100) { observer.onRuntimeFeatureLimitation(event) }
+
+        val diagnostic = observer.diagnostics.single()
+        assertEquals("usvm.runtime.array-index-growth", diagnostic.code)
+        assertEquals("original.ts:3:5-3:12", diagnostic.path)
+        assertTrue(diagnostic.message.contains("ARRAY_INDEX_GROWTH: sparse growth"))
+        assertTrue(diagnostic.message.contains("statement: ${event.statement}"))
+    }
+
+    @Test
+    fun `bounds unique diagnostics and reports truncation without losing retained records`() {
+        val observer = UsvmRuntimeLimitationObserver()
+        val first = event(detail = "first", withOrigin = false)
+        observer.onRuntimeFeatureLimitation(first)
+        val retained = observer.diagnostics.single()
+
+        repeat(times = 100) { index ->
+            observer.onRuntimeFeatureLimitation(first.copy(detail = "limitation $index"))
+        }
+
+        val diagnostics = observer.diagnostics
+        assertEquals(65, diagnostics.size)
+        assertEquals(retained, diagnostics.first())
+        assertEquals("generated.ts#example[0]", retained.path)
+        assertEquals("usvm.runtime.diagnostics-truncated", diagnostics.last().code)
+        assertEquals(diagnostics.size, diagnostics.distinct().size)
+    }
+
+    private fun event(detail: String, withOrigin: Boolean): TsRuntimeFeatureLimitationEvent {
+        val owner = EtsClassSignature(
+            name = "Example",
+            file = EtsFileSignature(projectName = "fixture", fileName = "generated.ts"),
+        )
+        val method = EtsMethodImpl(
+            EtsMethodSignature(
+                enclosingClass = owner,
+                name = "example",
+                parameters = emptyList(),
+                returnType = EtsUndefinedType,
+            ),
+        )
+        val location = EtsStmtLocation(method = method, index = 0)
+        if (withOrigin) {
+            location.origin = EtsSourceSpan(
+                fileName = "original.ts",
+                startOffset = 20,
+                endOffset = 27,
+                startLine = 2,
+                startColumn = 4,
+                endLine = 2,
+                endColumn = 11,
+                nodeKind = "ReturnStatement",
+            )
+        }
+
+        return TsRuntimeFeatureLimitationEvent(
+            statement = EtsReturnStmt(location = location, returnValue = null),
+            reason = TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH,
+            detail = detail,
+        )
+    }
+}