[TS] Materialize symbolic string input witnesses

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/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/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
@@ -743,6 +744,7 @@ class TsInterpreter(
             ctx = ctx,
             ownership = MutabilityOwnership(),
             entrypoint = method,
+            maxStringLength = options.maxArraySize,
             targets = UTargetsSet.from(targets),
         )
 
@@ -811,6 +813,19 @@ 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))
             }
 
             val parameterSort = typeToSort(parameterType)

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

@@ -1,6 +1,5 @@
 package org.usvm.machine.state
 
-import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBlockCfg
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsFile
@@ -48,6 +47,7 @@ class TsState(
     ctx: TsContext,
     ownership: MutabilityOwnership,
     override val entrypoint: EtsMethod,
+    val maxStringLength: Int,
     callStack: UCallStack<EtsMethod, EtsStmt> = UCallStack(),
     pathConstraints: UPathConstraints<EtsType> = UPathConstraints(ctx, ownership),
     memory: UMemory<EtsType, EtsMethod> = UMemory(ctx, ownership, pathConstraints.typeConstraints),
@@ -254,20 +254,17 @@ class TsState(
             memory.types.allocate(ref.address, EtsStringType)
 
             // Initialize char array
-            val valueType = EtsArrayType(EtsNumberType, dimensions = 1)
-            val descriptor = ctx.arrayDescriptorOf(valueType)
-
-            val charArray = memory.allocConcrete(valueType.elementType)
+            val charArray = memory.allocConcrete(EtsNumberType)
             memory.initializeArray(
                 arrayHeapRef = charArray,
-                type = descriptor,
+                type = stringBackingArrayDescriptor,
                 sort = bv16Sort,
                 sizeSort = sizeSort,
                 contents = value.asSequence().map { mkBv(it.code, bv16Sort) },
             )
 
             // Write char array to `ref.value`
-            val valueLValue = mkFieldLValue(addressSort, ref, "value")
+            val valueLValue = mkFieldLValue(addressSort, ref, field = "value")
             memory.write(valueLValue, charArray, guard = trueExpr)
 
             ref
@@ -289,6 +286,7 @@ class TsState(
             ctx = ctx,
             ownership = cloneOwnership,
             entrypoint = entrypoint,
+            maxStringLength = maxStringLength,
             callStack = callStack.clone(),
             pathConstraints = clonedConstraints,
             memory = memory.clone(clonedConstraints.typeConstraints, newThisOwnership, cloneOwnership),

usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt

@@ -1,5 +1,6 @@
 package org.usvm.util
 
+import io.ksmt.sort.KBv16Sort
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsField
 import org.jacodb.ets.model.EtsFieldSignature
@@ -76,6 +77,19 @@ fun mkArrayLengthLValue(
     return UArrayLengthLValue(ref, descriptor, sizeSort)
 }
 
+internal fun mkStringBackingLengthLValue(
+    ref: UHeapRef,
+): UArrayLengthLValue<EtsType, TsSizeSort> = with(ref.tctx) {
+    UArrayLengthLValue(ref, stringBackingArrayDescriptor, sizeSort)
+}
+
+internal fun mkStringBackingElementLValue(
+    ref: UHeapRef,
+    index: UExpr<TsSizeSort>,
+): UArrayIndexLValue<EtsType, KBv16Sort, TsSizeSort> = with(ref.tctx) {
+    UArrayIndexLValue(bv16Sort, ref, index, stringBackingArrayDescriptor)
+}
+
 fun <Sort : USort> mkRegisterStackLValue(
     sort: Sort,
     idx: Int,

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

@@ -0,0 +1,82 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsScene
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import org.usvm.util.jsString
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+import kotlin.time.Duration
+
+private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000
+
+class TsStringWitnessBoundTest : TsMethodTestRunner() {
+    @TempDir
+    lateinit var directory: Path
+
+    private val tsPath = "/samples/lang/SymbolicStringInput.ts"
+
+    override val scene: EtsScene = loadScene(tsPath)
+
+    @Test
+    fun `configured string bound is shared with concrete test extraction`() {
+        val method = getMethod(methodName = "lengthIs10001", className = "SymbolicStringInput")
+        val maxStringLength = 10_001
+        val machineOptions = UMachineOptions(
+            pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+            solverType = SolverType.YICES,
+            solverTimeout = Duration.INFINITE,
+            typeOperationsTimeout = Duration.INFINITE,
+        )
+
+        val tests = TsMachine(
+            scene = scene,
+            options = machineOptions,
+            tsOptions = TsOptions(maxArraySize = maxStringLength),
+        ).use { machine ->
+            machine.analyze(methods = listOf(method)).map { state -> TsTestResolver().resolve(method, state) }
+        }
+
+        assertEquals(
+            setOf(0.0, 1.0),
+            tests.map { test -> assertIs<TsTestValue.TsNumber>(test.returnValue).number }.toSet(),
+        )
+        val longWitness = tests.single { test ->
+            assertIs<TsTestValue.TsNumber>(test.returnValue).number == 1.0
+        }
+        assertEquals(
+            maxStringLength,
+            assertIs<TsTestValue.TsString>(longWitness.before.parameters.single()).value.length,
+        )
+
+        val script = buildString {
+            appendLine(getResourcePath(tsPath).readText())
+            tests.forEachIndexed { index, test ->
+                val input = assertIs<TsTestValue.TsString>(test.before.parameters.single()).value
+                val expected = assertIs<TsTestValue.TsNumber>(test.returnValue).number
+
+                appendLine("if (new SymbolicStringInput().lengthIs10001(${jsString(input)}) !== $expected) {")
+                appendLine("  throw Error('string bound witness $index');")
+                appendLine("}")
+            }
+        }
+
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "string-bound",
+            timeoutMessage = "String bound replay timed out",
+            failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT),
+        )
+    }
+}

usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt

@@ -14,9 +14,9 @@ import org.usvm.api.TsTestValue
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.jsString
 import java.nio.file.Path
-import java.util.concurrent.TimeUnit
-import kotlin.io.path.readText
 import kotlin.io.path.writeText
 import kotlin.test.assertEquals
 import kotlin.test.assertIs
@@ -64,7 +64,12 @@ class TsArrayShiftReplayTest {
                         appendLine("}")
                     }
                 }
-                assertReplay(script, index)
+                assertNodeReplay(
+                    source = script,
+                    directory = directory,
+                    name = "replay$index",
+                    timeoutMessage = "Replay timed out",
+                )
             }
         }
     }
