Re: [PATCH RFC bpf-next 1/4] bpf: representation and basic operations on circular numbers

Re: [PATCH RFC bpf-next 1/4] bpf: representation and basic operations on circular numbers

[Eduard Zingerman]

On Tue, 2026-04-21 at 17:18 +0000, sashiko-bot@kernel.org wrote:
> Sashiko AI review found 4 potential issue(s):
> - [Critical] `FN(cut)` emits wrapped chunks causing `FN(mk_mul_u)` to compute unsound narrow bounds.
> - [Critical] `cnum32_from_cnum64()` can return a struct mathematically equivalent to the `CNUM32_EMPTY` sentinel.
> - [High] Unconditional use of `__int128` breaks compilation on 32-bit architectures.
> - [Medium] Missing emptiness checks in `cnum64_cnum32_intersect` and `cnum32_from_cnum64` resurrect unreachable states.
> --
> 
> commit 5ab536543671bb2cd6865196d88e96f87d1e7888
> Author: Eduard Zingerman <eddyz87@gmail.com>
> 
> bpf: representation and basic operations on circular numbers
> 
> This commit introduces cnum32 and cnum64 representations for unified
> signed and unsigned numeric ranges in the BPF verifier. It includes
> functions for intersection, multiplication, and range conversion to
> refine bounds deductions.
> 
> Link: https://lore.kernel.org/all/ZTZxoDJJbX9mrQ9w@u94a/
> Link: https://jorgenavas.github.io/papers/ACM-TOPLAS-wrapped.pdf
> Link: https://github.com/eddyz87/cnum-verif/tree/master
> 
> > diff --git a/kernel/bpf/cnum.c b/kernel/bpf/cnum.c
> > new file mode 100644
> > index 0000000000000..38a805a6fc2a9
> > --- /dev/null
> > +++ b/kernel/bpf/cnum.c
> [ ... ]
> > +struct cnum32 cnum32_from_cnum64(struct cnum64 cnum)
> > +{
> 
> Are we missing a check for empty inputs here? If an empty 64-bit range is
> passed, does this code convert it directly into an unbounded 32-bit range?
> 
> > +	if (cnum.size > U32_MAX)
> > +		return (struct cnum32){ .base = 0, .size = U32_MAX };
> > +	else
> > +		return (struct cnum32){ .base = (u32)cnum.base, .size = cnum.size };
> > +}
> 
> Could this else branch return a value mathematically identical to the
> CNUM32_EMPTY sentinel?

This is a valid point, but it won't be hit in practice:
the function is called in reg_bounds_sync() and empty inputs are
short-circuited there.

