diff options
| author | Vinicius Sampaio <vldsampaio@pm.me> | 2026-07-30 10:21:18 +0000 |
|---|---|---|
| committer | Eduard Zingerman <eddyz87@gmail.com> | 2026-08-20 23:58:07 -0700 |
| commit | 4e3fb5bba680c1778e05a120c3793d22204f8fd4 (patch) | |
| tree | 12d22e9b9ed8855744fd2c050949f7d9890ec113 /scripts/Makefile.thinlto | |
| parent | d19862d923b9a785ec27bc51c334a8d457a0dd03 (diff) | |
| download | linux-next-4e3fb5bba680c1778e05a120c3793d22204f8fd4.tar.gz linux-next-4e3fb5bba680c1778e05a120c3793d22204f8fd4.zip | |
bpf: Simplify cnum contains() by removing redundant branches
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 <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-2-vldsampaio@pm.me
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Diffstat (limited to 'scripts/Makefile.thinlto')
0 files changed, 0 insertions, 0 deletions
