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

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2026-04-10 at 09:40 -0300, Helen Koike wrote:
> Unify handling of signed and unsigned using circular range logic.
> 
> Signed and unsigned numbers follows the same order in bit
> representation. We can think of it as a clock, were 12h is
> 0x0000_0000 and 11h is 0xFFFF_FFFF, regardless of its sign.
> 
> Then, instead of dealing with max and min, we deal with a base and len,
> where len = max - min.
> 
> Example:
>     range [-1, 3] is represented by base=0xFFFF_FFFF len=4
>     since (u32)3 - (u32)-1 is 4.
> 
> And we can verify if a value v is in range if:
>     (u32)(v - base) <= len
> which is true if v is signed -1 or v is unsigned 0xFFFF_FFFF.
> 
> This automatically handles the wrapping case, discarding the need to
> check if it crosses the signed range or not and handle each case.
> 
> It also fixes the following current issues:
> * [(u32)umin, (u32)umax] falling outside of [u32_min_value, u32_max_value]
> * [(u32)umin, (u32)umax] falling in the gap [(u32)s32_max_value, (u32)s32_min_value]
> 
> Fixes: c51d5ad6543c ("bpf: improve deduction of 64-bit bounds from 32-bit bounds")
> [Circular representation]
> Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
> Signed-off-by: Helen Koike <koike@igalia.com>
> 
> ---
> 
> This is a follow-up from discussion:
>   https://lore.kernel.org/all/7fb97184-baaa-4639-a0b9-ac289bf2e54d@igalia.com/
> 
> I didn't tag this as v2 since it is a completely different
> implementation.
> 
> I did do an implementation[1] without circular range logic, by using
> if/elses blocks, but it feels I'm always missing a corner case and using
> circular range logic feels safer.
> 
> Eduard, I didn't use the exact code you pointed, since it seems it is
> covered by your RFC, so I used the logic just for this case while your
> RFC doesn't move forward.
> 
> Please let me know what you think.
> 
> [1]
> https://github.com/helen-fornazier/linux/commits/bpf-min-max-if-else-solution/
> (3 last commits)
> 
> Thanks,
> Helen
> ---
>  kernel/bpf/verifier.c | 77 +++++++++++++++++++++++++++++++++++--------
>  1 file changed, 64 insertions(+), 13 deletions(-)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 8c1cf2eb6cbb..2944c17d2b7b 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2700,6 +2700,48 @@ static void deduce_bounds_64_from_64(struct bpf_reg_state *reg)
>  	}
>  }
>  
> +/*
> + * Find the smallest v >= lo such that (u32)v is in the circular u32 range
> + * [b_min, b_max] (b_len = b_max - b_min wraps naturally for wrapping ranges).
> + */
> +static u64 u64_tighten_umin(u64 lo, u64 hi, u32 b_min, u32 b_max)
> +{
> +	u32 b_len = b_max - b_min;
> +	u64 a_len = hi - lo;
> +	u64 cand;
> +
> +	/* lo32(lo) already in [b_min, b_max]? */
> +	if ((u32)((u32)lo - b_min) <= b_len)
> +		return lo;
> +	/* Set lo32 to b_min and check if it's in the range [lo, hi] */
> +	cand = (lo & ~(u64)U32_MAX) | b_min;
> +	if (cand - lo <= a_len)
> +		return cand;
> +	/* Advance to the next 2^32 block */
> +	return cand + BIT_ULL(32);
> +}

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

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?

[1] https://github.com/eddyz87/deduce-bounds-64-from-32-checks

[...]