[RFC bpf-next v0 0/7] Unifying signed and unsigned min/max tracking

[RFC bpf-next v0 0/7] Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

This patchset is a proof of concept for previously discussed concept[1]
of unifying smin/smax with umin/uax for both the 32-bit and 64-bit
range[2] within bpf_reg_state. This will allow the verifier to track
both signed and unsiged ranges using just two u32 (for 32-bit range) or
u64 (for 64-bit range), instead four as we currently do.

The size reduction we gain from this probably isn't very significant.
The main benefit is in lowering of code _complexity_. The verifier
currently employs 5 value tracking mechanisms, two for 64-bit range, two
for 32-bit range, and one tnum that tracks individual bits. Exchanging
knowledge between all the bound tracking mechanisms requires a
(theoretical) 20-way synchronization[3]; with signed and unsigned
unification the verifier will only need 3 value tracking mechanism,
cutting this down to a 6-way synchronization.

The unification is possible from a theoretical standpoint[4] and there
exists implementation[5]. The challenge lies in implementing it inside
the verifier and making sure it fits well with all the logic we have in
place.

To lower the difficulty, the unified min/max tracking is implemented in
isolation, and have it correctness checked using model checking. The
model checking code can be found in this patchset as well, but is not
meant to be merged since a better method already exists[6].

So far I've managed to implement add/sub/mul operations for unified
min/max tracking, the next steps are:
- implement operation that can be used gain knowledge from conditional
  jump, e.g wrange32_intersect, wrange32_diff
- implement wrange32_from_min_max and wrange32_to_min_max so we can
  check whether this PoC works using current selftests
- implement operations for wrange64, the 64-bit counterpart of wrange32
- come up with how to exchange knowledge between wrange64 and wrange32
  (this is likely the most difficult part)
- think about how to integrate this work in a manageable manner

Feedbacks for either the code, the naming, and/or the commit messages
are all welcome.


1: https://lore.kernel.org/bpf/ZTZxoDJJbX9mrQ9w@u94a/
2: To make model checking faster I'm only working with the 32-bit ranges
   for now
3: Synchronization can goes both ways, e.g. exchanging knowledge in
   umin/umax from/to tnum count as 2-way. But
4: https://dl.acm.org/doi/10.1145/2651360
5: https://github.com/caballa/wrapped-intervals/blob/master/lib/RangeAnalysis/WrappedRange.cpp
6: https://lore.kernel.org/r/1DA1AC52-6E2D-4CDA-8216-D1DD4648AD55@cs.rutgers.edu

Shung-Hsi Yu (7):
  Add inital wrange32 definition along with checks for umin/umax
  Lift the contrain requiring start <= end
  Support tracking signed min/max
  Implement wrange32_add()
  Implement wrange32_sub()
  Implement wrange32_mul()
  (WIP) Add helper functions that transform wrange32 to and from
    smin/smax/umin/umax

 include/linux/wrange.h                        |  61 ++++
 kernel/bpf/Makefile                           |   3 +-
 kernel/bpf/wrange.c                           |  61 ++++
 tools/testing/selftests/bpf/formal/wrange.py  | 274 ++++++++++++++++++
 .../selftests/bpf/formal/wrange_add.py        |  73 +++++
 .../selftests/bpf/formal/wrange_mul.py        |  87 ++++++
 .../selftests/bpf/formal/wrange_sub.py        |  72 +++++
 7 files changed, 630 insertions(+), 1 deletion(-)
 create mode 100644 include/linux/wrange.h
 create mode 100644 kernel/bpf/wrange.c
 create mode 100755 tools/testing/selftests/bpf/formal/wrange.py
 create mode 100755 tools/testing/selftests/bpf/formal/wrange_add.py
 create mode 100755 tools/testing/selftests/bpf/formal/wrange_mul.py
 create mode 100755 tools/testing/selftests/bpf/formal/wrange_sub.py


base-commit: 856624f12b04a3f51094fa277a31a333ee81cb3f
-- 
2.42.0

[RFC bpf-next v0 1/7] Add inital wrange32 definition along with checks for umin/umax

[Shung-Hsi Yu]

Add struct wrange32 (short for "32-bit wrapped range") and umin/umax
helpers, the latter simply return start/end at the moment. We call the
fields start and end instead of umin and umax, because later patch will
lift the umin <= umax requirement, so we can have cases where umax <
umin; and continuing to call them umin/umax would be confusing.

A struct wrange32 modeled with z3Py is also attached to show that wrange32 in
its current form work as intended.

Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
---
 include/linux/wrange.h                       |  26 ++++
 tools/testing/selftests/bpf/formal/wrange.py | 150 +++++++++++++++++++
 2 files changed, 176 insertions(+)
 create mode 100644 include/linux/wrange.h
 create mode 100755 tools/testing/selftests/bpf/formal/wrange.py

