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

[Paul Chaignon <paul.chaignon@gmail.com>]

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.

1: https://lore.kernel.org/bpf/CAM=Ch05-XWF-x_VzUZAWhRO9eum-bjdutuwvPXEcOvnx_0omAA@mail.gmail.com/