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

On Tue, 2026-04-21 at 17:18 +0000, [email protected] 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 <[email protected]>
> 
> 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;
> > +}
> [ ... ]