diff --git a/include/linux/wrange.h b/include/linux/wrange.h
new file mode 100644
index 000000000000..e2316c7bbb2d
--- /dev/null
+++ b/include/linux/wrange.h
@@ -0,0 +1,26 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+#ifndef _LINUX_WRANGE_H
+#define _LINUX_WRANGE_H
+
+#include <linux/types.h>
+
+struct wrange32 {
+	/* Start with a usual u32 min/max.
+	 *
+	 * Requiring umin/start <= umax/end, and cannot be use to track s32
+	 * range.
+	 */
+	u32 start; /* umin */
+	u32 end; /* umax */
+};
+
+/* Helper functions that will be required later */
+static inline u32 wrange32_umin(struct wrange32 a) {
+	return a.start;
+}
+
+static inline u32 wrange32_umax(struct wrange32 a) {
+	return a.end;
+}
+
+#endif /* _LINUX_WRANGE_H */
diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py
new file mode 100755
index 000000000000..8836f4cbbedb
--- /dev/null
+++ b/tools/testing/selftests/bpf/formal/wrange.py
@@ -0,0 +1,150 @@
+#!/usr/bin/env python3
+import abc
+from z3 import *
+
+
+# Helpers
+BitVec32 = lambda n: BitVec(n, bv=32)
+BitVecVal32 = lambda v: BitVecVal(v, bv=32)
+
+class Wrange(abc.ABC):
+    SIZE = None # Bitwidth, this will be defined in the subclass
+    name: str
+    start: BitVecRef
+    end: BitVecRef
+
+    def __init__(self, name, start=None, end=None):
+        self.name = name
+        self.start = BitVec(f'Wrange32-{name}-start', bv=self.SIZE) if start is None else start
+        assert(self.start.size() == self.SIZE)
+        self.end = BitVec(f'Wrange32-{name}-end', bv=self.SIZE) if end is None else end
+        assert(self.end.size() == self.SIZE)
+
+    def wellformed(self):
+        # start <= end
+        return ULE(self.start, self.end)
+
+    @property
+    def umin(self):
+        return self.start
+
+    @property
+    def umax(self):
+        return self.end
+
+    # Not used in wrange.c, but helps with checking later
+    def contains(self, val: BitVecRef):
+        assert(val.size() == self.SIZE)
+        # umin <= val <= umax
+        return And(ULE(self.umin, val), ULE(val, self.umax))
+
+
+class Wrange32(Wrange):
+    SIZE = 32 # Working with 32-bit integers
+
+
+__all__ = [
+        'Wrange',
+        'Wrange32',
+        'BitVec32',
+        'BitVecVal32',
+]
+
+
+def main():
+    # A random 32-bit integer called x, that can be of any possible value
+    # unless constrained
+    x = BitVec32('x')
+
+    w1 = Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(1))
+    print(f'Given w1 start={w1.start} end={w1.end}')
+    print('\nChecking w1 is wellformed')
+    prove(
+        w1.wellformed(),
+    )
+    print('\nChecking w1.umin is 1')
+    prove(
+        w1.umin == BitVecVal32(1),
+    )
+    print('\nChecking w1.umax is 1')
+    prove(
+        w1.umax == BitVecVal32(1),
+    )
+    print('\nChecking that w1 contains 1')
+    prove(
+        w1.contains(BitVecVal32(1)),
+    )
+    print('\nChecking that w1 is a set of {1}, with only one element')
+    prove(
+        w1.contains(x) == (x == BitVecVal32(1)),
+    )
+
+    w2 = Wrange32('w2', start=BitVecVal32(2), end=BitVecVal32(2**32 - 1))
+    print(f'\nGiven w2 start={w2.start} end={w2.end}')
+    print('\nChecking w2 is wellformed')
+    prove(
+        w2.wellformed(),
+    )
+    print('\nChecking w2.umin is 2')
+    prove(
+        w2.umin == BitVecVal32(2),
+    )
+    print('\nChecking w2.umax is 2**32-1')
+    prove(
+        w2.umax == BitVecVal32(2**32 - 1),
+    )
+    print('\nChecking that w2 contains 2**32 - 1')
+    prove(
+        w2.contains(BitVecVal32(2**32 - 1)),
+    )
+    print('\nChecking that w2 does NOT contains 1')
+    prove(
+        Not(w2.contains(BitVecVal32(1))),
+    )
+    print('\nChecking that w2 is a set of {2..2**32-1}')
+    prove(
+        # Contrain x such that 2 <= x <= 2**32-1 and check that if x between 2
+        # and 2**32-1 (inclusive), then w2.contains(x) will return true.
+        #
+        # In addition to that, check that the reverse is also true. That is if
+        # x it _not_ a value between 2 and 2**32-1, then w2.contains(x) will
+        # return false.
+        w2.contains(x) == And(ULE(BitVecVal32(2), x), ULE(x, BitVecVal32(2**32-1))),
+    )
+
+    # Right now our semantic doesn't allow umax/end < umin/start
+    w3 = Wrange32('w3', start=BitVecVal32(2), end=BitVecVal32(0))
+    print(f'\nGiven w3 start={w3.start} end={w3.end}')
+    print('\nChecking w3 is NOT wellformed')
+    prove(
+        Not(w3.wellformed()),
+    )
+
+    # General checks that does not assum the value of start/end, except that it
+    # meets the requirement that start <= end.
+    w = Wrange32('w') # Given a Wrange32 called w
+    x = BitVec32('x') # And an 32-bit integer x (redeclared for clarity)
+    print(f'\nGiven any possible Wrange32 called w, and any possible 32-bit integer called x')
+    print('\nChecking if w.contains(x) == True, then w.umin <= (u32)x is also true')
+    prove(
+        Implies(
+            And(
+                w.wellformed(),
+                w.contains(x),
+            ),
+            ULE(w.umin, x),
+        )
+    )
+    print('\nChecking if w.contains(x) == True, then (u32)x <= w.umax is also true')
+    prove(
+        Implies(
+            And(
+                w.wellformed(),
+                w.contains(x),
+            ),
+            ULE(x, w.umax),
+        )
+    )
+
+if __name__ == '__main__':
+    main()
-- 
2.42.0

[RFC bpf-next v0 2/7] Lift the contrain requiring start <= end

[Shung-Hsi Yu]

Lifting the restriction that requires start/umin <= end/umax can allow
us to track range that wraps around in the u32 range, e.g.
{0xffffffff, 0, 1} can be tracked with start=0xffffffff and end=1.
This makes retrieving umin/umax slightly more complicated, and requires
checking whether wrapping occurs in the u32 range; wrange32_uwrapping()
helper is introduced to simplify the check.

Additional z3Py checks are added to make sure the new reasoning around
umin/umax for the u32 wrapping case is correct.

Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
---
 include/linux/wrange.h                       | 26 ++++---
 tools/testing/selftests/bpf/formal/wrange.py | 77 +++++++++++++++++---
 2 files changed, 82 insertions(+), 21 deletions(-)

diff --git a/include/linux/wrange.h b/include/linux/wrange.h
index e2316c7bbb2d..f51e674d1f18 100644
--- a/include/linux/wrange.h
+++ b/include/linux/wrange.h
@@ -3,24 +3,30 @@
 #define _LINUX_WRANGE_H
 
 #include <linux/types.h>
+#include <linux/limits.h>
 
 struct wrange32 {
-	/* Start with a usual u32 min/max.
-	 *
-	 * Requiring umin/start <= umax/end, and cannot be use to track s32
-	 * range.
-	 */
-	u32 start; /* umin */
-	u32 end; /* umax */
+	/* Allow end < start */
+	u32 start;
+	u32 end;
 };
 
-/* Helper functions that will be required later */
+static inline bool wrange32_uwrapping(struct wrange32 a) {
+	return a.end < a.start;
+}
+
 static inline u32 wrange32_umin(struct wrange32 a) {
-	return a.start;
+	if (wrange32_uwrapping(a))
+		return U32_MIN;
+	else
+		return a.start;
 }
 
 static inline u32 wrange32_umax(struct wrange32 a) {
-	return a.end;
+	if (wrange32_uwrapping(a))
+		return U32_MAX;
+	else
+		return a.end;
 }
 
 #endif /* _LINUX_WRANGE_H */
diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py
index 8836f4cbbedb..a2b1b083d291 100755
--- a/tools/testing/selftests/bpf/formal/wrange.py
+++ b/tools/testing/selftests/bpf/formal/wrange.py
@@ -21,22 +21,31 @@ class Wrange(abc.ABC):
         assert(self.end.size() == self.SIZE)
 
     def wellformed(self):
-        # start <= end
-        return ULE(self.start, self.end)
+        # allow end < start, so any start/end combination is valid
+        return BoolVal(True)
+
+    @property
+    def uwrapping(self):
+        # unsigned comparison, (u32)end < (u32)start
+        return ULT(self.end, self.start)
 
     @property
     def umin(self):
-        return self.start
+        return If(self.uwrapping, BitVecVal(0, bv=self.SIZE), self.start)
 
     @property
     def umax(self):
