From 028d5b0c116502525cdb2329f24bde665807922f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 22:31:38 +0300 Subject: [PATCH] Run frozen property campaigns from JSON requests --- .../usvm/ts/pbt/cli/CampaignFileRequest.kt | 68 +++++++++++++++++ .../org/usvm/ts/pbt/cli/FastCheckCli.kt | 7 +- .../usvm/ts/pbt/cli/CampaignFileCliTest.kt | 74 +++++++++++++++++++ 3 files changed, 148 insertions(+), 1 deletion(-) create mode 100644 usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFileRequest.kt create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFileCliTest.kt diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFileRequest.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFileRequest.kt new file mode 100644 index 0000000000..4b26e54ff1 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignFileRequest.kt @@ -0,0 +1,68 @@ +package org.usvm.ts.pbt.cli + +import kotlinx.serialization.Serializable +import kotlinx.serialization.decodeFromString +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.campaign.PropertyCampaignMode +import org.usvm.ts.pbt.campaign.PropertyCampaignRunner +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import java.io.IOException +import java.nio.file.Files +import java.nio.file.Path + +/** One frozen experiment cell using the public campaign, with no service-loaded registry. */ +@Serializable +internal data class CampaignFileRequest( + val sourceRoot: String, + val property: PropertyDefinition, + val mode: PropertyCampaignMode, + val configuration: PropertyRunConfiguration, + val pbtAllocationMillis: Long? = null, + val validationReserveMillis: Long = PropertyCampaignRunner.DEFAULT_VALIDATION_RESERVE_MILLIS, + val completedInputLimit: Int = 0, + val shrinkWitness: Boolean = false, + val nodeExecutable: String = "node", +) + +internal fun runCampaignFile( + args: Array, + output: Appendable = System.out, + errors: Appendable = System.err, +): Int = try { + require(args.size == 2) { "campaign-file requires a request JSON and an artifact destination" } + val requestFile = Path.of(args[0]).toRealPath() + val request = PropertyManifestJson.json.decodeFromString(Files.readString(requestFile)) + val root = requestFile.parent.resolve(request.sourceRoot).normalize().toRealPath() + val artifact = PropertyCampaignRunner( + sourceRoot = root, + nodeExecutable = request.nodeExecutable, + machineOptions = UMachineOptions( + solverType = SolverType.YICES, + randomSeed = request.configuration.seed?.toLong() ?: 0, + ), + ).runArtifact( + property = request.property, + mode = request.mode, + configuration = request.configuration, + validationReserveMillis = request.validationReserveMillis, + pbtAllocationMillis = request.pbtAllocationMillis, + shrinkWitness = request.shrinkWitness, + completedInputLimit = request.completedInputLimit, + ) + + val json = PropertyManifestJson.json.encodeToUtf8SafeString(artifact) + output.appendLine(json) + Files.writeString(Path.of(args[1]), json) + + campaignExitCode(artifact.result) +} catch (error: IllegalArgumentException) { + errors.appendLine(error.message) + 2 +} catch (error: IOException) { + errors.appendLine(error.message) + 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 b0a7114a83..cc350566f1 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 @@ -337,7 +337,12 @@ class FastCheckCli( /** Process entry point used by Gradle application and installed distributions. */ fun main(args: Array) { - exitProcess(FastCheckCli().run(args)) + val exitCode = if (args.firstOrNull() == "campaign-file") { + runCampaignFile(args.drop(1).toTypedArray()) + } else { + FastCheckCli().run(args) + } + exitProcess(exitCode) } @Serializable diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFileCliTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFileCliTest.kt new file mode 100644 index 0000000000..3d858edabc --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignFileCliTest.kt @@ -0,0 +1,74 @@ +package org.usvm.ts.pbt.cli + +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.campaign.PropertyCampaignArtifact +import org.usvm.ts.pbt.campaign.PropertyCampaignMode +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.IntegerDomain +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.testResourcesRoot +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class CampaignFileCliTest { + @TempDir + lateinit var directory: Path + + @Test + fun `frozen file invokes the public symbolic campaign without a registry`() { + val request = request(mode = PropertyCampaignMode.SYMBOLIC_ONLY).copy(completedInputLimit = 3) + val path = directory.resolve("request.json") + val destination = directory.resolve("artifact.json") + Files.writeString(path, PropertyManifestJson.json.encodeToUtf8SafeString(request)) + val output = StringBuilder() + val errors = StringBuilder() + + val exit = runCampaignFile(arrayOf(path.toString(), destination.toString()), output, errors) + val artifact = PropertyCampaignArtifact.read(destination) + + assertEquals(0, exit) + assertEquals("", errors.toString()) + assertEquals(Files.readString(destination), output.toString().trim()) + assertEquals(37, artifact.configuration.seed) + assertEquals(PropertyCampaignMode.SYMBOLIC_ONLY, artifact.result.mode) + assertFalse(artifact.shrinkWitness) + assertTrue(artifact.result.symbolicInputReplays.isNotEmpty()) + } + + @Test + fun `file controls reject invalid capture before running or creating an artifact`() { + val request = request(mode = PropertyCampaignMode.PBT_ONLY).copy(completedInputLimit = 1) + val path = directory.resolve("request.json") + val destination = directory.resolve("artifact.json") + Files.writeString(path, PropertyManifestJson.json.encodeToUtf8SafeString(request)) + val output = StringBuilder() + val errors = StringBuilder() + + val exit = runCampaignFile(arrayOf(path.toString(), destination.toString()), output, errors) + + assertEquals(2, exit) + assertEquals("", output.toString()) + assertTrue(errors.contains("symbolic campaign")) + assertFalse(Files.exists(destination)) + } + + private fun request(mode: PropertyCampaignMode) = CampaignFileRequest( + sourceRoot = testResourcesRoot().resolve("properties/campaign").toString(), + property = PropertyDefinition( + id = PropertyId(value = "file.healthy"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))), + predicate = TypeScriptEntryPoint(module = "CompletedProperties.ts", exportName = "healthy"), + ), + mode = mode, + configuration = PropertyRunConfiguration(seed = 37, numRuns = 1, timeoutMillis = 60_000), + ) +}