On Mon, 2025-06-23 at 00:03 -0400, Harishankar Vishwanathan wrote:
> The previous commit improves the precision in scalar(32)_min_max_add,
> and scalar(32)_min_max_sub. The improvement in precision occurs in cases
> when all outcomes overflow or underflow, respectively.
>
> This commit adds selftests that exercise those cases.
>
> This commit also adds selftests for cases where the output register
> state bounds for u(32)_min/u(32)_max are conservatively set to unbounded
> (when there is partial overflow or underflow).
>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx>
> Co-developed-by: Matan Shachnai <m.shachnai@xxxxxxxxxxx>
> Signed-off-by: Matan Shachnai <m.shachnai@xxxxxxxxxxx>
> Suggested-by: Eduard Zingerman <eddyz87@xxxxxxxxx>
> ---
Thank you for adding these tests. Even with "human readable" numbers
took me 15-20 minutes to verify the numbers :)
Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx>
> .../selftests/bpf/progs/verifier_bounds.c | 161 ++++++++++++++++++
> 1 file changed, 161 insertions(+)
>
> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> index 30e16153fdf1..31986f6c609e 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> @@ -1371,4 +1371,165 @@ __naked void mult_sign_ovf(void)
> __imm(bpf_skb_store_bytes)
> : __clobber_all);
> }
> +
> +SEC("socket")
> +__description("64-bit addition, all outcomes overflow")
> +__success __log_level(2)
> +__msg("5: (0f) r3 += r3 {{.*}} R3_w=scalar(umin=0x4000000000000000,umax=0xfffffffffffffffe)")
> +__retval(0)
> +__naked void add64_full_overflow(void)
> +{
> + asm volatile (
> + "r4 = 0;"
> + "r4 = -r4;"
Nit: there is a change in the workings that would make range
propagation in negation instruction, a better way to get unbound
scalar here is e.g. call to bpf_get_prandom_u32() or read from a
constant global map.
Depending on order in which patches would be accepted this rework
would be either on you or on the other patch-set author.
> + "r3 = 0xa000000000000000 ll;"
> + "r3 |= r4;"
> + "r3 += r3;"
> + "r0 = 0;"
> + "exit"
> + :
> + :
> + : __clobber_all);
> +}
[...]