-        return self.end
+        return If(self.uwrapping, BitVecVal(2**self.SIZE - 1, bv=self.SIZE), self.end)
 
     # Not used in wrange.c, but helps with checking later
     def contains(self, val: BitVecRef):
         assert(val.size() == self.SIZE)
-        # umin <= val <= umax
-        return And(ULE(self.umin, val), ULE(val, self.umax))
+        # start <= val <= end
+        nonwrapping_cond = And(ULE(self.start, val), ULE(val, self.end))
+        # 0 <= val <= end or start <= val <= 2**32-1
+        # (omit checking 0 <= val and val <= 2**32-1 since they're always true)
+        wrapping_cond = Or(ULE(val, self.end), ULE(self.start, val))
+        return If(self.uwrapping, wrapping_cond, nonwrapping_cond)
 
 
 class Wrange32(Wrange):
@@ -115,13 +124,59 @@ def main():
     # Right now our semantic doesn't allow umax/end < umin/start
     w3 = Wrange32('w3', start=BitVecVal32(2), end=BitVecVal32(0))
     print(f'\nGiven w3 start={w3.start} end={w3.end}')
-    print('\nChecking w3 is NOT wellformed')
+    print('\nChecking w3 is also wellformed')
     prove(
-        Not(w3.wellformed()),
+        w3.wellformed(),
+    )
+    print('\nChecking w3.umin is 0')
+    prove(
+        w3.umin == BitVecVal32(0),
+    )
+    print('\nChecking w3.umax is 2**32-1')
+    prove(
+        w3.umax == BitVecVal32(2**32 - 1),
+    )
+    print('\nChecking that w3 contains 0')
+    prove(
+        w3.contains(BitVecVal32(0)),
+    )
+    print('\nChecking that w3 does NOT contain 1')
+    prove(
+        Not(w3.contains(BitVecVal32(1))),
+    )
+    print('\nChecking that w3 is a union set of ({0} U {2..2**32-1})')
+    prove(
+        w3.contains(x) == Or(x == BitVecVal32(0), And(ULE(2, x), ULE(x, 2**32-1))),
     )
 
-    # General checks that does not assum the value of start/end, except that it
-    # meets the requirement that start <= end.
+    w4 = Wrange32('w4', start=BitVecVal32(2**32 - 1), end=BitVecVal32(1))
+    print(f'\nGiven w4 start={w4.start} end={w4.end}')
+    print('\nChecking w4 is also wellformed')
+    prove(
+        w4.wellformed(),
+    )
+    print('\nChecking w4.umin is 0')
+    prove(
+        w4.umin == BitVecVal32(0),
+    )
+    print('\nChecking w4.umax is 2**32-1')
+    prove(
+        w4.umax == BitVecVal32(2**32 - 1),
+    )
+    print('\nChecking that w4 contains 0')
+    prove(
+        w4.contains(BitVecVal32(0)),
+    )
+    print('\nChecking that w4 does contain 2**32-1')
+    prove(
+        w4.contains(BitVecVal32(2**32-1)),
+    )
+    print('\nChecking that w4 is a union set of ({2**32-1} U {0..1})')
+    prove(
+        w4.contains(x) == Or(x == BitVecVal32(2**32-1), x == BitVecVal32(0), x == BitVecVal32(1)),
+    )
+
+    # General checks for umin/umax
     w = Wrange32('w') # Given a Wrange32 called w
     x = BitVec32('x') # And an 32-bit integer x (redeclared for clarity)
     print(f'\nGiven any possible Wrange32 called w, and any possible 32-bit integer called x')
