UnitTestBot · CaelmBleidd · Oct 1, 2026
diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/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 = "86b07fc9fb"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt
@@ -3,7 +3,6 @@ package org.usvm.ts.calls
 import kotlinx.serialization.SerialName
 import kotlinx.serialization.Serializable
 import kotlinx.serialization.decodeFromString
-import kotlinx.serialization.encodeToString
 import kotlinx.serialization.json.Json
 import org.usvm.PathSelectionStrategy
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
@@ -12,6 +11,7 @@ import org.usvm.machine.call.TsUnknownCallEvent
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.TypeScriptEntryPoint
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.file.Files
 import java.nio.file.Path
 import java.nio.file.StandardCopyOption
@@ -247,7 +247,7 @@ internal object CallsExperimentJson {
 
     fun decodeManifest(value: String): CallsExperimentManifest = json.decodeFromString(value)
 
-    fun encodeManifest(manifest: CallsExperimentManifest): String = json.encodeToString(manifest)
+    fun encodeManifest(manifest: CallsExperimentManifest): String = json.encodeToUtf8SafeString(manifest)
 }
 
 internal object CallsBuildIdentity {
@@ -470,7 +470,7 @@ internal class CallsExperimentRunner(
     private fun append(path: Path, record: CallsRawRecord) {
         Files.writeString(
             path,
-            CallsExperimentJson.json.encodeToString<CallsRawRecord>(record) + "\n",
+            CallsExperimentJson.json.encodeToUtf8SafeString<CallsRawRecord>(record) + "\n",
             StandardOpenOption.CREATE,
             StandardOpenOption.APPEND,
         )

diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt
@@ -1,7 +1,7 @@
 package org.usvm.ts.calls
 
-import kotlinx.serialization.encodeToString
 import kotlinx.serialization.json.Json
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.file.Files
 import java.nio.file.Path
 
@@ -47,7 +47,7 @@ internal fun replayWitness(args: List<String>) {
         selector = selector,
     )
 
-    val encoded = CallsExperimentJson.json.encodeToString(result)
+    val encoded = CallsExperimentJson.json.encodeToUtf8SafeString(result)
     System.out.appendLine(encoded)
 }
 
@@ -82,7 +82,7 @@ private fun summarize(args: List<String>) {
         prettyPrint = true
     }
     output.parent?.let(Files::createDirectories)
-    Files.writeString(output, json.encodeToString(summary) + "\n")
+    Files.writeString(output, json.encodeToUtf8SafeString(summary) + "\n")
 }
 
 private fun usage(): String = """

diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt
@@ -3,7 +3,6 @@ package org.usvm.ts.calls
 import kotlinx.serialization.SerialName
 import kotlinx.serialization.Serializable
 import kotlinx.serialization.decodeFromString
-import kotlinx.serialization.encodeToString
 import org.usvm.ts.pbt.backend.PropertyFailureKind
 import org.usvm.ts.pbt.backend.PropertyRunConfiguration
 import org.usvm.ts.pbt.backend.PropertyRunStatus
@@ -21,6 +20,7 @@ import org.usvm.ts.pbt.model.PropertyId
 import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.TupleDomain
 import org.usvm.ts.pbt.model.TypeScriptEntryPoint
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.file.Files
 import java.nio.file.LinkOption
 import java.nio.file.Path
@@ -385,7 +385,7 @@ internal class OriginalTypeScriptTargetReplayer : CallsTargetReplayer {
         }
     """.trimIndent() + "\n"
 
-    private fun jsString(value: String): String = CallsExperimentJson.json.encodeToString(value)
+    private fun jsString(value: String): String = CallsExperimentJson.json.encodeToUtf8SafeString(value)
 
     private data class ResolvedTarget(
         val sourceRootIndex: Int,

diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt
@@ -9,7 +9,6 @@ import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsLexicalEnvType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsNumberType
-import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnclearRefType
 import org.usvm.UBoolExpr
@@ -37,10 +36,10 @@ import org.usvm.ts.pbt.model.PropertyDomain
 import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.StringDomain
 import org.usvm.util.markDenseInputArray
-import org.usvm.util.markStringMaxLength
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
+import org.usvm.util.mkStringFromCodeUnits
 
 internal fun PropertyDomain.isSupportedCallsSymbolicDomain(): Boolean = when (this) {
     BooleanDomain, is NumberDomain, is StringDomain -> true
@@ -202,39 +201,11 @@ private fun TsState.initializeStringInput(
     stackSlot: Int,
     domain: StringDomain,
 ): StringInputSnapshot = with(ctx) {
-    val stringRef = memory.allocConcrete(EtsStringType)
-    val characterArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
-    val descriptor = arrayDescriptorOf(characterArrayType)
-    val charactersRef = memory.allocConcrete(descriptor)
     val length: UExpr<TsSizeSort> = makeSymbolicPrimitive(sizeSort)
     val codeUnits: List<UExpr<KBv16Sort>> = List(domain.maxLength) { makeSymbolicPrimitive(bv16Sort) }
 
     constrainLength(length = length, minLength = domain.minLength, maxLength = domain.maxLength)
-    memory.initializeArrayLength(
-        arrayHeapRef = charactersRef,
-        type = descriptor,
-        sizeSort = sizeSort,
-        count = length,
-    )
-    codeUnits.forEachIndexed { index, codeUnit ->
-        val liveIndex = mkBvSignedLessExpr(mkBv(index), length)
-        memory.write(
-            mkArrayIndexLValue(
-                sort = bv16Sort,
-                ref = charactersRef,
-                index = mkBv(index),
-                type = characterArrayType,
-            ),
-            codeUnit,
-            guard = liveIndex,
-        )
-    }
-    memory.write(
-        mkFieldLValue(addressSort, stringRef, "value"),
-        charactersRef.asExpr(addressSort),
-        guard = trueExpr,
-    )
-    markStringMaxLength(string = stringRef, maxLength = domain.maxLength)
+    val stringRef = mkStringFromCodeUnits(length = length, codeUnits = codeUnits)
     memory.write(
         mkRegisterStackLValue(addressSort, stackSlot),
         stringRef.asExpr(addressSort),

diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt
@@ -10,6 +10,26 @@ import kotlin.test.assertEquals
 import kotlin.test.assertNotNull
 
 class CallsSourceReplayTest {
+    @Test
+    fun `original source replay preserves an isolated UTF-16 surrogate`() {
+        val fixture = fixture()
+        val target = fixture.target(functionName = "isolatedSurrogate", statement = "return 13;")
+
+        val surrogate = fixture.replay(
+            exportName = "isolatedSurrogate",
+            inputs = listOf(JsConcreteValue.String("\ud800")),
+            target = target,
+        )
+        val replacement = fixture.replay(
+            exportName = "isolatedSurrogate",
+            inputs = listOf(JsConcreteValue.String("?")),
+            target = target,
+        )
+
+        assertEquals(CallsReplayStatus.CONFIRMED, surrogate.status, surrogate.toString())
+        assertEquals(CallsReplayStatus.REJECTED, replacement.status, replacement.toString())
+    }
+
     @Test
     fun `confirms only the exact source statement reached by original TypeScript`() {
         val fixture = fixture()

diff --git a/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts b/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts
@@ -1,5 +1,12 @@
 export function inlineChoose(value: number): number { if (value > 0) { return 1; } return 0; }
 
+export function isolatedSurrogate(value: string): number {
+  if (value.length === 1 && value.charCodeAt(0) === 0xd800) {
+    return 13;
+  }
+  return 0;
+}
+
 export function throwsAtTarget(): never {
   throw new Error('expected');
 }

diff --git a/usvm-ts-dataflow/src/main/resources/logback.xml b/usvm-ts-dataflow/src/main/resources/logback.xml
@@ -1,11 +1,12 @@
 <configuration>
-    <appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
+    <appender name="STDERR" class="ch.qos.logback.core.ConsoleAppender">
+        <target>System.err</target>
         <encoder>
             <pattern>%highlight([%level]) %replace(%c{0}){'(\$Companion)?\$logger\$1',''} - %msg%n</pattern>
         </encoder>
     </appender>
 
     <root level="info">
-        <appender-ref ref="STDOUT" />
+        <appender-ref ref="STDERR" />
     </root>
 </configuration>
diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt
@@ -3,7 +3,6 @@ package org.usvm.ts.pbt.cli
 import kotlinx.serialization.Serializable
 import kotlinx.serialization.SerializationException
 import kotlinx.serialization.decodeFromString
-import kotlinx.serialization.encodeToString
 import org.usvm.ts.pbt.FastCheckDiagnosticCode
 import org.usvm.ts.pbt.backend.CoverageCapabilityLevel
 import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend
@@ -15,6 +14,7 @@ import org.usvm.ts.pbt.manifest.PropertyManifestJson
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyId
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import org.usvm.ts.pbt.registry.DuplicatePropertyIdException
 import org.usvm.ts.pbt.registry.PropertyRegistry
 import org.usvm.ts.pbt.registry.PropertyRegistryProvider
@@ -127,7 +127,7 @@ class FastCheckCli(
         requireCoverageSupport(options, backend)
         val results = properties.map { property -> backend.run(property, configuration) }
 
-        output.appendLine(PropertyManifestJson.json.encodeToString(results))
+        output.appendLine(PropertyManifestJson.json.encodeToUtf8SafeString(results))
 
         val hasPropertyFailure = results.any { result -> result.status == PropertyRunStatus.FAILURE }
         return if (hasPropertyFailure) {
@@ -311,7 +311,7 @@ class FastCheckCli(
             kind = kind,
         )
 
-        errors.appendLine(PropertyManifestJson.json.encodeToString(diagnostic))
+        errors.appendLine(PropertyManifestJson.json.encodeToUtf8SafeString(diagnostic))
     }
 
     private companion object {

diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt
@@ -1,11 +1,11 @@
 package org.usvm.ts.pbt.fastcheck
 
 import kotlinx.serialization.decodeFromString
-import kotlinx.serialization.encodeToString
 import org.usvm.ts.pbt.FastCheckDiagnosticCode
 import org.usvm.ts.pbt.backend.PropertyRunResult
 import org.usvm.ts.pbt.manifest.PropertyManifestJson
 import org.usvm.ts.pbt.model.PropertyId
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.file.Path
 
 /** Encodes one execution request and validates the private fast-check adapter response. */
@@ -74,7 +74,7 @@ internal class FastCheckProcessClient(
     }
 
     private fun encodeRequest(request: FastCheckExecutionRequest): String {
-        val encodedRequest = PropertyManifestJson.json.encodeToString(request)
+        val encodedRequest = PropertyManifestJson.json.encodeToUtf8SafeString(request)
 
         if (encodedRequest.toByteArray(Charsets.UTF_8).size > MAX_REQUEST_BYTES) {
             throw backendError(

diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt
@@ -1,10 +1,10 @@
 package org.usvm.ts.pbt.fastcheck
 
 import kotlinx.serialization.decodeFromString
-import kotlinx.serialization.encodeToString
 import org.usvm.ts.pbt.FastCheckDiagnosticCode
 import org.usvm.ts.pbt.manifest.PropertyManifestJson
 import org.usvm.ts.pbt.model.contains
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.file.Path
 
 /** Limits for one projection request to the private Node adapter. */
@@ -55,7 +55,7 @@ class FastCheckProjectionClient private constructor(
     fun sample(request: FastCheckProjectionRequest): FastCheckProjectionResponse {
         validateRequest(request)
 
-        val encodedRequest = PropertyManifestJson.json.encodeToString(request)
+        val encodedRequest = PropertyManifestJson.json.encodeToUtf8SafeString(request)
         val output = invokeAdapter(encodedRequest)
         val response = decodeResponse(output)
 

diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt
@@ -2,11 +2,11 @@ package org.usvm.ts.pbt.manifest
 
 import kotlinx.serialization.Serializable
 import kotlinx.serialization.decodeFromString
-import kotlinx.serialization.encodeToString
 import kotlinx.serialization.json.Json
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.TypeScriptEntryPoint
+import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import org.usvm.ts.pbt.validation.requireValid
 import org.usvm.ts.pbt.validation.validatePropertyDefinition
 import org.usvm.ts.pbt.validation.validatePropertyManifest
@@ -46,7 +46,7 @@ object PropertyManifestJson {
 
     fun encode(manifest: PropertyManifest): String {
         requireValid(validatePropertyManifest(manifest))
-        return json.encodeToString(manifest)
+        return json.encodeToUtf8SafeString(manifest)
     }
 
     fun decode(value: String): PropertyManifest = json.decodeFromString<PropertyManifest>(value)

diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/Utf16Json.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/Utf16Json.kt
@@ -0,0 +1,28 @@
+package org.usvm.ts.pbt.model
+
+import kotlinx.serialization.encodeToString
+import kotlinx.serialization.json.Json
+
+/** Encodes JSON for UTF-8 transport without replacing JavaScript's isolated UTF-16 surrogates. */
+inline fun <reified T> Json.encodeToUtf8SafeString(value: T): String =
+    escapeJsonSurrogates(encodeToString(value))
+
+/**
+ * Escapes surrogate code units in an already encoded JSON document. All other JSON text is unchanged.
+ * Escaping paired units too preserves their value and avoids making transport depend on UTF-8 error handling.
+ * Keep this at the text boundary: JsonElement string contents must retain their original UTF-16 value.
+ */
+fun escapeJsonSurrogates(json: String): String {
+    if (json.none { it.isSurrogate() }) return json
+
+    return buildString {
+        json.forEach { unit ->
+            if (unit.isSurrogate()) {
+                append("\\u")
+                append(unit.code.toString(radix = 16).padStart(length = 4, padChar = '0'))
+            } else {
+                append(unit)
+            }
+        }
+    }
+}