Re: max<min after jset

[Yonghong Song <yonghong.song@linux.dev>]

On 11/21/23 12:32 PM, Tao Lyu wrote:
> Hi,
>
> The eBPF program shown below leads to an reversed min and max
> after insn 6 "if w0 & 0x894b6a55 goto +2",
> whic means max < min.
>
> Here is the introduction how it happens.
>
> Before insn 6,
> the range of r0 expressed by the min and max field is
> min1 = 884670597, max1 = 900354100
> And the range expressed by the var_off=(0x34000000; 0x1ff5fbf))
> is min2=872415232, max2=905928639.
>
> ---min2-----------------------min1-----max1-----max2---
>
> Here we can see that the range expressed by var_off is wider than that of min and max.
>
> When verifying insn6,
> it first uses the var_off and immediate "0x894b6a55" to
> calculate the new var_off=(0x34b00000; 0x415aa).
> The range expressed by the new var_off is:
> min3=883949568, max3=884217258
>
> ---min2-----min3-----max3-----min1-----max1-----max2---
>
> And then it will calculate the new min and max by:
> (1) new-min = MAX(min3, min1) = min1
> (2) new-max = MIN(max3, max1) = max3
>
> ---min2-----min3-----max3-----min1-----max1-----max2---
>           "new-max"          "new-min"
>
> Now, the new-max becomes less than the new min.
>
> Notably, [min1, max1] can never make "w0 & 0x894b6a55 == 0"
> and thus cannot goes the fall-through branch.
> In other words, actually the fall-trough branch is a dead path.
>
> BTW, I cannot successfully compile this instruciton "if w0 != 0 goto +2;\"
> in the c inline assembly code.

The format "if w0 != 0 goto +2;\" should be supported by recent clang compiler.
Which clang version you are using? Maybe try clang 15/16? Could you also
post the C inline assembly code here so we can investigate?

> So I can only attach the bytecodes.
>
> Signed-off-by: Tao Lyu <tao.lyu@epfl.ch>
> ---
>   .../selftests/bpf/verifier/jset_reversed_range.c  | 15 +++++++++++++++
>   1 file changed, 15 insertions(+)
>   create mode 100644 tools/testing/selftests/bpf/verifier/jset_reversed_range.c
>
> diff --git a/tools/testing/selftests/bpf/verifier/jset_reversed_range.c b/tools/testing/selftests/bpf/verifier/jset_reversed_range.c
> new file mode 100644
> index 000000000000..734f492a2a96
> --- /dev/null
> +++ b/tools/testing/selftests/bpf/verifier/jset_reversed_range.c
> @@ -0,0 +1,15 @@
> +{
> +    "BPF_JSET: incorrect scalar range",
> +    .insns = {
> +    BPF_MOV64_IMM(BPF_REG_5, 100),
> +    BPF_ALU64_IMM(BPF_DIV, BPF_REG_5, 3),
> +    BPF_ALU32_IMM(BPF_RSH, BPF_REG_5, 7),
> +    BPF_ALU64_IMM(BPF_AND, BPF_REG_5, -386969681),
> +    BPF_ALU64_IMM(BPF_SUB, BPF_REG_5, -884670597),
> +    BPF_MOV32_REG(BPF_REG_0, BPF_REG_5),
> +    BPF_JMP32_IMM(BPF_JSET, BPF_REG_0, 0x894b6a55, 1),
> +    BPF_MOV64_IMM(BPF_REG_0, 1),
> +    BPF_MOV64_IMM(BPF_REG_0, 0),
> +    BPF_EXIT_INSN(),
> +    },
> +},