[PATCH bpf-next 0/4] bpf: Improve 64bits bounds refinement

[PATCH bpf-next 0/4] bpf: Improve 64bits bounds refinement

[Paul Chaignon]

This patchset improves the 64bits bounds refinement when the s64 ranges
crosses the sign boundary. The first patch explains the small addition
to __reg64_deduce_bounds. The third patch adds a selftest with a more
complete example of the impact on verification. The second and last
patches update the existing selftests to take the new refinement into
account.

This patchset should reduce the number of kernel warnings hit by
syzkaller due to invariant violations [1]. It was also tested with
Agni [2] (and Cilium's CI for good measure).

Link: https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf [1]
Link: https://github.com/bpfverif/agni [2]

Paul Chaignon (4):
  bpf: Improve bounds when s64 crosses sign boundary
  selftests/bpf: Update reg_bound range refinement logic
  selftests/bpf: Test cross-sign 64bits range refinement
  selftests/bpf: Test invariants on JSLT crossing sign

 kernel/bpf/verifier.c                         | 44 +++++++++++++++++++
 .../selftests/bpf/prog_tests/reg_bounds.c     | 14 ++++++
 .../selftests/bpf/progs/verifier_bounds.c     | 25 ++++++++++-
 3 files changed, 82 insertions(+), 1 deletion(-)

-- 
2.43.0

[PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary

[Paul Chaignon]

__reg64_deduce_bounds currently improves the s64 range using the u64
range and vice versa, but only if it doesn't cross the sign boundary.

This patch improves __reg64_deduce_bounds to cover the case where the
s64 range crosses the sign boundary but overlaps with the u64 range on
only one end. In that case, we can improve both ranges. Consider the
following example, with the s64 range crossing the sign boundary:

    0                                                   U64_MAX
    |  [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]              |
    |----------------------------|----------------------------|
    |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
    0                     S64_MAX S64_MIN                    -1

The u64 range overlaps only with positive portion of the s64 range. We
can thus derive the following new s64 and u64 ranges.

    0                                                   U64_MAX
    |  [xxxxxx u64 range xxxxx]                               |
    |----------------------------|----------------------------|
    |  [xxxxxx s64 range xxxxx]                               |
    0                     S64_MAX S64_MIN                    -1

The same logic can probably apply to the s32/u32 ranges, but this patch
doesn't implement that change.

In addition to the selftests, this change was also tested with Agni,
the formal verification tool for the range analysis [1].

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

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index e2fcea860755..152b97a71f85 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2523,6 +2523,50 @@ static void __reg64_deduce_bounds(struct bpf_reg_state *reg)
 	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);
+	} else {
+		/* If the s64 range crosses the sign boundary, then it's split
+		 * between the beginning and end of the U64 domain. In that
+		 * case, we can derive new bounds if the u64 range overlaps
+		 * with only one end of the s64 range.
+		 *
+		 * In the following example, the u64 range overlaps only with
+		 * positive portion of the s64 range.
+		 *
+		 * 0                                                   U64_MAX
+		 * |  [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]              |
+		 * |----------------------------|----------------------------|
+		 * |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
+		 * 0                     S64_MAX S64_MIN                    -1
+		 *
+		 * We can thus derive the following new s64 and u64 ranges.
+		 *
+		 * 0                                                   U64_MAX
+		 * |  [xxxxxx u64 range xxxxx]                               |
+		 * |----------------------------|----------------------------|
+		 * |  [xxxxxx s64 range xxxxx]                               |
+		 * 0                     S64_MAX S64_MIN                    -1
+		 *
+		 * If they overlap in two places, we can't derive anything
+		 * because reg_state can't represent two ranges per numeric
+		 * domain.
+		 *
+		 * 0                                                   U64_MAX
+		 * |  [xxxxxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxxxxx]        |
+		 * |----------------------------|----------------------------|
+		 * |xxxxx s64 range xxxxxxxxx]                    [xxxxxxxxxx|
+		 * 0                     S64_MAX S64_MIN                    -1
+		 *
+		 * The first condition below corresponds to the diagram above.
+		 * The second condition considers the case where the u64 range
+		 * overlaps with the negative porition of the s64 range.
+		 */
+		if (reg->umax_value < (u64)reg->smin_value) {
+			reg->smin_value = (s64)reg->umin_value;
+			reg->umax_value = min_t(u64, reg->umax_value, reg->smax_value);
+		} else if ((u64)reg->smax_value < reg->umin_value) {
+			reg->smax_value = (s64)reg->umax_value;
+			reg->umin_value = max_t(u64, reg->umin_value, reg->smin_value);
+		}
 	}
 }
 
