From 0f66e4f9a5dd29db11a4e1ca714f7a39a5b71203 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 1 Oct 2026 14:35:27 +0300 Subject: [PATCH] [TS] Share analysis hooks and UTF-16 infrastructure between PBT and Calls --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- .../org/usvm/ts/calls/CallsExperiment.kt | 6 +- .../org/usvm/ts/calls/CallsExperimentCli.kt | 6 +- .../org/usvm/ts/calls/CallsSourceReplay.kt | 4 +- .../org/usvm/ts/calls/CallsSymbolicInputs.kt | 33 +-- .../usvm/ts/calls/CallsSourceReplayTest.kt | 20 ++ .../calls/SourceTargetReplayFixture.ts | 7 + .../src/main/resources/logback.xml | 5 +- .../org/usvm/ts/pbt/cli/FastCheckCli.kt | 6 +- .../pbt/fastcheck/FastCheckProcessClient.kt | 4 +- .../fastcheck/FastCheckProjectionClient.kt | 4 +- .../usvm/ts/pbt/manifest/PropertyManifest.kt | 4 +- .../kotlin/org/usvm/ts/pbt/model/Utf16Json.kt | 28 +++ .../org/usvm/ts/pbt/model/Utf16JsonTest.kt | 80 +++++++ .../org/usvm/machine/TsInterpreterObserver.kt | 19 ++ .../main/kotlin/org/usvm/machine/TsMachine.kt | 113 ++++++++-- .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 2 +- .../usvm/machine/interpreter/TsInterpreter.kt | 13 +- .../kotlin/org/usvm/util/StringStorage.kt | 43 ++++ .../org/usvm/machine/StringEngineTest.kt | 111 ++++++++++ .../org/usvm/machine/TsSharedAnalysisTest.kt | 201 ++++++++++++++++++ .../test/resources/models/SharedAnalysis.ts | 35 +++ .../resources/models/SymbolicStringEngine.ts | 33 +++ 23 files changed, 714 insertions(+), 65 deletions(-) create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/Utf16Json.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/Utf16JsonTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt create mode 100644 usvm-ts/src/test/resources/models/SharedAnalysis.ts create mode 100644 usvm-ts/src/test/resources/models/SymbolicStringEngine.ts diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 700801642a..1feaaf5479 100644 --- 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 index 9f01065411..6bc1c30b6f 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 @@ -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(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 d249b79596..acfad26830 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 @@ -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 index 56137b47c5..dae470c898 100644 --- 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 = makeSymbolicPrimitive(sizeSort) val codeUnits: List> = 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 index 5f485bd835..6ed05bab21 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 @@ -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 index 3cddbf802e..fe695f2760 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 48e52ecbb2..096a645227 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,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(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 2c9777109d..145a66d4c2 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 only after an assignment writes 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 is executed, while its arguments still 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 414ce7f5fc..11689031d2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -12,7 +12,10 @@ import org.usvm.USort import org.usvm.api.targets.TsTarget import org.usvm.machine.call.TsBuiltInUnknownCallModels import org.usvm.machine.call.TsModelUnknownCallDispatcher +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallDecision import org.usvm.machine.call.TsUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallModelCatalog import org.usvm.machine.call.deduplicateEtsFilesBySignature import org.usvm.machine.interpreter.TsInterpreter @@ -52,6 +55,17 @@ data class TsAnalysisResult( val stopReason: TsAnalysisStopReason, ) +/** Analysis-wide observations; collected states alone do not prove that every path completed. */ +data class TsMachineAnalysisResult( + val states: List, + val stopReason: TsAnalysisStopReason, + val timedOut: Boolean, + /** A STOP_PATH residual decision observed from the machine-owned model dispatcher. */ + val unsupportedCall: Boolean, + val engineFailed: Boolean, + val runtimeLimited: Boolean, +) + class TsMachine( scene: EtsScene, override val options: UMachineOptions, @@ -90,16 +104,17 @@ class TsMachine( applicationAndSdkClasses = scene.projectAndSdkClasses, dateNowMilliseconds = tsOptions.dateNowMilliseconds, ) + private val analysisObserver = AnalysisTrackingObserver(observer ?: object : TsInterpreterObserver {}) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), fallback = tsOptions.unknownCallFallback, - observer = observer, + observer = analysisObserver, ) private val interpreter = TsInterpreter( ctx = ctx, graph = graph, options = tsOptions, - observer = observer, + observer = analysisObserver, unknownCallDispatcher = resolvedUnknownCallDispatcher, throwExceptionOnStepFailure = options.throwExceptionOnStepFailure, ) @@ -110,19 +125,34 @@ class TsMachine( targets: List = emptyList(), ): List = analyzeWithOutcome(methods = methods, targets = targets).states + fun analyze( + methods: List, + targets: List = emptyList(), + configureInitialState: (EtsMethod, TsState) -> Unit, + ): List = analyzeWithMetadata(methods, targets, configureInitialState).states + fun analyzeWithOutcome( methods: List, targets: List = emptyList(), ): TsAnalysisResult { - val initialStates = mutableMapOf() - methods.forEach { method -> - initialStates[method] = interpreter.getInitialState( - method = method, - targets = targets, - configure = initialStateConfigurator, - parameterSortOverride = { stackSlot -> initialParameterSortOverride(ctx, stackSlot) }, - ) - } + val result = analyzeWithMetadata(methods = methods, targets = targets) + return TsAnalysisResult(states = result.states, stopReason = result.stopReason) + } + + /** + * The constructor configurator runs before [configureInitialState], both before the initial solver query. + * A caller-supplied dispatcher owns its telemetry; [TsMachineAnalysisResult.unsupportedCall] only tracks + * residual decisions made by this machine's default dispatcher. Runtime limitations are tracked separately. + */ + fun analyzeWithMetadata( + methods: List, + targets: List = emptyList(), + configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, + ): TsMachineAnalysisResult { + interpreter.resetStepFailure() + analysisObserver.reset() + + val initialStates = createInitialStates(methods, targets, configureInitialState) val methodsToTrackCoverage = when (options.coverageZone) { @@ -175,6 +205,7 @@ class TsMachine( } val stepsStatistics = StepsStatistics() + var timedOut = false val stopStrategy = object : StopStrategy { val strategy = createStopStrategy( options, @@ -186,7 +217,15 @@ class TsMachine( ) override fun shouldStop(): Boolean { + if (options.timeout <= kotlin.time.Duration.ZERO) { + timedOut = true + return true + } + val result = strategy.shouldStop() + if (result && timeStatistics.runningTime >= options.timeout) { + timedOut = true + } if (result) { logger.warn { "Stop strategy finished execution: ${strategy.stopReason()}" } @@ -227,10 +266,60 @@ class TsMachine( TsAnalysisStopReason.STOPPED } - return TsAnalysisResult(states = statesCollector.collectedStates, stopReason = stopReason) + return TsMachineAnalysisResult( + states = statesCollector.collectedStates, + stopReason = stopReason, + timedOut = timedOut, + unsupportedCall = analysisObserver.pathStopped, + engineFailed = interpreter.stepFailed, + runtimeLimited = analysisObserver.runtimeLimited, + ) + } + + private fun createInitialStates( + methods: List, + targets: List, + configureInitialState: (EtsMethod, TsState) -> Unit, + ): Map = methods.associateWith { method -> + interpreter.getInitialState( + method = method, + targets = targets, + configure = { state -> + initialStateConfigurator(state) + configureInitialState(method, state) + }, + parameterSortOverride = { stackSlot -> initialParameterSortOverride(ctx, stackSlot) }, + ) } override fun close() { components.close() } } + +private class AnalysisTrackingObserver( + private val delegate: TsInterpreterObserver, +) : TsInterpreterObserver by delegate { + var pathStopped: Boolean = false + private set + var runtimeLimited: Boolean = false + private set + + override fun onUnknownCall(event: TsUnknownCallEvent) { + val decision = event.decision + if (decision is TsUnknownCallDecision.ResidualFallback && decision.policy == TsResidualCallPolicy.STOP_PATH) { + pathStopped = true + } + delegate.onUnknownCall(event) + } + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + runtimeLimited = true + delegate.onRuntimeFeatureLimitation(event) + } + + fun reset() { + pathStopped = false + runtimeLimited = false + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 6cbe13d1d0..caee4f5036 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -46,7 +46,7 @@ internal fun TsContext.fieldReceiverLimitation( val types = scope.calcOnState { memory.typeStreamOf(receiver).take(2) } return TsRuntimeFeatureLimitationReason.FAKE_FIELD_RECEIVER_TYPE.takeIf { - types is TypesResult.SuccessfulTypesResult && types.types.any { it is EtsFakeType } + types is TypesResult.SuccessfulTypesResult && types.types.any { type -> type is EtsFakeType } } } 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 630dad0cd7..bb62cd3840 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 @@ -103,6 +103,12 @@ class TsInterpreter( ) : UInterpreter() { private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() + internal var stepFailed: Boolean = false + private set + + internal fun resetStepFailure() { + stepFailed = false + } override fun step(state: TsState): StepResult { val stmt = state.lastStmt @@ -152,6 +158,7 @@ class TsInterpreter( } } } catch (e: Exception) { + stepFailed = true if (throwExceptionOnStepFailure) { throw e } @@ -613,6 +620,8 @@ class TsInterpreter( assignTo(scope, stmt.lhv, expr) ?: return } + observer?.onAssignmentCompleted(exprResolver.simpleValueResolver, stmt, scope) + val nextStmt = stmt.nextStmt ?: return scope.doWithState { newStmt(nextStmt) } } @@ -625,8 +634,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/StringStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt index 7492f999dd..8847e81c30 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt @@ -1,10 +1,13 @@ package org.usvm.util +import io.ksmt.expr.KBitVec16Value +import io.ksmt.sort.KBv16Sort import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr @@ -13,10 +16,50 @@ import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.api.memcpy import org.usvm.machine.TsSizeSort +import org.usvm.machine.expr.extractInt import org.usvm.machine.state.TsState +import org.usvm.model.UModelBase import org.usvm.sizeSort internal val STRING_CHARACTER_ARRAY_TYPE = EtsArrayType(EtsNumberType, dimensions = 1) +private const val UTF16_CODE_UNIT_MASK = 0xffff + +/** Builds a bounded string in the engine's UTF-16 layout, constraining its length to the supplied capacity. */ +fun TsState.mkStringFromCodeUnits( + length: UExpr, + codeUnits: List>, +): UConcreteHeapRef = with(ctx) { + pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(codeUnits.size)) + val (string, characters) = allocateString(length = length, maxLength = codeUnits.size) + codeUnits.forEachIndexed { index, unit -> + val position = mkBv(index) + memory.write( + mkArrayIndexLValue(bv16Sort, characters, position, STRING_CHARACTER_ARRAY_TYPE), + unit, + guard = mkBvSignedLessExpr(position, length), + ) + } + + string +} + +/** Reads a bounded string from current memory under [model]; returns null for untracked, nonconstant refs. */ +fun TsState.resolveStringFromModel(model: UModelBase, ref: UConcreteHeapRef): String? = with(ctx) { + val maxLength = stringMaxLengths[ref] ?: return@with getStringConstantValue(ref) + val characters = stringCharacters(ref) + val length = model.eval(stringLength(ref)).extractInt() + require(length in 0..maxLength) { "Resolved string length $length exceeds its stored bounds" } + + buildString(length) { + repeat(length) { index -> + val slot = mkArrayIndexLValue(bv16Sort, characters, mkBv(index), STRING_CHARACTER_ARRAY_TYPE) + val unit = memory.read(slot) + val resolved = model.eval(unit) as KBitVec16Value + append((resolved.shortValue.toInt() and UTF16_CODE_UNIT_MASK).toChar()) + } + } +} internal fun TsState.stringCharacters(receiver: UHeapRef): UHeapRef = with(ctx) { memory.read(mkFieldLValue(addressSort, receiver, "value")).asExpr(addressSort) 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..ae88adf7ac --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt @@ -0,0 +1,111 @@ +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.PathSelectionStrategy +import org.usvm.SolverType +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.TsTestResolver +import org.usvm.util.getResourcePath +import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.mkStringFromCodeUnits +import org.usvm.util.resolveStringFromModel +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.time.Duration + +class StringEngineTest { + private val file = loadEtsFileAutoConvert( + getResourcePath("/models/SymbolicStringEngine.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(file)) + + @Test + fun `length uses UTF-16 units through a widened alias`() { + val direct = execute("length") + val alias = execute("anyAliasLength") + + assertEquals(2.0, assertIs(direct).number) + assertEquals(1.0, assertIs(alias).number) + } + + @Test + fun `character operations preserve isolated surrogate units`() { + val code = execute("charCodeAt") + val charEquals = execute("charAtEquals") + val indexEquals = execute("indexedReadEquals") + val outOfRange = execute("outOfRangeCharAt") + + assertEquals(0xd800.toDouble(), assertIs(code).number) + assertEquals(true, assertIs(charEquals).value) + assertEquals(true, assertIs(indexEquals).value) + assertEquals("", assertIs(outOfRange).value) + } + + @Test + fun `shared allocation and decoding preserve a solver selected surrogate`() { + val method = scene.projectClasses.single { it.name == "SymbolicStringEngine" } + .methods + .single { it.name == "inputRoundtrip" } + 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.resolveStringFromModel(model = state.models.single(), ref = input)) + val decoded = TsTestResolver().resolve(method, state).returnValue + assertEquals("\ud800", assertIs(decoded).value) + } + } + + private fun execute(name: String): TsTestValue { + val method = scene.projectClasses.single { it.name == "SymbolicStringEngine" } + .methods + .single { it.name == name } + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + return TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + val state = machine.analyze(listOf(method)).single() + TsTestResolver().resolve(method, state).returnValue + } + } +} 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..a302c530cd --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt @@ -0,0 +1,201 @@ +package org.usvm.machine + +import io.ksmt.utils.asExpr +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.machine.state.TsMethodResult +import org.usvm.util.getResourcePath +import org.usvm.util.mkRegisterStackLValue +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())) + + @Test + fun `both initial configurators run in order before the first model and preserve sort overrides`() { + val callbacks = mutableListOf() + val method = method("identity") + val machine = TsMachine( + scene = scene, + options = options, + tsOptions = tsOptions, + initialParameterSortOverride = { ctx, slot -> ctx.fp64Sort.takeIf { slot == 1 } }, + initialStateConfigurator = { callbacks += "constructor" }, + ) + + machine.use { + val result = it.analyzeWithMetadata( + methods = listOf(method), + configureInitialState = { configuredMethod, state -> + assertEquals(method, configuredMethod) + callbacks += "analysis" + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + state.pathConstraints += mkFpEqualExpr(input, mkFp(7.0, fp64Sort)) + } + }, + ) + + assertEquals(listOf("constructor", "analysis"), callbacks) + assertFalse(result.engineFailed) + val state = result.states.single() + val value = (state.methodResult as TsMethodResult.Success).value + assertEquals(state.ctx.mkFp(7.0, state.ctx.fp64Sort), state.models.single().eval(value)) + } + } + + @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" } + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { events += "runtime" } + } + + 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) + assertEquals(listOf("call", "runtime"), 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..8a4bc9fa34 --- /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(): boolean { + return /x/.test("x"); + } + + 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..7533fa9cfa --- /dev/null +++ b/usvm-ts/src/test/resources/models/SymbolicStringEngine.ts @@ -0,0 +1,33 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class SymbolicStringEngine { + inputRoundtrip(value: string): string { + return value; + } + + length(): number { + return "\ud800\udc00".length; + } + + charCodeAt(): number { + return "\ud800".charCodeAt(0); + } + + charAtEquals(): boolean { + return "\ud800".charAt(0) === "\ud800"; + } + + indexedReadEquals(): boolean { + return "\udc00"[0] === "\udc00"; + } + + outOfRangeCharAt(): string { + return "x".charAt(1); + } + + anyAliasLength(): number { + const value: any = "\ud800"; + return value.length; + } +}