On Thu, Sep 21, 2023 at 4:03 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > I repeat the complete example with added instruction numbers in the > end of the email. As of now verifier takes the following paths: > > First: > // First path is for "drained" iterator and is not very interesting. > 0: (b7) r8 = 0 ; R8_w=0 > ... > 2: (b7) r7 = -16 ; R7_w=-16 > ... > 4: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) > ... > 12: (85) call bpf_iter_num_next#63182 > ; R0_w=0 fp-8=iter_num(ref_id=2,state=drained,depth=0) refs=2 > 13: (15) if r0 == 0x0 goto pc+8 > 22: (bf) r1 = r10 > ... > 26: (95) exit > > Second: > // Note: at 13 a first checkpoint with "active" iterator state is reached > // this checkpoint is created for R7=-16 w/o read mark. Thanks for detailed example. The analysis in my previous email was based on C code where I assumed the asm code generated by compiler for if (r6 != 42) would be if (unlikely(r6 != 42)) and fallthrough insn after 'if' insn would be 'r0 = r10'. Now I see that asm matches if (likely(r6 != 42)). I suspect if you use that in C code you wouldn't need to write the test in asm. Just a thought. > from 12 to 13: R0_w=rdonly_mem(id=3,ref_obj_id=2,off=0,imm=0) R6=scalar(id=1) > R7=-16 R8=0 R10=fp0 fp-8=iter_num(ref_id=2,state=active,depth=1) > fp-16=00000000 refs=2 > 13: (15) if r0 == 0x0 goto pc+8 ; R0_w=rdonly_mem(id=3,ref_obj_id=2,off=0,imm=0) refs=2 > 14: (07) r6 += 1 ; R6=scalar() refs=2 > 15: (55) if r6 != 0x2a goto pc+2 ; R6=42 refs=2 > 16: (b7) r7 = -32 ; R7_w=-32 refs=2 > 17: (05) goto pc-8 > 10: (bf) r1 = r10 ; R1_w=fp0 R10=fp0 refs=2 > 11: (07) r1 += -8 > is_iter_next (12): > old: > R0=scalar() R1_rw=fp-8 R6_r=scalar(id=1) R7=-16 R8_r=0 R10=fp0 > fp-8_r=iter_num(ref_id=2,state=active,depth=0) fp-16=00000000 refs=2 > cur: > R0=rdonly_mem(id=3,ref_obj_id=2,off=0,imm=0) R1_w=fp-8 R6=42 R7_w=-32 > R8=0 R10=fp0 fp-8=iter_num(ref_id=2,state=active,depth=1) fp-16=00000000 refs=2 > > hit > 12: safe > // At this point R7=-32 but it still lacks read or precision marks, > // thus states_equal() called from is_state_visited() for is_iter_next_insn() > // branch returns true. (I added some logging to make it clear above) Maybe instead of brute forcing all regs to live and precise we can add iter.depth check to stacksafe() such that depth=0 != depth=1, but depth=1 == depthN ? (and a tweak to iter_active_depths_differ() as well) Then in the above r7 will be 'equivalent', but fp-8 will differ, then the state with r7=-32 won't be pruned and it will address this particular example ? or not ? Even if it does the gut feel that it won't be enough though, but I wanted to mention this to brainstorm, since below: > The "fix" that I have locally is not really a fix. It forces "exact" > states comparisons for is_iter_next_insn() case: > 1. liveness marks are ignored; > 2. precision marks are ignored; > 3. scalars are compared using regs_exact(). is too drastic. > It breaks a number a number of tests, because iterator "entry" states > are no longer equal and upper iteration bound is not tracked: > - iters/simplest_loop that's a clear sign that forcing 1,2,3 is a dead end. Another idea is to add another state.branches specifically for loop body and keep iterating the body until branches==0. Same concept as the verifier uses for the whole prog, but localized to a loop to make sure we don't declare 'equivalent' state until all paths in the loop body are explored.
