On Tue, Nov 21, 2023 at 7:08 AM Hao Sun <sunhao.th@xxxxxxxxx> wrote: > > 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)) this part looks suspicious, I'll take a look a bit later > 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. Generally speaking, if the verifier reports "REG INVARIANTS VIOLATION" warning above, it doesn't necessarily mean that verifier has some bug. We do know that in some conditions verifier doesn't detect conditions that *will not* be taken, and in such cases we might get reg invariants violation. But in such case verifier will revert to conservative unknown scalar state, which is correct, even if potentially unnecessarily pessimistic. > > Best > Hao Sun
