Bearing in mind that a non-empty cnum represents an inclusive circular range in the corresponding unsigned integer domain, membership could be tested by checking whether the distance from the range base to the queried value is within the range size. This makes the explicit wrapping and non-wrapping cases in contains() unnecessary, since: v - cnum.base <= cnum.size is equivalent for both ordinary ranges and ranges that cross the unsigned wrap boundary. We've also run some benchmarks to compare the performance of the new implementation, for example, for empty ranges, overflowing ranges non-overflowing ranges. We've run the tests with O2 optimization. Results: | Test | contains | contains_new | | -------------------- | ----------- | ------------ | | empty | 1.511 ns/op | 1.479 ns/op | | non-overflow inside | 1.156 ns/op | 1.270 ns/op | | non-overflow outside | 1.053 ns/op | 1.258 ns/op | | overflow high side | 1.469 ns/op | 1.257 ns/op | | overflow low side | 1.469 ns/op | 1.270 ns/op | | overflow outside | 1.478 ns/op | 1.256 ns/op | | singleton inside | 1.049 ns/op | 1.256 ns/op | | singleton outside | 1.051 ns/op | 1.254 ns/op | | full range | 1.053 ns/op | 1.256 ns/op | You can check the full implementation of these tests on this repository: https://github.com/OpenSourceVerif/open-verified-artifacts/tree/cnum-refactor-verif/cnum/benches Lean4 proofs showing that the new implementation preserves the soundness of the operation are available at: https://github.com/OpenSourceVerif/open-verified-artifacts/tree/cnum-refactor-verif/cnum/lean Co-developed-by: Yazhou Tang Signed-off-by: Yazhou Tang Co-developed-by: Shenghao Yuan Signed-off-by: Shenghao Yuan Signed-off-by: Vinicius Sampaio Acked-by: Shung-Hsi Yu --- kernel/bpf/cnum_defs.h | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/kernel/bpf/cnum_defs.h b/kernel/bpf/cnum_defs.h index a90e317e3578..ac1f62a0195d 100644 --- a/kernel/bpf/cnum_defs.h +++ b/kernel/bpf/cnum_defs.h @@ -210,12 +210,7 @@ bool FN(is_empty)(struct cnum_t cnum) bool FN(contains)(struct cnum_t cnum, ut v) { - if (FN(is_empty)(cnum)) - return false; - if (FN(urange_overflow)(cnum)) - return v >= cnum.base || v <= (ut)cnum.base + cnum.size; - else - return v >= cnum.base && v <= (ut)cnum.base + cnum.size; + return !FN(is_empty)(cnum) && v - cnum.base <= cnum.size; } bool FN(is_const)(struct cnum_t cnum) -- 2.54.0 In normalize(), there's no need to compare cnum.base with ST_MAX, because any cnum with size == UT_MAX represents the full unsigned domain independently of base, so normalize() can canonicalize all such values to base 0. Also, it's a no-op assigning 0 to cnum.base if the cnum is already unbounded, so we can remove the base != 0 check too. We've also run some benchmarks to compare the performance of the new implementation. We've run the tests with O2 optimization. Results: | Test | normalize | normalize_new | | ----------------------- | ----------- | ------------- | | normal small range | 1.255 ns/op | 1.217 ns/op | | full range normalized | 1.019 ns/op | 1.217 ns/op | | full range nonzero base | 1.031 ns/op | 1.221 ns/op | | empty | 1.023 ns/op | 1.217 ns/op | | signed max full range | 1.020 ns/op | 1.218 ns/op | | max base singleton | 1.218 ns/op | 1.219 ns/op | You can check the full implementation of these tests on this repository: https://github.com/OpenSourceVerif/open-verified-artifacts/tree/cnum-refactor-verif/cnum/benches Lean4 proofs showing that the new implementation preserves soundness of the operation are available at: https://github.com/OpenSourceVerif/open-verified-artifacts/tree/cnum-refactor-verif/cnum/lean Co-developed-by: Yazhou Tang Signed-off-by: Yazhou Tang Co-developed-by: Shenghao Yuan Signed-off-by: Shenghao Yuan Signed-off-by: Vinicius Sampaio Acked-by: Shung-Hsi Yu --- kernel/bpf/cnum_defs.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/bpf/cnum_defs.h b/kernel/bpf/cnum_defs.h index ac1f62a0195d..09535edbbafc 100644 --- a/kernel/bpf/cnum_defs.h +++ b/kernel/bpf/cnum_defs.h @@ -181,7 +181,7 @@ void FN(intersect_with_srange)(struct cnum_t *dst, st min, st max) static inline struct cnum_t FN(normalize)(struct cnum_t cnum) { - if (cnum.size == UT_MAX && cnum.base != 0 && cnum.base != (ut)ST_MAX) + if (cnum.size == UT_MAX) cnum.base = 0; return cnum; } -- 2.54.0 Simplify the smin() and smax() calculation by removing the integer min and max calculation on the non-overflowing branch. This is a valid simplification because when the arc does not cross the signed ST_MAX/ST_MIN boundary, the signed order of the endpoints is preserved, so base is the signed minimum and base + size is the signed maximum. Therefore, the min()/max() calls are redundant. We've also run benchmarks to compare the performance of this change. With O2 optimization we have: smin() results: | Test | smin | smin_new | | ------------------------ | ----------- | ----------- | | empty | 1.866 ns/op | 1.477 ns/op | | positive range | 1.870 ns/op | 1.248 ns/op | | negative range | 1.657 ns/op | 1.246 ns/op | | cross zero | 1.870 ns/op | 1.660 ns/op | | signed overflow boundary | 1.463 ns/op | 1.049 ns/op | | signed overflow range | 1.519 ns/op | 1.050 ns/op | | unsigned overflow range | 1.883 ns/op | 1.669 ns/op | | full range | 1.555 ns/op | 1.049 ns/op | smax() results: | Test | smax | smax_new | | ------------------------ | ----------- | ----------- | | empty | 1.462 ns/op | 1.456 ns/op | | positive range | 1.250 ns/op | 1.249 ns/op | | negative range | 1.259 ns/op | 1.297 ns/op | | cross zero | 1.471 ns/op | 1.475 ns/op | | signed overflow boundary | 1.056 ns/op | 1.260 ns/op | | signed overflow range | 1.049 ns/op | 1.259 ns/op | | unsigned overflow range | 1.470 ns/op | 1.477 ns/op | | full range | 1.072 ns/op | 1.263 ns/op | You can check the full implementation of these tests on this repository: https://github.com/OpenSourceVerif/open-verified-artifacts/tree/cnum-refactor-verif/cnum/benches Lean4 proofs showing that the new implementation preserves soundness of these operations are available at: https://github.com/OpenSourceVerif/open-verified-artifacts/tree/cnum-refactor-verif/cnum/lean Co-developed-by: Yazhou Tang Signed-off-by: Yazhou Tang Co-developed-by: Shenghao Yuan Signed-off-by: Shenghao Yuan Signed-off-by: Vinicius Sampaio Acked-by: Shung-Hsi Yu --- kernel/bpf/cnum_defs.h | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/kernel/bpf/cnum_defs.h b/kernel/bpf/cnum_defs.h index 09535edbbafc..30685e43de04 100644 --- a/kernel/bpf/cnum_defs.h +++ b/kernel/bpf/cnum_defs.h @@ -33,7 +33,12 @@ struct cnum_t FN(from_srange)(st min, st max) return (struct cnum_t){ .base = base, .size = size }; } -/* True if this cnum represents two unsigned ranges. */ +/* + * True if this cnum represents two unsigned ranges. + * + * The caller should ensure !is_empty(cnum) holds when calling + * this function. + */ static inline bool FN(urange_overflow)(struct cnum_t cnum) { /* Same as cnum.base + cnum.size > UT_MAX but avoids overflow */ @@ -44,6 +49,9 @@ static inline bool FN(urange_overflow)(struct cnum_t cnum) * cnum{T}_umin / cnum{T}_umax query an unsigned range represented by this cnum. * If cnum represents a range crossing the UT_MAX/0 boundary, the unbound range * [0..UT_MAX] is returned. + * + * The caller should ensure !is_empty(cnum) holds when calling + * cnum{T}_umin / cnum{T}_umax. */ ut FN(umin)(struct cnum_t cnum) { @@ -57,7 +65,12 @@ ut FN(umax)(struct cnum_t cnum) } EXPORT_SYMBOL_GPL(FN(umax)); -/* True if this cnum represents two signed ranges. */ +/* + * True if this cnum represents two signed ranges. + * + * The caller should ensure !is_empty(cnum) holds when calling + * this function. + */ static inline bool FN(srange_overflow)(struct cnum_t cnum) { return FN(contains)(cnum, (ut)ST_MAX) && FN(contains)(cnum, (ut)ST_MIN); @@ -67,19 +80,18 @@ static inline bool FN(srange_overflow)(struct cnum_t cnum) * cnum{T}_smin / cnum{T}_smax query a signed range represented by this cnum. * If cnum represents a range crossing the ST_MAX/ST_MIN boundary, the unbound range * [ST_MIN..ST_MAX] is returned. + * + * The caller should ensure !is_empty(cnum) holds when calling + * cnum{T}_smin / cnum{T}_smax. */ st FN(smin)(struct cnum_t cnum) { - return FN(srange_overflow)(cnum) - ? ST_MIN - : min((st)cnum.base, (st)(cnum.base + cnum.size)); + return FN(srange_overflow)(cnum) ? ST_MIN : (st)cnum.base; } st FN(smax)(struct cnum_t cnum) { - return FN(srange_overflow)(cnum) - ? ST_MAX - : max((st)cnum.base, (st)(cnum.base + cnum.size)); + return FN(srange_overflow)(cnum) ? ST_MAX : (st)(cnum.base + cnum.size); } /* -- 2.54.0