-- 
2.43.0

Re: [PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary

[Eduard Zingerman]

On Sat, 2025-07-19 at 16:22 +0200, Paul Chaignon wrote:

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

[...]

> +		/* If the s64 range crosses the sign boundary, then it's split
> +		 * between the beginning and end of the U64 domain. In that
> +		 * case, we can derive new bounds if the u64 range overlaps
> +		 * with only one end of the s64 range.
> +		 *
> +		 * In the following example, the u64 range overlaps only with
> +		 * positive portion of the s64 range.
> +		 *
> +		 * 0                                                   U64_MAX
> +		 * |  [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]              |
> +		 * |----------------------------|----------------------------|
> +		 * |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
> +		 * 0                     S64_MAX S64_MIN                    -1
> +		 *
> +		 * We can thus derive the following new s64 and u64 ranges.
> +		 *
> +		 * 0                                                   U64_MAX
> +		 * |  [xxxxxx u64 range xxxxx]                               |
> +		 * |----------------------------|----------------------------|
> +		 * |  [xxxxxx s64 range xxxxx]                               |
> +		 * 0                     S64_MAX S64_MIN                    -1
> +		 *
> +		 * If they overlap in two places, we can't derive anything
> +		 * because reg_state can't represent two ranges per numeric
> +		 * domain.
> +		 *
> +		 * 0                                                   U64_MAX
> +		 * |  [xxxxxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxxxxx]        |
> +		 * |----------------------------|----------------------------|
> +		 * |xxxxx s64 range xxxxxxxxx]                    [xxxxxxxxxx|
> +		 * 0                     S64_MAX S64_MIN                    -1
> +		 *
> +		 * The first condition below corresponds to the diagram above.
> +		 * The second condition considers the case where the u64 range
> +		 * overlaps with the negative porition of the s64 range.
> +		 */
> +		if (reg->umax_value < (u64)reg->smin_value) {
> +			reg->smin_value = (s64)reg->umin_value;
> +			reg->umax_value = min_t(u64, reg->umax_value, reg->smax_value);
> +		} else if ((u64)reg->smax_value < reg->umin_value) {

Nit: I'd add a drawing here as well:

		 * 0                                                   U64_MAX
		 * |              [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]  |
		 * |----------------------------|----------------------------|
		 * |xxxxxxxxx]                       [xxxxxxxxxxxx s64 range |
		 * 0                     S64_MAX S64_MIN                    -1

> +			reg->smax_value = (s64)reg->umax_value;
> +			reg->umin_value = max_t(u64, reg->umin_value, reg->smin_value);
> +		}
>  	}
>  }
>  

