[RFC PATCH bpf-next 0/1] bpf: Remove redundant __reg_deduce_bounds() call in reg_bounds_sync()

[Ömer Mete Kaya]

reg_bounds_sync() calls __reg_deduce_bounds() twice back-to-back. This
series removes the second call, which is a no-op with the current
cnum-based bounds representation.

Background & Motivation:

The double call predates the cnum representation. With the old tnum +
min/max logic, deduction between 32-bit and 64-bit views was not
idempotent: narrowing one view could allow further tightening of the
other, so two passes were needed to reach a fixpoint. With cnum, both
views are represented using the same circular-number model, so the first
pass already reaches the fixpoint.

I am sending this as RFC to confirm whether the second call was intentionally
kept as a defensive measure, or if it is simply a leftover. If there is a reason
to keep it, I would appreciate the context.

Correctness:

The idempotence of __reg_deduce_bounds() (call it D) was checked from
several approaches:

1. Algebraic argument:
   cnum64_cnum32_intersect() guarantees that for every value v in the
   result r64, (u32)v is in r32. This means r32 is already a subset of
   cnum32_from_cnum64(r64), so the first step of a second D application
   is intersecting a set with a superset, a no-op. With r32 unchanged,
   the second step is also a no-op by the idempotence of
   cnum64_cnum32_intersect() with a fixed second argument.

2. Z3 verification at full 32/64-bit width (bit-blast tactic):

   The Z3 encoding was first validated against the real kernel cnum
   object code (cnum_kern.o) on 20,000 inputs with zero mismatches.
   Four lemmas were verified at full 32/64-bit width:

     L1: cnum32_intersect(cnum32_intersect(a,b), b) == cnum32_intersect(a,b)
         UNSAT in 17s
     L2: after one D, cnum32_intersect(r32, from64(r64)) == r32
         UNSAT in 536s
     L3: cnum64_cnum32_intersect(cnum64_cnum32_intersect(a,b), b)
             == cnum64_cnum32_intersect(a,b)
         UNSAT in 26s
     L4: D(D(x)) == D(x)  [direct query, bit-blast]
         UNSAT in 8932s

     so:
        L1: cnum32_intersect() is idempotent with a fixed second operand.
        L2: after one D, the 32-bit intersection does not change r32.
        L3: cnum64_cnum32_intersect() is idempotent with a fixed r32.
        L4: D itself is idempotent.

   L2 and L3 together imply L4 algebraically; L4 was also verified
   directly as a cross-check. No counterexample exists in the full
   32/64-bit input space.

3. Exhaustive test at reduced bit widths:
   Widths from 2/4 up to 5/10 bits (preserving the algebraic structure
   of the full-width code) were tested exhaustively. Over 1 billion
   inputs, zero mismatches.

4. Random test at full 32/64-bit width:
   1.5 billion boundary-biased random inputs tested against the real
   kernel cnum object code. Zero divergences.

Performance:

reg_bounds_sync() is called from 14 sites in verifier.c, covering ALU
operations, comparisons, and helper/kfunc returns.
Removing the second __reg_deduce_bounds() call saves approximately
16-21 cycles per reg_bounds_sync() call (measured with
boundary-biased precomputed inputs on x86-64).

On a synthetic ALU-heavy BPF program (754 insns, 150 ALU chains),
verification time decreased by ~16%:

  before (2x __reg_deduce_bounds): 1464 us average over 2000 runs
  after  (1x __reg_deduce_bounds): 1221 us average over 2000 runs

Measured in a KASAN-free KVM guest on bpf-next at 4f3a5eae8, using
BPF_PROG_LOAD syscall timing with log_level=0.

Ömer Mete Kaya (1):
  bpf: Remove redundant second __reg_deduce_bounds() call in
    reg_bounds_sync()

 kernel/bpf/verifier.c | 1 -
 1 file changed, 1 deletion(-)

--
2.55.0