mirrors/linux
2
0
Fork 0
mirror of https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git synced 2026-05-16 13:41:48 -04:00
Code Issues Packages Projects Releases Wiki Activity

selftests/bpf: Test case for refinement improvement using 64b bounds

Browse Source 
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 <shung-hsi.yu@suse.com>
Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
Tested-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/r/622dc51c581cd4d652fff362188b2a5f73c1fe99.1773401138.git.paul.chaignon@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
This commit is contained in:
Paul Chaignon
2026-03-13 12:43:07 +01:00
committed by Alexei Starovoitov
parent 9e5fcb003a
commit 0a753d8cd6
1 changed files with 33 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

33
tools/testing/selftests/bpf/progs/verifier_bounds.c
View File

@@ -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";