[TS Calls] Define model selection and residual fallback profiles

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

@@ -1,6 +1,7 @@
 package org.usvm.api
 
 import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsVoidType
 import org.usvm.UAddressSort
 import org.usvm.UExpr
@@ -12,13 +13,14 @@ import org.usvm.machine.types.mkFakeValue
 fun mockMethodCall(
     scope: TsStepScope,
     method: EtsMethodSignature,
+    resultType: EtsType = method.returnType,
 ) {
     scope.doWithState {
         val result: UExpr<*>
-        if (method.returnType is EtsVoidType) {
+        if (resultType is EtsVoidType) {
             result = ctx.mkUndefinedValue()
         } else {
-            val sort = ctx.typeToSort(method.returnType)
+            val sort = ctx.typeToSort(resultType)
             result = when (sort) {
                 is UAddressSort -> makeSymbolicRefUntyped()
 

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

@@ -9,8 +9,10 @@ import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
 import org.usvm.api.targets.TsTarget
-import org.usvm.machine.call.TsCompatibilityUnknownCallDispatcher
+import org.usvm.machine.call.TsNoUnknownCallModels
+import org.usvm.machine.call.TsProfileUnknownCallDispatcher
 import org.usvm.machine.call.TsUnknownCallDispatcher
+import org.usvm.machine.call.TsUnknownCallModelProvider
 import org.usvm.machine.interpreter.TsInterpreter
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
@@ -42,13 +44,18 @@ class TsMachine(
     private val tsOptions: TsOptions,
     private val machineObserver: UMachineObserver<TsState>? = null,
     observer: TsInterpreterObserver? = null,
-    unknownCallDispatcher: TsUnknownCallDispatcher = TsCompatibilityUnknownCallDispatcher,
+    unknownCallDispatcher: TsUnknownCallDispatcher? = null,
+    unknownCallModelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels,
 ) : 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 interpreter = TsInterpreter(ctx, graph, tsOptions, observer, unknownCallDispatcher)
+    private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher(
+        tsOptions.unknownCallProfile,
+        unknownCallModelProvider,
+    )
+    private val interpreter = TsInterpreter(ctx, graph, tsOptions, observer, resolvedUnknownCallDispatcher)
     private val cfgStatistics = CfgStatisticsImpl(graph)
 
     fun analyze(

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

@@ -1,7 +1,11 @@
 package org.usvm.machine
 
+import org.usvm.machine.call.TsUnknownCallProfile
+import org.usvm.machine.call.TsUnknownCallProfiles
+
 data class TsOptions(
     val interproceduralAnalysis: Boolean = true,
     val enableVisualization: Boolean = false,
     val maxArraySize: Int = 1_000,
+    val unknownCallProfile: TsUnknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP,
 )

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

@@ -64,12 +64,12 @@ enum class TsUnknownCallFailureReason {
 
 /** Handles TypeScript calls that could not be executed by the regular call pipeline. */
 fun interface TsUnknownCallDispatcher {
-    fun dispatch(scope: TsStepScope, call: TsUnknownCall)
+    fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome
 }
 
 /** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */
 object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
-    override fun dispatch(scope: TsStepScope, call: TsUnknownCall) {
+    override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome {
         val isUnresolvedConstructor = call.failureReason == TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND &&
             call.callee.name == CONSTRUCTOR_NAME
 
@@ -81,7 +81,7 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
                 methodResult = TsMethodResult.Success.MockedCall(receiver, call.callee)
                 newStmt(call.callSite)
             }
-            return
+            return TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN
         }
 
         when (call.failureReason) {
@@ -94,6 +94,7 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
             -> {
                 mockMethodCall(scope, call.callee)
                 scope.doWithState { newStmt(call.callSite) }
+                return TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN
             }
 
             TsUnknownCallFailureReason.STATIC_METHOD_NOT_FOUND,
@@ -106,6 +107,7 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
             -> {
                 val falseExpr = scope.calcOnState { ctx.falseExpr }
                 scope.assert(falseExpr)
+                return TsUnknownCallOutcome.PATH_STOPPED
             }
         }
     }
@@ -119,7 +121,7 @@ internal fun TsUnknownCallDispatcher.dispatch(
     callee: EtsMethodSignature = call.callee,
     resolvedReceiver: UExpr<*>? = null,
     resolvedArguments: List<UExpr<*>?> = List(call.args.size) { null },
-) {
+): TsUnknownCallOutcome {
     require(resolvedArguments.size == call.args.size) {
         "Expected ${call.args.size} resolved argument slots, got ${resolvedArguments.size}"
     }
@@ -129,7 +131,7 @@ internal fun TsUnknownCallDispatcher.dispatch(
         is EtsPtrCallExpr -> call.ptr
         else -> null
     }
-    dispatch(
+    return dispatch(
         scope,
         TsUnknownCall(
             callee = callee,

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

@@ -0,0 +1,111 @@
+package org.usvm.machine.call
+
+import org.jacodb.ets.model.EtsClassSignature
+import org.usvm.api.mockMethodCall
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.newStmt
+
+/** The externally observable decision made for a call that could not be executed normally. */
+enum class TsUnknownCallOutcome {
+    MODEL_APPLIED,
+    FRESH_SYMBOLIC_RETURN,
+    PATH_STOPPED,
+}
+
+/** Controls whether the dispatcher asks the configured model provider to handle a call. */
+enum class TsUnknownCallModelLookup {
+    DISABLED,
+    ENABLED,
+}
+
+/**
+ * Selects what happens when model lookup is disabled or no model applies.
+ *
+ * [FRESH_SYMBOLIC_RETURN] creates a new symbolic value of the call expression's result type and advances past the
+ * call. It deliberately ignores all callee side effects and exceptions, so it is an opaque continuation rather than
+ * a semantic model of the callee.
+ */
+enum class TsResidualCallPolicy {
+    STOP_PATH,
+    FRESH_SYMBOLIC_RETURN,
+}
+
+/** Independently configures model lookup and the fallback for residual calls. */
+data class TsUnknownCallProfile(
+    val modelLookup: TsUnknownCallModelLookup,
+    val residualPolicy: TsResidualCallPolicy,
+    val residualOverrides: Map<EtsClassSignature, TsResidualCallPolicy> = emptyMap(),
+) {
+    internal fun residualPolicyFor(call: TsUnknownCall): TsResidualCallPolicy =
+        residualOverrides[call.callee.enclosingClass] ?: residualPolicy
+}
+
+/** Ready-to-use profiles for the four supported model/fallback combinations. */
+object TsUnknownCallProfiles {
+    val STOP_ALL = TsUnknownCallProfile(
+        modelLookup = TsUnknownCallModelLookup.DISABLED,
+        residualPolicy = TsResidualCallPolicy.STOP_PATH,
+    )
+    val FRESH_SYMBOLIC_FOR_ALL = TsUnknownCallProfile(
+        modelLookup = TsUnknownCallModelLookup.DISABLED,
+        residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+    )
+    val MODELS_THEN_STOP = TsUnknownCallProfile(
+        modelLookup = TsUnknownCallModelLookup.ENABLED,
+        residualPolicy = TsResidualCallPolicy.STOP_PATH,
+    )
+    val MODELS_THEN_FRESH_SYMBOLIC = TsUnknownCallProfile(
+        modelLookup = TsUnknownCallModelLookup.ENABLED,
+        residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+    )
+}
+
+/** The result of asking a model provider to handle one unknown call. */
+enum class TsUnknownCallModelApplication {
+    APPLIED,
+    NOT_APPLICABLE,
+}
+
+/**
+ * Applies semantic models without exposing their lookup or registry implementation to the dispatcher.
+ *
+ * A provider returning [TsUnknownCallModelApplication.APPLIED] must update the supplied scope with the model's
+ * successor states. The deterministic registry and concrete model implementations are introduced separately.
+ */
+fun interface TsUnknownCallModelProvider {
+    fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication
+}
+
+/** Empty provider used until an explicit model registry is configured. */
+object TsNoUnknownCallModels : TsUnknownCallModelProvider {
+    override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication =
+        TsUnknownCallModelApplication.NOT_APPLICABLE
+}
+
+/** Applies the selected model/fallback profile to every residual call. */
+class TsProfileUnknownCallDispatcher(
+    private val profile: TsUnknownCallProfile,
+    private val modelProvider: TsUnknownCallModelProvider,
+) : TsUnknownCallDispatcher {
+    override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome {
+        if (profile.modelLookup == TsUnknownCallModelLookup.ENABLED &&
+            modelProvider.apply(scope, call) == TsUnknownCallModelApplication.APPLIED
+        ) {
+            return TsUnknownCallOutcome.MODEL_APPLIED
+        }
+
+        return when (profile.residualPolicyFor(call)) {
+            TsResidualCallPolicy.STOP_PATH -> {
+                val falseExpr = scope.calcOnState { ctx.falseExpr }
+                scope.assert(falseExpr)
+                TsUnknownCallOutcome.PATH_STOPPED
+            }
+
+            TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> {
+                mockMethodCall(scope, call.callee, call.resultType)
+                scope.doWithState { newStmt(call.callSite) }
+                TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN
+            }
+        }
+    }
+}

usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt

@@ -20,6 +20,7 @@ import org.usvm.api.targets.ReachabilityObserver
 import org.usvm.api.targets.TsReachabilityTarget
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
+import org.usvm.machine.call.TsCompatibilityUnknownCallDispatcher
 import org.usvm.util.getResourcePath
 import kotlin.test.assertFalse
 import kotlin.test.assertIs
@@ -178,6 +179,7 @@ class CallFallbackBaselineTest {
             options = machineOptions,
             tsOptions = tsOptions,
             machineObserver = ReachabilityObserver(),
+            unknownCallDispatcher = TsCompatibilityUnknownCallDispatcher,
         ).use { machine ->
             machine.analyze(listOf(method), listOf(initialTarget))
                 .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements }

usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt

@@ -12,6 +12,7 @@ import org.usvm.UMachineOptions
 import org.usvm.api.checkers.UnreachableCodeDetector
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
+import org.usvm.machine.call.TsCompatibilityUnknownCallDispatcher
 import org.usvm.util.getResourcePath
 
 @TestInstance(PER_CLASS)
@@ -48,7 +49,14 @@ class UnreachableCodeDetectorTest {
     fun testUnreachableCodeWithMockedCallsInside() {
         val observer = UnreachableCodeDetector()
         val tsOptions = TsOptions(interproceduralAnalysis = false)
-        val machine = TsMachine(scene, options, tsOptions, observer, observer)
+        val machine = TsMachine(
+            scene,
+            options,
+            tsOptions,
+            observer,
+            observer,
+            TsCompatibilityUnknownCallDispatcher,
+        )
         val methods = scene.projectClasses
             .flatMap { it.methods }
             .filter { it.name == "unreachableCodeWithCallsInside" }