bpf.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: Hao Sun <sunhao.th@gmail.com>
To: bpf@vger.kernel.org
Cc: ast@kernel.org, daniel@iogearbox.net, andrii@kernel.org,
	eddyz87@gmail.com, john.fastabend@gmail.com,
	martin.lau@linux.dev, song@kernel.org, yonghong.song@linux.dev,
	linux-kernel@vger.kernel.org, sunhao.th@gmail.com,
	Hao Sun <hao.sun@inf.ethz.ch>
Subject: [PATCH RFC 08/17] bpf: Track mov and signed extension
Date: Thu,  6 Nov 2025 13:52:46 +0100	[thread overview]
Message-ID: <20251106125255.1969938-9-hao.sun@inf.ethz.ch> (raw)
In-Reply-To: <20251106125255.1969938-1-hao.sun@inf.ethz.ch>

Add `bcf_mov()` helpers to model MOV/cast operations in `bcf_track()` and add 
calls into ALU processing paths. The helpers extract the source to the target
width and apply zero/sign extension to the final width as needed.

- For MOV32, build a 32-bit expr for src and zero-extend it.
- For sign-extending MOVs (s8/s16 to W, or s8/s16 to R), extract the sub-width
  and sign-extend to 32 or 64.
- If the destination is known-constant, clear `dst_reg->bcf_expr` (-1) to avoid
  carrying redundant symbolic nodes.

These routines are only active when `env->bcf.tracking` is set. They are called
from `check_alu_op()` in the relevant MOV/SEXT cases.

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

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 7b6d509c773a..4491d665cc49 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -15959,6 +15959,57 @@ static int adjust_reg_min_max_vals(struct bpf_verifier_env *env,
 	return 0;
 }
 
+static int bcf_mov(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
+		   struct bpf_reg_state *src_reg, u32 sz, bool bit32, bool sext)
+{
+	int src_expr, ext_sz, bitsz = bit32 ? 32 : 64;
+
+	if (!env->bcf.tracking)
+		return 0;
+	if (tnum_is_const(dst_reg->var_off)) {
+		dst_reg->bcf_expr = -1;
+		return 0;
+	}
+
+	src_expr = bcf_reg_expr(env, src_reg, bit32 || sz == 32);
+	if (sz != 32) /* u/s16 u/s8 */
+		src_expr = bcf_extract(env, sz, src_expr);
+
+	if (sext) {
+		ext_sz = bitsz - sz;
+		dst_reg->bcf_expr =
+			bcf_extend(env, ext_sz, bitsz, true, src_expr);
+		if (bit32)
+			bcf_zext_32_to_64(env, dst_reg);
+	} else {
+		ext_sz = 64 - sz;
+		dst_reg->bcf_expr =
+			bcf_extend(env, ext_sz, 64, false, src_expr);
+	}
+	if (dst_reg->bcf_expr < 0)
+		return dst_reg->bcf_expr;
+
+	return 0;
+}
+
+static int bcf_mov32(struct bpf_verifier_env *env, struct bpf_reg_state *dst,
+		     struct bpf_reg_state *src)
+{
+	return bcf_mov(env, dst, src, 32, true, false);
+}
+
+static int bcf_sext32(struct bpf_verifier_env *env, struct bpf_reg_state *dst,
+		      struct bpf_reg_state *src, u32 sz)
+{
+	return bcf_mov(env, dst, src, sz, true, true);
+}
+
+static int bcf_sext64(struct bpf_verifier_env *env, struct bpf_reg_state *dst,
+		      struct bpf_reg_state *src, u32 sz)
+{
+	return bcf_mov(env, dst, src, sz, false, true);
+}
+
 /* check validity of 32-bit and 64-bit arithmetic operations */
 static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 {
@@ -16084,8 +16135,12 @@ static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 						if (no_sext)
 							assign_scalar_id_before_mov(env, src_reg);
 						copy_register_state(dst_reg, src_reg);
-						if (!no_sext)
+						if (!no_sext) {
 							dst_reg->id = 0;
+							err = bcf_sext64(env, dst_reg, src_reg, insn->off);
+							if (err)
+								return err;
+						}
 						coerce_reg_to_size_sx(dst_reg, insn->off >> 3);
 						dst_reg->subreg_def = DEF_NOT_SUBREG;
 					} else {
@@ -16110,8 +16165,12 @@ static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 						 * range otherwise dst_reg min/max could be incorrectly
 						 * propagated into src_reg by sync_linked_regs()
 						 */
-						if (!is_src_reg_u32)
+						if (!is_src_reg_u32) {
 							dst_reg->id = 0;
+							err = bcf_mov32(env, dst_reg, src_reg);
+							if (err)
+								return err;
+						}
 						dst_reg->subreg_def = env->insn_idx + 1;
 					} else {
 						/* case: W1 = (s8, s16)W2 */
@@ -16120,8 +16179,12 @@ static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 						if (no_sext)
 							assign_scalar_id_before_mov(env, src_reg);
 						copy_register_state(dst_reg, src_reg);
-						if (!no_sext)
+						if (!no_sext) {
 							dst_reg->id = 0;
+							err = bcf_sext32(env, dst_reg, src_reg, insn->off);
+							if (err)
+								return err;
+						}
 						dst_reg->subreg_def = env->insn_idx + 1;
 						coerce_subreg_to_size_sx(dst_reg, insn->off >> 3);
 					}
