bpf: Improve 64bits bounds refinement
Subsystems (4)
cover bpf: Improve 64bits bounds refinement
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).
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(-)
Signature · 1 line
2.43.0
PATCH 1/4 bpf: Improve bounds when s64 crosses sign boundary
__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].
--- kernel/bpf/verifier.c | 44 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+)
kernel/bpf/verifier.c +44 -0
@@ -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); + } } }
Signature · 1 line
2.43.0
Re: [PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary
On Sat, 2025-07-19 at 16:22 +0200, Paul Chaignon wrote:
[...]
Quoted 30 lines
kernel/bpf/verifier.c +30
-0+/* 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|
kernel/bpf/verifier.c static void __reg64_deduce_bounds(struct bpf_reg_state *reg) · line 2566
Quoted 10 lines
kernel/bpf/verifier.c +10
-0+* 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
Quoted 6 lines
kernel/bpf/verifier.c +3
-0+ 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
In reply to Paul ChaignonQuoted 73 lines · Paul Chaignon
__reg64_deduce_boundscurrently 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_boundsto 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|
0S64_MAXS64_MIN-1The 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] |
0S64_MAXS64_MIN-1The 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 <[email protected]>--- kernel/bpf/verifier.c | 44 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+)kernel/bpf/verifier.c +30
-0@@ -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] | +* |----------------------------|----------------------------|
kernel/bpf/verifier.c static void __reg64_deduce_bounds(struct bpf_reg_state *reg) · line 2565
Quoted 10 lines
kernel/bpf/verifier.c +10
-0+* |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);
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.
Quoted 10 lines
kernel/bpf/verifier.c +4
-0+ }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); + } } }Signature · 1 line
2.43.0
Re: [PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary
Quoted 1 line · Shung-Hsi Yu
On Sat, Jul 19, 2025 at 04:22:05PM +0200, Paul Chaignon wrote:
[...]
Quoted 50 lines
Quoted 29 lines
kernel/bpf/verifier.c +29
-0+/* 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] | +* |----------------------------|----------------------------| kernel/bpf/verifier.c static void __reg64_deduce_bounds(struct bpf_reg_state *reg) · line 2565
Quoted 10 lines
kernel/bpf/verifier.c +10
-0+* |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 <[email protected]>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
Quoted 8 lines
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 :)
Quoted 11 lines
Quoted 11 lines
kernel/bpf/verifier.c +4
-0+ }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); + } } }Signature · 2 lines
-- 2.43.0
Re: [PATCH bpf-next 1/4] bpf: Improve bounds when s64 crosses sign boundary
Quoted 67 lines · Paul Chaignon
Quoted 1 line · Shung-Hsi Yu
On Sat, Jul 19, 2025 at 04:22:05PM +0200, Paul Chaignon wrote:
[...]
Quoted 50 lines
Quoted 29 lines
kernel/bpf/verifier.c +29
-0+/* 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] | +* |----------------------------|----------------------------| kernel/bpf/verifier.c static void __reg64_deduce_bounds(struct bpf_reg_state *reg) · line 2565
Quoted 10 lines
kernel/bpf/verifier.c +10
-0+* |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 <[email protected]>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 -1Quoted 8 lines
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.
Quoted 6 lines
I considered returning an error from
__reg64_deduce_boundsif that invariant doesn't hold, but propagating it gets a bit messy. Adding it toreg_bounds_sanity_checkwould 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 2/4 selftests/bpf: Update reg_bound range refinement logic
In reply to Paul ChaignonThis 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.
--- .../testing/selftests/bpf/prog_tests/reg_bounds.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+)
tools/testing/selftests/bpf/prog_tests/reg_bounds.c +14 -0
@@ -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); }
Signature · 1 line
2.43.0
Re: [PATCH bpf-next 2/4] selftests/bpf: Update reg_bound range refinement logic
Quoted 7 lines · Paul Chaignon
This patch updates the range refinement logic in the
reg_boundtest 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 <[email protected]>---
tools/testing/selftests/bpf/prog_tests/reg_bounds.c static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t, · line 468
Quoted 12 lines
.../testing/selftests/bpf/prog_tests/reg_bounds.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+)tools/testing/selftests/bpf/prog_tests/reg_bounds.c +1
-0@@ -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.
tools/testing/selftests/bpf/prog_tests/reg_bounds.c static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t, · line 478
Quoted 10 lines
tools/testing/selftests/bpf/prog_tests/reg_bounds.c +10
-0+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.
Quoted 6 lines
tools/testing/selftests/bpf/prog_tests/reg_bounds.c +3
-0+ } + } +/* 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
Quoted 10 lines · Eduard Zingerman
Quoted 7 lines · Paul Chaignon
This patch updates the range refinement logic in the
reg_boundtest 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 <[email protected]>---
Acked-by Eduard Zingerman <[email protected]>
Thanks for the review!
Quoted 12 lines
Quoted 12 lines
.../testing/selftests/bpf/prog_tests/reg_bounds.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+)tools/testing/selftests/bpf/prog_tests/reg_bounds.c +0
-0@@ -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); }
Quoted 3 lines
tools/testing/selftests/bpf/prog_tests/reg_bounds.c static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t, · line 468
Quoted 1 line
tools/testing/selftests/bpf/prog_tests/reg_bounds.c +1
-0+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.
Quoted 15 lines
tools/testing/selftests/bpf/prog_tests/reg_bounds.c static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t, · line 478
Quoted 11 lines
tools/testing/selftests/bpf/prog_tests/reg_bounds.c +10
-0+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.
Quoted 8 lines
Quoted 7 lines
tools/testing/selftests/bpf/prog_tests/reg_bounds.c +3
-0+ } + } +/* otherwise, plain range cast and intersection works */ return range_improve (x_t, x, y_cast); }
Eduard Zingerman
maintainerRe: [PATCH bpf-next 2/4] selftests/bpf: Update reg_bound range refinement logic
Quoted 26 lines · Paul Chaignon
Quoted 10 lines · Eduard Zingerman
Quoted 7 lines · Paul Chaignon
This patch updates the range refinement logic in the
reg_boundtest 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 <[email protected]>---
Acked-by Eduard Zingerman <[email protected]>Thanks for the review!
Quoted 12 lines
Quoted 12 lines
.../testing/selftests/bpf/prog_tests/reg_bounds.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+)tools/testing/selftests/bpf/prog_tests/reg_bounds.c +0
-0@@ -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); }
Quoted 6 lines
Quoted 3 lines
tools/testing/selftests/bpf/prog_tests/reg_bounds.c static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t, · line 468
Quoted 1 line
tools/testing/selftests/bpf/prog_tests/reg_bounds.c +1
-0+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_improvebelow.
I missed the part that x_t/range need to be returned, please ignore my suggestions, patch is good as it is.
[...]
PATCH 3/4 selftests/bpf: Test cross-sign 64bits range refinement
In reply to Paul ChaignonThis 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 -1The 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.
--- .../selftests/bpf/progs/verifier_bounds.c | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+)
tools/testing/selftests/bpf/progs/verifier_bounds.c +23 -0
@@ -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) +{ + asmvolatile (" \ +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";
Signature · 1 line
2.43.0
Eduard Zingerman
maintainerRe: [PATCH bpf-next 3/4] selftests/bpf: Test cross-sign 64bits range refinement
On Sat, 2025-07-19 at 16:23 +0200, Paul Chaignon wrote:
[...]
Quoted 10 lines
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.
Quoted 18 lines
The updated
__reg64_deduce_boundscan 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 is0xffffffffand R0's umin is0xfffffffffffffd71((u64)-655). We avoid the dead branch and don't end up with an invariant violation.Signed-off-by Paul Chaignon <[email protected]>--- .../selftests/bpf/progs/verifier_bounds.c | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+)tools/testing/selftests/bpf/progs/verifier_bounds.c +0
-0
tools/testing/selftests/bpf/progs/verifier_bounds.c l0_%=: r0 = 0; \ · line 1557
Quoted 8 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +5
-0@@ -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?
Quoted 7 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +7
-0+{ + asm volatile(" \ + call %[bpf_get_prandom_u32]; \ + w3 = w0; \ + w6 = (s8)w0; \ + r0 = (s8)r0; \ + if w6 >= 0xf0000000 goto l0_%=; \
tools/testing/selftests/bpf/progs/verifier_bounds.c l0_%=: r0 = 0; \ · line 1574
Quoted 10 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +10
-0+ 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
Quoted 1 line · Eduard Zingerman
On Sat, 2025-07-19 at 16:23 +0200, Paul Chaignon wrote:
[...]
Quoted 3 lines
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 4/4 selftests/bpf: Test invariants on JSLT crossing sign
In reply to Paul ChaignonThe 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.
--- tools/testing/selftests/bpf/progs/verifier_bounds.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-)
tools/testing/selftests/bpf/progs/verifier_bounds.c +1 -1
@@ -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 voidcrossing_64_bit_signed_boundary_2 (void) { asm volatile (" \
Signature · 1 line
2.43.0