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