-- 
2.34.1


  parent reply	other threads:[~2025-11-06 12:53 UTC|newest]

Thread overview: 18+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
2025-11-06 12:52 ` [PATCH RFC 01/17] bpf: Add BCF expr and proof rule definitions Hao Sun
2025-11-06 12:52 ` [PATCH RFC 02/17] bpf: Add bcf_checker top-level workflow Hao Sun
2025-11-06 12:52 ` [PATCH RFC 03/17] bpf: Add UAPI fields for BCF proof interaction Hao Sun
2025-11-06 12:52 ` [PATCH RFC 04/17] bpf: Add top-level workflow of bcf_refine() Hao Sun
2025-11-06 12:52 ` [PATCH RFC 05/17] bpf: Add top-level workflow of bcf_track() Hao Sun
2025-11-06 12:52 ` [PATCH RFC 06/17] bpf: Add bcf_match_path() to follow the path suffix Hao Sun
2025-11-06 12:52 ` [PATCH RFC 07/17] bpf: Add bcf_expr management and binding Hao Sun
2025-11-06 12:52 ` Hao Sun [this message]
2025-11-06 12:52 ` [PATCH RFC 09/17] bpf: Track alu operations in bcf_track() Hao Sun
2025-11-06 12:52 ` [PATCH RFC 10/17] bpf: Add bcf_alu() 32bits optimization Hao Sun
2025-11-06 12:52 ` [PATCH RFC 11/17] bpf: Track stack spill/fill in bcf_track() Hao Sun
2025-11-06 12:52 ` [PATCH RFC 12/17] bpf: Track path constraint Hao Sun
2025-11-06 12:52 ` [PATCH RFC 13/17] bpf: Skip state pruning for the parent states Hao Sun
2025-11-06 12:52 ` [PATCH RFC 14/17] bpf: Add mem access bound refinement Hao Sun
2025-11-06 12:52 ` [PATCH RFC 15/17] bpf: Preserve verifier_env and request BCF Hao Sun
2025-11-06 12:52 ` [PATCH RFC 16/17] bpf: Resume verifier env and check proof Hao Sun
2025-11-06 12:52 ` [PATCH RFC 17/17] bpf: Enable bcf for priv users Hao Sun

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20251106125255.1969938-9-hao.sun@inf.ethz.ch \
    --to=sunhao.th@gmail.com \
    --cc=andrii@kernel.org \
    --cc=ast@kernel.org \
    --cc=bpf@vger.kernel.org \
    --cc=daniel@iogearbox.net \
    --cc=eddyz87@gmail.com \
    --cc=hao.sun@inf.ethz.ch \
    --cc=john.fastabend@gmail.com \
    --cc=linux-kernel@vger.kernel.org \
    --cc=martin.lau@linux.dev \
    --cc=song@kernel.org \
    --cc=yonghong.song@linux.dev \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).