Re: [PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary

[Shung-Hsi Yu]

On Sat, Jul 19, 2025 at 04:22:05PM +0200, Paul Chaignon wrote:
> __reg64_deduce_bounds currently improves the s64 range using the u64
> range and vice versa, but only if it doesn't cross the sign boundary.
> 
> This patch improves __reg64_deduce_bounds to cover the case where the
> s64 range crosses the sign boundary but overlaps with the u64 range on
> only one end. In that case, we can improve both ranges. Consider the
> following example, with the s64 range crossing the sign boundary:
> 
>     0                                                   U64_MAX
>     |  [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]              |
>     |----------------------------|----------------------------|
>     |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
>     0                     S64_MAX S64_MIN                    -1
> 
> The u64 range overlaps only with positive portion of the s64 range. We
> can thus derive the following new s64 and u64 ranges.
> 
>     0                                                   U64_MAX
>     |  [xxxxxx u64 range xxxxx]                               |
>     |----------------------------|----------------------------|
>     |  [xxxxxx s64 range xxxxx]                               |
>     0                     S64_MAX S64_MIN                    -1
> 
> The same logic can probably apply to the s32/u32 ranges, but this patch
> doesn't implement that change.
> 
> In addition to the selftests, this change was also tested with Agni,
> the formal verification tool for the range analysis [1].
> 
> Link: https://github.com/bpfverif/agni [1]
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---
>  kernel/bpf/verifier.c | 44 +++++++++++++++++++++++++++++++++++++++++++
>  1 file changed, 44 insertions(+)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index e2fcea860755..152b97a71f85 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2523,6 +2523,50 @@ static void __reg64_deduce_bounds(struct bpf_reg_state *reg)
>  	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);
> +	} else {
> +		/* If the s64 range crosses the sign boundary, then it's split
> +		 * between the beginning and end of the U64 domain. In that
> +		 * case, we can derive new bounds if the u64 range overlaps
> +		 * with only one end of the s64 range.
> +		 *
> +		 * In the following example, the u64 range overlaps only with
> +		 * positive portion of the s64 range.
> +		 *
> +		 * 0                                                   U64_MAX
> +		 * |  [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]              |
> +		 * |----------------------------|----------------------------|
> +		 * |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
> +		 * 0                     S64_MAX S64_MIN                    -1
> +		 *
> +		 * We can thus derive the following new s64 and u64 ranges.
> +		 *
> +		 * 0                                                   U64_MAX
> +		 * |  [xxxxxx u64 range xxxxx]                               |
> +		 * |----------------------------|----------------------------|
> +		 * |  [xxxxxx s64 range xxxxx]                               |
> +		 * 0                     S64_MAX S64_MIN                    -1
> +		 *
> +		 * If they overlap in two places, we can't derive anything
> +		 * because reg_state can't represent two ranges per numeric
> +		 * domain.
> +		 *
> +		 * 0                                                   U64_MAX
> +		 * |  [xxxxxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxxxxx]        |
> +		 * |----------------------------|----------------------------|
> +		 * |xxxxx s64 range xxxxxxxxx]                    [xxxxxxxxxx|
> +		 * 0                     S64_MAX S64_MIN                    -1
> +		 *
> +		 * The first condition below corresponds to the diagram above.
> +		 * The second condition considers the case where the u64 range
> +		 * overlaps with the negative porition of the s64 range.
> +		 */
> +		if (reg->umax_value < (u64)reg->smin_value) {
> +			reg->smin_value = (s64)reg->umin_value;
> +			reg->umax_value = min_t(u64, reg->umax_value, reg->smax_value);

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

Just one question/comment: could the u64 and s64 ranges be disjoint? Say

   0                                                   U64_MAX
   |                             [xxx u64 range xxx]         |
   |----------------------------|----------------------------|
   |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
   0                     S64_MAX S64_MIN                    -1

If such case this code still works as the s64 range gets a bit wider at
the smin end (thus still safe), and u64 range stays unchanged.

That said if the u64 and s64 range always overlaps somewhere, it may be
an invariant we want to check in reg_bounds_sanity_check(). I seems to
have some vague memory that with conditionals jumps it may be possible
to produce such disjoint signed & unsigned ranges, but I'm not sure if
that is still true.

> +		} else if ((u64)reg->smax_value < reg->umin_value) {
> +			reg->smax_value = (s64)reg->umax_value;
> +			reg->umin_value = max_t(u64, reg->umin_value, reg->smin_value);
> +		}
>  	}
>  }
>  
> -- 
> 2.43.0
> 

