Re: [syzbot ci] Re: bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Paul Chaignon <paul.chaignon@gmail.com>]

On Fri, Aug 15, 2025 at 01:24:40AM -0700, syzbot ci wrote:
> syzbot ci has tested the following series
> 
> [v1] bpf: Use tnums for JEQ/JNE is_branch_taken logic
> https://lore.kernel.org/all/ba9baf9f73d51d9bce9ef13778bd39408d67db79.1755098817.git.paul.chaignon@gmail.com
> * [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic
> * [PATCH bpf-next 2/2] selftests/bpf: Tests for is_scalar_branch_taken tnum logic
> 
> and found the following issue:
> WARNING in reg_bounds_sanity_check
> 
> Full report is available here:
> https://ci.syzbot.org/series/fd950b40-1da8-44b1-bd12-4366e4a354b1
> 
> ***
> 
> WARNING in reg_bounds_sanity_check
> 
> tree:      bpf-next
> URL:       https://kernel.googlesource.com/pub/scm/linux/kernel/git/bpf/bpf-next.git
> base:      07866544e410e4c895a729971e4164861b41fad5
> arch:      amd64
> compiler:  Debian clang version 20.1.7 (++20250616065708+6146a88f6049-1~exp1~20250616065826.132), Debian LLD 20.1.7
> config:    https://ci.syzbot.org/builds/c4af872a-9b42-4821-a832-941921acc063/config
> C repro:   https://ci.syzbot.org/findings/8dfae15e-cda5-4fa6-8f95-aab106ebd860/c_repro
> syz repro: https://ci.syzbot.org/findings/8dfae15e-cda5-4fa6-8f95-aab106ebd860/syz_repro
> 
> verifier bug: REG INVARIANTS VIOLATION (true_reg1): range bounds violation u64=[0xffffdfcd, 0xffffffffffffdfcc] s64=[0x80000000ffffdfcd, 0x7fffffffffffdfcc] u32=[0xffffdfcd, 0xffffdfcc] s32=[0xffffdfcd, 0xffffdfcc] var_off=(0xffffdfcc, 0xffffffff00000000)

My is_branch_taken patch fixes some invariant violations. The test from
the second patch is even adapted from a syzkaller reproduction manually
extracted from logs at [1]. Ironically, by improving the branch
detection, we can also sometimes degrade state pruning (as discussed in
the first patch) which causes the exploration of new branches.

All that to say the current syzkaller repro is not directly caused by
my patch. It simply causes a new branch to be explored, and there is a
different kind of invariant violation on that branch. The full (sk_skb)
program is below [2], but the end of verifier logs are enough to
understand what's happening:

    12: (2f) r5 *= r6                  ; R5_w=scalar(smax=0x7ffffffffffffffc,umax=0xfffffffffffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; 0xfffffffffffffffc)) R6_w=0x9fe719f2
    13: (65) if r7 s> 0x1 goto pc-7    ; R7_w=scalar(id=67,smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
    14: (07) r7 += -8243               ; R7=scalar(smin=smin32=-8243,smax=smax32=-8242,umin=0xffffffffffffdfcd,umax=0xffffffffffffdfce,umin32=0xffffdfcd,umax32=0xffffdfce,var_off=(0xffffffffffffdfcc; 0x3))
    15: (1e) if w5 == w7 goto pc+0
    verifier bug: REG INVARIANTS VIOLATION (true_reg1): range bounds violation u64=[0xffffdfcd, 0xffffffffffffdfcc] s64=[0x80000000ffffdfcd, 0x7fffffffffffdfcc] u32=[0xffffdfcd, 0xffffdfcc] s32=[0xffffdfcd, 0xffffdfcc] var_off=(0xffffdfcc, 0xffffffff00000000)

The invariant violation follows the same pattern as usual: the verifier
walks a dead branch, uses it to improve ranges, and ends up with
inconsistent ranges. In this case, the u32 min value is larger than the
u32 max value. We can notice that the condition at instruction 15 is
always false because, if w5 and w7 were equal, the intersection of their
tnums would give us a constant (0xffffdfcc) that isn't within R7's u32
range. Hence, w5 and w7 can't be equal.

I have a patch to potentially fix this, but I'm still testing it and
would prefer to send it separately as it doesn't really relate to my
current patchset.

1 - https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf
2 - syzkaller program:

    r5 = *(u32 *)(r1 +112)
    r3 = *(u32 *)(r1 +108)
    r0 = r10
    r0 += 85328110
    if w3 != w0 goto +1
    if w5 == 0x0 goto +0
    r6 = *(u16 *)(r1 +62)
    r7 = r0
    if w5 > 0x2007ff0f goto +7
    r6 <<= 32
    w6 -= 1612244494
    r0 = r5
    r5 *= r6
    if r7 s> 0x1 goto -7
    r7 += -8243
    if w5 == w7 goto +0
    r4 = r5
    r4 += -458748
    if r3 < r4 goto +1
    exit
    if r0 == 0x0 goto +0

[...]