On Thu, Sep 21, 2023 at 9:23 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> 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've been thinking in a similar direction as Alexei, overnight. Here
are some raw thoughts.
I think the overall approach with iter verification is sound. If we
loop and see an equivalent state at the entry to next loop iteration,
then it's safe to assume doing many iterations is safe. The problem is
that delayed precision and read marks make this state equivalence
wrong in some case. So we need to find a solution that will ensure
that all precision and read marks are propagated to parent state
before making a decision about convergence.
The idea is to let verifier explore all code paths starting from
iteration #N, except the code paths that lead to looping into
iteration #N+1. I tried to do that with validating NULL case first and
exiting from loop on each iteration (first), but clearly that doesn't
capture all the cases, as Eduard have shown.
So what if we delay convergence state checks (and then further
exploration at iteration #N+1) using BFS instead of DFS? That is, when
we are about to start new iteration and check state convergence, we
enqueue current state to be processed later after all the states that
"belong" to iteration #N are processed.
We should work out exact details on how to do this hybrid BFS+DFS, but
let's think carefully if this will solve the problems?
I think this is conceptually similar to what Alexei proposed above.
Basically, we "unroll" loop verification iteration by iteration, but
make sure that we explore all the branching within iteration #N before
going one iteration deeper.
Let's think if there are any cases which wouldn't be handled. And then
think how to implement this elegantly (e.g., some sort of queue within
a parent state, which sounds similar to this separate "branches"
counter that Alexei is proposing above).
> I'm still doubt range_within() check for is_iter_next_insn() case but
> can't come up with counter example.
