[TS Calls] Add guarded semantic model registry and execution

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

@@ -8,35 +8,46 @@ 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(
     scope: TsStepScope,
     method: EtsMethodSignature,
     resultType: EtsType = method.returnType,
 ) {
+    val result = makeFreshUnknownCallResult(scope, resultType)
+
     scope.doWithState {
-        val result: UExpr<*>
-        if (resultType is EtsVoidType) {
-            result = ctx.mkUndefinedValue()
-        } else {
-            val sort = ctx.typeToSort(resultType)
-            result = when (sort) {
-                is UAddressSort -> makeSymbolicRefUntyped()
-
-                is TsUnresolvedSort -> scope.calcOnState {
-                    mkFakeValue(
-                        scope = scope,
-                        boolValue = makeSymbolicPrimitive(ctx.boolSort),
-                        fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
-                        refValue = makeSymbolicRefUntyped(),
-                    )
-                }
-
-                else -> makeSymbolicPrimitive(sort)
-            }
-        }
-
-        methodResult = TsMethodResult.Success.MockedCall(result, method)
+        setMockMethodCallResult(method, result)
+    }
+}
+
+/** Stores a prepared opaque result on this state without applying callee effects or exceptions. */
+internal fun TsState.setMockMethodCallResult(
+    method: EtsMethodSignature,
+    result: UExpr<*>,
+) {
+    methodResult = TsMethodResult.Success.MockedCall(result, method)
+}
+
+/** Creates a fresh opaque result through [scope], keeping solver models consistent with new constraints. */
+internal fun makeFreshUnknownCallResult(
+    scope: TsStepScope,
+    resultType: EtsType,
+): UExpr<*> = scope.calcOnState {
+    if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue()
+
+    when (val sort = ctx.typeToSort(resultType)) {
+        is UAddressSort -> makeSymbolicRefUntyped()
+
+        is TsUnresolvedSort -> mkFakeValue(
+            scope,
+            boolValue = makeSymbolicPrimitive(ctx.boolSort),
+            fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
+            refValue = makeSymbolicRefUntyped(),
+        )
+
+        else -> makeSymbolicPrimitive(sort)
     }
 }

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