Re: [PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary

[Paul Chaignon]

On Tue, Jul 22, 2025 at 03:32:03PM +0800, Shung-Hsi Yu wrote:
> On Sat, Jul 19, 2025 at 04:22:05PM +0200, Paul Chaignon wrote:

[...]

> > +		/* If the s64 range crosses the sign boundary, then it's split
> > +		 * between the beginning and end of the U64 domain. In that
> > +		 * case, we can derive new bounds if the u64 range overlaps
> > +		 * with only one end of the s64 range.
> > +		 *
> > +		 * In the following example, the u64 range overlaps only with
> > +		 * positive portion of the s64 range.
> > +		 *
> > +		 * 0                                                   U64_MAX
> > +		 * |  [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]              |
> > +		 * |----------------------------|----------------------------|
> > +		 * |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
> > +		 * 0                     S64_MAX S64_MIN                    -1
> > +		 *
> > +		 * We can thus derive the following new s64 and u64 ranges.
> > +		 *
> > +		 * 0                                                   U64_MAX
> > +		 * |  [xxxxxx u64 range xxxxx]                               |
> > +		 * |----------------------------|----------------------------|
> > +		 * |  [xxxxxx s64 range xxxxx]                               |
> > +		 * 0                     S64_MAX S64_MIN                    -1
> > +		 *
> > +		 * If they overlap in two places, we can't derive anything
> > +		 * because reg_state can't represent two ranges per numeric
> > +		 * domain.
> > +		 *
> > +		 * 0                                                   U64_MAX
> > +		 * |  [xxxxxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxxxxx]        |
> > +		 * |----------------------------|----------------------------|
> > +		 * |xxxxx s64 range xxxxxxxxx]                    [xxxxxxxxxx|
> > +		 * 0                     S64_MAX S64_MIN                    -1
> > +		 *
> > +		 * The first condition below corresponds to the diagram above.
> > +		 * The second condition considers the case where the u64 range
> > +		 * overlaps with the negative porition of the s64 range.
> > +		 */
> > +		if (reg->umax_value < (u64)reg->smin_value) {
> > +			reg->smin_value = (s64)reg->umin_value;
> > +			reg->umax_value = min_t(u64, reg->umax_value, reg->smax_value);
> 
> Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> 
> Just one question/comment: could the u64 and s64 ranges be disjoint? Say
> 
>    0                                                   U64_MAX
>    |                             [xxx u64 range xxx]         |
>    |----------------------------|----------------------------|
>    |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
>    0                     S64_MAX S64_MIN                    -1
> 
> If such case this code still works as the s64 range gets a bit wider at
> the smin end (thus still safe), and u64 range stays unchanged.
> 
> That said if the u64 and s64 range always overlaps somewhere, it may be
> an invariant we want to check in reg_bounds_sanity_check(). I seems to
> have some vague memory that with conditionals jumps it may be possible
> to produce such disjoint signed & unsigned ranges, but I'm not sure if
> that is still true.

My assumption is that the u64 and s64 ranges can't be disjoint or that
would mean the register can't have any value. As you noted, even if that
were to happen, we would only lose some precision, i.e. the refinement
stays sound.

I considered returning an error from __reg64_deduce_bounds if that
invariant doesn't hold, but propagating it gets a bit messy. Adding it
to reg_bounds_sanity_check would likely be cleaner. Though to be
honest, I was hoping to see the impact of the present changes on the
syzbot reports before adding even more opportunities for invariant
violation reports :)

> 
> > +		} else if ((u64)reg->smax_value < reg->umin_value) {
> > +			reg->smax_value = (s64)reg->umax_value;
> > +			reg->umin_value = max_t(u64, reg->umin_value, reg->smin_value);
> > +		}
> >  	}
> >  }
> >  
> > -- 
> > 2.43.0
> > 

