diff mbox series

[bpf-next,v2,5/9] bpf, verifier: improve signed ranges inference for BPF_AND

Message ID 20240719110059.797546-6-xukuohai@huaweicloud.com (mailing list archive)
State Changes Requested
Delegated to: BPF
Headers show
Series Add BPF LSM return value range check, BPF part | expand

Checks

Context Check Description
netdev/series_format success Posting correctly formatted
netdev/tree_selection success Clearly marked for bpf-next, async
netdev/ynl success Generated files up to date; no warnings/errors; no diff in generated;
netdev/fixes_present success Fixes tag not required for -next series
netdev/header_inline success No static functions without inline keyword in header files
netdev/build_32bit success Errors and warnings before: 661 this patch: 661
netdev/build_tools success No tools touched, skip
netdev/cc_maintainers warning 11 maintainers not CCed: haoluo@google.com nathan@kernel.org llvm@lists.linux.dev justinstitt@google.com john.fastabend@gmail.com jolsa@kernel.org martin.lau@linux.dev song@kernel.org morbo@google.com ndesaulniers@google.com sdf@fomichev.me
netdev/build_clang success Errors and warnings before: 662 this patch: 662
netdev/verify_signedoff success Signed-off-by tag matches author and committer
netdev/deprecated_api success None detected
netdev/check_selftest success No net selftest shell script
netdev/verify_fixes success No Fixes tag
netdev/build_allmodconfig_warn success Errors and warnings before: 672 this patch: 672
netdev/checkpatch warning WARNING: line length of 81 exceeds 80 columns WARNING: line length of 83 exceeds 80 columns WARNING: line length of 85 exceeds 80 columns
netdev/build_clang_rust success No Rust files in patch. Skipping build
netdev/kdoc success Errors and warnings before: 0 this patch: 0
netdev/source_inline fail Was 0 now: 2
bpf/vmtest-bpf-next-VM_Test-5 success Logs for aarch64-gcc / build-release
bpf/vmtest-bpf-next-VM_Test-3 success Logs for Validate matrix.py
bpf/vmtest-bpf-next-VM_Test-1 success Logs for ShellCheck
bpf/vmtest-bpf-next-VM_Test-0 success Logs for Lint
bpf/vmtest-bpf-next-VM_Test-2 success Logs for Unittests
bpf/vmtest-bpf-next-VM_Test-10 success Logs for aarch64-gcc / veristat
bpf/vmtest-bpf-next-VM_Test-12 success Logs for s390x-gcc / build-release
bpf/vmtest-bpf-next-VM_Test-8 fail Logs for aarch64-gcc / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-4 success Logs for aarch64-gcc / build / build for aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-9 success Logs for aarch64-gcc / test (test_verifier, false, 360) / test_verifier on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-11 success Logs for s390x-gcc / build / build for s390x with gcc
bpf/vmtest-bpf-next-VM_Test-7 success Logs for aarch64-gcc / test (test_progs, false, 360) / test_progs on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-6 success Logs for aarch64-gcc / test (test_maps, false, 360) / test_maps on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-13 success Logs for s390x-gcc / test (test_maps, false, 360) / test_maps on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-16 success Logs for s390x-gcc / test (test_verifier, false, 360) / test_verifier on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-17 success Logs for s390x-gcc / veristat
bpf/vmtest-bpf-next-VM_Test-18 success Logs for set-matrix
bpf/vmtest-bpf-next-VM_Test-19 success Logs for x86_64-gcc / build / build for x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-20 success Logs for x86_64-gcc / build-release
bpf/vmtest-bpf-next-VM_Test-28 success Logs for x86_64-llvm-17 / build / build for x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-29 success Logs for x86_64-llvm-17 / build-release / build for x86_64 with llvm-17-O2
bpf/vmtest-bpf-next-VM_Test-34 success Logs for x86_64-llvm-17 / veristat
bpf/vmtest-bpf-next-VM_Test-35 success Logs for x86_64-llvm-18 / build / build for x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-36 success Logs for x86_64-llvm-18 / build-release / build for x86_64 with llvm-18-O2
bpf/vmtest-bpf-next-VM_Test-42 success Logs for x86_64-llvm-18 / veristat
bpf/vmtest-bpf-next-VM_Test-14 success Logs for s390x-gcc / test (test_progs, false, 360) / test_progs on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-15 success Logs for s390x-gcc / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-26 success Logs for x86_64-gcc / test (test_verifier, false, 360) / test_verifier on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-41 success Logs for x86_64-llvm-18 / test (test_verifier, false, 360) / test_verifier on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-21 success Logs for x86_64-gcc / test (test_maps, false, 360) / test_maps on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-22 success Logs for x86_64-gcc / test (test_progs, false, 360) / test_progs on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-23 success Logs for x86_64-gcc / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-24 success Logs for x86_64-gcc / test (test_progs_no_alu32_parallel, true, 30) / test_progs_no_alu32_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-25 success Logs for x86_64-gcc / test (test_progs_parallel, true, 30) / test_progs_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-27 success Logs for x86_64-gcc / veristat / veristat on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-33 success Logs for x86_64-llvm-17 / test (test_verifier, false, 360) / test_verifier on x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-37 success Logs for x86_64-llvm-18 / test (test_maps, false, 360) / test_maps on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-38 success Logs for x86_64-llvm-18 / test (test_progs, false, 360) / test_progs on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-39 success Logs for x86_64-llvm-18 / test (test_progs_cpuv4, false, 360) / test_progs_cpuv4 on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-40 success Logs for x86_64-llvm-18 / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on x86_64 with llvm-18
bpf/vmtest-bpf-next-PR fail PR summary
bpf/vmtest-bpf-next-VM_Test-30 success Logs for x86_64-llvm-17 / test (test_maps, false, 360) / test_maps on x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-31 success Logs for x86_64-llvm-17 / test (test_progs, false, 360) / test_progs on x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-32 success Logs for x86_64-llvm-17 / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on x86_64 with llvm-17

