Re: [PATCH 1/2] bpf: deduce_bounds_64_from_32 tightening with circular range logic

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

On Thu, Apr 16, 2026 at 12:43:44AM -0700, Eduard Zingerman wrote:
> On Thu, 2026-04-16 at 11:52 +0800, Shung-Hsi Yu wrote:
> > On Wed, Apr 15, 2026 at 12:12:45AM -0700, Eduard Zingerman wrote:
> > > On Fri, 2026-04-10 at 09:40 -0300, Helen Koike wrote:
> > > > Unify handling of signed and unsigned using circular range logic.
> > [...]
> > > Hi Helen, Harishankar, Shung-Hsi, Paul,
> > > 
> > > I think this algorithm is correct and covers all cases discussed earlier.
> > > I also prepared simple correctness check using cbmc in [1].
> > 
> > Given the "Fix invariant violations and improve branch detection" is
> > merged and the original Syzkaller reproducer no longer triggers an issue,
> > teaching the verfier how to do better bound deduction (i.e., precision
> > improvement) seems less appealing than before, unless:
> 
> There is only so much information that can be gained from 32->64
> tightening. I think this patch-set makes such tightening as precise as
> it can be. Which is a nice property, hence I'd like to proceed merging
> it.

I've sent a patch [1] that might be addressing the same gaps in
deduce_bounds_64_from_32() (outside of the s32 case maybe?). At least,
the selftests introduced here pass with that patch as well. It doesn't
require cnums and looks a bit easier to follow IMO.

I wrote it while trying to fix the reg_bounds selftests and only noticed
yesterday that it might be overlapping with this. cnums probably have
other benefits, but maybe they're not needed to address the issues
identified here?

1: https://lore.kernel.org/bpf/b2a0346a5b0818008503b721c62621918d84ad0a.1776344897.git.paul.chaignon@gmail.com/

> 
> > 1. LLVM produced program show similar pattern and was rejected by the
> >    verifier, which will be fixed by this patchset
> > 2. We're proceeding with cnum RFC as a whole, and this marks the first
> >    step (I am assuming this is the case?)
> 
> This is likely, I'm about to share the RFC.
> 
> > My understanding is that we just need the verifier to be smart enough
> > to accept safe LLVM-generated program, where as Syzkaller-generated one
> > is not as much of a concern if it does not causes any issue. cnum
> > improvement make sense because it simplifies the code, and could
> > potentially be the last time we have to touch 32->64 deduction (famous
> > last word).
> > 
> > Shung-Hsi
> > 
> > [...]