bpf: Add value tracking for BPF_DIV

[kernel-patches-daemon-bpf]

Pull request for series with
subject: bpf: Add value tracking for BPF_DIV
version: 1
url: https://patchwork.kernel.org/project/netdevbpf/list/?series=1035457

[kernel-patches-daemon-bpf]

Upstream branch: 3d60306
series: https://patchwork.kernel.org/project/netdevbpf/list/?series=1035457
version: 1

[kernel-patches-review-bot]

commit eeca3ca42ac176e41389a95902389f85bc70c977
Author: Yazhou Tang <tangyazhou518@outlook.com>

bpf: Add interval and tnum analysis for signed and unsigned BPF_DIV

This patch adds interval and tnum analysis for BPF_DIV operations to
reduce false positive verification failures for BPF programs using
division instructions.

> diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
> index f8e70e9c3998..d115528da6a6 100644

[ ... ]

> +/* __tnum_neg_width: tnum negation with given bit width.
> + * @a: the tnum to be negated.
> + * @width: the bit width to perform negation, 32 or 64.
> + */
> +static struct tnum __tnum_neg_width(struct tnum a, int width)
> +{
> +	if (width == 32)
> +		return tnum_sub(TNUM(U32_MAX, 0), a);
                                ^^^^^^^

For 32-bit negation, is subtracting from U32_MAX correct? This computes
the bitwise NOT (~a) rather than arithmetic negation (-a).

For example, for a = -10 (0xFFFFFFF6 in 32-bit):
  U32_MAX - 0xFFFFFFF6 = 9, but |-10| = 10

The 64-bit case correctly uses tnum_sub(TNUM(0, 0), a) for negation.
Should the 32-bit case also subtract from zero (with appropriate 32-bit
masking)?

This function is called by __tnum_abs() which is used by tnum_sdiv() for
32-bit signed division, so incorrect absolute values would lead to
incorrect tnum results.

> +	else if (width == 64)
> +		return tnum_sub(TNUM(0, 0), a);
> +	else
> +		return tnum_unknown;
> +}

[ ... ]

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index d6b8a77fbe3b..df04a35153ef 100644

[ ... ]

> +static void scalar32_min_max_sdiv(struct bpf_reg_state *dst_reg,
> +				struct bpf_reg_state *src_reg)
> +{
> +	u32 *dst_smin = &dst_reg->s32_min_value;
> +	u32 *dst_smax = &dst_reg->s32_max_value;
> +	u32 smin_val = src_reg->s32_min_value;
> +	u32 smax_val = src_reg->s32_max_value;
        ^^^

Should these be s32 rather than u32? The fields s32_min_value and
s32_max_value are declared as s32 in struct bpf_reg_state.

Using u32 causes the signed comparisons below to behave incorrectly:

> +	if (smin_val <= 0 && smax_val >= 0) {
            ^^^^^^^^^^^^

When s32_min_value contains a negative value like -10 (stored as
0xFFFFFFF6), reading it as u32 gives 4294967286, and the comparison
"smin_val <= 0" becomes "4294967286 <= 0" which is always false.

Similarly:

> +		if (smin_val < 0) {
                    ^^^^^^^^^^^^

This condition can never be true when smin_val is u32.

The 64-bit version scalar_min_max_sdiv() correctly uses s64 types.

[ ... ]

---

AI reviewed your patch. Please fix the bug or email reply why it's not a bug.
See: https://github.com/kernel-patches/vmtest/blob/master/ci/claude/README.md

In-Reply-To-Subject: bpf: Add interval and tnum analysis for signed and unsigned BPF_DIV
CI run summary: https://github.com/kernel-patches/bpf/actions/runs/20408116978

[kernel-patches-daemon-bpf]

Forwarding comment 3678654740 via email
In-Reply-To: tencent_7C98FAECA40C98489ACF4515CE346F031509@qq.com
Patch: https://patchwork.kernel.org/project/netdevbpf/patch/tencent_7C98FAECA40C98489ACF4515CE346F031509@qq.com/

[kernel-patches-daemon-bpf]

Upstream branch: d2749ae
series: https://patchwork.kernel.org/project/netdevbpf/list/?series=1035457
version: 1

[kernel-patches-daemon-bpf]

Upstream branch: f785a31
series: https://patchwork.kernel.org/project/netdevbpf/list/?series=1035457
version: 1