This new selftest demonstrates the improvement of bounds refinement from the previous patch. It is inspired from a set of reg_bounds_sync inputs generated using CBMC [1] by Shung-Hsi: reg.smin_value=0x8000000000000002 reg.smax_value=2 reg.umin_value=2 reg.umax_value=19 reg.s32_min_value=2 reg.s32_max_value=3 reg.u32_min_value=2 reg.u32_max_value=3 reg_bounds_sync returns R=[2; 3] without the previous patch, and R=2 with it. __reg64_deduce_bounds is able to derive that u64=2, but before the previous patch, those bounds are overwritten in __reg_deduce_mixed_bounds using the 32bits bounds. To arrive to these reg_bounds_sync inputs, we bound the 32bits value first to [2; 3]. We can then upper-bound s64 without impacting u64. At that point, the refinement to u64=2 doesn't happen because the ranges still overlap in two points: 0 umin=2 umax=0xff..ff00..03 U64_MAX | [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] | |----------------------------|------------------------------| |xx] [xxxxxxxxxxxxxxxxxxxxxxxxxxxx| 0 smax=2 smin=0x800..02 -1 With an upper-bound check at value 19, we can reach the above inputs for reg_bounds_sync. At that point, the refinement to u64=2 happens and because it isn't overwritten by __reg_deduce_mixed_bounds anymore, reg_bounds_sync returns with reg=2. The test validates this result by including an illegal instruction in the (dead) branch reg != 2. Link: https://github.com/shunghsiyu/reg_bounds_sync-review/ [1] Co-developed-by: Shung-Hsi Yu Signed-off-by: Shung-Hsi Yu Signed-off-by: Paul Chaignon --- .../selftests/bpf/progs/verifier_bounds.c | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c index ce09379130aa..3724d5e5bcb3 100644 --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c @@ -2037,4 +2037,37 @@ __naked void signed_unsigned_intersection32_case2(void *ctx) : __clobber_all); } +/* After instruction 3, the u64 and s64 ranges look as follows: + * 0 umin=2 umax=0xff..ff00..03 U64_MAX + * | [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] | + * |----------------------------|------------------------------| + * |xx] [xxxxxxxxxxxxxxxxxxxxxxxxxxxx| + * 0 smax=2 smin=0x800..02 -1 + * + * The two ranges can't be refined because they overlap in two places. Once we + * add an upper-bound to u64 at instruction 4, the refinement can happen. This + * test validates that this refinement does happen and is not overwritten by + * the less-precise 32bits ranges. + */ +SEC("socket") +__description("bounds refinement: 64bits ranges not overwritten by 32bits ranges") +__msg("3: (65) if r0 s> 0x2 {{.*}} R0=scalar(smin=0x8000000000000002,smax=2,umin=smin32=umin32=2,umax=0xffffffff00000003,smax32=umax32=3") +__msg("4: (25) if r0 > 0x13 {{.*}} R0=2") +__success __log_level(2) +__naked void refinement_32bounds_not_overwriting_64bounds(void *ctx) +{ + asm volatile(" \ + call %[bpf_get_prandom_u32]; \ + if w0 < 2 goto +5; \ + if w0 > 3 goto +4; \ + if r0 s> 2 goto +3; \ + if r0 > 19 goto +2; \ + if r0 == 2 goto +1; \ + r10 = 0; \ + exit; \ +" : + : __imm(bpf_get_prandom_u32) + : __clobber_all); +} + char _license[] SEC("license") = "GPL"; -- 2.43.0