Re: [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Eduard Zingerman <eddyz87@gmail.com>]

On Wed, 2025-08-13 at 17:34 +0200, Paul Chaignon wrote:
> In the following toy program (reg states minimized for readability), R0
> and R1 always have different values at instruction 6. This is obvious
> when reading the program but cannot be guessed from ranges alone as
> they overlap (R0 in [0; 0xc0000000], R1 in [1024; 0xc0000400]).
> 
>   0: call bpf_get_prandom_u32#7  ; R0_w=scalar()
>   1: w0 = w0                     ; R0_w=scalar(var_off=(0x0; 0xffffffff))
>   2: r0 >>= 30                   ; R0_w=scalar(var_off=(0x0; 0x3))
>   3: r0 <<= 30                   ; R0_w=scalar(var_off=(0x0; 0xc0000000))
>   4: r1 = r0                     ; R1_w=scalar(var_off=(0x0; 0xc0000000))
>   5: r1 += 1024                  ; R1_w=scalar(var_off=(0x400; 0xc0000000))
>   6: if r1 != r0 goto pc+1
> 
> Looking at tnums however, we can deduce that R1 is always different from
> R0 because their tnums don't agree on known bits. This patch uses this
> logic to improve is_scalar_branch_taken in case of BPF_JEQ and BPF_JNE.
> 
> This change has a tiny impact on complexity, which was measured with
> the Cilium complexity CI test. That test covers 72 programs with
> various build and load time configurations for a total of 970 test
> cases. For 80% of test cases, the patch has no impact. On the other
> test cases, the patch decreases complexity by only 0.08% on average. In
> the best case, the verifier needs to walk 3% less instructions and, in
> the worst case, 1.5% more. Overall, the patch has a small positive
> impact, especially for our largest programs.
> 
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

Note: CI reports verifier performance differences for Meta internal programs:
      https://github.com/kernel-patches/bpf/actions/runs/16942287206
      But I can't confirm the difference after running veristat for these programs,
      looks like a CI glitch.

[...]