Re: [BUG] verifier escape with iteration helpers (bpf_loop, ...)

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2023-09-21 at 05:56 -0700, Alexei Starovoitov wrote:
[...]
> 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.

Thank you this does change test behavior, however compiler still decides
to partially unroll the loop for whatever reason. Will stick to asm
snippets for now.

> 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 ?

This does help for the particular example, however a simple
modification can still trick the verifier:

     ...
     r6 = bpf_get_current_pid_tgid()
     bpf_iter_num_new(&fp[-8], 0, 10)
+    bpf_iter_num_next(&fp[-8])
     while (bpf_iter_num_next(&fp[-8])) {
       ...
     }
     ...

> 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.

I'm not sure I understand the idea. If we count branches there always
would be back-edges leading to new branches. Or do you suggest to not
prune "equivalent" loop states until all basic blocks in the loop are
visited? (So that all read marks are propagated and probably all
precision marks).

I'm still doubt range_within() check for is_iter_next_insn() case but
can't come up with counter example.