[TS] Preserve callback prefixes when reduce invariants fail

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

@@ -39,6 +39,9 @@ interface TsUnknownCallModel {
     val additionalSceneFiles: List<EtsFile>
         get() = emptyList()
 
+    /** Model-owned invariants may require stopping a prefix instead of inventing a helper result. */
+    fun residualPolicy(state: TsState, call: TsUnknownCall): TsResidualCallPolicy? = null
+
     fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution?
 }
 

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

@@ -35,7 +35,7 @@ class TsModelUnknownCallDispatcher(
     private val observer: TsInterpreterObserver? = null,
 ) : TsUnknownCallModelDispatcher {
     override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome {
-        val application = scope.calcOnState {
+        val (application, residualPolicy) = scope.calcOnState {
             val catalog = this@TsModelUnknownCallDispatcher.models
             val hasDirectTarget = catalog.select(call) != null
             // A direct target retains precedence even when its model rejects the call or is already active.
@@ -45,22 +45,24 @@ class TsModelUnknownCallDispatcher(
                 TsDateEtsIrModelFamily.canonicalModelCall(this, call) ?: call
             }
 
-            catalog.apply(this, modelCall)
+            val residualPolicy = catalog.select(modelCall)?.residualPolicy(this, modelCall) ?: fallback
+            catalog.apply(this, modelCall) to residualPolicy
         }
 
         return when (application) {
-            is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application)
-            TsUnknownCallModelApplication.NotApplicable -> applyFallback(scope, call)
+            is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application, residualPolicy)
+            TsUnknownCallModelApplication.NotApplicable -> applyFallback(scope, call, residualPolicy)
         }
     }
 
     private fun applyFallback(
         scope: TsStepScope,
         call: TsUnknownCall,
+        residualPolicy: TsResidualCallPolicy,
     ): TsUnknownCallOutcome {
-        val decision = TsUnknownCallDecision.ResidualFallback(fallback)
+        val decision = TsUnknownCallDecision.ResidualFallback(residualPolicy)
 
-        when (fallback) {
+        when (residualPolicy) {
             TsResidualCallPolicy.STOP_PATH -> {
                 val stoppedState = scope.calcOnState { this }
                 val falseExpr = stoppedState.ctx.falseExpr
@@ -78,26 +80,27 @@ class TsModelUnknownCallDispatcher(
             }
         }
 
-        reportFallback(call)
+        reportFallback(call, residualPolicy)
         return decision.outcome
     }
 
     private fun applyModel(
         scope: TsStepScope,
         call: TsUnknownCall,
         application: TsUnknownCallModelApplication.Applied,
+        residualPolicy: TsResidualCallPolicy,
     ): TsUnknownCallOutcome {
         val residualGuard = application.execution.residualGuard
         // Creating an unresolved value may add fake-value constraints. Do it before forking so the residual clone
         // inherits both the constraints and their solver models.
         val freshResidualResult = if (
-            residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN
+            residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN
         ) {
             makeFreshUnknownCallResult(scope, call.resultType)
         } else {
             null
         }
-        val stoppedResidualState = if (residualGuard != null && fallback == TsResidualCallPolicy.STOP_PATH) {
+        val stoppedResidualState = if (residualGuard != null && residualPolicy == TsResidualCallPolicy.STOP_PATH) {
             scope.checkSat(residualGuard)
         } else {
             null
@@ -126,7 +129,7 @@ class TsModelUnknownCallDispatcher(
             )
         }.toMutableList()
 
-        if (residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) {
+        if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) {
             guardedStateChanges += residualGuard to {
                 setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult))
                 newStmt(call.callSite)
@@ -150,7 +153,7 @@ class TsModelUnknownCallDispatcher(
             observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ModelApplied(application.modelId)))
         }
         if (freshResidualApplied || stoppedResidualIsSatisfiable) {
-            reportFallback(call)
+            reportFallback(call, residualPolicy)
         }
 
         return when {
@@ -164,14 +167,14 @@ class TsModelUnknownCallDispatcher(
     private fun stoppedPathReason(call: TsUnknownCall): String =
         "Unknown call ${call.callee} at ${call.callSite.location}: reason=${call.failureReason}"
 
-    private fun reportFallback(call: TsUnknownCall) {
-        if (fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) {
+    private fun reportFallback(call: TsUnknownCall, residualPolicy: TsResidualCallPolicy) {
+        if (residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) {
             logger.debug {
                 "Unknown call ${call.callee} at ${call.callSite.location}: " +
-                    "fallback=$fallback, reason=${call.failureReason}"
+                    "fallback=$residualPolicy, reason=${call.failureReason}"
             }
         }
-        observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ResidualFallback(fallback)))
+        observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ResidualFallback(residualPolicy)))
     }
 
     private fun modelStateChange(

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

@@ -16,6 +16,7 @@ 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.TsResidualCallPolicy
 import org.usvm.machine.call.TsUnknownCall
 import org.usvm.machine.call.TsUnknownCallFailureReason
 import org.usvm.machine.call.TsUnknownCallModel
@@ -388,6 +389,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 methodName = "requireDense",
                 arity = 1,
                 implementation = TsDenseArrayPrimitives::requireDense,
+                unsupportedCallPolicy = TsResidualCallPolicy.STOP_PATH,
             ),
             primitiveModel(
                 methodName = "prepareOwnSlots",
@@ -476,6 +478,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         methodName: String,
         arity: Int,
         implementation: (TsState, List<UExpr<*>>) -> TsUnknownCallModelExecution?,
+        unsupportedCallPolicy: TsResidualCallPolicy? = null,
     ): TsUnknownCallModel = TsPrimitiveUnknownCallModel(
         idPrefix = "ts.array.primitive",
         methodName = methodName,
@@ -485,6 +488,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass },
         owningModelIds = { sourceModelIds },
         implementation = implementation,
+        unsupportedCallPolicy = unsupportedCallPolicy,
     )
 
     private fun growArray(

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

@@ -2,6 +2,7 @@ package org.usvm.machine.call.intrinsic
 
 import org.jacodb.ets.model.EtsClassSignature
 import org.usvm.UExpr
+import org.usvm.machine.call.TsResidualCallPolicy
 import org.usvm.machine.call.TsUnknownCall
 import org.usvm.machine.call.TsUnknownCallFailureReason
 import org.usvm.machine.call.TsUnknownCallModel
@@ -19,6 +20,7 @@ internal class TsPrimitiveUnknownCallModel(
     private val sourceClassSignature: () -> EtsClassSignature,
     private val owningModelIds: () -> Set<String>,
     private val implementation: (TsState, List<UExpr<*>>) -> TsUnknownCallModelExecution?,
+    private val unsupportedCallPolicy: TsResidualCallPolicy? = null,
 ) : TsUnknownCallModel {
     override val id: String = "$idPrefix.$methodName"
     override val target = TsUnknownCallTarget(
@@ -28,11 +30,7 @@ internal class TsPrimitiveUnknownCallModel(
     )
 
     override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? {
-        val helperOwnerMatches = call.callee.enclosingClass == helperClassSignature()
-        val callerSignature = call.callSite.location.method.signature
-        val sourceCallerMatches = callerSignature.enclosingClass == sourceClassSignature()
-        val sourceModelIsActive = owningModelIds().any(state::isUnknownCallModelActive)
-        if (!helperOwnerMatches || !sourceCallerMatches || !sourceModelIsActive) return null
+        if (!ownsHelperCall(state, call)) return null
 
         if (call.receiver != null || call.arguments.size != arity) {
             return null
@@ -41,4 +39,15 @@ internal class TsPrimitiveUnknownCallModel(
         val inputs = call.arguments.map { argument -> argument.resolved ?: return null }
         return implementation(state, inputs)
     }
+
+    override fun residualPolicy(state: TsState, call: TsUnknownCall): TsResidualCallPolicy? =
+        unsupportedCallPolicy.takeIf { ownsHelperCall(state, call) }
+
+    private fun ownsHelperCall(state: TsState, call: TsUnknownCall): Boolean {
+        val helperOwnerMatches = call.callee.enclosingClass == helperClassSignature()
+        val callerSignature = call.callSite.location.method.signature
+        val sourceCallerMatches = callerSignature.enclosingClass == sourceClassSignature()
+        val sourceModelIsActive = owningModelIds().any(state::isUnknownCallModelActive)
+        return helperOwnerMatches && sourceCallerMatches && sourceModelIsActive
+    }
 }

usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt

@@ -1,7 +1,13 @@
 package org.usvm.machine.call
 
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsReturnStmt
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsStringType
+import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.Test
@@ -17,11 +23,16 @@ import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
 import org.usvm.machine.TsRuntimeFeatureLimitationReason
+import org.usvm.machine.expr.extractInt
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsState
+import org.usvm.memory.URegisterStackLValue
 import org.usvm.util.TsMethodTestRunner
 import org.usvm.util.TsTestResolver
 import org.usvm.util.assertNodeReplay
 import org.usvm.util.getResourcePath
 import org.usvm.util.jsString
+import org.usvm.util.mkArrayLengthLValue
 import java.nio.file.Path
 import kotlin.io.path.readText
 import kotlin.test.assertEquals
@@ -291,6 +302,46 @@ class TsGapModelsSourceTest : TsMethodTestRunner() {
         assertTrue(limitations.any { it.reason == TsRuntimeFeatureLimitationReason.ARRAY_ELEMENT_DELETE })
     }
 
+    @Test
+    fun `rejected reduce invariant retains callback mutation as a stopped prefix in fresh mode`() {
+        val events = mutableListOf<TsUnknownCallEvent>()
+        val prefixLengths = mutableListOf<Int>()
+        var callbackReturns = 0
+        val observer = object : TsInterpreterObserver {
+            override fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) {
+                val isCallbackReturn = stmt is EtsReturnStmt &&
+                    stmt.location.method.name.startsWith(ANONYMOUS_METHOD_PREFIX)
+                if (isCallbackReturn) callbackReturns++
+            }
+
+            override fun onPathStopped(state: TsState, reason: String) {
+                val receiver = state.memory.read(URegisterStackLValue(state.ctx.addressSort, idx = 1))
+                    .asExpr(state.ctx.addressSort)
+                val arrayType = EtsArrayType(EtsStringType, dimensions = 1)
+                val length = state.memory.read(mkArrayLengthLValue(receiver, arrayType))
+                prefixLengths += state.models.first().eval(length).extractInt()
+            }
+
+            override fun onUnknownCall(event: TsUnknownCallEvent) {
+                events += event
+            }
+        }
+
+        val analysis = TsMachine(
+            scene = scene,
+            options = options,
+            tsOptions = tsOptions.copy(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN),
+            observer = observer,
+        ).use { machine -> machine.analyzeWithMetadata(listOf(method("reduceShrink"))) }
+
+        assertTrue(analysis.states.isEmpty())
+        assertTrue(analysis.unsupportedCall)
+        assertEquals(listOf(0), prefixLengths)
+        assertEquals(expected = 1, actual = callbackReturns)
+        val invariantEvent = events.single { it.callee.name == "requireDense" }
+        assertEquals(TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH), invariantEvent.decision)
+    }
+
     @Test
     fun `own slot deletion revokes dense reduction and slice models`() {
         discoverProperties<TsTestValue.TsBoolean>(

usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt

@@ -12,6 +12,7 @@ import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.getResourcePath
 import kotlin.test.Test
+import kotlin.test.assertEquals
 import kotlin.test.assertTrue
 import kotlin.time.Duration
 
@@ -38,6 +39,27 @@ class TsPrimitiveOwnerBoundaryTest {
         assertForeignHelperResidual("foreignStringRange")
     }
 
+    @Test
+    fun `foreign invariant declaration retains the configured fresh fallback`() {
+        val method = scene.projectClasses.single { it.name == "ForeignPrimitiveHelpers" }
+            .methods
+            .single { it.name == "foreignDense" }
+        val observer = RecordingObserver()
+
+        val states = TsMachine(
+            scene = scene,
+            options = machineOptions,
+            tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN),
+            observer = observer,
+        ).use { machine -> machine.analyze(listOf(method)) }
+
+        assertEquals(expected = 1, actual = states.size)
+        assertEquals(
+            expected = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN),
+            actual = observer.events.single().decision,
+        )
+    }
+
     private fun assertForeignHelperResidual(methodName: String) {
         val method = scene.projectClasses.single { it.name == "ForeignPrimitiveHelpers" }
             .methods

usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts

@@ -6,6 +6,7 @@ declare class StringModelPrimitives {
 
 declare class ArrayModelPrimitives {
     static grow(values: number[], length: number): void;
+    static requireDense(values: number[]): void;
 }
 
 export class ForeignPrimitiveHelpers {
@@ -26,4 +27,10 @@ export class ForeignPrimitiveHelpers {
         ArrayModelPrimitives.grow(values, 2);
         return values.length;
     }
+
+    foreignDense(): number {
+        const values = [1];
+        ArrayModelPrimitives.requireDense(values);
+        return values.length;
+    }
 }