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 index 994ee9e322..c73673579a 100644 --- 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 @@ -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(record) + "\n", + CallsExperimentJson.json.encodeToUtf8SafeString(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 index fda9021f1c..2dc0a6448d 100644 --- 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) { 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) { 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 index cf53a6874a..ab1a8a021c 100644 --- 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 @@ -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, 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 index 055ffa7261..8345526a19 100644 --- 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 @@ -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() diff --git a/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts b/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts index 58eac3cae7..1ba8c94235 100644 --- 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 index 40d03b09a6..4ba96c668c 100644 --- a/usvm-ts-dataflow/src/main/resources/logback.xml +++ b/usvm-ts-dataflow/src/main/resources/logback.xml @@ -1,11 +1,12 @@ - + + System.err %highlight([%level]) %replace(%c{0}){'(\$Companion)?\$logger\$1',''} - %msg%n - + 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 index 00a80ff686..9bfb02c65b 100644 --- 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 index 43d3980eed..5f71da5460 100644 --- 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 index c00614d8d4..adc64a1ffa 100644 --- 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 index 03f0617c55..df4286a978 100644 --- 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,7 +2,6 @@ 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 @@ -10,6 +9,7 @@ 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(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 new file mode 100644 index 0000000000..d75c5beee5 --- /dev/null +++ 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 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) + } + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/Utf16JsonTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/Utf16JsonTest.kt new file mode 100644 index 0000000000..0dd1441f92 --- /dev/null +++ b/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(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.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.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>(output)) + } finally { + process.destroyForcibly() + } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 3051e1f9de..4e64a3119d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/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( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index eecba58aa9..9be48cfad6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -65,7 +65,10 @@ data class TsMachineAnalysisResult( val unsupportedCall: Boolean, val engineFailed: Boolean, val unsupportedPaths: List, -) +) { + /** Includes execution bounds and unsupported entry inputs retained in [unsupportedPaths]. */ + val runtimeLimited: Boolean get() = unsupportedPaths.isNotEmpty() +} class TsMachine( scene: EtsScene, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index a30bd0db0e..aa82ca3837 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -689,6 +689,8 @@ class TsInterpreter( assignTo(scope, stmt.lhv, expr) ?: return } + observer?.onAssignmentCompleted(exprResolver.simpleValueResolver, stmt, scope) + val nextStmt = stmt.nextStmt ?: return scope.doWithState { newStmt(nextStmt) } } @@ -701,8 +703,10 @@ class TsInterpreter( return } + val exprResolver = exprResolverWithScope(scope) + observer?.onCallStatement(exprResolver.simpleValueResolver, stmt, scope) + if (options.interproceduralAnalysis) { - val exprResolver = exprResolverWithScope(scope) exprResolver.resolve(stmt.expr) ?: return val nextStmt = stmt.nextStmt ?: return scope.doWithState { newStmt(nextStmt) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsStringValue.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsStringValue.kt index 468b8bf18f..eb792d1c2b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/TsStringValue.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsStringValue.kt @@ -1,6 +1,7 @@ package org.usvm.util import io.ksmt.expr.KBitVec16Value +import io.ksmt.sort.KBv16Sort import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringType @@ -8,7 +9,6 @@ import org.jacodb.ets.model.EtsType import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef -import org.usvm.api.initializeArray import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive import org.usvm.machine.TsSizeSort @@ -21,29 +21,37 @@ import org.usvm.sizeSort fun TsState.mkSymbolicString(minLength: Int, maxLength: Int): UConcreteHeapRef = with(ctx) { require(minLength >= 0 && maxLength >= minLength) { "Invalid symbolic string length bounds" } + val length = makeSymbolicPrimitive(sizeSort) + val codeUnits = List(maxLength) { makeSymbolicPrimitive(bv16Sort) } + val string = mkStringFromCodeUnits(length = length, codeUnits = codeUnits) + pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(minLength)) + + string +} + +/** Builds a UTF-16 string using the same private backing regions as ordinary string operations. */ +fun TsState.mkStringFromCodeUnits( + length: UExpr, + codeUnits: List>, +): UConcreteHeapRef = with(ctx) { val string = memory.allocConcrete(EtsStringType) val charactersType = EtsArrayType(EtsNumberType, dimensions = 1) val characters = memory.allocConcrete(charactersType) - val length = makeSymbolicPrimitive(sizeSort) - val meetsMinimum = mkBvSignedGreaterOrEqualExpr(length, mkBv(minLength)) - val meetsMaximum = mkBvSignedLessOrEqualExpr(length, mkBv(maxLength)) - val contents = sequence { - repeat(maxLength) { - yield(makeSymbolicPrimitive(bv16Sort)) - } - } + val nonnegativeLength = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val withinCapacity = mkBvSignedLessOrEqualExpr(length, mkBv(codeUnits.size)) - memory.initializeArray( - arrayHeapRef = characters, - type = stringBackingArrayDescriptor, - sort = bv16Sort, - sizeSort = sizeSort, - contents = contents, - ) memory.initializeArrayLength(characters, stringBackingArrayDescriptor, sizeSort, length) + codeUnits.forEachIndexed { index, codeUnit -> + val position = mkBv(index) + memory.write( + mkStringBackingElementLValue(characters, position), + codeUnit, + guard = mkBvSignedLessExpr(position, length), + ) + } memory.write(mkStringBackingLValue(string), characters, guard = trueExpr) - pathConstraints += mkAnd(meetsMinimum, meetsMaximum) - boundedStringBackingRefs += string to maxLength + pathConstraints += mkAnd(nonnegativeLength, withinCapacity) + boundedStringBackingRefs += string to codeUnits.size string } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt new file mode 100644 index 0000000000..e67df781a5 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt @@ -0,0 +1,78 @@ +package org.usvm.machine + +import io.ksmt.sort.KBv16Sort +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.api.makeSymbolicPrimitive +import org.usvm.sizeSort +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.mkStringFromCodeUnits +import org.usvm.util.resolveStringValue +import kotlin.test.assertEquals +import kotlin.test.assertIs + +class StringEngineTest : TsMethodTestRunner() { + private val file = loadEtsFileAutoConvert( + getResourcePath("/models/SymbolicStringEngine.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + override val scene = EtsScene(listOf(file)) + + @Test + fun `length uses UTF-16 units through a widened alias`() { + discoverProperties( + method = getMethod(methodName = "length", className = "SymbolicStringEngine"), + { value -> value.number == 2.0 }, + invariants = arrayOf({ value -> value.number == 2.0 }), + ) + discoverProperties( + method = getMethod(methodName = "anyAliasLength", className = "SymbolicStringEngine"), + { value -> value.number == 1.0 }, + invariants = arrayOf({ value -> value.number == 1.0 }), + ) + } + + /** Exercises the explicit code-unit allocation API, not source input discovery. */ + @Test + fun `shared allocation and bounded decoding preserve a solver selected surrogate`() { + val method = getMethod(methodName = "inputRoundtrip", className = "SymbolicStringEngine") + lateinit var input: UConcreteHeapRef + val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL) + + TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + val states = machine.analyze( + methods = listOf(method), + configureInitialState = { _, state -> + with(state.ctx) { + val length: UExpr = state.makeSymbolicPrimitive(sizeSort) + val unit: UExpr = state.makeSymbolicPrimitive(bv16Sort) + state.pathConstraints += mkEq(length, mkBv(1)) + state.pathConstraints += mkEq(unit, mkBv(0xd800, bv16Sort)) + input = state.mkStringFromCodeUnits(length = length, codeUnits = listOf(unit)) + state.memory.write( + mkRegisterStackLValue(addressSort, 1), + input.asExpr(addressSort), + guard = trueExpr, + ) + } + }, + ) + + val state = states.single() + assertEquals("\ud800", state.resolveStringValue(input, model = state.models.single(), maxLength = 1)) + val decoded = TsTestResolver().resolve(method, state).returnValue + assertEquals("\ud800", assertIs(decoded).value) + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt new file mode 100644 index 0000000000..c58e180e51 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt @@ -0,0 +1,168 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.machine.expr.TsSimpleValueResolver +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.util.getResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsSharedAnalysisTest { + private val file = loadEtsFileAutoConvert( + getResourcePath("/models/SharedAnalysis.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(projectFiles = listOf(file)) + private val options = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + solverType = SolverType.Z3, + ) + private val tsOptions = TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + maxArraySize = 2, + ) + + @Test + fun `step limit and zero time budget have distinct metadata`() { + val limited = analyze(options = options.copy(stepLimit = 1uL)) + val timedOut = analyze(options = options.copy(timeout = Duration.ZERO)) + + assertEquals(TsAnalysisStopReason.STOPPED, limited.stopReason) + assertFalse(limited.timedOut) + assertEquals(TsAnalysisStopReason.STOPPED, timedOut.stopReason) + assertTrue(timedOut.timedOut) + assertTrue(timedOut.states.isEmpty()) + } + + @Test + fun `stopped residual and runtime limitation are distinct and reset per analysis`() { + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { events += "call" } + } + + TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + val unknown = machine.analyzeWithMetadata(methods = listOf(method("unknown"))) + val limited = machine.analyzeWithMetadata(methods = listOf(method("limited"))) + val success = machine.analyzeWithMetadata(methods = listOf(method("success"))) + + assertTrue(unknown.unsupportedCall) + assertFalse(unknown.runtimeLimited) + assertFalse(unknown.engineFailed) + assertFalse(limited.unsupportedCall) + assertTrue(limited.runtimeLimited) + assertFalse(limited.engineFailed) + assertFalse(success.unsupportedCall) + assertFalse(success.runtimeLimited) + assertFalse(success.engineFailed) + assertTrue(limited.unsupportedPaths.any { "length bound" in it }, limited.unsupportedPaths.toString()) + assertEquals(listOf("call"), events) + } + } + + @Test + fun `fresh residual return is not reported as a stopped call`() { + val result = TsMachine( + scene = scene, + options = options, + tsOptions = tsOptions.copy(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + ).use { it.analyzeWithMetadata(methods = listOf(method("unknown"))) } + + assertFalse(result.unsupportedCall) + assertFalse(result.engineFailed) + assertTrue(result.states.isNotEmpty()) + } + + @Test + fun `suppressed step failure is reported and reset for a later analysis`() { + var shouldFail = true + val observer = object : TsInterpreterObserver { + override fun onReturnStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsReturnStmt, + scope: TsStepScope, + ) { + check(!shouldFail) { "Injected interpreter callback failure" } + } + } + + TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + val failed = machine.analyzeWithMetadata(methods = listOf(method("success"))) + shouldFail = false + val recovered = machine.analyzeWithMetadata(methods = listOf(method("success"))) + + assertTrue(failed.engineFailed) + assertTrue(failed.states.isEmpty()) + assertFalse(recovered.engineFailed) + assertEquals(1, recovered.states.size) + } + } + + @Test + fun `observers see standalone calls once and assignments after their value is stored`() { + val calls = mutableListOf() + var assignments = 0 + val observer = object : TsInterpreterObserver { + override fun onCallStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsCallStmt, + scope: TsStepScope, + ) { + calls += stmt.expr.callee.name + } + + override fun onAssignmentCompleted( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsAssignStmt, + scope: TsStepScope, + ) { + if ((stmt.lhv as? EtsLocal)?.name != "result") return + + assignments++ + val value = stmt.lhv.accept(simpleValueResolver) + val expected = scope.calcOnState { ctx.mkFp(7.0, ctx.fp64Sort) } + assertEquals(expected, value) + } + } + + TsMachine( + scene = scene, + options = options.copy(throwExceptionOnStepFailure = true), + tsOptions = tsOptions, + observer = observer, + ).use { machine -> + machine.analyze(methods = listOf(method("observed"))) + machine.analyze(methods = listOf(method("unknown"))) + } + + assertEquals(listOf("callee"), calls) + assertEquals(1, assignments) + } + + private fun method(name: String) = scene.projectClasses.single { it.name == "SharedAnalysis" } + .methods + .single { it.name == name } + + private fun analyze(options: UMachineOptions) = TsMachine( + scene = scene, + options = options, + tsOptions = tsOptions, + ).use { it.analyzeWithMetadata(methods = listOf(method("success"))) } +} diff --git a/usvm-ts/src/test/resources/models/SharedAnalysis.ts b/usvm-ts/src/test/resources/models/SharedAnalysis.ts new file mode 100644 index 0000000000..ae1c4bb7f7 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SharedAnalysis.ts @@ -0,0 +1,35 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +declare class External { + static value(): number; +} + +export class SharedAnalysis { + identity(value: any): any { + return value; + } + + success(): number { + return 7; + } + + unknown(): number { + const result = External.value(); + return result; + } + + limited(value: string): string { + return value + value; + } + + observed(): number { + this.callee(); + const result = 7; + return result; + } + + callee(): void { + return; + } +} diff --git a/usvm-ts/src/test/resources/models/SymbolicStringEngine.ts b/usvm-ts/src/test/resources/models/SymbolicStringEngine.ts new file mode 100644 index 0000000000..f9be8c6ff6 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SymbolicStringEngine.ts @@ -0,0 +1,17 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class SymbolicStringEngine { + inputRoundtrip(value: string): string { + return value; + } + + length(): number { + return "\ud800\udc00".length; + } + + anyAliasLength(): number { + const value: any = "\ud800"; + return value.length; + } +}