bpf: Improve 64bits bounds refinement
Subsystems (4)
v2 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).
Changes in v2 (all on Eduard's suggestions):
- Added two tests to ensure we cover all cases of u64/s64 overlap.
- Improved tests to check deduced ranges with __msg.
- Improved code comments.
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 | 52 ++++++++ .../selftests/bpf/prog_tests/reg_bounds.c | 14 ++ .../selftests/bpf/progs/verifier_bounds.c | 120 +++++++++++++++++- 3 files changed, 185 insertions(+), 1 deletion(-)
Signature · 1 line
2.43.0
PATCH v2 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 | 52 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+)
kernel/bpf/verifier.c +52 -0
@@ -2523,6 +2523,58 @@ 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 first diagram +* above. +*/ +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) { +/* This second condition considers the case where the u64 range +* overlaps with the negative portion of the s64 range: +* +* 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); + } } }
Signature · 1 line
2.43.0
PATCH v2 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
PATCH v2 3/4 selftests/bpf: Test cross-sign 64bits range refinement
In reply to Paul ChaignonThis patch adds coverage for the new cross-sign 64bits range refinement logic. The three tests cover the cases when the u64 and s64 ranges overlap (1) in the negative portion of s64, (2) in the positive portion of s64, and (3) in both portions.
The first 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.
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. The new refinement logic improves the bounds such that the second jump is properly detected as always-taken and the verifier doesn't end up walking a dead branch.
The second and third tests are inspired by the first, but rely on condition jumps to prepare the bounds instead of ALU instructions. An R10 write is used to trigger a verifier error when the bounds can't be refined.
--- .../selftests/bpf/progs/verifier_bounds.c | 118 ++++++++++++++++++ 1 file changed, 118 insertions(+)
tools/testing/selftests/bpf/progs/verifier_bounds.c +118 -0
@@ -1550,4 +1550,122 @@ l0_%=: r0 = 0; \ : __clobber_all); } +/* This test covers the bounds deduction on 64bits when the s64 and u64 ranges +* overlap on the negative side. 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 +* +* We should therefore deduce the following new bounds: +* +* 0 u64=[0xff..ffd71;0xff..ff6e] U64_MAX +* | [xxx] | +* |----------------------------|------------------------------| +* | [xxx] | +* 0 s64=[-655;-146] -1 +* +* Without the deduction cross sign boundary, we end up with an invariant +* violation error. +*/ +SEC("socket") +__description("bounds deduction cross sign boundary, negative overlap") +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS) +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))") +__retval(0) +__naked void bounds_deduct_negative_overlap(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); +} + +/* This test covers the bounds deduction on 64bits when the s64 and u64 ranges +* overlap on the positive side. At instruction 3, the ranges look as follows: +* +* 0 umin=0 umax=0xfffffffffffffeff U64_MAX +* [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] | +* |----------------------------|------------------------------| +* |xxxxxxxx] [xxxxxxxx| +* 0 smax=127 smin=-128 -1 +* +* We should therefore deduce the following new bounds: +* +* 0 u64=[0;127] U64_MAX +* [xxxxxxxx] | +* |----------------------------|------------------------------| +* [xxxxxxxx] | +* 0 s64=[0;127] -1 +* +* Without the deduction cross sign boundary, the program is rejected due to +* the frame pointer write. +*/ +SEC("socket") +__description("bounds deduction cross sign boundary, positive overlap") +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS) +__msg("3: (2d) if r0 > r1 {{.*}} R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=127,var_off=(0x0; 0x7f))") +__retval(0) +__naked void bounds_deduct_positive_overlap(void) +{ + asmvolatile (" \ +call %[bpf_get_prandom_u32]; \ +r0 = (s8)r0; \ +r1 = 0xffffffffffffff00; \ +if r0 > r1 goto l0_%=; \ +if r0 < 128 goto l0_%=; \ +r10 = 0; \ +l0_%=: r0 = 0; \ +exit; \ +" : + : __imm(bpf_get_prandom_u32) + : __clobber_all); +} + +/* This test is the same as above, but the s64 and u64 ranges overlap in two +* places. At instruction 3, the ranges look as follows: +* +* 0 umin=0 umax=0xffffffffffffff80 U64_MAX +* [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] | +* |----------------------------|------------------------------| +* |xxxxxxxx] [xxxxxxxx| +* 0 smax=127 smin=-128 -1 +* +* 0xffffffffffffff80 = (u64)-128. We therefore can't deduce anything new and +* the program should fail due to the frame pointer write. +*/ +SEC("socket") +__description("bounds deduction cross sign boundary, two overlaps") +__failure __flag(BPF_F_TEST_REG_INVARIANTS) +__msg("3: (2d) if r0 > r1 {{.*}} R0_w=scalar(smin=smin32=-128,smax=smax32=127,umax=0xffffffffffffff80)") +__msg("frame pointer is read only") +__naked void bounds_deduct_two_overlaps(void) +{ + asmvolatile (" \ +call %[bpf_get_prandom_u32]; \ +r0 = (s8)r0; \ +r1 = 0xffffffffffffff80; \ +if r0 > r1 goto l0_%=; \ +if r0 < 128 goto l0_%=; \ +r10 = 0; \ +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 v2 3/4] selftests/bpf: Test cross-sign 64bits range refinement
Quoted 19 lines · Paul Chaignon
This patch adds coverage for the new cross-sign 64bits range refinement logic. The three tests cover the cases when the u64 and s64 ranges overlap (1) in the negative portion of s64, (2) in the positive portion of s64, and (3) in both portions.
The first 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.
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. The new refinement logic improves the bounds such that the second jump is properly detected as always-taken and the verifier doesn't end up walking a dead branch.
Quoted 8 lines
The second and third tests are inspired by the first, but rely on condition jumps to prepare the bounds instead of ALU instructions. An R10 write is used to trigger a verifier error when the bounds can't be refined.
Signed-off-by Paul Chaignon <[email protected]>---
Hi Paul,
Thank you for adding the tests, I think the patch looks good.
Quoted 25 lines
.../selftests/bpf/progs/verifier_bounds.c | 118 ++++++++++++++++++ 1 file changed, 118 insertions(+)tools/testing/selftests/bpf/progs/verifier_bounds.c +14
-0@@ -1550,4 +1550,122 @@ l0_%=: r0 = 0; \ : __clobber_all); } +/* This test covers the bounds deduction on 64bits when the s64 and u64 ranges +* overlap on the negative side. 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 +* +* We should therefore deduce the following new bounds: +* +* 0 u64=[0xff..ffd71;0xff..ff6e] U64_MAX +* | [xxx] | +* |----------------------------|------------------------------|
tools/testing/selftests/bpf/progs/verifier_bounds.c l0_%=: r0 = 0; \ · line 1576
Quoted 10 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +10
-0+* | [xxx] | +* 0 s64=[-655;-146] -1 +* +* Without the deduction cross sign boundary, we end up with an invariant +* violation error. +*/ +SEC("socket") +__description("bounds deduction cross sign boundary, negative overlap") +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS) +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")
Interesting, note the difference: smin=-655, smin32=-783. There is a code to infer s32 range from s46 range in this situation in __reg32_deduce_bounds(), but it looks like a third __reg_deduce_bounds call is needed to trigger it. E.g. the following patch removes the difference for me:
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index f0a41f1596b6..87050d17baf9 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2686,6 +2686,7 @@ static void reg_bounds_sync(struct bpf_reg_state *reg)
/* We might have learned something about the sign bit. */
__reg_deduce_bounds(reg);
__reg_deduce_bounds(reg);
+ __reg_deduce_bounds(reg);
/* We might have learned some bits from the bounds. */
__reg_bound_offset(reg);
/* Intersecting with the old var_off might have improved our boundsQuoted 19 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +19
-0+__retval(0) +__naked void bounds_deduct_negative_overlap (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); +}
[...]
Re: [PATCH bpf-next v2 3/4] selftests/bpf: Test cross-sign 64bits range refinement
Quoted 1 line · Eduard Zingerman
On Thu, 2025-07-24 at 15:43 +0200, Paul Chaignon wrote:
[...]
Quoted 10 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c l0_%=: r0 = 0; \ · line 1576
Quoted 4 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +4
-0+SEC("socket") +__description("bounds deduction cross sign boundary, negative overlap") +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS) +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")Interesting, note the difference: smin=-655, smin32=-783. There is a code to infer s32 range from s46 range in this situation in
__reg32_deduce_bounds(), but it looks like a third__reg_deduce_boundscall is needed to trigger it. E.g. the following patch removes the difference for me:
Hm, I can add the third __reg_deduce_bounds to the first patch in the series. That said, we may want to rethink and optimize reg_bounds_sync in a followup patchset. It's probably worth listing all the inferences we have and their dependencies and see if we can reorganize the subfunctions.
Quoted 35 lines
diff --git
a/kernel/bpf/verifier.cb/kernel/bpf/verifier.cindexf0a41f1596b6..87050d17baf9100644
---a/kernel/bpf/verifier.c
+++b/kernel/bpf/verifier.c
@@ -2686,6 +2686,7 @@ static voidreg_bounds_sync(struct bpf_reg_state *reg)/* We might have learned something about the sign bit. */ __reg_deduce_bounds(reg); __reg_deduce_bounds(reg); + __reg_deduce_bounds(reg); /* We might have learned some bits from the bounds. */ __reg_bound_offset(reg); /* Intersecting with the old var_off might have improved our boundsQuoted 19 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +19
-0+__retval(0) +__naked void bounds_deduct_negative_overlap (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); +}[...]
Eduard Zingerman
maintainerRe: [PATCH bpf-next v2 3/4] selftests/bpf: Test cross-sign 64bits range refinement
Quoted 16 lines · Paul Chaignon
Quoted 1 line · Eduard Zingerman
On Thu, 2025-07-24 at 15:43 +0200, Paul Chaignon wrote:
[...]
Quoted 10 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c l0_%=: r0 = 0; \ · line 1576
Quoted 4 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +4
-0+SEC("socket") +__description("bounds deduction cross sign boundary, negative overlap") +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS) +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")Interesting, note the difference: smin=-655, smin32=-783. There is a code to infer s32 range from s46 range in this situation in
__reg32_deduce_bounds(), but it looks like a third__reg_deduce_boundscall is needed to trigger it. E.g. the following patch removes the difference for me:
Quoted 5 lines
Hm, I can add the third
__reg_deduce_boundsto the first patch in the series. That said, we may want to rethink and optimizereg_bounds_syncin a followup patchset. It's probably worth listing all the inferences we have and their dependencies and see if we can reorganize the subfunctions.
Let's not add third __reg_deduce_bounds yet. After inserting some prints and looking more closely at the log, something funny happens at instruction #2:
2: (bc) w6 = (s8)w0
reg_bounds_sync entry: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) reg_bounds_sync __update_reg_bounds #1: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) reg_bounds_sync __reg_deduce_bounds #1: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) reg_bounds_sync __reg_deduce_bounds #2: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) reg_bounds_sync __reg_bound_offset: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) reg_bounds_sync __update_reg_bounds #2: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) 3: R0_w=scalar() R6_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
It would be good to figure out what happens here.
That being said, the issue is not related to the patch in question. I suggest rephrasing the test to avoid the sign extension above.
[...]
Eduard Zingerman
maintainerRe: [PATCH bpf-next v2 3/4] selftests/bpf: Test cross-sign 64bits range refinement
Quoted 36 lines · Eduard Zingerman
Quoted 16 lines · Paul Chaignon
Quoted 1 line · Eduard Zingerman
On Thu, 2025-07-24 at 15:43 +0200, Paul Chaignon wrote:
[...]
Quoted 10 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c l0_%=: r0 = 0; \ · line 1576
Quoted 4 lines
tools/testing/selftests/bpf/progs/verifier_bounds.c +4
-0+SEC("socket") +__description("bounds deduction cross sign boundary, negative overlap") +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS) +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")Interesting, note the difference: smin=-655, smin32=-783. There is a code to infer s32 range from s46 range in this situation in
__reg32_deduce_bounds(), but it looks like a third__reg_deduce_boundscall is needed to trigger it. E.g. the following patch removes the difference for me:Quoted 5 lines
Hm, I can add the third
__reg_deduce_boundsto the first patch in the series. That said, we may want to rethink and optimizereg_bounds_syncin a followup patchset. It's probably worth listing all the inferences we have and their dependencies and see if we can reorganize the subfunctions.Let's not add third
__reg_deduce_boundsyet. After inserting some prints and looking more closely at the log, something funny happens at instruction #2:2: (bc) w6 = (s8)w0
reg_bounds_syncentry:scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))reg_bounds_sync__update_reg_bounds#1:scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))reg_bounds_sync__reg_deduce_bounds#1:scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))reg_bounds_sync__reg_deduce_bounds#2:scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))reg_bounds_sync__reg_bound_offset:scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))reg_bounds_sync__update_reg_bounds#2:scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))3: R0_w=scalar() R6_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0;0xffffffff))
Quoted 5 lines
It would be good to figure out what happens here.
That being said, the issue is not related to the patch in question. I suggest rephrasing the test to avoid the sign extension above.[...]
Apologies, I'm being stupid above. The range after sign extension is perfectly fine.
So, going back to the question of the test cases, here is a relevant part with debug prints [1]:
7: (1f) r0 -= r6
reg_bounds_sync entry: scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146)
reg_bounds_sync __update_reg_bounds #1: scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146)
__reg32_deduce_bounds #8: scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146,umin32=0xfffffcf1,umax32=0xffffff6e)
__reg_deduce_mixed_bounds #1: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e) reg_bounds_sync __reg_deduce_bounds #1: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e) __reg32_deduce_bounds #7: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e) __reg32_deduce_bounds #8: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e)
__reg64_deduce_bounds #4: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
__reg_deduce_mixed_bounds #1: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
reg_bounds_sync __reg_deduce_bounds #2: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
reg_bounds_sync __reg_bound_offset: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))
reg_bounds_sync __update_reg_bounds #2: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))
8: R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))
R6=scalar(smin=umin=smin32=umin32=400,smax=umax=smax32=umax32=527,var_off=(0x0; 0x3ff))
Important parts are:
a. "__reg32_deduce_bounds #8" updates umin32 and umax32
b. "__reg_deduce_mixed_bounds #1" updates umin and umax (uses values from a)
c. "__reg64_deduce_bounds #4" updates smax and umin (enabled by b)
Only at this point there is an opportunity to refine smin32 from smin using rule "__reg32_deduce_bounds #2", because of the conditions for umin and umax (umin refinement by (c) is crucial).
Your new check is (c).
So, it looks like adding third call to __reg_deduce_bounds() in reg_bounds_sync() is not wrong and the change is linked to this patch-set.
As you say, whether there is a better way to organize all these rules requires further analysis, and is a bit out of scope for this patch-set.
[1] https://github.com/kernel-patches/bpf/commit/f68d4957204f21caac67d24de40fb66e4618f354
Re: [PATCH bpf-next v2 3/4] selftests/bpf: Test cross-sign 64bits range refinement
On Fri, Jul 25, 2025 at 12:15:18AM -0700, Eduard Zingerman wrote:
[...]
Quoted 25 lines
So, going back to the question of the test cases, here is a relevant part with debug prints [1]:
7: (1f) r0 -= r6
reg_bounds_syncentry:scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146)
reg_bounds_sync__update_reg_bounds#1:scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146)
__reg32_deduce_bounds#8:scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146,umin32=0xfffffcf1,umax32=0xffffff6e)__reg_deduce_mixed_bounds #1: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e) reg_bounds_sync __reg_deduce_bounds #1: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e) __reg32_deduce_bounds #7: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e) __reg32_deduce_bounds #8: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e)
__reg64_deduce_bounds#4:scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
__reg_deduce_mixed_bounds#1:scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
reg_bounds_sync__reg_deduce_bounds#2:scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
reg_bounds_sync__reg_bound_offset: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00;0x3ff))
reg_bounds_sync__update_reg_bounds#2: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00;0x3ff))8: R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00;
0x3ff))R6=scalar(smin=umin=smin32=umin32=400,smax=umax=smax32=umax32=527,var_off=(0x0; 0x3ff))Important parts are:
a. "__reg32_deduce_bounds#8" updates umin32 and umax32
b. "__reg_deduce_mixed_bounds#1" updates umin and umax (uses values from a)
c. "__reg64_deduce_bounds#4" updates smax and umin (enabled by b)
Quoted 8 lines
Only at this point there is an opportunity to refine smin32 from smin using rule "
__reg32_deduce_bounds#2", because of the conditions for umin and umax (umin refinement by (c) is crucial).
Your new check is (c).So, it looks like adding third call to
__reg_deduce_bounds()inreg_bounds_sync()is not wrong and the change is linked to this patch-set.
Thanks a lot for the full analysis! I've added a patch in the v3 to call __reg_deduce_bounds a third time. I reused your analysis and trace from above in the patch description. Note I added you as a co-author; give me a shout if I shouldn't have.
Quoted 6 lines
As you say, whether there is a better way to organize all these rules requires further analysis, and is a bit out of scope for this patch-set.
[1] https://github.com/kernel-patches/bpf/commit/f68d4957204f21caac67d24de40fb66e4618f354
Eduard Zingerman
maintainerRe: [PATCH bpf-next v2 3/4] selftests/bpf: Test cross-sign 64bits range refinement
On Sat, 2025-07-26 at 12:07 +0200, Paul Chaignon wrote:
[...]
Quoted 4 lines
Thanks a lot for the full analysis! I've added a patch in the v3 to call
__reg_deduce_boundsa third time. I reused your analysis and trace from above in the patch description. Note I added you as a co-author; give me a shout if I shouldn't have.
Acked remaining patches, thank you for working on this!
PATCH v2 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
Re: [PATCH bpf-next v2 4/4] selftests/bpf: Test invariants on JSLT crossing sign
Quoted 9 lines · Paul Chaignon
The improvement of the u64/s64 range refinement fixed the invariant violation that was happening on this test for
BPF_JSLTwhen 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 <[email protected]>---
[...]