On Tue, Nov 21, 2023 at 4:57 AM Hao Sun <sunhao.th@xxxxxxxxx> wrote: > > 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? > It would be great if in addition to reporting the bug and repro program, you could also try to analyse why this is happening and suggest fixes in the verifier. As I mentioned in another email, when we see REG INVARIANTS VIOLATION, verifier reverts to conservative unknown scalar register state. We should try to avoid this pessimistic outcome, but generally speaking it should not be a critical bug. > Best > Hao Sun
