Re: [PATCH bpf-next v5 1/2] bpf: Add range tracking for BPF_DIV and BPF_MOD

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2026-01-19 at 16:54 +0800, Yazhou Tang wrote:
> From: Yazhou Tang <tangyazhou518@outlook.com>
> 
> This patch implements range tracking (interval analysis) for BPF_DIV and
> BPF_MOD operations when the divisor is a constant, covering both signed
> and unsigned variants.
> 
> While LLVM typically optimizes integer division and modulo by constants
> into multiplication and shift sequences, this optimization is less
> effective for the BPF target when dealing with 64-bit arithmetic.
> 
> Currently, the verifier does not track bounds for scalar division or
> modulo, treating the result as "unbounded". This leads to false positive
> rejections for safe code patterns.
> 
> For example, the following code (compiled with -O2):
> 
> ```c
> int test(struct pt_regs *ctx) {
>     char buffer[6] = {1};
>     __u64 x = bpf_ktime_get_ns();
>     __u64 res = x % sizeof(buffer);
>     char value = buffer[res];
>     bpf_printk("res = %llu, val = %d", res, value);
>     return 0;
> }
> ```
> 
> Generates a raw `BPF_MOD64` instruction:
> 
> ```asm
> ;     __u64 res = x % sizeof(buffer);
>        1:	97 00 00 00 06 00 00 00	r0 %= 0x6
> ;     char value = buffer[res];
>        2:	18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00	r1 = 0x0 ll
>        4:	0f 01 00 00 00 00 00 00	r1 += r0
>        5:	91 14 00 00 00 00 00 00	r4 = *(s8 *)(r1 + 0x0)
> ```
> 
> Without this patch, the verifier fails with "math between map_value
> pointer and register with unbounded min value is not allowed" because
> it cannot deduce that `r0` is within [0, 5].
> 
> According to the BPF instruction set[1], the instruction's offset field
> (`insn->off`) is used to distinguish between signed (`off == 1`) and
> unsigned division (`off == 0`). Moreover, we also follow the BPF division
> and modulo runtime behavior (semantics) to handle special cases, such as
> division by zero and signed division overflow.
> 
> - UDIV: dst = (src != 0) ? (dst / src) : 0
> - SDIV: dst = (src == 0) ? 0 : ((src == -1 && dst == LLONG_MIN) ? LLONG_MIN : (dst / src))
> - UMOD: dst = (src != 0) ? (dst % src) : dst
> - SMOD: dst = (src == 0) ? dst : ((src == -1 && dst == LLONG_MIN) ? 0: (dst s% src))
> 
> Here is the overview of the changes made in this patch (See the code comments
> for more details and examples):
> 
> 1. For BPF_DIV: Firstly check whether the divisor is zero. If so, set the
>    destination register to zero (matching runtime behavior).
> 
>    For non-zero constant divisors: goto `scalar(32)?_min_max_(u|s)div` functions.
>    - General cases: compute the new range by dividing max_dividend and
>      min_dividend by the constant divisor.
>    - Overflow case (SIGNED_MIN / -1) in signed division: mark the result
>      as unbounded if the dividend is not a single number.
> 
> 2. For BPF_MOD: Firstly check whether the divisor is zero. If so, leave the
>    destination register unchanged (matching runtime behavior).
> 
>    For non-zero constant divisors: goto `scalar(32)?_min_max_(u|s)mod` functions.
>    - General case: For signed modulo, the result's sign matches the
>      dividend's sign. And the result's absolute value is strictly bounded
>      by `min(abs(dividend), abs(divisor) - 1)`.
>      - Special care is taken when the divisor is SIGNED_MIN. By casting
>        to unsigned before negation and subtracting 1, we avoid signed
>        overflow and correctly calculate the maximum possible magnitude
>        (`res_max_abs` in the code).
>    - "Small dividend" case: If the dividend is already within the possible
>      result range (e.g., [-2, 5] % 10), the operation is an identity
>      function, and the destination register remains unchanged.
> 
> 3. In `scalar(32)?_min_max_(u|s)(div|mod)` functions: After updating current
>    range, reset other ranges and tnum to unbounded/unknown.
> 
>    e.g., in `scalar_min_max_sdiv`, signed 64-bit range is updated. Then reset
>    unsigned 64-bit range and 32-bit range to unbounded, and tnum to unknown.
> 
>    Exception: in BPF_MOD's "small dividend" case, since the result remains
>    unchanged, we do not reset other ranges/tnum.
> 
> 4. Also updated existing selftests based on the expected BPF_DIV and
>    BPF_MOD behavior.
> 
> [1] https://www.kernel.org/doc/Documentation/bpf/standardization/instruction-set.rst
> 
> Co-developed-by: Shenghao Yuan <shenghaoyuan0928@163.com>
> Signed-off-by: Shenghao Yuan <shenghaoyuan0928@163.com>
> Co-developed-by: Tianci Cao <ziye@zju.edu.cn>
> Signed-off-by: Tianci Cao <ziye@zju.edu.cn>
> Signed-off-by: Yazhou Tang <tangyazhou518@outlook.com>
> Tested-by: syzbot@syzkaller.appspotmail.com
> ---

Fwiw, the logic looks good to me.
smod is probably the trickiest part, I tried it using simple test [1]
and everything seem in order.

[1] https://gist.github.com/eddyz87/da600f6d738fccdd7cb8a0e7ab4214e7

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

[...]