[Bug Report] bpf: reg invariant voilation after JSET

From: Hao Sun
Date: Tue Nov 21 2023 - 07:57:13 EST


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