diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index f3a60eb63f..1f416b14de 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -84,6 +84,12 @@ 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. | +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 memory representation and supported input domain. 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/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/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/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 281f854e80..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,10 @@ 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 import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver import org.usvm.util.assertNodeReplay @@ -36,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 -> @@ -48,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) } } } @@ -72,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( @@ -120,13 +162,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 +181,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) } } } @@ -146,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) { @@ -170,6 +223,7 @@ class SparseArrayIteratorSourceTest : TsMethodTestRunner() { private val supportedMethods = listOf( "literalHoles", "newArrayHoles", "deletedSlot", "rewriteDeletedSlot", "movesPreserveHoles", "shiftMissingFirstSlot", "truncateAndMoveHoles", "destructureHoles", "forOfHoles", "liveDelete", - "sourceObjectLookalike", + "sourceObjectLookalike", "reverseAsymmetricHoles", "unshiftHoles", "fillAllHoles", + "unshiftSeveralHoles", "unshiftNoItems", "reverseBoxedValues", ) } 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..cb228cb672 100644 --- a/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts +++ b/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts @@ -1,4 +1,54 @@ 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(); + 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 +225,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; } }