| Age | Commit message (Collapse) | Author |
|---|
|
Add cnum32_union() and cnum64_union() to compute a smallest circular
range containing both inputs.
Do so by enumerating the following configurations in a rotated
frame (a.base at the origin):
0 UT_MAX
|---------------------------------------------------|
[= a ==============================] |
[= b tail =] [= b main ===================>
[= union ===========================================]
0 UT_MAX
|---------------------------------------------------|
[= a =====================] |
[= b tail ======] [= b main =====>
[= union tail ============] [= union main =>
0 UT_MAX
|---------------------------------------------------|
[= a =======] |
[= b tail =============] [= b main =====>
[= union tail =========] [= union main =>
0 UT_MAX
|---------------------------------------------------|
[= a =========================] |
| [= b ====================] |
[= union ==================================] |
0 UT_MAX
|---------------------------------------------------|
[= a =====================================] |
| [= b ========] |
[= union =================================] |
0 UT_MAX
|---------------------------------------------------|
[= a ============] |
| [= b =======] |
Two possible covering arcs:
[= ab ======================================] |
[= ba tail ======] [= ba main =========>
Pick the smaller one.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-13-bcba9bc53ac9@gmail.com
|
|
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 <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-4-vldsampaio@pm.me
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
|
|
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>
|
|
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>
|
|
ERROR: modpost: "cnum64_umin" [drivers/net/ethernet/netronome/nfp/nfp.ko] undefined!
ERROR: modpost: "cnum64_umax" [drivers/net/ethernet/netronome/nfp/nfp.ko] undefined!
Export symbols for these references.
Reported-by: Kaitao Cheng <pilgrimtao@gmail.com>
Fixes: bbc631085503 ("bpf: replace min/max fields with struct cnum{32,64}")
Signed-off-by: Alan Maguire <alan.maguire@oracle.com>
Acked-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/r/20260427112205.1346733-1-alan.maguire@oracle.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
|
|
states.c:range_within() must be updated to properly check if
cnum-based range in an old state is a superset of a range in the cur
state. Currently it makes the decision using min/max accessors:
reg_umin(old) <= reg_umin(cur) <= reg_umax(old)
This is wrong for cnums that cross both UT_MAX/0 and ST_MAX/ST_MIN
boundaries. Consider cnum32{base=0x7FFFFFF0, size=0x80000020},
which represents values [0x7FFFFFF0, ..., U32_MAX, 0, ..., 0x10].
Its projections are u32_min/max=0/U32_MAX, s32_min/max=S32_MIN/MAX.
A register with range [0x100, 0x200] (which lies entirely in the gap
of the wrapping range) would pass the min/max check despite having no
overlap with the actual cnum arc.
This commit replaces min/max comparison with cnum{32,64}_is_subset()
operation. The operation implementation is verified using cbmc model
checker in [1].
[1] https://github.com/eddyz87/cnum-verif/
Fixes: bbc631085503 ("bpf: replace min/max fields with struct cnum{32,64}")
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/r/20260425-cnum-range-within-v1-1-2fdca70cb09d@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
|
|
This commit adds basic definitions for cnum32/cnum64.
This is a unified numeric range representation for signed and unsigned
domains. Inspired by an old post from Shung-Hsi Yu [1] and paper [2].
Operations correctness is verified using cbmc model checker,
tests source code can be found in a separate repo [3].
The cnum64_cnum32_intersect() function is notable, because it handled
several cases verifier.c:deduce_bounds_64_from_32() does not.
Given:
- a is a 64-bit range
- b is a 32-bit range
- t is a refined 64-bit range, such that ∀ v ∈ a, (u32)v ∈ b: v ∈ t.
cnum64_cnum32_intersect() makes the following deductions:
(A): 'b' is a sub-range of the first or the last 32-bit
sub-range of 'a':
64-bit number axis --->
N*2^32 (N+1)*2^32 (N+2)*2^32 (N+3)*2^32
||------|---|=====|-------||----------|=====|-------||----------|=====|----|--||
| |< b >| |< b >| |< b >| |
| | | |
|<--+--------------------------- a ---------------------------+--->|
| |
|<-------------------------- t -------------------------->|
(B) 'b' does not intersect with the first of the last 32-bit
sub-range of 'a':
N*2^32 (N+1)*2^32 (N+2)*2^32 (N+3)*2^32
||--|=====|----|----------||--|=====|---------------||--|=====|------------|--||
|< b >| | |< b >| |< b >| |
| | | |
|<-------------+--------- a -------------------|----------->|
| |
|<-------- t ------------------>|
(C) 'b' crosses 0/U32_MAX boundary:
N*2^32 (N+1)*2^32 (N+2)*2^32 (N+3)*2^32
||===|---------|------|===||===|----------------|===||===|---------|------|===||
|b >| | |< b||b >| |< b||b >| | |< b|
| | | |
|<-----+----------------- a --------------+-------->|
| |
|<---------------- t ------------->|
Current implementation of deduce_bounds_64_from_32() only handles
case (A).
[1] https://lore.kernel.org/all/ZTZxoDJJbX9mrQ9w@u94a/
[2] https://jorgenavas.github.io/papers/ACM-TOPLAS-wrapped.pdf
[3] https://github.com/eddyz87/cnum-verif/tree/master
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/r/20260424-cnums-everywhere-rfc-v1-v3-1-ca434b39a486@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
|
