From 57897a2d1221688767116b423909fd9115508455 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 11:04:37 +0300 Subject: [PATCH] Expose direct property campaigns through the CLI --- .../usvm/ts/pbt/FastCheckDiagnosticCode.kt | 5 + .../kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt | 64 ++++ .../org/usvm/ts/pbt/cli/FastCheckCli.kt | 12 +- .../org/usvm/ts/pbt/cli/FastCheckOptions.kt | 57 ++- .../org/usvm/ts/pbt/cli/CampaignCliTest.kt | 336 ++++++++++++++++++ .../org/usvm/ts/pbt/cli/FastCheckCliTest.kt | 3 + 6 files changed, 474 insertions(+), 3 deletions(-) create mode 100644 usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt 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 index 963ad07793..a56ba2d6c1 100644 --- 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 @@ -3,6 +3,11 @@ 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_CAMPAIGN_ARTIFACT_REQUIRED = "cli.campaign.artifact.required" + const val CLI_CAMPAIGN_ARTIFACT_WRITE_FAILED = "cli.campaign.artifact.write-failed" + const val CLI_CAMPAIGN_MODE_REQUIRED = "cli.campaign.mode.required" + const val CLI_CAMPAIGN_RESERVE_INVALID = "cli.campaign.reserve.invalid" + const val CLI_CAMPAIGN_SOURCE_ROOT_INVALID = "cli.campaign.source-root.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" diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt new file mode 100644 index 0000000000..84d70e5a65 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt @@ -0,0 +1,64 @@ +package org.usvm.ts.pbt.cli + +import org.usvm.ts.pbt.FastCheckDiagnosticCode +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.campaign.PropertyCampaignResult +import org.usvm.ts.pbt.campaign.PropertyCampaignRunner +import org.usvm.ts.pbt.campaign.PropertyCampaignStop +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import java.io.IOException +import java.nio.file.Files + +internal fun executeCampaign( + options: CliOptions, + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + output: Appendable, +): Int { + val mode = requireNotNull(options.mode) + val destination = requireNotNull(options.artifactFile) + val runner = PropertyCampaignRunner(sourceRoot = options.sourceRoots.single()) + val reserve = options.validationReserveMillis + val artifact = if (reserve == null) { + runner.runArtifact(property, mode, configuration) + } else { + runner.runArtifact(property, mode, configuration, reserve) + } + + val json = PropertyManifestJson.json.encodeToUtf8SafeString(artifact) + output.appendLine(json) + + try { + Files.writeString(destination, json) + } catch (error: IOException) { + throw CliUsageException( + code = FastCheckDiagnosticCode.CLI_CAMPAIGN_ARTIFACT_WRITE_FAILED, + message = "Cannot write campaign artifact to $destination: " + error.message, + path = "artifact", + cause = error, + ) + } + + return campaignExitCode(artifact.result) +} + +/** A demonstrated violation remains a finding even when secondary work cannot finish. */ +internal fun campaignExitCode(result: PropertyCampaignResult): Int { + if (result.confirmedViolation) return EXIT_CONFIRMED_VIOLATION + + val concreteCompleted = result.concrete?.status != PropertyRunStatus.FAILURE + val symbolicCompleted = result.symbolic == null || + result.symbolic.status == UsvmPropertySearchStatus.NO_VIOLATION_REACHED + val completed = result.stop == PropertyCampaignStop.COMPLETED && + concreteCompleted && symbolicCompleted && result.confirmation == null + + return if (completed) EXIT_SUCCESS else EXIT_INCOMPLETE +} + +private const val EXIT_SUCCESS = 0 +private const val EXIT_CONFIRMED_VIOLATION = 1 +private const val EXIT_INCOMPLETE = 2 diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt index 9bfb02c65b..b0a7114a83 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt @@ -123,6 +123,10 @@ class FastCheckCli( coverageRequest = options.coverageRequest, ) + if (options.mode != null) { + return executeCampaign(options, properties.single(), configuration, output) + } + val backend = backendFactory(options.sourceRoots) requireCoverageSupport(options, backend) val results = properties.map { property -> backend.run(property, configuration) } @@ -187,12 +191,16 @@ class FastCheckCli( } private fun requireSinglePropertyForRunScopedControls(options: CliOptions, propertyCount: Int) { - val usesRunScopedControls = options.replayPath != null || options.examplesFile != null + val usesRunScopedControls = options.replayPath != null || options.examplesFile != null || options.mode != null if (usesRunScopedControls && propertyCount != 1) { throw CliUsageException( code = FastCheckDiagnosticCode.CLI_SINGLE_PROPERTY_REQUIRED, - message = "Replay paths and explicit examples require exactly one selected property", + message = if (options.mode == null) { + "Replay paths and explicit examples require exactly one selected property" + } else { + "Campaign artifacts require exactly one selected property" + }, path = "property", ) } diff --git a/usvm-ts-fast-check/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 index 56be2a4cc0..fd77b762a6 100644 --- a/usvm-ts-fast-check/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 @@ -8,6 +8,7 @@ import com.github.ajalt.clikt.parameters.options.default import com.github.ajalt.clikt.parameters.options.flag import com.github.ajalt.clikt.parameters.options.multiple import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.choice import com.github.ajalt.clikt.parameters.types.int import com.github.ajalt.clikt.parameters.types.long import com.github.ajalt.clikt.parameters.types.path @@ -15,6 +16,7 @@ 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 +import org.usvm.ts.pbt.campaign.PropertyCampaignMode import org.usvm.ts.pbt.model.PropertyId import java.nio.file.Path @@ -34,6 +36,9 @@ internal data class CliOptions( val timeoutMillis: Long, val examplesFile: Path?, val coverageRequest: PropertyCoverageRequest?, + val mode: PropertyCampaignMode?, + val artifactFile: Path?, + val validationReserveMillis: Long?, ) internal class CliUsageException( @@ -94,7 +99,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") private val timeoutMillis by option( "--timeout-ms", - help = "Property timeout in milliseconds", + help = "Property or total campaign timeout in milliseconds", ).long().default(PropertyRunConfiguration.DEFAULT_TIMEOUT_MILLIS) private val examplesFile by option( @@ -102,6 +107,21 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") help = "JSON file with positional tagged examples", ).path() + private val mode by option( + "--mode", + help = "Run one original-property campaign with FastCheck/USVM", + ).choice(PropertyCampaignMode.entries.associateBy { it.name }) + + private val artifactFile by option( + "--artifact", + help = "Write the campaign artifact JSON; requires --mode and one property/source root", + ).path() + + private val validationReserveMillis by option( + "--validation-reserve-ms", + help = "Reserve within the total campaign timeout for native confirmation and reduction; requires --mode", + ).long() + private val coverageEnabled by option( "--coverage", help = "Collect source-mapped coverage for every property run", @@ -129,6 +149,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") requireSourceRoots() requirePositiveRunControls() requireCoverageFlag() + requireCampaignControls() options = CliOptions( sourceRoots = sourceRoots, @@ -140,6 +161,9 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") timeoutMillis = timeoutMillis, examplesFile = examplesFile, coverageRequest = buildCoverageRequest(), + mode = mode, + artifactFile = artifactFile, + validationReserveMillis = validationReserveMillis, ) } @@ -171,6 +195,37 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") } } + private fun requireCampaignControls() { + val hasCampaignDetails = artifactFile != null || validationReserveMillis != null + val reserve = validationReserveMillis + val error = when { + mode == null && hasCampaignDetails -> CliUsageException( + code = FastCheckDiagnosticCode.CLI_CAMPAIGN_MODE_REQUIRED, + message = "--artifact and --validation-reserve-ms require --mode", + path = "mode", + ) + mode != null && artifactFile == null -> CliUsageException( + code = FastCheckDiagnosticCode.CLI_CAMPAIGN_ARTIFACT_REQUIRED, + message = "--mode requires --artifact", + path = "artifact", + ) + mode != null && sourceRoots.size != 1 -> CliUsageException( + code = FastCheckDiagnosticCode.CLI_CAMPAIGN_SOURCE_ROOT_INVALID, + message = "A campaign requires exactly one --source-root", + path = "sourceRoot", + ) + reserve != null && reserve <= 0 -> CliUsageException( + code = FastCheckDiagnosticCode.CLI_CAMPAIGN_RESERVE_INVALID, + message = "--validation-reserve-ms must be positive", + path = "validationReserveMillis", + ) + + else -> null + } + + if (error != null) throw error + } + private fun requireCoverageFlag() { val hasCoverageDetails = coverageScopes.isNotEmpty() || coverageIncludePatterns.isNotEmpty() || diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt new file mode 100644 index 0000000000..ef626edbbe --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt @@ -0,0 +1,336 @@ +package org.usvm.ts.pbt.cli + +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.json.jsonObject +import kotlinx.serialization.json.jsonPrimitive +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.campaign.PropertyCampaignArtifact +import org.usvm.ts.pbt.campaign.PropertyCampaignMode +import org.usvm.ts.pbt.campaign.PropertyCampaignPhase +import org.usvm.ts.pbt.campaign.PropertyCampaignStop +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.ExecutionKind +import org.usvm.ts.pbt.model.IntegerDomain +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 org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.registry.PropertyRegistry +import org.usvm.ts.pbt.registry.PropertyRegistryProvider +import org.usvm.ts.pbt.testResourcesRoot +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import java.nio.file.Files +import java.nio.file.Path +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class CampaignCliTest { + @TempDir + lateinit var directory: Path + + private val sourceRoot = testResourcesRoot().resolve("properties/campaign") + + @Test + fun `all direct modes use the original oracle and save their actual confirmed violation`() { + for (mode in PropertyCampaignMode.entries) { + val destination = directory.resolve("$mode.json") + val example = if (mode == PropertyCampaignMode.SEQUENTIAL) 20.0 else 42.0 + val coverage = if (mode == PropertyCampaignMode.PBT_ONLY) { + arrayOf("--coverage", "--coverage-scope", "property-entry-points") + } else { + emptyArray() + } + val run = runCli( + arguments(mode, destination) + arrayOf("--examples", writeExample(example).toString()) + coverage, + ) + + val artifact = readArtifact(run, destination) + + assertEquals(1, run.exitCode) + assertEquals("", run.errors) + assertEquals(mode, artifact.result.mode) + assertEquals(354, artifact.configuration.seed) + assertEquals(1, artifact.configuration.numRuns) + assertTrue(artifact.result.confirmedViolation) + if (mode == PropertyCampaignMode.PBT_ONLY) { + assertNull(artifact.result.symbolic) + assertTrue(assertNotNull(artifact.result.concrete?.coverage).files.isNotEmpty()) + } else { + assertEquals(listOf(JsConcreteValue.number(42.0)), artifact.result.symbolic?.inputs) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, artifact.result.confirmation?.status) + } + if (mode == PropertyCampaignMode.SYMBOLIC_ONLY) { + assertNull(artifact.result.concrete) + } + if (mode == PropertyCampaignMode.SEQUENTIAL) { + assertEquals(PropertyRunStatus.SUCCESS, artifact.result.concrete?.status) + } + + for (stop in listOf(PropertyCampaignStop.DEADLINE, PropertyCampaignStop.EXECUTION_FAILURE)) { + val interruptedAfterFinding = artifact.result.copy( + stop = stop, + stoppedAt = PropertyCampaignPhase.CONFIRMATION, + ) + + assertEquals(1, campaignExitCode(interruptedAfterFinding)) + } + } + } + + @Test + fun `completed direct controls with no finding return zero`() { + val admittedSingleton = property().copy( + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 20, max = 20))), + ) + + for (mode in PropertyCampaignMode.entries) { + val destination = directory.resolve("$mode.json") + + val run = runCli(arguments(mode, destination), properties = listOf(admittedSingleton)) + val artifact = readArtifact(run, destination) + + assertEquals(0, run.exitCode) + assertEquals("", run.errors) + assertFalse(artifact.result.confirmedViolation) + assertEquals(PropertyCampaignStop.COMPLETED, artifact.result.stop) + } + } + + @Test + fun `unsupported symbolic control remains incomplete and is saved`() { + val asynchronous = property().copy( + predicate = TypeScriptEntryPoint( + module = "DirectControls.ts", + exportName = "asyncHolds", + executionKind = ExecutionKind.ASYNC, + ), + ) + val destination = directory.resolve("unsupported.json") + + val run = runCli( + arguments(PropertyCampaignMode.SYMBOLIC_ONLY, destination), + properties = listOf(asynchronous), + ) + val artifact = readArtifact(run, destination) + + assertEquals(2, run.exitCode) + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, artifact.result.symbolic?.status) + assertFalse(artifact.result.confirmedViolation) + assertNull(artifact.result.concrete) + } + + @Test + fun `expired total deadline is not reported as no finding`() { + val destination = directory.resolve("timeout.json") + + val run = runCli( + arguments(PropertyCampaignMode.SYMBOLIC_ONLY, destination) + + arrayOf("--timeout-ms", "1", "--validation-reserve-ms", "1"), + ) + val artifact = readArtifact(run, destination) + + assertEquals(2, run.exitCode) + assertEquals(PropertyCampaignStop.DEADLINE, artifact.result.stop) + assertNull(artifact.result.symbolic) + assertFalse(artifact.result.confirmedViolation) + } + + @Test + fun `one deadline allocation retains PBT when the search reserve is already exhausted`() { + val destination = directory.resolve("sequential-timeout.json") + + val run = runCli( + arguments(PropertyCampaignMode.SEQUENTIAL, destination) + arrayOf( + "--examples", writeExample(value = 20.0).toString(), + "--timeout-ms", "60000", + "--validation-reserve-ms", "60000", + ), + ) + val artifact = readArtifact(run, destination) + + assertEquals(2, run.exitCode) + assertEquals(PropertyRunStatus.SUCCESS, artifact.result.concrete?.status) + assertEquals(PropertyCampaignStop.DEADLINE, artifact.result.stop) + assertEquals(PropertyCampaignPhase.SYMBOLIC, artifact.result.stoppedAt) + assertEquals(60_000, artifact.configuration.timeoutMillis) + assertEquals(60_000, artifact.validationReserveMillis) + assertNull(artifact.result.symbolic) + } + + @Test + fun `native execution failure is saved separately from a property violation`() { + val invalidExport = property().copy( + predicate = TypeScriptEntryPoint(module = "DirectControls.ts", exportName = "missing"), + ) + val destination = directory.resolve("execution-failure.json") + + val run = runCli(arguments(PropertyCampaignMode.PBT_ONLY, destination), properties = listOf(invalidExport)) + val artifact = readArtifact(run, destination) + + assertEquals(2, run.exitCode) + assertEquals(PropertyCampaignStop.EXECUTION_FAILURE, artifact.result.stop) + assertNotNull(artifact.result.diagnostic) + assertFalse(artifact.result.confirmedViolation) + } + + @Test + fun `an artifact write failure retains the demonstrated violation on stdout`() { + val run = runCli( + arguments(PropertyCampaignMode.PBT_ONLY, directory) + + arrayOf("--examples", writeExample(value = 42.0).toString()), + ) + + val artifact = PropertyManifestJson.json.decodeFromString(run.output) + + assertEquals(2, run.exitCode) + assertEquals("cli.campaign.artifact.write-failed", diagnosticCode(run)) + assertTrue(artifact.result.confirmedViolation) + assertEquals(listOf(JsConcreteValue.number(42.0)), artifact.result.concrete?.counterexample) + } + + @Test + fun `stdout and saved artifact come from one native campaign`() { + val sources = Files.createDirectory(directory.resolve("sources")) + val counter = directory.resolve("calls") + val counterLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(counter.toString()) + sources.resolve("Counted.ts").writeText( + """ + import { appendFileSync } from 'node:fs'; + export function counted(value: number): boolean { + appendFileSync($counterLiteral, 'x'); + return true; + } + """.trimIndent(), + ) + val countedProperty = property().copy( + predicate = TypeScriptEntryPoint(module = "Counted.ts", exportName = "counted"), + precondition = null, + ) + val destination = directory.resolve("counted.json") + + val run = runCli( + arguments(PropertyCampaignMode.PBT_ONLY, destination, root = sources, numRuns = 3), + properties = listOf(countedProperty), + ) + val artifact = readArtifact(run, destination) + + assertEquals(0, run.exitCode) + assertEquals(3, artifact.result.concrete?.numRuns) + assertEquals("xxx", Files.readString(counter)) + } + + @Test + fun `campaign options reject missing or inconsistent controls before execution`() { + val destination = directory.resolve("invalid.json").toString() + val root = sourceRoot.toString() + val cases = listOf( + arrayOf("--source-root", root, "--artifact", destination) to "cli.campaign.mode.required", + arrayOf("--source-root", root, "--validation-reserve-ms", "1") to "cli.campaign.mode.required", + arrayOf("--source-root", root, "--mode", "PBT_ONLY") to "cli.campaign.artifact.required", + arrayOf( + "--source-root", root, "--source-root", root, "--mode", "PBT_ONLY", "--artifact", destination, + ) to "cli.campaign.source-root.invalid", + arrayOf( + "--source-root", root, "--mode", "PBT_ONLY", "--artifact", destination, "--validation-reserve-ms", "0", + ) to "cli.campaign.reserve.invalid", + arrayOf( + "--source-root", root, "--mode", "UNKNOWN", "--artifact", destination, + ) to "cli.argument.invalid", + ) + + for ((arguments, expectedCode) in cases) { + val run = runCli(arguments) + + assertEquals(2, run.exitCode) + assertEquals(expectedCode, diagnosticCode(run)) + assertEquals("", run.output) + assertFalse(Files.exists(directory.resolve("invalid.json"))) + } + } + + @Test + fun `one artifact requires one selected property`() { + val destination = directory.resolve("multiple.json") + val second = property().copy(id = PropertyId(value = "cli.second")) + + val run = runCli( + arrayOf("--source-root", sourceRoot.toString(), "--mode", "PBT_ONLY", "--artifact", destination.toString()), + properties = listOf(property(), second), + ) + + assertEquals(2, run.exitCode) + assertEquals("cli.single-property.required", diagnosticCode(run)) + assertEquals("", run.output) + assertFalse(Files.exists(destination)) + } + + private fun arguments( + mode: PropertyCampaignMode, + destination: Path, + root: Path = sourceRoot, + numRuns: Int = 1, + ): Array = arrayOf( + "--source-root", root.toString(), + "--registry", "campaign-cli", + "--property", "cli.isolated", + "--seed", "354", + "--num-runs", numRuns.toString(), + "--mode", mode.name, + "--artifact", destination.toString(), + ) + + private fun writeExample(value: Double): Path { + val path = directory.resolve("example-$value.json") + val example: List = listOf(JsConcreteValue.number(value)) + val json = PropertyManifestJson.json.encodeToUtf8SafeString(listOf(example)) + Files.writeString(path, json) + + return path + } + + private fun runCli( + arguments: Array, + properties: List = listOf(property()), + ): CliRun { + val provider = object : PropertyRegistryProvider { + override val registryId: String = "campaign-cli" + override fun load(): PropertyRegistry = PropertyRegistry(properties) + } + val output = StringBuilder() + val errors = StringBuilder() + + val exitCode = FastCheckCli(providers = listOf(provider), output = output, errors = errors).run(arguments) + + return CliRun(exitCode, output.toString(), errors.toString()) + } + + private fun readArtifact(run: CliRun, path: Path): PropertyCampaignArtifact { + assertEquals(Files.readString(path), run.output.trimEnd()) + + return PropertyCampaignArtifact.read(path) + } + + private fun diagnosticCode(run: CliRun): String { + val diagnostic = PropertyManifestJson.json.parseToJsonElement(run.errors).jsonObject + + return diagnostic.getValue("code").jsonPrimitive.content + } + + private fun property() = PropertyDefinition( + id = PropertyId(value = "cli.isolated"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 0, max = 100))), + predicate = TypeScriptEntryPoint(module = "DirectControls.ts", exportName = "isolatedFailure"), + precondition = TypeScriptEntryPoint(module = "DirectControls.ts", exportName = "admits"), + ) + + private data class CliRun(val exitCode: Int, val output: String, val errors: String) +} diff --git a/usvm-ts-fast-check/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 index d00526becd..238ac8050c 100644 --- a/usvm-ts-fast-check/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 @@ -50,6 +50,9 @@ class FastCheckCliTest { assertContains(output, "TypeScript source root") assertContains(output, "--examples") assertContains(output, "--coverage-scope") + assertContains(output, "--mode") + assertContains(output, "--artifact") + assertContains(output, "--validation-reserve-ms") } @Test