diff mbox series

[v3,bpf-next,1/2] bpf: Relax precision marking in open coded iters and may_goto loop.

Message ID 20240525031156.13545-1-alexei.starovoitov@gmail.com (mailing list archive)
State Superseded
Delegated to: BPF
Headers show
Series [v3,bpf-next,1/2] bpf: Relax precision marking in open coded iters and may_goto loop. | expand

Checks

Context Check Description
bpf/vmtest-bpf-next-VM_Test-47 success Logs for x86_64-llvm-18 / veristat
bpf/vmtest-bpf-next-VM_Test-45 success Logs for x86_64-llvm-18 / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-43 success Logs for x86_64-llvm-18 / test (test_progs, false, 360) / test_progs on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-46 success Logs for x86_64-llvm-18 / test (test_verifier, false, 360) / test_verifier on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-44 success Logs for x86_64-llvm-18 / test (test_progs_cpuv4, false, 360) / test_progs_cpuv4 on x86_64 with llvm-18
bpf/vmtest-bpf-next-PR fail PR summary
bpf/vmtest-bpf-next-VM_Test-0 success Logs for Lint
bpf/vmtest-bpf-next-VM_Test-17 success Logs for s390x-gcc / veristat
bpf/vmtest-bpf-next-VM_Test-10 success Logs for aarch64-gcc / veristat
bpf/vmtest-bpf-next-VM_Test-12 success Logs for s390x-gcc / build-release
bpf/vmtest-bpf-next-VM_Test-18 success Logs for set-matrix
bpf/vmtest-bpf-next-VM_Test-28 success Logs for x86_64-llvm-17 / build / build for x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-5 success Logs for aarch64-gcc / build-release
bpf/vmtest-bpf-next-VM_Test-29 success Logs for x86_64-llvm-17 / build-release / build for x86_64 with llvm-17 and -O2 optimization
bpf/vmtest-bpf-next-VM_Test-3 success Logs for Validate matrix.py
bpf/vmtest-bpf-next-VM_Test-19 success Logs for x86_64-gcc / build / build for x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-11 success Logs for s390x-gcc / build / build for s390x with gcc
bpf/vmtest-bpf-next-VM_Test-16 success Logs for s390x-gcc / test (test_verifier, false, 360) / test_verifier on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-35 success Logs for x86_64-llvm-18 / build / build for x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-36 success Logs for x86_64-llvm-18 / build-release / build for x86_64 with llvm-18 and -O2 optimization
bpf/vmtest-bpf-next-VM_Test-1 success Logs for ShellCheck
bpf/vmtest-bpf-next-VM_Test-4 success Logs for aarch64-gcc / build / build for aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-2 success Logs for Unittests
bpf/vmtest-bpf-next-VM_Test-13 success Logs for s390x-gcc / test (test_maps, false, 360) / test_maps on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-9 success Logs for aarch64-gcc / test (test_verifier, false, 360) / test_verifier on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-42 success Logs for x86_64-llvm-18 / veristat
bpf/vmtest-bpf-next-VM_Test-20 success Logs for x86_64-gcc / build-release
bpf/vmtest-bpf-next-VM_Test-34 success Logs for x86_64-llvm-17 / veristat
bpf/vmtest-bpf-next-VM_Test-7 success Logs for aarch64-gcc / test (test_progs, false, 360) / test_progs on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-37 success Logs for x86_64-llvm-18 / test (test_maps, false, 360) / test_maps on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-22 success Logs for x86_64-gcc / test (test_progs, false, 360) / test_progs on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-31 success Logs for x86_64-llvm-17 / test (test_progs, false, 360) / test_progs on x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-40 success Logs for x86_64-llvm-18 / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-26 success Logs for x86_64-gcc / test (test_verifier, false, 360) / test_verifier on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-8 success Logs for aarch64-gcc / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-6 success Logs for aarch64-gcc / test (test_maps, false, 360) / test_maps on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-14 fail Logs for s390x-gcc / test (test_progs, false, 360) / test_progs on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-33 success Logs for x86_64-llvm-17 / test (test_verifier, false, 360) / test_verifier on x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-38 success Logs for x86_64-llvm-18 / test (test_progs, false, 360) / test_progs on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-41 success Logs for x86_64-llvm-18 / test (test_verifier, false, 360) / test_verifier on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-32 success Logs for x86_64-llvm-17 / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-24 success Logs for x86_64-gcc / test (test_progs_no_alu32_parallel, true, 30) / test_progs_no_alu32_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-15 fail Logs for s390x-gcc / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-21 success Logs for x86_64-gcc / test (test_maps, false, 360) / test_maps on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-30 success Logs for x86_64-llvm-17 / test (test_maps, false, 360) / test_maps on x86_64 with llvm-17
bpf/vmtest-bpf-next-VM_Test-25 success Logs for x86_64-gcc / test (test_progs_parallel, true, 30) / test_progs_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-27 success Logs for x86_64-gcc / veristat / veristat on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-39 success Logs for x86_64-llvm-18 / test (test_progs_cpuv4, false, 360) / test_progs_cpuv4 on x86_64 with llvm-18
bpf/vmtest-bpf-next-VM_Test-23 success Logs for x86_64-gcc / test (test_progs_no_alu32, false, 360) / test_progs_no_alu32 on x86_64 with gcc
netdev/tree_selection success Clearly marked for bpf-next
netdev/apply fail Patch does not apply to bpf-next-0

Commit Message

Alexei Starovoitov May 25, 2024, 3:11 a.m. UTC 
From: Alexei Starovoitov <ast@kernel.org>

v1->v2->v3:
- Algorithm changed completely.

Motivation for the patch
------------------------
Open coded iterators and may_goto is a great mechanism to implement loops,
but counted loops are problematic. For example:
  for (i = 0; i < 100 && can_loop; i++)
is verified as a bounded loop, since i < 100 condition forces the verifier to
mark 'i' as precise and loop states at different iterations are not equivalent.
That removes the benefit of open coded iterators and may_goto.
The workaround is to do:
  int zero = 0; /* global or volatile variable */
  for (i = zero; i < 100 && can_loop; i++)
to hide from the verifier the value of 'i'.
It's unnatural and so far users didn't learn such odd programming pattern.

This patch aims to improve the verifier to support
  for (i = 0; i < 100000 && can_loop; i++)
