diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassOracle.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassOracle.kt index 8e6d75d58e..01b3527cad 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassOracle.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassOracle.kt @@ -22,6 +22,7 @@ import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunStatus import org.usvm.ts.pbt.fastcheck.FastCheckBackend import org.usvm.ts.pbt.fastcheck.FastCheckRuntime +import org.usvm.ts.pbt.fastcheck.TypeScriptLocalSourceClosure import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.ConstantDomain @@ -269,6 +270,9 @@ internal class OriginalTypeScriptClassReplayer( sourceOverride: String? = null, overrideSourceFile: String? = null, private val counterGlobalName: String? = null, + // Saved environments may replay naturally evaluated initializers outside the lifecycle oracle's checked subset. + // The supplied graph still passes the normal copy/hash checks and cannot contain unresolved module boundaries. + sourceClosure: TypeScriptLocalSourceClosure? = null, ) : AutoCloseable { private val root = sourceRoot.toRealPath() private val workspace = Files.createTempDirectory("usvm-calls-class-replay-") @@ -282,7 +286,15 @@ internal class OriginalTypeScriptClassReplayer( require( (sourceOverride == null) == (overrideSourceFile == null) ) { "Source override needs a relative target file" } - val closure = checkedCallsSourceClosure(root = root, entry = root.resolve(function.sourceFile)) + val closure = sourceClosure ?: checkedCallsSourceClosure( + root = root, + entry = root.resolve(function.sourceFile), + ) + val closureResolved = closure.reasonCode == null && function.sourceFile in closure.files && + closure.resolution?.runtimeBoundaries.orEmpty().isEmpty() + require(closureResolved) { + "Native replay requires a resolved closure containing its harness" + } copyCallsSourceClosure(root = root, destination = overlay, closure = closure) if (overrideSourceFile != null) { require(overrideSourceFile in closure.files) { "Replay override is outside the frozen runtime closure" } @@ -452,7 +464,7 @@ ${classReplayThrownValueDiagnosticSource().prependIndent(indent = " ")} """.trimIndent() + "\n" } -private fun classReplayValueEncoderSource(): String = """ +internal fun classReplayValueEncoderSource(): String = """ function encode(value: unknown, seen = new Set()): unknown { if (value === undefined) return { kind: 'undefined' }; if (value === null) return { kind: 'null' }; diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsConcreteHeapReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsConcreteHeapReplay.kt index 15a51fe3ba..86d157ad0e 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsConcreteHeapReplay.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsConcreteHeapReplay.kt @@ -1,5 +1,28 @@ package org.usvm.ts.calls +/** Input slots have already passed the Kotlin primitive-only journal schema. */ +internal fun callsConcretePrimitiveDecoderSource(): String = """ + function decodeCallsConcretePrimitive(value: any): any { + switch (value.kind) { + case 'undefined': return undefined; + case 'null': return null; + case 'boolean': case 'string': return value.value; + case 'number': + switch (value.value) { + case 'nan': return NaN; + case 'positive-infinity': return Infinity; + case 'negative-infinity': return -Infinity; + case 'finite': { + const view = new DataView(new ArrayBuffer(8)); + view.setBigUint64(0, BigInt('0x' + value.bits), false); + return view.getFloat64(0, false); + } + } + } + throw Error('Invalid saved input primitive'); + } +""".trimIndent() + /** Used inside the existing native replay wrapper with its lossless primitive decoder and exact prototype registry. */ internal fun callsConcreteHeapRestoreSource(): String = """ function restoreCallsConcreteHeap(graph: any, prototypes: Map, decodePrimitive: (x: any) => any, 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 004c03d6d6..54669121ee 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 @@ -12,6 +12,7 @@ fun main(args: Array) { "class-catalog" -> runClassCatalog(args.drop(1)) "class-start-smoke" -> runClassStartSmoke(args.drop(1)) "class-symbolic-probe" -> runClassSymbolicProbe(args.drop(1)) + "class-replay-input" -> runSavedInputReplay(args.drop(1)) "class-prepare" -> runClassPrepare(args.drop(1)) "class-preflight" -> runClassPreflight(args.drop(1)) "class-cell" -> runClassCell(args.drop(1)) @@ -108,6 +109,7 @@ private fun usage(): String = """ calls class-catalog calls class-start-smoke calls class-symbolic-probe + calls class-replay-input calls class-prepare calls class-preflight calls class-cell diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSavedInputReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSavedInputReplay.kt new file mode 100644 index 0000000000..63e345915d --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSavedInputReplay.kt @@ -0,0 +1,351 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.Serializable +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.usvm.ts.pbt.fastcheck.TypeScriptLocalSourceClosure +import org.usvm.ts.pbt.fastcheck.TypeScriptSavedInputBindings +import org.usvm.ts.pbt.fastcheck.TypeScriptSavedInputClass +import org.usvm.ts.pbt.fastcheck.TypeScriptSourceInspector +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import java.io.OutputStream +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.StandardOpenOption +import java.security.DigestInputStream +import java.security.MessageDigest +import java.util.UUID + +@Serializable +internal enum class CallsSavedInputReplayStatus { INVOKED, UNSUPPORTED, HARNESS_FAILURE } + +/** Invocation evidence only: neither the suspended source location nor native class coverage is attested. */ +@Serializable +internal data class CallsSavedInputReplayResult( + val stateId: String, + val status: CallsSavedInputReplayStatus, + val diagnostic: String? = null, + val observation: CallsClassReplayObservation? = null, + val sourceInitializationDiagnostics: List = emptyList(), + val nativeReplayValidated: Boolean = false, + val nativeCoverageAvailable: Boolean = false, +) + +/** Select one immutable journal record and verify both frozen inputs and its producing probe manifest. */ +internal fun runSavedInputReplay(args: List) { + require(args.size == SAVED_INPUT_REPLAY_ARGUMENT_COUNT) { + "class-replay-input needs " + } + val arguments = args.iterator() + val manifestArgument = arguments.next() + val classId = arguments.next() + val probeArgument = arguments.next() + val stateId = arguments.next() + val timeoutMillis = arguments.next().toLong() + val outputArgument = arguments.next() + val manifestPath = Path.of(manifestArgument).toRealPath() + val manifestBytes = Files.readAllBytes(manifestPath) + val manifest = CallsExperimentJson.json.decodeFromString( + manifestBytes.toString(Charsets.UTF_8) + ) + val case = manifest.classes.single { it.classId == classId } + val root = case.verifyInputs() + val probe = Path.of(probeArgument).toRealPath() + val result = CallsExperimentJson.json.decodeFromString( + Files.readString(probe.resolve("result.json")) + ) + require(result.classId == case.classId && result.manifestSha256 == callsArtifactSha256(manifestBytes)) { + "Saved input probe differs from the supplied class manifest" + } + val metadata = checkNotNull(result.rawAnalysis?.inputCandidates) { "Probe has no concrete input journal" } + require(metadata.complete && metadata.schemaVersion == 1 && metadata.format == "JSONL") { + "Saved input replay needs a complete supported concrete journal" + } + val journal = probe.resolve(metadata.path).normalize().toRealPath() + require(journal.startsWith(probe)) { "Input journal escapes the probe directory" } + require(Files.size(journal) == metadata.bytes && savedInputFileSha256(journal) == metadata.sha256) { + "Saved concrete input journal changed" + } + val candidate = Files.lines(journal).use { lines -> + lines.iterator().asSequence() + .map { CallsExperimentJson.json.decodeFromString(it) } + .single { it.stateId == stateId } + } + require(candidate.className == case.className && candidate.profile == manifest.profile) { + "Saved candidate differs from the manifest class or profile" + } + val replay = replayCallsSavedInput( + sourceRoot = root, + sourceFile = case.sourceFile, + targetSignature = checkNotNull(result.targetSignature), + candidate = candidate, + timeoutMillis = timeoutMillis, + ) + case.verifyInputs() + + val output = Path.of(outputArgument).toAbsolutePath().normalize() + output.parent?.let(Files::createDirectories) + Files.writeString(output, encodeCallsArtifact(replay) + "\n", StandardOpenOption.CREATE_NEW) +} + +/** Reuses the normal frozen-closure copier, supervised native process and class observation transport. */ +internal fun replayCallsSavedInput( + sourceRoot: Path, + sourceFile: String, + targetSignature: String, + candidate: CallsClassInputCandidate, + timeoutMillis: Long, +): CallsSavedInputReplayResult { + require(timeoutMillis > 0) + if (!candidate.environmentComplete) { + return unsupportedSavedInput( + candidate = candidate, + reason = "Incomplete initial environment: ${candidate.environmentLimitations}", + ) + } + if (candidate.methodName.startsWith('%')) { + return unsupportedSavedInput( + candidate = candidate, + reason = "Synthetic initializer or lowered entry point is not a native callable", + ) + } + + val root = sourceRoot.toRealPath() + val closure = savedInputSourceClosure(root = root, sourceFile = sourceFile) + if (closure.reasonCode != null) { + return unsupportedSavedInput(candidate = candidate, reason = "${closure.reasonCode}: ${closure.diagnostic}") + } + val hasUnresolvedRuntimeBoundary = closure.resolution?.runtimeBoundaries.orEmpty().isNotEmpty() + if (hasUnresolvedRuntimeBoundary) { + return unsupportedSavedInput( + candidate = candidate, + reason = "Runtime source closure has unresolved module boundaries" + ) + } + val plan = try { + savedInputBindingPlan( + sourceFile = sourceFile, + targetSignature = targetSignature, + candidate = candidate, + closureFiles = closure.files.toSet(), + ) + } catch (unsupported: UnsupportedSavedInputBinding) { + return unsupportedSavedInput(candidate = candidate, reason = checkNotNull(unsupported.message)) + } + + val workspace = Files.createTempDirectory("usvm-calls-saved-input-") + try { + copyCallsSourceClosure(root = root, destination = workspace, closure = closure) + writeCallsFrozenTsconfig(root = workspace, resolution = closure.resolution) + for ((file, bindings) in plan.modules) { + val prepared = TypeScriptSourceInspector.savedInputBindings( + source = root.resolve(file), + bindings = bindings + ) + val preparedSource = prepared.source + if (preparedSource == null) { + return unsupportedSavedInput(candidate = candidate, reason = checkNotNull(prepared.reason)) + } + + Files.writeString(workspace.resolve(file), preparedSource) + } + val harnessName = ".usvm-saved-input-${UUID.randomUUID()}.mts" + Files.writeString(workspace.resolve(harnessName), savedInputHarness(candidate = candidate, plan = plan)) + val function = CallsFunctionCase( + functionId = "calls.saved-input.${candidate.stateId}", + sourceFile = harnessName, + entryPoint = TypeScriptEntryPoint(module = harnessName, exportName = "invokeSavedInput"), + inputs = emptyList(), + targets = emptyList(), + ) + val fields = mapOf( + "completion" to StringDomain(), + "returnValue" to StringDomain(maxLength = Int.MAX_VALUE), + "returnValueRepresentable" to BooleanDomain, + "diagnostic" to StringDomain(maxLength = Int.MAX_VALUE), + ) + val preparedClosure = savedInputSourceClosure(root = workspace, sourceFile = harnessName) + val preparedClosureResolved = preparedClosure.reasonCode == null && + preparedClosure.resolution?.runtimeBoundaries.orEmpty().isEmpty() + require(preparedClosureResolved) { + "Generated saved input harness has an unresolved native runtime closure" + } + val observation = OriginalTypeScriptClassReplayer( + sourceRoot = workspace, + function = function, + observationFields = fields, + sourceClosure = preparedClosure, + ).use { replayer -> replayer.replay(inputs = emptyList(), timeoutMillis = timeoutMillis) } + val invoked = observation.observation.completion == CallsCoverageCompletion.RETURNED && + observation.observation.representable + + return CallsSavedInputReplayResult( + stateId = candidate.stateId, + status = if (invoked) CallsSavedInputReplayStatus.INVOKED else CallsSavedInputReplayStatus.HARNESS_FAILURE, + diagnostic = if (invoked) null else observation.observation.diagnostic, + observation = observation, + sourceInitializationDiagnostics = closure.initializationIssues.map { it.diagnostic }, + ) + } finally { + Files.walk(workspace).use { paths -> paths.sorted(Comparator.reverseOrder()).forEach(Files::deleteIfExists) } + } +} + +private fun savedInputSourceClosure(root: Path, sourceFile: String): TypeScriptLocalSourceClosure = + TypeScriptSourceInspector.startupSourceClosure(sourceRoot = root, source = root.resolve(sourceFile)) + +private fun savedInputFileSha256(path: Path): String { + val digest = MessageDigest.getInstance("SHA-256") + DigestInputStream(Files.newInputStream(path), digest).use { input -> + input.transferTo(OutputStream.nullOutputStream()) + } + return digest.digest().joinToString(separator = "") { "%02x".format(it) } +} + +private fun unsupportedSavedInput(candidate: CallsClassInputCandidate, reason: String): CallsSavedInputReplayResult = + CallsSavedInputReplayResult( + stateId = candidate.stateId, + status = CallsSavedInputReplayStatus.UNSUPPORTED, + diagnostic = reason, + ) + +private class UnsupportedSavedInputBinding(message: String) : IllegalArgumentException(message) + +private data class SavedInputBindingPlan( + val modules: Map, + val classes: Map>, + val targetSignature: String, +) + +private fun savedInputBindingPlan( + sourceFile: String, + targetSignature: String, + candidate: CallsClassInputCandidate, + closureFiles: Set, +): SavedInputBindingPlan { + val projectName = targetSignature.removePrefix("@").substringBefore('/') + val classes = linkedMapOf>() + val statics = linkedMapOf>() + val modules = linkedMapOf>() + + fun classBinding(signature: String, file: String, name: String) { + val expected = EtsClassSignature( + name = name, + file = EtsFileSignature(projectName = projectName, fileName = file) + ) + if (signature != expected.toString() || file !in closureFiles) { + throw UnsupportedSavedInputBinding("Exact top-level source prototype is unavailable: $signature ($file)") + } + val binding = file to name + val previous = classes.putIfAbsent(signature, binding) + require(previous == null || previous == binding) { "Conflicting concrete prototype metadata: $signature" } + } + + classBinding(signature = targetSignature, file = sourceFile, name = candidate.className) + for (node in candidate.inputs.objects) { + val signature = node.classSignature ?: continue + classBinding( + signature = signature, + file = checkNotNull(node.classSourceFile), + name = checkNotNull(node.className), + ) + } + for (field in candidate.inputs.environmentFields) { + when (field.kind) { + CallsConcreteEnvironmentFieldKind.STATIC_FIELD -> { + classBinding(signature = field.ownerSignature, file = field.sourceFile, name = field.ownerName) + statics.getOrPut(field.ownerSignature) { linkedSetOf() }.add(field.name) + } + CallsConcreteEnvironmentFieldKind.MODULE_BINDING -> { + val owner = EtsClassSignature( + name = DEFAULT_ARK_CLASS_NAME, + file = EtsFileSignature(projectName = projectName, fileName = field.sourceFile), + ) + if (field.ownerSignature != owner.toString() || field.ownerName != DEFAULT_ARK_CLASS_NAME || + field.sourceFile !in closureFiles + ) { + throw UnsupportedSavedInputBinding("Exact module binding is unavailable: ${field.ownerSignature}") + } + modules.getOrPut(field.sourceFile) { linkedSetOf() }.add(field.name) + } + } + } + val files = classes.values.map { it.first }.toSet() + modules.keys + val bindings = files.associateWith { file -> + TypeScriptSavedInputBindings( + exportName = "__usvmSavedInput${UUID.randomUUID().toString().replace("-", "")}", + classes = classes.filterValues { it.first == file }.map { (signature, binding) -> + TypeScriptSavedInputClass(name = binding.second, staticFields = statics[signature].orEmpty().toList()) + }, + moduleBindings = modules[file].orEmpty().toList(), + ) + } + return SavedInputBindingPlan(modules = bindings, classes = classes, targetSignature = targetSignature) +} + +private fun savedInputHarness(candidate: CallsClassInputCandidate, plan: SavedInputBindingPlan): String { + val json = CallsExperimentJson.json + val aliases = plan.modules.keys.withIndex().associate { (index, file) -> file to "module$index" } + val imports = plan.modules.map { (file, bindings) -> + "import { ${bindings.exportName} as ${aliases.getValue(file)} } from ${json.encodeToUtf8SafeString("./$file")};" + } + val classes = plan.classes.map { (signature, binding) -> + val (file, name) = binding + val signatureKey = json.encodeToUtf8SafeString(signature) + val classKey = json.encodeToUtf8SafeString(name) + "[$signatureKey, ${aliases.getValue(file)}.classes[$classKey]]" + } + val environmentSetters = candidate.inputs.environmentFields.map { field -> + val module = aliases.getValue(field.sourceFile) + val key = json.encodeToUtf8SafeString(field.ownerSignature) + "if (field.ownerSignature === $key) { $module.writeBinding(field.ownerName, field.name, value); return; }" + }.distinct() + val owner = "classes.get(${json.encodeToUtf8SafeString(plan.targetSignature)})" + val method = json.encodeToUtf8SafeString(candidate.methodName) + val instanceInvocation = candidate.invocationKind == CallsClassInvocationKind.INSTANCE_METHOD + val constructorInvocation = candidate.invocationKind == CallsClassInvocationKind.CONSTRUCTOR + val receiver = if (instanceInvocation) "restored.receiver" else owner + val callable = if (constructorInvocation) "receiver" else "receiver[$method]" + val invocation = when (candidate.invocationKind) { + CallsClassInvocationKind.CONSTRUCTOR -> "Reflect.construct(callable, restored.arguments)" + CallsClassInvocationKind.STATIC_METHOD, CallsClassInvocationKind.INSTANCE_METHOD -> + "Reflect.apply(callable, receiver, restored.arguments)" + } + return """ + ${imports.joinToString("\n")} + ${callsConcretePrimitiveDecoderSource()} + ${callsConcreteHeapRestoreSource()} + ${classReplayValueEncoderSource()} + export function invokeSavedInput(): any { + const candidate = JSON.parse(${json.encodeToUtf8SafeString(encodeCallsArtifact(candidate))}); + const classes = new Map([${classes.joinToString()}]); + const prototypes = new Map(Array.from(classes, ([signature, owner]) => [signature, owner.prototype] as const)); + const restored = restoreCallsConcreteHeap(candidate.inputs, prototypes, decodeCallsConcretePrimitive, + (field, value) => { + ${environmentSetters.joinToString("\n")} + throw Error('Unknown exact saved input environment owner: ' + field.ownerSignature); + }); + const receiver = $receiver; + const callable = $callable; + if (typeof callable !== 'function') throw Error('Saved input native callable is unavailable'); + let returned: any; + try { returned = $invocation; } catch (error) { + const diagnostic = error instanceof Error ? error.name + ': ' + error.message : 'Thrown ' + typeof error; + return { completion: 'THREW', returnValue: '', returnValueRepresentable: false, diagnostic }; + } + try { + return { completion: 'RETURNED', returnValue: JSON.stringify(encode(returned)), + returnValueRepresentable: true, diagnostic: '' }; + } catch (error) { + const diagnostic = error instanceof Error ? error.message : 'Unrepresentable return value'; + return { completion: 'RETURNED', returnValue: '', returnValueRepresentable: false, diagnostic }; + } + } + """.trimIndent() +} + +private const val SAVED_INPUT_REPLAY_ARGUMENT_COUNT = 6 diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt index f575a1071f..f4b5a58a94 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt @@ -4,6 +4,7 @@ import org.junit.jupiter.api.io.TempDir import org.usvm.SolverType import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.NumberDomain @@ -219,28 +220,41 @@ class CallsClassDataRegistryOracleTest { constructorInputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)), ) - val result = CurrentTsCallsClassCoverageEngine().search( - CallsClassSearchRequest( - harness = harness, - profile = CallsExperimentProfile.EMPTY_STOP, - frozenModelIds = emptySet(), - expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision, - seed = 1, - budget = 3.seconds, - timeQuantum = 100.milliseconds, - solverQueryLimit = 1.seconds, - solverType = SolverType.YICES, - candidateCap = 20, - requireEntryPointWitness = true, - ), - ) + // Coverage-directed search need not enumerate every input model for each entry point. + val branchInputs = listOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)) + val candidates = branchInputs.flatMap { flag -> + val inputs = listOf(PropertyInput(name = "flag", domain = ConstantDomain(flag))) + val branchHarness = harness.copy( + surface = harness.surface.copy(constructorInputs = inputs), + functions = harness.functions.map { it.copy(inputs = inputs) }, + ) + val result = CurrentTsCallsClassCoverageEngine().search( + CallsClassSearchRequest( + harness = branchHarness, + profile = CallsExperimentProfile.EMPTY_STOP, + frozenModelIds = emptySet(), + expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision, + seed = 1, + budget = 3.seconds, + timeQuantum = 100.milliseconds, + solverQueryLimit = 1.seconds, + solverType = SolverType.YICES, + candidateCap = 20, + requireEntryPointWitness = true, + ), + ) + + val scenarioIds = result.search.candidates.map { it.entryPointId }.toSet() + assertEquals(harness.scenarios.map { it.id }.toSet(), scenarioIds, "flag=$flag") + result.search.candidates.forEach { assertEquals(listOf(flag), it.inputs) } + result.search.candidates + } val constructorScenarioId = harness.scenarios.first().id - val constructorBranches = result.search.candidates.filter { it.entryPointId == constructorScenarioId } + val constructorBranches = candidates.filter { it.entryPointId == constructorScenarioId } .map { it.inputs.single() }.toSet() assertEquals(setOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)), constructorBranches) - assertEquals(harness.scenarios.map { it.id }.toSet(), result.search.candidates.map { it.entryPointId }.toSet()) - for (candidate in result.search.candidates) { + for (candidate in candidates) { val index = harness.scenarios.indexOfFirst { it.id == candidate.entryPointId } val original = OriginalTypeScriptClassReplayer( directory, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt index bd7f29564c..4c44ce0025 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -10,16 +10,7 @@ import org.jacodb.ets.model.EtsSourceSpan import org.jacodb.ets.model.EtsStmtLocation import org.jacodb.ets.model.EtsUndefinedType import org.junit.jupiter.api.io.TempDir -import org.usvm.ts.pbt.backend.PropertyRunConfiguration -import org.usvm.ts.pbt.backend.PropertyRunStatus -import org.usvm.ts.pbt.fastcheck.FastCheckBackend -import org.usvm.ts.pbt.fastcheck.FastCheckRuntime -import org.usvm.ts.pbt.model.BooleanDomain 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.PropertyInput -import org.usvm.ts.pbt.model.TypeScriptEntryPoint import java.nio.file.Files import java.nio.file.Path import kotlin.test.Test @@ -211,7 +202,10 @@ class CallsClassStartSmokeTest { numeric(value: T): number { return value > 0 ? 1 : 0; } logical(value: T): number { return value ? 1 : 0; } reference(value: T): number { return value.length; } - defaulted(value: T): boolean { return typeof value === 'number'; } + defaulted(value: T): boolean { + if (typeof value === 'number') return true; + return false; + } } """.trimIndent() @@ -230,29 +224,31 @@ class CallsClassStartSmokeTest { assertTrue(values("logical").all { it is JsConcreteValue.Boolean }) assertTrue(values("reference").all { it is JsConcreteValue.String }) val failures = Files.readAllLines(directory.resolve("output/input-extraction-failures.jsonl")) - assertTrue(values("defaulted").isNotEmpty()) + // Distinct return paths force both kinds; one unconstrained return permits an arbitrary solver witness. + assertTrue(values("defaulted").any { it is JsConcreteValue.Number }) assertTrue(values("defaulted").any { it !is JsConcreteValue.Number }) assertTrue(failures.isEmpty(), failures.toString()) } @Test - fun `saved stopped candidate restores original receiver and arguments in native execution`() { + fun `saved stopped candidate replays original receiver aliases and static environment`() { val source = """ - declare class External { static stop(): number; } export class Box { value: number = 0; } export class Target { static marker: number = 17; value: number = 0; - run(box: Box, items: number[]): number { - if (this.value !== 11 || box.value !== 12 || items.length !== 1 || items[0] !== 13 || + run(box: Box, alias: Box, items: number[]): number { + if (this.value !== 11 || box.value !== 12 || box !== alias || items.length !== 1 || items[0] !== 13 || Target.marker !== 17) return 0; this.value = 91; box.value = 92; items[0] = 93; Target.marker = 97; - return this.nested(items, box); + return this.nested(items, alias); + } + nested(items: number[], box: Box): number { + return Math.abs(this.value + box.value + items[0] + Target.marker); } - nested(items: number[], box: Box): number { return External.stop(); } } """.trimIndent() @@ -262,7 +258,6 @@ class CallsClassStartSmokeTest { CallsExperimentJson.json.decodeFromString(it) } val candidate = candidates.single { it.methodName == "run" && it.outcome.startsWith("STOPPED_PREFIX") } - Files.writeString(directory.resolve("candidate.json"), encodeCallsArtifact(candidate)) assertEquals(CallsCoverageCandidateOrigin.SUSPENDED, candidate.origin) assertEquals(null, candidate.completion) @@ -271,7 +266,122 @@ class CallsClassStartSmokeTest { assertFalse(candidate.nativeReplayValidated) val marker = candidate.inputs.environmentFields.single { it.name == "marker" } assertEquals(JsConcreteValue.number(17.0), marker.value.primitive) - replaySavedStoppedCandidate() + assertEquals(candidate.inputs.arguments[0], candidate.inputs.arguments[1]) + + val replayPath = directory.resolve("native-input-replay.json") + runSavedInputReplay( + listOf( + directory.resolve("manifest.json").toString(), + "target", + directory.resolve("output").toString(), + candidate.stateId, + "20000", + replayPath.toString(), + ) + ) + val replay = CallsExperimentJson.json.decodeFromString( + Files.readString(replayPath) + ) + + assertSavedInputReturn(replay = replay, expected = 373.0) + + val adjusted = candidate.copy( + inputs = candidate.inputs.copy( + environmentFields = listOf( + marker.copy(value = CallsConcreteHeapValue(primitive = JsConcreteValue.number(19.0))) + ), + ) + ) + assertSavedInputReturned(result = result, candidate = adjusted, expected = 0.0) + } + + @Test + fun `saved stopped candidate restores mutable module binding before native invocation`() { + val source = """ + export let marker: number = 17; + export class Target { + run(value: number): number { + if (value !== 11) return 0; + marker = marker + 80; + return Math.abs(marker + value); + } + } + """.trimIndent() + + val result = runFixture(sourceText = source, exploratory = true, profile = CallsExperimentProfile.EMPTY_STOP) + val candidates = Files.readAllLines(directory.resolve("output/input-candidates.jsonl")).map { + CallsExperimentJson.json.decodeFromString(it) + } + val candidate = candidates.single { it.methodName == "run" && it.outcome.startsWith("STOPPED_PREFIX") } + val marker = candidate.inputs.environmentFields.single { it.name == "marker" } + + assertTrue(candidate.environmentComplete, candidate.environmentLimitations.toString()) + assertEquals(CallsConcreteEnvironmentFieldKind.MODULE_BINDING, marker.kind) + assertEquals(JsConcreteValue.number(17.0), marker.value.primitive) + assertSavedInputReturned(result = result, candidate = candidate, expected = 108.0) + + // A transport control distinguishes the setter from merely re-running the source initializer. + val adjusted = candidate.copy( + inputs = candidate.inputs.copy( + environmentFields = listOf( + marker.copy(value = CallsConcreteHeapValue(primitive = JsConcreteValue.number(5.0))) + ), + ) + ) + assertSavedInputReturned(result = result, candidate = adjusted, expected = 96.0) + + val partial = replayCallsSavedInput( + sourceRoot = directory, + sourceFile = "Target.ts", + targetSignature = checkNotNull(result.targetSignature), + candidate = candidate.copy( + environmentComplete = false, + environmentLimitations = listOf("incomplete initializer") + ), + timeoutMillis = 20_000, + ) + + assertEquals(CallsSavedInputReplayStatus.UNSUPPORTED, partial.status) + assertEquals(null, partial.observation) + assertFalse(partial.nativeReplayValidated) + + val missingCallable = replayCallsSavedInput( + sourceRoot = directory, + sourceFile = "Target.ts", + targetSignature = checkNotNull(result.targetSignature), + candidate = candidate.copy(methodName = "missingCallable"), + timeoutMillis = 20_000, + ) + + assertEquals(CallsSavedInputReplayStatus.HARNESS_FAILURE, missingCallable.status) + assertFalse(missingCallable.nativeReplayValidated) + } + + private fun assertSavedInputReturned( + result: CallsClassStartResult, + candidate: CallsClassInputCandidate, + expected: Double, + ) { + val replay = replayCallsSavedInput( + sourceRoot = directory, + sourceFile = "Target.ts", + targetSignature = checkNotNull(result.targetSignature), + candidate = candidate, + timeoutMillis = 20_000, + ) + + assertSavedInputReturn(replay = replay, expected = expected) + } + + private fun assertSavedInputReturn(replay: CallsSavedInputReplayResult, expected: Double) { + assertEquals(CallsSavedInputReplayStatus.INVOKED, replay.status, replay.toString()) + val observation = checkNotNull(replay.observation).observation + assertEquals(JsConcreteValue.String("RETURNED"), observation.values["completion"]) + val returnJson = observation.values["returnValue"] as JsConcreteValue.String + val returned = CallsExperimentJson.json.decodeFromString(returnJson.value) + assertEquals(JsConcreteValue.number(expected), returned) + assertFalse(replay.nativeReplayValidated) + assertFalse(replay.nativeCoverageAvailable) } @Test @@ -306,47 +416,6 @@ class CallsClassStartSmokeTest { assertTrue(failures.any { it.stateId == candidate.stateId && it.environmentOnly }) } - private fun replaySavedStoppedCandidate() { - val decoder = FastCheckRuntime.protocolJsonModule().resolveSibling("js-value.js").toUri().toString() - val replaySource = """ - import { readFileSync } from 'node:fs'; - import { Target, Box } from './Target.ts'; - import { decodeJsValue } from '$decoder'; - ${callsConcreteHeapRestoreSource()} - export function checkCandidate(_sentinel: boolean): boolean { - const candidate = JSON.parse(readFileSync(new URL('./candidate.json', import.meta.url), 'utf8')); - const prototypes = new Map(); - for (const node of candidate.inputs.objects) { - if (node.className === 'Target') prototypes.set(node.classSignature, Target.prototype); - if (node.className === 'Box') prototypes.set(node.classSignature, Box.prototype); - } - Target.marker = 999; - const restored = restoreCallsConcreteHeap(candidate.inputs, prototypes, decodeJsValue, (field, value) => { - if (field.ownerName !== 'Target' || field.name !== 'marker') throw Error('Unknown environment binding'); - Target.marker = value; - }); - try { restored.receiver.run(...restored.arguments); } catch (error) { - if (!(error instanceof ReferenceError)) throw error; - } - return restored.receiver.value === 91 && restored.arguments[0].value === 92 && - restored.arguments[1][0] === 93 && Target.marker === 97; - } - """.trimIndent() - Files.writeString(directory.resolve("replay.mts"), replaySource) - val property = PropertyDefinition( - id = PropertyId("calls.saved-stopped-inputs"), - inputs = listOf(PropertyInput(name = "sentinel", domain = BooleanDomain)), - predicate = TypeScriptEntryPoint(module = "replay.mts", exportName = "checkCandidate"), - ) - - val result = FastCheckBackend(sourceRoots = listOf(directory)).run( - property = property, - configuration = PropertyRunConfiguration(seed = 17, numRuns = 1, timeoutMillis = 20_000), - ) - - assertEquals(PropertyRunStatus.SUCCESS, result.status, result.toString()) - } - @Test fun `merged interface does not make its runtime class ambiguous`() { val result = runFixture( diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsConcreteHeapTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsConcreteHeapTest.kt index 8ddfe90385..1d4604a979 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsConcreteHeapTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsConcreteHeapTest.kt @@ -17,7 +17,6 @@ import org.usvm.machine.TsOptions import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunStatus import org.usvm.ts.pbt.fastcheck.FastCheckBackend -import org.usvm.ts.pbt.fastcheck.FastCheckRuntime import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyId @@ -44,6 +43,10 @@ class CallsConcreteHeapTest { fields["present"] = TsTestValue.TsUndefined fields["negativeZero"] = TsTestValue.TsNumber.TsDouble(-0.0) fields["nan"] = TsTestValue.TsNumber.TsDouble(Double.NaN) + fields["positiveInfinity"] = TsTestValue.TsNumber.TsDouble(Double.POSITIVE_INFINITY) + fields["negativeInfinity"] = TsTestValue.TsNumber.TsDouble(Double.NEGATIVE_INFINITY) + fields["nullable"] = TsTestValue.TsNull + fields["logical"] = TsTestValue.TsBoolean(value = true) val signature = EtsClassSignature( name = "Object", file = EtsFileSignature(projectName = "fixture", fileName = "Target.ts"), @@ -97,23 +100,24 @@ class CallsConcreteHeapTest { } private fun replayGraph() { - val decoder = FastCheckRuntime.protocolJsonModule().resolveSibling("js-value.js").toUri().toString() val source = """ import { readFileSync } from 'node:fs'; - import { decodeJsValue } from '$decoder'; class ObjectTarget {} + ${callsConcretePrimitiveDecoderSource()} ${callsConcreteHeapRestoreSource()} export function checkGraph(_sentinel: boolean): boolean { const graph = JSON.parse(readFileSync(new URL('./environment.json', import.meta.url), 'utf8')); const prototypes = new Map([[graph.objects[0].classSignature, ObjectTarget.prototype]]); - const restored = restoreCallsConcreteHeap(graph, prototypes, decodeJsValue); + const restored = restoreCallsConcreteHeap(graph, prototypes, decodeCallsConcretePrimitive); const receiver = restored.receiver; return Object.getPrototypeOf(receiver) === ObjectTarget.prototype && receiver.self === receiver && receiver.items === restored.arguments[0] && receiver === restored.arguments[1] && Object.hasOwn(receiver, 'present') && receiver.present === undefined && !Object.hasOwn(receiver, 'missing') && receiver.items[0].charCodeAt(0) === 0xD800 && - Object.is(receiver.negativeZero, -0) && Number.isNaN(receiver.nan); + Object.is(receiver.negativeZero, -0) && Number.isNaN(receiver.nan) && + receiver.positiveInfinity === Infinity && receiver.negativeInfinity === -Infinity && + receiver.nullable === null && receiver.logical === true; } """.trimIndent() Files.writeString(directory.resolve("replay.mts"), source) diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json index 3fcbf35f61..535b63ee3a 100644 --- a/usvm-ts-fast-check/fast-check-adapter/package.json +++ b/usvm-ts-fast-check/fast-check-adapter/package.json @@ -9,7 +9,7 @@ "build": "tsc --project tsconfig.json", "pretest": "npm run build", "test": "npm run test:compiled", - "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js dist/test/class-coverage-source.test.js" + "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js dist/test/class-coverage-source.test.js dist/test/saved-input-bindings.test.js" }, "dependencies": { "@jridgewell/trace-mapping": "0.3.31", diff --git a/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts b/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts index 7ea82753fb..47783a6a8f 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts @@ -619,7 +619,7 @@ function inspectDataClasses(file: ts.SourceFile): ClassDataClassDescriptor[] { return result.sort((left, right) => left.exportName.localeCompare(right.exportName)) } -function uniqueDirectClassExport(file: ts.SourceFile, candidate: ts.ClassDeclaration, name: string): boolean { +export function uniqueDirectClassExport(file: ts.SourceFile, candidate: ts.ClassDeclaration, name: string): boolean { const bindsName = (binding: ts.BindingName): boolean => ts.isIdentifier(binding) ? binding.text === name : binding.elements.some((element) => !ts.isOmittedExpression(element) && bindsName(element.name)) let declarations = 0 @@ -646,7 +646,7 @@ function uniqueDirectClassExport(file: ts.SourceFile, candidate: ts.ClassDeclara return declarations === 1 && candidate.name?.text === name } -function classBindingModified(file: ts.SourceFile, name: string): boolean { +export function classBindingModified(file: ts.SourceFile, name: string): boolean { const writesName = (target: ts.Node): boolean => { if (ts.isIdentifier(target)) return target.text === name if (ts.isParenthesizedExpression(target)) return writesName(target.expression) diff --git a/usvm-ts-fast-check/fast-check-adapter/src/saved-input-bindings.ts b/usvm-ts-fast-check/fast-check-adapter/src/saved-input-bindings.ts new file mode 100644 index 0000000000..265568825c --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/saved-input-bindings.ts @@ -0,0 +1,80 @@ +import ts from 'typescript' +import { classBindingModified, uniqueDirectClassExport } from './class-coverage-source.js' + +interface SavedClass { name: string; staticFields: string[] } +interface SavedBindings { exportName: string; classes: SavedClass[]; moduleBindings: string[] } +interface PreparedBindings { source: string | null; reason: string | null } + +/** Add a bridge only in the private native overlay; the original source and journal stay unchanged. */ +export function savedInputBindings(file: ts.SourceFile, request: SavedBindings): PreparedBindings { + const unsupported = (reason: string): PreparedBindings => ({ source: null, reason }) + const identifier = (name: string): boolean => /^[A-Za-z_$][A-Za-z0-9_$]*$/.test(name) + const requestedNames = [...request.classes.map((entry) => entry.name), ...request.moduleBindings, request.exportName] + if (!requestedNames.every(identifier)) return unsupported('Only ordinary top-level binding names are supported') + if (new Set(requestedNames).size !== requestedNames.length) return unsupported('Replay binding names must be distinct') + + let bridgeCollision = false + const checkBridgeName = (node: ts.Node): void => { + if (ts.isIdentifier(node) && node.text.startsWith(request.exportName)) bridgeCollision = true + ts.forEachChild(node, checkBridgeName) + } + checkBridgeName(file) + if (bridgeCollision) return unsupported('The private replay bridge name already occurs in the source') + + const parameters = `${request.exportName}Arguments` + const ownerArgument = `${parameters}[0]` + const nameArgument = `${parameters}[1]` + const valueArgument = `${parameters}[2]` + const setters: string[] = [] + for (const entry of request.classes) { + const matches = file.statements.filter(ts.isClassDeclaration).filter((node) => node.name?.text === entry.name) + const selected = matches[0] + if (matches.length !== 1 || selected === undefined || !uniqueDirectClassExport(file, selected, entry.name)) { + return unsupported(`Exact top-level class binding is unavailable: ${entry.name}`) + } + if (classBindingModified(file, entry.name)) return unsupported(`Class binding is mutable: ${entry.name}`) + const inherited = selected.heritageClauses?.some((clause) => clause.token === ts.SyntaxKind.ExtendsKeyword) + const decorated = ts.canHaveDecorators(selected) && (ts.getDecorators(selected)?.length ?? 0) > 0 + if (inherited || decorated) return unsupported(`Inherited or decorated class state is unsupported: ${entry.name}`) + + for (const member of selected.members) { + const privateName = member.name !== undefined && ts.isPrivateIdentifier(member.name) + const memberDecorated = ts.canHaveDecorators(member) && (ts.getDecorators(member)?.length ?? 0) > 0 + const asynchronous = ts.canHaveModifiers(member) + && (ts.getModifiers(member)?.some((modifier) => modifier.kind === ts.SyntaxKind.AsyncKeyword) ?? false) + const generator = ts.isMethodDeclaration(member) && member.asteriskToken !== undefined + if (privateName || memberDecorated || asynchronous || generator || ts.isClassStaticBlockDeclaration(member)) { + return unsupported(`Class has unsupported private, decorated, async or static-block state: ${entry.name}`) + } + } + + for (const name of entry.staticFields) { + const dataFields = selected.members.filter(ts.isPropertyDeclaration).filter((member) => + (ts.isIdentifier(member.name) || ts.isStringLiteral(member.name)) && member.name.text === name + && (ts.getModifiers(member)?.some((modifier) => modifier.kind === ts.SyntaxKind.StaticKeyword) ?? false)) + if (dataFields.length !== 1) return unsupported(`Exact static data field is unavailable: ${entry.name}.${name}`) + setters.push(`if (${ownerArgument} === ${JSON.stringify(entry.name)} && ${nameArgument} === ${JSON.stringify(name)}) {` + + ` ${entry.name}[${JSON.stringify(name)}] = ${valueArgument}; return; }`) + } + } + + for (const name of request.moduleBindings) { + const matches = file.statements.filter(ts.isVariableStatement).flatMap((statement) => + statement.declarationList.declarations.filter((declaration) => + ts.isIdentifier(declaration.name) && declaration.name.text === name) + .map((declaration) => ({ statement, declaration }))) + const selected = matches[0] + if (matches.length !== 1 || selected === undefined + || (selected.statement.declarationList.flags & ts.NodeFlags.Const) !== 0) { + return unsupported(`Mutable top-level module binding is unavailable: ${name}`) + } + setters.push(`if (${ownerArgument} === '%dflt' && ${nameArgument} === ${JSON.stringify(name)}) {` + + ` ${name} = ${valueArgument}; return; }`) + } + + const classes = request.classes.map((entry) => `[${JSON.stringify(entry.name)}]: ${entry.name}`).join(', ') + const bridge = `\nexport const ${request.exportName} = { classes: { ${classes} },\n` + + ` writeBinding(...${parameters}: any[]): void {\n${setters.join('\n')}\n` + + ` throw Error('Unknown saved input environment binding: ' + ${ownerArgument} + '.' + ${nameArgument});\n }\n};\n` + return { source: file.text + bridge, reason: null } +} diff --git a/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts b/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts index 81bf5c406e..b00ffc204e 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts @@ -4,6 +4,7 @@ import { instrumentSourceReplay } from './source-replay.js' import { inspectSourceCaptures } from './source-captures.js' import { inspectLocalSourceClosure, inspectStartupSourceClosure } from './local-source-closure.js' import { instrumentClassCoverage } from './class-coverage-source.js' +import { savedInputBindings } from './saved-input-bindings.js' const [operation, sourcePath, ...arguments_] = process.argv.slice(2) if (sourcePath === undefined) throw new Error('Expected a TypeScript source path') @@ -22,7 +23,11 @@ if (operation === 'inspect-local-closure' || operation === 'inspect-startup-clos }).diagnostics?.filter((diagnostic) => diagnostic.category === ts.DiagnosticCategory.Error) ?? [] if (diagnostics.length > 0) throw new Error(ts.flattenDiagnosticMessageText(diagnostics[0]?.messageText ?? '', '\n')) - if (operation === 'instrument-class-coverage') { + if (operation === 'saved-input-bindings') { + const request = arguments_[0] + if (request === undefined) throw new Error('Expected saved input bindings') + process.stdout.write(JSON.stringify(savedInputBindings(sourceFile, JSON.parse(request)))) + } else if (operation === 'instrument-class-coverage') { const className = arguments_[0] if (className === undefined) throw new Error('Expected a target class name') process.stdout.write(JSON.stringify(instrumentClassCoverage(sourceFile, className))) diff --git a/usvm-ts-fast-check/fast-check-adapter/test/saved-input-bindings.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/saved-input-bindings.test.ts new file mode 100644 index 0000000000..5a4e0d84cc --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/test/saved-input-bindings.test.ts @@ -0,0 +1,64 @@ +import assert from 'node:assert/strict' +import test from 'node:test' +import ts from 'typescript' +import { savedInputBindings } from '../src/saved-input-bindings.js' + +const prepare = (source: string, moduleBindings: string[] = []) => savedInputBindings( + ts.createSourceFile('Target.ts', source, ts.ScriptTarget.Latest, true), + { exportName: '__savedBridge', classes: [{ name: 'Target', staticFields: ['marker'] }], moduleBindings }, +) + +test('private overlay bridges exact static data and mutable module bindings', () => { + const source = 'export let count = 17; export class Target { static marker = 23; run() { return count; } }' + + const result = prepare(source, ['count']) + + assert.equal(result.reason, null) + assert.ok(result.source?.startsWith(source)) + assert.match(result.source!, /Target\["marker"\] = __savedBridgeArguments\[2\]/) + assert.match(result.source!, /count = __savedBridgeArguments\[2\]/) +}) + +test('bridge setter does not shadow module data named value', async () => { + const source = 'export let value = 17; export class Target { static marker = 23; read() { return value; } }' + const prepared = prepare(source, ['value']) + assert.equal(prepared.reason, null) + const emitted = ts.transpileModule(prepared.source!, { + compilerOptions: { target: ts.ScriptTarget.ES2022, module: ts.ModuleKind.ESNext }, + }).outputText + const module = await import(`data:text/javascript;base64,${Buffer.from(emitted).toString('base64')}`) + + module.__savedBridge.writeBinding('%dflt', 'value', 5) + + assert.equal(new module.Target().read(), 5) +}) + +test('constant, imported and nested bindings are explicit unsupported cases', () => { + const declarations = [ + 'export const count = 17;', + 'import { count } from "./other";', + 'function nested() { let count = 17; }', + ] + for (const declaration of declarations) { + const result = prepare(declaration + ' export class Target { static marker = 23; }', ['count']) + + assert.equal(result.source, null) + assert.match(result.reason!, /Mutable top-level module binding is unavailable/) + } +}) + +test('private native slots, inherited classes, reassigned bindings and static accessors are rejected', () => { + const sources = [ + 'export class Target { #value = 1; static marker = 23; }', + 'export class Target extends Base { static marker = 23; }', + 'export class Target { static marker = 23; } Target = Other;', + 'export class Target { static get marker() { return 23; } }', + 'namespace N { export class Target { static marker = 23; } }', + ] + for (const source of sources) { + const result = prepare(source) + + assert.equal(result.source, null) + assert.ok(result.reason) + } +}) diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt index 83e99151c3..31032294da 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt @@ -10,6 +10,17 @@ import java.util.concurrent.TimeUnit /** Uses the native TypeScript AST when lowered source ranges need validation or replay instrumentation. */ object TypeScriptSourceInspector { + /** A private replay overlay may expose only AST-checked source classes and mutable module data. */ + fun savedInputBindings(source: Path, bindings: TypeScriptSavedInputBindings): TypeScriptReplayInstrumentation { + val output = inspect( + source = source, + operation = "saved-input-bindings", + arguments = listOf(PropertyManifestJson.json.encodeToString(bindings)), + ) + + return PropertyManifestJson.json.decodeFromString(output) + } + fun instrumentClassCoverage(source: Path, className: String): TypeScriptClassCoverageInstrumentation { val output = inspect( source = source, @@ -139,6 +150,16 @@ object TypeScriptSourceInspector { private const val SOURCE_INSPECTION_TIMEOUT_SECONDS: Long = 10 } +@Serializable +data class TypeScriptSavedInputBindings( + val exportName: String, + val classes: List, + val moduleBindings: List, +) + +@Serializable +data class TypeScriptSavedInputClass(val name: String, val staticFields: List) + @Serializable data class TypeScriptReplayInstrumentation( val source: String?, @@ -240,4 +261,16 @@ data class TypeScriptClassDataClassDescriptor( data class TypeScriptFrozenModuleResolution( val inputSha256: Map, val tsconfig: String, + val runtimeBoundaries: List = emptyList(), +) + +@Serializable +data class TypeScriptRuntimeModuleBoundary( + val sourceFile: String, + val specifier: String, + val importKind: String, + val kind: String, + val startOffset: Int? = null, + val expression: String? = null, + val runtimeFile: String? = null, ) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt index aab7e5c3b6..5733b4e92f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt @@ -3,18 +3,31 @@ package org.usvm.samples.lang import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath import org.usvm.util.isTruthy +import java.nio.file.Path +import kotlin.io.path.readText private val TsTestValue.TsBoolean.number: Double get() = if (value) 1.0 else 0.0 class TypeCoercion : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + private val tsPath = "/samples/lang/TypeCoercion.ts" override val scene: EtsScene = loadScene(tsPath) + init { + options = options.copy(stopOnCoverage = 0, stateCollectionStrategy = StateCollectionStrategy.ALL) + } + @Test fun `test argWithConst`() { val method = getMethod("argWithConst") @@ -90,12 +103,62 @@ class TypeCoercion : TsMethodTestRunner() { } @Test - fun `test transitiveCoercionNoTypes`() { - val method = getMethod("transitiveCoercionNoTypes") + fun `untyped transitive coercion retains every numeric branch`() { + val method = getMethod("transitiveCoercionNumbers") + + discoverProperties( + method = method, + { _, _, _, result -> result.number == 1.0 }, + { _, _, _, result -> result.number == 2.0 }, + { _, _, _, result -> result.number == 3.0 }, + { _, _, _, result -> result.number == 4.0 }, + invariants = arrayOf({ a, b, c, result -> + result.number == transitiveResult(a.number, b.number, c.number) + }), + ) + } + + @Test + fun `untyped transitive coercion converts boolean inputs to numbers`() { + val method = getMethod("transitiveCoercionBoolean") - discoverProperties( - method, - // Too complicated to write property matchers, examine run log to verify the test. + discoverProperties( + method = method, + { _, _, _, result -> result.number == 2.0 }, + { _, _, _, result -> result.number == 3.0 }, + { _, _, _, result -> result.number == 4.0 }, + invariants = arrayOf({ a, b, c, result -> + result.number == transitiveResult(a.number, b.number, c.number) + }), ) } + + @Test + fun `native coercion agrees with numeric and boolean branch expectations`() { + assertNodeReplay( + source = getResourcePath(tsPath).readText() + "\n" + """ + const subject = new TypeCoercion(); + const numeric = [ + [2, 2, 2, 1], [2, 2, 3, 2], [1, 2, 3, 3], [0, 0, 0, 4], + [NaN, NaN, 2, 3], [Infinity, Infinity, Infinity, 1], [-0, 0, -0, 4], + ]; + for (const [a, b, c, expected] of numeric) { + if (subject.transitiveCoercionNumbers(a, b, c) !== expected) throw Error('numeric coercion'); + } + for (const [a, b, c, expected] of [[0, false, 2, 2], [1, false, 2, 3], [0, false, 0, 4]]) { + if (subject.transitiveCoercionBoolean(a, b, c) !== expected) throw Error('boolean coercion'); + } + """.trimIndent(), + directory = directory, + name = "transitive-coercion", + timeoutMessage = "Native transitive coercion replay timed out", + ) + } + + private fun transitiveResult(a: Double, b: Double, c: Double): Double = when { + a != b -> 3.0 + c == 0.0 || c == 1.0 -> 4.0 + !c.isNaN() && a == c -> 1.0 + else -> 2.0 + } } diff --git a/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts b/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts index 79deb9040a..ba01c77b53 100644 --- a/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts +++ b/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts @@ -79,6 +79,14 @@ class TypeCoercion { return 3; } + transitiveCoercionNumbers(a: number, b: number, c: number): number { + return this.transitiveCoercionNoTypes(a, b, c); + } + + transitiveCoercionBoolean(a: number, b: boolean, c: number): number { + return this.transitiveCoercionNoTypes(a, b, c); + } + transitiveCoercionNoTypes(a, b, c): number { if (a == b) { if (c != 0 && c != 1) {