[TS] Prepare dynamic string contents before truthiness and equality

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

@@ -455,8 +455,8 @@ private fun TsExprResolver.handleBooleanConstructor(expr: EtsInstanceCallExpr):
     }
     val arg = resolve(expr.args.single()) ?: return null
 
-    val truthy = mkTruthyExpr(arg, scope)
     scope.ensureTruthinessSupported(arg) ?: return null
+    val truthy = mkTruthyExpr(arg, scope)
 
     truthy
 }

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

@@ -68,8 +68,8 @@ private fun TsExprResolver.handleBooleanConverter(expr: EtsStaticCallExpr): UExp
     }
     val arg = resolve(expr.args.single()) ?: return null
 
-    val truthy = mkTruthyExpr(arg, scope)
     scope.ensureTruthinessSupported(arg) ?: return null
+    val truthy = mkTruthyExpr(arg, scope)
 
     return truthy
 }

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

@@ -24,6 +24,7 @@ import org.usvm.machine.TsSizeSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
+import org.usvm.machine.state.prepareStringBacking
 import org.usvm.machine.types.EtsFakeType
 import org.usvm.machine.types.ExprWithTypeConstraint
 import org.usvm.types.single
@@ -162,6 +163,7 @@ private fun TsState.unsupportedTruthinessCondition(expr: UExpr<out USort>): UBoo
 
 /** Validate the execution path separately from constructing its boolean expression. */
 fun TsStepScope.ensureTruthinessSupported(expr: UExpr<out USort>): Unit? {
+    prepareTruthinessStringBacking(expr) ?: return null
     val unsupportedString = calcOnState { unsupportedTruthinessCondition(expr) }
     if (unsupportedString.isFalse) return Unit
 
@@ -171,6 +173,41 @@ fun TsStepScope.ensureTruthinessSupported(expr: UExpr<out USort>): Unit? {
     })
 }
 
