vbpf / prevail / 26403522463

push

github

Extract Extrapolator to own the fixpoint iteration policy

Introduce an Extrapolator class (src/crab/) that encapsulates the entire
fixpoint acceleration strategy: ascending with widening, descending with
narrowing, convergence checks, and constant-limits clamping.

The Extrapolator is constructed once per analysis as an immutable strategy
object. Its single entry point, compute_fixpoint(initial, step), runs both
phases internally — the iterator provides a step function and receives the
converged invariant. All per-cycle state (iteration counters, current
invariant) is local to compute_fixpoint.

The iterator's cycle handler reduces to:
  converged = _extrapolator.compute_fixpoint(initial, run_cycle_body);

EbpfDomain::widen loses its policy parameters (to_constants, context,
loop_counters) and becomes a pure domain widening operation.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

46 of 50 new or added lines in 4 files covered. (92.0%)

8924 of 10324 relevant lines covered (86.44%)

6844913.76 hits per line