Re: [PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary

[Shung-Hsi Yu]

On Wed, Jul 23, 2025 at 12:09:52AM +0200, Paul Chaignon wrote:
> On Tue, Jul 22, 2025 at 03:32:03PM +0800, Shung-Hsi Yu wrote:
> > On Sat, Jul 19, 2025 at 04:22:05PM +0200, Paul Chaignon wrote:
> [...]
> > > +		/* If the s64 range crosses the sign boundary, then it's split
> > > +		 * between the beginning and end of the U64 domain. In that
> > > +		 * case, we can derive new bounds if the u64 range overlaps
> > > +		 * with only one end of the s64 range.
> > > +		 *
> > > +		 * In the following example, the u64 range overlaps only with
> > > +		 * positive portion of the s64 range.
> > > +		 *
> > > +		 * 0                                                   U64_MAX
> > > +		 * |  [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx]              |
> > > +		 * |----------------------------|----------------------------|
> > > +		 * |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
> > > +		 * 0                     S64_MAX S64_MIN                    -1
> > > +		 *
> > > +		 * We can thus derive the following new s64 and u64 ranges.
> > > +		 *
> > > +		 * 0                                                   U64_MAX
> > > +		 * |  [xxxxxx u64 range xxxxx]                               |
> > > +		 * |----------------------------|----------------------------|
> > > +		 * |  [xxxxxx s64 range xxxxx]                               |
> > > +		 * 0                     S64_MAX S64_MIN                    -1
> > > +		 *
> > > +		 * If they overlap in two places, we can't derive anything
> > > +		 * because reg_state can't represent two ranges per numeric
> > > +		 * domain.
> > > +		 *
> > > +		 * 0                                                   U64_MAX
> > > +		 * |  [xxxxxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxxxxx]        |
> > > +		 * |----------------------------|----------------------------|
> > > +		 * |xxxxx s64 range xxxxxxxxx]                    [xxxxxxxxxx|
> > > +		 * 0                     S64_MAX S64_MIN                    -1
> > > +		 *
> > > +		 * The first condition below corresponds to the diagram above.
> > > +		 * The second condition considers the case where the u64 range
> > > +		 * overlaps with the negative porition of the s64 range.
> > > +		 */
> > > +		if (reg->umax_value < (u64)reg->smin_value) {
> > > +			reg->smin_value = (s64)reg->umin_value;
> > > +			reg->umax_value = min_t(u64, reg->umax_value, reg->smax_value);
> > 
> > Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> > 
> > Just one question/comment: could the u64 and s64 ranges be disjoint? Say
> > 
> >    0                                                   U64_MAX
> >    |                             [xxx u64 range xxx]         |
> >    |----------------------------|----------------------------|
> >    |xxxxx s64 range xxxxxxxxx]                       [xxxxxxx|
> >    0                     S64_MAX S64_MIN                    -1
> > 
> > If such case this code still works as the s64 range gets a bit wider at
> > the smin end (thus still safe), and u64 range stays unchanged.
> > 
> > That said if the u64 and s64 range always overlaps somewhere, it may be
> > an invariant we want to check in reg_bounds_sanity_check(). I seems to
> > have some vague memory that with conditionals jumps it may be possible
> > to produce such disjoint signed & unsigned ranges, but I'm not sure if
> > that is still true.

> My assumption is that the u64 and s64 ranges can't be disjoint or that
> would mean the register can't have any value. As you noted, even if that
> were to happen, we would only lose some precision, i.e. the refinement
> stays sound.
> 
> I considered returning an error from __reg64_deduce_bounds if that
> invariant doesn't hold, but propagating it gets a bit messy. Adding it
> to reg_bounds_sanity_check would likely be cleaner. Though to be
> honest, I was hoping to see the impact of the present changes on the
> syzbot reports before adding even more opportunities for invariant
> violation reports :)

Make sense, that is the better plan :)

...

[PATCH bpf-next 2/4] selftests/bpf: Update reg_bound range refinement logic

[Paul Chaignon]

This patch updates the range refinement logic in the reg_bound test to
match the new logic from the previous commit. Without this change, tests
would fail because we end with more precise ranges than the tests
expect.

Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 .../testing/selftests/bpf/prog_tests/reg_bounds.c  | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
index 39d42271cc46..e261b0e872db 100644
--- a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
+++ b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
@@ -465,6 +465,20 @@ static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t,
 		return range_improve(x_t, x, x_swap);
 	}
 
+	if (!t_is_32(x_t) && !t_is_32(y_t) && x_t != y_t) {
+		if (x_t == S64 && x.a > x.b) {
+			if (x.b < y.a && x.a <= y.b)
+				return range(x_t, x.a, y.b);
+			if (x.a > y.b && x.b >= y.a)
+				return range(x_t, y.a, x.b);
+		} else if (x_t == U64 && y.a > y.b) {
+			if (y.b < x.a && y.a <= x.b)
+				return range(x_t, y.a, x.b);
+			if (y.a > x.b && y.b >= x.a)
+				return range(x_t, x.a, y.b);
+		}
+	}
+
 	/* otherwise, plain range cast and intersection works */
 	return range_improve(x_t, x, y_cast);
 }
-- 
2.43.0

Re: [PATCH bpf-next 2/4] selftests/bpf: Update reg_bound range refinement logic

[Eduard Zingerman]

On Sat, 2025-07-19 at 16:22 +0200, Paul Chaignon wrote:
> This patch updates the range refinement logic in the reg_bound test to
> match the new logic from the previous commit. Without this change, tests
> would fail because we end with more precise ranges than the tests
> expect.
> 
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

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

