Re: [PATCH v2 bpf-next 3/6] bpf: Exit early if reg_bounds_sync gets invalid inputs

Eduard Zingerman
2026-04-01T20:21:05Z

On Wed, 2026-04-01 at 15:36 -0400, Harishankar Vishwanathan wrote:
> On Wed, Apr 1, 2026 at 8:21 AM Paul Chaignon <paul.chaignon@gmail.com> wrote:
> > On Tue, Mar 24, 2026 at 12:33:51PM -0700, Eduard Zingerman wrote:
> > > On Tue, 2026-03-24 at 15:28 -0400, Harishankar Vishwanathan wrote:
> > > > On Mon, Mar 23, 2026 at 2:47 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > > > >
> > > > > On Fri, 2026-03-20 at 17:49 +0100, Paul Chaignon wrote:
> > > > >
> > > > > [...]
> > > > >
> > > > > > @@ -2786,8 +2786,13 @@ static void __reg_bound_offset(struct bpf_reg_state *reg)
> > > > > > reg->var_off = tnum_or(tnum_clear_subreg(var64_off), var32_off);
> > > > > > }
> > > > > >
> > > > > > +static bool range_bounds_violation(struct bpf_reg_state *reg);
> > > > > > +
> > > > > > static void reg_bounds_sync(struct bpf_reg_state *reg)
> > > > > > {
> > > > > > + /* If the input reg_state is invalid, we can exit early */
> > > > > > + if (range_bounds_violation(reg))
> > > > > > + return;
> > > > > > /* We might have learned new bounds from the var_off. */
> > > > > > __update_reg_bounds(reg);
> > > > > > /* We might have learned something about the sign bit. */
> > > > >
> > > > > Is it possible for the invariants violation to manifest after
> > > > > __update_reg{32,64}_bounds() calls, once cross domain boundaries are
> > > > > propagated?
> > > >
> > > > The short answer is yes.
> > > >
> > > > The sub-sync functions, i.e. __update_reg_bounds, __reg_deduce_bounds,
> > > > __reg_bound_offset are individually sound (checked by Agni).
> > > > This means that they preserve any concrete value x that is contained in all
> > > > the range bounds and tnum inputs, after refinement.
> > > >
> > > > But if in the input, there is no concrete value x that is contained in
> > > > ALL the range bounds and tnum, then an invariant violation can
> > > > manifest. Note that this can happen in the presence
> > > > of the current early exit commit, i.e., even if
> > > > range_bounds_violation(reg) is false.
> > > >
> > > > For example,
> > > >
> > > > before reg_bounds_sync: s64=[1, 1], tnum=0
> > > > after reg_bounds_sync: s64=[1, 0] tnum=0
> > > >
> > > > Could you elaborate on your concern? Did you perhaps imply that we should
> > > > be checking for reg_bounds_violation in
> > > > simulate_both_branches_taken after each sub-sync function?
> > >
> > > My main concern is that we might loose useful signal.
> > > It would be nice to adjust reg_bounds_sync() such
> > > that it would stop (e.g. return false, as you suggested previously)
> > > if it hits invariant violation mid-step.
> >
> > We discussed this with Hari and agree it would be good to use
> > transient/mid-step invariant violations as a signal to improve
> > precision. I'd however prefer to implement that as a follow-up, to keep
> > the current patchset small and focused on fixing the invariant
> > violations that cause kernel warnings and program rejections. It sounds
> > like we may want to backport this at some point, so it's easier if it
> > keeps a restrained scope.
> >
> > The "transient" invariant violations already exist today and using them
> > will only improve precision (potentially allow the verifier to accept
> > more program than it does today). I would see that as an improvement
> > rather than a fix we'd want to backport.
> >
> > Hari thinks we can also use the empty intersection checks he mentioned
> > in the other thread [1] to avoid/use these transient invariant
> > violations. It would allow us to use this as a signal to improve
> > precision without making reg_bounds_sync more complex (and harder for
> > Agni to verify). I'll let him explain, but as mentioned in the other
> > thread, it still needs a bit of benchmarking.
>
> The idea is that since reg_bounds_sync() and its sub-functions are sound,
> invariant violations (I'll call these range_bound_violations) can occur only
> when the *inputs* to these functions themselves have (i) range_bounds_violations
> (ii) an empty intersection, i.e. there does not exist a concrete value x that is
> contained in all the 5 abstract values. Let's say we have a way to detect empty
> intersections (as discussed in the other thread). We early return on empty
> intersections in reg_bounds_sync():
>
> reg_bounds_sync(reg) {
> if (empty_intersection(reg) || range_bounds_violation(reg))
> return;
>
> __update_reg_bounds(reg);
> // ...
> }
>
> That way reg_bounds_sync() preserves empty intersections and
> range_bounds_violations, rather than allowing the intermediate sub-sync
> functions to "fix" them. It's equivalent to the idea of returning every time we
> hit an invariant violation midstep, without the extensive code changes

This makes sense.

>
> As Paul mentioned we were discussing empty intersection checks in the other
> thread, and I agree the two ideas are probably better combined in a follow
> up that:
> (1) Introduces empty intersection checks
> (2) Uses them in simulate_branches in addition to range_bounds_violation, as
> discussed in the other thread
> (3) Uses them to exit early in reg_bounds_sync()
>
> That way we can keep this patchset focused on fixing the invariant violations.

Ok, we can go with a follow-up.
What are remaining steps for this patch-set?
Here are outstanding comments:
1. https://lore.kernel.org/bpf/33c006d7275cb443b5750f062cb78c38449a7537.camel@gmail.com/
resolved as noop
2. https://lore.kernel.org/bpf/ed85ac25cd315ac4273de335943f9f3a2c1f36e8.camel@gmail.com/
resolved, only if inputs are in bogus state, will be handled by a follow-up.
3. https://lore.kernel.org/bpf/7vwyzvy7cwy2n4c52fcurg4dnv4bqijtovmkeh3zgu6ey266vc@dtt3r5usvev5/
Some wording nits, do you intend to fix those?
4. https://lore.kernel.org/bpf/847173114a13630e1512ad05375c6b407720a916.camel@gmail.com/
Will be resolved as a follow-up.
5. https://lore.kernel.org/bpf/87ikamjv5q.fsf@gmail.com/
resolved as noop.

Is the above assessment correct?
Beside (3) is there anything you'd like to change or should we go with v2?