bpf: Finish the insn in the state that maybe_fork_scalars() splits off

When a register is -1 or 0, maybe_fork_scalars() splits the state in two
before an 'and' or an 'or' with a constant. The result is more accurate for
each value alone. The verifier continues with -1. It pushes a copy of the
state with 0 and verifies the copy later, from the same insn.

           today                              this patch

  N:   r1 &= 8    r1 is -1 or 0      N:   r1 &= 8    r1 is -1 or 0
        /     \                            /     \
    r1 = -1   r1 = 0                   r1 = -1   r1 = 0
    r1 &= 8   push to N                r1 &= 8   r1 &= 8
       |                                  |      push to N+1
  N+1: ...                           N+1: ...

At insn N the copy is a part of the state that it came from: 0 is in
[-1, 0]. If pruning compares the two states, it drops the copy, and no one
verifies the case r1 = 0.

The first state has branches that are not explored. Usually pruning does
not use such states. In a loop that scalar evolution counted it does, and
the head of such a loop always keeps its state. Thus a fork at the head of
a counted loop loses the case r1 = 0:

     r9 = a map value of 8 bytes
     r6 = -1
  1: r6 &= 8                  r6 is -1 or 0, only -1 is verified: 8
     r6 ^= 8                  0. It is 8 when r6 was 0.
     r1 = r9
     r1 += r6
     r0 = *(u8 *)(r1 + 0)
     r6 = -1 or 0
     r7 += 1
     if r7 < 100 goto 1b

  from 11 to 11: safe

The verifier accepts this prog. The prog reads the byte that follows the
map value. With a constant of 64 Tbyte in a register it reads an address
that is not mapped, and the kernel crashes.

Do the insn in the copy too, and push the copy to the next insn. All other
code that pushes a state does the same.

No verdict changes in selftests, Cilium and scx. Each fork processes one
insn less, and the sequence in which the verifier explores states changes
slightly. 62 of 161 progs of Cilium process a different number of insns,
from -0.7% to +3.3%. The total is 986970 -> 987013. 2 of 563 progs of scx
process one insn less.

Fixes: 6ccf49f79327 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261027190314.1440199-17-alexei.starovoitov@gmail.com

1 files changed, 18 insertions, 9 deletions

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 8139e41ace00..02b2915f0014 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -17289,11 +17289,14 @@ static bool is_safe_to_compute_dst_reg_range(struct bpf_insn *insn,
 	}
 }
 
+static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env, struct bpf_insn *insn,
+				      struct bpf_reg_state *dst_reg, struct bpf_reg_state src_reg);
+
 static int maybe_fork_scalars(struct bpf_verifier_env *env, struct bpf_insn *insn,
-			      struct bpf_reg_state *dst_reg)
+			      struct bpf_reg_state *dst_reg, const struct bpf_reg_state *src_reg)
 {
 	struct bpf_verifier_state *branch;
-	struct bpf_reg_state *regs;
+	struct bpf_reg_state *reg;
 	bool alu32;
 
 	if (reg_smin(dst_reg) == -1 && reg_smax(dst_reg) == 0)
@@ -17303,19 +17306,25 @@ static int maybe_fork_scalars(struct bpf_verifier_env *env, struct bpf_insn *ins
 	else
 		return 0;
 
-	branch = push_stack(env, env->insn_idx, env->insn_idx, false);
+	branch = push_stack(env, env->insn_idx + 1, env->insn_idx, false);
 	if (IS_ERR(branch))
 		return PTR_ERR(branch);
 
-	regs = branch->frame[branch->curframe]->regs;
+	reg = &branch->frame[branch->curframe]->regs[insn->dst_reg];
 	if (alu32) {
-		__mark_reg32_known(&regs[insn->dst_reg], 0);
+		__mark_reg32_known(reg, 0);
 		__mark_reg32_known(dst_reg, -1ull);
 	} else {
-		__mark_reg_known(&regs[insn->dst_reg], 0);
+		__mark_reg_known(reg, 0);
 		__mark_reg_known(dst_reg, -1ull);
 	}
-	return 0;
+	/*
+	 * The insn is done with in the branch too, and what gets to the next insn is a state
+	 * like any other. At this insn the branch is a part of the state that is looked at:
+	 * it must not be compared with it.
+	 */
+	clear_scalar_id(reg);
+	return adjust_scalar_min_max_vals(env, insn, reg, *src_reg);
 }
 
 /* WARNING: This function does calculations on 64-bit values, but the actual
@@ -17420,7 +17429,7 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 		break;
 	case BPF_AND:
 		if (tnum_is_const(src_reg.var_off)) {
-			ret = maybe_fork_scalars(env, insn, dst_reg);
+			ret = maybe_fork_scalars(env, insn, dst_reg, &src_reg);
 			if (ret)
 				return ret;
 		}
@@ -17431,7 +17440,7 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 		break;
 	case BPF_OR:
 		if (tnum_is_const(src_reg.var_off)) {
-			ret = maybe_fork_scalars(env, insn, dst_reg);
+			ret = maybe_fork_scalars(env, insn, dst_reg, &src_reg);
 			if (ret)
 				return ret;
 		}