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

Commit Message

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

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 <[e-mail]>
---
 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

Patch

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