>  .../testing/selftests/bpf/prog_tests/reg_bounds.c  | 14 ++++++++++++++
>  1 file changed, 14 insertions(+)
> 
> diff --git a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> index 39d42271cc46..e261b0e872db 100644
> --- a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> +++ b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> @@ -465,6 +465,20 @@ static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t,
>  		return range_improve(x_t, x, x_swap);
>  	}
>  
> +	if (!t_is_32(x_t) && !t_is_32(y_t) && x_t != y_t) {

Nit: I'd swap x and y if necessary, to avoid a second branch.

> +		if (x_t == S64 && x.a > x.b) {
> +			if (x.b < y.a && x.a <= y.b)
> +				return range(x_t, x.a, y.b);
> +			if (x.a > y.b && x.b >= y.a)
> +				return range(x_t, y.a, x.b);
> +		} else if (x_t == U64 && y.a > y.b) {
> +			if (y.b < x.a && y.a <= x.b)
> +				return range(x_t, y.a, x.b);
> +			if (y.a > x.b && y.b >= x.a)
> +				return range(x_t, x.a, y.b);

Nit: here returned type us U64, while above it is S64, I don't think
     it matters but having same type in both branches would be less
     confusing.

> +		}
> +	}
> +
>  	/* otherwise, plain range cast and intersection works */
>  	return range_improve(x_t, x, y_cast);
>  }

Re: [PATCH bpf-next 2/4] selftests/bpf: Update reg_bound range refinement logic

[Paul Chaignon]

On Mon, Jul 21, 2025 at 02:29:47PM -0700, Eduard Zingerman wrote:
> On Sat, 2025-07-19 at 16:22 +0200, Paul Chaignon wrote:
> > This patch updates the range refinement logic in the reg_bound test to
> > match the new logic from the previous commit. Without this change, tests
> > would fail because we end with more precise ranges than the tests
> > expect.
> > 
> > Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> > ---
> 
> Acked-by: Eduard Zingerman <eddyz87@gmail.com>

Thanks for the review!

> 
> >  .../testing/selftests/bpf/prog_tests/reg_bounds.c  | 14 ++++++++++++++
> >  1 file changed, 14 insertions(+)
> > 
> > diff --git a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> > index 39d42271cc46..e261b0e872db 100644
> > --- a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> > +++ b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> > @@ -465,6 +465,20 @@ static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t,
> >  		return range_improve(x_t, x, x_swap);
> >  	}
> >  
> > +	if (!t_is_32(x_t) && !t_is_32(y_t) && x_t != y_t) {
> 
> Nit: I'd swap x and y if necessary, to avoid a second branch.

That works, but we'd have to swap them back before we hit range_improve
below. Something like:

    if (x_t != S64)
        swap(x, y);
    if (x.a > x.b) {
        if (x.b < y.a && x.a <= y.b)
            return range(x_t, x.a, y.b);
        if (x.a > y.b && x.b >= y.a)
            return range(x_t, y.a, x.b);
    }
    if (x_t != S64)
        swap(x, y);

I'm not sure it's better.

> 
> > +		if (x_t == S64 && x.a > x.b) {
> > +			if (x.b < y.a && x.a <= y.b)
> > +				return range(x_t, x.a, y.b);
> > +			if (x.a > y.b && x.b >= y.a)
> > +				return range(x_t, y.a, x.b);
> > +		} else if (x_t == U64 && y.a > y.b) {
> > +			if (y.b < x.a && y.a <= x.b)
> > +				return range(x_t, y.a, x.b);
> > +			if (y.a > x.b && y.b >= x.a)
> > +				return range(x_t, x.a, y.b);
> 
> Nit: here returned type us U64, while above it is S64, I don't think
>      it matters but having same type in both branches would be less
>      confusing.

What do you mean? We have to return x's original type as we're refining
the x range by using the y range.

> 
> > +		}
> > +	}
> > +
> >  	/* otherwise, plain range cast and intersection works */
> >  	return range_improve(x_t, x, y_cast);
> >  }
> 

Re: [PATCH bpf-next 2/4] selftests/bpf: Update reg_bound range refinement logic

[Eduard Zingerman]

