On Wed, Mar 6, 2024 at 5:12 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Tue, 2024-03-05 at 19:19 -0800, Alexei Starovoitov wrote:
> > From: Alexei Starovoitov <ast@xxxxxxxxxx>
>
> [...]
>
> > JCOND stands for conditional pseudo jump.
> > Since goto_or_nop insn was proposed, it may use the same opcode.
> > may_goto vs goto_or_nop can be distinguished by src_reg:
> > code = BPF_JMP | BPF_JCOND
> > src_reg = 0 - may_goto
> > src_reg = 1 - goto_or_nop
> >
> > Acked-by: Andrii Nakryiko <andrii@xxxxxxxxxx>
> > Signed-off-by: Alexei Starovoitov <ast@xxxxxxxxxx>
> > ---
>
> Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx>
>
> [...]
>
> > @@ -14871,11 +14882,36 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
> > int err;
> >
> > /* Only conditional jumps are expected to reach here. */
> > - if (opcode == BPF_JA || opcode > BPF_JSLE) {
> > + if (opcode == BPF_JA || opcode > BPF_JCOND) {
> > verbose(env, "invalid BPF_JMP/JMP32 opcode %x\n", opcode);
> > return -EINVAL;
> > }
> >
> > + if (opcode == BPF_JCOND) {
> > + struct bpf_verifier_state *cur_st = env->cur_state, *queued_st, *prev_st;
> > + int idx = *insn_idx;
> > +
> > + if (insn->code != (BPF_JMP | BPF_JCOND) ||
> > + insn->src_reg != BPF_MAY_GOTO ||
> > + insn->dst_reg || insn->imm || insn->off == 0) {
> > + verbose(env, "invalid may_goto off %d imm %d\n",
> > + insn->off, insn->imm);
> > + return -EINVAL;
> > + }
> > + prev_st = find_prev_entry(env, cur_st->parent, idx);
> > +
> > + /* branch out 'fallthrough' insn as a new state to explore */
> > + queued_st = push_stack(env, idx + 1, idx, false);
> > + if (!queued_st)
> > + return -ENOMEM;
> > +
> > + queued_st->may_goto_depth++;
> > + if (prev_st)
> > + widen_imprecise_scalars(env, prev_st, queued_st);
> > + *insn_idx += insn->off;
> > + return 0;
> > + }
>
> Nit: for other conditional jumps the fallthrough branch is explored first,
> I tried the following and the tests keep passing:
>
> @@ -14901,14 +14901,13 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
> prev_st = find_prev_entry(env, cur_st->parent, idx);
>
> /* branch out 'fallthrough' insn as a new state to explore */
> - queued_st = push_stack(env, idx + 1, idx, false);
> + queued_st = push_stack(env, idx + insn->off + 1, idx, false);
> if (!queued_st)
> return -ENOMEM;
>
> - queued_st->may_goto_depth++;
> + cur_st->may_goto_depth++;
> if (prev_st)
> - widen_imprecise_scalars(env, prev_st, queued_st);
> - *insn_idx += insn->off;
> + widen_imprecise_scalars(env, prev_st, cur_st);
> return 0;
> }
>
> Maybe this is a property worth preserving, wdyt?
My gut feel that may_goto should do what bpf_loop and open coded iters
are doing by exploring the "zero loops" path first.
But I will explore your idea to explore looping states first
in the follow up. It feels like a major change.
If it works for may_goto it should work for bpf_loop too.
Normal conditional jumps are different.
The way compilers layout basic blocks it's beneficial to explore
fall through, since it has a higher chance of state pruning earlier.
For may_goto the "explore zero loop first" feels more critical
for safety.
Thanks for the reviews.
