On Wed, Dec 13, 2023 at 4:08 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > On Wed, 2023-12-13 at 15:30 -0800, Andrii Nakryiko wrote: > [...] > > Yes, thanks, the execution trace above was helpful. Let's try to > > minimize the example here, I'll keep original instruction indices, > > though: > > > > 23: (bf) r5 = r8 ; here we link r5 and r8 together > > 26: (7e) if w8 s>= w0 goto pc+5 ; here it's not always/never > > taken, so w8 and w0 remain imprecise > > 28: (0f) r8 += r8 ; here link between r8 and r5 is broken > > 29: (d6) if w5 s<= 0x1d goto pc+2 ; here we know value of w5 and > > so it's always/never taken, r5 is marked precise > > > > Now, if we look at r5's precision log at this instruction: > > > > 29: (d6) if w5 s<= 0x1d goto pc+2 > > mark_precise: frame0: last_idx 29 first_idx 26 subseq_idx -1 > > mark_precise: frame0: regs=r5 stack= before 28: (0f) r8 += r8 > > mark_precise: frame0: regs=r5 stack= before 27: (4f) r8 |= r8 > > mark_precise: frame0: regs=r5 stack= before 26: (7e) if w8 s>= w0 goto pc+5 > > Sorry, maybe it's time for me to get some sleep, but I don't see an > issue here. The "before" log is printed by backtrack_insn() before > instruction is backtracked. So the following: > > > mark_precise: frame0: regs=r5 stack= before 26: (7e) if w8 s>= w0 goto pc+5 > > Is a state of backtracker before "if w8 s>= w0 ..." is processed. > But running the test case I've shared wider precision trace for > this instruction looks as follows: > > 26: (7e) if w8 s>= w0 goto pc+5 ; R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3)) > R8=scalar(id=2,smax32=1) > 27: (4f) r8 |= r8 ; R8_w=scalar() > 28: (0f) r8 += r8 ; R8_w=scalar() > 29: (d6) if w5 s<= 0x1d goto pc+2 > mark_precise: frame0: last_idx 29 first_idx 26 subseq_idx -1 > mark_precise: frame0: regs=r5 stack= before 28: (0f) r8 += r8 What if we had a checkpoint here and not have a checkpoint at conditional jump instruction? The general point is that the checkpoint has information about linked registers at the very end of the instruction span that it represents, but any intermediate changes will be lost. It's a similar issue to stack access tracking. At some point we know that r3 is actually fp-8, but we will lose it by the time we actually get to the checkpoint. Yet this information is important in the context of some instruction before the checkpoint. I might be missing something as well, my brain is fried from all these verifier issues. > mark_precise: frame0: regs=r5 stack= before 27: (4f) r8 |= r8 > mark_precise: frame0: regs=r5 stack= before 26: (7e) if w8 s>= w0 goto pc+5 > mark_precise: frame0: parent state regs=r5 stack=: > R0_rw=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3)) > R2_w=4 > R3_w=0x1f00000034 > R4_w=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc, > var_off=(0x0; 0x3fffffffc)) > R5_rw=Pscalar(id=2) > R8_rw=scalar(id=2) R10=fp0 > mark_precise: frame0: last_idx 24 first_idx 11 subseq_idx 26 would this all work if we didn't have a checkpoint here? > mark_precise: frame0: regs=r5,r8 stack= before 24: (18) r2 = 0x4 <------ !!! > mark_precise: frame0: regs=r5,r8 stack= before 23: (bf) r5 = r8 > mark_precise: frame0: regs=r8 stack= before 22: (67) r4 <<= 2 > ... > > Note, that right after "if w8 s>= w0 goto pc+5" is processed the > backtracker state is: > > mark_precise: frame0: regs=r5,r8 stack= before 24: (18) r2 = 0x4 > > So both r5 and r8 are accounted for. > > > Note how at this instruction r5 and r8 *WERE* linked together, but we > > already lost this information for backtracking. So we don't mark w8 as > > precise. That's one part of the problem. > > > > The second part is that even if we knew that w8/r8 is precise, should > > we mark w0/r0 as precise? I actually need to think about this some > > more. Right now for conditional jumps we eagerly mark precision for > > both registers only in always/never taken scenarios. > > > > For now just narrowing down the issue, as I'm sure not many people > > followed all the above stuff carefully. > > > > > > P.S. For solving tracking of linked registers we can probably utilize > > instruction history, though technically they can be spread across > > multiple frames, between registers and stack slots, so that's a bit > > tricky. > > For precision back-propagation we currently rely on id values stored > in the parent state, when moving up from child to parent boundary. Everything might be good with linked IDs. But there is a real issue here, let's find what it is.
