| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2026-10-09 | bpf: Add cnum64_intersect_linear() | Eduard Zingerman | |
| 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 | |||
| 2026-04-24 | bpf: representation and basic operations on circular numbers | Eduard Zingerman | |
| 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> | |||
 |
index : lwn.git | |
| Linux kernel documentation tree maintained by Jonathan Corbet |
| summaryrefslogtreecommitdiff |