From: Alexei Starovoitov TLDR: not worth doing. When the verifier processes JEQ/JNE against a known constant, the existing logic in reg_set_min_max() refines: - equal branch: dst_reg = const (exact value) - not-equal branch: dst_reg != const (edge-trim only) The JNE edge-trim only tightens bounds when the constant sits at a range boundary (e.g. umin == const → umin++). For a register with range [0, 255] and "if r0 != 100", the not-equal branch keeps the full [0, 255] range — no useful information is gained. Improve this by forking the not-equal branch into two sub-states: - fork 1: dst > const (via JGT refinement → e.g. [101, 255]) - fork 2: dst < const (via JLT refinement → e.g. [0, 99]) This is implemented by pushing an additional verifier state onto the exploration stack after reg_set_min_max() and sync_linked_regs() have already processed the original two branches. The fork is guarded by feasibility checks requiring both unsigned and signed ranges to strictly span the constant (umin < val < umax and smin < val < smax). The signed check prevents infeasible states from reg_bounds_sync() cross-propagating signed bounds into unsigned after the JGT/JLT refinement. For JEQ: the not-equal branch is this_branch (fallthrough), and fork2 targets the next instruction. For JNE: the not-equal branch is other_branch (jump target), and push_stack copies env->cur_state (the equal branch), so dst_reg in fork2 must be overwritten with the not-equal branch's copy. Linked registers sharing the same ID are propagated via sync_linked_regs() on both forks. File Program Insns (A) Insns (B) Insns (DIFF) ------------------ ---------------------- --------- --------- ---------------- scx_beerland.bpf.o beerland_enqueue 332 361 +29 (+8.73%) scx_central.bpf.o central_enqueue 68 74 +6 (+8.82%) scx_central.bpf.o central_init 200 210 +10 (+5.00%) scx_chaos.bpf.o chaos_tick 14 15 +1 (+7.14%) scx_flash.bpf.o enable_sibling_cpu 120 113 -7 (-5.83%) scx_flatcg.bpf.o fcg_cgroup_init 120 132 +12 (+10.00%) scx_lavd.bpf.o lavd_dispatch 218925 237897 +18972 (+8.67%) scx_lavd.bpf.o lavd_quiescent 168 191 +23 (+13.69%) scx_lavd.bpf.o set_power_profile 167 109 -58 (-34.73%) scx_layered.bpf.o layered_dispatch 13909 14480 +571 (+4.11%) scx_layered.bpf.o layered_enqueue 13798 24143 +10345 (+74.97%) scx_layered.bpf.o layered_runnable 6077 6447 +370 (+6.09%) scx_layered.bpf.o layered_select_cpu 2288 3121 +833 (+36.41%) scx_layered.bpf.o layered_set_cpumask 238 250 +12 (+5.04%) scx_layered.bpf.o layered_stopping 598 643 +45 (+7.53%) scx_layered.bpf.o tp_task_rename 70 73 +3 (+4.29%) scx_qmap.bpf.o qmap_select_cpu 52 55 +3 (+5.77%) scx_rlfifo.bpf.o rustland_dispatch 340 363 +23 (+6.76%) scx_rustland.bpf.o rustland_dispatch 340 363 +23 (+6.76%) scx_rusty.bpf.o rusty_set_cpumask 3259 3552 +293 (+8.99%) scx_userland.bpf.o userland_enqueue 91 97 +6 (+6.59%) scx_userland.bpf.o userland_select_cpu 53 56 +3 (+5.66%) scxtop.bpf.o long_tail_tracker_exit 104 119 +15 (+14.42%) scxtop.bpf.o start_trace 127 134 +7 (+5.51%) Program Insns (A) Insns (B) Insns (DIFF) ---------------------------------------- --------- --------- ------------------ bpfj_dns_sendmsg 6322 8432 +2110 (+33.38%) bpfj_exec_execve 4790 4091 -699 (-14.59%) bpfj_exec_execveat 4790 4091 -699 (-14.59%) do_parse 157621 688994 +531373 (+337.12%) do_sendmsg 157635 689008 +531373 (+337.09%) balancer_ingress 62403 70516 +8113 (+13.00%) on_py_event 88094 76037 -12057 (-13.69%) on_custom_event_start 13847 15347 +1500 (+10.83%) Signed-off-by: Alexei Starovoitov --- kernel/bpf/verifier.c | 107 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index edf5342b982f..c9f0c62ab4e0 100644 --- a/kernel/bpf/verifier.c +++ b/kernel/bpf/verifier.c @@ -17579,6 +17579,113 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env, &linked_regs); } + /* For JEQ/JNE with a known constant, fork the not-equal branch + * into dst > const and dst < const for tighter range tracking. + */ + if ((opcode == BPF_JEQ || opcode == BPF_JNE) && + dst_reg->type == SCALAR_VALUE) { + struct bpf_verifier_state *neq_branch2, *neq_state; + struct bpf_reg_state *neq_regs, *neq2_regs; + struct bpf_reg_state fake_const; + bool can_fork = false; + s32 neq_target; + u64 val; + + /* Determine which src is the constant */ + if (BPF_SRC(insn->code) == BPF_K) { + val = (u64)(s64)insn->imm; + can_fork = true; + } else if (is_reg_const(src_reg, is_jmp32)) { + val = reg_const_value(src_reg, is_jmp32); + can_fork = true; + } else if (is_reg_const(dst_reg, is_jmp32)) { + /* dst is const — JNE/JEQ is symmetric for forking, + * but we'd fork on src's range. Skip for now. + */ + can_fork = false; + } + + if (can_fork) { + /* Identify the not-equal branch and check feasibility */ + if (opcode == BPF_JEQ) { + neq_regs = regs; /* this_branch = fallthrough = != */ + neq_target = *insn_idx + 1; + neq_state = this_branch; + } else { + neq_regs = other_branch_regs; /* other_branch = jump = != */ + neq_target = *insn_idx + insn->off + 1; + neq_state = other_branch; + } + + /* Check that the range spans across the constant. + * Check both unsigned and signed ranges, because + * reg_bounds_sync() may cross-propagate signed + * bounds into unsigned after JGT/JLT refinement, + * creating infeasible states if the signed range + * doesn't also span the constant. + */ + if (is_jmp32) { + can_fork = neq_regs[insn->dst_reg].u32_min_value < (u32)val && + neq_regs[insn->dst_reg].u32_max_value > (u32)val && + neq_regs[insn->dst_reg].s32_min_value < (s32)val && + neq_regs[insn->dst_reg].s32_max_value > (s32)val; + } else { + can_fork = neq_regs[insn->dst_reg].umin_value < val && + neq_regs[insn->dst_reg].umax_value > val && + neq_regs[insn->dst_reg].smin_value < (s64)val && + neq_regs[insn->dst_reg].smax_value > (s64)val; + } + } + + if (can_fork) { + /* Create a fake const register for regs_refine_cond_op */ + memset(&fake_const, 0, sizeof(fake_const)); + fake_const.type = SCALAR_VALUE; + __mark_reg_known(&fake_const, val); + + /* Push second fork for the not-equal branch. + * push_stack copies env->cur_state (this_branch). + * For JNE this_branch is the equal branch, so we + * must overwrite dst_reg with the not-equal copy. + */ + neq_branch2 = push_stack(env, neq_target, *insn_idx, false); + if (IS_ERR(neq_branch2)) + return PTR_ERR(neq_branch2); + neq2_regs = neq_branch2->frame[neq_branch2->curframe]->regs; + neq2_regs[insn->dst_reg] = neq_regs[insn->dst_reg]; + + /* Fork 1 (existing not-equal branch): dst > const */ + regs_refine_cond_op(&neq_regs[insn->dst_reg], + &fake_const, BPF_JGT, is_jmp32); + reg_bounds_sync(&neq_regs[insn->dst_reg]); + + /* Fork 2 (new state): dst < const */ + memset(&fake_const, 0, sizeof(fake_const)); + fake_const.type = SCALAR_VALUE; + __mark_reg_known(&fake_const, val); + regs_refine_cond_op(&neq2_regs[insn->dst_reg], + &fake_const, BPF_JLT, is_jmp32); + reg_bounds_sync(&neq2_regs[insn->dst_reg]); + + /* Propagate JGT/JLT bounds to linked registers */ + if (neq_regs[insn->dst_reg].id) { + sync_linked_regs(env, neq_state, + &neq_regs[insn->dst_reg], + &linked_regs); + sync_linked_regs(env, neq_branch2, + &neq2_regs[insn->dst_reg], + &linked_regs); + } + + err = reg_bounds_sanity_check(env, + &neq_regs[insn->dst_reg], "neq_gt"); + err = err ?: reg_bounds_sanity_check(env, + &neq2_regs[insn->dst_reg], "neq_lt"); + if (err) + return err; + } + } + /* if one pointer register is compared to another pointer * register check if PTR_MAYBE_NULL could be lifted. * E.g. register A - maybe null -- 2.47.3