| Age | Commit message (Collapse) | Author |
|---|
|
A compare with pkt_end sets 'range' in all packet pointers that have the
same id. Then 'range - offset' bytes from the pointer are in the packet.
When a state returns to the head of a counted loop, bpf_clamp_scev_regs()
gives a new id to a packet pointer, and the offsets of all iterations. It
does not change the range. But the range is valid only together with the
old id and the old offsets.
1: ; R6=pkt(id=1,r=0,off=0..100)
r5 = r6
r5 += 100
if r5 > pkt_end goto 2f ; R6=pkt(id=1,r=200,off=0..100)
r6 += 100 ; R6=pkt(id=1,r=200,off=100..200)
r9 += 1
if r9 < 2 goto 1b ; clamp: R6=pkt(id=2,r=200,off=0..100)
after bytes from r6 that the verifier accepts
---------------------- ---------------------------------------
the compare 100, correct
r6 += 100 0, correct
the clamp 100, incorrect. Nothing compared this r6
Usually the verifier prunes the state at the head, and the range has no
effect. The verifier continues with the state when a different part of it
is not within the state at the head. A flag in a 32-bit spill is
sufficient. Then the prog reads and writes after pkt_end. A write to
skb_shared_info crashes the kernel.
Take the range that the pointer has at the entry of the loop. No compare in
the loop found this range, so it is valid in all iterations. The state at
the head has the same range, so the verifier prunes as before.
Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261027190314.1440199-15-alexei.starovoitov@gmail.com
|
|
When a state returns to the head of a counted loop, bpf_clamp_scev_regs()
replaces the range of each register that changes by a constant step. The
new range is the range over all iterations. The function calculates it from
the register in the state that entered the loop. For a pointer this range
is the range of its offsets.
A call in the loop can invalidate the pointer. bpf_skb_pull_data() does it
to packet pointers, bpf_ringbuf_discard() does it to ringbuf memory. Then
the register is an unknown scalar. Scalar evolution does not see that, and
the clamp gives the offsets of the pointer to the scalar.
r6 = bpf_ringbuf_reserve() ; R6=ringbuf_mem
r7 = r6
1: if first iteration goto 2f
r1 = map_value
r1 += r6 ; accepted: R6 is 0 or 1
r0 = *(u8 *)(r1 + 0)
goto 3f
2: bpf_ringbuf_discard(r7) ; R6=scalar()
3: r6 += 1
r9 += 1
if r9 < 2 goto 1b ; clamp: R6=scalar(umax=1)
At run time r6 is the address of the ringbuf memory plus 1. The prog adds
it to a pointer to a map value, and the kernel crashes in the access.
Do not clamp a register that has a different type than at the entry of the
loop. Such a state is not within the state at the head. Thus the verifier
continues with it, and r6 stays an unknown scalar.
Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261027190314.1440199-14-alexei.starovoitov@gmail.com
|
|
Scalar evolution widens counted loops. Since that change the verifier
rejects a loop over the per-cpu values of a map element:
SEC("iter/bpf_map_elem")
...
for (i = 0; i < n; i++) {
out[i] = *(__u32 *)pptr;
pptr += 8;
}
loop header at 12, widening r2 to 0..56 step 8
R2 invalid variable buffer offset: off=0, var_off=(0x0; 0x38)
pptr is a pointer to a buffer (PTR_TO_BUF). Scalar evolution replaces its
offset with the range over all iterations. But __check_buffer_access()
accepts only a constant offset. Thus a prog cannot use a widened
PTR_TO_BUF.
Do not widen it. Then the verifier verifies the loop one iteration at a
time, as it did before.
loop before SCEV with SCEV this patch
-------------------------------- ----------- ---------- ----------
counts in i, reads through pptr loads rejected loads
counts in p ('p < end'), no read 1M insns loads 1M insns
counts in p, reads through p 1M insns rejected 1M insns
The verifier cannot decide a comparison of two pointers to a buffer. Thus
it follows 'p < end' until the limit of 1M insns.
bpf_iter_bpf_percpu_array_map.c and bpf_iter_bpf_percpu_hash_map.c have the
first loop. They load today because num_cpus is volatile. The prog reads
the bound again in each iteration. Scalar evolution cannot count such a
loop, and it widens nothing.
Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261027190314.1440199-12-alexei.starovoitov@gmail.com
|
|
After 'r3 = r8; r3 += 4' the verifier knows that r3 == r8 + 4. The two
registers have the same id, and r3 keeps the difference in reg->delta. When
the prog compares one of them with a constant, sync_linked_regs()
calculates the range of the other register from the difference of the two
deltas.
At a loop head scalar evolution widens a register: it replaces the register
with its range over all iterations. Then the register is not linked to
other registers. scratch_widened_reg_id() clears reg->id, but it does not
clear reg->delta. A subsequent copy of the register gets the stale delta.
Then the range of the copy is incorrect by this delta.
r3 = r8
r3 += 4 ; R3=scalar(id=1+4)
1: ; r3 is widened: no id, delta is still 4
r4 = r3 ; id=2 and delta 4 in both
r4 += 1 ; R4=scalar(id=2+1)
if r3 > 10 goto 3f ; R3 <= 10, R4 = R3 + 1 - 4 <= 7
if r4 <= 7 goto 2f
... ; not verified, r4 is up to 11 here
The verifier does not verify code that can run. Use clear_scalar_id(). It
clears id and delta together. Move it to bpf_verifier.h, so that scev.c can
call it.
Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261027190314.1440199-8-alexei.starovoitov@gmail.com
|
|
- Print large 32-bit bounds without sign extension.
- Omit 32-bit bounds when they coincide with 64-bit bounds.
Before:
loop header at ..., widening r0 to 0x80000000..0xffffffff (s32 0xffffffff80000000..-1) step 1
loop header at ..., widening r0 to 0..3 (s32 0..3) step 1
After:
loop header at ..., widening r0 to 0x80000000..0xffffffff (s32 0x80000000..-1) step 1
loop header at ..., widening r0 to 0..3 step 1
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261026-scev-simpler-clamp-v2-6-f373aec9825f@gmail.com
|
|
The compiler can preserve an induction variable across a call by
copying it to a callee-saved register. For example:
w1 = 0;
loop:
w7 = w1;
call foo;
w1 = w7;
w1 += 2;
if w7 < 10 goto loop;
When building expressions for the loop body, each 32-bit move adds a
zero extension:
w7 = w1; r7 = (zext32 r1)
w1 = w7; r1 = (zext32 (zext32 r1))
w1 += 2; r1 = (zext32 (+ (zext32 (zext32 r1)) 2))
The existing ALU32 simplification rules allow recognizing the header
SCEV for r1 as:
(zext32 (linear r1 2))
Substituting this SCEV into r7's expression at the latch produces:
(zext32 (zext32 (linear r1 2)))
Add the simplification rule:
(zext32 (zext32 X)) -> (zext32 X)
This allows recognizing the saved induction variable in r7 as a
32-bit linear SCEV and computing the loop iteration bound.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261026-scev-simpler-clamp-v2-5-f373aec9825f@gmail.com
|
|
The comment before `total_change` computation:
/*
* compute_backedge_taken_count() guarantees that 'total_change'
* does not overflow in 64-bit domain.
*/
total_change = initial + step * backedge_taken_count;
Is not true before the check:
if (backedge_taken_count >= U32_MAX - 1)
return false;
Move the check before `total_change` computation in order to reconcile
the code with comments. Old position is not a bug the check was
performed either way.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261026-scev-simpler-clamp-v2-4-f373aec9825f@gmail.com
|
|
scev.c:bpf_clamp_scev_regs() is called each time verifier returns to a
loop header via a backedge. It's purpose is to re-establish computed
variable ranges for registers with linear SCEVs.
It can be defined as:
- For each register R with linear SCEV compute:
- loop_range(R) := entry_range(R) * iterations_count
- range(R) := range(R) ∩ loop_range(R)
Such formulation is necessary to avoid ranges over-approximation in
examples like below:
r1 = 0; SCEVs: r1 = (linear r1 1)
r3 = 0; r3 = (linear r3 1)
loop: r3 += 1;
r1 += 1;
if r1 < 5 goto loop;
r0 = 0;
exit;
- At loop entry r3 is widened to be in a range r3 ∈ {0,1,2,3,4}.
- After increment it becomes r3 ∈ {1,2,3,4,5}.
- On a second iteration the bpf_clamp_scev_regs() forces r3 to become
r3 ∈ {1,2,3,4}. W/o clamping logic r3 range wouldn't shrink
preventing loop from converging in states.c:states_equal().
However, intersection logic might lead to assigning an empty range to
a register, as in example below:
r1 = 0; verification
r3 = 0; path
loop: r3 += 1; | <---------.
if r3 != 5 goto +0; | r3 ∈ {5} |
r1 += 1; | |
if r1 != 5 goto loop; '-----------'
r0 = 0;
exit;
- At header r3 ∈ {0,1,2,3,4}.
- While exploring the branch `if r3 != 5 goto ...` with r3 ∈ {5}.
- On a second iteration:
r3 := {0,1,2,3,4} ∩ {5} = ∅
Which stops verification with the following error:
verifier bug: scev clamp produced empty range for r3
Technically this means that the current verification path is
impossible at runtime and should not be traced further.
This commit mitigates the above by removing the intersection logic,
the function is now defined as:
- For each register R with linear SCEV compute:
- range(R) := entry_range(R) * iterations_count
This is still sound, provided that SCEV expressions loop execution
counts are correct.
Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261026-scev-simpler-clamp-v2-2-f373aec9825f@gmail.com
|
|
Avoid inferring loop bounds for the following program shapes:
32-bit latch (A) | 32-bit recurrence (B)
-------------------------+--------------------------
r1 = ... pointer ... | r1 = ... pointer ...
r2 = ... pointer ... | r2 = ... pointer ...
l: r1 += 8 | l: w1 += 8
... | ...
if w1 < w2 goto l | if r1 < r2 goto l
(A) Scalar bounds for pointers represent only offsets from their
common origin values. The 32-bit operations also depend on the
runtime base address: the addresses can wrap at 32 bits without
the tracked offsets wrapping. Thus, offsets alone do not determine
the iteration count.
(B) 32-bit operations on pointers either prohibited (wX += 1)
or convert them to scalars (wX = wX). No need to deal with
this at SCEV level.
Fixes: 32e962577d2d ("bpf: Support 32-bit linear scalar evolution")
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261026-scev-simpler-clamp-v2-1-f373aec9825f@gmail.com
|
|
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
|