On Tue, 2025-07-22 at 23:20 +0200, Paul Chaignon wrote:
> On Mon, Jul 21, 2025 at 02:29:47PM -0700, Eduard Zingerman wrote:
> > On Sat, 2025-07-19 at 16:22 +0200, Paul Chaignon wrote:
> > > This patch updates the range refinement logic in the reg_bound test to
> > > match the new logic from the previous commit. Without this change, tests
> > > would fail because we end with more precise ranges than the tests
> > > expect.
> > > 
> > > Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> > > ---
> > 
> > Acked-by: Eduard Zingerman <eddyz87@gmail.com>
> 
> Thanks for the review!
> 
> > 
> > >  .../testing/selftests/bpf/prog_tests/reg_bounds.c  | 14 ++++++++++++++
> > >  1 file changed, 14 insertions(+)
> > > 
> > > diff --git a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> > > index 39d42271cc46..e261b0e872db 100644
> > > --- a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> > > +++ b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> > > @@ -465,6 +465,20 @@ static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t,
> > >  		return range_improve(x_t, x, x_swap);
> > >  	}
> > >  
> > > +	if (!t_is_32(x_t) && !t_is_32(y_t) && x_t != y_t) {
> > 
> > Nit: I'd swap x and y if necessary, to avoid a second branch.
> 
> That works, but we'd have to swap them back before we hit range_improve
> below.

I missed the part that x_t/range need to be returned,
please ignore my suggestions, patch is good as it is.

[...]

[PATCH bpf-next 3/4] selftests/bpf: Test cross-sign 64bits range refinement

[Paul Chaignon]

This test is a simplified version of a BPF program generated by
syzkaller that caused an invariant violation [1]. It looks like
syzkaller could not extract the reproducer itself (and therefore didn't
report it to the mailing list), but I was able to extract it from the
console logs of a crash.

  0: call bpf_get_prandom_u32#7    ; R0_w=scalar()
  1: w3 = w0                       ; R3_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
  2: w6 = (s8)w0                   ; R6_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
  3: r0 = (s8)r0                   ; R0_w=scalar(smin=smin32=-128,smax=smax32=127)
  4: if w6 >= 0xf0000000 goto pc+4 ; R6_w=scalar(smin=0,smax=umax=umax32=0xefffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
  5: r0 += r6                      ; R0_w=scalar(smin=-128,smax=0xf000007e,smin32=-256,smax32=254)
  6: r6 += 400                     ; R6_w=scalar(smin=umin=smin32=umin32=400,smax=umax=smax32=umax32=527,var_off=(0x0; 0x3ff))
  7: r0 -= r6                      ; R0=scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1,umax=0xffffffffffffff6e,smin32=-783,smax32=-146,umax32=0xffffff6e,var_off=(0xfffffc00; 0xffffffff000003ff))
  8: if r3 < r0 goto pc+0
  REG INVARIANTS VIOLATION (false_reg2): range bounds violation u64=[0xfffffcf1, 0xffffff6e] s64=[0xfffffcf1, 0xeffffeee] u32=[0xfffffcf1, 0xffffff6e] s32=[0xfffffcf1, 0xffffff6e] var_off=(0xfffffc00, 0x3ff)

The principle is similar to the invariant violation described in
6279846b9b25 ("bpf: Forget ranges when refining tnum after JSET"): the
verifier walks a dead branch, uses the condition to refine ranges, and
ends up with inconsistent ranges. In this case, the dead branch is when
we fallthrough on both jumps.

At the second fallthrough, the verifier concludes that R0's umax is
bounded by R3's umax so R0_u64=[0xfffffcf1; 0xffffffff]. That refinement
allows __reg64_deduce_bounds to further refine R0's smin value to
0xfffffcf1. It ends up with R0_s64=[0xfffffcf1; 0xeffffeee], which
doesn't make any sense.

The first patch in this series ("bpf: Improve bounds when s64 crosses
sign boundary") fixes this by refining ranges before we reach the
condition, such that the verifier can detect the jump is always taken.
Indeed, at instruction 7, the ranges look as follows:

    0          umin=0xfffffcf1                 umax=0xff..ff6e  U64_MAX
    |                [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx]        |
    |----------------------------|------------------------------|
    |xxxxxxxxxx]                                   [xxxxxxxxxxxx|
    0    smax=0xeffffeee                       smin=-655        -1

The updated __reg64_deduce_bounds can therefore improve the ranges to
s64=[-655; -146] (and the u64 equivalent). With this new range, it's
clear that the condition at instruction 8 is always true: R3's umax is
0xffffffff and R0's umin is 0xfffffffffffffd71 ((u64)-655). We avoid the
dead branch and don't end up with an invariant violation.

Link: https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf [1]
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 .../selftests/bpf/progs/verifier_bounds.c     | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index 63b533ca4933..d104d43ff911 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -1550,4 +1550,27 @@ l0_%=:	r0 = 0;				\
 	: __clobber_all);
 }
 
