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
