diff options
| author | Vinicius Sampaio <vldsampaio@pm.me> | 2026-07-30 10:21:24 +0000 |
|---|---|---|
| committer | Eduard Zingerman <eddyz87@gmail.com> | 2026-08-20 23:58:07 -0700 |
| commit | b601a4ecbe672371776785bd7ac142af0ac395ac (patch) | |
| tree | 15e056dfdb4f0d3b2dd27704ce73e505ef7e64fc /scripts/Makefile.thinlto | |
| parent | 4e3fb5bba680c1778e05a120c3793d22204f8fd4 (diff) | |
| download | linux-next-b601a4ecbe672371776785bd7ac142af0ac395ac.tar.gz linux-next-b601a4ecbe672371776785bd7ac142af0ac395ac.zip | |
bpf: Simplify cnum normalize() by dropping unnecessary comparisons
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 <tangyazhou518@outlook.com>
Co-developed-by: Shenghao Yuan <shenghaoyuan0928@163.com>
Signed-off-by: Yazhou Tang <tangyazhou518@outlook.com>
Signed-off-by: Shenghao Yuan <shenghaoyuan0928@163.com>
Signed-off-by: Vinicius Sampaio <vldsampaio@pm.me>
Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Link: https://patch.msgid.link/20260730102129.15209-3-vldsampaio@pm.me
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Diffstat (limited to 'scripts/Makefile.thinlto')
0 files changed, 0 insertions, 0 deletions
