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
next prev 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).