[Core] Add a selector with explicit coverage updates

[CaelmBleidd]

Coverage changes can invalidate every queued state's priority. Refreshing the whole queue on every changed-coverage peek repeatedly drains and reinserts all states and recalculates their distances.

Add CoverageGuidedPathSelector with explicit markCovered/addTargets updates and snapshot-based priority refreshes. The configurable interval defaults to 128 completed selections. Updating or removing the selected state completes a selection; repeated peek calls do not advance the interval. New and updated states use the same snapshot. Goal sets and snapshots use HashSet because their order is irrelevant. Unknown/repeated reports do not trigger work, covered goals stay covered, and saturation retains states while avoiding distance calculations. Stopped-work draining bypasses refresh.

Add DeterministicPriorityCollection.updatePriorities to evaluate each queued element once, including the cached selection, then heapify in O(N). It replaces drain/toList/add and preserves the old queue if priority evaluation fails. The PR includes the cached-ordering prerequisite from #538 as a separate commit. WeightedPathSelector, CoverageStatistics and PathSelectorFactory remain unchanged.

Manual JVM measurements now cover Commons Codec BinaryCodec, Guava IntMath.gcd and LoanExam: 28 retained runs, 2,422,205 interpreter steps, queues up to 4,921 states. The periodic selector still spends substantial time scanning every snapshot goal on ordinary state updates:

• Codec, 100,000 steps, interval 128: median 6.319 s in the selector (29.48% of analysis), including 90.32 ms in refresh peeks; 23,826,680 per-target distance calls. Aggregate closest-to-uncovered control: 0.134 s in the selector (0.78%). Codec has two fresh-process repeats per mode; whole-analysis timings vary substantially.
• Guava, interval 128: 63,808 steps before the 120 s timeout, 14.249 s in the selector (11.86%). Aggregate control: 61,538 steps, 0.235 s in the selector.
• LoanExam, interval 128: queue exhausted after 73,519 steps, 0.266 s in the selector (11.39%). Aggregate control: the same step count, 0.069 s in the selector.

Increasing the interval to 512 did not remove the per-update target-scan cost. These local runs do not demonstrate a stable whole-analysis speedup: exploration order and solver work differ, and only 1-26 coverage-guided refresh peeks occurred per run. Dynamic goal discovery is unmeasured. The next API improvement would allow a caller-supplied batched minimum-distance calculation over a snapshot with domain-specific caching; that proposal is not implemented here.

Uniform random and the production RANDOM_PATH selector were also measured with selector RNG seeds 0 and 1:

• Codec uniform random: 100,000 steps in 3.430-3.937 s, 74 covered goals, and 0.315-0.339 s in the selector. RANDOM_PATH took 7.283-13.359 s, including 3.991-6.585 s in its selector.
• Guava uniform random: 100,000 steps in 7.328-10.153 s and 28 covered goals, versus interval 128's 63,808 steps / 17 goals at the 120 s timeout. RANDOM_PATH also reached 100,000 steps and 28 goals, in 18.281-19.171 s.
• LoanExam is a counterexample: uniform random took 2.745-3.046 s versus interval 128's 2.333 s, with the same 73,519 steps and 123 covered goals.

These two seeds support using cheap uniform random as a baseline; they do not prove universal dominance. Different path order also changes work outside the selector, which has not been separately profiled. Covered-goal counts do not establish equality of covered-goal sets or concrete replay coverage. Production selection defaults have not been changed by the benchmark.

Full methodology, raw data and reproduction runner.

Validation on Zulu JDK 11.0.32.1:

• After periodic-refresh implementation: :usvm-util:check 65 passed; :usvm-core:check 274 passed and one existing skipped test; :usvm-sample-language:check 12 passed.
• After HashSet optimization: :usvm-core:check again passed (274 passed, one existing skipped test).
• Strict Detekt on changed core main/tests, queue main/tests and the manual JVM experiment: no findings.
• All 28 retained benchmark processes completed; the four distance-guidance Guava analyses stopped at the explicit timeout, while random baselines reached 100,000 steps. Benchmark is tagged manual and excluded from ordinary JVM tests.
• git diff --check passed.

Tests cover the 128-selection boundary, repeated peeks, shared snapshots, selection accounting, batched updates, interval reset, saturation/later goals, retry after failed refresh, both comparator directions, cached selections, equal-priority retention and linear heapify comparisons. Existing goal semantics, CFG distance reuse and selector composition also pass.

Goals may be statements, exact edges or caller-defined types; distance semantics, PBT admission, source/runtime identity and native confirmation remain caller responsibilities. Core building block for #524; refs #399.