From 6ccf49f7932781f441e1e52459a4053bbfd19ddb Mon Sep 17 00:00:00 2001 From: Eduard Zingerman Date: Fri, 9 Oct 2026 03:47:52 -0700 Subject: bpf: Use SCEV to widen bounded loops Loop-bound computation and register widening =========================================== During the main verification pass, use SCEV expressions and register values at the entry to the loop to estimate the number of iterations the loop might execute. Use this number to widen loop induction variables. For example: 0: r7 = 5; 1: r6 = 0; 2: while (r6 < 3) { // latch 3: if (r6 == 1) 4: r7 = 10; 5: r6 += 1; 6: } 8: use(r7); - Scalar evolution expressions (SCEVs) at the latch are: - r6 = (linear r6 1) - r7 = (any r7 10) - For this pre-condition loop, this corresponds to the linear inequality `r6_entry + n < 3`. With r6_entry = 0, the inequality is `n < 3`. - Hence infer that r6's range at line 2 is [0,3], including the final failed test. The body starts with r6 in [0,2]. - r7's (any r7 10) expression means that its initial value 5 from line 0 is joined with 10 from line 4: it is widened to [5,10] within and after the loop. Currently such inference is supported for: - Reducible loops with one backedge and complete backedge/exit lists. - A linear latch dominating the backedge, with one successor exiting the loop. Additional exits are allowed; they can shorten execution. - 64-bit arithmetic and comparisons whose continuation condition normalizes to signed/unsigned < or <=, or !=. - Initial counter, latch offset, slope and bound evaluable as constants at loop entry, yielding a finite, representable iteration bound. - Values with an eligible type at loop entry, e.g. SCALAR_VALUE or PTR_TO_STACK, but not PTR_TO_CTX. In order for widening to proceed, every register live at the loop entry has to have a SCEV that can be widened. Currently, the following expressions are supported: - (linear ): entry value + iteration# * constant step. - (reg ): loop invariant; keep its entry value unchanged. - (any ...): join the entry value with immediates or invariant registers; types must match, and immediates require SCALAR_VALUE. Main verification loop integration ================================== Before proceeding with the usual instruction processing, do_check() takes the following steps at loop entries (H): - Checks whether the loop can be widened and obtains its iteration bound (scev.c:bpf_compute_loop_iters()). - If it can, saves an unwidened checkpoint E0, which will be used as a base for deriving widened values throughout this invocation of the loop. - Widens registers in the current state using E0 and SCEV expressions computed for H (scev.c:bpf_widen_scev_regs()). - Pushes a per-frame loop-stack record to the current verifier state. For terminating loops, the record stores E0 and the iteration bounds. - Lets is_state_visited() create a new checkpoint W at the same header, now containing the widened values, and proceeds with normal checking. - On an exit edge, pops the loop record and verifies the exit path normally. is_state_visited() treats a loop proven to terminate like an iterator-based loop: RANGE_WITHIN comparison attempts to establish convergence against a checkpoint whose exploration is still in progress. For example: r0 = 0; H: r0 += 1; if (r0 != 3) goto H; exit; first H: prove H_count = 3; save E0(r0 = 0) widen r0 to [0,2]; push the loop record save W(r0 = [0,2]) body: r0 becomes [1,3]; fork at the conditional exit: r0 = 3; pop the loop record and check exit backedge: r0 = [1,2]; clamp, then match with W and prune Clamping -------- Independent register ranges lose correlations between induction variables. For example: r6 = 0; r7 = 0; do { r6 += 1; r7 += 2; } while (r6 < 3); use(r7); header: r6 in [0,2], r7 in {0,2,4} body: r6 in [1,3], r7 in {2,4,6} backedge: r6 in [1,2], r7 still in {2,4,6} The latch narrows r6 but does not propagate this refinement to r7. To account for this, before comparing states on a backedge, scev.c:bpf_clamp_scev_regs() recomputes r7's range from E0 and the saved iteration bound, then intersects the current range {2,4,6} with the recomputed {0,2,4}, arriving at {2,4}. Signed-off-by: Eduard Zingerman Signed-off-by: Alexei Starovoitov Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-34-bcba9bc53ac9@gmail.com --- tools/testing/selftests/bpf/progs/verifier_gotox.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'tools/testing') diff --git a/tools/testing/selftests/bpf/progs/verifier_gotox.c b/tools/testing/selftests/bpf/progs/verifier_gotox.c index dc7baa0f2458..84302a122ccf 100644 --- a/tools/testing/selftests/bpf/progs/verifier_gotox.c +++ b/tools/testing/selftests/bpf/progs/verifier_gotox.c @@ -511,7 +511,7 @@ __naked void too_many_gotox_edges(void) SEC("socket") __description("gotox-edges-at-limit") -__success __retval(0) +__failure __msg("Too many nested loops") __naked void gotox_edges_at_limit(void) { asm volatile ( @@ -519,6 +519,10 @@ __naked void gotox_edges_at_limit(void) * 1000 gotox * 1000 targets = 1,000,000 CFG edges. At run * time, each block loads the next table entry and jumps to * the following block, so the program terminates. + * + * Every block can jump to every later block, so the CFG is + * a nest of ~1000 irreducible loops, deeper than the + * verifier's loop stack; the program is rejected. */ GOTOX_TABLE_BEGIN(1000) ".rept 1000;" -- cgit v1.2.3