bpf: Do not intersect with current register range on clamp

scev.c:bpf_clamp_scev_regs() is called each time verifier returns to a
loop header via a backedge. It's purpose is to re-establish computed
variable ranges for registers with linear SCEVs.
It can be defined as:
- For each register R with linear SCEV compute:
  - loop_range(R) := entry_range(R) * iterations_count
  - range(R) := range(R) ∩ loop_range(R)

Such formulation is necessary to avoid ranges over-approximation in
examples like below:

        r1 = 0;              SCEVs: r1 = (linear r1 1)
        r3 = 0;                     r3 = (linear r3 1)
  loop:   r3 += 1;
          r1 += 1;
          if r1 < 5 goto loop;
        r0 = 0;
        exit;

- At loop entry r3 is widened to be in a range r3 ∈ {0,1,2,3,4}.
- After increment it becomes r3 ∈ {1,2,3,4,5}.
- On a second iteration the bpf_clamp_scev_regs() forces r3 to become
  r3 ∈ {1,2,3,4}. W/o clamping logic r3 range wouldn't shrink
  preventing loop from converging in states.c:states_equal().

However, intersection logic might lead to assigning an empty range to
a register, as in example below:

        r1 = 0;           verification
        r3 = 0;               path
  loop:   r3 += 1;              | <---------.
          if r3 != 5 goto +0;   | r3 ∈ {5}  |
          r1 += 1;              |           |
          if r1 != 5 goto loop; '-----------'
        r0 = 0;
        exit;

- At header r3 ∈ {0,1,2,3,4}.
- While exploring the branch `if r3 != 5 goto ...` with r3 ∈ {5}.
- On a second iteration:

    r3 := {0,1,2,3,4} ∩ {5} = ∅

Which stops verification with the following error:

  verifier bug: scev clamp produced empty range for r3

Technically this means that the current verification path is
impossible at runtime and should not be traced further.

This commit mitigates the above by removing the intersection logic,
the function is now defined as:
- For each register R with linear SCEV compute:
  - range(R) := entry_range(R) * iterations_count

This is still sound, provided that SCEV expressions loop execution
counts are correct.

Fixes: 6ccf49f793 ("bpf: Use SCEV to widen bounded loops")
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261026-scev-simpler-clamp-v2-2-f373aec9825f@gmail.com

kernel/bpf/scev.c

@@ -2896,12 +2896,6 @@ int bpf_clamp_scev_regs(struct bpf_verifier_env *env, struct bpf_func_state *cur
 			continue;
 
 		linear_bounds(entry_reg, max_header_count, &coefs, &bounds);
-		bounds.r64 = cnum64_intersect(reg->r64, bounds.r64);
-		bounds.r32 = cnum32_intersect(reg->r32, bounds.r32);
-		if (cnum64_is_empty(bounds.r64)) {
-			verifier_bug(env, "scev clamp produced empty range for r%d", r);
-			return -EFAULT;
-		}
 		if (log->level & BPF_LOG_LEVEL2) {
 			bpf_log(log, "loop header at %d, clamping ", insn_idx);
 			log_reg(env, r);

tools/testing/selftests/bpf/progs/verifier_scev.c

@@ -1592,7 +1592,7 @@ __msg_next("  r0=(+ r0 -1) / (linear (+ r0 -1) -1)")
 __msg("loop header at 1, header_count is 3 ")
 __msg("loop header at 1, widening r0 to 1..3 step 1")
 __msg("1: R0=scalar(smin=umin=smin32=umin32=1,smax=umax=smax32=umax32=3,var_off=(0x0; 0x3)) loop_stack=1")
-__msg("loop header at 1, clamping r0 to 1..2 (s32 1..2) step 1")
+__msg("loop header at 1, clamping r0 to 1..3 step 1")
 __msg("processed 5 insns")
 __naked void post_cond_jne_neg_step(void)
 {

tools/testing/selftests/bpf/progs/verifier_stack_ptr.c

@@ -601,11 +601,8 @@ __flag(BPF_F_TEST_STATE_FREQ)
  */
 __msg("loop header at 3, widening r7 to -72..-16 step 8")
 __msg("R7=fp(smin=smin32=-64,smax=smax32=-8")
-/*
- * back-edge state is clamped to the remaining iterations and pruned
- * at the header, because [-64, -16] is within the widened [-72, -16]
- */
-__msg("loop header at 3, clamping r7 to -64..-16 (s32 -64..-8) step 8")
+/* back-edge state is clamped to the widened range and pruned at the header */
+__msg("loop header at 3, clamping r7 to -72..-16 step 8")
 __msg("from 5 to 3: safe")
 __msg("processed 9 insns")
 __naked void stack_ptr_subrange_in_loop(void)