Re: [PATCH bpf-next v1 3/4] bpf: use SCC info instead of loop_entry

[Eduard Zingerman <eddyz87@gmail.com>]

On Sat, 2025-04-26 at 22:45 +0800, kernel test robot wrote:
> Hi Eduard,
> 
> kernel test robot noticed the following build warnings:
> 
> [auto build test WARNING on bpf-next/master]
> 
> url:    https://github.com/intel-lab-lkp/linux/commits/Eduard-Zingerman/bpf-compute-SCCs-in-program-control-flow-graph/20250426-184824
> base:   https://git.kernel.org/pub/scm/linux/kernel/git/bpf/bpf-next.git master
> patch link:    https://lore.kernel.org/r/20250426104634.744077-4-eddyz87%40gmail.com
> patch subject: [PATCH bpf-next v1 3/4] bpf: use SCC info instead of loop_entry
> config: riscv-randconfig-001-20250426 (https://download.01.org/0day-ci/archive/20250426/202504262235.h5B7vJiB-lkp@intel.com/config)
> compiler: riscv64-linux-gcc (GCC) 14.2.0
> reproduce (this is a W=1 build): (https://download.01.org/0day-ci/archive/20250426/202504262235.h5B7vJiB-lkp@intel.com/reproduce)
> 
> 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>
> > Closes: https://lore.kernel.org/oe-kbuild-all/202504262235.h5B7vJiB-lkp@intel.com/
> 
> All warnings (new ones prefixed by >>):
> 
>    kernel/bpf/verifier.c: In function 'mark_all_regs_read_and_precise':
> > > kernel/bpf/verifier.c:18238:13: warning: variable 'insn_idx' set but not used [-Wunused-but-set-variable]
>    18238 |         u32 insn_idx;
>          |             ^~~~~~~~
>    At top level:
>    cc1: note: unrecognized command-line option '-Wno-unterminated-string-initialization' may have been intended to silence earlier diagnostics

I messed up when extracting frame_insn_idx().
The function needs to be updated as:

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index ae642459f342..06c2b3806666 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -18240,7 +18240,7 @@ static void mark_all_regs_read_and_precise(struct bpf_verifier_env *env,
 
        for (i = 0; i <= st->curframe; i++) {
                insn_idx = frame_insn_idx(st, i);
-               live_regs = env->insn_aux_data[st->insn_idx].live_regs_before;
+               live_regs = env->insn_aux_data[insn_idx].live_regs_before;
                func = st->frame[i];
                for (j = 0; j < BPF_REG_FP; j++) {
                        reg = &func->regs[j];

I'll try to figure out a test case failing w/o above hunk.
Also, patch #3 probably worth splitting in two:
- one adding new logic;
- one removing old logic.

Will wait a few days before sending v2.

> vim +/insn_idx +18238 kernel/bpf/verifier.c
> 
>  18154	
>  18155	/* Open coded iterators introduce loops in the verifier state graph.
>  18156	 * State graph loops can result in incomplete read and precision marks
>  18157	 * on individual states. E.g. consider the following states graph:
>  18158	 *
>  18159	 *  .-> A --.  Assume the states are visited in the order A, B, C.
>  18160	 *  |   |   |  Assume that state B reaches a state equivalent to state A.
>  18161	 *  |   v   v  At this point, state C has not been processed yet,
>  18162	 *  '-- B   C  so state A does not have any read or precision marks from C yet.
>  18163	 *             As a result, these marks won't be propagated to B.
>  18164	 *
>  18165	 * If the marks on B are incomplete, it would be unsafe to use it in
>  18166	 * states_equal() checks.
>  18167	 *
>  18168	 * To avoid this safety issue, and since states with incomplete read
>  18169	 * marks can only occur within control flow graph loops, the verifier
>  18170	 * assumes that any state with bpf_verifier_state->insn_idx residing
>  18171	 * in a strongly connected component (SCC) has read and precision
>  18172	 * marks for all registers. This assumption is enforced by the
>  18173	 * function mark_all_regs_read_and_precise(), which assigns
>  18174	 * corresponding marks.
>  18175	 *
>  18176	 * An intuitive point to call mark_all_regs_read_and_precise() would
>  18177	 * be when a new state is created in is_state_visited().
>  18178	 * However, doing so would interfere with widen_imprecise_scalars(),
>  18179	 * which widens scalars in the current state after checking registers in a
>  18180	 * parent state. Registers are not widened if they are marked as precise
>  18181	 * in the parent state.
>  18182	 *
>  18183	 * To avoid interfering with widening logic,
>  18184	 * a call to mark_all_regs_read_and_precise() for state is postponed
>  18185	 * until no widening is possible in any descendant of state S.
>  18186	 *
>  18187	 * Another intuitive spot to call mark_all_regs_read_and_precise()
>  18188	 * would be in update_branch_counts() when S's branches counter
>  18189	 * reaches 0. However, this falls short in the following case:
>  18190	 *
>  18191	 *	sum = 0
>  18192	 *	bpf_repeat(10) {                              // a
>  18193	 *		if (unlikely(bpf_get_prandom_u32()))  // b
>  18194	 *			sum += 1;
>  18195	 *		if (bpf_get_prandom_u32())            // c
>  18196	 *			asm volatile ("");
>  18197	 *		asm volatile ("goto +0;");            // d
>  18198	 *	}
>  18199	 *
>  18200	 * Here a checkpoint is created at (d) with {sum=0} and the branch counter
>  18201	 * for (d) reaches 0, so 'sum' would be marked precise.
>  18202	 * When second branch of (c) reaches (d), checkpoint would be hit,
>  18203	 * and the precision mark for 'sum' propagated to (a).
>  18204	 * When the second branch of (b) reaches (a), the state would be {sum=1},
>  18205	 * no widening would occur, causing verification to continue forever.
>  18206	 *
>  18207	 * To avoid such premature precision markings, the verifier postpones
>  18208	 * the call to mark_all_regs_read_and_precise() for state S even further.
>  18209	 * Suppose state P is a [grand]parent of state S and is the first state
>  18210	 * in the current state chain with state->insn_idx within current SCC.
>  18211	 * mark_all_regs_read_and_precise() for state S is only called once P
>  18212	 * is fully explored.
>  18213	 *
>  18214	 * The struct 'bpf_scc_info' is used to track this condition:
>  18215	 * - bpf_scc_info->branches counts how many states currently
>  18216	 *   in env->cur_state or env->head originate from this SCC;
>  18217	 * - bpf_scc_info->scc_epoch counts how many times 'branches'
>  18218	 *   has reached zero;
>  18219	 * - bpf_verifier_state->scc_epoch records the epoch of the SCC
>  18220	 *   corresponding to bpf_verifier_state->insn_idx at the moment
>  18221	 *   of state creation.
>  18222	 *
>  18223	 * Functions parent_scc_enter() and parent_scc_exit() maintain the
>  18224	 * bpf_scc_info->{branches,scc_epoch} counters.
>  18225	 *
>  18226	 * bpf_scc_info->branches reaching zero indicates that state P is
>  18227	 * fully explored. Its descendants residing in the same SCC have
>  18228	 * state->scc_epoch == scc_info->scc_epoch. parent_scc_exit()
>  18229	 * increments scc_info->scc_epoch, allowing clean_live_states() to
>  18230	 * detect these states and apply mark_all_regs_read_and_precise().
>  18231	 */
>  18232	static void mark_all_regs_read_and_precise(struct bpf_verifier_env *env,
>  18233						   struct bpf_verifier_state *st)
>  18234	{
>  18235		struct bpf_func_state *func;
>  18236		struct bpf_reg_state *reg;
>  18237		u16 live_regs;
>  18238		u32 insn_idx;
>  18239		int i, j;
>  18240	
>  18241		for (i = 0; i <= st->curframe; i++) {
>  18242			insn_idx = frame_insn_idx(st, i);
>  18243			live_regs = env->insn_aux_data[st->insn_idx].live_regs_before;
>  18244			func = st->frame[i];
>  18245			for (j = 0; j < BPF_REG_FP; j++) {
>  18246				reg = &func->regs[j];
>  18247				if (!(BIT(j) & live_regs) || reg->type == NOT_INIT)
>  18248					continue;
>  18249				reg->live |= REG_LIVE_READ64;
>  18250				if (reg->type == SCALAR_VALUE && !is_reg_unbounded(reg))
>  18251					reg->precise = true;
>  18252			}
>  18253			for (j = 0; j < func->allocated_stack / BPF_REG_SIZE; j++) {
>  18254				reg = &func->stack[j].spilled_ptr;
>  18255				reg->live |= REG_LIVE_READ64;
>  18256				if (is_spilled_reg(&func->stack[j]) &&
>  18257				    reg->type == SCALAR_VALUE && !is_reg_unbounded(reg))
>  18258					reg->precise = true;
>  18259			}
>  18260		}
>  18261	}
>  18262	
>