Share TypeScript analysis and UTF-16 infrastructure between PBT and Calls

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
@@ -248,7 +248,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 {
@@ -479,7 +479,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,
         )

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 = """

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
@@ -377,7 +377,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,

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt

@@ -59,6 +59,26 @@ class CallsSourceReplayTest {
         assertEquals(false, untakenReplay.invocation?.targetHit)
     }
 
+    @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()

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');
 }

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>

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 {

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(

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)
 

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt

@@ -2,14 +2,14 @@ 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.ArrayIndexGenerator
 import org.usvm.ts.pbt.model.PropertyAssertion
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.PropertySourceIdentity
 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
@@ -55,7 +55,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)

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)
+            }
+        }
+    }
+}

usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/Utf16JsonTest.kt

@@ -0,0 +1,80 @@
+package org.usvm.ts.pbt.model
+
+import kotlinx.serialization.decodeFromString
+import kotlinx.serialization.encodeToString
+import kotlinx.serialization.json.Json
+import org.junit.jupiter.api.Test
+import java.security.MessageDigest
+import java.util.concurrent.TimeUnit
+import kotlin.test.assertEquals
+import kotlin.test.assertFalse
+import kotlin.test.assertNotEquals
+import kotlin.test.assertTrue
+
+class Utf16JsonTest {
+    @Test
+    fun `all UTF-16 code units survive JSON UTF-8 transport`() {
+        val source = (Char.MIN_VALUE..Char.MAX_VALUE).joinToString(separator = "")
+        val value: JsConcreteValue = JsConcreteValue.Array(listOf(JsConcreteValue.String(source)))
+
+        val encoded = Json.encodeToUtf8SafeString(value)
+        val transported = encoded.toByteArray(Charsets.UTF_8).toString(Charsets.UTF_8)
+
+        assertFalse(encoded.any { it.isSurrogate() })
+        assertEquals(value, Json.decodeFromString<JsConcreteValue>(transported))
+    }
+
+    @Test
+    fun `plain JSON remains unchanged and escaping is idempotent`() {
+        val original = Json.encodeToString("quotes: \" slash: \\ literal: \\ud800 Cyrillic: привет")
+        val surrogate = Json.encodeToUtf8SafeString("\ud800\udc00\udfff")
+
+        assertEquals(original, escapeJsonSurrogates(original))
+        assertEquals(surrogate, escapeJsonSurrogates(surrogate))
+    }
+
+    @Test
+    fun `different isolated surrogates retain distinct UTF-8 hashes`() {
+        val digests = listOf("\ud800", "\ud801", "?").map { value ->
+            val encoded = Json.encodeToUtf8SafeString<JsConcreteValue>(JsConcreteValue.String(value))
+            MessageDigest.getInstance("SHA-256").digest(encoded.toByteArray(Charsets.UTF_8)).toList()
+        }
+
+        assertEquals(3, digests.distinct().size)
+        assertNotEquals(digests[0], digests[1])
+    }
+
+    @Test
+    fun `ordinary JsonElement roundtrip retains string contents`() {
+        val value: JsConcreteValue = JsConcreteValue.Array(listOf(JsConcreteValue.String("\ud800")))
+
+        val tree = Json.encodeToJsonElement(JsConcreteValueSerializer, value)
+        val decoded = Json.decodeFromJsonElement(JsConcreteValueSerializer, tree)
+
+        assertEquals(value, decoded)
+    }
+
+    @Test
+    fun `Node receives exact UTF-16 units through the unchanged tagged schema`() {
+        val source = "\ud800?\udfff\ud83d\ude00\"\\\n"
+        val encoded = Json.encodeToUtf8SafeString<JsConcreteValue>(JsConcreteValue.String(source))
+        val script = """
+            const input = JSON.parse(require('fs').readFileSync(0, 'utf8'));
+            if (input.kind !== 'string') process.exit(2);
+            const units = Array.from({length: input.value.length}, (_, i) => input.value.charCodeAt(i));
+            process.stdout.write(JSON.stringify(units));
+        """.trimIndent()
+        val process = ProcessBuilder("node", "-e", script).redirectErrorStream(true).start()
+
+        try {
+            process.outputStream.use { it.write(encoded.toByteArray(Charsets.UTF_8)) }
+            assertTrue(process.waitFor(10, TimeUnit.SECONDS))
+            val output = process.inputStream.bufferedReader().readText()
+
+            assertEquals(0, process.exitValue(), output)
+            assertEquals(source.map { it.code }, Json.decodeFromString<List<Int>>(output))
+        } finally {
+            process.destroyForcibly()
+        }
+    }
+}

usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt

@@ -2,6 +2,7 @@ package org.usvm.machine
 
 import org.jacodb.ets.model.EtsAssignStmt
 import org.jacodb.ets.model.EtsCallExpr
+import org.jacodb.ets.model.EtsCallStmt
 import org.jacodb.ets.model.EtsIfStmt
 import org.jacodb.ets.model.EtsReturnStmt
 import org.jacodb.ets.model.EtsStmt
@@ -35,6 +36,15 @@ interface TsInterpreterObserver : UInterpreterObserver {
         // default empty implementation
     }
 
+    /** Called after a completed assignment stores its value, before execution advances. */
+    fun onAssignmentCompleted(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsAssignStmt,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+
     // TODO on entry point
 
     fun onCallWithUnresolvedArguments(
@@ -45,6 +55,15 @@ interface TsInterpreterObserver : UInterpreterObserver {
         // default empty implementation
     }
 
+    /** Called before a standalone call starts, while its arguments denote the current state. */
+    fun onCallStatement(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsCallStmt,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+
     // TODO onCallWithResolvedArguments
 
     fun onIfStatement(