| Age | Commit message (Collapse) | Author |
|---|
|
Representation
--------------
Represent ALU32 recurrences as:
w0 += step -> (zext32 (linear r0 step))
Extend simplify() rules to maintain the above form for latch
expressions. E.g. for a post-condition loop such as:
w0 = 0;
l: w0 += 1;
if w0 != 3 goto l;
exit;
SCEV at header: (zext32 (linear r0 1))
Initial SCEV at latch: (zext32 (+ (zext32 (linear r0 1)) 1))
Simplified SCEV at latch: (zext32 (+ (zext32 (linear r0 1)) 1))
-> (zext32 (+ (linear r0 1) 1))
-> (zext32 (linear (+ r0 1) 1))
Iterations count computation
----------------------------
- Extract the main iteration-count logic from compute_max_iters() into
compute_backedge_taken_count(). Reuse its 64-bit arithmetic after
sign/zero extending the latch operands.
- Reject the computed count if the predicted exit value falls outside
signed/unsigned 32-bit range, e.g.:
w0 = 0x7ffffffe;
l: w0 += 1;
if w0 s<= 0x7fffffff goto l;
The 64-bit computation predicts an exit at S32_MAX + 1, but the
32-bit value wraps to S32_MIN and the comparison remains true.
- Handle mixed 64-bit/32-bit comparisons/recurrences only when initial
bounds and step fit in 32-bit ranges, e.g.:
w0 = 0;
r1 = 0x100000003 ll;
l: w0 += 1;
if r0 != r1 goto l;
Truncating the bound to 32 bits would predict three header visits.
However, `w0 += 1` keeps r0 within [0, U32_MAX], so it can never
be equal to the 64-bit bound.
Widened bounds computation
--------------------------
- Update linear_bounds() to truncate the initially computed 64-bit
range to 32 bits, then zero-extend it to obtain the 64-bit range
of iteration values. Step computation needs to handle:
- unsigned 32-bit wraparound;
- entry and zero-extended iteration values disagreeing on base/step.
- Union both ranges with the corresponding register ranges at entry,
since the entry value need not be zero-extended.
- Extend `struct bounds` to keep both {32,64}-bit ranges and pass both
to bpf_set_reg_range(). A 64-bit range alone loses useful 32-bit
information, e.g.:
entry = 0, step = -1, two header visits
r64: [0, U32_MAX]
r32: [-1, 0]
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261020-scev-32bit-v1-1-838f34f9f0cd@gmail.com
|
|
For whatever reason gcc built-ins implementing 64-bit division are not
wired into 32-bit kernel builds:
ld: kernel/bpf/scev.c:2074:(.text+0x4512): undefined reference to `__udivdi3'
ld: kernel/bpf/scev.c:2141:(.text+0x475b): undefined reference to `__udivmoddi4'
Instead, one has to use div64_u64() and div64_u64_rem() explicitly.
Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Reported-by: Tejun Heo <tj@kernel.org>
Reported-by: kernel test robot <lkp@intel.com>
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/bpf/20261010205828.3366892-1-eddyz87@gmail.com
Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
|
|
For loops like this:
int arr[10];
for (int i = 0; i < 10; i++)
arr[i] = i;
use(arr[i]);
SCEV-based loop widening converts `i` from being enumerated 10 times
as a constant value 0, 1, ..., 9 to being enumerated once as a range
[0..9]. From the point of view of the main verification pass, this
replaces constant-offset stack access with varying-offset
stack access.
The verifier tracks stack values accessed through varying offsets much
less precisely than those accessed via constant offsets.
For example, the read at use(arr[i]) would yield STACK_MISC.
Precision might be lost for the following operations:
- spills (BPF_ST/STX to the stack): stored value can no longer be
recovered when read back, e.g. after the loop;
- fills (BPF_LDX from the stack): a varying-offset read of a spilled
pointer yields a SCALAR_VALUE, so the pointer is lost.
- calls that construct objects on the stack (dynptr, iter, irq_flag,
res_spin_lock): the stack argument is required to have a
constant offset.
This commit adds logic to avoid widening registers used by
such instructions:
- During the main SCEV computation stage, collect_store_base_regs():
- inspects instructions accessing the stack (spill, fill, call to a
function listed in bpf_needs_fixed_stack_off), and
- if there is a SCEV expression for a stack base address register,
records which registers the expression depends on in
the bpf_loop->store_base_reg field.
- `store_base_reg`s accumulated for nested loops are propagated
to outer loops as well.
- During the loop-widening stage, bpf_compute_loop_iters() refuses to
widen a loop when some of the registers the loop changes appear in
store_base_regs.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-35-bcba9bc53ac9@gmail.com
|
|
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 <self> <step>): entry value + iteration# * constant step.
- (reg <self>): 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 <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-34-bcba9bc53ac9@gmail.com
|
|
Assign algebraic expressions to loop variables (registers and stack
spills), describing how their values evolve across iterations. These
summaries provide symbolic input for the subsequent widening patch.
The algorithm draws on ideas from the following papers:
- "Symbolic Evaluation of Chains of Recurrences for Loop Optimization"
Robert A. van Engelen, 2000
- "The CR# Algebra and its Application in Loop Analysis and Optimization"
Robert A. van Engelen, 2004
The analysis proceeds in two phases:
- Compute expressions for one symbolic iteration: start each variable
with a reference to its input value, apply instruction effects and
join expressions where control-flow paths merge.
- Convert the resulting backedge updates to recurrences at the header,
then substitute these recurrences into expressions at the latch.
Analyze loops innermost first. Within each loop, visit blocks in
topological order (reverse postorder, with backedges ignored and nested
loops collapsed). Treat each nested loop as an opaque operation:
preserve its invariant values, forget the others and continue at its
exits, without expanding its iterations.
For example, using 64-bit arithmetic:
0: r7 = 5;
1: r6 = 0;
2: do { // header
3: if (r6 == 1)
4: r7 = 10;
5: r6 += 1;
6: } while (r6 < 3); // latch
Expressions use symbolic inputs r6 and r7; the concrete values from
lines 0-1 are supplied later by the main verifier.
First phase:
------------
At each instruction, an environment maps register numbers to their
current expressions. Transfer functions update this mapping, while
joins merge the environments arriving along different paths.
For illustration, follow each branch separately to the backedge:
- At 3, take the path skipping 4: r6 = r6, r7 = r7.
- At 5, transfer(r6 += 1): r6 = r6 -> r6 = (+ r6 1).
- At 2, the first path contributes r6 = (+ r6 1), r7 = r7.
- At 4, on the other path from 3, transfer(r7 = 10):
r7 = r7 -> r7 = 10.
- At 5, transfer(r6 += 1): r6 = r6 -> r6 = (+ r6 1).
- At 2, join the two paths' contributions:
join((+ r6 1), (+ r6 1)) = (+ r6 1) for r6;
join(r7, 10) = (any r7 10) for r7.
Equal expressions stay unchanged; different expressions become ANY
alternatives. These summarize one iteration, without unrolling the loop.
Second phase:
-------------
The update r6 = (+ r6 1) says that each iteration adds 1 to r6.
Repeating this update n times gives r6_entry + n, a linear recurrence.
- At header 2, r6 = (+ r6 1) becomes (linear r6 1), meaning
r6_entry + n, where n counts iterations from zero.
- At latch 6, substitute this recurrence into (+ r6 1):
(+ (linear r6 1) 1) simplifies to (linear (+ r6 1) 1),
meaning r6_entry + 1 + n.
- At both points, r7 retains (any r7 10): either its entry value
or 10. ANY records alternatives, not numeric ranges or the path
conditions selecting them. Unchanged variables retain their inputs.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-33-bcba9bc53ac9@gmail.com
|