@@ -129,7 +184,7 @@ def main():
     prove(
         Implies(
             And(
-                w.wellformed(),
+                w.wellformed(), # Always true, but keeping it for now
                 w.contains(x),
             ),
             ULE(w.umin, x),
-- 
2.42.0

[RFC bpf-next v0 3/7] Support tracking signed min/max

[Shung-Hsi Yu]

With the start <= end restriction lifted, wrange32 gains the ability to
track the s32 range as well. The example provided in previous patch
shows that wrange32 can now track {0xffffffff, 0, 1}, which is in fact
just a plain s32 range {-1, 0, 1}. This patch add helpers to extract the
smin and smax from wrange32 along with wrange32_swrapping() helper that
checks whether this wrange32 wraps in the s32 range.

Additional z3Py checks are added to make sure that the smin/smax
reasoning is correct as well.

Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
---
 include/linux/wrange.h                       | 19 ++++++
 tools/testing/selftests/bpf/formal/wrange.py | 67 +++++++++++++++++++-
 2 files changed, 85 insertions(+), 1 deletion(-)

diff --git a/include/linux/wrange.h b/include/linux/wrange.h
index f51e674d1f18..876e260017fe 100644
--- a/include/linux/wrange.h
+++ b/include/linux/wrange.h
@@ -29,4 +29,23 @@ static inline u32 wrange32_umax(struct wrange32 a) {
 		return a.end;
 }
 
+static inline bool wrange32_swrapping(struct wrange32 a) {
+	return (s32)a.end < (s32)a.start;
+}
+
+/* Helper functions that will be required later */
+static inline s32 wrange32_smin(struct wrange32 a) {
+	if (wrange32_swrapping(a))
+		return S32_MIN;
+	else
+		return a.start;
+}
+
+static inline s32 wrange32_smax(struct wrange32 a) {
+	if (wrange32_swrapping(a))
+		return S32_MAX;
+	else
+		return a.end;
+}
+
 #endif /* _LINUX_WRANGE_H */
diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py
index a2b1b083d291..825d79c6570f 100755
--- a/tools/testing/selftests/bpf/formal/wrange.py
+++ b/tools/testing/selftests/bpf/formal/wrange.py
@@ -37,6 +37,19 @@ class Wrange(abc.ABC):
     def umax(self):
         return If(self.uwrapping, BitVecVal(2**self.SIZE - 1, bv=self.SIZE), self.end)
 
+    @property
+    def swrapping(self):
+        # signed comparison, (s32)end < (s32)start
+        return self.end < self.start
+
+    @property
+    def smin(self):
+        return If(self.swrapping, BitVecVal(1 << (self.SIZE - 1), bv=self.SIZE), self.start)
+
+    @property
+    def smax(self):
+        return If(self.swrapping, BitVecVal((2**self.SIZE - 1) >> 1, bv=self.SIZE), self.end)
+
     # Not used in wrange.c, but helps with checking later
     def contains(self, val: BitVecRef):
         assert(val.size() == self.SIZE)
@@ -79,6 +92,14 @@ def main():
     prove(
         w1.umax == BitVecVal32(1),
     )
+    print('\nChecking w1.smin is 1')
+    prove(
+        w1.smin == BitVecVal32(1),
+    )
+    print('\nChecking w1.smax is 1')
+    prove(
+        w1.smax == BitVecVal32(1),
+    )
     print('\nChecking that w1 contains 1')
     prove(
         w1.contains(BitVecVal32(1)),
@@ -102,6 +123,14 @@ def main():
     prove(
         w2.umax == BitVecVal32(2**32 - 1),
     )
+    print('\nChecking w2.smin is -2147483648/0x80000000')
+    prove(
+        w2.smin == BitVecVal32(0x80000000),
+    )
+    print('\nChecking w2.smax is 2147483647/0x7fffffff')
+    prove(
+        w2.smax == BitVecVal32(0x7fffffff),
+    )
     print('\nChecking that w2 contains 2**32 - 1')
     prove(
         w2.contains(BitVecVal32(2**32 - 1)),
@@ -136,6 +165,14 @@ def main():
     prove(
         w3.umax == BitVecVal32(2**32 - 1),
     )
+    print('\nChecking w3.smin is -2147483648/0x80000000')
+    prove(
+        w3.smin == BitVecVal32(0x80000000),
+    )
+    print('\nChecking w3.smax is 2147483647/0x7fffffff')
+    prove(
+        w3.smax == BitVecVal32(0x7fffffff),
+    )
     print('\nChecking that w3 contains 0')
     prove(
         w3.contains(BitVecVal32(0)),
@@ -163,6 +200,14 @@ def main():
     prove(
         w4.umax == BitVecVal32(2**32 - 1),
     )
+    print('\nChecking w4.smin is -1')
+    prove(
+        w4.smin == BitVecVal32(-1),
+    )
+    print('\nChecking w4.smax is 1')
+    prove(
+        w4.smax == BitVecVal32(1),
+    )
     print('\nChecking that w4 contains 0')
     prove(
         w4.contains(BitVecVal32(0)),
@@ -176,7 +221,7 @@ def main():
         w4.contains(x) == Or(x == BitVecVal32(2**32-1), x == BitVecVal32(0), x == BitVecVal32(1)),
     )
 
-    # General checks for umin/umax
+    # General checks for umin/umax/smin/smax
     w = Wrange32('w') # Given a Wrange32 called w
     x = BitVec32('x') # And an 32-bit integer x (redeclared for clarity)
     print(f'\nGiven any possible Wrange32 called w, and any possible 32-bit integer called x')
@@ -200,6 +245,26 @@ def main():
             ULE(x, w.umax),
         )
     )
+    print('\nChecking if w.contains(x) == True, then w.smin <= (s32)x is also true')
+    prove(
+        Implies(
+            And(
+                w.wellformed(),
+                w.contains(x),
+            ),
+            w.smin <= x,
+        )
+    )
+    print('\nChecking if w.contains(x) == True, then (s32)x <= w.smax is also true')
+    prove(
+        Implies(
+            And(
+                w.wellformed(),
+                w.contains(x),
+            ),
+            x <= w.smax,
+        )
+    )
 
 if __name__ == '__main__':
     main()
-- 
2.42.0

[RFC bpf-next v0 4/7] Implement wrange32_add()

[Shung-Hsi Yu]

Implement wrange32_add() that takes two wrange32 and compute a new wrange32
that contains all possible combinations of sums produced by adding values in
the two wrange32.

This is done by adding start and end of both wrange32 for the majority of
cases, and works even when the addition overflows. However, there still exist
cases where the addition of two wrange32 result in a range that is too large to
track, this happens when the combined length is too large. When this happens we
fallback to start=U32_MIN and end=U32_MAX.
(Calling end-minus-start as "length" because one can visual wrange32 as
a number line, and thus end point minus starting point would naturally
be the length of such line)

Additionally, make sure wrange.c gets compilation checked, and add
wrange_add.py that models and check wrange32_add().

Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
---
 include/linux/wrange.h                        |  2 +
 kernel/bpf/Makefile                           |  3 +-
 kernel/bpf/wrange.c                           | 17 +++++
 tools/testing/selftests/bpf/formal/wrange.py  |  4 +
 .../selftests/bpf/formal/wrange_add.py        | 73 +++++++++++++++++++
 5 files changed, 98 insertions(+), 1 deletion(-)
 create mode 100644 kernel/bpf/wrange.c
 create mode 100755 tools/testing/selftests/bpf/formal/wrange_add.py

diff --git a/include/linux/wrange.h b/include/linux/wrange.h
index 876e260017fe..0c4a8affd877 100644
--- a/include/linux/wrange.h
+++ b/include/linux/wrange.h
@@ -11,6 +11,8 @@ struct wrange32 {
 	u32 end;
 };
 
+struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b);
+
 static inline bool wrange32_uwrapping(struct wrange32 a) {
 	return a.end < a.start;
 }
diff --git a/kernel/bpf/Makefile b/kernel/bpf/Makefile
index f526b7573e97..f0a4ce21e2ff 100644
--- a/kernel/bpf/Makefile
+++ b/kernel/bpf/Makefile
@@ -6,7 +6,8 @@ cflags-nogcse-$(CONFIG_X86)$(CONFIG_CC_IS_GCC) := -fno-gcse
 endif
 CFLAGS_core.o += $(call cc-disable-warning, override-init) $(cflags-nogcse-yy)
 
-obj-$(CONFIG_BPF_SYSCALL) += syscall.o verifier.o inode.o helpers.o tnum.o log.o
+# At least make sure wrange.c compiles
+obj-$(CONFIG_BPF_SYSCALL) += syscall.o verifier.o inode.o helpers.o tnum.o log.o wrange.o
 obj-$(CONFIG_BPF_SYSCALL) += bpf_iter.o map_iter.o task_iter.o prog_iter.o link_iter.o
 obj-$(CONFIG_BPF_SYSCALL) += hashtab.o arraymap.o percpu_freelist.o bpf_lru_list.o lpm_trie.o map_in_map.o bloom_filter.o
 obj-$(CONFIG_BPF_SYSCALL) += local_storage.o queue_stack_maps.o ringbuf.o
diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c
new file mode 100644
index 000000000000..8cdbc21a51f2
--- /dev/null
+++ b/kernel/bpf/wrange.c
@@ -0,0 +1,17 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+#include <linux/wrange.h>
+
+#define WRANGE32(_s, _e) ((struct wrange32) {.start = _s, .end = _e})
+
+struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b)
+{
+	u32 a_len = a.end - a.start;
+	u32 b_len = b.end - b.start;
+	u32 new_len = a_len + b_len;
+
+	/* the new start/end pair goes full circle, so any value is possible */
+	if (new_len < a_len || new_len < b_len)
+		return WRANGE32(U32_MIN, U32_MAX);
+	else
+		return WRANGE32(a.start + b.start, a.end + b.end);
+}
diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py
index 825d79c6570f..c659cfd3a52c 100755
--- a/tools/testing/selftests/bpf/formal/wrange.py
+++ b/tools/testing/selftests/bpf/formal/wrange.py
@@ -24,6 +24,10 @@ class Wrange(abc.ABC):
         # allow end < start, so any start/end combination is valid
         return BoolVal(True)
 
+    @property
+    def length(self):
+        return self.end - self.start
+
     @property
     def uwrapping(self):
         # unsigned comparison, (u32)end < (u32)start
diff --git a/tools/testing/selftests/bpf/formal/wrange_add.py b/tools/testing/selftests/bpf/formal/wrange_add.py
new file mode 100755
index 000000000000..43d035383fe4
--- /dev/null
+++ b/tools/testing/selftests/bpf/formal/wrange_add.py
@@ -0,0 +1,73 @@
+#!/usr/bin/env python3
+from z3 import *
+from wrange import *
+
+
+def wrange_add(a: Wrange, b: Wrange):
+    wrange_class = type(a)
+    assert(a.SIZE == b.SIZE)
+
+    new_length = a.length + b.length
+    too_wide = Or(ULT(new_length, a.length), ULT(new_length, b.length))
+    new_start = If(too_wide, BitVecVal(0, a.SIZE), a.start + b.start)
+    new_end = If(too_wide, BitVecVal(2**a.SIZE-1, a.SIZE), a.end + b.end)
+    return wrange_class(f'{a.name} + {b.name}', new_start, new_end)
+
+
+def main():
+    x = BitVec32('x')
+    w = wrange_add(
+        # {1, 2, 3}
+        Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(3)),
+        # + {0}
+        Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(0)),
+    )   # = {1, 2, 3}
+    print('Checking {1, 2, 3} + {0} = {1, 2, 3}')
+    prove(               # 1 <= x <= 3
+        w.contains(x) == And(BitVecVal32(1) <= x, x <= BitVecVal32(3)),
+    )
+
+    w = wrange_add(
+        # {-1}
+        Wrange32('w1', start=BitVecVal32(-1), end=BitVecVal32(-1)),
+        # + {0, 1, 2}
+        Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(2)),
+    )   # = {-1, 0, 1}
+    print('\nChecking {-1} + {0, 1, 2} = {-1, 0, 1}')
+    prove(               # -1 <= x <= 1
+        w.contains(x) == And(BitVecVal32(-1) <= x, x <= BitVecVal32(1)),
+    )
+
+    # A general check to make sure wrange_add() is sound
+    x = BitVec32('x')
+    y = BitVec32('y')
+    w1 = Wrange32('w1')
+    w2 = Wrange32('w2')
+    w = wrange_add(w1, w2)
+    premise = And(
+        w1.wellformed(),
+        w2.wellformed(),
+        w1.contains(x),
+        w2.contains(y),
+    )
+    # Suppose we have a wrange32 called w1 that contains the 32-bit integer x
+    # (where x can be any possible value contained inside w1), and another
+    # wrange32 called w2 that similarly contains 32-bit integer y.
+    #
+    # The sum of w1 and w2 calculated from wrange_add(w1, w2), called w, should
+    # _always_ contains the sum of x and y, no matter what.
+    print('\nChecking that if w1.contains(x) and w2.contains(y), then wrange32_add(w1, w2).contains(x+y)')
+    print('(note: this may take awhile)')
+    prove(
+        Implies(
+            premise,
+            And(
+                w.contains(x + y),
+                w.wellformed(),
+            ),
+        )
+    )
+
+
+if __name__ == '__main__':
+    main()
-- 
2.42.0

