* [PATCH bpf-next v5 1/2] bpf: Add range tracking for BPF_DIV and BPF_MOD
2026-01-19 8:54 [PATCH bpf-next v5 0/2] bpf: Add range tracking for BPF_DIV and BPF_MOD Yazhou Tang
@ 2026-01-19 8:54 ` Yazhou Tang
2026-01-20 18:51 ` Eduard Zingerman
2026-01-21 0:32 ` Eduard Zingerman
2026-01-19 8:54 ` [PATCH bpf-next v5 2/2] selftests/bpf: Add tests for BPF_DIV and BPF_MOD range tracking Yazhou Tang
2026-01-21 0:50 ` [PATCH bpf-next v5 0/2] bpf: Add range tracking for BPF_DIV and BPF_MOD patchwork-bot+netdevbpf
2 siblings, 2 replies; 9+ messages in thread
From: Yazhou Tang @ 2026-01-19 8:54 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, john.fastabend, andrii, martin.lau, eddyz87, song,
yonghong.song, kpsingh, sdf, haoluo, jolsa, tangyazhou518,
shenghaoyuan0928, ziye, syzbot
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
---
kernel/bpf/verifier.c | 299 ++++++++++++++++++
.../bpf/progs/verifier_value_illegal_alu.c | 7 +-
.../testing/selftests/bpf/verifier/precise.c | 4 +-
3 files changed, 305 insertions(+), 5 deletions(-)
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 9de0ec0c3ed9..c5a30a0f8ac5 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2341,6 +2341,18 @@ static void __mark_reg32_unbounded(struct bpf_reg_state *reg)
reg->u32_max_value = U32_MAX;
}
+static void reset_reg64_and_tnum(struct bpf_reg_state *reg)
+{
+ __mark_reg64_unbounded(reg);
+ reg->var_off = tnum_unknown;
+}
+
+static void reset_reg32_and_tnum(struct bpf_reg_state *reg)
+{
+ __mark_reg32_unbounded(reg);
+ reg->var_off = tnum_unknown;
+}
+
static void __update_reg32_bounds(struct bpf_reg_state *reg)
{
struct tnum var32_off = tnum_subreg(reg->var_off);
@@ -15090,6 +15102,252 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg,
}
}
+static void scalar32_min_max_udiv(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ u32 *dst_umin = &dst_reg->u32_min_value;
+ u32 *dst_umax = &dst_reg->u32_max_value;
+ u32 src_val = src_reg->u32_min_value; /* non-zero, const divisor */
+
+ *dst_umin = *dst_umin / src_val;
+ *dst_umax = *dst_umax / src_val;
+
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->s32_min_value = S32_MIN;
+ dst_reg->s32_max_value = S32_MAX;
+ reset_reg64_and_tnum(dst_reg);
+}
+
+static void scalar_min_max_udiv(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ u64 *dst_umin = &dst_reg->umin_value;
+ u64 *dst_umax = &dst_reg->umax_value;
+ u64 src_val = src_reg->umin_value; /* non-zero, const divisor */
+
+ *dst_umin = div64_u64(*dst_umin, src_val);
+ *dst_umax = div64_u64(*dst_umax, src_val);
+
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->smin_value = S64_MIN;
+ dst_reg->smax_value = S64_MAX;
+ reset_reg32_and_tnum(dst_reg);
+}
+
+static void scalar32_min_max_sdiv(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ s32 *dst_smin = &dst_reg->s32_min_value;
+ s32 *dst_smax = &dst_reg->s32_max_value;
+ s32 src_val = src_reg->s32_min_value; /* non-zero, const divisor */
+ s32 res1, res2;
+
+ /* BPF div specification: S32_MIN / -1 = S32_MIN */
+ if (*dst_smin == S32_MIN && src_val == -1) {
+ /*
+ * If the dividend range contains more than just S32_MIN,
+ * we cannot precisely track the result, so it becomes unbounded.
+ * e.g., [S32_MIN, S32_MIN+10]/(-1),
+ * = {S32_MIN} U [-(S32_MIN+10), -(S32_MIN+1)]
+ * = {S32_MIN} U [S32_MAX-9, S32_MAX] = [S32_MIN, S32_MAX]
+ * Otherwise (if dividend is exactly S32_MIN), result remains S32_MIN.
+ */
+ if (*dst_smax != S32_MIN) {
+ *dst_smin = S32_MIN;
+ *dst_smax = S32_MAX;
+ }
+ goto reset;
+ }
+
+ res1 = *dst_smin / src_val;
+ res2 = *dst_smax / src_val;
+ *dst_smin = min(res1, res2);
+ *dst_smax = max(res1, res2);
+
+reset:
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->u32_min_value = 0;
+ dst_reg->u32_max_value = U32_MAX;
+ reset_reg64_and_tnum(dst_reg);
+}
+
+static void scalar_min_max_sdiv(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ s64 *dst_smin = &dst_reg->smin_value;
+ s64 *dst_smax = &dst_reg->smax_value;
+ s64 src_val = src_reg->smin_value; /* non-zero, const divisor */
+ s64 res1, res2;
+
+ /* BPF div specification: S64_MIN / -1 = S64_MIN */
+ if (*dst_smin == S64_MIN && src_val == -1) {
+ /*
+ * If the dividend range contains more than just S64_MIN,
+ * we cannot precisely track the result, so it becomes unbounded.
+ * e.g., [S64_MIN, S64_MIN+10]/(-1),
+ * = {S64_MIN} U [-(S64_MIN+10), -(S64_MIN+1)]
+ * = {S64_MIN} U [S64_MAX-9, S64_MAX] = [S64_MIN, S64_MAX]
+ * Otherwise (if dividend is exactly S64_MIN), result remains S64_MIN.
+ */
+ if (*dst_smax != S64_MIN) {
+ *dst_smin = S64_MIN;
+ *dst_smax = S64_MAX;
+ }
+ goto reset;
+ }
+
+ res1 = div64_s64(*dst_smin, src_val);
+ res2 = div64_s64(*dst_smax, src_val);
+ *dst_smin = min(res1, res2);
+ *dst_smax = max(res1, res2);
+
+reset:
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->umin_value = 0;
+ dst_reg->umax_value = U64_MAX;
+ reset_reg32_and_tnum(dst_reg);
+}
+
+static void scalar32_min_max_umod(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ u32 *dst_umin = &dst_reg->u32_min_value;
+ u32 *dst_umax = &dst_reg->u32_max_value;
+ u32 src_val = src_reg->u32_min_value; /* non-zero, const divisor */
+ u32 res_max = src_val - 1;
+
+ /*
+ * If dst_umax <= res_max, the result remains unchanged.
+ * e.g., [2, 5] % 10 = [2, 5].
+ */
+ if (*dst_umax <= res_max)
+ return;
+
+ *dst_umin = 0;
+ *dst_umax = min(*dst_umax, res_max);
+
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->s32_min_value = S32_MIN;
+ dst_reg->s32_max_value = S32_MAX;
+ reset_reg64_and_tnum(dst_reg);
+}
+
+static void scalar_min_max_umod(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ u64 *dst_umin = &dst_reg->umin_value;
+ u64 *dst_umax = &dst_reg->umax_value;
+ u64 src_val = src_reg->umin_value; /* non-zero, const divisor */
+ u64 res_max = src_val - 1;
+
+ /*
+ * If dst_umax <= res_max, the result remains unchanged.
+ * e.g., [2, 5] % 10 = [2, 5].
+ */
+ if (*dst_umax <= res_max)
+ return;
+
+ *dst_umin = 0;
+ *dst_umax = min(*dst_umax, res_max);
+
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->smin_value = S64_MIN;
+ dst_reg->smax_value = S64_MAX;
+ reset_reg32_and_tnum(dst_reg);
+}
+
+static void scalar32_min_max_smod(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ s32 *dst_smin = &dst_reg->s32_min_value;
+ s32 *dst_smax = &dst_reg->s32_max_value;
+ s32 src_val = src_reg->s32_min_value; /* non-zero, const divisor */
+
+ /*
+ * Safe absolute value calculation:
+ * If src_val == S32_MIN (-2147483648), src_abs becomes 2147483648.
+ * Here use unsigned integer to avoid overflow.
+ */
+ u32 src_abs = (src_val > 0) ? (u32)src_val : -(u32)src_val;
+
+ /*
+ * Calculate the maximum possible absolute value of the result.
+ * Even if src_abs is 2147483648 (S32_MIN), subtracting 1 gives
+ * 2147483647 (S32_MAX), which fits perfectly in s32.
+ */
+ s32 res_max_abs = src_abs - 1;
+
+ /*
+ * If the dividend is already within the result range,
+ * the result remains unchanged. e.g., [-2, 5] % 10 = [-2, 5].
+ */
+ if (*dst_smin >= -res_max_abs && *dst_smax <= res_max_abs)
+ return;
+
+ /* General case: result has the same sign as the dividend. */
+ if (*dst_smin >= 0) {
+ *dst_smin = 0;
+ *dst_smax = min(*dst_smax, res_max_abs);
+ } else if (*dst_smax <= 0) {
+ *dst_smax = 0;
+ *dst_smin = max(*dst_smin, -res_max_abs);
+ } else {
+ *dst_smin = -res_max_abs;
+ *dst_smax = res_max_abs;
+ }
+
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->u32_min_value = 0;
+ dst_reg->u32_max_value = U32_MAX;
+ reset_reg64_and_tnum(dst_reg);
+}
+
+static void scalar_min_max_smod(struct bpf_reg_state *dst_reg,
+ struct bpf_reg_state *src_reg)
+{
+ s64 *dst_smin = &dst_reg->smin_value;
+ s64 *dst_smax = &dst_reg->smax_value;
+ s64 src_val = src_reg->smin_value; /* non-zero, const divisor */
+
+ /*
+ * Safe absolute value calculation:
+ * If src_val == S64_MIN (-2^63), src_abs becomes 2^63.
+ * Here use unsigned integer to avoid overflow.
+ */
+ u64 src_abs = (src_val > 0) ? (u64)src_val : -(u64)src_val;
+
+ /*
+ * Calculate the maximum possible absolute value of the result.
+ * Even if src_abs is 2^63 (S64_MIN), subtracting 1 gives
+ * 2^63 - 1 (S64_MAX), which fits perfectly in s64.
+ */
+ s64 res_max_abs = src_abs - 1;
+
+ /*
+ * If the dividend is already within the result range,
+ * the result remains unchanged. e.g., [-2, 5] % 10 = [-2, 5].
+ */
+ if (*dst_smin >= -res_max_abs && *dst_smax <= res_max_abs)
+ return;
+
+ /* General case: result has the same sign as the dividend. */
+ if (*dst_smin >= 0) {
+ *dst_smin = 0;
+ *dst_smax = min(*dst_smax, res_max_abs);
+ } else if (*dst_smax <= 0) {
+ *dst_smax = 0;
+ *dst_smin = max(*dst_smin, -res_max_abs);
+ } else {
+ *dst_smin = -res_max_abs;
+ *dst_smax = res_max_abs;
+ }
+
+ /* Reset other ranges/tnum to unbounded/unknown. */
+ dst_reg->umin_value = 0;
+ dst_reg->umax_value = U64_MAX;
+ reset_reg32_and_tnum(dst_reg);
+}
+
static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
struct bpf_reg_state *src_reg)
{
@@ -15495,6 +15753,14 @@ static bool is_safe_to_compute_dst_reg_range(struct bpf_insn *insn,
case BPF_MUL:
return true;
+ /*
+ * Division and modulo operators range is only safe to compute when the
+ * divisor is a constant.
+ */
+ case BPF_DIV:
+ case BPF_MOD:
+ return src_is_const;
+
/* Shift operators range is only computable if shift dimension operand
* is a constant. Shifts greater than 31 or 63 are undefined. This
* includes shifts by a negative number.
@@ -15547,6 +15813,7 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
struct bpf_reg_state src_reg)
{
u8 opcode = BPF_OP(insn->code);
+ s16 off = insn->off;
bool alu32 = (BPF_CLASS(insn->code) != BPF_ALU64);
int ret;
@@ -15598,6 +15865,38 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
scalar32_min_max_mul(dst_reg, &src_reg);
scalar_min_max_mul(dst_reg, &src_reg);
break;
+ case BPF_DIV:
+ /* BPF div specification: x / 0 = 0 */
+ if ((alu32 && src_reg.u32_min_value == 0) || (!alu32 && src_reg.umin_value == 0)) {
+ ___mark_reg_known(dst_reg, 0);
+ break;
+ }
+ if (alu32)
+ if (off == 1)
+ scalar32_min_max_sdiv(dst_reg, &src_reg);
+ else
+ scalar32_min_max_udiv(dst_reg, &src_reg);
+ else
+ if (off == 1)
+ scalar_min_max_sdiv(dst_reg, &src_reg);
+ else
+ scalar_min_max_udiv(dst_reg, &src_reg);
+ break;
+ case BPF_MOD:
+ /* BPF mod specification: x % 0 = x */
+ if ((alu32 && src_reg.u32_min_value == 0) || (!alu32 && src_reg.umin_value == 0))
+ break;
+ if (alu32)
+ if (off == 1)
+ scalar32_min_max_smod(dst_reg, &src_reg);
+ else
+ scalar32_min_max_umod(dst_reg, &src_reg);
+ else
+ if (off == 1)
+ scalar_min_max_smod(dst_reg, &src_reg);
+ else
+ scalar_min_max_umod(dst_reg, &src_reg);
+ break;
case BPF_AND:
if (tnum_is_const(src_reg.var_off)) {
ret = maybe_fork_scalars(env, insn, dst_reg);
diff --git a/tools/testing/selftests/bpf/progs/verifier_value_illegal_alu.c b/tools/testing/selftests/bpf/progs/verifier_value_illegal_alu.c
index 2129e4353fd9..4d8273c258d5 100644
--- a/tools/testing/selftests/bpf/progs/verifier_value_illegal_alu.c
+++ b/tools/testing/selftests/bpf/progs/verifier_value_illegal_alu.c
@@ -173,14 +173,15 @@ __naked void flow_keys_illegal_variable_offset_alu(void)
asm volatile(" \
r6 = r1; \
r7 = *(u64*)(r6 + %[flow_keys_off]); \
- r8 = 8; \
- r8 /= 1; \
+ call %[bpf_get_prandom_u32]; \
+ r8 = r0; \
r8 &= 8; \
r7 += r8; \
r0 = *(u64*)(r7 + 0); \
exit; \
" :
- : __imm_const(flow_keys_off, offsetof(struct __sk_buff, flow_keys))
+ : __imm_const(flow_keys_off, offsetof(struct __sk_buff, flow_keys)),
+ __imm(bpf_get_prandom_u32)
: __clobber_all);
}
diff --git a/tools/testing/selftests/bpf/verifier/precise.c b/tools/testing/selftests/bpf/verifier/precise.c
index 59a020c35647..061d98f6e9bb 100644
--- a/tools/testing/selftests/bpf/verifier/precise.c
+++ b/tools/testing/selftests/bpf/verifier/precise.c
@@ -229,11 +229,11 @@
{
"precise: program doesn't prematurely prune branches",
.insns = {
- BPF_ALU64_IMM(BPF_MOV, BPF_REG_6, 0x400),
+ BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_get_prandom_u32),
+ BPF_ALU64_REG(BPF_MOV, BPF_REG_6, BPF_REG_0),
BPF_ALU64_IMM(BPF_MOV, BPF_REG_7, 0),
BPF_ALU64_IMM(BPF_MOV, BPF_REG_8, 0),
BPF_ALU64_IMM(BPF_MOV, BPF_REG_9, 0x80000000),
- BPF_ALU64_IMM(BPF_MOD, BPF_REG_6, 0x401),
BPF_JMP_IMM(BPF_JA, 0, 0, 0),
BPF_JMP_REG(BPF_JLE, BPF_REG_6, BPF_REG_9, 2),
BPF_ALU64_IMM(BPF_MOD, BPF_REG_6, 1),
--
2.52.0
^ permalink raw reply related [flat|nested] 9+ messages in thread* [PATCH bpf-next v5 2/2] selftests/bpf: Add tests for BPF_DIV and BPF_MOD range tracking
2026-01-19 8:54 [PATCH bpf-next v5 0/2] bpf: Add range tracking for BPF_DIV and BPF_MOD Yazhou Tang
2026-01-19 8:54 ` [PATCH bpf-next v5 1/2] " Yazhou Tang
@ 2026-01-19 8:54 ` Yazhou Tang
2026-01-21 0:50 ` [PATCH bpf-next v5 0/2] bpf: Add range tracking for BPF_DIV and BPF_MOD patchwork-bot+netdevbpf
2 siblings, 0 replies; 9+ messages in thread
From: Yazhou Tang @ 2026-01-19 8:54 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, john.fastabend, andrii, martin.lau, eddyz87, song,
yonghong.song, kpsingh, sdf, haoluo, jolsa, tangyazhou518,
shenghaoyuan0928, ziye
From: Yazhou Tang <tangyazhou518@outlook.com>
Now BPF_DIV has range tracking support via interval analysis. This patch
adds selftests to cover various cases of BPF_DIV and BPF_MOD operations
when the divisor is a constant, also covering both signed and unsigned variants.
This patch includes several types of tests in 32-bit and 64-bit variants:
1. For UDIV
- positive divisor
- zero divisor
2. For SDIV
- positive divisor, positive dividend
- positive divisor, negative dividend
- positive divisor, mixed sign dividend
- negative divisor, positive dividend
- negative divisor, negative dividend
- negative divisor, mixed sign dividend
- zero divisor
- overflow (SIGNED_MIN/-1), normal dividend
- overflow (SIGNED_MIN/-1), constant dividend
3. For UMOD
- positive divisor
- positive divisor, small dividend
- zero divisor
4. For SMOD
- positive divisor, positive dividend
- positive divisor, negative dividend
- positive divisor, mixed sign dividend
- positive divisor, mixed sign dividend, small dividend
- negative divisor, positive dividend
- negative divisor, negative dividend
- negative divisor, mixed sign dividend
- negative divisor, mixed sign dividend, small dividend
- zero divisor
- overflow (SIGNED_MIN/-1), normal dividend
- overflow (SIGNED_MIN/-1), constant dividend
Specifically, these selftests are based on dead code elimination:
If the BPF verifier can precisely analyze the result of BPF_DIV/BPF_MOD
instruction, it can prune the path that leads to an error (here we use
invalid memory access as the error case), allowing the program to pass
verification.
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>
---
.../selftests/bpf/prog_tests/verifier.c | 2 +
.../bpf/progs/verifier_div_mod_bounds.c | 1149 +++++++++++++++++
2 files changed, 1151 insertions(+)
create mode 100644 tools/testing/selftests/bpf/progs/verifier_div_mod_bounds.c
diff --git a/tools/testing/selftests/bpf/prog_tests/verifier.c b/tools/testing/selftests/bpf/prog_tests/verifier.c
index 38c5ba70100c..fa9e506cc36f 100644
--- a/tools/testing/selftests/bpf/prog_tests/verifier.c
+++ b/tools/testing/selftests/bpf/prog_tests/verifier.c
@@ -33,6 +33,7 @@
#include "verifier_direct_packet_access.skel.h"
#include "verifier_direct_stack_access_wraparound.skel.h"
#include "verifier_div0.skel.h"
+#include "verifier_div_mod_bounds.skel.h"
#include "verifier_div_overflow.skel.h"
#include "verifier_global_subprogs.skel.h"
#include "verifier_global_ptr_args.skel.h"
@@ -175,6 +176,7 @@ void test_verifier_d_path(void) { RUN(verifier_d_path); }
void test_verifier_direct_packet_access(void) { RUN(verifier_direct_packet_access); }
void test_verifier_direct_stack_access_wraparound(void) { RUN(verifier_direct_stack_access_wraparound); }
void test_verifier_div0(void) { RUN(verifier_div0); }
+void test_verifier_div_mod_bounds(void) { RUN(verifier_div_mod_bounds); }
void test_verifier_div_overflow(void) { RUN(verifier_div_overflow); }
void test_verifier_global_subprogs(void) { RUN(verifier_global_subprogs); }
void test_verifier_global_ptr_args(void) { RUN(verifier_global_ptr_args); }
diff --git a/tools/testing/selftests/bpf/progs/verifier_div_mod_bounds.c b/tools/testing/selftests/bpf/progs/verifier_div_mod_bounds.c
new file mode 100644
index 000000000000..4672af0b3268
--- /dev/null
+++ b/tools/testing/selftests/bpf/progs/verifier_div_mod_bounds.c
@@ -0,0 +1,1149 @@
+// SPDX-License-Identifier: GPL-2.0
+
+#include <linux/bpf.h>
+#include <limits.h>
+#include <bpf/bpf_helpers.h>
+#include "bpf_misc.h"
+
+/* This file contains unit tests for signed/unsigned division and modulo
+ * operations (with divisor as a constant), focusing on verifying whether
+ * BPF verifier's range tracking module soundly and precisely computes
+ * the results.
+ */
+
+SEC("socket")
+__description("UDIV32, positive divisor")
+__success __retval(0) __log_level(2)
+__msg("w1 /= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=3,var_off=(0x0; 0x3))")
+__naked void udiv32_pos_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w1 &= 8; \
+ w1 |= 1; \
+ w1 /= 3; \
+ if w1 > 3 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UDIV32, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("w1 /= w2 {{.*}}; R1=0 R2=0")
+__naked void udiv32_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w1 &= 8; \
+ w1 |= 1; \
+ w2 = 0; \
+ w1 /= w2; \
+ if w1 != 0 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UDIV64, positive divisor")
+__success __retval(0) __log_level(2)
+__msg("r1 /= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=3,var_off=(0x0; 0x3))")
+__naked void udiv64_pos_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ r1 &= 8; \
+ r1 |= 1; \
+ r1 /= 3; \
+ if r1 > 3 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UDIV64, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("r1 /= r2 {{.*}}; R1=0 R2=0")
+__naked void udiv64_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ r1 &= 8; \
+ r1 |= 1; \
+ r2 = 0; \
+ r1 /= r2; \
+ if r1 != 0 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, positive divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= 3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
+__naked void sdiv32_pos_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< 8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s/= 3; \
+ if w1 s< 2 goto l1_%=; \
+ if w1 s> 3 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, positive divisor, negative dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= 3 {{.*}}; R1=scalar(smin=umin=umin32=0xfffffffd,smax=umax=umax32=0xfffffffe,smin32=-3,smax32=-2,var_off=(0xfffffffc; 0x3))")
+__naked void sdiv32_pos_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s> -8 goto l0_%=; \
+ if w1 s< -10 goto l0_%=; \
+ w1 s/= 3; \
+ if w1 s< -3 goto l1_%=; \
+ if w1 s> -2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, positive divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=3,var_off=(0x0; 0xffffffff))")
+__naked void sdiv32_pos_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< -8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s/= 3; \
+ if w1 s< -2 goto l1_%=; \
+ if w1 s> 3 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, negative divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= -3 {{.*}}; R1=scalar(smin=umin=umin32=0xfffffffd,smax=umax=umax32=0xfffffffe,smin32=-3,smax32=-2,var_off=(0xfffffffc; 0x3))")
+__naked void sdiv32_neg_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< 8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s/= -3; \
+ if w1 s< -3 goto l1_%=; \
+ if w1 s> -2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, negative divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= -3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
+__naked void sdiv32_neg_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s> -8 goto l0_%=; \
+ if w1 s< -10 goto l0_%=; \
+ w1 s/= -3; \
+ if w1 s< 2 goto l1_%=; \
+ if w1 s> 3 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, negative divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-3,smax32=2,var_off=(0x0; 0xffffffff))")
+__naked void sdiv32_neg_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< -8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s/= -3; \
+ if w1 s< -3 goto l1_%=; \
+ if w1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= w2 {{.*}}; R1=0 R2=0")
+__naked void sdiv32_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w1 &= 8; \
+ w1 |= 1; \
+ w2 = 0; \
+ w1 s/= w2; \
+ if w1 != 0 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, overflow (S32_MIN/-1)")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= -1 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))")
+__naked void sdiv32_overflow_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w2 = %[int_min]; \
+ w2 += 10; \
+ if w1 s> w2 goto l0_%=; \
+ w1 s/= -1; \
+l0_%=: r0 = 0; \
+ exit; \
+" :
+ : __imm_const(int_min, INT_MIN),
+ __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV32, overflow (S32_MIN/-1), constant dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s/= -1 {{.*}}; R1=0x80000000")
+__naked void sdiv32_overflow_2(void)
+{
+ asm volatile (" \
+ w1 = %[int_min]; \
+ w1 s/= -1; \
+ if w1 != %[int_min] goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm_const(int_min, INT_MIN)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, positive divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= 3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
+__naked void sdiv64_pos_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< 8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s/= 3; \
+ if r1 s< 2 goto l1_%=; \
+ if r1 s> 3 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, positive divisor, negative dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= 3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=-2,umin=0xfffffffffffffffd,umax=0xfffffffffffffffe,umin32=0xfffffffd,umax32=0xfffffffe,var_off=(0xfffffffffffffffc; 0x3))")
+__naked void sdiv64_pos_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s> -8 goto l0_%=; \
+ if r1 s< -10 goto l0_%=; \
+ r1 s/= 3; \
+ if r1 s< -3 goto l1_%=; \
+ if r1 s> -2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, positive divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=3)")
+__naked void sdiv64_pos_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< -8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s/= 3; \
+ if r1 s< -2 goto l1_%=; \
+ if r1 s> 3 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, negative divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= -3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=-2,umin=0xfffffffffffffffd,umax=0xfffffffffffffffe,umin32=0xfffffffd,umax32=0xfffffffe,var_off=(0xfffffffffffffffc; 0x3))")
+__naked void sdiv64_neg_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< 8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s/= -3; \
+ if r1 s< -3 goto l1_%=; \
+ if r1 s> -2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, negative divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= -3 {{.*}}; R1=scalar(smin=umin=smin32=umin32=2,smax=umax=smax32=umax32=3,var_off=(0x2; 0x1))")
+__naked void sdiv64_neg_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s> -8 goto l0_%=; \
+ if r1 s< -10 goto l0_%=; \
+ r1 s/= -3; \
+ if r1 s< 2 goto l1_%=; \
+ if r1 s> 3 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, negative divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= -3 {{.*}}; R1=scalar(smin=smin32=-3,smax=smax32=2)")
+__naked void sdiv64_neg_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< -8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s/= -3; \
+ if r1 s< -3 goto l1_%=; \
+ if r1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= r2 {{.*}}; R1=0 R2=0")
+__naked void sdiv64_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ r1 &= 8; \
+ r1 |= 1; \
+ r2 = 0; \
+ r1 s/= r2; \
+ if r1 != 0 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, overflow (S64_MIN/-1)")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= -1 {{.*}}; R1=scalar()")
+__naked void sdiv64_overflow_1(void)
+{
+ asm volatile (" \
+ call %[bpf_ktime_get_ns]; \
+ r1 = r0; \
+ r2 = %[llong_min] ll; \
+ r2 += 10; \
+ if r1 s> r2 goto l0_%=; \
+ r1 s/= -1; \
+l0_%=: r0 = 0; \
+ exit; \
+" :
+ : __imm_const(llong_min, LLONG_MIN),
+ __imm(bpf_ktime_get_ns)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SDIV64, overflow (S64_MIN/-1), constant dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s/= -1 {{.*}}; R1=0x8000000000000000")
+__naked void sdiv64_overflow_2(void)
+{
+ asm volatile (" \
+ r1 = %[llong_min] ll; \
+ r1 s/= -1; \
+ r2 = %[llong_min] ll; \
+ if r1 != r2 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm_const(llong_min, LLONG_MIN)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UMOD32, positive divisor")
+__success __retval(0) __log_level(2)
+__msg("w1 %= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
+__naked void umod32_pos_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w1 &= 8; \
+ w1 |= 1; \
+ w1 %%= 3; \
+ if w1 > 3 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UMOD32, positive divisor, small dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 %= 10 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
+__naked void umod32_pos_divisor_unchanged(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w1 &= 8; \
+ w1 |= 1; \
+ w1 %%= 10; \
+ if w1 < 1 goto l0_%=; \
+ if w1 > 9 goto l0_%=; \
+ if w1 & 1 != 1 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UMOD32, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("w1 %= w2 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8)) R2=0")
+__naked void umod32_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w1 &= 8; \
+ w1 |= 1; \
+ w2 = 0; \
+ w1 %%= w2; \
+ if w1 < 1 goto l0_%=; \
+ if w1 > 9 goto l0_%=; \
+ if w1 & 1 != 1 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UMOD64, positive divisor")
+__success __retval(0) __log_level(2)
+__msg("r1 %= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
+__naked void umod64_pos_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ r1 &= 8; \
+ r1 |= 1; \
+ r1 %%= 3; \
+ if r1 > 3 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UMOD64, positive divisor, small dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 %= 10 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8))")
+__naked void umod64_pos_divisor_unchanged(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ r1 &= 8; \
+ r1 |= 1; \
+ r1 %%= 10; \
+ if r1 < 1 goto l0_%=; \
+ if r1 > 9 goto l0_%=; \
+ if r1 & 1 != 1 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("UMOD64, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("r1 %= r2 {{.*}}; R1=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=9,var_off=(0x1; 0x8)) R2=0")
+__naked void umod64_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ r1 &= 8; \
+ r1 |= 1; \
+ r2 = 0; \
+ r1 %%= r2; \
+ if r1 < 1 goto l0_%=; \
+ if r1 > 9 goto l0_%=; \
+ if r1 & 1 != 1 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, positive divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
+__naked void smod32_pos_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< 8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s%%= 3; \
+ if w1 s< 0 goto l1_%=; \
+ if w1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, positive divisor, negative dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=0,var_off=(0x0; 0xffffffff))")
+__naked void smod32_pos_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s> -8 goto l0_%=; \
+ if w1 s< -10 goto l0_%=; \
+ w1 s%%= 3; \
+ if w1 s< -2 goto l1_%=; \
+ if w1 s> 0 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, positive divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= 3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=2,var_off=(0x0; 0xffffffff))")
+__naked void smod32_pos_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< -8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s%%= 3; \
+ if w1 s< -2 goto l1_%=; \
+ if w1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, positive divisor, small dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= 11 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff))")
+__naked void smod32_pos_divisor_unchanged(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< -8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s%%= 11; \
+ if w1 s< -8 goto l1_%=; \
+ if w1 s> 10 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, negative divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= -3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
+__naked void smod32_neg_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< 8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s%%= -3; \
+ if w1 s< 0 goto l1_%=; \
+ if w1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, negative divisor, negative dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=0,var_off=(0x0; 0xffffffff))")
+__naked void smod32_neg_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s> -8 goto l0_%=; \
+ if w1 s< -10 goto l0_%=; \
+ w1 s%%= -3; \
+ if w1 s< -2 goto l1_%=; \
+ if w1 s> 0 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, negative divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= -3 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-2,smax32=2,var_off=(0x0; 0xffffffff))")
+__naked void smod32_neg_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< -8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s%%= -3; \
+ if w1 s< -2 goto l1_%=; \
+ if w1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, negative divisor, small dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= -11 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff))")
+__naked void smod32_neg_divisor_unchanged(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< -8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w1 s%%= -11; \
+ if w1 s< -8 goto l1_%=; \
+ if w1 s> 10 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= w2 {{.*}}; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-8,smax32=10,var_off=(0x0; 0xffffffff)) R2=0")
+__naked void smod32_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ if w1 s< -8 goto l0_%=; \
+ if w1 s> 10 goto l0_%=; \
+ w2 = 0; \
+ w1 s%%= w2; \
+ if w1 s< -8 goto l1_%=; \
+ if w1 s> 10 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, overflow (S32_MIN%-1)")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= -1 {{.*}}; R1=0")
+__naked void smod32_overflow_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ w1 = w0; \
+ w2 = %[int_min]; \
+ w2 += 10; \
+ if w1 s> w2 goto l0_%=; \
+ w1 s%%= -1; \
+ if w1 != 0 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm_const(int_min, INT_MIN),
+ __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD32, overflow (S32_MIN%-1), constant dividend")
+__success __retval(0) __log_level(2)
+__msg("w1 s%= -1 {{.*}}; R1=0")
+__naked void smod32_overflow_2(void)
+{
+ asm volatile (" \
+ w1 = %[int_min]; \
+ w1 s%%= -1; \
+ if w1 != 0 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm_const(int_min, INT_MIN)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, positive divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
+__naked void smod64_pos_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< 8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s%%= 3; \
+ if r1 s< 0 goto l1_%=; \
+ if r1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, positive divisor, negative dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=0)")
+__naked void smod64_pos_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s> -8 goto l0_%=; \
+ if r1 s< -10 goto l0_%=; \
+ r1 s%%= 3; \
+ if r1 s< -2 goto l1_%=; \
+ if r1 s> 0 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, positive divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= 3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=2)")
+__naked void smod64_pos_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< -8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s%%= 3; \
+ if r1 s< -2 goto l1_%=; \
+ if r1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, positive divisor, small dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= 11 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10)")
+__naked void smod64_pos_divisor_unchanged(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< -8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s%%= 11; \
+ if r1 s< -8 goto l1_%=; \
+ if r1 s> 10 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, negative divisor, positive dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3))")
+__naked void smod64_neg_divisor_1(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< 8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s%%= -3; \
+ if r1 s< 0 goto l1_%=; \
+ if r1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, negative divisor, negative dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=0)")
+__naked void smod64_neg_divisor_2(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s> -8 goto l0_%=; \
+ if r1 s< -10 goto l0_%=; \
+ r1 s%%= -3; \
+ if r1 s< -2 goto l1_%=; \
+ if r1 s> 0 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, negative divisor, mixed sign dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= -3 {{.*}}; R1=scalar(smin=smin32=-2,smax=smax32=2)")
+__naked void smod64_neg_divisor_3(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< -8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s%%= -3; \
+ if r1 s< -2 goto l1_%=; \
+ if r1 s> 2 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, negative divisor, small dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= -11 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10)")
+__naked void smod64_neg_divisor_unchanged(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< -8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r1 s%%= -11; \
+ if r1 s< -8 goto l1_%=; \
+ if r1 s> 10 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, zero divisor")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= r2 {{.*}}; R1=scalar(smin=smin32=-8,smax=smax32=10) R2=0")
+__naked void smod64_zero_divisor(void)
+{
+ asm volatile (" \
+ call %[bpf_get_prandom_u32]; \
+ r1 = r0; \
+ if r1 s< -8 goto l0_%=; \
+ if r1 s> 10 goto l0_%=; \
+ r2 = 0; \
+ r1 s%%= r2; \
+ if r1 s< -8 goto l1_%=; \
+ if r1 s> 10 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm(bpf_get_prandom_u32)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, overflow (S64_MIN%-1)")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= -1 {{.*}}; R1=0")
+__naked void smod64_overflow_1(void)
+{
+ asm volatile (" \
+ call %[bpf_ktime_get_ns]; \
+ r1 = r0; \
+ r2 = %[llong_min] ll; \
+ r2 += 10; \
+ if r1 s> r2 goto l0_%=; \
+ r1 s%%= -1; \
+ if r1 != 0 goto l1_%=; \
+l0_%=: r0 = 0; \
+ exit; \
+l1_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm_const(llong_min, LLONG_MIN),
+ __imm(bpf_ktime_get_ns)
+ : __clobber_all);
+}
+
+SEC("socket")
+__description("SMOD64, overflow (S64_MIN%-1), constant dividend")
+__success __retval(0) __log_level(2)
+__msg("r1 s%= -1 {{.*}}; R1=0")
+__naked void smod64_overflow_2(void)
+{
+ asm volatile (" \
+ r1 = %[llong_min] ll; \
+ r1 s%%= -1; \
+ if r1 != 0 goto l0_%=; \
+ r0 = 0; \
+ exit; \
+l0_%=: r0 = *(u64 *)(r1 + 0); \
+ exit; \
+" :
+ : __imm_const(llong_min, LLONG_MIN)
+ : __clobber_all);
+}
--
2.52.0
^ permalink raw reply related [flat|nested] 9+ messages in thread