[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 = "7a2cda3bfd9175ba11a60e47ff4a32e6e3e209e2"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

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

@@ -149,19 +149,29 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
             MachineResult(
                 states = entryObserver.reachedStates,
                 stopReason = outcome.stopReason,
+                unsupportedPaths = outcome.unsupportedPaths,
             )
         }
         val states = analysis.states
         if (states.isEmpty()) {
             val status = when (analysis.stopReason) {
-                TsAnalysisStopReason.EXHAUSTED -> CallsSymbolicStatus.UNREACHED
+                TsAnalysisStopReason.EXHAUSTED -> {
+                    if (analysis.unsupportedPaths.isEmpty()) {
+                        CallsSymbolicStatus.UNREACHED
+                    } else {
+                        CallsSymbolicStatus.UNSUPPORTED
+                    }
+                }
                 // The machine options above disable every stop condition except the per-target timeout.
-                TsAnalysisStopReason.STOPPED -> CallsSymbolicStatus.TIMEOUT
+                TsAnalysisStopReason.STOPPED -> {
+                    CallsSymbolicStatus.TIMEOUT
+                }
             }
 
             return result(
                 status = status,
                 startedAt = startedAt,
+                diagnostic = analysis.unsupportedPaths.joinToString().ifEmpty { null },
             )
         }
 
@@ -284,6 +294,7 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
     private data class MachineResult(
         val states: List<TsState>,
         val stopReason: TsAnalysisStopReason,
+        val unsupportedPaths: List<String>,
     )
 }
 

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -17,6 +17,7 @@ import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberLiteralType
 import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsParameterRef
