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

Commit Message

Shung-Hsi Yu Nov. 8, 2023, 5:46 a.m. UTC

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 <[e-mail]>
---
 include/linux/wrange.h                       | 26 ++++---
 tools/testing/selftests/bpf/formal/wrange.py | 77 +++++++++++++++++---
 2 files changed, 82 insertions(+), 21 deletions(-)

Patch

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),