Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

Shung-Hsi Yu
2026-03-23T12:23:38Z

On Fri, Mar 20, 2026 at 05:49:44PM +0100, Paul Chaignon wrote:
> From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
>
> This patch fixes the invariant violations that can happen after we
> refine ranges & tnum based on an incorrectly-detected branch condition.
> For example, the branch is always true, but we miss it in
> is_branch_taken; we then refine based on the branch being false and end
> up with incoherent ranges (e.g. umax < umin).
>
> To avoid this, we can simulate the refinement on both branches. More
> specifically, this patch simulates both branches taken using
> regs_refine_cond_op and reg_bounds_sync. If the resulting register
> states are ill-formed on one of the branches, is_branch_taken can mark
> that branch as "never taken".
>
> On a more formal note, we can deduce a branch is not taken when
> regs_refine_cond_op or reg_bounds_sync returns an ill-formed state
> because the branch operators are sound (formally verified). Soundness

Nit1: would be nice to get a link or at least mentioning of Agni,
otherwise it is not obvious where this claim comes from. And that seems
like a healthy dose of project promotion, too.

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

...
> +/* Learn more information about live branches by simulating both branches being
> + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when

Nit2: while this statement is very specific, "sound" is a rather
uncommon vocabulary in current codebase, I see no such usage.

$ git grep -A1 -ie sound -- kernel/bpf/ Documentation/bpf/
Documentation/bpf/kfuncs.rst: no warning will not be a common occurrence or take place without sound
Documentation/bpf/kfuncs.rst- justification, but it is a possibility that must be accepted if one is to

> + * the branch is taken, if it produces ill-formed register bounds, it must mean
> + * that the branch is dead.
> + */
> +static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
> +{
...