[RFC bpf-next v0 5/7] Implement wrange32_sub()

[Shung-Hsi Yu]

Implement wrange32_sub() that takes two wrange32 and compute a new
wrange32 that contains all possible combinations of difference produced
by subtracting values in the two wrange32. Simliar to wrange32_add(),
the implementation can work even when underflow occurs, but when the
resulting length is too large to track we again fallback to
start=U32_MIN and end=U32_MAX.

Also add wrange_sub.py that models and check wrange32_sub().

Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
---
 include/linux/wrange.h                        |  1 +
 kernel/bpf/wrange.c                           | 13 ++++
 .../selftests/bpf/formal/wrange_sub.py        | 72 +++++++++++++++++++
 3 files changed, 86 insertions(+)
 create mode 100755 tools/testing/selftests/bpf/formal/wrange_sub.py

diff --git a/include/linux/wrange.h b/include/linux/wrange.h
index 0c4a8affd877..ef02f5b06705 100644
--- a/include/linux/wrange.h
+++ b/include/linux/wrange.h
@@ -12,6 +12,7 @@ struct wrange32 {
 };
 
 struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b);
+struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b);
 
 static inline bool wrange32_uwrapping(struct wrange32 a) {
 	return a.end < a.start;
diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c
index 8cdbc21a51f2..08bb7e129d7f 100644
--- a/kernel/bpf/wrange.c
+++ b/kernel/bpf/wrange.c
@@ -15,3 +15,16 @@ struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b)
 	else
 		return WRANGE32(a.start + b.start, a.end + b.end);
 }
+
+struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b)
+{
+	u32 a_len = a.end - a.start;
+	u32 b_len = b.end - b.start;
+	u32 new_len = a_len + b_len;
+
+	/* the new start/end pair goes full circle, so any value is possible */
+	if (new_len < a_len || new_len < b_len)
+		return WRANGE32(U32_MIN, U32_MAX);
+	else
+		return WRANGE32(a.start - b.end, a.end - b.start);
+}
diff --git a/tools/testing/selftests/bpf/formal/wrange_sub.py b/tools/testing/selftests/bpf/formal/wrange_sub.py
new file mode 100755
index 000000000000..63abf4d2d978
--- /dev/null
+++ b/tools/testing/selftests/bpf/formal/wrange_sub.py
@@ -0,0 +1,72 @@
+#!/usr/bin/env python3
+from z3 import *
+from wrange import *
+
+
+def wrange_sub(a: Wrange, b: Wrange):
+    wrange_class = type(a)
+    assert(a.SIZE == b.SIZE)
+
+    new_length = a.length + b.length
+    too_wide = Or(ULT(new_length, a.length), ULT(new_length, b.length))
+    new_start = If(too_wide, BitVecVal(0, a.SIZE), a.start - b.end)
+    new_end = If(too_wide, BitVecVal(2**a.SIZE-1, a.SIZE), a.end - b.start)
+    return wrange_class(f'{a.name} - {b.name}', new_start, new_end)
+
+
+def main():
+    x = BitVec32('x')
+    w = wrange_sub(
+        # {1, 2, 3}
+        Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(3)),
+        # - {0}
+        Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(0)),
+    )   # = {1, 2, 3}
+    print('Checking {1, 2, 3} - {0} = {1, 2, 3}')
+    prove(               # 1 <= x <= 3
+        w.contains(x) == And(1 <= x, x <= 3)
+    )
+
+    w = wrange_sub(
+        # {-1}
+        Wrange32('w1', start=BitVecVal32(-1), end=BitVecVal32(-1)),
+        # - {0, 1, 2}
+        Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(2)),
+    )   # = {-3, -2, -1}
+    print('\nChecking {-1} - {0, 1, 2} = {-3, -2, -1}')
+    prove(               # -3 <= x <= -1
+        w.contains(x) == And(-3 <= x, x <= -1),
+    )
+
+    # A general check to make sure wrange_sub() is sound
+    w1 = Wrange32('w1')
+    w2 = Wrange32('w2')
+    w = wrange_sub(w1, w2)
+    x = BitVec32('x')
+    y = BitVec32('y')
+    premise = And(
+        w1.wellformed(),
+        w2.wellformed(),
+        w1.contains(x),
+        w2.contains(y),
+    )
+    # Suppose we have a wrange32 called w1 that contains the 32-bit integer x
+    # (where x can be any possible value contained inside w1), and another
+    # wrange32 called w2 that similarly contains 32-bit integer y.
+    #
+    # The difference of w1 and w2 calculated from wrange_sub(w1, w2), called w,
+    # should _always_ contains the difference of x and y, no matter what.
+    print('\nChecking that if w1.contains(x) and w2.contains(y), then wrange32_sub(w1, w2).contains(x-y)')
+    print('(note: this may take awhile)')
+    prove(
+        Implies(
+            premise,
+            And(
+                w.contains(x - y),
+                w.wellformed(),
+            ),
+        )
+    )
+
+if __name__ == '__main__':
+    main()
-- 
2.42.0

