[PATCH RFC 10/17] bpf: Add bcf_alu() 32bits optimization

[Hao Sun <sunhao.th@gmail.com>]

Lower symbolic ALU nodes to 32-bit when both operands and the resulting dst
fit in 32 bits, to reduce solver/proof complexity.

- Extend `bcf_alu()` with `op_u32`/`op_s32` hints and derive a `zext` decision:
  when ALU32 or both operands/results fit u32, emit a 32-bit op and zero-extend
  to 64; when signed-32 is in effect, sign-extend to 64 after the op.

- Compute `op_u32`/`op_s32` for pointer and scalar ALUs (using fit_u32/fit_s32)
  before emitting the node, then mask them again with the post-ALU dst range so
  the final node width reflects the verifier’s bounds.

This shrinks many BV nodes and helps keep per-node vlen within limits (U8_MAX),
reducing proof size.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 30 +++++++++++++++++++++++++-----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 66682d365e5e..df6d16a1c6f6 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14866,11 +14866,13 @@ static int sanitize_check_bounds(struct bpf_verifier_env *env,
 }
 
 static int bcf_alu(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
-		   struct bpf_reg_state *src_reg, u8 op, bool alu32)
+		   struct bpf_reg_state *src_reg, u8 op, bool alu32,
+		   bool op_u32, bool op_s32)
 {
 	DEFINE_RAW_FLEX(struct bcf_expr, alu_expr, args, 2);
 	bool unary = (op == BPF_NEG);
 	int dst, src = 0, bits;
+	bool zext = alu32 || op_u32;
 
 	if (!env->bcf.tracking)
 		return 0;
@@ -14879,6 +14881,7 @@ static int bcf_alu(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
 		return 0;
 	}
 
+	alu32 |= (op_u32 || op_s32);
 	dst = bcf_reg_expr(env, dst_reg, alu32);
 	if (!unary)
 		src = bcf_reg_expr(env, src_reg, alu32);
@@ -14892,8 +14895,11 @@ static int bcf_alu(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
 	alu_expr->args[0] = dst;
 	alu_expr->args[1] = src;
 	dst_reg->bcf_expr = bcf_add_expr(env, alu_expr);
-	if (alu32)
+	if (zext)
 		bcf_zext_32_to_64(env, dst_reg);
+	else if (op_s32)
+		bcf_sext_32_to_64(env, dst_reg);
+
 	if (dst_reg->bcf_expr < 0)
 		return dst_reg->bcf_expr;
 
@@ -14922,6 +14928,7 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 	u8 opcode = BPF_OP(insn->code);
 	u32 dst = insn->dst_reg;
 	int ret, bounds_ret;
+	bool op_u32, op_s32;
 
 	dst_reg = &regs[dst];
 	src_reg = dst_reg == ptr_reg ? off_reg : ptr_reg;
@@ -15034,6 +15041,8 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			if (dst_reg->bcf_expr < 0)
 				return dst_reg->bcf_expr;
 		}
+		op_u32 = fit_u32(dst_reg) && fit_u32(src_reg);
+		op_s32 = fit_s32(dst_reg) && fit_s32(src_reg);
 		/* A new variable offset is created.  Note that off_reg->off
 		 * == 0, since it's a scalar.
 		 * dst_reg gets the pointer type and since some positive
@@ -15062,7 +15071,9 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			memset(&dst_reg->raw, 0, sizeof(dst_reg->raw));
 		}
 
-		ret = bcf_alu(env, dst_reg, src_reg, opcode, false);
+		op_u32 &= fit_u32(dst_reg);
+		op_s32 &= fit_s32(dst_reg);
+		ret = bcf_alu(env, dst_reg, src_reg, opcode, false, op_u32, op_s32);
 		if (ret)
 			return ret;
 		break;
@@ -15102,6 +15113,8 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			if (dst_reg->bcf_expr < 0)
 				return dst_reg->bcf_expr;
 		}
+		op_u32 = fit_u32(dst_reg) && fit_u32(src_reg);
+		op_s32 = fit_s32(dst_reg) && fit_s32(src_reg);
 		/* A new variable offset is created.  If the subtrahend is known
 		 * nonnegative, then any reg->range we had before is still good.
 		 */
@@ -15130,7 +15143,9 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 				memset(&dst_reg->raw, 0, sizeof(dst_reg->raw));
 		}
 
-		ret = bcf_alu(env, dst_reg, src_reg, opcode, false);
+		op_u32 &= fit_u32(dst_reg);
+		op_s32 &= fit_s32(dst_reg);
+		ret = bcf_alu(env, dst_reg, src_reg, opcode, false, op_u32, op_s32);
 		if (ret)
 			return ret;
 		break;
@@ -15787,6 +15802,7 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 	u8 opcode = BPF_OP(insn->code);
 	bool alu32 = (BPF_CLASS(insn->code) != BPF_ALU64);
 	int ret, dst_expr = dst_reg->bcf_expr;
+	bool op_u32, op_s32;
 
 	if (!is_safe_to_compute_dst_reg_range(insn, &src_reg)) {
 		__mark_reg_unknown(env, dst_reg);
@@ -15806,6 +15822,8 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 		if (dst_expr < 0)
 			return dst_expr;
 	}
+	op_u32 = fit_u32(dst_reg) && fit_u32(&src_reg);
+	op_s32 = fit_s32(dst_reg) && fit_s32(&src_reg);
 
 	/* Calculate sign/unsigned bounds and tnum for alu32 and alu64 bit ops.
 	 * There are two classes of instructions: The first class we track both
@@ -15887,7 +15905,9 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 	reg_bounds_sync(dst_reg);
 
 	dst_reg->bcf_expr = dst_expr;
-	ret = bcf_alu(env, dst_reg, &src_reg, opcode, alu32);
+	op_u32 &= fit_u32(dst_reg);
+	op_s32 &= fit_s32(dst_reg);
+	ret = bcf_alu(env, dst_reg, &src_reg, opcode, alu32, op_u32, op_s32);
 	if (ret)
 		return ret;
 
-- 
2.34.1