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

[Eduard Zingerman <eddyz87@gmail.com>]

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.

> 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
> 
> [...]