From 718ff55ca40c4eeaeed45f4cdef2afd6b0568b6c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 00:04:50 +0300 Subject: [PATCH 1/2] Preserve known sparse array mutations before dense model dispatch --- usvm-ts/UNKNOWN_CALL_MODELS.md | 5 ++++ .../call/TsUnknownCallModelDispatcher.kt | 2 ++ .../usvm/machine/expr/CallApproximations.kt | 29 +++++++++++++++++++ .../call/TsArrayMutationEtsIrModelTest.kt | 4 +-- .../expr/SparseArrayIteratorSourceTest.kt | 22 +++++++++++--- .../resources/models/ArrayMutationEtsIr.ts | 4 +-- .../models/SparseArrayIteratorSource.ts | 25 +++++++++++++++- 7 files changed, 82 insertions(+), 9 deletions(-) diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index f3a60eb63f..217dfd96d0 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -84,6 +84,11 @@ The built-in catalog includes the following public APIs and their internal stora | `ts.error.constructor`, `ts.typeError.constructor` | TypeScript/EtsIR bodies | Genuine `new Error(message)` / `new TypeError(message)` with one string argument; initializes `name` and `message`. Other arities, coercions, subclasses, `cause` and stack inspection are outside these models. | | `ts.date.*` (38 IDs) | TypeScript/EtsIR bodies | Numeric Date construction, `UTC`, fixed-clock `now`, getters, setters, `valueOf`, and source `toISOString`; see the Date boundary below. | +When their models are enabled, arrays with known own-slot presence use the existing +zero-argument `reverse` and one-argument `unshift` +storage operations before model dispatch. These operations preserve holes and boxed overrides without requiring +a dense-input proof. Arrays without either a slot-presence proof or a current dense-input proof still use fallback. + Matching standard calls are assumed to refer to genuine builtins. Monkey patching and prototype replacement are outside this experiment; no runtime provenance protocol is imposed. Receiver and argument checks establish the memory representation and supported input domain. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 5ab9ad9772..7f862e0440 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -33,6 +33,8 @@ class TsModelUnknownCallDispatcher( private val fallback: TsResidualCallPolicy, private val observer: TsInterpreterObserver? = null, ) : TsUnknownCallModelDispatcher { + internal fun hasModel(modelId: String): Boolean = modelId in models.modelIds + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { val application = scope.calcOnState { this@TsModelUnknownCallDispatcher.models.apply(this, call) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 120776dd90..760a310879 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -25,6 +25,7 @@ import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.call.TsBuiltInUnknownCallModels +import org.usvm.machine.call.TsModelUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModelDispatcher import org.usvm.machine.call.dispatch @@ -132,6 +133,31 @@ private fun TsExprResolver.tryDispatchNumericBuiltin( return TsExprApproximationResult.ResolveFailure } +private fun TsExprResolver.tryApproximateKnownSlotMutation( + stmt: TsVirtualMethodCallStmt, + arrayType: EtsArrayType, + array: UHeapRef, +): TsExprApproximationResult { + val expr = stmt.call + val dispatcher = unknownCallDispatcher as? TsModelUnknownCallDispatcher + val modelEnabled = dispatcher?.hasModel(modelId = "ts.array.${expr.callee.name}") == true + if (!modelEnabled) return TsExprApproximationResult.NoApproximation + + val hasKnownSlots = scope.calcOnState { array in knownArrayPropertyPresence } + val preservesKnownSlots = hasKnownSlots && when (expr.callee.name) { + "reverse" -> expr.args.isEmpty() + "unshift" -> expr.args.size == 1 + else -> false + } + if (!preservesKnownSlots) return TsExprApproximationResult.NoApproximation + + // These storage operations preserve known holes; the dense source models cannot handle them. + return when (expr.callee.name) { + "reverse" -> from(handleArrayReverse(expr, arrayType, array)) + else -> from(handleArrayUnshift(expr, arrayType, array)) + } +} + internal fun TsExprResolver.tryApproximateInstanceCall( stmt: TsVirtualMethodCallStmt, ): TsExprApproximationResult = with(ctx) { @@ -175,6 +201,9 @@ internal fun TsExprResolver.tryApproximateInstanceCall( .takeIf { it !is TsUnresolvedSort } ?: addressSort + val knownSlotMutation = tryApproximateKnownSlotMutation(stmt, instanceType, array) + if (knownSlotMutation !is TsExprApproximationResult.NoApproximation) return knownSlotMutation + val usesModelDispatcher = unknownCallDispatcher is TsUnknownCallModelDispatcher val modeledArrayCall = usesModelDispatcher && TsBuiltInUnknownCallModels.hasPartialApproximationModel( methodName = expr.callee.name, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayMutationEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayMutationEtsIrModelTest.kt index 74b074a523..57ca99dc99 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayMutationEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayMutationEtsIrModelTest.kt @@ -122,8 +122,8 @@ class TsArrayMutationEtsIrModelTest { } @Test - fun `sparse reverse remains residual`() { - val result = analyze(methodName = "sparseReverseUsesResidual") + fun `reverse without a slot presence or dense input proof remains residual`() { + val result = analyze(methodName = "unprovenReverseUsesResidual") assertTrue(result.values.isEmpty()) assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt index 281f854e80..f19c6e4cd3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt @@ -16,6 +16,9 @@ import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallOutcome import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver import org.usvm.util.assertNodeReplay @@ -120,13 +123,18 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { } @Test - fun `unknown array storage retains explicit iterator limitations`() { - for (name in listOf("unknownCopiedStorage", "unsupportedFillStorage")) { + fun `unproven copy and fill storage stop at the source model boundary`() { + for (name in listOf("unknownCopiedStorage", "unprovenPartialFillStorage")) { val limitations = mutableListOf() + val unknownCalls = mutableListOf() val observer = object : TsInterpreterObserver { override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { limitations += event.reason } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + unknownCalls += event + } } TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> @@ -134,7 +142,13 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, name) assertTrue(outcome.states.isEmpty(), name) - assertEquals(listOf(TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED), limitations, name) + assertTrue(limitations.isEmpty(), "$name: $limitations") + val event = unknownCalls.single() + val expectedMethod = if (name == "unknownCopiedStorage") "slice" else "fill" + + assertEquals(expectedMethod, event.callee.name, name) + assertEquals(TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, event.failureReason, name) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, event.outcome, name) } } } @@ -170,6 +184,6 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { private val supportedMethods = listOf( "literalHoles", "newArrayHoles", "deletedSlot", "rewriteDeletedSlot", "movesPreserveHoles", "shiftMissingFirstSlot", "truncateAndMoveHoles", "destructureHoles", "forOfHoles", "liveDelete", - "sourceObjectLookalike", + "sourceObjectLookalike", "reverseAsymmetricHoles", "unshiftHoles", "fillAllHoles", ) } diff --git a/usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts index b8167be051..c6fba0783d 100644 --- a/usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts @@ -77,7 +77,7 @@ export class ArrayMutationEtsIr { + result[3]; } - sparseReverseUsesResidual(): number[] { - return new Array(2).reverse(); + unprovenReverseUsesResidual(values: number[]): number[] { + return values.reverse(); } } diff --git a/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts b/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts index f9d5920b37..96ed7e78c0 100644 --- a/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts +++ b/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts @@ -1,4 +1,20 @@ export class SparseArrayIteratorSource { + static reverseAsymmetricHoles(): number { + const values = [, 7, 11]; + const alias = values.reverse(); + const copy = [...values]; + return alias === values && copy.length === 3 && copy[0] === 11 && + copy[1] === 7 && copy[2] === undefined ? 1 : 0; + } + + static unshiftHoles(): number { + const values = [, 11]; + const length = values.unshift(7); + const copy = [...values]; + return length === 3 && copy.length === 3 && copy[0] === 7 && + copy[1] === undefined && copy[2] === 11 ? 1 : 0; + } + static literalHoles(): number { const values = [7, , 11]; const copy = [...values]; @@ -175,9 +191,16 @@ export class SparseArrayIteratorSource { return [...values].length; } - static unsupportedFillStorage(): number { + static fillAllHoles(): number { const values = new Array(2); values.fill(7); + const copy = [...values]; + return copy.length === 2 && copy[0] === 7 && copy[1] === 7 ? 1 : 0; + } + + static unprovenPartialFillStorage(): number { + const values = new Array(2); + values.fill(7, 0, 1); return [...values].length; } } From ff9d35406c36ce662ec3a36b4740cbdd7a75d150 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 00:36:19 +0300 Subject: [PATCH 2/2] Handle sparse array mutations within source models --- usvm-ts/UNKNOWN_CALL_MODELS.md | 9 +- .../call/TsUnknownCallModelDispatcher.kt | 2 - .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 32 +++---- .../call/intrinsic/TsArraySlotPrimitives.kt | 90 +++++++++++++++++++ .../usvm/machine/expr/CallApproximations.kt | 29 ------ .../usvm/machine/call/models/ArrayModels.ts | 22 ++++- .../call/TsUnknownCallModelCatalogTest.kt | 2 + .../expr/SparseArrayIteratorSourceTest.kt | 42 ++++++++- .../models/SparseArrayIteratorSource.ts | 34 +++++++ 9 files changed, 206 insertions(+), 56 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArraySlotPrimitives.kt diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 217dfd96d0..1f416b14de 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -84,10 +84,11 @@ The built-in catalog includes the following public APIs and their internal stora | `ts.error.constructor`, `ts.typeError.constructor` | TypeScript/EtsIR bodies | Genuine `new Error(message)` / `new TypeError(message)` with one string argument; initializes `name` and `message`. Other arities, coercions, subclasses, `cause` and stack inspection are outside these models. | | `ts.date.*` (38 IDs) | TypeScript/EtsIR bodies | Numeric Date construction, `UTC`, fixed-clock `now`, getters, setters, `valueOf`, and source `toISOString`; see the Date boundary below. | -When their models are enabled, arrays with known own-slot presence use the existing -zero-argument `reverse` and one-argument `unshift` -storage operations before model dispatch. These operations preserve holes and boxed overrides without requiring -a dense-input proof. Arrays without either a slot-presence proof or a current dense-input proof still use fallback. +The `reverse` and `unshift` source models accept known own-slot presence as well as a current dense-array proof. +Their TypeScript bodies distinguish missing slots from present values, including `undefined`, and use ordinary +indexed writes and deletes to preserve holes and boxed overrides. Two model-owned primitives prepare trusted +own-slot metadata and read slot presence. Model selection, application events, and residual fallback all use the +normal dispatcher; receivers without either proof remain residual. These models retain the length/result bound of 16. Matching standard calls are assumed to refer to genuine builtins. Monkey patching and prototype replacement are outside this experiment; no runtime provenance protocol is imposed. Receiver and argument checks establish the diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 7f862e0440..5ab9ad9772 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -33,8 +33,6 @@ class TsModelUnknownCallDispatcher( private val fallback: TsResidualCallPolicy, private val observer: TsInterpreterObserver? = null, ) : TsUnknownCallModelDispatcher { - internal fun hasModel(modelId: String): Boolean = modelId in models.modelIds - override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { val application = scope.calcOnState { this@TsModelUnknownCallDispatcher.models.apply(this, call) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index c0a78a0967..b2dab02fd5 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -150,20 +150,6 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { state.boundedArrayGuard(array, arrayType, maximumLength = MAX_SOURCE_ARRAY_LENGTH) } - private val unshiftDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> - val (array, arrayType) = state.concreteArray(call, inputs) - ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr - val arguments = call.arguments.map { argument -> - argument.resolved ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr - } - val isDenseInput = state.isUnmodifiedDenseInputArray(array, arrayType) - if (!isDenseInput) { - return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr - } - - state.boundedArrayGuard(array, arrayType, maximumLength = MAX_SOURCE_ARRAY_LENGTH - arguments.size) - } - private val concatDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr @@ -378,13 +364,13 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { id = "ts.array.reverse", methodName = "reverse", inputAdapter = noArgumentsAdapter, - domainGuard = denseReceiverDomain, + domainGuard = TsArraySlotPrimitives.reverseDomain, ), sourceModel( id = "ts.array.unshift", methodName = "unshift", inputAdapter = variadicMutationAdapter, - domainGuard = unshiftDomain, + domainGuard = TsArraySlotPrimitives.unshiftDomain, ), sourceModel( id = "ts.array.slice", @@ -407,6 +393,16 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { arity = 1, implementation = TsDenseArrayPrimitives::requireDense, ), + primitiveModel( + methodName = "prepareOwnSlots", + arity = 1, + implementation = TsArraySlotPrimitives::prepareOwnSlots, + ), + primitiveModel( + methodName = "hasOwnSlot", + arity = 2, + implementation = TsArraySlotPrimitives::hasOwnSlot, + ), primitiveModel( methodName = "grow", arity = 2, @@ -444,6 +440,10 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { domainGuard = domainGuard, inputAdapter = inputAdapter, requiredModelIds = buildSet { + if (methodName in setOf("reverse", "unshift")) { + add("ts.array.primitive.prepareOwnSlots") + add("ts.array.primitive.hasOwnSlot") + } if (methodName == "join") { add("ts.array.primitive.elementString") add(TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArraySlotPrimitives.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArraySlotPrimitives.kt new file mode 100644 index 0000000000..f3568052cc --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArraySlotPrimitives.kt @@ -0,0 +1,90 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.expr.mkFpToUint32AfterValidation +import org.usvm.machine.expr.mkValidArrayIndexProperty +import org.usvm.machine.state.TsState +import org.usvm.sizeSort +import org.usvm.util.arrayStorageType +import org.usvm.util.hasDenseArrayShape +import org.usvm.util.knownArrayIndexPresence +import org.usvm.util.markDenseArrayOwnSlots +import org.usvm.util.mkArrayLengthLValue + +/** Own-slot metadata operations used by the source reverse and unshift algorithms. */ +internal object TsArraySlotPrimitives { + val reverseDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + knownSlotGuard(state, call, inputs, additionalSlots = 0) + } + + val unshiftDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + knownSlotGuard(state, call, inputs, additionalSlots = call.arguments.size) + } + + private fun knownSlotGuard( + state: TsState, + call: TsUnknownCall, + inputs: List>, + additionalSlots: Int, + ): UBoolExpr { + val (array, type) = state.concreteArray(call, inputs) ?: return state.ctx.falseExpr + val hasSlotProof = array in state.knownArrayPropertyPresence || state.hasDenseArrayShape(array, type) + if (!hasSlotProof) return state.ctx.falseExpr + + return state.boundedArrayGuard(array, type, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY - additionalSlots) + } + + fun prepareOwnSlots(state: TsState, inputs: List>): TsUnknownCallModelExecution? { + val array = inputs.single() as? UConcreteHeapRef ?: return null + val type = state.arrayStorageType(array, EtsArrayType(EtsUnknownType, dimensions = 1)) as? EtsArrayType + ?: return null + val hasKnownSlots = array in state.knownArrayPropertyPresence + val hasSlotProof = hasKnownSlots || state.hasDenseArrayShape(array, type) + if (!hasSlotProof) return null + + val guard = state.boundedArrayGuard(array, type, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY) + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.Normal { + if (!hasKnownSlots) { + val length = memory.read(mkArrayLengthLValue(array, type)) + markDenseArrayOwnSlots(array = array, length = length, capacity = SOURCE_ARRAY_MODEL_CAPACITY) + } + + ctx.mkUndefinedValue() + }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.mkNot(guard), + ) + } + + fun hasOwnSlot(state: TsState, inputs: List>): TsUnknownCallModelExecution? = with(state.ctx) { + val array = inputs[0] as? UConcreteHeapRef ?: return null + val number = inputs[1].takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val guard = mkValidArrayIndexProperty(number) + val index = mkFpToUint32AfterValidation(number, guard).asExpr(sizeSort) + val present = state.knownArrayIndexPresence(array, index) ?: return null + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.Normal { present }, + ) + + TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = mkNot(guard), + ) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 760a310879..120776dd90 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -25,7 +25,6 @@ import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.call.TsBuiltInUnknownCallModels -import org.usvm.machine.call.TsModelUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModelDispatcher import org.usvm.machine.call.dispatch @@ -133,31 +132,6 @@ private fun TsExprResolver.tryDispatchNumericBuiltin( return TsExprApproximationResult.ResolveFailure } -private fun TsExprResolver.tryApproximateKnownSlotMutation( - stmt: TsVirtualMethodCallStmt, - arrayType: EtsArrayType, - array: UHeapRef, -): TsExprApproximationResult { - val expr = stmt.call - val dispatcher = unknownCallDispatcher as? TsModelUnknownCallDispatcher - val modelEnabled = dispatcher?.hasModel(modelId = "ts.array.${expr.callee.name}") == true - if (!modelEnabled) return TsExprApproximationResult.NoApproximation - - val hasKnownSlots = scope.calcOnState { array in knownArrayPropertyPresence } - val preservesKnownSlots = hasKnownSlots && when (expr.callee.name) { - "reverse" -> expr.args.isEmpty() - "unshift" -> expr.args.size == 1 - else -> false - } - if (!preservesKnownSlots) return TsExprApproximationResult.NoApproximation - - // These storage operations preserve known holes; the dense source models cannot handle them. - return when (expr.callee.name) { - "reverse" -> from(handleArrayReverse(expr, arrayType, array)) - else -> from(handleArrayUnshift(expr, arrayType, array)) - } -} - internal fun TsExprResolver.tryApproximateInstanceCall( stmt: TsVirtualMethodCallStmt, ): TsExprApproximationResult = with(ctx) { @@ -201,9 +175,6 @@ internal fun TsExprResolver.tryApproximateInstanceCall( .takeIf { it !is TsUnresolvedSort } ?: addressSort - val knownSlotMutation = tryApproximateKnownSlotMutation(stmt, instanceType, array) - if (knownSlotMutation !is TsExprApproximationResult.NoApproximation) return knownSlotMutation - val usesModelDispatcher = unknownCallDispatcher is TsUnknownCallModelDispatcher val modeledArrayCall = usesModelDispatcher && TsBuiltInUnknownCallModels.hasPartialApproximationModel( methodName = expr.callee.name, diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts index 7d9b30a349..ca36a2ce26 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts @@ -4,6 +4,8 @@ declare class ArrayModelPrimitives { static allocateLike(receiver: any[], length: number): any[]; static elementString(value: any): string; static requireDense(receiver: any[]): void; + static prepareOwnSlots(receiver: any[]): void; + static hasOwnSlot(receiver: any[], index: number): boolean; } export class ArrayModels { @@ -189,26 +191,38 @@ export class ArrayModels { } static reverse(receiver: any[]): any[] { + ArrayModelPrimitives.prepareOwnSlots(receiver); const length = receiver.length; let lower = 0; while (lower < Math.floor(length / 2)) { const upper = length - lower - 1; - const value = receiver[lower]; - receiver[lower] = receiver[upper]; - receiver[upper] = value; + const lowerPresent = ArrayModelPrimitives.hasOwnSlot(receiver, lower); + const upperPresent = ArrayModelPrimitives.hasOwnSlot(receiver, upper); + const lowerValue = receiver[lower]; + const upperValue = receiver[upper]; + + if (upperPresent) receiver[lower] = upperValue; + else delete receiver[lower]; + + if (lowerPresent) receiver[upper] = lowerValue; + else delete receiver[upper]; + lower++; } return receiver; } static unshift(receiver: any[], first: any, second: any, third: any, count: number): number { + ArrayModelPrimitives.prepareOwnSlots(receiver); const length = receiver.length; const resultLength = length + count; ArrayModelPrimitives.grow(receiver, resultLength); let index = length; while (index > 0) { index--; - receiver[index + count] = receiver[index]; + const present = ArrayModelPrimitives.hasOwnSlot(receiver, index); + if (present) receiver[index + count] = receiver[index]; + else delete receiver[index + count]; } if (count >= 1) receiver[0] = first; if (count >= 2) receiver[1] = second; diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 377b8647e9..a0896e7fc3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -193,6 +193,8 @@ class TsUnknownCallModelCatalogTest { "ts.array.primitive.allocateStrings", "ts.array.primitive.elementString", "ts.array.primitive.grow", + "ts.array.primitive.hasOwnSlot", + "ts.array.primitive.prepareOwnSlots", "ts.array.primitive.requireDense", "ts.array.primitive.truncateDense", "ts.array.push", diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt index f19c6e4cd3..058e6c9985 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt @@ -16,6 +16,7 @@ import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.call.TsUnknownCallDecision import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallOutcome @@ -39,10 +40,16 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { override val tsOptions = TsOptions(maxArraySize = 6) override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> val limitations = mutableListOf() + val modelIds = mutableListOf() val observer = object : TsInterpreterObserver { override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { limitations += event } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + val model = event.decision as? TsUnknownCallDecision.ModelApplied + if (model != null) modelIds += model.modelId + } } TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions, observer = observer).use { machine -> @@ -51,6 +58,20 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, method.name) assertTrue(outcome.unsupportedPaths.isEmpty(), "${method.name}: ${outcome.unsupportedPaths}") assertTrue(limitations.isEmpty(), "${method.name}: $limitations") + val expectedModels = when (method.name) { + "movesPreserveHoles", "truncateAndMoveHoles" -> setOf("ts.array.reverse", "ts.array.unshift") + "reverseAsymmetricHoles", "reverseBoxedValues", "symbolicDeleteThenReverse" -> { + setOf("ts.array.reverse") + } + + "unshiftHoles", "unshiftSeveralHoles", "unshiftNoItems" -> setOf("ts.array.unshift") + else -> emptySet() + } + assertTrue(modelIds.containsAll(expectedModels), "${method.name}: $modelIds") + if (expectedModels.isNotEmpty()) { + assertTrue("ts.array.primitive.prepareOwnSlots" in modelIds, "${method.name}: $modelIds") + assertTrue("ts.array.primitive.hasOwnSlot" in modelIds, "${method.name}: $modelIds") + } outcome.states.map { state -> TsTestResolver().resolve(method, state) } } } @@ -75,6 +96,24 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { } } + @Test + fun `conditional holes reverse through the source model`() { + discoverProperties( + method = method("symbolicDeleteThenReverse"), + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 2.0 }, + invariants = arrayOf({ index, result -> + val expected = when (index.number) { + 0.0 -> 1.0 + 1.0 -> 2.0 + else -> 0.0 + } + result.number == expected + }), + ) + } + @Test fun `symbolic deletion preserves conditional slot presence`() { discoverProperties( @@ -160,7 +199,7 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { for (name in supportedMethods) { appendLine("if (SparseArrayIteratorSource.$name() !== 1) throw Error('$name');") } - for (name in listOf("symbolicDelete", "symbolicWriteThenDelete")) { + for (name in listOf("symbolicDelete", "symbolicWriteThenDelete", "symbolicDeleteThenReverse")) { val tests = runner(method(name), options) assertTrue(tests.isNotEmpty(), name) for (test in tests) { @@ -185,5 +224,6 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { "literalHoles", "newArrayHoles", "deletedSlot", "rewriteDeletedSlot", "movesPreserveHoles", "shiftMissingFirstSlot", "truncateAndMoveHoles", "destructureHoles", "forOfHoles", "liveDelete", "sourceObjectLookalike", "reverseAsymmetricHoles", "unshiftHoles", "fillAllHoles", + "unshiftSeveralHoles", "unshiftNoItems", "reverseBoxedValues", ) } diff --git a/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts b/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts index 96ed7e78c0..cb228cb672 100644 --- a/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts +++ b/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts @@ -1,4 +1,38 @@ export class SparseArrayIteratorSource { + static unshiftSeveralHoles(): number { + const values = [, 11]; + const length = values.unshift(7, 8, 9); + const copy = [...values]; + return length === 5 && copy.length === 5 && copy[0] === 7 && copy[1] === 8 && + copy[2] === 9 && copy[3] === undefined && copy[4] === 11 ? 1 : 0; + } + + static unshiftNoItems(): number { + const values = [, 11]; + const length = values.unshift(); + const copy = [...values]; + return length === 2 && copy.length === 2 && copy[0] === undefined && copy[1] === 11 ? 1 : 0; + } + + static reverseBoxedValues(): number { + const values = [7, , 11]; + const alias: any[] = values; + alias[0] = true; + values.reverse(); + const copy = [...values]; + return copy.length === 3 && copy[0] === 11 && copy[1] === undefined && copy[2] === true ? 1 : 0; + } + + static symbolicDeleteThenReverse(index: number): number { + if (index !== 0 && index !== 1) return 0; + const values = [7, 11]; + delete values[index]; + values.reverse(); + const copy = [...values]; + if (index === 0) return copy[0] === 11 && copy[1] === undefined ? 1 : 3; + return copy[0] === undefined && copy[1] === 7 ? 2 : 3; + } + static reverseAsymmetricHoles(): number { const values = [, 7, 11]; const alias = values.reverse();