From a928cc605cb223a007a9dc886064fe71617c1129 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 8 Oct 2026 00:41:22 +0300 Subject: [PATCH] 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/TsArrayShiftMatrixTest.kt | 10 +- .../machine/call/TsSequenceEtsIrModelTest.kt | 304 ++++++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 42 ++ .../test/resources/models/SequenceEtsIr.ts | 131 +++++++ 14 files changed, 1442 insertions(+), 84 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 ec72f82efb..c7c8d4ca5d 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/TsArrayShiftMatrixTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt index 312b88dbd7..51c72deea0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt @@ -66,9 +66,15 @@ class TsArrayShiftMatrixTest { } val actual = values.map { assertIs(it).number } + val removalDecision = TsUnknownCallDecision.ModelApplied(modelId = "ts.array.$methodName") + val allowedDecisions = setOf( + removalDecision, + TsUnknownCallDecision.ModelApplied(modelId = "ts.number.isNaN"), + ) + assertEquals(listOf(expected[index].toDouble()), actual) - assertEquals(case.shiftCount, events.size) - assertTrue(events.all { it.decision == TsUnknownCallDecision.ModelApplied("ts.array.$methodName") }) + assertEquals(case.shiftCount, events.count { it.decision == removalDecision }) + assertTrue(events.all { it.decision in allowedDecisions }) } } } 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 77d8018b3a..8b167083db 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,6 +178,9 @@ class TsUnknownCallModelCatalogTest { val catalog = TsBuiltInUnknownCallModels.catalog() val expectedModelIds = listOf( + "ts.array.includes", + "ts.array.indexOf", + "ts.array.lastIndexOf", "ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID, TsNumericIntrinsicModelFamily.MATH_ABS_ID, @@ -166,6 +195,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) @@ -280,6 +319,7 @@ class TsUnknownCallModelCatalogTest { failureReason: TsUnknownCallFailureReason? = null, className: String? = null, additionalSceneFiles: List = emptyList(), + requiredModelIds: Set = emptySet(), ): TsUnknownCallModel = FakeModel( id = id, target = TsUnknownCallTarget( @@ -288,12 +328,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); + } +}