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@xxxxxxxx>
---
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
