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 c9b0738fc4..5329188aa7 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 @@ -27,6 +27,7 @@ data class PropertyCampaignArtifact( val pbtAllocationMillis: Long? = null, val shrinkWitness: Boolean = true, val completedInputLimit: Int = 0, + val relationGuidanceControls: PropertyRelationGuidanceControls? = null, ) { init { val resultProperties = listOfNotNull( @@ -36,7 +37,10 @@ data class PropertyCampaignArtifact( result.confirmation?.candidate?.propertyId, ) + result.symbolicInputReplays.flatMap { replay -> listOfNotNull(replay.candidate.propertyId, replay.replay.coverage?.propertyId) - } + } + listOfNotNull(result.relationGuidance?.selection?.inference?.propertyId) + + result.relationGuidance?.attempts.orEmpty().flatMap { attempt -> + listOfNotNull(attempt.witness?.propertyId, attempt.confirmation?.candidate?.propertyId) + } val sameProperty = resultProperties.all { it == property.id } require(sameProperty) { "Campaign evidence belongs to another property" } require(completedInputLimit >= 0) 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 9b1fb0b695..a32f1fa6ba 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 @@ -25,6 +25,7 @@ import org.usvm.ts.pbt.fastcheck.FastCheckBackend import org.usvm.ts.pbt.fastcheck.PbtBackendException import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyId import org.usvm.ts.pbt.observation.PropertyObservationRequest @@ -63,10 +64,14 @@ data class PropertyCampaignResult( val elapsedMillis: Long, val diagnostic: String?, val symbolicInputReplays: List = emptyList(), + val relationGuidance: PropertyRelationGuidanceTrace? = null, ) { val confirmedViolation: Boolean get() = concrete?.failure?.kind == PropertyFailureKind.PROPERTY || - confirmation?.status == WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION + confirmation?.status == WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION || + relationGuidance?.attempts?.any { + it.confirmation?.status == WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION + } == true } /** One concrete generation phase followed by the unchanged original-property symbolic query. */ @@ -86,12 +91,21 @@ class PropertyCampaignRunner( pbtAllocationMillis: Long? = null, shrinkWitness: Boolean = true, completedInputLimit: Int = 0, + relationGuidance: PropertyRelationGuidance? = null, ): 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) + if (relationGuidance != null) { + require(mode == PropertyCampaignMode.SEQUENTIAL || mode == PropertyCampaignMode.COVERAGE_FEEDBACK) { + "Relation guidance requires one PBT phase followed by a symbolic phase" + } + require(relationGuidance.compiled == null || relationGuidance.compiled.definition == property) { + "Retained compiler output belongs to another property" + } + } val guided = mode == PropertyCampaignMode.COVERAGE_FEEDBACK val startedAt = System.nanoTime() val deadline = WitnessReplayDeadline(timeoutMillis = configuration.timeoutMillis) @@ -105,6 +119,7 @@ class PropertyCampaignRunner( var symbolic: UsvmPropertySearchResult? = null var confirmation: WitnessEvidenceDelta? = null var inputReplays: SymbolicInputReplayCollector? = null + var relationTrace: PropertyRelationGuidanceTrace? = null fun result( stop: PropertyCampaignStop = PropertyCampaignStop.COMPLETED, @@ -116,6 +131,7 @@ class PropertyCampaignRunner( pbtAllocationMillis = pbtAllocationMillis, shrinkWitness = shrinkWitness, completedInputLimit = completedInputLimit, + relationGuidanceControls = relationGuidance?.controls(), result = PropertyCampaignResult( propertyId = property.id, mode = mode, @@ -123,6 +139,7 @@ class PropertyCampaignRunner( symbolic = symbolic, confirmation = confirmation, symbolicInputReplays = inputReplays?.replays.orEmpty(), + relationGuidance = relationTrace, stop = stop, stoppedAt = phase.takeUnless { stop == PropertyCampaignStop.COMPLETED }, elapsedMillis = (System.nanoTime() - startedAt) / NANOS_PER_MILLISECOND, @@ -144,6 +161,7 @@ class PropertyCampaignRunner( usedConfiguration = evidenceConfiguration( configuration, requireNotNull(metadata).sources, guided, captureNative = completedInputLimit > 0, + relationGuidance = relationGuidance, ) if (mode != PropertyCampaignMode.SYMBOLIC_ONLY) { @@ -195,7 +213,21 @@ class PropertyCampaignRunner( null }, completedInputLimit = completedInputLimit, + relationChallenger = relationGuidance?.let { guidance -> + { + scene, mapping -> + PropertyRelationChallenger( + scene, mapping, backend, machineOptions, deadline, validationReserveMillis, + ).challenge(property, concrete?.observations, guidance, shrinkWitness) + } + }, + retainRelationTrace = { relationTrace = it }, ) + val relationFault = relationTrace?.confirmedOriginalFault() + if (relationFault != null) { + confirmation = relationFault + return result() + } if (symbolic == null) return result(PropertyCampaignStop.DEADLINE) val hasNativeWork = symbolic.target != null || symbolic.completedInputs.isNotEmpty() @@ -249,6 +281,7 @@ class PropertyCampaignRunner( pbtAllocationMillis: Long? = null, shrinkWitness: Boolean = true, completedInputLimit: Int = 0, + relationGuidance: PropertyRelationGuidance? = null, ): PropertyCampaignResult = runArtifact( property = property, mode = mode, @@ -257,6 +290,7 @@ class PropertyCampaignRunner( pbtAllocationMillis = pbtAllocationMillis, shrinkWitness = shrinkWitness, completedInputLimit = completedInputLimit, + relationGuidance = relationGuidance, ).result private fun validateControls( @@ -281,13 +315,19 @@ class PropertyCampaignRunner( sources: List, guided: Boolean, captureNative: Boolean, + relationGuidance: PropertyRelationGuidance?, ): PropertyRunConfiguration { - if (!guided && !captureNative) return configuration + if (!guided && !captureNative && relationGuidance == null) return configuration val request = configuration.coverageRequest ?: PropertyCoverageRequest() return configuration.copy( coverageRequest = request.copy(admittedOnly = true), - observationRequest = if (guided && configuration.inputExportRequest == null) { + observationRequest = if (relationGuidance != null) { + configuration.observationRequest ?: PropertyObservationRequest( + points = relationGuidance.pairs.flatMap { listOf(it.left, it.right) }.distinct(), + sources = sources, + ) + } else if (guided && configuration.inputExportRequest == null) { configuration.observationRequest ?: PropertyObservationRequest(points = emptyList(), sources = sources) } else { configuration.observationRequest @@ -363,6 +403,8 @@ class PropertyCampaignRunner( validationReserveMillis: Long, feedback: UsvmCoverageFeedback?, completedInputLimit: Int, + relationChallenger: ((EtsScene, PropertyEtsMappingArtifact) -> PropertyRelationGuidanceTrace)?, + retainRelationTrace: (PropertyRelationGuidanceTrace) -> Unit, ): UsvmPropertySearchResult? { if (deadline.remainingMillis() <= validationReserveMillis) return null @@ -371,11 +413,20 @@ class PropertyCampaignRunner( val manifest = property.toManifest() val mapping = PropertyEtsMapper(scene = scene, sourceRoots = listOf(root)).map(manifest) + val relationTrace = relationChallenger?.invoke(scene, mapping) + if (relationTrace?.confirmedOriginalFault() != null) { + retainRelationTrace(relationTrace) + return null + } val budgetMillis = deadline.remainingMillis() - validationReserveMillis + relationTrace?.let { + retainRelationTrace(it.copy(originalAllocatedMillis = budgetMillis.coerceAtLeast(minimumValue = 0))) + } if (budgetMillis <= 0) return null val searchTimeout = minOf(machineOptions.timeout, budgetMillis.milliseconds) - return UsvmPropertySearcher( + val originalStartedAt = System.nanoTime() + val result = UsvmPropertySearcher( scene = scene, machineOptions = machineOptions.copy(timeout = searchTimeout, stopOnCoverage = 0), ).search( @@ -386,6 +437,15 @@ class PropertyCampaignRunner( coverageFeedback = feedback, completedInputLimit = completedInputLimit, ) + relationTrace?.let { + retainRelationTrace( + it.copy( + originalAllocatedMillis = searchTimeout.inWholeMilliseconds, + originalElapsedMillis = (System.nanoTime() - originalStartedAt) / NANOS_PER_MILLISECOND, + ) + ) + } + return result } private fun confirm( diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationGuidance.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationGuidance.kt new file mode 100644 index 0000000000..6111825fd2 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationGuidance.kt @@ -0,0 +1,325 @@ +package org.usvm.ts.pbt.campaign + +import kotlinx.serialization.Serializable +import org.jacodb.ets.model.EtsScene +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ExternalWitnessCandidate +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.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.captureWitness +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.inference.ScalarGuidanceCandidate +import org.usvm.ts.pbt.inference.ScalarGuidanceRelevance +import org.usvm.ts.pbt.inference.ScalarGuidanceSelection +import org.usvm.ts.pbt.inference.ScalarObservationPair +import org.usvm.ts.pbt.inference.ScalarRelationInference +import org.usvm.ts.pbt.inference.inferScalarRelations +import org.usvm.ts.pbt.inference.selectScalarGuidance +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.observation.ObservationPointKind +import org.usvm.ts.pbt.observation.PropertyObservationArtifact +import org.usvm.ts.pbt.usvm.UsvmDslNumericLocalRefuter +import org.usvm.ts.pbt.usvm.UsvmEntryRelationRefuter +import org.usvm.ts.pbt.usvm.UsvmPropertyProjectionCapability +import org.usvm.ts.pbt.usvm.UsvmRelationRefutationStatus +import java.io.IOException +import kotlin.time.Duration.Companion.milliseconds +import kotlin.time.TimeSource + +/** Explicit opt-in; retained compiler authority is never reconstructed from source hashes or JSON. */ +data class PropertyRelationGuidance( + val pairs: List, + val compiled: CompiledDslProperty? = null, + val allowUnknownRelevance: Boolean = false, + val maxCandidates: Int = 16, + val maxRelationMillis: Long = 5_000, + val originalReserveMillis: Long = 5_000, +) { + init { + require(pairs.isNotEmpty()) { "Select at least one assertion operand pair" } + require(maxCandidates > 0 && maxRelationMillis > 0 && originalReserveMillis > 0) + } + + companion object { + fun numericLocal(compiled: CompiledDslProperty): PropertyRelationGuidance { + val capture = requireNotNull(compiled.numericLocalCapture) { "Compile the selected numeric local first" } + return PropertyRelationGuidance( + pairs = listOf(ScalarObservationPair(capture.result, capture.input)), + compiled = compiled, + ) + } + } + + internal fun controls() = PropertyRelationGuidanceControls( + pairs, + compilerRetained = compiled != null, + allowUnknownRelevance, + maxCandidates, + maxRelationMillis, + originalReserveMillis, + ) +} + +/** Serializable requested controls; the compiler object itself remains with its typed caller. */ +@Serializable +data class PropertyRelationGuidanceControls( + val pairs: List, + val compilerRetained: Boolean, + val allowUnknownRelevance: Boolean, + val maxCandidates: Int, + val maxRelationMillis: Long, + val originalReserveMillis: Long, +) + +/** The selected relation stays an empirical hypothesis, including after successful refutation. */ +@Serializable +data class PropertyRelationAttempt( + val selected: ScalarGuidanceCandidate, + val searchStatus: UsvmRelationRefutationStatus, + val bindingStatus: String, + val bindingDiagnostics: List, + val diagnostics: List, + val capability: UsvmPropertyProjectionCapability?, + val witness: ExternalWitnessCandidate?, + val confirmation: WitnessEvidenceDelta?, + val elapsedMillis: Long, + val completedWithinDeadline: Boolean, +) + +/** Complete bounded selection and decisions from one PBT snapshot; no second random generation phase. */ +@Serializable +data class PropertyRelationGuidanceTrace( + val selection: ScalarGuidanceSelection?, + val attempts: List, + val skippedUnknownRelevance: List, + val diagnostics: List, + val allocatedMillis: Long, + val originalReserveMillis: Long, + val elapsedMillis: Long, + val originalAllocatedMillis: Long = 0, + val originalElapsedMillis: Long = 0, +) + +/** Reuses the existing refuters and confirmation lifecycle under a slice of the caller's deadline. */ +internal class PropertyRelationChallenger( + private val scene: EtsScene, + private val mapping: PropertyEtsMappingArtifact, + private val backend: FastCheckBackend, + private val machineOptions: UMachineOptions, + private val deadline: WitnessReplayDeadline, + private val validationReserveMillis: Long, +) { + fun challenge( + property: PropertyDefinition, + observations: PropertyObservationArtifact?, + guidance: PropertyRelationGuidance, + shrinkWitness: Boolean, + ): PropertyRelationGuidanceTrace { + val started = TimeSource.Monotonic.markNow() + val attempts = mutableListOf() + val skipped = mutableListOf() + val diagnostics = mutableListOf() + val budget = minOf( + guidance.maxRelationMillis, + (deadline.remainingMillis() - validationReserveMillis - guidance.originalReserveMillis) + .coerceAtLeast(minimumValue = 0), + ) + val relationDeadline = WitnessReplayDeadline(timeoutMillis = budget.coerceAtLeast(minimumValue = 1)) + if (observations == null) { + return PropertyRelationGuidanceTrace( + selection = null, + attempts, + skipped, + diagnostics = listOf("No PBT point observations were retained"), + allocatedMillis = budget, + originalReserveMillis = guidance.originalReserveMillis, + elapsedMillis = started.elapsedNow().inWholeMilliseconds, + ) + } + + val inference = inferScalarRelations(property, observations, guidance.pairs) + val selection = selectScalarGuidance(inference, guidance.compiled, guidance.maxCandidates) + for (selected in selection.candidates) { + val unknown = selected.relevance == ScalarGuidanceRelevance.UNKNOWN + if (unknown && !guidance.allowUnknownRelevance) { + skipped += selected + continue + } + if (budget <= 0 || relationDeadline.remainingMillis() <= 0) { + diagnostics += "Relation allocation expired; unattempted candidates remain in the selection" + break + } + + val attempt = attempt(property, inference = inference, selected, guidance, relationDeadline, shrinkWitness) + attempts += attempt + if (attempt.confirmedOriginalFault() != null) break + } + + return PropertyRelationGuidanceTrace( + selection, + attempts, + skipped, + diagnostics, + allocatedMillis = budget, + originalReserveMillis = guidance.originalReserveMillis, + elapsedMillis = started.elapsedNow().inWholeMilliseconds, + ) + } + + private fun attempt( + property: PropertyDefinition, + inference: ScalarRelationInference, + selected: ScalarGuidanceCandidate, + guidance: PropertyRelationGuidance, + relationDeadline: WitnessReplayDeadline, + shrinkWitness: Boolean, + ): PropertyRelationAttempt { + val started = TimeSource.Monotonic.markNow() + val options = machineOptions.copy( + timeout = minOf( + machineOptions.timeout, + relationDeadline.remainingMillis().coerceAtLeast(minimumValue = 1).milliseconds, + ), + stopOnCoverage = 0, + ) + val relation = selected.relation + val entryOnly = relation.pair.left.kind == ObservationPointKind.ENTRY_ARGUMENT && + relation.pair.right.kind == ObservationPointKind.ENTRY_ARGUMENT + val concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT) + val status: UsvmRelationRefutationStatus + val bindingStatus: String + val bindingDiagnostics: List + val diagnostics: List + val capability: UsvmPropertyProjectionCapability + val witness: ExternalWitnessCandidate? + + if (entryOnly) { + val result = UsvmEntryRelationRefuter(scene, options).refute( + property.toManifest(), + mapping, + concreteCapability, + inference, + relation, + ) + status = result.status + bindingStatus = result.binding.status.name + bindingDiagnostics = result.binding.diagnostics.map { "${it.code}:${it.sourcePath}:${it.message}" } + diagnostics = result.diagnostics + capability = result.capability + witness = if (status.hasCandidate()) result.captureWitness() else null + } else { + val compiled = guidance.compiled + if (compiled == null) { + return PropertyRelationAttempt( + selected, + searchStatus = UsvmRelationRefutationStatus.UNSUPPORTED, + bindingStatus = "UNSUPPORTED", + bindingDiagnostics = listOf("Numeric local requires retained compiler output"), + diagnostics = emptyList(), + capability = null, + witness = null, + confirmation = null, + elapsedMillis = started.elapsedNow().inWholeMilliseconds, + completedWithinDeadline = relationDeadline.remainingMillis() > 0 && deadline.remainingMillis() > 0, + ) + } + val result = UsvmDslNumericLocalRefuter(scene, options).refute( + compiled, + mapping, + concreteCapability, + inference, + relation, + ) + status = result.status + bindingStatus = result.binding.status.name + bindingDiagnostics = result.binding.diagnostics.map { "${it.code}:${it.sourcePath}:${it.message}" } + diagnostics = result.diagnostics + capability = result.capability + witness = if (status.hasCandidate()) result.captureWitness() else null + } + + val native = confirm(property, witness, relationDeadline, shrinkWitness) + + return PropertyRelationAttempt( + selected, + status, + bindingStatus, + bindingDiagnostics, + diagnostics + listOfNotNull(native.diagnostic), + capability, + witness, + native.evidence, + elapsedMillis = started.elapsedNow().inWholeMilliseconds, + completedWithinDeadline = relationDeadline.remainingMillis() > 0 && deadline.remainingMillis() > 0, + ) + } + + private fun confirm( + property: PropertyDefinition, + witness: ExternalWitnessCandidate?, + deadline: WitnessReplayDeadline, + shrinkWitness: Boolean, + ): RelationConfirmation { + if (witness == null || deadline.remainingMillis() <= 0) return RelationConfirmation(evidence = null) + + return try { + val evidence = backend.confirmWitness( + property, + witness, + WitnessReplayConfiguration( + timeoutMillis = deadline.remainingMillis().coerceAtLeast(minimumValue = 1), + validationReserveMillis = validationReserveMillis, + shrink = shrinkWitness, + coverageRequest = PropertyCoverageRequest(admittedOnly = true), + ), + deadline, + ) + RelationConfirmation(evidence = evidence) + } catch (error: PbtBackendException) { + RelationConfirmation( + evidence = null, + diagnostic = CapabilityDiagnostic(error.code, error.message.orEmpty(), path = "relation.confirmation"), + ) + } catch (error: IOException) { + RelationConfirmation( + evidence = null, + diagnostic = CapabilityDiagnostic( + "campaign.relation.io", + error.toString(), + path = "relation.confirmation", + ), + ) + } + } +} + +private fun UsvmRelationRefutationStatus.hasCandidate(): Boolean = when (this) { + UsvmRelationRefutationStatus.REFUTATION_REACHED, + UsvmRelationRefutationStatus.FAILED_INPUT_RESOLUTION, + -> true + else -> false +} + +private data class RelationConfirmation( + val evidence: WitnessEvidenceDelta?, + val diagnostic: CapabilityDiagnostic? = null, +) + +internal fun PropertyRelationGuidanceTrace.confirmedOriginalFault(): WitnessEvidenceDelta? = + attempts.firstNotNullOfOrNull { it.confirmedOriginalFault() } + +private fun PropertyRelationAttempt.confirmedOriginalFault(): WitnessEvidenceDelta? { + if (!completedWithinDeadline) return null + + return confirmation?.takeIf { it.status == WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION } +} 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 42f83e21bf..746c0af528 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 @@ -166,13 +166,9 @@ internal class FastCheckWitnessCoordinator( val coverageRequest = configuration.coverageRequest if (coverageRequest != null) { try { - val coverageResult = replay(property, candidate, inputs, deadline, coverageRequest) - val covered = when (coverageResult) { - is FastCheckOperationResult.Completed -> coverageResult.value - is FastCheckOperationResult.TimedOut -> null - } - if (covered == null) { - coverageDiagnostic = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT + val covered = replayInput(property, candidate, coverageRequest, deadline) + if (covered.diagnostic != null) { + coverageDiagnostic = covered.diagnostic } else if (!repeatable(original, covered)) { return delta( candidate = candidate, 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 index fc39124bcb..a2a4caadd4 100644 --- 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 @@ -68,7 +68,9 @@ class GuidedPropertyCampaignTest { val configuration = configuration.copy( examples = examples(1), inputExportRequest = PropertyInputExportRequest( - sources = listOf(PropertyObservationSource(module = MODULE, sha256 = campaignSourceSha256(root.resolve(MODULE)))), + sources = listOf( + PropertyObservationSource(module = MODULE, sha256 = campaignSourceSha256(root.resolve(MODULE))) + ), ), ) @@ -79,10 +81,12 @@ class GuidedPropertyCampaignTest { pbtAllocationMillis = 15_000, ) - assertEquals(1, artifact.result.concrete?.inputExport?.records?.size) - assertNull(artifact.result.concrete?.observations) + val concrete = assertNotNull(artifact.result.concrete) + assertEquals(1, concrete.inputExport?.records?.size) + assertNull(concrete.observations) assertNotNull(artifact.result.symbolic?.edgeGuidance) - assertTrue(assertNotNull(artifact.result.concrete?.coverage).provenance.request.admittedOnly) + val concreteCoverage = assertNotNull(concrete.coverage) + assertTrue(concreteCoverage.provenance.request.admittedOnly) } @Test diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationCampaignTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationCampaignTest.kt new file mode 100644 index 0000000000..7947569f40 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyRelationCampaignTest.kt @@ -0,0 +1,255 @@ +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.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessRole +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.DslNumericLocalCapture +import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler +import org.usvm.ts.pbt.dsl.defineProperty +import org.usvm.ts.pbt.dsl.invoke +import org.usvm.ts.pbt.dsl.lessOrEqual +import org.usvm.ts.pbt.inference.ScalarGuidanceExclusionReason +import org.usvm.ts.pbt.inference.ScalarGuidanceRelevance +import org.usvm.ts.pbt.inference.ScalarObservationPair +import org.usvm.ts.pbt.inference.ScalarRelationTemplate +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyAssertion +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.PropertyOperand +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.observation.ObservationBuildStatus +import org.usvm.ts.pbt.observation.ObservationPointKind +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import org.usvm.ts.pbt.usvm.UsvmRelationRefutationStatus +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class PropertyRelationCampaignTest { + @TempDir + lateinit var root: Path + + private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 8, timeoutMillis = 30_000) + + @Test + fun `one PBT snapshot challenges a sampled local equality and retains the unrestricted original search`() { + val compiled = numericProperty() + + val artifact = run(compiled, PropertyRelationGuidance.numericLocal(compiled)) + val file = root.resolve("campaign.json") + artifact.write(file) + val restored = PropertyCampaignArtifact.read(file) + + val trace = assertNotNull(restored.result.relationGuidance) + val selection = assertNotNull(trace.selection) + val attempt = trace.attempts.single() + assertEquals(8, restored.result.concrete?.numRuns) + assertEquals(ObservationBuildStatus.UNVERIFIED, selection.inference.buildStatus) + assertEquals(ScalarGuidanceRelevance.KNOWN_DSL_CHECK, attempt.selected.relevance) + assertEquals(ScalarRelationTemplate.STRICT_EQUAL, attempt.selected.relation.template) + assertTrue(selection.excluded.any { it.reason == ScalarGuidanceExclusionReason.ORIGINAL_CHECK }) + assertEquals(UsvmRelationRefutationStatus.REFUTATION_REACHED, attempt.searchStatus) + assertEquals(WitnessRole.HYPOTHESIS, attempt.witness?.target?.role) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, attempt.confirmation?.status) + assertEquals(WitnessOracleOutcome.HOLDS, attempt.confirmation?.originalReplay?.outcome) + assertNotNull(attempt.confirmation?.originalReplay?.coverage?.identity) + assertTrue(attempt.completedWithinDeadline) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, restored.result.symbolic?.status) + assertTrue(trace.originalAllocatedMillis >= trace.originalReserveMillis) + assertFalse(restored.result.confirmedViolation) + assertEquals(artifact.result.relationGuidance, trace) + } + + @Test + fun `an original named fault found by a relation query stays a property violation`() { + val compiled = numericProperty(delta = "+ 1") + val guidance = PropertyRelationGuidance.numericLocal(compiled) + val pair = guidance.pairs.single() + val twoCandidates = guidance.copy(pairs = guidance.pairs + ScalarObservationPair(pair.right, pair.left)) + + val artifact = run(compiled, twoCandidates) + + val trace = assertNotNull(artifact.result.relationGuidance) + val attempt = trace.attempts.single() + val canonical = assertNotNull(artifact.result.confirmation) + assertEquals(2, assertNotNull(trace.selection).candidates.size) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, attempt.confirmation?.status) + assertEquals("bound", attempt.confirmation?.originalReplay?.failure?.checkId) + assertEquals(attempt.confirmation, canonical) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, canonical.status) + assertEquals("bound", canonical.originalReplay?.failure?.checkId) + assertTrue(artifact.result.confirmedViolation) + assertEquals(PropertyCampaignStop.COMPLETED, artifact.result.stop) + assertNull(artifact.result.symbolic) + assertEquals(0, trace.originalAllocatedMillis) + assertEquals(0, trace.originalElapsedMillis) + } + + @Test + fun `a timed out auxiliary allocation leaves positive time for the original objective`() { + val compiled = numericProperty() + val guidance = PropertyRelationGuidance.numericLocal(compiled).copy(maxRelationMillis = 1) + + val artifact = run(compiled, guidance) + + val trace = assertNotNull(artifact.result.relationGuidance) + assertTrue(trace.attempts.size <= 1) + assertEquals(1, trace.allocatedMillis) + assertTrue(trace.originalAllocatedMillis >= guidance.originalReserveMillis) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, artifact.result.symbolic?.status) + assertFalse(artifact.result.confirmedViolation) + } + + @Test + fun `unsupported prefixes retain their reason without removing the original objective`() { + val compiled = numericProperty(sparsePrefix = true) + + val artifact = run(compiled, PropertyRelationGuidance.numericLocal(compiled)) + + val trace = assertNotNull(artifact.result.relationGuidance) + val attempt = trace.attempts.single() + assertEquals(UsvmRelationRefutationStatus.UNSUPPORTED, attempt.searchStatus) + assertTrue(attempt.diagnostics.any { it.code == "usvm.runtime.array-index-growth" }) + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, artifact.result.symbolic?.status) + assertTrue(trace.originalAllocatedMillis > 0) + assertFalse(artifact.result.confirmedViolation) + } + + @Test + fun `insufficient observations remain evidence and do not suppress the original search`() { + val compiled = numericProperty() + + val artifact = run(compiled, PropertyRelationGuidance.numericLocal(compiled), numRuns = 1) + + val trace = assertNotNull(artifact.result.relationGuidance) + assertTrue(trace.attempts.isEmpty()) + assertTrue(assertNotNull(trace.selection).excluded.isNotEmpty()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, artifact.result.symbolic?.status) + } + + @Test + fun `unknown relevance is skipped by default and only explicit opt in activates its exact entry challenge`() { + Files.writeString( + root.resolve("entry.ts"), + "export function holds(a: number, b: number): boolean { return a === a; }" + ) + val call = PropertySourcePoint(module = "entry.ts", line = 1, column = 1) + val left = PropertyObservationPoint( + id = "left", + assertionId = "original", + operandId = "left", + source = call, + callSite = call, + kind = ObservationPointKind.ENTRY_ARGUMENT, + inputIndex = 0, + ) + val right = left.copy(id = "right", operandId = "right", inputIndex = 1) + val property = PropertyDefinition( + id = PropertyId(value = "entry.guidance"), + inputs = listOf( + PropertyInput(name = "a", domain = IntegerDomain(min = 0, max = 2)), + PropertyInput(name = "b", domain = IntegerDomain(min = 0, max = 2)), + ), + predicate = TypeScriptEntryPoint(module = "entry.ts", exportName = "holds"), + assertions = listOf( + PropertyAssertion( + id = "original", + source = call, + testedCall = call, + operands = listOf( + PropertyOperand(id = "left", source = call), + PropertyOperand(id = "right", source = call) + ), + ) + ), + ) + val guidance = PropertyRelationGuidance(pairs = listOf(ScalarObservationPair(left, right))) + val runner = PropertyCampaignRunner(sourceRoot = root) + val configuration = configuration.copy(seed = 1, numRuns = 2) + + val skipped = runner.runArtifact( + property, + mode = PropertyCampaignMode.SEQUENTIAL, + configuration, + pbtAllocationMillis = 8_000, + shrinkWitness = false, + relationGuidance = guidance, + ) + val optedIn = runner.runArtifact( + property, + mode = PropertyCampaignMode.SEQUENTIAL, + configuration, + pbtAllocationMillis = 8_000, + shrinkWitness = false, + relationGuidance = guidance.copy(allowUnknownRelevance = true), + ) + + val skippedTrace = assertNotNull(skipped.result.relationGuidance) + val selectedTrace = assertNotNull(optedIn.result.relationGuidance) + assertTrue(skippedTrace.attempts.isEmpty()) + assertTrue(skippedTrace.skippedUnknownRelevance.isNotEmpty()) + assertTrue(selectedTrace.attempts.isNotEmpty()) + assertTrue(selectedTrace.attempts.all { it.selected.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertTrue( + selectedTrace.attempts.any { + it.confirmation?.status == WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION + } + ) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, optedIn.result.symbolic?.status) + } + + private fun run( + compiled: CompiledDslProperty, + guidance: PropertyRelationGuidance, + numRuns: Int = 8, + ) = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = compiled.definition, + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration.copy(numRuns = numRuns), + pbtAllocationMillis = 8_000, + shrinkWitness = false, + relationGuidance = guidance, + ) + + private fun numericProperty(delta: String = "- 1", sparsePrefix: Boolean = false): CompiledDslProperty { + val prefix = if (sparsePrefix) "const cache: number[] = []; cache[1001] = input;" else "" + Files.writeString( + root.resolve("functions.ts"), + """ + export function transform(input: number): number { + $prefix + if (input === 417) return input $delta; + return input; + } + """.trimIndent() + ) + val program = defineProperty(id = "campaign.local-relation") { + val transform = function<(Double) -> Double>(module = "functions.ts", exportName = "transform") + val input by int(min = 0, max = 1000) + val result by value(transform(input)) + + check(name = "bound") { result lessOrEqual input } + } + val compiled = PropertyTypeScriptCompiler().compile( + program, + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "bound"), + ) + Files.writeString(root.resolve("generated.ts"), compiled.typeScript) + + return compiled + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt index b36d5f8b0f..67218101c7 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt @@ -11,6 +11,7 @@ import org.usvm.ts.pbt.observation.PropertyObservationSource import org.usvm.ts.pbt.observation.PropertyPointEvent /** An explicitly selected pair of assertion operands, each evaluated once per invocation. */ +@Serializable data class ScalarObservationPair( val left: PropertyObservationPoint, val right: PropertyObservationPoint, @@ -24,6 +25,7 @@ enum class ScalarRelationTemplate { } /** Sample agreement is empirical evidence, never an invariant or permission to prune a path. */ +@Serializable enum class ScalarRelationStatus { SAMPLED, REFUTED, @@ -32,6 +34,7 @@ enum class ScalarRelationStatus { } /** Reasons an invocation or selection cannot supply complete numeric evidence. */ +@Serializable enum class ScalarRelationLimitation { INVALID_PAIR, SOURCE_MISMATCH, @@ -48,6 +51,7 @@ enum class ScalarRelationLimitation { } /** Exact same-invocation point values, retaining origin, phase, input and event identities. */ +@Serializable data class ScalarRelationEvidence( val invocation: PropertyInvocationObservation, val left: PropertyPointEvent, @@ -56,6 +60,7 @@ data class ScalarRelationEvidence( ) /** Evaluation of one template for one selected pair, including every observed contradiction. */ +@Serializable data class ScalarRelation( val pair: ScalarObservationPair, val template: ScalarRelationTemplate, @@ -66,6 +71,7 @@ data class ScalarRelation( ) /** Bounded, property-scoped results preserving selected-source and executable-build provenance. */ +@Serializable data class ScalarRelationInference( val propertyId: PropertyId, val runId: String, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt index 8018e7e713..15acfcc9f3 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt @@ -1,5 +1,6 @@ package org.usvm.ts.pbt.inference +import kotlinx.serialization.Serializable import org.usvm.ts.pbt.dsl.CompiledDslProperty import org.usvm.ts.pbt.dsl.DslNumericLocalCapture import org.usvm.ts.pbt.dsl.PropertyExpressionTerm @@ -8,9 +9,11 @@ import org.usvm.ts.pbt.dsl.selectNumericLocalCapture import org.usvm.ts.pbt.observation.ObservationPointKind /** KNOWN_DSL_CHECK identifies a direct original check, not a proved relation or executable body. */ +@Serializable enum class ScalarGuidanceRelevance { KNOWN_DSL_CHECK, UNKNOWN } /** Selection decisions preserve each excluded relation and its original evidence. */ +@Serializable enum class ScalarGuidanceExclusionReason { NOT_SAMPLED, DOMAIN_IMPLIED, @@ -21,9 +24,11 @@ enum class ScalarGuidanceExclusionReason { } /** An empirical candidate whose exact symbolic support still needs a consumer's binding checks. */ +@Serializable data class ScalarGuidanceCandidate(val relation: ScalarRelation, val relevance: ScalarGuidanceRelevance) /** An unselected relation; exclusion never removes it from the original inference. */ +@Serializable data class ScalarGuidanceExclusion( val relation: ScalarRelation, val reason: ScalarGuidanceExclusionReason, @@ -31,6 +36,7 @@ data class ScalarGuidanceExclusion( ) /** Retains the complete original inference, including contradictory, insufficient and excluded evidence. */ +@Serializable data class ScalarGuidanceSelection( val inference: ScalarRelationInference, val candidates: List, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt index 6ad76dee7e..994f9eee79 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt @@ -1,5 +1,6 @@ package org.usvm.ts.pbt.usvm +import kotlinx.serialization.Serializable import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType import org.usvm.StateCollectionStrategy @@ -26,6 +27,7 @@ import org.usvm.ts.pbt.model.JsConcreteValue import java.util.concurrent.CancellationException /** Auxiliary search outcomes, independently of the original property's truth. */ +@Serializable enum class UsvmRelationRefutationStatus { REFUTATION_REACHED, NO_REFUTATION_REACHED,