Re: [PATCH bpf-next v3 07/11] bpf: Fix a false rejection caused by AND operation

[Xu Kuohai <xukuohai@huaweicloud.com>]

On 4/25/2024 6:06 AM, Yonghong Song wrote:
> 
> On 4/23/24 7:25 PM, Xu Kuohai wrote:
>> On 4/24/2024 5:55 AM, Yonghong Song wrote:
>>>
>>> On 4/20/24 1:33 AM, Xu Kuohai wrote:
>>>> On 4/20/2024 7:00 AM, Eduard Zingerman wrote:
>>>>> On Thu, 2024-04-11 at 20:27 +0800, Xu Kuohai wrote:
>>>>>> From: Xu Kuohai <xukuohai@huawei.com>
>>>>>>
>>>>>> With lsm return value check, the no-alu32 version test_libbpf_get_fd_by_id_opts
>>>>>> is rejected by the verifier, and the log says:
>>>>>>
>>>>>>    0: R1=ctx() R10=fp0
>>>>>>    ; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
>>>>>>    0: (b7) r0 = 0                        ; R0_w=0
>>>>>>    1: (79) r2 = *(u64 *)(r1 +0)
>>>>>>    func 'bpf_lsm_bpf_map' arg0 has btf_id 916 type STRUCT 'bpf_map'
>>>>>>    2: R1=ctx() R2_w=trusted_ptr_bpf_map()
>>>>>>    ; if (map != (struct bpf_map *)&data_input) @ test_libbpf_get_fd_by_id_opts.c:29
>>>>>>    2: (18) r3 = 0xffff9742c0951a00       ; R3_w=map_ptr(map=data_input,ks=4,vs=4)
>>>>>>    4: (5d) if r2 != r3 goto pc+4         ; R2_w=trusted_ptr_bpf_map() R3_w=map_ptr(map=data_input,ks=4,vs=4)
>>>>>>    ; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
>>>>>>    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))
>>>>>>    ; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
>>>>>>    9: (95) exit
>>>>>>
>>>>>> And here is the C code of the prog.
>>>>>>
>>>>>> 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;
>>>>>> }
>>>>>>
>>>>>> It is clear that the prog can only return either 0 or -EACCESS, and both
>>>>>> values are legal.
>>>>>>
>>>>>> So why is it rejected by the verifier?
>>>>>>
>>>>>> The verifier log shows that the second if and return value setting
>>>>>> statements in the prog is optimized to bitwise operations "r0 s>>= 63"
>>>>>> and "r0 &= -13". The verifier correctly deduces that the the value of
>>>>>> r0 is in the range [-1, 0] after verifing instruction "r0 s>>= 63".
>>>>>> But when the verifier proceeds to verify instruction "r0 &= -13", it
>>>>>> fails to deduce the correct value range of r0.
>>>>>>
>>>>>> 7: (c7) r0 s>>= 63                    ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
>>>>>> 8: (57) r0 &= -13                     ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
>>>>>>
>>>>>> So why the verifier fails to deduce the result of 'r0 &= -13'?
>>>>>>
>>>>>> The verifier uses tnum to track values, and the two ranges "[-1, 0]" and
>>>>>> "[0, -1ULL]" are encoded to the same tnum. When verifing instruction
>>>>>> "r0 &= -13", the verifier erroneously deduces the result from
>>>>>> "[0, -1ULL] AND -13", which is out of the expected return range
>>>>>> [-4095, 0].
>>>>>>
>>>>>> To fix it, this patch simply adds a special SCALAR32 case for the
>>>>>> verifier. That is, when the source operand of the AND instruction is
>>>>>> a constant and the destination operand changes from negative to
>>>>>> non-negative and falls in range [-256, 256], deduce the result range
>>>>>> by enumerating all possible AND results.
>>>>>>
>>>>>> Signed-off-by: Xu Kuohai <xukuohai@huawei.com>
>>>>>> ---
>>>>>
>>>>> Hello,
>>>>>
>>>>> Sorry for the delay, I had to think about this issue a bit.
>>>>> I found the clang transformation that generates the pattern this patch
>>>>> tries to handle.
>>>>> It is located in DAGCombiner::SimplifySelectCC() method (see [1]).
>>>>> The transformation happens as a part of DAG to DAG rewrites
>>>>> (LLVM uses several internal representations:
>>>>>   - generic optimizer uses LLVM IR, most of the work is done
>>>>>     using this representation;
>>>>>   - before instruction selection IR is converted to Selection DAG,
>>>>>     some optimizations are applied at this stage,
>>>>>     all such optimizations are a set of pattern replacements;
>>>>>   - Selection DAG is converted to machine code, some optimizations
>>>>>     are applied at the machine code level).
>>>>>
>>>>> Full pattern is described as follows:
>>>>>
>>>>>    // fold (select_cc seteq (and x, y), 0, 0, A) -> (and (sra (shl x)) A)
>>>>>    // where y is has a single bit set.
>>>>>    // A plaintext description would be, we can turn the SELECT_CC into an AND
>>>>>    // when the condition can be materialized as an all-ones register.  Any
>>>>>    // single bit-test can be materialized as an all-ones register with
>>>>>    // shift-left and shift-right-arith.
>>>>>
>>>>> For this particular test case the DAG is converted as follows:
>>>>>
>>>>>                      .---------------- lhs         The meaning of this select_cc is:
>>>>>                      |        .------- rhs         `lhs == rhs ? true value : false value`
>>>>>                      |        | .----- true value
>>>>>                      |        | |  .-- false value
>>>>>                      v        v v  v
>>>>>    (select_cc seteq (and X 2) 0 0 -13)
>>>>>                            ^
>>>>> ->                        '---------------.
>>>>>    (and (sra (sll X 62) 63)                |
>>>>>         -13)                               |
>>>>>                                            |
>>>>> Before pattern is applied, it checks that second 'and' operand has
>>>>> only one bit set, (which is true for '2').
>>>>>
>>>>> The pattern itself generates logical shift left / arithmetic shift
>>>>> right pair, that ensures that result is either all ones (-1) or all
>>>>> zeros (0). Hence, applying 'and' to shifts result and false value
>>>>> generates a correct result.
>>>>>
>>>>
>>>> Thanks for your detailed and invaluable explanation!
>>>
>>> Thanks Eduard for detailed explanation. It looks like we could
>>> resolve this issue without adding too much complexity to verifier.
>>> Also, this code pattern above seems generic enough to be worthwhile
>>> with verifier change.
>>>
>>> Kuohai, please added detailed explanation (as described by Eduard)
>>> in the commit message.
>>>
>>
>> Sure, already added, the commit message and the change now is like this:
>>
>> ---
>>
>>     bpf: Fix a false rejection caused by AND operation
>>
>>     With lsm return value check, the no-alu32 version test_libbpf_get_fd_by_id_opts
>>     is rejected by the verifier, and the log says:
>>
>>     0: R1=ctx() R10=fp0
>>     ; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
>>     0: (b7) r0 = 0                        ; R0_w=0
>>     1: (79) r2 = *(u64 *)(r1 +0)
>>     func 'bpf_lsm_bpf_map' arg0 has btf_id 916 type STRUCT 'bpf_map'
>>     2: R1=ctx() R2_w=trusted_ptr_bpf_map()
>>     ; if (map != (struct bpf_map *)&data_input) @ test_libbpf_get_fd_by_id_opts.c:29
>>     2: (18) r3 = 0xffff9742c0951a00       ; R3_w=map_ptr(map=data_input,ks=4,vs=4)
>>     4: (5d) if r2 != r3 goto pc+4         ; R2_w=trusted_ptr_bpf_map() R3_w=map_ptr(map=data_input,ks=4,vs=4)
>>     ; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
>>     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))
>>     ; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
>>     9: (95) exit
>>
>>     And here is the C code of the prog.
>>
>>     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;
>>     }
>>
>>     It is clear that the prog can only return either 0 or -EACCESS, and both
>>     values are legal.
>>
>>     So why is it rejected by the verifier?
>>
>>     The verifier log shows that the second if and return value setting
>>     statements in the prog is optimized to bitwise operations "r0 s>>= 63"
>>     and "r0 &= -13". The verifier correctly deduces that the the value of
>>     r0 is in the range [-1, 0] after verifing instruction "r0 s>>= 63".
>>     But when the verifier proceeds to verify instruction "r0 &= -13", it
>>     fails to deduce the correct value range of r0.
>>
>>     7: (c7) r0 s>>= 63                    ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
>>     8: (57) r0 &= -13                     ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
>>
>>     So why the verifier fails to deduce the result of 'r0 &= -13'?
>>
>>     The verifier uses tnum to track values, and the two ranges "[-1, 0]" and
>>     "[0, -1ULL]" are encoded to the same tnum. When verifing instruction
>>     "r0 &= -13", the verifier erroneously deduces the result from
>>     "[0, -1ULL] AND -13", which is out of the expected return range
>>     [-4095, 0].
>>
>>     As explained by Eduard in [0], the clang transformation that generates this
>>     pattern is located in DAGCombiner::SimplifySelectCC() method (see [1]).
>>
>>     The transformation happens as a part of DAG to DAG rewrites
>>     (LLVM uses several internal representations:
>>      - generic optimizer uses LLVM IR, most of the work is done
>>        using this representation;
>>      - before instruction selection IR is converted to Selection DAG,
>>        some optimizations are applied at this stage,
>>        all such optimizations are a set of pattern replacements;
>>      - Selection DAG is converted to machine code, some optimizations
>>        are applied at the machine code level).
>>
>>     Full pattern is described as follows:
>>
>>       // fold (select_cc seteq (and x, y), 0, 0, A) -> (and (sra (shl x)) A)
>>       // where y is has a single bit set.
>>       // A plaintext description would be, we can turn the SELECT_CC into an AND
>>       // when the condition can be materialized as an all-ones register.  Any
>>       // single bit-test can be materialized as an all-ones register with
>>       // shift-left and shift-right-arith.
>>
>>     For this particular test case the DAG is converted as follows:
>>
>>                         .---------------- lhs         The meaning of this select_cc is:
>>                         |        .------- rhs         `lhs == rhs ? true value : false value`
>>                         |        | .----- true value
>>                         |        | |  .-- false value
>>                         v        v v  v
>>       (select_cc seteq (and X 2) 0 0 -13)
>>                               ^
>>     ->                        '---------------.
>>       (and (sra (sll X 62) 63)                |
>>            -13)                               |
>>                                               |
>>     Before pattern is applied, it checks that second 'and' operand has
>>     only one bit set, (which is true for '2').
>>
>>     The pattern itself generates logical shift left / arithmetic shift
>>     right pair, that ensures that result is either all ones (-1) or all
>>     zeros (0). Hence, applying 'and' to shifts result and false value
>>     generates a correct result.
>>
>>     As suggested by Eduard, this patch makes a special case for source
>>     or destination register of '&=' operation being in range [-1, 0].
>>
>>     Meaning that one of the '&=' operands is either:
>>     - all ones, in which case the counterpart is the result of the operation;
>>     - all zeros, in which case zero is the result of the operation.
>>
>>     And MIN and MAX values could be derived based on above two observations.
>>
>>     [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
>>     [1] https://github.com/llvm/llvm-project/blob/4523a267829c807f3fc8fab8e5e9613985a51565/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp
>>
>>     Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
>>     Signed-off-by: Xu Kuohai <xukuohai@huawei.com>
>>
>> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
>> index 640747b53745..30c551d39329 100644
>> --- a/kernel/bpf/verifier.c
>> +++ b/kernel/bpf/verifier.c
>> @@ -13374,6 +13374,24 @@ 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);
>>
>> +       /* Special case: src_reg is known and dst_reg is in range [-1, 0] */
>> +       if (src_known &&
>> +               dst_reg->s32_min_value == -1 && dst_reg->s32_max_value == 0 &&
>> +               dst_reg->smin_value == -1 && dst_reg->smax_value == 0) {
> 
> do we need to check dst_reg->smin_value/smax_value here? They should not impact
> final dst_reg->s32_{min,max}_value computation, right?

right, the check was simply copied from the old code, which only handled
the case where 64-bit range is the same as the 32-bit range

> Similarly, for later 64bit min/max and, 32bit value does not really matter.
> 

hmm, the 32-bit check is completely unnecessary.


>> + dst_reg->s32_min_value = min_t(s32, src_reg->s32_min_value, 0);
>> +               dst_reg->s32_max_value = max_t(s32, src_reg->s32_min_value, 0);
>> +               return;
>> +       }
>> +
>> +       /* Special case: dst_reg is known and src_reg is in range [-1, 0] */
>> +       if (dst_known &&
>> +               src_reg->s32_min_value == -1 && src_reg->s32_max_value == 0 &&
>> +               src_reg->smin_value == -1 && src_reg->smax_value == 0) {
>> +               dst_reg->s32_min_value = min_t(s32, dst_reg->s32_min_value, 0);
>> +               dst_reg->s32_max_value = max_t(s32, dst_reg->s32_min_value, 0);
>> +               return;
>> +       }
>> +
>>         /* Safe to set s32 bounds by casting u32 result into s32 when u32
>>          * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded.
>>          */
>> @@ -13404,6 +13422,24 @@ 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);
>>
>> +       /* Special case: src_reg is known and dst_reg is in range [-1, 0] */
>> +       if (src_known &&
>> +               dst_reg->smin_value == -1 && dst_reg->smax_value == 0 &&
>> +               dst_reg->s32_min_value == -1 && dst_reg->s32_max_value == 0) {
>> +               dst_reg->smin_value = min_t(s64, src_reg->smin_value, 0);
>> +               dst_reg->smax_value = max_t(s64, src_reg->smin_value, 0);
>> +               return;
>> +       }
>> +
>> +       /* Special case: dst_reg is known and src_reg is in range [-1, 0] */
>> +       if (dst_known &&
>> +               src_reg->smin_value == -1 && src_reg->smax_value == 0 &&
>> +               src_reg->s32_min_value == -1 && src_reg->s32_max_value == 0) {
>> +               dst_reg->smin_value = min_t(s64, dst_reg->smin_value, 0);
>> +               dst_reg->smax_value = max_t(s64, dst_reg->smin_value, 0);
>> +               return;
>> +       }
>> +
>>         /* Safe to set s64 bounds by casting u64 result into s64 when u64
>>          * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded.
>>          */
>>
>>>>
>>>>> In my opinion the approach taken by this patch is sub-optimal:
>>>>> - 512 iterations is too much;
>>>>> - this does not cover all code that could be generated by the above
>>>>>    mentioned LLVM transformation
>>>>>    (e.g. second 'and' operand could be 1 << 16).
>>>>>
>>>>> Instead, I suggest to make a special case for source or dst register
>>>>> of '&=' operation being in range [-1,0].
>>>>> Meaning that one of the '&=' operands is either:
>>>>> - all ones, in which case the counterpart is the result of the operation;
>>>>> - all zeros, in which case zero is the result of the operation;
>>>>> - derive MIN and MAX values based on above two observations.
>>>>>
>>>>
>>>> Totally agree, I'll cook a new patch as you suggested.
>>>>
>>>>> [1] https://github.com/llvm/llvm-project/blob/4523a267829c807f3fc8fab8e5e9613985a51565/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L5391
>>>>>
>>>>> Best regards,
>>>>> Eduard
>>>>
>>>>
>>>
>>