On Wed, Sep 27, 2023 at 6:09 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
> {
> ...
> while (sl) {
> ...
> if (sl->state.branches) {
> ...
> if (is_iter_next_insn(env, insn_idx)) {
> if (states_equal(env, &sl->state, cur)) {
> ...
> iter_state = &func(env, iter_reg)->stack[spi].spilled_ptr;
> if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE) {
> + // Don't want to proceed with 'cur' verification,
> + // push it to iters queue to check again if states
> + // are still equal after env->head is exahusted.
> + if (env->stack_size != 0)
> + push_iter_stack(env, cur, ...);
> goto hit;
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.
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.
