[TS] Route thrown exceptions into catch blocks

buildSrc/src/main/kotlin/Dependencies.kt

@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "ddb127d9ef"
+    const val jacodb = "147d3b2797b693755c1d09fc28047ba43577a609"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

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

@@ -1161,8 +1161,8 @@ class TsExprResolver(
     override fun visit(value: EtsStaticFieldRef): UExpr<*>? = handleStaticFieldRef(value)
 
     override fun visit(value: EtsCaughtExceptionRef): UExpr<out USort>? {
-        logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
-        error("Not supported $value")
+        return scope.calcOnState { caughtException }
+            ?: throw UnsupportedOperationException("Caught exception value is unavailable")
     }
 
     override fun visit(value: EtsGlobalRef): UExpr<out USort>? {

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

@@ -113,11 +113,18 @@ class TsInterpreter(
 
         val result = state.methodResult
         if (result is TsMethodResult.TsException) {
-            // TODO catch processing
             scope.doWithState {
+                val catchers = stmt.location.method.cfg.catchers(stmt)
+                val catcher = catchers.singleOrNull()
+                if (catcher != null) {
+                    caughtException = result.value
+                    methodResult = TsMethodResult.NoCall
+                    newStmt(catcher)
+                    return@doWithState
+                }
+
                 leaveUnknownCallModelIfReturning()
                 val returnSite = callStack.pop()
-
                 if (callStack.isNotEmpty()) {
                     memory.stack.pop()
                     popLocalToSortStack()
@@ -706,37 +713,16 @@ class TsInterpreter(
 
         observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope)
 
-        val exception = exprResolver.resolve(stmt.exception)
-
-        // Pop the call stack to return to the caller
-        scope.doWithState {
-            memory.stack.pop()
+        val exception = exprResolver.resolve(stmt.exception) ?: return
+        val exceptionType: EtsType = when (exception.sort) {
+            ctx.addressSort -> EtsStringType // TODO: improve object type detection
+            ctx.fp64Sort -> EtsNumberType
+            ctx.boolSort -> EtsBooleanType
+            else -> EtsStringType
         }
 
-        if (exception != null) {
-            val exceptionType: EtsType = when (exception.sort) {
-                ctx.addressSort -> {
-                    // If it's an object reference, try to determine its type
-                    val ref = exception.asExpr(ctx.addressSort)
-                    // For now, assume it's a generic error type
-                    EtsStringType // TODO: improve type detection
-                }
-
-                ctx.fp64Sort -> EtsNumberType
-
-                ctx.boolSort -> EtsBooleanType
-
-                else -> EtsStringType
-            }
-
-            scope.doWithState {
-                methodResult = TsMethodResult.TsException(exception, exceptionType)
-            }
-        } else {
-            scope.doWithState {
-                // If we couldn't resolve the exception value, throw a generic exception
-                methodResult = TsMethodResult.TsException(ctx.mkUndefinedValue(), EtsStringType)
-            }
+        scope.doWithState {
+            methodResult = TsMethodResult.TsException(exception, exceptionType)
         }
     }
 

usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt

@@ -89,6 +89,8 @@ class TsState(
     var boundedStringBackingRefs: Set<UHeapRef> = emptySet(),
     /** Unresolved reference payloads that may acquire string backing after type refinement. */
     var symbolicStringCandidates: Set<UHeapRef> = emptySet(),
+    /** Exception delivered to the current catch block, before its binding is initialized. */
+    var caughtException: UExpr<*>? = null,
     var unsupportedReason: String? = null,
     private val activeUnknownCallModels: MutableList<Pair<String, Int>> = mutableListOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
@@ -326,6 +328,7 @@ class TsState(
             stringConstantAllocatedRefs = stringConstantAllocatedRefs,
             boundedStringBackingRefs = boundedStringBackingRefs,
             symbolicStringCandidates = symbolicStringCandidates,
+            caughtException = caughtException,
             unsupportedReason = unsupportedReason,
             activeUnknownCallModels = activeUnknownCallModels.toMutableList(),
         )

usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt

@@ -153,7 +153,8 @@ class ImportExportResolutionTest {
         assertIs<SymbolResolutionResult.Success>(result)
         assertTrue(result.exportInfo.isDefaultExport)
         assertEquals("default", result.exportInfo.name)
-        assertEquals("Helper", result.exportInfo.originalName)
+        assertEquals(expected = "default", actual = result.exportInfo.originalName)
+        assertEquals(expected = "Helper", actual = result.exportInfo.nameBeforeAs)
         assertEquals(EtsExportType.CLASS, result.exportInfo.type)
     }
 
@@ -319,7 +320,8 @@ class ImportExportResolutionTest {
         val result = scene.resolveImportInfo(currentFile, importInfo)
         assertIs<SymbolResolutionResult.Success>(result)
         assertEquals("default", result.exportInfo.name)
-        assertEquals("Helper", result.exportInfo.originalName)
+        assertEquals(expected = "default", actual = result.exportInfo.originalName)
+        assertEquals(expected = "Helper", actual = result.exportInfo.nameBeforeAs)
     }
 
     @Test

usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt

@@ -0,0 +1,127 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.StateCollectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+import kotlin.test.assertTrue
+import kotlin.time.Duration
+
+class TsCatchRoutingTest : TsMethodTestRunner() {
+    @TempDir
+    lateinit var directory: Path
+
+    private val source = getResourcePath("/samples/lang/Exceptions.ts")
+    override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)))
+    private val analysisOptions = UMachineOptions(
+        pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+        solverType = SolverType.YICES,
+        solverTimeout = Duration.INFINITE,
+        typeOperationsTimeout = Duration.INFINITE,
+        stateCollectionStrategy = StateCollectionStrategy.ALL,
+        stopOnCoverage = 0,
+        throwExceptionOnStepFailure = true,
+    )
+
+    @Test
+    fun `catch paths retain the thrown value and replay in Node`() {
+        val conditionalCatch = getMethod(methodName = "conditionalCatch", className = "Exceptions")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = conditionalCatch,
+            { input, result -> input.number == 0.0 && result.number == 2.0 },
+            { input, result -> input.number != 0.0 && result.number == 1.0 },
+            invariants = arrayOf({ input, result -> result.number == (if (input.number == 0.0) 2.0 else 1.0) }),
+        )
+
+        for (name in listOf("caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter")) {
+            val method = getMethod(methodName = name, className = "Exceptions")
+            discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+                method = method,
+                { input, result -> result.number == input.number + 1.0 },
+                invariants = arrayOf({ input, result -> result.number == input.number + 1.0 }),
+            )
+        }
+
+        val tests = listOf("conditionalCatch", "caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter")
+            .associateWith(::analyze)
+
+        assertEquals(setOf(1, 2), tests.getValue("conditionalCatch").map(::resultNumber).toSet())
+        tests.forEach { (name, generated) ->
+            generated.forEach { test -> assertExpectedResult(name, test) }
+        }
+
+        replay(tests)
+    }
+
+    private fun assertExpectedResult(name: String, test: TsTest) {
+        val input = assertIs<TsTestValue.TsNumber>(test.before.parameters.single()).number
+        val expected = when (name) {
+            "conditionalCatch" -> if (input == 0.0) 2.0 else 1.0
+            "caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter" -> input + 1.0
+            else -> error("Unexpected method $name")
+        }
+
+        assertEquals(expected, assertIs<TsTestValue.TsNumber>(test.returnValue).number, "$name: $test")
+    }
+
+    private fun analyze(name: String): List<TsTest> {
+        val method = scene.projectClasses.single { it.name == "Exceptions" }
+            .methods
+            .single { it.name == name }
+        val result = TsMachine(
+            scene = scene,
+            options = analysisOptions,
+            tsOptions = TsOptions(),
+        ).use { machine ->
+            machine.analyzeWithOutcome(methods = listOf(method))
+        }
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason, name)
+        assertTrue(result.unsupportedPaths.isEmpty(), "$name: ${result.unsupportedPaths}")
+        assertTrue(result.states.isNotEmpty(), name)
+        assertTrue(result.states.all { it.methodResult is TsMethodResult.Success }, name)
+
+        return result.states.map { state -> TsTestResolver().resolve(method, state) }
+    }
+
+    private fun resultNumber(test: TsTest): Int =
+        assertIs<TsTestValue.TsNumber>(test.returnValue).number.toInt()
+
+    private fun replay(tests: Map<String, List<TsTest>>) {
+        val script = buildString {
+            appendLine(source.readText())
+            tests.forEach { (name, generated) ->
+                generated.forEachIndexed { index, test ->
+                    val input = assertIs<TsTestValue.TsNumber>(test.before.parameters.single()).number
+                    val expected = assertIs<TsTestValue.TsNumber>(test.returnValue).number
+
+                    appendLine("if (new Exceptions().$name($input) !== $expected) {")
+                    appendLine("  throw Error('$name witness $index');")
+                    appendLine("}")
+                }
+            }
+        }
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "catch-routing",
+            timeoutMessage = "Node replay timed out",
+        )
+    }
+}

usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt

@@ -98,4 +98,44 @@ class Exceptions : TsMethodTestRunner() {
             },
         )
     }
