Re: [PATCH bpf-next] bpf: Relax precision marking in open coded iters and may_goto loop.

[Eduard Zingerman <eddyz87@gmail.com>]

On Wed, 2024-05-22 at 14:13 -0700, Alexei Starovoitov wrote:

[...]

> Agree with this conclusion.
> As discussed offlist we can add a check that
> Si->parent->parent...->parent == Sk.
> to make the algorithm "by the book".
> I'll play with that.

Actually, I don't think this is necessary, here is the code for
update_loop_entry():

    static void update_loop_entry(struct bpf_verifier_state *cur,
                                  struct bpf_verifier_state *hdr)
    {
            struct bpf_verifier_state *cur1, *hdr1;

            cur1 = get_loop_entry(cur) ?: cur;
            hdr1 = get_loop_entry(hdr) ?: hdr;
            if (hdr1->branches && hdr1->dfs_depth <= cur1->dfs_depth) {
                    cur->loop_entry = hdr;
                    hdr->used_as_loop_entry = true;
            }
    }
    
It relies on the following properties:
- every state in the current DFS path (except current)
  has branches > 0;
- states not in the DFS path are either:
  - in explored_states, are fully explored and have branches == 0;
  - in env->stack, are not yet explored and have branches == 0
    (and also not reachable from is_state_visited()).

So, I don't think there is a need to check that hdr1 is in the parent
chain for cur1.