diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt index f37987f29d..e88bc5cb7d 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt @@ -330,13 +330,6 @@ class DslPropertyRunner(sourceRoots: List) { }.toList() } - private fun remainingBudget(deadline: WitnessReplayDeadline): Long { - val remaining = deadline.remainingMillis() - check(remaining > 0) { "Property execution deadline expired" } - - return remaining - } - private fun resolveModule(module: String, directory: Path): String { val modulePath = Path.of(module) val normalized = !modulePath.isAbsolute && '\\' !in module && diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index 03bad17dbb..001fa4187b 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt @@ -1,9 +1,9 @@ package org.usvm.ts.pbt.fastcheck import org.usvm.ts.pbt.FastCheckDiagnosticCode +import org.usvm.ts.pbt.backend.CoverageDiagnostic import org.usvm.ts.pbt.backend.ExternalWitnessBackend import org.usvm.ts.pbt.backend.ExternalWitnessCandidate -import org.usvm.ts.pbt.backend.CoverageDiagnostic import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend import org.usvm.ts.pbt.backend.PropertyCoverageCapability import org.usvm.ts.pbt.backend.PropertyRunConfiguration diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt index 7e2b43269c..80e53f53bf 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt @@ -239,7 +239,7 @@ class KotlinPropertyDslTest { "elapsedMillis=$elapsedMillis, budgetMillis=$budgetMillis, " + "symbolicSkippedDueToDeadline=$symbolicSkippedDueToDeadline, symbolicStatus=${symbolic?.status}, " + "concreteStatus=${concrete?.status}, replayStatus=${symbolicReplay?.status}, " + - "replayFailure=${symbolicReplay?.failure}" + "replayFailure=${symbolicReplay?.originalReplay?.failure}" private fun addition(exportName: String): DslProperty = defineProperty(id = "calculator.$exportName") { val sum = function<(Double, Double) -> Double>(module = "calculator.ts", exportName = exportName) diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt index a80dce86d2..4fa722cf4c 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt @@ -119,7 +119,7 @@ class PbtEdgeGuidanceTest { assertTrue(trace.selections.isNotEmpty()) assertTrue(trace.selections.all { it.goal == null && it.originalObjectiveTurn }) assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, run.symbolic?.status) - assertEquals("original", run.symbolicReplay?.failure?.checkId) + assertEquals("original", run.symbolicReplay?.originalReplay?.failure?.checkId) } private fun positiveResult(exportName: String): DslProperty = defineProperty(id = "edge-guidance.$exportName") { diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt index 98fc854d79..237fcd397e 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/RuntimeLimitationDslTest.kt @@ -3,6 +3,7 @@ package org.usvm.ts.pbt.dsl import org.junit.jupiter.api.Test import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.backend.WitnessReplayStatus import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.testResourcesRoot import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus @@ -44,7 +45,10 @@ class RuntimeLimitationDslTest { @Test fun `supported counterexample and its native replay survive an excluded path`() { val program = defineProperty(id = "runtime.mixed-counterexample") { - val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse") + val write = function<(Double) -> Double>( + module = "runtime-limitations.ts", + exportName = "supportedOrSparse", + ) val index by int(min = 0, max = 2) check(name = "zero") { write(index) equalTo 0 } @@ -56,15 +60,18 @@ class RuntimeLimitationDslTest { assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, symbolic.status) assertEquals(listOf(JsConcreteValue.number(0.0)), symbolic.inputs) assertTrue(symbolic.diagnostics.any { it.code == "usvm.runtime.array-index-growth" }) - assertEquals(PropertyRunStatus.FAILURE, run.symbolicReplay?.status) - assertEquals("zero", run.symbolicReplay?.failure?.checkId) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, run.symbolicReplay?.status) + assertEquals("zero", run.symbolicReplay?.originalReplay?.failure?.checkId) assertFailsWith { run.requireSuccess() } } @Test fun `supported successful paths do not hide excluded model paths`() { val program = defineProperty(id = "runtime.mixed-no-violation") { - val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse") + val write = function<(Double) -> Double>( + module = "runtime-limitations.ts", + exportName = "supportedOrSparse", + ) val index by int(min = 0, max = 2) check(name = "positive") { write(index) greaterThan 0 } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt index 55fc793b43..c752cfb8a1 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt @@ -1,5 +1,6 @@ package org.usvm.ts.pbt.usvm +import kotlinx.serialization.Serializable import org.usvm.ts.pbt.backend.PropertyCoverageArtifact import org.usvm.ts.pbt.backend.PropertyRunResult import org.usvm.ts.pbt.model.JsConcreteValue @@ -11,6 +12,7 @@ data class UsvmCoverageFeedback( ) /** Why a report can or cannot supply exact coverage goals for this property/source snapshot. */ +@Serializable enum class UsvmCoverageEvidenceStatus { ABSENT, STALE, @@ -21,6 +23,7 @@ enum class UsvmCoverageEvidenceStatus { } /** Distinguishes a CFG edge from either of its endpoint statements. */ +@Serializable data class UsvmCoverageEdge( val method: String, val conditionIndex: Int, @@ -29,6 +32,7 @@ data class UsvmCoverageEdge( ) /** A real queue decision made during the original predicate analysis. */ +@Serializable data class UsvmEdgeSelection( val evidenceRevision: Int, val stateId: UInt, @@ -41,6 +45,7 @@ data class UsvmEdgeSelection( ) /** Concrete confirmation outcomes; none except CONFIRMED can add edges. */ +@Serializable enum class UsvmEdgeReplayStatus { CONFIRMED, EDGE_MISMATCH, @@ -50,6 +55,7 @@ enum class UsvmEdgeReplayStatus { } /** A bounded exact-input native replay and its effect on the shared edge set. */ +@Serializable data class UsvmEdgeReplay( val inputs: List, val status: UsvmEdgeReplayStatus, @@ -59,6 +65,7 @@ data class UsvmEdgeReplay( ) /** Bounded history; symbolic reachability never updates [confirmedCovered]. */ +@Serializable data class UsvmEdgeGuidanceTrace( val evidenceStatus: UsvmCoverageEvidenceStatus, val initialCovered: Set, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt index 9e12fb632c..44723908a7 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt @@ -18,6 +18,7 @@ import org.usvm.ts.pbt.backend.PropertyRunStatus import org.usvm.ts.pbt.coverage.captureCoverageIdentity import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.mapping.EtsBranchArmTarget +import org.usvm.ts.pbt.mapping.EtsCoverageMapping import org.usvm.ts.pbt.mapping.EtsMappingStatus import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact @@ -54,57 +55,57 @@ internal class UsvmEdgeGuidance( private val initialGoals: Set init { - val coverage = feedback.initialCoverage - evidenceStatus = evidenceStatus(coverage) - val usable = evidenceStatus == UsvmCoverageEvidenceStatus.EXACT || - evidenceStatus == UsvmCoverageEvidenceStatus.PARTIAL - if (usable) { - val evidence = exactEdges(requireNotNull(coverage)) - evidence.forEach { (edge, target, hits) -> - targets[edge] = target - if (hits > 0) covered += edge - } + val evidence = evaluateEvidence(feedback.initialCoverage) + evidenceStatus = evidence.status + evidence.edges.forEach { (edge, target, hits) -> + targets[edge] = target + if (hits > 0) covered += edge } initialCovered = covered.toSet() initialGoals = pendingGoals() } - private fun evidenceStatus(coverage: PropertyCoverageArtifact?): UsvmCoverageEvidenceStatus { + private fun evaluateEvidence(coverage: PropertyCoverageArtifact?): CoverageEvidence { if (!selectionSupported) { diagnostics += "Edge scheduling does not support state merging or selector loop bounds; " + "original selection retained" - return UsvmCoverageEvidenceStatus.UNSUPPORTED + return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED) } - if (coverage == null) return UsvmCoverageEvidenceStatus.ABSENT + if (coverage == null) return CoverageEvidence(status = UsvmCoverageEvidenceStatus.ABSENT) if (!coverage.provenance.request.admittedOnly || coverage.identity == null) { - return UsvmCoverageEvidenceStatus.UNSUPPORTED + return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED) } val stale = coverage.identity != identity || coverage.propertyId.value != manifest.propertyId || coverage.diagnostics.any { it.code == "coverage.source.stale" } - if (stale) return UsvmCoverageEvidenceStatus.STALE - if (coverage.admittedInvocations == null) return UsvmCoverageEvidenceStatus.UNSUPPORTED - if (coverage.admittedInvocations == 0) return UsvmCoverageEvidenceStatus.NO_ADMITTED_INPUTS + if (stale) return CoverageEvidence(status = UsvmCoverageEvidenceStatus.STALE) + if (coverage.admittedInvocations == null) { + return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED) + } + if (coverage.admittedInvocations == 0) { + return CoverageEvidence(status = UsvmCoverageEvidenceStatus.NO_ADMITTED_INPUTS) + } val mapped = mapper().map(manifest, coverage).coverage - val exact = exactEdges(coverage) + val exact = exactEdges(mapped) val mappingDiagnostics = mapped.diagnostics + mapped.branches.flatMap { branch -> branch.mapping.diagnostics + branch.arms.flatMap { it.mapping.diagnostics } } diagnostics += mappingDiagnostics.map { "${it.code}: ${it.message}" }.distinct() - if (exact.isEmpty()) return UsvmCoverageEvidenceStatus.UNSUPPORTED + if (exact.isEmpty()) return CoverageEvidence(status = UsvmCoverageEvidenceStatus.UNSUPPORTED) val unknownBranches = mapped.branches.any { it.mapping.status != EtsMappingStatus.EXACT } - return if (unknownBranches || mapped.diagnostics.isNotEmpty()) { + val status = if (unknownBranches || mapped.diagnostics.isNotEmpty()) { UsvmCoverageEvidenceStatus.PARTIAL } else { UsvmCoverageEvidenceStatus.EXACT } + return CoverageEvidence(status = status, edges = exact) } private fun mapper() = PropertyEtsMapper(scene = scene, sourceRoots = roots) - private fun exactEdges(coverage: PropertyCoverageArtifact): List { - return mapper().map(manifest, coverage).coverage.branches.flatMap { branch -> + private fun exactEdges(mapped: EtsCoverageMapping): List { + return mapped.branches.flatMap { branch -> val sourcePath = branch.location?.path if (sourcePath !in identity.sourceSha256) return@flatMap emptyList() @@ -191,7 +192,8 @@ internal class UsvmEdgeGuidance( return ReplayDecision(status = UsvmEdgeReplayStatus.REJECTED_OR_INCOMPATIBLE) } - val observed = exactEdges(requireNotNull(coverage)) + val mapped = mapper().map(manifest, requireNotNull(coverage)).coverage + val observed = exactEdges(mapped) val confirmed = observed.filter { it.hits > 0 }.mapTo(hashSetOf()) { it.edge } if (!confirmed.containsAll(claimed)) return ReplayDecision(status = UsvmEdgeReplayStatus.EDGE_MISMATCH) @@ -259,6 +261,11 @@ internal class UsvmEdgeGuidance( elapsedMillis = started.elapsedNow().inWholeMilliseconds, ) + private data class CoverageEvidence( + val status: UsvmCoverageEvidenceStatus, + val edges: List = emptyList(), + ) + private data class ObservedEdge(val edge: UsvmCoverageEdge, val target: EtsBranchArmTarget, val hits: Long) private data class GoalDistance(val goal: UsvmCoverageEdge, val distance: Int) private data class ReplayDecision( 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 b475aa8fec..07f091472b 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 @@ -103,7 +103,7 @@ class UsvmPropertySearcher( predicate = predicate, precondition = precondition, capability = capability, - deadlineReached = deadlineReached, + deadlineReached = deadlineReached ?: this.deadlineReached, guidance = guidance, ).copy(edgeGuidance = guidance?.snapshot()) }