[v5,bpf-next,06/23] bpf: add special smin32/smax32 derivation from 64-bit bounds

Commit Message

Andrii Nakryiko Oct. 27, 2023, 6:13 p.m. UTC

Add a special case where we can derive valid s32 bounds from umin/umax
or smin/smax by stitching together negative s32 subrange and
non-negative s32 subrange. That requires upper 32 bits to form a [N, N+1]
range in u32 domain (taking into account wrap around, so 0xffffffff
to 0x00000000 is a valid [N, N+1] range in this sense). See code comment
for concrete examples.

Acked-by: Shung-Hsi Yu <[e-mail]>
Signed-off-by: Andrii Nakryiko <[e-mail]>
---
 kernel/bpf/verifier.c | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

Comments

Eduard Zingerman Oct. 31, 2023, 3:37 p.m. UTC | #1

On Fri, 2023-10-27 at 11:13 -0700, Andrii Nakryiko wrote:
> Add a special case where we can derive valid s32 bounds from umin/umax
> or smin/smax by stitching together negative s32 subrange and
> non-negative s32 subrange. That requires upper 32 bits to form a [N, N+1]
> range in u32 domain (taking into account wrap around, so 0xffffffff
> to 0x00000000 is a valid [N, N+1] range in this sense). See code comment
> for concrete examples.
> 
> Acked-by: Shung-Hsi Yu <[e-mail]>
> Signed-off-by: Andrii Nakryiko <[e-mail]>

Acked-by: Eduard Zingerman <[e-mail]>

fwiw, an alternative explanation might be arithmetic based.
Suppose:
. there are numbers a, b, c
. 2**31 <= b < 2**32
. 0 <= c < 2**31
. umin = 2**32 * a + b
. umax = 2**32 * (a + 1) + c

The number of values in the range represented by [umin; umax] is:
. N = umax - umin + 1 = 2**32 + c - b + 1
. min(N) = 2**32 + 0 - (2**32-1) + 1 = 2
. max(N) = 2**32 + (2**31 - 1) - 2**31 + 1 = 2**32
Hence [(s32)b; (s32)c] form a valid range.

At-least that's how I convinced myself.

> ---
>  kernel/bpf/verifier.c | 23 +++++++++++++++++++++++
>  1 file changed, 23 insertions(+)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 5082ca1ea5dc..38d21d0e46bd 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2369,6 +2369,29 @@ static void __reg32_deduce_bounds(struct bpf_reg_state *reg)
>  			reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
>  		}
>  	}
> +	/* Special case where upper bits form a small sequence of two
> +	 * sequential numbers (in 32-bit unsigned space, so 0xffffffff to
> +	 * 0x00000000 is also valid), while lower bits form a proper s32 range
> +	 * going from negative numbers to positive numbers. E.g., let's say we
> +	 * have s64 range [-1, 1] ([0xffffffffffffffff, 0x0000000000000001]).
> +	 * Possible s64 values are {-1, 0, 1} ({0xffffffffffffffff,
> +	 * 0x0000000000000000, 0x00000000000001}). Ignoring upper 32 bits,
> +	 * we still get a valid s32 range [-1, 1] ([0xffffffff, 0x00000001]).
> +	 * Note that it doesn't have to be 0xffffffff going to 0x00000000 in
> +	 * upper 32 bits. As a random example, s64 range
> +	 * [0xfffffff0ffffff00; 0xfffffff100000010], forms a valid s32 range
> +	 * [-16, 16] ([0xffffff00; 0x00000010]) in its 32 bit subregister.
> +	 */
> +	if ((u32)(reg->umin_value >> 32) + 1 == (u32)(reg->umax_value >> 32) &&
> +	    (s32)reg->umin_value < 0 && (s32)reg->umax_value >= 0) {
> +		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->umin_value);
> +		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->umax_value);
> +	}
> +	if ((u32)(reg->smin_value >> 32) + 1 == (u32)(reg->smax_value >> 32) &&
> +	    (s32)reg->smin_value < 0 && (s32)reg->smax_value >= 0) {
> +		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->smin_value);
> +		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
> +	}
>  	/* if u32 range forms a valid s32 range (due to matching sign bit),
>  	 * try to learn from that
>  	 */

Andrii Nakryiko Oct. 31, 2023, 5:39 p.m. UTC | #2

