[TS PBT] Run direct campaign controls from the existing CLI

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"

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

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",
             )
         }

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt

@@ -8,13 +8,15 @@ 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
 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,14 +99,29 @@ 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(
         "--examples",
         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() ||