Hi, The following program (reduced) breaks reg invariant: C Repro: https://pastebin.com/raw/SRQJYx91 -------- Verifier Log -------- func#0 @0 0: R1=ctx() R10=fp0 0: (b7) r0 = -2 ; R0_w=-2 1: (37) r0 /= 1 ; R0_w=scalar() 2: (bf) r8 = r0 ; R0_w=scalar(id=1) R8_w=scalar(id=1) 3: (56) if w8 != 0xfffffffe goto pc+4 ; R8_w=scalar(id=1,smin=0x80000000fffffffe,smax=0x7ffffffffffffffe,umin=umin32=0xfffffffe,umax=0xfffffffffffffffe,smin32=-2,smax32=-2,umax32=0xfffffffe,var_off=(0xfffffffe; 0xffffffff00000000)) 4: (65) if r8 s> 0xd goto pc+3 ; R8_w=scalar(id=1,smin=0x80000000fffffffe,smax=13,umin=umin32=0xfffffffe,umax=0xfffffffffffffffe,smin32=-2,smax32=-2,umax32=0xfffffffe,var_off=(0xfffffffe; 0xffffffff00000000)) 5: (b7) r4 = 2 ; R4_w=2 6: (dd) if r8 s<= r4 goto pc+1 REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xfffffffe, 0xd] s64=[0xfffffffe, 0xd] u32=[0xfffffffe, 0xd] s32=[0x3, 0xfffffffe] var_off=(0xfffffffe, 0x0) 6: R4_w=2 R8_w=0xfffffffe 7: (cc) w8 s>>= w0 ; R0=0xfffffffe R8=scalar() 8: (77) r0 >>= 32 ; R0_w=0 9: (57) r0 &= 1 ; R0_w=0 10: (95) exit from 6 to 8: safe from 4 to 8: safe from 3 to 8: safe processed 14 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 Besides, the verifier enforces the return value of some prog types to be zero, the bug may lead to programs with arbitrary values loaded. Best Hao Sun