[RFC bpf-next v0 6/7] Implement wrange32_mul()

[Shung-Hsi Yu]

Implement wrange32_mul() that takes two wrange32 and compute a new
wrange32 that contains all possible combinations of product produced by
multiplying values in the two wrange32. This implementation is pretty
much the unsigned version of scalar32_min_max_mul(), and does not take
full advantage of unification. This can be further improved if needed.

Also add wrange_mul.py that models and check wrange32_mul(). However at
the time of writing this model checking for wrange32_mul is still
on-going.

Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
---
 include/linux/wrange.h                        |  1 +
 kernel/bpf/wrange.c                           | 15 ++++
 .../selftests/bpf/formal/wrange_mul.py        | 87 +++++++++++++++++++
 3 files changed, 103 insertions(+)
 create mode 100755 tools/testing/selftests/bpf/formal/wrange_mul.py

diff --git a/include/linux/wrange.h b/include/linux/wrange.h
index ef02f5b06705..45d3db3f518b 100644
--- a/include/linux/wrange.h
+++ b/include/linux/wrange.h
@@ -13,6 +13,7 @@ struct wrange32 {
 
 struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b);
 struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b);
+struct wrange32 wrange32_mul(struct wrange32 a, struct wrange32 b);
 
 static inline bool wrange32_uwrapping(struct wrange32 a) {
 	return a.end < a.start;
diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c
index 08bb7e129d7f..4ca253e55743 100644
--- a/kernel/bpf/wrange.c
+++ b/kernel/bpf/wrange.c
@@ -28,3 +28,18 @@ struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b)
 	else
 		return WRANGE32(a.start - b.end, a.end - b.start);
 }
+
+/* Model checking is still on-going for wrange32_mul() */
+struct wrange32 wrange32_mul(struct wrange32 a, struct wrange32 b)
+{
+	/* Be lazy and don't deal with wrange that contains large value that
+	 * may overflow as well as wrange32 with negative number. This can be
+	 * improved if needed.
+	 */
+	if (a.end > U16_MAX || b.end > U16_MAX)
+		return WRANGE32(U32_MIN, U32_MAX);
+	else if (wrange32_smin(a) < 0 || wrange32_smin(b) < 0)
+		return WRANGE32(U32_MIN, U32_MAX);
+	else
+		return WRANGE32(a.start - b.end, a.end - b.start);
+}
diff --git a/tools/testing/selftests/bpf/formal/wrange_mul.py b/tools/testing/selftests/bpf/formal/wrange_mul.py
new file mode 100755
index 000000000000..bd95fc6367b2
--- /dev/null
+++ b/tools/testing/selftests/bpf/formal/wrange_mul.py
@@ -0,0 +1,87 @@
+#!/usr/bin/env python3
+from z3 import *
+from wrange import *
+
+
+# This could be further improved if needed
+def wrange_mul(a: Wrange, b: Wrange):
+    wrange_class = type(a)
+    assert(a.SIZE == b.SIZE)
+
+    too_large = Or(UGT(a.end, BitVecVal(2**(a.SIZE/2)-1, bv=a.SIZE)), UGT(b.end, BitVecVal(2**(b.SIZE/2)-1, bv=b.SIZE)))
+    negative = Or(a.smin < 0, b.smin < 0)
+    giveup = Or(too_large, negative)
+    new_start = If(giveup, BitVecVal(0, a.SIZE), a.start * b.start)
+    new_end = If(giveup, BitVecVal(-1, a.SIZE), a.end * b.end)
+    return wrange_class(f'{a.name} * {b.name}', new_start, new_end)
+
+
+def main():
+    x = BitVec32('x')
+    w = wrange_mul(
+        # {1, 2, 3}
+        Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(3)),
+        # - {0}
+        Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(0)),
+    )   # = {0}
+    print('Checking {1, 2, 3} * {0} = {0}')
+    prove(               #x can only be 0
+        w.contains(x) == (x == BitVecVal32(0))
+    )
+
+    w = wrange_mul(
+        # {0xfff0..0xffff}
+        Wrange32('w1', start=BitVecVal32(0xff0), end=BitVecVal32(0xfff)),
+        # - {0xf0..0xff}
+        Wrange32('w2', start=BitVecVal32(0xf0), end=BitVecVal32(0xff)),
+    )   # = {0xeff100..0xfeff01}
+    print('Checking {0xff0..0xfff} * {0xf0..0xff} = {0xef100..0xfef01}')
+    prove(               # 0xef100 <= x <= 0xfef01
+        w.contains(x) == And(ULE(BitVecVal32(0xef100), x), ULE(x, BitVecVal32(0xfef01)))
+    )
+
+    # Multiplication is not implemented when there's negative number, but it
+    # could be made to work
+    w = wrange_mul(
+        # {-1}
+        Wrange32('w1', start=BitVecVal32(-1), end=BitVecVal32(-1)),
+        # * {0, 1, 2}
+        Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(2)),
+    )   # = {-2, -1, 0}
+    print('\nChecking {-1} * {0, 1, 2} = {S32_MIN..S32_MAX}')
+    prove(
+        w.contains(x) == BoolVal(True),
+    )
+
+    # A general check to make sure wrange_mul() is sound
+    w1 = Wrange32('w1')
+    w2 = Wrange32('w2')
+    w = wrange_mul(w1, w2)
+    x = BitVec32('x')
+    y = BitVec32('y')
+    premise = And(
+        w1.wellformed(),
+        w2.wellformed(),
+        w1.contains(x),
+        w2.contains(y),
+    )
+    # Suppose we have a wrange32 called w1 that contains the 32-bit integer x
+    # (where x can be any possible value contained inside w1), and another
+    # wrange32 called w2 that similarly contains 32-bit integer y.
+    #
+    # The product of w1 and w2 calculated from wrange32_mul(w1, w2), called w,
+    # should _always_ contains the product of x and y, no matter what.
+    print('\nChecking that if w1.contains(x) and w2.contains(y), then wrange32_mul(w1, w2).contains(x*y)')
+    print('(note: this takes a very, very, long time to run)')
+    prove(
+        Implies(
+            premise,
+            And(
+                w.contains(x * y),
+                w.wellformed(),
+            ),
+        )
+    )
+
+if __name__ == '__main__':
+    main()
-- 
2.42.0

