On Fri, 2023-09-29 at 17:41 -0700, Alexei Starovoitov wrote:
[...]
> I suspect that neither option A "Exit or Loop" or B "widening"
> are not correct.
> In both cases we will do states_equal() with states that have
> not reached exit and don't have live/precision marks.
I'd like to argue about B "widening" for a bit, as I think it might be
interesting in general, and put A aside for now. The algorithm for
widening looks as follows:
- In is_states_equal() for (sl->state.branches > 0 && is_iter_next_insn()) case:
- Check if states are equal exactly:
- ignore liveness marks on old state;
- demand same type for registers and stack slots;
- ignore precision marks, instead compare scalars using
regs_exact() [this differs from my previous emails, I'm now sure
that for this scheme to be correct regs_exact() is needed].
- If there is an exact match then follow "hit" branch. The idea
being that visiting exactly the same state can't produce new
execution paths (like with graph traversal).
- If there is no exact match but there is some state V which for
which states_equal(V, C) and V and C differ only in inexact
scalars:
- copy C to state C';
- mark range for above mentioned inexact scalars as unbound;
- continue verification from C';
- if C' verification fails discard it and resume verification from C.
The hope here is that guess for "wide" scalars would be correct and
range for those would not matter. In such case C' would be added to
the explored states right after it's creation (as it is a checkpoint),
and later verification would get to the explored C' copy again, so
that exact comparison would prune further traversals.
Unfortunately, this is riddled with a number of technical
complications on implementation side.
What Andrii suggests might be simpler.
> The key aspect of the verifier state pruning is that safe states
> in sl list explored all possible paths.
> Say, there is an 'if' block after iter_destroy.
> The push_stack/pop_stack logic is done as a stack to make sure
> that the last 'if' has to be explored before earlier 'if' blocks are checked.
> The existing bpf iter logic violated that.
> To fix that we need to logically do:
>
> if (is_iter_next_insn(env, insn_idx))
> if (states_equal(env, &sl->state, cur)) {
> if (iter_state->iter.state == BPF_ITER_STATE_DRAINED)
> goto hit;
>
> instead of BPF_ITER_STATE_ACTIVE.
> In other words we need to process loop iter == 0 case first
> all the way till bpf_exit (just like we do right now),
> then process loop iter == 1 and let it exit the loop and
> go till bpf_exit (hopefully state prune will find equal states
> right after exit from the loop).
> then process loop iter == 2 and so on.
> If there was an 'if' pushed to stack during loop iter == 1
> it has to be popped and explored all the way till bpf_exit.
>
> We cannot just replace BPF_ITER_STATE_ACTIVE with DRAINED.
> It would still be ACTIVE with sl->state.branches==0 after that
> state explored all paths to bpf_exit.
This is similar to what Andrii suggests, please correct me if I'm wrong:
> 1. If V and C (using your terminology from earlier, where V is the old
> parent state at some next() call instruction, and C is the current one
> on the same instruction) are different -- we just keep going. So
> always try to explore different input states for the loop.
> 2. But if V and C are equivalent, it's too early to conclude anything.
> So enqueue C for later in a separate BFS queue (and perhaps that queue
> is per-instruction, actually; or maybe even per-state, not sure), and
> keep exploring all the other pending queues from the (global) DFS
> queue, until we get back to state V again. At that point we need to
> start looking at postponed states for that V state. But this time we
> should be sure that precision and read marks are propagated from all
> those terminatable code paths.
More formally, before pruning potential looping states we need to
make sure that all precision and read marks are in place.
To achieve this:
- Process states from env->head while those are available, in case if
potential looping state (is_states_equal()) is reached put it to a
separate queue.
- Once all env->head states are processed the only source for new read
and precision marks is in postponed looping states, some of which
might not be is_states_equal() anymore. Submit each such state for
verification until fixed point is reached (repeating steps for
env->head processing).
