Re: [PATCH bpf-next 1/1] bpf: Avoid one round of bounds deduction

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

On Thu, Mar 05, 2026 at 03:10:00AM -0800, Eduard Zingerman wrote:
> On Thu, 2026-03-05 at 14:54 +0800, Shung-Hsi Yu wrote:
> > On Wed, Mar 04, 2026 at 04:48:43PM -0800, Ihor Solodrai wrote:
> > > On 3/3/26 11:27 AM, Paul Chaignon wrote:

[...]

> > > Side note: you might be interested to know that Eduard is working on
> > > consolidating signed and unsigned domains [1].
> > 
> > \o/
> > 
> > When I last look into this[1] there's was the "Interval Analysis and
> > Machine Arithmetic: Why Signedness Ignorance Is Bliss" paper[2] that
> > looks rather promising. And lately there was also "Program Analysis
> > Combining Generalized Bit-Level and Word-Level Abstractions"[3] (haven't
> > read) that seems more specific to BPF verifier.
> 
> Thank you for the links, I've only seen [1].
> I was about to send [a], feeling really smug about cbmc tests.
> But then a much simpler solution [b] occurred when figuring out why
> 64-bit test can't be written.

If I understand [b] correctly, it's the 32-bits equivalent of
00bf8d0c6c9b ("bpf: Improve bounds when s64 crosses sign boundary"). I
didn't make the 32bits change back then, but it makes sense that we
would eventually need it :)

If you end up sending [b] as a patchset, note that we still have a
selftest for which we skip the invariant violation check:

  $ git grep -hB3 "\!BPF_F_TEST_REG_INVARIANTS" tools/testing/selftests/bpf/progs/verifier_bounds.c
  SEC("xdp")
  __description("bound check with JMP32_JSLT for crossing 32-bit signed boundary")
  __success __retval(0)
  __flag(!BPF_F_TEST_REG_INVARIANTS) /* known invariants violation */

I believe, with your patch, we would be able to invert that test flag. 

> 
> I'll probably continue playing with cnums at leisure pace.
> 
> [a] https://github.com/eddyz87/bpf/tree/cnum-sync-bounds
> [b] https://github.com/eddyz87/bpf/tree/32-bit-range-overflow

IIUC, your current patch doesn't maintain a cnum domain alongside the
existing abstract domain, but instead builds it only when needed, in
is_scalar_branch_taken. Would your long-term goal still be to replace
the existing four ranges with two cnum domains?

Either way, I believe it will require significant changes in Agni so
I'm interested to see where this goes :)