diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt index 346b5564db..66dff1e9b9 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt +++ b/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,7 +87,34 @@ 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" @@ -94,7 +122,8 @@ class PropertyCampaignRunner( 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 { 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, ) 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 index 52427582cc..ea9cac84c3 100644 --- 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 @@ -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) diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunnerTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunnerTest.kt index 0f9b338b10..a2f47446b3 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunnerTest.kt +++ b/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) 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 index 543e9df775..e53a367ec8 100644 --- 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 @@ -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(