Re: [PATCH v6 bpf-next 1/4] bpf: Introduce may_goto instruction

[Eduard Zingerman <eddyz87@gmail.com>]

On Tue, 2024-03-05 at 19:19 -0800, Alexei Starovoitov wrote:
> From: Alexei Starovoitov <ast@kernel.org>

[...]

> 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@kernel.org>
> Signed-off-by: Alexei Starovoitov <ast@kernel.org>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

> @@ -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?

[...]