[TS PBT] Guide original property search with admitted edge coverage

usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt

@@ -36,6 +36,7 @@ private fun <Method, Statement, Target, State> createPathSelector(
     cfgStatisticsFactory: () -> CfgStatistics<Method, Statement>? = { null },
     callGraphStatisticsFactory: () -> CallGraphStatistics<Method>? = { null },
     loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null },
+    coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator<Method, Statement>? = { null },
 ): UPathSelector<State>
     where Target : UTarget<Statement, Target>,
           State : UState<*, Method, Statement, *, Target, State> {
@@ -69,14 +70,16 @@ private fun <Method, Statement, Target, State> createPathSelector(
             PathSelectionStrategy.CLOSEST_TO_UNCOVERED -> createClosestToUncoveredPathSelector(
                 requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" },
                 requireNotNull(cfgStatisticsFactory()) { "CFG statistics is required for closest to uncovered path selector" },
-                applicationGraph
+                applicationGraph,
+                distanceCalculator = coverageDistanceCalculatorFactory(),
             )
 
             PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM -> createClosestToUncoveredPathSelector(
                 requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" },
                 requireNotNull(cfgStatisticsFactory()) { "CFG statistics is required for closest to uncovered path selector" },
                 applicationGraph,
-                random
+                random,
+                distanceCalculator = coverageDistanceCalculatorFactory(),
             )
 
             PathSelectionStrategy.TARGETED -> createTargetedPathSelector<Method, Statement, Target, State>(
@@ -153,6 +156,7 @@ fun <Method, Statement, Target, State> createPathSelector(
     cfgStatisticsFactory: () -> CfgStatistics<Method, Statement>? = { null },
     callGraphStatisticsFactory: () -> CallGraphStatistics<Method>? = { null },
     loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null },
+    coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator<Method, Statement>? = { null },
 ): UPathSelector<State> where Target : UTarget<Statement, Target>, State : UState<*, Method, Statement, *, Target, State> =
     createPathSelector(
         listOf(initialState),
@@ -161,7 +165,8 @@ fun <Method, Statement, Target, State> createPathSelector(
         coverageStatisticsFactory,
         cfgStatisticsFactory,
         callGraphStatisticsFactory,
-        loopStatisticFactory
+        loopStatisticFactory,
+        coverageDistanceCalculatorFactory,
     )
 
 fun <Method, Statement, Target, State> createPathSelector(
@@ -173,6 +178,7 @@ fun <Method, Statement, Target, State> createPathSelector(
     cfgStatisticsFactory: () -> CfgStatistics<Method, Statement>? = { null },
     callGraphStatisticsFactory: () -> CallGraphStatistics<Method>? = { null },
     loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null },
+    coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator<Method, Statement>? = { null },
 ): UPathSelector<State> where Target : UTarget<Statement, Target>, State : UState<*, Method, Statement, *, Target, State> {
     val hasSingleEntryPoint = initialStates.size == 1
     val hasUnlimitedScheduling = options.timeout == Duration.INFINITE &&
@@ -185,7 +191,8 @@ fun <Method, Statement, Target, State> createPathSelector(
             coverageStatisticsFactory,
             cfgStatisticsFactory,
             callGraphStatisticsFactory,
-            loopStatisticFactory
+            loopStatisticFactory,
+            coverageDistanceCalculatorFactory,
         )
     }
 
@@ -202,7 +209,8 @@ fun <Method, Statement, Target, State> createPathSelector(
             coverageStatisticsFactory,
             cfgStatisticsFactory,
             callGraphStatisticsFactory,
-            loopStatisticFactory
+            loopStatisticFactory,
+            coverageDistanceCalculatorFactory,
         )
 
     val coverageStatistics = coverageStatisticsFactory()
@@ -317,15 +325,16 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
     cfgStatistics: CfgStatistics<Method, Statement>,
     applicationGraph: ApplicationGraph<Method, Statement>,
     random: Random? = null,
+    distanceCalculator: CallStackDistanceCalculator<Method, Statement>? = null,
 ): UPathSelector<State> {
-    val distanceCalculator = CallStackDistanceCalculator(
+    val calculator = distanceCalculator ?: CallStackDistanceCalculator(
         targets = coverageStatistics.getUncoveredStatements(),
         cfgStatistics = cfgStatistics,
         applicationGraph
     )
 
     coverageStatistics.addOnCoveredObserver { _, method, statement ->
-        distanceCalculator.removeTarget(
+        calculator.removeTarget(
             method,
             statement
         )
@@ -334,21 +343,25 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
     if (random == null) {
         return WeightedPathSelector(
             priorityCollectionFactory = { DeterministicPriorityCollection(Comparator.naturalOrder()) },
-            weighter = { distanceCalculator.calculateDistance(it.currentStatement, it.callStack) }
+            weighter = { calculator.calculateDistance(it.currentStatement, it.callStack) }
         )
     }
 
-    return WeightedPathSelector(
-        priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } },
-        weighter = {
-            1.0 / max(
-                distanceCalculator.calculateDistance(it.currentStatement, it.callStack).toDouble(),
-                1.0
-            )
-        }
+    return createClosestToUncoveredRandomPathSelector(
+        distance = { calculator.calculateDistance(it.currentStatement, it.callStack) },
+        random = random,
     )
 }
 
+/** NURS weights change only on ordinary add/update; coverage changes never scan queued states. */
+fun <State : UState<*, *, *, *, *, State>> createClosestToUncoveredRandomPathSelector(
+    distance: StateWeighter<State, UInt>,
+    random: Random,
+): UPathSelector<State> = WeightedPathSelector(
+    priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } },
+    weighter = { 1.0 / max(distance.weight(it).toDouble(), 1.0) },
+)
+
 fun <Method, Statement, State : UState<*, Method, Statement, *, *, State>> createForkDepthPathSelector(
     random: Random? = null,
 ): UPathSelector<State> {

usvm-core/src/test/kotlin/org/usvm/ps/ClosestToUncoveredRandomPathSelectorTest.kt

@@ -0,0 +1,149 @@
+package org.usvm.ps
+
+import io.mockk.every
+import org.junit.jupiter.api.Test
+import org.usvm.PathNode
+import org.usvm.PathSelectionStrategy
+import org.usvm.TestInstruction
+import org.usvm.TestState
+import org.usvm.UMachineOptions
+import org.usvm.appGraph
+import org.usvm.mockState
+import org.usvm.statistics.CoverageStatistics
+import org.usvm.statistics.distances.CallStackDistanceCalculator
+import org.usvm.statistics.distances.CfgStatistics
+import org.usvm.statistics.distances.CfgStatisticsImpl
+import kotlin.test.assertEquals
+import kotlin.test.assertSame
+import kotlin.test.assertTrue
+
+class ClosestToUncoveredRandomPathSelectorTest {
+    private val graph = appGraph {
+        method(name = "method", instructionsCount = 7) {
+            entryPoint(offset = 0)
+            edge(from = 0, to = 1)
+            edge(from = 1, to = 2)
+            edge(from = 0, to = 3)
+            edge(from = 3, to = 4)
+            edge(from = 4, to = 5)
+            edge(from = 5, to = 6)
+            exitPoint(offset = 2)
+            exitPoint(offset = 6)
+        }
+    }
+
+    @Test
+    fun `coverage and peek never recalculate queued weights while update touches only its state`() {
+        val cfg = CfgStatisticsImpl(graph)
+        val evaluated = mutableListOf<TestInstruction>()
+        val countedCfg = object : CfgStatistics<String, TestInstruction> by cfg {
+            override fun getShortestDistanceToExit(method: String, stmtFrom: TestInstruction): UInt {
+                evaluated.add(stmtFrom)
+                return cfg.getShortestDistanceToExit(method, stmtFrom)
+            }
+        }
+        val leftGoal = TestInstruction(method = "method", offset = 1)
+        val rightGoal = TestInstruction(method = "method", offset = 6)
+        val calculator = CallStackDistanceCalculator(
+            targets = listOf(leftGoal, rightGoal),
+            cfgStatistics = countedCfg,
+            applicationGraph = graph,
+        )
+        val nativeCoverage = CoverageStatistics<String, TestInstruction, TestState>(
+            methods = setOf("method"),
+            applicationGraph = graph,
+        )
+        val left = mockState(id = 1u, startMethod = "method", startInstruction = 1)
+        val right = mockState(id = 2u, startMethod = "method", startInstruction = 3)
+        val selector = createPathSelector(
+            initialState = left,
+            options = UMachineOptions(
+                pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
+                randomSeed = 0,
+            ),
+            applicationGraph = graph,
+            coverageStatisticsFactory = { nativeCoverage },
+            cfgStatisticsFactory = { countedCfg },
+            coverageDistanceCalculatorFactory = { calculator },
+        )
+        selector.add(states = listOf(right))
+        assertEquals(expected = listOf(left.currentStatement, right.currentStatement), actual = evaluated)
+        assertSame(expected = left, actual = selector.peek())
+        evaluated.clear()
+
+        assertTrue(calculator.removeTarget(method = "method", statement = leftGoal))
+        repeat(256) { selector.peek() }
+
+        assertTrue(evaluated.isEmpty())
+        assertEquals(expected = 0, actual = nativeCoverage.getTotalCoveredStatements())
+
+        selector.update(state = left)
+
+        assertEquals(expected = listOf(left.currentStatement), actual = evaluated)
+        assertSame(expected = right, actual = selector.peek())
+        evaluated.clear()
+
+        val fork = mockState(id = 3u, startMethod = "method", startInstruction = 2)
+        selector.add(states = listOf(fork))
+
+        assertEquals(expected = listOf(fork.currentStatement), actual = evaluated)
+        assertSame(expected = right, actual = selector.peek())
+        assertEquals(expected = setOf(left, right, fork), actual = selector.drain().toHashSet())
+    }
+
+    @Test
+    fun `native coverage still removes targets from the supplied calculator`() {
+        val cfg = CfgStatisticsImpl(graph)
+        val goal = TestInstruction(method = "method", offset = 1)
+        val calculator = CallStackDistanceCalculator(
+            targets = listOf(goal),
+            cfgStatistics = cfg,
+            applicationGraph = graph,
+        )
+        val state = mockState(id = 1u, startMethod = "method", startInstruction = 1)
+        every { state.pathNode } returns PathNode.root<TestInstruction>() + goal
+        val coverage = CoverageStatistics<String, TestInstruction, TestState>(
+            methods = setOf("method"),
+            applicationGraph = graph,
+        )
+        val selector = createPathSelector(
+            initialState = state,
+            options = UMachineOptions(
+                pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
+            ),
+            applicationGraph = graph,
+            coverageStatisticsFactory = { coverage },
+            cfgStatisticsFactory = { cfg },
+            coverageDistanceCalculatorFactory = { calculator },
+        )
+
+        coverage.onStateTerminated(state = state, stateReachable = true)
+        selector.update(state = state)
+
+        assertEquals(expected = 1, actual = coverage.getTotalCoveredStatements())
+        assertEquals(
+            expected = UInt.MAX_VALUE,
+            actual = calculator.calculateDistance(state.currentStatement, state.callStack),
+        )
+        assertSame(expected = state, actual = selector.peek())
+        assertEquals(expected = listOf(state), actual = selector.drain().toList())
+    }
+
+    @Test
+    fun `covered prefixes can still lead to uncovered successors`() {
+        val goal = TestInstruction(method = "method", offset = 6)
+        val prefix = mockState(id = 1u, startMethod = "method", startInstruction = 3)
+        val calculator = CallStackDistanceCalculator(
+            targets = listOf(prefix.currentStatement, goal),
+            cfgStatistics = CfgStatisticsImpl(graph),
+            applicationGraph = graph,
+        )
+
+        calculator.removeTarget(method = "method", statement = prefix.currentStatement)
+
+        assertEquals(
+            expected = 3u,
+            actual = calculator.calculateDistance(prefix.currentStatement, prefix.callStack),
+        )
+    }
+}

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt

@@ -571,6 +571,7 @@ private fun runRawClassAnalysis(args: List<String>, exploratory: Boolean) {
         TsMachine(
             scene = scene,
             options = UMachineOptions(
+                pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY),
                 stateCollectionStrategy = StateCollectionStrategy.ALL,
                 randomSeed = manifest.seed,
                 collectedStatesLimit = manifest.collectedStatesLimit,

usvm-ts-fast-check/README.md

@@ -12,14 +12,57 @@ remain in [`usvm-ts-pbt`](../usvm-ts-pbt/README.md).
 One c8 execution produces the existing source-mapped Istanbul statement report and raw V8 ranges. The bounded
 TypeScript branch converter reads those same raw ranges, the executed source snapshot, and the source map. It emits
 ordered `if` arms only when the original TypeScript points map back exactly, each arm has a distinct V8 execution
-point, and the arm counts add up to the count at the condition. A supported `if` without `else` additionally needs
-a single terminating `return` or `throw` in its true arm and a following statement that is reached only on false.
+point, and the arm counts add up to the count at the condition. An `if` without `else` uses either a terminating
+true arm and a distinct false successor, or a following join whose execution count equals the condition count.
+In the latter case the false count is the condition count minus the true count. Missing points, early exits and
+throwing conditions that violate this conservation rule remain unknown.
 Nested `if` statements are supported under those conditions. Ambiguous counts or ranges and unsupported constructs
 produce diagnostics; exact statement mappings remain available.
 
 Loops, `switch`, conditional expressions, logical short-circuit ranges, and function or script ranges are never
 reinterpreted as `if` arms. The converter does not instrument the TypeScript program or execute it a second time.
-The resulting edges are coverage artifacts; target-selection integration belongs to #399/#355.
+The DSL's `BOTH` mode uses exact admitted coverage to guide the original property search as described below.
+
+## PBT edge feedback in `BOTH`
+
+`DslPropertyRunner.run(program, engine = PropertyEngine.BOTH, configuration = ...)` first runs FastCheck and then
+passes its confirmed source edges to the same USVM analysis that searches for a violation of the author checks.
+Coverage is enabled automatically in this mode. The predicate, domains and precondition keep their original roles;
+coverage affects scheduling only and adds no constraints.
+
+This mode collects V8 counters only during admitted predicate invocations, excluding the precondition, rejected
+inputs, import initialization and shrinking trials. A synchronous worker handshake keeps synchronous precondition
+and predicate calls uninterrupted. Each report carries a digest of the manifest and local TypeScript source files.
+Absent, stale, unsupported and no-admission evidence produce distinct classifications. Only exact mapped `if` arms
+provide known covered or uncovered edges; statement hits and missing branch records provide neither.
+
+The deterministic selector alternates a nearest known-uncovered edge priority with a fair original-objective turn.
+Covered prefixes stay in the graph. Full edge coverage stops the coverage objective while property exploration
+continues; statement saturation does not stop a property search. Distances follow calls and active return sites and
+are scheduling overapproximations, not claims of feasibility.
+Configurations using state merging or selector loop bounds retain their existing selector with an explicit
+unsupported-feedback diagnostic; this first policy does not silently bypass those controls.
+
+When a completed property path crosses a new target, its input is replayed natively as a single explicit example:
+no fallback generation and no shrinking. A rejected input, changed oracle result, incompatible source/runtime or
+missing claimed edge leaves coverage unchanged. Confirmed additions immediately change subsequent selections in
+the running machine. Exact branches first observed during replay also become eligible goals. Each edge has at most
+two replay attempts with distinct inputs; failed targets remain listed
+as uncovered after that limit. At least half of scheduling turns remain available to the original objective.
+
+Inspect `run.symbolic?.edgeGuidance` for initial coverage/goals, actual selected states and traversed goals,
+evidence revisions, replay outcomes/additions, remaining goals and diagnostics. Selection history is bounded to
+4096 entries with an explicit omitted count. `run.elapsedMillis` and `run.budgetMillis` report the shared wall-time
+budget; replay entries report native replay costs. FastCheck receives at most one third of the total budget.
+After frontend preparation, one third of the remaining time is reserved for final witness replay and shrinking;
+feedback replays use at most one third of the symbolic allocation. Mapping, startup, search and replay use the
+same monotonic deadline. Stop checks occur between interpreter steps and backend calls; an already-running solver
+query, frontend conversion already in progress, or process shutdown can exceed the deadline and is included in
+elapsed time. A frontend conversion is never started after the deadline; `symbolicSkippedDueToDeadline` reports
+that no symbolic analysis ran, and `requireSuccess()` treats it as inconclusive.
+
+The admitted collector covers the main Node isolate only. This slice does not infer relations, change PBT
+generation, retain a session between separate runner calls or implement the repeated two-way campaign of #355.
 
 Run the backend checks with:
 

usvm-ts-fast-check/fast-check-adapter/package.json

@@ -12,6 +12,7 @@
     "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js dist/test/class-coverage-source.test.js"
   },
   "dependencies": {
+    "@bcoe/v8-coverage": "1.0.2",
     "@jridgewell/trace-mapping": "0.3.31",
     "c8": "10.1.3",
     "fast-check": "4.9.0",