@@ -436,29 +441,6 @@ class TsArrayShiftReplayTest {
         else -> error("Unsupported replay value: $value")
     }
 
-    private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString(
-        separator = "",
-        prefix = "\"",
-        postfix = "\"",
-    )
-
-    private fun assertReplay(source: String, index: Int) {
-        val script = directory.resolve("replay$index.ts")
-        val output = directory.resolve("replay$index.out")
-        script.writeText(source)
-        val process = ProcessBuilder("node", "--experimental-strip-types", script.toString())
-            .redirectErrorStream(true)
-            .redirectOutput(output.toFile())
-            .start()
-
-        try {
-            assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Replay timed out")
-            assertEquals(0, process.exitValue(), "${output.readText()}\n$source")
-        } finally {
-            if (process.isAlive) process.destroyForcibly()
-        }
-    }
-
     private data class ReplayCase(
         val name: String,
         val parameters: String,

usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt

@@ -15,11 +15,11 @@ import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
 import org.usvm.util.getResourcePath
+import org.usvm.util.jsString
 import java.nio.file.Path
-import java.util.concurrent.TimeUnit
 import kotlin.io.path.readText
-import kotlin.io.path.writeText
 import kotlin.test.assertEquals
 import kotlin.test.assertIs
 import kotlin.test.assertTrue
@@ -81,7 +81,12 @@ class TsInstanceCallReceiverTest {
                         appendLine("}")
                     }
                 }
-                assertReplay(replay, case.method)
+                assertNodeReplay(
+                    source = replay,
+                    directory = directory,
+                    name = case.method,
+                    timeoutMessage = "Receiver replay timed out",
+                )
             }
         }
     }
@@ -98,29 +103,6 @@ class TsInstanceCallReceiverTest {
         else -> error("Unsupported receiver input: $value")
     }
 
-    private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString(
-        separator = "",
-        prefix = "\"",
-        postfix = "\"",
-    )
-
-    private fun assertReplay(source: String, name: String) {
-        val script = directory.resolve("$name.ts")
-        val output = directory.resolve("$name.out")
-        script.writeText(source)
-        val process = ProcessBuilder("node", "--experimental-strip-types", script.toString())
-            .redirectErrorStream(true)
-            .redirectOutput(output.toFile())
-            .start()
-
-        try {
-            assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Receiver replay timed out")
-            assertEquals(0, process.exitValue(), "${output.readText()}\n$source")
-        } finally {
-            if (process.isAlive) process.destroyForcibly()
-        }
-    }
-
     private data class Case(
         val method: String,
         val results: Set<Double>,