| Age | Commit message (Collapse) | Author |
|---|
|
Add cnum64_intersect_linear(), which intersects a cnum64 interval with the
set of integers congruent to 'base' modulo 'step', i.e. the points
base + step * k. It tightens the interval by rounding its signed minimum up
and its signed maximum down to the nearest such point, and returns an empty
cnum when no point falls within the interval.
The arithmetic is done on the signed bounds [smin, smax]. The line is defined
over the integers, while a cnum64 is an arc on the u64 circle, so a u64-modular
computation would misplace the line for negative values whenever 'step' does
not divide 2^64. Working from the signed bounds keeps the residues consistent,
e.g. it can reason about a range like [-9, 3] with step 3.
Also add imod() to bpf_verifier.h: a mathematical modulo returning an
always-non-negative residue (unlike C's '%', which follows the sign of the
dividend). It is used by cnum64_intersect_linear() and by the base/step
tracking added in subsequent patches.
This is a building block for tracking scalar registers whose value is known
to lie on a line base + step * k.
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-14-bcba9bc53ac9@gmail.com
|
|
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
|
|
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>
|
