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.