Commit Message

Xu Kuohai July 19, 2024, 11 a.m. UTC 
From: Shung-Hsi Yu <shung-hsi.yu@suse.com>

This commit improve BPF verifier's inference of signed ranges by learning new
signed ranges directly from signed ranges of the operands by doing

    dst_reg->smin_value = negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value))
    dst_reg->smax_value = max(dst_reg->smax_value, src_reg->smax_value)

See below for th complete explanation. The improvement is needed to prevent
verifier rejection of BPF program like the one presented by Xu Kuohai:

    SEC("lsm/bpf_map")
    int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode)
    {
         if (map != (struct bpf_map *)&data_input)
    	    return 0;

    	 if (fmode & FMODE_WRITE)
    	    return -EACCES;

         return 0;
    }

Where the relevant verifer log upon rejection are:

    ...
    5: (79) r0 = *(u64 *)(r1 +8)          ; R0_w=scalar() R1=ctx()
    ; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32
    6: (67) r0 <<= 62                     ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000))
    7: (c7) r0 s>>= 63                    ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
    ;  @ test_libbpf_get_fd_by_id_opts.c:0
    8: (57) r0 &= -13                     ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
    9: (95) exit

This sequence of instructions comes from Clang's transformation located in
DAGCombiner::SimplifySelectCC() method, which combined the "fmode &
FMODE_WRITE" check with the return statement without needing BPF_JMP at all.
See Eduard's comment for more detail of this transformation[0].

While the verifier can correctly infer that the value of r0 is in a tight [-1,
0] range after instruction "r0 s>>= 63", is was not able to come up with a
tight range for "r0 &= -13" (which would be [-13, 0]), and instead inferred a
very loose range:

    r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
    r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))

The reason is that scalar*_min_max_add() mainly relies on tnum for inferring
bounds in register after BPF_AND, however [-1, 0] cannot be tracked precisely
with tnum, and was effectively turns into [0, -1] (i.e. tnum_unknown). So upon
BPF_AND the resulting tnum is equivalent to

    dst_reg->var_off = tnum_and(tnum_unknown, tnum_const(-13))

And from there the BPF verifier was only able to infer smin=S64_MIN and
smax=0x7ffffffffffffff3, which is outside of the expected [-4095, 0] range for
return values, and thus the program was rejected.

To allow verification of such instruction pattern, update scalar*_min_max_and()
to infer signed ranges directly from signed ranges of the operands.

For BPF_AND, the resulting value always gains more unset '0' bit, thus it only
move towards 0x0000000000000000. The difficulty lies with how to deal with
signs. While non-negative (positive and zero) value simply grows smaller, a
negative number can grows smaller, but may also "underflow" and become a larger
value.