as open coded iter loop (when 'i' doesn't need to be precise).

Algorithm
---------
First of all:
   if (is_may_goto_insn_at(env, insn_idx)) {
+          update_loop_entry(cur, &sl->state);
           if (states_equal(env, &sl->state, cur, RANGE_WITHIN)) {
-                  update_loop_entry(cur, &sl->state);

It changes the definition of the verifier states loop.
Previously, we considered a state loop to be such a sequence of states
Si -> ... -> Sj -> ... -> Sk that states_equal(Si, Sk, RANGE_WITHIN)
is true.

With this change Si -> ... -> Sj -> ... Sk is a loop if call sites and
instruction pointers for Si and Sk match.

Whether or not Si and Sk are in the loop influences two things:
(a) if exact comparison is needed for states cache;
(b) if widening transformation could be applied to some scalars.

All pairs (Si, Sk) marked as a loop using old definition would be
marked as such using new definition (in a addition to some new pairs).

Hence it is safe to apply (a) and (b) in strictly more cases.

Note that update_loop_entry() relies on the following properties:
- every state in the current DFS path (except current)
  has branches > 0;
- states not in the DFS path are either:
  - in explored_states, are fully explored and have branches == 0;
  - in env->stack, are not yet explored and have branches == 0
    (and also not reachable from is_state_visited()).

With that the get_loop_entry() can be used to gate is_branch_taken() logic.
When the verifier sees 'r1 > 1000' inside the loop and it can predict it
instead of marking r1 as precise it widens both branches, so r1 becomes
[0, 1000] in fallthrough and [1001, UMAX] in other_branch.

Consider the loop:
    bpf_for_each(...) {
       if (r1 > 1000)
          break;

       arr[r1] = ..;
    }
At arr[r1] access the r1 is bounded and the loop can quickly converge.

Unfortunately compilers (both GCC and LLVM) often optimize loop exit
condition to equality, so
 for (i = 0; i < 100; i++) arr[i] = 1
becomes
 for (i = 0; i != 100; i++) arr[1] = 1

Hence treat != and == conditions specially in the verifier.
Widen only not-predicted branch and keep predict branch as is. Example:
  r1 = 0
  goto L1
L2:
  arr[r1] = 1
  r1++
L1:
  if r1 != 100 goto L2
  fallthrough: r1=100 after widening
  other_branch: r1 stays as-is (0, 1, 2, ..)

Also recognize the case where both LHS and RHS are constant and equal to each
other. In this case don't widen at all and take the predicted path.
This key heuristic allows the verifier detect loop end condition.
Such 'for (i = 0; i != 100; i++)' is validated just like bounded loop.

With that the users can use 'for (i = 0; ...' pattern everywhere
and many i = zero workarounds can be removed.

One tests has drastic improvement. The rest are noise.

File                  Insns (A)  Insns (B)  Insns     (DIFF)  States (A)  States (B)  States    (DIFF)
--------------------  ---------  ---------  ----------------  ----------  ----------  ----------------
iters_task_vma.bpf.o      22043        132  -21911 (-99.40%)        1006          10    -996 (-99.01%)

Signed-off-by: Alexei Starovoitov <ast@kernel.org>
---
 kernel/bpf/verifier.c | 136 +++++++++++++++++++++++++++++++++---------
 1 file changed, 109 insertions(+), 27 deletions(-)

Comments

Dan Carpenter May 27, 2024, 7:26 a.m. UTC | #1 
Hi Alexei,

kernel test robot noticed the following build warnings:

url:    https://github.com/intel-lab-lkp/linux/commits/Alexei-Starovoitov/selftests-bpf-Remove-i-zero-workaround-and-add-new-tests/20240525-111247
base:   https://git.kernel.org/pub/scm/linux/kernel/git/bpf/bpf-next.git master
patch link:    https://lore.kernel.org/r/20240525031156.13545-1-alexei.starovoitov%40gmail.com
patch subject: [PATCH v3 bpf-next 1/2] bpf: Relax precision marking in open coded iters and may_goto loop.
config: nios2-randconfig-r071-20240526 (https://download.01.org/0day-ci/archive/20240526/202405260726.0H6QiGNy-lkp@intel.com/config)
compiler: nios2-linux-gcc (GCC) 13.2.0

If you fix the issue in a separate patch/commit (i.e. not just a new version of
the same patch/commit), kindly add following tags
| Reported-by: kernel test robot <lkp@intel.com>
| Reported-by: Dan Carpenter <dan.carpenter@linaro.org>
| Closes: https://lore.kernel.org/r/202405260726.0H6QiGNy-lkp@intel.com/

New smatch warnings:
kernel/bpf/verifier.c:15315 check_cond_jmp_op() error: uninitialized symbol 'other_dst_reg'.

Old smatch warnings:
arch/nios2/include/asm/thread_info.h:62 current_thread_info() error: uninitialized symbol 'sp'.

vim +/other_dst_reg +15315 kernel/bpf/verifier.c

58e2af8b3a6b58 Jakub Kicinski     2016-09-21  15108  static int check_cond_jmp_op(struct bpf_verifier_env *env,
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15109  			     struct bpf_insn *insn, int *insn_idx)
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15110  {
f4d7e40a5b7157 Alexei Starovoitov 2017-12-14  15111  	struct bpf_verifier_state *this_branch = env->cur_state;
f4d7e40a5b7157 Alexei Starovoitov 2017-12-14  15112  	struct bpf_verifier_state *other_branch;
f4d7e40a5b7157 Alexei Starovoitov 2017-12-14  15113  	struct bpf_reg_state *regs = this_branch->frame[this_branch->curframe]->regs;
fb8d251ee2a6bf Alexei Starovoitov 2019-06-15  15114  	struct bpf_reg_state *dst_reg, *other_branch_regs, *src_reg = NULL;
689049426b9d3b Alexei Starovoitov 2024-05-24  15115  	struct bpf_reg_state *eq_branch_regs, *other_dst_reg, *other_src_reg = NULL;
c31534267c180f Andrii Nakryiko    2023-11-01  15116  	struct bpf_reg_state fake_reg = {};
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15117  	u8 opcode = BPF_OP(insn->code);
689049426b9d3b Alexei Starovoitov 2024-05-24  15118  	bool is_jmp32, ignore_pred;
689049426b9d3b Alexei Starovoitov 2024-05-24  15119  	bool has_src_reg = false;
fb8d251ee2a6bf Alexei Starovoitov 2019-06-15  15120  	int pred = -1;
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15121  	int err;
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15122  
092ed0968bb648 Jiong Wang         2019-01-26  15123  	/* Only conditional jumps are expected to reach here. */
011832b97b311b Alexei Starovoitov 2024-03-05  15124  	if (opcode == BPF_JA || opcode > BPF_JCOND) {
092ed0968bb648 Jiong Wang         2019-01-26  15125  		verbose(env, "invalid BPF_JMP/JMP32 opcode %x\n", opcode);
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15126  		return -EINVAL;
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15127  	}
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15128  
011832b97b311b Alexei Starovoitov 2024-03-05  15129  	if (opcode == BPF_JCOND) {
011832b97b311b Alexei Starovoitov 2024-03-05  15130  		struct bpf_verifier_state *cur_st = env->cur_state, *queued_st, *prev_st;
011832b97b311b Alexei Starovoitov 2024-03-05  15131  		int idx = *insn_idx;
011832b97b311b Alexei Starovoitov 2024-03-05  15132  
011832b97b311b Alexei Starovoitov 2024-03-05  15133  		if (insn->code != (BPF_JMP | BPF_JCOND) ||
011832b97b311b Alexei Starovoitov 2024-03-05  15134  		    insn->src_reg != BPF_MAY_GOTO ||
011832b97b311b Alexei Starovoitov 2024-03-05  15135  		    insn->dst_reg || insn->imm || insn->off == 0) {
011832b97b311b Alexei Starovoitov 2024-03-05  15136  			verbose(env, "invalid may_goto off %d imm %d\n",
011832b97b311b Alexei Starovoitov 2024-03-05  15137  				insn->off, insn->imm);
011832b97b311b Alexei Starovoitov 2024-03-05  15138  			return -EINVAL;
011832b97b311b Alexei Starovoitov 2024-03-05  15139  		}
011832b97b311b Alexei Starovoitov 2024-03-05  15140  		prev_st = find_prev_entry(env, cur_st->parent, idx);
011832b97b311b Alexei Starovoitov 2024-03-05  15141  
011832b97b311b Alexei Starovoitov 2024-03-05  15142  		/* branch out 'fallthrough' insn as a new state to explore */
011832b97b311b Alexei Starovoitov 2024-03-05  15143  		queued_st = push_stack(env, idx + 1, idx, false);
011832b97b311b Alexei Starovoitov 2024-03-05  15144  		if (!queued_st)
011832b97b311b Alexei Starovoitov 2024-03-05  15145  			return -ENOMEM;
011832b97b311b Alexei Starovoitov 2024-03-05  15146  
011832b97b311b Alexei Starovoitov 2024-03-05  15147  		queued_st->may_goto_depth++;
011832b97b311b Alexei Starovoitov 2024-03-05  15148  		if (prev_st)
011832b97b311b Alexei Starovoitov 2024-03-05  15149  			widen_imprecise_scalars(env, prev_st, queued_st);
011832b97b311b Alexei Starovoitov 2024-03-05  15150  		*insn_idx += insn->off;
011832b97b311b Alexei Starovoitov 2024-03-05  15151  		return 0;
011832b97b311b Alexei Starovoitov 2024-03-05  15152  	}
011832b97b311b Alexei Starovoitov 2024-03-05  15153  
d75e30dddf7344 Yafang Shao        2023-08-23  15154  	/* check src2 operand */
d75e30dddf7344 Yafang Shao        2023-08-23  15155  	err = check_reg_arg(env, insn->dst_reg, SRC_OP);
d75e30dddf7344 Yafang Shao        2023-08-23  15156  	if (err)
d75e30dddf7344 Yafang Shao        2023-08-23  15157  		return err;
d75e30dddf7344 Yafang Shao        2023-08-23  15158  
d75e30dddf7344 Yafang Shao        2023-08-23  15159  	dst_reg = &regs[insn->dst_reg];
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15160  	if (BPF_SRC(insn->code) == BPF_X) {
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15161  		if (insn->imm != 0) {
092ed0968bb648 Jiong Wang         2019-01-26  15162  			verbose(env, "BPF_JMP/JMP32 uses reserved fields\n");
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15163  			return -EINVAL;
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15164  		}
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15165  
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15166  		/* check src1 operand */
dc503a8ad98474 Edward Cree        2017-08-15  15167  		err = check_reg_arg(env, insn->src_reg, SRC_OP);
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15168  		if (err)
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15169  			return err;
1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15170  
689049426b9d3b Alexei Starovoitov 2024-05-24  15171  		has_src_reg = true;
d75e30dddf7344 Yafang Shao        2023-08-23  15172  		src_reg = &regs[insn->src_reg];
d75e30dddf7344 Yafang Shao        2023-08-23  15173  		if (!(reg_is_pkt_pointer_any(dst_reg) && reg_is_pkt_pointer_any(src_reg)) &&
d75e30dddf7344 Yafang Shao        2023-08-23  15174  		    is_pointer_value(env, insn->src_reg)) {
61bd5218eef349 Jakub Kicinski     2017-10-09  15175  			verbose(env, "R%d pointer comparison prohibited\n",
1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15176  				insn->src_reg);
1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15177  			return -EACCES;
1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15178  		}
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15179  	} else {
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15180  		if (insn->src_reg != BPF_REG_0) {
092ed0968bb648 Jiong Wang         2019-01-26  15181  			verbose(env, "BPF_JMP/JMP32 uses reserved fields\n");
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15182  			return -EINVAL;
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15183  		}
c31534267c180f Andrii Nakryiko    2023-11-01  15184  		src_reg = &fake_reg;
c31534267c180f Andrii Nakryiko    2023-11-01  15185  		src_reg->type = SCALAR_VALUE;
c31534267c180f Andrii Nakryiko    2023-11-01  15186  		__mark_reg_known(src_reg, insn->imm);
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15187  	}
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15188  
092ed0968bb648 Jiong Wang         2019-01-26  15189  	is_jmp32 = BPF_CLASS(insn->code) == BPF_JMP32;
689049426b9d3b Alexei Starovoitov 2024-05-24  15190  	if (dst_reg->type != SCALAR_VALUE || src_reg->type != SCALAR_VALUE)
689049426b9d3b Alexei Starovoitov 2024-05-24  15191  		ignore_pred = false;
689049426b9d3b Alexei Starovoitov 2024-05-24  15192  	/*
689049426b9d3b Alexei Starovoitov 2024-05-24  15193  	 * Compilers often optimize loop exit condition to equality, so
689049426b9d3b Alexei Starovoitov 2024-05-24  15194  	 *      for (i = 0; i < 100; i++) arr[i] = 1
689049426b9d3b Alexei Starovoitov 2024-05-24  15195  	 * becomes
689049426b9d3b Alexei Starovoitov 2024-05-24  15196  	 *      for (i = 0; i != 100; i++) arr[1] = 1
689049426b9d3b Alexei Starovoitov 2024-05-24  15197  	 * Hence treat != and == conditions specially in the verifier.
689049426b9d3b Alexei Starovoitov 2024-05-24  15198  	 * Widen only not-predicted branch and keep predict branch as is. Example:
689049426b9d3b Alexei Starovoitov 2024-05-24  15199  	 *    r1 = 0
689049426b9d3b Alexei Starovoitov 2024-05-24  15200  	 *    goto L1
689049426b9d3b Alexei Starovoitov 2024-05-24  15201  	 * L2:
689049426b9d3b Alexei Starovoitov 2024-05-24  15202  	 *    arr[r1] = 1
689049426b9d3b Alexei Starovoitov 2024-05-24  15203  	 *    r1++
689049426b9d3b Alexei Starovoitov 2024-05-24  15204  	 * L1:
689049426b9d3b Alexei Starovoitov 2024-05-24  15205  	 *    if r1 != 100 goto L2
689049426b9d3b Alexei Starovoitov 2024-05-24  15206  	 *    fallthrough: r1=100 after widening
689049426b9d3b Alexei Starovoitov 2024-05-24  15207  	 *    other_branch: r1 stays as-is (0, 1, 2, ..)
689049426b9d3b Alexei Starovoitov 2024-05-24  15208  	 *
689049426b9d3b Alexei Starovoitov 2024-05-24  15209  	 *  Also recognize the case where both LHS and RHS are constant and
689049426b9d3b Alexei Starovoitov 2024-05-24  15210  	 *  equal to each other. In this case don't widen at all and take the
689049426b9d3b Alexei Starovoitov 2024-05-24  15211  	 *  predicted path. This key heuristic allows the verifier detect loop
689049426b9d3b Alexei Starovoitov 2024-05-24  15212  	 *  end condition and 'for (i = 0; i != 100; i++)' is validated just
689049426b9d3b Alexei Starovoitov 2024-05-24  15213  	 *  like bounded loop.
689049426b9d3b Alexei Starovoitov 2024-05-24  15214  	 */
689049426b9d3b Alexei Starovoitov 2024-05-24  15215  	else if (is_reg_const(dst_reg, is_jmp32) && is_reg_const(src_reg, is_jmp32) &&
689049426b9d3b Alexei Starovoitov 2024-05-24  15216  	    reg_const_value(dst_reg, is_jmp32) == reg_const_value(src_reg, is_jmp32))
689049426b9d3b Alexei Starovoitov 2024-05-24  15217  		ignore_pred = false;
689049426b9d3b Alexei Starovoitov 2024-05-24  15218  	else
689049426b9d3b Alexei Starovoitov 2024-05-24  15219  		ignore_pred = (get_loop_entry(this_branch) ||
689049426b9d3b Alexei Starovoitov 2024-05-24  15220  			       this_branch->may_goto_depth) &&
689049426b9d3b Alexei Starovoitov 2024-05-24  15221  				/* Gate widen_reg() logic */
689049426b9d3b Alexei Starovoitov 2024-05-24  15222  				env->bpf_capable;
689049426b9d3b Alexei Starovoitov 2024-05-24  15223  
c31534267c180f Andrii Nakryiko    2023-11-01  15224  	pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
689049426b9d3b Alexei Starovoitov 2024-05-24  15225  	if (pred >= 0 && !ignore_pred) {
cac616db39c207 John Fastabend     2020-05-21  15226  		/* If we get here with a dst_reg pointer type it is because
cac616db39c207 John Fastabend     2020-05-21  15227  		 * above is_branch_taken() special cased the 0 comparison.
cac616db39c207 John Fastabend     2020-05-21  15228  		 */
cac616db39c207 John Fastabend     2020-05-21  15229  		if (!__is_pointer_value(false, dst_reg))
b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15230  			err = mark_chain_precision(env, insn->dst_reg);
6d94e741a8ff81 Alexei Starovoitov 2020-11-10  15231  		if (BPF_SRC(insn->code) == BPF_X && !err &&
6d94e741a8ff81 Alexei Starovoitov 2020-11-10  15232  		    !__is_pointer_value(false, src_reg))
b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15233  			err = mark_chain_precision(env, insn->src_reg);
b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15234  		if (err)
b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15235  			return err;
b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15236  	}
9183671af6dbf6 Daniel Borkmann    2021-05-28  15237  
689049426b9d3b Alexei Starovoitov 2024-05-24  15238  	if (pred < 0 || ignore_pred) {
689049426b9d3b Alexei Starovoitov 2024-05-24  15239  		other_branch = push_stack(env, *insn_idx + insn->off + 1, *insn_idx,
689049426b9d3b Alexei Starovoitov 2024-05-24  15240  					  false);
689049426b9d3b Alexei Starovoitov 2024-05-24  15241  		if (!other_branch)
689049426b9d3b Alexei Starovoitov 2024-05-24  15242  			return -EFAULT;
689049426b9d3b Alexei Starovoitov 2024-05-24  15243  		other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
689049426b9d3b Alexei Starovoitov 2024-05-24  15244  		other_dst_reg = &other_branch_regs[insn->dst_reg];
689049426b9d3b Alexei Starovoitov 2024-05-24  15245  		if (has_src_reg)
689049426b9d3b Alexei Starovoitov 2024-05-24  15246  			other_src_reg = &other_branch_regs[insn->src_reg];
689049426b9d3b Alexei Starovoitov 2024-05-24  15247  	}

other_dst_reg not set on else path.

689049426b9d3b Alexei Starovoitov 2024-05-24  15248  
4f7b3e82589e0d Alexei Starovoitov 2018-12-03  15249  	if (pred == 1) {
9183671af6dbf6 Daniel Borkmann    2021-05-28  15250  		/* Only follow the goto, ignore fall-through. If needed, push
9183671af6dbf6 Daniel Borkmann    2021-05-28  15251  		 * the fall-through branch for simulation under speculative
9183671af6dbf6 Daniel Borkmann    2021-05-28  15252  		 * execution.
9183671af6dbf6 Daniel Borkmann    2021-05-28  15253  		 */
9183671af6dbf6 Daniel Borkmann    2021-05-28  15254  		if (!env->bypass_spec_v1 &&
9183671af6dbf6 Daniel Borkmann    2021-05-28  15255  		    !sanitize_speculative_path(env, insn, *insn_idx + 1,
9183671af6dbf6 Daniel Borkmann    2021-05-28  15256  					       *insn_idx))
9183671af6dbf6 Daniel Borkmann    2021-05-28  15257  			return -EFAULT;
1a8a315f008a58 Andrii Nakryiko    2023-10-11  15258  		if (env->log.level & BPF_LOG_LEVEL)
1a8a315f008a58 Andrii Nakryiko    2023-10-11  15259  			print_insn_state(env, this_branch->frame[this_branch->curframe]);
689049426b9d3b Alexei Starovoitov 2024-05-24  15260  		if (ignore_pred) {
689049426b9d3b Alexei Starovoitov 2024-05-24  15261  			/* dst and src regs are scalars. Widen them */
689049426b9d3b Alexei Starovoitov 2024-05-24  15262  			widen_reg(dst_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15263  			if (has_src_reg)
689049426b9d3b Alexei Starovoitov 2024-05-24  15264  				widen_reg(src_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15265  			/*
689049426b9d3b Alexei Starovoitov 2024-05-24  15266  			 * Widen other branch only if not comparing for equlity.
689049426b9d3b Alexei Starovoitov 2024-05-24  15267  			 * Example:
689049426b9d3b Alexei Starovoitov 2024-05-24  15268  			 *   r1 = 1
689049426b9d3b Alexei Starovoitov 2024-05-24  15269  			 *   if (r1 < 100)
689049426b9d3b Alexei Starovoitov 2024-05-24  15270  			 * will produce
689049426b9d3b Alexei Starovoitov 2024-05-24  15271  			 *   [0, 99] and [100, UMAX] after widening and reg_set_min_max().
689049426b9d3b Alexei Starovoitov 2024-05-24  15272  			 *
689049426b9d3b Alexei Starovoitov 2024-05-24  15273  			 *   r1 = 1
689049426b9d3b Alexei Starovoitov 2024-05-24  15274  			 *   if (r1 == 100)
689049426b9d3b Alexei Starovoitov 2024-05-24  15275  			 * will produce
689049426b9d3b Alexei Starovoitov 2024-05-24  15276  			 *    [1] and [100] after widening in other_branch and reg_set_min_max().
689049426b9d3b Alexei Starovoitov 2024-05-24  15277  			 */
689049426b9d3b Alexei Starovoitov 2024-05-24  15278  			if (opcode != BPF_JEQ && opcode != BPF_JNE) {
689049426b9d3b Alexei Starovoitov 2024-05-24  15279  				widen_reg(other_dst_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15280  				if (has_src_reg)
689049426b9d3b Alexei Starovoitov 2024-05-24  15281  					widen_reg(other_src_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15282  			}
689049426b9d3b Alexei Starovoitov 2024-05-24  15283  		} else {
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15284  			*insn_idx += insn->off;
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15285  			return 0;
689049426b9d3b Alexei Starovoitov 2024-05-24  15286  		}
4f7b3e82589e0d Alexei Starovoitov 2018-12-03  15287  	} else if (pred == 0) {
9183671af6dbf6 Daniel Borkmann    2021-05-28  15288  		/* Only follow the fall-through branch, since that's where the
9183671af6dbf6 Daniel Borkmann    2021-05-28  15289  		 * program will go. If needed, push the goto branch for
9183671af6dbf6 Daniel Borkmann    2021-05-28  15290  		 * simulation under speculative execution.
9183671af6dbf6 Daniel Borkmann    2021-05-28  15291  		 */
9183671af6dbf6 Daniel Borkmann    2021-05-28  15292  		if (!env->bypass_spec_v1 &&
9183671af6dbf6 Daniel Borkmann    2021-05-28  15293  		    !sanitize_speculative_path(env, insn,
9183671af6dbf6 Daniel Borkmann    2021-05-28  15294  					       *insn_idx + insn->off + 1,
9183671af6dbf6 Daniel Borkmann    2021-05-28  15295  					       *insn_idx))
9183671af6dbf6 Daniel Borkmann    2021-05-28  15296  			return -EFAULT;
1a8a315f008a58 Andrii Nakryiko    2023-10-11  15297  		if (env->log.level & BPF_LOG_LEVEL)
1a8a315f008a58 Andrii Nakryiko    2023-10-11  15298  			print_insn_state(env, this_branch->frame[this_branch->curframe]);
689049426b9d3b Alexei Starovoitov 2024-05-24  15299  		if (ignore_pred) {
689049426b9d3b Alexei Starovoitov 2024-05-24  15300  			if (opcode != BPF_JEQ && opcode != BPF_JNE) {
689049426b9d3b Alexei Starovoitov 2024-05-24  15301  				widen_reg(dst_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15302  				if (has_src_reg)
689049426b9d3b Alexei Starovoitov 2024-05-24  15303  					widen_reg(src_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15304  			}
689049426b9d3b Alexei Starovoitov 2024-05-24  15305  			widen_reg(other_dst_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15306  			if (has_src_reg)
689049426b9d3b Alexei Starovoitov 2024-05-24  15307  				widen_reg(other_src_reg);
689049426b9d3b Alexei Starovoitov 2024-05-24  15308  		} else {
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15309  			return 0;
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15310  		}
689049426b9d3b Alexei Starovoitov 2024-05-24  15311  	}
17a5267067f3c3 Alexei Starovoitov 2014-09-26  15312  
484611357c19f9 Josef Bacik        2016-09-28  15313  	if (BPF_SRC(insn->code) == BPF_X) {
5f99f312bd3bed Andrii Nakryiko    2023-11-11  15314  		err = reg_set_min_max(env,
689049426b9d3b Alexei Starovoitov 2024-05-24 @15315  				      other_dst_reg, other_src_reg,
                                                                                      ^^^^^^^^^^^^^

4621202adc5bc0 Andrii Nakryiko    2023-11-01  15316  				      dst_reg, src_reg, opcode, is_jmp32);
4621202adc5bc0 Andrii Nakryiko    2023-11-01  15317  	} else /* BPF_SRC(insn->code) == BPF_K */ {
5f99f312bd3bed Andrii Nakryiko    2023-11-11  15318  		err = reg_set_min_max(env,
689049426b9d3b Alexei Starovoitov 2024-05-24  15319  				      other_dst_reg,
                                                                                      ^^^^^^^^^^^^^
Passed to reg_set_min_max() without being initialized.

4621202adc5bc0 Andrii Nakryiko    2023-11-01  15320  				      src_reg /* fake one */,
4621202adc5bc0 Andrii Nakryiko    2023-11-01  15321  				      dst_reg, src_reg /* same fake one */,
3f50f132d8400e John Fastabend     2020-03-30  15322  				      opcode, is_jmp32);
484611357c19f9 Josef Bacik        2016-09-28  15323  	}
5f99f312bd3bed Andrii Nakryiko    2023-11-11  15324  	if (err)
Alexei Starovoitov May 27, 2024, 10:44 p.m. UTC | #2 
On Mon, May 27, 2024 at 12:26 AM Dan Carpenter <dan.carpenter@linaro.org> wrote:
>
> Hi Alexei,
>
> kernel test robot noticed the following build warnings:
>
> url:    https://github.com/intel-lab-lkp/linux/commits/Alexei-Starovoitov/selftests-bpf-Remove-i-zero-workaround-and-add-new-tests/20240525-111247
> base:   https://git.kernel.org/pub/scm/linux/kernel/git/bpf/bpf-next.git master
> patch link:    https://lore.kernel.org/r/20240525031156.13545-1-alexei.starovoitov%40gmail.com
> patch subject: [PATCH v3 bpf-next 1/2] bpf: Relax precision marking in open coded iters and may_goto loop.
> config: nios2-randconfig-r071-20240526 (https://download.01.org/0day-ci/archive/20240526/202405260726.0H6QiGNy-lkp@intel.com/config)
> compiler: nios2-linux-gcc (GCC) 13.2.0
>
> If you fix the issue in a separate patch/commit (i.e. not just a new version of
> the same patch/commit), kindly add following tags
> | Reported-by: kernel test robot <lkp@intel.com>
> | Reported-by: Dan Carpenter <dan.carpenter@linaro.org>
> | Closes: https://lore.kernel.org/r/202405260726.0H6QiGNy-lkp@intel.com/
>
> New smatch warnings:
> kernel/bpf/verifier.c:15315 check_cond_jmp_op() error: uninitialized symbol 'other_dst_reg'.
>
> Old smatch warnings:
> arch/nios2/include/asm/thread_info.h:62 current_thread_info() error: uninitialized symbol 'sp'.
>
> vim +/other_dst_reg +15315 kernel/bpf/verifier.c
>
> 58e2af8b3a6b58 Jakub Kicinski     2016-09-21  15108  static int check_cond_jmp_op(struct bpf_verifier_env *env,
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15109                          struct bpf_insn *insn, int *insn_idx)
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15110  {
> f4d7e40a5b7157 Alexei Starovoitov 2017-12-14  15111     struct bpf_verifier_state *this_branch = env->cur_state;
> f4d7e40a5b7157 Alexei Starovoitov 2017-12-14  15112     struct bpf_verifier_state *other_branch;
> f4d7e40a5b7157 Alexei Starovoitov 2017-12-14  15113     struct bpf_reg_state *regs = this_branch->frame[this_branch->curframe]->regs;
> fb8d251ee2a6bf Alexei Starovoitov 2019-06-15  15114     struct bpf_reg_state *dst_reg, *other_branch_regs, *src_reg = NULL;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15115     struct bpf_reg_state *eq_branch_regs, *other_dst_reg, *other_src_reg = NULL;
> c31534267c180f Andrii Nakryiko    2023-11-01  15116     struct bpf_reg_state fake_reg = {};
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15117     u8 opcode = BPF_OP(insn->code);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15118     bool is_jmp32, ignore_pred;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15119     bool has_src_reg = false;
> fb8d251ee2a6bf Alexei Starovoitov 2019-06-15  15120     int pred = -1;
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15121     int err;
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15122
> 092ed0968bb648 Jiong Wang         2019-01-26  15123     /* Only conditional jumps are expected to reach here. */
> 011832b97b311b Alexei Starovoitov 2024-03-05  15124     if (opcode == BPF_JA || opcode > BPF_JCOND) {
> 092ed0968bb648 Jiong Wang         2019-01-26  15125             verbose(env, "invalid BPF_JMP/JMP32 opcode %x\n", opcode);
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15126             return -EINVAL;
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15127     }
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15128
> 011832b97b311b Alexei Starovoitov 2024-03-05  15129     if (opcode == BPF_JCOND) {
> 011832b97b311b Alexei Starovoitov 2024-03-05  15130             struct bpf_verifier_state *cur_st = env->cur_state, *queued_st, *prev_st;
> 011832b97b311b Alexei Starovoitov 2024-03-05  15131             int idx = *insn_idx;
> 011832b97b311b Alexei Starovoitov 2024-03-05  15132
> 011832b97b311b Alexei Starovoitov 2024-03-05  15133             if (insn->code != (BPF_JMP | BPF_JCOND) ||
> 011832b97b311b Alexei Starovoitov 2024-03-05  15134                 insn->src_reg != BPF_MAY_GOTO ||
> 011832b97b311b Alexei Starovoitov 2024-03-05  15135                 insn->dst_reg || insn->imm || insn->off == 0) {
> 011832b97b311b Alexei Starovoitov 2024-03-05  15136                     verbose(env, "invalid may_goto off %d imm %d\n",
> 011832b97b311b Alexei Starovoitov 2024-03-05  15137                             insn->off, insn->imm);
> 011832b97b311b Alexei Starovoitov 2024-03-05  15138                     return -EINVAL;
> 011832b97b311b Alexei Starovoitov 2024-03-05  15139             }
> 011832b97b311b Alexei Starovoitov 2024-03-05  15140             prev_st = find_prev_entry(env, cur_st->parent, idx);
> 011832b97b311b Alexei Starovoitov 2024-03-05  15141
> 011832b97b311b Alexei Starovoitov 2024-03-05  15142             /* branch out 'fallthrough' insn as a new state to explore */
> 011832b97b311b Alexei Starovoitov 2024-03-05  15143             queued_st = push_stack(env, idx + 1, idx, false);
> 011832b97b311b Alexei Starovoitov 2024-03-05  15144             if (!queued_st)
> 011832b97b311b Alexei Starovoitov 2024-03-05  15145                     return -ENOMEM;
> 011832b97b311b Alexei Starovoitov 2024-03-05  15146
> 011832b97b311b Alexei Starovoitov 2024-03-05  15147             queued_st->may_goto_depth++;
> 011832b97b311b Alexei Starovoitov 2024-03-05  15148             if (prev_st)
> 011832b97b311b Alexei Starovoitov 2024-03-05  15149                     widen_imprecise_scalars(env, prev_st, queued_st);
> 011832b97b311b Alexei Starovoitov 2024-03-05  15150             *insn_idx += insn->off;
> 011832b97b311b Alexei Starovoitov 2024-03-05  15151             return 0;
> 011832b97b311b Alexei Starovoitov 2024-03-05  15152     }
> 011832b97b311b Alexei Starovoitov 2024-03-05  15153
> d75e30dddf7344 Yafang Shao        2023-08-23  15154     /* check src2 operand */
> d75e30dddf7344 Yafang Shao        2023-08-23  15155     err = check_reg_arg(env, insn->dst_reg, SRC_OP);
> d75e30dddf7344 Yafang Shao        2023-08-23  15156     if (err)
> d75e30dddf7344 Yafang Shao        2023-08-23  15157             return err;
> d75e30dddf7344 Yafang Shao        2023-08-23  15158
> d75e30dddf7344 Yafang Shao        2023-08-23  15159     dst_reg = &regs[insn->dst_reg];
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15160     if (BPF_SRC(insn->code) == BPF_X) {
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15161             if (insn->imm != 0) {
> 092ed0968bb648 Jiong Wang         2019-01-26  15162                     verbose(env, "BPF_JMP/JMP32 uses reserved fields\n");
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15163                     return -EINVAL;
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15164             }
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15165
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15166             /* check src1 operand */
> dc503a8ad98474 Edward Cree        2017-08-15  15167             err = check_reg_arg(env, insn->src_reg, SRC_OP);
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15168             if (err)
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15169                     return err;
> 1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15170
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15171             has_src_reg = true;
> d75e30dddf7344 Yafang Shao        2023-08-23  15172             src_reg = &regs[insn->src_reg];
> d75e30dddf7344 Yafang Shao        2023-08-23  15173             if (!(reg_is_pkt_pointer_any(dst_reg) && reg_is_pkt_pointer_any(src_reg)) &&
> d75e30dddf7344 Yafang Shao        2023-08-23  15174                 is_pointer_value(env, insn->src_reg)) {
> 61bd5218eef349 Jakub Kicinski     2017-10-09  15175                     verbose(env, "R%d pointer comparison prohibited\n",
> 1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15176                             insn->src_reg);
> 1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15177                     return -EACCES;
> 1be7f75d1668d6 Alexei Starovoitov 2015-10-07  15178             }
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15179     } else {
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15180             if (insn->src_reg != BPF_REG_0) {
> 092ed0968bb648 Jiong Wang         2019-01-26  15181                     verbose(env, "BPF_JMP/JMP32 uses reserved fields\n");
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15182                     return -EINVAL;
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15183             }
> c31534267c180f Andrii Nakryiko    2023-11-01  15184             src_reg = &fake_reg;
> c31534267c180f Andrii Nakryiko    2023-11-01  15185             src_reg->type = SCALAR_VALUE;
> c31534267c180f Andrii Nakryiko    2023-11-01  15186             __mark_reg_known(src_reg, insn->imm);
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15187     }
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15188
> 092ed0968bb648 Jiong Wang         2019-01-26  15189     is_jmp32 = BPF_CLASS(insn->code) == BPF_JMP32;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15190     if (dst_reg->type != SCALAR_VALUE || src_reg->type != SCALAR_VALUE)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15191             ignore_pred = false;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15192     /*
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15193      * Compilers often optimize loop exit condition to equality, so
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15194      *      for (i = 0; i < 100; i++) arr[i] = 1
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15195      * becomes
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15196      *      for (i = 0; i != 100; i++) arr[1] = 1
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15197      * Hence treat != and == conditions specially in the verifier.
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15198      * Widen only not-predicted branch and keep predict branch as is. Example:
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15199      *    r1 = 0
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15200      *    goto L1
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15201      * L2:
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15202      *    arr[r1] = 1
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15203      *    r1++
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15204      * L1:
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15205      *    if r1 != 100 goto L2
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15206      *    fallthrough: r1=100 after widening
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15207      *    other_branch: r1 stays as-is (0, 1, 2, ..)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15208      *
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15209      *  Also recognize the case where both LHS and RHS are constant and
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15210      *  equal to each other. In this case don't widen at all and take the
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15211      *  predicted path. This key heuristic allows the verifier detect loop
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15212      *  end condition and 'for (i = 0; i != 100; i++)' is validated just
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15213      *  like bounded loop.
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15214      */
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15215     else if (is_reg_const(dst_reg, is_jmp32) && is_reg_const(src_reg, is_jmp32) &&
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15216         reg_const_value(dst_reg, is_jmp32) == reg_const_value(src_reg, is_jmp32))
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15217             ignore_pred = false;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15218     else
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15219             ignore_pred = (get_loop_entry(this_branch) ||
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15220                            this_branch->may_goto_depth) &&
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15221                             /* Gate widen_reg() logic */
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15222                             env->bpf_capable;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15223
> c31534267c180f Andrii Nakryiko    2023-11-01  15224     pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15225     if (pred >= 0 && !ignore_pred) {
> cac616db39c207 John Fastabend     2020-05-21  15226             /* If we get here with a dst_reg pointer type it is because
> cac616db39c207 John Fastabend     2020-05-21  15227              * above is_branch_taken() special cased the 0 comparison.
> cac616db39c207 John Fastabend     2020-05-21  15228              */
> cac616db39c207 John Fastabend     2020-05-21  15229             if (!__is_pointer_value(false, dst_reg))
> b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15230                     err = mark_chain_precision(env, insn->dst_reg);
> 6d94e741a8ff81 Alexei Starovoitov 2020-11-10  15231             if (BPF_SRC(insn->code) == BPF_X && !err &&
> 6d94e741a8ff81 Alexei Starovoitov 2020-11-10  15232                 !__is_pointer_value(false, src_reg))
> b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15233                     err = mark_chain_precision(env, insn->src_reg);
> b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15234             if (err)
> b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15235                     return err;
> b5dc0163d8fd78 Alexei Starovoitov 2019-06-15  15236     }
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15237
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15238     if (pred < 0 || ignore_pred) {
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15239             other_branch = push_stack(env, *insn_idx + insn->off + 1, *insn_idx,
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15240                                       false);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15241             if (!other_branch)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15242                     return -EFAULT;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15243             other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15244             other_dst_reg = &other_branch_regs[insn->dst_reg];
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15245             if (has_src_reg)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15246                     other_src_reg = &other_branch_regs[insn->src_reg];
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15247     }
>
> other_dst_reg not set on else path.
>
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15248
> 4f7b3e82589e0d Alexei Starovoitov 2018-12-03  15249     if (pred == 1) {
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15250             /* Only follow the goto, ignore fall-through. If needed, push
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15251              * the fall-through branch for simulation under speculative
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15252              * execution.
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15253              */
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15254             if (!env->bypass_spec_v1 &&
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15255                 !sanitize_speculative_path(env, insn, *insn_idx + 1,
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15256                                            *insn_idx))
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15257                     return -EFAULT;
> 1a8a315f008a58 Andrii Nakryiko    2023-10-11  15258             if (env->log.level & BPF_LOG_LEVEL)
> 1a8a315f008a58 Andrii Nakryiko    2023-10-11  15259                     print_insn_state(env, this_branch->frame[this_branch->curframe]);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15260             if (ignore_pred) {
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15261                     /* dst and src regs are scalars. Widen them */
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15262                     widen_reg(dst_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15263                     if (has_src_reg)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15264                             widen_reg(src_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15265                     /*
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15266                      * Widen other branch only if not comparing for equlity.
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15267                      * Example:
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15268                      *   r1 = 1
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15269                      *   if (r1 < 100)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15270                      * will produce
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15271                      *   [0, 99] and [100, UMAX] after widening and reg_set_min_max().
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15272                      *
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15273                      *   r1 = 1
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15274                      *   if (r1 == 100)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15275                      * will produce
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15276                      *    [1] and [100] after widening in other_branch and reg_set_min_max().
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15277                      */
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15278                     if (opcode != BPF_JEQ && opcode != BPF_JNE) {
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15279                             widen_reg(other_dst_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15280                             if (has_src_reg)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15281                                     widen_reg(other_src_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15282                     }
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15283             } else {
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15284                     *insn_idx += insn->off;
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15285                     return 0;
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15286             }
> 4f7b3e82589e0d Alexei Starovoitov 2018-12-03  15287     } else if (pred == 0) {
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15288             /* Only follow the fall-through branch, since that's where the
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15289              * program will go. If needed, push the goto branch for
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15290              * simulation under speculative execution.
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15291              */
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15292             if (!env->bypass_spec_v1 &&
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15293                 !sanitize_speculative_path(env, insn,
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15294                                            *insn_idx + insn->off + 1,
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15295                                            *insn_idx))
> 9183671af6dbf6 Daniel Borkmann    2021-05-28  15296                     return -EFAULT;
> 1a8a315f008a58 Andrii Nakryiko    2023-10-11  15297             if (env->log.level & BPF_LOG_LEVEL)
> 1a8a315f008a58 Andrii Nakryiko    2023-10-11  15298                     print_insn_state(env, this_branch->frame[this_branch->curframe]);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15299             if (ignore_pred) {
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15300                     if (opcode != BPF_JEQ && opcode != BPF_JNE) {
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15301                             widen_reg(dst_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15302                             if (has_src_reg)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15303                                     widen_reg(src_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15304                     }
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15305                     widen_reg(other_dst_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15306                     if (has_src_reg)
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15307                             widen_reg(other_src_reg);
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15308             } else {
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15309                     return 0;
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15310             }
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15311     }
> 17a5267067f3c3 Alexei Starovoitov 2014-09-26  15312
> 484611357c19f9 Josef Bacik        2016-09-28  15313     if (BPF_SRC(insn->code) == BPF_X) {
> 5f99f312bd3bed Andrii Nakryiko    2023-11-11  15314             err = reg_set_min_max(env,
> 689049426b9d3b Alexei Starovoitov 2024-05-24 @15315                                   other_dst_reg, other_src_reg,
>                                                                                       ^^^^^^^^^^^^^
>
> 4621202adc5bc0 Andrii Nakryiko    2023-11-01  15316                                   dst_reg, src_reg, opcode, is_jmp32);
> 4621202adc5bc0 Andrii Nakryiko    2023-11-01  15317     } else /* BPF_SRC(insn->code) == BPF_K */ {
> 5f99f312bd3bed Andrii Nakryiko    2023-11-11  15318             err = reg_set_min_max(env,
> 689049426b9d3b Alexei Starovoitov 2024-05-24  15319                                   other_dst_reg,
>                                                                                       ^^^^^^^^^^^^^
> Passed to reg_set_min_max() without being initialized.

No. It's initialized when passed. It's a false positive.
Try to make smatch smarter?
Eduard Zingerman May 28, 2024, 4:10 a.m. UTC | #3 
On Fri, 2024-05-24 at 20:11 -0700, Alexei Starovoitov wrote:
> From: Alexei Starovoitov <ast@kernel.org>

[...]

> With that the get_loop_entry() can be used to gate is_branch_taken() logic.
> When the verifier sees 'r1 > 1000' inside the loop and it can predict it
> instead of marking r1 as precise it widens both branches, so r1 becomes
> [0, 1000] in fallthrough and [1001, UMAX] in other_branch.
> 
> Consider the loop:
>     bpf_for_each(...) {
>        if (r1 > 1000)
>           break;
> 
>        arr[r1] = ..;
>     }
> At arr[r1] access the r1 is bounded and the loop can quickly converge.
> 
> Unfortunately compilers (both GCC and LLVM) often optimize loop exit
> condition to equality, so
>  for (i = 0; i < 100; i++) arr[i] = 1
> becomes
>  for (i = 0; i != 100; i++) arr[1] = 1
> 
> Hence treat != and == conditions specially in the verifier.
> Widen only not-predicted branch and keep predict branch as is. Example:
>   r1 = 0
>   goto L1
> L2:
>   arr[r1] = 1
>   r1++
> L1:
>   if r1 != 100 goto L2
>   fallthrough: r1=100 after widening
>   other_branch: r1 stays as-is (0, 1, 2, ..)

[...]

I'm not sure how much of a deal-breaker this is, but proposed
heuristics precludes verification for the following program:

  char arr[10];
  
  SEC("socket")
  __success __flag(BPF_F_TEST_STATE_FREQ)
  int simple_loop(const void *ctx)
  {
  	struct bpf_iter_num it;
  	int *v, sum = 0, i = 0;
  
  	bpf_iter_num_new(&it, 0, 10);
  	while ((v = bpf_iter_num_next(&it))) {
  		if (i < 5)
  			sum += arr[i++];
  	}
  	bpf_iter_num_destroy(&it);
  	return sum;
  }

The presence of the loop with bpf_iter_num creates a set of states
with non-null loop_header, which in turn switches-off predictions for
comparison operations inside the loop.
This looks like a bad a compose-ability of verifier features to me.

--

Instead of heuristics, maybe rely on hints from the programmer?
E.g. add a kfunc `u64 bpf_widen(u64)` which will be compiled as an
identity function, but would instruct verifier to drop precision for a
specific value. When work on no_caller_saved_registers finishes this
even could be available w/o runtime cost.
(And at the moment could be emulated by something like `rX /= 1`).
Alexei Starovoitov May 29, 2024, 12:34 a.m. UTC | #4 
On Mon, May 27, 2024 at 9:10 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Fri, 2024-05-24 at 20:11 -0700, Alexei Starovoitov wrote:
> > From: Alexei Starovoitov <ast@kernel.org>
>
> [...]
>
> > With that the get_loop_entry() can be used to gate is_branch_taken() logic.
> > When the verifier sees 'r1 > 1000' inside the loop and it can predict it
> > instead of marking r1 as precise it widens both branches, so r1 becomes
> > [0, 1000] in fallthrough and [1001, UMAX] in other_branch.
> >
> > Consider the loop:
> >     bpf_for_each(...) {
> >        if (r1 > 1000)
> >           break;
> >
> >        arr[r1] = ..;
> >     }
> > At arr[r1] access the r1 is bounded and the loop can quickly converge.
> >
> > Unfortunately compilers (both GCC and LLVM) often optimize loop exit
> > condition to equality, so
> >  for (i = 0; i < 100; i++) arr[i] = 1
> > becomes
> >  for (i = 0; i != 100; i++) arr[1] = 1
> >
> > Hence treat != and == conditions specially in the verifier.
> > Widen only not-predicted branch and keep predict branch as is. Example:
> >   r1 = 0
> >   goto L1
> > L2:
> >   arr[r1] = 1
> >   r1++
> > L1:
> >   if r1 != 100 goto L2
> >   fallthrough: r1=100 after widening
> >   other_branch: r1 stays as-is (0, 1, 2, ..)
>
> [...]
>
> I'm not sure how much of a deal-breaker this is, but proposed
> heuristics precludes verification for the following program:

not quite.

>   char arr[10];
>
>   SEC("socket")
>   __success __flag(BPF_F_TEST_STATE_FREQ)
>   int simple_loop(const void *ctx)
>   {
>         struct bpf_iter_num it;
>         int *v, sum = 0, i = 0;
>
>         bpf_iter_num_new(&it, 0, 10);
>         while ((v = bpf_iter_num_next(&it))) {
>                 if (i < 5)
>                         sum += arr[i++];
>         }
>         bpf_iter_num_destroy(&it);
>         return sum;
>   }
>
> The presence of the loop with bpf_iter_num creates a set of states
> with non-null loop_header, which in turn switches-off predictions for
> comparison operations inside the loop.

Is this a pseudo code ?
Because your guess at the reason for the verifier reject is not correct.
It's signed stuff that is causing issues.
s/int i/__u32 i/
and this test is passing the verifier with just 143 insn processed.

> This looks like a bad a compose-ability of verifier features to me.

As with any heuristic there are two steps forward and one step back.
The heuristic is trying to minimize the size of that step back.
If you noticed in v1 and v2 I had to add 'if (!v) break;'
to iter_pragma_unroll_loop().
And it would have been ok this way.
It is a step back for a corner case like iter_pragma_unroll_loop().
Luckily this new algorithm in v3 doesn't need this if (!v) workaround
anymore. So the step back is minimized.
Is it still there? Absolutely. There is a chance that some working prog
will stop working. (as with any verifier change).


> --
>
> Instead of heuristics, maybe rely on hints from the programmer?
> E.g. add a kfunc `u64 bpf_widen(u64)` which will be compiled as an
> identity function, but would instruct verifier to drop precision for a
> specific value. When work on no_caller_saved_registers finishes this
> even could be available w/o runtime cost.
> (And at the moment could be emulated by something like `rX /= 1`).

No way. i = zero is an unpleasant enough workaround.
The verifier precision tracking is not something users understand.
Using i=zero is not pretty, but asking them doing i = bpf_widen(0)
or i = 0; asm("i /= 1") is definitely no go.
The main issue is that users don't know when to do that.
bpf_widen(0) is magic. People will be just guessing.
Just like i=zero is magical.
All such magic has to go. The users should write normal C.
Eduard Zingerman May 29, 2024, 1:08 a.m. UTC | #5 
On Tue, 2024-05-28 at 17:34 -0700, Alexei Starovoitov wrote:

[...]

> > I'm not sure how much of a deal-breaker this is, but proposed
> > heuristics precludes verification for the following program:
> 
> not quite.
> 
> >   char arr[10];
> > 
> >   SEC("socket")
> >   __success __flag(BPF_F_TEST_STATE_FREQ)
> >   int simple_loop(const void *ctx)
> >   {
> >         struct bpf_iter_num it;
> >         int *v, sum = 0, i = 0;
> > 
> >         bpf_iter_num_new(&it, 0, 10);
> >         while ((v = bpf_iter_num_next(&it))) {
> >                 if (i < 5)
> >                         sum += arr[i++];
> >         }
> >         bpf_iter_num_destroy(&it);
> >         return sum;
> >   }
> > 
> > The presence of the loop with bpf_iter_num creates a set of states
> > with non-null loop_header, which in turn switches-off predictions for
> > comparison operations inside the loop.
> 
> Is this a pseudo code ?

No, I tried this test with v3 of this patch and on master.
It passes on master and fails with v3.
(Full test in the end of the email, I run it as
 ./test_progs -vvv -a verifier_loops1/simple_loop).

> Because your guess at the reason for the verifier reject is not correct.
> It's signed stuff that is causing issues.
> s/int i/__u32 i/
> and this test is passing the verifier with just 143 insn processed.

I'm reading through verifier log, will get back shortly.

> > This looks like a bad a compose-ability of verifier features to me.
> 
> As with any heuristic there are two steps forward and one step back.
> The heuristic is trying to minimize the size of that step back.
> If you noticed in v1 and v2 I had to add 'if (!v) break;'
> to iter_pragma_unroll_loop().
> And it would have been ok this way.
> It is a step back for a corner case like iter_pragma_unroll_loop().
> Luckily this new algorithm in v3 doesn't need this if (!v) workaround
> anymore. So the step back is minimized.
> Is it still there? Absolutely. There is a chance that some working prog
> will stop working. (as with any verifier change).

Not sure I understand how 'if (!v) break;' is relevant.
The patch says:

+		ignore_pred = (get_loop_entry(this_branch) ||
+			       this_branch->may_goto_depth) &&
+				/* Gate widen_reg() logic */
+				env->bpf_capable;

get_loop_entry(this_branch) would return true for states inside a
'while' because of the bpf_iter_num_next() calls.
Hence, predictions for all conditionals inside the loop would be
ignored and also src/dst registers would be widened because comparison
is not JEQ/JNE.

[...]

> Just like i=zero is magical.
> All such magic has to go. The users should write normal C.

Noted.

---

diff --git a/tools/testing/selftests/bpf/progs/verifier_loops1.c b/tools/testing/selftests/bpf/progs/verifier_loops1.c
index e07b43b78fd2..1ebf0c829d5e 100644
--- a/tools/testing/selftests/bpf/progs/verifier_loops1.c
+++ b/tools/testing/selftests/bpf/progs/verifier_loops1.c
@@ -283,4 +283,22 @@ exit_%=:                                           \
        : __clobber_all);
 }
 
+char arr[10];
+
+SEC("socket")
+__success __flag(BPF_F_TEST_STATE_FREQ)
+int simple_loop(const void *ctx)
+{
+      struct bpf_iter_num it;
+      int *v, sum = 0, i = 0;
+
+      bpf_iter_num_new(&it, 0, 10);
+      while ((v = bpf_iter_num_next(&it))) {
+              if (i < 5)
+                      sum += arr[i++];
+      }
+      bpf_iter_num_destroy(&it);
+      return sum;
+}
+
 char _license[] SEC("license") = "GPL";
Eduard Zingerman May 29, 2024, 2:18 a.m. UTC | #6 
On Tue, 2024-05-28 at 18:08 -0700, Eduard Zingerman wrote:

[...]

> > Because your guess at the reason for the verifier reject is not correct.
> > It's signed stuff that is causing issues.
> > s/int i/__u32 i/
> > and this test is passing the verifier with just 143 insn processed.
> 
> I'm reading through verifier log, will get back shortly.

Ok, so it is a bit more subtle than I thought.
Comparing verification log for master and v3 here is the state in
which they diverge and v3 rejects the program:

    from 14 to 15: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5) R7=2
                   R10=fp0 fp-8=iter_num(ref_id=1,state=active,depth=3) refs=1
    15: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5)
        R7=2 R10=fp0 fp-8=iter_num(ref_id=1,state=active,depth=3) refs=1
    15: (55) if r0 != 0x0 goto pc+5       ; R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) refs=1
    ; if (i < 5) @ verifier_loops1.c:298
0-> 21: (65) if r7 s> 0x4 goto pc-10      ; R7=2 refs=1
    21: refs=1
    ; sum += arr[i++]; @ verifier_loops1.c:299
1-> 22: (bf) r1 = r7                      ; R1_w=scalar(id=7,smax=4) R7=scalar(id=7,smax=4) refs=1
2-> 23: (67) r1 <<= 3                     ; R1_w=scalar(smax=0x7ffffffffffffff8,
                                                        umax=0xfffffffffffffff8,
                                                        smax32=0x7ffffff8,
                                                        umax32=0xfffffff8,
                                                        var_off=(0x0; 0xfffffffffffffff8)) refs=1
    24: (18) r2 = 0xffffc900000f6000      ; R2_w=map_value(map=verifier.bss,ks=4,vs=80) refs=1
    26: (0f) r2 += r1
    mark_precise: frame0: last_idx 26 first_idx 21 subseq_idx -1 
    ...
    math between map_value pointer and register with unbounded min value is not allowed

At point (0) the r7 is tracked as 2, at point (1) it is widened by the
following code in the falltrhough branch processing:

+		if (ignore_pred) {
+			if (opcode != BPF_JEQ && opcode != BPF_JNE) {
+				widen_reg(dst_reg);
+				if (has_src_reg)
+					widen_reg(src_reg);
+			}
+			widen_reg(other_dst_reg);
+			if (has_src_reg)
+				widen_reg(other_src_reg);
+		} else {

Here src_reg is a fake register set to 4,
because comparison instruction is BPF_K it does not get widened.
So, reg_set_min_max() produces range [-SMIN,+4] for R7.
And at (2) all goes south because of the "<<" logic.
Switch to unsigned values helps because umax range is computed
instead of smax at point (1).

However, below is an example where if comparison is BPF_X.
Note that I obfuscated constant 5 as a volatile variable.
And here is what happens when verifier rejects the program:

    from 16 to 17: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5)
                   R7=2 R10=fp0 fp-8=5 fp-16=iter_num(ref_id=1,state=active,depth=3) refs=1
    17: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5)
        R7=2 R10=fp0 fp-8=5 fp-16=iter_num(ref_id=1,state=active,depth=3) refs=1
    17: (55) if r0 != 0x0 goto pc+5       ; R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) refs=1
    ; if (i < five) @ verifier_loops1.c:299
    23: (79) r1 = *(u64 *)(r10 -8)        ; R1=5 R10=fp0 fp-8=5 refs=1
0-> 24: (3d) if r7 >= r1 goto pc-11       ; R1=5 R7=2 refs=1
    24: refs=1
    ; sum += arr[i++]; @ verifier_loops1.c:300
1-> 25: (bf) r1 = r7                      ; R1_w=scalar(id=7,umax=0xfffffffffffffffe)
                                            R7=scalar(id=7,umax=0xfffffffffffffffe) refs=1
    26: (67) r1 <<= 3                     ; R1_w=scalar(smax=0x7ffffffffffffff8,umax=0xfffffffffffffff8,
                                                        smax32=0x7ffffff8,umax32=0xfffffff8,
                                                        var_off=(0x0; 0xfffffffffffffff8)) refs=1
    27: (18) r2 = 0xffffc90000112000      ; R2_w=map_value(map=verifier.bss,ks=4,vs=80) refs=1
    29: (0f) r2 += r1

Note R7 has exact value 2 at point (0) and is widened to
umax=0xfffffffffffffffe at point (1).
Widening happens at the same point as before, but this time src_reg is
widened as well, so there is no upper bound for r7 anymore.

---

diff --git a/tools/testing/selftests/bpf/progs/verifier_loops1.c b/tools/testing/selftests/bpf/progs/verifier_loops1.c
index e07b43b78fd2..0249fb63f18b 100644
--- a/tools/testing/selftests/bpf/progs/verifier_loops1.c
+++ b/tools/testing/selftests/bpf/progs/verifier_loops1.c
@@ -283,4 +283,24 @@ exit_%=:                                           \
        : __clobber_all);
 }
 
+unsigned long arr[10];
+
+SEC("socket")
+__success __flag(BPF_F_TEST_STATE_FREQ)
+int simple_loop(const void *ctx)
+{
+      volatile unsigned long five = 5;
+      unsigned long sum = 0, i = 0;
+      struct bpf_iter_num it;
+      int *v;
+
+      bpf_iter_num_new(&it, 0, 10);
+      while ((v = bpf_iter_num_next(&it))) {
+              if (i < five)
+                      sum += arr[i++];
+      }
+      bpf_iter_num_destroy(&it);
+      return sum;
+}
+
Alexei Starovoitov May 29, 2024, 3:22 a.m. UTC | #7 
On Tue, May 28, 2024 at 7:18 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Tue, 2024-05-28 at 18:08 -0700, Eduard Zingerman wrote:
>
> [...]
>
> > > Because your guess at the reason for the verifier reject is not correct.
> > > It's signed stuff that is causing issues.
> > > s/int i/__u32 i/
> > > and this test is passing the verifier with just 143 insn processed.
> >
> > I'm reading through verifier log, will get back shortly.
>
> Ok, so it is a bit more subtle than I thought.
> Comparing verification log for master and v3 here is the state in
> which they diverge and v3 rejects the program:
>
>     from 14 to 15: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5) R7=2
>                    R10=fp0 fp-8=iter_num(ref_id=1,state=active,depth=3) refs=1
>     15: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5)
>         R7=2 R10=fp0 fp-8=iter_num(ref_id=1,state=active,depth=3) refs=1
>     15: (55) if r0 != 0x0 goto pc+5       ; R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) refs=1
>     ; if (i < 5) @ verifier_loops1.c:298
> 0-> 21: (65) if r7 s> 0x4 goto pc-10      ; R7=2 refs=1
>     21: refs=1
>     ; sum += arr[i++]; @ verifier_loops1.c:299
> 1-> 22: (bf) r1 = r7                      ; R1_w=scalar(id=7,smax=4) R7=scalar(id=7,smax=4) refs=1
> 2-> 23: (67) r1 <<= 3                     ; R1_w=scalar(smax=0x7ffffffffffffff8,
>                                                         umax=0xfffffffffffffff8,
>                                                         smax32=0x7ffffff8,
>                                                         umax32=0xfffffff8,
>                                                         var_off=(0x0; 0xfffffffffffffff8)) refs=1
>     24: (18) r2 = 0xffffc900000f6000      ; R2_w=map_value(map=verifier.bss,ks=4,vs=80) refs=1
>     26: (0f) r2 += r1
>     mark_precise: frame0: last_idx 26 first_idx 21 subseq_idx -1
>     ...
>     math between map_value pointer and register with unbounded min value is not allowed
>
> At point (0) the r7 is tracked as 2, at point (1) it is widened by the
> following code in the falltrhough branch processing:
>
> +               if (ignore_pred) {
> +                       if (opcode != BPF_JEQ && opcode != BPF_JNE) {
> +                               widen_reg(dst_reg);
> +                               if (has_src_reg)
> +                                       widen_reg(src_reg);
> +                       }
> +                       widen_reg(other_dst_reg);
> +                       if (has_src_reg)
> +                               widen_reg(other_src_reg);
> +               } else {
>
> Here src_reg is a fake register set to 4,
> because comparison instruction is BPF_K it does not get widened.
> So, reg_set_min_max() produces range [-SMIN,+4] for R7.
> And at (2) all goes south because of the "<<" logic.
> Switch to unsigned values helps because umax range is computed
> instead of smax at point (1).

Exactly. Unsigned is the answer (as I mentioned in the previous email).
The heuristic of _not_ doing bounded loop inside open iter
is that step back that may cause pain.
But really, doing bpf_for() { for(i; i < ..;i++) ..}
is asking for trouble, since it's mixing two concepts.

And in this case the compiler is confused too,
since it cannot normalize i < 5 into i != 5 as it would
do for a canonical loop.

>
> However, below is an example where if comparison is BPF_X.
> Note that I obfuscated constant 5 as a volatile variable.
> And here is what happens when verifier rejects the program:

Sounds pretty much like: doctor it hurts when I do that.

> +      volatile unsigned long five = 5;
> +      unsigned long sum = 0, i = 0;
> +      struct bpf_iter_num it;
> +      int *v;
> +
> +      bpf_iter_num_new(&it, 0, 10);
> +      while ((v = bpf_iter_num_next(&it))) {
> +              if (i < five)
> +                      sum += arr[i++];

If you're saying that the verifier should accept that
no matter what then I have to disagree.
Not interested in avoiding issues in programs that
are actively looking to explore a verifier implementation detail.

I'll add this test with __u64 i = 0;
to demo how such mixed loop constructs can be used.
-no_alu32, default and -cpuv4 all pass.
Eduard Zingerman May 29, 2024, 10:14 a.m. UTC | #8 
On Tue, 2024-05-28 at 20:22 -0700, Alexei Starovoitov wrote:

[...]

> 

> > However, below is an example where if comparison is BPF_X.
> > Note that I obfuscated constant 5 as a volatile variable.
> > And here is what happens when verifier rejects the program:
> 
> Sounds pretty much like: doctor it hurts when I do that.

Well, the point is not in the volatile variable but in the BPF_X
comparison instruction. The bound might a size of some buffer,
e.g. encoded like this:

struct foo {
  int *items;
  int max_items; // suppose this is 5 for some verification path
};               // and 7 for another.

And you don't need bpf_for specifically, an outer loop with
can_loop should also lead to get_loop_entry(...) being non-NULL.

> > +      volatile unsigned long five = 5;
> > +      unsigned long sum = 0, i = 0;
> > +      struct bpf_iter_num it;
> > +      int *v;
> > +
> > +      bpf_iter_num_new(&it, 0, 10);
> > +      while ((v = bpf_iter_num_next(&it))) {
> > +              if (i < five)
> > +                      sum += arr[i++];
> 
> If you're saying that the verifier should accept that
> no matter what then I have to disagree.
> Not interested in avoiding issues in programs that
> are actively looking to explore a verifier implementation detail.

I don't think that this is a very exotic pattern,
such code could be written if one has a buffer with a dynamic bound
and seeks to fill it with items from some collection applying filtering.

I do not insist that varifier should accept such programs,
but since we are going for heuristics to do the widening,
I think we should try and figure out a few examples when
heuristics breaks, just to understand if that is ok.
Dan Carpenter May 29, 2024, 2:32 p.m. UTC | #9 
On Mon, May 27, 2024 at 03:44:44PM -0700, Alexei Starovoitov wrote:
> > 484611357c19f9 Josef Bacik        2016-09-28  15313     if (BPF_SRC(insn->code) == BPF_X) {
> > 5f99f312bd3bed Andrii Nakryiko    2023-11-11  15314             err = reg_set_min_max(env,
> > 689049426b9d3b Alexei Starovoitov 2024-05-24 @15315                                   other_dst_reg, other_src_reg,
> >                                                                                       ^^^^^^^^^^^^^
> >
> > 4621202adc5bc0 Andrii Nakryiko    2023-11-01  15316                                   dst_reg, src_reg, opcode, is_jmp32);
> > 4621202adc5bc0 Andrii Nakryiko    2023-11-01  15317     } else /* BPF_SRC(insn->code) == BPF_K */ {
> > 5f99f312bd3bed Andrii Nakryiko    2023-11-11  15318             err = reg_set_min_max(env,
> > 689049426b9d3b Alexei Starovoitov 2024-05-24  15319                                   other_dst_reg,
> >                                                                                       ^^^^^^^^^^^^^
> > Passed to reg_set_min_max() without being initialized.
> 
> No. It's initialized when passed. It's a false positive.
> Try to make smatch smarter?

Ah yes.  I didn't read it carefully enough.

The kbuild bot doesn't use cross function analysis.  So it didn't know
that pred can only be -1, 0, or 1.  If you have cross function analysis
this should work.  Unfortunately cross function analysis is too slow to
scale enough for the zero day bot.

regards,
dan carpenter
Alexei Starovoitov June 1, 2024, 3:08 a.m. UTC | #10 
On Wed, May 29, 2024 at 3:14 AM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Tue, 2024-05-28 at 20:22 -0700, Alexei Starovoitov wrote:
>
> [...]
>
> >
>
> > > However, below is an example where if comparison is BPF_X.
> > > Note that I obfuscated constant 5 as a volatile variable.
> > > And here is what happens when verifier rejects the program:
> >
> > Sounds pretty much like: doctor it hurts when I do that.
>
> Well, the point is not in the volatile variable but in the BPF_X
> comparison instruction. The bound might a size of some buffer,
> e.g. encoded like this:
>
> struct foo {
>   int *items;
>   int max_items; // suppose this is 5 for some verification path
> };               // and 7 for another.
>
> And you don't need bpf_for specifically, an outer loop with
> can_loop should also lead to get_loop_entry(...) being non-NULL.

Right. Open coded iters and can_loop have the same convergence
property. They both need loop iterations to look like infinite
loop (same states) while bounded loop logic needs the opposite.
It needs loop states to be different otherwise it's an infinite loop
and prog is rejected.
So it's simply impossible for the verifier to excel in both.
The heuristic I'm adding is trying to make it work well
for open coded iters and focusing on converging when loop count
is high and impractical for a bounded loop.
At the same time the heuristic is trying not to degrade a corner
case where bounded loop logic might help (by recognizing
const_dst ?= const_src and not widening equality operation).
But heuristic is not going to be perfect.

As I said it's two steps forward and minimal step back.
I'm adding the following selftests:
       volatile const int limit = 100000; /* global */
        while ((v = bpf_iter_num_next(&it))) {
                if (i < limit)
                        sum += arr[i++];
        }
influenced by your test and it passes due to widening logic.
Such a test is an impossible task for a bounded loop.
Hence this step forward for open coded iters is much
bigger than corner case loss of bounded loop logic inside
open coded iter.

> > > +      volatile unsigned long five = 5;
> > > +      unsigned long sum = 0, i = 0;
> > > +      struct bpf_iter_num it;
> > > +      int *v;
> > > +
> > > +      bpf_iter_num_new(&it, 0, 10);
> > > +      while ((v = bpf_iter_num_next(&it))) {
> > > +              if (i < five)
> > > +                      sum += arr[i++];
> >
> > If you're saying that the verifier should accept that
> > no matter what then I have to disagree.
> > Not interested in avoiding issues in programs that
> > are actively looking to explore a verifier implementation detail.
>
> I don't think that this is a very exotic pattern,
> such code could be written if one has a buffer with a dynamic bound
> and seeks to fill it with items from some collection applying filtering.

After thinking more I had to agree. Hence I added it as a test.
volatile on stack is exotic and impractical, but
volatile const int limit;
as global var is a very real use case.

My widening logic was indeed too broad for BPF_X case.
reg_set_min_max() will see two unknown scalars and there will be
nothing to learn bounds from.
I'm fixing it with a double call to reg_set_min_max().
Once for src and other_src and 2nd time for dst and other_dst.
This way "i < five" is properly widened for both registers.

> I do not insist that varifier should accept such programs,
> but since we are going for heuristics to do the widening,
> I think we should try and figure out a few examples when
> heuristics breaks, just to understand if that is ok.

btw the existing widen_imprecise_scalars() heuristic
for open coded iters is more or less the same thing.
It may hurt bounded loop logic too. A bit of hand waving:
while ((v = bpf_iter_num_next(&it))) {
   if (i < 100) {
        j++;
        i++;
        // use 'j' such that it's safe only when 'j' is precise.
  }

Without this patch 'i < 100' will force precision on 'i',
but widen_imprecise_scalars() might widen 'j'.

At the end the users would need to understand how the
verifier widened 'i < 100' to write progs with open coded iters
and normal maps.
Or they will switch to may_goto and arena and things will "just work".

In arena progs we currently do a ton of useless mark_chain_precision
work because of 'i < 100' conditions. When all other pointers are arena
pointers they don't trigger precision marking.
Only 'i < 100' do. So after this patch the verifier is doing a lot
less work for arena programs. That's another reason why I want
to remove precision marking after is_branch_taken.

Anyway, v4 will be soon.
diff mbox series

Patch

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 77da1f438bec..2b79b623b492 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2321,6 +2321,14 @@  static void __mark_reg_unknown(const struct bpf_verifier_env *env,
 	reg->precise = !env->bpf_capable;
 }
 
+static void widen_reg(struct bpf_reg_state *reg)
+{
+	u32 id = reg->id;
+
+	__mark_reg_unknown_imprecise(reg);
+	reg->id = id;
+}
+
 static void mark_reg_unknown(struct bpf_verifier_env *env,
 			     struct bpf_reg_state *regs, u32 regno)
 {
@@ -15104,10 +15112,11 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 	struct bpf_verifier_state *other_branch;
 	struct bpf_reg_state *regs = this_branch->frame[this_branch->curframe]->regs;
 	struct bpf_reg_state *dst_reg, *other_branch_regs, *src_reg = NULL;
-	struct bpf_reg_state *eq_branch_regs;
+	struct bpf_reg_state *eq_branch_regs, *other_dst_reg, *other_src_reg = NULL;
 	struct bpf_reg_state fake_reg = {};
 	u8 opcode = BPF_OP(insn->code);
-	bool is_jmp32;
+	bool is_jmp32, ignore_pred;
+	bool has_src_reg = false;
 	int pred = -1;
 	int err;
 
@@ -15159,6 +15168,7 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 		if (err)
 			return err;
 
+		has_src_reg = true;
 		src_reg = &regs[insn->src_reg];
 		if (!(reg_is_pkt_pointer_any(dst_reg) && reg_is_pkt_pointer_any(src_reg)) &&
 		    is_pointer_value(env, insn->src_reg)) {
@@ -15177,8 +15187,42 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 	}
 
 	is_jmp32 = BPF_CLASS(insn->code) == BPF_JMP32;
+	if (dst_reg->type != SCALAR_VALUE || src_reg->type != SCALAR_VALUE)
+		ignore_pred = false;
+	/*
+	 * Compilers often optimize loop exit condition to equality, so
+	 *      for (i = 0; i < 100; i++) arr[i] = 1
+	 * becomes
+	 *      for (i = 0; i != 100; i++) arr[1] = 1
+	 * Hence treat != and == conditions specially in the verifier.
+	 * Widen only not-predicted branch and keep predict branch as is. Example:
+	 *    r1 = 0
+	 *    goto L1
+	 * L2:
+	 *    arr[r1] = 1
+	 *    r1++
+	 * L1:
+	 *    if r1 != 100 goto L2
+	 *    fallthrough: r1=100 after widening
+	 *    other_branch: r1 stays as-is (0, 1, 2, ..)
+	 *
+	 *  Also recognize the case where both LHS and RHS are constant and
+	 *  equal to each other. In this case don't widen at all and take the
+	 *  predicted path. This key heuristic allows the verifier detect loop
+	 *  end condition and 'for (i = 0; i != 100; i++)' is validated just
+	 *  like bounded loop.
+	 */
+	else if (is_reg_const(dst_reg, is_jmp32) && is_reg_const(src_reg, is_jmp32) &&
+	    reg_const_value(dst_reg, is_jmp32) == reg_const_value(src_reg, is_jmp32))
+		ignore_pred = false;
+	else
+		ignore_pred = (get_loop_entry(this_branch) ||
+			       this_branch->may_goto_depth) &&
+				/* Gate widen_reg() logic */
+				env->bpf_capable;
+
 	pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
-	if (pred >= 0) {
+	if (pred >= 0 && !ignore_pred) {
 		/* If we get here with a dst_reg pointer type it is because
 		 * above is_branch_taken() special cased the 0 comparison.
 		 */
@@ -15191,6 +15235,17 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 			return err;
 	}
 
+	if (pred < 0 || ignore_pred) {
+		other_branch = push_stack(env, *insn_idx + insn->off + 1, *insn_idx,
+					  false);
+		if (!other_branch)
+			return -EFAULT;
+		other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
+		other_dst_reg = &other_branch_regs[insn->dst_reg];
+		if (has_src_reg)
+			other_src_reg = &other_branch_regs[insn->src_reg];
+	}
+
 	if (pred == 1) {
 		/* Only follow the goto, ignore fall-through. If needed, push
 		 * the fall-through branch for simulation under speculative
@@ -15202,8 +15257,33 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 			return -EFAULT;
 		if (env->log.level & BPF_LOG_LEVEL)
 			print_insn_state(env, this_branch->frame[this_branch->curframe]);
-		*insn_idx += insn->off;
-		return 0;
+		if (ignore_pred) {
+			/* dst and src regs are scalars. Widen them */
+			widen_reg(dst_reg);
+			if (has_src_reg)
+				widen_reg(src_reg);
+			/*
+			 * Widen other branch only if not comparing for equlity.
+			 * Example:
+			 *   r1 = 1
+			 *   if (r1 < 100)
+			 * will produce
+			 *   [0, 99] and [100, UMAX] after widening and reg_set_min_max().
+			 *
+			 *   r1 = 1
+			 *   if (r1 == 100)
+			 * will produce
+			 *    [1] and [100] after widening in other_branch and reg_set_min_max().
+			 */
+			if (opcode != BPF_JEQ && opcode != BPF_JNE) {
+				widen_reg(other_dst_reg);
+				if (has_src_reg)
+					widen_reg(other_src_reg);
+			}
+		} else {
+			*insn_idx += insn->off;
+			return 0;
+		}
 	} else if (pred == 0) {
 		/* Only follow the fall-through branch, since that's where the
 		 * program will go. If needed, push the goto branch for
@@ -15216,23 +15296,27 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 			return -EFAULT;
 		if (env->log.level & BPF_LOG_LEVEL)
 			print_insn_state(env, this_branch->frame[this_branch->curframe]);
-		return 0;
+		if (ignore_pred) {
+			if (opcode != BPF_JEQ && opcode != BPF_JNE) {
+				widen_reg(dst_reg);
+				if (has_src_reg)
+					widen_reg(src_reg);
+			}
+			widen_reg(other_dst_reg);
+			if (has_src_reg)
+				widen_reg(other_src_reg);
+		} else {
+			return 0;
+		}
 	}
 
-	other_branch = push_stack(env, *insn_idx + insn->off + 1, *insn_idx,
-				  false);
-	if (!other_branch)
-		return -EFAULT;
-	other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
-
 	if (BPF_SRC(insn->code) == BPF_X) {
 		err = reg_set_min_max(env,
-				      &other_branch_regs[insn->dst_reg],
-				      &other_branch_regs[insn->src_reg],
+				      other_dst_reg, other_src_reg,
 				      dst_reg, src_reg, opcode, is_jmp32);
 	} else /* BPF_SRC(insn->code) == BPF_K */ {
 		err = reg_set_min_max(env,
-				      &other_branch_regs[insn->dst_reg],
+				      other_dst_reg,
 				      src_reg /* fake one */,
 				      dst_reg, src_reg /* same fake one */,
 				      opcode, is_jmp32);
@@ -15240,16 +15324,16 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 	if (err)
 		return err;
 
-	if (BPF_SRC(insn->code) == BPF_X &&
+	if (has_src_reg &&
 	    src_reg->type == SCALAR_VALUE && src_reg->id &&
-	    !WARN_ON_ONCE(src_reg->id != other_branch_regs[insn->src_reg].id)) {
+	    !WARN_ON_ONCE(src_reg->id != other_src_reg->id)) {
 		find_equal_scalars(this_branch, src_reg);
-		find_equal_scalars(other_branch, &other_branch_regs[insn->src_reg]);
+		find_equal_scalars(other_branch, other_src_reg);
 	}
 	if (dst_reg->type == SCALAR_VALUE && dst_reg->id &&
-	    !WARN_ON_ONCE(dst_reg->id != other_branch_regs[insn->dst_reg].id)) {
+	    !WARN_ON_ONCE(dst_reg->id != other_dst_reg->id)) {
 		find_equal_scalars(this_branch, dst_reg);
-		find_equal_scalars(other_branch, &other_branch_regs[insn->dst_reg]);
+		find_equal_scalars(other_branch, other_dst_reg);
 	}
 
 	/* if one pointer register is compared to another pointer
@@ -15264,7 +15348,7 @@  static int check_cond_jmp_op(struct bpf_verifier_env *env,
 	 * could be null even without PTR_MAYBE_NULL marking, so
 	 * only propagate nullness when neither reg is that type.
 	 */
-	if (!is_jmp32 && BPF_SRC(insn->code) == BPF_X &&
+	if (!is_jmp32 && has_src_reg &&
 	    __is_pointer_value(false, src_reg) && __is_pointer_value(false, dst_reg) &&
 	    type_may_be_null(src_reg->type) != type_may_be_null(dst_reg->type) &&
 	    base_type(src_reg->type) != PTR_TO_BTF_ID &&
@@ -17409,6 +17493,7 @@  static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
 			 * => unsafe memory access at 11 would not be caught.
 			 */
 			if (is_iter_next_insn(env, insn_idx)) {
+				update_loop_entry(cur, &sl->state);
 				if (states_equal(env, &sl->state, cur, RANGE_WITHIN)) {
 					struct bpf_func_state *cur_frame;
 					struct bpf_reg_state *iter_state, *iter_reg;
@@ -17425,18 +17510,15 @@  static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
 					 */
 					spi = __get_spi(iter_reg->off + iter_reg->var_off.value);
 					iter_state = &func(env, iter_reg)->stack[spi].spilled_ptr;
-					if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE) {
-						update_loop_entry(cur, &sl->state);
+					if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE)
 						goto hit;
-					}
 				}
 				goto skip_inf_loop_check;
 			}
 			if (is_may_goto_insn_at(env, insn_idx)) {
-				if (states_equal(env, &sl->state, cur, RANGE_WITHIN)) {
-					update_loop_entry(cur, &sl->state);
+				update_loop_entry(cur, &sl->state);
+				if (states_equal(env, &sl->state, cur, RANGE_WITHIN))
 					goto hit;
-				}
 				goto skip_inf_loop_check;
 			}
 			if (calls_callback(env, insn_idx)) {