+import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringLiteralType
@@ -66,6 +67,9 @@ class TsContext(
 
     val unresolvedSort: TsUnresolvedSort = TsUnresolvedSort(this)
 
+    /** Array storage for UTF-16 code units; ordinary TypeScript arrays never use this region. */
+    internal val stringBackingArrayDescriptor: EtsType = EtsRawType(kind = "usvm.ts.string.backing")
+
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 

usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

@@ -49,6 +49,8 @@ enum class TsAnalysisStopReason {
 data class TsAnalysisResult(
     val states: List<TsState>,
     val stopReason: TsAnalysisStopReason,
+    /** Reasons for satisfiable paths excluded by an explicit engine model bound. */
+    val unsupportedPaths: List<String>,
 )
 
 class TsMachine(
@@ -101,6 +103,7 @@ class TsMachine(
     )
     private val cfgStatistics = CfgStatisticsImpl(graph)
 
+    /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */
     fun analyze(
         methods: List<EtsMethod>,
         targets: List<TsTarget> = emptyList(),
@@ -154,6 +157,7 @@ class TsMachine(
 
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
+        val unsupportedPaths = mutableSetOf<String>()
 
         if (tsOptions.enableVisualization) {
             observers += TsStateVisualizer()
@@ -202,10 +206,25 @@ class TsMachine(
             )
         }
 
+        val supportedObserver = CompositeUMachineObserver(observers)
+        val outcomeObserver = object : UMachineObserver<TsState> by supportedObserver {
+            override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
+                val unsupportedReason = state.unsupportedReason
+                if (unsupportedReason != null) {
+                    if (stateReachable) {
+                        unsupportedPaths += unsupportedReason
+                    }
+                    return
+                }
+
+                supportedObserver.onStateTerminated(state, stateReachable)
+            }
+        }
+
         run(
             interpreter,
             pathSelector,
-            observer = CompositeUMachineObserver(observers),
+            observer = outcomeObserver,
             isStateTerminated = { state -> state.callStack.isEmpty() },
             stopStrategy = stopStrategy
         )
@@ -216,7 +235,11 @@ class TsMachine(
             TsAnalysisStopReason.STOPPED
         }
 
-        return TsAnalysisResult(states = statesCollector.collectedStates, stopReason = stopReason)
+        return TsAnalysisResult(
+            states = statesCollector.collectedStates,
+            stopReason = stopReason,
+            unsupportedPaths = unsupportedPaths.toList(),
+        )
     }
 
     override fun close() {

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

@@ -6,14 +6,19 @@ import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsStringType
+import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnknownType
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsSizeSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.sizeSort
 import org.usvm.util.arrayStorageType
 import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.mkFieldLValue
+import org.usvm.util.mkStringBackingLengthLValue
 
 // Handles reading the `length` property.
 fun TsContext.readLengthProperty(
@@ -34,31 +39,39 @@ fun TsContext.readLengthProperty(
         }
 
         is EtsStringType -> {
-            // Strings are treated as arrays of characters (represented as strings).
-            EtsArrayType(EtsStringType, dimensions = 1)
+            val charsRef = scope.calcOnState {
+                val valueLValue = mkFieldLValue(addressSort, instance, field = "value")
+                memory.read(valueLValue)
+            }
+
+            return readArrayLength(
+                scope = scope,
+                lengthLValue = mkStringBackingLengthLValue(charsRef),
+                maxArraySize = maxArraySize,
+            )
         }
 
         else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type")
     }
 
     // Read the length of the array.
-    return readArrayLength(scope, instance, arrayType, maxArraySize)
+    return readArrayLength(
+        scope = scope,
+        lengthLValue = mkArrayLengthLValue(instance, arrayType),
+        maxArraySize = maxArraySize,
+    )
 }
 
 // Reads the length of the array and returns it as a fp64 expression.
 fun TsContext.readArrayLength(
     scope: TsStepScope,
-    array: UHeapRef,
-    arrayType: EtsArrayType,
+    lengthLValue: UArrayLengthLValue<EtsType, TsSizeSort>,
     maxArraySize: Int,
 ): UExpr<KFp64Sort>? {
-    checkNotFake(array)
+    checkNotFake(lengthLValue.ref)
 
     // Read the length of the array.
-    val length = scope.calcOnState {
-        val lengthLValue = mkArrayLengthLValue(array, arrayType)
-        memory.read(lengthLValue)
-    }
+    val length = scope.calcOnState { memory.read(lengthLValue) }
 
     // Check that the length is within the allowed bounds.
     ensureLengthBounds(scope, length, maxArraySize) ?: return null

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

@@ -1023,8 +1023,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

@@ -82,6 +82,7 @@ import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
+import org.usvm.util.mkStringBackingLengthLValue
 import org.usvm.util.resolveEtsMethods
 import org.usvm.util.type
 import org.usvm.utils.ensureSat
@@ -109,11 +110,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()
@@ -150,6 +158,18 @@ class TsInterpreter(
                     }
                 }
             }
+        } catch (e: UnsupportedOperationException) {
+            if (throwExceptionOnStepFailure) {
+                throw e
+            }
+
+            val reason = e.message?.takeIf(String::isNotBlank) ?: "Unsupported TypeScript operation"
+            state.terminateAsUnsupported(reason)
+
+            return StepResult(
+                forkedStates = scope.stepResult().forkedStates,
+                originalStateAlive = true,
+            )
         } catch (e: Exception) {
             if (throwExceptionOnStepFailure) {
                 throw e
@@ -686,37 +706,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)
         }
     }
 
@@ -743,6 +742,7 @@ class TsInterpreter(
             ctx = ctx,
             ownership = MutabilityOwnership(),
             entrypoint = method,
+            maxStringLength = options.maxArraySize,
             targets = UTargetsSet.from(targets),
         )
 
@@ -811,6 +811,20 @@ class TsInterpreter(
                 state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
 
                 state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType)
+
+                // String constants store UTF-16 code units in their `value` array.
+                // Give symbolic inputs the same backing representation and bound its length.
+                val charsType = EtsArrayType(EtsNumberType, dimensions = 1)
+                val valueLValue = mkFieldLValue(addressSort, ref, field = "value")
+                val charsRef = state.memory.read(valueLValue).asExpr(addressSort)
+                state.pathConstraints += mkNot(mkHeapRefEq(charsRef, mkUndefinedValue()))
+                state.pathConstraints += state.memory.types.evalTypeEquals(charsRef, charsType)
+
+                val lengthLValue = mkStringBackingLengthLValue(charsRef)
+                val length = state.memory.read(lengthLValue).asExpr(sizeSort)
+                state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0))
+                state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize))
+                state.boundedStringBackingRefs += ref
             }
 
             val parameterSort = typeToSort(parameterType)