Re: [PATCH bpf-next v3 04/12] bpf: Track low-32 scalar equality across zero-extending movs

[bot+bpf-ci]

> bpf: Track low-32 scalar equality across zero-extending movs

TL;DR: The comment and changelog claim a zero delta from an add is refused
composition, but a 32-bit add of known zero records the same link as the mov
and composes. Behaviour is sound; the explanation looks inaccurate.

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c

[ ... ]

> @@ -17594,11 +17584,28 @@ static int adjust_reg_min_max_vals(struct bpf_verifier_env *env,
>
>  		if (dst_reg->link_kind) {
>  			/*
> -			 * If the register already went through rX += val
> -			 * we cannot accumulate another val into rx->off.
> +			 * Only the zero-extending link the mov above records,
> +			 * BPF_REG_LINK_ZEXT with delta 0, can take a delta:
> +			 * (u32)((u32)(base + 0) + off) is (u32)(base + off).
> +			 * The add has to be 32-bit as well, since a 64-bit one
> +			 * parts company with the link once the low half wraps.
> +			 *
> +			 * Everything else still drops the link. A zero delta
> +			 * reached by an add rather than by the mov, say "r1 +=
> +			 * r3" with r3 known to be 0, has already spent its
> +			 * delta; composing onto it keeps a link alive across a
> +			 * loop's increments, and since the delta is compared
> +			 * for equality, every value the loop reaches becomes a
> +			 * state of its own and stops pruning.
>  			 */
> +			if (dst_reg->link_kind != BPF_REG_LINK_ZEXT || !alu32 ||
> +			    dst_reg->delta) {
> +				/* also the target of the two gotos above */
>  clear_id:
> -			bpf_clear_scalar_id(dst_reg);
> +				bpf_clear_scalar_id(dst_reg);
> +			} else {
> +				dst_reg->delta = off;
> +			}
>  		} else {
>  			if (alu32)
>  				dst_reg->link_kind = BPF_REG_LINK_ZEXT;

The comment says a zero delta "reached by an add rather than by the mov"
has already spent its delta, and the commit message says allowing
composition onto "a zero delta that an add produced rather than the mov
still costs 1176 -> 1196".  Can this test actually tell the two apart?

A 32-bit add or sub of a known zero ("w1 += 0", "w1 -= 0", or "w1 += w3"
with w3 known to be 0) on a register that has an id but no link_kind goes
through the else arm quoted above and records:

    dst_reg->link_kind = BPF_REG_LINK_ZEXT;
    dst_reg->delta = off;    /* off == 0 */

That is the same state the mov records, so a following "w1 += 1" passes the
"dst_reg->link_kind != BPF_REG_LINK_ZEXT || !alu32 || dst_reg->delta" test
and composes.

Only the 64-bit example from the comment ("r1 += r3", which records
BPF_REG_LINK_FULL) is actually refused.

The result is still sound, since (u32)((u32)(base + 0) + off) is
(u32)(base + off).  Should the comment and the changelog limit the claim to
64-bit adds, or does the mov-produced link need to be made distinguishable
from the add-produced one?


---
AI reviewed your patch. Please fix the bug or email reply why it's not a bug.
See: https://github.com/kernel-patches/vmtest/blob/master/ci/claude/README.md

CI run summary: https://github.com/kernel-patches/bpf/actions/runs/39458500836