This patch introduces a optimization for the normalize() function. 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, for example, for empty ranges, overflowing ranges non-overflowing ranges. We've run the tests with O2 optimization. Results: | Test | normalize | normalize_new | | ----------------------- | ----------- | ------------- | | normal small range | 1.254 ns/op | 1.049 ns/op | | full range normalized | 1.055 ns/op | 1.046 ns/op | | full range nonzero base | 1.053 ns/op | 1.055 ns/op | | empty | 1.054 ns/op | 1.059 ns/op | | signed max full range | 1.051 ns/op | 1.049 ns/op | | max base singleton | 1.253 ns/op | 1.045 ns/op | You can check the full implementation of theses 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 | 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