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

[sashiko-bot@kernel.org]

Sashiko AI review found 1 potential issue(s):
- [Low] The `FN(normalize)` function incorrectly skips normalizing full circular ranges if their base evaluates to `ST_MAX`.
--

commit addd9a35120cb1e8b327011ef0f97fa736918a87
Author: Eduard Zingerman <eddyz87@gmail.com>

bpf: representation and basic operations on circular numbers

This commit adds basic definitions for cnum32/cnum64, providing a unified
numeric range representation for signed and unsigned domains. The operations
correctness is verified using a cbmc model checker.

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_defs.h b/kernel/bpf/cnum_defs.h
> new file mode 100644
> index 00000000000000..3ebd8f723dbb53
> --- /dev/null
> +++ b/kernel/bpf/cnum_defs.h

[ ... ]

> +static inline struct cnum_t FN(normalize)(struct cnum_t cnum)
> +{
> +	if (cnum.size == UT_MAX && cnum.base != 0 && cnum.base != (ut)ST_MAX)

Should this condition be checking ST_MAX? It appears that this skips
normalizing full circular ranges if their base evaluates to ST_MAX. This
can leave the range denormalized as { ST_MAX, UT_MAX } instead of
canonicalizing it to { 0, UT_MAX } (for example, when adding a constant
ST_MAX to an UNBOUNDED range).

Leaving the range denormalized breaks canonical representation guarantees
and causes fast-path equality checks to fail, leading to unnecessary
fallbacks to slower subset checks.

If the intent was to check UT_MAX to protect the EMPTY representation
({ UT_MAX, UT_MAX }), operations like add(UNBOUNDED, -1) legitimately
produce { UT_MAX, UT_MAX } representing a full circle, which must be
normalized to UNBOUNDED.

Would it make sense to remove the exception entirely so that all full
ranges are normalized safely?

> +		cnum.base = 0;
> +	return cnum;
> +}

-- 
Sashiko AI review · https://sashiko.dev/#/patchset/20260424-cnums-everywhere-rfc-v1-v3-0-ca434b39a486@gmail.com?part=1