diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 13f9f2912a..50ade7a65b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -188,7 +188,7 @@ jobs: node-version: 22 - name: Run TS PBT integration baseline - run: env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend ./gradlew :usvm-ts-pbt:check + run: env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend ./gradlew :usvm-ts-pbt:check :usvm-ts-fast-check:check lint: runs-on: ubuntu-latest diff --git a/build.gradle.kts b/build.gradle.kts index 0c4158164e..181c4fb92e 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -22,6 +22,8 @@ tasks.register("validateProjectList") { project(":usvm-jvm-instrumentation"), project(":usvm-python"), project(":usvm-ts"), + project(":usvm-ts-calls"), + project(":usvm-ts-fast-check"), project(":usvm-ts-pbt"), project(":usvm-ts-dataflow"), ) diff --git a/settings.gradle.kts b/settings.gradle.kts index 6e81861905..4331282cae 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -34,6 +34,8 @@ include("usvm-jvm:usvm-jvm-api") include("usvm-jvm:usvm-jvm-test-api") include("usvm-jvm:usvm-jvm-util") include("usvm-ts") +include("usvm-ts-calls") +include("usvm-ts-fast-check") include("usvm-ts-pbt") include("usvm-util") include("usvm-jvm-instrumentation") diff --git a/usvm-ts-calls/build.gradle.kts b/usvm-ts-calls/build.gradle.kts new file mode 100644 index 0000000000..bcc0ba431b --- /dev/null +++ b/usvm-ts-calls/build.gradle.kts @@ -0,0 +1,86 @@ +plugins { + id("usvm.kotlin-conventions") + kotlin("plugin.serialization") version Versions.kotlin + application +} + +dependencies { + implementation(project(":usvm-core")) + implementation(project(":usvm-ts")) + implementation(project(":usvm-ts-fast-check")) + implementation(project(":usvm-ts-pbt")) + implementation(Libs.jacodb_ets) + implementation(Libs.kotlinx_serialization_json) + + testImplementation(Libs.logback) +} + +val fastCheckAdapterDir = project(":usvm-ts-fast-check").layout.projectDirectory.dir("fast-check-adapter") +val fastCheckRuntimeProperty = "org.usvm.ts.pbt.fastcheck.runtime" +val generatedBuildMetadataDirectory = layout.buildDirectory.dir("generated/resources/callsBuildMetadata") +val toolRevision = providers.exec { + workingDir(rootProject.projectDir) + commandLine("git", "rev-parse", "HEAD") +}.standardOutput.asText.map(String::trim) +val toolStatus = providers.exec { + workingDir(rootProject.projectDir) + commandLine("git", "status", "--porcelain", "--untracked-files=all") +}.standardOutput.asText.map(String::trim) + +val generateBuildMetadata = tasks.register("generateBuildMetadata") { + inputs.property("toolRevision", toolRevision) + inputs.property("toolStatus", toolStatus) + outputs.dir(generatedBuildMetadataDirectory) + + doLast { + val revision = toolRevision.get() + val buildIdentity = if (toolStatus.get().isBlank()) revision else "$revision-dirty" + val metadataFile = generatedBuildMetadataDirectory.get() + .file("org/usvm/ts/calls/build.properties") + .asFile + metadataFile.parentFile.mkdirs() + metadataFile.writeText("tool.revision=$buildIdentity\n", Charsets.UTF_8) + } +} + +sourceSets.main { + resources.srcDir(generatedBuildMetadataDirectory) +} + +tasks.processResources { + dependsOn(generateBuildMetadata) +} + +tasks.test { + dependsOn(":usvm-ts-fast-check:buildFastCheckAdapter") + systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) +} + +application { + mainClass = "org.usvm.ts.calls.CallsExperimentCliKt" + applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") +} + +tasks.named("run") { + dependsOn(":usvm-ts-fast-check:buildFastCheckAdapter") + systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) +} + +distributions { + main { + contents { + into("lib/fast-check-adapter") { + from(fastCheckAdapterDir) + include("dist/src/**") + include("node_modules/**") + include("package.json") + } + } + } +} + +listOf("startScripts", "installDist", "distZip", "distTar").forEach { taskName -> + tasks.named(taskName) { + dependsOn(":usvm-ts-fast-check:buildFastCheckAdapter") + } +} 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 new file mode 100644 index 0000000000..3746582ff3 --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt @@ -0,0 +1,577 @@ +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.call.TsResidualCallPolicy +import org.usvm.ts.pbt.model.JsConcreteValue +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 java.nio.file.StandardCopyOption +import java.nio.file.StandardOpenOption +import java.util.Properties +import kotlin.time.Duration +import kotlin.time.Duration.Companion.milliseconds + +internal val CALLS_PATH_SELECTION_STRATEGY = PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM +internal const val CALLS_STOP_ON_COVERAGE = 0 + +@Serializable +internal enum class CallsExperimentProfile( + val usesFrozenModels: Boolean, + val fallback: TsResidualCallPolicy, +) { + EMPTY_STOP(usesFrozenModels = false, fallback = TsResidualCallPolicy.STOP_PATH), + EMPTY_FRESH(usesFrozenModels = false, fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + FROZEN_STOP(usesFrozenModels = true, fallback = TsResidualCallPolicy.STOP_PATH), + FROZEN_FRESH(usesFrozenModels = true, fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), +} + +@Serializable +internal data class CallsModelSetIdentity( + val ids: Set, + val toolRevision: String, +) + +@Serializable +internal data class CallsFunctionCase( + val functionId: String, + val sourceFile: String, + val entryPoint: TypeScriptEntryPoint, + val inputs: List, + val targets: List, +) + +@Serializable +internal data class CallsProjectCase( + val projectId: String, + val revision: String, + val sourceRoot: String, + val development: Boolean, + val functions: List, +) + +@Serializable +internal data class CallsExperimentManifest( + val schemaVersion: Int, + val experimentId: String, + val toolRevision: String, + val nativeFrontendRevision: String, + val solver: String, + val searchPolicy: String, + val modelSet: CallsModelSetIdentity, + val seeds: List, + val perTargetBudgetMillis: Long, + val projects: List, +) { + init { + require(schemaVersion == SCHEMA_VERSION) { "Unsupported calls experiment schema: $schemaVersion" } + require(experimentId.isNotBlank()) { "Experiment ID must not be blank" } + require(seeds.isNotEmpty() && seeds.distinct().size == seeds.size) { "Seeds must be non-empty and unique" } + require(perTargetBudgetMillis > 0) { "Per-target budget must be positive" } + require(projects.isNotEmpty()) { "At least one project is required" } + require(solver == "Z3") { "The frozen calls experiment requires the Z3 solver" } + require(searchPolicy == CALLS_PATH_SELECTION_STRATEGY.name) { + "The frozen calls experiment requires ${CALLS_PATH_SELECTION_STRATEGY.name} search" + } + val cleanGitRevision = Regex("[0-9a-f]{40}") + require(toolRevision.matches(cleanGitRevision)) { + "Tool revision must identify a clean Git commit" + } + require(toolRevision == modelSet.toolRevision) { "Tool and model-set revisions must match" } + val functions = projects.flatMap(CallsProjectCase::functions) + require(functions.map(CallsFunctionCase::functionId).distinct().size == functions.size) { + "Function IDs must be unique" + } + require(functions.all { function -> function.sourceFile == function.entryPoint.module }) { + "Function source files must match their replay entry-point modules" + } + val targets = functions.flatMap(CallsFunctionCase::targets) + require(targets.map(CallsSourceTarget::targetId).distinct().size == targets.size) { + "Target IDs must be unique" + } + require( + functions.all { function -> + function.targets.all { target -> target.sourcePath == function.sourceFile } + }, + ) { + "Every target must belong to its function source file" + } + } + + companion object { + const val SCHEMA_VERSION = 1 + } +} + +@Serializable +internal enum class CallsSymbolicStatus { + REACHED, + UNREACHED, + UNREPRESENTABLE, + UNSUPPORTED, + TIMEOUT, + TOOL_ERROR, + UNMAPPED, + AMBIGUOUS, +} + +internal data class CallsSymbolicSearchRequest( + val sourceRoot: Path, + val project: CallsProjectCase, + val function: CallsFunctionCase, + val target: CallsSourceTarget, + val profile: CallsExperimentProfile, + val frozenModelIds: Set, + val expectedNativeFrontendRevision: String, + val seed: Long, + val budget: Duration, +) + +internal data class CallsSymbolicSearchResult( + val status: CallsSymbolicStatus, + val solverReached: Boolean = status == CallsSymbolicStatus.REACHED, + val inputs: List? = null, + val elapsedMillis: Long, + val diagnostic: String? = null, +) { + init { + require(solverReached || inputs == null) { + "Only a solver-reached source target may carry extracted inputs" + } + } +} + +internal fun interface CallsSymbolicEngine { + fun search(request: CallsSymbolicSearchRequest): CallsSymbolicSearchResult +} + +@Serializable +internal sealed interface CallsRawRecord + +@Serializable +@SerialName("run-metadata") +internal data class CallsRunMetadata( + val experimentId: String, + val toolRevision: String, + val nativeFrontendRevision: String, + val modelSet: CallsModelSetIdentity, + val profiles: List, + val seeds: List, + val commonEligibleTargets: Int, + val targets: List, +) : CallsRawRecord + +@Serializable +internal data class CallsRunTargetIdentity( + val projectId: String, + val revision: String, + val development: Boolean, + val functionId: String, + val targetId: String, + val siteId: String, +) + +@Serializable +@SerialName("target-result") +internal data class CallsTargetResult( + val experimentId: String, + val projectId: String, + val revision: String, + val development: Boolean, + val functionId: String, + val targetId: String, + val siteId: String, + val profile: CallsExperimentProfile, + val seed: Long, + val symbolicStatus: CallsSymbolicStatus, + val solverReached: Boolean, + val inputExtracted: Boolean, + val inputs: List? = null, + val replayStatus: CallsReplayStatus?, + val symbolicElapsedMillis: Long, + val diagnostic: String? = null, +) : CallsRawRecord + +@Serializable +@SerialName("run-completion") +internal data class CallsRunCompletion( + val experimentId: String, + val resultRows: Int, +) : CallsRawRecord + +@Serializable +internal data class CallsExperimentSummary( + val experimentId: String, + val commonEligibleTargets: Int, + val resultRows: Int, + val byProfile: Map, +) + +@Serializable +internal data class CallsProfileSummary( + val runs: Int, + val solverReached: Int, + val inputExtracted: Int, + val replayConfirmed: Int, + val replayRejected: Int, + val unsupported: Int, + val timeouts: Int, + val toolErrors: Int, + val symbolicStatuses: Map, + val replayStatuses: Map, + val replayNotRun: Int, +) + +internal object CallsExperimentJson { + val json = Json { + classDiscriminator = "kind" + encodeDefaults = true + explicitNulls = false + ignoreUnknownKeys = false + useAlternativeNames = false + prettyPrint = false + } + + fun decodeManifest(value: String): CallsExperimentManifest = json.decodeFromString(value) + + fun encodeManifest(manifest: CallsExperimentManifest): String = json.encodeToString(manifest) +} + +internal object CallsBuildIdentity { + val toolRevision: String by lazy { + val properties = Properties() + val resource = checkNotNull(javaClass.getResourceAsStream("/org/usvm/ts/calls/build.properties")) { + "Missing calls build identity" + } + resource.use(properties::load) + + checkNotNull(properties.getProperty("tool.revision")).takeIf(String::isNotBlank) + ?: error("Missing tool revision in calls build identity") + } +} + +internal class CallsExperimentRunner( + private val symbolicEngine: CallsSymbolicEngine, + private val targetReplayer: CallsTargetReplayer, + private val runtimeToolRevision: String = CallsBuildIdentity.toolRevision, +) { + fun run( + manifest: CallsExperimentManifest, + manifestDirectory: Path, + rawOutput: Path, + ) { + require(manifest.toolRevision == runtimeToolRevision) { + "Manifest tool revision ${manifest.toolRevision} does not match running build $runtimeToolRevision" + } + require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { + "ETS_FRONTEND_SCRIPT must be unset so the frozen native frontend runtime is used" + } + val outputDirectory = requireNotNull(rawOutput.parent) { "Raw output must have a parent directory" } + val partialOutput = outputDirectory.resolve("${rawOutput.fileName}.partial") + Files.createDirectories(outputDirectory) + Files.deleteIfExists(partialOutput) + val commonEligibleTargets = manifest.projects.sumOf { project -> + project.functions.sumOf { function -> function.targets.size } + } + val metadata = CallsRunMetadata( + experimentId = manifest.experimentId, + toolRevision = manifest.toolRevision, + nativeFrontendRevision = manifest.nativeFrontendRevision, + modelSet = manifest.modelSet, + profiles = CallsExperimentProfile.entries, + seeds = manifest.seeds, + commonEligibleTargets = commonEligibleTargets, + targets = manifest.projects.flatMap { project -> + project.functions.flatMap { function -> + function.targets.map { target -> + CallsRunTargetIdentity( + projectId = project.projectId, + revision = project.revision, + development = project.development, + functionId = function.functionId, + targetId = target.targetId, + siteId = target.siteId, + ) + } + } + }, + ) + + append(partialOutput, metadata) + + manifest.projects.forEach { project -> + runProject( + manifest = manifest, + manifestDirectory = manifestDirectory, + rawOutput = partialOutput, + project = project, + ) + } + + val resultRows = Math.multiplyExact( + Math.multiplyExact(commonEligibleTargets, manifest.seeds.size), + CallsExperimentProfile.entries.size, + ) + append( + partialOutput, + CallsRunCompletion( + experimentId = manifest.experimentId, + resultRows = resultRows, + ), + ) + Files.move( + partialOutput, + rawOutput, + StandardCopyOption.ATOMIC_MOVE, + StandardCopyOption.REPLACE_EXISTING, + ) + } + + private fun runProject( + manifest: CallsExperimentManifest, + manifestDirectory: Path, + rawOutput: Path, + project: CallsProjectCase, + ) { + val sourceRoot = manifestDirectory.resolve(project.sourceRoot).normalize().toRealPath() + + project.functions.forEach { function -> + runFunction( + manifest = manifest, + rawOutput = rawOutput, + sourceRoot = sourceRoot, + project = project, + function = function, + ) + } + } + + private fun runFunction( + manifest: CallsExperimentManifest, + rawOutput: Path, + sourceRoot: Path, + project: CallsProjectCase, + function: CallsFunctionCase, + ) { + function.targets.forEach { target -> + manifest.seeds.forEach { seed -> + rotatedProfiles(seed).forEach { profile -> + val result = runTarget( + manifest = manifest, + sourceRoot = sourceRoot, + project = project, + function = function, + target = target, + seed = seed, + profile = profile, + ) + + append(rawOutput, result) + } + } + } + } + + private fun runTarget( + manifest: CallsExperimentManifest, + sourceRoot: Path, + project: CallsProjectCase, + function: CallsFunctionCase, + target: CallsSourceTarget, + seed: Long, + profile: CallsExperimentProfile, + ): CallsTargetResult { + val symbolic = symbolicEngine.search( + CallsSymbolicSearchRequest( + sourceRoot = sourceRoot, + project = project, + function = function, + target = target, + profile = profile, + frozenModelIds = manifest.modelSet.ids, + expectedNativeFrontendRevision = manifest.nativeFrontendRevision, + seed = seed, + budget = manifest.perTargetBudgetMillis.milliseconds, + ), + ) + val replay = symbolic.inputs?.let { inputs -> + targetReplayer.replay( + sourceRoots = listOf(sourceRoot), + entryPoint = function.entryPoint, + inputs = inputs, + target = target, + timeoutMillis = manifest.perTargetBudgetMillis, + ) + } + + return CallsTargetResult( + experimentId = manifest.experimentId, + projectId = project.projectId, + revision = project.revision, + development = project.development, + functionId = function.functionId, + targetId = target.targetId, + siteId = target.siteId, + profile = profile, + seed = seed, + symbolicStatus = symbolic.status, + solverReached = symbolic.solverReached, + inputExtracted = symbolic.inputs != null, + inputs = symbolic.inputs, + replayStatus = replay?.status, + symbolicElapsedMillis = symbolic.elapsedMillis, + diagnostic = replay?.message ?: replay?.reason ?: symbolic.diagnostic, + ) + } + + private fun rotatedProfiles(seed: Long): List { + val profiles = CallsExperimentProfile.entries + val offset = Math.floorMod(seed, profiles.size.toLong()).toInt() + + return profiles.drop(offset) + profiles.take(offset) + } + + private fun append(path: Path, record: CallsRawRecord) { + Files.writeString( + path, + CallsExperimentJson.json.encodeToString(record) + "\n", + StandardOpenOption.CREATE, + StandardOpenOption.APPEND, + ) + } +} + +internal data class CallsValidatedRawResults( + val metadata: CallsRunMetadata, + val results: List, +) + +internal object CallsRawResultsReader { + @Suppress("LongMethod") + fun read(rawInput: Path): CallsValidatedRawResults { + val records = Files.readAllLines(rawInput).filter(String::isNotBlank).map { line -> + CallsExperimentJson.json.decodeFromString(line) + } + val metadataRows = records.filterIsInstance() + require(metadataRows.size == 1) { "Raw results must contain exactly one metadata record" } + val metadata = metadataRows.single() + val results = records.filterIsInstance() + val completionRows = records.filterIsInstance() + require(completionRows.size == 1) { "Raw results must contain exactly one completion record" } + val completion = completionRows.single() + val expectedRows = Math.multiplyExact( + Math.multiplyExact(metadata.commonEligibleTargets, metadata.seeds.size), + metadata.profiles.size, + ) + require(completion.experimentId == metadata.experimentId) { "Completion experiment ID does not match metadata" } + require(completion.resultRows == expectedRows) { "Completion row count does not match metadata" } + require(results.size == expectedRows) { "Raw result row count does not match metadata" } + require(metadata.targets.size == metadata.commonEligibleTargets) { + "Metadata target count does not match common eligible target count" + } + val targetIdentities = metadata.targets.associateBy { target -> + Triple(target.projectId, target.functionId, target.targetId) + } + require(targetIdentities.size == metadata.targets.size) { "Metadata contains duplicate targets" } + require(results.all { result -> result.experimentId == metadata.experimentId }) { + "Result experiment ID does not match metadata" + } + require( + results.all { result -> + val identity = targetIdentities[Triple(result.projectId, result.functionId, result.targetId)] + identity != null && + result.revision == identity.revision && + result.development == identity.development && + result.siteId == identity.siteId + }, + ) { "Result target identity does not match metadata" } + val resultKeys = results.map { result -> + ResultKey( + projectId = result.projectId, + functionId = result.functionId, + targetId = result.targetId, + profile = result.profile, + seed = result.seed, + ) + } + require(resultKeys.distinct().size == resultKeys.size) { "Raw results contain duplicate target runs" } + val expectedKeys = metadata.targets.flatMap { target -> + metadata.seeds.flatMap { seed -> + metadata.profiles.map { profile -> + ResultKey( + projectId = target.projectId, + functionId = target.functionId, + targetId = target.targetId, + profile = profile, + seed = seed, + ) + } + } + } + require(resultKeys.toSet() == expectedKeys.toSet()) { "Raw results do not match the frozen target matrix" } + + return CallsValidatedRawResults(metadata = metadata, results = results) + } + + private data class ResultKey( + val projectId: String, + val functionId: String, + val targetId: String, + val profile: CallsExperimentProfile, + val seed: Long, + ) +} + +internal object CallsExperimentAggregator { + fun summarize(rawInput: Path): CallsExperimentSummary { + val (metadata, results) = CallsRawResultsReader.read(rawInput) + val byProfile = CallsExperimentProfile.entries.associateWith { profile -> + val rows = results.filter { result -> result.profile == profile } + val symbolicStatuses = CallsSymbolicStatus.entries.associateWith { status -> + rows.count { result -> result.symbolicStatus == status } + } + val replayStatuses = CallsReplayStatus.entries.associateWith { status -> + rows.count { result -> result.replayStatus == status } + } + val replayNotRun = rows.count { result -> result.replayStatus == null } + check(symbolicStatuses.values.sum() == rows.size) { "Symbolic statuses do not reconcile with profile runs" } + check(replayStatuses.values.sum() + replayNotRun == rows.size) { + "Replay statuses do not reconcile with profile runs" + } + CallsProfileSummary( + runs = rows.size, + solverReached = rows.count(CallsTargetResult::solverReached), + inputExtracted = rows.count(CallsTargetResult::inputExtracted), + replayConfirmed = rows.count { result -> result.replayStatus == CallsReplayStatus.CONFIRMED }, + replayRejected = rows.count { result -> result.replayStatus == CallsReplayStatus.REJECTED }, + unsupported = rows.count { result -> + result.symbolicStatus == CallsSymbolicStatus.UNSUPPORTED + }, + timeouts = rows.count { result -> + result.symbolicStatus == CallsSymbolicStatus.TIMEOUT || + result.replayStatus == CallsReplayStatus.TIMEOUT + }, + toolErrors = rows.count { result -> + result.symbolicStatus == CallsSymbolicStatus.TOOL_ERROR || + result.replayStatus == CallsReplayStatus.TOOL_ERROR + }, + symbolicStatuses = symbolicStatuses, + replayStatuses = replayStatuses, + replayNotRun = replayNotRun, + ) + } + + return CallsExperimentSummary( + experimentId = metadata.experimentId, + commonEligibleTargets = metadata.commonEligibleTargets, + resultRows = results.size, + byProfile = byProfile, + ) + } +} 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 new file mode 100644 index 0000000000..fda9021f1c --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt @@ -0,0 +1,95 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.encodeToString +import kotlinx.serialization.json.Json +import java.nio.file.Files +import java.nio.file.Path + +fun main(args: Array) { + require(args.isNotEmpty()) { usage() } + + when (args.first()) { + "run" -> runExperiment(args.drop(1)) + "replay-witness" -> replayWitness(args.drop(1)) + "summarize" -> summarize(args.drop(1)) + else -> error(usage()) + } +} + +internal fun replayWitness(args: List) { + require(args.size == REPLAY_WITNESS_ARGUMENT_COUNT) { usage() } + val arguments = args.iterator() + val manifestArgument = arguments.next() + val rawArgument = arguments.next() + val projectId = arguments.next() + val functionId = arguments.next() + val targetId = arguments.next() + val profileName = arguments.next() + val seedText = arguments.next() + val manifestPath = Path.of(manifestArgument).toAbsolutePath().normalize() + val rawInput = Path.of(rawArgument).toAbsolutePath().normalize() + val selector = CallsWitnessSelector( + projectId = projectId, + functionId = functionId, + targetId = targetId, + profile = CallsExperimentProfile.valueOf(profileName), + seed = seedText.toLong(), + ) + preflightCallsWitness(rawInput = rawInput, selector = selector) + + val manifest = CallsExperimentJson.decodeManifest(Files.readString(manifestPath)) + val result = CallsWitnessReplayer( + targetReplayer = OriginalTypeScriptTargetReplayer(), + ).replay( + manifest = manifest, + manifestDirectory = requireNotNull(manifestPath.parent), + rawInput = rawInput, + selector = selector, + ) + + val encoded = CallsExperimentJson.json.encodeToString(result) + System.out.appendLine(encoded) +} + +private fun runExperiment(args: List) { + require(args.size == 2) { usage() } + val manifestPath = Path.of(args[0]).toAbsolutePath().normalize() + val rawDirectory = Path.of(args[1]).toAbsolutePath().normalize() + val manifest = CallsExperimentJson.decodeManifest(Files.readString(manifestPath)) + + CallsExperimentRunner( + symbolicEngine = CurrentTsCallsSymbolicEngine(), + targetReplayer = OriginalTypeScriptTargetReplayer(), + ).run( + manifest = manifest, + manifestDirectory = requireNotNull(manifestPath.parent), + rawOutput = rawDirectory.resolve("results.jsonl"), + ) + Files.writeString( + rawDirectory.resolve("manifest.json"), + CallsExperimentJson.encodeManifest(manifest) + "\n", + ) +} + +private fun summarize(args: List) { + require(args.size == 2) { usage() } + val rawInput = Path.of(args[0]).toAbsolutePath().normalize() + val output = Path.of(args[1]).toAbsolutePath().normalize() + val summary = CallsExperimentAggregator.summarize(rawInput) + val json = Json { + encodeDefaults = true + explicitNulls = false + prettyPrint = true + } + output.parent?.let(Files::createDirectories) + Files.writeString(output, json.encodeToString(summary) + "\n") +} + +private fun usage(): String = """ + Usage: + calls run + calls replay-witness + calls summarize +""".trimIndent() + +private const val REPLAY_WITNESS_ARGUMENT_COUNT = 7 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 new file mode 100644 index 0000000000..4118cc6ade --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt @@ -0,0 +1,374 @@ +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 +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.model.ConstantDomain +import org.usvm.ts.pbt.model.ExecutionKind +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.LinkOption +import java.nio.file.Path +import java.nio.file.StandardCopyOption +import java.util.UUID + +@Serializable +internal enum class CallsReplayStatus { + @SerialName("confirmed") + CONFIRMED, + + @SerialName("rejected") + REJECTED, + + @SerialName("unmapped") + UNMAPPED, + + @SerialName("ambiguous") + AMBIGUOUS, + + @SerialName("unsupported") + UNSUPPORTED, + + @SerialName("timeout") + TIMEOUT, + + @SerialName("tool-error") + TOOL_ERROR, +} + +@Serializable +internal data class CallsSourcePosition( + val line: Int, + val column: Int, +) + +@Serializable +internal data class CallsSourceTarget( + val targetId: String, + val siteId: String, + val sourcePath: String, + val startOffset: Int, + val endOffset: Int, + val start: CallsSourcePosition, + val end: CallsSourcePosition, +) + +@Serializable +internal data class CallsSourceReplayResult( + val status: CallsReplayStatus, + val invocation: CallsInvocationResult? = null, + val reason: String? = null, + val message: String? = null, +) + +@Serializable +internal data class CallsInvocationResult( + val invocation: String, + val targetHit: Boolean, + val errorName: String? = null, + val errorMessage: String? = null, +) + +internal fun interface CallsTargetReplayer { + fun replay( + sourceRoots: List, + entryPoint: TypeScriptEntryPoint, + inputs: List, + target: CallsSourceTarget, + timeoutMillis: Long, + ): CallsSourceReplayResult +} + +internal class OriginalTypeScriptTargetReplayer : CallsTargetReplayer { + override fun replay( + sourceRoots: List, + entryPoint: TypeScriptEntryPoint, + inputs: List, + target: CallsSourceTarget, + timeoutMillis: Long, + ): CallsSourceReplayResult { + require(entryPoint.executionKind == ExecutionKind.SYNC) { + "Source-target replay currently supports synchronous callables only" + } + + return runCatching { + replaySupported( + sourceRoots = sourceRoots, + entryPoint = entryPoint, + inputs = inputs, + target = target, + timeoutMillis = timeoutMillis, + ) + }.getOrElse { error -> + CallsSourceReplayResult( + status = if (error is PbtBackendException && error.code.endsWith("timeout")) { + CallsReplayStatus.TIMEOUT + } else { + CallsReplayStatus.TOOL_ERROR + }, + message = error.message, + ) + } + } + + private fun replaySupported( + sourceRoots: List, + entryPoint: TypeScriptEntryPoint, + inputs: List, + target: CallsSourceTarget, + timeoutMillis: Long, + ): CallsSourceReplayResult { + val resolved = resolveTarget(sourceRoots = sourceRoots, sourcePath = target.sourcePath) + val source = Files.readString(resolved.source) + requireTargetCoordinates(source = source, target = target) + val workspace = Files.createTempDirectory("usvm-ts-calls-replay-") + + return try { + val overlayRoot = workspace.resolve("source-overlay") + val marker = "__usvm_source_target_${UUID.randomUUID().toString().replace('-', '_')}" + val markerStatement = ";(globalThis as Record)[${jsString(marker)}] = true;\n" + val instrumented = source.substring(0, target.startOffset) + markerStatement + + source.substring(target.startOffset) + createOverlay( + sourceRoot = resolved.sourceRoot, + overlayRoot = overlayRoot, + relativeTarget = resolved.relativeTarget, + instrumentedSource = instrumented, + ) + val resultPath = workspace.resolve("invocation.json") + val wrapperName = ".usvm-source-replay-${UUID.randomUUID()}.ts" + Files.writeString( + overlayRoot.resolve(wrapperName), + replayWrapper( + sourcePath = target.sourcePath, + exportName = entryPoint.exportName, + marker = marker, + resultPath = resultPath, + ), + ) + val replayRoots = sourceRoots.mapIndexed { index, root -> + if (index == resolved.sourceRootIndex) overlayRoot else root + } + val replayInputs = inputs.ifEmpty { listOf(JsConcreteValue.Boolean(true)) } + val property = PropertyDefinition( + id = PropertyId("calls.source-target-replay"), + inputs = replayInputs.mapIndexed { index, value -> + PropertyInput(name = "input$index", domain = ConstantDomain(value)) + }, + predicate = TypeScriptEntryPoint(module = wrapperName, exportName = REPLAY_EXPORT), + ) + val result = FastCheckBackend(sourceRoots = replayRoots).run( + property = property, + configuration = PropertyRunConfiguration( + seed = 0, + numRuns = 1, + timeoutMillis = timeoutMillis, + ), + ) + if (result.failure?.kind == PropertyFailureKind.TIMEOUT) { + return CallsSourceReplayResult(status = CallsReplayStatus.TIMEOUT) + } + val invocation = if (Files.isRegularFile(resultPath)) { + CallsExperimentJson.json.decodeFromString(Files.readString(resultPath)) + } else { + return CallsSourceReplayResult( + status = CallsReplayStatus.TOOL_ERROR, + message = result.failure?.message ?: "Source replay produced no invocation result", + ) + } + val status = when (result.status) { + PropertyRunStatus.SUCCESS -> CallsReplayStatus.CONFIRMED + PropertyRunStatus.FAILURE -> CallsReplayStatus.REJECTED + } + check(invocation.targetHit == (status == CallsReplayStatus.CONFIRMED)) { + "Source replay result does not match the concrete property outcome" + } + + CallsSourceReplayResult(status = status, invocation = invocation) + } finally { + deleteTree(workspace) + } + } + + private fun resolveTarget(sourceRoots: List, sourcePath: String): ResolvedTarget { + val relativeTarget = Path.of(sourcePath) + require(!relativeTarget.isAbsolute && relativeTarget.normalize() == relativeTarget) { + "Target source path must be normalized and relative" + } + val matches = sourceRoots.mapIndexedNotNull { index, root -> + val sourceRoot = root.toRealPath() + val candidate = sourceRoot.resolve(relativeTarget).normalize() + if (!candidate.startsWith(sourceRoot) || !Files.isRegularFile(candidate)) { + null + } else { + ResolvedTarget( + sourceRootIndex = index, + sourceRoot = sourceRoot, + relativeTarget = relativeTarget, + source = candidate.toRealPath(), + ) + } + } + require(matches.size == 1) { "Target source path resolved to ${matches.size} files" } + + return matches.single() + } + + private fun requireTargetCoordinates(source: String, target: CallsSourceTarget) { + require(target.startOffset in 0..source.length && target.endOffset in target.startOffset..source.length) { + "Target offsets are outside the source file" + } + require(sourcePositionAt(source = source, offset = target.startOffset) == target.start) { + "Target start coordinate does not match its source offset" + } + require(sourcePositionAt(source = source, offset = target.endOffset) == target.end) { + "Target end coordinate does not match its source offset" + } + } + + private fun createOverlay( + sourceRoot: Path, + overlayRoot: Path, + relativeTarget: Path, + instrumentedSource: String, + ) { + var sourceDirectory = sourceRoot + var overlayDirectory = overlayRoot + Files.createDirectories(overlayDirectory) + relativeTarget.forEachIndexed { index, segment -> + Files.newDirectoryStream(sourceDirectory).use { entries -> + entries.filter { entry -> entry.fileName != segment }.forEach { entry -> + mirrorEntry(source = entry, target = overlayDirectory.resolve(entry.fileName)) + } + } + val last = index == relativeTarget.nameCount - 1 + if (last) { + Files.writeString(overlayDirectory.resolve(segment), instrumentedSource) + } else { + sourceDirectory = sourceDirectory.resolve(segment) + overlayDirectory = overlayDirectory.resolve(segment) + Files.createDirectory(overlayDirectory) + } + } + } + + private fun mirrorEntry(source: Path, target: Path) { + val linked = runCatching { Files.createSymbolicLink(target, source.toAbsolutePath()) }.isSuccess + if (!linked) { + copyTree(source = source, target = target) + } + } + + private fun copyTree(source: Path, target: Path) { + if (Files.isDirectory(source, LinkOption.NOFOLLOW_LINKS)) { + Files.createDirectory(target) + Files.newDirectoryStream(source).use { entries -> + entries.forEach { entry -> copyTree(source = entry, target = target.resolve(entry.fileName)) } + } + } else { + Files.copy(source, target, LinkOption.NOFOLLOW_LINKS, StandardCopyOption.COPY_ATTRIBUTES) + } + } + + private fun deleteTree(root: Path) { + Files.walk(root).use { paths -> + paths.sorted(Comparator.reverseOrder()).forEach(Files::deleteIfExists) + } + } + + private fun replayWrapper( + sourcePath: String, + exportName: String, + marker: String, + resultPath: Path, + ): String = """ + import { writeFileSync } from 'node:fs'; + import * as targetModule from ${jsString("./$sourcePath")}; + + const callable = targetModule[${jsString(exportName)}]; + if (typeof callable !== 'function') throw new Error('Replay export is not a function'); + + export function $REPLAY_EXPORT(...args: unknown[]): boolean { + Object.defineProperty(globalThis, ${jsString(marker)}, { + configurable: true, + enumerable: false, + value: false, + writable: true, + }); + let invocation: 'returned' | 'threw' = 'returned'; + let caught: unknown; + try { + const result = callable(...args); + if (result !== null && (typeof result === 'object' || typeof result === 'function') + && typeof (result as { then?: unknown }).then === 'function') { + void Promise.resolve(result).catch(() => undefined); + throw new Error('Synchronous replay export returned an awaitable value'); + } + } catch (error: unknown) { + invocation = 'threw'; + caught = error; + } + const targetHit = (globalThis as Record)[${jsString(marker)}] === true; + const output: Record = { invocation, targetHit }; + if (invocation === 'threw') { + output.errorName = caught instanceof Error ? caught.name : typeof caught; + output.errorMessage = caught instanceof Error ? caught.message : String(caught); + } + writeFileSync(${jsString(resultPath.toString())}, `${'$'}{JSON.stringify(output)}\n`, 'utf8'); + + return targetHit; + } + """.trimIndent() + "\n" + + private fun jsString(value: String): String = CallsExperimentJson.json.encodeToString(value) + + private data class ResolvedTarget( + val sourceRootIndex: Int, + val sourceRoot: Path, + val relativeTarget: Path, + val source: Path, + ) + + private companion object { + const val REPLAY_EXPORT = "replaySourceTarget" + } +} + +internal fun sourcePositionAt(source: String, offset: Int): CallsSourcePosition { + var line = 0 + var column = 0 + var index = 0 + while (index < offset) { + when (source[index]) { + '\r' -> { + line += 1 + column = 0 + if (index + 1 < offset && source[index + 1] == '\n') { + index += 1 + } + } + + '\n', '\u2028', '\u2029' -> { + line += 1 + column = 0 + } + + else -> { + column += 1 + } + } + index += 1 + } + + return CallsSourcePosition(line = line, column = column) +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsWitnessReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsWitnessReplay.kt new file mode 100644 index 0000000000..631ef895b3 --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsWitnessReplay.kt @@ -0,0 +1,144 @@ +package org.usvm.ts.calls + +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.contains +import java.nio.file.Path + +internal data class CallsWitnessSelector( + val projectId: String, + val functionId: String, + val targetId: String, + val profile: CallsExperimentProfile, + val seed: Long, +) + +internal fun preflightCallsWitness(rawInput: Path, selector: CallsWitnessSelector) { + loadCallsWitness(rawInput = rawInput, selector = selector) +} + +private data class LoadedCallsWitness( + val raw: CallsValidatedRawResults, + val row: CallsTargetResult, + val inputs: List, +) + +private fun loadCallsWitness(rawInput: Path, selector: CallsWitnessSelector): LoadedCallsWitness { + val raw = CallsRawResultsReader.read(rawInput) + val row = raw.results.singleOrNull { result -> result.matches(selector) } + ?: error("Raw results must contain exactly one row for $selector") + val inputs = row.inputs + if (inputs == null && row.inputExtracted) { + error( + "The selected row is from a historical raw artifact that did not store its extracted witness; " + + "single-witness replay is unavailable", + ) + } + + return LoadedCallsWitness( + raw = raw, + row = row, + inputs = requireNotNull(inputs) { + "The selected row has no extracted witness; single-witness replay is unavailable" + }, + ) +} + +internal class CallsWitnessReplayer( + private val targetReplayer: CallsTargetReplayer, + private val runtimeToolRevision: String = CallsBuildIdentity.toolRevision, + private val verifyProjectCheckout: (Path, String) -> Unit = ::verifyCallsGitCheckout, +) { + fun replay( + manifest: CallsExperimentManifest, + manifestDirectory: Path, + rawInput: Path, + selector: CallsWitnessSelector, + ): CallsSourceReplayResult { + val loaded = loadCallsWitness(rawInput = rawInput, selector = selector) + val row = loaded.row + val inputs = loaded.inputs + + verifyExperimentIdentity(manifest = manifest, metadata = loaded.raw.metadata) + require(runtimeToolRevision == manifest.toolRevision) { + "Manifest tool revision ${manifest.toolRevision} does not match running build $runtimeToolRevision; " + + "single-witness replay requires the same clean tool revision" + } + + val project = manifest.projects.single { project -> project.projectId == selector.projectId } + require(row.revision == project.revision && row.development == project.development) { + "Selected raw row project identity does not match the frozen manifest" + } + val function = project.functions.single { function -> function.functionId == selector.functionId } + val target = function.targets.single { target -> target.targetId == selector.targetId } + require(row.siteId == target.siteId) { + "Selected raw row target identity does not match the frozen manifest" + } + require(inputs.size == function.inputs.size) { + "Stored witness has ${inputs.size} values, expected ${function.inputs.size}" + } + inputs.zip(function.inputs).forEach { (value, input) -> + require(value in input.domain) { + "Stored witness value for ${input.name} is outside the frozen input domain" + } + } + + val sourceRoot = manifestDirectory.resolve(project.sourceRoot).normalize().toRealPath() + verifyProjectCheckout(sourceRoot, project.revision) + + return targetReplayer.replay( + sourceRoots = listOf(sourceRoot), + entryPoint = function.entryPoint, + inputs = inputs, + target = target, + timeoutMillis = manifest.perTargetBudgetMillis, + ) + } + + private fun verifyExperimentIdentity( + manifest: CallsExperimentManifest, + metadata: CallsRunMetadata, + ) { + require(metadata.experimentId == manifest.experimentId) { + "Raw experiment ID does not match the frozen manifest" + } + require(metadata.toolRevision == manifest.toolRevision) { + "Raw tool revision does not match the frozen manifest" + } + require(metadata.nativeFrontendRevision == manifest.nativeFrontendRevision) { + "Raw native frontend revision does not match the frozen manifest" + } + require(metadata.modelSet == manifest.modelSet) { + "Raw model-set identity does not match the frozen manifest" + } + require(metadata.profiles == CallsExperimentProfile.entries) { + "Raw profiles do not match the frozen experiment contract" + } + require(metadata.seeds == manifest.seeds) { + "Raw seeds do not match the frozen manifest" + } + val manifestTargets = manifest.projects.flatMap { project -> + project.functions.flatMap { function -> + function.targets.map { target -> + CallsRunTargetIdentity( + projectId = project.projectId, + revision = project.revision, + development = project.development, + functionId = function.functionId, + targetId = target.targetId, + siteId = target.siteId, + ) + } + } + } + require(metadata.commonEligibleTargets == manifestTargets.size && metadata.targets == manifestTargets) { + "Raw target matrix does not match the frozen manifest" + } + } +} + +private fun CallsTargetResult.matches(selector: CallsWitnessSelector): Boolean = + projectId == selector.projectId && + functionId == selector.functionId && + targetId == selector.targetId && + profile == selector.profile && + seed == selector.seed diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt new file mode 100644 index 0000000000..b7767ed426 --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -0,0 +1,370 @@ +package org.usvm.ts.calls + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.machine.expr.extractDouble +import org.usvm.machine.expr.toConcreteBoolValue +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.contains +import org.usvm.util.mkRegisterStackLValue +import java.nio.file.Path +import kotlin.time.TimeSource + +internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { + private val verifiedProjects = mutableMapOf() + private var verifiedNativeFrontend: Pair? = null + + override fun search(request: CallsSymbolicSearchRequest): CallsSymbolicSearchResult { + val startedAt = TimeSource.Monotonic.markNow() + val unsupportedInput = request.function.inputs.firstOrNull { input -> + input.domain != BooleanDomain && input.domain !is NumberDomain + } + if (unsupportedInput != null) { + return result( + status = CallsSymbolicStatus.UNSUPPORTED, + startedAt = startedAt, + diagnostic = "Only boolean and number input domains are supported; found ${unsupportedInput.domain}", + ) + } + + return runCatching { + searchSupported(request = request, startedAt = startedAt) + }.getOrElse { error -> + result( + status = CallsSymbolicStatus.TOOL_ERROR, + startedAt = startedAt, + diagnostic = error.message ?: error::class.java.name, + ) + } + } + + @Suppress("LongMethod") + private fun searchSupported( + request: CallsSymbolicSearchRequest, + startedAt: TimeSource.Monotonic.ValueTimeMark, + ): CallsSymbolicSearchResult { + verifyGitCheckoutOnce( + checkout = request.sourceRoot, + expectedRevision = request.project.revision, + cache = verifiedProjects, + ) + verifyNativeFrontendOnce(expectedRevision = request.expectedNativeFrontendRevision) + + val source = request.sourceRoot.resolve(request.function.sourceFile).normalize() + require(source.startsWith(request.sourceRoot)) { "Function source escapes its frozen source root" } + + val sourceFile = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + if (sourceFile.importInfos.isNotEmpty()) { + return result( + status = CallsSymbolicStatus.UNSUPPORTED, + startedAt = startedAt, + diagnostic = "Single-file symbolic replay does not support imported project callees", + ) + } + val scene = EtsScene(projectFiles = listOf(sourceFile)) + val frontendEntryPoint = request.function.entryPoint.copy( + module = requireNotNull(source.fileName).toString(), + ) + val propertyManifest = PropertyManifest( + propertyId = "calls.mapping", + inputs = request.function.inputs, + predicate = frontendEntryPoint, + ) + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = listOf(request.sourceRoot)).map(propertyManifest) + if (mapping.predicate.status != EtsMappingStatus.EXACT) { + return result( + status = mapping.predicate.status.toSymbolicStatus(), + startedAt = startedAt, + diagnostic = mapping.predicate.diagnostics.joinToString { diagnostic -> diagnostic.message }, + ) + } + + val method = mapping.predicate.targets.single().method + val exactTargetCandidates = exactTargetCandidates(method, request.target) + if (exactTargetCandidates.isEmpty()) { + return result( + status = CallsSymbolicStatus.UNMAPPED, + startedAt = startedAt, + diagnostic = "No EtsIR statement has the exact frozen source range", + ) + } + val statementEntry = sourceStatementEntry(method, request.target) + if (statementEntry == null) { + return result( + status = CallsSymbolicStatus.UNSUPPORTED, + startedAt = startedAt, + diagnostic = "EtsIR origins do not prove entry before evaluation of the frozen source statement", + ) + } + + val modelSelection = if (request.profile.usesFrozenModels) { + TsUnknownCallModelSelection.Only(request.frozenModelIds) + } else { + TsUnknownCallModelSelection.Only(emptySet()) + } + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY), + stateCollectionStrategy = StateCollectionStrategy.REACHED_TARGET, + randomSeed = request.seed, + timeout = request.budget, + solverType = SolverType.Z3, + stopOnCoverage = CALLS_STOP_ON_COVERAGE, + stopOnTargetsReached = false, + throwExceptionOnStepFailure = true, + ) + val tsOptions = TsOptions( + unknownCallModelSelection = modelSelection, + unknownCallFallback = request.profile.fallback, + ) + // Observe the unique CFG entry into the source statement's origin-contained lowering region. + // This matches the replay marker before statement evaluation, including nested constructor and call lowering. + val entryObserver = SourceStatementEntryObserver(statementEntry.statement) + val analysis = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + machineObserver = entryObserver, + ).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + MachineResult( + states = entryObserver.reachedStates, + stopReason = outcome.stopReason, + ) + } + val states = analysis.states + if (states.isEmpty()) { + val status = when (analysis.stopReason) { + TsAnalysisStopReason.EXHAUSTED -> CallsSymbolicStatus.UNREACHED + // The machine options above disable every stop condition except the per-target timeout. + TsAnalysisStopReason.STOPPED -> CallsSymbolicStatus.TIMEOUT + } + + return result( + status = status, + startedAt = startedAt, + ) + } + + val inputs = states.asSequence() + .map { state -> resolveScalarInputs(state, method) } + .firstOrNull { candidate -> + candidate.zip(request.function.inputs).all { (value, input) -> value in input.domain } + } + if (inputs == null) { + return result( + status = CallsSymbolicStatus.UNREPRESENTABLE, + solverReached = true, + startedAt = startedAt, + diagnostic = "No reached state has inputs inside every frozen domain", + ) + } + + return result( + status = CallsSymbolicStatus.REACHED, + inputs = inputs, + startedAt = startedAt, + diagnostic = "source-statement-lowering-size=${statementEntry.loweringSize};" + + "exact-source-lowering-size=${exactTargetCandidates.size}", + ) + } + + private fun exactTargetCandidates(method: EtsMethod, target: CallsSourceTarget): List = + method.cfg.stmts.filter { statement -> + val origin = statement.location.origin ?: return@filter false + origin.startOffset == target.startOffset && + origin.endOffset == target.endOffset && + origin.startLine == target.start.line && + origin.startColumn == target.start.column && + origin.endLine == target.end.line && + origin.endColumn == target.end.column + } + + private fun resolveScalarInputs(state: TsState, method: EtsMethod): List = with(state.ctx) { + val model = state.models.single() + + method.parameters.mapIndexed { index, parameter -> + val stackIndex = index + 1 + when (parameter.type) { + EtsNumberType -> { + val lValue = mkRegisterStackLValue(fp64Sort, stackIndex) + val value = model.eval(state.memory.read(lValue).asExpr(fp64Sort)).extractDouble() + JsConcreteValue.number(value) + } + + EtsBooleanType -> { + val lValue = mkRegisterStackLValue(boolSort, stackIndex) + val value = model.eval(state.memory.read(lValue).asExpr(boolSort)).toConcreteBoolValue() + JsConcreteValue.Boolean(value) + } + + else -> { + error("Unsupported scalar parameter type: ${parameter.type}") + } + } + } + } + + private fun result( + status: CallsSymbolicStatus, + startedAt: TimeSource.Monotonic.ValueTimeMark, + solverReached: Boolean = status == CallsSymbolicStatus.REACHED, + inputs: List? = null, + diagnostic: String? = null, + ) = CallsSymbolicSearchResult( + status = status, + solverReached = solverReached, + inputs = inputs, + elapsedMillis = startedAt.elapsedNow().inWholeMilliseconds, + diagnostic = diagnostic, + ) + + private fun verifyNativeFrontendOnce(expectedRevision: String) { + require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { + "ETS_FRONTEND_SCRIPT must be unset so the frozen native frontend runtime is used" + } + val configuredFrontend = requireNotNull(System.getenv("ETS_FRONTEND_DIR")) { + "ETS_FRONTEND_DIR is required to verify the frozen native frontend revision" + } + val frontendDirectory = Path.of(configuredFrontend).toRealPath() + val cached = verifiedNativeFrontend + val expectedIdentity = expectedRevision + if (cached == Pair(frontendDirectory, expectedIdentity)) { + return + } + + verifyCallsGitCheckout(frontendDirectory, expectedRevision) + verifiedNativeFrontend = frontendDirectory to expectedIdentity + } + + private fun verifyGitCheckoutOnce( + checkout: Path, + expectedRevision: String, + cache: MutableMap, + ) { + if (cache[checkout] == expectedRevision) { + return + } + + verifyCallsGitCheckout(checkout, expectedRevision) + cache[checkout] = expectedRevision + } + + private class SourceStatementEntryObserver( + private val target: EtsStmt, + ) : UMachineObserver { + val reachedStates = mutableListOf() + + override fun onStatePeeked(state: TsState) { + if (state.currentStatement == target) { + reachedStates += state.clone() + } + } + } + + private data class MachineResult( + val states: List, + val stopReason: TsAnalysisStopReason, + ) +} + +internal data class SourceStatementEntry( + val statement: EtsStmt, + val loweringSize: Int, +) + +internal fun sourceStatementEntry(method: EtsMethod, target: CallsSourceTarget): SourceStatementEntry? { + val loweringRegion = method.cfg.stmts.filter { statement -> + val origin = statement.location.origin ?: return@filter false + origin.startOffset >= target.startOffset && origin.endOffset <= target.endOffset + } + val loweringRegionSet = loweringRegion.toSet() + if (loweringRegionSet.isEmpty()) { + return null + } + + val boundaryStatements = loweringRegion.filter { statement -> + val predecessors = method.cfg.predecessors(statement) + predecessors.isEmpty() || predecessors.any { predecessor -> predecessor !in loweringRegionSet } + } + val entry = boundaryStatements.singleOrNull() ?: return null + val outsidePredecessors = method.cfg.predecessors(entry).filter { predecessor -> + predecessor !in loweringRegionSet + } + val outsideOriginsAreBeforeTarget = outsidePredecessors.all { predecessor -> + val origin = predecessor.location.origin ?: return@all false + origin.endOffset <= target.startOffset + } + if (!outsideOriginsAreBeforeTarget) { + return null + } + + val reachable = mutableSetOf() + val pending = ArrayDeque() + pending += entry + while (pending.isNotEmpty()) { + val statement = pending.removeFirst() + if (!reachable.add(statement)) { + continue + } + + method.cfg.successors(statement) + .filterTo(pending) { successor -> successor in loweringRegionSet } + } + if (reachable.size != loweringRegionSet.size) { + return null + } + + return SourceStatementEntry( + statement = entry, + loweringSize = loweringRegionSet.size, + ) +} + +internal fun verifyCallsGitCheckout(checkout: Path, expectedRevision: String) { + val actualRevision = runCallsGit(checkout, "rev-parse", "HEAD").trim() + require(actualRevision == expectedRevision) { + "Checkout $checkout is at $actualRevision, expected frozen revision $expectedRevision" + } + runCallsGit(checkout, "diff", "--quiet", "HEAD", "--") +} + +private fun runCallsGit(checkout: Path, vararg arguments: String): String { + val process = ProcessBuilder(listOf("git", "-C", checkout.toString()) + arguments) + .redirectErrorStream(true) + .start() + val output = process.inputStream.bufferedReader().use { reader -> reader.readText() } + val exitCode = process.waitFor() + require(exitCode == 0) { + val command = arguments.joinToString(separator = " ") + "Git $command failed for $checkout with exit $exitCode: ${output.trim()}" + } + + return output +} + +private fun EtsMappingStatus.toSymbolicStatus(): CallsSymbolicStatus = when (this) { + EtsMappingStatus.EXACT -> error("Exact mapping has no failure status") + EtsMappingStatus.AMBIGUOUS -> CallsSymbolicStatus.AMBIGUOUS + EtsMappingStatus.UNMAPPED -> CallsSymbolicStatus.UNMAPPED + EtsMappingStatus.UNSUPPORTED -> CallsSymbolicStatus.UNSUPPORTED +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt new file mode 100644 index 0000000000..d4307c6080 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt @@ -0,0 +1,451 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.encodeToString +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.JsConcreteValue +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.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class CallsExperimentTest { + @Test + fun `manifest rejects breadth first search`() { + val accepted = manifest(sourceRoot = ".", seeds = listOf(17L)) + + assertEquals(CALLS_PATH_SELECTION_STRATEGY.name, accepted.searchPolicy) + val error = assertFailsWith { + accepted.copy(searchPolicy = "BFS") + } + + assertTrue(error.message.orEmpty().contains(CALLS_PATH_SELECTION_STRATEGY.name)) + } + + @Test + fun `runner rotates profiles and records symbolic and replay outcomes separately`(@TempDir directory: Path) { + val requests = mutableListOf() + val engine = CallsSymbolicEngine { request -> + requests += request + + when (request.profile) { + CallsExperimentProfile.EMPTY_STOP -> result(status = CallsSymbolicStatus.UNREACHED) + CallsExperimentProfile.EMPTY_FRESH -> result( + status = CallsSymbolicStatus.REACHED, + inputs = listOf(JsConcreteValue.Boolean(false)), + ) + + CallsExperimentProfile.FROZEN_STOP -> result( + status = CallsSymbolicStatus.REACHED, + inputs = listOf(JsConcreteValue.Boolean(true)), + ) + + CallsExperimentProfile.FROZEN_FRESH -> result( + status = CallsSymbolicStatus.UNREPRESENTABLE, + solverReached = true, + ) + } + } + val replayer = CallsTargetReplayer { _, _, inputs, _, _ -> + val input = inputs.single() as JsConcreteValue.Boolean + + CallsSourceReplayResult( + status = if (input.value) CallsReplayStatus.CONFIRMED else CallsReplayStatus.REJECTED, + ) + } + val rawOutput = directory.resolve("raw/results.jsonl") + + CallsExperimentRunner( + symbolicEngine = engine, + targetReplayer = replayer, + runtimeToolRevision = FIXTURE_TOOL_REVISION, + ).run( + manifest = manifest(sourceRoot = ".", seeds = listOf(1L)), + manifestDirectory = directory, + rawOutput = rawOutput, + ) + + val records = readRecords(rawOutput) + val metadata = records.filterIsInstance().single() + val results = records.filterIsInstance() + val completion = records.filterIsInstance().single() + + assertEquals(1, metadata.commonEligibleTargets) + assertEquals(4, completion.resultRows) + assertFalse(Files.exists(rawOutput.resolveSibling("results.jsonl.partial"))) + assertEquals( + listOf( + CallsExperimentProfile.EMPTY_FRESH, + CallsExperimentProfile.FROZEN_STOP, + CallsExperimentProfile.FROZEN_FRESH, + CallsExperimentProfile.EMPTY_STOP, + ), + requests.map(CallsSymbolicSearchRequest::profile), + ) + assertEquals(requests.map(CallsSymbolicSearchRequest::profile), results.map(CallsTargetResult::profile)) + + val emptyFresh = results.single { result -> result.profile == CallsExperimentProfile.EMPTY_FRESH } + assertTrue(emptyFresh.solverReached) + assertTrue(emptyFresh.inputExtracted) + assertEquals(listOf(JsConcreteValue.Boolean(false)), emptyFresh.inputs) + assertEquals(CallsReplayStatus.REJECTED, emptyFresh.replayStatus) + + val frozenStop = results.single { result -> result.profile == CallsExperimentProfile.FROZEN_STOP } + assertTrue(frozenStop.solverReached) + assertTrue(frozenStop.inputExtracted) + assertEquals(listOf(JsConcreteValue.Boolean(true)), frozenStop.inputs) + assertEquals(CallsReplayStatus.CONFIRMED, frozenStop.replayStatus) + + val emptyStop = results.single { result -> result.profile == CallsExperimentProfile.EMPTY_STOP } + assertFalse(emptyStop.solverReached) + assertFalse(emptyStop.inputExtracted) + assertNull(emptyStop.inputs) + assertNull(emptyStop.replayStatus) + + val frozenFresh = results.single { result -> result.profile == CallsExperimentProfile.FROZEN_FRESH } + assertTrue(frozenFresh.solverReached) + assertFalse(frozenFresh.inputExtracted) + assertNull(frozenFresh.inputs) + assertNull(frozenFresh.replayStatus) + } + + @Test + fun `target result witness uses lossless concrete value serialization`() { + val witness = listOf( + JsConcreteValue.number(-0.0), + JsConcreteValue.number(Double.NaN), + JsConcreteValue.Array( + elements = listOf(JsConcreteValue.Undefined, JsConcreteValue.Null, JsConcreteValue.String("value")), + ), + ) + val result = targetResult(inputs = witness) + + val encoded = CallsExperimentJson.json.encodeToString(result) + val decoded = CallsExperimentJson.json.decodeFromString(encoded) as CallsTargetResult + + assertEquals(result, decoded) + assertEquals(witness, decoded.inputs) + } + + @Test + fun `single witness replay uses selected stored inputs without symbolic search`(@TempDir directory: Path) { + val rawOutput = directory.resolve("results.jsonl") + val frozenManifest = manifest(sourceRoot = ".", seeds = listOf(11L)) + CallsExperimentRunner( + symbolicEngine = CallsSymbolicEngine { + result( + status = CallsSymbolicStatus.REACHED, + inputs = listOf(JsConcreteValue.Boolean(true)), + ) + }, + targetReplayer = CallsTargetReplayer { _, _, _, _, _ -> + CallsSourceReplayResult(status = CallsReplayStatus.CONFIRMED) + }, + runtimeToolRevision = FIXTURE_TOOL_REVISION, + ).run( + manifest = frozenManifest, + manifestDirectory = directory, + rawOutput = rawOutput, + ) + var replayedInputs: List? = null + var replayedTarget: CallsSourceTarget? = null + var replayedTimeout: Long? = null + var verifiedCheckout: Path? = null + val witnessReplayer = CallsWitnessReplayer( + targetReplayer = CallsTargetReplayer { _, _, inputs, target, timeoutMillis -> + replayedInputs = inputs + replayedTarget = target + replayedTimeout = timeoutMillis + + CallsSourceReplayResult(status = CallsReplayStatus.REJECTED) + }, + runtimeToolRevision = FIXTURE_TOOL_REVISION, + verifyProjectCheckout = { checkout, expectedRevision -> + assertEquals("project-revision", expectedRevision) + verifiedCheckout = checkout + }, + ) + + val replay = witnessReplayer.replay( + manifest = frozenManifest, + manifestDirectory = directory, + rawInput = rawOutput, + selector = selector(seed = 11L, profile = CallsExperimentProfile.FROZEN_STOP), + ) + + val expectedTarget = frozenManifest.projects + .single() + .functions + .single() + .targets + .single() + assertEquals(CallsReplayStatus.REJECTED, replay.status) + assertEquals(listOf(JsConcreteValue.Boolean(true)), replayedInputs) + assertEquals(expectedTarget, replayedTarget) + assertEquals(1_000L, replayedTimeout) + assertEquals(directory.toRealPath(), verifiedCheckout) + } + + @Test + fun `historical extracted row without stored witness reports replay unavailable first`(@TempDir directory: Path) { + val rawOutput = directory.resolve("results.jsonl") + val frozenManifest = manifest(sourceRoot = ".", seeds = listOf(5L)) + CallsExperimentRunner( + symbolicEngine = CallsSymbolicEngine { + result( + status = CallsSymbolicStatus.REACHED, + inputs = listOf(JsConcreteValue.Boolean(true)), + ) + }, + targetReplayer = CallsTargetReplayer { _, _, _, _, _ -> + CallsSourceReplayResult(status = CallsReplayStatus.CONFIRMED) + }, + runtimeToolRevision = FIXTURE_TOOL_REVISION, + ).run( + manifest = frozenManifest, + manifestDirectory = directory, + rawOutput = rawOutput, + ) + val historicalRecords = readRecords(rawOutput).map { record -> + when { + record is CallsTargetResult && record.profile == CallsExperimentProfile.EMPTY_FRESH -> { + record.copy(inputs = null) + } + + else -> { + record + } + } + } + writeRecords(rawOutput, historicalRecords) + val witnessReplayer = CallsWitnessReplayer( + targetReplayer = CallsTargetReplayer { _, _, _, _, _ -> error("Replay must not run") }, + runtimeToolRevision = "different-runtime-revision", + verifyProjectCheckout = { _, _ -> error("Checkout verification must not run") }, + ) + + val error = assertFailsWith { + witnessReplayer.replay( + manifest = frozenManifest, + manifestDirectory = directory, + rawInput = rawOutput, + selector = selector(seed = 5L, profile = CallsExperimentProfile.EMPTY_FRESH), + ) + } + + assertTrue(error.message.orEmpty().contains("historical raw artifact")) + assertTrue(error.message.orEmpty().contains("single-witness replay is unavailable")) + + val manifestPath = directory.resolve("historical-manifest.json") + Files.writeString(manifestPath, CallsExperimentJson.encodeManifest(frozenManifest)) + + val cliError = assertFailsWith { + replayWitness( + listOf( + manifestPath.toString(), + rawOutput.toString(), + "fixture/project", + "fixture.ts::predicate/1", + "fixture.ts::predicate/1#return", + CallsExperimentProfile.EMPTY_FRESH.name, + "5", + ), + ) + } + + assertTrue(cliError.message.orEmpty().contains("historical raw artifact")) + assertTrue(cliError.message.orEmpty().contains("single-witness replay is unavailable")) + } + + @Test + fun `aggregator rejects an interrupted raw prefix without completion`(@TempDir directory: Path) { + val rawOutput = directory.resolve("results.jsonl") + val engine = CallsSymbolicEngine { result(status = CallsSymbolicStatus.UNREACHED) } + + CallsExperimentRunner( + symbolicEngine = engine, + targetReplayer = CallsTargetReplayer { _, _, _, _, _ -> error("Replay must not run") }, + runtimeToolRevision = FIXTURE_TOOL_REVISION, + ).run( + manifest = manifest(sourceRoot = ".", seeds = listOf(0L)), + manifestDirectory = directory, + rawOutput = rawOutput, + ) + val interrupted = directory.resolve("interrupted.jsonl") + Files.write(interrupted, Files.readAllLines(rawOutput).dropLast(1)) + + assertFailsWith { + CallsExperimentAggregator.summarize(interrupted) + } + } + + @Test + fun `aggregator counts each profile from raw rows without collapsing outcome stages`(@TempDir directory: Path) { + val rawOutput = directory.resolve("results.jsonl") + val statuses = mapOf( + CallsExperimentProfile.EMPTY_STOP to CallsSymbolicStatus.TIMEOUT, + CallsExperimentProfile.EMPTY_FRESH to CallsSymbolicStatus.REACHED, + CallsExperimentProfile.FROZEN_STOP to CallsSymbolicStatus.REACHED, + CallsExperimentProfile.FROZEN_FRESH to CallsSymbolicStatus.TOOL_ERROR, + ) + val engine = CallsSymbolicEngine { request -> + val status = statuses.getValue(request.profile) + result( + status = status, + inputs = if (status == CallsSymbolicStatus.REACHED) { + listOf(JsConcreteValue.Boolean(request.profile.usesFrozenModels)) + } else { + null + }, + ) + } + val replayer = CallsTargetReplayer { _, _, inputs, _, _ -> + val input = inputs.single() as JsConcreteValue.Boolean + CallsSourceReplayResult( + status = if (input.value) CallsReplayStatus.CONFIRMED else CallsReplayStatus.REJECTED, + ) + } + + CallsExperimentRunner( + symbolicEngine = engine, + targetReplayer = replayer, + runtimeToolRevision = FIXTURE_TOOL_REVISION, + ).run( + manifest = manifest(sourceRoot = ".", seeds = listOf(0L, 3L)), + manifestDirectory = directory, + rawOutput = rawOutput, + ) + val summary = CallsExperimentAggregator.summarize(rawOutput) + + assertEquals("fixture", summary.experimentId) + assertEquals(1, summary.commonEligibleTargets) + assertEquals(8, summary.resultRows) + assertEquals( + CallsProfileSummary( + runs = 2, + solverReached = 0, + inputExtracted = 0, + replayConfirmed = 0, + replayRejected = 0, + unsupported = 0, + timeouts = 2, + toolErrors = 0, + symbolicStatuses = CallsSymbolicStatus.entries.associateWith { status -> + if (status == CallsSymbolicStatus.TIMEOUT) 2 else 0 + }, + replayStatuses = CallsReplayStatus.entries.associateWith { 0 }, + replayNotRun = 2, + ), + summary.byProfile.getValue(CallsExperimentProfile.EMPTY_STOP), + ) + assertEquals(2, summary.byProfile.getValue(CallsExperimentProfile.EMPTY_FRESH).replayRejected) + assertEquals(2, summary.byProfile.getValue(CallsExperimentProfile.FROZEN_STOP).replayConfirmed) + assertEquals(2, summary.byProfile.getValue(CallsExperimentProfile.FROZEN_FRESH).toolErrors) + } + + private fun manifest(sourceRoot: String, seeds: List) = CallsExperimentManifest( + schemaVersion = CallsExperimentManifest.SCHEMA_VERSION, + experimentId = "fixture", + toolRevision = FIXTURE_TOOL_REVISION, + nativeFrontendRevision = "frontend-revision", + solver = "Z3", + searchPolicy = CALLS_PATH_SELECTION_STRATEGY.name, + modelSet = CallsModelSetIdentity( + ids = setOf("ts.array.pop", "ts.array.shift"), + toolRevision = FIXTURE_TOOL_REVISION, + ), + seeds = seeds, + perTargetBudgetMillis = 1_000L, + projects = listOf( + CallsProjectCase( + projectId = "fixture/project", + revision = "project-revision", + sourceRoot = sourceRoot, + development = true, + functions = listOf( + CallsFunctionCase( + functionId = "fixture.ts::predicate/1", + sourceFile = "fixture.ts", + entryPoint = TypeScriptEntryPoint( + module = "fixture.ts", + exportName = "predicate", + ), + inputs = listOf(PropertyInput(name = "value", domain = BooleanDomain)), + targets = listOf( + CallsSourceTarget( + targetId = "fixture.ts::predicate/1#return", + siteId = "fixture.ts:1:1-1:12::predicate/1", + sourcePath = "fixture.ts", + startOffset = 0, + endOffset = 11, + start = CallsSourcePosition(line = 0, column = 0), + end = CallsSourcePosition(line = 0, column = 11), + ), + ), + ), + ), + ), + ), + ) + + private fun result( + status: CallsSymbolicStatus, + solverReached: Boolean = status == CallsSymbolicStatus.REACHED, + inputs: List? = null, + ) = CallsSymbolicSearchResult( + status = status, + solverReached = solverReached, + inputs = inputs, + elapsedMillis = 7L, + ) + + private fun readRecords(path: Path): List = Files.readAllLines(path) + .filter(String::isNotBlank) + .map { line -> CallsExperimentJson.json.decodeFromString(line) } + + private fun writeRecords(path: Path, records: List) { + Files.writeString( + path, + records.joinToString(separator = "\n", postfix = "\n") { record -> + CallsExperimentJson.json.encodeToString(record) + }, + ) + } + + private fun selector(seed: Long, profile: CallsExperimentProfile) = CallsWitnessSelector( + projectId = "fixture/project", + functionId = "fixture.ts::predicate/1", + targetId = "fixture.ts::predicate/1#return", + profile = profile, + seed = seed, + ) + + private fun targetResult(inputs: List) = CallsTargetResult( + experimentId = "fixture", + projectId = "fixture/project", + revision = "project-revision", + development = true, + functionId = "fixture.ts::predicate/1", + targetId = "fixture.ts::predicate/1#return", + siteId = "fixture.ts:1:1-1:12::predicate/1", + profile = CallsExperimentProfile.FROZEN_STOP, + seed = 1L, + symbolicStatus = CallsSymbolicStatus.REACHED, + solverReached = true, + inputExtracted = true, + inputs = inputs, + replayStatus = CallsReplayStatus.CONFIRMED, + symbolicElapsedMillis = 7L, + ) + + private companion object { + const val FIXTURE_TOOL_REVISION = "0000000000000000000000000000000000000001" + } +} 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 new file mode 100644 index 0000000000..7f764c3a7c --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt @@ -0,0 +1,108 @@ +package org.usvm.ts.calls + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.test.assertEquals +import kotlin.test.assertNotNull + +class CallsSourceReplayTest { + @Test + fun `confirms only the exact source statement reached by original TypeScript`() { + val fixture = fixture() + val taken = fixture.target(functionName = "inlineChoose", statement = "return 1;") + val untaken = fixture.target(functionName = "inlineChoose", statement = "return 0;") + + val takenReplay = fixture.replay(exportName = "inlineChoose", inputs = listOf(number(1.0)), target = taken) + val untakenReplay = fixture.replay(exportName = "inlineChoose", inputs = listOf(number(1.0)), target = untaken) + + assertEquals(CallsReplayStatus.CONFIRMED, takenReplay.status) + assertEquals(true, takenReplay.invocation?.targetHit) + assertEquals(CallsReplayStatus.REJECTED, untakenReplay.status) + assertEquals(false, untakenReplay.invocation?.targetHit) + } + + @Test + fun `retains target confirmation when the original invocation throws`() { + val fixture = fixture() + val target = fixture.target(functionName = "throwsAtTarget", statement = "throw new Error('expected');") + + val replay = fixture.replay(exportName = "throwsAtTarget", inputs = emptyList(), target = target) + + assertEquals(CallsReplayStatus.CONFIRMED, replay.status, replay.toString()) + assertEquals("threw", replay.invocation?.invocation) + assertEquals(true, replay.invocation?.targetHit) + assertEquals("Error", replay.invocation?.errorName) + assertEquals("expected", replay.invocation?.errorMessage) + } + + @Test + fun `counts target hits from the selected invocation rather than module import`() { + val fixture = fixture() + val target = fixture.target(functionName = "importOnlyTarget", statement = "return 7;") + + val importOnly = fixture.replay(exportName = "skipsImportOnlyTarget", inputs = emptyList(), target = target) + val invoked = fixture.replay(exportName = "importOnlyTarget", inputs = emptyList(), target = target) + + assertEquals(CallsReplayStatus.REJECTED, importOnly.status, importOnly.toString()) + assertEquals(false, importOnly.invocation?.targetHit) + assertEquals(CallsReplayStatus.CONFIRMED, invoked.status) + assertEquals(true, invoked.invocation?.targetHit) + } + + private fun fixture(): Fixture { + val sourcePath = resourcePath("/calls/SourceTargetReplayFixture.ts") + + return Fixture( + sourceRoot = assertNotNull(sourcePath.parent?.parent), + sourcePath = sourcePath, + source = Files.readString(sourcePath), + ) + } + + private fun resourcePath(name: String): Path { + val resource = assertNotNull(javaClass.getResource(name), "Missing test resource $name") + + return Paths.get(resource.toURI()) + } + + private fun number(value: Double): JsConcreteValue = JsConcreteValue.number(value) + + private data class Fixture( + val sourceRoot: Path, + val sourcePath: Path, + val source: String, + ) { + fun target(functionName: String, statement: String): CallsSourceTarget { + val functionStart = source.indexOf("function $functionName") + val startOffset = source.indexOf(statement, startIndex = functionStart) + check(functionStart >= 0 && startOffset >= 0) { "Missing $statement in $functionName" } + val endOffset = startOffset + statement.length + + return CallsSourceTarget( + targetId = "$functionName#$statement", + siteId = "$functionName:$startOffset:$endOffset", + sourcePath = sourceRoot.relativize(sourcePath).joinToString(separator = "/"), + startOffset = startOffset, + endOffset = endOffset, + start = sourcePositionAt(source = source, offset = startOffset), + end = sourcePositionAt(source = source, offset = endOffset), + ) + } + + fun replay( + exportName: String, + inputs: List, + target: CallsSourceTarget, + ): CallsSourceReplayResult = OriginalTypeScriptTargetReplayer().replay( + sourceRoots = listOf(sourceRoot), + entryPoint = TypeScriptEntryPoint(module = target.sourcePath, exportName = exportName), + inputs = inputs, + target = target, + timeoutMillis = 10_000L, + ) + } +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/SourceStatementEntryTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/SourceStatementEntryTest.kt new file mode 100644 index 0000000000..b1949af26c --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/SourceStatementEntryTest.kt @@ -0,0 +1,153 @@ +package org.usvm.ts.calls + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.test.assertEquals +import kotlin.test.assertNotEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class SourceStatementEntryTest { + @Test + fun `throw entry precedes constructor lowering and exact throw instruction`() { + val fixture = loadFixture() + val sourceStatement = "throw new Error('negative');" + val target = fixture.target(sourceStatement) + val exactThrow = fixture.method("nestedLowering").exactStatement(target) + + val entry = assertNotNull(sourceStatementEntry(fixture.method("nestedLowering"), target)) + + assertTrue(entry.loweringSize > 1, "Throw statement must contain nested constructor lowering") + assertNotEquals(exactThrow, entry.statement, "Entry must precede the exact throw instruction") + assertTrue( + fixture.method("nestedLowering").reachesWithinTarget(entry.statement, exactThrow, target), + "Exact throw instruction must be reachable from the selected entry inside the statement", + ) + } + + @Test + fun `return entry precedes nested call lowering and exact return instruction`() { + val fixture = loadFixture() + val sourceStatement = "return Math.round(value) / 2;" + val target = fixture.target(sourceStatement) + val exactReturn = fixture.method("nestedLowering").exactStatement(target) + + val entry = assertNotNull(sourceStatementEntry(fixture.method("nestedLowering"), target)) + + assertTrue(entry.loweringSize > 1, "Return statement must contain nested call lowering") + assertNotEquals(exactReturn, entry.statement, "Entry must precede the exact return instruction") + assertTrue( + fixture.method("nestedLowering").reachesWithinTarget(entry.statement, exactReturn, target), + "Exact return instruction must be reachable from the selected entry inside the statement", + ) + } + + @Test + fun `multiple CFG entries into a candidate source range are rejected`() { + val fixture = loadFixture() + val source = fixture.source + val firstBranch = source.indexOf("return -value;") + val secondBranchEnd = source.indexOf("return value;") + "return value;".length + val target = fixture.target(startOffset = firstBranch, endOffset = secondBranchEnd) + + val entry = sourceStatementEntry(fixture.method("separateBranches"), target) + + assertNull(entry) + } + + private fun loadFixture(): Fixture { + val path = resourcePath("/calls/SourceStatementEntryFixture.ts") + val source = Files.readString(path) + val file = loadEtsFileAutoConvert(path, provider = EtsIrProvider.TS_FRONTEND) + val methods = EtsScene(projectFiles = listOf(file)).projectClasses + .flatMap { projectClass -> projectClass.methods } + .associateBy { method -> method.name } + + return Fixture(source = source, methods = methods) + } + + private fun resourcePath(name: String): Path { + val resource = assertNotNull(javaClass.getResource(name), "Missing test resource $name") + return Paths.get(resource.toURI()) + } + + private data class Fixture( + val source: String, + val methods: Map, + ) { + fun method(name: String): EtsMethod = assertNotNull(methods[name], "Missing method $name") + + fun target(sourceStatement: String): CallsSourceTarget { + val startOffset = source.indexOf(sourceStatement) + assertTrue(startOffset >= 0, "Missing source statement: $sourceStatement") + + return target(startOffset = startOffset, endOffset = startOffset + sourceStatement.length) + } + + fun target(startOffset: Int, endOffset: Int): CallsSourceTarget = CallsSourceTarget( + targetId = "test-target", + siteId = "test-site", + sourcePath = "SourceStatementEntryFixture.ts", + startOffset = startOffset, + endOffset = endOffset, + start = source.positionAt(startOffset), + end = source.positionAt(endOffset), + ) + } +} + +private inline fun EtsMethod.exactStatement(target: CallsSourceTarget): T { + val matches = cfg.stmts.filterIsInstance().filter { statement -> + val origin = statement.location.origin ?: return@filter false + origin.startOffset == target.startOffset && origin.endOffset == target.endOffset + } + + return assertEquals(1, matches.size, "Expected one exact ${T::class.simpleName} statement").let { + matches.single() + } +} + +private fun EtsMethod.reachesWithinTarget( + start: EtsStmt, + targetStatement: EtsStmt, + target: CallsSourceTarget, +): Boolean { + val pending = ArrayDeque() + val visited = mutableSetOf() + pending += start + while (pending.isNotEmpty()) { + val statement = pending.removeFirst() + if (!visited.add(statement)) { + continue + } + if (statement == targetStatement) { + return true + } + + cfg.successors(statement).filterTo(pending) { successor -> + val origin = successor.location.origin ?: return@filterTo false + origin.startOffset >= target.startOffset && origin.endOffset <= target.endOffset + } + } + + return false +} + +private fun String.positionAt(offset: Int): CallsSourcePosition { + val prefix = substring(startIndex = 0, endIndex = offset) + val line = prefix.count { character -> character == '\n' } + val lastLineBreak = prefix.lastIndexOf('\n') + val column = offset - lastLineBreak - 1 + + return CallsSourcePosition(line = line, column = column) +} diff --git a/usvm-ts-calls/src/test/resources/calls/SourceStatementEntryFixture.ts b/usvm-ts-calls/src/test/resources/calls/SourceStatementEntryFixture.ts new file mode 100644 index 0000000000..aa00452346 --- /dev/null +++ b/usvm-ts-calls/src/test/resources/calls/SourceStatementEntryFixture.ts @@ -0,0 +1,15 @@ +export function nestedLowering(value: number): number { + if (value < 0) { + throw new Error('negative'); + } + + return Math.round(value) / 2; +} + +export function separateBranches(value: number): number { + if (value < 0) { + return -value; + } else { + return value; + } +} diff --git a/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts b/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts new file mode 100644 index 0000000000..dd20e17a49 --- /dev/null +++ b/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts @@ -0,0 +1,15 @@ +export function inlineChoose(value: number): number { if (value > 0) { return 1; } return 0; } + +export function throwsAtTarget(): never { + throw new Error('expected'); +} + +export function importOnlyTarget(): number { + return 7; +} + +const importedTargetValue = importOnlyTarget(); + +export function skipsImportOnlyTarget(): number { + return importedTargetValue; +} diff --git a/usvm-ts-pbt/DESIGN.md b/usvm-ts-fast-check/DESIGN.md similarity index 96% rename from usvm-ts-pbt/DESIGN.md rename to usvm-ts-fast-check/DESIGN.md index 0e40b60571..8859c5196d 100644 --- a/usvm-ts-pbt/DESIGN.md +++ b/usvm-ts-fast-check/DESIGN.md @@ -1,11 +1,13 @@ # Kotlin–TypeScript fast-check integration -This document describes the internal boundary between Kotlin and the private Node adapter. For the public property -API and CLI examples, see [README.md](README.md). +This document describes the `usvm-ts-fast-check` boundary between Kotlin and the private Node adapter. The +backend-neutral property, coverage, and mapping contracts live in `usvm-ts-pbt`. For public backend and CLI +examples, see [README.md](README.md). ## Design goals -- Kotlin owns property definitions, validation, registries, orchestration, and public results. +- `usvm-ts-pbt` owns property definitions, validation, registries, coverage decoding, mapping, and public results. +- `usvm-ts-fast-check` owns FastCheck orchestration and runtime packaging. - Node is a thin adapter around fast-check and direct TypeScript loading. - Per-property source coverage is an optional backend capability collected by Kotlin through an isolated c8 run. - A backend-neutral Kotlin mapping layer connects manifests and source coverage to EtsIR without changing the @@ -72,7 +74,7 @@ separate Istanbul report after a valid response. Backend identity belongs to `co Kotlin validates trusted model objects and examples early so callers get local errors. Node validates the decoded JSON again because the process boundary must not trust malformed input. Diagnostic codes have one owner per -language: `PbtDiagnosticCode.kt` for Kotlin and `diagnostics.ts` for Node. Node also sends the diagnostic category, +language: `FastCheckDiagnosticCode.kt` for Kotlin and `diagnostics.ts` for Node. Node also sends the diagnostic category, so Kotlin never infers error meaning from code prefixes. ## One property run diff --git a/usvm-ts-fast-check/README.md b/usvm-ts-fast-check/README.md new file mode 100644 index 0000000000..746c3ea1ab --- /dev/null +++ b/usvm-ts-fast-check/README.md @@ -0,0 +1,15 @@ +# USVM TypeScript FastCheck backend + +`usvm-ts-fast-check` implements the backend-neutral contracts from `usvm-ts-pbt` with FastCheck. It owns +`FastCheckBackend`, the Node adapter, supervised process transport, c8 coverage collection, CLI, and packaged +runtime. + +The public property model, validation, registries, coverage contracts and decoders, and property-to-EtsIR mapping +remain in [`usvm-ts-pbt`](../usvm-ts-pbt/README.md). + +Run the backend checks with: + +```shell +env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ + ./gradlew --no-daemon :usvm-ts-fast-check:check +``` diff --git a/usvm-ts-fast-check/build.gradle.kts b/usvm-ts-fast-check/build.gradle.kts new file mode 100644 index 0000000000..bd10be1065 --- /dev/null +++ b/usvm-ts-fast-check/build.gradle.kts @@ -0,0 +1,171 @@ +import groovy.json.JsonSlurper + +plugins { + id("usvm.kotlin-conventions") + kotlin("plugin.serialization") version Versions.kotlin + application +} + +dependencies { + implementation(project(":usvm-ts-pbt")) + implementation(Libs.clikt) + implementation(Libs.kotlinx_serialization_json) + + testImplementation(Libs.logback) +} + +val fastCheckAdapterDir = layout.projectDirectory.dir("fast-check-adapter") +val fastCheckAdapterPackageJson = fastCheckAdapterDir.file("package.json") +val fastCheckAdapterPackageLock = fastCheckAdapterDir.file("package-lock.json") +val fastCheckRuntimeProperty = "org.usvm.ts.pbt.fastcheck.runtime" +val generatedFastCheckRuntimeMetadataDirectory = layout.buildDirectory.dir( + "generated/resources/fastCheckRuntimeMetadata", +) +val hostOperatingSystem = System.getProperty("os.name").lowercase() +val hostPlatform = when { + hostOperatingSystem.contains("mac") -> "darwin" + hostOperatingSystem.contains("linux") -> "linux" + hostOperatingSystem.contains("windows") -> "win32" + else -> error("Unsupported fast-check runtime operating system: $hostOperatingSystem") +} +val hostArchitecture = when (val architecture = System.getProperty("os.arch").lowercase()) { + "aarch64", "arm64" -> "arm64" + "amd64", "x86_64" -> "x64" + "x86", "i386", "i686" -> "ia32" + else -> error("Unsupported fast-check runtime architecture: $architecture") +} +val fastCheckRuntimeClassifier = "$hostPlatform-$hostArchitecture" +val npmExecutable = if (hostPlatform == "win32") "npm.cmd" else "npm" + +val generateFastCheckRuntimeMetadata = tasks.register("generateFastCheckRuntimeMetadata") { + inputs.file(fastCheckAdapterPackageLock) + outputs.dir(generatedFastCheckRuntimeMetadataDirectory) + + doLast { + val packageLock = JsonSlurper().parse(fastCheckAdapterPackageLock.asFile) as? Map<*, *> + ?: error("Invalid fast-check adapter package lock") + val packages = packageLock["packages"] as? Map<*, *> + ?: error("Missing packages in fast-check adapter package lock") + fun dependencyVersion(dependency: String): String { + val metadata = packages["node_modules/$dependency"] as? Map<*, *> + ?: error("Missing locked fast-check adapter dependency: $dependency") + + return (metadata["version"] as? String) + ?.takeIf(String::isNotBlank) + ?: error("Missing locked fast-check adapter dependency version: $dependency") + } + + val metadataFile = generatedFastCheckRuntimeMetadataDirectory.get() + .file("org/usvm/ts/pbt/fastcheck/runtime-dependencies.properties") + .asFile + metadataFile.parentFile.mkdirs() + metadataFile.writeText( + """ + fast-check.version=${dependencyVersion("fast-check")} + c8.version=${dependencyVersion("c8")} + """.trimIndent() + "\n", + Charsets.UTF_8, + ) + } +} + +sourceSets.main { + resources.srcDir(generatedFastCheckRuntimeMetadataDirectory) +} + +tasks.processResources { + dependsOn(generateFastCheckRuntimeMetadata) +} + +val installFastCheckAdapter = tasks.register("installFastCheckAdapter") { + workingDir(fastCheckAdapterDir) + commandLine(npmExecutable, "ci", "--ignore-scripts") + inputs.files( + fastCheckAdapterPackageJson, + fastCheckAdapterPackageLock, + ) + inputs.property("runtimeClassifier", fastCheckRuntimeClassifier) + outputs.dir(fastCheckAdapterDir.dir("node_modules")) +} + +val verifyFastCheckAdapterRuntime = tasks.register("verifyFastCheckAdapterRuntime") { + dependsOn(installFastCheckAdapter) + val nativeRuntime = fastCheckAdapterDir.dir("node_modules/@esbuild/$fastCheckRuntimeClassifier") + + inputs.dir(nativeRuntime) + doLast { + check(nativeRuntime.asFile.isDirectory) { + "Missing esbuild runtime for $fastCheckRuntimeClassifier at ${nativeRuntime.asFile}" + } + } +} + +val buildFastCheckAdapter = tasks.register("buildFastCheckAdapter") { + dependsOn(verifyFastCheckAdapterRuntime) + workingDir(fastCheckAdapterDir) + commandLine(npmExecutable, "run", "build") + inputs.files( + fastCheckAdapterDir.file("package.json"), + fastCheckAdapterDir.file("package-lock.json"), + fastCheckAdapterDir.file("tsconfig.json"), + ) + inputs.dir(fastCheckAdapterDir.dir("src")) + inputs.dir(fastCheckAdapterDir.dir("test")) + outputs.dir(fastCheckAdapterDir.dir("dist")) +} + +tasks.named("distZip") { + archiveClassifier.set(fastCheckRuntimeClassifier) +} + +tasks.named("distTar") { + archiveClassifier.set(fastCheckRuntimeClassifier) +} + +val testFastCheckAdapter = tasks.register("testFastCheckAdapter") { + dependsOn(buildFastCheckAdapter) + workingDir(fastCheckAdapterDir) + commandLine(npmExecutable, "run", "test:compiled") + inputs.dir(fastCheckAdapterDir.dir("dist")) +} + +tasks.test { + dependsOn(buildFastCheckAdapter) + systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) +} + +tasks.check { + dependsOn(testFastCheckAdapter) +} + +tasks.clean { + delete(fastCheckAdapterDir.dir("dist")) +} + +application { + mainClass = "org.usvm.ts.pbt.cli.FastCheckCliKt" + applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") +} + +tasks.named("run") { + systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) +} + +distributions { + main { + contents { + into("lib/fast-check-adapter") { + from(fastCheckAdapterDir) + include("dist/src/**") + include("node_modules/**") + include("package.json") + } + } + } +} + +listOf("run", "startScripts", "installDist", "distZip", "distTar").forEach { taskName -> + tasks.named(taskName) { + dependsOn(buildFastCheckAdapter) + } +} diff --git a/usvm-ts-pbt/fast-check-adapter/.gitignore b/usvm-ts-fast-check/fast-check-adapter/.gitignore similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/.gitignore rename to usvm-ts-fast-check/fast-check-adapter/.gitignore diff --git a/usvm-ts-pbt/fast-check-adapter/package-lock.json b/usvm-ts-fast-check/fast-check-adapter/package-lock.json similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/package-lock.json rename to usvm-ts-fast-check/fast-check-adapter/package-lock.json diff --git a/usvm-ts-pbt/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/package.json rename to usvm-ts-fast-check/fast-check-adapter/package.json diff --git a/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts rename to usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts b/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/entry-point.ts rename to usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/execute-property.ts rename to usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/execution-cli.ts b/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/execution-cli.ts rename to usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/js-value.ts b/usvm-ts-fast-check/fast-check-adapter/src/js-value.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/js-value.ts rename to usvm-ts-fast-check/fast-check-adapter/src/js-value.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/process-group-shutdown.ts b/usvm-ts-fast-check/fast-check-adapter/src/process-group-shutdown.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/process-group-shutdown.ts rename to usvm-ts-fast-check/fast-check-adapter/src/process-group-shutdown.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/process-supervisor.ts b/usvm-ts-fast-check/fast-check-adapter/src/process-supervisor.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/process-supervisor.ts rename to usvm-ts-fast-check/fast-check-adapter/src/process-supervisor.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts b/usvm-ts-fast-check/fast-check-adapter/src/project-domain.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/project-domain.ts rename to usvm-ts-fast-check/fast-check-adapter/src/project-domain.ts diff --git a/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts b/usvm-ts-fast-check/fast-check-adapter/src/projection-cli.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts rename to usvm-ts-fast-check/fast-check-adapter/src/projection-cli.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/entry-point.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/entry-point.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/execution-cli.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/execution-cli.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/execution-cli.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/execution-cli.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/js-value.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/js-value.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/js-value.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/js-value.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/process-group-shutdown.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/process-group-shutdown.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/process-group-shutdown.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/process-group-shutdown.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/process-supervisor.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/process-supervisor.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/process-supervisor.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/process-supervisor.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/projection-cli.test.ts similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts rename to usvm-ts-fast-check/fast-check-adapter/test/projection-cli.test.ts diff --git a/usvm-ts-pbt/fast-check-adapter/tsconfig.json b/usvm-ts-fast-check/fast-check-adapter/tsconfig.json similarity index 100% rename from usvm-ts-pbt/fast-check-adapter/tsconfig.json rename to usvm-ts-fast-check/fast-check-adapter/tsconfig.json diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt new file mode 100644 index 0000000000..88b794cbd6 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt @@ -0,0 +1,46 @@ +package org.usvm.ts.pbt + +/** Stable identifiers for diagnostics created by the FastCheck integration. */ +internal object FastCheckDiagnosticCode { + const val CLI_ARGUMENT_INVALID = "cli.argument.invalid" + const val CLI_COVERAGE_REQUIRED = "cli.coverage.required" + const val CLI_COVERAGE_SCOPE_INVALID = "cli.coverage.scope.invalid" + const val CLI_EXAMPLES_INVALID = "cli.examples.invalid" + const val CLI_NUM_RUNS_INVALID = "cli.num-runs.invalid" + const val CLI_PROPERTY_EMPTY = "cli.property.empty" + const val CLI_PROPERTY_INVALID = "cli.property.invalid" + const val CLI_PROPERTY_UNKNOWN = "cli.property.unknown" + const val CLI_REGISTRY_EMPTY = "cli.registry.empty" + const val CLI_REGISTRY_ID_DUPLICATE = "cli.registry.id.duplicate" + const val CLI_REGISTRY_ID_INVALID = "cli.registry.id.invalid" + const val CLI_REGISTRY_UNKNOWN = "cli.registry.unknown" + const val CLI_SINGLE_PROPERTY_REQUIRED = "cli.single-property.required" + const val CLI_SOURCE_ROOT_REQUIRED = "cli.source-root.required" + const val CLI_TIMEOUT_INVALID = "cli.timeout.invalid" + + const val REGISTRY_PROPERTY_ID_DUPLICATE = "registry.property-id.duplicate" + const val REGISTRY_PROPERTY_INVALID = "registry.property.invalid" + const val REGISTRY_PROVIDER_LOAD_FAILED = "registry.provider.load.failed" + + const val BACKEND_EXAMPLES_ARITY = "backend.examples.arity" + const val BACKEND_EXAMPLES_DOMAIN = "backend.examples.domain" + const val BACKEND_EXAMPLES_VALUE_INVALID = "backend.examples.value.invalid" + const val BACKEND_PROCESS_FAILED = "backend.process.failed" + const val BACKEND_PROCESS_INTERRUPTED = "backend.process.interrupted" + const val BACKEND_PROCESS_READ_FAILED = "backend.process.read.failed" + const val BACKEND_PROCESS_START_FAILED = "backend.process.start.failed" + const val BACKEND_PROCESS_TIMEOUT = "backend.process.timeout" + const val BACKEND_PROCESS_WRITE_FAILED = "backend.process.write.failed" + const val BACKEND_REQUEST_TOO_LARGE = "backend.request.too-large" + const val BACKEND_RESPONSE_EMPTY = "backend.response.empty" + const val BACKEND_RESPONSE_INVALID = "backend.response.invalid" + const val BACKEND_RESPONSE_TOO_LARGE = "backend.response.too-large" + const val BACKEND_RUNTIME_NOT_FOUND = "backend.runtime.not-found" + + const val COVERAGE_COLLECTOR_NOT_FOUND = "coverage.collector.not-found" + const val COVERAGE_RUNTIME_UNSUPPORTED = "coverage.runtime.unsupported" + const val COVERAGE_RUNTIME_VERSION_UNAVAILABLE = "coverage.runtime.version-unavailable" + + const val PROTOCOL_REQUEST_INVALID = "protocol.request.invalid" + const val SOURCE_ROOT_INVALID = "source-root.invalid" +} diff --git a/usvm-ts-pbt/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 similarity index 92% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt index 198ab3d74b..00a80ff686 100644 --- a/usvm-ts-pbt/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 @@ -4,7 +4,7 @@ import kotlinx.serialization.Serializable import kotlinx.serialization.SerializationException import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString -import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.CoverageCapabilityLevel import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend import org.usvm.ts.pbt.backend.PropertyRunConfiguration @@ -55,7 +55,7 @@ class FastCheckCli( EXIT_ERROR } catch (error: DuplicatePropertyIdException) { reportError( - code = PbtDiagnosticCode.REGISTRY_PROPERTY_ID_DUPLICATE, + code = FastCheckDiagnosticCode.REGISTRY_PROPERTY_ID_DUPLICATE, message = error.message.orEmpty(), path = "properties", propertyId = error.propertyId.value, @@ -64,7 +64,7 @@ class FastCheckCli( EXIT_ERROR } catch (error: UnknownPropertyIdException) { reportError( - code = PbtDiagnosticCode.CLI_PROPERTY_UNKNOWN, + code = FastCheckDiagnosticCode.CLI_PROPERTY_UNKNOWN, message = error.message.orEmpty(), path = "property", propertyId = error.propertyId.value, @@ -73,7 +73,7 @@ class FastCheckCli( EXIT_ERROR } catch (error: InvalidPropertyDefinitionException) { reportError( - code = PbtDiagnosticCode.REGISTRY_PROPERTY_INVALID, + code = FastCheckDiagnosticCode.REGISTRY_PROPERTY_INVALID, message = error.message.orEmpty(), path = error.result.diagnostics.firstOrNull()?.path, ) @@ -91,7 +91,7 @@ class FastCheckCli( EXIT_ERROR } catch (error: ServiceConfigurationError) { reportError( - code = PbtDiagnosticCode.REGISTRY_PROVIDER_LOAD_FAILED, + code = FastCheckDiagnosticCode.REGISTRY_PROVIDER_LOAD_FAILED, message = error.message.orEmpty(), path = "registry", ) @@ -99,7 +99,7 @@ class FastCheckCli( EXIT_ERROR } catch (error: IllegalArgumentException) { reportError( - code = PbtDiagnosticCode.CLI_ARGUMENT_INVALID, + code = FastCheckDiagnosticCode.CLI_ARGUMENT_INVALID, message = error.message.orEmpty(), ) @@ -164,7 +164,7 @@ class FastCheckCli( val properties = registry.properties if (properties.isEmpty()) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_PROPERTY_EMPTY, + code = FastCheckDiagnosticCode.CLI_PROPERTY_EMPTY, message = "Selected registries contain no properties", path = "registry", ) @@ -191,7 +191,7 @@ class FastCheckCli( if (usesRunScopedControls && propertyCount != 1) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_SINGLE_PROPERTY_REQUIRED, + code = FastCheckDiagnosticCode.CLI_SINGLE_PROPERTY_REQUIRED, message = "Replay paths and explicit examples require exactly one selected property", path = "property", ) @@ -210,7 +210,7 @@ class FastCheckCli( if (unknown != null) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_REGISTRY_UNKNOWN, + code = FastCheckDiagnosticCode.CLI_REGISTRY_UNKNOWN, message = "Unknown registry ID $unknown; available IDs: ${availableIds.sorted().joinToString()}", path = "registry", ) @@ -227,7 +227,7 @@ class FastCheckCli( if (orderedProviders.isEmpty()) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_REGISTRY_EMPTY, + code = FastCheckDiagnosticCode.CLI_REGISTRY_EMPTY, message = "No PropertyRegistryProvider services were found", path = "registry", ) @@ -239,7 +239,7 @@ class FastCheckCli( private fun validateProviderId(providerId: String) { if (!REGISTRY_ID_REGEX.matches(providerId)) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_REGISTRY_ID_INVALID, + code = FastCheckDiagnosticCode.CLI_REGISTRY_ID_INVALID, message = "Invalid registry ID: $providerId", path = "registry", ) @@ -255,7 +255,7 @@ class FastCheckCli( if (duplicateRegistryId != null) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_REGISTRY_ID_DUPLICATE, + code = FastCheckDiagnosticCode.CLI_REGISTRY_ID_DUPLICATE, message = "Duplicate registry ID: $duplicateRegistryId", path = "registry", ) @@ -275,7 +275,7 @@ class FastCheckCli( } private fun providerFailure(providerName: String, cause: Throwable) = CliUsageException( - code = PbtDiagnosticCode.REGISTRY_PROVIDER_LOAD_FAILED, + code = FastCheckDiagnosticCode.REGISTRY_PROVIDER_LOAD_FAILED, message = "Property registry provider $providerName failed: ${cause.message}", path = "registry", cause = cause, @@ -290,7 +290,7 @@ class FastCheckCli( } private fun invalidExamples(path: Path, cause: Exception) = CliUsageException( - code = PbtDiagnosticCode.CLI_EXAMPLES_INVALID, + code = FastCheckDiagnosticCode.CLI_EXAMPLES_INVALID, message = "Cannot read explicit examples from $path: ${cause.message}", path = "examples", cause = cause, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt similarity index 92% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt index 5df77fcf52..56be2a4cc0 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt @@ -11,7 +11,7 @@ import com.github.ajalt.clikt.parameters.options.option import com.github.ajalt.clikt.parameters.types.int import com.github.ajalt.clikt.parameters.types.long import com.github.ajalt.clikt.parameters.types.path -import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.CoverageScope import org.usvm.ts.pbt.backend.PropertyCoverageRequest import org.usvm.ts.pbt.backend.PropertyRunConfiguration @@ -54,14 +54,14 @@ internal fun parseCliOptions(args: Array): CliParseResult { CliParseResult.Help(parser.getFormattedHelp(help).orEmpty()) } catch (error: CliktError) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_ARGUMENT_INVALID, + code = FastCheckDiagnosticCode.CLI_ARGUMENT_INVALID, message = error.message ?: "Invalid command line arguments", cause = error, ) } } -private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-pbt") { +private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") { private val sourceRoots by option( "--source-root", help = "TypeScript source root; repeat for multiple roots", @@ -146,7 +146,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-pbt") { private fun requireSourceRoots() { if (sourceRoots.isEmpty()) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_SOURCE_ROOT_REQUIRED, + code = FastCheckDiagnosticCode.CLI_SOURCE_ROOT_REQUIRED, message = "At least one --source-root is required", path = "sourceRoot", ) @@ -156,7 +156,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-pbt") { private fun requirePositiveRunControls() { if (numRuns <= 0) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_NUM_RUNS_INVALID, + code = FastCheckDiagnosticCode.CLI_NUM_RUNS_INVALID, message = "--num-runs must be positive", path = "numRuns", ) @@ -164,7 +164,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-pbt") { if (timeoutMillis !in 1..PropertyRunConfiguration.MAX_TIMEOUT_MILLIS) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_TIMEOUT_INVALID, + code = FastCheckDiagnosticCode.CLI_TIMEOUT_INVALID, message = "--timeout-ms must be in 1..${PropertyRunConfiguration.MAX_TIMEOUT_MILLIS}", path = "timeoutMillis", ) @@ -177,7 +177,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-pbt") { coverageExcludePatterns.isNotEmpty() if (!coverageEnabled && hasCoverageDetails) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_COVERAGE_REQUIRED, + code = FastCheckDiagnosticCode.CLI_COVERAGE_REQUIRED, message = "Coverage scope and path rules require --coverage", path = "coverage", ) @@ -205,7 +205,7 @@ private fun parseCoverageScope(value: String): CoverageScope = when (value) { "generated-backend-wrappers" -> CoverageScope.GENERATED_BACKEND_WRAPPERS "dependencies" -> CoverageScope.DEPENDENCIES else -> throw CliUsageException( - code = PbtDiagnosticCode.CLI_COVERAGE_SCOPE_INVALID, + code = FastCheckDiagnosticCode.CLI_COVERAGE_SCOPE_INVALID, message = "Unknown coverage scope $value", path = "coverageScope", ) @@ -215,7 +215,7 @@ private fun parsePropertyId(value: String): PropertyId = try { PropertyId(value) } catch (error: IllegalArgumentException) { throw CliUsageException( - code = PbtDiagnosticCode.CLI_PROPERTY_INVALID, + code = FastCheckDiagnosticCode.CLI_PROPERTY_INVALID, message = error.message.orEmpty(), path = "property", cause = error, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt similarity index 92% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index a1afb8c29a..7b2d95510d 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt @@ -1,6 +1,6 @@ package org.usvm.ts.pbt.fastcheck -import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend import org.usvm.ts.pbt.backend.PropertyCoverageCapability import org.usvm.ts.pbt.backend.PropertyRunConfiguration @@ -71,7 +71,7 @@ class FastCheckBackend( configuration.examples.forEachIndexed { index, example -> if (example.size != property.inputs.size) { throw invalidRequest( - code = PbtDiagnosticCode.BACKEND_EXAMPLES_ARITY, + code = FastCheckDiagnosticCode.BACKEND_EXAMPLES_ARITY, message = "Explicit example $index has ${example.size} values, expected ${property.inputs.size}", property = property, path = "examples[$index]", @@ -89,7 +89,7 @@ class FastCheckBackend( if (value !in property.inputs[valueIndex].domain) { throw invalidRequest( - code = PbtDiagnosticCode.BACKEND_EXAMPLES_DOMAIN, + code = FastCheckDiagnosticCode.BACKEND_EXAMPLES_DOMAIN, message = "Explicit example does not belong to the declared input domain", property = property, path = path, @@ -106,7 +106,7 @@ class FastCheckBackend( ) { if (value is JsConcreteValue.Number && !hasValidEncoding(value)) { throw invalidRequest( - code = PbtDiagnosticCode.BACKEND_EXAMPLES_VALUE_INVALID, + code = FastCheckDiagnosticCode.BACKEND_EXAMPLES_VALUE_INVALID, message = "Explicit example contains an invalid tagged JavaScript number", property = property, path = path, @@ -151,7 +151,7 @@ class FastCheckBackend( if (sourceRoots.isEmpty()) { throw PbtBackendException( kind = BackendErrorKind.INVALID_REQUEST, - code = PbtDiagnosticCode.SOURCE_ROOT_INVALID, + code = FastCheckDiagnosticCode.SOURCE_ROOT_INVALID, message = "At least one TypeScript source root is required", path = "sourceRoots", ) @@ -165,7 +165,7 @@ class FastCheckBackend( if (!Files.isDirectory(realPath)) { throw PbtBackendException( kind = BackendErrorKind.INVALID_REQUEST, - code = PbtDiagnosticCode.SOURCE_ROOT_INVALID, + code = FastCheckDiagnosticCode.SOURCE_ROOT_INVALID, message = "TypeScript source root is not a directory: $sourceRoot", path = "sourceRoots[$index]", ) @@ -174,7 +174,7 @@ class FastCheckBackend( } catch (error: IOException) { throw PbtBackendException( kind = BackendErrorKind.INVALID_REQUEST, - code = PbtDiagnosticCode.SOURCE_ROOT_INVALID, + code = FastCheckDiagnosticCode.SOURCE_ROOT_INVALID, message = "Cannot resolve TypeScript source root $sourceRoot: ${error.message}", path = "sourceRoots[$index]", cause = error, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt similarity index 93% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt index 2191f3f42d..d4567c9f77 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt @@ -1,6 +1,6 @@ package org.usvm.ts.pbt.fastcheck -import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.CoverageScope import org.usvm.ts.pbt.backend.PropertyRunResult import org.usvm.ts.pbt.coverage.CoverageArtifactException @@ -130,7 +130,7 @@ internal class FastCheckCoverageSession private constructor( if (!Files.isRegularFile(c8EntryPoint)) { failPreparation( request = request, - code = PbtDiagnosticCode.COVERAGE_COLLECTOR_NOT_FOUND, + code = FastCheckDiagnosticCode.COVERAGE_COLLECTOR_NOT_FOUND, message = "Cannot locate c8 ${FastCheckRuntimeMetadata.coverageCollector.version} " + "in the fast-check adapter runtime", path = c8EntryPoint.toString(), @@ -149,7 +149,7 @@ internal class FastCheckCoverageSession private constructor( } private fun createWorkspace(c8EntryPoint: Path, adapterRoot: Path): CoverageWorkspace { - val root = Files.createTempDirectory("usvm-ts-pbt-coverage-") + val root = Files.createTempDirectory("usvm-ts-fast-check-coverage-") try { val configPath = Files.writeString(root.resolve("c8-config.json"), "{}") @@ -177,7 +177,7 @@ internal class FastCheckCoverageSession private constructor( } catch (error: IOException) { failPreparation( request = request, - code = PbtDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, + code = FastCheckDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, message = "Cannot query the Node.js runtime version: ${error.message}", cause = error, ) @@ -191,7 +191,7 @@ internal class FastCheckCoverageSession private constructor( if (process.exitValue() != 0 || version.isBlank()) { failPreparation( request = request, - code = PbtDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, + code = FastCheckDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, message = "Cannot query the Node.js runtime version", ) } @@ -211,7 +211,7 @@ internal class FastCheckCoverageSession private constructor( Thread.currentThread().interrupt() failPreparation( request = request, - code = PbtDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, message = "Interrupted while querying the Node.js runtime version", kind = BackendErrorKind.PROCESS_FAILURE, cause = error, @@ -221,7 +221,7 @@ internal class FastCheckCoverageSession private constructor( process.destroyForcibly() failPreparation( request = request, - code = PbtDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, + code = FastCheckDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, message = "Timed out while querying the Node.js runtime version", ) } @@ -234,7 +234,7 @@ internal class FastCheckCoverageSession private constructor( if (major == null || minor == null) { failPreparation( request = request, - code = PbtDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, + code = FastCheckDiagnosticCode.COVERAGE_RUNTIME_VERSION_UNAVAILABLE, message = "Cannot parse the Node.js runtime version: $version", ) } @@ -245,7 +245,7 @@ internal class FastCheckCoverageSession private constructor( if (!supported) { failPreparation( request = request, - code = PbtDiagnosticCode.COVERAGE_RUNTIME_UNSUPPORTED, + code = FastCheckDiagnosticCode.COVERAGE_RUNTIME_UNSUPPORTED, message = "Coverage requires Node.js 18.18 or newer; found $version", ) } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt similarity index 100% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt diff --git a/usvm-ts-pbt/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 similarity index 91% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt index ff759dc98b..43d3980eed 100644 --- a/usvm-ts-pbt/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 @@ -2,7 +2,7 @@ package org.usvm.ts.pbt.fastcheck import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString -import org.usvm.ts.pbt.PbtDiagnosticCode +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 @@ -79,7 +79,7 @@ internal class FastCheckProcessClient( if (encodedRequest.toByteArray(Charsets.UTF_8).size > MAX_REQUEST_BYTES) { throw backendError( kind = BackendErrorKind.INVALID_REQUEST, - code = PbtDiagnosticCode.BACKEND_REQUEST_TOO_LARGE, + code = FastCheckDiagnosticCode.BACKEND_REQUEST_TOO_LARGE, message = "fast-check request exceeds $MAX_REQUEST_BYTES bytes", request = request, ) @@ -97,7 +97,7 @@ internal class FastCheckProcessClient( throw backendError( kind = BackendErrorKind.PROCESS_FAILURE, - code = PbtDiagnosticCode.BACKEND_PROCESS_FAILED, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_FAILED, message = "fast-check adapter exited with code ${output.exitCode}: $detail", request = request, ) @@ -106,7 +106,7 @@ internal class FastCheckProcessClient( if (output.stdout.isBlank()) { throw backendError( kind = BackendErrorKind.PROTOCOL_ERROR, - code = PbtDiagnosticCode.BACKEND_RESPONSE_EMPTY, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_EMPTY, message = "fast-check adapter returned an empty response", request = request, ) @@ -121,7 +121,7 @@ internal class FastCheckProcessClient( } catch (error: IllegalArgumentException) { throw backendError( kind = BackendErrorKind.PROTOCOL_ERROR, - code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_INVALID, message = "fast-check adapter returned invalid JSON: ${error.message}", request = request, cause = error, @@ -179,7 +179,7 @@ internal class FastCheckProcessClient( } catch (error: IllegalArgumentException) { throw backendError( kind = BackendErrorKind.PROTOCOL_ERROR, - code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_INVALID, message = "fast-check result property ID is invalid: ${error.message}", request = request, cause = error, @@ -199,7 +199,7 @@ internal class FastCheckProcessClient( request: FastCheckExecutionRequest, ): PbtBackendException = backendError( kind = BackendErrorKind.PROTOCOL_ERROR, - code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_INVALID, message = message, request = request, ) @@ -230,8 +230,8 @@ internal class FastCheckProcessClient( } private fun FastCheckTransportException.backendErrorKind(): BackendErrorKind = when (code) { - PbtDiagnosticCode.BACKEND_REQUEST_TOO_LARGE -> BackendErrorKind.INVALID_REQUEST - PbtDiagnosticCode.BACKEND_RESPONSE_TOO_LARGE -> BackendErrorKind.PROTOCOL_ERROR - PbtDiagnosticCode.BACKEND_PROCESS_TIMEOUT -> BackendErrorKind.TIMEOUT + FastCheckDiagnosticCode.BACKEND_REQUEST_TOO_LARGE -> BackendErrorKind.INVALID_REQUEST + FastCheckDiagnosticCode.BACKEND_RESPONSE_TOO_LARGE -> BackendErrorKind.PROTOCOL_ERROR + FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT -> BackendErrorKind.TIMEOUT else -> BackendErrorKind.PROCESS_FAILURE } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt similarity index 95% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt index f7b2be7d56..fa2cb7205f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessTransport.kt @@ -1,6 +1,6 @@ package org.usvm.ts.pbt.fastcheck -import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.FastCheckDiagnosticCode import java.io.ByteArrayOutputStream import java.io.IOException import java.io.InputStream @@ -99,7 +99,7 @@ internal class FastCheckProcessTransport( private fun requireRequestWithinLimit(request: String, description: String) { if (request.toByteArray(Charsets.UTF_8).size > maxRequestBytes) { fail( - code = PbtDiagnosticCode.BACKEND_REQUEST_TOO_LARGE, + code = FastCheckDiagnosticCode.BACKEND_REQUEST_TOO_LARGE, message = "$description request exceeds $maxRequestBytes bytes", ) } @@ -116,14 +116,14 @@ internal class FastCheckProcessTransport( process.inputStream.readBounded(maxStdoutBytes, stream = "stdout") }, operation = "reading $description stdout", - failureCode = PbtDiagnosticCode.BACKEND_PROCESS_READ_FAILED, + failureCode = FastCheckDiagnosticCode.BACKEND_PROCESS_READ_FAILED, ) val stderr = ProcessIoTask( future = executor.submit { process.errorStream.readBounded(maxStderrBytes, stream = "stderr") }, operation = "reading $description stderr", - failureCode = PbtDiagnosticCode.BACKEND_PROCESS_READ_FAILED, + failureCode = FastCheckDiagnosticCode.BACKEND_PROCESS_READ_FAILED, ) val writer = ProcessIoTask( future = executor.submit { @@ -132,7 +132,7 @@ internal class FastCheckProcessTransport( } }, operation = "writing the $description request", - failureCode = PbtDiagnosticCode.BACKEND_PROCESS_WRITE_FAILED, + failureCode = FastCheckDiagnosticCode.BACKEND_PROCESS_WRITE_FAILED, ) return ProcessIoTasks(stdout = stdout, stderr = stderr, writer = writer) @@ -158,7 +158,7 @@ internal class FastCheckProcessTransport( } catch (error: InterruptedException) { Thread.currentThread().interrupt() fail( - code = PbtDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, message = "Interrupted while waiting for the $description", cause = error, ) @@ -221,7 +221,7 @@ internal class FastCheckProcessTransport( } private fun processStartFailure(description: String, error: IOException): Nothing = fail( - code = PbtDiagnosticCode.BACKEND_PROCESS_START_FAILED, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_START_FAILED, message = "Failed to start $description: ${error.message}", cause = error, ) @@ -296,7 +296,7 @@ internal class FastCheckProcessTransport( } private fun timeout(description: String, reportedTimeoutMillis: Long): Nothing = fail( - code = PbtDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, message = "$description exceeded the $reportedTimeoutMillis ms timeout", ) @@ -354,7 +354,7 @@ private data class ProcessIoTask( } catch (error: InterruptedException) { Thread.currentThread().interrupt() throw FastCheckTransportException( - code = PbtDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, message = "Interrupted while $operation", cause = error, ) @@ -362,7 +362,7 @@ private data class ProcessIoTask( val cause = error.cause ?: error if (cause is ProcessOutputLimitExceeded) { throw FastCheckTransportException( - code = PbtDiagnosticCode.BACKEND_RESPONSE_TOO_LARGE, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_TOO_LARGE, message = "$description ${cause.stream} exceeds ${cause.limit} bytes", cause = cause, ) diff --git a/usvm-ts-pbt/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 similarity index 95% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt index b74c86c49f..c00614d8d4 100644 --- a/usvm-ts-pbt/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 @@ -2,7 +2,7 @@ package org.usvm.ts.pbt.fastcheck import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString -import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.manifest.PropertyManifestJson import org.usvm.ts.pbt.model.contains import java.nio.file.Path @@ -93,12 +93,12 @@ class FastCheckProjectionClient private constructor( private fun processFailure(output: FastCheckProcessOutput): Nothing = throw FastCheckProjectionException( - code = PbtDiagnosticCode.BACKEND_PROCESS_FAILED, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_FAILED, message = "fast-check adapter exited with code ${output.exitCode}: ${output.stderr.trim()}", ) private fun emptyResponse(): Nothing = throw FastCheckProjectionException( - code = PbtDiagnosticCode.BACKEND_RESPONSE_EMPTY, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_EMPTY, message = "fast-check adapter returned an empty response", ) @@ -106,7 +106,7 @@ class FastCheckProjectionClient private constructor( PropertyManifestJson.json.decodeFromString(stdout) } catch (error: IllegalArgumentException) { throw FastCheckProjectionException( - code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_INVALID, message = "fast-check adapter returned invalid JSON: ${error.message}", cause = error, ) @@ -152,7 +152,7 @@ class FastCheckProjectionClient private constructor( private fun validateRequest(request: FastCheckProjectionRequest) { if (request.numSamples !in 1..MAX_SAMPLES || request.domains.isEmpty()) { throw FastCheckProjectionException( - code = PbtDiagnosticCode.PROTOCOL_REQUEST_INVALID, + code = FastCheckDiagnosticCode.PROTOCOL_REQUEST_INVALID, message = "Request requires domains and numSamples in 1..$MAX_SAMPLES", path = "request", ) @@ -161,7 +161,7 @@ class FastCheckProjectionClient private constructor( private fun invalidResponse(message: String, path: String? = null): Nothing = throw FastCheckProjectionException( - code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + code = FastCheckDiagnosticCode.BACKEND_RESPONSE_INVALID, message = message, path = path, ) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt similarity index 100% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt similarity index 94% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt index 860a04f579..c193295000 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt @@ -1,6 +1,6 @@ package org.usvm.ts.pbt.fastcheck -import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.FastCheckDiagnosticCode import java.nio.file.Files import java.nio.file.Path @@ -20,7 +20,7 @@ internal object FastCheckRuntime { return candidates.firstOrNull(Files::isRegularFile) ?: throw PbtBackendException( kind = BackendErrorKind.INVALID_REQUEST, - code = PbtDiagnosticCode.BACKEND_RUNTIME_NOT_FOUND, + code = FastCheckDiagnosticCode.BACKEND_RUNTIME_NOT_FOUND, message = "Cannot locate built fast-check adapter; checked $candidates", ) } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadata.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadata.kt similarity index 100% rename from usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadata.kt rename to usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadata.kt diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/TestResources.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/TestResources.kt new file mode 100644 index 0000000000..82542885a0 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/TestResources.kt @@ -0,0 +1,17 @@ +package org.usvm.ts.pbt + +import java.nio.file.Path + +internal fun testResourcePath(name: String): Path { + val resource = requireNotNull(TestResourceMarker::class.java.getResource(name)) { + "Missing test resource: $name" + } + + require(resource.protocol == "file") { "Test resource is not a regular file-system path: $resource" } + + return Path.of(resource.toURI()) +} + +internal fun testResourcesRoot(): Path = requireNotNull(testResourcePath("/properties").parent) + +private object TestResourceMarker diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/FastCheckCliTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/FastCheckCliTest.kt similarity index 100% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/FastCheckCliTest.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/FastCheckCliTest.kt diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/InstalledDistributionRegistryProvider.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/InstalledDistributionRegistryProvider.kt similarity index 100% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/InstalledDistributionRegistryProvider.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/InstalledDistributionRegistryProvider.kt diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt similarity index 100% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackendTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackendTest.kt similarity index 100% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackendTest.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackendTest.kt diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt similarity index 98% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt index 14cef79ef6..cfcfa58d4d 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt @@ -206,12 +206,12 @@ class FastCheckCoverageTest { fun adapterEntryPoint(): Path = locateFile( "fast-check-adapter/dist/src/execution-cli.js", - "usvm-ts-pbt/fast-check-adapter/dist/src/execution-cli.js", + "usvm-ts-fast-check/fast-check-adapter/dist/src/execution-cli.js", ) fun sourceRoot(): Path = locateDirectory( "src/test/resources", - "usvm-ts-pbt/src/test/resources", + "usvm-ts-fast-check/src/test/resources", ) fun locateFile(vararg candidates: String): Path = candidates diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt similarity index 99% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt index 2d7addcfba..08220b6ff1 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt @@ -394,7 +394,7 @@ class FastCheckProcessClientTest { private fun coverageWorkspaces(): Set { val temporaryRoot = Path.of(System.getProperty("java.io.tmpdir")) - return Files.newDirectoryStream(temporaryRoot, "usvm-ts-pbt-coverage-*").use { entries -> + return Files.newDirectoryStream(temporaryRoot, "usvm-ts-fast-check-coverage-*").use { entries -> entries.toHashSet() } } diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt similarity index 100% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadataTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadataTest.kt similarity index 100% rename from usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadataTest.kt rename to usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntimeMetadataTest.kt diff --git a/usvm-ts-pbt/src/test/resources/META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider b/usvm-ts-fast-check/src/test/resources/META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider similarity index 100% rename from usvm-ts-pbt/src/test/resources/META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider rename to usvm-ts-fast-check/src/test/resources/META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider diff --git a/usvm-ts-pbt/src/test/resources/properties/coverage/CoverageProperties.ts b/usvm-ts-fast-check/src/test/resources/properties/coverage/CoverageProperties.ts similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/coverage/CoverageProperties.ts rename to usvm-ts-fast-check/src/test/resources/properties/coverage/CoverageProperties.ts diff --git a/usvm-ts-pbt/src/test/resources/properties/coverage/invalid-map-entry.js b/usvm-ts-fast-check/src/test/resources/properties/coverage/invalid-map-entry.js similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/coverage/invalid-map-entry.js rename to usvm-ts-fast-check/src/test/resources/properties/coverage/invalid-map-entry.js diff --git a/usvm-ts-pbt/src/test/resources/properties/coverage/invalid-map-entry.js.map b/usvm-ts-fast-check/src/test/resources/properties/coverage/invalid-map-entry.js.map similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/coverage/invalid-map-entry.js.map rename to usvm-ts-fast-check/src/test/resources/properties/coverage/invalid-map-entry.js.map diff --git a/usvm-ts-pbt/src/test/resources/properties/coverage/missing-map-entry.js b/usvm-ts-fast-check/src/test/resources/properties/coverage/missing-map-entry.js similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/coverage/missing-map-entry.js rename to usvm-ts-fast-check/src/test/resources/properties/coverage/missing-map-entry.js diff --git a/usvm-ts-pbt/src/test/resources/properties/coverage/package.json b/usvm-ts-fast-check/src/test/resources/properties/coverage/package.json similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/coverage/package.json rename to usvm-ts-fast-check/src/test/resources/properties/coverage/package.json diff --git a/usvm-ts-pbt/src/test/resources/properties/coverage/source-under-test.ts b/usvm-ts-fast-check/src/test/resources/properties/coverage/source-under-test.ts similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/coverage/source-under-test.ts rename to usvm-ts-fast-check/src/test/resources/properties/coverage/source-under-test.ts diff --git a/usvm-ts-pbt/src/test/resources/properties/examples/PropertyExamples.ts b/usvm-ts-fast-check/src/test/resources/properties/examples/PropertyExamples.ts similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/examples/PropertyExamples.ts rename to usvm-ts-fast-check/src/test/resources/properties/examples/PropertyExamples.ts diff --git a/usvm-ts-pbt/src/test/resources/properties/execution/ExecutionProperties.ts b/usvm-ts-fast-check/src/test/resources/properties/execution/ExecutionProperties.ts similarity index 100% rename from usvm-ts-pbt/src/test/resources/properties/execution/ExecutionProperties.ts rename to usvm-ts-fast-check/src/test/resources/properties/execution/ExecutionProperties.ts diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index 5f01f441a0..41c70656c5 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -1,10 +1,11 @@ # USVM TypeScript property-based testing -`usvm-ts-pbt` is the Kotlin-owned integration layer for concrete property-based testing backends and USVM. -Kotlin defines each property once; fast-check is the first concrete backend. +`usvm-ts-pbt` is the backend-neutral Kotlin layer between property-based testing backends and USVM. It owns the +property model, validation, registries, coverage contracts and decoders, and property-to-EtsIR mapping. The first +concrete backend lives in [`usvm-ts-fast-check`](../usvm-ts-fast-check/README.md). -See [DESIGN.md](DESIGN.md) for component responsibilities, Kotlin–TypeScript data flow, process supervision, and -runtime packaging. +See [`usvm-ts-fast-check/DESIGN.md`](../usvm-ts-fast-check/DESIGN.md) for the FastCheck process boundary and runtime +packaging. ## Kotlin property model @@ -219,7 +220,7 @@ Register the provider in provider JAR on the application classpath, then run: ```shell -java -cp '/opt/usvm-ts-pbt/lib/*:/workspace/example-properties.jar' \ +java -cp '/opt/usvm-ts-fast-check/lib/*:/workspace/example-properties.jar' \ org.usvm.ts.pbt.cli.FastCheckCliKt \ --source-root /workspace/packages/core/src \ --registry example \ @@ -248,11 +249,11 @@ Requires JDK 11, Node.js 18.18 or newer, npm, and the repository Gradle wrapper. The private distribution pins c8 10.1.3 because it supports the module's Node 18 floor. ```shell -npm ci --prefix usvm-ts-pbt/fast-check-adapter --ignore-scripts -npm test --prefix usvm-ts-pbt/fast-check-adapter +npm ci --prefix usvm-ts-fast-check/fast-check-adapter --ignore-scripts +npm test --prefix usvm-ts-fast-check/fast-check-adapter env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ - ./gradlew --no-daemon :usvm-ts-pbt:check + ./gradlew --no-daemon :usvm-ts-pbt:check :usvm-ts-fast-check:check ``` To substitute a local JacoDB checkout, add `-PuseLocalJacodb=/absolute/path/to/jacodb` to the Gradle command. diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts index afc82d9f47..1197ec28fa 100644 --- a/usvm-ts-pbt/build.gradle.kts +++ b/usvm-ts-pbt/build.gradle.kts @@ -1,172 +1,12 @@ -import groovy.json.JsonSlurper - plugins { id("usvm.kotlin-conventions") kotlin("plugin.serialization") version Versions.kotlin - application } dependencies { implementation(project(":usvm-ts")) implementation(Libs.jacodb_ets) - implementation(Libs.clikt) implementation(Libs.kotlinx_serialization_json) testImplementation(Libs.logback) } - -val fastCheckAdapterDir = layout.projectDirectory.dir("fast-check-adapter") -val fastCheckAdapterPackageJson = fastCheckAdapterDir.file("package.json") -val fastCheckAdapterPackageLock = fastCheckAdapterDir.file("package-lock.json") -val fastCheckRuntimeProperty = "org.usvm.ts.pbt.fastcheck.runtime" -val generatedFastCheckRuntimeMetadataDirectory = layout.buildDirectory.dir( - "generated/resources/fastCheckRuntimeMetadata", -) -val hostOperatingSystem = System.getProperty("os.name").lowercase() -val hostPlatform = when { - hostOperatingSystem.contains("mac") -> "darwin" - hostOperatingSystem.contains("linux") -> "linux" - hostOperatingSystem.contains("windows") -> "win32" - else -> error("Unsupported fast-check runtime operating system: $hostOperatingSystem") -} -val hostArchitecture = when (val architecture = System.getProperty("os.arch").lowercase()) { - "aarch64", "arm64" -> "arm64" - "amd64", "x86_64" -> "x64" - "x86", "i386", "i686" -> "ia32" - else -> error("Unsupported fast-check runtime architecture: $architecture") -} -val fastCheckRuntimeClassifier = "$hostPlatform-$hostArchitecture" -val npmExecutable = if (hostPlatform == "win32") "npm.cmd" else "npm" - -val generateFastCheckRuntimeMetadata = tasks.register("generateFastCheckRuntimeMetadata") { - inputs.file(fastCheckAdapterPackageLock) - outputs.dir(generatedFastCheckRuntimeMetadataDirectory) - - doLast { - val packageLock = JsonSlurper().parse(fastCheckAdapterPackageLock.asFile) as? Map<*, *> - ?: error("Invalid fast-check adapter package lock") - val packages = packageLock["packages"] as? Map<*, *> - ?: error("Missing packages in fast-check adapter package lock") - fun dependencyVersion(dependency: String): String { - val metadata = packages["node_modules/$dependency"] as? Map<*, *> - ?: error("Missing locked fast-check adapter dependency: $dependency") - - return (metadata["version"] as? String) - ?.takeIf(String::isNotBlank) - ?: error("Missing locked fast-check adapter dependency version: $dependency") - } - - val metadataFile = generatedFastCheckRuntimeMetadataDirectory.get() - .file("org/usvm/ts/pbt/fastcheck/runtime-dependencies.properties") - .asFile - metadataFile.parentFile.mkdirs() - metadataFile.writeText( - """ - fast-check.version=${dependencyVersion("fast-check")} - c8.version=${dependencyVersion("c8")} - """.trimIndent() + "\n", - Charsets.UTF_8, - ) - } -} - -sourceSets.main { - resources.srcDir(generatedFastCheckRuntimeMetadataDirectory) -} - -tasks.processResources { - dependsOn(generateFastCheckRuntimeMetadata) -} - -val installFastCheckAdapter = tasks.register("installFastCheckAdapter") { - workingDir(fastCheckAdapterDir) - commandLine(npmExecutable, "ci", "--ignore-scripts") - inputs.files( - fastCheckAdapterPackageJson, - fastCheckAdapterPackageLock, - ) - inputs.property("runtimeClassifier", fastCheckRuntimeClassifier) - outputs.dir(fastCheckAdapterDir.dir("node_modules")) -} - -val verifyFastCheckAdapterRuntime = tasks.register("verifyFastCheckAdapterRuntime") { - dependsOn(installFastCheckAdapter) - val nativeRuntime = fastCheckAdapterDir.dir("node_modules/@esbuild/$fastCheckRuntimeClassifier") - - inputs.dir(nativeRuntime) - doLast { - check(nativeRuntime.asFile.isDirectory) { - "Missing esbuild runtime for $fastCheckRuntimeClassifier at ${nativeRuntime.asFile}" - } - } -} - -val buildFastCheckAdapter = tasks.register("buildFastCheckAdapter") { - dependsOn(verifyFastCheckAdapterRuntime) - workingDir(fastCheckAdapterDir) - commandLine(npmExecutable, "run", "build") - inputs.files( - fastCheckAdapterDir.file("package.json"), - fastCheckAdapterDir.file("package-lock.json"), - fastCheckAdapterDir.file("tsconfig.json"), - ) - inputs.dir(fastCheckAdapterDir.dir("src")) - inputs.dir(fastCheckAdapterDir.dir("test")) - outputs.dir(fastCheckAdapterDir.dir("dist")) -} - -tasks.named("distZip") { - archiveClassifier.set(fastCheckRuntimeClassifier) -} - -tasks.named("distTar") { - archiveClassifier.set(fastCheckRuntimeClassifier) -} - -val testFastCheckAdapter = tasks.register("testFastCheckAdapter") { - dependsOn(buildFastCheckAdapter) - workingDir(fastCheckAdapterDir) - commandLine(npmExecutable, "run", "test:compiled") - inputs.dir(fastCheckAdapterDir.dir("dist")) -} - -tasks.test { - dependsOn(buildFastCheckAdapter) - systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) -} - -tasks.check { - dependsOn(testFastCheckAdapter) -} - -tasks.clean { - delete(fastCheckAdapterDir.dir("dist")) -} - -application { - mainClass = "org.usvm.ts.pbt.cli.FastCheckCliKt" - applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") -} - -tasks.named("run") { - systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) -} - -distributions { - main { - contents { - into("lib/fast-check-adapter") { - from(fastCheckAdapterDir) - include("dist/src/**") - include("node_modules/**") - include("package.json") - } - } - } -} - -listOf("run", "startScripts", "installDist", "distZip", "distTar").forEach { taskName -> - tasks.named(taskName) { - dependsOn(buildFastCheckAdapter) - } -} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt index 65dbf5170d..8971a44c4f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt @@ -2,46 +2,8 @@ package org.usvm.ts.pbt /** Stable identifiers for diagnostics created on the Kotlin side of the PBT boundary. */ internal object PbtDiagnosticCode { - const val CLI_ARGUMENT_INVALID = "cli.argument.invalid" - const val CLI_COVERAGE_REQUIRED = "cli.coverage.required" - const val CLI_COVERAGE_SCOPE_INVALID = "cli.coverage.scope.invalid" - const val CLI_EXAMPLES_INVALID = "cli.examples.invalid" - const val CLI_NUM_RUNS_INVALID = "cli.num-runs.invalid" - const val CLI_PROPERTY_EMPTY = "cli.property.empty" - const val CLI_PROPERTY_INVALID = "cli.property.invalid" - const val CLI_PROPERTY_UNKNOWN = "cli.property.unknown" - const val CLI_REGISTRY_EMPTY = "cli.registry.empty" - const val CLI_REGISTRY_ID_DUPLICATE = "cli.registry.id.duplicate" - const val CLI_REGISTRY_ID_INVALID = "cli.registry.id.invalid" - const val CLI_REGISTRY_UNKNOWN = "cli.registry.unknown" - const val CLI_SINGLE_PROPERTY_REQUIRED = "cli.single-property.required" - const val CLI_SOURCE_ROOT_REQUIRED = "cli.source-root.required" - const val CLI_TIMEOUT_INVALID = "cli.timeout.invalid" - - const val REGISTRY_PROPERTY_ID_DUPLICATE = "registry.property-id.duplicate" - const val REGISTRY_PROPERTY_INVALID = "registry.property.invalid" - const val REGISTRY_PROVIDER_LOAD_FAILED = "registry.provider.load.failed" - - const val BACKEND_EXAMPLES_ARITY = "backend.examples.arity" - const val BACKEND_EXAMPLES_DOMAIN = "backend.examples.domain" - const val BACKEND_EXAMPLES_VALUE_INVALID = "backend.examples.value.invalid" - const val BACKEND_PROCESS_FAILED = "backend.process.failed" - const val BACKEND_PROCESS_INTERRUPTED = "backend.process.interrupted" - const val BACKEND_PROCESS_READ_FAILED = "backend.process.read.failed" - const val BACKEND_PROCESS_START_FAILED = "backend.process.start.failed" - const val BACKEND_PROCESS_TIMEOUT = "backend.process.timeout" - const val BACKEND_PROCESS_WRITE_FAILED = "backend.process.write.failed" - const val BACKEND_REQUEST_TOO_LARGE = "backend.request.too-large" - const val BACKEND_RESPONSE_EMPTY = "backend.response.empty" - const val BACKEND_RESPONSE_INVALID = "backend.response.invalid" - const val BACKEND_RESPONSE_TOO_LARGE = "backend.response.too-large" - const val BACKEND_RUNTIME_NOT_FOUND = "backend.runtime.not-found" - - const val COVERAGE_COLLECTOR_NOT_FOUND = "coverage.collector.not-found" const val COVERAGE_REPORT_INVALID = "coverage.report.invalid" const val COVERAGE_REPORT_MISSING = "coverage.report.missing" - const val COVERAGE_RUNTIME_UNSUPPORTED = "coverage.runtime.unsupported" - const val COVERAGE_RUNTIME_VERSION_UNAVAILABLE = "coverage.runtime.version-unavailable" const val COVERAGE_SOURCE_MAP_INVALID = "coverage.source-map.invalid" const val COVERAGE_SOURCE_MAP_MISSING = "coverage.source-map.missing" @@ -61,9 +23,6 @@ internal object PbtDiagnosticCode { const val MAPPING_STATEMENT_AMBIGUOUS = "mapping.statement.ambiguous" const val MAPPING_STATEMENT_UNMAPPED = "mapping.statement.unmapped" - const val PROTOCOL_REQUEST_INVALID = "protocol.request.invalid" - const val SOURCE_ROOT_INVALID = "source-root.invalid" - const val PROPERTY_ID_INVALID = "property.id.invalid" const val PROPERTY_INPUTS_EMPTY = "property.inputs.empty" const val INPUT_NAME_DUPLICATE = "input.name.duplicate" diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/RawV8SourceMapInspector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/RawV8SourceMapInspector.kt index d19176a68d..7ceef0c0a0 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/RawV8SourceMapInspector.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/RawV8SourceMapInspector.kt @@ -18,7 +18,7 @@ import java.util.stream.Collectors import kotlin.io.path.invariantSeparatorsPathString /** Reads bounded raw V8 source-map caches that c8 does not retain in its final Istanbul report. */ -internal fun inspectRawV8SourceMapDiagnostics( +fun inspectRawV8SourceMapDiagnostics( rawDirectory: Path, sourceRoots: List, maxReportFiles: Int = MAX_RAW_V8_REPORT_FILES, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/SourceMapDiagnostics.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/SourceMapDiagnostics.kt index 863911a0f9..7dbaf15531 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/SourceMapDiagnostics.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/SourceMapDiagnostics.kt @@ -4,7 +4,7 @@ import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.backend.CoverageDiagnostic /** Raw V8 evidence replaces the less precise source-map guesses made from the final Istanbul report. */ -internal fun mergeCoverageDiagnostics( +fun mergeCoverageDiagnostics( finalDiagnostics: List, rawDiagnostics: List, ): List { 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 637b91d3d2..5c5d344b3b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -39,6 +39,18 @@ import kotlin.time.Duration.Companion.seconds private val logger = KotlinLogging.logger {} +/** Whether symbolic analysis exhausted its paths or a configured strategy stopped it. */ +enum class TsAnalysisStopReason { + EXHAUSTED, + STOPPED, +} + +/** Collected states together with the machine completion kind. */ +data class TsAnalysisResult( + val states: List, + val stopReason: TsAnalysisStopReason, +) + class TsMachine( scene: EtsScene, override val options: UMachineOptions, @@ -92,7 +104,12 @@ class TsMachine( fun analyze( methods: List, targets: List = emptyList(), - ): List { + ): List = analyzeWithOutcome(methods = methods, targets = targets).states + + fun analyzeWithOutcome( + methods: List, + targets: List = emptyList(), + ): TsAnalysisResult { val initialStates = mutableMapOf() methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } @@ -147,7 +164,6 @@ class TsMachine( } val stepsStatistics = StepsStatistics() - val stopStrategy = object : StopStrategy { val strategy = createStopStrategy( options, @@ -194,7 +210,13 @@ class TsMachine( stopStrategy = stopStrategy ) - return statesCollector.collectedStates + val stopReason = if (pathSelector.isEmpty()) { + TsAnalysisStopReason.EXHAUSTED + } else { + TsAnalysisStopReason.STOPPED + } + + return TsAnalysisResult(states = statesCollector.collectedStates, stopReason = stopReason) } override fun close() { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineCompletionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineCompletionTest.kt new file mode 100644 index 0000000000..416e1910ae --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineCompletionTest.kt @@ -0,0 +1,40 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.UMachineOptions +import org.usvm.util.TsMethodTestRunner +import kotlin.test.assertEquals +import kotlin.time.Duration + +class TsMachineCompletionTest : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/lang/StaticOverloads.ts") + + @Test + fun `analysis distinguishes path exhaustion from strategy stop`() { + val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") + val exhaustedOptions = UMachineOptions( + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + val stoppedOptions = exhaustedOptions.copy(stepLimit = 1uL) + + val exhausted = TsMachine( + scene = scene, + options = exhaustedOptions, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + val stopped = TsMachine( + scene = scene, + options = stoppedOptions, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, exhausted.stopReason) + assertEquals(TsAnalysisStopReason.STOPPED, stopped.stopReason) + } +}