diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt new file mode 100644 index 0000000000..98fc854d79 --- /dev/null +++ b/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 { 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 { 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 { run.requireSuccess() } + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/dsl/runtime-limitations.ts b/usvm-ts-fast-check/src/test/resources/properties/dsl/runtime-limitations.ts new file mode 100644 index 0000000000..c3ad30831f --- /dev/null +++ b/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); +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 10bf82289f..255ee3d5c2 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/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 diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt new file mode 100644 index 0000000000..1318a16ec1 --- /dev/null +++ b/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() + private var truncated = false + + val diagnostics: List + 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", + ) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt new file mode 100644 index 0000000000..1711e96f47 --- /dev/null +++ b/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, + ) + } +}