From: Alexei Starovoitov Date: Sat, 25 Apr 2026 01:14:18 +0000 (-0700) Subject: Merge branch 'bpf-replace-min-max-fields-with-struct-cnum-32-64' X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=6c60b2dd5a7889a583389e95e79689191206f86f;p=thirdparty%2Fkernel%2Flinux.git Merge branch 'bpf-replace-min-max-fields-with-struct-cnum-32-64' Eduard Zingerman says: ==================== bpf: replace min/max fields with struct cnum{32,64} This RFC replaces s64, u64, s32, u32 scalar range domains tracked by verifier by a pair of circular numbers (cnums): one for 64-bit domain and another for 32-bit domain. Each cnum represents a range as a single arc on the circular number line, from which signed and unsigned bounds are derived on demand. See also wrapped intervals representation as in [1]. The use of such representation simplifies arithmetic and conditions handling in verifier.c and allows to express 32 <-> 64 bit deductions in a more mathematically rigorous way. [1] https://jorgenavas.github.io/papers/ACM-TOPLAS-wrapped.pdf Changelog ========= v2 -> v1: - Fixes in source code comments highlighted by bot+bpf-ci. RFCv1 -> v2: - Dropped RFC tag. - Dropped cnum{32,64}_mul(), too much complexity and no veristat or selftests gains. - cnum32_from_cnum64() normalizes to CNUM32_EMPTY when input cnum64.size >= U32_MAX, previously only checked for > U32_MAX (bot+bpf-ci). - cnum32_from_cnum64() and cnum64_cnum32_intersect() now check for empty inputs (sashiko). - In regs_refine_cond_op() case BPF_JSLT use cnum{32,64}_from_srange constructors instead of unsigned variants (sashiko). - cnum{32,64}_intersect_with{,_urange,_srange}() helpers added (Alexei) [RFCv1] https://lore.kernel.org/bpf/0c47b0b7ea476647746806c46fded4353be885f7.camel@gmail.com/T/ [v2] https://lore.kernel.org/bpf/c4fb60bafd526ae2d92b86e2250255aef0ba5ee1.camel@gmail.com/T/ Patch set layout ================ Patch #1 introduces the cnum (circular number) data type and basic operations: intersection, addition, multiplication, negation, 32-to-64 and 64-to-32 projections. CBMC based proofs for these operations are available at [2]. (The proofs lag behind the current patch set and need an update if this RFC moves further. Although, I don't expect any significant changes). [2] https://github.com/eddyz87/cnum-verif Patch #2 mechanically converts all direct accesses to bpf_reg_state's min/max fields to use accessor functions, preparing for the field replacement. Patch #3 replaces the eight independent min/max fields in bpf_reg_state with two cnum fields. The signed and unsigned bounds are derived on demand from the cnum via the accessor functions. This eliminates the separate signed<->unsigned cross-deduction logic, simplifies reg_bounds_sync(), regs_refine_cond_op() and some arithmetic operations. Patch #4 adds selftest cases for improved 32->64 range refinements enabled by cnum64_cnum32_intersect(). Precision trade-offs ==================== A cnum represents a contiguous arc on the circular number line. Current master tracks four independent ranges (s64, u64, s32, u32) whose intersection could implicitly represent value sets that are two disjoint arcs on the circle - something a single cnum cannot. Cnums lose precision when a cross-domain conditional comparison (e.g., unsigned comparison on a register with a signed-derived range) produces an intersection that would be two disjoint arcs. The cnum must over-approximate by returning one of the input arcs. E.g. a pair of ranges u64:[1,U64_MAX] s:[-1,1] represents a set of two values: {-1,1}, this can only be approximated as a set of three values by cnum: {-1,0,1}. Cnums gain precision in arithmetic: when addition, subtraction or multiplication causes register value to cross both signed and unsigned min/max boundaries. Current master resets the register as unbound in such cases, while cnums preserve the exact wrapping arc. In practice precision loss turned out to matter only for a set of specifically crafted selftests from reg_bounds.c (see patch #3 for more details). On the other hand, precision gains are observable for a set real-life programs. Verification performance measurements ===================================== Tested on 6683 programs across four corpora: Cilium (134 programs), selftests (4635), sched_ext (376), and Meta internal BPF corpus (1540). Program verification verdicts are identical across all four program sets - no program changes between success and failure. Instruction count comparison (cnum vs signed/unsigned pair): - 83 programs improve, 44 regress, 6596 unchanged - Total saved: ~290K insns, total added: 10K insns - Largest improvements: -26% insns in a internal network firewall program; -47% insns in rusty/wd40 sched_ext schedulers. - Largest regression: +24% insns in one Cilium program (5062 insns added). Raw performance data is at the bottom of the email. Raw verification performance metrics ==================================== Filtered out by -f insns_pct>5 -f !insns<10000 ========= selftests: master vs cnums-everywhere-v2 ========= File Program Insns (A) Insns (B) Insns (DIFF) ---- ------- --------- --------- ------------ Total progs: 4665 total_insns diff min: -15.71% total_insns diff max: 45.45% -20 .. -10 %: 3 -5 .. 0 %: 6 0 .. 5 %: 4654 45 .. 50 %: 2 ========= scx: master vs cnums-everywhere-v2 ========= File Program Insns (A) Insns (B) Insns (DIFF) --------------- -------------- --------- --------- ---------------- scx_rusty.bpf.o rusty_enqueue 39842 22053 -17789 (-44.65%) scx_rusty.bpf.o rusty_stopping 37738 19949 -17789 (-47.14%) scx_wd40.bpf.o wd40_stopping 37729 19880 -17849 (-47.31%) Total progs: 376 total_insns diff min: -47.31% total_insns diff max: 19.61% -50 .. -40 %: 3 -5 .. 0 %: 5 0 .. 5 %: 366 5 .. 15 %: 1 15 .. 20 %: 1 ========= meta: master vs cnums-everywhere-v2 ========= File Program Insns (A) Insns (B) Insns (DIFF) --------------------------------- ---------- --------- --------- ---------------- ...egress 222327 164648 -57679 (-25.94%) ..._tc_eg 222839 164772 -58067 (-26.06%) ...egress 222327 164648 -57679 (-25.94%) ..._tc_eg 222839 164772 -58067 (-26.06%) Total progs: 1540 total_insns diff min: -26.06% total_insns diff max: 6.69% -30 .. -20 %: 4 -15 .. -5 %: 6 -5 .. 0 %: 36 0 .. 5 %: 1493 5 .. 10 %: 1 ========= cilium: master vs cnums-everywhere-v2 ========= File Program Insns (A) Insns (B) Insns (DIFF) ---------- ------------------------------- --------- --------- --------------- bpf_host.o tail_handle_ipv4_cont_from_host 20962 26024 +5062 (+24.15%) bpf_host.o tail_handle_ipv6_cont_from_host 17036 18672 +1636 (+9.60%) Total progs: 134 total_insns diff min: -3.32% total_insns diff max: 24.15% -5 .. 0 %: 12 0 .. 5 %: 120 5 .. 15 %: 1 20 .. 25 %: 1 --- ==================== Link: https://patch.msgid.link/20260424-cnums-everywhere-rfc-v1-v3-0-ca434b39a486@gmail.com Signed-off-by: Alexei Starovoitov --- 6c60b2dd5a7889a583389e95e79689191206f86f