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

[Eduard Zingerman]

On Wed, 2026-04-15 at 12:19 -0400, Harishankar Vishwanathan wrote:
> On Wed, Apr 15, 2026 at 3:12 AM Eduard Zingerman <eddyz87@xxxxxxxxx> 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].
> > It shows that for any valid input register state deduce_bounds_64_from_32
> > does not loose any values (check_soundness() function in [1], which validates).
> > It also shows that there exist invalid input register state,
> > such that deduce_bounds_64_from_32() "fixes" it to be valid
> > (check_invalid_preserved() function in [1], which produces a counter-example).
> 
> IIUC, this patch enhances the new deduce_bounds_64_from_32, while
> also having the property that it "maintains invalid input register states".

It enhances deduce_bounds_64_from_32, but it does *not* maintain the
invalid stays invalid property. It can be adjusted to provide a signal
when 64-bit and 32-bit ranges do not intersect.
In any case, I see that you handle this situation already in [1].
Therefore, I think we can proceed with this patch as-is.

[1] https://lore.kernel.org/bpf/20260415160728.657270-1-harishankar.vishwanathan@xxxxxxxxx/T/#t

> 
> > Now, the question is whether we want check_invalid_preserved() to hold.
> > Harishankar is working on an extension to simulate_both_branches_taken()
> > checking for additional cases of invariant violation.
> > Disagreement between 64-bit and 32-bit ranges is one of such violations.
> > The logic in deduce_bounds_64_from_32() can be extracted as "intersect"
> > function producing a signal describing if intersection actually exist.
> > So, the question is for Harishankar, would you like to have such
> > "intersect" function?
> 
> I  think using the new reg_bounds_intersect() "intersection checks"
> introduced in [1] to exit early in sync is still useful because
> the other sub-sync function might still "fix" the bounds
> 
> [1] https://lore.kernel.org/bpf/20260415160728.657270-2-harishankar.vishwanathan@xxxxxxxxx/T/#u
> 
> > [...]