From 97dbf0b03840827f3525e662cbab528949efd242 Mon Sep 17 00:00:00 2001
From: Aleksei Menshutin <a.menshutin@vkteam.ru>
Date: Tue, 22 Sep 2026 14:37:54 +0300
Subject: [PATCH] Handle conditional string operands before type lookup

---
 .../calls/CurrentTsCallsSymbolicEngineTest.kt | 43 ++++++++++++++++++-
 .../org/usvm/machine/expr/TsExprResolver.kt   | 15 ++++++-
 2 files changed, 55 insertions(+), 3 deletions(-)

diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt
index 03bf910e9..26a4a6d72 100644
--- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt
+++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt
@@ -54,6 +54,46 @@ class CurrentTsCallsSymbolicEngineTest {
         assertTrue(result.diagnostic.orEmpty().contains("ARRAY_NAMED_PROPERTY_WRITE"))
     }
 
+    @Test
+    fun `fresh unknown string index branches remain executable and extractable`() {
+        val alphabet = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ~!@#${'$'}%^&*_-+=|:.><?/'"
+        val fixture = fixture(
+            source = """
+                export function encodeNum(n: number): string {
+                    const enc = "$alphabet";
+                    const base = enc.length;
+                    let ret = '';
+                    do {
+                        ret += enc[n % base];
+                        n = Math.floor(n / base);
+                    } while (n >= 1);
+                    return ret;
+                }
+
+                let nUid = 0;
+
+                export function uid(): string {
+                    return encodeNum(nUid++);
+                }
+            """.trimIndent(),
+            exportName = "uid",
+            inputs = emptyList(),
+            targetStatement = "return encodeNum(nUid++);",
+            targetMode = CallsSourceTargetMode.COMPLETED_RETURN,
+            returnExpression = "encodeNum(nUid++)",
+        )
+        val unknownCalls = mutableListOf<TsUnknownCallEvent>()
+
+        val result = fixture.search(
+            modelIds = emptySet(),
+            profile = CallsExperimentProfile.EMPTY_FRESH,
+            unknownCallEventSink = unknownCalls::add,
+        )
+
+        assertEquals(CallsSymbolicStatus.REACHED, result.status, "$result; unknownCalls=$unknownCalls")
+        assertEquals(emptyList(), result.inputs)
+    }
+
     @Test
     fun `bundled frontend accepts only the revision baked into the running build`() {
         val engine = CurrentTsCallsSymbolicEngine(
@@ -904,6 +944,7 @@ class CurrentTsCallsSymbolicEngineTest {
 
         fun search(
             modelIds: Set<String>,
+            profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP,
             unknownCallEventSink: ((TsUnknownCallEvent) -> Unit)? = null,
             runtimeLimitationEventSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)? = null,
         ): CallsSymbolicSearchResult = engine.search(
@@ -912,7 +953,7 @@ class CurrentTsCallsSymbolicEngineTest {
                 project = project,
                 function = function,
                 target = target,
-                profile = CallsExperimentProfile.FROZEN_STOP,
+                profile = profile,
                 frozenModelIds = modelIds,
                 expectedNativeFrontendRevision = "bundled:test",
                 seed = 0,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 52397ba30..99f05ccf8 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -575,6 +575,18 @@ class TsExprResolver(
     }
 
     private fun stringStorageRef(value: UExpr<*>): UHeapRef? = with(ctx) {
+        if (value is UIteExpr<*>) {
+            val trueBranch = stringStorageRef(value.trueBranch) ?: return null
+            val falseBranch = stringStorageRef(value.falseBranch) ?: return null
+
+            return mkIte(value.condition, trueBranch, falseBranch)
+        }
+
+        val concrete = concreteStringValue(value)
+        if (concrete != null && (value == mkTsNullValue() || value == mkUndefinedValue())) {
+            return mkStringConstant(concrete, scope)
+        }
+
         if (value.sort == addressSort) {
             val ref = value.asExpr(addressSort)
             val type = scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() }
@@ -583,8 +595,7 @@ class TsExprResolver(
             }
         }
 
-        val concrete = concreteStringValue(value) ?: return null
-        mkStringConstant(concrete, scope)
+        concrete?.let { mkStringConstant(it, scope) }
     }
 
     private fun concreteStringValue(value: UExpr<*>): String? = with(ctx) {