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..9cce5ae48e --- /dev/null +++ b/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 { 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 { 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 { 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.") }) + } +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt index 17978ced59..037ee17189 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt +++ b/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))) diff --git a/usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts index 0b663e437d..739846cb35 100644 --- a/usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts +++ b/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; 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/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt index 21463bce69..4015372b1c 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt +++ b/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 } 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 8e2cadda37..6efb200b4b 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 @@ -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 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, + ) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index 1e582d23c1..9cb70fe1e8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -19,6 +19,7 @@ import org.usvm.util.arrayStorageType import org.usvm.util.boxArrayValue import org.usvm.util.componentType import org.usvm.util.initializeTypedArrayOverrides +import org.usvm.util.invalidateDenseArrayShape import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.typedArrayBoxedLValue @@ -106,7 +107,7 @@ internal fun TsExprResolver.handleAssignToArrayIndex( }) ?: return null val bvIndex = mkFpToUint32AfterValidation(index.value, indexIsSupported).asExpr(sizeSort) - extendArrayForIndexAppend(array = array, index = bvIndex, arrayType = storageType) ?: return null + extendArrayForIndexWrite(array = array, index = bvIndex, arrayType = storageType) ?: return null return assignToArrayIndex( scope = scope, @@ -123,27 +124,42 @@ internal fun TsExprResolver.handleAssignToArrayIndex( ) } -private fun TsExprResolver.extendArrayForIndexAppend( +private fun TsExprResolver.extendArrayForIndexWrite( array: UHeapRef, index: UExpr, arrayType: EtsArrayType, ): Unit? = with(ctx) { val lengthLValue = mkArrayLengthLValue(array, arrayType) val length = scope.calcOnState { memory.read(lengthLValue) } - val isAppend = mkEq(index, length) - val belowCapacity = mkBvSignedLessExpr(length, mkBv(options.maxArraySize)) - val appendExceedsCapacity = mkAnd(isAppend, mkNot(belowCapacity)) - if (scope.checkSat(appendExceedsCapacity) != null) { + val grows = mkBvUnsignedGreaterOrEqualExpr(index, length) + val belowCapacity = mkBvUnsignedLessExpr(index, mkBv(options.maxArraySize)) + val growthExceedsCapacity = mkAnd(grows, mkNot(belowCapacity)) + val growthBeyondCapacityIsFeasible = scope.checkSat(growthExceedsCapacity) != null + if (growthBeyondCapacityIsFeasible) { reportRuntimeFeatureLimitation( reason = TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, - detail = "array index append exceeds configured length bound ${options.maxArraySize}", + detail = "array index write exceeds configured length bound ${options.maxArraySize}", ) } - scope.assert(mkNot(appendExceedsCapacity)) ?: return null + scope.assert(mkNot(growthExceedsCapacity)) ?: return null - // Dense appends have no uninitialized gap. Sparse growth remains unsupported below. + val sparseGrowth = mkBvUnsignedGreaterExpr(index, length) + val sparseGrowthIsFeasible = scope.checkSat(sparseGrowth) != null + val hasKnownOwnSlots = scope.calcOnState { array in knownArrayPropertyPresence } + if (sparseGrowthIsFeasible && !hasKnownOwnSlots) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, + detail = "sparse indexed growth requires known own-slot provenance", + ) + scope.assert(mkNot(sparseGrowth)) ?: return null + } + + // Existing presence metadata leaves gaps absent, including slots deleted by earlier shrinking. scope.doWithState { - memory.write(lengthLValue, mkBvAddExpr(length, mkBv(1)), guard = isAppend) + if (sparseGrowthIsFeasible && hasKnownOwnSlots) { + invalidateDenseArrayShape(array) + } + memory.write(lengthLValue, mkBvAddExpr(index, mkBv(1)), guard = grows) } } @@ -163,8 +179,7 @@ fun TsContext.assignToArrayIndex( memory.read(lengthLValue) } - // Callers extend the length for supported dense appends before writing the element. - // Skipping indices would create holes, which this storage model does not represent. + // Callers establish the new length and any required own-slot provenance before writing. val indexIsNonNegative = mkBvSignedGreaterOrEqualExpr(index, mkBv(0)) val indexIsBelowLength = mkBvSignedLessExpr(index, length) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt index 7fd8d8737f..9fa410d601 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt @@ -35,17 +35,21 @@ internal fun TsState.writtenArrayIndexPresence(array: UHeapRef, index: UExpr) = with(ctx) { // Deletion can create a hole without changing length or payload storage. + invalidateDenseArrayShape(array) + + val initialized = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to initialized.mapValues { (writtenIndex, present) -> + mkAnd(present, mkNot(mkEq(index, writtenIndex))) + } +} + +internal fun TsState.invalidateDenseArrayShape(array: UHeapRef) { if (array is UConcreteHeapRef) { denseInputArrays.remove(array) } else { // A symbolic receiver can alias any recorded dense array. denseInputArrays.clear() } - - val initialized = initializedArrayIndices[array].orEmpty() - initializedArrayIndices += array to initialized.mapValues { (writtenIndex, present) -> - mkAnd(present, mkNot(mkEq(index, writtenIndex))) - } } internal fun TsState.truncateKnownArrayIndices(array: UHeapRef, length: UExpr) = with(ctx) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt index 2796513877..20b659a087 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt @@ -29,7 +29,7 @@ class ArrayAppendSourceTest : TsMethodTestRunner() { @Test fun `dense appends preserve length payload kinds and aliases`() { - listOf("appendToEmpty", "appendThroughMixedAlias", "overwriteAtCapacity", "appendAfterTruncate") + listOf("appendToEmpty", "appendThroughMixedAlias", "overwriteAtCapacity", "appendAfterTruncate", "sparseGrowth") .forEach { methodName -> discoverProperties( method = getMethod(methodName = methodName, className = "ArrayAppendSource"), @@ -40,10 +40,9 @@ class ArrayAppendSourceTest : TsMethodTestRunner() { } @Test - fun `capacity and sparse growth remain explicit limitations`() { + fun `capacity remains an explicit limitation`() { val boundaries = mapOf( "appendBeyondCapacity" to TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, - "sparseGrowth" to TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, ) for ((methodName, expectedReason) in boundaries) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArraySparseGrowthSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArraySparseGrowthSourceTest.kt new file mode 100644 index 0000000000..b27a3b7bbe --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArraySparseGrowthSourceTest.kt @@ -0,0 +1,148 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class ArraySparseGrowthSourceTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/ArraySparseGrowthSource.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions(maxArraySize = 6) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + val limitations = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions, observer = observer).use { machine -> + val outcome = machine.analyzeWithMetadata(methods = listOf(method)) + + assertTrue(outcome.unsupportedPaths.isEmpty(), outcome.toString()) + assertTrue(!outcome.engineFailed && !outcome.unsupportedCall, outcome.toString()) + assertTrue(limitations.isEmpty(), limitations.toString()) + outcome.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + init { + options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL, stopOnCoverage = 0) + } + + @Test + fun `bounded indexed growth preserves gap reads kinds references and prior deletion`() { + for (name in supportedMethods) { + discoverProperties( + method = method(name), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `symbolic gap index preserves both supported values without stale slots`() { + discoverProperties( + method = method("symbolicIndex"), + { index, result -> index.number == 2.0 && result.number == 1.0 }, + { index, result -> index.number == 3.0 && result.number == 1.0 }, + invariants = arrayOf({ index, result -> + if (index.number == 2.0 || index.number == 3.0) result.number == 1.0 else result.number == 0.0 + }), + ) + } + + @Test + fun `growth capacity remains a reported limitation`() { + val reasons = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + reasons += event.reason + } + } + + TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method("beyondCapacity"))) + + assertTrue(result.states.isEmpty()) + assertEquals(listOf(TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY), reasons) + } + } + + @Test + fun `dense only operations stay explicitly outside the sparse model`() { + for (name in listOf("denseOnlyConsumer", "denseProofAfterSparseGrowth")) { + TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method(name))) + + assertTrue(result.states.isEmpty(), "$name: $result") + assertTrue(result.unsupportedCall || result.unsupportedPaths.isNotEmpty(), "$name: $result") + } + } + } + + @Test + fun `generated source witnesses agree with native TypeScript`() { + val script = buildString { + appendLine(source.readText()) + for (name in supportedMethods) { + appendLine("if (ArraySparseGrowthSource.$name() !== 1) throw Error('$name');") + } + appendLine( + "if (ArraySparseGrowthSource.denseProofAfterSparseGrowth() !== 'c,,') throw Error('dense proof');", + ) + val tests = runner(method("symbolicIndex"), options) + assertTrue(tests.isNotEmpty()) + for (test in tests) { + val index = assertIs(test.before.parameters.single()).number + val expected = assertIs(test.returnValue).number + appendLine("if (ArraySparseGrowthSource.symbolicIndex($index) !== $expected) throw Error('$index');") + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "array-sparse-growth", + timeoutMessage = "Sparse indexed growth replay timed out", + ) + } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "ArraySparseGrowthSource") + + private val supportedMethods = listOf( + "numbers", + "booleans", + "references", + "widenedAlias", + "unresolvedValues", + "shrinkThenRegrow", + "movesAndPops", + "fillGaps", + ) +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt index 5c62ac3524..bb1c53eeb3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt @@ -112,11 +112,10 @@ class NumericBoundarySemanticsTest : TsMethodTestRunner() { } @Test - fun `unsupported named property and growth writes stop their paths`() { + fun `unsupported named property writes stop their paths`() { val unsupportedMethods = mapOf( "fractionalArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, "negativeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, - "outOfRangeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, "chainedMissingArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, ) @@ -134,6 +133,17 @@ class NumericBoundarySemanticsTest : TsMethodTestRunner() { ) } + @Test + fun `bounded indexed growth preserves existing array elements`() { + val observer = RecordingObserver() + + val states = analyze("outOfRangeArrayWrite", observer) + + assertEquals(expected = 1, actual = states.size) + assertTrue(observer.limitations.isEmpty()) + discoverNumber("outOfRangeArrayWrite", expected = 22.0) + } + @Test fun `chained array indexes preserve numeric and undefined branches`() { discoverNumber("chainedArrayRead", expected = 22.0) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt index 4fc9bbacfa..068946005d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt @@ -6,13 +6,12 @@ import org.junit.jupiter.api.io.TempDir import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.api.TsTestValue -import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions -import org.usvm.machine.TsRuntimeFeatureLimitationEvent -import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.test.util.checkers.eq as exactly import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.TsUnsupportedWitnessException import org.usvm.util.assertNodeReplay import org.usvm.util.eq import org.usvm.util.getResourcePath @@ -20,6 +19,8 @@ import org.usvm.util.neq import java.nio.file.Path import kotlin.io.path.readText import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse import kotlin.test.assertTrue class AllocatedArrays : TsMethodTestRunner() { @@ -115,7 +116,26 @@ class AllocatedArrays : TsMethodTestRunner() { @Test fun `test allocatedArrayLengthExpansion`() { - assertArrayIndexGrowthLimitation("allocatedArrayLengthExpansion") + val target = getMethod(methodName = "allocatedArrayLengthExpansion") + val result = TsMachine( + scene = scene, + options = UMachineOptions(solverType = SolverType.YICES), + tsOptions = TsOptions(), + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(target)) } + + assertEquals(expected = 1, actual = result.states.size) + assertFalse(result.runtimeLimited) + assertFalse(result.engineFailed) + val witnessFailure = assertFailsWith { + TsTestResolver().resolve(target, result.states.single()) + } + assertTrue(witnessFailure.message.orEmpty().contains("Sparse array slot 3")) + + discoverProperties( + method = getMethod(methodName = "inspectAllocatedArrayLengthExpansion"), + { value -> value.number == 5.0 }, + invariants = arrayOf({ value -> value.number == 5.0 }), + ) } @Test @@ -150,29 +170,26 @@ class AllocatedArrays : TsMethodTestRunner() { ) } - private fun assertArrayIndexGrowthLimitation(methodName: String) { - val observer = RecordingObserver() - val states = TsMachine( - scene = scene, - options = UMachineOptions(solverType = SolverType.YICES), - tsOptions = TsOptions(), - observer = observer, - ).use { machine -> - machine.analyze(listOf(getMethod(methodName))) - } + @Test + fun `sparse allocated growth preserves values length and holes in native JavaScript`() { + val script = getResourcePath(tsPath).readText() + "\n" + + getResourcePath("/models/NumericBoundarySemantics.ts").readText() + """ + + const subject = new AllocatedArrays(); + const values = subject.allocatedArrayLengthExpansion(); + if (!Array.isArray(values) || values.length !== 6) throw new Error('Sparse length'); + if (values[0] !== 1 || values[1] !== 2 || values[2] !== 3 || values[5] !== 5) throw new Error('Sparse values'); + if (3 in values || 4 in values) throw new Error('Sparse holes became own elements'); + if (values[3] !== undefined || values[4] !== undefined) throw new Error('Sparse hole read'); + if (subject.inspectAllocatedArrayLengthExpansion() !== 5) throw new Error('Sparse observation'); + if (new NumericBoundarySemantics().outOfRangeArrayWrite() !== 22) throw new Error('Existing element changed'); + """.trimIndent() - assertTrue(states.isEmpty()) - assertEquals( - TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, - observer.limitations.single().reason, + assertNodeReplay( + source = script, + directory = directory, + name = "allocated-array-sparse-growth", + timeoutMessage = "Allocated sparse growth native replay timed out", ) } - - private class RecordingObserver : TsInterpreterObserver { - val limitations = mutableListOf() - - override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { - limitations += event - } - } } diff --git a/usvm-ts/src/test/resources/models/ArrayAppendSource.ts b/usvm-ts/src/test/resources/models/ArrayAppendSource.ts index 070dba9dca..6efff0b1f0 100644 --- a/usvm-ts/src/test/resources/models/ArrayAppendSource.ts +++ b/usvm-ts/src/test/resources/models/ArrayAppendSource.ts @@ -36,6 +36,6 @@ export class ArrayAppendSource { static sparseGrowth(): number { const values = [1]; values[2] = 7; - return values.length; + return values.length === 3 && values[0] === 1 && values[1] === undefined && values[2] === 7 ? 1 : 0; } } diff --git a/usvm-ts/src/test/resources/models/ArraySparseGrowthSource.ts b/usvm-ts/src/test/resources/models/ArraySparseGrowthSource.ts new file mode 100644 index 0000000000..fed1a1bd71 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArraySparseGrowthSource.ts @@ -0,0 +1,92 @@ +export class ArraySparseGrowthSource { + static numbers(): number { + const values: number[] = []; + values[2] = 7; + return values.length === 3 && values[0] === undefined && values[1] === undefined && values[2] === 7 ? 1 : 0; + } + + static booleans(): number { + const values: boolean[] = []; + values[2] = false; + return values.length === 3 && values[0] === undefined && values[1] === undefined && values[2] === false ? 1 : 0; + } + + static references(): number { + const cache: number[][] = []; + const item = [7, 11]; + cache[2] = item; + return cache.length === 3 && cache[0] === undefined && cache[1] === undefined && cache[2] === item ? 1 : 0; + } + + static widenedAlias(): number { + const values: number[] = []; + const alias: any[] = values; + alias[2] = true; + return values.length === 3 && values[0] === undefined && alias[1] === undefined && alias[2] === true ? 1 : 0; + } + + static unresolvedValues(): number { + const values: unknown[] = []; + values[2] = undefined; + values[3] = true; + return values.length === 4 && values[0] === undefined && values[1] === undefined && + values[2] === undefined && values[3] === true ? 1 : 0; + } + + static shrinkThenRegrow(): number { + const values = [10, 20, 30, 40]; + values.length = 1; + values[3] = 7; + return values.length === 4 && values[0] === 10 && values[1] === undefined && + values[2] === undefined && values[3] === 7 ? 1 : 0; + } + + static movesAndPops(): number { + const values: number[] = []; + values[2] = 7; + if (values.pop() !== 7 || values.pop() !== undefined) return 0; + values.push(11); + values.reverse(); + values.unshift(13); + if (values.shift() !== 13) return 0; + const copy = [...values]; + return copy.length === 2 && copy[0] === 11 && copy[1] === undefined ? 1 : 0; + } + + static fillGaps(): number { + const values: number[] = []; + values[2] = 7; + values.fill(9); + return values[0] === 9 && values[1] === 9 && values[2] === 9 ? 1 : 0; + } + + static symbolicIndex(index: number): number { + if (index !== 2 && index !== 3) return 0; + const values = [7]; + values[index] = 11; + return values.length === index + 1 && values[0] === 7 && values[1] === undefined && + values[index] === 11 ? 1 : 2; + } + + static beyondCapacity(): number { + const values: number[] = []; + values[6] = 7; + return values.length; + } + + static denseOnlyConsumer(): number { + const values: number[] = []; + values[2] = 7; + return values.map(value => value + 1).length; + } + + static denseProofAfterSparseGrowth(): string { + const values = "a,b,c".split(","); + values.reverse(); + const alias: any[] = values; + alias.length = 1; + alias[4] = "x"; + alias.length = 3; + return values.join(","); + } +} diff --git a/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts index 1e683c710a..e63d058d73 100644 --- a/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts @@ -58,6 +58,15 @@ class AllocatedArrays { } } + inspectAllocatedArrayLengthExpansion() { + const values = this.allocatedArrayLengthExpansion(); + if (typeof values === 'number') return -1; + if (values.length !== 6) return -2; + if (values[0] !== 1 || values[1] !== 2 || values[2] !== 3) return -3; + if (values[3] !== undefined || values[4] !== undefined) return -4; + return values[5]; + } + writeInTheIndexEqualToLength() { let x = [1, 2, 3]; x[3] = 4;