[TS PBT] Honor caller cutoff in campaign-file

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

@@ -37,6 +37,8 @@ import org.usvm.ts.pbt.validation.requireValid
 import org.usvm.ts.pbt.validation.validatePropertyDefinition
 import java.io.IOException
 import java.nio.file.Path
+import java.time.Duration
+import java.time.Instant
 import java.util.concurrent.CancellationException
 import kotlin.time.Duration.Companion.milliseconds
 
@@ -77,7 +79,6 @@ class PropertyCampaignRunner(
     private val machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES),
 ) {
     /** Keeps phase transitions and retained partial results under the same deadline. */
-    @Suppress("LongMethod")
     fun runArtifact(
         property: PropertyDefinition,
         mode: PropertyCampaignMode,
@@ -86,15 +87,43 @@ class PropertyCampaignRunner(
         pbtAllocationMillis: Long? = null,
         shrinkWitness: Boolean = true,
         completedInputLimit: Int = 0,
+    ): PropertyCampaignArtifact = runArtifact(
+        property = property,
+        mode = mode,
+        configuration = configuration,
+        validationReserveMillis = validationReserveMillis,
+        pbtAllocationMillis = pbtAllocationMillis,
+        shrinkWitness = shrinkWitness,
+        completedInputLimit = completedInputLimit,
+        externalDeadlineEpochMillis = null,
+        publicationReserveMillis = 0,
+    )
+
+    @Suppress("LongMethod", "LongParameterList")
+    internal fun runArtifact(
+        property: PropertyDefinition,
+        mode: PropertyCampaignMode,
+        configuration: PropertyRunConfiguration = PropertyRunConfiguration(),
+        validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS,
+        pbtAllocationMillis: Long? = null,
+        shrinkWitness: Boolean = true,
+        completedInputLimit: Int = 0,
+        externalDeadlineEpochMillis: Long?,
+        publicationReserveMillis: Long = 0,
     ): PropertyCampaignArtifact {
+        require(externalDeadlineEpochMillis == null || externalDeadlineEpochMillis > 0) {
+            "External deadline epoch must be positive"
+        }
+        require(publicationReserveMillis >= 0) { "Publication reserve must not be negative" }
         require(completedInputLimit >= 0) { "Completed input limit must not be negative" }
         require(completedInputLimit == 0 || mode != PropertyCampaignMode.PBT_ONLY) {
             "Completed input capture requires a symbolic campaign mode"
         }
         validateControls(mode, configuration, validationReserveMillis, pbtAllocationMillis)
         val guided = mode == PropertyCampaignMode.COVERAGE_FEEDBACK
         val startedAt = System.nanoTime()
-        val deadline = WitnessReplayDeadline(timeoutMillis = configuration.timeoutMillis)
+        val timeoutMillis = campaignTimeoutMillis(configuration, externalDeadlineEpochMillis, publicationReserveMillis)
+        val deadline = if (timeoutMillis > 0) WitnessReplayDeadline(timeoutMillis = timeoutMillis) else null
         requireValid(validatePropertyDefinition(property))
 
         var usedConfiguration = configuration
@@ -133,6 +162,8 @@ class PropertyCampaignRunner(
         )
 
         try {
+            if (deadline == null) return result(PropertyCampaignStop.DEADLINE)
+
             val root = sourceRoot.toRealPath()
             if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE)
 
@@ -259,6 +290,20 @@ class PropertyCampaignRunner(
         completedInputLimit = completedInputLimit,
     ).result
 
+    private fun campaignTimeoutMillis(
+        configuration: PropertyRunConfiguration,
+        externalDeadlineEpochMillis: Long?,
+        publicationReserveMillis: Long,
+    ): Long {
+        if (externalDeadlineEpochMillis == null) return configuration.timeoutMillis
+
+        val remaining = Duration.between(Instant.now(), Instant.ofEpochMilli(externalDeadlineEpochMillis))
+            .minusMillis(publicationReserveMillis)
+        if (remaining.isNegative || remaining.isZero) return 0
+
+        return minOf(remaining, Duration.ofMillis(configuration.timeoutMillis)).toMillis()
+    }
+
     private fun validateControls(
         mode: PropertyCampaignMode,
         configuration: PropertyRunConfiguration,
@@ -303,8 +348,8 @@ class PropertyCampaignRunner(
         pbtAllocationMillis: Long?,
     ): Result<PropertyRunResult> {
         val allocation = pbtAllocationMillis?.coerceAtMost(deadline.remainingMillis())
-        val generationDeadline = allocation?.let { WitnessReplayDeadline(timeoutMillis = it.coerceAtLeast(1)) }
-            ?: deadline
+        val generationDeadline = allocation?.takeIf { it > 0 }
+            ?.let { WitnessReplayDeadline(timeoutMillis = it) } ?: deadline
         val generationConfiguration = configuration.copy(
             timeoutMillis = allocation?.coerceAtLeast(1) ?: configuration.timeoutMillis,
         )

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

@@ -26,6 +26,8 @@ internal data class CampaignFileRequest(
     val completedInputLimit: Int = 0,
     val shrinkWitness: Boolean = false,
     val nodeExecutable: String = "node",
+    val externalDeadlineEpochMillis: Long? = null,
+    val publicationReserveMillis: Long = 0,
 )
 
 internal fun runCampaignFile(
@@ -52,6 +54,8 @@ internal fun runCampaignFile(
         pbtAllocationMillis = request.pbtAllocationMillis,
         shrinkWitness = request.shrinkWitness,
         completedInputLimit = request.completedInputLimit,
+        externalDeadlineEpochMillis = request.externalDeadlineEpochMillis,
+        publicationReserveMillis = request.publicationReserveMillis,
     )
 
     val json = PropertyManifestJson.json.encodeToUtf8SafeString(artifact)

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

@@ -222,6 +222,46 @@ class PropertyCampaignRunnerTest {
         assertTrue(result.elapsedMillis < 5_000, "A 100 ms campaign acquired a fresh backend timeout")
     }
 
+    @Test
+    fun `external cutoff does not renew the original campaign timeout`() {
+        val hanging = property().copy(predicate = TypeScriptEntryPoint(module = MODULE, exportName = "hangs"))
+        val original = configuration.copy(timeoutMillis = 100)
+
+        val artifact = runner.runArtifact(
+            property = hanging,
+            mode = PropertyCampaignMode.PBT_ONLY,
+            configuration = original,
+            externalDeadlineEpochMillis = Long.MAX_VALUE,
+        )
+
+        assertEquals(original, artifact.configuration)
+        assertEquals(PropertyCampaignStop.DEADLINE, artifact.result.stop)
+        assertNull(artifact.result.symbolic)
+        assertTrue(artifact.result.elapsedMillis < 5_000, "External cutoff renewed the 100 ms request timeout")
+    }
+
+    @Test
+    fun `external cutoff shortens execution without invalidating the original PBT allocation`() {
+        val hanging = property().copy(predicate = TypeScriptEntryPoint(module = MODULE, exportName = "hangs"))
+        val allocationMillis = 5_000L
+        val cutoffEpochMillis = System.currentTimeMillis() + 500
+
+        val artifact = runner.runArtifact(
+            property = hanging,
+            mode = PropertyCampaignMode.SEQUENTIAL,
+            configuration = configuration,
+            validationReserveMillis = 1,
+            pbtAllocationMillis = allocationMillis,
+            externalDeadlineEpochMillis = cutoffEpochMillis,
+        )
+
+        assertEquals(configuration, artifact.configuration)
+        assertEquals(allocationMillis, artifact.pbtAllocationMillis)
+        assertEquals(PropertyCampaignStop.DEADLINE, artifact.result.stop)
+        assertNull(artifact.result.symbolic)
+        assertTrue(artifact.result.elapsedMillis < 5_000, "Caller cutoff acquired a new full PBT allocation")
+    }
+
     @Test
     fun `the backend does not reset an already consumed caller deadline`() {
         val deadline = WitnessReplayDeadline(timeoutMillis = 1)

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

@@ -1,11 +1,16 @@
 package org.usvm.ts.pbt.cli
 
 import kotlinx.serialization.decodeFromString
+import kotlinx.serialization.json.JsonObject
+import kotlinx.serialization.json.JsonPrimitive
+import kotlinx.serialization.json.jsonObject
 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.campaign.PropertyCampaignPhase
+import org.usvm.ts.pbt.campaign.PropertyCampaignStop
 import org.usvm.ts.pbt.manifest.PropertyManifestJson
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.PropertyDefinition
@@ -20,6 +25,7 @@ import java.nio.file.Files
 import java.nio.file.Path
 import kotlin.test.assertEquals
 import kotlin.test.assertFalse
+import kotlin.test.assertNull
 import kotlin.test.assertTrue
 
 class CampaignFileCliTest {
@@ -115,6 +121,74 @@ class CampaignFileCliTest {
         assertEquals(37, artifact.configuration.seed)
     }
 
+    @Test
+    fun `expired external cutoff retains original controls without starting an engine`() {
+        val request = request(mode = PropertyCampaignMode.SEQUENTIAL).copy(
+            pbtAllocationMillis = 5_000,
+            completedInputLimit = 3,
+            nodeExecutable = directory.resolve("missing-node").toString(),
+        )
+
+        val artifact = runWithExternalDeadline(request, deadlineEpochMillis = 1, publicationReserveMillis = 1_000)
+
+        assertEquals(request.property, artifact.property)
+        assertEquals(request.configuration, artifact.configuration)
+        assertEquals(request.pbtAllocationMillis, artifact.pbtAllocationMillis)
+        assertEquals(request.completedInputLimit, artifact.completedInputLimit)
+        assertEquals(PropertyCampaignStop.DEADLINE, artifact.result.stop)
+        assertEquals(PropertyCampaignPhase.PREPARATION, artifact.result.stoppedAt)
+        assertNull(artifact.result.concrete)
+        assertNull(artifact.result.symbolic)
+        assertNull(artifact.result.confirmation)
+        assertNull(artifact.metadata)
+    }
+
+    @Test
+    fun `publication reserve can consume all remaining time without arithmetic overflow`() {
+        val request = request(mode = PropertyCampaignMode.PBT_ONLY).copy(
+            nodeExecutable = directory.resolve("missing-node").toString(),
+        )
+
+        val artifact = runWithExternalDeadline(
+            request,
+            deadlineEpochMillis = Long.MAX_VALUE,
+            publicationReserveMillis = Long.MAX_VALUE,
+        )
+
+        assertEquals(PropertyCampaignStop.DEADLINE, artifact.result.stop)
+        assertEquals(PropertyCampaignPhase.PREPARATION, artifact.result.stoppedAt)
+        assertNull(artifact.result.concrete)
+        assertNull(artifact.metadata)
+    }
+
+    private fun runWithExternalDeadline(
+        request: CampaignFileRequest,
+        deadlineEpochMillis: Long,
+        publicationReserveMillis: Long,
+    ): PropertyCampaignArtifact {
+        val requestFields = PropertyManifestJson.json.parseToJsonElement(
+            PropertyManifestJson.json.encodeToUtf8SafeString(request),
+        ).jsonObject
+        val json = JsonObject(
+            requestFields + mapOf(
+                "externalDeadlineEpochMillis" to JsonPrimitive(deadlineEpochMillis),
+                "publicationReserveMillis" to JsonPrimitive(publicationReserveMillis),
+            ),
+        )
+        val path = directory.resolve("request.json")
+        val destination = directory.resolve("artifact.json")
+        Files.writeString(path, json.toString())
+        val output = StringBuilder()
+        val errors = StringBuilder()
+
+        val exit = runCampaignFile(arrayOf(path.toString(), destination.toString()), output, errors)
+
+        assertEquals(2, exit)
+        assertEquals("", errors.toString())
+        assertEquals(Files.readString(destination), output.toString().trim())
+        return PropertyCampaignArtifact.read(destination)
+    }
+
     private fun request(mode: PropertyCampaignMode) = CampaignFileRequest(
         sourceRoot = testResourcesRoot().resolve("properties/campaign").toString(),
         property = PropertyDefinition(