[TS] Model Array and String operations with guarded fallback

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<String>
 
     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.
 

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<String> = emptySet(),
 ) : TsUnknownCallModel, TsMachineLocalUnknownCallModel {
     override val additionalSceneFiles: List<EtsFile> = listOf(artifact.file)
+    override val requiredModelIds: Set<String> = 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<UExpr<*>>,
     ): List<UExpr<*>>?
 
     companion object {
-        val IDENTITY = TsEtsIrUnknownCallModelInputAdapter { _, _, resolvedInputs -> resolvedInputs }
+        val IDENTITY = TsEtsIrUnknownCallModelInputAdapter { _, call -> call.resolvedInputs() }
     }
 }
 

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<String>
+        get() = emptySet()
 
     /** EtsIR files that must be visible to the interpreter while this model is enabled. */
     val additionalSceneFiles: List<EtsFile>

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<String>()
+                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)
 

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<TsUnknownCallModel> 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<UExpr<*>>? {
+        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"
+}