diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt index f575a1071f..f4b5a58a94 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt @@ -4,6 +4,7 @@ import org.junit.jupiter.api.io.TempDir import org.usvm.SolverType import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.NumberDomain @@ -219,28 +220,41 @@ class CallsClassDataRegistryOracleTest { constructorInputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)), ) - val result = CurrentTsCallsClassCoverageEngine().search( - CallsClassSearchRequest( - harness = harness, - profile = CallsExperimentProfile.EMPTY_STOP, - frozenModelIds = emptySet(), - expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision, - seed = 1, - budget = 3.seconds, - timeQuantum = 100.milliseconds, - solverQueryLimit = 1.seconds, - solverType = SolverType.YICES, - candidateCap = 20, - requireEntryPointWitness = true, - ), - ) + // Coverage-directed search need not enumerate every input model for each entry point. + val branchInputs = listOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)) + val candidates = branchInputs.flatMap { flag -> + val inputs = listOf(PropertyInput(name = "flag", domain = ConstantDomain(flag))) + val branchHarness = harness.copy( + surface = harness.surface.copy(constructorInputs = inputs), + functions = harness.functions.map { it.copy(inputs = inputs) }, + ) + val result = CurrentTsCallsClassCoverageEngine().search( + CallsClassSearchRequest( + harness = branchHarness, + profile = CallsExperimentProfile.EMPTY_STOP, + frozenModelIds = emptySet(), + expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision, + seed = 1, + budget = 3.seconds, + timeQuantum = 100.milliseconds, + solverQueryLimit = 1.seconds, + solverType = SolverType.YICES, + candidateCap = 20, + requireEntryPointWitness = true, + ), + ) + + val scenarioIds = result.search.candidates.map { it.entryPointId }.toSet() + assertEquals(harness.scenarios.map { it.id }.toSet(), scenarioIds, "flag=$flag") + result.search.candidates.forEach { assertEquals(listOf(flag), it.inputs) } + result.search.candidates + } val constructorScenarioId = harness.scenarios.first().id - val constructorBranches = result.search.candidates.filter { it.entryPointId == constructorScenarioId } + val constructorBranches = candidates.filter { it.entryPointId == constructorScenarioId } .map { it.inputs.single() }.toSet() assertEquals(setOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)), constructorBranches) - assertEquals(harness.scenarios.map { it.id }.toSet(), result.search.candidates.map { it.entryPointId }.toSet()) - for (candidate in result.search.candidates) { + for (candidate in candidates) { val index = harness.scenarios.indexOfFirst { it.id == candidate.entryPointId } val original = OriginalTypeScriptClassReplayer( directory, 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 b72d69dad9..c9b0738fc4 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 @@ -26,6 +26,7 @@ data class PropertyCampaignArtifact( val metadata: PropertyCampaignMetadata? = null, val pbtAllocationMillis: Long? = null, val shrinkWitness: Boolean = true, + val completedInputLimit: Int = 0, ) { init { val resultProperties = listOfNotNull( @@ -33,9 +34,13 @@ data class PropertyCampaignArtifact( result.concrete?.propertyId, result.symbolic?.propertyId, result.confirmation?.candidate?.propertyId, - ) + ) + result.symbolicInputReplays.flatMap { replay -> + listOfNotNull(replay.candidate.propertyId, replay.replay.coverage?.propertyId) + } val sameProperty = resultProperties.all { it == property.id } require(sameProperty) { "Campaign evidence belongs to another property" } + require(completedInputLimit >= 0) + require(result.symbolicInputReplays.size <= completedInputLimit) 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 030451d8f2..346b5564db 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 @@ -19,7 +19,6 @@ 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 @@ -63,6 +62,7 @@ data class PropertyCampaignResult( val stoppedAt: PropertyCampaignPhase?, val elapsedMillis: Long, val diagnostic: String?, + val symbolicInputReplays: List = emptyList(), ) { val confirmedViolation: Boolean get() = concrete?.failure?.kind == PropertyFailureKind.PROPERTY || @@ -76,7 +76,8 @@ class PropertyCampaignRunner( private val nodeExecutable: String = "node", private val machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), ) { - /** Captures the requested direct controls and their actual result without repeating execution. */ + /** Keeps phase transitions and retained partial results under the same deadline. */ + @Suppress("LongMethod") fun runArtifact( property: PropertyDefinition, mode: PropertyCampaignMode, @@ -84,7 +85,12 @@ class PropertyCampaignRunner( validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS, pbtAllocationMillis: Long? = null, shrinkWitness: Boolean = true, + completedInputLimit: Int = 0, ): PropertyCampaignArtifact { + 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() @@ -98,6 +104,7 @@ class PropertyCampaignRunner( var concrete: PropertyRunResult? = null var symbolic: UsvmPropertySearchResult? = null var confirmation: WitnessEvidenceDelta? = null + var inputReplays: SymbolicInputReplayCollector? = null fun result( stop: PropertyCampaignStop = PropertyCampaignStop.COMPLETED, @@ -108,12 +115,14 @@ class PropertyCampaignRunner( validationReserveMillis = validationReserveMillis, pbtAllocationMillis = pbtAllocationMillis, shrinkWitness = shrinkWitness, + completedInputLimit = completedInputLimit, result = PropertyCampaignResult( propertyId = property.id, mode = mode, concrete = concrete, symbolic = symbolic, confirmation = confirmation, + symbolicInputReplays = inputReplays?.replays.orEmpty(), stop = stop, stoppedAt = phase.takeUnless { stop == PropertyCampaignStop.COMPLETED }, elapsedMillis = (System.nanoTime() - startedAt) / NANOS_PER_MILLISECOND, @@ -133,7 +142,9 @@ 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) + usedConfiguration = evidenceConfiguration( + configuration, requireNotNull(metadata).sources, guided, captureNative = completedInputLimit > 0, + ) if (mode != PropertyCampaignMode.SYMBOLIC_ONLY) { phase = PropertyCampaignPhase.PBT @@ -163,38 +174,47 @@ class PropertyCampaignRunner( } val sources = captureSources(property, root) + val coverageRequest = usedConfiguration.coverageRequest ?: PropertyCoverageRequest() + if (guided || completedInputLimit > 0) { + inputReplays = SymbolicInputReplayCollector( + property, backend, root, sources, coverageRequest.copy(admittedOnly = true), + deadline, validationReserveMillis, limit = completedInputLimit, + ) + } symbolic = search( property = property, root = root, deadline = deadline, validationReserveMillis = validationReserveMillis, feedback = if (guided) { - coverageFeedback( - property, concrete, backend, sources, usedConfiguration, deadline, validationReserveMillis, + UsvmCoverageFeedback( + initialCoverage = concrete?.coverage, + nativeReplay = requireNotNull(inputReplays)::replayForGuidance, ) } else { null }, + completedInputLimit = completedInputLimit, ) if (symbolic == null) return result(PropertyCampaignStop.DEADLINE) - val searchTimedOut = symbolic.status == UsvmPropertySearchStatus.TIMEOUT - if (symbolic.target == null) { - val stop = if (searchTimedOut) PropertyCampaignStop.DEADLINE else PropertyCampaignStop.COMPLETED - return result(stop) - } - - phase = PropertyCampaignPhase.CONFIRMATION - confirmation = confirm( - backend, property, symbolic, sources, usedConfiguration, deadline, - validationReserveMillis, shrinkWitness, - ) - - return if (confirmation.status == WitnessReplayStatus.TIMEOUT) { - result(PropertyCampaignStop.DEADLINE) - } else { - result() + val hasNativeWork = symbolic.target != null || symbolic.completedInputs.isNotEmpty() + if (hasNativeWork) phase = PropertyCampaignPhase.CONFIRMATION + if (symbolic.target != null) { + confirmation = confirm( + backend, property, symbolic, inputReplays?.sources ?: sources, usedConfiguration, deadline, + validationReserveMillis, shrinkWitness, + ) } + inputReplays?.collect(symbolic.completedInputs) + phaseDiagnostic = listOfNotNull(phaseDiagnostic, inputReplays?.diagnostic) + .joinToString(separator = "; ").takeIf(String::isNotEmpty) + + val expired = symbolic.status == UsvmPropertySearchStatus.TIMEOUT || + confirmation?.status == WitnessReplayStatus.TIMEOUT || inputReplays?.timedOut == true || + deadline.remainingMillis() <= 0 + val stop = if (expired) PropertyCampaignStop.DEADLINE else PropertyCampaignStop.COMPLETED + return result(stop) } catch (error: PbtBackendException) { val stop = if (error.kind == BackendErrorKind.TIMEOUT) { PropertyCampaignStop.DEADLINE @@ -228,6 +248,7 @@ class PropertyCampaignRunner( validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS, pbtAllocationMillis: Long? = null, shrinkWitness: Boolean = true, + completedInputLimit: Int = 0, ): PropertyCampaignResult = runArtifact( property = property, mode = mode, @@ -235,6 +256,7 @@ class PropertyCampaignRunner( validationReserveMillis = validationReserveMillis, pbtAllocationMillis = pbtAllocationMillis, shrinkWitness = shrinkWitness, + completedInputLimit = completedInputLimit, ).result private fun validateControls( @@ -258,16 +280,18 @@ class PropertyCampaignRunner( configuration: PropertyRunConfiguration, sources: List, guided: Boolean, + captureNative: Boolean, ): PropertyRunConfiguration { - if (!guided) return configuration + if (!guided && !captureNative) return configuration val request = configuration.coverageRequest ?: PropertyCoverageRequest() return configuration.copy( coverageRequest = request.copy(admittedOnly = true), - observationRequest = configuration.observationRequest ?: PropertyObservationRequest( - points = emptyList(), - sources = sources, - ), + observationRequest = if (guided) { + configuration.observationRequest ?: PropertyObservationRequest(points = emptyList(), sources = sources) + } else { + configuration.observationRequest + }, ) } @@ -338,6 +362,7 @@ class PropertyCampaignRunner( deadline: WitnessReplayDeadline, validationReserveMillis: Long, feedback: UsvmCoverageFeedback?, + completedInputLimit: Int, ): UsvmPropertySearchResult? { if (deadline.remainingMillis() <= validationReserveMillis) return null @@ -359,6 +384,7 @@ class PropertyCampaignRunner( concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), deadlineReached = { deadline.remainingMillis() <= validationReserveMillis }, coverageFeedback = feedback, + completedInputLimit = completedInputLimit, ) } @@ -386,37 +412,6 @@ class PropertyCampaignRunner( } } - 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() 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 new file mode 100644 index 0000000000..4daedaabca --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplay.kt @@ -0,0 +1,178 @@ +package org.usvm.ts.pbt.campaign + +import kotlinx.serialization.Serializable +import kotlinx.serialization.decodeFromString +import org.usvm.ts.pbt.FastCheckDiagnosticCode +import org.usvm.ts.pbt.backend.ExternalWitnessCandidate +import org.usvm.ts.pbt.backend.PropertyCoverageArtifact +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.WitnessAdmission +import org.usvm.ts.pbt.backend.WitnessNativeReplay +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReplayDeadline +import org.usvm.ts.pbt.backend.WitnessTarget +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.coverage.captureCoverageIdentity +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmCompletedInput +import java.io.IOException +import java.nio.file.Path +import kotlin.time.TimeSource + +/** One actual fixed-input operation; a native false/exception remains separate from fault confirmation. */ +@Serializable +data class SymbolicInputReplay( + val candidate: ExternalWitnessCandidate, + val replay: WitnessNativeReplay, + val elapsedMillis: Long, + val completedWithinDeadline: Boolean, + val predictedOutcomes: Set = emptySet(), +) { + /** Only an admitted, repeatable, fresh and timely native receipt contributes coverage. */ + val admittedCoverage: PropertyCoverageArtifact? + get() { + val coverage = replay.coverage ?: return null + val matchesPrediction = predictedOutcomes == setOf(WitnessOracleOutcome.HOLDS) && + replay.outcome == WitnessOracleOutcome.HOLDS + val exact = coverage.identity != null && coverage.provenance.request.admittedOnly && + coverage.admittedInvocations == 1 && coverage.propertyId == candidate.propertyId + val admitted = completedWithinDeadline && replay.admission == WitnessAdmission.ADMITTED && + matchesPrediction && exact && replay.diagnostic == null + return if (admitted) coverage else null + } +} + +/** Owns immutable input snapshots and the bounded same-phase cache shared by capture and edge guidance. */ +internal class SymbolicInputReplayCollector( + private val property: PropertyDefinition, + private val backend: FastCheckBackend, + root: Path, + sources: List, + private val coverageRequest: PropertyCoverageRequest, + private val deadline: WitnessReplayDeadline, + private val validationReserveMillis: Long, + private val limit: Int, +) { + private val identity = if (limit > 0) captureCoverageIdentity(property.toManifest(), listOf(root)) else null + val sources = identity?.sourceSha256?.map { (path, hash) -> + val source = Path.of(path) + require(source.startsWith(root)) { "Native capture source escapes its source root: $path" } + PropertyObservationSource(module = root.relativize(source).toString().replace('\\', '/'), sha256 = hash) + } ?: sources + private val cache = linkedMapOf() + private val completed = mutableListOf() + + val replays: List + get() = completed.toList() + + var diagnostic: String? = null + private set + + var timedOut: Boolean = false + private set + + fun replayForGuidance(inputs: List): WitnessNativeReplay? { + val record = replay(inputs, reserveMillis = validationReserveMillis) ?: return null + return if (record.completedWithinDeadline) { + record.replay + } else { + record.replay.copy(coverage = null, diagnostic = "campaign.native-replay.deadline") + } + } + + fun collect(inputs: List) { + val groups = inputs.groupBy { key(it.inputs) }.values.take(limit) + val selectedKeys = groups.mapTo(hashSetOf()) { key(it.first().inputs) } + cache.keys.retainAll(selectedKeys) + for ((index, group) in groups.withIndex()) { + val record = replay(group.first().inputs, reserveMillis = 0) + if (record == null) { + diagnostic = "Native verification deadline reached; ${groups.size - index} inputs remain unchecked" + timedOut = true + break + } + val predictions = group.mapTo(linkedSetOf()) { it.expectedOutcome } + val native = record.replay + val outcomeMatches = native.outcome in predictions && predictions.size == 1 + val replay = if (native.admission == WitnessAdmission.ADMITTED && !outcomeMatches) { + native.copy(diagnostic = native.diagnostic ?: "symbolic.native.oracle-mismatch") + } else { + native + } + completed += record.copy(replay = replay, predictedOutcomes = predictions) + val operationTimedOut = native.diagnostic?.contains(FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT) == true + if (!record.completedWithinDeadline || operationTimedOut) { + diagnostic = "Native verification deadline reached; ${groups.size - index - 1} inputs remain unchecked" + timedOut = true + break + } + val admitted = replay.admission == WitnessAdmission.ADMITTED && replay.diagnostic == null + if (!admitted) { + diagnostic = "Native input verification incomplete: " + + (replay.diagnostic ?: "${replay.admission}/${replay.outcome}") + } + } + } + + private fun replay(inputs: List, reserveMillis: Long): SymbolicInputReplay? { + val key = key(inputs) + cache[key]?.let { return it } + val remaining = deadline.remainingMillis() - reserveMillis + if (remaining <= 0) return null + + val snapshot = PropertyManifestJson.json.decodeFromString>(key) + val candidate = property.captureWitness( + inputs = snapshot, + target = WitnessTarget(id = property.predicate.exportName), + sources = sources, + provenance = "usvm:completed-input", + ) + val started = TimeSource.Monotonic.markNow() + val operationDeadline = WitnessReplayDeadline(timeoutMillis = remaining) + val native = invoke(candidate, operationDeadline) + val nativeCoverage = native.coverage + val fresh = identity == null || nativeCoverage == null || nativeCoverage.identity == identity + val record = SymbolicInputReplay( + candidate = candidate, + replay = if (fresh) { + native + } else { + native.copy(diagnostic = listOfNotNull(native.diagnostic, "coverage.source.stale").joinToString("; ")) + }, + elapsedMillis = started.elapsedNow().inWholeMilliseconds, + completedWithinDeadline = deadline.remainingMillis() > 0, + ) + if (cache.size < limit) cache[key] = record + return record + } + + private fun invoke( + candidate: ExternalWitnessCandidate, + operationDeadline: WitnessReplayDeadline, + ): WitnessNativeReplay = try { + backend.replayInput(property, candidate, coverageRequest, operationDeadline) + } catch (error: PbtBackendException) { + unavailable("${error.code}: ${error.message}") + } catch (error: IOException) { + unavailable("Native source snapshot failed: ${error.message}") + } catch (error: IllegalArgumentException) { + unavailable("Native input is unsupported: ${error.message}") + } + + private fun unavailable(diagnostic: String) = WitnessNativeReplay( + admission = WitnessAdmission.UNKNOWN, + outcome = WitnessOracleOutcome.UNKNOWN, + targetMatched = false, + diagnostic = diagnostic, + ) + + private fun key(inputs: List): String = + PropertyManifestJson.json.encodeToUtf8SafeString(inputs) +} 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 0af46635f9..6b15b7ed32 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 @@ -30,6 +30,7 @@ internal fun executeCampaign( validationReserveMillis = reserve ?: PropertyCampaignRunner.DEFAULT_VALIDATION_RESERVE_MILLIS, pbtAllocationMillis = options.pbtAllocationMillis, shrinkWitness = options.shrinkWitness, + completedInputLimit = options.completedInputLimit, ) val json = PropertyManifestJson.json.encodeToUtf8SafeString(artifact) 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 f5261ad0cd..64188502d0 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 @@ -41,6 +41,7 @@ internal data class CliOptions( val validationReserveMillis: Long?, val pbtAllocationMillis: Long? = null, val shrinkWitness: Boolean = true, + val completedInputLimit: Int = 0, ) internal class CliUsageException( @@ -129,6 +130,11 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") help = "PBT allocation within a two-phase campaign; required for COVERAGE_FEEDBACK", ).long() + private val completedInputLimit by option( + "--completed-input-limit", + help = "Maximum completed symbolic inputs to verify natively; defaults to disabled", + ).int().default(0) + private val noShrinking by option( "--no-shrinking", help = "Disable native candidate reduction; requires --mode", @@ -178,6 +184,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") validationReserveMillis = validationReserveMillis, pbtAllocationMillis = pbtAllocationMillis, shrinkWitness = !noShrinking, + completedInputLimit = completedInputLimit, ) } @@ -211,7 +218,7 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") private fun requireCampaignControls() { val hasCampaignDetails = artifactFile != null || validationReserveMillis != null || - pbtAllocationMillis != null || noShrinking + pbtAllocationMillis != null || noShrinking || completedInputLimit != 0 val reserve = validationReserveMillis val allocation = pbtAllocationMillis val twoPhase = mode == PropertyCampaignMode.SEQUENTIAL || mode == PropertyCampaignMode.COVERAGE_FEEDBACK @@ -233,6 +240,12 @@ private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-fast-check") message = "A campaign requires exactly one --source-root", path = "sourceRoot", ) + completedInputLimit < 0 || (completedInputLimit > 0 && mode == PropertyCampaignMode.PBT_ONLY) -> + CliUsageException( + code = FastCheckDiagnosticCode.CLI_ARGUMENT_INVALID, + message = "--completed-input-limit must be non-negative and requires a symbolic campaign mode", + path = "completedInputLimit", + ) invalidAllocation || missingAllocation -> CliUsageException( code = FastCheckDiagnosticCode.CLI_ARGUMENT_INVALID, message = "COVERAGE_FEEDBACK requires --pbt-allocation-ms between 1 and the total timeout; " + diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt index d22e536693..fc8d6b189d 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt @@ -46,7 +46,9 @@ internal class FastCheckWitnessCoordinator( val result = replay(property, candidate, requireNotNull(candidate.inputs), deadline, coverageRequest) val native = when (result) { is FastCheckOperationResult.Completed -> result.value - is FastCheckOperationResult.TimedOut -> return unavailableReplay(result.message) + is FastCheckOperationResult.TimedOut -> return unavailableReplay( + "${FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT}: ${result.message}", + ) } val coverage = native.coverage ?: return native val unchanged = identity == captureCoverageIdentity(candidate.manifest, sourceRoots) 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 new file mode 100644 index 0000000000..4a9dfdb02b --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/SymbolicInputReplayTest.kt @@ -0,0 +1,275 @@ +package org.usvm.ts.pbt.campaign + +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReplayDeadline +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.PropertyManifestJson +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.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.testResourcesRoot +import org.usvm.ts.pbt.usvm.UsvmCompletedInput +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import java.nio.file.Files +import java.nio.file.Path +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class SymbolicInputReplayTest { + @TempDir + lateinit var directory: Path + + private val root = testResourcesRoot().resolve("properties/campaign") + private val configuration = PropertyRunConfiguration(timeoutMillis = 60_000) + + @Test + fun `healthy symbolic-only class paths produce checked native source coverage without a fault`() { + val artifact = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = property(exportName = "healthy"), + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + completedInputLimit = 8, + ) + val path = directory.resolve("healthy.json") + + artifact.write(path) + val restored = PropertyCampaignArtifact.read(path) + + assertNull(restored.result.concrete) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, restored.result.symbolic?.status) + val replays = restored.result.symbolicInputReplays + assertTrue(replays.size >= 2, restored.toString()) + assertTrue(replays.all { it.predictedOutcomes == setOf(WitnessOracleOutcome.HOLDS) }) + assertTrue(replays.all { it.replay.outcome == WitnessOracleOutcome.HOLDS }) + val checked = replays.flatMap { assertNotNull(it.admittedCoverage).files } + .filter { it.path.endsWith("CompletedSubject.ts") } + assertTrue(checked.isNotEmpty()) + assertTrue(checked.any { file -> file.statements.any { it.hits > 0 } }) + assertEquals(artifact.result.symbolicInputReplays, replays) + assertFalse(restored.result.confirmedViolation) + + val first = replays.first() + val other = first.copy(candidate = first.candidate.copy(propertyId = PropertyId(value = "other.property"))) + assertFailsWith { + artifact.copy(result = artifact.result.copy(symbolicInputReplays = listOf(other))) + } + val coverage = assertNotNull(first.replay.coverage).copy(propertyId = PropertyId(value = "other.property")) + val wrongCoverage = first.copy(replay = first.replay.copy(coverage = coverage)) + assertFailsWith { + artifact.copy(result = artifact.result.copy(symbolicInputReplays = listOf(wrongCoverage))) + } + } + + @Test + fun `fault inputs remain raw until the separate original confirmation and retain checked fault coverage`() { + val artifact = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = property(exportName = "faulty"), + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + completedInputLimit = 8, + shrinkWitness = false, + ) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, artifact.result.symbolic?.status) + val rawFaults = artifact.result.symbolicInputReplays.filter { it.replay.outcome == WitnessOracleOutcome.FALSE } + assertTrue(rawFaults.isNotEmpty(), artifact.toString()) + assertTrue(rawFaults.all { it.admittedCoverage == null }) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, artifact.result.confirmation?.status) + val faultCoverage = assertNotNull(artifact.result.confirmation?.originalReplay?.coverage) + assertTrue(faultCoverage.files.any { it.path.endsWith("CompletedSubject.ts") }) + assertTrue(artifact.result.confirmedViolation) + } + + @Test + fun `capture cap stops collection while the original healthy search continues`() { + val artifact = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = property(exportName = "healthy"), + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + completedInputLimit = 1, + ) + + val symbolic = assertNotNull(artifact.result.symbolic) + assertEquals(1, symbolic.completedInputs.size) + assertTrue(symbolic.omittedCompletedInputs > 0, symbolic.toString()) + assertEquals(1, artifact.result.symbolicInputReplays.size) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, symbolic.status) + } + + @Test + fun `rejected preconditions never become completed native inputs`() { + val property = property(exportName = "healthy").copy( + precondition = TypeScriptEntryPoint(module = MODULE, exportName = "positive"), + ) + val artifact = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = property, + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + completedInputLimit = 8, + ) + + val inputs = assertNotNull(artifact.result.symbolic).completedInputs + assertTrue(inputs.isNotEmpty()) + assertTrue(inputs.all { (it.inputs.single() as JsConcreteValue.Number).toDouble() > 0 }) + assertTrue(artifact.result.symbolicInputReplays.all { it.admittedCoverage != null }) + } + + @Test + fun `unsupported symbolic capture stays explicit and does not manufacture native coverage`() { + val property = property(exportName = "healthy").copy( + predicate = TypeScriptEntryPoint( + module = MODULE, + exportName = "healthy", + executionKind = ExecutionKind.ASYNC, + ), + ) + + val artifact = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = property, + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + completedInputLimit = 8, + ) + + val symbolic = assertNotNull(artifact.result.symbolic) + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, symbolic.status) + assertTrue(symbolic.diagnostics.isNotEmpty()) + assertTrue(symbolic.completedInputs.isEmpty()) + assertTrue(artifact.result.symbolicInputReplays.isEmpty()) + } + + @Test + fun `immutable inputs and dedup reuse the guidance native operation instead of executing twice`() { + 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 value === value; + } + """.trimIndent(), + ) + val collector = collector() + val mutableInputs = mutableListOf(JsConcreteValue.number(1.0)) + + collector.replayForGuidance(mutableInputs) + mutableInputs[0] = JsConcreteValue.number(2.0) + val original = completion(value = 1.0) + collector.collect(listOf(original, original)) + + assertEquals(listOf("1", "1"), Files.readAllLines(log)) + assertEquals(1, collector.replays.size) + assertEquals(original.inputs, collector.replays.single().candidate.inputs) + assertNotNull(collector.replays.single().admittedCoverage) + } + + @Test + fun `source drift rejects native evidence without replacing its original snapshot`() { + writePredicate("export function holds(value: number): boolean { return value === value; }") + val originalHash = campaignSourceSha256(directory.resolve("predicate.ts")) + val collector = collector() + Files.writeString(directory.resolve("predicate.ts"), "\n", java.nio.file.StandardOpenOption.APPEND) + + collector.collect(listOf(completion(value = 1.0))) + + val replay = collector.replays.single() + assertNull(replay.admittedCoverage) + assertTrue(replay.replay.diagnostic?.contains("source-hash") == true, replay.toString()) + assertTrue(replay.candidate.sources.any { it.sha256 == originalHash }) + assertNotNull(collector.diagnostic) + } + + @Test + fun `nondeterminism and a native oracle mismatch never contribute coverage`() { + writePredicate("let calls = 0; export function holds(value: number): boolean { calls++; return calls === 1; }") + val nondeterministic = collector() + + nondeterministic.collect(listOf(completion(value = 1.0))) + + val nativeReplay = nondeterministic.replays.single() + assertTrue(nativeReplay.replay.diagnostic?.contains("nondeterministic") == true) + assertNull(nativeReplay.admittedCoverage) + + writePredicate("export function holds(value: number): boolean { return false; }") + val mismatch = collector() + + mismatch.collect(listOf(completion(value = 1.0))) + + assertEquals(WitnessOracleOutcome.FALSE, mismatch.replays.single().replay.outcome) + assertEquals("symbolic.native.oracle-mismatch", mismatch.replays.single().replay.diagnostic) + assertNull(mismatch.replays.single().admittedCoverage) + } + + @Test + fun `expired native budget preserves unchecked inputs and never credits a late receipt`() { + writePredicate("export function holds(value: number): boolean { while (value === value) {} return true; }") + val deadline = WitnessReplayDeadline(timeoutMillis = 500) + val collector = collector(deadline = deadline) + + collector.collect(listOf(completion(value = 1.0), completion(value = 2.0))) + + assertTrue(collector.timedOut) + assertNotNull(collector.diagnostic) + assertTrue(collector.replays.all { it.admittedCoverage == null }) + assertTrue(collector.replays.size <= 1) + } + + private fun collector( + deadline: WitnessReplayDeadline = WitnessReplayDeadline(timeoutMillis = 30_000), + ): SymbolicInputReplayCollector { + val property = property(exportName = "holds").copy( + predicate = TypeScriptEntryPoint(module = "predicate.ts", exportName = "holds"), + ) + val sources = listOf( + PropertyObservationSource( + module = "predicate.ts", + sha256 = campaignSourceSha256(directory.resolve("predicate.ts")), + ), + ) + return SymbolicInputReplayCollector( + property = property, + backend = FastCheckBackend(sourceRoots = listOf(directory)), + root = directory.toRealPath(), + sources = sources, + coverageRequest = PropertyCoverageRequest(admittedOnly = true), + deadline = deadline, + validationReserveMillis = 0, + limit = 8, + ) + } + + private fun property(exportName: String) = PropertyDefinition( + id = PropertyId("completed.$exportName"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = exportName), + ) + + private fun completion(value: Double) = UsvmCompletedInput( + inputs = listOf(JsConcreteValue.number(value)), + expectedOutcome = WitnessOracleOutcome.HOLDS, + ) + + private fun writePredicate(source: String) = directory.resolve("predicate.ts").writeText(source) + + private companion object { + const val MODULE = "CompletedProperties.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 4ee5d6eaa4..4faca0782e 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 @@ -115,6 +115,29 @@ class CampaignCliTest { assertTrue(trace.remainingGoals.isEmpty()) } + @Test + fun `symbolic CLI enables bounded native input capture in the saved artifact`() { + val property = property().copy( + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))), + predicate = TypeScriptEntryPoint(module = "CompletedProperties.ts", exportName = "healthy"), + precondition = null, + ) + val destination = directory.resolve("completed.json") + + val run = runCli( + arguments(PropertyCampaignMode.SYMBOLIC_ONLY, destination) + arrayOf("--completed-input-limit", "3"), + properties = listOf(property), + ) + val artifact = readArtifact(run, destination) + + assertEquals(0, run.exitCode) + assertEquals("", run.errors) + assertEquals(3, artifact.completedInputLimit) + assertTrue(artifact.result.symbolicInputReplays.isNotEmpty()) + assertTrue(artifact.result.symbolicInputReplays.size <= 3) + assertTrue(artifact.result.symbolicInputReplays.all { it.admittedCoverage != null }) + } + @Test fun `completed direct controls with no finding return zero`() { val admittedSingleton = property().copy( @@ -281,6 +304,17 @@ class CampaignCliTest { arrayOf( "--source-root", root, "--mode", "UNKNOWN", "--artifact", destination, ) to "cli.argument.invalid", + arrayOf( + "--source-root", root, "--mode", "PBT_ONLY", "--artifact", destination, + "--completed-input-limit", "1", + ) to "cli.argument.invalid", + arrayOf( + "--source-root", root, "--mode", "SYMBOLIC_ONLY", "--artifact", destination, + "--completed-input-limit", "-1", + ) to "cli.argument.invalid", + arrayOf( + "--source-root", root, "--completed-input-limit", "1", + ) to "cli.campaign.mode.required", ) for ((arguments, expectedCode) in cases) { diff --git a/usvm-ts-fast-check/src/test/resources/properties/campaign/CompletedProperties.ts b/usvm-ts-fast-check/src/test/resources/properties/campaign/CompletedProperties.ts new file mode 100644 index 0000000000..ff46341653 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/campaign/CompletedProperties.ts @@ -0,0 +1,16 @@ +import { BranchingCounter } from './CompletedSubject'; + +export function healthy(value: number): boolean { + const counter = new BranchingCounter(); + counter.value(value); + return true; +} + +export function faulty(value: number): boolean { + const counter = new BranchingCounter(); + return counter.value(value) !== value; +} + +export function positive(value: number): boolean { + return value > 0; +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/campaign/CompletedSubject.ts b/usvm-ts-fast-check/src/test/resources/properties/campaign/CompletedSubject.ts new file mode 100644 index 0000000000..868767c919 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/campaign/CompletedSubject.ts @@ -0,0 +1,9 @@ +export class BranchingCounter { + value(input: number): number { + if (input > 0) { + return 1; + } else { + return 2; + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt index 2576749508..aff55e2db9 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt @@ -2,6 +2,7 @@ package org.usvm.ts.pbt.usvm import kotlinx.serialization.Serializable import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.WitnessOracleOutcome import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyId @@ -27,6 +28,20 @@ enum class UsvmPropertyViolationTarget { ASSERTION_FAILURE, } +/** Predicted completion for one original immutable input; native replay remains a separate observation. */ +@Serializable +data class UsvmCompletedInput( + val inputs: List, + val expectedOutcome: WitnessOracleOutcome, +) { + init { + require( + expectedOutcome == WitnessOracleOutcome.HOLDS || expectedOutcome == WitnessOracleOutcome.FALSE || + expectedOutcome == WitnessOracleOutcome.THREW + ) + } +} + /** Backend-neutral result of searching one mapped TypeScript property with USVM. */ @Serializable data class UsvmPropertySearchResult( @@ -37,8 +52,12 @@ data class UsvmPropertySearchResult( val capability: UsvmPropertyProjectionCapability, val diagnostics: List, val edgeGuidance: UsvmEdgeGuidanceTrace? = null, + val completedInputs: List = emptyList(), + val omittedCompletedInputs: Int = 0, ) { init { + require(omittedCompletedInputs >= 0) + when (status) { UsvmPropertySearchStatus.VIOLATION_REACHED -> { requireNotNull(target) { "A reached violation requires its target" } 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 07f091472b..17e5941de7 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 @@ -24,10 +24,13 @@ import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.backend.CapabilityDiagnostic 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.EtsEntryPointTarget import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyId +import java.util.concurrent.CancellationException import kotlin.random.Random /** Searches mapped TypeScript predicates for concrete property violations with USVM. */ @@ -58,7 +61,9 @@ class UsvmPropertySearcher( concreteCapability: ProjectionCapability, deadlineReached: (() -> Boolean)? = null, coverageFeedback: UsvmCoverageFeedback? = null, + completedInputLimit: Int = 0, ): UsvmPropertySearchResult { + require(completedInputLimit >= 0) { "Completed input limit must not be negative" } val capability = capabilityResolver.resolve( manifest = manifest, mapping = mapping, @@ -105,6 +110,7 @@ class UsvmPropertySearcher( capability = capability, deadlineReached = deadlineReached ?: this.deadlineReached, guidance = guidance, + completedInputLimit = completedInputLimit, ).copy(edgeGuidance = guidance?.snapshot()) } @@ -115,22 +121,42 @@ class UsvmPropertySearcher( capability: UsvmPropertyProjectionCapability, deadlineReached: (() -> Boolean)?, guidance: UsvmEdgeGuidance?, + completedInputLimit: Int, ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection + val completedInputs = linkedSetOf() + val completionDiagnostics = mutableListOf() + var omittedCompletedInputs = 0 val target = UsvmViolationTsTarget() lateinit var observer: UsvmViolationObserver observer = UsvmViolationObserver(target) { state -> - if (guidance != null) { + val methodResult = state.methodResult + val completed = methodResult is TsMethodResult.TsException || + (methodResult is TsMethodResult.Success && methodResult.value.sort == state.ctx.boolSort) + val capture = completed && completedInputLimit > 0 && completedInputs.size < completedInputLimit + if (completed && completedInputLimit > 0 && !capture) omittedCompletedInputs += 1 + if (guidance != null || capture) { val violation = observer.violationStates.lastOrNull { it.pathNode === state.pathNode } val replayState = violation ?: state - val inputs = runCatching { - UsvmCandidateInputResolver(projection.objectShapes).resolve( - replayState, manifest.inputs, projection, + val resolved = resolveCompletedInput(replayState, manifest, projection) + val inputs = resolved.getOrNull() + if (capture && inputs == null) { + completionDiagnostics += diagnostic( + code = "usvm.completed-input.unavailable", + message = resolved.exceptionOrNull()?.message ?: "Original input could not be resolved", + path = "completedInputs", ) - }.getOrNull() - if (inputs != null) guidance.confirm(replayState, inputs, expectsViolation = violation != null) + } + if (inputs != null) { + if (capture) { + val expected = completedOutcome(violation) + completedInputs += UsvmCompletedInput(inputs = inputs, expectedOutcome = expected) + } + guidance?.confirm(replayState, inputs, expectsViolation = violation != null) + } } } + val runtimeLimitations = UsvmRuntimeLimitationObserver() val objectShapes = PlainObjectInputShapes(scene, manifest.inputs.map { it.domain }) val domainProjector = UsvmDomainProjector(projectionOptions, objectShapes) @@ -190,8 +216,36 @@ class UsvmPropertySearcher( runtimeLimited = runtimeDiagnostics.isNotEmpty(), ) - searchResult.copy(diagnostics = (searchResult.diagnostics + runtimeDiagnostics).distinct()) + searchResult.copy( + diagnostics = (searchResult.diagnostics + runtimeDiagnostics + completionDiagnostics).distinct(), + completedInputs = completedInputs.toList(), + omittedCompletedInputs = omittedCompletedInputs, + ) + } + } + + private fun completedOutcome(violation: TsState?): WitnessOracleOutcome = when { + violation?.methodResult is TsMethodResult.TsException -> WitnessOracleOutcome.THREW + violation != null -> WitnessOracleOutcome.FALSE + else -> WitnessOracleOutcome.HOLDS + } + + private fun resolveCompletedInput( + state: TsState, + manifest: PropertyManifest, + projection: UsvmDeclaredDomainProjection, + ): Result> { + val resolved = runCatching { + UsvmCandidateInputResolver(projection.objectShapes).resolve(state, manifest.inputs, projection) + } + val error = resolved.exceptionOrNull() + if (error is CancellationException) throw error + if (error is InterruptedException) { + Thread.currentThread().interrupt() + throw error } + + return resolved } private fun classifyTerminalFailure( @@ -437,7 +491,7 @@ class UsvmPropertySearcher( status: UsvmPropertySearchStatus, capability: UsvmPropertyProjectionCapability, target: UsvmPropertyViolationTarget? = null, - inputs: List? = null, + inputs: List? = null, additionalDiagnostic: CapabilityDiagnostic? = null, ) = UsvmPropertySearchResult( propertyId = PropertyId(manifest.propertyId),