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

Harishankar Vishwanathan
2026-04-01T19:36:39Z

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

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.

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