On Tue, Oct 31, 2023 at 8:37 AM Eduard Zingerman <[e-mail]> wrote:
>
> On Fri, 2023-10-27 at 11:13 -0700, Andrii Nakryiko wrote:
> > Add a special case where we can derive valid s32 bounds from umin/umax
> > or smin/smax by stitching together negative s32 subrange and
> > non-negative s32 subrange. That requires upper 32 bits to form a [N, N+1]
> > range in u32 domain (taking into account wrap around, so 0xffffffff
> > to 0x00000000 is a valid [N, N+1] range in this sense). See code comment
> > for concrete examples.
> >
> > Acked-by: Shung-Hsi Yu <[e-mail]>
> > Signed-off-by: Andrii Nakryiko <[e-mail]>
>
> Acked-by: Eduard Zingerman <[e-mail]>
>
> fwiw, an alternative explanation might be arithmetic based.
> Suppose:
> . there are numbers a, b, c
> . 2**31 <= b < 2**32
> . 0 <= c < 2**31
> . umin = 2**32 * a + b
> . umax = 2**32 * (a + 1) + c
>
> The number of values in the range represented by [umin; umax] is:
> . N = umax - umin + 1 = 2**32 + c - b + 1
> . min(N) = 2**32 + 0 - (2**32-1) + 1 = 2
> . max(N) = 2**32 + (2**31 - 1) - 2**31 + 1 = 2**32
> Hence [(s32)b; (s32)c] form a valid range.
>
> At-least that's how I convinced myself.

So the logic here follows the (visual) intuition how s64 and u64 (and
also u32 and s32) correlate. That's how I saw it. TBH, the above
mathematical way seems scary and not so straightforward to follow, so
I'm hesitant to add it to comments to not scare anyone away :)

I did try to visually represent it, but I'm not creative enough ASCII
artist to pull this off, apparently. I'll just leave it as it is for
now.

>
> > ---
> >  kernel/bpf/verifier.c | 23 +++++++++++++++++++++++
> >  1 file changed, 23 insertions(+)
> >
> > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > index 5082ca1ea5dc..38d21d0e46bd 100644
> > --- a/kernel/bpf/verifier.c
> > +++ b/kernel/bpf/verifier.c
> > @@ -2369,6 +2369,29 @@ static void __reg32_deduce_bounds(struct bpf_reg_state *reg)
> >                       reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
> >               }
> >       }
> > +     /* Special case where upper bits form a small sequence of two
> > +      * sequential numbers (in 32-bit unsigned space, so 0xffffffff to
> > +      * 0x00000000 is also valid), while lower bits form a proper s32 range
> > +      * going from negative numbers to positive numbers. E.g., let's say we
> > +      * have s64 range [-1, 1] ([0xffffffffffffffff, 0x0000000000000001]).
> > +      * Possible s64 values are {-1, 0, 1} ({0xffffffffffffffff,
> > +      * 0x0000000000000000, 0x00000000000001}). Ignoring upper 32 bits,
> > +      * we still get a valid s32 range [-1, 1] ([0xffffffff, 0x00000001]).
> > +      * Note that it doesn't have to be 0xffffffff going to 0x00000000 in
> > +      * upper 32 bits. As a random example, s64 range
> > +      * [0xfffffff0ffffff00; 0xfffffff100000010], forms a valid s32 range
> > +      * [-16, 16] ([0xffffff00; 0x00000010]) in its 32 bit subregister.
> > +      */
> > +     if ((u32)(reg->umin_value >> 32) + 1 == (u32)(reg->umax_value >> 32) &&
> > +         (s32)reg->umin_value < 0 && (s32)reg->umax_value >= 0) {
> > +             reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->umin_value);
> > +             reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->umax_value);
> > +     }
> > +     if ((u32)(reg->smin_value >> 32) + 1 == (u32)(reg->smax_value >> 32) &&
> > +         (s32)reg->smin_value < 0 && (s32)reg->smax_value >= 0) {
> > +             reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->smin_value);
> > +             reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
> > +     }
> >       /* if u32 range forms a valid s32 range (due to matching sign bit),
> >        * try to learn from that
> >        */
>
>
>

Alexei Starovoitov Oct. 31, 2023, 6:41 p.m. UTC | #3

On Tue, Oct 31, 2023 at 10:39 AM Andrii Nakryiko
<[e-mail]> wrote:
> > fwiw, an alternative explanation might be arithmetic based.
> > Suppose:
> > . there are numbers a, b, c
> > . 2**31 <= b < 2**32
> > . 0 <= c < 2**31
> > . umin = 2**32 * a + b
> > . umax = 2**32 * (a + 1) + c
> >
> > The number of values in the range represented by [umin; umax] is:
> > . N = umax - umin + 1 = 2**32 + c - b + 1
> > . min(N) = 2**32 + 0 - (2**32-1) + 1 = 2
> > . max(N) = 2**32 + (2**31 - 1) - 2**31 + 1 = 2**32
> > Hence [(s32)b; (s32)c] form a valid range.
> >
> > At-least that's how I convinced myself.
>
> So the logic here follows the (visual) intuition how s64 and u64 (and
> also u32 and s32) correlate. That's how I saw it. TBH, the above
> mathematical way seems scary and not so straightforward to follow, so
> I'm hesitant to add it to comments to not scare anyone away :)

