On Thu, Nov 9, 2023 at 5:26 PM Alexei Starovoitov <alexei.starovoitov@xxxxxxxxx> wrote: > > On Wed, Nov 8, 2023 at 3:12 PM Andrii Nakryiko <andrii@xxxxxxxxxx> wrote: > > > > > > @@ -15622,11 +15619,11 @@ static int visit_insn(int t, struct bpf_verifier_env *env) > > /* conditional jump with two edges */ > > mark_prune_point(env, t); > > > > - ret = push_insn(t, t + 1, FALLTHROUGH, env, true); > > + ret = push_insn(t, t + 1, FALLTHROUGH | CONDITIONAL, env); > > if (ret) > > return ret; > > > > - return push_insn(t, t + insn->off + 1, BRANCH, env, true); > > + return push_insn(t, t + insn->off + 1, BRANCH | CONDITIONAL, env); > > If I'm reading this correctly, after the first conditional jmp > both fallthrough and branch become sticky with the CONDITIONAL flag. > So all processing after first 'if a == b' insn is running > with loop_ok==true. > If so, all this complexity is not worth it. Let's just remove 'loop_ok' flag. So you mean just always assume loop_ok, right? > > Also > if (ret) return ret; > in the above looks like an existing bug. > It probably should be if (ret < 0) return ret; yeah, probably should be error-handling case > Otherwise it's probably possible to craft a prog where fallthrough > is explored and in such case the branch target will be ignored. > Not a safety issue, since the verifier will walk that path anyway, > but a bug in check_cfg nevertheless.