[PATCH bpf-next] bpf: Simplify bounds refinement from s32

[PATCH bpf-next] bpf: Simplify bounds refinement from s32

[Paul Chaignon]

During the bounds refinement, we improve the precision of various ranges
by looking at other ranges. Among others, we improve the following in
this order (other things happen between 1 and 2):

  1. Improve u32 from s32 in __reg32_deduce_bounds.
  2. Improve s/u64 from u32 in __reg_deduce_mixed_bounds.
  3. Improve s/u64 from s32 in __reg_deduce_mixed_bounds.

In particular, if the s32 range forms a valid u32 range, we will use it
to improve the u32 range in __reg32_deduce_bounds. In
__reg_deduce_mixed_bounds, under the same condition, we will use the s32
range to improve the s/u64 ranges.

If at (1) we were able to learn from s32 to improve u32, we'll then be
able to use that in (2) to improve s/u64. Hence, as (3) happens under
the same precondition as (1), it won't improve s/u64 ranges further than
(1)+(2) did. Thus, we can get rid of (3).

In addition to the extensive suite of selftests for bounds refinement,
this patch was also tested with the Agni formal verification tool [1].

Link: https://github.com/bpfverif/agni [1]
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 kernel/bpf/verifier.c | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index e2fcea860755..d218516c3b33 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2554,20 +2554,6 @@ static void __reg_deduce_mixed_bounds(struct bpf_reg_state *reg)
 	reg->smin_value = max_t(s64, reg->smin_value, new_smin);
 	reg->smax_value = min_t(s64, reg->smax_value, new_smax);
 