Actually Ed's math carried me across the line.
Could you add it to the commit log at least?

> I did try to visually represent it, but I'm not creative enough ASCII
> artist to pull this off, apparently. I'll just leave it as it is for
> now.

Your comment is also good, keep it as-is,
but it's harder to see that it's correct without the math part.

> > > +      * upper 32 bits. As a random example, s64 range
> > > +      * [0xfffffff0ffffff00; 0xfffffff100000010], forms a valid s32 range
> > > +      * [-16, 16] ([0xffffff00; 0x00000010]) in its 32 bit subregister.
> > > +      */

typo. It's [-256, 16]

Andrii Nakryiko Oct. 31, 2023, 6:49 p.m. UTC | #4

On Tue, Oct 31, 2023 at 11:41 AM Alexei Starovoitov
<[e-mail]> wrote:
>
> On Tue, Oct 31, 2023 at 10:39 AM Andrii Nakryiko
> <[e-mail]> wrote:
> > > fwiw, an alternative explanation might be arithmetic based.
> > > Suppose:
> > > . there are numbers a, b, c
> > > . 2**31 <= b < 2**32
> > > . 0 <= c < 2**31
> > > . umin = 2**32 * a + b
> > > . umax = 2**32 * (a + 1) + c
> > >
> > > The number of values in the range represented by [umin; umax] is:
> > > . N = umax - umin + 1 = 2**32 + c - b + 1
> > > . min(N) = 2**32 + 0 - (2**32-1) + 1 = 2
> > > . max(N) = 2**32 + (2**31 - 1) - 2**31 + 1 = 2**32
> > > Hence [(s32)b; (s32)c] form a valid range.
> > >
> > > At-least that's how I convinced myself.
> >
> > So the logic here follows the (visual) intuition how s64 and u64 (and
> > also u32 and s32) correlate. That's how I saw it. TBH, the above
> > mathematical way seems scary and not so straightforward to follow, so
> > I'm hesitant to add it to comments to not scare anyone away :)
>
> Actually Ed's math carried me across the line.
> Could you add it to the commit log at least?

Sure, whatever it takes :) Will add to the commit message.

>
> > I did try to visually represent it, but I'm not creative enough ASCII
> > artist to pull this off, apparently. I'll just leave it as it is for
> > now.
>
> Your comment is also good, keep it as-is,
> but it's harder to see that it's correct without the math part.
>
> > > > +      * upper 32 bits. As a random example, s64 range
> > > > +      * [0xfffffff0ffffff00; 0xfffffff100000010], forms a valid s32 range
> > > > +      * [-16, 16] ([0xffffff00; 0x00000010]) in its 32 bit subregister.
> > > > +      */
>
> typo. It's [-256, 16]

I think I wanted to have 0xfffffff0 (one more f) for [-16, 16], but I
can also leave asymmetrical bounds [-256, 16]

Patch

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 5082ca1ea5dc..38d21d0e46bd 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2369,6 +2369,29 @@  static void __reg32_deduce_bounds(struct bpf_reg_state *reg)
 			reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
 		}
 	}
+	/* Special case where upper bits form a small sequence of two
+	 * sequential numbers (in 32-bit unsigned space, so 0xffffffff to
+	 * 0x00000000 is also valid), while lower bits form a proper s32 range
+	 * going from negative numbers to positive numbers. E.g., let's say we
+	 * have s64 range [-1, 1] ([0xffffffffffffffff, 0x0000000000000001]).
+	 * Possible s64 values are {-1, 0, 1} ({0xffffffffffffffff,
+	 * 0x0000000000000000, 0x00000000000001}). Ignoring upper 32 bits,
+	 * we still get a valid s32 range [-1, 1] ([0xffffffff, 0x00000001]).
+	 * Note that it doesn't have to be 0xffffffff going to 0x00000000 in
+	 * upper 32 bits. As a random example, s64 range
+	 * [0xfffffff0ffffff00; 0xfffffff100000010], forms a valid s32 range
+	 * [-16, 16] ([0xffffff00; 0x00000010]) in its 32 bit subregister.
+	 */
+	if ((u32)(reg->umin_value >> 32) + 1 == (u32)(reg->umax_value >> 32) &&
+	    (s32)reg->umin_value < 0 && (s32)reg->umax_value >= 0) {
+		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->umin_value);
+		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->umax_value);
+	}
+	if ((u32)(reg->smin_value >> 32) + 1 == (u32)(reg->smax_value >> 32) &&
+	    (s32)reg->smin_value < 0 && (s32)reg->smax_value >= 0) {
+		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->smin_value);
+		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
+	}
 	/* if u32 range forms a valid s32 range (due to matching sign bit),
 	 * try to learn from that
 	 */