[TS] Harden model provenance and Calls replay semantics

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

@@ -22,6 +22,18 @@ object TsBuiltInUnknownCallModels {
     }
     private val allModels by lazy { TsUnknownCallModelCatalog(models) }
 
+    internal fun hasPartialApproximationModel(
+        methodName: String,
+        enclosingClassName: String,
+        allowUnqualifiedTarget: Boolean = false,
+    ): Boolean =
+        allModels.hasTarget(
+            methodName = methodName,
+            enclosingClassName = enclosingClassName,
+            failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION,
+            allowUnqualifiedTarget = allowUnqualifiedTarget,
+        )
+
     fun catalog(selection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All): TsUnknownCallModelCatalog =
         if (selection == TsUnknownCallModelSelection.All) allModels else TsUnknownCallModelCatalog(models, selection)
 }

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

@@ -75,6 +75,16 @@ class TsUnknownCallModelCatalog(
         return candidates[call.callee.enclosingClass.name] ?: candidates[null]
     }
 
+    internal fun hasTarget(
+        methodName: String,
+        enclosingClassName: String,
+        failureReason: TsUnknownCallFailureReason,
+        allowUnqualifiedTarget: Boolean,
+    ): Boolean {
+        val candidates = index[methodName]?.get(failureReason) ?: return false
+        return enclosingClassName in candidates || (allowUnqualifiedTarget && null in candidates)
+    }
+
     fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication {
         val directModel = select(call)
         val modelCall = if (directModel == null) {

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

@@ -46,6 +46,10 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         )
     }
 
+    private val sourceModelIds by lazy {
+        models.filterIsInstance<TsEtsIrUnknownCallModel>().map { model -> model.id }.toSet()
+    }
+
     private val primitiveClassSignature by lazy {
         baseArtifact.file.allClasses.single { it.name == PRIMITIVES_CLASS_NAME }.signature
     }
@@ -436,9 +440,14 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         methodName: String,
         arity: Int,
         implementation: (TsState, List<UExpr<*>>) -> TsUnknownCallModelExecution?,
-    ): TsUnknownCallModel = ArrayPrimitiveModel(
+    ): TsUnknownCallModel = TsPrimitiveUnknownCallModel(
+        idPrefix = "ts.array.primitive",
         methodName = methodName,
+        enclosingClassName = PRIMITIVES_CLASS_NAME,
         arity = arity,
+        helperClassSignature = { primitiveClassSignature },
+        sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass },
+        owningModelIds = { sourceModelIds },
         implementation = implementation,
     )
 
@@ -536,30 +545,6 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         )
     }
 
-    private class ArrayPrimitiveModel(
-        methodName: String,
-        private val arity: Int,
-        private val implementation: (TsState, List<UExpr<*>>) -> TsUnknownCallModelExecution?,
-    ) : TsUnknownCallModel {
-        override val id: String = "ts.array.primitive.$methodName"
-        override val target = TsUnknownCallTarget(
-            methodName = methodName,
-            enclosingClassName = PRIMITIVES_CLASS_NAME,
-            failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE,
-        )
-
-        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? {
-            if (call.callee.enclosingClass != primitiveClassSignature) return null
-
-            if (call.receiver != null || call.arguments.size != arity) {
-                return null
-            }
-
-            val inputs = call.arguments.map { argument -> argument.resolved ?: return null }
-            return implementation(state, inputs)
-        }
-    }
-
     private const val MATH_FLOOR_MODEL_ID = "ts.math.floor"
     private const val PRIMITIVE_GROW_ID = "ts.array.primitive.grow"
     private const val PRIMITIVE_ALLOCATE_LIKE_ID = "ts.array.primitive.allocateLike"

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

@@ -0,0 +1,44 @@
+package org.usvm.machine.call.intrinsic
+
+import org.jacodb.ets.model.EtsClassSignature
+import org.usvm.UExpr
+import org.usvm.machine.call.TsUnknownCall
+import org.usvm.machine.call.TsUnknownCallFailureReason
+import org.usvm.machine.call.TsUnknownCallModel
+import org.usvm.machine.call.TsUnknownCallModelExecution
+import org.usvm.machine.call.TsUnknownCallTarget
+import org.usvm.machine.state.TsState
+
+/** Dispatches a helper method used by an EtsIR source model. */
+internal class TsPrimitiveUnknownCallModel(
+    idPrefix: String,
+    methodName: String,
+    enclosingClassName: String,
+    private val arity: Int,
+    private val helperClassSignature: () -> EtsClassSignature,
+    private val sourceClassSignature: () -> EtsClassSignature,
+    private val owningModelIds: () -> Set<String>,
+    private val implementation: (TsState, List<UExpr<*>>) -> TsUnknownCallModelExecution?,
+) : TsUnknownCallModel {
+    override val id: String = "$idPrefix.$methodName"
+    override val target = TsUnknownCallTarget(
+        methodName = methodName,
+        enclosingClassName = enclosingClassName,
+        failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE,
+    )
+
+    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 (call.receiver != null || call.arguments.size != arity) {
+            return null
+        }
+
+        val inputs = call.arguments.map { argument -> argument.resolved ?: return null }
+        return implementation(state, inputs)
+    }
+}

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