@@ -183,6 +183,12 @@ class TsContext(
     fun UConcreteHeapRef.getFakeType(scope: TsStepScope): EtsFakeType =
         scope.calcOnState { getFakeType(memory) }
 
+    /**
+     * Returns whether this expression is the storage identity of a synthetic fake-value wrapper.
+     *
+     * A positive result says nothing about the wrapper's active runtime kind. In particular, the expression must not
+     * be used as the represented object reference; inspect [EtsFakeType.refTypeExpr] and extract the reference payload.
+     */
     @OptIn(ExperimentalContracts::class)
     fun UExpr<*>.isFakeObject(): Boolean {
         contract {
@@ -238,13 +244,22 @@ class TsContext(
         }
     }
 
+    /**
+     * Returns the reference payload of a fake-value wrapper without adding a reference-kind constraint.
+     *
+     * Use this only when [EtsFakeType.refTypeExpr] is already known or the caller guards the result equivalently.
+     * Otherwise use [unwrapRefWithPathConstraint].
+     */
     fun UHeapRef.unwrapRef(scope: TsStepScope): UHeapRef {
         if (isFakeObject()) {
             return extractRef(scope)
         }
         return this
     }
 
+    /**
+     * Extracts the reference payload from a fake-value wrapper and constrains that wrapper to the reference kind.
+     */
     fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef {
         if (isFakeObject()) {
             scope.assert(getFakeType(scope).refTypeExpr)
@@ -285,6 +300,12 @@ class TsContext(
         return memory.read(lValue)
     }
 
+    /**
+     * Reads the reference payload without constraining [EtsFakeType.refTypeExpr].
+     *
+     * This operation alone does not prove that the wrapped value is a reference. The caller must either assert the
+     * discriminator through a live [TsStepScope] or use the payload only under an equivalent guard.
+     */
     fun UConcreteHeapRef.extractRef(memory: UReadOnlyMemory<*>): UHeapRef {
         check(isFakeObject())
         val lValue = getIntermediateRefLValue(address)
@@ -299,6 +320,7 @@ class TsContext(
         return scope.calcOnState { extractFp(memory) }
     }
 
+    /** Reads the reference payload through [scope] without adding a reference-kind constraint. */
     fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
         return scope.calcOnState { extractRef(memory) }
     }

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(
@@ -62,6 +74,7 @@ class TsMachine(
         options = tsOptions,
         observer = observer,
         unknownCallDispatcher = resolvedUnknownCallDispatcher,
+        throwExceptionOnStepFailure = options.throwExceptionOnStepFailure,
     )
     private val cfgStatistics = CfgStatisticsImpl(graph)
 

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/TsBuiltInUnknownCallModels.kt

@@ -0,0 +1,14 @@
+package org.usvm.machine.call
+
+import org.usvm.machine.call.intrinsic.TsArrayPopIntrinsicModel
+import org.usvm.machine.call.intrinsic.TsIntrinsicUnknownCallModelBackend
+
+/** The intentionally small built-in catalog enabled by default for profile-based unknown-call dispatch. */
+object TsBuiltInUnknownCallModels {
+    const val ARRAY_POP_MODEL_ID: String = TsArrayPopIntrinsicModel.MODEL_ID
+
+    val registry = TsUnknownCallModelRegistry(
+        registrations = listOf(TsArrayPopIntrinsicModel.registration),
+        backends = listOf(TsIntrinsicUnknownCallModelBackend),
+    )
+}

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")
+            }
         }
     }
 }
@@ -152,10 +160,10 @@ internal fun TsUnknownCallDispatcher.dispatch(
     failureReason: TsUnknownCallFailureReason,
     resolvedReceiver: UExpr<*>,
 ) = dispatch(
-    scope = scope,
-    call = call.call,
-    callSite = call.returnSite,
-    failureReason = failureReason,
+    scope,
+    call.call,
+    call.returnSite,
+    failureReason,
     resolvedReceiver = resolvedReceiver,
     resolvedArguments = call.args,
 )
@@ -166,11 +174,11 @@ internal fun TsUnknownCallDispatcher.dispatch(
     failureReason: TsUnknownCallFailureReason,
     callee: EtsMethodSignature,
 ) = dispatch(
-    scope = scope,
-    call = call.call,
-    callSite = call.returnSite,
-    failureReason = failureReason,
-    callee = callee,
+    scope,
+    call.call,
+    call.returnSite,
+    failureReason,
+    callee,
     resolvedReceiver = call.resolvedReceiver,
     resolvedArguments = call.args.takeLast(call.call.args.size),
 )

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

@@ -0,0 +1,117 @@
+package org.usvm.machine.call
+
+import org.jacodb.ets.model.EtsType
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.machine.state.TsState
+
+/** Identifies the backend that executes a semantic model implementation. */
+enum class TsUnknownCallModelImplementationKind {
+    INTRINSIC,
+}
+
+/** Describes the semantic precision of a model within its declared supported domain. */
+enum class TsUnknownCallModelPrecision {
+    EXACT,
+    PARTIAL,
+}
+
+/** Documents the inputs for which a semantic model provides its declared precision. */
+data class TsUnknownCallModelSupportedDomain(
+    val id: String,
+    val description: String,
+) {
+    init {
+        require(id.isNotBlank()) { "Semantic model supported-domain ID must not be blank" }
+        require(description.isNotBlank()) { "Semantic model supported-domain description must not be blank" }
+    }
+}
+
+/** Selects calls that are candidates for one semantic model without depending on its implementation backend. */
+fun interface TsUnknownCallModelMatcher {
+    fun matches(call: TsUnknownCall): Boolean
+}
+
+/** Backend-neutral metadata used to select and audit one semantic model. */
+class TsUnknownCallModelDescriptor(
+    val id: String,
+    val matcher: TsUnknownCallModelMatcher,
+    val supportedDomain: TsUnknownCallModelSupportedDomain,
+    val precision: TsUnknownCallModelPrecision,
+    val implementationKind: TsUnknownCallModelImplementationKind,
+) {
+    init {
+        require(id.isNotBlank()) { "Semantic model ID must not be blank" }
+    }
+}
+
+/** Describes how a guarded model successor completes the original call. */
+sealed interface TsUnknownCallModelCompletion {
+    /** Produces a normal result on the selected successor state. */
+    class Normal(
+        val result: TsState.() -> UExpr<*>,
+    ) : TsUnknownCallModelCompletion
+
+    /** Produces an exceptional result and its TypeScript type on the selected successor state. */
+    class Exceptional(
+        val exception: TsState.() -> Pair<UExpr<*>, EtsType>,
+    ) : TsUnknownCallModelCompletion
+}
+
+/**
+ * One guarded model successor.
+ *
+ * Successor guards within one execution must be pairwise disjoint. State changes and completion values are evaluated
+ * only after the dispatcher has selected the corresponding successor state.
+ */
+class TsUnknownCallModelSuccessor(
+    val guard: UBoolExpr,
+    val completion: TsUnknownCallModelCompletion,
+    val applyStateChanges: TsState.() -> Unit = {},
+)
+
+/**
+ * A backend-neutral semantic-model execution plan.
+ *
+ * [residualGuard] denotes the unsupported part of a partial model's domain. Together, successor guards and the
+ * residual guard must partition the current call domain. The dispatcher validates disjointness and coverage before
+ * applying any successor.
+ */
+class TsUnknownCallModelExecution(
+    successors: List<TsUnknownCallModelSuccessor>,
+    val residualGuard: UBoolExpr?,
+) {
+    val successors: List<TsUnknownCallModelSuccessor> = successors.toList()
+
+    init {
+        require(this.successors.isNotEmpty()) { "A semantic model must declare at least one guarded successor" }
+    }
+}
+
+/** The result of selecting and executing a semantic model for one call. */
+sealed interface TsUnknownCallModelApplication {
+    /** A structured guarded plan produced by the selected model. */
+    class Applied(
+        val modelId: String,
+        val precision: TsUnknownCallModelPrecision,
+        val execution: TsUnknownCallModelExecution,
+    ) : TsUnknownCallModelApplication {
+        init {
+            require(modelId.isNotBlank()) { "Applied model ID must not be blank" }
+            require(precision != TsUnknownCallModelPrecision.EXACT || execution.residualGuard == null) {
+                "Exact semantic model $modelId must not produce a residual guard"
+            }
+            require(precision != TsUnknownCallModelPrecision.PARTIAL || execution.residualGuard != null) {
+                "Partial semantic model $modelId must produce a residual guard"
+            }
+        }
+    }
+
+    /** Indicates that no enabled model matched the call. */
+    data object NotApplicable : TsUnknownCallModelApplication
+}
+
+/** Selects and executes models without exposing registry or backend details to the dispatcher. */
+fun interface TsUnknownCallModelProvider {
+    fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication
+}