[TS PBT] Retain residual unknown-call diagnostics in property results

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt

@@ -1,12 +1,15 @@
 package org.usvm.ts.pbt.inference
 
+import kotlinx.serialization.encodeToString
+import kotlinx.serialization.json.Json
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.BeforeAll
 import org.junit.jupiter.api.Test
 import org.usvm.SolverType
 import org.usvm.UMachineOptions
+import org.usvm.ts.pbt.backend.CapabilityDiagnostic
 import org.usvm.ts.pbt.backend.ProjectionCapability
 import org.usvm.ts.pbt.backend.ProjectionLevel
 import org.usvm.ts.pbt.backend.PropertyRunConfiguration
@@ -52,6 +55,23 @@ import kotlin.time.Duration
 class EntryRelationRefutationTest {
     private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot()))
 
+    @Test
+    fun `unknown call in original admission retains its reason before the auxiliary target`() {
+        val inference = observe(predicate = "reflexive", precondition = "sliceAdmission")
+        val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL }
+
+        val refutation = refute(inference, equality)
+        val restored = Json.decodeFromString<List<CapabilityDiagnostic>>(Json.encodeToString(refutation.diagnostics))
+
+        assertEquals(UsvmEntryRefutationStatus.UNSUPPORTED, refutation.status)
+        assertNull(refutation.inputs)
+        val diagnostic = restored.single { it.code == "usvm.unknown-call.path-stopped" }
+        assertTrue("Array::slice" in diagnostic.message, diagnostic.message)
+        assertTrue("reason=PARTIAL_APPROXIMATION" in diagnostic.message, diagnostic.message)
+        assertTrue(diagnostic.path.contains("EntryRelations.ts:39:"), diagnostic.path)
+        assertEquals(refutation.diagnostics, restored)
+    }
+
     @Test
     fun `an auxiliary equality refutation is confirmed while the complete original property holds`() {
         val inference = observe(predicate = "reflexive")

usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts

@@ -33,3 +33,8 @@ export function throwing(left: number, right: number): boolean {
     if (left > right) throw new Error('original fault');
     return true;
 }
+
+export function sliceAdmission(left: number, right: number): boolean {
+    const values = [left, right];
+    return values.slice().length === 2;
+}

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt

@@ -12,6 +12,7 @@ import org.usvm.machine.TsMachine
 import org.usvm.machine.TsMachineAnalysisResult
 import org.usvm.machine.TsOptions
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
+import org.usvm.machine.call.TsUnknownCallEvent
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsEntryPointGuardOutcome
 import org.usvm.machine.state.TsState
@@ -200,6 +201,10 @@ internal open class UsvmRelationRefutationObserver : TsInterpreterObserver {
     override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
         runtimeLimitations.onRuntimeFeatureLimitation(event)
     }
+
+    override fun onUnknownCall(event: TsUnknownCallEvent) {
+        runtimeLimitations.onUnknownCall(event)
+    }
 }
 
 private fun resolveInputs(

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt

@@ -1,7 +1,10 @@
 package org.usvm.ts.pbt.usvm
 
+import org.jacodb.ets.model.EtsStmt
 import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
+import org.usvm.machine.call.TsUnknownCallEvent
+import org.usvm.machine.call.TsUnknownCallOutcome
 import org.usvm.ts.pbt.backend.CapabilityDiagnostic
 
 /** Retains a bounded sample of distinct model boundaries without keeping live engine objects. */
@@ -13,22 +16,28 @@ internal class UsvmRuntimeLimitationObserver : TsInterpreterObserver {
         get() = limitations.toList() + if (truncated) listOf(TRUNCATED_DIAGNOSTIC) else emptyList()
 
     override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
-        val location = event.statement.location
-        val origin = location.origin
-        val path = if (origin != null) {
-            // EtsIR origins use zero-based positions; diagnostics use ordinary editor coordinates.
-            "${origin.fileName}:${origin.startLine + 1}:${origin.startColumn + 1}-" +
-                "${origin.endLine + 1}:${origin.endColumn + 1}"
-        } else {
-            val method = location.method.signature
-            val source = method.enclosingClass.file.fileName
-            "$source#${method.name}[${location.index}]"
-        }
         val diagnostic = CapabilityDiagnostic(
             code = "usvm.runtime.${event.reason.name.lowercase().replace('_', '-')}",
             message = "${event.reason.name}: ${event.detail}; statement: ${event.statement}",
-            path = path,
+            path = event.statement.diagnosticPath(),
+        )
+        record(diagnostic)
+    }
+
+    override fun onUnknownCall(event: TsUnknownCallEvent) {
+        if (event.outcome == TsUnknownCallOutcome.MODEL_APPLIED) return
+
+        val outcome = event.outcome.name.lowercase().replace('_', '-')
+        val diagnostic = CapabilityDiagnostic(
+            code = "usvm.unknown-call.$outcome",
+            message = "${event.outcome.name}: ${event.callee}; reason=${event.failureReason.name}; " +
+                "statement: ${event.callSite}",
+            path = event.callSite.diagnosticPath(),
         )
+        record(diagnostic)
+    }
+
+    private fun record(diagnostic: CapabilityDiagnostic) {
         if (diagnostic in limitations) return
 
         if (limitations.size < MAX_DIAGNOSTICS) {
@@ -47,3 +56,16 @@ internal class UsvmRuntimeLimitationObserver : TsInterpreterObserver {
         )
     }
 }
+
+private fun EtsStmt.diagnosticPath(): String {
+    val origin = location.origin
+    if (origin != null) {
+        // EtsIR origins use zero-based positions; diagnostics use ordinary editor coordinates.
+        return "${origin.fileName}:${origin.startLine + 1}:${origin.startColumn + 1}-" +
+            "${origin.endLine + 1}:${origin.endColumn + 1}"
+    }
+
+    val method = location.method.signature
+    val source = method.enclosingClass.file.fileName
+    return "$source#${method.name}[${location.index}]"
+}

usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt

@@ -1,5 +1,7 @@
 package org.usvm.ts.pbt.usvm
 
+import kotlinx.serialization.encodeToString
+import kotlinx.serialization.json.Json
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
@@ -34,6 +36,30 @@ import kotlin.test.assertTrue
 import kotlin.time.Duration
 
 class UsvmPropertySearcherTest {
+    @Test
+    fun `unknown call diagnostics survive public result serialization`() {
+        assertUnknownCallDiagnostic(
+            predicate = "unsupportedSliceProperty",
+            callee = "Array::slice",
+            reason = "PARTIAL_APPROXIMATION",
+            sourceLine = 154,
+        )
+        assertUnknownCallDiagnostic(
+            predicate = "unsupportedTypedArrayProperty",
+            callee = "Float64Array::constructor",
+            reason = "RECEIVER_CLASS_NOT_FOUND",
+            sourceLine = 158,
+        )
+    }
+
+    @Test
+    fun `an applied call model does not introduce an unknown call limitation`() {
+        val result = search(manifest(predicateExport = "modeledAbsoluteProperty"))
+
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status)
+        assertTrue(result.diagnostics.none { it.code.startsWith("usvm.unknown-call.") }, result.diagnostics.toString())
+    }
+
     @Test
     fun `reports when no violation is reachable`() {
         val manifest = manifest(predicateExport = "validProperty")
@@ -355,6 +381,19 @@ class UsvmPropertySearcherTest {
         assertNull(result.inputs)
     }
 
+    private fun assertUnknownCallDiagnostic(predicate: String, callee: String, reason: String, sourceLine: Int) {
+        val result = search(manifest(predicateExport = predicate))
+        val restored = Json.decodeFromString<UsvmPropertySearchResult>(Json.encodeToString(result))
+
+        assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, restored.status)
+        val diagnostic = restored.diagnostics.single { it.code == "usvm.unknown-call.path-stopped" }
+        assertTrue(callee in diagnostic.message, diagnostic.message)
+        assertTrue("reason=$reason" in diagnostic.message, diagnostic.message)
+        assertTrue("PATH_STOPPED" in diagnostic.message, diagnostic.message)
+        assertTrue(diagnostic.path.contains("UsvmPropertySearchFixture.ts:$sourceLine:"), diagnostic.path)
+        assertEquals(result.diagnostics, restored.diagnostics)
+    }
+
     private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search(
         manifest = manifest,
         mapping = mapper.map(manifest),

usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt

@@ -11,10 +11,71 @@ import org.jacodb.ets.model.EtsUndefinedType
 import org.junit.jupiter.api.Test
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
 import org.usvm.machine.TsRuntimeFeatureLimitationReason
+import org.usvm.machine.call.TsResidualCallPolicy
+import org.usvm.machine.call.TsUnknownCallDecision
+import org.usvm.machine.call.TsUnknownCallEvent
+import org.usvm.machine.call.TsUnknownCallFailureReason
 import kotlin.test.assertEquals
 import kotlin.test.assertTrue
 
 class UsvmRuntimeLimitationObserverTest {
+    @Test
+    fun `unknown call fallbacks retain their decisions without treating applied models as limitations`() {
+        val observer = UsvmRuntimeLimitationObserver()
+        val statement = event(detail = "unused", withOrigin = true).statement
+        val stopped = TsUnknownCallEvent(
+            callSite = statement,
+            callee = statement.location.method.signature.copy(name = "missing"),
+            failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE,
+            decision = TsUnknownCallDecision.ResidualFallback(policy = TsResidualCallPolicy.STOP_PATH),
+        )
+        val fresh = stopped.copy(
+            callSite = event(detail = "unused", withOrigin = false).statement,
+            decision = TsUnknownCallDecision.ResidualFallback(policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN),
+        )
+
+        observer.onUnknownCall(stopped.copy(decision = TsUnknownCallDecision.ModelApplied(modelId = "modeled")))
+        assertTrue(observer.diagnostics.isEmpty())
+        repeat(times = 100) { observer.onUnknownCall(stopped) }
+        observer.onUnknownCall(fresh)
+
+        val diagnostics = observer.diagnostics
+        assertEquals(2, diagnostics.size)
+        assertEquals("usvm.unknown-call.path-stopped", diagnostics[0].code)
+        assertEquals("original.ts:3:5-3:12", diagnostics[0].path)
+        assertTrue("Example::missing" in diagnostics[0].message)
+        assertTrue("reason=METHOD_BODY_UNAVAILABLE" in diagnostics[0].message)
+        assertEquals("usvm.unknown-call.fresh-symbolic-return", diagnostics[1].code)
+        assertEquals("generated.ts#example[0]", diagnostics[1].path)
+        assertTrue("FRESH_SYMBOLIC_RETURN" in diagnostics[1].message)
+    }
+
+    @Test
+    fun `unknown calls share the existing distinct diagnostic bound with runtime limits`() {
+        val observer = UsvmRuntimeLimitationObserver()
+        val first = event(detail = "first", withOrigin = false)
+        observer.onRuntimeFeatureLimitation(first)
+        val retained = observer.diagnostics.single()
+        val callee = first.statement.location.method.signature
+
+        repeat(times = 100) { index ->
+            observer.onUnknownCall(
+                TsUnknownCallEvent(
+                    callSite = first.statement,
+                    callee = callee.copy(name = "missing$index"),
+                    failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE,
+                    decision = TsUnknownCallDecision.ResidualFallback(policy = TsResidualCallPolicy.STOP_PATH),
+                ),
+            )
+        }
+
+        val diagnostics = observer.diagnostics
+        assertEquals(65, diagnostics.size)
+        assertEquals(retained, diagnostics.first())
+        assertEquals("usvm.runtime.diagnostics-truncated", diagnostics.last().code)
+        assertEquals(diagnostics.size, diagnostics.distinct().size)
+    }
+
     @Test
     fun `deduplicates identical events and retains the original statement location`() {
         val observer = UsvmRuntimeLimitationObserver()

usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts

@@ -148,3 +148,17 @@ export function optionalNumberArrayMutationProperty(values: (number | undefined)
   values[0] = undefined;
   return old !== 2;
 }
+
+export function unsupportedSliceProperty(value: number): boolean {
+  const values = [value];
+  return values.slice().length === 1;
+}
+
+export function unsupportedTypedArrayProperty(value: number): boolean {
+  const values = new Float64Array(1);
+  return values[0] === value;
+}
+
+export function modeledAbsoluteProperty(value: number): boolean {
+  return Math.abs(value) >= 0;
+}