[RFC bpf-next v0 7/7] (WIP) Add helper functions that transform wrange32 to and from smin/smax/umin/umax

[Shung-Hsi Yu]

To check how wrange32 logic interacts with current verifier codebase, it
is necessary to try integrating it as soon as possible in order to take
advantange of the selftests we have. One way for this to be done is by
adding a helper function that takes smin/smax/umin/umax from
bpf_reg_state and turn them into wrange32, then do calculation in
wrange32_{add,sub,mul} instead of scalar32_min_max_{add,sub,mul}, and
turn the resulting wrange32 back into smin/smax/umin/umax with another
helper function.

wrange32_to_min_max() is easy and readily available, however I'm still
working on wrange32_from_min_max(), which is trickier.

Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
---
 include/linux/wrange.h |  6 ++++++
 kernel/bpf/wrange.c    | 16 ++++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/include/linux/wrange.h b/include/linux/wrange.h
index 45d3db3f518b..cecdecefab53 100644
--- a/include/linux/wrange.h
+++ b/include/linux/wrange.h
@@ -11,6 +11,12 @@ struct wrange32 {
 	u32 end;
 };
 
+/* Create wrange32 from bpf_reg_state's s32_min/s32_max/u32_min/u32_max */
+struct wrange32 wrange32_from_min_max(s32 s32_min, s32 s32_max,
+		                      u32 u32_min, u32 u32_max);
+/* Turn wrange32 back into s32_min/s32_max/u32_min/u32_max */
+void wrange32_to_min_max(struct wrange32 w, s32 *s32_min, s32 *s32_max,
+			 u32 *u32_min, u32 *u32_max);
 struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b);
 struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b);
 struct wrange32 wrange32_mul(struct wrange32 a, struct wrange32 b);
diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c
index 4ca253e55743..c150efb42cd2 100644
--- a/kernel/bpf/wrange.c
+++ b/kernel/bpf/wrange.c
@@ -3,6 +3,22 @@
 
 #define WRANGE32(_s, _e) ((struct wrange32) {.start = _s, .end = _e})
 
+struct wrange32 wrange32_from_min_max(s32 s32_min, s32 s32_max,
+				      u32 u32_min, u32 u32_max)
+{
+	/* To be implemented */
+	return WRANGE32(U32_MIN, U32_MAX);
+}
+
+void wrange32_to_min_max(struct wrange32 w, s32 *s32_min, s32 *s32_max,
+			 u32 *u32_min, u32 *u32_max)
+{
+	*s32_min = wrange32_smin(w);
+	*s32_max = wrange32_smax(w);
+	*u32_min = wrange32_umin(w);
+	*u32_max = wrange32_umax(w);
+}
+
 struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b)
 {
 	u32 a_len = a.end - a.start;
-- 
2.42.0

Re: [RFC bpf-next v0 0/7] Unifying signed and unsigned min/max tracking

[Alexei Starovoitov]

On Tue, Nov 7, 2023 at 9:46 PM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>
> This patchset is a proof of concept for previously discussed concept[1]
> of unifying smin/smax with umin/uax for both the 32-bit and 64-bit
> range[2] within bpf_reg_state. This will allow the verifier to track
> both signed and unsiged ranges using just two u32 (for 32-bit range) or
> u64 (for 64-bit range), instead four as we currently do.
>
> The size reduction we gain from this probably isn't very significant.
> The main benefit is in lowering of code _complexity_. The verifier
> currently employs 5 value tracking mechanisms, two for 64-bit range, two
> for 32-bit range, and one tnum that tracks individual bits. Exchanging
> knowledge between all the bound tracking mechanisms requires a
> (theoretical) 20-way synchronization[3]; with signed and unsigned
> unification the verifier will only need 3 value tracking mechanism,
> cutting this down to a 6-way synchronization.
>
> The unification is possible from a theoretical standpoint[4] and there
> exists implementation[5]. The challenge lies in implementing it inside
> the verifier and making sure it fits well with all the logic we have in
> place.
>
> To lower the difficulty, the unified min/max tracking is implemented in
> isolation, and have it correctness checked using model checking. The
> model checking code can be found in this patchset as well, but is not
> meant to be merged since a better method already exists[6].
>
> So far I've managed to implement add/sub/mul operations for unified
> min/max tracking, the next steps are:
> - implement operation that can be used gain knowledge from conditional
>   jump, e.g wrange32_intersect, wrange32_diff
> - implement wrange32_from_min_max and wrange32_to_min_max so we can
>   check whether this PoC works using current selftests
> - implement operations for wrange64, the 64-bit counterpart of wrange32
> - come up with how to exchange knowledge between wrange64 and wrange32
>   (this is likely the most difficult part)
> - think about how to integrate this work in a manageable manner

Thanks for taking a stab at it.
The biggest question is how to integrate it without breaking anything.
I suspect you might need to implement all alu and branch logic
just to be able to run the tests.
It's difficult to see a path for partial/incremental addition.
The concern is that at the end this approach might hit an issue
which will make it infeasible.
So it's a big bet. Might be nice correctness and memory saving or nothing.
Certainly exciting, but proceed with caution.

Re: [RFC bpf-next v0 0/7] Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

On Thu, Nov 09, 2023 at 11:38:09AM -0800, Alexei Starovoitov wrote:
> On Tue, Nov 7, 2023 at 9:46 PM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > This patchset is a proof of concept for previously discussed concept[1]
> > of unifying smin/smax with umin/uax for both the 32-bit and 64-bit
> > range[2] within bpf_reg_state. This will allow the verifier to track
> > both signed and unsiged ranges using just two u32 (for 32-bit range) or
> > u64 (for 64-bit range), instead four as we currently do.
> >
> > The size reduction we gain from this probably isn't very significant.
> > The main benefit is in lowering of code _complexity_. The verifier
> > currently employs 5 value tracking mechanisms, two for 64-bit range, two
> > for 32-bit range, and one tnum that tracks individual bits. Exchanging
> > knowledge between all the bound tracking mechanisms requires a
> > (theoretical) 20-way synchronization[3]; with signed and unsigned
> > unification the verifier will only need 3 value tracking mechanism,
> > cutting this down to a 6-way synchronization.
> >
> > The unification is possible from a theoretical standpoint[4] and there
> > exists implementation[5]. The challenge lies in implementing it inside
> > the verifier and making sure it fits well with all the logic we have in
> > place.
> >
> > To lower the difficulty, the unified min/max tracking is implemented in
> > isolation, and have it correctness checked using model checking. The
> > model checking code can be found in this patchset as well, but is not
> > meant to be merged since a better method already exists[6].
> >
> > So far I've managed to implement add/sub/mul operations for unified
> > min/max tracking, the next steps are:
> > - implement operation that can be used gain knowledge from conditional
> >   jump, e.g wrange32_intersect, wrange32_diff
> > - implement wrange32_from_min_max and wrange32_to_min_max so we can
> >   check whether this PoC works using current selftests
> > - implement operations for wrange64, the 64-bit counterpart of wrange32
> > - come up with how to exchange knowledge between wrange64 and wrange32
> >   (this is likely the most difficult part)
> > - think about how to integrate this work in a manageable manner
> 
> Thanks for taking a stab at it.
> The biggest question is how to integrate it without breaking anything.
> I suspect you might need to implement all alu and branch logic
> just to be able to run the tests.

Once the wrange32_{to,from}_min_max() helpers in patch 7 is implemented, I
should be able to swap out individual alu operation while keeping
bpf_reg_state untouched. E.g. for addition in 32-bit

  static void scalar32_min_max_add(struct bpf_reg_state *dst_reg,
                                   struct bpf_reg_state *src_reg)
  {
      struct wrange32 a = wrange32_from_min_max(dst_reg->smin, dst_reg->smax,
                                                dst_reg->umin, dst_reg->umax);
      struct wrange32 b = wrange32_from_min_max(src_reg->smin, src_reg->smax,
                                                src_reg->umin, src_reg->umax);
      
      wrange32_to_min_max(wrange32_add(a, b), &dst_reg->smin, &dst_reg->smax,
                          &dst_reg->umin, &dst_reg->umax);
  }

and get current tests to run on top of the new algorithm. This won't cover
every aspect, but should be enough as a first taste on how well (or unwell)
the integration will be.

These helpers also can help to create finer intermediate steps for smoother
integration; something that's added in the beginning to aid the transition,
but removed after the transition is done.

> It's difficult to see a path for partial/incremental addition.
> The concern is that at the end this approach might hit an issue
> which will make it infeasible.

Agree. While the helpers above can aid with integration, I do not see a safe
path for partial addition. At least not before everything until
reg_bound_sync() proofs to work should it be considered.
Still a long way to go.

> So it's a big bet. Might be nice correctness and memory saving or nothing.
> Certainly exciting, but proceed with caution.

Having enough optimism and attachment to tackle this but not too much to the
point of overlooking its flaws is certainly a challenging task.
Will try my best :)

