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

[Shung-Hsi Yu]

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:

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?)

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

[...]