To better address this situation we split the signed ranges into negative range
and non-negative range cases, ignoring the mixed sign cases for now; and only
consider how to calculate smax_value.

Since negative range & negative range preserve the sign bit, so we know the
result is still a negative value, thus it only move towards S64_MIN, but never
underflow, thus a save bet is to use a value in ranges that is closet to 0,
thus "max(dst_reg->smax_value, src->smax_value)". For negative range & positive
range the sign bit is always cleared, thus we know the resulting value is
non-negative, and only moves towards 0, so a safe bet is to use smax_value of
the non-negative range. Last but not least, non-negative range & non-negative
range is still a non-negative value, and only moves towards 0; however same as
the unsigned range case, the maximum is actually capped by the lesser of the
two, and thus min(dst_reg->smax_value, src_reg->smax_value);

Listing out the above reasoning as a table (dst_reg abbreviated as dst, src_reg
abbreviated as src, smax_value abbrivated as smax) we get:

                        |                         src_reg
       smax = ?         +---------------------------+---------------------------
                        |        negative           |       non-negative
---------+--------------+---------------------------+---------------------------
         | negative     | max(dst->smax, src->smax) |         src->smax
dst_reg  +--------------+---------------------------+---------------------------
         | non-negative |         dst->smax         | min(dst->smax, src->smax)

However this is quite complicated, and could use some simplification given the
following observations:

    max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value
    max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value
    max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value)

So we could substitute the cells in the table above all with max(...), and
arrive at:

                        |                         src_reg
      smax' = ?         +---------------------------+---------------------------
  smax'(r) >= smax(r)   |        negative           |       non-negative
---------+--------------+---------------------------+---------------------------
         | negative     | max(dst->smax, src->smax) | max(dst->smax, src->smax)
dst_reg  +--------------+---------------------------+---------------------------
         | non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)

Meaning that simply using

    max(dst_reg->smax_value, src_reg->smax_value)

to calculate the resulting smax_value would work across all sign combinations.

For smin_value, we know that both non-negative range & non-negative range and
negative range & non-negative range both result in a non-negative value, so an
easy guess is to use the minimum value in non-negative range, thus 0.

                        |                         src_reg
       smin = ?         +----------------------------+---------------------------
                        |          negative          |       non-negative
---------+--------------+----------------------------+---------------------------
         | negative     |             ?              |             0
dst_reg  +--------------+----------------------------+---------------------------
         | non-negative |             0              |             0

That leaves the negative range & negative range case to be considered. We know
that negative range & negative range always yield a negative value, so a
preliminary guess would be S64_MIN. However, that guess is too imprecise to
help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern we're trying to deal
with here.

Further improvement comes with the observation that for negative range &
negative range, the smallest possible value must be one that has longest
_common_ most-significant set '1' bits sequence, thus we can use
min(dst_reg->smin_value, src->smin_value) as the starting point, as the smaller
value will be the one with the shorter most-significant set '1' bits sequence.
But that alone is not enough, as we do not know whether rest of the bits would
be set, so the safest guess would be one that clear alls bits after the
most-significant set '1' bits sequence, something akin to bit_floor(), but for
rounding to a negative power-of-2 instead.

    negative_bit_floor(0xffff000000000003) == 0xffff000000000000
    negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000
    negative_bit_floor(0xffffffffffffffff) == 0xffffffffffffffff /* -1 remains unchanged */
    negative_bit_floor(0x0000fb0000000000) == 0x0000000000000000 /* non-negative values became 0 */

With negative range & negative range solve, we now have:

                        |                         src_reg
       smin = ?         +----------------------------+---------------------------
                        |        negative            |       non-negative
---------+--------------+----------------------------+---------------------------
         |   negative   |negative_bit_floor(         |             0
         |              |  min(dst->smin, src->smin))|
dst_reg  +--------------+----------------------------+---------------------------
         | non-negative |           0                |             0

This can be also simplified with some observations (quadrants refers to the
cells in above table, number start from top-right cell -- I, and goes
counter-clockwise):

  A. min(dst_reg->smin_value, src_reg->smin_value) < 0  /* dst negative & src non-negative, quadrant I */
  B. min(dst_reg->smin_value, src_reg->smin_value) < 0  /* dst non-negative & src negative, quadrant III */
  C. min(dst_reg->smin_value, src_reg->smin_value) >= 0 /* dst non-negative & src non-negative, quadrant IV */

  D. negative_bit_floor(x) s<= x /* for any x, negative_bit_floor(x) is always smaller (or equal to the original value) */
  E. negative_bit_floor(y) == 0  /* when y is non-negative, i.e. y >= 0, since the most-significant is unset, so every bit is unset */

