[TS PBT] Run one PBT phase followed by coverage-guided USVM

usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts

@@ -833,7 +833,7 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
     assertion.id === point.assertionId && samePoint(assertion.testedCall, point.callSite)
       && assertion.operands.some((operand) =>
         operand.id === point.operandId && samePoint(operand.source, point.source))) ?? false);
-  if (points.length === 0 || uniquePoints.size !== points.length || uniqueSources.size !== sources.length
+  if (uniquePoints.size !== points.length || uniqueSources.size !== sources.length
     || !allSourcesPresent || !allPointsBound) {
     throw protocolError(adapterDiagnostic.protocolRequestInvalid,
       'Observation points must bind to declared assertion operands and selected source hashes', 'observationRequest');

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt

@@ -24,6 +24,8 @@ data class PropertyCampaignArtifact(
     val result: PropertyCampaignResult,
     val targetRole: WitnessRole = WitnessRole.PROPERTY,
     val metadata: PropertyCampaignMetadata? = null,
+    val pbtAllocationMillis: Long? = null,
+    val shrinkWitness: Boolean = true,
 ) {
     init {
         val resultProperties = listOfNotNull(
@@ -34,6 +36,7 @@ data class PropertyCampaignArtifact(
         )
         val sameProperty = resultProperties.all { it == property.id }
         require(sameProperty) { "Campaign evidence belongs to another property" }
+        require(pbtAllocationMillis == null || pbtAllocationMillis in 1 until configuration.timeoutMillis)
         require(validationReserveMillis > 0) { "Validation reserve must be positive" }
         require(targetRole == WitnessRole.PROPERTY) { "Direct controls search the original property" }
     }

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

@@ -23,11 +23,14 @@ internal fun executeCampaign(
     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 artifact = runner.runArtifact(
+        property = property,
+        mode = mode,
+        configuration = configuration,
+        validationReserveMillis = reserve ?: PropertyCampaignRunner.DEFAULT_VALIDATION_RESERVE_MILLIS,
+        pbtAllocationMillis = options.pbtAllocationMillis,
+        shrinkWitness = options.shrinkWitness,
+    )
 
     val json = PropertyManifestJson.json.encodeToUtf8SafeString(artifact)
     output.appendLine(json)
@@ -53,7 +56,7 @@ internal fun campaignExitCode(result: PropertyCampaignResult): Int {
     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 &&
+    val completed = result.stop == PropertyCampaignStop.COMPLETED && result.diagnostic == null &&
         concreteCompleted && symbolicCompleted && result.confirmation == null
 
     return if (completed) EXIT_SUCCESS else EXIT_INCOMPLETE

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

@@ -39,6 +39,8 @@ internal data class CliOptions(
     val mode: PropertyCampaignMode?,
     val artifactFile: Path?,
     val validationReserveMillis: Long?,
+    val pbtAllocationMillis: Long? = null,
+    val shrinkWitness: Boolean = true,
 )
 
 internal class CliUsageException(
@@ -122,6 +124,16 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check")
         help = "Reserve within the total campaign timeout for native confirmation and reduction; requires --mode",
     ).long()
 
+    private val pbtAllocationMillis by option(
+        "--pbt-allocation-ms",
+        help = "PBT allocation within a two-phase campaign; required for COVERAGE_FEEDBACK",
+    ).long()
+
+    private val noShrinking by option(
+        "--no-shrinking",
+        help = "Disable native candidate reduction; requires --mode",
+    ).flag()
+
     private val coverageEnabled by option(
         "--coverage",
         help = "Collect source-mapped coverage for every property run",
@@ -164,6 +176,8 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check")
             mode = mode,
             artifactFile = artifactFile,
             validationReserveMillis = validationReserveMillis,
+            pbtAllocationMillis = pbtAllocationMillis,
+            shrinkWitness = !noShrinking,
         )
     }
 
@@ -196,12 +210,17 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check")
     }
 
     private fun requireCampaignControls() {
-        val hasCampaignDetails = artifactFile != null || validationReserveMillis != null
+        val hasCampaignDetails = artifactFile != null || validationReserveMillis != null ||
+            pbtAllocationMillis != null || noShrinking
         val reserve = validationReserveMillis
+        val allocation = pbtAllocationMillis
+        val twoPhase = mode == PropertyCampaignMode.SEQUENTIAL || mode == PropertyCampaignMode.COVERAGE_FEEDBACK
+        val invalidAllocation = allocation != null && (!twoPhase || allocation !in 1 until timeoutMillis)
+        val missingAllocation = mode == PropertyCampaignMode.COVERAGE_FEEDBACK && allocation == null
         val error = when {
             mode == null && hasCampaignDetails -> CliUsageException(
                 code = FastCheckDiagnosticCode.CLI_CAMPAIGN_MODE_REQUIRED,
-                message = "--artifact and --validation-reserve-ms require --mode",
+                message = "Campaign artifact and allocation controls require --mode",
                 path = "mode",
             )
             mode != null && artifactFile == null -> CliUsageException(
@@ -214,6 +233,12 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check")
                 message = "A campaign requires exactly one --source-root",
                 path = "sourceRoot",
             )
+            invalidAllocation || missingAllocation -> CliUsageException(
+                code = FastCheckDiagnosticCode.CLI_ARGUMENT_INVALID,
+                message = "COVERAGE_FEEDBACK requires --pbt-allocation-ms between 1 and the total timeout; " +
+                    "an explicit allocation is supported only by two-phase modes",
+                path = "pbtAllocationMillis",
+            )
             reserve != null && reserve <= 0 -> CliUsageException(
                 code = FastCheckDiagnosticCode.CLI_CAMPAIGN_RESERVE_INVALID,
                 message = "--validation-reserve-ms must be positive",

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt

@@ -172,7 +172,7 @@ class FastCheckBackend(
         }
         val hashesValid = request.sources.all { source -> source.sha256.matches(SHA256_REGEX) }
 
-        val validRequest = validLimits && request.points.isNotEmpty() && allSourcesPresent &&
+        val validRequest = validLimits && allSourcesPresent &&
             allPointsBound && allInputIndexesValid && hashesValid
 
         if (!validRequest) {

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/GuidedPropertyCampaignTest.kt

@@ -0,0 +1,180 @@
+package org.usvm.ts.pbt.campaign
+
+import org.junit.jupiter.api.Test
+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.backend.PropertyRunStatus
+import org.usvm.ts.pbt.backend.WitnessReductionStatus
+import org.usvm.ts.pbt.backend.WitnessReplayStatus
+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.testResourcesRoot
+import org.usvm.ts.pbt.usvm.UsvmEdgeReplayStatus
+import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus
+import java.nio.file.Files
+import kotlin.test.assertEquals
+import kotlin.test.assertNotNull
+import kotlin.test.assertNull
+import kotlin.test.assertTrue
+
+class GuidedPropertyCampaignTest {
+    private val root = testResourcesRoot().resolve("properties/campaign")
+    private val runner = PropertyCampaignRunner(sourceRoot = root)
+    private val configuration = PropertyRunConfiguration(seed = 355, numRuns = 1, timeoutMillis = 60_000)
+
+    @Test
+    fun `one real PBT batch changes the next symbolic work for the same original property`() {
+        val positive = run(exportName = "branchHolds", examples = listOf(1))
+        val negative = run(exportName = "branchHolds", examples = listOf(-1))
+
+        val positiveTrace = assertNotNull(positive.result.symbolic?.edgeGuidance)
+        val negativeTrace = assertNotNull(negative.result.symbolic?.edgeGuidance)
+        val positiveChoice = positiveTrace.selections.first { it.pendingStates > 1 && it.distance == 0 }
+        val negativeChoice = negativeTrace.selections.first { it.pendingStates > 1 && it.distance == 0 }
+        assertEquals(false, positiveChoice.goal?.outcome)
+        assertEquals(true, negativeChoice.goal?.outcome)
+        assertTrue(positiveTrace.replays.any { it.status == UsvmEdgeReplayStatus.CONFIRMED })
+        assertTrue(negativeTrace.replays.any { it.status == UsvmEdgeReplayStatus.CONFIRMED })
+        assertTrue(positiveTrace.remainingGoals.isEmpty())
+        assertTrue(negativeTrace.remainingGoals.isEmpty())
+        assertEquals(1, positive.result.concrete?.numRuns)
+        val observations = assertNotNull(positive.result.concrete?.observations)
+        assertEquals(1, observations.invocations.size)
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, positive.result.symbolic?.status)
+    }
+
+    @Test
+    fun `covered prefixes remain traversable for an uncovered nested edge`() {
+        val artifact = run(exportName = "nestedHolds", examples = listOf(1))
+
+        val trace = assertNotNull(artifact.result.symbolic?.edgeGuidance)
+        val missingNested = trace.initialGoals.single { it.outcome }
+        assertTrue(trace.replays.any { missingNested in it.additions }, trace.toString())
+        assertTrue(trace.remainingGoals.isEmpty(), trace.toString())
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, artifact.result.symbolic?.status)
+    }
+
+    @Test
+    fun `saturated coverage still finds and natively confirms an original defect and saves the full trace`() {
+        val artifact = run(exportName = "branchDifferent", examples = listOf(-1, 3), shrinkWitness = false)
+        val path = Files.createTempFile("guided-campaign-", ".json")
+
+        try {
+            artifact.write(path)
+            val restored = PropertyCampaignArtifact.read(path)
+
+            val symbolic = assertNotNull(restored.result.symbolic)
+            val trace = assertNotNull(symbolic.edgeGuidance)
+            assertTrue(trace.initialGoals.isEmpty(), trace.toString())
+            assertTrue(trace.selections.isNotEmpty())
+            assertTrue(trace.selections.all { it.originalObjectiveTurn })
+            assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, symbolic.status)
+            assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, restored.result.confirmation?.status)
+            assertEquals(WitnessReductionStatus.DISABLED, restored.result.confirmation?.reduction?.status)
+            assertEquals(artifact.result.symbolic?.edgeGuidance, trace)
+            assertEquals(artifact.result.symbolic?.diagnostics, symbolic.diagnostics)
+            assertEquals(15_000L, restored.pbtAllocationMillis)
+            assertTrue(restored.result.confirmedViolation)
+        } finally {
+            Files.deleteIfExists(path)
+        }
+    }
+
+    @Test
+    fun `sequential retains the no guidance control with the same explicit allocation`() {
+        val artifact = runner.runArtifact(
+            property = property(exportName = "branchHolds"),
+            mode = PropertyCampaignMode.SEQUENTIAL,
+            configuration = configuration.copy(examples = examples(1)),
+            pbtAllocationMillis = 15_000,
+        )
+
+        assertEquals(PropertyRunStatus.SUCCESS, artifact.result.concrete?.status)
+        assertNull(artifact.result.symbolic?.edgeGuidance)
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, artifact.result.symbolic?.status)
+    }
+
+    @Test
+    fun `PBT phase timeout leaves an explicit diagnostic and does not consume the symbolic remainder`() {
+        val property = property(exportName = "delayedHolds").copy(
+            predicate = TypeScriptEntryPoint(
+                module = MODULE,
+                exportName = "delayedHolds",
+                executionKind = ExecutionKind.ASYNC,
+            ),
+        )
+
+        val artifact = runner.runArtifact(
+            property = property,
+            mode = PropertyCampaignMode.COVERAGE_FEEDBACK,
+            configuration = configuration.copy(timeoutMillis = 30_000),
+            pbtAllocationMillis = 1_000,
+        )
+
+        assertNull(artifact.result.concrete)
+        assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, artifact.result.symbolic?.status)
+        assertTrue(artifact.result.diagnostic?.contains("PBT allocation expired") == true)
+        assertEquals(PropertyCampaignStop.COMPLETED, artifact.result.stop)
+    }
+
+    @Test
+    fun `runtime limitation reason and source survive the ordinary artifact roundtrip`() {
+        val property = property(exportName = "growthLimit").copy(
+            inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 1000, max = 1000))),
+        )
+        val artifact = runner.runArtifact(
+            property = property,
+            mode = PropertyCampaignMode.SYMBOLIC_ONLY,
+            configuration = configuration,
+        )
+        val path = Files.createTempFile("runtime-limitation-campaign-", ".json")
+
+        try {
+            artifact.write(path)
+            val restored = PropertyCampaignArtifact.read(path)
+
+            assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, restored.result.symbolic?.status)
+            val diagnostic = assertNotNull(restored.result.symbolic).diagnostics
+                .single { it.code == "usvm.runtime.array-index-growth" }
+            assertTrue(diagnostic.message.contains("array index write"), diagnostic.message)
+            assertTrue(diagnostic.path.contains(MODULE), diagnostic.toString())
+            assertEquals(artifact.result.symbolic?.diagnostics, restored.result.symbolic?.diagnostics)
+        } finally {
+            Files.deleteIfExists(path)
+        }
+    }
+
+    private fun run(
+        exportName: String,
+        examples: List<Int>,
+        shrinkWitness: Boolean = true,
+    ) = runner.runArtifact(
+        property = property(exportName),
+        mode = PropertyCampaignMode.COVERAGE_FEEDBACK,
+        configuration = configuration.copy(
+            numRuns = examples.size,
+            examples = examples.map { listOf(JsConcreteValue.number(it.toDouble())) },
+            coverageRequest = PropertyCoverageRequest(scopes = setOf(CoverageScope.SOURCE_UNDER_TEST)),
+        ),
+        pbtAllocationMillis = 15_000,
+        shrinkWitness = shrinkWitness,
+    )
+
+    private fun property(exportName: String) = PropertyDefinition(
+        id = PropertyId("campaign.guided.$exportName"),
+        inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))),
+        predicate = TypeScriptEntryPoint(module = MODULE, exportName = exportName),
+    )
+
+    private fun examples(value: Int) = listOf(listOf(JsConcreteValue.number(value.toDouble())))
+
+    private companion object {
+        const val MODULE = "GuidedProperties.ts"
+    }
+}

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt

