On Tue, Mar 5, 2024 at 7:19 PM Alexei Starovoitov
<alexei.starovoitov@xxxxxxxxx> wrote:
>
> From: Alexei Starovoitov <ast@xxxxxxxxxx>
>
> Introduce may_goto instruction that from the verifier pov is similar to
> open coded iterators bpf_for()/bpf_repeat() and bpf_loop() helper, but it
> doesn't iterate any objects.
> In assembly 'may_goto' is a nop most of the time until bpf runtime has to
> terminate the program for whatever reason. In the current implementation
> may_goto has a hidden counter, but other mechanisms can be used.
> For programs written in C the later patch introduces 'cond_break' macro
> that combines 'may_goto' with 'break' statement and has similar semantics:
> cond_break is a nop until bpf runtime has to break out of this loop.
> It can be used in any normal "for" or "while" loop, like
>
> for (i = zero; i < cnt; cond_break, i++) {
>
> The verifier recognizes that may_goto is used in the program, reserves
> additional 8 bytes of stack, initializes them in subprog prologue, and
> replaces may_goto instruction with:
> aux_reg = *(u64 *)(fp - 40)
> if aux_reg == 0 goto pc+off
> aux_reg -= 1
> *(u64 *)(fp - 40) = aux_reg
>
> may_goto instruction can be used by LLVM to implement __builtin_memcpy,
> __builtin_strcmp.
>
> may_goto is not a full substitute for bpf_for() macro.
> bpf_for() doesn't have induction variable that verifiers sees,
> so 'i' in bpf_for(i, 0, 100) is seen as imprecise and bounded.
>
> But when the code is written as:
> for (i = 0; i < 100; cond_break, i++)
> the verifier see 'i' as precise constant zero,
> hence cond_break (aka may_goto) doesn't help to converge the loop.
> A static or global variable can be used as a workaround:
> static int zero = 0;
> for (i = zero; i < 100; cond_break, i++) // works!
>
> may_goto works well with arena pointers that don't need to be bounds
> checked on access. Load/store from arena returns imprecise unbounded
> scalar and loops with may_goto pass the verifier.
>
> Reserve new opcode BPF_JMP | BPF_JCOND for may_goto insn.
> 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>
> ---
> include/linux/bpf_verifier.h | 2 +
> include/uapi/linux/bpf.h | 5 +
> kernel/bpf/core.c | 1 +
> kernel/bpf/disasm.c | 4 +
> kernel/bpf/verifier.c | 163 +++++++++++++++++++++++++++------
> tools/include/uapi/linux/bpf.h | 5 +
> 6 files changed, 150 insertions(+), 30 deletions(-)
>
[...]
> @@ -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) {
Why rejecting insn->off == 0? It's still a legal instruction, even if
not super useful in practice. insn->off == -1 is also weird, but legal
(and not rejected in this case).
> + 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;
> + }
> +
> /* check src2 operand */
> err = check_reg_arg(env, insn->dst_reg, SRC_OP);
> if (err)
[...]
