[TS] Compare string values in equality operators

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/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

@@ -17,7 +17,7 @@ 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.mkStringBackingLValue
 import org.usvm.util.mkStringBackingLengthLValue
 
 // Handles reading the `length` property.
@@ -40,8 +40,7 @@ fun TsContext.readLengthProperty(
 
         is EtsStringType -> {
             val charsRef = scope.calcOnState {
-                val valueLValue = mkFieldLValue(addressSort, instance, field = "value")
-                memory.read(valueLValue)
+                memory.read(mkStringBackingLValue(instance))
             }
 
             return readArrayLength(

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

@@ -69,7 +69,9 @@ import org.usvm.machine.state.lastStmt
 import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.parametersWithThisCount
+import org.usvm.machine.state.prepareRefinedStringBackings
 import org.usvm.machine.state.returnValue
+import org.usvm.machine.state.symbolicStringBackingConstraint
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.machine.types.toAuxiliaryType
 import org.usvm.sizeSort
@@ -82,7 +84,6 @@ 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
@@ -135,6 +136,8 @@ class TsInterpreter(
         //  if no call, visit
 
         try {
+            scope.prepareRefinedStringBackings() ?: return scope.stepResult()
+
             when (stmt) {
                 is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt)
                 is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt)
@@ -151,6 +154,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
@@ -814,18 +829,8 @@ class TsInterpreter(
 
                 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.pathConstraints += state.symbolicStringBackingConstraint(ref)
+                state.boundedStringBackingRefs += ref
             }
 
             val parameterSort = typeToSort(parameterType)