@@ -41,7 +41,7 @@ class CampaignCliTest {
 
     @Test
     fun `all direct modes use the original oracle and save their actual confirmed violation`() {
-        for (mode in PropertyCampaignMode.entries) {
+        for (mode in PropertyCampaignMode.entries.filter { it != PropertyCampaignMode.COVERAGE_FEEDBACK }) {
             val destination = directory.resolve("$mode.json")
             val example = if (mode == PropertyCampaignMode.SEQUENTIAL) 20.0 else 42.0
             val coverage = if (mode == PropertyCampaignMode.PBT_ONLY) {
@@ -86,6 +86,35 @@ class CampaignCliTest {
         }
     }
 
+    @Test
+    fun `guided CLI generates once and prints and saves the same completed native feedback artifact`() {
+        val property = property().copy(
+            inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))),
+            predicate = TypeScriptEntryPoint(module = "GuidedProperties.ts", exportName = "branchHolds"),
+            precondition = null,
+        )
+        val destination = directory.resolve("guided.json")
+
+        val run = runCli(
+            arguments(PropertyCampaignMode.COVERAGE_FEEDBACK, destination) + arrayOf(
+                "--pbt-allocation-ms", "15000", "--examples", writeExample(value = 1.0).toString(), "--no-shrinking",
+            ),
+            properties = listOf(property),
+        )
+        val artifact = readArtifact(run, destination)
+
+        assertEquals(0, run.exitCode)
+        assertEquals("", run.errors)
+        assertEquals(1, artifact.result.concrete?.numRuns)
+        val observations = assertNotNull(artifact.result.concrete?.observations)
+        assertEquals(1, observations.invocations.size)
+        assertEquals(15_000L, artifact.pbtAllocationMillis)
+        assertFalse(artifact.shrinkWitness)
+        val trace = assertNotNull(artifact.result.symbolic?.edgeGuidance)
+        assertTrue(trace.replays.isNotEmpty())
+        assertTrue(trace.remainingGoals.isEmpty())
+    }
+
     @Test
     fun `completed direct controls with no finding return zero`() {
         val admittedSingleton = property().copy(
@@ -95,13 +124,20 @@ class CampaignCliTest {
         for (mode in PropertyCampaignMode.entries) {
             val destination = directory.resolve("$mode.json")
 
-            val run = runCli(arguments(mode, destination), properties = listOf(admittedSingleton))
+            val allocation = if (mode == PropertyCampaignMode.COVERAGE_FEEDBACK) {
+                arrayOf("--pbt-allocation-ms", "15000")
+            } else {
+                emptyArray()
+            }
+            val run = runCli(arguments(mode, destination) + allocation, 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)
+            val incompletePbt = artifact.result.copy(concrete = null, diagnostic = "PBT allocation expired")
+            assertEquals(2, campaignExitCode(incompletePbt))
         }
     }