-	/* if s32 can be treated as valid u32 range, we can use it as well */
-	if ((u32)reg->s32_min_value <= (u32)reg->s32_max_value) {
-		/* s32 -> u64 tightening */
-		new_umin = (reg->umin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
-		new_umax = (reg->umax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
-		reg->umin_value = max_t(u64, reg->umin_value, new_umin);
-		reg->umax_value = min_t(u64, reg->umax_value, new_umax);
-		/* s32 -> s64 tightening */
-		new_smin = (reg->smin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
-		new_smax = (reg->smax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
-		reg->smin_value = max_t(s64, reg->smin_value, new_smin);
-		reg->smax_value = min_t(s64, reg->smax_value, new_smax);
-	}
-
 	/* Here we would like to handle a special case after sign extending load,
 	 * when upper bits for a 64-bit range are all 1s or all 0s.
 	 *
-- 
2.43.0

Re: [PATCH bpf-next] bpf: Simplify bounds refinement from s32

[Eduard Zingerman]

On Thu, 2025-07-24 at 19:42 +0200, Paul Chaignon wrote:
> During the bounds refinement, we improve the precision of various ranges
> by looking at other ranges. Among others, we improve the following in
> this order (other things happen between 1 and 2):
> 
>   1. Improve u32 from s32 in __reg32_deduce_bounds.
>   2. Improve s/u64 from u32 in __reg_deduce_mixed_bounds.
>   3. Improve s/u64 from s32 in __reg_deduce_mixed_bounds.
> 
> In particular, if the s32 range forms a valid u32 range, we will use it
> to improve the u32 range in __reg32_deduce_bounds. In
> __reg_deduce_mixed_bounds, under the same condition, we will use the s32
> range to improve the s/u64 ranges.
> 
> If at (1) we were able to learn from s32 to improve u32, we'll then be
> able to use that in (2) to improve s/u64. Hence, as (3) happens under
> the same precondition as (1), it won't improve s/u64 ranges further than
> (1)+(2) did. Thus, we can get rid of (3).
> 
> In addition to the extensive suite of selftests for bounds refinement,
> this patch was also tested with the Agni formal verification tool [1].
> 
> Link: https://github.com/bpfverif/agni [1]
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

So, the argument appears to be as follows:

Under precondition `(u32)reg->s32_min <= (u32)reg->s32_max`
__reg32_deduce_bounds produces:

  reg->u32_min = max_t(u32, reg->s32_min, reg->u32_min);
  reg->u32_max = min_t(u32, reg->s32_max, reg->u32_max);

And then first part of __reg_deduce_mixed_bounds assigns:

  a. reg->umin umax= (reg->umin & ~0xffffffffULL) | max_t(u32, reg->s32_min, reg->u32_min);
  b. reg->umax umin= (reg->umax & ~0xffffffffULL) | min_t(u32, reg->s32_max, reg->u32_max);

And then second part of __reg_deduce_mixed_bounds assigns:

  c. reg->umin umax= (reg->umin & ~0xffffffffULL) | (u32)reg->s32_min;
  d. reg->umax umin= (reg->umax & ~0xffffffffULL) | (u32)reg->s32_max;

But assignment (c) is a noop because:

   max_t(u32, reg->s32_min, reg->u32_min) >= (u32)reg->s32_min

Hence RHS(a) >= RHS(c) and umin= does nothing.

Also assignment (d) is a noop because:

  min_t(u32, reg->s32_max, reg->u32_max) <= (u32)reg->s32_max

Hence RHS(b) <= RHS(d) and umin= does nothing.

Plus the same reasoning for the part dealing with reg->s{min,max}_value:

  e. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | max_t(u32, reg->s32_min_value, reg->u32_min_value);
  f. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | min_t(u32, reg->s32_max_value, reg->u32_max_value);

    vs

  g. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
  h. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;

    RHS(e) >= RHS(g) and RHS(f) <= RHS(h), hence smax=,smin= do nothing.

This appears to be correct.

Shung-Hsi, wdyt?

[...]

Re: [PATCH bpf-next] bpf: Simplify bounds refinement from s32

[Shung-Hsi Yu]

[-- Attachment #1: Type: text/plain, Size: 3449 bytes --]

On Thu, Jul 24, 2025 at 02:49:47PM -0700, Eduard Zingerman wrote:
> On Thu, 2025-07-24 at 19:42 +0200, Paul Chaignon wrote:
> > During the bounds refinement, we improve the precision of various ranges
> > by looking at other ranges. Among others, we improve the following in
> > this order (other things happen between 1 and 2):
> > 
> >   1. Improve u32 from s32 in __reg32_deduce_bounds.
> >   2. Improve s/u64 from u32 in __reg_deduce_mixed_bounds.
> >   3. Improve s/u64 from s32 in __reg_deduce_mixed_bounds.
> > 
> > In particular, if the s32 range forms a valid u32 range, we will use it
> > to improve the u32 range in __reg32_deduce_bounds. In
> > __reg_deduce_mixed_bounds, under the same condition, we will use the s32
> > range to improve the s/u64 ranges.
> > 
> > If at (1) we were able to learn from s32 to improve u32, we'll then be
> > able to use that in (2) to improve s/u64. Hence, as (3) happens under
> > the same precondition as (1), it won't improve s/u64 ranges further than
> > (1)+(2) did. Thus, we can get rid of (3).
> > 
> > In addition to the extensive suite of selftests for bounds refinement,
> > this patch was also tested with the Agni formal verification tool [1].
> > 
> > Link: https://github.com/bpfverif/agni [1]
> > Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> > ---
> 
> So, the argument appears to be as follows:
> 
> Under precondition `(u32)reg->s32_min <= (u32)reg->s32_max`
> __reg32_deduce_bounds produces:
> 
>   reg->u32_min = max_t(u32, reg->s32_min, reg->u32_min);
>   reg->u32_max = min_t(u32, reg->s32_max, reg->u32_max);
> 
> And then first part of __reg_deduce_mixed_bounds assigns:
> 
>   a. reg->umin umax= (reg->umin & ~0xffffffffULL) | max_t(u32, reg->s32_min, reg->u32_min);
>   b. reg->umax umin= (reg->umax & ~0xffffffffULL) | min_t(u32, reg->s32_max, reg->u32_max);
> 
> And then second part of __reg_deduce_mixed_bounds assigns:
> 
>   c. reg->umin umax= (reg->umin & ~0xffffffffULL) | (u32)reg->s32_min;
>   d. reg->umax umin= (reg->umax & ~0xffffffffULL) | (u32)reg->s32_max;
> 
> But assignment (c) is a noop because:
> 
>    max_t(u32, reg->s32_min, reg->u32_min) >= (u32)reg->s32_min
> 
> Hence RHS(a) >= RHS(c) and umin= does nothing.
> 
> Also assignment (d) is a noop because:
> 
>   min_t(u32, reg->s32_max, reg->u32_max) <= (u32)reg->s32_max
> 
> Hence RHS(b) <= RHS(d) and umin= does nothing.
> 
> Plus the same reasoning for the part dealing with reg->s{min,max}_value:
> 
>   e. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | max_t(u32, reg->s32_min_value, reg->u32_min_value);
>   f. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | min_t(u32, reg->s32_max_value, reg->u32_max_value);
> 
>     vs
> 
>   g. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
>   h. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
> 
>     RHS(e) >= RHS(g) and RHS(f) <= RHS(h), hence smax=,smin= do nothing.
> 
> This appears to be correct.
> 
> Shung-Hsi, wdyt?

Agree with the reasoning above, it looks solid.

Beside going through the reasoning, I also played with CBMC a bit to
double check that as far as a single run of __reg_deduce_bounds() is
concerned (and that the register state matches certain handwavy
expectations), the change indeed still preserve the original behavior.

Reviewed-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

Simplification of bound deduction logic! \o/


[-- Attachment #2: Type: text/x-c, Size: 8985 bytes --]

#include <stdint.h>
#include <limits.h>
#include <stdbool.h>
#include <assert.h>

// Define Linux kernel types
typedef uint64_t u64;
typedef int64_t s64;
typedef uint32_t u32;
typedef int32_t s32;
typedef uint8_t u8;
typedef int8_t s8;
typedef uint16_t u16;
typedef int16_t s16;

// Define limits
#define S8_MIN  INT8_MIN
#define S8_MAX  INT8_MAX
#define S16_MIN INT16_MIN
#define S16_MAX INT16_MAX
#define S32_MIN INT32_MIN
#define S32_MAX INT32_MAX
#define U32_MAX UINT32_MAX
#define S64_MIN INT64_MIN
#define S64_MAX INT64_MAX
#define U64_MAX UINT64_MAX

/* Crude approximation of min_t() and max_t() */
#define min_t(type, x, y) (((type) (x)) < ((type) (y)) ? ((type) (x)) : ((type) (y)))
#define max_t(type, x, y) (((type) (x)) > ((type) (y)) ? ((type) (x)) : ((type) (y)))

// Simplified version of bpf_reg_state with only field needed by
// coerce_reg_to_size_sx
struct bpf_reg_state {
	s64 smin_value;
	s64 smax_value;
	u64 umin_value;
	u64 umax_value;
	s32 s32_min_value;
	s32 s32_max_value;
	u32 u32_min_value;
	u32 u32_max_value;
};

static void __reg32_deduce_bounds(struct bpf_reg_state *reg)
{
	if ((reg->umin_value >> 32) == (reg->umax_value >> 32)) {
		reg->u32_min_value = max_t(u32, reg->u32_min_value, (u32)reg->umin_value);
		reg->u32_max_value = min_t(u32, reg->u32_max_value, (u32)reg->umax_value);

		if ((s32)reg->umin_value <= (s32)reg->umax_value) {
			reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->umin_value);
			reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->umax_value);
		}
	}
	if ((reg->smin_value >> 32) == (reg->smax_value >> 32)) {
		if ((u32)reg->smin_value <= (u32)reg->smax_value) {
			reg->u32_min_value = max_t(u32, reg->u32_min_value, (u32)reg->smin_value);
			reg->u32_max_value = min_t(u32, reg->u32_max_value, (u32)reg->smax_value);
		}
		if ((s32)reg->smin_value <= (s32)reg->smax_value) {
			reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->smin_value);
			reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
		}
	}
	if ((u32)(reg->umin_value >> 32) + 1 == (u32)(reg->umax_value >> 32) &&
	    (s32)reg->umin_value < 0 && (s32)reg->umax_value >= 0) {
		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->umin_value);
		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->umax_value);
	}
	if ((u32)(reg->smin_value >> 32) + 1 == (u32)(reg->smax_value >> 32) &&
	    (s32)reg->smin_value < 0 && (s32)reg->smax_value >= 0) {
		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->smin_value);
		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
	}
	if ((s32)reg->u32_min_value <= (s32)reg->u32_max_value) {
		reg->s32_min_value = max_t(s32, reg->s32_min_value, reg->u32_min_value);
		reg->s32_max_value = min_t(s32, reg->s32_max_value, reg->u32_max_value);
	}
	if ((u32)reg->s32_min_value <= (u32)reg->s32_max_value) {
		reg->u32_min_value = max_t(u32, reg->s32_min_value, reg->u32_min_value);
		reg->u32_max_value = min_t(u32, reg->s32_max_value, reg->u32_max_value);
	}
}

