Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::3:3 as permitted sender) client-ip=2620:137:e000::3:3;
MIME-Version: 1.0
From:   Hao Sun <sunhao.th@gmail.com>
Date:   Tue, 21 Nov 2023 13:56:57 +0100
Message-ID: <CACkBjsZ-M=1Yj2PQZM7JN4=9rnDLP36fVO35o9fuAvAMKe=9Nw@mail.gmail.com>
Subject: [Bug Report] bpf: reg invariant voilation after JSET
To:     Andrii Nakryiko <andrii@kernel.org>,
        Alexei Starovoitov <ast@kernel.org>,
        Daniel Borkmann <daniel@iogearbox.net>,
        John Fastabend <john.fastabend@gmail.com>,
        Martin KaFai Lau <martin.lau@linux.dev>,
        Song Liu <song@kernel.org>,
        Yonghong Song <yonghong.song@linux.dev>,
        KP Singh <kpsingh@kernel.org>,
        Stanislav Fomichev <sdf@google.com>,
        Jiri Olsa <jolsa@kernel.org>
Cc:     bpf <bpf@vger.kernel.org>,
        Linux Kernel Mailing List <linux-kernel@vger.kernel.org>
Content-Type: text/plain; charset="UTF-8"
Precedence: bulk

Hi,

The following program (reduced) breaks reg invariant:

C Repro: https://pastebin.com/raw/FmM9q9D4

-------- Verifier Log --------
func#0 @0
0: R1=ctx() R10=fp0
0: (18) r8 = 0x3d                     ; R8_w=61
2: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
3: (ce) if w8 s< w0 goto pc+1         ; R0_w=scalar(smax32=61) R8_w=61
4: (95) exit

from 3 to 5: R0_w=scalar(smin=0x800000000000003e,smax=0x7fffffff7fffffff,umin=smin32=umin32=62,umax=0xffffffff7fffffff,umax32=0x7fffffff,var_off=(0x0;
0xffffffff7fffffff)) R8_w=61 R10=fp0
5: R0_w=scalar(smin=0x800000000000003e,smax=0x7fffffff7fffffff,umin=smin32=umin32=62,umax=0xffffffff7fffffff,umax32=0x7fffffff,var_off=(0x0;
0xffffffff7fffffff)) R8_w=61 R10=fp0
5: (45) if r0 & 0xfffffff7 goto pc+2
REG INVARIANTS VIOLATION (false_reg1): range bounds violation
u64=[0x3e, 0x8] s64=[0x3e, 0x8] u32=[0x3e, 0x8] s32=[0x3e, 0x8]
var_off=(0x0, 0x8)
5: R0_w=scalar(var_off=(0x0; 0x8))
6: (dd) if r0 s<= r8 goto pc+1
REG INVARIANTS VIOLATION (false_reg1): range bounds violation
u64=[0x0, 0x8] s64=[0x3e, 0x8] u32=[0x0, 0x8] s32=[0x0, 0x8]
var_off=(0x0, 0x8)
6: R0_w=scalar(var_off=(0x0; 0x8)) R8_w=61
7: (bc) w1 = w0                       ; R0=scalar(var_off=(0x0; 0x8))
R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=8,var_off=(0x0; 0x8))
8: (95) exit

from 6 to 8: safe

from 5 to 8: safe
processed 10 insns (limit 1000000) max_states_per_insn 0 total_states
1 peak_states 1 mark_read 1

The tnum after #5 is correct, but the ranges are incorrect, which seems a bug in
reg_bounds_sync().  Thoughts?

Best
Hao Sun