[TS PBT] Preserve runtime limitation diagnostics in property search

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

@@ -0,0 +1,81 @@
+package org.usvm.ts.pbt.dsl
+
+import org.junit.jupiter.api.Test
+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)
+
+    @Test
+    fun `sparse indexed growth reports its original source instead of unexplained exhaustion`() {
+        val program = defineProperty(id = "runtime.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)
+
+        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-index-growth" }
+        assertTrue(limitation.message.contains("ARRAY_INDEX_GROWTH"))
+        assertTrue(limitation.message.contains("array index write would grow beyond the current length"))
+        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 = 2)
+
+            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-index-growth" })
+        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 = 2)
+
+            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-index-growth" })
+        assertFailsWith<DslPropertyExecutionError> { run.requireSuccess() }
+    }
+}

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/UsvmPropertySearcher.kt

@@ -91,6 +91,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)
 
@@ -99,6 +100,7 @@ class UsvmPropertySearcher(
             options = machineOptions,
             tsOptions = tsOptions,
             machineObserver = observer,
+            observer = runtimeLimitations,
         ).use { machine ->
             val analysis = machine.analyzeWithMetadata(
                 methods = listOf(predicate.method),
@@ -135,17 +137,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())
         }
     }
 
@@ -282,6 +285,7 @@ class UsvmPropertySearcher(
         capability: UsvmPropertyProjectionCapability,
         analysis: TsMachineAnalysisResult,
         observer: UsvmViolationObserver,
+        runtimeLimited: Boolean,
     ): UsvmPropertySearchResult {
         val predicateCompleted = analysis.states.any { state ->
             state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE &&
@@ -293,6 +297,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,
+        )
+    }
+}