@@ -10,7 +10,6 @@ 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.TsUnknownCallModelCompletion
@@ -41,6 +40,10 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         )
     }
 
+    private val sourceModelIds by lazy {
+        models.filterIsInstance<TsEtsIrUnknownCallModel>().map { model -> model.id }.toSet()
+    }
+
     private val primitiveClassSignature by lazy {
         baseArtifact.file.allClasses.single { it.name == PRIMITIVES_CLASS_NAME }.signature
     }
@@ -328,9 +331,14 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         methodName: String,
         arity: Int,
         implementation: (TsState, List<UExpr<*>>) -> TsUnknownCallModelExecution?,
-    ): TsUnknownCallModel = StringPrimitiveModel(
+    ): TsUnknownCallModel = TsPrimitiveUnknownCallModel(
+        idPrefix = "ts.string.primitive",
         methodName = methodName,
+        enclosingClassName = PRIMITIVES_CLASS_NAME,
         arity = arity,
+        helperClassSignature = { primitiveClassSignature },
+        sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass },
+        owningModelIds = { sourceModelIds },
         implementation = implementation,
     )
 
@@ -406,32 +414,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         )
     }
 
-    private class StringPrimitiveModel(
-        methodName: String,
-        private val arity: Int,
-        private val implementation: (TsState, List<UExpr<*>>) -> TsUnknownCallModelExecution?,
-    ) : TsUnknownCallModel {
-        override val id: String = "ts.string.primitive.$methodName"
-        override val target = TsUnknownCallTarget(
-            methodName = methodName,
-            enclosingClassName = PRIMITIVES_CLASS_NAME,
-            failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE,
-        )
-
-        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? {
-            if (call.callee.enclosingClass != primitiveClassSignature) {
-                return null
-            }
-
-            if (call.receiver != null || call.arguments.size != arity) {
-                return null
-            }
-
-            val inputs = call.arguments.map { argument -> argument.resolved ?: return null }
-            return implementation(state, inputs)
-        }
-    }
-
     private const val PRIMITIVE_CODE_UNIT_AT_ID = "ts.string.primitive.codeUnitAt"
     private const val PRIMITIVE_FROM_CODE_UNIT_ID = "ts.string.primitive.fromCodeUnit"
     private const val MATH_FLOOR_MODEL_ID = "ts.math.floor"

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt

@@ -24,6 +24,7 @@ import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.TsRuntimeFeatureLimitationReason
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.TsVirtualMethodCallStmt
+import org.usvm.machine.call.TsBuiltInUnknownCallModels
 import org.usvm.machine.call.TsUnknownCallFailureReason
 import org.usvm.machine.call.TsUnknownCallModelDispatcher
 import org.usvm.machine.call.dispatch
@@ -52,24 +53,6 @@ import org.usvm.util.typedArrayBoxedLValue
 import org.usvm.util.typedArrayOverrideLValue
 
 private val logger = KotlinLogging.logger {}