static void __reg64_deduce_bounds(struct bpf_reg_state *reg)
{
	if ((s64)reg->umin_value <= (s64)reg->umax_value) {
		reg->smin_value = max_t(s64, reg->smin_value, reg->umin_value);
		reg->smax_value = min_t(s64, reg->smax_value, reg->umax_value);
	}
	if ((u64)reg->smin_value <= (u64)reg->smax_value) {
		reg->umin_value = max_t(u64, reg->smin_value, reg->umin_value);
		reg->umax_value = min_t(u64, reg->smax_value, reg->umax_value);
	}
}

static void __reg_deduce_mixed_bounds_old(struct bpf_reg_state *reg)
{
	u64 new_umin, new_umax;
	s64 new_smin, new_smax;

	new_umin = (reg->umin_value & ~0xffffffffULL) | reg->u32_min_value;
	new_umax = (reg->umax_value & ~0xffffffffULL) | reg->u32_max_value;
	reg->umin_value = max_t(u64, reg->umin_value, new_umin);
	reg->umax_value = min_t(u64, reg->umax_value, new_umax);
	new_smin = (reg->smin_value & ~0xffffffffULL) | reg->u32_min_value;
	new_smax = (reg->smax_value & ~0xffffffffULL) | reg->u32_max_value;
	reg->smin_value = max_t(s64, reg->smin_value, new_smin);
	reg->smax_value = min_t(s64, reg->smax_value, new_smax);

	if ((u32)reg->s32_min_value <= (u32)reg->s32_max_value) {
		new_umin = (reg->umin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
		new_umax = (reg->umax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
		reg->umin_value = max_t(u64, reg->umin_value, new_umin);
		reg->umax_value = min_t(u64, reg->umax_value, new_umax);
		new_smin = (reg->smin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
		new_smax = (reg->smax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
		reg->smin_value = max_t(s64, reg->smin_value, new_smin);
		reg->smax_value = min_t(s64, reg->smax_value, new_smax);
	}
	if (reg->s32_min_value >= 0 && reg->smin_value >= S32_MIN && reg->smax_value <= S32_MAX) {
		reg->smin_value = reg->s32_min_value;
		reg->smax_value = reg->s32_max_value;
		reg->umin_value = reg->s32_min_value;
		reg->umax_value = reg->s32_max_value;
		/* var_off update with tnum_intersect() removed, was the last
		 * step, so shouldn't make a difference
		 */
	}
}

static void __reg_deduce_mixed_bounds_new(struct bpf_reg_state *reg)
{
	u64 new_umin, new_umax;
	s64 new_smin, new_smax;

	new_umin = (reg->umin_value & ~0xffffffffULL) | reg->u32_min_value;
	new_umax = (reg->umax_value & ~0xffffffffULL) | reg->u32_max_value;
	reg->umin_value = max_t(u64, reg->umin_value, new_umin);
	reg->umax_value = min_t(u64, reg->umax_value, new_umax);
	new_smin = (reg->smin_value & ~0xffffffffULL) | reg->u32_min_value;
	new_smax = (reg->smax_value & ~0xffffffffULL) | reg->u32_max_value;
	reg->smin_value = max_t(s64, reg->smin_value, new_smin);
	reg->smax_value = min_t(s64, reg->smax_value, new_smax);

	/* s32 -> u/s64 tightening removed */

	if (reg->s32_min_value >= 0 && reg->smin_value >= S32_MIN && reg->smax_value <= S32_MAX) {
		reg->smin_value = reg->s32_min_value;
		reg->smax_value = reg->s32_max_value;
		reg->umin_value = reg->s32_min_value;
		reg->umax_value = reg->s32_max_value;
		/* var_off update with tnum_intersect() removed, was the last
		 * step, so shouldn't make a difference
		 */
	}
}

static void __reg_deduce_bounds_old(struct bpf_reg_state *reg)
{
	__reg32_deduce_bounds(reg);
	__reg64_deduce_bounds(reg);
	__reg_deduce_mixed_bounds_old(reg);
}

static void __reg_deduce_bounds_new(struct bpf_reg_state *reg)
{
	__reg32_deduce_bounds(reg);
	__reg64_deduce_bounds(reg);
	__reg_deduce_mixed_bounds_new(reg);
}

/* helper function to initialize 'struct bpf_reg_state' */
static struct bpf_reg_state __bpf_reg_state_input(void)
{
	struct bpf_reg_state reg;
	reg.smin_value = nondet_long_long_input();
	reg.smax_value = nondet_long_long_input();
	reg.umin_value = nondet_unsigned_long_long_input();
	reg.umax_value = nondet_unsigned_long_long_input();
	reg.s32_min_value = nondet_int_input();
	reg.s32_max_value = nondet_int_input();
	reg.u32_min_value = nondet_unsigned_int_input();
	reg.u32_max_value = nondet_unsigned_int_input();
	return reg;
}

/* helper function to ensure 'struct bpf_reg_state' is in a proper state */
static bool valid_bpf_reg_state(struct bpf_reg_state *reg)
{
	bool ret = true;
	/* Ensure maximum >= minimum for all ranges */
	ret &= reg->umin_value <= reg->umax_value;
	ret &= reg->smin_value <= reg->smax_value;
	ret &= reg->u32_min_value <= reg->u32_max_value;
	ret &= reg->s32_min_value <= reg->s32_max_value;
	/* Ensure 64-bit bounds are consistent with 32-bit bounds */
	ret &= reg->umin_value <= (u64)reg->u32_max_value;
	ret &= reg->umax_value >= (u64)reg->u32_min_value;
	ret &= (s64)reg->smin_value <= (s64)reg->s32_max_value;
	ret &= (s64)reg->smax_value >= (s64)reg->s32_min_value;
	return ret;
}

/* helper function to check whether 'struct bpf_reg_state' contains certain value */
static bool val_in_reg(struct bpf_reg_state *reg, u64 val)
{
	bool ret = true;
	ret &= reg->umin_value <= val;
	ret &= val <= reg->umax_value;
	ret &= reg->smin_value <= (s64)val;
	ret &= (s64)val <= reg->smax_value;
	ret &= reg->u32_min_value <= (u32)val;
	ret &= (u32)val <= reg->u32_max_value;
	ret &= reg->s32_min_value <= (s32)val;
	ret &= (s32)val <= reg->s32_max_value;
	return ret;
}

void main(void)
{
	/* ------------ Assumptions and Setup ------------ */

	/* Input data structure that represents current knowledge of the possible
	 * values in a register, as well as some possible value 'x', which could be
	 * any value that is in the register right now.
	 */
	struct bpf_reg_state reg = __bpf_reg_state_input();
	u64 x = nondet_unsigned_long_long_input();
	__CPROVER_assume(valid_bpf_reg_state(&reg));
	__CPROVER_assume(val_in_reg(&reg, x));

	/* ------------- Operation to Check -------------- */
	/* Data structure to store the new output */
	struct bpf_reg_state new_reg;
	/* Clone the register state since __reg_deduce_bounds() modifies it */
	new_reg = reg;

	__reg_deduce_bounds_old(&reg);
	__reg_deduce_bounds_new(&new_reg);

	/* -------------- Property Checking -------------- */
	assert(new_reg == reg);
}

Re: [PATCH bpf-next] bpf: Simplify bounds refinement from s32

[Eduard Zingerman]

On Fri, 2025-07-25 at 17:21 +0800, Shung-Hsi Yu wrote:

[...]

> Beside going through the reasoning, I also played with CBMC a bit to
> double check that as far as a single run of __reg_deduce_bounds() is
> concerned (and that the register state matches certain handwavy
> expectations), the change indeed still preserve the original behavior.

Interesting, thank you!

Re: [PATCH bpf-next] bpf: Simplify bounds refinement from s32

[Paul Chaignon]

On Fri, Jul 25, 2025 at 05:21:38PM +0800, Shung-Hsi Yu wrote:
> On Thu, Jul 24, 2025 at 02:49:47PM -0700, Eduard Zingerman wrote:
> > On Thu, 2025-07-24 at 19:42 +0200, Paul Chaignon wrote:
> > > During the bounds refinement, we improve the precision of various ranges
> > > by looking at other ranges. Among others, we improve the following in
> > > this order (other things happen between 1 and 2):
> > > 
> > >   1. Improve u32 from s32 in __reg32_deduce_bounds.
> > >   2. Improve s/u64 from u32 in __reg_deduce_mixed_bounds.
> > >   3. Improve s/u64 from s32 in __reg_deduce_mixed_bounds.
> > > 
> > > In particular, if the s32 range forms a valid u32 range, we will use it
> > > to improve the u32 range in __reg32_deduce_bounds. In
> > > __reg_deduce_mixed_bounds, under the same condition, we will use the s32
> > > range to improve the s/u64 ranges.
> > > 
> > > If at (1) we were able to learn from s32 to improve u32, we'll then be
> > > able to use that in (2) to improve s/u64. Hence, as (3) happens under
> > > the same precondition as (1), it won't improve s/u64 ranges further than
> > > (1)+(2) did. Thus, we can get rid of (3).
> > > 
> > > In addition to the extensive suite of selftests for bounds refinement,
> > > this patch was also tested with the Agni formal verification tool [1].
> > > 
> > > Link: https://github.com/bpfverif/agni [1]
> > > Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> > > ---
> > 
> > So, the argument appears to be as follows:
> > 
> > Under precondition `(u32)reg->s32_min <= (u32)reg->s32_max`
> > __reg32_deduce_bounds produces:
> > 
> >   reg->u32_min = max_t(u32, reg->s32_min, reg->u32_min);
> >   reg->u32_max = min_t(u32, reg->s32_max, reg->u32_max);
> > 
> > And then first part of __reg_deduce_mixed_bounds assigns:
> > 
> >   a. reg->umin umax= (reg->umin & ~0xffffffffULL) | max_t(u32, reg->s32_min, reg->u32_min);
> >   b. reg->umax umin= (reg->umax & ~0xffffffffULL) | min_t(u32, reg->s32_max, reg->u32_max);
> > 
> > And then second part of __reg_deduce_mixed_bounds assigns:
> > 
> >   c. reg->umin umax= (reg->umin & ~0xffffffffULL) | (u32)reg->s32_min;
> >   d. reg->umax umin= (reg->umax & ~0xffffffffULL) | (u32)reg->s32_max;
> > 
> > But assignment (c) is a noop because:
> > 
> >    max_t(u32, reg->s32_min, reg->u32_min) >= (u32)reg->s32_min
> > 
> > Hence RHS(a) >= RHS(c) and umin= does nothing.
> > 
> > Also assignment (d) is a noop because:
> > 
> >   min_t(u32, reg->s32_max, reg->u32_max) <= (u32)reg->s32_max
> > 
> > Hence RHS(b) <= RHS(d) and umin= does nothing.
> > 
> > Plus the same reasoning for the part dealing with reg->s{min,max}_value:
> > 
> >   e. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | max_t(u32, reg->s32_min_value, reg->u32_min_value);
> >   f. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | min_t(u32, reg->s32_max_value, reg->u32_max_value);
> > 
> >     vs
> > 
> >   g. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
> >   h. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
> > 
> >     RHS(e) >= RHS(g) and RHS(f) <= RHS(h), hence smax=,smin= do nothing.
> > 
> > This appears to be correct.
> > 
> > Shung-Hsi, wdyt?
> 
> Agree with the reasoning above, it looks solid.
> 
> Beside going through the reasoning, I also played with CBMC a bit to
> double check that as far as a single run of __reg_deduce_bounds() is
> concerned (and that the register state matches certain handwavy
> expectations), the change indeed still preserve the original behavior.

Ah, I didn't even think about checking input-output equivalence. Thanks
for testing this!

> 
> Reviewed-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> 
> Simplification of bound deduction logic! \o/

Yeah, I'll admit it felt too good to be true :')
I feel more confident with both of your reviews. Thank you both for
reviewing this closely!

[...]

Re: [PATCH bpf-next] bpf: Simplify bounds refinement from s32

[Eduard Zingerman]

On Thu, 2025-07-24 at 19:42 +0200, Paul Chaignon wrote:
> During the bounds refinement, we improve the precision of various ranges
> by looking at other ranges. Among others, we improve the following in
> this order (other things happen between 1 and 2):
> 
>   1. Improve u32 from s32 in __reg32_deduce_bounds.
>   2. Improve s/u64 from u32 in __reg_deduce_mixed_bounds.
>   3. Improve s/u64 from s32 in __reg_deduce_mixed_bounds.
> 
> In particular, if the s32 range forms a valid u32 range, we will use it
> to improve the u32 range in __reg32_deduce_bounds. In
> __reg_deduce_mixed_bounds, under the same condition, we will use the s32
> range to improve the s/u64 ranges.
> 
> If at (1) we were able to learn from s32 to improve u32, we'll then be
> able to use that in (2) to improve s/u64. Hence, as (3) happens under
> the same precondition as (1), it won't improve s/u64 ranges further than
> (1)+(2) did. Thus, we can get rid of (3).
> 
> In addition to the extensive suite of selftests for bounds refinement,
> this patch was also tested with the Agni formal verification tool [1].
> 
> Link: https://github.com/bpfverif/agni [1]
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

Re: [PATCH bpf-next] bpf: Simplify bounds refinement from s32

[patchwork-bot+netdevbpf]

Hello:

This patch was applied to bpf/bpf-next.git (master)
by Daniel Borkmann <daniel@iogearbox.net>:

On Thu, 24 Jul 2025 19:42:52 +0200 you wrote:
> During the bounds refinement, we improve the precision of various ranges
> by looking at other ranges. Among others, we improve the following in
> this order (other things happen between 1 and 2):
> 
>   1. Improve u32 from s32 in __reg32_deduce_bounds.
>   2. Improve s/u64 from u32 in __reg_deduce_mixed_bounds.
>   3. Improve s/u64 from s32 in __reg_deduce_mixed_bounds.
> 
> [...]

Here is the summary with links:
  - [bpf-next] bpf: Simplify bounds refinement from s32
    https://git.kernel.org/bpf/bpf-next/c/5345e64760d3

You are awesome, thank you!
-- 
Deet-doot-dot, I am a bot.
https://korg.docs.kernel.org/patchwork/pwbot.html