Thanks for the feedbacks!

Re: [RFC bpf-next v0 0/7] Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

On Sat, Nov 11, 2023 at 11:45:22AM +0800, Shung-Hsi Yu wrote:
> On Thu, Nov 09, 2023 at 11:38:09AM -0800, Alexei Starovoitov wrote:
> > On Tue, Nov 7, 2023 at 9:46 PM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > > This patchset is a proof of concept for previously discussed concept[1]
> > > of unifying smin/smax with umin/uax for both the 32-bit and 64-bit
> > > range[2] within bpf_reg_state. This will allow the verifier to track
> > > both signed and unsiged ranges using just two u32 (for 32-bit range) or
> > > u64 (for 64-bit range), instead four as we currently do.
> > >
> > > The size reduction we gain from this probably isn't very significant.
> > > The main benefit is in lowering of code _complexity_. The verifier
> > > currently employs 5 value tracking mechanisms, two for 64-bit range, two
> > > for 32-bit range, and one tnum that tracks individual bits. Exchanging
> > > knowledge between all the bound tracking mechanisms requires a
> > > (theoretical) 20-way synchronization[3]; with signed and unsigned
> > > unification the verifier will only need 3 value tracking mechanism,
> > > cutting this down to a 6-way synchronization.
> > >
> > > The unification is possible from a theoretical standpoint[4] and there
> > > exists implementation[5]. The challenge lies in implementing it inside
> > > the verifier and making sure it fits well with all the logic we have in
> > > place.
> > >
> > > To lower the difficulty, the unified min/max tracking is implemented in
> > > isolation, and have it correctness checked using model checking. The
> > > model checking code can be found in this patchset as well, but is not
> > > meant to be merged since a better method already exists[6].
> > >
> > > So far I've managed to implement add/sub/mul operations for unified
> > > min/max tracking, the next steps are:
> > > - implement operation that can be used gain knowledge from conditional
> > >   jump, e.g wrange32_intersect, wrange32_diff
> > > - implement wrange32_from_min_max and wrange32_to_min_max so we can
> > >   check whether this PoC works using current selftests
> > > - implement operations for wrange64, the 64-bit counterpart of wrange32
> > > - come up with how to exchange knowledge between wrange64 and wrange32
> > >   (this is likely the most difficult part)
> > > - think about how to integrate this work in a manageable manner
> > 
> > Thanks for taking a stab at it.
> > The biggest question is how to integrate it without breaking anything.
> > I suspect you might need to implement all alu and branch logic
> > just to be able to run the tests.
> 
> Once the wrange32_{to,from}_min_max() helpers in patch 7 is implemented, I
> should be able to swap out individual alu operation while keeping
> bpf_reg_state untouched. E.g. for addition in 32-bit
> 
>   static void scalar32_min_max_add(struct bpf_reg_state *dst_reg,
>                                    struct bpf_reg_state *src_reg)
>   {
>       struct wrange32 a = wrange32_from_min_max(dst_reg->smin, dst_reg->smax,
>                                                 dst_reg->umin, dst_reg->umax);
>       struct wrange32 b = wrange32_from_min_max(src_reg->smin, src_reg->smax,
>                                                 src_reg->umin, src_reg->umax);
>       
>       wrange32_to_min_max(wrange32_add(a, b), &dst_reg->smin, &dst_reg->smax,
>                           &dst_reg->umin, &dst_reg->umax);
>   }
> 
> and get current tests to run on top of the new algorithm. This won't cover
> every aspect, but should be enough as a first taste on how well (or unwell)
> the integration will be.
> 
> These helpers also can help to create finer intermediate steps for smoother
> integration; something that's added in the beginning to aid the transition,
> but removed after the transition is done.
> 
> > It's difficult to see a path for partial/incremental addition.
> > The concern is that at the end this approach might hit an issue
> > which will make it infeasible.
> 
> Agree. While the helpers above can aid with integration, I do not see a safe
> path for partial addition. At least not before everything until
> reg_bound_sync() proofs to work should it be considered.
> Still a long way to go.

Meant to say "everything until, and including, reg_bound_sync() are
proofed to work", since it is likely the hardest part.

[...]