From 7f8054eba5b9bbdb9d7867f9e97d21d1a86818be Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 8 Oct 2026 00:41:22 +0300 Subject: [PATCH 01/10] Model String and Array methods with private string backing --- usvm-ts/UNKNOWN_CALL_MODELS.md | 39 +- .../machine/call/TsEtsIrUnknownCallModel.kt | 8 +- .../usvm/machine/call/TsUnknownCallModel.kt | 2 + .../machine/call/TsUnknownCallModelCatalog.kt | 17 +- .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 172 ++++++++ .../call/intrinsic/TsArrayPopEtsIrModel.kt | 66 ---- .../intrinsic/TsStringEtsIrModelFamily.kt | 370 ++++++++++++++++++ .../usvm/machine/expr/CallApproximations.kt | 83 +++- .../usvm/machine/call/models/ArrayModels.ts | 101 +++++ .../usvm/machine/call/models/StringModels.ts | 181 +++++++++ .../machine/call/TsSequenceEtsIrModelTest.kt | 304 ++++++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 42 ++ .../test/resources/models/SequenceEtsIr.ts | 131 +++++++ 13 files changed, 1434 insertions(+), 82 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt create mode 100644 usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt create mode 100644 usvm-ts/src/test/resources/models/SequenceEtsIr.ts diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index b4506e3f6f..2af98497fb 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,25 @@ 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`, and +`endsWith`. Its TypeScript algorithms depend on atomic length, UTF-16 code-unit read, and one-code-unit construction +models, plus `ts.math.floor` for positions. Current symbolic String parameters do not initialize backing character +storage, so receivers and search strings must be initialized concrete constants. `charAt` also requires a concrete +index because a dynamically constructed one-code-unit String does not yet participate in value-based String equality. +Numeric-result and predicate methods can still use symbolic numeric positions over concrete strings. + +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 +327,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/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/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..825fbe8170 --- /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.UExpr +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.TsUnknownCallTarget +import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +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 + val searchElement = inputs.getOrNull(1) + val searchRef = searchElement + ?.takeIf { it.sort == addressSort } + ?.asExpr(addressSort) + if ( + array.hasFakeValueBranch() || receiverType?.dimensions != 1 || + searchRef?.hasFakeValueBranch() == true + ) { + 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 optionalFromIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + call.resolvedInstanceInputs()?.let { inputs -> + when { + call.arguments.size == 1 -> inputs + state.ctx.mkFp64(0.0) + call.arguments.size == 2 && inputs.last() == state.ctx.mkUndefinedValue() -> { + inputs.dropLast(1) + state.ctx.mkFp64(0.0) + } + + call.arguments.size == 2 && inputs.last().sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + } + + private val optionalLastIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + call.resolvedInstanceInputs()?.let { inputs -> + when { + call.arguments.size == 1 -> inputs + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) + call.arguments.size == 2 && inputs.last() == state.ctx.mkUndefinedValue() -> { + inputs.dropLast(1) + state.ctx.mkFp64(0.0) + } + + call.arguments.size == 2 && inputs.last().sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + } + + override val models: List by lazy { + listOf( + sourceModel( + id = "ts.array.pop", + methodName = "pop", + ), + 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 = TsEtsIrUnknownCallModelInputAdapter.IDENTITY, + ): 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 fun TsUnknownCall.resolvedInstanceInputs(): List>? { + val resolvedReceiver = receiver?.resolved ?: return null + val resolvedArguments = arguments.map { argument -> argument.resolved ?: return null } + + return listOf(resolvedReceiver) + resolvedArguments + } + + 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..ffda619edd --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -0,0 +1,370 @@ +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.UConcreteHeapRef +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.state.TsState +import org.usvm.sizeSort +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue + +/** 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 optionalIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + call.resolvedInstanceInputs()?.let { inputs -> + when { + call.arguments.isEmpty() -> inputs + state.ctx.mkFp64(0.0) + call.arguments.size == 1 && inputs.last() == state.ctx.mkUndefinedValue() -> { + inputs.dropLast(1) + state.ctx.mkFp64(0.0) + } + + call.arguments.size == 1 && inputs.last().sort == state.ctx.fp64Sort -> inputs + else -> null + } + } + } + + private val optionalPositionAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + call.resolvedInstanceInputs()?.let { inputs -> + when { + call.arguments.size == 1 && inputs.last().sort == state.ctx.addressSort -> { + inputs + state.ctx.mkFp64(0.0) + } + + call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && + inputs.last() == state.ctx.mkUndefinedValue() -> { + inputs.dropLast(1) + state.ctx.mkFp64(0.0) + } + + call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && + inputs.last().sort == state.ctx.fp64Sort -> inputs + + else -> null + } + } + } + + private val optionalEndPositionAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + call.resolvedInstanceInputs()?.let { inputs -> + when { + call.arguments.size == 1 && inputs.last().sort == state.ctx.addressSort -> { + inputs + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) + } + + call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && + inputs.last() == state.ctx.mkUndefinedValue() -> { + inputs.dropLast(1) + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) + } + + call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && + inputs.last().sort == state.ctx.fp64Sort -> inputs + + else -> null + } + } + } + + private val receiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + with(state.ctx) { + val receiver = inputs.firstOrNull() + // Symbolic String parameters do not initialize the backing character array yet. + if (receiver !is UConcreteHeapRef || getStringConstantValue(receiver) == null) { + falseExpr + } else { + state.memory.types.evalTypeEquals(receiver, EtsStringType) + } + } + } + + private val receiverAndSearchDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + with(state.ctx) { + val receiver = inputs.getOrNull(0) + val searchString = inputs.getOrNull(1) + val receiverIsConstant = receiver is UConcreteHeapRef && getStringConstantValue(receiver) != null + val searchStringIsConstant = + searchString is UConcreteHeapRef && getStringConstantValue(searchString) != null + + if (!receiverIsConstant || !searchStringIsConstant) { + falseExpr + } else { + mkAnd( + state.memory.types.evalTypeEquals(receiver, EtsStringType), + state.memory.types.evalTypeEquals(searchString, EtsStringType), + ) + } + } + } + + private val receiverAndConcreteIndexDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + if (inputs.getOrNull(1) !is KFp64Value) { + state.ctx.falseExpr + } else { + receiverDomain.evaluate(state, call, inputs) + } + } + + override val models: List by lazy { + listOf( + sourceModel( + id = "ts.string.charAt", + methodName = "charAt", + inputAdapter = optionalIndexAdapter, + domainGuard = receiverAndConcreteIndexDomain, + ), + 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, + ), + primitiveModel( + methodName = "length", + arity = 1, + implementation = ::stringLength, + ), + 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 { + add(MATH_FLOOR_MODEL_ID) + add(PRIMITIVE_LENGTH_ID) + add(PRIMITIVE_CODE_UNIT_AT_ID) + if (methodName == "charAt") { + add(PRIMITIVE_FROM_CODE_UNIT_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 stringLength( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val receiver = inputs.singleOrNull()?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null + if (receiver.hasFakeValueBranch()) { + return null + } + + val characters = state.memory.read(mkStringBackingLValue(receiver)) + val length = state.memory.read(mkStringBackingLengthLValue(characters)) + val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType) + val result = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = length.cast(), + signed = true, + ) + + singleSuccessor( + state = state, + guard = receiverIsString, + result = result, + ) + } + + 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() as? KFp64Value ?: return null + val successor = TsUnknownCallModelSuccessor( + guard = trueExpr, + completion = TsUnknownCallModelCompletion.Normal { + mkInitializedStringConstant(code.value.toInt().toChar().toString()) + }, + ) + + 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 fun TsUnknownCall.resolvedInstanceInputs(): List>? { + val resolvedReceiver = receiver?.resolved ?: return null + val resolvedArguments = arguments.map { argument -> argument.resolved ?: return null } + + return listOf(resolvedReceiver) + resolvedArguments + } + + 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.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_LENGTH_ID = "ts.string.primitive.length" + 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" +} 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..cb8bc6a0dc 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,83 @@ internal fun TsExprResolver.tryApproximateInstanceCall( } } + val modeledStringMethods = setOf( + "charAt", + "charCodeAt", + "endsWith", + "includes", + "indexOf", + "lastIndexOf", + "startsWith", + ) + 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/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..b464a89de8 --- /dev/null +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -0,0 +1,181 @@ +declare class StringModelPrimitives { + static length(receiver: string): number; + static codeUnitAt(receiver: string, index: number): number; + static fromCodeUnit(codeUnit: number): string; +} + +export class StringModels { + static charAt(receiver: string, index: number): string { + const length = StringModelPrimitives.length(receiver); + const integerIndex = StringModels.normalizeCharIndex(index, length); + if (integerIndex < 0 || integerIndex >= length) { + return ""; + } + + const codeUnit = StringModelPrimitives.codeUnitAt(receiver, integerIndex); + return StringModelPrimitives.fromCodeUnit(codeUnit); + } + + static indexOf(receiver: string, searchString: string, position: number): number { + const length = StringModelPrimitives.length(receiver); + const searchLength = StringModelPrimitives.length(searchString); + const start = StringModels.normalizePosition(position, length); + + if (searchLength === 0) { + return start; + } + + let index = start; + while (index + searchLength <= length) { + let searchIndex = 0; + while ( + searchIndex < searchLength && + StringModelPrimitives.codeUnitAt(receiver, index + searchIndex) === + StringModelPrimitives.codeUnitAt(searchString, searchIndex) + ) { + 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 = StringModelPrimitives.length(receiver); + const integerIndex = StringModels.normalizeCharIndex(index, length); + if (integerIndex < 0 || integerIndex >= length) { + return NaN; + } + + return StringModelPrimitives.codeUnitAt(receiver, integerIndex); + } + + static startsWith(receiver: string, searchString: string, position: number): boolean { + const length = StringModelPrimitives.length(receiver); + const searchLength = StringModelPrimitives.length(searchString); + const start = StringModels.normalizePosition(position, length); + if (start + searchLength > length) { + return false; + } + + let searchIndex = 0; + while (searchIndex < searchLength) { + if ( + StringModelPrimitives.codeUnitAt(receiver, start + searchIndex) !== + StringModelPrimitives.codeUnitAt(searchString, searchIndex) + ) { + return false; + } + + searchIndex++; + } + + return true; + } + + static endsWith(receiver: string, searchString: string, endPosition: number): boolean { + const length = StringModelPrimitives.length(receiver); + const searchLength = StringModelPrimitives.length(searchString); + const end = StringModels.normalizePosition(endPosition, length); + const start = end - searchLength; + if (start < 0) { + return false; + } + + let searchIndex = 0; + while (searchIndex < searchLength) { + if ( + StringModelPrimitives.codeUnitAt(receiver, start + searchIndex) !== + StringModelPrimitives.codeUnitAt(searchString, searchIndex) + ) { + return false; + } + + searchIndex++; + } + + return true; + } + + static lastIndexOf(receiver: string, searchString: string, position: number): number { + const length = StringModelPrimitives.length(receiver); + const searchLength = StringModelPrimitives.length(searchString); + let index = StringModels.normalizeLastPosition(position, length); + if (index + searchLength > length) { + index = length - searchLength; + } + + while (index >= 0) { + let searchIndex = 0; + while ( + searchIndex < searchLength && + StringModelPrimitives.codeUnitAt(receiver, index + searchIndex) === + StringModelPrimitives.codeUnitAt(searchString, searchIndex) + ) { + 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); + } +} 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..e8d3ee2963 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt @@ -0,0 +1,304 @@ +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 `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 also enables its primitives`() { + 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", + "ts.string.primitive.codeUnitAt", + "ts.string.primitive.fromCodeUnit", + "ts.string.primitive.length", + ), + 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 falls back until string value equality is modeled`() { + val result = analyze(methodName = "symbolicCharAt") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + } + + @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) + } + + 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, + 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..13cb8eabb8 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,16 @@ 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.primitive.length", + "ts.string.startsWith", ) assertEquals(expectedModelIds, catalog.modelIds) @@ -281,6 +320,7 @@ class TsUnknownCallModelCatalogTest { failureReason: TsUnknownCallFailureReason? = null, className: String? = null, additionalSceneFiles: List = emptyList(), + requiredModelIds: Set = emptySet(), ): TsUnknownCallModel = FakeModel( id = id, target = TsUnknownCallTarget( @@ -289,12 +329,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/resources/models/SequenceEtsIr.ts b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts new file mode 100644 index 0000000000..0a34f10342 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts @@ -0,0 +1,131 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class SequenceEtsIr { + 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); + } +} From c44606ab971f0b4d5b8b8480e637e71c41a8d50f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 12 Oct 2026 14:58:11 +0000 Subject: [PATCH 02/10] Resolve main conflict in built-in model catalog test Co-authored-by: CaelmBleidd <31047452+CaelmBleidd@users.noreply.github.com> --- .../call/TsUnknownCallModelCatalogTest.kt | 32 ++++++++++++------- 1 file changed, 20 insertions(+), 12 deletions(-) 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 13cb8eabb8..30d81a5c82 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -178,10 +178,7 @@ 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, @@ -196,6 +193,25 @@ class TsUnknownCallModelCatalogTest { TsNumericIntrinsicModelFamily.NUMBER_IS_INTEGER_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_NAN_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID, + ) + + assertEquals(expectedModelIds, catalog.modelIds) + assertSame(catalog, TsBuiltInUnknownCallModels.catalog()) + assertFailsWith { (catalog.modelIds as MutableList).clear() } + assertEquals( + expectedModelIds, + TsBuiltInUnknownCallModels.catalog().modelIds, + ) + 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", @@ -207,15 +223,7 @@ class TsUnknownCallModelCatalogTest { "ts.string.primitive.length", "ts.string.startsWith", ) - - assertEquals(expectedModelIds, catalog.modelIds) - assertSame(catalog, TsBuiltInUnknownCallModels.catalog()) - assertFailsWith { (catalog.modelIds as MutableList).clear() } - assertEquals( - expectedModelIds, - TsBuiltInUnknownCallModels.catalog().modelIds, - ) - assertTrue(TsBuiltInUnknownCallModels.catalog(TsUnknownCallModelSelection.Only(emptySet())).modelIds.isEmpty()) + assertTrue(modelIds.containsAll(expectedModelIds)) } @Test From 93a68ae6836ab9590a8b260df51108eef685a72b Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 19:54:23 +0300 Subject: [PATCH 03/10] Update complete built-in catalog expectation after model discovery --- .../machine/call/TsUnknownCallModelCatalogTest.kt | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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 30d81a5c82..94b45a9588 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -178,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, @@ -193,6 +196,16 @@ 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.primitive.length", + "ts.string.startsWith", ) assertEquals(expectedModelIds, catalog.modelIds) From 6af13741dedbe22cc54a2cf42bcaa1979ced56d6 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 20:08:28 +0300 Subject: [PATCH 04/10] Complete sequence models with bounded UTF-16 storage --- .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 10 +- .../intrinsic/TsStringEtsIrModelFamily.kt | 160 +++++++++++++++++- .../usvm/machine/expr/CallApproximations.kt | 3 + .../kotlin/org/usvm/machine/expr/ReadField.kt | 2 +- .../org/usvm/machine/expr/ReadLength.kt | 28 +-- .../org/usvm/machine/expr/TsExprResolver.kt | 2 +- .../usvm/machine/interpreter/TsInterpreter.kt | 17 +- .../usvm/machine/operator/TsBinaryOperator.kt | 7 +- .../kotlin/org/usvm/machine/state/TsState.kt | 16 +- .../org/usvm/machine/state/TsStringBacking.kt | 2 +- .../main/kotlin/org/usvm/util/ArrayStorage.kt | 40 +++++ .../kotlin/org/usvm/util/StringStorage.kt | 97 +++++++++++ .../usvm/machine/call/models/StringModels.ts | 56 ++++++ .../machine/call/TsSequenceEtsIrModelTest.kt | 70 ++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 8 + .../kotlin/org/usvm/util/TsTestResolver.kt | 8 +- .../test/resources/models/SequenceEtsIr.ts | 95 +++++++++++ 17 files changed, 586 insertions(+), 35 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index 825fbe8170..f896269a5a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -2,6 +2,7 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact @@ -13,6 +14,7 @@ import org.usvm.machine.call.TsUnknownCallModel import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.util.arrayStorageType +import org.usvm.util.isUnmodifiedDenseInputArray /** Built-in Array algorithms implemented by ordinary TypeScript bodies. */ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { @@ -48,22 +50,24 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { falseExpr } else { val elementSort = typeToSort(receiverType.elementType) + val hasNoMissingSlots = array is UConcreteHeapRef && + state.isUnmodifiedDenseInputArray(array, receiverType) val excludesMissingSlot = when { searchElement == mkUndefinedValue() && ( call.callee.name in setOf("indexOf", "lastIndexOf") || elementSort == fp64Sort || elementSort == boolSort - ) -> falseExpr + ) -> mkBool(hasNoMissingSlots) elementSort == fp64Sort && searchElement?.sort == fp64Sort -> { val searchNumber = searchElement.asExpr(fp64Sort) val zero = mkFp64(0.0) - mkNot(mkFpEqualExpr(searchNumber, zero)) + mkOr(mkBool(hasNoMissingSlots), mkNot(mkFpEqualExpr(searchNumber, zero))) } elementSort == boolSort && searchElement?.sort == boolSort -> { - searchElement.asExpr(boolSort) + mkOr(mkBool(hasNoMissingSlots), searchElement.asExpr(boolSort)) } else -> trueExpr diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index ffda619edd..1fe49fbf30 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -21,9 +21,11 @@ import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.state.TsState import org.usvm.sizeSort +import org.usvm.util.copyStringRange 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 { @@ -94,11 +96,51 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } + private val sliceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs() ?: return@TsEtsIrUnknownCallModelInputAdapter null + val receiver = inputs.firstOrNull()?.takeIf { it.sort == state.ctx.addressSort } + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = inputs.drop(1) + if (arguments.size > 2) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + fun numericOrDefault(index: Int, default: UExpr<*>): UExpr<*> { + val value = arguments.getOrNull(index) ?: return default + return when { + value == state.ctx.mkUndefinedValue() -> default + value.sort == state.ctx.fp64Sort -> value + else -> return default + } + } + + 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), + ) + val hasUnsupportedArgument = arguments.any { value -> + value != state.ctx.mkUndefinedValue() && value.sort != state.ctx.fp64Sort + } + if (hasUnsupportedArgument) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + listOf(receiver, start, end) + } + + private val noArgumentsAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + if (call.arguments.isNotEmpty()) { + null + } else { + call.resolvedInstanceInputs() + } + } + private val receiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> with(state.ctx) { val receiver = inputs.firstOrNull() - // Symbolic String parameters do not initialize the backing character array yet. - if (receiver !is UConcreteHeapRef || getStringConstantValue(receiver) == null) { + if (receiver !is UConcreteHeapRef || receiver.hasFakeValueBranch()) { falseExpr } else { state.memory.types.evalTypeEquals(receiver, EtsStringType) @@ -110,9 +152,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { with(state.ctx) { val receiver = inputs.getOrNull(0) val searchString = inputs.getOrNull(1) - val receiverIsConstant = receiver is UConcreteHeapRef && getStringConstantValue(receiver) != null - val searchStringIsConstant = - searchString is UConcreteHeapRef && getStringConstantValue(searchString) != null + val receiverIsConstant = receiver is UConcreteHeapRef && !receiver.hasFakeValueBranch() + val searchStringIsConstant = searchString is UConcreteHeapRef && !searchString.hasFakeValueBranch() if (!receiverIsConstant || !searchStringIsConstant) { falseExpr @@ -125,6 +166,38 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } + private val asciiReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiverGuard = receiverDomain.evaluate(state, call, inputs) + val receiver = inputs.firstOrNull() as? UConcreteHeapRef + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + 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(), + ) + } + } + private val receiverAndConcreteIndexDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> if (inputs.getOrNull(1) !is KFp64Value) { state.ctx.falseExpr @@ -177,6 +250,24 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = optionalEndPositionAdapter, domainGuard = receiverAndSearchDomain, ), + sourceModel( + id = "ts.string.slice", + methodName = "slice", + inputAdapter = sliceAdapter, + domainGuard = receiverDomain, + ), + sourceModel( + id = "ts.string.toUpperCase", + methodName = "toUpperCase", + inputAdapter = noArgumentsAdapter, + domainGuard = asciiReceiverDomain, + ), + sourceModel( + id = "ts.string.toLowerCase", + methodName = "toLowerCase", + inputAdapter = noArgumentsAdapter, + domainGuard = asciiReceiverDomain, + ), primitiveModel( methodName = "length", arity = 1, @@ -192,6 +283,11 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { arity = 1, implementation = ::stringFromCodeUnit, ), + primitiveModel( + methodName = "copyRange", + arity = 3, + implementation = ::stringCopyRange, + ), ) } @@ -214,9 +310,12 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { add(MATH_FLOOR_MODEL_ID) add(PRIMITIVE_LENGTH_ID) add(PRIMITIVE_CODE_UNIT_AT_ID) - if (methodName == "charAt") { + if (methodName in setOf("charAt", "toUpperCase", "toLowerCase")) { add(PRIMITIVE_FROM_CODE_UNIT_ID) } + if (methodName == "slice") { + add(PRIMITIVE_COPY_RANGE_ID) + } }, ) @@ -305,16 +404,58 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { state: TsState, inputs: List>, ): TsUnknownCallModelExecution? = with(state.ctx) { - val code = inputs.singleOrNull() as? KFp64Value ?: return null + val code = inputs.singleOrNull()?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null val successor = TsUnknownCallModelSuccessor( guard = trueExpr, completion = TsUnknownCallModelCompletion.Normal { - mkInitializedStringConstant(code.value.toInt().toChar().toString()) + if (code is KFp64Value) { + mkInitializedStringConstant(code.value.toInt().toChar().toString()) + } else { + stringFromCodeUnit(code) + } + }, + ) + + TsUnknownCallModelExecution( + successors = listOf(successor), + ) + } + + private fun stringCopyRange( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val receiver = inputs.getOrNull(0)?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null + val start = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val end = inputs.getOrNull(2)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + if (receiver.hasFakeValueBranch()) { + return null + } + + val from = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = start, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val to = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = end, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + val length = mkBvSubExpr(to, from) + val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType) + val successor = TsUnknownCallModelSuccessor( + guard = receiverIsString, + completion = TsUnknownCallModelCompletion.Normal { + copyStringRange(receiver = receiver, from = from, length = length) }, ) TsUnknownCallModelExecution( successors = listOf(successor), + residualGuard = receiverIsString.takeUnless { it == trueExpr }?.let(::mkNot), ) } @@ -366,5 +507,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private const val PRIMITIVE_LENGTH_ID = "ts.string.primitive.length" 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 PRIMITIVE_COPY_RANGE_ID = "ts.string.primitive.copyRange" 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 cb8bc6a0dc..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 @@ -218,7 +218,10 @@ internal fun TsExprResolver.tryApproximateInstanceCall( "includes", "indexOf", "lastIndexOf", + "slice", "startsWith", + "toLowerCase", + "toUpperCase", ) if (instanceType is EtsStringType && expr.callee.name in modeledStringMethods) { val dispatcher = unknownCallDispatcher 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/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 419d1aeaf2..f1d307aca3 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 @@ -804,7 +804,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/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 048df55899..062cb4a356 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 @@ -40,6 +40,7 @@ import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UExpr import org.usvm.UInterpreter +import org.usvm.USort import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArray import org.usvm.api.targets.TsTarget @@ -783,7 +784,12 @@ class TsInterpreter( observer = observer, ) - fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { + fun getInitialState( + method: EtsMethod, + targets: List, + configure: (TsState) -> Unit = {}, + parameterSortOverride: (Int) -> USort? = { null }, + ): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -811,6 +817,11 @@ class TsInterpreter( method.parameters.forEachIndexed { i, param -> val idx = i + 1 // +1 because 0 is reserved for `this` + val overriddenSort = parameterSortOverride(idx) + if (overriddenSort != null) { + state.saveSortForLocal(idx, overriddenSort) + return@forEachIndexed + } val ref by lazy { val lValue = mkRegisterStackLValue(addressSort, idx) @@ -859,7 +870,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) @@ -877,6 +888,8 @@ class TsInterpreter( } } + configure(state) + val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) 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..daed206637 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 @@ -1,5 +1,6 @@ package org.usvm.machine.state +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsFile @@ -32,6 +33,7 @@ import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsFunction import org.usvm.memory.ULValue import org.usvm.memory.UMemory +import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelBase import org.usvm.sizeSort import org.usvm.targets.UTargetsSet @@ -87,11 +89,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. */ @@ -100,6 +102,7 @@ class TsState( var trackedObjectProperties: Set = emptySet(), var writtenConcreteFields: Set> = emptySet(), var writtenObjectLiteralFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), + internal val denseInputArrays: MutableMap = mutableMapOf(), private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, @@ -300,6 +303,7 @@ class TsState( ref } stringConstantAllocatedRefs = updated + boundedStringBackingRefs += result to value.length result } @@ -347,6 +351,7 @@ class TsState( trackedObjectProperties = trackedObjectProperties, writtenConcreteFields = writtenConcreteFields, writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts, + denseInputArrays = denseInputArrays.toMutableMap(), activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } @@ -354,3 +359,10 @@ class TsState( override val isExceptional: Boolean get() = methodResult is TsMethodResult.TsException } + +/** Snapshot of the storage regions that establish dense input-array contents. */ +data class TsDenseInputArray( + val type: EtsArrayType, + val lengthRegion: UReadOnlyMemoryRegion<*, *>, + val elementRegion: UReadOnlyMemoryRegion<*, *>, +) 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/ArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt index 3cd941ce4b..b308634a5e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt @@ -14,11 +14,14 @@ import org.usvm.USort import org.usvm.api.memcpy import org.usvm.collection.array.UArrayRegion import org.usvm.collection.array.UArrayRegionId +import org.usvm.collection.array.length.UArrayLengthsRegionId import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsDenseInputArray import org.usvm.machine.state.TsState import org.usvm.machine.types.TsUnresolvedArrayKind +import org.usvm.sizeSort /** Enumerates payload regions independently of whether an array was allocated or came from the input. */ internal inline fun TsContext.forEachArrayPayloadRegion(arrayType: EtsArrayType, action: (EtsType, USort) -> Unit) { @@ -73,3 +76,40 @@ internal fun TsState.initializeArrayKind( ) memory.setRegion(regionId, initialized) } + +/** Records that every slot below the current input length has an initialized value. */ +fun TsState.markDenseInputArray( + array: UConcreteHeapRef, + type: EtsArrayType, +) = with(ctx) { + val descriptor = arrayDescriptorOf(type) + val elementSort = typeToSort(type.elementType) + require(elementSort !is TsUnresolvedSort) { "A dense input array needs a concrete element sort" } + + val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) + val elementRegionId = UArrayRegionId(descriptor, elementSort) + denseInputArrays[array] = TsDenseInputArray( + type = type, + lengthRegion = memory.getRegion(lengthRegionId), + elementRegion = memory.getRegion(elementRegionId), + ) +} + +/** Returns true only while neither the recorded length nor payload region has changed. */ +internal fun TsState.isUnmodifiedDenseInputArray( + array: UConcreteHeapRef, + type: EtsArrayType, +): Boolean = with(ctx) { + val snapshot = denseInputArrays[array] ?: return false + if (snapshot.type != type) return false + + val descriptor = arrayDescriptorOf(type) + val elementSort = typeToSort(type.elementType) + if (elementSort is TsUnresolvedSort) return false + + val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) + val elementRegionId = UArrayRegionId(descriptor, elementSort) + + memory.getRegion(lengthRegionId) === snapshot.lengthRegion && + memory.getRegion(elementRegionId) === snapshot.elementRegion +} 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..a07f72f8fe --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt @@ -0,0 +1,97 @@ +package org.usvm.util + +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.api.memcpy +import org.usvm.machine.TsSizeSort +import org.usvm.machine.state.TsState +import org.usvm.sizeSort + +internal 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)) +} + +fun TsState.markStringMaxLength( + string: UConcreteHeapRef, + maxLength: Int, +) { + require(maxLength >= 0) { "String maximum length must be non-negative" } + boundedStringBackingRefs += string to maxLength +} + +private fun TsState.trackedStringMaxLength(string: UHeapRef): Int? = + boundedStringBackingRefs[string] + +internal fun TsState.allocateString( + length: UExpr, + maxLength: Int? = null, +): 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, + ) + if (maxLength != null) { + markStringMaxLength(string = string, maxLength = maxLength) + } + + string to characters +} + +internal fun TsState.copyStringRange( + receiver: UHeapRef, + from: UExpr, + length: UExpr, +): UConcreteHeapRef = with(ctx) { + val source = stringCharacters(receiver) + val (result, destination) = allocateString(length, maxLength = trackedStringMaxLength(receiver)) + memory.memcpy( + source, + destination, + stringBackingArrayDescriptor, + bv16Sort, + fromSrc = from, + fromDst = mkBv(0), + length = length, + ) + result +} + +internal fun TsState.stringFromCodeUnit(codeUnit: UExpr): UConcreteHeapRef = with(ctx) { + val (result, characters) = allocateString(mkBv(1), maxLength = 1) + val value = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = codeUnit, + bvSize = bv16Sort.sizeBits.toInt(), + isSigned = false, + ).asExpr(bv16Sort) + val character = mkStringBackingElementLValue(ref = characters, index = mkBv(0)) + memory.write( + character, + value, + guard = trueExpr, + ) + result +} diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts index b464a89de8..fcc28f3c09 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -2,6 +2,7 @@ declare class StringModelPrimitives { static length(receiver: string): number; static codeUnitAt(receiver: string, index: number): number; static fromCodeUnit(codeUnit: number): string; + static copyRange(receiver: string, start: number, end: number): string; } export class StringModels { @@ -60,6 +61,43 @@ export class StringModels { return StringModelPrimitives.codeUnitAt(receiver, integerIndex); } + static slice(receiver: string, start: number, end: number): string { + const length = StringModelPrimitives.length(receiver); + const from = StringModels.normalizeSliceIndex(start, length); + const to = StringModels.normalizeSliceIndex(end, length); + return StringModelPrimitives.copyRange(receiver, from, to < from ? from : to); + } + + static toUpperCase(receiver: string): string { + const length = StringModelPrimitives.length(receiver); + 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 = StringModelPrimitives.length(receiver); + 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 = StringModelPrimitives.length(receiver); const searchLength = StringModelPrimitives.length(searchString); @@ -178,4 +216,22 @@ export class StringModels { 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/call/TsSequenceEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt index e8d3ee2963..37b661b393 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt @@ -242,6 +242,76 @@ class TsSequenceEtsIrModelTest { 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(), 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 94b45a9588..9bb27c8f13 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 @@ -203,9 +203,13 @@ class TsUnknownCallModelCatalogTest { "ts.string.indexOf", "ts.string.lastIndexOf", "ts.string.primitive.codeUnitAt", + "ts.string.primitive.copyRange", "ts.string.primitive.fromCodeUnit", "ts.string.primitive.length", + "ts.string.slice", "ts.string.startsWith", + "ts.string.toLowerCase", + "ts.string.toUpperCase", ) assertEquals(expectedModelIds, catalog.modelIds) @@ -232,9 +236,13 @@ class TsUnknownCallModelCatalogTest { "ts.string.indexOf", "ts.string.lastIndexOf", "ts.string.primitive.codeUnitAt", + "ts.string.primitive.copyRange", "ts.string.primitive.fromCodeUnit", "ts.string.primitive.length", + "ts.string.slice", "ts.string.startsWith", + "ts.string.toLowerCase", + "ts.string.toUpperCase", ) assertTrue(modelIds.containsAll(expectedModelIds)) } 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 index 0a34f10342..9c6cbde6c6 100644 --- a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts +++ b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts @@ -128,4 +128,99 @@ export class SequenceEtsIr { + "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(); + } } From 897bea67f17669fc706605c3405ae86f5cae1370 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 22:08:06 +0300 Subject: [PATCH 05/10] Use ordinary string indexing in EtsIR models --- usvm-ts/UNKNOWN_CALL_MODELS.md | 22 +- .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 10 +- .../intrinsic/TsStringEtsIrModelFamily.kt | 150 +++-------- .../kotlin/org/usvm/machine/expr/Property.kt | 23 +- .../kotlin/org/usvm/machine/expr/ReadArray.kt | 5 + .../org/usvm/machine/expr/ReadString.kt | 64 +++++ .../org/usvm/machine/expr/TsExprResolver.kt | 6 + .../org/usvm/machine/expr/WriteArray.kt | 5 + .../usvm/machine/interpreter/TsInterpreter.kt | 11 - .../kotlin/org/usvm/machine/state/TsState.kt | 11 - .../main/kotlin/org/usvm/util/ArrayStorage.kt | 40 --- .../kotlin/org/usvm/util/StringStorage.kt | 51 +--- .../usvm/machine/call/models/StringModels.ts | 83 +++--- .../org/usvm/machine/TsStringIndexingTest.kt | 237 ++++++++++++++++++ .../machine/call/TsSequenceEtsIrModelTest.kt | 15 +- .../call/TsUnknownCallModelCatalogTest.kt | 4 - .../test/resources/models/StringIndexing.ts | 79 ++++++ 17 files changed, 533 insertions(+), 283 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadString.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt create mode 100644 usvm-ts/src/test/resources/models/StringIndexing.ts diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 2af98497fb..46c204fb8a 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -242,12 +242,22 @@ numeric and boolean search values use a guarded model branch outside the typed d 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`, and -`endsWith`. Its TypeScript algorithms depend on atomic length, UTF-16 code-unit read, and one-code-unit construction -models, plus `ts.math.floor` for positions. Current symbolic String parameters do not initialize backing character -storage, so receivers and search strings must be initialized concrete constants. `charAt` also requires a concrete -index because a dynamically constructed one-code-unit String does not yet participate in value-based String equality. -Numeric-result and predicate methods can still use symbolic numeric positions over concrete strings. +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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index f896269a5a..825fbe8170 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -2,7 +2,6 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact @@ -14,7 +13,6 @@ import org.usvm.machine.call.TsUnknownCallModel import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.util.arrayStorageType -import org.usvm.util.isUnmodifiedDenseInputArray /** Built-in Array algorithms implemented by ordinary TypeScript bodies. */ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { @@ -50,24 +48,22 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { falseExpr } else { val elementSort = typeToSort(receiverType.elementType) - val hasNoMissingSlots = array is UConcreteHeapRef && - state.isUnmodifiedDenseInputArray(array, receiverType) val excludesMissingSlot = when { searchElement == mkUndefinedValue() && ( call.callee.name in setOf("indexOf", "lastIndexOf") || elementSort == fp64Sort || elementSort == boolSort - ) -> mkBool(hasNoMissingSlots) + ) -> falseExpr elementSort == fp64Sort && searchElement?.sort == fp64Sort -> { val searchNumber = searchElement.asExpr(fp64Sort) val zero = mkFp64(0.0) - mkOr(mkBool(hasNoMissingSlots), mkNot(mkFpEqualExpr(searchNumber, zero))) + mkNot(mkFpEqualExpr(searchNumber, zero)) } elementSort == boolSort && searchElement?.sort == boolSort -> { - mkOr(mkBool(hasNoMissingSlots), searchElement.asExpr(boolSort)) + searchElement.asExpr(boolSort) } else -> trueExpr diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index 1fe49fbf30..88931e4fb0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -4,7 +4,6 @@ import io.ksmt.expr.KFp64Value import io.ksmt.utils.asExpr import io.ksmt.utils.cast import org.jacodb.ets.model.EtsStringType -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.api.evalTypeEquals import org.usvm.machine.call.TsEtsIrUnknownCallModel @@ -21,7 +20,6 @@ import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.state.TsState import org.usvm.sizeSort -import org.usvm.util.copyStringRange import org.usvm.util.mkStringBackingElementLValue import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue @@ -137,40 +135,39 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } - private val receiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> - with(state.ctx) { - val receiver = inputs.firstOrNull() - if (receiver !is UConcreteHeapRef || receiver.hasFakeValueBranch()) { - falseExpr - } else { - state.memory.types.evalTypeEquals(receiver, EtsStringType) - } + 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 -> - with(state.ctx) { - val receiver = inputs.getOrNull(0) - val searchString = inputs.getOrNull(1) - val receiverIsConstant = receiver is UConcreteHeapRef && !receiver.hasFakeValueBranch() - val searchStringIsConstant = searchString is UConcreteHeapRef && !searchString.hasFakeValueBranch() + val receiverGuard = stringDomain(state = state, input = inputs.getOrNull(0)) + val searchGuard = stringDomain(state = state, input = inputs.getOrNull(1)) - if (!receiverIsConstant || !searchStringIsConstant) { - falseExpr - } else { - mkAnd( - state.memory.types.evalTypeEquals(receiver, EtsStringType), - state.memory.types.evalTypeEquals(searchString, EtsStringType), - ) - } - } + state.ctx.mkAnd(receiverGuard, searchGuard) } private val asciiReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> with(state.ctx) { val receiverGuard = receiverDomain.evaluate(state, call, inputs) - val receiver = inputs.firstOrNull() as? UConcreteHeapRef - ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + 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)) @@ -198,21 +195,13 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } - private val receiverAndConcreteIndexDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> - if (inputs.getOrNull(1) !is KFp64Value) { - state.ctx.falseExpr - } else { - receiverDomain.evaluate(state, call, inputs) - } - } - override val models: List by lazy { listOf( sourceModel( id = "ts.string.charAt", methodName = "charAt", inputAdapter = optionalIndexAdapter, - domainGuard = receiverAndConcreteIndexDomain, + domainGuard = receiverDomain, ), sourceModel( id = "ts.string.indexOf", @@ -268,11 +257,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = noArgumentsAdapter, domainGuard = asciiReceiverDomain, ), - primitiveModel( - methodName = "length", - arity = 1, - implementation = ::stringLength, - ), primitiveModel( methodName = "codeUnitAt", arity = 2, @@ -283,11 +267,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { arity = 1, implementation = ::stringFromCodeUnit, ), - primitiveModel( - methodName = "copyRange", - arity = 3, - implementation = ::stringCopyRange, - ), ) } @@ -307,14 +286,15 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { domainGuard = domainGuard, inputAdapter = inputAdapter, requiredModelIds = buildSet { - add(MATH_FLOOR_MODEL_ID) - add(PRIMITIVE_LENGTH_ID) - add(PRIMITIVE_CODE_UNIT_AT_ID) - if (methodName in setOf("charAt", "toUpperCase", "toLowerCase")) { + val convertsCase = methodName in setOf("toUpperCase", "toLowerCase") + if (convertsCase) { + add(PRIMITIVE_CODE_UNIT_AT_ID) add(PRIMITIVE_FROM_CODE_UNIT_ID) - } - if (methodName == "slice") { - add(PRIMITIVE_COPY_RANGE_ID) + } else { + add(MATH_FLOOR_MODEL_ID) + if (methodName == "charCodeAt") { + add(PRIMITIVE_CODE_UNIT_AT_ID) + } } }, ) @@ -339,32 +319,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { implementation = implementation, ) - private fun stringLength( - state: TsState, - inputs: List>, - ): TsUnknownCallModelExecution? = with(state.ctx) { - val receiver = inputs.singleOrNull()?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null - if (receiver.hasFakeValueBranch()) { - return null - } - - val characters = state.memory.read(mkStringBackingLValue(receiver)) - val length = state.memory.read(mkStringBackingLengthLValue(characters)) - val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType) - val result = mkBvToFpExpr( - sort = fp64Sort, - roundingMode = fpRoundingModeSortDefaultValue(), - value = length.cast(), - signed = true, - ) - - singleSuccessor( - state = state, - guard = receiverIsString, - result = result, - ) - } - private fun stringCodeUnitAt( state: TsState, inputs: List>, @@ -421,44 +375,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } - private fun stringCopyRange( - state: TsState, - inputs: List>, - ): TsUnknownCallModelExecution? = with(state.ctx) { - val receiver = inputs.getOrNull(0)?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null - val start = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null - val end = inputs.getOrNull(2)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null - if (receiver.hasFakeValueBranch()) { - return null - } - - val from = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = start, - bvSize = sizeSort.sizeBits.toInt(), - isSigned = true, - ).asExpr(sizeSort) - val to = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = end, - bvSize = sizeSort.sizeBits.toInt(), - isSigned = true, - ).asExpr(sizeSort) - val length = mkBvSubExpr(to, from) - val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType) - val successor = TsUnknownCallModelSuccessor( - guard = receiverIsString, - completion = TsUnknownCallModelCompletion.Normal { - copyStringRange(receiver = receiver, from = from, length = length) - }, - ) - - TsUnknownCallModelExecution( - successors = listOf(successor), - residualGuard = receiverIsString.takeUnless { it == trueExpr }?.let(::mkNot), - ) - } - private fun singleSuccessor( state: TsState, guard: org.usvm.UBoolExpr, @@ -504,10 +420,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } - private const val PRIMITIVE_LENGTH_ID = "ts.string.primitive.length" 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 PRIMITIVE_COPY_RANGE_ID = "ts.string.primitive.copyRange" 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/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/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 f1d307aca3..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) 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 062cb4a356..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 @@ -40,7 +40,6 @@ import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UExpr import org.usvm.UInterpreter -import org.usvm.USort import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArray import org.usvm.api.targets.TsTarget @@ -787,8 +786,6 @@ class TsInterpreter( fun getInitialState( method: EtsMethod, targets: List, - configure: (TsState) -> Unit = {}, - parameterSortOverride: (Int) -> USort? = { null }, ): TsState = with(ctx) { val state = TsState( ctx = ctx, @@ -817,12 +814,6 @@ class TsInterpreter( method.parameters.forEachIndexed { i, param -> val idx = i + 1 // +1 because 0 is reserved for `this` - val overriddenSort = parameterSortOverride(idx) - if (overriddenSort != null) { - state.saveSortForLocal(idx, overriddenSort) - return@forEachIndexed - } - val ref by lazy { val lValue = mkRegisterStackLValue(addressSort, idx) state.memory.read(lValue).asExpr(addressSort) @@ -888,8 +879,6 @@ class TsInterpreter( } } - configure(state) - val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) 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 daed206637..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 @@ -1,6 +1,5 @@ package org.usvm.machine.state -import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsFile @@ -33,7 +32,6 @@ import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsFunction import org.usvm.memory.ULValue import org.usvm.memory.UMemory -import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelBase import org.usvm.sizeSort import org.usvm.targets.UTargetsSet @@ -102,7 +100,6 @@ class TsState( var trackedObjectProperties: Set = emptySet(), var writtenConcreteFields: Set> = emptySet(), var writtenObjectLiteralFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), - internal val denseInputArrays: MutableMap = mutableMapOf(), private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, @@ -351,7 +348,6 @@ class TsState( trackedObjectProperties = trackedObjectProperties, writtenConcreteFields = writtenConcreteFields, writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts, - denseInputArrays = denseInputArrays.toMutableMap(), activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } @@ -359,10 +355,3 @@ class TsState( override val isExceptional: Boolean get() = methodResult is TsMethodResult.TsException } - -/** Snapshot of the storage regions that establish dense input-array contents. */ -data class TsDenseInputArray( - val type: EtsArrayType, - val lengthRegion: UReadOnlyMemoryRegion<*, *>, - val elementRegion: UReadOnlyMemoryRegion<*, *>, -) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt index b308634a5e..3cd941ce4b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt @@ -14,14 +14,11 @@ import org.usvm.USort import org.usvm.api.memcpy import org.usvm.collection.array.UArrayRegion import org.usvm.collection.array.UArrayRegionId -import org.usvm.collection.array.length.UArrayLengthsRegionId import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.TsUnresolvedSort -import org.usvm.machine.state.TsDenseInputArray import org.usvm.machine.state.TsState import org.usvm.machine.types.TsUnresolvedArrayKind -import org.usvm.sizeSort /** Enumerates payload regions independently of whether an array was allocated or came from the input. */ internal inline fun TsContext.forEachArrayPayloadRegion(arrayType: EtsArrayType, action: (EtsType, USort) -> Unit) { @@ -76,40 +73,3 @@ internal fun TsState.initializeArrayKind( ) memory.setRegion(regionId, initialized) } - -/** Records that every slot below the current input length has an initialized value. */ -fun TsState.markDenseInputArray( - array: UConcreteHeapRef, - type: EtsArrayType, -) = with(ctx) { - val descriptor = arrayDescriptorOf(type) - val elementSort = typeToSort(type.elementType) - require(elementSort !is TsUnresolvedSort) { "A dense input array needs a concrete element sort" } - - val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) - val elementRegionId = UArrayRegionId(descriptor, elementSort) - denseInputArrays[array] = TsDenseInputArray( - type = type, - lengthRegion = memory.getRegion(lengthRegionId), - elementRegion = memory.getRegion(elementRegionId), - ) -} - -/** Returns true only while neither the recorded length nor payload region has changed. */ -internal fun TsState.isUnmodifiedDenseInputArray( - array: UConcreteHeapRef, - type: EtsArrayType, -): Boolean = with(ctx) { - val snapshot = denseInputArrays[array] ?: return false - if (snapshot.type != type) return false - - val descriptor = arrayDescriptorOf(type) - val elementSort = typeToSort(type.elementType) - if (elementSort is TsUnresolvedSort) return false - - val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) - val elementRegionId = UArrayRegionId(descriptor, elementSort) - - memory.getRegion(lengthRegionId) === snapshot.lengthRegion && - memory.getRegion(elementRegionId) === snapshot.elementRegion -} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt index a07f72f8fe..f6c3255b5d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt @@ -1,5 +1,6 @@ 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 @@ -9,12 +10,11 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.api.initializeArrayLength -import org.usvm.api.memcpy import org.usvm.machine.TsSizeSort import org.usvm.machine.state.TsState import org.usvm.sizeSort -internal val STRING_CHARACTER_ARRAY_TYPE = EtsArrayType(EtsNumberType, dimensions = 1) +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) @@ -25,20 +25,9 @@ internal fun TsState.stringLength(receiver: UHeapRef): UExpr { return memory.read(mkStringBackingLengthLValue(characters)) } -fun TsState.markStringMaxLength( - string: UConcreteHeapRef, - maxLength: Int, -) { - require(maxLength >= 0) { "String maximum length must be non-negative" } - boundedStringBackingRefs += string to maxLength -} - -private fun TsState.trackedStringMaxLength(string: UHeapRef): Int? = - boundedStringBackingRefs[string] - -internal fun TsState.allocateString( +private fun TsState.allocateString( length: UExpr, - maxLength: Int? = null, + maxLength: Int, ): Pair = with(ctx) { val string = memory.allocConcrete(EtsStringType) val characters = memory.allocConcrete(STRING_CHARACTER_ARRAY_TYPE.elementType) @@ -53,44 +42,28 @@ internal fun TsState.allocateString( characters, guard = trueExpr, ) - if (maxLength != null) { - markStringMaxLength(string = string, maxLength = maxLength) - } + boundedStringBackingRefs += string to maxLength string to characters } -internal fun TsState.copyStringRange( - receiver: UHeapRef, - from: UExpr, - length: UExpr, -): UConcreteHeapRef = with(ctx) { - val source = stringCharacters(receiver) - val (result, destination) = allocateString(length, maxLength = trackedStringMaxLength(receiver)) - memory.memcpy( - source, - destination, - stringBackingArrayDescriptor, - bv16Sort, - fromSrc = from, - fromDst = mkBv(0), - length = length, - ) - result -} - internal fun TsState.stringFromCodeUnit(codeUnit: UExpr): UConcreteHeapRef = with(ctx) { - val (result, characters) = allocateString(mkBv(1), maxLength = 1) 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, - value, + codeUnit, guard = trueExpr, ) result diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts index fcc28f3c09..858bbd6035 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -1,25 +1,22 @@ declare class StringModelPrimitives { - static length(receiver: string): number; static codeUnitAt(receiver: string, index: number): number; static fromCodeUnit(codeUnit: number): string; - static copyRange(receiver: string, start: number, end: number): string; } export class StringModels { static charAt(receiver: string, index: number): string { - const length = StringModelPrimitives.length(receiver); + const length = receiver.length; const integerIndex = StringModels.normalizeCharIndex(index, length); if (integerIndex < 0 || integerIndex >= length) { return ""; } - const codeUnit = StringModelPrimitives.codeUnitAt(receiver, integerIndex); - return StringModelPrimitives.fromCodeUnit(codeUnit); + return receiver[integerIndex]; } static indexOf(receiver: string, searchString: string, position: number): number { - const length = StringModelPrimitives.length(receiver); - const searchLength = StringModelPrimitives.length(searchString); + const length = receiver.length; + const searchLength = searchString.length; const start = StringModels.normalizePosition(position, length); if (searchLength === 0) { @@ -29,11 +26,14 @@ export class StringModels { let index = start; while (index + searchLength <= length) { let searchIndex = 0; - while ( - searchIndex < searchLength && - StringModelPrimitives.codeUnitAt(receiver, index + searchIndex) === - StringModelPrimitives.codeUnitAt(searchString, searchIndex) - ) { + while (searchIndex < searchLength) { + const character = receiver[index + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { + break; + } + searchIndex++; } @@ -52,7 +52,7 @@ export class StringModels { } static charCodeAt(receiver: string, index: number): number { - const length = StringModelPrimitives.length(receiver); + const length = receiver.length; const integerIndex = StringModels.normalizeCharIndex(index, length); if (integerIndex < 0 || integerIndex >= length) { return NaN; @@ -62,14 +62,22 @@ export class StringModels { } static slice(receiver: string, start: number, end: number): string { - const length = StringModelPrimitives.length(receiver); + const length = receiver.length; const from = StringModels.normalizeSliceIndex(start, length); const to = StringModels.normalizeSliceIndex(end, length); - return StringModelPrimitives.copyRange(receiver, from, to < from ? from : to); + + let result = ""; + let index = from; + while (index < to) { + result += receiver[index]; + index++; + } + + return result; } static toUpperCase(receiver: string): string { - const length = StringModelPrimitives.length(receiver); + const length = receiver.length; let result = ""; let index = 0; while (index < length) { @@ -84,7 +92,7 @@ export class StringModels { } static toLowerCase(receiver: string): string { - const length = StringModelPrimitives.length(receiver); + const length = receiver.length; let result = ""; let index = 0; while (index < length) { @@ -99,8 +107,8 @@ export class StringModels { } static startsWith(receiver: string, searchString: string, position: number): boolean { - const length = StringModelPrimitives.length(receiver); - const searchLength = StringModelPrimitives.length(searchString); + const length = receiver.length; + const searchLength = searchString.length; const start = StringModels.normalizePosition(position, length); if (start + searchLength > length) { return false; @@ -108,10 +116,10 @@ export class StringModels { let searchIndex = 0; while (searchIndex < searchLength) { - if ( - StringModelPrimitives.codeUnitAt(receiver, start + searchIndex) !== - StringModelPrimitives.codeUnitAt(searchString, searchIndex) - ) { + const character = receiver[start + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { return false; } @@ -122,8 +130,8 @@ export class StringModels { } static endsWith(receiver: string, searchString: string, endPosition: number): boolean { - const length = StringModelPrimitives.length(receiver); - const searchLength = StringModelPrimitives.length(searchString); + const length = receiver.length; + const searchLength = searchString.length; const end = StringModels.normalizePosition(endPosition, length); const start = end - searchLength; if (start < 0) { @@ -132,10 +140,10 @@ export class StringModels { let searchIndex = 0; while (searchIndex < searchLength) { - if ( - StringModelPrimitives.codeUnitAt(receiver, start + searchIndex) !== - StringModelPrimitives.codeUnitAt(searchString, searchIndex) - ) { + const character = receiver[start + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { return false; } @@ -146,8 +154,8 @@ export class StringModels { } static lastIndexOf(receiver: string, searchString: string, position: number): number { - const length = StringModelPrimitives.length(receiver); - const searchLength = StringModelPrimitives.length(searchString); + const length = receiver.length; + const searchLength = searchString.length; let index = StringModels.normalizeLastPosition(position, length); if (index + searchLength > length) { index = length - searchLength; @@ -155,11 +163,14 @@ export class StringModels { while (index >= 0) { let searchIndex = 0; - while ( - searchIndex < searchLength && - StringModelPrimitives.codeUnitAt(receiver, index + searchIndex) === - StringModelPrimitives.codeUnitAt(searchString, searchIndex) - ) { + while (searchIndex < searchLength) { + const character = receiver[index + searchIndex]; + const expectedCharacter = searchString[searchIndex]; + const matches = character === expectedCharacter; + if (!matches) { + break; + } + searchIndex++; } 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..ca55c103d0 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt @@ -0,0 +1,237 @@ +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 `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/TsSequenceEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt index 37b661b393..294409335d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt @@ -153,7 +153,7 @@ class TsSequenceEtsIrModelTest { } @Test - fun `selecting charAt also enables its primitives`() { + fun `selecting charAt only enables position normalization`() { val result = analyze( methodName = "stringCharAtHandlesBounds", tsOptions = TsOptions( @@ -166,9 +166,6 @@ class TsSequenceEtsIrModelTest { setOf( "ts.string.charAt", "ts.math.floor", - "ts.string.primitive.codeUnitAt", - "ts.string.primitive.fromCodeUnit", - "ts.string.primitive.length", ), result.modelIds.toSet(), ) @@ -211,11 +208,14 @@ class TsSequenceEtsIrModelTest { } @Test - fun `symbolic charAt falls back until string value equality is modeled`() { + 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(result.values.isEmpty()) - assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + 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 @@ -362,6 +362,7 @@ class TsSequenceEtsIrModelTest { val machineOptions = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, exceptionsPropagation = true, throwExceptionOnStepFailure = true, timeout = 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 9bb27c8f13..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 @@ -203,9 +203,7 @@ class TsUnknownCallModelCatalogTest { "ts.string.indexOf", "ts.string.lastIndexOf", "ts.string.primitive.codeUnitAt", - "ts.string.primitive.copyRange", "ts.string.primitive.fromCodeUnit", - "ts.string.primitive.length", "ts.string.slice", "ts.string.startsWith", "ts.string.toLowerCase", @@ -236,9 +234,7 @@ class TsUnknownCallModelCatalogTest { "ts.string.indexOf", "ts.string.lastIndexOf", "ts.string.primitive.codeUnitAt", - "ts.string.primitive.copyRange", "ts.string.primitive.fromCodeUnit", - "ts.string.primitive.length", "ts.string.slice", "ts.string.startsWith", "ts.string.toLowerCase", 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..e5c54bce8c --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringIndexing.ts @@ -0,0 +1,79 @@ +export class StringIndexing { + 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(); + } +} From 2f74dcf6042b5ce5a286b4cd8eee53bd336a0c30 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 23:49:14 +0300 Subject: [PATCH 06/10] Preserve sequence call arguments and restrict string helper ownership --- .../org/usvm/machine/call/TsUnknownCall.kt | 8 ++ .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 62 +++++----- .../intrinsic/TsStringEtsIrModelFamily.kt | 117 ++++++++---------- .../machine/call/TsArrayPopEtsIrModelTest.kt | 7 +- .../machine/call/TsSequenceEtsIrModelTest.kt | 75 +++++++++++ .../test/resources/models/SequenceEtsIr.ts | 74 +++++++++++ 6 files changed, 244 insertions(+), 99 deletions(-) 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..f3216930e6 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 argument prefix only after every source argument has been resolved. */ +internal fun TsUnknownCall.resolvedInstanceInputs(maxArgumentCount: Int): List>? { + val resolvedReceiver = receiver?.resolved ?: return null + val resolvedArguments = arguments.map { argument -> argument.resolved ?: return null } + + return listOf(resolvedReceiver) + resolvedArguments.take(maxArgumentCount) +} + /** 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/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index 825fbe8170..b77c5bb9b4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -2,16 +2,15 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType -import org.usvm.UExpr 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.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. */ @@ -37,14 +36,14 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } 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) - if ( - array.hasFakeValueBranch() || receiverType?.dimensions != 1 || + val hasUnsupportedArrayShape = array.hasFakeValueBranch() || receiverType.dimensions != 1 || searchRef?.hasFakeValueBranch() == true - ) { + if (hasUnsupportedArrayShape) { falseExpr } else { val elementSort = typeToSort(receiverType.elementType) @@ -78,31 +77,38 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } + private val receiverOnlyAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + call.resolvedInstanceInputs(maxArgumentCount = 0) + } + private val optionalFromIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> - call.resolvedInstanceInputs()?.let { inputs -> - when { - call.arguments.size == 1 -> inputs + state.ctx.mkFp64(0.0) - call.arguments.size == 2 && inputs.last() == state.ctx.mkUndefinedValue() -> { - inputs.dropLast(1) + state.ctx.mkFp64(0.0) - } + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (inputs.size < 2) { + return@TsEtsIrUnknownCallModelInputAdapter null + } - call.arguments.size == 2 && inputs.last().sort == state.ctx.fp64Sort -> inputs - else -> 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 -> - call.resolvedInstanceInputs()?.let { inputs -> - when { - call.arguments.size == 1 -> inputs + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) - call.arguments.size == 2 && inputs.last() == state.ctx.mkUndefinedValue() -> { - inputs.dropLast(1) + state.ctx.mkFp64(0.0) - } + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (inputs.size < 2) { + return@TsEtsIrUnknownCallModelInputAdapter null + } - call.arguments.size == 2 && inputs.last().sort == state.ctx.fp64Sort -> inputs - else -> 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 } } @@ -111,6 +117,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { sourceModel( id = "ts.array.pop", methodName = "pop", + inputAdapter = receiverOnlyAdapter, ), sourceModel( id = "ts.array.indexOf", @@ -133,7 +140,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private fun sourceModel( id: String, methodName: String, - inputAdapter: TsEtsIrUnknownCallModelInputAdapter = TsEtsIrUnknownCallModelInputAdapter.IDENTITY, + inputAdapter: TsEtsIrUnknownCallModelInputAdapter, ): TsUnknownCallModel { val target = TsUnknownCallTarget( methodName = methodName, @@ -161,12 +168,5 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { return artifact.copy(entryPoint = entryPoint) } - private fun TsUnknownCall.resolvedInstanceInputs(): List>? { - val resolvedReceiver = receiver?.resolved ?: return null - val resolvedArguments = arguments.map { argument -> argument.resolved ?: return null } - - return listOf(resolvedReceiver) + resolvedArguments - } - private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index 88931e4fb0..74e953913f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -18,6 +18,7 @@ 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 @@ -40,76 +41,73 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + private val primitiveClassSignature by lazy { + baseArtifact.file.allClasses.single { it.name == PRIMITIVES_CLASS_NAME }.signature + } + private val optionalIndexAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> - call.resolvedInstanceInputs()?.let { inputs -> - when { - call.arguments.isEmpty() -> inputs + state.ctx.mkFp64(0.0) - call.arguments.size == 1 && inputs.last() == state.ctx.mkUndefinedValue() -> { - inputs.dropLast(1) + state.ctx.mkFp64(0.0) - } + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 1) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val index = inputs.getOrNull(1) - call.arguments.size == 1 && inputs.last().sort == state.ctx.fp64Sort -> inputs - else -> null - } + 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 -> - call.resolvedInstanceInputs()?.let { inputs -> - when { - call.arguments.size == 1 && inputs.last().sort == state.ctx.addressSort -> { - inputs + state.ctx.mkFp64(0.0) - } - - call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && - inputs.last() == state.ctx.mkUndefinedValue() -> { - inputs.dropLast(1) + state.ctx.mkFp64(0.0) - } - - call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && - inputs.last().sort == state.ctx.fp64Sort -> inputs + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val search = inputs.getOrNull(1) + if (search?.sort != state.ctx.addressSort) { + return@TsEtsIrUnknownCallModelInputAdapter null + } - else -> 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 -> - call.resolvedInstanceInputs()?.let { inputs -> - when { - call.arguments.size == 1 && inputs.last().sort == state.ctx.addressSort -> { - inputs + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) - } - - call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && - inputs.last() == state.ctx.mkUndefinedValue() -> { - inputs.dropLast(1) + state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort) - } - - call.arguments.size == 2 && inputs[1].sort == state.ctx.addressSort && - inputs.last().sort == state.ctx.fp64Sort -> inputs + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val search = inputs.getOrNull(1) + if (search?.sort != state.ctx.addressSort) { + return@TsEtsIrUnknownCallModelInputAdapter null + } - else -> 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() ?: return@TsEtsIrUnknownCallModelInputAdapter null + 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) - if (arguments.size > 2) { + 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 when { - value == state.ctx.mkUndefinedValue() -> default - value.sort == state.ctx.fp64Sort -> value - else -> return default - } + return if (value == state.ctx.mkUndefinedValue()) default else value } val start = numericOrDefault(index = 0, default = state.ctx.mkFp64(0.0)) @@ -117,22 +115,12 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { index = 1, default = state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort), ) - val hasUnsupportedArgument = arguments.any { value -> - value != state.ctx.mkUndefinedValue() && value.sort != state.ctx.fp64Sort - } - if (hasUnsupportedArgument) { - return@TsEtsIrUnknownCallModelInputAdapter null - } listOf(receiver, start, end) } - private val noArgumentsAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> - if (call.arguments.isNotEmpty()) { - null - } else { - call.resolvedInstanceInputs() - } + private val receiverOnlyAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + call.resolvedInstanceInputs(maxArgumentCount = 0) } private fun stringDomain(state: TsState, input: UExpr<*>?): org.usvm.UBoolExpr = with(state.ctx) { @@ -248,13 +236,13 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { sourceModel( id = "ts.string.toUpperCase", methodName = "toUpperCase", - inputAdapter = noArgumentsAdapter, + inputAdapter = receiverOnlyAdapter, domainGuard = asciiReceiverDomain, ), sourceModel( id = "ts.string.toLowerCase", methodName = "toLowerCase", - inputAdapter = noArgumentsAdapter, + inputAdapter = receiverOnlyAdapter, domainGuard = asciiReceiverDomain, ), primitiveModel( @@ -391,13 +379,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } - private fun TsUnknownCall.resolvedInstanceInputs(): List>? { - val resolvedReceiver = receiver?.resolved ?: return null - val resolvedArguments = arguments.map { argument -> argument.resolved ?: return null } - - return listOf(resolvedReceiver) + resolvedArguments - } - private class StringPrimitiveModel( methodName: String, private val arity: Int, @@ -411,6 +392,10 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) 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 } 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..dd4f009a15 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 diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt index 294409335d..73b8be2c2a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt @@ -27,6 +27,81 @@ class TsSequenceEtsIrModelTest { ) 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 result = analyze(methodName = "arraySearchesEvaluateIgnoredArguments") + + assertTrue(assertIs(result.values.single()).value) + assertTrue(setOf("ts.array.indexOf", "ts.array.includes", "ts.array.lastIndexOf").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") diff --git a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts index 9c6cbde6c6..6d1741fb75 100644 --- a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts +++ b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts @@ -1,7 +1,81 @@ // @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 From cacdae80cffe7072a1467539f4101fbe7ecedc90 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 23:50:00 +0300 Subject: [PATCH 07/10] Read only meaningful resolved sequence argument slots --- .../src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 f3216930e6..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,12 +47,12 @@ data class TsUnknownCallValue( val resolved: UExpr<*>?, ) -/** Takes the meaningful argument prefix only after every source argument has been resolved. */ +/** 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.map { argument -> argument.resolved ?: return null } + val resolvedArguments = arguments.take(maxArgumentCount).map { argument -> argument.resolved ?: return null } - return listOf(resolvedReceiver) + resolvedArguments.take(maxArgumentCount) + return listOf(resolvedReceiver) + resolvedArguments } /** Identifies the execution stage that prevented a TypeScript call from continuing normally. */ From e700710d60d59d381080cd967d1e6eebe2c8b821 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 00:10:42 +0300 Subject: [PATCH 08/10] Clean up sequence model regression assertions --- .../org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt | 10 ---------- .../org/usvm/machine/call/TsSequenceEtsIrModelTest.kt | 4 +++- 2 files changed, 3 insertions(+), 11 deletions(-) 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 dd4f009a15..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 @@ -278,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 index 73b8be2c2a..35898cee0e 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt @@ -57,10 +57,12 @@ class TsSequenceEtsIrModelTest { @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(setOf("ts.array.indexOf", "ts.array.includes", "ts.array.lastIndexOf").all(result.modelIds::contains)) + assertTrue(expectedModels.all(result.modelIds::contains)) } @Test From e1be364964f304ff9636feabf7a489068e7d3f5f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:32:52 +0300 Subject: [PATCH 09/10] Own isolated surrogate and out-of-range checks with string indexing --- .../org/usvm/machine/TsStringIndexingTest.kt | 18 ++++++++++++++++++ .../test/resources/models/StringIndexing.ts | 8 ++++++++ 2 files changed, 26 insertions(+) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt index ca55c103d0..a37aa0cfca 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexingTest.kt @@ -49,6 +49,24 @@ class TsStringIndexingTest : TsMethodTestRunner() { ) } + @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( diff --git a/usvm-ts/src/test/resources/models/StringIndexing.ts b/usvm-ts/src/test/resources/models/StringIndexing.ts index e5c54bce8c..c0849a1beb 100644 --- a/usvm-ts/src/test/resources/models/StringIndexing.ts +++ b/usvm-ts/src/test/resources/models/StringIndexing.ts @@ -1,4 +1,12 @@ 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" && From ac52b314bb28719a74dcb0c7ce9a677f6d836fb6 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 12:46:54 +0300 Subject: [PATCH 10/10] Preserve fresh-string bounds after sequence model rebase --- usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 }