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 66dff1e9b9..dba43ec4fd 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 @@ -29,6 +29,7 @@ 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.UsvmCompletedInput import org.usvm.ts.pbt.usvm.UsvmCoverageFeedback import org.usvm.ts.pbt.usvm.UsvmPropertySearchResult import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus @@ -226,6 +227,7 @@ class PropertyCampaignRunner( null }, completedInputLimit = completedInputLimit, + onCompletedInput = inputReplays?.let { it::captureForValidation }, ) if (symbolic == null) return result(PropertyCampaignStop.DEADLINE) @@ -408,6 +410,7 @@ class PropertyCampaignRunner( validationReserveMillis: Long, feedback: UsvmCoverageFeedback?, completedInputLimit: Int, + onCompletedInput: ((UsvmCompletedInput) -> Unit)?, ): UsvmPropertySearchResult? { if (deadline.remainingMillis() <= validationReserveMillis) return null @@ -430,6 +433,7 @@ class PropertyCampaignRunner( deadlineReached = { deadline.remainingMillis() <= validationReserveMillis }, coverageFeedback = feedback, completedInputLimit = completedInputLimit, + onCompletedInput = onCompletedInput, ) } diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplay.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplay.kt index 4daedaabca..966b61c7fa 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplay.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplay.kt @@ -78,6 +78,15 @@ internal class SymbolicInputReplayCollector( var timedOut: Boolean = false private set + fun captureForValidation(input: UsvmCompletedInput) { + // A fault must reach canonical confirmation before optional input coverage consumes its budget. + if (input.expectedOutcome != WitnessOracleOutcome.HOLDS) return + if (deadline.remainingMillis() <= validationReserveMillis) return + + // The search cutoff already reserves validation time; do not subtract it from this operation again. + replay(input.inputs, reserveMillis = 0) + } + fun replayForGuidance(inputs: List): WitnessNativeReplay? { val record = replay(inputs, reserveMillis = validationReserveMillis) ?: return null return if (record.completedWithinDeadline) { diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplayTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplayTest.kt index 4a9dfdb02b..740b809f38 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplayTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplayTest.kt @@ -91,6 +91,7 @@ class SymbolicInputReplayTest { assertTrue(rawFaults.isNotEmpty(), artifact.toString()) assertTrue(rawFaults.all { it.admittedCoverage == null }) assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, artifact.result.confirmation?.status) + assertEquals(artifact.result.symbolic?.inputs, artifact.result.confirmation?.candidate?.inputs) val faultCoverage = assertNotNull(artifact.result.confirmation?.originalReplay?.coverage) assertTrue(faultCoverage.files.any { it.path.endsWith("CompletedSubject.ts") }) assertTrue(artifact.result.confirmedViolation) @@ -181,6 +182,122 @@ class SymbolicInputReplayTest { assertNotNull(collector.replays.single().admittedCoverage) } + @Test + fun `live validation uses the remaining deadline and is reused after the search reserve cutoff`() { + val log = directory.resolve("calls.txt") + val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString()) + writePredicate( + """ + import { appendFileSync } from 'node:fs'; + export function holds(value: number): boolean { + appendFileSync($logLiteral, String(value) + '\n'); + const until = Date.now() + 750; + while (Date.now() < until) {} + return true; + } + """.trimIndent(), + ) + val deadline = WitnessReplayDeadline(timeoutMillis = 8_000) + val collector = collector(deadline = deadline, validationReserveMillis = 7_000) + val input = completion(value = 1.0) + + collector.captureForValidation(input) + val guidanceReplay = collector.replayForGuidance(input.inputs) + collector.collect(listOf(input, input)) + + assertTrue(deadline.remainingMillis() < 7_000) + assertEquals(listOf("1", "1"), Files.readAllLines(log)) + assertEquals(WitnessOracleOutcome.HOLDS, guidanceReplay?.outcome) + assertEquals(1, collector.replays.size) + assertNotNull(collector.replays.single().admittedCoverage) + assertFalse(collector.timedOut) + } + + @Test + fun `live validation leaves fault inputs to canonical confirmation and preserves grouped predictions`() { + val log = directory.resolve("calls.txt") + val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString()) + writePredicate( + """ + import { appendFileSync } from 'node:fs'; + export function holds(value: number): boolean { + appendFileSync($logLiteral, String(value) + '\n'); + return true; + } + """.trimIndent(), + ) + val collector = collector() + val healthy = completion(value = 1.0) + val fault = healthy.copy(expectedOutcome = WitnessOracleOutcome.FALSE) + + collector.captureForValidation(fault) + + assertFalse(Files.exists(log)) + + collector.captureForValidation(healthy) + collector.collect(listOf(healthy, fault)) + + assertEquals(listOf("1", "1"), Files.readAllLines(log)) + val replay = collector.replays.single() + assertEquals(setOf(WitnessOracleOutcome.HOLDS, WitnessOracleOutcome.FALSE), replay.predictedOutcomes) + assertEquals("symbolic.native.oracle-mismatch", replay.replay.diagnostic) + assertNull(replay.admittedCoverage) + } + + @Test + fun `a capture after the search cutoff remains available for final validation`() { + val log = directory.resolve("calls.txt") + val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString()) + writePredicate( + """ + import { appendFileSync } from 'node:fs'; + export function holds(value: number): boolean { + appendFileSync($logLiteral, String(value) + '\n'); + return true; + } + """.trimIndent(), + ) + val collector = collector(validationReserveMillis = 30_000) + val input = completion(value = 1.0) + + collector.captureForValidation(input) + + assertFalse(Files.exists(log)) + + collector.collect(listOf(input)) + + assertEquals(listOf("1", "1"), Files.readAllLines(log)) + assertNotNull(collector.replays.single().admittedCoverage) + } + + @Test + fun `live validation preserves unknown native receipts for final collection`() { + val log = directory.resolve("calls.txt") + val logLiteral = PropertyManifestJson.json.encodeToUtf8SafeString(log.toString()) + writePredicate( + """ + import { appendFileSync } from 'node:fs'; + let calls = 0; + export function holds(value: number): boolean { + appendFileSync($logLiteral, String(value) + '\n'); + return ++calls === 1; + } + """.trimIndent(), + ) + val collector = collector() + val input = completion(value = 1.0) + + collector.captureForValidation(input) + collector.collect(listOf(input)) + + val replay = collector.replays.single() + assertEquals(listOf("1", "1"), Files.readAllLines(log)) + assertTrue(replay.replay.diagnostic?.contains("nondeterministic") == true) + assertEquals(setOf(WitnessOracleOutcome.HOLDS), replay.predictedOutcomes) + assertNull(replay.admittedCoverage) + assertNotNull(collector.diagnostic) + } + @Test fun `source drift rejects native evidence without replacing its original snapshot`() { writePredicate("export function holds(value: number): boolean { return value === value; }") @@ -234,6 +351,7 @@ class SymbolicInputReplayTest { private fun collector( deadline: WitnessReplayDeadline = WitnessReplayDeadline(timeoutMillis = 30_000), + validationReserveMillis: Long = 0, ): SymbolicInputReplayCollector { val property = property(exportName = "holds").copy( predicate = TypeScriptEntryPoint(module = "predicate.ts", exportName = "holds"), @@ -251,7 +369,7 @@ class SymbolicInputReplayTest { sources = sources, coverageRequest = PropertyCoverageRequest(admittedOnly = true), deadline = deadline, - validationReserveMillis = 0, + validationReserveMillis = validationReserveMillis, limit = 8, ) } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 17e5941de7..6a47c5a953 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -62,6 +62,24 @@ class UsvmPropertySearcher( deadlineReached: (() -> Boolean)? = null, coverageFeedback: UsvmCoverageFeedback? = null, completedInputLimit: Int = 0, + ): UsvmPropertySearchResult = search( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + deadlineReached = deadlineReached, + coverageFeedback = coverageFeedback, + completedInputLimit = completedInputLimit, + onCompletedInput = null, + ) + + fun search( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + deadlineReached: (() -> Boolean)?, + coverageFeedback: UsvmCoverageFeedback?, + completedInputLimit: Int, + onCompletedInput: ((UsvmCompletedInput) -> Unit)?, ): UsvmPropertySearchResult { require(completedInputLimit >= 0) { "Completed input limit must not be negative" } val capability = capabilityResolver.resolve( @@ -111,6 +129,7 @@ class UsvmPropertySearcher( deadlineReached = deadlineReached ?: this.deadlineReached, guidance = guidance, completedInputLimit = completedInputLimit, + onCompletedInput = onCompletedInput, ).copy(edgeGuidance = guidance?.snapshot()) } @@ -122,6 +141,7 @@ class UsvmPropertySearcher( deadlineReached: (() -> Boolean)?, guidance: UsvmEdgeGuidance?, completedInputLimit: Int, + onCompletedInput: ((UsvmCompletedInput) -> Unit)?, ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection val completedInputs = linkedSetOf() @@ -149,8 +169,9 @@ class UsvmPropertySearcher( } if (inputs != null) { if (capture) { - val expected = completedOutcome(violation) - completedInputs += UsvmCompletedInput(inputs = inputs, expectedOutcome = expected) + val input = UsvmCompletedInput(inputs = inputs, expectedOutcome = completedOutcome(violation)) + val added = completedInputs.add(input) + if (added) onCompletedInput?.invoke(input) } guidance?.confirm(replayState, inputs, expectsViolation = violation != null) } diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt index bee127d202..63927759f0 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt @@ -10,6 +10,7 @@ import org.usvm.UMachineOptions import org.usvm.machine.TsOptions import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.WitnessOracleOutcome import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.model.ArrayDomain @@ -355,6 +356,52 @@ class UsvmPropertySearcherTest { assertNull(result.inputs) } + @Test + fun `completed input validation can exhaust the caller budget before another path runs`() { + val manifest = manifest(predicateExport = "branchingValidProperty") + val captured = mutableListOf() + var deadlineReached = false + + val result = searcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + deadlineReached = { deadlineReached }, + coverageFeedback = null, + completedInputLimit = 8, + onCompletedInput = { input -> + captured += input + deadlineReached = true + }, + ) + + assertEquals(UsvmPropertySearchStatus.TIMEOUT, result.status) + assertEquals(1, captured.size) + assertEquals(captured, result.completedInputs) + assertEquals(WitnessOracleOutcome.HOLDS, captured.single().expectedOutcome) + assertEquals(0, result.omittedCompletedInputs) + } + + @Test + fun `disabled completed input capture never invokes validation`() { + val manifest = manifest(predicateExport = "branchingValidProperty") + val captured = mutableListOf() + + val result = searcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + deadlineReached = null, + coverageFeedback = null, + completedInputLimit = 0, + onCompletedInput = { captured += it }, + ) + + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + assertTrue(captured.isEmpty()) + assertTrue(result.completedInputs.isEmpty()) + } + private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search( manifest = manifest, mapping = mapper.map(manifest), diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts index f196473103..d70f1586bd 100644 --- a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts @@ -2,6 +2,12 @@ export function validProperty(value: number): boolean { return value === value; } +export function branchingValidProperty(value: number): boolean { + if (value < 0) return true; + + return value === value; +} + export function violatedProperty(value: number): boolean { return value !== 2; }