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

Commit Message

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

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

Patch

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