[TS Calls] Add guarded semantic model registry and execution

usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt

@@ -8,6 +8,7 @@ import org.usvm.UExpr
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.TsState
 import org.usvm.machine.types.mkFakeValue
 
 fun mockMethodCall(
@@ -16,27 +17,34 @@ fun mockMethodCall(
     resultType: EtsType = method.returnType,
 ) {
     scope.doWithState {
-        val result: UExpr<*>
-        if (resultType is EtsVoidType) {
-            result = ctx.mkUndefinedValue()
-        } else {
-            val sort = ctx.typeToSort(resultType)
-            result = when (sort) {
-                is UAddressSort -> makeSymbolicRefUntyped()
+        mockMethodCall(method = method, resultType = resultType)
+    }
+}
+
+/** Creates a fresh opaque result directly on this state without applying callee effects or exceptions. */
+fun TsState.mockMethodCall(
+    method: EtsMethodSignature,
+    resultType: EtsType = method.returnType,
+) {
+    val result = freshUnknownCallResult(resultType)
+    methodResult = TsMethodResult.Success.MockedCall(result, method)
+}
+
+private fun TsState.freshUnknownCallResult(resultType: EtsType): UExpr<*> {
+    if (resultType is EtsVoidType) {
+        return ctx.mkUndefinedValue()
+    }
 
-                is TsUnresolvedSort -> scope.calcOnState {
-                    mkFakeValue(
-                        scope = scope,
-                        boolValue = makeSymbolicPrimitive(ctx.boolSort),
-                        fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
-                        refValue = makeSymbolicRefUntyped(),
-                    )
-                }
+    return when (val sort = ctx.typeToSort(resultType)) {
+        is UAddressSort -> makeSymbolicRefUntyped()
 
-                else -> makeSymbolicPrimitive(sort)
-            }
-        }
+        is TsUnresolvedSort -> mkFakeValue(
+            scope = null,
+            boolValue = makeSymbolicPrimitive(ctx.boolSort),
+            fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
+            refValue = makeSymbolicRefUntyped(),
+        )
 
-        methodResult = TsMethodResult.Success.MockedCall(result, method)
+        else -> makeSymbolicPrimitive(sort)
     }
 }

usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

@@ -9,6 +9,7 @@ import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
 import org.usvm.api.targets.TsTarget
+import org.usvm.machine.call.TsBuiltInUnknownCallModels
 import org.usvm.machine.call.TsNoUnknownCallModels
 import org.usvm.machine.call.TsProfileUnknownCallDispatcher
 import org.usvm.machine.call.TsUnknownCallDispatcher
@@ -45,15 +46,26 @@ class TsMachine(
     private val machineObserver: UMachineObserver<TsState>? = null,
     observer: TsInterpreterObserver? = null,
     unknownCallDispatcher: TsUnknownCallDispatcher? = null,
-    unknownCallModelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels,
+    unknownCallModelProvider: TsUnknownCallModelProvider? = null,
 ) : UMachine<TsState>() {
     private val graph = TsGraph(scene)
     private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy)
     private val components = TsComponents(typeSystem, options)
     private val ctx = TsContext(scene, components)
+    private val frozenUnknownCallModels = when {
+        unknownCallDispatcher != null || unknownCallModelProvider != null -> null
+        else -> TsBuiltInUnknownCallModels.registry.freeze(tsOptions.unknownCallModels.enabledModelIds)
+    }
+
+    /** Fingerprint of the frozen built-in catalog, or `null` when custom dispatch/model wiring is used. */
+    val unknownCallModelCatalogFingerprint: String?
+        get() = frozenUnknownCallModels?.fingerprint
+
+    private val resolvedUnknownCallModelProvider =
+        unknownCallModelProvider ?: frozenUnknownCallModels ?: TsNoUnknownCallModels
     private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher(
         profile = tsOptions.unknownCallProfile,
-        modelProvider = unknownCallModelProvider,
+        modelProvider = resolvedUnknownCallModelProvider,
         observer = observer,
     )
     private val interpreter = TsInterpreter(

usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt

@@ -1,5 +1,6 @@
 package org.usvm.machine
 
+import org.usvm.machine.call.TsUnknownCallModelSelection
 import org.usvm.machine.call.TsUnknownCallProfile
 import org.usvm.machine.call.TsUnknownCallProfiles
 
@@ -8,4 +9,5 @@ data class TsOptions(
     val enableVisualization: Boolean = false,
     val maxArraySize: Int = 1_000,
     val unknownCallProfile: TsUnknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP,
+    val unknownCallModels: TsUnknownCallModelSelection = TsUnknownCallModelSelection(),
 )

usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt

@@ -0,0 +1,158 @@
+package org.usvm.machine.call
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
+import org.usvm.UAddressSort
+import org.usvm.UExpr
+import org.usvm.USort
+import org.usvm.api.typeStreamOf
+import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.state.TsState
+import org.usvm.types.firstOrNull
+import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
+
+/** Builds constraint-level execution plans directly from a TypeScript symbolic state. */
+fun interface TsIntrinsicUnknownCallModel {
+    fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution
+}
+
+/** Opaque registry handle for a Kotlin intrinsic semantic model. */
+class TsIntrinsicUnknownCallModelImplementation(
+    val model: TsIntrinsicUnknownCallModel,
+) : TsUnknownCallModelImplementation {
+    override val kind: TsUnknownCallModelImplementationKind =
+        TsUnknownCallModelImplementationKind.INTRINSIC
+}
+
+/** Executes intrinsic model handles without exposing them to the common registry or dispatcher contract. */
+object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend {
+    override val kind: TsUnknownCallModelImplementationKind =
+        TsUnknownCallModelImplementationKind.INTRINSIC
+
+    override fun execute(
+        implementation: TsUnknownCallModelImplementation,
+        state: TsState,
+        call: TsUnknownCall,
+    ): TsUnknownCallModelExecution {
+        val intrinsic = requireNotNull(implementation as? TsIntrinsicUnknownCallModelImplementation) {
+            "INTRINSIC backend requires TsIntrinsicUnknownCallModelImplementation, got ${implementation::class}"
+        }
+
+        return intrinsic.model.execute(state = state, call = call)
+    }
+}
+
+/** The intentionally small built-in catalog enabled by default for profile-based unknown-call dispatch. */
+object TsBuiltInUnknownCallModels {
+    const val ARRAY_POP_MODEL_ID: String = "ts.array.pop"
+
+    private val arrayPopDescriptor = TsUnknownCallModelDescriptor(
+        id = ARRAY_POP_MODEL_ID,
+        matcher = TsUnknownCallModelMatcher { call ->
+            call.failureReason == TsUnknownCallFailureReason.PARTIAL_APPROXIMATION &&
+                call.callee.name == "pop"
+        },
+        supportedDomain = TsUnknownCallModelSupportedDomain(
+            id = "native-array-pop",
+            description = "Resolved one-dimensional native arrays with no arguments and a resolved element sort",
+        ),
+        precision = TsUnknownCallModelPrecision.PARTIAL,
+        implementationKind = TsUnknownCallModelImplementationKind.INTRINSIC,
+    )
+
+    val registry = TsUnknownCallModelRegistry(
+        registrations = listOf(
+            TsUnknownCallModelRegistration(
+                descriptor = arrayPopDescriptor,
+                implementation = TsIntrinsicUnknownCallModelImplementation(TsArrayPopIntrinsicModel),
+            ),
+        ),
+        backends = listOf(TsIntrinsicUnknownCallModelBackend),
+    )
+}
+
+private object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel {
+    override fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution {
+        val input = resolveInput(state = state, call = call)
+            ?: return unsupportedExecution(state)
+
+        val lengthLValue = mkArrayLengthLValue(input.array, input.arrayType)
+        val length = state.memory.read(lengthLValue)
+        val zero = state.ctx.mkBv(0)
+        val emptyGuard = state.ctx.mkEq(length, zero)
+        val nonEmptyGuard = state.ctx.mkBvSignedLessExpr(zero, length)
+        val residualGuard = state.ctx.mkNot(state.ctx.mkOr(emptyGuard, nonEmptyGuard))
+        val newLength = state.ctx.mkBvSubExpr(length, state.ctx.mkBv(1))
+        val lastElementLValue = mkArrayIndexLValue(
+            sort = input.elementSort,
+            ref = input.array,
+            index = newLength,
+            type = input.arrayType,
+        )
+
+        val emptySuccessor = TsUnknownCallModelSuccessor(
+            guard = emptyGuard,
+            completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() },
+        )
+        val nonEmptySuccessor = TsUnknownCallModelSuccessor(
+            guard = nonEmptyGuard,
+            completion = TsUnknownCallModelCompletion.Normal { memory.read(lastElementLValue) },
+            applyStateChanges = {
+                memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
+            },
+        )
+
+        return TsUnknownCallModelExecution(
+            successors = listOf(emptySuccessor, nonEmptySuccessor),
+            residualGuard = residualGuard,
+        )
+    }
+
+    private fun resolveInput(state: TsState, call: TsUnknownCall): ArrayPopInput? {
+        if (call.arguments.isNotEmpty()) {
+            return null
+        }
+
+        val receiverValue = call.receiver?.resolved ?: return null
+        if (receiverValue.sort != state.ctx.addressSort) {
+            return null
+        }
+
+        val array = receiverValue.asExpr(state.ctx.addressSort)
+        val sourceType = requireNotNull(call.receiver).source.type
+        val memoryType = state.memory.typeStreamOf(array).firstOrNull()
+        val arrayType = sequenceOf(memoryType, sourceType)
+            .mapNotNull { it as? EtsArrayType }
+            .firstOrNull { candidate ->
+                candidate.dimensions == 1 && state.ctx.typeToSort(candidate.elementType) !is TsUnresolvedSort
+            }
+            ?: return null
+
+        val elementSort = state.ctx.typeToSort(arrayType.elementType)
+
+        return ArrayPopInput(
+            array = array,
+            arrayType = arrayType,
+            elementSort = elementSort,
+        )
+    }
+
+    private fun unsupportedExecution(state: TsState): TsUnknownCallModelExecution {
+        val unreachableSuccessor = TsUnknownCallModelSuccessor(
+            guard = state.ctx.falseExpr,
+            completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() },
+        )
+
+        return TsUnknownCallModelExecution(
+            successors = listOf(unreachableSuccessor),
+            residualGuard = state.ctx.trueExpr,
+        )
+    }
+
+    private class ArrayPopInput(
+        val array: UExpr<UAddressSort>,
+        val arrayType: EtsArrayType,
+        val elementSort: USort,
+    )
+}

usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt

@@ -60,13 +60,17 @@ enum class TsUnknownCallFailureReason {
     METHOD_BODY_UNAVAILABLE,
     INTERPROCEDURAL_ANALYSIS_DISABLED,
     LOGGING_CALL,
+    PARTIAL_APPROXIMATION,
 }
 
 /** Handles TypeScript calls that could not be executed by the regular call pipeline. */
 fun interface TsUnknownCallDispatcher {
     fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome
 }
 
+/** Marks profile dispatchers that replace migrated compatibility approximations with registered models. */
+interface TsUnknownCallModelDispatcher : TsUnknownCallDispatcher
+
 /** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */
 object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
     override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome {
@@ -109,6 +113,10 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
                 scope.assert(falseExpr)
                 return TsUnknownCallOutcome.PATH_STOPPED
             }
+
+            TsUnknownCallFailureReason.PARTIAL_APPROXIMATION -> {
+                error("Migrated approximations must not be sent to the compatibility dispatcher")
+            }
         }
     }
 }