Re: [PATCH bpf-next v3 19/51] bpf: representation for intervals with steps

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2026-10-09 at 12:07 +0000, bot+bpf-ci@kernel.org wrote:
> > bpf: representation for intervals with steps
> 
> TL;DR:
> - Commit message says eq/neq branches ignore base/step, but they appear to
>   change branch pruning
> - Comment in reg_bounds_sync() names reg_umin() where reg_smin() seems
>   intended (nit)
> 
> >     bpf: representation for intervals with steps
> > 
> >     Extend scalar register tracking with a linear "base + step * k" description:
> >     each scalar carries two u16 fields, base and step (invariant: base < step),
> >     recording that its value is some point on the line base + step * k.
> >     A fresh scalar starts as base=0, step=1, i.e. any integer.
> > 
> >     This lets the verifier reason about strided values, e.g. an index multiplied
> >     by an element size, which neither the min/max bounds nor the tnum can capture
> >     for a non-power-of-2 stride. Such reasoning is necessary to allow
> >     array access with a variable offset through PTR_TO_BTF_ID, e.g.
> >     for expressions like p->arr[i].field.
> > 
> >     reg_bounds_sync() uses the description in two ways:
> >     - __reg_bound_offset() clears the low bits of var_off implied by the number
> >       of trailing zeros shared by base and step.
> >     - __update_bounds_from_step() intersects the 64-bit range with the line via
> >       cnum64_intersect_linear(), snapping smin/smax to actual points on it.
> >       This is the last step of the sync, as refining the range from var_off
> >       can move the bounds off the line.
> > 
> >     range_within() is extended to check whether the cur register's equation
> >     describes a subset of the points described by the old register's equation.
> > 
> >     Scalar ALU operations update base/step as follows:
> >     - ADD of a constant (including pointer + scalar): keep step, shift base;
> >     - MUL by a constant: scale step and base by the constant;
> >     - LSH by a constant: scale step and base by the corresponding power of two;
> >     - sign extension: keep the register unchanged if all values fit the target
> >       type, reset to base=0, step=1 otherwise;
> >     - All other operations reset to base=0, step=1.
> > 
> >     Branch (eq/neq) checks do not take into account base/step yet.
> > 
> >     Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
> 
> The changelog says "Branch (eq/neq) checks do not take into account base/step
> yet."  Is that accurate for this patch?
> 
> is_scalar_branch_taken() ends by calling simulate_both_branches_taken().  That
> function runs regs_refine_cond_op() and reg_bounds_sync() on copies of the
> registers, and treats range_bounds_violation() as proof that a branch is dead.
> 
> reg_bounds_sync() now ends with __update_bounds_from_step(), and
> cnum64_intersect_linear() returns CNUM64_EMPTY when the refined range holds no
> point of base + step * k.
> 
> For example, take r1 in [0, 30] with step=3, base=0 (say from r0 *= 3 with r0
> in [0, 10]), followed by:
> 
>     if r1 == 4 goto L
> 
> The tnum and min/max checks cannot decide this.  In
> simulate_both_branches_taken() the true branch refines r64 to [4, 4], and then
> in cnum64_intersect_linear():
> 
>     d = imod(base - imod(smin, step), step);   /* imod(0 - 1, 3) == 2 */
>     if ((u64)smax - (u64)smin < d)              /* 0 < 2 */
>             return CNUM64_EMPTY;
> 
> So the JEQ branch is treated as dead (pred = 0) purely because of
> base/step.  JNE behaves the same way, and JNE against a range edge now snaps
> the bound onto the line ([0, 29] becomes [0, 27]).
> 
> This looks sound as long as base/step are sound, but it is a real change to
> branch pruning, and mark_chain_precision() is called on the compared registers
> whenever pred >= 0.  Should the changelog describe this instead of saying
> eq/neq branches ignore base/step?

Kind of. Sort of.
There is no explicit handling in is_scalar_branch_taken(),
as well as it is not wired for pointers.
I didn't think through if simulate_both_branches_taken()
is sufficient or some explicit rules is_scalar_branch_taken()
might be of use as well.

> 
> > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > index 47a632a6749a..f5b2500335a7 100644
> > --- a/kernel/bpf/verifier.c
> > +++ b/kernel/bpf/verifier.c
> 
> [ ... ]
> 
> > @@ -2208,6 +2337,15 @@ static void reg_bounds_sync(struct bpf_reg_state *reg)
> >  	 * then new var_off is (0; 0x7f...fc) which improves our umax.
> >  	 */
> >  	__update_reg_bounds(reg);
> > +	/*
> > +	 * Both tnum and base+step define a sequence of points,
> > +	 * potentially w/o intersection, or intersecting after N
> > +	 * tnum_step()'s, where N can be large. On the other hand,
> > +	 * step+base *must* be in sync with r64 in order for
> > +	 * array traversal logic starting at reg_umin() to be sound.
>                                           ^^^^^^^^^^
> 
> This isn't a bug, but is reg_umin() the right function to name here?  The
> array traversal logic isn't part of this patch.

Yes, this should be reg_smin().