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, the __reg64_deduce_bounds change was
also tested with Agni, the formal verification tool for the range
analysis [1].

Link: https://github.com/bpfverif/agni
Acked-by: Eduard Zingerman <eddyz87@gmail.com>
Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
Link: https://lore.kernel.org/r/933bd9ce1f36ded5559f92fdc09e5dbc823fa245.1753695655.git.paul.chaignon@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index d218516c3b33efed4190e5b8ccde1dc73f33cc68..251e06dc07ebcf7d6b8e3266d8159f58d73103dc 100644 (file)
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -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);
+               }
        }
 }