+SEC("socket")
+__description("bounds deduction sync cross sign boundary")
+__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
+__retval(0)
+__naked void test_invariants(void)
+{
+	asm volatile("			\
+	call %[bpf_get_prandom_u32];	\
+	w3 = w0;			\
+	w6 = (s8)w0;			\
+	r0 = (s8)r0;			\
+	if w6 >= 0xf0000000 goto l0_%=;	\
+	r0 += r6;			\
+	r6 += 400;			\
+	r0 -= r6;			\
+	if r3 < r0 goto l0_%=;		\
+l0_%=:	r0 = 0;				\
+	exit;				\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.43.0

Re: [PATCH bpf-next 3/4] selftests/bpf: Test cross-sign 64bits range refinement

[Eduard Zingerman]

On Sat, 2025-07-19 at 16:23 +0200, Paul Chaignon wrote:

[...]

> The first patch in this series ("bpf: Improve bounds when s64 crosses
> sign boundary") fixes this by refining ranges before we reach the
> condition, such that the verifier can detect the jump is always taken.
> Indeed, at instruction 7, the ranges look as follows:
> 
>     0          umin=0xfffffcf1                 umax=0xff..ff6e  U64_MAX
>     |                [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx]        |
>     |----------------------------|------------------------------|
>     |xxxxxxxxxx]                                   [xxxxxxxxxxxx|
>     0    smax=0xeffffeee                       smin=-655        -1

I'd move this diagram to the selftest itself.

> 
> The updated __reg64_deduce_bounds can therefore improve the ranges to
> s64=[-655; -146] (and the u64 equivalent). With this new range, it's
> clear that the condition at instruction 8 is always true: R3's umax is
> 0xffffffff and R0's umin is 0xfffffffffffffd71 ((u64)-655). We avoid the
> dead branch and don't end up with an invariant violation.
> 
> Link: https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf [1]
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---
>  .../selftests/bpf/progs/verifier_bounds.c     | 23 +++++++++++++++++++
>  1 file changed, 23 insertions(+)
> 
> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> index 63b533ca4933..d104d43ff911 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> @@ -1550,4 +1550,27 @@ l0_%=:	r0 = 0;				\
>  	: __clobber_all);
>  }
>  
> +SEC("socket")
> +__description("bounds deduction sync cross sign boundary")
> +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__retval(0)
> +__naked void test_invariants(void)

Could you please check deduced range with __msg?

> +{
> +	asm volatile("			\
> +	call %[bpf_get_prandom_u32];	\
> +	w3 = w0;			\
> +	w6 = (s8)w0;			\
> +	r0 = (s8)r0;			\
> +	if w6 >= 0xf0000000 goto l0_%=;	\
> +	r0 += r6;			\
> +	r6 += 400;			\
> +	r0 -= r6;			\
> +	if r3 < r0 goto l0_%=;		\
> +l0_%=:	r0 = 0;				\
> +	exit;				\
> +"	:
> +	: __imm(bpf_get_prandom_u32)
> +	: __clobber_all);
> +}

I think two more test cases are needed:
- when intersection is on the other side of the interval;
- when signed and unsigned intervals overlap in two places.

Re: [PATCH bpf-next 3/4] selftests/bpf: Test cross-sign 64bits range refinement

[Paul Chaignon]

On Mon, Jul 21, 2025 at 02:30:07PM -0700, Eduard Zingerman wrote:
> On Sat, 2025-07-19 at 16:23 +0200, Paul Chaignon wrote:

[...]

> I think two more test cases are needed:
> - when intersection is on the other side of the interval;
> - when signed and unsigned intervals overlap in two places.

Thanks for the review! I've added the two new tests in the v2, along
with appropriate __msg checks. I also made sure the tests fail as
expected without the first patch improving range refinement.

[PATCH bpf-next 4/4] selftests/bpf: Test invariants on JSLT crossing sign

[Paul Chaignon]

The improvement of the u64/s64 range refinement fixed the invariant
violation that was happening on this test for BPF_JSLT when crossing the
sign boundary.

After this patch, we have one test remaining with a known invariant
violation. It's the same test as fixed here but for 32 bits ranges.

Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 tools/testing/selftests/bpf/progs/verifier_bounds.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index d104d43ff911..ddf36d8ab07a 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -1066,7 +1066,7 @@ l0_%=:	r0 = 0;						\
 SEC("xdp")
 __description("bound check with JMP_JSLT for crossing 64-bit signed boundary")
 __success __retval(0)
-__flag(!BPF_F_TEST_REG_INVARIANTS) /* known invariants violation */
+__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void crossing_64_bit_signed_boundary_2(void)
 {
 	asm volatile ("					\
-- 
2.43.0