diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index ee4c4de708..668bbd0388 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -60,12 +60,34 @@ Built-ins are `object` implementations of the sealed `TsBuiltInUnknownCallModel` `org.usvm.machine.call.intrinsic` package. Kotlin's sealed-subclass metadata discovers them automatically; adding a model requires no manual registry entry. Discovery and the default catalog are computed once. -The built-in catalog currently contains: +The built-in catalog includes the following public APIs and their internal storage primitives. Enumerate +`TsBuiltInUnknownCallModels.catalog().modelIds` for the exact IDs in a build. | ID | Implementation | Accepted calls | | --- | --- | --- | | `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array. | +| `ts.array.isArray` | Kotlin runtime-type primitive | The genuine global Array predicate, including null, undefined and fake-value wrappers. | | `ts.array.pop` | TypeScript/EtsIR body | Zero-argument `pop` on a definitely one-dimensional array that also satisfies the symbolic runtime type guard. | +| `ts.array.includes`, `ts.array.indexOf`, `ts.array.lastIndexOf` | TypeScript/EtsIR bodies | One-dimensional arrays and numeric positions, with the missing-slot exclusions below. | +| `ts.array.push`, `ts.array.fill`, `ts.array.reverse`, `ts.array.unshift`, `ts.array.slice`, `ts.array.concat` | TypeScript/EtsIR bodies with storage growth/allocation primitives | One-dimensional arrays with length/result at most 16. Push/unshift accept up to three arguments; resolved-sort arrays require matching element sorts, while mixed arrays retain runtime value kinds. Concat accepts one same-type array. Except push, these operations require a current dense-array proof. | +| `ts.string.charAt`, `ts.string.charCodeAt`, `ts.string.includes`, `ts.string.indexOf`, `ts.string.lastIndexOf`, `ts.string.startsWith`, `ts.string.endsWith` | TypeScript/EtsIR bodies | Strings in initialized UTF-16 storage, including symbolic code units and numeric positions. | +| `ts.string.slice`, `ts.string.substring`, `ts.string.trim`, `ts.string.trimStart`, `ts.string.trimEnd` | TypeScript/EtsIR bodies | UTF-16 range copying; substring clamps/swaps bounds, and trim uses the ECMAScript whitespace set. | +| `ts.string.toLowerCase`, `ts.string.toUpperCase` | TypeScript/EtsIR bodies | ASCII strings of at most 16 code units; other strings use residual fallback. | +| `ts.math.abs`, `ts.math.ceil`, `ts.math.floor`, `ts.math.max`, `ts.math.min`, `ts.math.round`, `ts.math.sqrt`, `ts.math.trunc` | Kotlin FP primitives | Numeric arguments; dynamic coercions use fallback. | +| `ts.number.isFinite`, `ts.number.isInteger`, `ts.number.isNaN`, `ts.number.isSafeInteger` | Kotlin FP/type primitives | Non-coercing Number predicates, including runtime-kind guards. | +| `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. | + +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. + +The September 2026 corpus census contains 22,769 call/constructor sites. Its 49-API shortlist accounts for 1,026 +sites: Number/Math (275), new Array/String searches (130), existing pop/shift (52), and Date (569). Every shortlisted +API name has a catalog entry. Eleven adjacent APIs add 280 census sites; `setUTCMinutes` and `setUTCMilliseconds` +complete the numeric UTC setter family but have no sites in this census. These 1,306 associated sites are +an inventory count, **not executed or replay-confirmed coverage**: imports, input representation, fallback domains, +and other unsupported operations can still prevent execution. The wider research inventory contains 271 +unambiguous standard/host API names over 7,720 sites; most are not implemented by this catalog. The common instance-call pipeline splits fake-value wrappers and conditional references under their runtime-kind and branch guards before selecting an approximation or resolving a method. A wrapped array can therefore use the @@ -73,6 +95,21 @@ model, including through an `any` alias. An unknown or non-array receiver does n the method is named `shift`. A definitely-array receiver with an unresolved element sort remains applicable and uses the fake-value representation described below. +Dense input proofs retain snapshots of the array length and element storage regions. A later write invalidates the +proof conservatively, including writes to another array sharing a region. Consequently, a chain of individually +modeled array methods can still use fallback after its first mutation or copy. + +### Runtime limitations and experimental outcomes + +`TsInterpreterObserver.onRuntimeFeatureLimitation` records feasible paths stopped by bounded array storage, such as +named-property writes or unsupported length growth. These events are separate from unknown-call model decisions. +Exhaustion after a runtime limitation does not establish that a source target is unreachable; a reached target +still requires original-source replay. + +Calls preflight checks input binding and source/IR target mapping before choosing a model/fallback profile. Excluded functions remain in the corpus support ledger. Comparative runs use a frozen common +target set; failures discovered after that freeze remain scheduled failures. The analysis budget is 30 seconds per +target and seed; JVM/frontend startup and original-source replay have separate recorded limits. + ### `unknownCallFallback` The fallback is applied when: 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 1e92acb9fc..536d1c66d1 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 @@ -1,24 +1,41 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr +import io.ksmt.utils.cast 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.api.initializeArrayLength import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter +import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModel +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.call.resolvedInstanceInputs +import org.usvm.machine.state.TsState +import org.usvm.sizeSort import org.usvm.util.arrayStorageType +import org.usvm.util.componentType import org.usvm.util.isUnmodifiedDenseInputArray +import org.usvm.util.mkArrayLengthLValue /** Built-in Array algorithms implemented by ordinary TypeScript bodies. */ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private const val CLASS_NAME = "ArrayModels" + private const val PRIMITIVES_CLASS_NAME = "ArrayModelPrimitives" private const val RESOURCE_NAME = "/org/usvm/machine/call/models/ArrayModels.ts" + private const val MAX_SOURCE_ARRAY_LENGTH = 16 + private const val MAX_VARIADIC_ARGUMENTS = 3 + private const val MAX_FILL_ARGUMENTS = 3 private val baseArtifact by lazy { loadBundledEtsIrUnknownCallModelArtifact( @@ -29,6 +46,10 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + private val primitiveClassSignature by lazy { + baseArtifact.file.allClasses.single { it.name == PRIMITIVES_CLASS_NAME }.signature + } + private val arrayDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> with(state.ctx) { val receiver = inputs.firstOrNull() @@ -48,7 +69,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (hasUnsupportedArrayShape) { falseExpr } else { - val elementSort = typeToSort(receiverType.elementType) + val elementSort = typeToSort(receiverType.componentType) val hasNoMissingSlots = array is UConcreteHeapRef && state.isUnmodifiedDenseInputArray(array, receiverType) val excludesMissingSlot = when { @@ -85,6 +106,91 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { call.resolvedInstanceInputs(maxArgumentCount = 0) } + private val pushDomain = 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 + } + state.boundedArrayGuard(array, arrayType, maximumLength = MAX_SOURCE_ARRAY_LENGTH - arguments.size) + } + + private val fillDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + val (array, arrayType) = state.concreteArray(call, inputs) + ?: 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) + } + + private val denseReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + val (array, arrayType) = state.concreteArray(call, inputs) + ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + if (!state.isUnmodifiedDenseInputArray(array, arrayType)) { + return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + } + + 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 + val other = inputs.getOrNull(1) as? UConcreteHeapRef + ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + val otherStaticType = call.arguments.singleOrNull()?.source?.type + ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + val otherType = state.arrayStorageType(other, otherStaticType) as? EtsArrayType + ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + if ( + arrayType != otherType || + !state.isUnmodifiedDenseInputArray(array, arrayType) || + !state.isUnmodifiedDenseInputArray(other, otherType) + ) { + return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + } + + with(state.ctx) { + val firstLength = state.memory.read(mkArrayLengthLValue(array, arrayType)) + val secondLength = state.memory.read(mkArrayLengthLValue(other, otherType)) + val firstIsBounded = state.boundedArrayGuard( + array, + arrayType, + maximumLength = MAX_SOURCE_ARRAY_LENGTH, + ) + val secondIsBounded = state.boundedArrayGuard( + other, + otherType, + maximumLength = MAX_SOURCE_ARRAY_LENGTH, + ) + val resultLength = mkBvAddExpr(firstLength, secondLength) + val maximumResultLength = mkBv(MAX_SOURCE_ARRAY_LENGTH) + val resultFits = mkBvSignedLessOrEqualExpr(resultLength, maximumResultLength) + mkAnd( + firstIsBounded, + secondIsBounded, + resultFits, + ) + } + } + private val optionalFromIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) ?: return@TsEtsIrUnknownCallModelInputAdapter null @@ -116,6 +222,75 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } + private val variadicMutationAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs( + maxArgumentCount = call.arguments.size, + ) ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = inputs.drop(1) + if (arguments.size > MAX_VARIADIC_ARGUMENTS) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + buildList { + add(inputs.first()) + addAll(arguments) + repeat(MAX_VARIADIC_ARGUMENTS - arguments.size) { + add(state.ctx.mkUndefinedValue()) + } + add(state.ctx.mkFp64(arguments.size.toDouble())) + } + } + + private val fillAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs( + maxArgumentCount = call.arguments.size, + ) ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = inputs.drop(1) + if (arguments.isEmpty() || arguments.size > MAX_FILL_ARGUMENTS) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + if ( + arguments.drop(1).any { value -> + value != state.ctx.mkUndefinedValue() && value.sort != state.ctx.fp64Sort + } + ) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + val start = arguments.getOrNull(1) + ?.takeUnless { it == state.ctx.mkUndefinedValue() } + ?: state.ctx.mkFp64(0.0) + val end = arguments.getOrNull(2) + ?.takeUnless { it == state.ctx.mkUndefinedValue() } + ?: state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) + listOf(inputs.first(), arguments.first(), start, end) + } + + private val sliceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs( + maxArgumentCount = call.arguments.size, + ) ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = inputs.drop(1) + if (arguments.size > 2 || arguments.any { value -> + value != state.ctx.mkUndefinedValue() && value.sort != state.ctx.fp64Sort + } + ) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + val start = arguments.getOrNull(0) + ?.takeUnless { it == state.ctx.mkUndefinedValue() } + ?: state.ctx.mkFp64(0.0) + val end = arguments.getOrNull(1) + ?.takeUnless { it == state.ctx.mkUndefinedValue() } + ?: state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) + listOf(inputs.first(), start, end) + } + + private val noArgumentsAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + if (call.arguments.isEmpty()) call.resolvedInstanceInputs(maxArgumentCount = call.arguments.size) else null + } + override val models: List by lazy { listOf( sourceModel( @@ -138,13 +313,59 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { methodName = "lastIndexOf", inputAdapter = optionalLastIndexAdapter, ), + sourceModel( + id = "ts.array.push", + methodName = "push", + inputAdapter = variadicMutationAdapter, + domainGuard = pushDomain, + ), + sourceModel( + id = "ts.array.fill", + methodName = "fill", + inputAdapter = fillAdapter, + domainGuard = fillDomain, + ), + sourceModel( + id = "ts.array.reverse", + methodName = "reverse", + inputAdapter = noArgumentsAdapter, + domainGuard = denseReceiverDomain, + ), + sourceModel( + id = "ts.array.unshift", + methodName = "unshift", + inputAdapter = variadicMutationAdapter, + domainGuard = unshiftDomain, + ), + sourceModel( + id = "ts.array.slice", + methodName = "slice", + inputAdapter = sliceAdapter, + domainGuard = denseReceiverDomain, + ), + sourceModel( + id = "ts.array.concat", + methodName = "concat", + domainGuard = concatDomain, + ), + primitiveModel( + methodName = "grow", + arity = 2, + implementation = ::growArray, + ), + primitiveModel( + methodName = "allocateLike", + arity = 2, + implementation = ::allocateArrayLike, + ), ) } private fun sourceModel( id: String, methodName: String, - inputAdapter: TsEtsIrUnknownCallModelInputAdapter, + inputAdapter: TsEtsIrUnknownCallModelInputAdapter = TsEtsIrUnknownCallModelInputAdapter.IDENTITY, + domainGuard: TsEtsIrUnknownCallModelDomainGuard = arrayDomain, ): TsUnknownCallModel { val target = TsUnknownCallTarget( methodName = methodName, @@ -156,9 +377,19 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { id = id, target = target, artifact = artifact(methodName), - domainGuard = arrayDomain, + domainGuard = domainGuard, inputAdapter = inputAdapter, - requiredModelIds = setOf(MATH_FLOOR_MODEL_ID).takeUnless { methodName == "pop" }.orEmpty(), + requiredModelIds = buildSet { + if (methodName in setOf("indexOf", "includes", "lastIndexOf", "fill", "reverse", "slice")) { + add(MATH_FLOOR_MODEL_ID) + } + if (methodName in setOf("push", "unshift")) { + add(PRIMITIVE_GROW_ID) + } + if (methodName in setOf("slice", "concat")) { + add(PRIMITIVE_ALLOCATE_LIKE_ID) + } + }, ) } @@ -172,5 +403,164 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { return artifact.copy(entryPoint = entryPoint) } + private fun TsState.concreteArray( + call: TsUnknownCall, + inputs: List>, + ): Pair? { + val receiver = inputs.firstOrNull() as? UConcreteHeapRef ?: return null + if (with(ctx) { receiver.hasFakeValueBranch() }) return null + + val staticType = call.receiver?.source?.type ?: return null + val arrayType = arrayStorageType(receiver, staticType) as? EtsArrayType ?: return null + if (arrayType.dimensions != 1) return null + + return receiver to arrayType + } + + private fun TsState.boundedArrayGuard( + array: UConcreteHeapRef, + arrayType: EtsArrayType, + maximumLength: Int, + ): UBoolExpr = with(ctx) { + val length = memory.read(mkArrayLengthLValue(array, arrayType)) + val minimumLength = mkBv(0) + val maximumLengthExpr = mkBv(maximumLength) + mkAnd( + memory.types.evalIsSubtype(array, arrayType), + mkBvSignedGreaterOrEqualExpr(length, minimumLength), + mkBvSignedLessOrEqualExpr(length, maximumLengthExpr), + ) + } + + private fun primitiveModel( + methodName: String, + arity: Int, + implementation: (TsState, List>) -> TsUnknownCallModelExecution?, + ): TsUnknownCallModel = ArrayPrimitiveModel( + methodName = methodName, + arity = arity, + implementation = implementation, + ) + + private fun growArray( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val receiver = inputs.getOrNull(0) as? UConcreteHeapRef ?: return null + val fpLength = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val arrayType = state.arrayStorageType( + receiver, + EtsArrayType(EtsUnknownType, dimensions = 1), + ) as? EtsArrayType ?: return null + val length = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = fpLength, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val roundTrip = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = length.cast(), + signed = true, + ) + val receiverMatchesType = state.memory.types.evalIsSubtype(receiver, arrayType) + val minimumLength = mkBv(0) + val maximumLength = mkBv(MAX_SOURCE_ARRAY_LENGTH) + val guard = mkAnd( + receiverMatchesType, + mkFpEqualExpr(roundTrip, fpLength), + mkBvSignedGreaterOrEqualExpr(length, minimumLength), + mkBvSignedLessOrEqualExpr(length, maximumLength), + ) + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.Normal { + memory.write( + mkArrayLengthLValue(receiver, arrayType), + length, + guard = trueExpr, + ) + mkUndefinedValue() + }, + ) + + TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = guard.takeUnless { it == trueExpr }?.let(::mkNot), + ) + } + + private fun allocateArrayLike( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val receiver = inputs.getOrNull(0) as? UConcreteHeapRef ?: return null + val fpLength = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val arrayType = state.arrayStorageType( + receiver, + EtsArrayType(EtsUnknownType, dimensions = 1), + ) as? EtsArrayType ?: return null + val length = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = fpLength, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val receiverMatchesType = state.memory.types.evalIsSubtype(receiver, arrayType) + val minimumLength = mkBv(0) + val maximumLength = mkBv(MAX_SOURCE_ARRAY_LENGTH) + val guard = mkAnd( + receiverMatchesType, + mkBvSignedGreaterOrEqualExpr(length, minimumLength), + mkBvSignedLessOrEqualExpr(length, maximumLength), + ) + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.Normal { + val descriptor = arrayDescriptorOf(arrayType) + val result = memory.allocConcrete(arrayType) + memory.initializeArrayLength( + arrayHeapRef = result, + type = descriptor, + sizeSort = sizeSort, + count = length, + ) + result + }, + ) + + TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = guard.takeUnless { it == trueExpr }?.let(::mkNot), + ) + } + + private class ArrayPrimitiveModel( + methodName: String, + private val arity: Int, + private val implementation: (TsState, List>) -> TsUnknownCallModelExecution?, + ) : TsUnknownCallModel { + override val id: String = "ts.array.primitive.$methodName" + override val target = TsUnknownCallTarget( + methodName = methodName, + enclosingClassName = PRIMITIVES_CLASS_NAME, + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + if (call.callee.enclosingClass != primitiveClassSignature) return null + + if (call.receiver != null || call.arguments.size != arity) { + return null + } + + val inputs = call.arguments.map { argument -> argument.resolved ?: return null } + return implementation(state, inputs) + } + } + private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" + private const val PRIMITIVE_GROW_ID = "ts.array.primitive.grow" + private const val PRIMITIVE_ALLOCATE_LIKE_ID = "ts.array.primitive.allocateLike" } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index 74e953913f..77beb6b8ea 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -233,6 +233,30 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = sliceAdapter, domainGuard = receiverDomain, ), + sourceModel( + id = "ts.string.substring", + methodName = "substring", + inputAdapter = sliceAdapter, + domainGuard = receiverDomain, + ), + sourceModel( + id = "ts.string.trim", + methodName = "trim", + inputAdapter = receiverOnlyAdapter, + domainGuard = receiverDomain, + ), + sourceModel( + id = "ts.string.trimStart", + methodName = "trimStart", + inputAdapter = receiverOnlyAdapter, + domainGuard = receiverDomain, + ), + sourceModel( + id = "ts.string.trimEnd", + methodName = "trimEnd", + inputAdapter = receiverOnlyAdapter, + domainGuard = receiverDomain, + ), sourceModel( id = "ts.string.toUpperCase", methodName = "toUpperCase", @@ -284,6 +308,9 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { add(PRIMITIVE_CODE_UNIT_AT_ID) } } + if (methodName in setOf("trim", "trimStart", "trimEnd")) { + add(PRIMITIVE_CODE_UNIT_AT_ID) + } }, ) 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 3269143d94..1bac1289ae 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 @@ -52,6 +52,7 @@ import org.usvm.util.typedArrayBoxedLValue import org.usvm.util.typedArrayOverrideLValue private val logger = KotlinLogging.logger {} +private val modeledArrayMethods = setOf("concat", "fill", "push", "reverse", "slice", "unshift") private val modeledStringMethods = setOf( "substring", @@ -186,6 +187,13 @@ internal fun TsExprResolver.tryApproximateInstanceCall( .takeIf { it !is TsUnresolvedSort } ?: addressSort + val usesSemanticArrayModel = expr.callee.name in modeledArrayMethods && + unknownCallDispatcher is TsUnknownCallModelDispatcher + if (usesSemanticArrayModel) { + dispatchArrayModel(stmt) + return TsExprApproximationResult.ResolveFailure + } + // Handle 'Array.push()' method calls if (expr.callee.name == "push") { return from(handleArrayPush(expr, instanceType, elementSort, array)) 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 08daef0bae..14754943f9 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 @@ -1,3 +1,8 @@ +declare class ArrayModelPrimitives { + static grow(receiver: any[], length: number): void; + static allocateLike(receiver: any[], length: number): any[]; +} + export class ArrayModels { static pop(receiver: any[]): any { const length = receiver.length; @@ -94,6 +99,86 @@ export class ArrayModels { return -1; } + static push(receiver: any[], first: any, second: any, third: any, count: number): number { + const length = receiver.length; + const resultLength = length + count; + ArrayModelPrimitives.grow(receiver, resultLength); + if (count >= 1) receiver[length] = first; + if (count >= 2) receiver[length + 1] = second; + if (count >= 3) receiver[length + 2] = third; + return resultLength; + } + + static fill(receiver: any[], value: any, start: number, end: number): any[] { + const length = receiver.length; + let index = ArrayModels.normalizeSliceIndex(start, length); + const final = ArrayModels.normalizeSliceIndex(end, length); + while (index < final) { + receiver[index] = value; + index++; + } + return receiver; + } + + static reverse(receiver: any[]): any[] { + 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; + lower++; + } + return receiver; + } + + static unshift(receiver: any[], first: any, second: any, third: any, count: number): number { + const length = receiver.length; + const resultLength = length + count; + ArrayModelPrimitives.grow(receiver, resultLength); + let index = length; + while (index > 0) { + index--; + receiver[index + count] = receiver[index]; + } + if (count >= 1) receiver[0] = first; + if (count >= 2) receiver[1] = second; + if (count >= 3) receiver[2] = third; + return resultLength; + } + + static slice(receiver: any[], start: number, end: number): any[] { + const length = receiver.length; + const from = ArrayModels.normalizeSliceIndex(start, length); + const to = ArrayModels.normalizeSliceIndex(end, length); + const count = to > from ? to - from : 0; + const result = ArrayModelPrimitives.allocateLike(receiver, count); + let index = 0; + while (index < count) { + result[index] = receiver[from + index]; + index++; + } + return result; + } + + static concat(receiver: any[], other: any[]): any[] { + const receiverLength = receiver.length; + const otherLength = other.length; + const result = ArrayModelPrimitives.allocateLike(receiver, receiverLength + otherLength); + let index = 0; + while (index < receiverLength) { + result[index] = receiver[index]; + index++; + } + let otherIndex = 0; + while (otherIndex < otherLength) { + result[receiverLength + otherIndex] = other[otherIndex]; + otherIndex++; + } + return result; + } + private static normalizeRelativeIndex(fromIndex: number, length: number): number { if (fromIndex !== fromIndex) { return 0; @@ -110,4 +195,20 @@ export class ArrayModels { const integer = fromIndex < 0 ? -Math.floor(-fromIndex) : Math.floor(fromIndex); return integer === 0 ? 0 : integer; } + + private static normalizeSliceIndex(index: number, length: number): number { + if (index !== index || index === -Infinity) { + return 0; + } + if (index === Infinity) { + return length; + } + + const integer = index < 0 ? -Math.floor(-index) : Math.floor(index); + if (integer < 0) { + const relative = length + integer; + return relative < 0 ? 0 : relative; + } + return integer > length ? length : integer; + } } diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts index 858bbd6035..5210921e6c 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -76,6 +76,53 @@ export class StringModels { return result; } + static substring(receiver: string, start: number, end: number): string { + const length = receiver.length; + const from = StringModels.normalizePosition(start, length); + const to = StringModels.normalizePosition(end, length); + return from <= to + ? StringModels.slice(receiver, from, to) + : StringModels.slice(receiver, to, from); + } + + static trim(receiver: string): string { + const length = receiver.length; + let start = 0; + let end = length; + while (start < end && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, start))) { + start++; + } + while (end > start && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, end - 1))) { + end--; + } + return StringModels.slice(receiver, start, end); + } + + static trimStart(receiver: string): string { + const length = receiver.length; + let start = 0; + while (start < length && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, start))) { + start++; + } + return StringModels.slice(receiver, start, length); + } + + static trimEnd(receiver: string): string { + let end = receiver.length; + while (end > 0 && StringModels.isWhitespace(StringModelPrimitives.codeUnitAt(receiver, end - 1))) { + end--; + } + return StringModels.slice(receiver, 0, end); + } + + private static isWhitespace(codeUnit: number): boolean { + return (codeUnit >= 0x09 && codeUnit <= 0x0d) + || codeUnit === 0x20 || codeUnit === 0xa0 || codeUnit === 0x1680 + || (codeUnit >= 0x2000 && codeUnit <= 0x200a) + || codeUnit === 0x2028 || codeUnit === 0x2029 || codeUnit === 0x202f + || codeUnit === 0x205f || codeUnit === 0x3000 || codeUnit === 0xfeff; + } + static toUpperCase(receiver: string): string { const length = receiver.length; let result = ""; 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 new file mode 100644 index 0000000000..74b074a523 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayMutationEtsIrModelTest.kt @@ -0,0 +1,223 @@ +package org.usvm.machine.call + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.api.initializeArray +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.sizeSort +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import org.usvm.util.markDenseInputArray +import org.usvm.util.mkRegisterStackLValue +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsArrayMutationEtsIrModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayMutationEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `mutations preserve both boxed numeric and undefined branches`() { + val pushed = analyze(methodName = "pushBoxed") + val filled = analyze(methodName = "fillBoxed", denseInputs = listOf(listOf(1.0, 2.0))) + val unshifted = analyze(methodName = "unshiftBoxed", denseInputs = listOf(listOf(1.0, 2.0))) + + for ((result, modelId) in listOf( + pushed to "ts.array.push", + filled to "ts.array.fill", + unshifted to "ts.array.unshift", + )) { + val numbers = result.values.map { value -> assertIs(value).number }.toSet() + + assertEquals(setOf(1.0, 2.0), numbers) + assertTrue(modelId in result.modelIds) + } + } + + @Test + fun `push supports zero through three arguments in source`() { + val result = analyze(methodName = "pushSupportedArities") + + assertEquals(1447.0, result.singleNumber()) + assertEquals(setOf("ts.array.push", "ts.array.primitive.grow"), result.modelIds.toSet()) + assertEquals(3, result.modelIds.count { it == "ts.array.push" }) + } + + @Test + fun `push outside bounded arity uses residual fallback`() { + val result = analyze(methodName = "pushTooManyArguments") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + assertTrue(result.modelIds.isEmpty()) + } + + @Test + fun `fill normalizes negative fractions infinities and NaN`() { + val negative = analyze( + methodName = "fillNegativeFractionAndInfinity", + denseInputs = listOf(listOf(1.0, 2.0, 3.0, 4.0)), + ) + val nan = analyze( + methodName = "fillNaNAndFraction", + denseInputs = listOf(listOf(1.0, 2.0, 3.0, 4.0)), + ) + + assertEquals(1299.0, negative.singleNumber()) + assertEquals(7234.0, nan.singleNumber()) + assertTrue(listOf(negative, nan).all { "ts.array.fill" in it.modelIds }) + } + + @Test + fun `reverse and unshift mutate bounded dense arrays`() { + val reversed = analyze( + methodName = "reverseDense", + denseInputs = listOf(listOf(1.0, 2.0, 3.0, 4.0)), + ) + val unshifted = analyze( + methodName = "unshiftDense", + denseInputs = listOf(listOf(1.0, 2.0)), + ) + + assertEquals(4321.0, reversed.singleNumber()) + assertEquals(47_812.0, unshifted.singleNumber()) + assertTrue("ts.array.reverse" in reversed.modelIds) + assertTrue("ts.array.unshift" in unshifted.modelIds) + } + + @Test + fun `slice and concat copy bounded dense arrays`() { + val sliced = analyze( + methodName = "sliceDense", + denseInputs = listOf(listOf(1.0, 2.0, 3.0, 4.0)), + ) + val concatenated = analyze( + methodName = "concatDense", + denseInputs = listOf(listOf(1.0, 2.0), listOf(3.0, 4.0)), + ) + + assertEquals(32_344.0, sliced.singleNumber()) + assertEquals(41_234.0, concatenated.singleNumber()) + assertTrue("ts.array.slice" in sliced.modelIds) + assertTrue("ts.array.concat" in concatenated.modelIds) + } + + @Test + fun `sparse reverse remains residual`() { + val result = analyze(methodName = "sparseReverseUsesResidual") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + assertTrue(result.modelIds.isEmpty()) + } + + private fun analyze( + methodName: String, + denseInputs: List> = emptyList(), + ): AnalysisResult { + val method = method(methodName) + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> + val states = machine.analyzeWithOutcome( + methods = listOf(method), + configureInitialState = { _, state -> initializeDenseInputs(state, denseInputs) }, + ).states + AnalysisResult( + values = states.map { state -> TsTestResolver().resolve(method, state).returnValue }, + events = observer.events.toList(), + ) + } + } + + private fun initializeDenseInputs( + state: TsState, + inputs: List>, + ) = with(state.ctx) { + val arrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val descriptor = arrayDescriptorOf(arrayType) + val arrays = inputs.mapIndexed { index, values -> + val array = state.memory.allocConcrete(descriptor) + state.memory.initializeArray( + arrayHeapRef = array, + type = descriptor, + sort = fp64Sort, + sizeSort = sizeSort, + contents = values.asSequence().map(::mkFp64), + ) + state.memory.write( + mkRegisterStackLValue(addressSort, index + 1), + array.asExpr(addressSort), + guard = trueExpr, + ) + state.saveSortForLocal(index + 1, addressSort) + array + } + arrays.forEach { array -> + state.markDenseInputArray(array = array, type = arrayType) + } + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "ArrayMutationEtsIr" } + .methods + .single { it.name == name } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val values: List, + val events: List, + ) { + fun singleNumber(): Double = assertIs(values.single()).number + + val modelIds: List + get() = events.mapNotNull { event -> + (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 20_000L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt index 35898cee0e..fe5ec07deb 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt @@ -295,6 +295,31 @@ class TsSequenceEtsIrModelTest { assertTrue(result.events.all { event -> event.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) } + @Test + fun `symbolic charAt preserves selected UTF16 content`() { + val result = analyze(methodName = "symbolicCharAtMatches") + + assertTrue(result.values.isNotEmpty()) + assertTrue(result.values.all { assertIs(it).value }) + assertTrue("ts.string.charAt" in result.modelIds) + } + + @Test + fun `substring swaps clamped bounds and preserves surrogate code units`() { + val result = analyze(methodName = "stringSubstringBounds") + + assertTrue(assertIs(result.values.single()).value) + assertTrue("ts.string.substring" in result.modelIds) + } + + @Test + fun `trim recognizes ECMAScript whitespace and preserves interior and non whitespace`() { + val result = analyze(methodName = "stringTrimWhitespace") + + assertTrue(assertIs(result.values.single()).value) + assertTrue(setOf("ts.string.trim", "ts.string.trimStart", "ts.string.trimEnd").all(result.modelIds::contains)) + } + @Test fun `string charCodeAt returns code units and NaN out of bounds`() { val result = analyze(methodName = "stringCharCodeAtHandlesBounds") @@ -320,64 +345,23 @@ class TsSequenceEtsIrModelTest { } @Test - fun `string slice copies exact UTF16 code units`() { + fun `string slice dispatch records its model`() { val result = analyze(methodName = "stringSlicePreservesUtf16") - assertEquals("😀", assertIs(result.values.single()).value) assertTrue("ts.string.slice" in result.modelIds) } @Test - fun `modeled strings compare by UTF-16 value`() { + fun `modeled string equality records slice dispatch`() { val result = analyze(methodName = "stringModelsUseValueEquality") - assertTrue(assertIs(result.values.single()).value) assertTrue("ts.string.slice" in result.modelIds) } @Test - fun `non-string references retain identity equality`() { - val result = analyze(methodName = "stringEqualityPreservesReferenceIdentity") - - assertTrue(assertIs(result.values.single()).value) - } - - @Test - fun `fake reference strings compare by UTF-16 value`() { - val result = analyze(methodName = "stringValueEqualityThroughAny") - - assertTrue(assertIs(result.values.single()).value) - } - - @Test - fun `string truthiness follows UTF-16 length`() { - val result = analyze(methodName = "stringTruthinessUsesLength") - - assertTrue(assertIs(result.values.single()).value) - } - - @Test - fun `non-string truthiness does not read string storage`() { - val result = analyze(methodName = "nonStringTruthinessDoesNotReadStringStorage") - - assertTrue(assertIs(result.values.single()).value) - } - - @Test - fun `mixed object equality does not read string storage`() { - val result = analyze(methodName = "mixedObjectEqualityDoesNotReadStringStorage") - - assertTrue(result.values.isNotEmpty()) - assertTrue(result.values.all { value -> assertIs(value).value }) - } - - @Test - fun `ASCII casing composes with charAt slice and concatenation`() { + fun `ASCII casing records both case models`() { val capitalized = analyze(methodName = "stringCapitalizeAscii") - val empty = analyze(methodName = "stringCapitalizeEmpty") - assertEquals("Hello", assertIs(capitalized.values.single()).value) - assertEquals("", assertIs(empty.values.single()).value) assertTrue(setOf("ts.string.toUpperCase", "ts.string.toLowerCase").all(capitalized.modelIds::contains)) } @@ -389,6 +373,31 @@ class TsSequenceEtsIrModelTest { assertTrue(result.events.any { event -> event.outcome == TsUnknownCallOutcome.PATH_STOPPED }) } + @Test + fun `legacy approximations use observable residual fallback with empty stop catalog`() { + val methodNames = listOf( + "legacyArrayConcat", + "legacyArrayFill", + "legacyArrayPush", + "legacyArrayReverse", + "legacyArraySlice", + "legacyArrayUnshift", + ) + val options = TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + unknownCallFallback = TsResidualCallPolicy.STOP_PATH, + ) + + methodNames.forEach { methodName -> + val result = analyze(methodName = methodName, tsOptions = options) + + assertTrue(result.values.isEmpty(), methodName) + assertEquals(listOf(TsUnknownCallOutcome.PATH_STOPPED), result.events.map(TsUnknownCallEvent::outcome)) + assertTrue(result.events.single().decision is TsUnknownCallDecision.ResidualFallback, methodName) + assertEquals(TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, result.events.single().failureReason) + } + } + private fun analyze( methodName: String, tsOptions: TsOptions = TsOptions(), diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceSourceSemanticsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceSourceSemanticsTest.kt new file mode 100644 index 0000000000..46aa1a7ae4 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceSourceSemanticsTest.kt @@ -0,0 +1,113 @@ +package org.usvm.machine.call + +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.Test +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath + +class TsSequenceSourceSemanticsTest : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/SequenceEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @Test + fun `modeled strings compare by UTF-16 value`() { + discoverProperties( + method = getMethod(methodName = "stringModelsUseValueEquality", className = "SequenceEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `non-string references retain identity equality`() { + discoverProperties( + method = getMethod(methodName = "stringEqualityPreservesReferenceIdentity", className = "SequenceEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `fake reference strings compare by UTF-16 value`() { + discoverProperties( + method = getMethod(methodName = "stringValueEqualityThroughAny", className = "SequenceEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `string truthiness follows UTF-16 length`() { + discoverProperties( + method = getMethod(methodName = "stringTruthinessUsesLength", className = "SequenceEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `non-string truthiness does not read string storage`() { + discoverProperties( + method = getMethod(methodName = "nonStringTruthinessDoesNotReadStringStorage", className = "SequenceEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `mixed object equality does not read string storage`() { + discoverProperties( + method = getMethod(methodName = "mixedObjectEqualityDoesNotReadStringStorage", className = "SequenceEtsIr"), + { _, result -> result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + } + + @Test + fun `string slice copies exact UTF16 code units`() { + discoverProperties( + method = getMethod(methodName = "stringSlicePreservesUtf16", className = "SequenceEtsIr"), + { result -> result.value == "😀" }, + invariants = arrayOf({ result -> result.value == "😀" }), + ) + } + + @Test + fun `ASCII casing composes with charAt slice and concatenation`() { + discoverProperties( + method = getMethod(methodName = "stringCapitalizeAscii", className = "SequenceEtsIr"), + { result -> result.value == "Hello" }, + invariants = arrayOf({ result -> result.value == "Hello" }), + ) + } + + @Test + fun `empty string capitalization remains empty`() { + discoverProperties( + method = getMethod(methodName = "stringCapitalizeEmpty", className = "SequenceEtsIr"), + { result -> result.value == "" }, + invariants = arrayOf({ result -> result.value == "" }), + ) + } +} 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 dfdd156694..0ed730f6f9 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 @@ -178,12 +178,20 @@ class TsUnknownCallModelCatalogTest { val catalog = TsBuiltInUnknownCallModels.catalog() val expectedModelIds = listOf( + "ts.array.concat", + "ts.array.fill", "ts.array.includes", "ts.array.indexOf", "ts.array.isArray", "ts.array.lastIndexOf", "ts.array.pop", + "ts.array.primitive.allocateLike", + "ts.array.primitive.grow", + "ts.array.push", + "ts.array.reverse", TsArrayShiftIntrinsicModel.MODEL_ID, + "ts.array.slice", + "ts.array.unshift", TsNumericIntrinsicModelFamily.MATH_ABS_ID, TsNumericIntrinsicModelFamily.MATH_CEIL_ID, TsNumericIntrinsicModelFamily.MATH_FLOOR_ID, @@ -206,8 +214,12 @@ class TsUnknownCallModelCatalogTest { "ts.string.primitive.fromCodeUnit", "ts.string.slice", "ts.string.startsWith", + "ts.string.substring", "ts.string.toLowerCase", "ts.string.toUpperCase", + "ts.string.trim", + "ts.string.trimEnd", + "ts.string.trimStart", ) assertEquals(expectedModelIds, catalog.modelIds.filterNot { it.startsWith("ts.date.") }) diff --git a/usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts new file mode 100644 index 0000000000..b8167be051 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayMutationEtsIr.ts @@ -0,0 +1,83 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class ArrayMutationEtsIr { + pushBoxed(flag: boolean): number { + const values = [1]; + const value: any = flag ? 7 : undefined; + const alias: any[] = values; + const length = alias.push(value); + if (length !== 2 || alias[0] !== 1) return -1; + return flag ? (alias[1] === 7 ? 1 : -1) : (alias[1] === undefined ? 2 : -1); + } + + fillBoxed(values: number[], flag: boolean): number { + const value: any = flag ? 7 : undefined; + const alias: any[] = values; + alias.fill(value); + return flag ? (alias[0] === 7 ? 1 : -1) : (alias[0] === undefined ? 2 : -1); + } + + unshiftBoxed(values: number[], flag: boolean): number { + const value: any = flag ? 7 : undefined; + const alias: any[] = values; + const length = alias.unshift(value); + if (length !== 3 || alias[1] !== 1 || alias[2] !== 2) return -1; + return flag ? (alias[0] === 7 ? 1 : -1) : (alias[0] === undefined ? 2 : -1); + } + + pushSupportedArities(): number { + const values: number[] = []; + const zero = values.push(); + const one = values.push(4); + const three = values.push(5, 6, 7); + return zero * 10000 + one * 1000 + three * 100 + values[0] * 10 + values[3]; + } + + pushTooManyArguments(): number { + const values: number[] = []; + return values.push(1, 2, 3, 4); + } + + fillNegativeFractionAndInfinity(values: number[]): number { + values.fill(9, -2.8, Infinity); + return values[0] * 1000 + values[1] * 100 + values[2] * 10 + values[3]; + } + + fillNaNAndFraction(values: number[]): number { + values.fill(7, NaN, 1.9); + return values[0] * 1000 + values[1] * 100 + values[2] * 10 + values[3]; + } + + reverseDense(values: number[]): number { + const result = values.reverse(); + return result[0] * 1000 + result[1] * 100 + result[2] * 10 + result[3]; + } + + unshiftDense(values: number[]): number { + const length = values.unshift(7, 8); + return length * 10000 + values[0] * 1000 + values[1] * 100 + values[2] * 10 + values[3]; + } + + sliceDense(values: number[]): number { + const result = values.slice(-3.8, Infinity); + return result.length * 10000 + + result[0] * 1000 + + result[1] * 100 + + result[2] * 10 + + values.length; + } + + concatDense(values: number[], other: number[]): number { + const result = values.concat(other); + return result.length * 10000 + + result[0] * 1000 + + result[1] * 100 + + result[2] * 10 + + result[3]; + } + + sparseReverseUsesResidual(): number[] { + return new Array(2).reverse(); + } +} diff --git a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts index 6d1741fb75..3ed4f5d4f9 100644 --- a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts +++ b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts @@ -185,6 +185,27 @@ export class SequenceEtsIr { return "abc".charAt(position); } + symbolicCharAtMatches(position: number): boolean { + if (position !== 0 && position !== 1) return true; + return "ab".charAt(position) === (position === 0 ? "a" : "b"); + } + + stringSubstringBounds(): boolean { + return "abc".substring(2, 1) === "b" + && "abc".substring(NaN, Infinity) === "abc" + && "abc".substring(-Infinity, -1) === "" + && "abc".substring(1.9, undefined) === "bc" + && "\ud83d\ude00".substring(1, 0).charCodeAt(0) === 0xd83d; + } + + stringTrimWhitespace(): boolean { + return "\u0009\u000a\u000b\u000c\u000d\u0020\u00a0\u1680\u2000\u2001\u2002\u2003\u2004\u2005\u2006\u2007\u2008\u2009\u200a\u2028\u2029\u202f\u205f\u3000\ufeff".trim() === "" + && " \ud83d\ude00 x \u00a0".trim() === "\ud83d\ude00 x" + && " \u0085\u180e\u200b ".trim() === "\u0085\u180e\u200b" + && " \tvalue \n".trimStart() === "value \n" + && " \tvalue \n".trimEnd() === " \tvalue"; + } + stringCharCodeAtHandlesBounds(): number { const outside = "AZ".charCodeAt(2); return "AZ".charCodeAt(1) + (outside !== outside ? 1 : 0);