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

Commit Message

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

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 <[e-mail]>
---
 include/linux/wrange.h                       | 19 ++++++
 tools/testing/selftests/bpf/formal/wrange.py | 67 +++++++++++++++++++-
 2 files changed, 85 insertions(+), 1 deletion(-)

Patch

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