> 
> If a valid 64-bit range has a size of U32_MAX and a base ending in
> 0xFFFFFFFF, this would return { .base = 0xFFFFFFFF, .size = 0xFFFFFFFF }.
> Would the verifier then incorrectly assume this code path is dead and
> prune it?
> 
> [ ... ]
> > +struct cnum64 cnum64_cnum32_intersect(struct cnum64 a, struct cnum32 b)
> > +{
> 
> Does this function need to verify if the input ranges are empty before
> operating on them? If the variable a is empty, could the arithmetic below
> return a non-empty, garbage range, effectively resurrecting dead code paths?

Here as well, a valid point, but does not happen with current verifier
structure.

> > +	/*
> > +	 * To simplify reasoning, rotate the circles so that [virtual] a1 starts
> > +	 * at u32 boundary, b1 represents b in this new frame of reference.
> > +	 */
> > +	struct cnum32 b1 = { b.base - (u32)a.base, b.size };
> [ ... ]
> > diff --git a/kernel/bpf/cnum_defs.h b/kernel/bpf/cnum_defs.h
> > new file mode 100644
> > index 0000000000000..28dcb79ba6950
> > --- /dev/null
> > +++ b/kernel/bpf/cnum_defs.h
> [ ... ]
> > +#if T == 32
> > +#define ut2 u64
> > +#define st2 s64
> > +#define utt u32
> > +#define stt s32
> > +#define EMPTY CNUM32_EMPTY
> > +#elif T == 64
> > +#define ut2 unsigned __int128
> > +#define st2 signed __int128
> 
> Will the unconditional use of unsigned __int128 and signed __int128 break
> compilation on 32-bit architectures? Since the BPF subsystem and verifier
> are built on 32-bit kernels when CONFIG_BPF_SYSCALL is enabled, this
> might cause widespread build failures.
> 
> > +#define utt u64
> > +#define stt s64
> > +#define EMPTY CNUM64_EMPTY
> > +#else
> > +#error "Unsupported T value, cannot define ut2/st2"
> > +#endif
> [ ... ]
> > +static int FN(cut)(struct cnum_t a, struct cnum_t chunks[3])
> > +{
> > +	int ncuts = 0;
> > +
> > +	if (FN(srange_overflow)(a)) {
> > +		chunks[ncuts++] = FN(from_urange)(a.base, ST_MAX);
> > +		a = FN(from_urange)(ST_MIN, a.base + a.size);
> > +	}
> 
> Can this splitting logic emit wrapped chunks that cause bound deductions
> to underflow?
> 
> When an arc crosses both boundaries, this splits it first at ST_MAX. The
> resulting first chunk crosses the unsigned boundary 0.
> 
> When passed to FN(mul_chunk) with a multiplier, it falls into the fallback
> branch utilizing FN(mk_mul_u):
> 
> static struct cnum_t FN(mk_mul_u)(utt a, utt b, utt c, utt d)
> {
>         ut2 size = (ut2)c * d - (ut2)a * b;
> 
> Because the chunk wraps, its unsigned start is mathematically greater than
> its end. Does this cause the subtraction to severely underflow in unsigned
> arithmetic, producing an artificially tight size that misses valid
> runtime products?

This might be an issue. However, it does not lead to unsound results,
at-least in u8 domain [1,2].

[1] https://github.com/eddyz87/cnum-verif/blob/arithm-ops/cbmc_helpers8.c
[2] https://github.com/eddyz87/cnum-verif/blob/arithm-ops/main.c

I'll this and post updated veristat results.

> 
> > +	if (FN(urange_overflow)(a)) {
> > +		chunks[ncuts++] = FN(from_urange)(a.base, UT_MAX);
> > +		a = FN(from_urange)(0, a.base + a.size);
> > +	}
> > +	chunks[ncuts++] = a;
> > +	return ncuts;
> > +}
> [ ... ]

Re: [PATCH RFC bpf-next 1/4] bpf: representation and basic operations on circular numbers

[Eduard Zingerman]

On Tue, 2026-04-21 at 17:18 +0000, sashiko-bot@kernel.org wrote:

[...]

> > diff --git a/kernel/bpf/cnum_defs.h b/kernel/bpf/cnum_defs.h
> > new file mode 100644
> > index 0000000000000..28dcb79ba6950
> > --- /dev/null
> > +++ b/kernel/bpf/cnum_defs.h
> [ ... ]
> > +#if T == 32
> > +#define ut2 u64
> > +#define st2 s64
> > +#define utt u32
> > +#define stt s32
> > +#define EMPTY CNUM32_EMPTY
> > +#elif T == 64
> > +#define ut2 unsigned __int128
> > +#define st2 signed __int128
>
> Will the unconditional use of unsigned __int128 and signed __int128 break
> compilation on 32-bit architectures? Since the BPF subsystem and verifier
> are built on 32-bit kernels when CONFIG_BPF_SYSCALL is enabled, this
> might cause widespread build failures.

Forgoing __int128 would require something along the following lines:

  /* *result = c*d - a*b, if fits in u32; all operands unsigned */
  static bool check_mul_u32_u32_sub(u32 a, u32 b, u32 c, u32 d, u32 *result)
  {
          u64 size = (u64)c * d - (u64)a * b;

          if (size > U32_MAX)
                  return false;
          *result = size;
          return true;
  }

  /* *result = c*d - a*b, if fits in u32; all operands signed */
  static bool check_mul_s32_s32_sub(s32 a, s32 b, s32 c, s32 d, u32 *result)
  {
          s64 size = (s64)c * d - (s64)a * b;

          if (size > U32_MAX)
                  return false;
          *result = size;
          return true;
  }

  /* Return (s128)a * b >> shift */
  static s64 mul_s64_s64_shr(s64 a, s64 b, unsigned int shift)
  {
          return mul_s64_u64_shr(a, abs(b), shift) * (b < 0 ? -1 : 1);
  }

  /* *result = c*d - a*b, if fits in u64; all operands unsigned */
  static bool check_mul_u64_u64_sub(u64 a, u64 b, u64 c, u64 d, u64 *result)
  {
          u64 cd_hi = mul_u64_u64_shr(c, d, 64);
          u64 cd_lo = c * d;
          u64 ab_hi = mul_u64_u64_shr(a, b, 64);
          u64 ab_lo = a * b;
          u64 borrow = cd_lo < ab_lo;
          u64 hi = cd_hi - ab_hi - borrow;

          if (hi != 0)
                  return false;
          *result = cd_lo - ab_lo;
          return true;
  }

  /* *result = c*d - a*b, if fits in u64; all operands signed */
  static bool check_mul_s64_s64_sub(s64 a, s64 b, s64 c, s64 d, u64 *result)
  {
          s64 cd_hi = mul_s64_s64_shr(c, d, 64);
          u64 cd_lo = (u64)c * (u64)d;
          s64 ab_hi = mul_s64_s64_shr(a, b, 64);
          u64 ab_lo = (u64)a * (u64)b;
          u64 borrow = cd_lo < ab_lo;
          s64 hi = cd_hi - ab_hi - borrow;

          if (hi != 0)
                  return false;
          *result = cd_lo - ab_lo;
          return true;
  }

For use in mk_mul_{u,s}. This is on top of the following functions:
- cnum{32,64}_gap
- cnum{32,64}_extend
- cnum{32,64}_bigger
- cnum{32,64}_union
- cnum{32,64}_cut
- cnum{32,64}_mk_mul_{u,s}
- cnum{32,64}_mul_chunk
- cnum{32,64}_mul

Overall +230 lines of non-trivial code.
I did some work to consolidate existing checks in [1], and was unable
to get union, cut and mul_chunk verified for 32-bit and 64-bit domains,
cbmc does not converge to an answer. I'm a bit hesitant regarding
brute-force 8-bit domain verification: there were a few non-trivial
bugs in check_mul because of C implicit cast rules and 8-bit testing
did not reveal them. Looks like a theorem prover is needed indeed.

[1] https://github.com/eddyz87/cnum-verif/tree/consolidated-checks

I tried reinstating the old mul implementation:

  static void scalar_min_max_mul(struct bpf_reg_state *dst_reg,
                                  struct bpf_reg_state *src_reg)
  {
          s64 smin = reg_smin(dst_reg);
          s64 smax = reg_smax(dst_reg);
          u64 umin = reg_umin(dst_reg);
          u64 umax = reg_umax(dst_reg);
          s64 tmp_prod[4];
  
          if (check_mul_overflow(umax, reg_umax(src_reg), &umax) ||
              check_mul_overflow(umin, reg_umin(src_reg), &umin)) {
                  /* Overflow possible, we know nothing */
                  umin = 0;
                  umax = U64_MAX;
          }
          if (check_mul_overflow(smin, reg_smin(src_reg), &tmp_prod[0]) ||
              check_mul_overflow(smin, reg_smax(src_reg), &tmp_prod[1]) ||
              check_mul_overflow(smax, reg_smin(src_reg), &tmp_prod[2]) ||
              check_mul_overflow(smax, reg_smax(src_reg), &tmp_prod[3])) {
                  /* Overflow possible, we know nothing */
                  smin = S64_MIN;
                  smax = S64_MAX;
          } else {
                  smin = min_array(tmp_prod, 4);
                  smax = max_array(tmp_prod, 4);
          }
  
          dst_reg->r64 = cnum64_intersect(cnum64_from_urange(umin, umax),
                                          cnum64_from_srange(smin, smax));
  }

As it still handles cases like [+-a, +-b] x [+-b, +-d] reasonably well
for bounded a, b, c, d. As a result:
- no tests failed
- no difference in veristat results.

Therefore, for v2 I'll drop cnum{32,64}_mul completely and defer to
the old code (or move it inside cnum_defs.h to avoid code duplication).


[...]