diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index b4506e3f6f..46c204fb8a 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -99,6 +99,7 @@ Every model implements `TsUnknownCallModel`: interface TsUnknownCallModel { val id: String val target: TsUnknownCallTarget + val requiredModelIds: Set fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? } @@ -127,6 +128,10 @@ The ID is used for configuration, observer events, and recursion prevention. Do Keep the same ID when an equivalent model moves from Kotlin to TypeScript. +Selecting models with `TsUnknownCallModelSelection.Only` expands `requiredModelIds` transitively and sorts the final +catalog by ID. This keeps a high-level source model usable when it calls helper models. Missing dependency IDs are +rejected while building the catalog; an explicitly empty selection remains empty. + ### Choosing a target `TsUnknownCallTarget` matches stable call metadata declaratively: @@ -146,11 +151,11 @@ a priority rule. The enabled model set is frozen and sorted by ID when the catal The target identifies a call family. State-dependent checks, such as the receiver's symbolic runtime type, belong in `apply` or in an EtsIR model's domain guard. -The built-in array targets intentionally combine the method name with `PARTIAL_APPROXIMATION` instead of a class name. -That failure reason is emitted only after the regular approximation path has classified the receiver as an -`EtsArrayType` using the normalized receiver's storage type. An `any` alias of a known array can satisfy that check; -a receiver without array-type evidence cannot. The model still validates the resolved receiver and array shape -before changing memory. Both models preserve the array's storage type, including reference and unresolved elements. +The built-in array targets combine the method name with `PARTIAL_APPROXIMATION`. Array and String methods with the +same name also use a canonical enclosing class at this boundary. The failure reason is emitted only after the regular +approximation path has classified the normalized receiver by its storage type. An `any` alias of a known array can +satisfy that check; a receiver without array-type evidence cannot. The model still validates the resolved receiver +and array shape before changing memory. ## Applicability and residual states @@ -228,8 +233,35 @@ Array indexing and `length` assignment use the receiver's storage type. Writing zero through the current length, within the configured array-size limit. Growth remains unsupported because the engine does not represent newly created holes; those paths are pruned. -The entry point must be static and have a non-empty body. Its parameter count must equal the resolved receiver plus -argument count. Unresolved inputs or an arity mismatch make the model not applicable. +`Array.pop`, `indexOf`, `includes`, and `lastIndexOf` share one source-model family. Search offsets accept numbers and +the standard omitted or explicit-`undefined` defaults; other dynamic coercions use fallback. Array memory has no slot +presence bit, so a hole can look like a typed default. Searches for `0` or `false` therefore use fallback, as do +`indexOf(undefined)` and `lastIndexOf(undefined)`. `includes(undefined)` is accepted only for address or unresolved +storage; numeric and boolean storage use fallback because their holes currently read as typed defaults. Symbolic +numeric and boolean search values use a guarded model branch outside the typed default and residual fallback on the +unsupported default. Fake-wrapped dynamic search values use fallback. Position normalization depends on +`ts.math.floor`. + +The String source family implements `charAt`, `charCodeAt`, `indexOf`, `lastIndexOf`, `includes`, `startsWith`, +`endsWith`, `slice`, and ASCII case conversion. Character access, search, and slicing use ordinary `.length`, +`receiver[index]`, comparisons, loops, and concatenation in TypeScript/EtsIR. Only numeric UTF-16 code-unit reads +and one-code-unit construction remain intrinsic helpers for `charCodeAt` and case conversion. Position +normalization depends on `ts.math.floor`; case conversion needs only the two code-unit helpers. + +String indexing accepts canonical integral numeric positions and canonical numeric string keys. It returns one +UTF-16 code unit in range and `undefined` out of range, for fractions, or for non-finite numeric positions. Numeric +property-key conversion preserves symbolic numbers internally until the string property read; general object +properties still require concrete converted keys. String index writes and other unmodeled String properties +remain unsupported. + +Typed symbolic String parameters initialize bounded backing storage, so model guards accept symbolic receivers +and search strings with known backing, as well as constructed strings. `charAt` accepts symbolic positions, and +created character strings participate in value-based equality. ASCII case conversion retains its guarded length +limit of 16 code units and uses residual fallback for non-ASCII inputs. + +The entry point must be static and have a non-empty body. After its input adapter handles optional arguments or drops +non-semantic namespace receivers, its parameter count must equal the adapted input count. Unresolved required inputs +or an arity mismatch make the model not applicable. The domain guard has three useful outcomes: @@ -305,6 +337,9 @@ type guard. Unknown calls made inside a TypeScript model body use the same catalog and fallback as the original program. This lets source models compose with other source models and intrinsics. +Declare every nested semantic-model call in `requiredModelIds`. A selection containing only the high-level API then +expands to its helpers before the machine scene is materialized. + The state tracks each active model ID together with its call-stack depth. If the same model would redirect recursively, lookup declines that redirection and fallback is applied instead of entering an infinite loop. diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index f7ac37a74e..8a68506075 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -143,6 +143,6 @@ private fun TsState.makeFreshBoundedString(): UConcreteHeapRef = with(ctx) { ) memory.write(mkStringBackingLengthLValue(characters), length, guard = trueExpr) memory.write(mkStringBackingLValue(string), characters, guard = trueExpr) - boundedStringBackingRefs += string + boundedStringBackingRefs += string to maxStringLength string } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt index 304ee16335..a55c40d2e2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt @@ -112,15 +112,15 @@ class TsEtsIrUnknownCallModel( val artifact: TsEtsIrUnknownCallModelArtifact, val domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS, val inputAdapter: TsEtsIrUnknownCallModelInputAdapter = TsEtsIrUnknownCallModelInputAdapter.IDENTITY, + requiredModelIds: Set = emptySet(), ) : TsUnknownCallModel, TsMachineLocalUnknownCallModel { override val additionalSceneFiles: List = listOf(artifact.file) + override val requiredModelIds: Set = requiredModelIds.toSet() override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { - val resolvedInputs = call.resolvedInputs() ?: return null val inputs = inputAdapter.adapt( state = state, call = call, - resolvedInputs = resolvedInputs, ) ?: return null if (inputs.size != artifact.entryPoint.parameters.size) { return null @@ -161,6 +161,7 @@ class TsEtsIrUnknownCallModel( artifact = materializedArtifact, domainGuard = domainGuard, inputAdapter = inputAdapter, + requiredModelIds = requiredModelIds, ) } } @@ -170,11 +171,10 @@ fun interface TsEtsIrUnknownCallModelInputAdapter { fun adapt( state: TsState, call: TsUnknownCall, - resolvedInputs: List>, ): List>? companion object { - val IDENTITY = TsEtsIrUnknownCallModelInputAdapter { _, _, resolvedInputs -> resolvedInputs } + val IDENTITY = TsEtsIrUnknownCallModelInputAdapter { _, call -> call.resolvedInputs() } } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt index af0b657357..ee9c4d4a16 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt @@ -47,6 +47,14 @@ data class TsUnknownCallValue( val resolved: UExpr<*>?, ) +/** Takes the meaningful values from arguments already evaluated by the caller. */ +internal fun TsUnknownCall.resolvedInstanceInputs(maxArgumentCount: Int): List>? { + val resolvedReceiver = receiver?.resolved ?: return null + val resolvedArguments = arguments.take(maxArgumentCount).map { argument -> argument.resolved ?: return null } + + return listOf(resolvedReceiver) + resolvedArguments +} + /** Identifies the execution stage that prevented a TypeScript call from continuing normally. */ enum class TsUnknownCallFailureReason { STATIC_METHOD_NOT_FOUND, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt index 15d6f5c334..60feb720dc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt @@ -32,6 +32,8 @@ data class TsUnknownCallTarget( interface TsUnknownCallModel { val id: String val target: TsUnknownCallTarget + val requiredModelIds: Set + get() = emptySet() /** EtsIR files that must be visible to the interpreter while this model is enabled. */ val additionalSceneFiles: List diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt index ff7db78c35..c55afe0251 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt @@ -23,13 +23,28 @@ class TsUnknownCallModelCatalog( require(model.id.isNotBlank()) { "Semantic model ID must not be blank" } require(modelsById.put(model.id, model) == null) { "Duplicate semantic model ID: ${model.id}" } } + modelsById.values.forEach { model -> + val missingDependencies = model.requiredModelIds.subtract(modelsById.keys) + require(missingDependencies.isEmpty()) { + "Semantic model ${model.id} requires unknown model IDs: ${missingDependencies.sorted().joinToString()}" + } + } selectedModels = when (selection) { TsUnknownCallModelSelection.All -> modelsById.values is TsUnknownCallModelSelection.Only -> { val unknownIds = selection.ids.subtract(modelsById.keys) require(unknownIds.isEmpty()) { "Unknown semantic model IDs: ${unknownIds.sorted().joinToString()}" } - selection.ids.map(modelsById::getValue) + val expandedIds = linkedSetOf() + fun addWithDependencies(id: String) { + if (!expandedIds.add(id)) { + return + } + + modelsById.getValue(id).requiredModelIds.sorted().forEach(::addWithDependencies) + } + selection.ids.sorted().forEach(::addWithDependencies) + expandedIds.map(modelsById::getValue) } }.sortedBy(TsUnknownCallModel::id) 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 new file mode 100644 index 0000000000..b77c5bb9b4 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -0,0 +1,172 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +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.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.machine.call.resolvedInstanceInputs +import org.usvm.util.arrayStorageType + +/** Built-in Array algorithms implemented by ordinary TypeScript bodies. */ +internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { + private const val CLASS_NAME = "ArrayModels" + private const val RESOURCE_NAME = "/org/usvm/machine/call/models/ArrayModels.ts" + + private val baseArtifact by lazy { + loadBundledEtsIrUnknownCallModelArtifact( + resourceName = RESOURCE_NAME, + sourceFileName = "ArrayModels.ts", + entryPointClassName = CLASS_NAME, + entryPointMethodName = "pop", + ) + } + + private val arrayDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiver = inputs.firstOrNull() + val staticType = call.receiver?.source?.type + if (staticType == null || receiver?.sort != addressSort) { + falseExpr + } else { + val array = receiver.asExpr(addressSort) + val receiverType = state.arrayStorageType(array, staticType) as? EtsArrayType + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val searchElement = inputs.getOrNull(1) + val searchRef = searchElement + ?.takeIf { it.sort == addressSort } + ?.asExpr(addressSort) + val hasUnsupportedArrayShape = array.hasFakeValueBranch() || receiverType.dimensions != 1 || + searchRef?.hasFakeValueBranch() == true + if (hasUnsupportedArrayShape) { + falseExpr + } else { + val elementSort = typeToSort(receiverType.elementType) + val excludesMissingSlot = when { + searchElement == mkUndefinedValue() && + ( + call.callee.name in setOf("indexOf", "lastIndexOf") || + elementSort == fp64Sort || elementSort == boolSort + ) -> falseExpr + + elementSort == fp64Sort && searchElement?.sort == fp64Sort -> { + val searchNumber = searchElement.asExpr(fp64Sort) + val zero = mkFp64(0.0) + + mkNot(mkFpEqualExpr(searchNumber, zero)) + } + + elementSort == boolSort && searchElement?.sort == boolSort -> { + searchElement.asExpr(boolSort) + } + + else -> trueExpr + } + + mkAnd( + state.memory.types.evalIsSubtype(array, receiverType), + excludesMissingSlot, + ) + } + } + } + } + + private val receiverOnlyAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + call.resolvedInstanceInputs(maxArgumentCount = 0) + } + + private val optionalFromIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (inputs.size < 2) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + val fromIndex = inputs.getOrNull(2) + when { + fromIndex == null || fromIndex == state.ctx.mkUndefinedValue() -> inputs.take(2) + state.ctx.mkFp64(0.0) + fromIndex.sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + + private val optionalLastIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (inputs.size < 2) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + val fromIndex = inputs.getOrNull(2) + when { + fromIndex == null -> inputs + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) + fromIndex == state.ctx.mkUndefinedValue() -> inputs.take(2) + state.ctx.mkFp64(0.0) + fromIndex.sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + + override val models: List by lazy { + listOf( + sourceModel( + id = "ts.array.pop", + methodName = "pop", + inputAdapter = receiverOnlyAdapter, + ), + sourceModel( + id = "ts.array.indexOf", + methodName = "indexOf", + inputAdapter = optionalFromIndexAdapter, + ), + sourceModel( + id = "ts.array.includes", + methodName = "includes", + inputAdapter = optionalFromIndexAdapter, + ), + sourceModel( + id = "ts.array.lastIndexOf", + methodName = "lastIndexOf", + inputAdapter = optionalLastIndexAdapter, + ), + ) + } + + private fun sourceModel( + id: String, + methodName: String, + inputAdapter: TsEtsIrUnknownCallModelInputAdapter, + ): TsUnknownCallModel { + val target = TsUnknownCallTarget( + methodName = methodName, + enclosingClassName = "Array".takeUnless { methodName == "pop" }, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + + return TsEtsIrUnknownCallModel( + id = id, + target = target, + artifact = artifact(methodName), + domainGuard = arrayDomain, + inputAdapter = inputAdapter, + requiredModelIds = setOf(MATH_FLOOR_MODEL_ID).takeUnless { methodName == "pop" }.orEmpty(), + ) + } + + private fun artifact(methodName: String): TsEtsIrUnknownCallModelArtifact { + val artifact = baseArtifact + val entryPoint = artifact.file.allClasses + .single { it.name == CLASS_NAME } + .methods + .single { it.name == methodName } + + return artifact.copy(entryPoint = entryPoint) + } + + private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt deleted file mode 100644 index e6e0ad88c0..0000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt +++ /dev/null @@ -1,66 +0,0 @@ -package org.usvm.machine.call.intrinsic - -import io.ksmt.utils.asExpr -import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsFile -import org.usvm.machine.call.TsEtsIrUnknownCallModel -import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard -import org.usvm.machine.call.TsMachineLocalUnknownCallModel -import org.usvm.machine.call.TsUnknownCall -import org.usvm.machine.call.TsUnknownCallFailureReason -import org.usvm.machine.call.TsUnknownCallModel -import org.usvm.machine.call.TsUnknownCallTarget -import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact -import org.usvm.machine.state.TsState -import org.usvm.util.arrayStorageType -import java.util.IdentityHashMap - -/** Built-in `Array.pop` implemented by an ordinary TypeScript body. */ -internal object TsArrayPopEtsIrModel : TsBuiltInUnknownCallModel, TsMachineLocalUnknownCallModel { - override val id: String = "ts.array.pop" - override val target = TsUnknownCallTarget( - methodName = "pop", - failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, - ) - - private val model by lazy { - val artifact = loadBundledEtsIrUnknownCallModelArtifact( - resourceName = "/org/usvm/machine/call/models/ArrayModels.ts", - sourceFileName = "ArrayModels.ts", - entryPointClassName = "ArrayModels", - entryPointMethodName = "pop", - ) - val domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> - with(state.ctx) { - val receiver = inputs.singleOrNull() - val staticType = call.receiver?.source?.type - if (staticType == null || receiver?.sort != addressSort) { - falseExpr - } else { - val array = receiver.asExpr(addressSort) - val receiverType = state.arrayStorageType(array, staticType) as? EtsArrayType - if (array.hasFakeValueBranch() || receiverType?.dimensions != 1) { - falseExpr - } else { - state.memory.types.evalIsSubtype(array, receiverType) - } - } - } - } - - TsEtsIrUnknownCallModel( - id = id, - target = target, - artifact = artifact, - domainGuard = domainGuard, - ) - } - - override val additionalSceneFiles get() = model.additionalSceneFiles - - override fun apply(state: TsState, call: TsUnknownCall) = model.apply(state, call) - - override fun materializeForMachine( - materializedFiles: IdentityHashMap, - ): TsUnknownCallModel = model.materializeForMachine(materializedFiles) -} 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 new file mode 100644 index 0000000000..74e953913f --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -0,0 +1,413 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.expr.KFp64Value +import io.ksmt.utils.asExpr +import io.ksmt.utils.cast +import org.jacodb.ets.model.EtsStringType +import org.usvm.UExpr +import org.usvm.api.evalTypeEquals +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.mkStringBackingElementLValue +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue +import org.usvm.util.stringFromCodeUnit + +/** Built-in String algorithms implemented by ordinary TypeScript bodies. */ +internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { + private const val CLASS_NAME = "StringModels" + private const val PRIMITIVES_CLASS_NAME = "StringModelPrimitives" + private const val RESOURCE_NAME = "/org/usvm/machine/call/models/StringModels.ts" + + private val baseArtifact by lazy { + loadBundledEtsIrUnknownCallModelArtifact( + resourceName = RESOURCE_NAME, + sourceFileName = "StringModels.ts", + entryPointClassName = CLASS_NAME, + entryPointMethodName = "charAt", + ) + } + + private val primitiveClassSignature by lazy { + baseArtifact.file.allClasses.single { it.name == PRIMITIVES_CLASS_NAME }.signature + } + + private val optionalIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 1) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val index = inputs.getOrNull(1) + + when { + index == null || index == state.ctx.mkUndefinedValue() -> inputs.take(1) + state.ctx.mkFp64(0.0) + index.sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + + private val optionalPositionAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val search = inputs.getOrNull(1) + if (search?.sort != state.ctx.addressSort) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + val position = inputs.getOrNull(2) + when { + position == null || position == state.ctx.mkUndefinedValue() -> inputs.take(2) + state.ctx.mkFp64(0.0) + position.sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + + private val optionalEndPositionAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val search = inputs.getOrNull(1) + if (search?.sort != state.ctx.addressSort) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + val position = inputs.getOrNull(2) + when { + position == null || position == state.ctx.mkUndefinedValue() -> { + inputs.take(2) + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) + } + + position.sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + + private val sliceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val receiver = inputs.firstOrNull()?.takeIf { it.sort == state.ctx.addressSort } + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = inputs.drop(1) + val hasUnsupportedArgument = arguments.any { value -> + value != state.ctx.mkUndefinedValue() && value.sort != state.ctx.fp64Sort + } + if (hasUnsupportedArgument) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + fun numericOrDefault(index: Int, default: UExpr<*>): UExpr<*> { + val value = arguments.getOrNull(index) ?: return default + return if (value == state.ctx.mkUndefinedValue()) default else value + } + + val start = numericOrDefault(index = 0, default = state.ctx.mkFp64(0.0)) + val end = numericOrDefault( + index = 1, + default = state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort), + ) + + listOf(receiver, start, end) + } + + private val receiverOnlyAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + call.resolvedInstanceInputs(maxArgumentCount = 0) + } + + private fun stringDomain(state: TsState, input: UExpr<*>?): org.usvm.UBoolExpr = with(state.ctx) { + if (input == null || input.sort != addressSort) { + return falseExpr + } + + val receiver = input.asExpr(addressSort) + val hasBacking = receiver in state.boundedStringBackingRefs && !receiver.hasFakeValueBranch() + if (!hasBacking) { + return falseExpr + } + + state.memory.types.evalTypeEquals(receiver, EtsStringType) + } + + private val receiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + stringDomain(state = state, input = inputs.firstOrNull()) + } + + private val receiverAndSearchDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + val receiverGuard = stringDomain(state = state, input = inputs.getOrNull(0)) + val searchGuard = stringDomain(state = state, input = inputs.getOrNull(1)) + + state.ctx.mkAnd(receiverGuard, searchGuard) + } + + private val asciiReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiverGuard = receiverDomain.evaluate(state, call, inputs) + if (receiverGuard == falseExpr) { + return@TsEtsIrUnknownCallModelDomainGuard falseExpr + } + + val receiver = inputs.first().asExpr(addressSort) + val characters = state.memory.read(mkStringBackingLValue(receiver)) + .asExpr(addressSort) + val length = state.memory.read(mkStringBackingLengthLValue(characters)) + val characterGuards = (0 until MAX_ASCII_CASE_LENGTH).map { index -> + val symbolicIndex = mkBv(index) + val codeUnit = state.memory.read( + mkStringBackingElementLValue(ref = characters, index = symbolicIndex) + ) + val isOutsideLength = mkBvSignedGreaterOrEqualExpr(symbolicIndex, length) + val asciiMax = mkBv(ASCII_MAX_CODE_UNIT, bv16Sort) + val isAscii = mkBvUnsignedLessOrEqualExpr(codeUnit, asciiMax) + mkOr( + isOutsideLength, + isAscii, + ) + } + + val maximumLength = mkBv(MAX_ASCII_CASE_LENGTH) + val withinLengthLimit = mkBvSignedLessOrEqualExpr(length, maximumLength) + mkAnd( + receiverGuard, + withinLengthLimit, + *characterGuards.toTypedArray(), + ) + } + } + + override val models: List by lazy { + listOf( + sourceModel( + id = "ts.string.charAt", + methodName = "charAt", + inputAdapter = optionalIndexAdapter, + domainGuard = receiverDomain, + ), + sourceModel( + id = "ts.string.indexOf", + methodName = "indexOf", + inputAdapter = optionalPositionAdapter, + domainGuard = receiverAndSearchDomain, + ), + sourceModel( + id = "ts.string.includes", + methodName = "includes", + inputAdapter = optionalPositionAdapter, + domainGuard = receiverAndSearchDomain, + ), + sourceModel( + id = "ts.string.charCodeAt", + methodName = "charCodeAt", + inputAdapter = optionalIndexAdapter, + domainGuard = receiverDomain, + ), + sourceModel( + id = "ts.string.startsWith", + methodName = "startsWith", + inputAdapter = optionalPositionAdapter, + domainGuard = receiverAndSearchDomain, + ), + sourceModel( + id = "ts.string.endsWith", + methodName = "endsWith", + inputAdapter = optionalEndPositionAdapter, + domainGuard = receiverAndSearchDomain, + ), + sourceModel( + id = "ts.string.lastIndexOf", + methodName = "lastIndexOf", + inputAdapter = optionalEndPositionAdapter, + domainGuard = receiverAndSearchDomain, + ), + sourceModel( + id = "ts.string.slice", + methodName = "slice", + inputAdapter = sliceAdapter, + domainGuard = receiverDomain, + ), + sourceModel( + id = "ts.string.toUpperCase", + methodName = "toUpperCase", + inputAdapter = receiverOnlyAdapter, + domainGuard = asciiReceiverDomain, + ), + sourceModel( + id = "ts.string.toLowerCase", + methodName = "toLowerCase", + inputAdapter = receiverOnlyAdapter, + domainGuard = asciiReceiverDomain, + ), + primitiveModel( + methodName = "codeUnitAt", + arity = 2, + implementation = ::stringCodeUnitAt, + ), + primitiveModel( + methodName = "fromCodeUnit", + arity = 1, + implementation = ::stringFromCodeUnit, + ), + ) + } + + private fun sourceModel( + id: String, + methodName: String, + inputAdapter: TsEtsIrUnknownCallModelInputAdapter, + domainGuard: TsEtsIrUnknownCallModelDomainGuard, + ): TsUnknownCallModel = TsEtsIrUnknownCallModel( + id = id, + target = TsUnknownCallTarget( + methodName = methodName, + enclosingClassName = "String", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ), + artifact = artifact(methodName), + domainGuard = domainGuard, + inputAdapter = inputAdapter, + requiredModelIds = buildSet { + val convertsCase = methodName in setOf("toUpperCase", "toLowerCase") + if (convertsCase) { + add(PRIMITIVE_CODE_UNIT_AT_ID) + add(PRIMITIVE_FROM_CODE_UNIT_ID) + } else { + add(MATH_FLOOR_MODEL_ID) + if (methodName == "charCodeAt") { + add(PRIMITIVE_CODE_UNIT_AT_ID) + } + } + }, + ) + + private fun artifact(methodName: String): TsEtsIrUnknownCallModelArtifact { + val artifact = baseArtifact + val entryPoint = artifact.file.allClasses + .single { it.name == CLASS_NAME } + .methods + .single { it.name == methodName } + + return artifact.copy(entryPoint = entryPoint) + } + + private fun primitiveModel( + methodName: String, + arity: Int, + implementation: (TsState, List>) -> TsUnknownCallModelExecution?, + ): TsUnknownCallModel = StringPrimitiveModel( + methodName = methodName, + arity = arity, + implementation = implementation, + ) + + private fun stringCodeUnitAt( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val receiver = inputs.getOrNull(0)?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null + val fpIndex = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + if (receiver.hasFakeValueBranch()) { + return null + } + + val index = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = fpIndex, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val characters = state.memory.read(mkStringBackingLValue(receiver)) + val codeUnit = state.memory.read( + mkStringBackingElementLValue(ref = characters, index = index) + ) + val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType) + val result = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = codeUnit.cast(), + signed = false, + ) + + singleSuccessor( + state = state, + guard = receiverIsString, + result = result, + ) + } + + private fun stringFromCodeUnit( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val code = inputs.singleOrNull()?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val successor = TsUnknownCallModelSuccessor( + guard = trueExpr, + completion = TsUnknownCallModelCompletion.Normal { + if (code is KFp64Value) { + mkInitializedStringConstant(code.value.toInt().toChar().toString()) + } else { + stringFromCodeUnit(code) + } + }, + ) + + TsUnknownCallModelExecution( + successors = listOf(successor), + ) + } + + private fun singleSuccessor( + state: TsState, + guard: org.usvm.UBoolExpr, + result: UExpr<*>, + ): TsUnknownCallModelExecution { + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.Normal { result }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = guard.takeUnless { it == state.ctx.trueExpr }?.let(state.ctx::mkNot), + ) + } + + private class StringPrimitiveModel( + methodName: String, + private val arity: Int, + private val implementation: (TsState, List>) -> TsUnknownCallModelExecution?, + ) : TsUnknownCallModel { + override val id: String = "ts.string.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 PRIMITIVE_CODE_UNIT_AT_ID = "ts.string.primitive.codeUnitAt" + private const val PRIMITIVE_FROM_CODE_UNIT_ID = "ts.string.primitive.fromCodeUnit" + private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" + private const val MAX_ASCII_CASE_LENGTH = 16 + private const val ASCII_MAX_CODE_UNIT = 0x7f +} 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 dcbe25f78a..5ea7ca9200 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 @@ -7,6 +7,7 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsInstanceCallExpr import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UBoolExpr @@ -194,14 +195,14 @@ internal fun TsExprResolver.tryApproximateInstanceCall( return handleArrayConcat(stmt, instanceType, array) } - // Handle `Array.indexOf() method calls - if (expr.callee.name == "indexOf") { - return from(handleArrayIndexOf(expr, instanceType, elementSort, array)) + // Handle Array search and indexed access method calls. + if (expr.callee.name in setOf("indexOf", "lastIndexOf")) { + return handleArrayIndexSearchCall(stmt, instanceType, elementSort, array) } // Handle `Array.includes() method calls if (expr.callee.name == "includes") { - return from(handleArrayIncludes(expr)) + return handleArrayIncludesCall(stmt) } // Handle `Array.reverse() method calls @@ -210,9 +211,86 @@ internal fun TsExprResolver.tryApproximateInstanceCall( } } + val modeledStringMethods = setOf( + "charAt", + "charCodeAt", + "endsWith", + "includes", + "indexOf", + "lastIndexOf", + "slice", + "startsWith", + "toLowerCase", + "toUpperCase", + ) + if (instanceType is EtsStringType && expr.callee.name in modeledStringMethods) { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + return TsExprApproximationResult.NoApproximation + } + + dispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + callee = stmt.call.callee.withEnclosingClassName("String"), + resolvedReceiver = stmt.instance, + resolvedArguments = stmt.args, + ) + + return TsExprApproximationResult.ResolveFailure + } + return TsExprApproximationResult.NoApproximation } +private fun TsExprResolver.handleArrayIndexSearchCall( + stmt: TsVirtualMethodCallStmt, + instanceType: EtsArrayType, + elementSort: USort, + array: UHeapRef, +): TsExprApproximationResult { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + if (stmt.call.callee.name != "indexOf") { + return TsExprApproximationResult.NoApproximation + } + + return from(handleArrayIndexOf(stmt.call, instanceType, elementSort, array)) + } + + dispatchArrayModel(stmt) + return TsExprApproximationResult.ResolveFailure +} + +private fun TsExprResolver.handleArrayIncludesCall( + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + return from(handleArrayIncludes(stmt.call)) + } + + dispatchArrayModel(stmt) + return TsExprApproximationResult.ResolveFailure +} + +private fun TsExprResolver.dispatchArrayModel(stmt: TsVirtualMethodCallStmt) { + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + callee = stmt.call.callee.withEnclosingClassName("Array"), + resolvedReceiver = stmt.instance, + resolvedArguments = stmt.args, + ) +} + +private fun EtsMethodSignature.withEnclosingClassName(name: String): EtsMethodSignature = + copy(enclosingClass = enclosingClass.copy(name = name)) + private fun TsExprResolver.handleArrayPopCall( stmt: TsVirtualMethodCallStmt, instanceType: EtsArrayType, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt index 2e80d17661..1f26ff0cb7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt @@ -13,6 +13,7 @@ import org.jacodb.ets.model.EtsLValue import org.jacodb.ets.model.EtsNumberConstant import org.jacodb.ets.model.EtsPropertyRef import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnknownType import org.usvm.UConcreteHeapRef @@ -43,11 +44,9 @@ internal fun TsExprResolver.handleAssignToProperty(value: EtsPropertyRef, expr: internal fun TsExprResolver.normalizePropertyRef(value: EtsPropertyRef): EtsLValue? = with(ctx) { var key = resolve(value.key) ?: return null if (key.isFakeObject()) { - scope.assert(key.getFakeType(scope).refTypeExpr) ?: return null - key = key.extractRef(scope) + key = key.extractSingleValueFromFakeObjectOrNull(scope) + ?: throw UnsupportedOperationException("Property access needs a resolved key: ${value.key}") } - val name = (key as? UConcreteHeapRef)?.let(::getStringConstantValue) - ?: throw UnsupportedOperationException("Property access needs a constant converted key: ${value.key}") val receiver = resolve(value.instance) ?: return null val rawReference = if (receiver.isFakeObject()) { @@ -60,6 +59,21 @@ internal fun TsExprResolver.normalizePropertyRef(value: EtsPropertyRef): EtsLVal // Storage selection must inspect each feasible reference produced by a guarded property write. val reference = resolveHeapRef(scope, rawReference) ?: return null val storageType = scope.calcOnState { arrayStorageType(reference, value.instance.type) } + if (storageType == EtsStringType && key.sort == fp64Sort) { + return EtsArrayAccess(array = value.instance, index = value.key, type = value.type) + } + + val name = (key as? UConcreteHeapRef)?.let(::getStringConstantValue) + ?: throw UnsupportedOperationException("Property access needs a constant converted key: ${value.key}") + if (storageType == EtsStringType && name != "length") { + val number = name.toDoubleOrNull() + ?: throw UnsupportedOperationException("Unsupported string property: $name") + val isCanonicalIndex = number.isFinite() && number >= 0.0 && number.toEcmaScriptString() == name + val index = if (isCanonicalIndex) number else Double.NaN + + return EtsArrayAccess(array = value.instance, index = EtsNumberConstant(index), type = value.type) + } + if (storageType is EtsArrayType) { val index = name.toIntOrNull()?.takeIf { it >= 0 && it.toString() == name } ?: throw UnsupportedOperationException("Unsupported array property: $name") @@ -69,6 +83,7 @@ internal fun TsExprResolver.normalizePropertyRef(value: EtsPropertyRef): EtsLVal val owner = when (storageType) { is EtsClassType -> storageType.signature is EtsUnclearRefType, EtsUnknownType, EtsAnyType -> EtsClassSignature.UNKNOWN + EtsStringType -> EtsClassSignature.UNKNOWN else -> throw UnsupportedOperationException("Property access needs a modeled object: ${value.instance}") } val field = EtsFieldSignature(enclosingClass = owner, name = name, type = value.type) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index 5e07a39ab8..89c117138e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -6,6 +6,7 @@ import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef @@ -49,6 +50,10 @@ internal fun TsExprResolver.handleArrayAccess( // Resolve the index. val resolvedIndex = resolve(value.index) ?: return null val receiverType = scope.calcOnState { arrayStorageType(array, value.array.type) } + if (receiverType == EtsStringType) { + return readStringIndex(receiver = array, index = resolvedIndex) + } + val propertyName = concreteStringValue(resolvedIndex) if (propertyName != null && receiverType !is EtsArrayType) { val field = EtsFieldSignature( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 5f491b230a..7edb730e7a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -410,7 +410,7 @@ private fun TsContext.materializeTypedStringField( val activeStringConstraints = mkImplies(activeGuard, constraints) scope.assert(activeStringConstraints) ?: return null - scope.doWithState { boundedStringBackingRefs += stringRef } + scope.doWithState { boundedStringBackingRefs += stringRef to maxStringLength } return stringRef } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index 918e39f15c..ad126e10d3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -18,8 +18,7 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue -import org.usvm.util.mkStringBackingLValue -import org.usvm.util.mkStringBackingLengthLValue +import org.usvm.util.stringLength // Handles reading the `length` property. fun TsContext.readLengthProperty( @@ -31,6 +30,19 @@ fun TsContext.readLengthProperty( ): UExpr<*>? { // Determine the array type. val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } + if (storageType is EtsStringType) { + val length = scope.calcOnState { stringLength(instance) } + val lengthBound = scope.calcOnState { boundedStringBackingRefs[instance] ?: maxArraySize } + ensureLengthBounds(scope, length, lengthBound) ?: return null + + return mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = length.asExpr(sizeSort), + signed = true, + ) + } + val arrayType: EtsArrayType = when (val type = storageType) { is EtsArrayType -> type @@ -40,18 +52,6 @@ fun TsContext.readLengthProperty( EtsArrayType(EtsUnknownType, dimensions = 1) } - is EtsStringType -> { - val charsRef = scope.calcOnState { - memory.read(mkStringBackingLValue(instance)) - } - - return readArrayLength( - scope = scope, - lengthLValue = mkStringBackingLengthLValue(charsRef), - maxArraySize = maxArraySize, - ) - } - else -> { val reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE val detail = "Length read requires supported array storage: static=${instanceLocal.type}, storage=$type" diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadString.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadString.kt new file mode 100644 index 0000000000..7dd5fd0257 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadString.kt @@ -0,0 +1,64 @@ +package org.usvm.machine.expr + +import io.ksmt.expr.KBitVec16Value +import io.ksmt.expr.KFpRoundingMode +import io.ksmt.utils.asExpr +import io.ksmt.utils.cast +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.isFalse +import org.usvm.sizeSort +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.stringCharacters +import org.usvm.util.stringFromUtf16CodeUnit +import org.usvm.util.stringLength + +/** String indexing reads one UTF-16 code unit, or undefined for every non-index property number. */ +internal fun TsExprResolver.readStringIndex(receiver: UHeapRef, index: UExpr<*>): UExpr<*>? = with(ctx) { + require(index.sort == fp64Sort) { "String indexing needs a numeric property key" } + + val lengthBound = scope.calcOnState { boundedStringBackingRefs[receiver] } + ?: throw UnsupportedOperationException("String indexing needs modeled backing for $receiver") + val length = scope.calcOnState { stringLength(receiver) } + ensureLengthBounds(scope = scope, length = length, maxLength = lengthBound) ?: return null + + val number = index.asExpr(fp64Sort) + val integer = mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), + value = number, + ) + val fpLength = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = length.cast(), + signed = true, + ) + val zero = mkFp64(0.0) + val isIndex = mkAnd( + mkFpEqualExpr(number, integer), + mkFpGreaterOrEqualExpr(number, zero), + mkFpLessExpr(number, fpLength), + ) + if (isIndex.isFalse) { + return mkUndefinedValue() + } + + val position = mkFpToBvExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), + value = number, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val character = scope.calcOnState { + val characters = stringCharacters(receiver) + val codeUnit = memory.read(mkStringBackingElementLValue(ref = characters, index = position)) + + if (codeUnit is KBitVec16Value) { + mkInitializedStringConstant(codeUnit.shortValue.toInt().toChar().toString()) + } else { + stringFromUtf16CodeUnit(codeUnit) + } + } + + mkIte(isIndex, character, mkUndefinedValue()) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 419d1aeaf2..5b60f64c3e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -342,6 +342,12 @@ class TsExprResolver( else -> throw UnsupportedOperationException("Symbolic property key conversion: ${expr.arg}") } } + // Keep a symbolic numeric key in numeric form until the property read. String indexing can then + // test canonical integer positions directly; object properties still require a concrete string key. + if (value.sort == fp64Sort && value !is KFp64Value) { + return value + } + val key = concreteStringValue(value) ?: throw UnsupportedOperationException("Unmodeled property key conversion: ${expr.arg}") mkStringConstant(key, scope) @@ -804,7 +810,7 @@ class TsExprResolver( guard = trueExpr, ) memory.write(mkStringBackingLengthLValue(resultChars), resultLength, guard = trueExpr) - boundedStringBackingRefs += result + boundedStringBackingRefs += result to options.maxArraySize memory.memcpy( srcRef = leftChars, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index 2b728f86a6..e963032393 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef @@ -40,6 +41,10 @@ internal fun TsExprResolver.handleAssignToArrayIndex( // Resolve the index. val resolvedIndex = resolve(lhv.index) ?: return null val receiverType = scope.calcOnState { arrayStorageType(array, lhv.array.type) } + if (receiverType == EtsStringType) { + throw UnsupportedOperationException("Writes to string indexes are not modeled") + } + val propertyName = concreteStringValue(resolvedIndex) if (propertyName != null && receiverType !is EtsArrayType) { val field = EtsFieldSignature( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 048df55899..858ec044a3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -783,7 +783,10 @@ class TsInterpreter( observer = observer, ) - fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { + fun getInitialState( + method: EtsMethod, + targets: List, + ): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -811,7 +814,6 @@ class TsInterpreter( method.parameters.forEachIndexed { i, param -> val idx = i + 1 // +1 because 0 is reserved for `this` - val ref by lazy { val lValue = mkRegisterStackLValue(addressSort, idx) state.memory.read(lValue).asExpr(addressSort) @@ -859,7 +861,7 @@ class TsInterpreter( state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) state.pathConstraints += state.symbolicStringBackingConstraint(ref) - state.boundedStringBackingRefs += ref + state.boundedStringBackingRefs += ref to state.maxStringLength } val parameterSort = typeToSort(parameterType) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 3a9ef594eb..5b6842bffe 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -86,7 +86,10 @@ private fun TsContext.stringValueEquals( rhsChars = rhsChars, lhsLength = lhsLength, rhsLength = rhsLength, - maxLength = maxStringLength, + maxLength = maxOf( + boundedStringBackingRefs[lhs] ?: maxStringLength, + boundedStringBackingRefs[rhs] ?: maxStringLength, + ), ) } @@ -119,7 +122,7 @@ private fun TsContext.stringValueEquals( boundedLengths, ) scope.fork(supported, blockOnFalseState = { - terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..$maxStringLength") + terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..${comparison.maxLength}") }) ?: return null // Known literals supply a tighter comparison bound; all other string lengths are constrained above. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 29056d7dfe..89e5b4064b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -87,11 +87,11 @@ class TsState( */ var stringConstantAllocatedRefs: UPersistentHashMap = persistentHashMapOf(), /** - * References whose string backing and length bound have been modeled. + * Maps references with modeled string backing to their maximum length. * A new symbolic string producer must register its reference here after creating the backing model. * String literals are recognized separately through [TsContext.getStringConstantValue]. */ - var boundedStringBackingRefs: Set = emptySet(), + var boundedStringBackingRefs: Map = emptyMap(), /** Unresolved reference payloads that may acquire string backing after type refinement. */ var symbolicStringCandidates: Set = emptySet(), /** Exception delivered to the current catch block, before its binding is initialized. */ @@ -300,6 +300,7 @@ class TsState( ref } stringConstantAllocatedRefs = updated + boundedStringBackingRefs += result to value.length result } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt index 55a87920ed..91b181f1b4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt @@ -70,7 +70,7 @@ internal fun TsStepScope.prepareRefinedStringBackings(): Unit? { val backingConstraint = calcOnState { symbolicStringBackingConstraint(ref) } assert(backingConstraint) ?: return null doWithState { - boundedStringBackingRefs += ref + boundedStringBackingRefs += ref to maxStringLength symbolicStringCandidates -= ref } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt new file mode 100644 index 0000000000..f6c3255b5d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt @@ -0,0 +1,70 @@ +package org.usvm.util + +import io.ksmt.sort.KBv16Sort +import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.initializeArrayLength +import org.usvm.machine.TsSizeSort +import org.usvm.machine.state.TsState +import org.usvm.sizeSort + +private val STRING_CHARACTER_ARRAY_TYPE = EtsArrayType(EtsNumberType, dimensions = 1) + +internal fun TsState.stringCharacters(receiver: UHeapRef): UHeapRef = with(ctx) { + memory.read(mkStringBackingLValue(receiver)).asExpr(addressSort) +} + +internal fun TsState.stringLength(receiver: UHeapRef): UExpr { + val characters = stringCharacters(receiver) + return memory.read(mkStringBackingLengthLValue(characters)) +} + +private fun TsState.allocateString( + length: UExpr, + maxLength: Int, +): Pair = with(ctx) { + val string = memory.allocConcrete(EtsStringType) + val characters = memory.allocConcrete(STRING_CHARACTER_ARRAY_TYPE.elementType) + memory.initializeArrayLength( + arrayHeapRef = characters, + type = stringBackingArrayDescriptor, + sizeSort = sizeSort, + count = length, + ) + memory.write( + mkStringBackingLValue(string), + characters, + guard = trueExpr, + ) + boundedStringBackingRefs += string to maxLength + + string to characters +} + +internal fun TsState.stringFromCodeUnit(codeUnit: UExpr): UConcreteHeapRef = with(ctx) { + val value = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = codeUnit, + bvSize = bv16Sort.sizeBits.toInt(), + isSigned = false, + ).asExpr(bv16Sort) + + stringFromUtf16CodeUnit(value) +} + +internal fun TsState.stringFromUtf16CodeUnit(codeUnit: UExpr): UConcreteHeapRef = with(ctx) { + val (result, characters) = allocateString(length = mkBv(1), maxLength = 1) + val character = mkStringBackingElementLValue(ref = characters, index = mkBv(0)) + memory.write( + character, + codeUnit, + guard = trueExpr, + ) + result +} 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 0e22541d97..08daef0bae 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 @@ -9,4 +9,105 @@ export class ArrayModels { receiver.length = length - 1; return result; } + + static indexOf(receiver: any[], searchElement: any, fromIndex: number): number { + const length = receiver.length; + if (length === 0) { + return -1; + } + + const start = ArrayModels.normalizeRelativeIndex(fromIndex, length); + if (start === Infinity || start >= length) { + return -1; + } + + let index = start >= 0 ? start : length + start; + if (index < 0) { + index = 0; + } + + while (index < length) { + if (receiver[index] === searchElement) { + return index; + } + + index++; + } + + return -1; + } + + static includes(receiver: any[], searchElement: any, fromIndex: number): boolean { + const length = receiver.length; + if (length === 0) { + return false; + } + + const start = ArrayModels.normalizeRelativeIndex(fromIndex, length); + if (start === Infinity || start >= length) { + return false; + } + + let index = start >= 0 ? start : length + start; + if (index < 0) { + index = 0; + } + + while (index < length) { + const element = receiver[index]; + if (element === searchElement || (element !== element && searchElement !== searchElement)) { + return true; + } + + index++; + } + + return false; + } + + static lastIndexOf(receiver: any[], searchElement: any, fromIndex: number): number { + const length = receiver.length; + if (length === 0 || fromIndex === -Infinity) { + return -1; + } + + let start = fromIndex !== fromIndex ? 0 : fromIndex; + if (start !== Infinity) { + start = start < 0 ? -Math.floor(-start) : Math.floor(start); + if (start === 0) { + start = 0; + } + } + if (start < -length) { + return -1; + } + + let index = start >= length ? length - 1 : (start >= 0 ? start : length + start); + while (index >= 0) { + if (receiver[index] === searchElement) { + return index; + } + + index--; + } + + return -1; + } + + private static normalizeRelativeIndex(fromIndex: number, length: number): number { + if (fromIndex !== fromIndex) { + return 0; + } + + if (fromIndex === Infinity || fromIndex >= length) { + return length; + } + + if (fromIndex === -Infinity || fromIndex <= -length) { + return -length; + } + + const integer = fromIndex < 0 ? -Math.floor(-fromIndex) : Math.floor(fromIndex); + return integer === 0 ? 0 : 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 new file mode 100644 index 0000000000..858bbd6035 --- /dev/null +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -0,0 +1,248 @@ +declare class StringModelPrimitives { + static codeUnitAt(receiver: string, index: number): number; + static fromCodeUnit(codeUnit: number): string; +} + +export class StringModels { + static charAt(receiver: string, index: number): string { + const length = receiver.length; + const integerIndex = StringModels.normalizeCharIndex(index, length); + if (integerIndex < 0 || integerIndex >= length) { + return ""; + } + + return receiver[integerIndex]; + } + + static indexOf(receiver: string, searchString: string, position: number): number { + const length = receiver.length; + const searchLength = searchString.length; + const start = StringModels.normalizePosition(position, length); + + if (searchLength === 0) { + return start; + } + + let index = start; + while (index + searchLength <= length) { + let searchIndex = 0; + while (searchIndex < searchLength) { + const character = receiver[index + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { + break; + } + + searchIndex++; + } + + if (searchIndex === searchLength) { + return index; + } + + index++; + } + + return -1; + } + + static includes(receiver: string, searchString: string, position: number): boolean { + return StringModels.indexOf(receiver, searchString, position) !== -1; + } + + static charCodeAt(receiver: string, index: number): number { + const length = receiver.length; + const integerIndex = StringModels.normalizeCharIndex(index, length); + if (integerIndex < 0 || integerIndex >= length) { + return NaN; + } + + return StringModelPrimitives.codeUnitAt(receiver, integerIndex); + } + + static slice(receiver: string, start: number, end: number): string { + const length = receiver.length; + const from = StringModels.normalizeSliceIndex(start, length); + const to = StringModels.normalizeSliceIndex(end, length); + + let result = ""; + let index = from; + while (index < to) { + result += receiver[index]; + index++; + } + + return result; + } + + static toUpperCase(receiver: string): string { + const length = receiver.length; + let result = ""; + let index = 0; + while (index < length) { + let codeUnit = StringModelPrimitives.codeUnitAt(receiver, index); + if (codeUnit >= 0x61 && codeUnit <= 0x7a) { + codeUnit -= 0x20; + } + result += StringModelPrimitives.fromCodeUnit(codeUnit); + index++; + } + return result; + } + + static toLowerCase(receiver: string): string { + const length = receiver.length; + let result = ""; + let index = 0; + while (index < length) { + let codeUnit = StringModelPrimitives.codeUnitAt(receiver, index); + if (codeUnit >= 0x41 && codeUnit <= 0x5a) { + codeUnit += 0x20; + } + result += StringModelPrimitives.fromCodeUnit(codeUnit); + index++; + } + return result; + } + + static startsWith(receiver: string, searchString: string, position: number): boolean { + const length = receiver.length; + const searchLength = searchString.length; + const start = StringModels.normalizePosition(position, length); + if (start + searchLength > length) { + return false; + } + + let searchIndex = 0; + while (searchIndex < searchLength) { + const character = receiver[start + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { + return false; + } + + searchIndex++; + } + + return true; + } + + static endsWith(receiver: string, searchString: string, endPosition: number): boolean { + const length = receiver.length; + const searchLength = searchString.length; + const end = StringModels.normalizePosition(endPosition, length); + const start = end - searchLength; + if (start < 0) { + return false; + } + + let searchIndex = 0; + while (searchIndex < searchLength) { + const character = receiver[start + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { + return false; + } + + searchIndex++; + } + + return true; + } + + static lastIndexOf(receiver: string, searchString: string, position: number): number { + const length = receiver.length; + const searchLength = searchString.length; + let index = StringModels.normalizeLastPosition(position, length); + if (index + searchLength > length) { + index = length - searchLength; + } + + while (index >= 0) { + let searchIndex = 0; + while (searchIndex < searchLength) { + const character = receiver[index + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { + break; + } + + searchIndex++; + } + + if (searchIndex === searchLength) { + return index; + } + + index--; + } + + return -1; + } + + private static normalizeCharIndex(value: number, length: number): number { + if (value !== value) { + return 0; + } + + if (value === Infinity || value >= length) { + return length; + } + + if (value === -Infinity || value <= -length) { + return -length; + } + + return value < 0 ? -Math.floor(-value) : Math.floor(value); + } + + private static normalizePosition(value: number, length: number): number { + if (value !== value) { + return 0; + } + + if (value === Infinity || value >= length) { + return length; + } + + if (value === -Infinity || value <= 0) { + return 0; + } + + return Math.floor(value); + } + + private static normalizeLastPosition(value: number, length: number): number { + if (value !== value || value === Infinity || value >= length) { + return length; + } + + if (value === -Infinity || value <= 0) { + return 0; + } + + return Math.floor(value); + } + + private static normalizeSliceIndex(value: number, length: number): number { + if (value !== value) { + return 0; + } + if (value === Infinity) { + return length; + } + if (value === -Infinity) { + return 0; + } + + const integer = value < 0 ? -Math.floor(-value) : Math.floor(value); + if (integer < 0) { + return integer + length < 0 ? 0 : integer + length; + } + return integer > length ? length : integer; + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt new file mode 100644 index 0000000000..a37aa0cfca --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt @@ -0,0 +1,255 @@ +package org.usvm.machine + +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.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class TsStringIndexingTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/StringIndexing.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions(maxArraySize = 4) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + val analysis = machine.analyzeWithOutcome(listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), "${method.name}: ${analysis.unsupportedPaths}") + analysis.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `indexed reads preserve isolated surrogate units`() { + discoverProperties( + method = method("indexedReadEquals"), + { value -> value.value }, + invariants = arrayOf({ value -> value.value }), + ) + } + + @Test + fun `out of range string index yields undefined`() { + discoverProperties( + method = method("outOfRangeIndex"), + { value -> value.value }, + invariants = arrayOf({ value -> value.value }), + ) + } + + @Test + fun `indexing reads individual UTF-16 code units`() { + discoverProperties( + method = method("literalUtf16"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `invalid numeric indexes return undefined without truncation or wrapping`() { + discoverProperties( + method = method("invalidIndexes"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `string property keys use canonical indexes`() { + discoverProperties( + method = method("stringKeys"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `symbolic numeric indexing explores characters and undefined`() { + discoverProperties( + method = method("symbolicIndex"), + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 2.0 }, + { _, result -> result.number == 3.0 }, + invariants = arrayOf({ index, result -> + val number = index.number + val isIndex = number.isFinite() && number >= 0.0 && number < 3.0 && number % 1.0 == 0.0 + val expected = if (isIndex) { + if ("aba"[number.toInt()] == 'a') 1.0 else 2.0 + } else { + 3.0 + } + + result.number == expected + }), + ) + } + + @Test + fun `symbolic string indexing preserves empty match and nonmatch branches`() { + discoverProperties( + method = method("symbolicString"), + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 2.0 }, + invariants = arrayOf({ input, result -> + val expected = when { + input.value.isEmpty() -> 0.0 + input.value.first() == 'a' -> 1.0 + else -> 2.0 + } + + result.number == expected + }), + ) + } + + @Test + fun `charAt supports symbolic strings and positions`() { + discoverProperties( + method = method("symbolicCharAt"), + { _, _, result -> result.number == 0.0 }, + { _, _, result -> result.number == 1.0 }, + { _, _, result -> result.number == 2.0 }, + invariants = arrayOf({ input, index, result -> + val integer = if (index.number.isNaN()) 0.0 else index.number.toLong().toDouble() + val character = if (integer >= 0.0 && integer < input.value.length) { + input.value[integer.toInt()].toString() + } else { + "" + } + val expected = if (input.value.length > 2) 0.0 else if (character == "a") 1.0 else 2.0 + + result.number == expected + }), + ) + } + + @Test + fun `slice copies a symbolic code unit through ordinary indexing`() { + discoverProperties( + method = method("symbolicSlice"), + { input, result -> input.value.length == 2 && result.value == input.value.take(1) }, + invariants = arrayOf({ input, result -> + result.value == if (input.value.length == 2) input.value.take(1) else "" + }), + ) + } + + @Test + fun `search reads symbolic receivers and patterns`() { + discoverProperties( + method = method("symbolicSearch"), + { _, result -> result.number == -2.0 }, + { _, result -> result.number == -1.0 }, + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ input, result -> + val expected = if (input.value.length > 2) -2.0 else input.value.indexOf('a').toDouble() + + result.number == expected + }), + ) + + discoverProperties( + method = method("symbolicPattern"), + { _, result -> result.number == -2.0 }, + { _, result -> result.number == -1.0 }, + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ input, result -> + val expected = if (input.value.length > 1) -2.0 else "aba".indexOf(input.value).toDouble() + + result.number == expected + }), + ) + } + + @Test + fun `numeric code unit helpers compose on symbolic ASCII strings`() { + discoverProperties( + method = method("symbolicCase"), + { input, result -> input.value.length == 1 && result.value.length == 2 }, + invariants = arrayOf({ input, result -> + val value = input.value + val isAsciiCharacter = value.length == 1 && value.first().code <= 127 + val expected = if (isAsciiCharacter) { + value.uppercase() + value.lowercase() + } else { + "" + } + + result.value == expected + }), + ) + } + + @Test + fun `generated string indexing and model witnesses replay in JavaScript`() { + val methodNames = listOf( + "symbolicIndex", + "symbolicString", + "symbolicCharAt", + "symbolicSlice", + "symbolicSearch", + "symbolicPattern", + "symbolicCase", + ) + val script = buildString { + appendLine(source.readText()) + for (name in methodNames) { + for (test in runner(method(name), options)) { + val arguments = test.before.parameters.joinToString { value -> jsValue(value) } + val expected = jsValue(test.returnValue) + + appendLine("if (new StringIndexing().$name($arguments) !== $expected) throw Error('$name');") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "string-indexing", + timeoutMessage = "String indexing replay timed out", + failureContext = script.take(1000), + ) + } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "StringIndexing") + + private fun jsValue(value: TsTestValue): String = when (value) { + is TsTestValue.TsString -> jsString(value.value) + else -> assertIs(value).number.toString() + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt index a0ab71d2ab..4c2958418a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt @@ -222,8 +222,11 @@ class TsArrayPopEtsIrModelTest { } @Test - fun `arity mismatch uses fallback`() { - assertUsesResidualFallback(methodName = "popWithArguments") + fun `pop ignores extra arguments`() { + val result = analyze(methodName = "popWithArguments") + + assertEquals(49.0, assertIs(result.values.single()).number) + assertEquals(listOf("ts.array.pop"), result.modelIds) } @Test @@ -275,16 +278,6 @@ class TsArrayPopEtsIrModelTest { } } - private fun assertUsesResidualFallback(methodName: String) { - val result = analyze(methodName) - - assertTrue( - result.values.isEmpty(), - "Expected fallback to stop the path, got values=${result.values}, events=${result.events}", - ) - assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) - } - private fun makeFakeReceiver(state: TsState): UConcreteHeapRef { val result = assertIs(state.methodResult).value val fakeReceiver = assertIs(result) 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 new file mode 100644 index 0000000000..35898cee0e --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt @@ -0,0 +1,452 @@ +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.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsSequenceEtsIrModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/SequenceEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `unrelated codeUnitAt declaration uses residual fallback`() { + val result = analyze(methodName = "unrelatedCodeUnitAtDeclaration") + + assertTrue(result.values.isEmpty()) + assertTrue(result.modelIds.isEmpty()) + assertEquals(TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, result.events.single().failureReason) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.single().outcome) + } + + @Test + fun `unrelated fromCodeUnit declaration uses residual fallback`() { + val result = analyze(methodName = "unrelatedFromCodeUnitDeclaration") + + assertTrue(result.values.isEmpty()) + assertTrue(result.modelIds.isEmpty()) + assertEquals(TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, result.events.single().failureReason) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.single().outcome) + } + + @Test + fun `array pop evaluates ignored arguments before reading the receiver`() { + val result = analyze(methodName = "arrayPopEvaluatesIgnoredArguments") + + assertEquals(32.0, assertIs(result.values.single()).number) + assertTrue("ts.array.pop" in result.modelIds) + } + + @Test + fun `array searches ignore evaluated extras and preserve undefined lastIndexOf semantics`() { + val expectedModels = setOf("ts.array.indexOf", "ts.array.includes", "ts.array.lastIndexOf") + + val result = analyze(methodName = "arraySearchesEvaluateIgnoredArguments") + + assertTrue(assertIs(result.values.single()).value) + assertTrue(expectedModels.all(result.modelIds::contains)) + } + + @Test + fun `string indexes evaluate ignored arguments`() { + val result = analyze(methodName = "stringIndexesEvaluateIgnoredArguments") + + assertTrue(assertIs(result.values.single()).value) + assertTrue(setOf("ts.string.charAt", "ts.string.charCodeAt").all(result.modelIds::contains)) + } + + @Test + fun `string searches evaluate ignored arguments and default undefined positions`() { + val result = analyze(methodName = "stringSearchesEvaluateIgnoredArguments") + val expectedModels = setOf( + "ts.string.indexOf", + "ts.string.includes", + "ts.string.startsWith", + "ts.string.endsWith", + "ts.string.lastIndexOf", + ) + + assertTrue(assertIs(result.values.single()).value) + assertTrue(expectedModels.all(result.modelIds::contains)) + } + + @Test + fun `string slice evaluates ignored arguments`() { + val result = analyze(methodName = "stringSliceEvaluatesIgnoredArguments") + + assertTrue(assertIs(result.values.single()).value) + assertTrue("ts.string.slice" in result.modelIds) + } + + @Test + fun `string case conversion evaluates ignored arguments`() { + val result = analyze(methodName = "stringCaseConversionEvaluatesIgnoredArguments") + + assertTrue(assertIs(result.values.single()).value) + assertTrue(setOf("ts.string.toUpperCase", "ts.string.toLowerCase").all(result.modelIds::contains)) + } + + @Test + fun `array indexOf uses strict equality and offsets`() { + val result = analyze(methodName = "arrayIndexOfUsesStrictEqualityAndOffsets") + + assertEquals(-681.0, assertIs(result.values.single()).number) + assertEquals(listOf("ts.array.indexOf", "ts.math.floor"), result.modelIds.distinct()) + } + + @Test + fun `array includes uses SameValueZero`() { + val result = analyze(methodName = "arrayIncludesUsesSameValueZero") + + assertTrue(assertIs(result.values.single()).value) + assertEquals(listOf("ts.array.includes", "ts.math.floor"), result.modelIds.distinct()) + } + + @Test + fun `typed default searches fall back without array presence metadata`() { + val result = analyze(methodName = "numericDefaultSearchFallsBack") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + } + + @Test + fun `array offsets normalize fractions and NaN`() { + val result = analyze(methodName = "arrayOffsetsAreNormalized") + + assertEquals(131.0, assertIs(result.values.single()).number) + assertEquals(setOf("ts.array.includes", "ts.array.indexOf", "ts.math.floor"), result.modelIds.toSet()) + } + + @Test + fun `empty arrays do not match`() { + val result = analyze(methodName = "emptyArraysDoNotMatch") + + assertTrue(assertIs(result.values.single()).value) + } + + @Test + fun `explicit undefined uses the default array offset`() { + val result = analyze(methodName = "arrayExplicitUndefinedOffset") + + assertEquals(0.0, assertIs(result.values.single()).number) + } + + @Test + fun `array lastIndexOf searches backward from normalized offsets`() { + val result = analyze(methodName = "arrayLastIndexOfHandlesOffsets") + + assertEquals(199.0, assertIs(result.values.single()).number) + assertTrue("ts.array.lastIndexOf" in result.modelIds) + } + + @Test + fun `array lastIndexOf distinguishes omitted and undefined offsets`() { + val result = analyze(methodName = "arrayLastIndexOfExplicitUndefined") + + assertEquals(0.0, assertIs(result.values.single()).number) + } + + @Test + fun `array lastIndexOf stops before indexes below negative length`() { + val result = analyze(methodName = "arrayLastIndexOfBeforeStart") + + assertEquals(-1.0, assertIs(result.values.single()).number) + } + + @Test + fun `array searches canonicalize negative zero results`() { + val result = analyze(methodName = "arraySearchReturnsPositiveZero") + + assertEquals(3.0, assertIs(result.values.single()).number) + } + + @Test + fun `numeric holes do not match zero`() { + val result = analyze(methodName = "numericHoleDoesNotMatchZero") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + } + + @Test + fun `numeric holes reject includes undefined without presence metadata`() { + val result = analyze(methodName = "numericHoleDoesNotIncludeUndefined") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + } + + @Test + fun `symbolic typed-default search uses residual fallback`() { + val result = analyze(methodName = "numericHoleWithSymbolicSearch") + + assertTrue(result.values.isNotEmpty()) + assertTrue(result.values.all { value -> !assertIs(value).value }) + assertTrue(result.events.any { it.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + assertTrue(result.events.any { it.outcome == TsUnknownCallOutcome.PATH_STOPPED }) + } + + @Test + fun `array includes finds explicit undefined`() { + val result = analyze(methodName = "explicitUndefinedArrayIncludesUndefined") + + assertTrue(assertIs(result.values.single()).value) + } + + @Test + fun `array indexOf rejects undefined search when slot presence is unavailable`() { + val result = analyze(methodName = "explicitUndefinedArrayIndexOfUndefined") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + } + + @Test + fun `string charAt handles in-range and out-of-range indexes`() { + val result = analyze(methodName = "stringCharAtHandlesBounds") + + assertEquals("b", assertIs(result.values.single()).value) + assertTrue("ts.string.charAt" in result.modelIds) + assertTrue(result.events.all { it.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `selecting charAt only enables position normalization`() { + val result = analyze( + methodName = "stringCharAtHandlesBounds", + tsOptions = TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf("ts.string.charAt")), + ), + ) + + assertEquals("b", assertIs(result.values.single()).value) + assertEquals( + setOf( + "ts.string.charAt", + "ts.math.floor", + ), + result.modelIds.toSet(), + ) + } + + @Test + fun `string indexOf handles offsets and empty search`() { + val result = analyze(methodName = "stringIndexOfHandlesOffsetsAndEmptySearch") + + assertEquals(330.0, assertIs(result.values.single()).number) + assertTrue("ts.string.indexOf" in result.modelIds) + assertTrue(result.events.all { it.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `string includes handles NaN and infinity positions`() { + val result = analyze(methodName = "stringIncludesHandlesNaNPosition") + + assertTrue(assertIs(result.values.single()).value) + assertTrue("ts.string.includes" in result.modelIds) + assertTrue(result.events.all { it.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `explicit undefined uses default string positions`() { + val result = analyze(methodName = "stringExplicitUndefinedPositions") + + assertEquals(1.0, assertIs(result.values.single()).number) + } + + @Test + fun `symbolic string position explores exact matches`() { + val result = analyze(methodName = "stringSymbolicPosition") + val numbers = result.values.filterIsInstance().map { it.number }.toSet() + + assertTrue(1.0 in numbers, "Expected first match for positions at or before 1: $numbers") + assertTrue(3.0 in numbers, "Expected second match for positions 2 or 3: $numbers") + assertTrue(-1.0 in numbers, "Expected no match after the last occurrence: $numbers") + assertTrue("ts.string.indexOf" in result.modelIds) + } + + @Test + fun `symbolic charAt explores in-range and out-of-range positions`() { + val result = analyze(methodName = "symbolicCharAt") + val values = result.values.map { value -> assertIs(value).value }.toSet() + + assertTrue("" in values) + assertTrue(values.any { value -> value.isNotEmpty() }) + assertTrue(values.all { value -> value in setOf("", "a", "b", "c") }) + assertTrue(result.events.all { event -> event.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `string charCodeAt returns code units and NaN out of bounds`() { + val result = analyze(methodName = "stringCharCodeAtHandlesBounds") + + assertEquals(91.0, assertIs(result.values.single()).number) + assertTrue("ts.string.charCodeAt" in result.modelIds) + } + + @Test + fun `string startsWith and endsWith honor positions`() { + val result = analyze(methodName = "stringStartsAndEndsWithHandlePositions") + + assertTrue(assertIs(result.values.single()).value) + assertTrue(setOf("ts.string.startsWith", "ts.string.endsWith").all(result.modelIds::contains)) + } + + @Test + fun `string lastIndexOf searches backward and matches empty suffix`() { + val result = analyze(methodName = "stringLastIndexOfHandlesPositions") + + assertEquals(315.0, assertIs(result.values.single()).number) + assertTrue("ts.string.lastIndexOf" in result.modelIds) + } + + @Test + fun `string slice copies exact UTF16 code units`() { + 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`() { + 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`() { + 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)) + } + + @Test + fun `ASCII casing leaves non ASCII strings to residual fallback`() { + val result = analyze(methodName = "stringCapitalizeNonAscii") + + assertTrue(result.values.isEmpty()) + assertTrue(result.events.any { event -> event.outcome == TsUnknownCallOutcome.PATH_STOPPED }) + } + + private fun analyze( + methodName: String, + tsOptions: TsOptions = TsOptions(), + ): AnalysisResult { + val method = method(methodName) + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + observer = observer, + ).use { machine -> + val states = machine.analyze(listOf(method)) + val values = states.map { state -> TsTestResolver().resolve(method, state).returnValue } + + AnalysisResult( + values = values, + events = observer.events.toList(), + ) + } + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "SequenceEtsIr" } + .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, + ) { + 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, + stopOnCoverage = 0, + 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/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 4de5a89b20..307ee9d89b 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 @@ -81,6 +81,32 @@ class TsUnknownCallModelCatalogTest { assertEquals("Unknown semantic model IDs: missing", error.message) } + @Test + fun `selection includes transitive model dependencies`() { + val catalog = TsUnknownCallModelCatalog( + models = listOf( + model(id = "entry", requiredModelIds = setOf("helper")), + model(id = "helper", requiredModelIds = setOf("primitive")), + model(id = "primitive"), + model(id = "unrelated"), + ), + selection = TsUnknownCallModelSelection.Only(setOf("entry")), + ) + + assertEquals(listOf("entry", "helper", "primitive"), catalog.modelIds) + } + + @Test + fun `missing model dependency is rejected`() { + val error = assertFailsWith { + TsUnknownCallModelCatalog( + models = listOf(model(id = "entry", requiredModelIds = setOf("missing"))), + ) + } + + assertEquals("Semantic model entry requires unknown model IDs: missing", error.message) + } + @Test fun `selection does not depend on model order`() { val forward = listOf( @@ -152,7 +178,10 @@ class TsUnknownCallModelCatalogTest { val catalog = TsBuiltInUnknownCallModels.catalog() val expectedModelIds = listOf( + "ts.array.includes", + "ts.array.indexOf", "ts.array.isArray", + "ts.array.lastIndexOf", "ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID, TsNumericIntrinsicModelFamily.MATH_ABS_ID, @@ -167,6 +196,18 @@ class TsUnknownCallModelCatalogTest { TsNumericIntrinsicModelFamily.NUMBER_IS_INTEGER_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_NAN_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID, + "ts.string.charAt", + "ts.string.charCodeAt", + "ts.string.endsWith", + "ts.string.includes", + "ts.string.indexOf", + "ts.string.lastIndexOf", + "ts.string.primitive.codeUnitAt", + "ts.string.primitive.fromCodeUnit", + "ts.string.slice", + "ts.string.startsWith", + "ts.string.toLowerCase", + "ts.string.toUpperCase", ) assertEquals(expectedModelIds, catalog.modelIds) @@ -179,6 +220,29 @@ class TsUnknownCallModelCatalogTest { assertTrue(TsBuiltInUnknownCallModels.catalog(TsUnknownCallModelSelection.Only(emptySet())).modelIds.isEmpty()) } + @Test + fun `array and string built in model families are discovered`() { + val modelIds = TsBuiltInUnknownCallModels.catalog().modelIds + val expectedModelIds = listOf( + "ts.array.includes", + "ts.array.indexOf", + "ts.array.lastIndexOf", + "ts.string.charAt", + "ts.string.charCodeAt", + "ts.string.endsWith", + "ts.string.includes", + "ts.string.indexOf", + "ts.string.lastIndexOf", + "ts.string.primitive.codeUnitAt", + "ts.string.primitive.fromCodeUnit", + "ts.string.slice", + "ts.string.startsWith", + "ts.string.toLowerCase", + "ts.string.toUpperCase", + ) + assertTrue(modelIds.containsAll(expectedModelIds)) + } + @Test fun `unmatched call selects no model`() { val catalog = TsUnknownCallModelCatalog(listOf(model(id = "known", methodName = "known"))) @@ -281,6 +345,7 @@ class TsUnknownCallModelCatalogTest { failureReason: TsUnknownCallFailureReason? = null, className: String? = null, additionalSceneFiles: List = emptyList(), + requiredModelIds: Set = emptySet(), ): TsUnknownCallModel = FakeModel( id = id, target = TsUnknownCallTarget( @@ -289,12 +354,14 @@ class TsUnknownCallModelCatalogTest { enclosingClassName = className, ), additionalSceneFiles = additionalSceneFiles, + requiredModelIds = requiredModelIds, ) private class FakeModel( override val id: String, override val target: TsUnknownCallTarget, override val additionalSceneFiles: List = emptyList(), + override val requiredModelIds: Set = emptySet(), ) : TsUnknownCallModel { override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution = error("Fake model must not execute in catalog metadata tests") diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 9dd242ac27..1fee530dff 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -79,6 +79,7 @@ class TsTestResolver { method, resolvedLValuesToFakeObjects, state.maxStringLength, + stringLengthBounds = state.boundedStringBackingRefs, propertyState = state, ) val afterMemoryScope = MemoryScope( @@ -88,6 +89,7 @@ class TsTestResolver { method, resolvedLValuesToFakeObjects, state.maxStringLength, + stringLengthBounds = state.boundedStringBackingRefs, propertyState = state, ) @@ -193,6 +195,7 @@ class TsTestResolver { method: EtsMethod, resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, maxStringLength: Int, + stringLengthBounds: Map, propertyState: TsState, ) : TsTestStateResolver( ctx = ctx, @@ -201,6 +204,7 @@ class TsTestResolver { method = method, resolvedLValuesToFakeObjects = resolvedLValuesToFakeObjects, maxStringLength = maxStringLength, + stringLengthBounds = stringLengthBounds, propertyState = propertyState, ) { fun resolveState(): TsParametersState { @@ -219,6 +223,7 @@ open class TsTestStateResolver( val method: EtsMethod, val resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, val maxStringLength: Int, + private val stringLengthBounds: Map = emptyMap(), private val propertyState: TsState? = null, ) { private val resolvedClasses = hashMapOf() @@ -370,7 +375,8 @@ open class TsTestStateResolver( val lengthLValue = mkStringBackingLengthLValue(charsRef) val length = evaluateInModel(stringMemory.read(lengthLValue)).extractInt() - require(length in 0..maxStringLength) { "Unsupported symbolic string length: $length" } + val lengthBound = stringLengthBounds[heapRef] ?: stringLengthBounds[concreteRef] ?: maxStringLength + require(length in 0..lengthBound) { "Unsupported symbolic string length: $length" } val value = buildString(length) { repeat(length) { index -> diff --git a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts new file mode 100644 index 0000000000..6d1741fb75 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts @@ -0,0 +1,300 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +declare class StringModelPrimitives { + static codeUnitAt(receiver: string, index: number): number; + static fromCodeUnit(codeUnit: number): string; +} + +export class SequenceEtsIr { + unrelatedCodeUnitAtDeclaration(): number { + return StringModelPrimitives.codeUnitAt("AZ", 1); + } + + unrelatedFromCodeUnitDeclaration(): string { + return StringModelPrimitives.fromCodeUnit(65); + } + + arrayPopEvaluatesIgnoredArguments(): number { + const values = [1, 2]; + + const popped = values.pop(values.push(3), { ignored: true }); + + return popped * 10 + values.length; + } + + arraySearchesEvaluateIgnoredArguments(): boolean { + const values = [1, 2, 1]; + const effects: number[] = []; + + const index = values.indexOf(3, 0, values.push(3)); + const includes = values.includes(1, undefined, effects.push(1)); + const lastOmitted = values.lastIndexOf(1); + const lastUndefined = values.lastIndexOf(1, undefined, effects.push(2)); + const lastNumeric = values.lastIndexOf(1, 3, { ignored: true }); + + return index === 3 && includes && lastOmitted === 2 && lastUndefined === 0 + && lastNumeric === 2 && effects.length === 2; + } + + stringIndexesEvaluateIgnoredArguments(): boolean { + const effects: number[] = []; + + const character = "abc".charAt(undefined, effects.push(1)); + const codeUnit = "abc".charCodeAt(1, effects.push(2)); + + return character === "a" && codeUnit === 98 && effects.length === 2; + } + + stringSearchesEvaluateIgnoredArguments(): boolean { + const effects: number[] = []; + + const index = "abc".indexOf("b", undefined, effects.push(1)); + const includes = "abc".includes("c", 1, effects.push(2)); + const starts = "abc".startsWith("b", 1, { ignored: true }); + const ends = "abc".endsWith("c", undefined, effects.push(3)); + const last = "ababa".lastIndexOf("ba", undefined, effects.push(4)); + + return index === 1 && includes && starts && ends && last === 3 && effects.length === 4; + } + + stringSliceEvaluatesIgnoredArguments(): boolean { + const effects: number[] = []; + + const suffix = "abc".slice(1, undefined, effects.push(1)); + const middle = "abc".slice(1, 2, { ignored: true }); + + return suffix === "bc" && middle === "b" && effects.length === 1; + } + + stringCaseConversionEvaluatesIgnoredArguments(): boolean { + const effects: number[] = []; + + const upper = "ab".toUpperCase(effects.push(1), { ignored: true }); + const lower = "CD".toLowerCase(effects.push(2)); + + return upper === "AB" && lower === "cd" && effects.length === 2; + } + + arrayIndexOfUsesStrictEqualityAndOffsets(): number { + const values = [NaN, 2, 3, 2]; + return values.indexOf(NaN) * 1000 + + values.indexOf(2, 2) * 100 + + values.indexOf(3, -Infinity) * 10 + + values.indexOf(2, Infinity); + } + + arrayIncludesUsesSameValueZero(): boolean { + return [NaN].includes(NaN); + } + + numericDefaultSearchFallsBack(): boolean { + return [0].includes(0); + } + + arrayOffsetsAreNormalized(): number { + const values = [1, 2, 3, 2]; + return values.indexOf(2, 1.9) * 100 + + values.indexOf(2, -1.9) * 10 + + (values.includes(1, NaN) ? 1 : 0); + } + + emptyArraysDoNotMatch(): boolean { + return ![].includes(1) && [].indexOf(1) === -1; + } + + arrayExplicitUndefinedOffset(): number { + return [1].indexOf(1, undefined); + } + + arrayLastIndexOfHandlesOffsets(): number { + const values = [1, 2, 1]; + return values.lastIndexOf(1) * 100 + + values.lastIndexOf(1, -2) * 10 + + values.lastIndexOf(1, -Infinity); + } + + arrayLastIndexOfExplicitUndefined(): number { + return [1, 2, 1].lastIndexOf(1, undefined); + } + + arrayLastIndexOfBeforeStart(): number { + return [1].lastIndexOf(1, -2); + } + + arraySearchReturnsPositiveZero(): number { + const first = [1].indexOf(1, -0); + const last = [1].lastIndexOf(1, -0.9); + let result = 0; + if (1 / first === Infinity) result += 1; + if (1 / last === Infinity) result += 2; + return result; + } + + numericHoleDoesNotMatchZero(): number { + const values = new Array(1); + return values.indexOf(0); + } + + numericHoleDoesNotIncludeUndefined(): boolean { + const values = new Array(1); + return values.includes(undefined); + } + + numericHoleWithSymbolicSearch(value: number): boolean { + const values = new Array(1); + return values.includes(value); + } + + explicitUndefinedArrayIncludesUndefined(): boolean { + const values = [undefined]; + return values.includes(undefined); + } + + explicitUndefinedArrayIndexOfUndefined(): number { + const values = [undefined]; + return values.indexOf(undefined); + } + + stringCharAtHandlesBounds(): string { + return "abc".charAt(1) + "abc".charAt(-1); + } + + stringIndexOfHandlesOffsetsAndEmptySearch(): number { + return "ababa".indexOf("ba", 2) * 100 + + "abc".indexOf("", Infinity) * 10 + + "abc".indexOf("a", -Infinity); + } + + stringIncludesHandlesNaNPosition(): boolean { + return "abc".includes("a", NaN) && !"abc".includes("a", Infinity); + } + + stringExplicitUndefinedPositions(): number { + return "abc".indexOf("a", undefined) + ("abc".charAt(undefined) === "a" ? 1 : 0); + } + + stringSymbolicPosition(position: number): number { + if (position === 0) return "ababa".indexOf("ba", position); + if (position === 2) return "ababa".indexOf("ba", position); + if (position === 4) return "ababa".indexOf("ba", position); + return -100; + } + + symbolicCharAt(position: number): string { + return "abc".charAt(position); + } + + stringCharCodeAtHandlesBounds(): number { + const outside = "AZ".charCodeAt(2); + return "AZ".charCodeAt(1) + (outside !== outside ? 1 : 0); + } + + stringStartsAndEndsWithHandlePositions(): boolean { + return "abc".startsWith("b", 1) + && "abc".startsWith("", Infinity) + && "abc".endsWith("b", 2) + && "abc".endsWith("c", undefined); + } + + stringLastIndexOfHandlesPositions(): number { + return "ababa".lastIndexOf("ba") * 100 + + "ababa".lastIndexOf("ba", 2) * 10 + + "ababa".lastIndexOf("", Infinity); + } + + stringSlicePreservesUtf16(): string { + return "A😀Z".slice(1, 3); + } + + stringModelsUseValueEquality(): boolean { + const whole = "abc".slice(0); + const independent = "abc".slice(0); + const empty = "abc".slice(0, 0); + + return whole === "abc" + && whole == "abc" + && whole === independent + && empty === "" + && empty === "x".slice(1) + && empty !== "a" + && whole + "d" === "abcd"; + } + + stringEqualityPreservesReferenceIdentity(): boolean { + const alias: number[] = [1]; + return alias === alias && alias !== [1]; + } + + stringValueEqualityThroughAny(): boolean { + const whole: any = "abc".slice(0); + const empty: any = "abc".slice(0, 0); + return whole === "abc" && whole == "abc" && empty === ""; + } + + stringTruthinessUsesLength(): boolean { + const empty = "abc".slice(0, 0); + const nonEmpty = "abc".slice(0, 1); + return !empty && !"" && !!nonEmpty; + } + + nonStringTruthinessDoesNotReadStringStorage(): boolean { + const object = { value: 1 }; + const array: number[] = []; + return !undefined && !null && !!object && !!array; + } + + mixedObjectEqualityDoesNotReadStringStorage(index: number): boolean { + if (index !== 0 && index !== 1) return true; + const dummy = "x"; + const values: any[] = [{}, {}]; + return values[index] !== ""; + } + + stringCapitalizeAscii(): string { + const value = "hELLO"; + return value.charAt(0).toUpperCase() + value.slice(1).toLowerCase(); + } + + stringCapitalizeEmpty(): string { + const value = ""; + return value.charAt(0).toUpperCase() + value.slice(1).toLowerCase(); + } + + stringCapitalizeNonAscii(): string { + const value = "éCOLE"; + return value.charAt(0).toUpperCase() + value.slice(1).toLowerCase(); + } + + legacyArrayPush(): number { + return [1].push(2); + } + + legacyArrayFill(): number[] { + return [1].fill(2); + } + + legacyArrayUnshift(): number { + return [1].unshift(2); + } + + legacyArrayJoin(): string { + return [1, 2].join("-"); + } + + legacyArraySlice(): number[] { + return [1, 2].slice(1); + } + + legacyArrayConcat(): number[] { + return [1].concat([2]); + } + + legacyArrayReverse(): number[] { + return [1, 2].reverse(); + } + + legacyArrayToString(): string { + return [1, 2].toString(); + } +} diff --git a/usvm-ts/src/test/resources/models/StringIndexing.ts b/usvm-ts/src/test/resources/models/StringIndexing.ts new file mode 100644 index 0000000000..c0849a1beb --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringIndexing.ts @@ -0,0 +1,87 @@ +export class StringIndexing { + indexedReadEquals(): boolean { + return "\udc00"[0] === "\udc00"; + } + + outOfRangeIndex(): boolean { + return "x"[1] === undefined; + } + + literalUtf16(): boolean { + const value = "A\u0000\u03a9\ud83d\ude00"; + return value[0] === "A" && value[1] === "\u0000" && value[2] === "\u03a9" && + value[3] === "\ud83d" && value[4] === "\ude00"; + } + + invalidIndexes(): boolean { + const value = "ab"; + return value[-1] === undefined && value[2] === undefined && value[0.5] === undefined && + value[NaN] === undefined && value[Infinity] === undefined && value[-Infinity] === undefined && + value[4294967296] === undefined && value[-0] === "a"; + } + + stringKeys(): boolean { + const value = "ab"; + return value["1"] === "b" && value["01"] === undefined && value["-0"] === undefined && + value["1.0"] === undefined && value["length"] === 2; + } + + symbolicIndex(index: number): number { + const character = "aba"[index]; + if (character === "a") { + return 1; + } + if (character === "b") { + return 2; + } + return 3; + } + + symbolicString(value: string): number { + if (value.length === 0) { + return value[0] === undefined ? 0 : -1; + } + return value[0] === "a" ? 1 : 2; + } + + symbolicCharAt(value: string, index: number): number { + if (value.length > 2) { + return 0; + } + return value.charAt(index) === "a" ? 1 : 2; + } + + symbolicSlice(value: string): string { + if (value.length !== 2) { + return ""; + } + return value.slice(0, 1); + } + + symbolicSearch(value: string): number { + if (value.length > 2) { + return -2; + } + return value.indexOf("a"); + } + + symbolicPattern(value: string): number { + if (value.length > 1) { + return -2; + } + return "aba".indexOf(value); + } + + symbolicCase(value: string): string { + if (value.length !== 1) { + return ""; + } + + const codeUnit = value.charCodeAt(0); + if (codeUnit > 127) { + return ""; + } + + return value.toUpperCase() + value.toLowerCase(); + } +}