On Wed, Dec 13, 2023 at 2:25 AM Hao Sun <sunhao.th@xxxxxxxxx> wrote: > > On Wed, Dec 13, 2023 at 1:51 AM Andrii Nakryiko > <andrii.nakryiko@xxxxxxxxx> wrote: > > > > On Mon, Dec 11, 2023 at 7:31 AM Hao Sun <sunhao.th@xxxxxxxxx> wrote: > > > > > > Hi, > > > > > > The verifier incorrectly prunes a path expected to be executed at > > > runtime. In the following program, the execution path is: > > > from 6 to 8 (taken) -> from 11 to 15 (taken) -> from 18 to 22 > > > (taken) -> from 26 to 27 (fall-through) -> from 29 to 30 > > > (fall-through) > > > The verifier prunes the checking path at #26, skipping the actual > > > execution path. > > > > > > 0: (18) r2 = 0x1a000000be > > > 2: (bf) r5 = r1 > > > 3: (bf) r8 = r2 > > > 4: (bc) w4 = w5 > > > 5: (85) call bpf_get_current_cgroup_id#680112 > > > 6: (36) if w8 >= 0x69 goto pc+1 > > > 7: (95) exit > > > 8: (18) r4 = 0x52 > > > 10: (84) w4 = -w4 > > > 11: (45) if r0 & 0xfffffffe goto pc+3 > > > 12: (1f) r8 -= r4 > > > 13: (0f) r0 += r0 > > > 14: (2f) r4 *= r4 > > > 15: (18) r3 = 0x1f00000034 > > > 17: (c4) w4 s>>= 29 > > > 18: (56) if w8 != 0xf goto pc+3 > > > 19: r3 = bswap32 r3 > > > 20: (18) r2 = 0x1c > > > 22: (67) r4 <<= 2 > > > 23: (bf) r5 = r8 > > > 24: (18) r2 = 0x4 > > > 26: (7e) if w8 s>= w0 goto pc+5 > > > 27: (4f) r8 |= r8 > > > 28: (0f) r8 += r8 > > > 29: (d6) if w5 s<= 0x1d goto pc+2 > > > 30: (18) r0 = 0x4 ; incorrectly pruned here > > > > > > > > > 32: (95) exit > > > [...] > > > > > > Here is a reduced C repro, maybe someone else can shed some light on this. > > > C repro: https://pastebin.com/raw/chrshhGQ > > > > So you claim is that > > > > 30: (18) r0 = 0x4 ; incorrectly pruned here > > > > > > Can you please show a detailed code patch in which we do reach 30 > > actually? I might have missed it, but so far it look like verifier is > > doing everything right. > > > > I tried to convert the repro to a valid test case in inline asm, but seems > JSET (if r0 & 0xfffffffe goto pc+3) is currently not supported in clang-17. > Will try after clang-18 is released. JSET has nothing to do with the issue, it's just a distraction, I'm not sure why you bring JSET into the discussion at all. Your repro can be actually much smaller, as it was really hard to follow which parts are important and which weren't. If you can try to minimize repros, it will definitely help with analysis for future issues. > > #30 is expected to be executed, see below where everything after ";" is > the runtime value: > ... > 6: (36) if w8 >= 0x69 goto pc+1 ; w8 = 0xbe, always taken > ... > 11: (45) if r0 & 0xfffffffe goto pc+3 ; r0 = 0x616, taken > ... > 18: (56) if w8 != 0xf goto pc+3 ; w8 not touched, taken > ... > 23: (bf) r5 = r8 ; w5 = 0xbe > 24: (18) r2 = 0x4 > 26: (7e) if w8 s>= w0 goto pc+5 ; non-taken > 27: (4f) r8 |= r8 > 28: (0f) r8 += r8 > 29: (d6) if w5 s<= 0x1d goto pc+2 ; non-taken > 30: (18) r0 = 0x4 ; executed > > Since the verifier prunes at #26, #30 is dead and eliminated. So, #30 > is executed after manually commenting out the dead code rewrite pass. > > From my understanding, I think r0 should be marked as precise when > first backtrack from #29, because r5 range at this point depends on w0 > as r8 and r5 share the same id at #26. 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 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.