+private fun TsStepScope.prepareTruthinessStringBacking(
+    expr: UExpr<out USort>,
+    activeGuard: UBoolExpr = calcOnState { ctx.trueExpr },
+): Unit? {
+    val context = calcOnState { ctx }
+    val hasFakeBranches = with(context) {
+        expr.sort == addressSort && expr.asExpr(addressSort).hasFakeValueBranch()
+    }
+    if (expr is UIteExpr<*> && hasFakeBranches) {
+        val trueGuard = context.mkAnd(activeGuard, expr.condition)
+        val falseGuard = context.mkAnd(activeGuard, context.mkNot(expr.condition))
+        prepareTruthinessStringBacking(expr.trueBranch, trueGuard) ?: return null
+        return prepareTruthinessStringBacking(expr.falseBranch, falseGuard)
+    }
+
+    val isFake = with(context) { expr.isFakeObject() }
+    if (isFake) {
+        val fakeValue = expr as UConcreteHeapRef
+        val (reference, referenceGuard) = calcOnState {
+            with(ctx) {
+                val type = fakeValue.getFakeType(memory)
+                val guard = mkAnd(activeGuard, type.refTypeExpr)
+
+                memory.read(getIntermediateRefLValue(fakeValue.address)) to guard
+            }
+        }
+        return prepareStringBacking(reference, referenceGuard)
+    }
+    if (expr.sort == context.addressSort) {
+        return prepareStringBacking(expr.asExpr(context.addressSort), activeGuard)
+    }
+
+    return Unit
+}
+
 /** Construct a condition; call [ensureTruthinessSupported] before executing with it. */
 fun TsContext.mkTruthyExpr(
     expr: UExpr<out USort>,

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

@@ -542,14 +542,14 @@ class TsInterpreter(
 
         val expr = exprResolver.resolve(stmt.condition) ?: return
 
+        scope.ensureTruthinessSupported(expr) ?: return
+
         val boolExpr = if (expr.sort == ctx.boolSort) {
             expr.asExpr(ctx.boolSort)
         } else {
             ctx.mkTruthyExpr(expr, scope)
         }
 
-        scope.ensureTruthinessSupported(expr) ?: return
-
         observer?.onIfStatementWithResolvedCondition(simpleValueResolver, stmt, boolExpr, scope)
 
         val successors = graph.successors(stmt).take(2).toList()

usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt

@@ -20,10 +20,12 @@ import org.usvm.machine.TsContext
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.expr.ensureTruthinessSupported
 import org.usvm.machine.expr.mkIsNullOrUndefined
+import org.usvm.machine.expr.mkNotNullOrUndefined
 import org.usvm.machine.expr.mkNumericExpr
 import org.usvm.machine.expr.mkNumericExprWithGuard
 import org.usvm.machine.expr.mkTruthyExpr
 import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.prepareStringBacking
 import org.usvm.machine.types.ExprWithTypeConstraint
 import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.util.boolToFp
@@ -260,6 +262,12 @@ private fun TsContext.stringValueEquals(
     if (lhsIsString.isFalse || rhsIsString.isFalse) return falseExpr
 
     val bothStrings = mkAnd(lhsIsString, rhsIsString)
+    val lhsNonNullish = mkNotNullOrUndefined(lhs)
+    val rhsNonNullish = mkNotNullOrUndefined(rhs)
+    val stringComparisonGuard = mkAnd(activeGuard, bothStrings, lhsNonNullish, rhsNonNullish)
+    scope.prepareStringBacking(lhs, stringComparisonGuard) ?: return null
+    scope.prepareStringBacking(rhs, stringComparisonGuard) ?: return null
+
     val missingBacking = scope.calcOnState {
         (lhsConstant == null && lhs !in boundedStringBackingRefs) ||
             (rhsConstant == null && rhs !in boundedStringBackingRefs)
@@ -379,6 +387,9 @@ private fun TsContext.referenceOrStringValueEquals(
     val sameReference = mkHeapRefEq(lhs, rhs)
     if (sameReference.isTrue) return trueExpr
 
+    val comparesNullishConstant = mkIsNullOrUndefined(lhs).isTrue || mkIsNullOrUndefined(rhs).isTrue
+    if (comparesNullishConstant) return sameReference
+
     val equalStringValues = stringValueEquals(lhs, rhs, sameReference, activeGuard, scope) ?: return null
     return mkOr(sameReference, equalStringValues)
 }
@@ -1445,8 +1456,8 @@ sealed interface TsBinaryOperator {
         ): UExpr<*>? {
             check(lhs.isFakeObject() || rhs.isFakeObject())
 
-            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
             scope.ensureTruthinessSupported(lhs) ?: return null
+            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
 
             return scope.calcOnState {
                 iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs)
@@ -1460,8 +1471,8 @@ sealed interface TsBinaryOperator {
         ): UExpr<*>? {
             check(!lhs.isFakeObject() && !rhs.isFakeObject())
 
-            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
             scope.ensureTruthinessSupported(lhs) ?: return null
+            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
 
             return scope.calcOnState {
                 iteWriteIntoFakeObject(scope, lhsTruthyExpr, rhs, lhs)
@@ -1501,8 +1512,8 @@ sealed interface TsBinaryOperator {
         ): UExpr<*>? {
             check(lhs.isFakeObject() || rhs.isFakeObject())
 
-            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
             scope.ensureTruthinessSupported(lhs) ?: return null
+            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
 
             return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
         }
@@ -1514,8 +1525,8 @@ sealed interface TsBinaryOperator {
         ): UExpr<*>? {
             check(!lhs.isFakeObject() && !rhs.isFakeObject())
 
-            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
             scope.ensureTruthinessSupported(lhs) ?: return null
+            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
 
             return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
         }

usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsUnaryOperator.kt

@@ -70,8 +70,8 @@ sealed interface TsUnaryOperator {
             arg: UExpr<UAddressSort>,
             scope: TsStepScope,
         ): UBoolExpr? {
-            val truthy = mkTruthyExpr(arg, scope)
             scope.ensureTruthinessSupported(arg) ?: return null
+            val truthy = mkTruthyExpr(arg, scope)
 
             return mkNot(truthy)
         }
@@ -80,8 +80,8 @@ sealed interface TsUnaryOperator {
             arg: UConcreteHeapRef,
             scope: TsStepScope,
         ): UBoolExpr? {
-            val truthy = mkTruthyExpr(arg, scope)
             scope.ensureTruthinessSupported(arg) ?: return null
+            val truthy = mkTruthyExpr(arg, scope)
 
             return mkNot(truthy)
         }

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

@@ -12,6 +12,8 @@ import org.usvm.UNullRef
 import org.usvm.USymbolicHeapRef
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.typeStreamOf
+import org.usvm.isFalse
+import org.usvm.isTrue
 import org.usvm.machine.expr.mkNotNullOrUndefined
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.solver.UUnsatResult
@@ -45,6 +47,40 @@ internal fun TsState.symbolicStringBackingConstraint(ref: UHeapRef): UBoolExpr =
     mkAnd(definedBacking, backingType, nonnegativeLength, boundedLength)
 }
 
+/** Split the runtime string alternative before reading contents; other values retain their original state. */
+internal fun TsStepScope.prepareStringBacking(ref: UHeapRef, activeGuard: UBoolExpr): Unit? {
+    val context = calcOnState { ctx }
+    if (ref is UIteExpr<*>) {
+        val trueGuard = context.mkAnd(activeGuard, ref.condition)
+        val falseGuard = context.mkAnd(activeGuard, context.mkNot(ref.condition))
+        prepareStringBacking(ref.trueBranch.asExpr(context.addressSort), trueGuard) ?: return null
+        return prepareStringBacking(ref.falseBranch.asExpr(context.addressSort), falseGuard)
+    }
+    val needsBacking = calcOnState { ref is USymbolicHeapRef && ref !in boundedStringBackingRefs }
+    if (!needsBacking) return Unit
+
+    val stringCondition = calcOnState {
+        val stringType = memory.types.evalTypeEquals(ref, EtsStringType)
+        val nonNullish = ctx.mkNotNullOrUndefined(ref)
+        ctx.mkAnd(activeGuard, stringType, nonNullish)
+    }
+    if (stringCondition.isFalse) return Unit
+
+    val takeString = calcOnState { models.first().eval(stringCondition).isTrue }
+    val selectedCondition = if (takeString) stringCondition else context.mkNot(stringCondition)
+    fork(selectedCondition) ?: return null
+    if (!takeString) return Unit
+
+    val backingConstraint = calcOnState { symbolicStringBackingConstraint(ref) }
+    assert(backingConstraint) ?: return null
+    doWithState {
+        boundedStringBackingRefs += ref to maxStringLength
+        symbolicStringCandidates -= ref
+    }
+
+    return Unit
+}
+
 /** Prepare only references that are already non-nullish strings on this execution path. */
 internal fun TsStepScope.prepareRefinedStringBackings(): Unit? {
     val candidates = calcOnState {

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

@@ -13,7 +13,6 @@ import org.usvm.api.TsTest
 import org.usvm.api.TsTestValue
 import org.usvm.util.TsMethodTestRunner
 import org.usvm.util.TsTestResolver
-import org.usvm.util.TsUnsupportedWitnessException
 import org.usvm.util.assertNodeReplay
 import org.usvm.util.getResourcePath
 import org.usvm.util.jsString
@@ -25,14 +24,11 @@ import kotlin.test.assertTrue
 import kotlin.time.Duration
 
 private const val TRUTHINESS_REPLAY_FAILURE_CONTEXT_LIMIT = 1000
-private const val UNBACKED_STRING_REASON = "Truthiness needs a modeled string backing for dynamic references"
-private const val MISSING_STRING_BACKING_PREFIX = "Symbolic string is missing backing array:"
 
 class TsDynamicTruthinessTest : TsMethodTestRunner() {
     private data class AnalysisWitnesses(
         val analysis: TsAnalysisResult,
         val witnesses: List<TsTest>,
-        val unsupportedWitnesses: List<String>,
     )
 
     @TempDir
@@ -42,14 +38,23 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() {
     override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)))
 
     @Test
-    fun `unbacked any strings are unsupported in truthiness without losing object paths`() {
+    fun `dynamic truthiness prepares string backing without losing object paths`() {
         discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
             method = getMethod(methodName = "objectTruthy", className = "SymbolicStringInput"),
             { _, result -> result.number == 1.0 },
             invariants = arrayOf({ _, result -> result.number == 1.0 }),
         )
 
-        val names = setOf("anyTruthy", "anyNegated", "anyAnd", "anyOr", "anyObjectTruthy", "objectTruthy")
+        val names = setOf(
+            "anyTruthy",
+            "anyNegated",
+            "anyAnd",
+            "anyOr",
+            "anyObjectTruthy",
+            "objectTruthy",
+            "truthinessBeforeKind",
+            "equalsObjectBeforeKind",
+        )
         val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods
             .filter { it.name in names }
             .associateBy { it.name }
@@ -59,6 +64,7 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() {
             solverTimeout = Duration.INFINITE,
             typeOperationsTimeout = Duration.INFINITE,
             stateCollectionStrategy = StateCollectionStrategy.ALL,
+            stopOnCoverage = 0,
         )
 
         val results = TsMachine(
@@ -68,47 +74,25 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() {
         ).use { machine ->
             methods.mapValues { (_, method) ->
                 val analysis = machine.analyzeWithOutcome(listOf(method))
-                val unsupportedWitnesses = mutableListOf<String>()
-                val witnesses = analysis.states.mapNotNull { state ->
-                    try {
-                        TsTestResolver().resolve(method, state)
-                    } catch (e: TsUnsupportedWitnessException) {
-                        if (method.name != "anyObjectTruthy" ||
-                            e.message?.startsWith(MISSING_STRING_BACKING_PREFIX) != true
-                        ) {
-                            throw e
-                        }
-
-                        unsupportedWitnesses += e.message.orEmpty()
-                        null
-                    }
-                }
+                val witnesses = analysis.states.map { state -> TsTestResolver().resolve(method, state) }
 
-                AnalysisWitnesses(analysis, witnesses, unsupportedWitnesses)
+                AnalysisWitnesses(analysis, witnesses)
             }
         }
 
         assertEquals(names, methods.keys)
         results.forEach { (name, result) ->
-            val (analysis, witnesses, unsupportedWitnesses) = result
+            val (analysis, witnesses) = result
             assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason)
-            if (name == "objectTruthy") {
-                assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}")
-            } else if (name == "anyObjectTruthy") {
-                assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}")
-                assertTrue(
-                    unsupportedWitnesses.isEmpty(),
-                    "$name regressed a string witness prepared after type refinement: $unsupportedWitnesses",
-                )
+            assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}")
+            if (name == "anyObjectTruthy") {
                 assertTrue(
                     witnesses.any { witness ->
                         witness.before.parameters.single() is TsTestValue.TsClass &&
                             assertIs<TsTestValue.TsNumber>(witness.returnValue).number == 1.0
                     },
                     "$name lost its object path",
                 )
-            } else {
-                assertTrue(UNBACKED_STRING_REASON in analysis.unsupportedPaths, "$name: ${analysis.unsupportedPaths}")
             }
             assertTrue(witnesses.isNotEmpty(), "$name produced no supported witnesses")
         }
@@ -143,4 +127,32 @@ class TsDynamicTruthinessTest : TsMethodTestRunner() {
             failureContext = script.take(TRUTHINESS_REPLAY_FAILURE_CONTEXT_LIMIT),
         )
     }
+
+    @Test
+    fun `truthiness before type refinement retains empty strings null and undefined`() {
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method = getMethod(methodName = "truthinessBeforeKind", className = "SymbolicStringInput"),
+            { input, result -> input is TsTestValue.TsString && input.value.isEmpty() && result.number == 10.0 },
+            { input, result -> input is TsTestValue.TsString && input.value.isNotEmpty() && result.number == 21.0 },
+            { input, result -> input == TsTestValue.TsNull && result.number == 30.0 },
+            { input, result -> input == TsTestValue.TsUndefined && result.number == 40.0 },
+        )
+    }
+
+    @Test
+    fun `object equality before type refinement retains all runtime kinds`() {
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method = getMethod(methodName = "equalsObjectBeforeKind", className = "SymbolicStringInput"),
+            { input, result -> input is TsTestValue.TsString && result.number == 10.0 },
+            { input, result -> input == TsTestValue.TsNull && result.number == 20.0 },
+            { input, result -> input == TsTestValue.TsUndefined && result.number == 30.0 },
+            { input, result ->
+                val otherKind = input !is TsTestValue.TsString &&
+                    input != TsTestValue.TsNull && input != TsTestValue.TsUndefined
+
+                otherKind && result.number == 40.0
+            },
+            invariants = arrayOf({ _, result -> result.number < 100.0 }),
+        )
+    }
 }