From: Puranjay Mohan <puranjay@kernel.org>
To: Daniel Borkmann <daniel@iogearbox.net>, eddyz87@gmail.com
Cc: ast@kernel.org, bpf@vger.kernel.org
Subject: Re: [PATCH bpf 2/2] selftests/bpf: Add more precision tracking tests for atomics
Date: Mon, 30 Mar 2026 15:42:11 +0100 [thread overview]
Message-ID: <m2ldf9z8e4.fsf@kernel.org> (raw)
In-Reply-To: <20260330132750.377862-2-daniel@iogearbox.net>
Daniel Borkmann <daniel@iogearbox.net> writes:
> Add verifier precision tracking tests for BPF atomic fetch operations.
> Validate that backtrack_insn correctly propagates precision from the
> fetch dst_reg to the stack slot for atomic64_{fetch_add,xchg,cmpxchg}.
>
> # LDLIBS=-static PKG_CONFIG='pkg-config --static' ./vmtest.sh -- ./test_progs -t verifier_precision
> [...]
> + /etc/rcS.d/S50-startup
> ./test_progs -t verifier_precision
> [ 1.697105] bpf_testmod: loading out-of-tree module taints kernel.
> [ 1.700220] bpf_testmod: module verification failed: signature and/or required key missing - tainting kernel
> [ 1.777043] tsc: Refined TSC clocksource calibration: 3407.986 MHz
> [ 1.777619] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x311fc6d7268, max_idle_ns: 440795260133 ns
> [ 1.778658] clocksource: Switched to clocksource tsc
> #623/1 verifier_precision/bpf_neg:OK
> #623/2 verifier_precision/bpf_end_to_le:OK
> #623/3 verifier_precision/bpf_end_to_be:OK
> #623/4 verifier_precision/bpf_end_bswap:OK
> #623/5 verifier_precision/bpf_load_acquire:OK
> #623/6 verifier_precision/bpf_store_release:OK
> #623/7 verifier_precision/state_loop_first_last_equal:OK
> #623/8 verifier_precision/bpf_cond_op_r10:OK
> #623/9 verifier_precision/bpf_cond_op_not_r10:OK
> #623/10 verifier_precision/bpf_atomic_fetch_add_precision:OK
> #623/11 verifier_precision/bpf_atomic_xchg_precision:OK
> #623/12 verifier_precision/bpf_atomic_cmpxchg_precision:OK
> #623/13 verifier_precision/bpf_atomic_fetch_add_dual_precision:OK
> #623/14 verifier_precision/bpf_atomic_cmpxchg_dual_precision:OK
> #623/15 verifier_precision/bpf_atomic_fetch_add_map_precision:OK
> #623/16 verifier_precision/bpf_atomic_cmpxchg_map_precision:OK
> #623/17 verifier_precision/bpf_neg_2:OK
> #623/18 verifier_precision/bpf_neg_3:OK
> #623/19 verifier_precision/bpf_neg_4:OK
> #623/20 verifier_precision/bpf_neg_5:OK
> #623 verifier_precision:OK
> Summary: 1/20 PASSED, 0 SKIPPED, 0 FAILED
>
> Signed-off-by: Daniel Borkmann <daniel@iogearbox.net>
Reviewed-by: Puranjay Mohan <puranjay@kernel.org>
> ---
> .../selftests/bpf/progs/verifier_precision.c | 207 ++++++++++++++++++
> 1 file changed, 207 insertions(+)
>
> diff --git a/tools/testing/selftests/bpf/progs/verifier_precision.c b/tools/testing/selftests/bpf/progs/verifier_precision.c
> index 1fe090cd6744..6dbd4feda337 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_precision.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_precision.c
> @@ -5,6 +5,13 @@
> #include "../../../include/linux/filter.h"
> #include "bpf_misc.h"
>
> +struct {
> + __uint(type, BPF_MAP_TYPE_ARRAY);
> + __uint(max_entries, 1);
> + __type(key, __u32);
> + __type(value, __u64);
> +} precision_map SEC(".maps");
> +
> SEC("?raw_tp")
> __success __log_level(2)
> __msg("mark_precise: frame0: regs=r2 stack= before 3: (bf) r1 = r10")
> @@ -301,4 +308,204 @@ __naked int bpf_neg_5(void)
> ::: __clobber_all);
> }
>
> +SEC("?raw_tp")
> +__success __log_level(2)
> +__msg("mark_precise: frame0: regs=r2 stack= before 4: (bf) r3 = r10")
> +__msg("mark_precise: frame0: regs=r2 stack= before 3: (db) r2 = atomic64_fetch_add((u64 *)(r10 -8), r2)")
> +__msg("mark_precise: frame0: regs= stack=-8 before 2: (b7) r2 = 0")
> +__msg("mark_precise: frame0: regs= stack=-8 before 1: (7b) *(u64 *)(r10 -8) = r1")
> +__msg("mark_precise: frame0: regs=r1 stack= before 0: (b7) r1 = 8")
> +__naked int bpf_atomic_fetch_add_precision(void)
> +{
> + asm volatile (
> + "r1 = 8;"
> + "*(u64 *)(r10 - 8) = r1;"
> + "r2 = 0;"
> + ".8byte %[fetch_add_insn];" /* r2 = atomic_fetch_add(*(u64 *)(r10 - 8), r2) */
> + "r3 = r10;"
> + "r3 += r2;" /* mark_precise */
> + "r0 = 0;"
> + "exit;"
> + :
> + : __imm_insn(fetch_add_insn,
> + BPF_ATOMIC_OP(BPF_DW, BPF_ADD | BPF_FETCH, BPF_REG_10, BPF_REG_2, -8))
> + : __clobber_all);
> +}
> +
> +SEC("?raw_tp")
> +__success __log_level(2)
> +__msg("mark_precise: frame0: regs=r2 stack= before 4: (bf) r3 = r10")
> +__msg("mark_precise: frame0: regs=r2 stack= before 3: (db) r2 = atomic64_xchg((u64 *)(r10 -8), r2)")
> +__msg("mark_precise: frame0: regs= stack=-8 before 2: (b7) r2 = 0")
> +__msg("mark_precise: frame0: regs= stack=-8 before 1: (7b) *(u64 *)(r10 -8) = r1")
> +__msg("mark_precise: frame0: regs=r1 stack= before 0: (b7) r1 = 8")
> +__naked int bpf_atomic_xchg_precision(void)
> +{
> + asm volatile (
> + "r1 = 8;"
> + "*(u64 *)(r10 - 8) = r1;"
> + "r2 = 0;"
> + ".8byte %[xchg_insn];" /* r2 = atomic_xchg(*(u64 *)(r10 - 8), r2) */
> + "r3 = r10;"
> + "r3 += r2;" /* mark_precise */
> + "r0 = 0;"
> + "exit;"
> + :
> + : __imm_insn(xchg_insn,
> + BPF_ATOMIC_OP(BPF_DW, BPF_XCHG, BPF_REG_10, BPF_REG_2, -8))
> + : __clobber_all);
> +}
> +
> +SEC("?raw_tp")
> +__success __log_level(2)
> +__msg("mark_precise: frame0: regs=r0 stack= before 5: (bf) r3 = r10")
> +__msg("mark_precise: frame0: regs=r0 stack= before 4: (db) r0 = atomic64_cmpxchg((u64 *)(r10 -8), r0, r2)")
> +__msg("mark_precise: frame0: regs= stack=-8 before 3: (b7) r2 = 0")
> +__msg("mark_precise: frame0: regs= stack=-8 before 2: (b7) r0 = 0")
> +__msg("mark_precise: frame0: regs= stack=-8 before 1: (7b) *(u64 *)(r10 -8) = r1")
> +__msg("mark_precise: frame0: regs=r1 stack= before 0: (b7) r1 = 8")
> +__naked int bpf_atomic_cmpxchg_precision(void)
> +{
> + asm volatile (
> + "r1 = 8;"
> + "*(u64 *)(r10 - 8) = r1;"
> + "r0 = 0;"
> + "r2 = 0;"
> + ".8byte %[cmpxchg_insn];" /* r0 = atomic_cmpxchg(*(u64 *)(r10 - 8), r0, r2) */
> + "r3 = r10;"
> + "r3 += r0;" /* mark_precise */
> + "r0 = 0;"
> + "exit;"
> + :
> + : __imm_insn(cmpxchg_insn,
> + BPF_ATOMIC_OP(BPF_DW, BPF_CMPXCHG, BPF_REG_10, BPF_REG_2, -8))
> + : __clobber_all);
> +}
> +
> +/* Regression test for dual precision: Both the fetched value (r2) and
> + * a reread of the same stack slot (r3) are tracked for precision. After
> + * the atomic operation, the stack slot is STACK_MISC. Thus, the ldx at
> + * insn 4 does NOT set INSN_F_STACK_ACCESS. Precision for the stack slot
> + * propagates solely through the atomic fetch's load side (insn 3).
> + */
> +SEC("?raw_tp")
> +__success __log_level(2)
> +__msg("mark_precise: frame0: regs=r2,r3 stack= before 4: (79) r3 = *(u64 *)(r10 -8)")
> +__msg("mark_precise: frame0: regs=r2 stack= before 3: (db) r2 = atomic64_fetch_add((u64 *)(r10 -8), r2)")
> +__msg("mark_precise: frame0: regs= stack=-8 before 2: (b7) r2 = 0")
> +__msg("mark_precise: frame0: regs= stack=-8 before 1: (7b) *(u64 *)(r10 -8) = r1")
> +__msg("mark_precise: frame0: regs=r1 stack= before 0: (b7) r1 = 8")
> +__naked int bpf_atomic_fetch_add_dual_precision(void)
> +{
> + asm volatile (
> + "r1 = 8;"
> + "*(u64 *)(r10 - 8) = r1;"
> + "r2 = 0;"
> + ".8byte %[fetch_add_insn];" /* r2 = atomic_fetch_add(*(u64 *)(r10 - 8), r2) */
> + "r3 = *(u64 *)(r10 - 8);"
> + "r4 = r2;"
> + "r4 += r3;"
> + "r4 &= 7;"
> + "r5 = r10;"
> + "r5 += r4;" /* mark_precise */
> + "r0 = 0;"
> + "exit;"
> + :
> + : __imm_insn(fetch_add_insn,
> + BPF_ATOMIC_OP(BPF_DW, BPF_ADD | BPF_FETCH, BPF_REG_10, BPF_REG_2, -8))
> + : __clobber_all);
> +}
> +
> +SEC("?raw_tp")
> +__success __log_level(2)
> +__msg("mark_precise: frame0: regs=r0,r3 stack= before 5: (79) r3 = *(u64 *)(r10 -8)")
> +__msg("mark_precise: frame0: regs=r0 stack= before 4: (db) r0 = atomic64_cmpxchg((u64 *)(r10 -8), r0, r2)")
> +__msg("mark_precise: frame0: regs= stack=-8 before 3: (b7) r2 = 0")
> +__msg("mark_precise: frame0: regs= stack=-8 before 2: (b7) r0 = 8")
> +__msg("mark_precise: frame0: regs= stack=-8 before 1: (7b) *(u64 *)(r10 -8) = r1")
> +__msg("mark_precise: frame0: regs=r1 stack= before 0: (b7) r1 = 8")
> +__naked int bpf_atomic_cmpxchg_dual_precision(void)
> +{
> + asm volatile (
> + "r1 = 8;"
> + "*(u64 *)(r10 - 8) = r1;"
> + "r0 = 8;"
> + "r2 = 0;"
> + ".8byte %[cmpxchg_insn];" /* r0 = atomic_cmpxchg(*(u64 *)(r10 - 8), r0, r2) */
> + "r3 = *(u64 *)(r10 - 8);"
> + "r4 = r0;"
> + "r4 += r3;"
> + "r4 &= 7;"
> + "r5 = r10;"
> + "r5 += r4;" /* mark_precise */
> + "r0 = 0;"
> + "exit;"
> + :
> + : __imm_insn(cmpxchg_insn,
> + BPF_ATOMIC_OP(BPF_DW, BPF_CMPXCHG, BPF_REG_10, BPF_REG_2, -8))
> + : __clobber_all);
> +}
> +
> +SEC("?raw_tp")
> +__success __log_level(2)
> +__msg("mark_precise: frame0: regs=r1 stack= before 10: (57) r1 &= 7")
> +__msg("mark_precise: frame0: regs=r1 stack= before 9: (db) r1 = atomic64_fetch_add((u64 *)(r0 +0), r1)")
> +__not_msg("falling back to forcing all scalars precise")
> +__naked int bpf_atomic_fetch_add_map_precision(void)
> +{
> + asm volatile (
> + "r1 = 0;"
> + "*(u64 *)(r10 - 8) = r1;"
> + "r2 = r10;"
> + "r2 += -8;"
> + "r1 = %[precision_map] ll;"
> + "call %[bpf_map_lookup_elem];"
> + "if r0 == 0 goto 1f;"
> + "r1 = 0;"
> + ".8byte %[fetch_add_insn];" /* r1 = atomic_fetch_add(*(u64 *)(r0 + 0), r1) */
> + "r1 &= 7;"
> + "r2 = r10;"
> + "r2 += r1;" /* mark_precise */
> + "1: r0 = 0;"
> + "exit;"
> + :
> + : __imm_addr(precision_map),
> + __imm(bpf_map_lookup_elem),
> + __imm_insn(fetch_add_insn,
> + BPF_ATOMIC_OP(BPF_DW, BPF_ADD | BPF_FETCH, BPF_REG_0, BPF_REG_1, 0))
> + : __clobber_all);
> +}
> +
> +SEC("?raw_tp")
> +__success __log_level(2)
> +__msg("mark_precise: frame0: regs=r0 stack= before 12: (57) r0 &= 7")
> +__msg("mark_precise: frame0: regs=r0 stack= before 11: (db) r0 = atomic64_cmpxchg((u64 *)(r6 +0), r0, r1)")
> +__not_msg("falling back to forcing all scalars precise")
> +__naked int bpf_atomic_cmpxchg_map_precision(void)
> +{
> + asm volatile (
> + "r1 = 0;"
> + "*(u64 *)(r10 - 8) = r1;"
> + "r2 = r10;"
> + "r2 += -8;"
> + "r1 = %[precision_map] ll;"
> + "call %[bpf_map_lookup_elem];"
> + "if r0 == 0 goto 1f;"
> + "r6 = r0;"
> + "r0 = 0;"
> + "r1 = 0;"
> + ".8byte %[cmpxchg_insn];" /* r0 = atomic_cmpxchg(*(u64 *)(r6 + 0), r0, r1) */
> + "r0 &= 7;"
> + "r2 = r10;"
> + "r2 += r0;" /* mark_precise */
> + "1: r0 = 0;"
> + "exit;"
> + :
> + : __imm_addr(precision_map),
> + __imm(bpf_map_lookup_elem),
> + __imm_insn(cmpxchg_insn,
> + BPF_ATOMIC_OP(BPF_DW, BPF_CMPXCHG, BPF_REG_6, BPF_REG_1, 0))
> + : __clobber_all);
> +}
> +
> char _license[] SEC("license") = "GPL";
> --
> 2.43.0
next prev parent reply other threads:[~2026-03-30 14:42 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-03-30 13:27 [PATCH bpf 1/2] bpf: Fix incorrect pruning due to atomic fetch precision tracking Daniel Borkmann
2026-03-30 13:27 ` [PATCH bpf 2/2] selftests/bpf: Add more precision tracking tests for atomics Daniel Borkmann
2026-03-30 14:42 ` Puranjay Mohan [this message]
2026-03-30 14:41 ` [PATCH bpf 1/2] bpf: Fix incorrect pruning due to atomic fetch precision tracking Puranjay Mohan
2026-03-30 21:56 ` Daniel Borkmann
2026-03-30 14:45 ` Alexei Starovoitov
2026-03-30 22:02 ` Daniel Borkmann
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=m2ldf9z8e4.fsf@kernel.org \
--to=puranjay@kernel.org \
--cc=ast@kernel.org \
--cc=bpf@vger.kernel.org \
--cc=daniel@iogearbox.net \
--cc=eddyz87@gmail.com \
/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 an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.