Thus we can derive

    negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)) < 0  /* combine A and D, where dst negative & src non-negative */
    negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)) < 0  /* combine B and D, where dst non-negative & src negative */
	negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)) == 0 /* combine C and E, where dst non-negative & src non-negative */

Substitute quadrants I, III, and IV cells in the table above all with
negative_bit_floor(min(...)), we arrive at:

                        |                         src_reg
       smin' = ?        +----------------------------+---------------------------
  smin'(r) <= smin(r)   |        negative            |       non-negative
---------+--------------+----------------------------+---------------------------
         |   negative   |negative_bit_floor(         |negative_bit_floor(
         |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
dst_reg  +--------------+----------------------------+---------------------------
         | non-negative |negative_bit_floor(         |negative_bit_floor(
         |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))

Meaning that simply using

    negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value))

to calculate the resulting smin_value would work across all sign combinations.

Together these allows the BPF verifier to infer the signed range of the
result of BPF_AND operation using the signed range from its operands,
and use that information

    r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
    r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))

[0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/

Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/
Cc: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Acked-by: Xu Kuohai <xukuohai@huawei.com>
---
 kernel/bpf/verifier.c | 63 +++++++++++++++++++++++++++++--------------
 1 file changed, 43 insertions(+), 20 deletions(-)

Comments

Eduard Zingerman July 22, 2024, 7:13 a.m. UTC | #1 
On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote:
> From: Shung-Hsi Yu <shung-hsi.yu@suse.com>

[...]

> 
>                         |                         src_reg
>        smin' = ?        +----------------------------+---------------------------
>   smin'(r) <= smin(r)   |        negative            |       non-negative
> ---------+--------------+----------------------------+---------------------------
>          |   negative   |negative_bit_floor(         |negative_bit_floor(
>          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> dst_reg  +--------------+----------------------------+---------------------------
>          | non-negative |negative_bit_floor(         |negative_bit_floor(
>          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> 
> Meaning that simply using
> 
>     negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value))
> 
> to calculate the resulting smin_value would work across all sign combinations.
> 
> Together these allows the BPF verifier to infer the signed range of the
> result of BPF_AND operation using the signed range from its operands,
> and use that information
> 
>     r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
>     r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
> 
> [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
> 
> Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/
> Cc: Eduard Zingerman <eddyz87@gmail.com>
> Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> Acked-by: Xu Kuohai <xukuohai@huawei.com>
> ---

I find derivation of these new rules logical.
Also tried a simple brute force testing of this algorithm for 6-bit
signed integers, and have not found any constraint violations:
https://github.com/eddyz87/bpf-and-brute-force-check

As a nitpick, I think that it would be good to have some shortened
version of the derivation in the comments alongside the code.
(Maybe with a link to the mailing list).

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]
Shung-Hsi Yu July 22, 2024, 12:57 p.m. UTC | #2 
On Mon, Jul 22, 2024 at 12:13:20AM GMT, Eduard Zingerman wrote:
> On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote:
> > From: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> 
> [...]
> 
> > 
> >                         |                         src_reg
> >        smin' = ?        +----------------------------+---------------------------
> >   smin'(r) <= smin(r)   |        negative            |       non-negative
> > ---------+--------------+----------------------------+---------------------------
> >          |   negative   |negative_bit_floor(         |negative_bit_floor(
> >          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> > dst_reg  +--------------+----------------------------+---------------------------
> >          | non-negative |negative_bit_floor(         |negative_bit_floor(
> >          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> > 
> > Meaning that simply using
> > 
> >     negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value))
> > 
> > to calculate the resulting smin_value would work across all sign combinations.
> > 
> > Together these allows the BPF verifier to infer the signed range of the
> > result of BPF_AND operation using the signed range from its operands,
> > and use that information

I accidentally left the above paragraph unfinished, it should end with

... and using that information, it can be sure that that the result of
[-1, 0] & -13 will be within that expected range of [-4095, 0].

> >     r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
> >     r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
> > 
> > [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
> > 
> > Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/
> > Cc: Eduard Zingerman <eddyz87@gmail.com>
> > Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> > Acked-by: Xu Kuohai <xukuohai@huawei.com>
> > ---
> 
> I find derivation of these new rules logical.
> Also tried a simple brute force testing of this algorithm for 6-bit
> signed integers, and have not found any constraint violations:
> https://github.com/eddyz87/bpf-and-brute-force-check

Thanks!

> As a nitpick, I think that it would be good to have some shortened
> version of the derivation in the comments alongside the code.

Agree it would. Will try to add a 2-4 sentence explanation.

> (Maybe with a link to the mailing list).

Adding a link to the mailing list seems out of the usual for comment in
verifier.c though, and it would be quite long. That said, it would be
nice to hint that there exists a more verbose version of the
explanation.

Maybe an explicit "see commit for the full detail" at the end of
the added comment?

> Acked-by: Eduard Zingerman <eddyz87@gmail.com>
> 
> [...]

Will send an update for this tomorrow.
Eduard Zingerman July 22, 2024, 6:47 p.m. UTC | #3 
On Mon, 2024-07-22 at 20:57 +0800, Shung-Hsi Yu wrote:

[...]

> > As a nitpick, I think that it would be good to have some shortened
> > version of the derivation in the comments alongside the code.
> 
> Agree it would. Will try to add a 2-4 sentence explanation.
> 
> > (Maybe with a link to the mailing list).
> 
> Adding a link to the mailing list seems out of the usual for comment in
> verifier.c though, and it would be quite long. That said, it would be
> nice to hint that there exists a more verbose version of the
> explanation.
> 
> Maybe an explicit "see commit for the full detail" at the end of
> the added comment?

Tbh, I find bounds deduction code extremely confusing.
Imho, having lengthy comments there is a good thing.
Alexei Starovoitov July 23, 2024, 12:48 a.m. UTC | #4 
On Mon, Jul 22, 2024 at 11:48 AM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Mon, 2024-07-22 at 20:57 +0800, Shung-Hsi Yu wrote:
>
> [...]
>
> > > As a nitpick, I think that it would be good to have some shortened
> > > version of the derivation in the comments alongside the code.
> >
> > Agree it would. Will try to add a 2-4 sentence explanation.
> >
> > > (Maybe with a link to the mailing list).
> >
> > Adding a link to the mailing list seems out of the usual for comment in
> > verifier.c though, and it would be quite long. That said, it would be
> > nice to hint that there exists a more verbose version of the
> > explanation.
> >
> > Maybe an explicit "see commit for the full detail" at the end of
> > the added comment?
>
> Tbh, I find bounds deduction code extremely confusing.
> Imho, having lengthy comments there is a good thing.

+1
Pls document the logic in the code.
commit log is good, but good chunk of it probably should be copied
as a comment.

I've applied the rest of the patches and removed 'test 3' selftest.
Pls respin this patch and a test.
More than one test would be nice too.
Shung-Hsi Yu July 23, 2024, 6:36 a.m. UTC | #5 
On Mon, Jul 22, 2024 at 05:48:22PM GMT, Alexei Starovoitov wrote:
> On Mon, Jul 22, 2024 at 11:48 AM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > On Mon, 2024-07-22 at 20:57 +0800, Shung-Hsi Yu wrote:
> >
> > [...]
> >
> > > > As a nitpick, I think that it would be good to have some shortened
> > > > version of the derivation in the comments alongside the code.
> > >
> > > Agree it would. Will try to add a 2-4 sentence explanation.
> > >
> > > > (Maybe with a link to the mailing list).
> > >
> > > Adding a link to the mailing list seems out of the usual for comment in
> > > verifier.c though, and it would be quite long. That said, it would be
> > > nice to hint that there exists a more verbose version of the
> > > explanation.
> > >
> > > Maybe an explicit "see commit for the full detail" at the end of
> > > the added comment?
> >
> > Tbh, I find bounds deduction code extremely confusing.
> > Imho, having lengthy comments there is a good thing.
> 
> +1
> Pls document the logic in the code.
> commit log is good, but good chunk of it probably should be copied
> as a comment.
> 
> I've applied the rest of the patches and removed 'test 3' selftest.
> Pls respin this patch and a test.
> More than one test would be nice too.

Ack. Will send send another series that:

1. update current patch
  - add code comment explanation how signed ranges are deduced in
    scalar*_min_max_and()
  - revert 229d6db14942 "selftests/bpf: Workaround strict bpf_lsm return
    value check."
2. reintroduce Xu Kuohai's "test 3" into verifier_lsm.c
3. add a few tests for BPF_AND's signed range deduction
   - should it be added to verifier_bounds*.c or verifier_and.c?

     I think former, because if we later add signed range deduction for
     BPF_OR as well, then test for signed range deducation of both
     BPF_AND and BPF_OR can live in the same file, which would be nice
     as signed range deduction of the two are somewhat symmetric
Shung-Hsi Yu July 23, 2024, 7:07 a.m. UTC | #6 
On Tue, Jul 23, 2024 at 02:36:18PM GMT, Shung-Hsi Yu wrote:
[...]
> > +1
> > Pls document the logic in the code.
> > commit log is good, but good chunk of it probably should be copied
> > as a comment.
> > 
> > I've applied the rest of the patches and removed 'test 3' selftest.
> > Pls respin this patch and a test.
> > More than one test would be nice too.
> 
> Ack. Will send send another series that:
> 
> 1. update current patch
>   - add code comment explanation how signed ranges are deduced in
>     scalar*_min_max_and()
>   - revert 229d6db14942 "selftests/bpf: Workaround strict bpf_lsm return
>     value check."
> 2. reintroduce Xu Kuohai's "test 3" into verifier_lsm.c
> 3. add a few tests for BPF_AND's signed range deduction
>    - should it be added to verifier_bounds*.c or verifier_and.c?
> 
>      I think former, because if we later add signed range deduction for
>      BPF_OR as well...

I was curious whether there would be imminent need for signed range
deduction for BPF_OR, though looks like there is _not_.

Looking at DAGCombiner::SimplifySelectCC() it does not do the
bitwise-OR variant of what we've encountered[1,2], that is

    fold (select_cc seteq (and x, y), 0, A, -1) -> (or (sra (shl x)) A)

In other words, transforming the following theoretial C code that
returns -EACCES when certain bit is unset, and -1 when certain bit is
set

    if (fmode & FMODE_WRITE)
        return -1;
    
    return -EACCESS;

into the following instructions

    r0  <<= 62
    r0 s>>= 63 /* set => r0 = -1, unset => r0 = 0 */
    r0  |= -13 /* set => r0 = (-1 | -13) = -1, unset => r0 = (0 | -13) = -13 = -EACCESS */
	exit       /* returns either -1 or -EACCESS */

So signed ranged deduction with BPF_OR is probably just a nice-to-have
for now.

1: https://github.com/llvm/llvm-project/blob/2b78303/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L27657-L27684
2: neither was the setne version transformed, i.e.
   fold (select_cc setne (and x, y), 0, A, 0) -> (and (sra (shl x)) A)
   
>      then test for signed range deducation of both
>      BPF_AND and BPF_OR can live in the same file, which would be nice
>      as signed range deduction of the two are somewhat symmetric
Alexei Starovoitov July 24, 2024, 1:17 a.m. UTC | #7 
On Tue, Jul 23, 2024 at 12:07 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>
> On Tue, Jul 23, 2024 at 02:36:18PM GMT, Shung-Hsi Yu wrote:
> [...]
> > > +1
> > > Pls document the logic in the code.
> > > commit log is good, but good chunk of it probably should be copied
> > > as a comment.
> > >
> > > I've applied the rest of the patches and removed 'test 3' selftest.
> > > Pls respin this patch and a test.
> > > More than one test would be nice too.
> >
> > Ack. Will send send another series that:
> >
> > 1. update current patch
> >   - add code comment explanation how signed ranges are deduced in
> >     scalar*_min_max_and()
> >   - revert 229d6db14942 "selftests/bpf: Workaround strict bpf_lsm return
> >     value check."
> > 2. reintroduce Xu Kuohai's "test 3" into verifier_lsm.c
> > 3. add a few tests for BPF_AND's signed range deduction
> >    - should it be added to verifier_bounds*.c or verifier_and.c?
> >
> >      I think former, because if we later add signed range deduction for
> >      BPF_OR as well...
>
> I was curious whether there would be imminent need for signed range
> deduction for BPF_OR, though looks like there is _not_.
>
> Looking at DAGCombiner::SimplifySelectCC() it does not do the
> bitwise-OR variant of what we've encountered[1,2], that is
>
>     fold (select_cc seteq (and x, y), 0, A, -1) -> (or (sra (shl x)) A)
>
> In other words, transforming the following theoretial C code that
> returns -EACCES when certain bit is unset, and -1 when certain bit is
> set
>
>     if (fmode & FMODE_WRITE)
>         return -1;
>
>     return -EACCESS;
>
> into the following instructions
>
>     r0  <<= 62
>     r0 s>>= 63 /* set => r0 = -1, unset => r0 = 0 */
>     r0  |= -13 /* set => r0 = (-1 | -13) = -1, unset => r0 = (0 | -13) = -13 = -EACCESS */
>         exit       /* returns either -1 or -EACCESS */
>
> So signed ranged deduction with BPF_OR is probably just a nice-to-have
> for now.

Yeah. Let's not complicate the verifier until really necessary.

But I wonder whether we should override shouldFoldSelectWithSingleBitTest()
in the backend to suppress this optimization.
I guess not, since removal of a branch is a good thing.
diff mbox series

Patch

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 78104bd85274..d3f3a464a871 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -13511,6 +13511,40 @@  static void scalar_min_max_mul(struct bpf_reg_state *dst_reg,
 	}
 }
 
+/* Clears all trailing bits after the most significant unset bit.
+ *
+ * Used for estimating the minimum possible value after BPF_AND. This
+ * effectively rounds a negative value down to a negative power-of-2 value
+ * (except for -1, which just return -1) and returning 0 for non-negative
+ * values. E.g. negative32_bit_floor(0xff0ff0ff) == 0xff000000.
+ */
+static inline s32 negative32_bit_floor(s32 v)
+{
+	u8 bits = fls(~v); /* find most-significant unset bit */
+	u32 delta;
+
+	/* special case, needed because 1UL << 32 is undefined */
+	if (bits > 31)
+		return 0;
+
+	delta = (1UL << bits) - 1;
+	return ~delta;
+}
+
+/* Same as negative32_bit_floor() above, but for 64-bit signed value */
+static inline s64 negative_bit_floor(s64 v)
+{
+	u8 bits = fls64(~v); /* find most-significant unset bit */
+	u64 delta;
+
+	/* special case, needed because 1ULL << 64 is undefined */
+	if (bits > 63)
+		return 0;
+
+	delta = (1ULL << bits) - 1;
+	return ~delta;
+}
+
 static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
 				 struct bpf_reg_state *src_reg)
 {
@@ -13530,16 +13564,10 @@  static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
 	dst_reg->u32_min_value = var32_off.value;
 	dst_reg->u32_max_value = min(dst_reg->u32_max_value, umax_val);
 
-	/* Safe to set s32 bounds by casting u32 result into s32 when u32
-	 * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded.
-	 */
-	if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
-		dst_reg->s32_min_value = dst_reg->u32_min_value;
-		dst_reg->s32_max_value = dst_reg->u32_max_value;
-	} else {
-		dst_reg->s32_min_value = S32_MIN;
-		dst_reg->s32_max_value = S32_MAX;
-	}
+	/* Handle the [-1, 0] & -CONSTANT case that's difficult for tnum */
+	dst_reg->s32_min_value = negative32_bit_floor(min(dst_reg->s32_min_value,
+							  src_reg->s32_min_value));
+	dst_reg->s32_max_value = max(dst_reg->s32_max_value, src_reg->s32_max_value);
 }
 
 static void scalar_min_max_and(struct bpf_reg_state *dst_reg,
@@ -13560,16 +13588,11 @@  static void scalar_min_max_and(struct bpf_reg_state *dst_reg,
 	dst_reg->umin_value = dst_reg->var_off.value;
 	dst_reg->umax_value = min(dst_reg->umax_value, umax_val);
 
-	/* Safe to set s64 bounds by casting u64 result into s64 when u64
-	 * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded.
-	 */
-	if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
-		dst_reg->smin_value = dst_reg->umin_value;
-		dst_reg->smax_value = dst_reg->umax_value;
-	} else {
-		dst_reg->smin_value = S64_MIN;
-		dst_reg->smax_value = S64_MAX;
-	}
+	/* Handle the [-1, 0] & -CONSTANT case that's difficult for tnum */
+	dst_reg->smin_value = negative_bit_floor(min(dst_reg->smin_value,
+						     src_reg->smin_value));
+	dst_reg->smax_value = max(dst_reg->smax_value, src_reg->smax_value);
+
 	/* We may learn something more from the var_off */
 	__update_reg_bounds(dst_reg);
 }