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

[Harishankar Vishwanathan]

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".

> 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

> [...]