diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts index 83f601790e..2b66a21557 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts +++ b/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'); diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt index ce1287e775..b72d69dad9 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt +++ b/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" } } 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 e18dc3b36a..030451d8f2 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 @@ -11,6 +11,7 @@ import org.usvm.UMachineOptions import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyCoverageRequest import org.usvm.ts.pbt.backend.PropertyFailureKind import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunResult @@ -18,6 +19,7 @@ import org.usvm.ts.pbt.backend.WitnessEvidenceDelta import org.usvm.ts.pbt.backend.WitnessReplayConfiguration import org.usvm.ts.pbt.backend.WitnessReplayDeadline import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessTarget import org.usvm.ts.pbt.backend.captureWitness import org.usvm.ts.pbt.fastcheck.BackendErrorKind import org.usvm.ts.pbt.fastcheck.FastCheckBackend @@ -26,7 +28,9 @@ import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.observation.PropertyObservationRequest import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmCoverageFeedback import org.usvm.ts.pbt.usvm.UsvmPropertySearchResult import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus import org.usvm.ts.pbt.usvm.UsvmPropertySearcher @@ -38,7 +42,7 @@ import java.util.concurrent.CancellationException import kotlin.time.Duration.Companion.milliseconds @Serializable -enum class PropertyCampaignMode { PBT_ONLY, SYMBOLIC_ONLY, SEQUENTIAL } +enum class PropertyCampaignMode { PBT_ONLY, SYMBOLIC_ONLY, SEQUENTIAL, COVERAGE_FEEDBACK } @Serializable enum class PropertyCampaignPhase { PREPARATION, PBT, SYMBOLIC, CONFIRMATION } @@ -65,7 +69,7 @@ data class PropertyCampaignResult( confirmation?.status == WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION } -/** Direct controls over the same original property; coverage and observations are retained without feedback. */ +/** One concrete generation phase followed by the unchanged original-property symbolic query. */ class PropertyCampaignRunner( private val sourceRoot: Path, private val tsconfig: Path? = null, @@ -78,12 +82,17 @@ class PropertyCampaignRunner( mode: PropertyCampaignMode, configuration: PropertyRunConfiguration = PropertyRunConfiguration(), validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS, + pbtAllocationMillis: Long? = null, + shrinkWitness: Boolean = true, ): PropertyCampaignArtifact { - require(validationReserveMillis > 0) { "Validation reserve must be positive" } + validateControls(mode, configuration, validationReserveMillis, pbtAllocationMillis) + val guided = mode == PropertyCampaignMode.COVERAGE_FEEDBACK val startedAt = System.nanoTime() val deadline = WitnessReplayDeadline(timeoutMillis = configuration.timeoutMillis) requireValid(validatePropertyDefinition(property)) + var usedConfiguration = configuration + var phaseDiagnostic: String? = null var metadata: PropertyCampaignMetadata? = null var phase = PropertyCampaignPhase.PREPARATION var concrete: PropertyRunResult? = null @@ -92,11 +101,13 @@ class PropertyCampaignRunner( fun result( stop: PropertyCampaignStop = PropertyCampaignStop.COMPLETED, - diagnostic: String? = null, + diagnostic: String? = phaseDiagnostic, ) = PropertyCampaignArtifact( property = property, - configuration = configuration, + configuration = usedConfiguration, validationReserveMillis = validationReserveMillis, + pbtAllocationMillis = pbtAllocationMillis, + shrinkWitness = shrinkWitness, result = PropertyCampaignResult( propertyId = property.id, mode = mode, @@ -106,7 +117,8 @@ class PropertyCampaignRunner( stop = stop, stoppedAt = phase.takeUnless { stop == PropertyCampaignStop.COMPLETED }, elapsedMillis = (System.nanoTime() - startedAt) / NANOS_PER_MILLISECOND, - diagnostic = diagnostic, + diagnostic = listOfNotNull(phaseDiagnostic, diagnostic).distinct() + .joinToString(separator = "; ").takeIf(String::isNotEmpty), ), metadata = metadata, ) @@ -121,21 +133,27 @@ class PropertyCampaignRunner( val backend = FastCheckBackend(listOf(root), nodeExecutable = nodeExecutable, tsconfig = tsconfig) if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE) + usedConfiguration = evidenceConfiguration(configuration, requireNotNull(metadata).sources, guided) + if (mode != PropertyCampaignMode.SYMBOLIC_ONLY) { phase = PropertyCampaignPhase.PBT - concrete = backend.run(property = property, configuration = configuration, deadline = deadline) - - val coverageTimedOut = coverageCollectionTimedOut(concrete) - if (coverageTimedOut || deadline.remainingMillis() <= 0) { - return result( - stop = PropertyCampaignStop.DEADLINE, - diagnostic = "Concrete result retained after the campaign or coverage collection timed out", - ) + val generation = generate(property, backend, usedConfiguration, deadline, pbtAllocationMillis) + concrete = generation.getOrNull() + phaseDiagnostic = generation.exceptionOrNull()?.let { error -> + "PBT allocation expired: ${error.message}" } - if (concrete.failure?.kind == PropertyFailureKind.PROPERTY) return result() - if (concrete.failure?.kind == PropertyFailureKind.TIMEOUT) { + + if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE) + if (concrete?.failure?.kind == PropertyFailureKind.PROPERTY) return result() + val coverageTimedOut = concrete?.let(::coverageCollectionTimedOut) == true + val generationTimedOut = concrete?.failure?.kind == PropertyFailureKind.TIMEOUT + if ((coverageTimedOut || generationTimedOut) && pbtAllocationMillis == null) { return result(PropertyCampaignStop.DEADLINE) } + if (coverageTimedOut || generationTimedOut) { + phaseDiagnostic = "PBT allocation ended with incomplete evidence; " + + "symbolic search uses the remainder" + } if (mode == PropertyCampaignMode.PBT_ONLY) return result() } @@ -145,39 +163,31 @@ class PropertyCampaignRunner( } val sources = captureSources(property, root) - val frontendBudgetMillis = deadline.remainingMillis() - validationReserveMillis - if (frontendBudgetMillis <= 0) return result(PropertyCampaignStop.DEADLINE) - - val scene = loadScene(root = root, timeoutMillis = frontendBudgetMillis) symbolic = search( property = property, root = root, - scene = scene, deadline = deadline, validationReserveMillis = validationReserveMillis, + feedback = if (guided) { + coverageFeedback( + property, concrete, backend, sources, usedConfiguration, deadline, validationReserveMillis, + ) + } else { + null + }, ) if (symbolic == null) return result(PropertyCampaignStop.DEADLINE) + val searchTimedOut = symbolic.status == UsvmPropertySearchStatus.TIMEOUT if (symbolic.target == null) { - return if (symbolic.status == UsvmPropertySearchStatus.TIMEOUT) { - result(PropertyCampaignStop.DEADLINE) - } else { - result() - } + val stop = if (searchTimedOut) PropertyCampaignStop.DEADLINE else PropertyCampaignStop.COMPLETED + return result(stop) } phase = PropertyCampaignPhase.CONFIRMATION - val candidate = symbolic.captureWitness(property = property, sources = sources) - - confirmation = backend.confirmWitness( - property = property, - candidate = candidate, - configuration = WitnessReplayConfiguration( - timeoutMillis = configuration.timeoutMillis, - validationReserveMillis = validationReserveMillis, - coverageRequest = configuration.coverageRequest, - ), - deadline = deadline, + confirmation = confirm( + backend, property, symbolic, sources, usedConfiguration, deadline, + validationReserveMillis, shrinkWitness, ) return if (confirmation.status == WitnessReplayStatus.TIMEOUT) { @@ -216,7 +226,74 @@ class PropertyCampaignRunner( mode: PropertyCampaignMode, configuration: PropertyRunConfiguration = PropertyRunConfiguration(), validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS, - ): PropertyCampaignResult = runArtifact(property, mode, configuration, validationReserveMillis).result + pbtAllocationMillis: Long? = null, + shrinkWitness: Boolean = true, + ): PropertyCampaignResult = runArtifact( + property = property, + mode = mode, + configuration = configuration, + validationReserveMillis = validationReserveMillis, + pbtAllocationMillis = pbtAllocationMillis, + shrinkWitness = shrinkWitness, + ).result + + private fun validateControls( + mode: PropertyCampaignMode, + configuration: PropertyRunConfiguration, + validationReserveMillis: Long, + pbtAllocationMillis: Long?, + ) { + require(validationReserveMillis > 0) { "Validation reserve must be positive" } + val guided = mode == PropertyCampaignMode.COVERAGE_FEEDBACK + require(!guided || pbtAllocationMillis != null) { "Coverage feedback requires an explicit PBT allocation" } + require(pbtAllocationMillis == null || pbtAllocationMillis in 1 until configuration.timeoutMillis) { + "PBT allocation must be positive and smaller than the total campaign timeout" + } + require(pbtAllocationMillis == null || mode == PropertyCampaignMode.SEQUENTIAL || guided) { + "PBT allocation requires a two-phase campaign" + } + } + + private fun evidenceConfiguration( + configuration: PropertyRunConfiguration, + sources: List, + guided: Boolean, + ): PropertyRunConfiguration { + if (!guided) return configuration + + val request = configuration.coverageRequest ?: PropertyCoverageRequest() + return configuration.copy( + coverageRequest = request.copy(admittedOnly = true), + observationRequest = configuration.observationRequest ?: PropertyObservationRequest( + points = emptyList(), + sources = sources, + ), + ) + } + + private fun generate( + property: PropertyDefinition, + backend: FastCheckBackend, + configuration: PropertyRunConfiguration, + deadline: WitnessReplayDeadline, + pbtAllocationMillis: Long?, + ): Result { + val allocation = pbtAllocationMillis?.coerceAtMost(deadline.remainingMillis()) + val generationDeadline = allocation?.let { WitnessReplayDeadline(timeoutMillis = it.coerceAtLeast(1)) } + ?: deadline + val generationConfiguration = configuration.copy( + timeoutMillis = allocation?.coerceAtLeast(1) ?: configuration.timeoutMillis, + ) + + return try { + Result.success(backend.run(property, generationConfiguration, generationDeadline)) + } catch (error: PbtBackendException) { + val phaseExpired = allocation != null && error.kind == BackendErrorKind.TIMEOUT + if (!phaseExpired) throw error + + Result.failure(error) + } + } private fun captureMetadata(property: PropertyDefinition, root: Path): PropertyCampaignMetadata { val explicitTsconfig = tsconfig?.toRealPath() @@ -258,12 +335,15 @@ class PropertyCampaignRunner( private fun search( property: PropertyDefinition, root: Path, - scene: EtsScene, deadline: WitnessReplayDeadline, validationReserveMillis: Long, + feedback: UsvmCoverageFeedback?, ): UsvmPropertySearchResult? { if (deadline.remainingMillis() <= validationReserveMillis) return null + val scene = loadScene(root, timeoutMillis = deadline.remainingMillis() - validationReserveMillis) + if (deadline.remainingMillis() <= validationReserveMillis) return null + val manifest = property.toManifest() val mapping = PropertyEtsMapper(scene = scene, sourceRoots = listOf(root)).map(manifest) val budgetMillis = deadline.remainingMillis() - validationReserveMillis @@ -278,9 +358,65 @@ class PropertyCampaignRunner( mapping = mapping, concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), deadlineReached = { deadline.remainingMillis() <= validationReserveMillis }, + coverageFeedback = feedback, + ) + } + + private fun confirm( + backend: FastCheckBackend, + property: PropertyDefinition, + symbolic: UsvmPropertySearchResult, + sources: List, + configuration: PropertyRunConfiguration, + deadline: WitnessReplayDeadline, + validationReserveMillis: Long, + shrinkWitness: Boolean, + ): WitnessEvidenceDelta { + val candidate = symbolic.captureWitness(property = property, sources = sources) + val replayConfiguration = WitnessReplayConfiguration( + timeoutMillis = configuration.timeoutMillis, + validationReserveMillis = validationReserveMillis, + coverageRequest = configuration.coverageRequest, + shrink = shrinkWitness, ) + return if (property.assertions.isEmpty()) { + backend.confirmWitness(property, candidate, replayConfiguration, deadline) + } else { + backend.confirmOriginalWitness(property, candidate, replayConfiguration, deadline) + } } + private fun coverageFeedback( + property: PropertyDefinition, + concrete: PropertyRunResult?, + backend: FastCheckBackend, + sources: List, + configuration: PropertyRunConfiguration, + deadline: WitnessReplayDeadline, + validationReserveMillis: Long, + ) = UsvmCoverageFeedback( + initialCoverage = concrete?.coverage, + nativeReplay = { inputs -> + val remainingMillis = deadline.remainingMillis() - validationReserveMillis + if (remainingMillis <= 0) { + null + } else { + val candidate = property.captureWitness( + inputs = inputs, + target = WitnessTarget(id = property.predicate.exportName), + sources = sources, + provenance = "usvm:coverage", + ) + backend.replayInput( + property = property, + candidate = candidate, + coverageRequest = requireNotNull(configuration.coverageRequest), + deadline = WitnessReplayDeadline(timeoutMillis = remainingMillis), + ) + } + }, + ) + private fun captureSources(property: PropertyDefinition, root: Path): List { val modules = listOfNotNull(property.predicate.module, property.precondition?.module).distinct() @@ -292,8 +428,8 @@ class PropertyCampaignRunner( } } - private companion object { + companion object { const val DEFAULT_VALIDATION_RESERVE_MILLIS = 5_000L - const val NANOS_PER_MILLISECOND = 1_000_000L + private const val NANOS_PER_MILLISECOND = 1_000_000L } } diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt index 84d70e5a65..0af46635f9 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/CampaignCli.kt +++ b/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 diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt index fd77b762a6..f5261ad0cd 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt +++ b/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", diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index 4c7b8ca121..c49d05310c 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt +++ b/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) { diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/GuidedPropertyCampaignTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/GuidedPropertyCampaignTest.kt new file mode 100644 index 0000000000..b695ebd58e --- /dev/null +++ b/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, + 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" + } +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt index ef626edbbe..4ee5d6eaa4 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/cli/CampaignCliTest.kt +++ b/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)) } } diff --git a/usvm-ts-fast-check/src/test/resources/properties/campaign/GuidedProperties.ts b/usvm-ts-fast-check/src/test/resources/properties/campaign/GuidedProperties.ts new file mode 100644 index 0000000000..af8ee38d43 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/campaign/GuidedProperties.ts @@ -0,0 +1,24 @@ +import { branch, nested } from './GuidedSubject'; + +export function branchHolds(value: number): boolean { + return branch(value) > 0; +} + +export function nestedHolds(value: number): boolean { + return nested(value) > 0; +} + +export function branchDifferent(value: number): boolean { + return branch(value) !== value; +} + +export async function delayedHolds(value: number): Promise { + await new Promise(resolve => setTimeout(resolve, 10_000)); + return value === value; +} + +export function growthLimit(value: number): boolean { + const array = [1]; + array[value] = 2; + return array.length > 0; +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/campaign/GuidedSubject.ts b/usvm-ts-fast-check/src/test/resources/properties/campaign/GuidedSubject.ts new file mode 100644 index 0000000000..f77cb1f3e8 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/campaign/GuidedSubject.ts @@ -0,0 +1,19 @@ +export function branch(value: number): number { + if (value > 0) { + return 1; + } else { + return 2; + } +} + +export function nested(value: number): number { + if (value > 0) { + if (value === 42) { + return 3; + } else { + return 1; + } + } else { + return 2; + } +}