+
+    @Test
+    fun `conditional catch only handles the throwing path`() {
+        val method = getMethod("conditionalCatch")
+
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { value, result -> (value eq 0) && (result eq 2) },
+            { value, result -> !(value eq 0) && (result eq 1) },
+            invariants = arrayOf(
+                { value, result -> if (value eq 0) result eq 2 else result eq 1 },
+            ),
+        )
+    }
+
+    @Test
+    fun `catch binding receives the thrown number`() {
+        val method = getMethod("caughtValue")
+
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { value, result -> result eq (value.number + 1.0) },
+            invariants = arrayOf(
+                { value, result -> result eq (value.number + 1.0) },
+            ),
+        )
+    }
+
+    @Test
+    fun `nested catch uses the nearest handler`() {
+        val method = getMethod("nestedCatch")
+
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { value, result -> result eq (value.number + 1.0) },
+            invariants = arrayOf(
+                { value, result -> result eq (value.number + 1.0) },
+            ),
+        )
+    }
 }

usvm-ts/src/test/resources/samples/lang/Exceptions.ts

@@ -38,4 +38,59 @@ class Exceptions {
         }
         return 42;
     }
+
+    conditionalCatch(value: number): number {
+        try {
+            if (value === 0) {
+                throw 7;
+            }
+            return 1;
+        } catch {
+            return 2;
+        }
+    }
+
+    caughtValue(value: number): number {
+        try {
+            throw value;
+        } catch (error) {
+            return error + 1;
+        }
+    }
+
+    nestedCatch(value: number): number {
+        try {
+            try {
+                throw value;
+            } catch (inner) {
+                return inner + 1;
+            }
+        } catch (outer) {
+            return 99;
+        }
+    }
+
+    throwsValue(value: number): number {
+        throw value;
+    }
+
+    catchesCall(value: number): number {
+        try {
+            return this.throwsValue(value);
+        } catch (error) {
+            return error + 1;
+        }
+    }
+
+    rethrowToOuter(value: number): number {
+        try {
+            try {
+                throw value;
+            } catch (inner) {
+                throw inner;
+            }
+        } catch (outer) {
+            return outer + 1;
+        }
+    }
 }