[Calls] Preserve engine failure evidence during witness extraction

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassInputCandidates.kt

@@ -52,6 +52,10 @@ internal data class CallsClassInputExtractionFailure(
     val outcome: String,
     val diagnostic: String,
     val environmentOnly: Boolean = false,
+    val originalEngineFailureReason: String? = null,
+    val currentMethod: String? = null,
+    val currentSourceFile: String? = null,
+    val statementIndex: Int? = null,
 )
 
 @Serializable
@@ -92,17 +96,19 @@ internal class CallsClassInputCandidates(output: Path, private val profile: Call
 
     fun append(state: TsState, outcome: String, emittedAtMillis: Long, stopped: Boolean) {
         val started = TimeSource.Monotonic.markNow()
+        val location = state.lastStmt.location
+        val currentMethod = location.method.signature
+        val currentSourceFile = currentMethod.enclosingClass.file.toString()
         val extracted = runCatching {
             val method = state.entrypoint
             val environment = resolveOriginalEnvironment(state = state)
             val suspended = outcome != "RETURNED" && outcome != "THREW"
             val reason = if (suspended) state.engineFailureReason ?: state.unsupportedReason ?: outcome else null
-            val currentMethod = state.lastStmt.location.method.signature
             CallsClassInputCandidate(
                 stateId = state.id.toString(),
                 entryMethod = method.signature.toString(),
                 currentMethod = currentMethod.toString(),
-                statementIndex = state.lastStmt.location.index,
+                statementIndex = location.index,
                 className = method.signature.enclosingClass.name,
                 methodName = method.name,
                 invocationKind = when {
@@ -144,6 +150,10 @@ internal class CallsClassInputCandidates(output: Path, private val profile: Call
                             outcome = outcome,
                             diagnostic = environmentFailure,
                             environmentOnly = true,
+                            originalEngineFailureReason = state.engineFailureReason,
+                            currentMethod = currentMethod.toString(),
+                            currentSourceFile = currentSourceFile,
+                            statementIndex = location.index,
                         )
                         failures.append(encodeCallsArtifact(diagnostic))
                     }
@@ -154,6 +164,10 @@ internal class CallsClassInputCandidates(output: Path, private val profile: Call
                         entryMethod = state.entrypoint.signature.toString(),
                         outcome = outcome,
                         diagnostic = "${failure::class.java.name}: ${failure.message}",
+                        originalEngineFailureReason = state.engineFailureReason,
+                        currentMethod = currentMethod.toString(),
+                        currentSourceFile = currentSourceFile,
+                        statementIndex = location.index,
                     )
                     failures.append(encodeCallsArtifact(diagnostic))
                 },

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawEngineFailureTest.kt

@@ -30,6 +30,15 @@ class CallsClassRawEngineFailureTest {
 
     @Test
     fun `suppressed interpreter failure persists as a failed prefix instead of UNSAT or a return`() {
+        checkFailure(retainRawStateDiagnostics = true, registerBindings = true)
+    }
+
+    @Test
+    fun `secondary extraction failure preserves original engine reason with raw dumps disabled`() {
+        checkFailure(retainRawStateDiagnostics = false, registerBindings = false)
+    }
+
+    private fun checkFailure(retainRawStateDiagnostics: Boolean, registerBindings: Boolean) {
         val source = directory.resolve("Target.ts")
         Files.writeString(source, "export class Target { run(): number { return 7; } }")
         val file = loadEtsFileAutoConvert(path = source, provider = EtsIrProvider.TS_FRONTEND)
@@ -39,7 +48,7 @@ class CallsClassRawEngineFailureTest {
             sourceFile = "Target.ts",
             universe = emptyList(),
             output = directory,
-            retainRawStateDiagnostics = true,
+            retainRawStateDiagnostics = retainRawStateDiagnostics,
             profile = CallsExperimentProfile.FROZEN_STOP,
         )
         val observer = object : TsInterpreterObserver {
@@ -68,18 +77,14 @@ class CallsClassRawEngineFailureTest {
         ).use { machine ->
             machine.analyzeWithMetadata(
                 methods = listOf(method),
-                configureInitialState = { entry, state -> raw.registerInitialState(method = entry, state = state) },
+                configureInitialState = { entry, state ->
+                    // Deliberately omit bindings to exercise a secondary journal extraction failure.
+                    if (registerBindings) raw.registerInitialState(method = entry, state = state)
+                },
             )
         }
         val manifest = manifest(source = source)
         val analysis = raw.result(manifest = manifest, analysisElapsedMillis = 0)
-        val snapshotPath = directory.resolve(checkNotNull(analysis.stateSnapshots).path)
-        val snapshots = GZIPInputStream(Files.newInputStream(snapshotPath))
-            .bufferedReader().use { reader ->
-                reader.lineSequence().map { CallsExperimentJson.json.decodeFromString<CallsClassRawStateSnapshot>(it) }
-                    .toList()
-            }
-
         assertTrue(result.engineFailed)
         assertFalse(result.runtimeLimited)
         assertTrue(result.states.isEmpty())
@@ -88,12 +93,36 @@ class CallsClassRawEngineFailureTest {
         assertEquals(expected = 0L, actual = analysis.unsupportedTerminalStates)
         assertEquals(expected = 0L, actual = analysis.unreachableTerminalStates)
         assertTrue(analysis.stateSnapshotFailures.isEmpty())
-        val snapshot = snapshots.single()
-        assertEquals(expected = "ENGINE_FAILURE", actual = snapshot.outcome)
-        assertTrue(snapshot.callStack.isNotEmpty())
-        assertTrue(snapshot.engineFailureReason?.contains("Injected raw-journal step failure") == true)
-        assertNull(snapshot.unsupportedReason)
-        assertNull(snapshot.symbolicResultId)
+        if (retainRawStateDiagnostics) {
+            val snapshotPath = directory.resolve(checkNotNull(analysis.stateSnapshots).path)
+            val snapshots = GZIPInputStream(Files.newInputStream(snapshotPath)).bufferedReader().use { reader ->
+                reader.lineSequence().map { CallsExperimentJson.json.decodeFromString<CallsClassRawStateSnapshot>(it) }
+                    .toList()
+            }
+            val snapshot = snapshots.single()
+            assertEquals(expected = "ENGINE_FAILURE", actual = snapshot.outcome)
+            assertTrue(snapshot.callStack.isNotEmpty())
+            assertTrue(snapshot.engineFailureReason?.contains("Injected raw-journal step failure") == true)
+            assertNull(snapshot.unsupportedReason)
+            assertNull(snapshot.symbolicResultId)
+        } else {
+            assertNull(analysis.stateSnapshots)
+            assertNull(analysis.symbolicExpressions)
+            val lines = Files.readAllLines(directory.resolve(checkNotNull(analysis.inputExtractionFailures).path))
+            val failure = lines.map {
+                CallsExperimentJson.json.decodeFromString<CallsClassInputExtractionFailure>(it)
+            }.single()
+
+            assertTrue(failure.diagnostic.contains("Missing original entry bindings"))
+            val original = checkNotNull(failure.originalEngineFailureReason)
+            assertTrue(original.contains("IllegalStateException: Injected raw-journal step failure"))
+            assertTrue(original.contains("statement="))
+            assertTrue(original.contains("CallsClassRawEngineFailureTest"))
+            assertTrue(original.length <= 2048)
+            assertTrue(checkNotNull(failure.currentMethod).contains("run"))
+            assertTrue(checkNotNull(failure.currentSourceFile).contains("Target"))
+            assertTrue(checkNotNull(failure.statementIndex) >= 0)
+        }
     }
 
     private fun manifest(source: Path) = CallsClassStartManifest(

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

@@ -793,7 +793,7 @@ class TsExprResolver(
 
     override fun visit(expr: EtsYieldExpr): UExpr<out USort>? {
         logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        throw UnsupportedOperationException("Not supported $expr")
     }
 
     // endregion

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

@@ -94,6 +94,9 @@ private typealias Reason = TsUnknownCallFailureReason
 
 typealias TsStepScope = StepScope<TsState, EtsType, EtsStmt, TsContext>
 
+private const val MAX_ENGINE_FAILURE_MESSAGE_LENGTH = 1024
+private const val MAX_ENGINE_FAILURE_DIAGNOSTIC_LENGTH = 2048
+
 @Suppress("UNUSED_PARAMETER")
 class TsInterpreter(
     private val ctx: TsContext,
@@ -221,7 +224,12 @@ class TsInterpreter(
 
             // Preserve the failed prefix and any forks whose callbacks already completed.
             // The machine stops this state separately from unsupported or returned paths.
-            state.engineFailureReason = "${e::class.java.name}: ${e.message}"
+            val method = stmt.location.method.signature
+            val sourceFile = method.enclosingClass.file
+            val originalReason = "${e::class.java.name}: ${e.message}".take(MAX_ENGINE_FAILURE_MESSAGE_LENGTH)
+            val frames = e.stackTrace.take(5).joinToString(separator = "\n")
+            val diagnostic = "$originalReason\n$sourceFile::$method statement=${stmt.location.index}\n$frames"
+            state.engineFailureReason = diagnostic.take(MAX_ENGINE_FAILURE_DIAGNOSTIC_LENGTH)
             return scope.stepResult()
         }
 

usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt

@@ -701,15 +701,17 @@ open class TsTestStateResolver(
                     else -> error("TODO")
                 }
             }
-            if (classes.size == 1) {
-                return classes.single()
+            val runtimeDeclarations = classes.groupBy { it.signature }.values.flatMap(::canonicalClassDeclarations)
+            if (runtimeDeclarations.size == 1) {
+                return runtimeDeclarations.single()
             }
         }
 
         // Sad signature:
         val classes = ctx.scene.projectAndSdkClasses.filter { it.signature.name == name }
-        if (classes.size == 1) {
-            return classes.single()
+        val runtimeDeclarations = classes.groupBy { it.signature }.values.flatMap(::canonicalClassDeclarations)
+        if (runtimeDeclarations.size == 1) {
+            return runtimeDeclarations.single()
         }
 
         throw TsUnsupportedWitnessException("Concrete class identity is unresolved or ambiguous: $name")

usvm-ts/src/test/kotlin/org/usvm/util/TsMergedWitnessResolverTest.kt

@@ -0,0 +1,30 @@
+package org.usvm.util
+
+import org.usvm.api.TsTestValue
+import kotlin.test.Test
+
+class TsMergedWitnessResolverTest : TsMethodTestRunner() {
+    override val scene = loadScene("/models/MergedWitness.ts")
+
+    @Test
+    fun `interface before class resolves the runtime instance`() {
+        checkWitness(methodName = "first", expected = 17.0)
+    }
+
+    @Test
+    fun `interface after class resolves the runtime instance`() {
+        checkWitness(methodName = "last", expected = 19.0)
+    }
+
+    private fun checkWitness(methodName: String, expected: Double) {
+        val method = scene.projectClasses.flatMap { it.methods }.single { it.name == methodName }
+
+        discoverProperties<TsTestValue.TsClass>(
+            method = method,
+            { result -> (result.properties["value"] as? TsTestValue.TsNumber)?.number == expected },
+            invariants = arrayOf({ result ->
+                (result.properties["value"] as? TsTestValue.TsNumber)?.number == expected
+            }),
+        )
+    }
+}

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

@@ -0,0 +1,11 @@
+export interface MergedFirst { value: number; }
+export class MergedFirst {
+    value: number = 17;
+    static first(): MergedFirst { return new MergedFirst(); }
+}
+
+export class MergedLast {
+    value: number = 19;
+    static last(): MergedLast { return new MergedLast(); }
+}
+export interface MergedLast { value: number; }