-private val modeledArrayMethods = setOf("concat", "fill", "push", "reverse", "slice", "unshift")
-
-private val modeledStringMethods = setOf(
-    "substring",
-    "trim",
-    "trimStart",
-    "trimEnd",
-    "charAt",
-    "charCodeAt",
-    "endsWith",
-    "includes",
-    "indexOf",
-    "lastIndexOf",
-    "slice",
-    "startsWith",
-    "toLowerCase",
-    "toUpperCase",
-)
 
 internal fun TsExprResolver.tryApproximateGlobalInstanceCall(
     expr: EtsInstanceCallExpr,
@@ -161,6 +144,11 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
 
     // Mock `.toString()` method calls
     if (expr.callee.name == "toString") {
+        if (unknownCallDispatcher is TsUnknownCallModelDispatcher) {
+            dispatchLegacyInstanceCall(stmt)
+            return TsExprApproximationResult.ResolveFailure
+        }
+
         if (expr.args.isNotEmpty()) {
             logger.warn { "toString() should have no arguments, but got ${expr.args.size}" }
         }
@@ -187,9 +175,15 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
             .takeIf { it !is TsUnresolvedSort }
             ?: addressSort
 
-        val usesSemanticArrayModel = expr.callee.name in modeledArrayMethods &&
-            unknownCallDispatcher is TsUnknownCallModelDispatcher
-        if (usesSemanticArrayModel) {
+        val usesModelDispatcher = unknownCallDispatcher is TsUnknownCallModelDispatcher
+        val modeledArrayCall = usesModelDispatcher && TsBuiltInUnknownCallModels.hasPartialApproximationModel(
+            methodName = expr.callee.name,
+            enclosingClassName = "Array",
+            allowUnqualifiedTarget = true,
+        )
+
+        // join has no source model yet; the model run intentionally sends it to the residual policy.
+        if (modeledArrayCall || (usesModelDispatcher && expr.callee.name == "join")) {
             dispatchArrayModel(stmt)
             return TsExprApproximationResult.ResolveFailure
         }
@@ -250,12 +244,13 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
         }
     }
 
-    if (instanceType is EtsStringType && expr.callee.name in modeledStringMethods) {
-        val dispatcher = unknownCallDispatcher
-        if (dispatcher !is TsUnknownCallModelDispatcher) {
-            return TsExprApproximationResult.NoApproximation
-        }
-
+    val dispatcher = unknownCallDispatcher
+    val modeledStringCall = instanceType is EtsStringType && dispatcher is TsUnknownCallModelDispatcher &&
+        TsBuiltInUnknownCallModels.hasPartialApproximationModel(
+            methodName = expr.callee.name,
+            enclosingClassName = "String",
+        )
+    if (modeledStringCall) {
         dispatcher.dispatch(
             scope = scope,
             call = stmt.call,
@@ -315,6 +310,17 @@ private fun TsExprResolver.dispatchArrayModel(stmt: TsVirtualMethodCallStmt) {
     )
 }
 
+private fun TsExprResolver.dispatchLegacyInstanceCall(stmt: TsVirtualMethodCallStmt) {
+    unknownCallDispatcher.dispatch(
+        scope = scope,
+        call = stmt.call,
+        callSite = stmt.returnSite,
+        failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION,
+        resolvedReceiver = stmt.instance,
+        resolvedArguments = stmt.args,
+    )
+}
+
 private fun EtsMethodSignature.withEnclosingClassName(name: String): EtsMethodSignature =
     copy(enclosingClass = enclosingClass.copy(name = name))
 

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

@@ -61,11 +61,27 @@ class TsInstanceCallReceiverTest {
                 assertEquals(case.results, results)
                 assertEquals(case.throws, tests.any { it.returnValue is TsTestValue.TsException })
                 assertTrue(tests.isNotEmpty())
-                if (method.parameters.singleOrNull()?.name == "index") {
+                val modelToStringIsUnsupported = case.method == "primitiveToString" && !case.compatibility
+                val exploresBothReceiverAlternatives = method.parameters.singleOrNull()?.name == "index" &&
+                    !modelToStringIsUnsupported
+                if (exploresBothReceiverAlternatives) {
                     val indices = tests.map { assertIs<TsTestValue.TsNumber>(it.before.parameters.single()).number }
                     assertTrue(indices.containsAll(listOf(0.0, 1.0)), "Both receiver alternatives must be explored")
                 }
 
+                if (modelToStringIsUnsupported) {
+                    assertTrue(events.isNotEmpty(), "Primitive toString calls must reach the residual policy")
+                    events.forEach { event ->
+                        assertEquals("toString", event.callee.name)
+                        assertEquals(TsUnknownCallOutcome.PATH_STOPPED, event.outcome)
+                        assertEquals(TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, event.failureReason)
+                        assertEquals(
+                            TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH),
+                            event.decision,
+                        )
+                    }
+                }
+
                 if (case.method == "wrappedShift") {
                     assertEquals(TsUnknownCallDecision.ModelApplied("ts.array.shift"), events.single().decision)
                 }
@@ -138,6 +154,7 @@ class TsInstanceCallReceiverTest {
             Case(method = "conditionalEmptyArray", results = setOf(0.0, 1.0)),
             Case(method = "arrayOrUserMethod", results = setOf(0.0, 1.0)),
             Case(method = "primitiveValueOf", results = setOf(0.0, 1.0)),
+            Case(method = "primitiveToString", results = setOf(0.0)),
             Case(method = "primitiveToString", results = setOf(0.0, 1.0), compatibility = true),
             Case(method = "constrainedFake", results = setOf(0.0, 1.0, 2.0)),
             Case(method = "nullableReceiver", results = setOf(0.0, 1.0), throws = true),