[PATCH v2 bpf-next 0/7] BPF register bounds logic and testing improvements

[PATCH v2 bpf-next 0/7] BPF register bounds logic and testing improvements

[Andrii Nakryiko]

This patch set adds a big set of manual and auto-generated test cases
validating BPF verifier's register bounds tracking and deduction logic. See
details in the last patch.

To make this approach work, BPF verifier's logic needed a bunch of
improvements to handle some cases that previously were not covered. This had
no implications as to correctness of verifier logic, but it was incomplete
enough to cause significant disagreements with alternative implementation of
register bounds logic that tests in this patch set implement. So we need BPF
verifier logic improvements to make all the tests pass.

This is a first part of work with the end goal intended to extend register
bounds logic to cover range vs range comparisons, which will be submitted
later assuming changes in this patch set land.

See individual patches for details.

v1->v2:
  - fix compilation when building selftests with llvm-16 toolchain (CI).

Andrii Nakryiko (7):
  bpf: improve JEQ/JNE branch taken logic
  bpf: derive smin/smax from umin/max bounds
  bpf: enhance subregister bounds deduction logic
  bpf: improve deduction of 64-bit bounds from 32-bit bounds
  bpf: try harder to deduce register bounds from different numeric
    domains
  bpf: drop knowledge-losing __reg_combine_{32,64}_into_{64,32} logic
  selftests/bpf: BPF register range bounds tester

 kernel/bpf/verifier.c                         |  175 +-
 .../selftests/bpf/prog_tests/reg_bounds.c     | 1668 +++++++++++++++++
 2 files changed, 1791 insertions(+), 52 deletions(-)
 create mode 100644 tools/testing/selftests/bpf/prog_tests/reg_bounds.c

-- 
2.34.1

[PATCH v2 bpf-next 1/7] bpf: improve JEQ/JNE branch taken logic

[Andrii Nakryiko]

When determining if if/else branch will always or never be taken, use
signed range knowledge in addition to currently used unsigned range knowledge.
If either signed or unsigned range suggests that condition is
always/never taken, return corresponding branch_taken verdict.

Current use of unsigned range for this seems arbitrary and unnecessarily
incomplete. It is possible for *signed* operations to be performed on
register, which could "invalidate" unsigned range for that register. In
such case branch_taken will be artificially useless, even if we can
still tell that some constant is outside of register value range based
on its signed bounds.

veristat-based validation shows zero differences across selftests,
Cilium, and Meta-internal BPF object files.

Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 kernel/bpf/verifier.c | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index bb58987e4844..c87144e3c5e8 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -13663,12 +13663,16 @@ static int is_branch32_taken(struct bpf_reg_state *reg, u32 val, u8 opcode)
 			return !!tnum_equals_const(subreg, val);
 		else if (val < reg->u32_min_value || val > reg->u32_max_value)
 			return 0;
+		else if (sval < reg->s32_min_value || sval > reg->s32_max_value)
+			return 0;
 		break;
 	case BPF_JNE:
 		if (tnum_is_const(subreg))
 			return !tnum_equals_const(subreg, val);
 		else if (val < reg->u32_min_value || val > reg->u32_max_value)
 			return 1;
+		else if (sval < reg->s32_min_value || sval > reg->s32_max_value)
+			return 1;
 		break;
 	case BPF_JSET:
 		if ((~subreg.mask & subreg.value) & val)
@@ -13740,12 +13744,16 @@ static int is_branch64_taken(struct bpf_reg_state *reg, u64 val, u8 opcode)
 			return !!tnum_equals_const(reg->var_off, val);
 		else if (val < reg->umin_value || val > reg->umax_value)
 			return 0;
+		else if (sval < reg->smin_value || sval > reg->smax_value)
+			return 0;
 		break;
 	case BPF_JNE:
 		if (tnum_is_const(reg->var_off))
 			return !tnum_equals_const(reg->var_off, val);
 		else if (val < reg->umin_value || val > reg->umax_value)
 			return 1;
+		else if (sval < reg->smin_value || sval > reg->smax_value)
+			return 1;
 		break;
 	case BPF_JSET:
 		if ((~reg->var_off.mask & reg->var_off.value) & val)
-- 
2.34.1

[PATCH v2 bpf-next 2/7] bpf: derive smin/smax from umin/max bounds

[Andrii Nakryiko]

Add smin/smax derivation from appropriate umin/umax values. Previously the
logic was surprisingly asymmetric, trying to derive umin/umax from smin/smax
(if possible), but not trying to do the same in the other direction. A simple
addition to __reg64_deduce_bounds() fixes this.

Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 kernel/bpf/verifier.c | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index c87144e3c5e8..ee9837463092 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2151,6 +2151,13 @@ static void __reg32_deduce_bounds(struct bpf_reg_state *reg)
 
 static void __reg64_deduce_bounds(struct bpf_reg_state *reg)
 {
+	/* u64 range forms a valid s64 range (due to matching sign bit),
+	 * so try to learn from that
+	 */
+	if ((s64)reg->umin_value <= (s64)reg->umax_value) {
+		reg->smin_value = max_t(s64, reg->smin_value, reg->umin_value);
+		reg->smax_value = min_t(s64, reg->smax_value, reg->umax_value);
+	}
 	/* Learn sign from signed bounds.
 	 * If we cannot cross the sign boundary, then signed and unsigned bounds
 	 * are the same, so combine.  This works even in the negative case, e.g.
-- 
2.34.1

[PATCH v2 bpf-next 3/7] bpf: enhance subregister bounds deduction logic

[Andrii Nakryiko]

Add handling of a bunch of possible cases which allows deducing extra
information about subregister bounds, both u32 and s32, from full register
u64/s64 bounds.

Also add smin32/smax32 bounds derivation from corresponding umin32/umax32
bounds, similar to what we did with smin/smax from umin/umax derivation in
previous patch.

Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 kernel/bpf/verifier.c | 52 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index ee9837463092..d5fd41fb3031 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2117,6 +2117,58 @@ static void __update_reg_bounds(struct bpf_reg_state *reg)
 /* Uses signed min/max values to inform unsigned, and vice-versa */
 static void __reg32_deduce_bounds(struct bpf_reg_state *reg)
 {
+	/* if upper 32 bits of u64/s64 range don't change,
+	 * we can use lower 32 bits to improve our u32/s32 boundaries
+	 */
+	if ((reg->umin_value >> 32) == (reg->umax_value >> 32)) {
+		/* u64 to u32 casting preserves validity of low 32 bits as
+		 * a range, if upper 32 bits are the same
+		 */
+		reg->u32_min_value = max_t(u32, reg->u32_min_value, (u32)reg->umin_value);
+		reg->u32_max_value = min_t(u32, reg->u32_max_value, (u32)reg->umax_value);
+
+		if ((s32)reg->umin_value <= (s32)reg->umax_value) {
+			reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->umin_value);
+			reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->umax_value);
+		}
+	}
+	if ((reg->smin_value >> 32) == (reg->smax_value >> 32)) {
+		/* low 32 bits should form a proper u32 range */
+		if ((u32)reg->smin_value <= (u32)reg->smax_value) {
+			reg->u32_min_value = max_t(u32, reg->u32_min_value, (u32)reg->smin_value);
+			reg->u32_max_value = min_t(u32, reg->u32_max_value, (u32)reg->smax_value);
+		}
+		/* low 32 bits should form a proper s32 range */
+		if ((s32)reg->smin_value <= (s32)reg->smax_value) {
+			reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->smin_value);
+			reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
+		}
+	}
+	/* Special case where upper bits form a small sequence of two
+	 * sequential numbers (in 32-bit unsigned space, so 0xffffffff to
+	 * 0x00000000 is also valid), while lower bits form a proper s32 range
+	 * going from negative numbers to positive numbers.
+	 * E.g.: [0xfffffff0ffffff00; 0xfffffff100000010]. Iterating
+	 * over full 64-bit numbers range will form a proper [-16, 16]
+	 * ([0xffffff00; 0x00000010]) range in its lower 32 bits.
+	 */
+	if ((u32)(reg->umin_value >> 32) + 1 == (u32)(reg->umax_value >> 32) &&
+	    (s32)reg->umin_value < 0 && (s32)reg->umax_value >= 0) {
+		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->umin_value);
+		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->umax_value);
+	}
+	if ((u32)(reg->smin_value >> 32) + 1 == (u32)(reg->smax_value >> 32) &&
+	    (s32)reg->smin_value < 0 && (s32)reg->smax_value >= 0) {
+		reg->s32_min_value = max_t(s32, reg->s32_min_value, (s32)reg->smin_value);
+		reg->s32_max_value = min_t(s32, reg->s32_max_value, (s32)reg->smax_value);
+	}
+	/* if u32 range forms a valid s32 range (due to matching sign bit),
+	 * try to learn from that
+	 */
+	if ((s32)reg->u32_min_value <= (s32)reg->u32_max_value) {
+		reg->s32_min_value = max_t(s32, reg->s32_min_value, reg->u32_min_value);
+		reg->s32_max_value = min_t(s32, reg->s32_max_value, reg->u32_max_value);
+	}
 	/* Learn sign from signed bounds.
 	 * If we cannot cross the sign boundary, then signed and unsigned bounds
 	 * are the same, so combine.  This works even in the negative case, e.g.
-- 
2.34.1

[PATCH v2 bpf-next 4/7] bpf: improve deduction of 64-bit bounds from 32-bit bounds

[Andrii Nakryiko]

Add a few interesting cases in which we can tighten 64-bit bounds based
on newly learnt information about 32-bit bounds. E.g., when full u64/s64
registers are used in BPF program, and then eventually compared as
u32/s32. The latter comparison doesn't change the value of full
register, but it does impose new restrictions on possible lower 32 bits
of such full registers. And we can use that to derive additional full
register bounds information.

Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 kernel/bpf/verifier.c | 47 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index d5fd41fb3031..0a968dac3294 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2242,10 +2242,57 @@ static void __reg64_deduce_bounds(struct bpf_reg_state *reg)
 	}
 }
 
+static void __reg_deduce_mixed_bounds(struct bpf_reg_state *reg)
+{
+	/* Try to tighten 64-bit bounds from 32-bit knowledge, using 32-bit
+	 * values on both sides of 64-bit range in hope to have tigher range.
+	 * E.g., if r1 is [0x1'00000000, 0x3'80000000], and we learn from
+	 * 32-bit signed > 0 operation that s32 bounds are now [1; 0x7fffffff].
+	 * With this, we can substitute 1 as low 32-bits of _low_ 64-bit bound
+	 * (0x100000000 -> 0x100000001) and 0x7fffffff as low 32-bits of
+	 * _high_ 64-bit bound (0x380000000 -> 0x37fffffff) and arrive at a
+	 * better overall bounds for r1 as [0x1'000000001; 0x3'7fffffff].
+	 * We just need to make sure that derived bounds we are intersecting
+	 * with are well-formed ranges in respecitve s64 or u64 domain, just
+	 * like we do with similar kinds of 32-to-64 or 64-to-32 adjustments.
+	 */
+	__u64 new_umin, new_umax;
+	__s64 new_smin, new_smax;
+
+	/* u32 -> u64 tightening, it's always well-formed */
+	new_umin = (reg->umin_value & ~0xffffffffULL) | reg->u32_min_value;
+	new_umax = (reg->umax_value & ~0xffffffffULL) | reg->u32_max_value;
+	reg->umin_value = max_t(u64, reg->umin_value, new_umin);
+	reg->umax_value = min_t(u64, reg->umax_value, new_umax);
+
+	/* s32 -> u64 tightening, s32 should be a valid u32 range (same sign) */
+	if ((u32)reg->s32_min_value <= (u32)reg->s32_max_value) {
+		new_umin = (reg->umin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
+		new_umax = (reg->umax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
+		reg->umin_value = max_t(u64, reg->umin_value, new_umin);
+		reg->umax_value = min_t(u64, reg->umax_value, new_umax);
+	}
+
+	/* u32 -> s64 tightening, u32 range embedded into s64 preserves range validity */
+	new_smin = (reg->smin_value & ~0xffffffffULL) | reg->u32_min_value;
+	new_smax = (reg->smax_value & ~0xffffffffULL) | reg->u32_max_value;
+	reg->smin_value = max_t(s64, reg->smin_value, new_smin);
+	reg->smax_value = min_t(s64, reg->smax_value, new_smax);
+
+	/* s32 -> s64 tightening, check that s32 range behaves as u32 range */
+	if ((u32)reg->s32_min_value <= (u32)reg->s32_max_value) {
+		new_smin = (reg->smin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
+		new_smax = (reg->smax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
+		reg->smin_value = max_t(s64, reg->smin_value, new_smin);
+		reg->smax_value = min_t(s64, reg->smax_value, new_smax);
+	}
+}
+
 static void __reg_deduce_bounds(struct bpf_reg_state *reg)
 {
 	__reg32_deduce_bounds(reg);
 	__reg64_deduce_bounds(reg);
+	__reg_deduce_mixed_bounds(reg);
 }
 
 /* Attempts to improve var_off based on unsigned min/max information */
-- 
2.34.1

[PATCH v2 bpf-next 5/7] bpf: try harder to deduce register bounds from different numeric domains

[Andrii Nakryiko]

There are cases (caught by subsequent reg_bounds tests in selftests/bpf)
where performing one round of __reg_deduce_bounds() doesn't propagate
all the information from, say, s32 to u32 bounds and than from newly
learned u32 bounds back to u64 and s64. So perform __reg_deduce_bounds()
twice to make sure such derivations are propagated fully after
reg_bounds_sync().

One such example is test `(s64)[0xffffffff00000001; 0] (u64)<
0xffffffff00000000` from selftest patch from this patch set. It demonstrates an
intricate dance of u64 -> s64 -> u64 -> u32 bounds adjustments, which requires
two rounds of __reg_deduce_bounds(). Here are corresponding refinement log from
selftest, showing evolution of knowledge.

REFINING (FALSE R1) (u64)SRC=[0xffffffff00000000; U64_MAX] (u64)DST_OLD=[0; U64_MAX] (u64)DST_NEW=[0xffffffff00000000; U64_MAX]
REFINING (FALSE R1) (u64)SRC=[0xffffffff00000000; U64_MAX] (s64)DST_OLD=[0xffffffff00000001; 0] (s64)DST_NEW=[0xffffffff00000001; -1]
REFINING (FALSE R1) (s64)SRC=[0xffffffff00000001; -1] (u64)DST_OLD=[0xffffffff00000000; U64_MAX] (u64)DST_NEW=[0xffffffff00000001; U64_MAX]
REFINING (FALSE R1) (u64)SRC=[0xffffffff00000001; U64_MAX] (u32)DST_OLD=[0; U32_MAX] (u32)DST_NEW=[1; U32_MAX]

R1 initially has smin/smax set to [0xffffffff00000001; -1], while umin/umax is
unknown. After (u64)< comparison, in FALSE branch we gain knowledge that
umin/umax is [0xffffffff00000000; U64_MAX]. That causes smin/smax to learn that
zero can't happen and upper bound is -1. Then smin/smax is adjusted from
umin/umax improving lower bound from 0xffffffff00000000 to 0xffffffff00000001.
And then eventually umin32/umax32 bounds are drived from umin/umax and become
[1; U32_MAX].

Selftest in the last patch is actually implementing a multi-round fixed-point
convergence logic, but so far all the tests are handled by two rounds of
reg_bounds_sync() on the verifier state, so we keep it simple for now.

Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 kernel/bpf/verifier.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 0a968dac3294..cf5cd6bf8652 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2314,6 +2314,7 @@ static void reg_bounds_sync(struct bpf_reg_state *reg)
 	__update_reg_bounds(reg);
 	/* We might have learned something about the sign bit. */
 	__reg_deduce_bounds(reg);
+	__reg_deduce_bounds(reg);
 	/* We might have learned some bits from the bounds. */
 	__reg_bound_offset(reg);
 	/* Intersecting with the old var_off might have improved our bounds
-- 
2.34.1

[PATCH v2 bpf-next 6/7] bpf: drop knowledge-losing __reg_combine_{32,64}_into_{64,32} logic

[Andrii Nakryiko]

When performing 32-bit conditional operation operating on lower 32 bits
of a full 64-bit register, register full value isn't changed. We just
potentially gain new knowledge about that register's lower 32 bits.

Unfortunately, __reg_combine_{32,64}_into_{64,32} logic that
reg_set_min_max() performs as a last step, can lose information in some
cases due to __mark_reg64_unbounded() and __reg_assign_32_into_64().
That's bad and completely unnecessary. Especially __reg_assign_32_into_64()
looks completely out of place here, because we are not performing
zero-extending subregister assignment during conditional jump.

So this patch replaced __reg_combine_* with just a normal
reg_bounds_sync() which will do a proper job of deriving u64/s64 bounds
from u32/s32, and vice versa (among all other combinations).

__reg_combine_64_into_32() is also used in one more place,
coerce_reg_to_size(), while handling 1- and 2-byte register loads.
Looking into this, it seems like besides marking subregister as
unbounded before performing reg_bounds_sync(), we were also performing
deduction of smin32/smax32 and umin32/umax32 bounds from respective
smin/smax and umin/umax bounds. It's now redundant as reg_bounds_sync()
performs all the same logic more generically (e.g., without unnecessary
assumption that upper 32 bits of full register should be zero).

Long story short, we remove __reg_combine_64_into_32() completely, and
coerce_reg_to_size() now only does resetting subreg to unbounded and then
performing reg_bounds_sync() to recover as much information as possible
from 64-bit umin/umax and smin/smax bounds, set explicitly in
coerce_reg_to_size() earlier.

Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 kernel/bpf/verifier.c | 60 ++++++-------------------------------------
 1 file changed, 8 insertions(+), 52 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index cf5cd6bf8652..a603ac82d50c 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2348,51 +2348,6 @@ static void __reg_assign_32_into_64(struct bpf_reg_state *reg)
 	}
 }
 
-static void __reg_combine_32_into_64(struct bpf_reg_state *reg)
-{
-	/* special case when 64-bit register has upper 32-bit register
-	 * zeroed. Typically happens after zext or <<32, >>32 sequence
-	 * allowing us to use 32-bit bounds directly,
-	 */
-	if (tnum_equals_const(tnum_clear_subreg(reg->var_off), 0)) {
-		__reg_assign_32_into_64(reg);
-	} else {
-		/* Otherwise the best we can do is push lower 32bit known and
-		 * unknown bits into register (var_off set from jmp logic)
-		 * then learn as much as possible from the 64-bit tnum
-		 * known and unknown bits. The previous smin/smax bounds are
-		 * invalid here because of jmp32 compare so mark them unknown
-		 * so they do not impact tnum bounds calculation.
-		 */
-		__mark_reg64_unbounded(reg);
-	}
-	reg_bounds_sync(reg);
-}
-
-static bool __reg64_bound_s32(s64 a)
-{
-	return a >= S32_MIN && a <= S32_MAX;
-}
-
-static bool __reg64_bound_u32(u64 a)
-{
-	return a >= U32_MIN && a <= U32_MAX;
-}
-
-static void __reg_combine_64_into_32(struct bpf_reg_state *reg)
-{
-	__mark_reg32_unbounded(reg);
-	if (__reg64_bound_s32(reg->smin_value) && __reg64_bound_s32(reg->smax_value)) {
-		reg->s32_min_value = (s32)reg->smin_value;
-		reg->s32_max_value = (s32)reg->smax_value;
-	}
-	if (__reg64_bound_u32(reg->umin_value) && __reg64_bound_u32(reg->umax_value)) {
-		reg->u32_min_value = (u32)reg->umin_value;
-		reg->u32_max_value = (u32)reg->umax_value;
-	}
-	reg_bounds_sync(reg);
-}
-
 /* Mark a register as having a completely unknown (scalar) value. */
 static void __mark_reg_unknown(const struct bpf_verifier_env *env,
 			       struct bpf_reg_state *reg)
@@ -6089,9 +6044,10 @@ static void coerce_reg_to_size(struct bpf_reg_state *reg, int size)
 	 * values are also truncated so we push 64-bit bounds into
 	 * 32-bit bounds. Above were truncated < 32-bits already.
 	 */
-	if (size >= 4)
-		return;
-	__reg_combine_64_into_32(reg);
+	if (size < 4) {
+		__mark_reg32_unbounded(reg);
+		reg_bounds_sync(reg);
+	}
 }
 
 static void set_sext64_default_val(struct bpf_reg_state *reg, int size)
@@ -14169,13 +14125,13 @@ static void reg_set_min_max(struct bpf_reg_state *true_reg,
 					     tnum_subreg(false_32off));
 		true_reg->var_off = tnum_or(tnum_clear_subreg(true_64off),
 					    tnum_subreg(true_32off));
-		__reg_combine_32_into_64(false_reg);
-		__reg_combine_32_into_64(true_reg);
+		reg_bounds_sync(false_reg);
+		reg_bounds_sync(true_reg);
 	} else {
 		false_reg->var_off = false_64off;
 		true_reg->var_off = true_64off;
-		__reg_combine_64_into_32(false_reg);
-		__reg_combine_64_into_32(true_reg);
+		reg_bounds_sync(false_reg);
+		reg_bounds_sync(true_reg);
 	}
 }
 
-- 
2.34.1

[PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

Add tests that validate correctness and completeness of BPF verifier's
register range bounds.

The main bulk is a lot of auto-generated tests based on a small set of
seed values for lower and upper 32 bits of full 64-bit values.
Currently we validate only range vs const comparisons, but the idea is
to start validating range over range comparisons in subsequent patch set.

When setting up initial register ranges we treat registers as one of
u64/s64/u32/s32 numeric types, and then independently perform conditional
comparisons based on a potentially different u64/s64/u32/s32 types. This
tests lots of tricky cases of deriving bounds information across
different numeric domains.

Given there are lots of auto-generated cases, we guard them behind
SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
With current full set of upper/lower seed value, all supported
comparison operators and all the combinations of u64/s64/u32/s32 number
domains, we get about 7.7 million tests, which run in about 35 minutes
on my local qemu instance. So it's something that can be run manually
for exhaustive check in a reasonable time, and perhaps as a nightly CI
test, but certainly is too slow to run as part of a default test_progs run.

We also add a small set of tricky conditions that came up during
development and triggered various bugs or corner cases in either
selftest's reimplementation of range bounds logic or in verifier's logic
itself. These are fast enough to be run as part of normal test_progs
test run and are great for a quick sanity checking.

Let's take a look at test output to understand what's going on:

  $ sudo ./test_progs -t reg_bounds_crafted
  #191/1   reg_bounds_crafted/(u64)[0; 0xffffffff] (u64)< 0:OK
  ...
  #191/115 reg_bounds_crafted/(u64)[0; 0x17fffffff] (s32)< 0:OK
  ...
  #191/137 reg_bounds_crafted/(u64)[0xffffffff; 0x100000000] (u64)== 0:OK

Each test case is uniquely and fully described by this generated string.
E.g.: "(u64)[0; 0x17fffffff] (s32)< 0". This means that we
initialize a register (R6) in such a way that verifier knows that it can
have a value in [(u64)0; (u64)0x17fffffff] range. Another
register (R7) is also set up as u64, but this time a constant (zero in
this case). They then are compared using 32-bit signed < operation.
Resulting TRUE/FALSE branches are evaluated (including cases where it's
known that one of the branches will never be taken, in which case we
validate that verifier also determines this as a dead code). Test
validates that verifier's final register state matches expected state
based on selftest's own reg_state logic, implemented from scratch for
cross-checking purposes.

These test names can be conveniently used for further debugging, and if -vv
verboseness is requested we can get a corresponding verifier log (with
mark_precise logs filtered out as irrelevant and distracting). Example below is
slightly redacted for brevity, omitting irrelevant register output in
some places, marked with [...].

  $ sudo ./test_progs -a 'reg_bounds_crafted/(u32)[0; U32_MAX] (s32)< -1' -vv
  ...
  VERIFIER LOG:
  ========================
  func#0 @0
  0: R1=ctx(off=0,imm=0) R10=fp0
  0: (05) goto pc+2
  3: (85) call bpf_get_current_pid_tgid#14      ; R0_w=scalar()
  4: (bc) w6 = w0                       ; R0_w=scalar() R6_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff))
  5: (85) call bpf_get_current_pid_tgid#14      ; R0_w=scalar()
  6: (bc) w7 = w0                       ; R0_w=scalar() R7_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff))
  7: (b4) w1 = 0                        ; R1_w=0
  8: (b4) w2 = -1                       ; R2=4294967295
  9: (ae) if w6 < w1 goto pc-9
  9: R1=0 R6=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff))
  10: (2e) if w6 > w2 goto pc-10
  10: R2=4294967295 R6=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff))
  11: (b4) w1 = -1                      ; R1_w=4294967295
  12: (b4) w2 = -1                      ; R2_w=4294967295
  13: (ae) if w7 < w1 goto pc-13        ; R1_w=4294967295 R7=4294967295
  14: (2e) if w7 > w2 goto pc-14
  14: R2_w=4294967295 R7=4294967295
  15: (bc) w0 = w6                      ; [...] R6=scalar(id=1,smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff))
  16: (bc) w0 = w7                      ; [...] R7=4294967295
  17: (ce) if w6 s< w7 goto pc+3        ; R6=scalar(id=1,smin=0,smax=umax=4294967295,smin32=-1,var_off=(0x0; 0xffffffff)) R7=4294967295
  18: (bc) w0 = w6                      ; [...] R6=scalar(id=1,smin=0,smax=umax=4294967295,smin32=-1,var_off=(0x0; 0xffffffff))
  19: (bc) w0 = w7                      ; [...] R7=4294967295
  20: (95) exit

  from 17 to 21: [...]
  21: (bc) w0 = w6                      ; [...] R6=scalar(id=1,smin=umin=umin32=2147483648,smax=umax=umax32=4294967294,smax32=-2,var_off=(0x80000000; 0x7fffffff))
  22: (bc) w0 = w7                      ; [...] R7=4294967295
  23: (95) exit

  from 13 to 1: [...]
  1: [...]
  1: (b7) r0 = 0                        ; R0_w=0
  2: (95) exit
  processed 24 insns (limit 1000000) max_states_per_insn 0 total_states 2 peak_states 2 mark_read 1
  =====================

Verifier log above is for `(u32)[0; U32_MAX] (s32)< -1` use cases, where u32
range is used for initialization, followed by signed < operator. Note
how we use w6/w7 in this case for register initialization (it would be
R6/R7 for 64-bit types) and then `if w6 s< w7` for comparison at
instruction #17. It will be `if R6 < R7` for 64-bit unsigned comparison.
Above example gives a good impression of the overall structure of a BPF
programs generated for reg_bounds tests.

In the future, this "framework" can be extended to test not just
conditional jumps, but also arithmetic operations. Adding randomized
testing is another possibility.

Some implementation notes. We basically have our own generics-like
operations on numbers, where all the numbers are stored in u64, but how
they are interpreted is passed as runtime argument enum num_t. Further,
`struct range` represents a bounds range, and those are collected
together into a minimal `struct reg_state`, which collects range bounds
across all four numberical domains: u64, s64, u32, s64.

Based on these primitives and `enum op` representing possible
conditional operation (<, <=, >, >=, ==, !=), there is a set of generic
helpers to perform "range arithmetics", which is used to maintain struct
reg_state. We simulate what verifier will do for reg bounds of R6 and R7
registers using these range and reg_state primitives. Simulated
information is used to determine branch taken conclusion and expected
exact register state across all four number domains.

Implementation of "range arithmetics" is more generic than what verifier
is currently performing: it allows range over range comparisons and
adjustments. This is the intended end goal of this work and verifier
logic is expected to be enhanced to range vs range operations in
subsequent patch set.

Signed-off-by: Andrii Nakryiko <andrii@kernel.org>
---
 .../selftests/bpf/prog_tests/reg_bounds.c     | 1668 +++++++++++++++++
 1 file changed, 1668 insertions(+)
 create mode 100644 tools/testing/selftests/bpf/prog_tests/reg_bounds.c

diff --git a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
new file mode 100644
index 000000000000..8d433a1d7654
--- /dev/null
+++ b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
@@ -0,0 +1,1668 @@
+// SPDX-License-Identifier: GPL-2.0
+/* Copyright (c) 2023 Meta Platforms, Inc. and affiliates. */
+
+#define _GNU_SOURCE
+#include <limits.h>
+#include <test_progs.h>
+#include <linux/filter.h>
+#include <linux/bpf.h>
+
+/* =================================
+ * SHORT AND CONSISTENT NUMBER TYPES
+ * =================================
+ */
+#define U64_MAX ((u64)UINT64_MAX)
+#define U32_MAX ((u32)UINT_MAX)
+#define S64_MIN ((s64)INT64_MIN)
+#define S64_MAX ((s64)INT64_MAX)
+#define S32_MIN ((s32)INT_MIN)
+#define S32_MAX ((s32)INT_MAX)
+
+typedef unsigned long long ___u64;
+typedef unsigned int ___u32;
+typedef long long ___s64;
+typedef int ___s32;
+
+/* avoid conflicts with already defined types in kernel headers */
+#define u64 ___u64
+#define u32 ___u32
+#define s64 ___s64
+#define s32 ___s32
+
+/* ==================================
+ * STRING BUF ABSTRACTION AND HELPERS
+ * ==================================
+ */
+struct strbuf {
+	size_t buf_sz;
+	int pos;
+	char buf[0];
+};
+
+#define DEFINE_STRBUF(name, N)						\
+	struct { struct strbuf buf; char data[(N)]; } ___##name;	\
+	struct strbuf *name = (___##name.buf.buf_sz = (N), ___##name.buf.pos = 0, &___##name.buf)
+
+__printf(2, 3)
+static inline void snappendf(struct strbuf *s, const char *fmt, ...)
+{
+	va_list args;
+
+	va_start(args, fmt);
+	s->pos += vsnprintf(s->buf + s->pos, s->buf_sz - s->pos, fmt, args);
+	va_end(args);
+}
+
+/* ==================================
+ * GENERIC NUMBER TYPE AND OPERATIONS
+ * ==================================
+ */
+enum num_t { U64, U32, S64, S32 };
+#define MIN_T U64
+#define MAX_T S32
+
+static __always_inline u64 min_t(enum num_t t, u64 x, u64 y)
+{
+	switch (t) {
+	case U64: return (u64)x < (u64)y ? (u64)x : (u64)y;
+	case U32: return (u32)x < (u32)y ? (u32)x : (u32)y;
+	case S64: return (s64)x < (s64)y ? (s64)x : (s64)y;
+	case S32: return (s32)x < (s32)y ? (s32)x : (s32)y;
+	default: printf("min_t!\n"); exit(1);
+	}
+}
+
+static __always_inline u64 max_t(enum num_t t, u64 x, u64 y)
+{
+	switch (t) {
+	case U64: return (u64)x > (u64)y ? (u64)x : (u64)y;
+	case U32: return (u32)x > (u32)y ? (u32)x : (u32)y;
+	case S64: return (s64)x > (s64)y ? (s64)x : (s64)y;
+	case S32: return (s32)x > (s32)y ? (u32)(s32)x : (u32)(s32)y;
+	default: printf("max_t!\n"); exit(1);
+	}
+}
+
+static const char *t_str(enum num_t t)
+{
+	switch (t) {
+	case U64: return "u64";
+	case U32: return "u32";
+	case S64: return "s64";
+	case S32: return "s32";
+	default: printf("t_str!\n"); exit(1);
+	}
+}
+
+static enum num_t t_is_32(enum num_t t)
+{
+	switch (t) {
+	case U64: return false;
+	case U32: return true;
+	case S64: return false;
+	case S32: return true;
+	default: printf("t_is_32!\n"); exit(1);
+	}
+}
+
+static enum num_t t_signed(enum num_t t)
+{
+	switch (t) {
+	case U64: return S64;
+	case U32: return S32;
+	case S64: return S64;
+	case S32: return S32;
+	default: printf("t_signed!\n"); exit(1);
+	}
+}
+
+static enum num_t t_unsigned(enum num_t t)
+{
+	switch (t) {
+	case U64: return U64;
+	case U32: return U32;
+	case S64: return U64;
+	case S32: return U32;
+	default: printf("t_unsigned!\n"); exit(1);
+	}
+}
+
+static bool num_is_small(enum num_t t, u64 x)
+{
+	switch (t) {
+	case U64: return (u64)x <= 256;
+	case U32: return (u32)x <= 256;
+	case S64: return (s64)x >= -256 && (s64)x <= 256;
+	case S32: return (s32)x >= -256 && (s32)x <= 256;
+	default: printf("num_is_small!\n"); exit(1);
+	}
+}
+
+static void snprintf_num(enum num_t t, struct strbuf *sb, u64 x)
+{
+	bool is_small = num_is_small(t, x);
+
+	if (is_small) {
+		switch (t) {
+		case U64: return snappendf(sb, "%llu", (u64)x);
+		case U32: return snappendf(sb, "%u", (u32)x);
+		case S64: return snappendf(sb, "%lld", (s64)x);
+		case S32: return snappendf(sb, "%d", (s32)x);
+		default: printf("snprintf_num!\n"); exit(1);
+		}
+	} else {
+		switch (t) {
+		case U64:
+			if (x == U64_MAX)
+				return snappendf(sb, "U64_MAX");
+			else if (x >= U64_MAX - 256)
+				return snappendf(sb, "U64_MAX-%llu", U64_MAX - x);
+			else
+				return snappendf(sb, "%#llx", (u64)x);
+		case U32:
+			if ((u32)x == U32_MAX)
+				return snappendf(sb, "U32_MAX");
+			else if ((u32)x >= U32_MAX - 256)
+				return snappendf(sb, "U32_MAX-%u", U32_MAX - (u32)x);
+			else
+				return snappendf(sb, "%#x", (u32)x);
+		case S64:
+			if ((s64)x == S64_MAX)
+				return snappendf(sb, "S64_MAX");
+			else if ((s64)x >= S64_MAX - 256)
+				return snappendf(sb, "S64_MAX-%lld", S64_MAX - (s64)x);
+			else if ((s64)x == S64_MIN)
+				return snappendf(sb, "S64_MIN");
+			else if ((s64)x <= S64_MIN + 256)
+				return snappendf(sb, "S64_MIN+%lld", (s64)x - S64_MIN);
+			else
+				return snappendf(sb, "%#llx", (s64)x);
+		case S32:
+			if ((s32)x == S32_MAX)
+				return snappendf(sb, "S32_MAX");
+			else if ((s32)x >= S32_MAX - 256)
+				return snappendf(sb, "S32_MAX-%d", S32_MAX - (s32)x);
+			else if ((s32)x == S32_MIN)
+				return snappendf(sb, "S32_MIN");
+			else if ((s32)x <= S32_MIN + 256)
+				return snappendf(sb, "S32_MIN+%d", (s32)x - S32_MIN);
+			else
+				return snappendf(sb, "%#x", (s32)x);
+		default: printf("snprintf_num!\n"); exit(1);
+		}
+	}
+}
+
+/* ===================================
+ * GENERIC RANGE STRUCT AND OPERATIONS
+ * ===================================
+ */
+struct range {
+	u64 a, b;
+};
+
+static void snprintf_range(enum num_t t, struct strbuf *sb, struct range x)
+{
+	if (x.a == x.b)
+		return snprintf_num(t, sb, x.a);
+
+	snappendf(sb, "[");
+	snprintf_num(t, sb, x.a);
+	snappendf(sb, "; ");
+	snprintf_num(t, sb, x.b);
+	snappendf(sb, "]");
+}
+
+static void print_range(enum num_t t, struct range x, const char *sfx)
+{
+	DEFINE_STRBUF(sb, 128);
+
+	snprintf_range(t, sb, x);
+	printf("%s%s", sb->buf, sfx);
+}
+
+static const struct range unkn[] = {
+	[U64] = { 0, U64_MAX },
+	[U32] = { 0, U32_MAX },
+	[S64] = { (u64)S64_MIN, (u64)S64_MAX },
+	[S32] = { (u64)(u32)S32_MIN, (u64)(u32)S32_MAX },
+};
+
+static struct range unkn_subreg(enum num_t t)
+{
+	switch (t) {
+	case U64: return unkn[U32];
+	case U32: return unkn[U32];
+	case S64: return unkn[U32];
+	case S32: return unkn[S32];
+	default: printf("unkn_subreg!\n"); exit(1);
+	}
+}
+
+static struct range range(enum num_t t, u64 a, u64 b)
+{
+	switch (t) {
+	case U64: return (struct range){ (u64)a, (u64)b };
+	case U32: return (struct range){ (u32)a, (u32)b };
+	case S64: return (struct range){ (s64)a, (s64)b };
+	case S32: return (struct range){ (u32)(s32)a, (u32)(s32)b };
+	default: printf("range!\n"); exit(1);
+	}
+}
+
+static __always_inline u32 sign64(u64 x) { return (x >> 63) & 1; }
+static __always_inline u32 sign32(u64 x) { return ((u32)x >> 31) & 1; }
+static __always_inline u32 upper32(u64 x) { return (u32)(x >> 32); }
+static __always_inline u64 swap_low32(u64 x, u32 y) { return (x & 0xffffffff00000000ULL) | y; }
+
+static bool range_eq(struct range x, struct range y)
+{
+	return x.a == y.a && x.b == y.b;
+}
+
+static struct range range_cast_to_s32(struct range x)
+{
+	u64 a = x.a, b = x.b;
+
+	/* if upper 32 bits are constant, lower 32 bits should form a proper
+	 * s32 range to be correct
+	 */
+	if (upper32(a) == upper32(b) && (s32)a <= (s32)b)
+		return range(S32, a, b);
+
+	/* Special case where upper bits form a small sequence of two
+	 * sequential numbers (in 32-bit unsigned space, so 0xffffffff to
+	 * 0x00000000 is also valid), while lower bits form a proper s32 range
+	 * going from negative numbers to positive numbers.
+	 *
+	 * E.g.: [0xfffffff0ffffff00; 0xfffffff100000010]. Iterating
+	 * over full 64-bit numbers range will form a proper [-16, 16]
+	 * ([0xffffff00; 0x00000010]) range in its lower 32 bits.
+	 */
+	if (upper32(a) + 1 == upper32(b) && (s32)a < 0 && (s32)b >= 0)
+		return range(S32, a, b);
+
+	/* otherwise we can't derive much meaningful information */
+	return unkn[S32];
+}
+
+static struct range range_cast_u64(enum num_t to_t, struct range x)
+{
+	u64 a = (u64)x.a, b = (u64)x.b;
+
+	switch (to_t) {
+	case U64:
+		return x;
+	case U32:
+		if (upper32(a) != upper32(b))
+			return unkn[U32];
+		return range(U32, a, b);
+	case S64:
+		if (sign64(a) != sign64(b))
+			return unkn[S64];
+		return range(S64, a, b);
+	case S32:
+		return range_cast_to_s32(x);
+	default: printf("range_cast_u64!\n"); exit(1);
+	}
+}
+
+static struct range range_cast_s64(enum num_t to_t, struct range x)
+{
+	s64 a = (s64)x.a, b = (s64)x.b;
+
+	switch (to_t) {
+	case U64:
+		/* equivalent to (s64)a <= (s64)b check */
+		if (sign64(a) != sign64(b))
+			return unkn[U64];
+		return range(U64, a, b);
+	case U32:
+		if (upper32(a) != upper32(b) || sign32(a) != sign32(b))
+			return unkn[U32];
+		return range(U32, a, b);
+	case S64:
+		return x;
+	case S32:
+		return range_cast_to_s32(x);
+	default: printf("range_cast_s64!\n"); exit(1);
+	}
+}
+
+static struct range range_cast_u32(enum num_t to_t, struct range x)
+{
+	u32 a = (u32)x.a, b = (u32)x.b;
+
+	switch (to_t) {
+	case U64:
+	case S64:
+		/* u32 is always a valid zero-extended u64/s64 */
+		return range(to_t, a, b);
+	case U32:
+		return x;
+	case S32:
+		return range_cast_to_s32(range(U32, a, b));
+	default: printf("range_cast_u32!\n"); exit(1);
+	}
+}
+
+static struct range range_cast_s32(enum num_t to_t, struct range x)
+{
+	s32 a = (s32)x.a, b = (s32)x.b;
+
+	switch (to_t) {
+	case U64:
+	case U32:
+	case S64:
+		if (sign32(a) != sign32(b))
+			return unkn[to_t];
+		return range(to_t, a, b);
+	case S32:
+		return x;
+	default: printf("range_cast_s32!\n"); exit(1);
+	}
+}
+
+/* Reinterpret range in *from_t* domain as a range in *to_t* domain preserving
+ * all possible information. Worst case, it will be unknown range within
+ * *to_t* domain, if nothing more specific can be guaranteed during the
+ * conversion
+ */
+static struct range range_cast(enum num_t from_t, enum num_t to_t, struct range from)
+{
+	switch (from_t) {
+	case U64: return range_cast_u64(to_t, from);
+	case U32: return range_cast_u32(to_t, from);
+	case S64: return range_cast_s64(to_t, from);
+	case S32: return range_cast_s32(to_t, from);
+	default: printf("range_cast!\n"); exit(1);
+	}
+}
+
+static bool is_valid_num(enum num_t t, u64 x)
+{
+	switch (t) {
+	case U64: return true;
+	case U32: return upper32(x) == 0;
+	case S64: return true;
+	case S32: return upper32(x) == 0;
+	default: printf("is_valid_num!\n"); exit(1);
+	}
+}
+
+static bool is_valid_range(enum num_t t, struct range x)
+{
+	if (!is_valid_num(t, x.a) || !is_valid_num(t, x.b))
+		return false;
+
+	switch (t) {
+	case U64: return (u64)x.a <= (u64)x.b;
+	case U32: return (u32)x.a <= (u32)x.b;
+	case S64: return (s64)x.a <= (s64)x.b;
+	case S32: return (s32)x.a <= (s32)x.b;
+	default: printf("is_valid_range!\n"); exit(1);
+	}
+}
+
+static struct range range_improve(enum num_t t, struct range old, struct range new)
+{
+	return range(t, max_t(t, old.a, new.a), min_t(t, old.b, new.b));
+}
+
+static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t, struct range y)
+{
+	struct range y_cast;
+
+	y_cast = range_cast(y_t, x_t, y);
+
+	/* the case when new range knowledge, *y*, is a 32-bit subregister
+	 * range, while previous range knowledge, *x*, is a full register
+	 * 64-bit range, needs special treatment to take into account upper 32
+	 * bits of full register range
+	 */
+	if (t_is_32(y_t) && !t_is_32(x_t)) {
+		struct range x_swap;
+
+		/* some combinations of upper 32 bits and sign bit can lead to
+		 * invalid ranges, in such cases it's easier to detect them
+		 * after cast/swap than try to enumerate all the conditions
+		 * under which transformation and knowledge transfer is valid
+		 */
+		x_swap = range(x_t, swap_low32(x.a, y_cast.a), swap_low32(x.b, y_cast.b));
+		if (!is_valid_range(x_t, x_swap))
+			return x;
+		return range_improve(x_t, x, x_swap);
+	}
+
+	/* otherwise, plain range cast and intersection works */
+	return range_improve(x_t, x, y_cast);
+}
+
+/* =======================
+ * GENERIC CONDITIONAL OPS
+ * =======================
+ */
+enum op { OP_LT, OP_LE, OP_GT, OP_GE, OP_EQ, OP_NE };
+#define MIN_OP OP_LT
+#define MAX_OP OP_NE
+
+static enum op complement_op(enum op op)
+{
+	switch (op) {
+	case OP_LT: return OP_GE;
+	case OP_LE: return OP_GT;
+	case OP_GT: return OP_LE;
+	case OP_GE: return OP_LT;
+	case OP_EQ: return OP_NE;
+	case OP_NE: return OP_EQ;
+	default: printf("complement_op!\n"); exit(1);
+	}
+}
+
+static const char *op_str(enum op op)
+{
+	switch (op) {
+	case OP_LT: return "<";
+	case OP_LE: return "<=";
+	case OP_GT: return ">";
+	case OP_GE: return ">=";
+	case OP_EQ: return "==";
+	case OP_NE: return "!=";
+	default: printf("op_str!\n"); exit(1);
+	}
+}
+
+/* Can register with range [x.a, x.b] *EVER* satisfy
+ * OP (<, <=, >, >=, ==, !=) relation to
+ * a regsiter with range [y.a, y.b]
+ * _in *num_t* domain_
+ */
+static bool range_canbe_op(enum num_t t, struct range x, struct range y, enum op op)
+{
+#define range_canbe(T) do {									\
+	switch (op) {										\
+	case OP_LT: return (T)x.a < (T)y.b;							\
+	case OP_LE: return (T)x.a <= (T)y.b;							\
+	case OP_GT: return (T)x.b > (T)y.a;							\
+	case OP_GE: return (T)x.b >= (T)y.a;							\
+	case OP_EQ: return (T)max_t(t, x.a, y.a) <= (T)min_t(t, x.b, y.b);			\
+	case OP_NE: return !((T)x.a == (T)x.b && (T)y.a == (T)y.b && (T)x.a == (T)y.a);		\
+	default: printf("range_canbe op %d\n", op); exit(1);					\
+	}											\
+} while (0)
+
+	switch (t) {
+	case U64: { range_canbe(u64); }
+	case U32: { range_canbe(u32); }
+	case S64: { range_canbe(s64); }
+	case S32: { range_canbe(s32); }
+	default: printf("range_canbe!\n"); exit(1);
+	}
+#undef range_canbe
+}
+
+/* Does register with range [x.a, x.b] *ALWAYS* satisfy
+ * OP (<, <=, >, >=, ==, !=) relation to
+ * a regsiter with range [y.a, y.b]
+ * _in *num_t* domain_
+ */
+static bool range_always_op(enum num_t t, struct range x, struct range y, enum op op)
+{
+	/* always op <=> ! canbe complement(op) */
+	return !range_canbe_op(t, x, y, complement_op(op));
+}
+
+/* Does register with range [x.a, x.b] *NEVER* satisfy
+ * OP (<, <=, >, >=, ==, !=) relation to
+ * a regsiter with range [y.a, y.b]
+ * _in *num_t* domain_
+ */
+static bool range_never_op(enum num_t t, struct range x, struct range y, enum op op)
+{
+	return !range_canbe_op(t, x, y, op);
+}
+
+/* similar to verifier's is_branch_taken():
+ *    1 - always taken;
+ *    0 - never taken,
+ *   -1 - unsure.
+ */
+static int range_branch_taken_op(enum num_t t, struct range x, struct range y, enum op op)
+{
+	if (range_always_op(t, x, y, op))
+		return 1;
+	if (range_never_op(t, x, y, op))
+		return 0;
+	return -1;
+}
+
+/* What would be the new estimates for register x and y ranges assuming truthful
+ * OP comparison between them. I.e., (x OP y == true) => x <- newx, y <- newy.
+ *
+ * We assume "interesting" cases where ranges overlap. Cases where it's
+ * obvious that (x OP y) is either always true or false should be filtered with
+ * range_never and range_always checks.
+ */
+static void range_cond(enum num_t t, struct range x, struct range y,
+		       enum op op, struct range *newx, struct range *newy)
+{
+	if (!range_canbe_op(t, x, y, op)) {
+		/* nothing to adjust, can't happen, return original values */
+		*newx = x;
+		*newy = y;
+		return;
+	}
+	switch (op) {
+	case OP_LT:
+		*newx = range(t, x.a, min_t(t, x.b, y.b - 1));
+		*newy = range(t, max_t(t, x.a + 1, y.a), y.b);
+		break;
+	case OP_LE:
+		*newx = range(t, x.a, min_t(t, x.b, y.b));
+		*newy = range(t, max_t(t, x.a, y.a), y.b);
+		break;
+	case OP_GT:
+		*newx = range(t, max_t(t, x.a, y.a + 1), x.b);
+		*newy = range(t, y.a, min_t(t, x.b - 1, y.b));
+		break;
+	case OP_GE:
+		*newx = range(t, max_t(t, x.a, y.a), x.b);
+		*newy = range(t, y.a, min_t(t, x.b, y.b));
+		break;
+	case OP_EQ:
+		*newx = range(t, max_t(t, x.a, y.a), min_t(t, x.b, y.b));
+		*newy = range(t, max_t(t, x.a, y.a), min_t(t, x.b, y.b));
+		break;
+	case OP_NE:
+		/* generic case, can't derive more information */
+		*newx = range(t, x.a, x.b);
+		*newy = range(t, y.a, y.b);
+		break;
+
+		/* below extended logic is not supported by verifier just yet */
+		if (x.a == x.b && x.a == y.a) {
+			/* X is a constant matching left side of Y */
+			*newx = range(t, x.a, x.b);
+			*newy = range(t, y.a + 1, y.b);
+		} else if (x.a == x.b && x.b == y.b) {
+			/* X is a constant matching rigth side of Y */
+			*newx = range(t, x.a, x.b);
+			*newy = range(t, y.a, y.b - 1);
+		} else if (y.a == y.b && x.a == y.a) {
+			/* Y is a constant matching left side of X */
+			*newx = range(t, x.a + 1, x.b);
+			*newy = range(t, y.a, y.b);
+		} else if (y.a == y.b && x.b == y.b) {
+			/* Y is a constant matching rigth side of X */
+			*newx = range(t, x.a, x.b - 1);
+			*newy = range(t, y.a, y.b);
+		} else {
+			/* generic case, can't derive more information */
+			*newx = range(t, x.a, x.b);
+			*newy = range(t, y.a, y.b);
+		}
+
+		break;
+	default:
+		break;
+	}
+}
+
+/* =======================
+ * REGISTER STATE HANDLING
+ * =======================
+ */
+struct reg_state {
+	struct range r[4]; /* indexed by enum num_t: U64, U32, S64, S32 */
+	bool valid;
+};
+
+static void print_reg_state(struct reg_state *r, const char *sfx)
+{
+	DEFINE_STRBUF(sb, 512);
+	enum num_t t;
+	int cnt = 0;
+
+	if (!r->valid) {
+		printf("<not found>%s", sfx);
+		return;
+	}
+
+	snappendf(sb, "scalar(");
+	for (t = MIN_T; t <= MAX_T; t++) {
+		snappendf(sb, "%s%s=", cnt++ ? "," : "", t_str(t));
+		snprintf_range(t, sb, r->r[t]);
+	}
+	snappendf(sb, ")");
+
+	printf("%s%s", sb->buf, sfx);
+}
+
+static void print_refinement(enum num_t s_t, struct range src,
+			     enum num_t d_t, struct range old, struct range new,
+			     const char *ctx)
+{
+	printf("REFINING (%s) (%s)SRC=", ctx, t_str(s_t));
+	print_range(s_t, src, "");
+	printf(" (%s)DST_OLD=", t_str(d_t));
+	print_range(d_t, old, "");
+	printf(" (%s)DST_NEW=", t_str(d_t));
+	print_range(d_t, new, "\n");
+}
+
+static void reg_state_refine(struct reg_state *r, enum num_t t, struct range x, const char *ctx)
+{
+	enum num_t d_t, s_t;
+	struct range old;
+	bool keep_going = false;
+
+again:
+	/* try to derive new knowledge from just learned range x of type t */
+	for (d_t = MIN_T; d_t <= MAX_T; d_t++) {
+		old = r->r[d_t];
+		r->r[d_t] = range_refine(d_t, r->r[d_t], t, x);
+		if (!range_eq(r->r[d_t], old)) {
+			keep_going = true;
+			if (env.verbosity >= VERBOSE_NORMAL)
+				print_refinement(t, x, d_t, old, r->r[d_t], ctx);
+		}
+	}
+
+	/* now see if we can derive anything new from updated reg_state's ranges */
+	for (s_t = MIN_T; s_t <= MAX_T; s_t++) {
+		for (d_t = MIN_T; d_t <= MAX_T; d_t++) {
+			old = r->r[d_t];
+			r->r[d_t] = range_refine(d_t, r->r[d_t], s_t, r->r[s_t]);
+			if (!range_eq(r->r[d_t], old)) {
+				keep_going = true;
+				if (env.verbosity >= VERBOSE_NORMAL)
+					print_refinement(s_t, r->r[s_t], d_t, old, r->r[d_t], ctx);
+			}
+		}
+	}
+
+	/* keep refining until we converge */
+	if (keep_going) {
+		keep_going = false;
+		goto again;
+	}
+}
+
+static void reg_state_set_const(struct reg_state *rs, enum num_t t, u64 val)
+{
+	enum num_t tt;
+
+	rs->valid = true;
+	for (tt = MIN_T; tt <= MAX_T; tt++)
+		rs->r[tt] = tt == t ? range(t, val, val) : unkn[tt];
+
+	reg_state_refine(rs, t, rs->r[t], "CONST");
+}
+
+static void reg_state_cond(enum num_t t, struct reg_state *x, struct reg_state *y, enum op op,
+			   struct reg_state *newx, struct reg_state *newy, const char *ctx)
+{
+	char buf[32];
+	struct range z1 = x->r[t], z2 = y->r[t];
+
+	range_cond(t, z1, z2, op, &z1, &z2);
+
+	if (newx) {
+		snprintf(buf, sizeof(buf), "%s R1", ctx);
+		if (newx != x)
+			*newx = *x;
+		reg_state_refine(newx, t, z1, buf);
+	}
+
+	if (newy) {
+		snprintf(buf, sizeof(buf), "%s R2", ctx);
+		if (newy != y)
+			*newy = *y;
+		reg_state_refine(newy, t, z2, buf);
+	}
+}
+
+static int reg_state_branch_taken_op(enum num_t t, struct reg_state *x, struct reg_state *y,
+				     enum op op)
+{
+	if (op == OP_EQ || op == OP_NE) {
+		/* OP_EQ and OP_NE are sign-agnostic */
+		enum num_t tu = t_unsigned(t);
+		enum num_t ts = t_signed(t);
+		int br_u, br_s;
+
+		br_u = range_branch_taken_op(tu, x->r[tu], y->r[tu], op);
+		br_s = range_branch_taken_op(ts, x->r[ts], y->r[ts], op);
+
+		if (br_u >= 0 && br_s >= 0 && br_u != br_s)
+			ASSERT_FALSE(true, "branch taken inconsistency!\n");
+		if (br_u >= 0)
+			return br_u;
+		return br_s;
+	}
+	return range_branch_taken_op(t, x->r[t], y->r[t], op);
+}
+
+/* =====================================
+ * BPF PROGS GENERATION AND VERIFICATION
+ * =====================================
+ */
+struct case_spec {
+	/* whether to init full register (r1) or sub-register (w1) */
+	bool init_subregs;
+	/* whether to establish initial value range on full register (r1) or
+	 * sub-register (w1)
+	 */
+	bool setup_subregs;
+	/* whether to establish initial value range using signed or unsigned
+	 * comparisons (i.e., initialize umin/umax or smin/smax directly)
+	 */
+	bool setup_signed;
+	/* whether to perform comparison on full registers or sub-registers */
+	bool compare_subregs;
+	/* whether to perform comparison using signed or unsigned operations */
+	bool compare_signed;
+};
+
+/* Generate test BPF program based on provided test ranges, operation, and
+ * specifications about register bitness and signedness.
+ */
+static int load_range_cmp_prog(struct range x, struct range y, enum op op,
+			       int branch_taken, struct case_spec spec,
+			       char *log_buf, size_t log_sz,
+			       int *false_pos, int *true_pos)
+{
+#define emit(insn) ({							\
+	struct bpf_insn __insns[] = { insn };				\
+	int __i;							\
+	for (__i = 0; __i < ARRAY_SIZE(__insns); __i++)			\
+		insns[cur_pos + __i] = __insns[__i];			\
+	cur_pos += __i;							\
+})
+#define JMP_TO(target) (target - cur_pos - 1)
+	int cur_pos = 0, exit_pos, fd, op_code;
+	struct bpf_insn insns[64];
+	LIBBPF_OPTS(bpf_prog_load_opts, opts,
+		.log_level = 2,
+		.log_buf = log_buf,
+		.log_size = log_sz,
+	);
+
+	/* ; skip exit block below
+	 * goto +2;
+	 */
+	emit(BPF_JMP_A(2));
+	exit_pos = cur_pos;
+	/* ; exit block for all the preparatory conditionals
+	 * out:
+	 * r0 = 0;
+	 * exit;
+	 */
+	emit(BPF_MOV64_IMM(BPF_REG_0, 0));
+	emit(BPF_EXIT_INSN());
+	/*
+	 * ; assign r6/w6 and r7/w7 unpredictable u64/u32 value
+	 * call bpf_get_current_pid_tgid;
+	 * r6 = r0;               | w6 = w0;
+	 * call bpf_get_current_pid_tgid;
+	 * r7 = r0;               | w7 = w0;
+	 */
+	emit(BPF_EMIT_CALL(BPF_FUNC_get_current_pid_tgid));
+	if (spec.init_subregs)
+		emit(BPF_MOV32_REG(BPF_REG_6, BPF_REG_0));
+	else
+		emit(BPF_MOV64_REG(BPF_REG_6, BPF_REG_0));
+	emit(BPF_EMIT_CALL(BPF_FUNC_get_current_pid_tgid));
+	if (spec.init_subregs)
+		emit(BPF_MOV32_REG(BPF_REG_7, BPF_REG_0));
+	else
+		emit(BPF_MOV64_REG(BPF_REG_7, BPF_REG_0));
+	/* ; setup initial r6/w6 possible value range ([x.a, x.b])
+	 * r1 = %[x.a] ll;        | w1 = %[x.a];
+	 * r2 = %[x.b] ll;        | w2 = %[x.b];
+	 * if r6 < r1 goto out;   | if w6 < w1 goto out;
+	 * if r6 > r2 goto out;   | if w6 > w2 goto out;
+	 */
+	if (spec.setup_subregs) {
+		emit(BPF_MOV32_IMM(BPF_REG_1, (s32)x.a));
+		emit(BPF_MOV32_IMM(BPF_REG_2, (s32)x.b));
+		emit(BPF_JMP32_REG(spec.setup_signed ? BPF_JSLT : BPF_JLT,
+				   BPF_REG_6, BPF_REG_1, JMP_TO(exit_pos)));
+		emit(BPF_JMP32_REG(spec.setup_signed ? BPF_JSGT : BPF_JGT,
+				   BPF_REG_6, BPF_REG_2, JMP_TO(exit_pos)));
+	} else {
+		emit(BPF_LD_IMM64(BPF_REG_1, x.a));
+		emit(BPF_LD_IMM64(BPF_REG_2, x.b));
+		emit(BPF_JMP_REG(spec.setup_signed ? BPF_JSLT : BPF_JLT,
+				 BPF_REG_6, BPF_REG_1, JMP_TO(exit_pos)));
+		emit(BPF_JMP_REG(spec.setup_signed ? BPF_JSGT : BPF_JGT,
+				 BPF_REG_6, BPF_REG_2, JMP_TO(exit_pos)));
+	}
+	/* ; setup initial r7/w7 possible value range ([y.a, y.b])
+	 * r1 = %[y.a] ll;        | w1 = %[y.a];
+	 * r2 = %[y.b] ll;        | w2 = %[y.b];
+	 * if r7 < r1 goto out;   | if w7 < w1 goto out;
+	 * if r7 > r2 goto out;   | if w7 > w2 goto out;
+	 */
+	if (spec.setup_subregs) {
+		emit(BPF_MOV32_IMM(BPF_REG_1, (s32)y.a));
+		emit(BPF_MOV32_IMM(BPF_REG_2, (s32)y.b));
+		emit(BPF_JMP32_REG(spec.setup_signed ? BPF_JSLT : BPF_JLT,
+				   BPF_REG_7, BPF_REG_1, JMP_TO(exit_pos)));
+		emit(BPF_JMP32_REG(spec.setup_signed ? BPF_JSGT : BPF_JGT,
+				   BPF_REG_7, BPF_REG_2, JMP_TO(exit_pos)));
+	} else {
+		emit(BPF_LD_IMM64(BPF_REG_1, y.a));
+		emit(BPF_LD_IMM64(BPF_REG_2, y.b));
+		emit(BPF_JMP_REG(spec.setup_signed ? BPF_JSLT : BPF_JLT,
+				 BPF_REG_7, BPF_REG_1, JMP_TO(exit_pos)));
+		emit(BPF_JMP_REG(spec.setup_signed ? BPF_JSGT : BPF_JGT,
+				 BPF_REG_7, BPF_REG_2, JMP_TO(exit_pos)));
+	}
+	/* ; range test instruction
+	 * if r6 <op> r7 goto +3; | if w6 <op> w7 goto +3;
+	 */
+	switch (op) {
+	case OP_LT: op_code = spec.compare_signed ? BPF_JSLT : BPF_JLT; break;
+	case OP_LE: op_code = spec.compare_signed ? BPF_JSLE : BPF_JLE; break;
+	case OP_GT: op_code = spec.compare_signed ? BPF_JSGT : BPF_JGT; break;
+	case OP_GE: op_code = spec.compare_signed ? BPF_JSGE : BPF_JGE; break;
+	case OP_EQ: op_code = BPF_JEQ; break;
+	case OP_NE: op_code = BPF_JNE; break;
+	default:
+		printf("unrecognized op %d\n", op);
+		return -ENOTSUP;
+	}
+	/* ; BEFORE conditiona, r0/w0 = {r6/w6,r7/w7} is to extract verifier state reliably
+	 * ; this is used for debugging, as verifier doesn't always print
+	 * ; registers states as of condition jump instruction (e.g., when
+	 * ; precision marking happens)
+	 * r0 = r6;               | w0 = w6;
+	 * r0 = r7;               | w0 = w7;
+	 */
+	if (spec.compare_subregs) {
+		emit(BPF_MOV32_REG(BPF_REG_0, BPF_REG_6));
+		emit(BPF_MOV32_REG(BPF_REG_0, BPF_REG_7));
+	} else {
+		emit(BPF_MOV64_REG(BPF_REG_0, BPF_REG_6));
+		emit(BPF_MOV64_REG(BPF_REG_0, BPF_REG_7));
+	}
+	if (spec.compare_subregs)
+		emit(BPF_JMP32_REG(op_code, BPF_REG_6, BPF_REG_7, 3));
+	else
+		emit(BPF_JMP_REG(op_code, BPF_REG_6, BPF_REG_7, 3));
+	/* ; FALSE branch, r0/w0 = {r6/w6,r7/w7} is to extract verifier state reliably
+	 * r0 = r6;               | w0 = w6;
+	 * r0 = r7;               | w0 = w7;
+	 * exit;
+	 */
+	*false_pos = cur_pos;
+	if (spec.compare_subregs) {
+		emit(BPF_MOV32_REG(BPF_REG_0, BPF_REG_6));
+		emit(BPF_MOV32_REG(BPF_REG_0, BPF_REG_7));
+	} else {
+		emit(BPF_MOV64_REG(BPF_REG_0, BPF_REG_6));
+		emit(BPF_MOV64_REG(BPF_REG_0, BPF_REG_7));
+	}
+	if (branch_taken == 1) /* false branch is never taken */
+		emit(BPF_EMIT_CALL(0xDEAD)); /* poison this branch */
+	else
+		emit(BPF_EXIT_INSN());
+	/* ; TRUE branch, r0/w0 = {r6/w6,r7/w7} is to extract verifier state reliably
+	 * r0 = r6;               | w0 = w6;
+	 * r0 = r7;               | w0 = w7;
+	 * exit;
+	 */
+	*true_pos = cur_pos;
+	if (spec.compare_subregs) {
+		emit(BPF_MOV32_REG(BPF_REG_0, BPF_REG_6));
+		emit(BPF_MOV32_REG(BPF_REG_0, BPF_REG_7));
+	} else {
+		emit(BPF_MOV64_REG(BPF_REG_0, BPF_REG_6));
+		emit(BPF_MOV64_REG(BPF_REG_0, BPF_REG_7));
+	}
+	if (branch_taken == 0) /* true branch is never taken */
+		emit(BPF_EMIT_CALL(0xDEAD)); /* poison this branch */
+	emit(BPF_EXIT_INSN()); /* last instruction has to be exit */
+
+	fd = bpf_prog_load(BPF_PROG_TYPE_RAW_TRACEPOINT, "reg_bounds_test",
+			   "GPL", insns, cur_pos, &opts);
+	if (fd < 0)
+		return fd;
+
+	close(fd);
+	return 0;
+#undef emit
+#undef JMP_TO
+}
+
+#define str_has_pfx(str, pfx) \
+	(strncmp(str, pfx, __builtin_constant_p(pfx) ? sizeof(pfx) - 1 : strlen(pfx)) == 0)
+
+/* Parse register state from verifier log.
+ * `s` should point to the start of "Rx = ..." substring in the verifier log.
+ */
+static int parse_reg_state(const char *s, struct reg_state *reg)
+{
+	/* There are two generic forms for SCALAR register:
+	 * - known constant: R6_rwD=P%lld
+	 * - range: R6_rwD=scalar(id=1,...), where "..." is a comma-separated
+	 *   list of optional range specifiers:
+	 *     - umin=%llu, if missing, assumed 0;
+	 *     - umax=%llu, if missing, assumed U64_MAX;
+	 *     - smin=%lld, if missing, assumed S64_MIN;
+	 *     - smax=%lld, if missing, assummed S64_MAX;
+	 *     - umin32=%d, if missing, assumed 0;
+	 *     - umax32=%d, if missing, assumed U32_MAX;
+	 *     - smin32=%d, if missing, assumed S32_MIN;
+	 *     - smax32=%d, if missing, assummed S32_MAX;
+	 *     - var_off=(%#llx; %#llx), tnum part, we don't care about it.
+	 *
+	 * If some of the values are equal, they will be grouped (but min/max
+	 * are not mixed together, and similarly negative values are not
+	 * grouped with non-negative ones). E.g.:
+	 *
+	 *   R6_w=Pscalar(smin=smin32=0, smax=umax=umax32=1000)
+	 *
+	 * _rwD part is optional (and any of the letters can be missing).
+	 * P (precision mark) is optional as well.
+	 *
+	 * Anything inside scalar() is optional, including id, of course.
+	 */
+	struct {
+		const char *pfx;
+		const char *fmt;
+		u64 *dst, def;
+		bool is_32, is_set;
+	} *f, fields[8] = {
+		{"smin=", "%lld", &reg->r[S64].a, S64_MIN},
+		{"smax=", "%lld", &reg->r[S64].b, S64_MAX},
+		{"umin=", "%llu", &reg->r[U64].a, 0},
+		{"umax=", "%llu", &reg->r[U64].b, U64_MAX},
+		{"smin32=", "%d", &reg->r[S32].a, (u32)S32_MIN, true},
+		{"smax32=", "%d", &reg->r[S32].b, (u32)S32_MAX, true},
+		{"umin32=", "%u", &reg->r[U32].a, 0,            true},
+		{"umax32=", "%u", &reg->r[U32].b, U32_MAX,      true},
+	};
+	const char *p, *fmt;
+	int i;
+
+	p = strchr(s, '=');
+	if (!p)
+		return -EINVAL;
+	p++;
+	if (*p == 'P')
+		p++;
+
+	if (!str_has_pfx(p, "scalar(")) {
+		long long sval;
+		enum num_t t;
+
+		if (sscanf(p, "%lld", &sval) != 1)
+			return -EINVAL;
+
+		reg->valid = true;
+		for (t = MIN_T; t <= MAX_T; t++) {
+			reg->r[t] = range(t, sval, sval);
+		}
+		return 0;
+	}
+
+	p += sizeof("scalar");
+	while (p) {
+		int midxs[ARRAY_SIZE(fields)], mcnt = 0;
+		u64 val;
+
+		for (i = 0; i < ARRAY_SIZE(fields); i++) {
+			f = &fields[i];
+			if (!str_has_pfx(p, f->pfx))
+				continue;
+			midxs[mcnt++] = i;
+			p += strlen(f->pfx);
+		}
+
+		if (mcnt) {
+			/* populate all matched fields */
+			fmt = fields[midxs[0]].fmt;
+			if (sscanf(p, fmt, &val) != 1)
+				return -EINVAL;
+
+			for (i = 0; i < mcnt; i++) {
+				f = &fields[midxs[i]];
+				f->is_set = true;
+				*f->dst = f->is_32 ? (u64)(u32)val : val;
+			}
+		} else if (str_has_pfx(p, "var_off")) {
+			/* skip "var_off=(0x0; 0x3f)" part completely */
+			p = strchr(p, ')');
+			if (!p)
+				return -EINVAL;
+			p++;
+		}
+
+		p = strpbrk(p, ",)");
+		if (*p == ')')
+			break;
+		if (p)
+			p++;
+	}
+
+	reg->valid = true;
+
+	for (i = 0; i < ARRAY_SIZE(fields); i++) {
+		f = &fields[i];
+		if (!f->is_set)
+			*f->dst = f->def;
+	}
+
+	return 0;
+}
+
+
+/* Parse all register states (TRUE/FALSE branches and DST/SRC registers)
+ * out of the verifier log for a corresponding test case BPF program.
+ */
+static int parse_range_cmp_log(const char *log_buf, struct case_spec spec,
+			       int false_pos, int true_pos,
+			       struct reg_state *false1_reg, struct reg_state *false2_reg,
+			       struct reg_state *true1_reg, struct reg_state *true2_reg)
+{
+	struct {
+		int insn_idx;
+		int reg_idx;
+		const char *reg_upper;
+		struct reg_state *state;
+	} specs[] = {
+		{false_pos,     6, "R6=", false1_reg},
+		{false_pos + 1, 7, "R7=", false2_reg},
+		{true_pos,      6, "R6=", true1_reg},
+		{true_pos + 1,  7, "R7=", true2_reg},
+	};
+	char buf[32];
+	const char *p = log_buf, *q;
+	int i, err;
+
+	for (i = 0; i < 4; i++) {
+		sprintf(buf, "%d: (%s) %s = %s%d", specs[i].insn_idx,
+			spec.compare_subregs ? "bc" : "bf",
+			spec.compare_subregs ? "w0" : "r0",
+			spec.compare_subregs ? "w" : "r", specs[i].reg_idx);
+
+		q = strstr(p, buf);
+		if (!q) {
+			*specs[i].state = (struct reg_state){.valid = false};
+			continue;
+		}
+		p = strstr(q, specs[i].reg_upper);
+		if (!p)
+			return -EINVAL;
+		err = parse_reg_state(p, specs[i].state);
+		if (err)
+			return -EINVAL;
+	}
+	return 0;
+}
+
+/* Validate ranges match, and print details if they don't */
+static bool assert_range_eq(enum num_t t, struct range x, struct range y,
+			    const char *ctx1, const char *ctx2)
+{
+	DEFINE_STRBUF(sb, 512);
+
+	if (range_eq(x, y))
+		return true;
+
+	snappendf(sb, "MISMATCH %s.%s: ", ctx1, ctx2);
+	snprintf_range(t, sb, x);
+	snappendf(sb, " != ");
+	snprintf_range(t, sb, y);
+
+	printf("%s\n", sb->buf);
+
+	return false;
+}
+
+/* Validate that register states match, and print details if they don't */
+static bool assert_reg_state_eq(struct reg_state *r, struct reg_state *e, const char *ctx)
+{
+	bool ok = true;
+	enum num_t t;
+
+	if (r->valid != e->valid) {
+		printf("MISMATCH %s: actual %s != expected %s\n", ctx,
+		       r->valid ? "<valid>" : "<invalid>",
+		       e->valid ? "<valid>" : "<invalid>");
+		return false;
+	}
+
+	if (!r->valid)
+		return true;
+
+	for (t = MIN_T; t <= MAX_T; t++) {
+		if (!assert_range_eq(t, r->r[t], e->r[t], ctx, t_str(t)))
+			ok = false;
+	}
+
+	return ok;
+}
+
+/* Printf verifier log, filtering out irrelevant noise */
+static void print_verifier_log(const char *buf)
+{
+	const char *p;
+
+	while (buf[0]) {
+		p = strchrnul(buf, '\n');
+
+		/* filter out irrelevant precision backtracking logs */
+		if (str_has_pfx(buf, "mark_precise: "))
+			goto skip_line;
+
+		printf("%.*s\n", (int)(p - buf), buf);
+
+skip_line:
+		buf = *p == '\0' ? p : p + 1;
+	}
+}
+
+/* Simulate provided test case purely with our own range-based logic.
+ * This is done to set up expectations for verifier's branch_taken logic and
+ * verifier's register states in the verifier log.
+ */
+static void sim_case(enum num_t init_t, enum num_t cond_t,
+		     struct range x, struct range y, enum op op,
+		     struct reg_state *fr1, struct reg_state *fr2,
+		     struct reg_state *tr1, struct reg_state *tr2,
+		     int *branch_taken)
+{
+	const u64 A = x.a;
+	const u64 B = x.b;
+	const u64 C = y.a;
+	const u64 D = y.b;
+	struct reg_state rc;
+	enum op rev_op = complement_op(op);
+	enum num_t t;
+
+	fr1->valid = fr2->valid = true;
+	tr1->valid = tr2->valid = true;
+	for (t = MIN_T; t <= MAX_T; t++) {
+		/* if we are initializing using 32-bit subregisters,
+		 * full registers get upper 32 bits zeroed automatically
+		 */
+		struct range z = t_is_32(init_t) ? unkn_subreg(t) : unkn[t];
+
+		fr1->r[t] = fr2->r[t] = tr1->r[t] = tr2->r[t] = z;
+	}
+
+	/* step 1: r1 >= A, r2 >= C */
+	reg_state_set_const(&rc, init_t, A);
+	reg_state_cond(init_t, fr1, &rc, OP_GE, fr1, NULL, "r1>=A");
+	reg_state_set_const(&rc, init_t, C);
+	reg_state_cond(init_t, fr2, &rc, OP_GE, fr2, NULL, "r2>=C");
+	*tr1 = *fr1;
+	*tr2 = *fr2;
+	printf("STEP1 (%s) R1: ", t_str(init_t)); print_reg_state(fr1, "\n");
+	printf("STEP1 (%s) R2: ", t_str(init_t)); print_reg_state(fr2, "\n");
+
+	/* step 2: r1 <= B, r2 <= D */
+	reg_state_set_const(&rc, init_t, B);
+	reg_state_cond(init_t, fr1, &rc, OP_LE, fr1, NULL, "r1<=B");
+	reg_state_set_const(&rc, init_t, D);
+	reg_state_cond(init_t, fr2, &rc, OP_LE, fr2, NULL, "r2<=D");
+	*tr1 = *fr1;
+	*tr2 = *fr2;
+	printf("STEP2 (%s) R1: ", t_str(init_t)); print_reg_state(fr1, "\n");
+	printf("STEP2 (%s) R2: ", t_str(init_t)); print_reg_state(fr2, "\n");
+
+	/* step 3: r1 <op> r2 */
+	*branch_taken = reg_state_branch_taken_op(cond_t, fr1, fr2, op);
+	fr1->valid = fr2->valid = false;
+	tr1->valid = tr2->valid = false;
+	if (*branch_taken != 1) { /* FALSE is possible */
+		fr1->valid = fr2->valid = true;
+		reg_state_cond(cond_t, fr1, fr2, rev_op, fr1, fr2, "FALSE");
+	}
+	if (*branch_taken != 0) { /* TRUE is possible */
+		tr1->valid = tr2->valid = true;
+		reg_state_cond(cond_t, tr1, tr2, op, tr1, tr2, "TRUE");
+	}
+	printf("STEP3 (%s) FALSE R1:", t_str(cond_t)); print_reg_state(fr1, "\n");
+	printf("STEP3 (%s) FALSE R2:", t_str(cond_t)); print_reg_state(fr2, "\n");
+	printf("STEP3 (%s) TRUE  R1:", t_str(cond_t)); print_reg_state(tr1, "\n");
+	printf("STEP3 (%s) TRUE  R2:", t_str(cond_t)); print_reg_state(tr2, "\n");
+}
+
+/* ===============================
+ * HIGH-LEVEL TEST CASE VALIDATION
+ * ===============================
+ */
+struct subtest_case {
+	enum num_t init_t;
+	enum num_t cond_t;
+	struct range x;
+	struct range y;
+	enum op op;
+};
+
+static void subtest_case_str(struct strbuf *sb, struct subtest_case *t)
+{
+	snappendf(sb, "(%s)", t_str(t->init_t));
+	snprintf_range(t->init_t, sb, t->x);
+	snappendf(sb, " (%s)%s ", t_str(t->cond_t), op_str(t->op));
+	snprintf_range(t->cond_t, sb, t->y);
+}
+
+/* Generate and validate test case based on specific combination of setup
+ * register ranges (including their expected num_t domain), and conditional
+ * operation to perform (including num_t domain in which it has to be
+ * performed)
+ */
+static int verify_case_op(enum num_t init_t, enum num_t cond_t,
+			  struct range x, struct range y, enum op op)
+{
+	char log_buf[256 * 1024];
+	size_t log_sz = sizeof(log_buf);
+	int err, false_pos = 0, true_pos = 0, branch_taken;
+	struct reg_state fr1, fr2, tr1, tr2;
+	struct reg_state fe1, fe2, te1, te2;
+	bool failed = false;
+	struct case_spec spec = {
+		.init_subregs = (init_t == U32 || init_t == S32),
+		.setup_subregs = (init_t == U32 || init_t == S32),
+		.setup_signed = (init_t == S64 || init_t == S32),
+		.compare_subregs = (cond_t == U32 || cond_t == S32),
+		.compare_signed = (cond_t == S64 || cond_t == S32),
+	};
+
+	log_buf[0] = '\0';
+
+	sim_case(init_t, cond_t, x, y, op, &fe1, &fe2, &te1, &te2, &branch_taken);
+
+	err = load_range_cmp_prog(x, y, op, branch_taken, spec,
+				  log_buf, log_sz, &false_pos, &true_pos);
+	if (err) {
+		ASSERT_OK(err, "load_range_cmp_prog");
+		failed = true;
+	}
+
+	err = parse_range_cmp_log(log_buf, spec, false_pos, true_pos,
+				  &fr1, &fr2, &tr1, &tr2);
+	if (err) {
+		ASSERT_OK(err, "parse_range_cmp_log");
+		failed = true;
+	}
+
+	if (!assert_reg_state_eq(&fr1, &fe1, "false_reg1") ||
+	    !assert_reg_state_eq(&fr2, &fe2, "false_reg2") ||
+	    !assert_reg_state_eq(&tr1, &te1, "true_reg1") ||
+	    !assert_reg_state_eq(&tr2, &te2, "true_reg2")) {
+		failed = true;
+	}
+
+	if (failed || env.verbosity >= VERBOSE_NORMAL) {
+		if (env.verbosity >= VERBOSE_VERY) {
+			printf("VERIFIER LOG:\n========================\n");
+			print_verifier_log(log_buf);
+			printf("=====================\n");
+		}
+		printf("ACTUAL   FALSE1: "); print_reg_state(&fr1, "\n");
+		printf("EXPECTED FALSE1: "); print_reg_state(&fe1, "\n");
+		printf("ACTUAL   FALSE2: "); print_reg_state(&fr2, "\n");
+		printf("EXPECTED FALSE2: "); print_reg_state(&fe2, "\n");
+		printf("ACTUAL   TRUE1:  "); print_reg_state(&tr1, "\n");
+		printf("EXPECTED TRUE1:  "); print_reg_state(&te1, "\n");
+		printf("ACTUAL   TRUE2:  "); print_reg_state(&tr2, "\n");
+		printf("EXPECTED TRUE2:  "); print_reg_state(&te2, "\n");
+
+		return failed ? -EINVAL : 0;
+	}
+
+	return 0;
+}
+
+static int max_failure_cnt = 0, cur_failure_cnt = 0;
+
+/* Given setup ranges and number types, go over all supported operations,
+ * generating individual subtest for each allowed combination
+ */
+static int verify_case(enum num_t init_t, enum num_t cond_t, struct range x, struct range y)
+{
+	DEFINE_STRBUF(sb, 256);
+	int err;
+	struct subtest_case sub = {
+		.init_t = init_t,
+		.cond_t = cond_t,
+		.x = x,
+		.y = y,
+	};
+
+	for (sub.op = MIN_OP; sub.op <= MAX_OP; sub.op++) {
+		sb->pos = 0; /* reset position in strbuf */
+		subtest_case_str(sb, &sub);
+		if (!test__start_subtest(sb->buf))
+			continue;
+
+		if (env.verbosity >= VERBOSE_NORMAL) /* this speeds up debugging */
+			printf("TEST CASE: %s\n", sb->buf);
+
+		err = verify_case_op(init_t, cond_t, x, y, sub.op);
+		if (err || env.verbosity >= VERBOSE_NORMAL)
+			ASSERT_OK(err, sb->buf);
+		if (err) {
+			cur_failure_cnt++;
+			if (cur_failure_cnt > max_failure_cnt)
+				return err;
+			return 0; /* keep testing other cases */
+		}
+	}
+
+	return 0;
+}
+
+/* ================================
+ * GENERATED CASES FROM SEED VALUES
+ * ================================
+ */
+static u32 upper_seeds[] = {
+	0,
+	1,
+	U32_MAX,
+	U32_MAX - 1,
+	S32_MAX,
+	(u32)S32_MIN,
+};
+
+static u32 lower_seeds[] = {
+	0,
+	1,
+	2, (u32)-2,
+	255, (u32)-255,
+	UINT_MAX,
+	UINT_MAX - 1,
+	INT_MAX,
+	(u32)INT_MIN,
+};
+
+static int val_cnt, range_cnt;
+static u64 uvals[ARRAY_SIZE(upper_seeds) * ARRAY_SIZE(lower_seeds)];
+static s64 svals[ARRAY_SIZE(upper_seeds) * ARRAY_SIZE(lower_seeds)];
+static struct range *uranges, *sranges;
+
+static int u64_cmp(const void *p1, const void *p2)
+{
+	u64 x1 = *(const u64 *)p1, x2 = *(const u64 *)p2;
+
+	return x1 != x2 ? (x1 < x2 ? -1 : 1) : 0;
+}
+
+static int s64_cmp(const void *p1, const void *p2)
+{
+	s64 x1 = *(const s64 *)p1, x2 = *(const s64 *)p2;
+
+	return x1 != x2 ? (x1 < x2 ? -1 : 1) : 0;
+}
+
+/* Generate valid unique constants from seeds, both signed and unsigned */
+static void gen_vals(void)
+{
+	int i, j, cnt = 0;
+
+	for (i = 0; i < ARRAY_SIZE(upper_seeds); i++) {
+		for (j = 0; j < ARRAY_SIZE(lower_seeds); j++) {
+			uvals[cnt++] = (((u64)upper_seeds[i]) << 32) | lower_seeds[j];
+		}
+	}
+
+	/* sort and compact uvals (i.e., it's `sort | uniq`) */
+	qsort(uvals, cnt, sizeof(*uvals), u64_cmp);
+	for (i = 1, j = 0; i < cnt; i++)
+	{
+		if (uvals[j] == uvals[i])
+			continue;
+		j++;
+		uvals[j] = uvals[i];
+	}
+	val_cnt = j + 1;
+
+	/* we have exactly the same number of s64 values, they are just in
+	 * a different order than u64s, so just sort them differently
+	 */
+	for (i = 0; i < val_cnt; i++)
+		svals[i] = uvals[i];
+	qsort(svals, cnt, sizeof(*svals), s64_cmp);
+
+	if (env.verbosity >= VERBOSE_SUPER) {
+		DEFINE_STRBUF(sb1, 256);
+		DEFINE_STRBUF(sb2, 256);
+
+		for (i = 0; i < val_cnt; i++) {
+			snprintf_num(U64, sb1, uvals[i]);
+			snprintf_num(S64, sb2, svals[i]);
+			printf("SEED #%d: u64=%-20s s64=%-20s\n", i, sb1->buf, sb2->buf);
+		}
+	}
+}
+
+/* Generate valid ranges from upper/lower seeds */
+static int gen_ranges(void)
+{
+	int i, j, cnt = 0;
+
+	for (i = 0; i < val_cnt; i++) {
+		for (j = i; j < val_cnt; j++) {
+			if (env.verbosity >= VERBOSE_SUPER) {
+				DEFINE_STRBUF(sb1, 256);
+				DEFINE_STRBUF(sb2, 256);
+
+				snprintf_range(U64, sb1, range(U64, uvals[i], uvals[j]));
+				snprintf_range(S64, sb2, range(S64, svals[i], svals[j]));
+				printf("RANGE #%d: u64=%-40s s64=%-40s\n", i, sb1->buf, sb2->buf);
+			}
+			cnt++;
+		}
+	}
+
+	uranges = calloc(cnt, sizeof(*uranges));
+	if (!ASSERT_OK_PTR(uranges, "uranges_calloc"))
+		return -EINVAL;
+	sranges = calloc(cnt, sizeof(*sranges));
+	if (!ASSERT_OK_PTR(sranges, "sranges_calloc"))
+		return -EINVAL;
+
+	for (i = 0; i < val_cnt; i++) {
+		for (j = i; j < val_cnt; j++) {
+			uranges[range_cnt].a = uvals[i];
+			uranges[range_cnt].b = uvals[j];
+
+			sranges[range_cnt].a = (u64)svals[i];
+			sranges[range_cnt].b = (u64)svals[j];
+
+			range_cnt++;
+		}
+	}
+
+	return 0;
+}
+
+static struct subtest_case known_cases[] = {
+};
+
+static bool is_known_case(enum num_t init_t, enum num_t cond_t, struct range x, struct range y)
+{
+	int i;
+
+	for (i = 0; i < ARRAY_SIZE(known_cases); i++) {
+		struct subtest_case *c = &known_cases[i];
+
+		if (c->init_t == init_t && c->cond_t == cond_t &&
+		    range_eq(c->x, x) && range_eq(c->y, y))
+			return true;
+	}
+
+	return false;
+}
+
+static bool allow_mixed_bitness = false;
+static bool allow_type_casts = false;
+
+/* Go over generated constants and ranges and validate various supported
+ * combinations of them
+ */
+static void validate_gen_ranges_vs_consts(void)
+{
+	struct range uconst, sconst;
+	enum num_t cond_t;
+	int i, j;
+
+	for (i = 0; i < val_cnt; i++)
+	for (j = 0; j < range_cnt; j++)
+	for (cond_t = MIN_T; cond_t <= MAX_T; cond_t++) {
+		uconst = range(U64, uvals[i], uvals[i]);
+		if (is_known_case(U64, cond_t, uranges[j], uconst))
+			goto skip_unsigned;
+
+		if ((cond_t == U64 || allow_type_casts) &&
+		    (!t_is_32(cond_t) || allow_mixed_bitness)) {
+			/* (u64)(<range> x <const>) */
+			if (verify_case(U64, cond_t, uranges[j], uconst))
+				return;
+			/* (u64)(<const> x <range>) */
+			if (verify_case(U64, cond_t, uconst, uranges[j]))
+				return;
+		}
+
+		if ((cond_t == U32 || allow_type_casts) &&
+		    (t_is_32(cond_t) || allow_mixed_bitness) &&
+		    is_valid_range(U32, uranges[j]) &&
+		    is_valid_range(U32, uconst)) {
+			/* (u32)(<range> x <const>) */
+			if (verify_case(U32, cond_t, uranges[j], uconst))
+				return;
+			/* (u32)(<const> x <range>) */
+			if (verify_case(U32, cond_t, uconst, uranges[j]))
+				return;
+		}
+
+skip_unsigned:
+		sconst = range(S64, svals[i], svals[i]);
+		if (is_known_case(S64, cond_t, sranges[j], sconst))
+			continue;
+
+		if ((cond_t == S64 || allow_type_casts) &&
+		    (!t_is_32(cond_t) || allow_mixed_bitness)) {
+			/* (s64)(<range> x <const>) */
+			if (verify_case(S64, cond_t, sranges[j], sconst))
+				return;
+			/* (s64)(<const> x <range>) */
+			if (verify_case(S64, cond_t, sconst, sranges[j]))
+				return;
+		}
+
+		if ((cond_t == S32 || allow_type_casts) &&
+		    (t_is_32(cond_t) || allow_mixed_bitness) &&
+		    is_valid_range(S32, sranges[j]) &&
+		    is_valid_range(S32, sconst)) {
+			/* (s32)(<range> x <const>) */
+			if (verify_case(S32, cond_t, sranges[j], sconst))
+				return;
+			/* (s32)(<const> x <range>) */
+			if (verify_case(S32, cond_t, sconst, sranges[j]))
+				return;
+		}
+	}
+}
+
+/* Go over thousands of test cases generated from initial seed values.
+ * Given this take a long time, guard this begind SLOW_TESTS=1 envvar. If
+ * envvar is not set, this test is skipped during test_progs testing.
+ */
+void test_reg_bounds_gen(void)
+{
+	const char *s;
+
+	if (!(s = getenv("SLOW_TESTS")) || strcmp(s, "1") != 0) {
+		test__skip();
+		return;
+	}
+
+	if ((s = getenv("REG_BOUNDS_ALLOW_TYPE_CASTS")) && strcmp(s, "1") == 0)
+		allow_type_casts = true;
+	if ((s = getenv("REG_BOUNDS_ALLOW_MIXED_BITNESS")) && strcmp(s, "1") == 0)
+		allow_mixed_bitness = true;
+	if ((s = getenv("REG_BOUNDS_MAX_FAILURE_CNT"))) {
+		errno = 0;
+		max_failure_cnt = strtol(s, NULL, 10);
+		if (errno || max_failure_cnt < 0) {
+			ASSERT_OK(-errno, "REG_BOUNDS_MAX_FAILURE_CNT");
+			return;
+		}
+	}
+
+	gen_vals();
+	if (!ASSERT_OK(gen_ranges(), "gen_ranges"))
+		return;
+
+	validate_gen_ranges_vs_consts();
+}
+
+/* A set of hard-coded "interesting" cases to validate as part of normal
+ * test_progs test runs
+ */
+static struct subtest_case crafted_cases[] = {
+	{U64, U64, {0, 0xffffffff}, {0, 0}},
+	{U64, U64, {0, 0x80000000}, {0, 0}},
+	{U64, U64, {0x100000000ULL, 0x100000100ULL}, {0, 0}},
+	{U64, U64, {0x100000000ULL, 0x180000000ULL}, {0, 0}},
+	{U64, U64, {0x100000000ULL, 0x1ffffff00ULL}, {0, 0}},
+	{U64, U64, {0x100000000ULL, 0x1ffffff01ULL}, {0, 0}},
+	{U64, U64, {0x100000000ULL, 0x1fffffffeULL}, {0, 0}},
+	{U64, U64, {0x100000001ULL, 0x1000000ffULL}, {0, 0}},
+
+	{U64, S64, {0, 0xffffffff00000000ULL}, {0, 0}},
+	{U64, S64, {0x7fffffffffffffffULL, 0xffffffff00000000ULL}, {0, 0}},
+	{U64, S64, {0x7fffffff00000001ULL, 0xffffffff00000000ULL}, {0, 0}},
+	{U64, S64, {0, 0xffffffffULL}, {1, 1}},
+	{U64, S64, {0, 0xffffffffULL}, {0x7fffffff, 0x7fffffff}},
+
+	{U64, U32, {0xfffffffe, 0x100000000}, {0x80000000, 0x80000000}},
+
+	{U64, S32, {0, 0xffffffff00000000ULL}, {0, 0}},
+	/* these are tricky cases where lower 32 bits allow to tighten 64
+	 * bit boundaries based on tightened lower 32 bit boundaries
+	 */
+	{U64, S32, {0, 0x0ffffffffULL}, {0, 0}},
+	{U64, S32, {0, 0x100000000ULL}, {0, 0}},
+	{U64, S32, {0, 0x100000001ULL}, {0, 0}},
+	{U64, S32, {0, 0x180000000ULL}, {0, 0}},
+	{U64, S32, {0, 0x17fffffffULL}, {0, 0}},
+	{U64, S32, {0, 0x180000001ULL}, {0, 0}},
+
+	/* verifier knows about [-1, 0] range for s32 for this case already */
+	{S64, S64, {0xffffffffffffffffULL, 0}, {0xffffffff00000000ULL, 0xffffffff00000000ULL}},
+	/* but didn't know about these cases initially */
+	{U64, U64, {0xffffffff, 0x100000000ULL}, {0, 0}}, /* s32: [-1, 0] */
+	{U64, U64, {0xffffffff, 0x100000001ULL}, {0, 0}}, /* s32: [-1, 1] */
+
+	/* longer convergence case: learning from u64 -> s64 -> u64 -> u32,
+	 * arriving at u32: [1, U32_MAX] (instead of more pessimistic [0, U32_MAX])
+	 */
+	{S64, U64, {0xffffffff00000001ULL, 0}, {0xffffffff00000000ULL, 0xffffffff00000000ULL}},
+
+	{U32, U32, {1, U32_MAX}, {0, 0}},
+
+	{U32, S32, {0, U32_MAX}, {U32_MAX, U32_MAX}},
+};
+
+/* Go over crafted hard-coded cases. This is fast, so we do it as part of
+ * normal test_progs run.
+ */
+void test_reg_bounds_crafted(void)
+{
+	int i;
+
+	for (i = 0; i < ARRAY_SIZE(crafted_cases); i++) {
+		struct subtest_case *c = &crafted_cases[i];
+
+		verify_case(c->init_t, c->cond_t, c->x, c->y);
+	}
+}
-- 
2.34.1

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[kernel test robot]

Hi Andrii,

kernel test robot noticed the following build warnings:

[auto build test WARNING on bpf-next/master]

url:    https://github.com/intel-lab-lkp/linux/commits/Andrii-Nakryiko/bpf-improve-JEQ-JNE-branch-taken-logic/20231019-122550
base:   https://git.kernel.org/pub/scm/linux/kernel/git/bpf/bpf-next.git master
patch link:    https://lore.kernel.org/r/20231019042405.2971130-8-andrii%40kernel.org
patch subject: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester
reproduce: (https://download.01.org/0day-ci/archive/20231019/202310191409.pIIb2buD-lkp@intel.com/reproduce)

If you fix the issue in a separate patch/commit (i.e. not just a new version of
the same patch/commit), kindly add following tags
| Reported-by: kernel test robot <lkp@intel.com>
| Closes: https://lore.kernel.org/oe-kbuild-all/202310191409.pIIb2buD-lkp@intel.com/

# many are suggestions rather than must-fix

WARNING:NEW_TYPEDEFS: do not add new typedefs
#169: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:21:
+typedef unsigned long long ___u64;

WARNING:NEW_TYPEDEFS: do not add new typedefs
#170: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:22:
+typedef unsigned int ___u32;

WARNING:NEW_TYPEDEFS: do not add new typedefs
#171: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:23:
+typedef long long ___s64;

WARNING:NEW_TYPEDEFS: do not add new typedefs
#172: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:24:
+typedef int ___s32;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#215: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:67:
+	case U64: return (u64)x < (u64)y ? (u64)x : (u64)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#216: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:68:
+	case U32: return (u32)x < (u32)y ? (u32)x : (u32)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#217: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:69:
+	case S64: return (s64)x < (s64)y ? (s64)x : (s64)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#218: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:70:
+	case S32: return (s32)x < (s32)y ? (s32)x : (s32)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#219: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:71:
+	default: printf("min_t!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'min_t', this function's name, in a string
#219: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:71:
+	default: printf("min_t!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#226: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:78:
+	case U64: return (u64)x > (u64)y ? (u64)x : (u64)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#227: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:79:
+	case U32: return (u32)x > (u32)y ? (u32)x : (u32)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#228: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:80:
+	case S64: return (s64)x > (s64)y ? (s64)x : (s64)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#229: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:81:
+	case S32: return (s32)x > (s32)y ? (u32)(s32)x : (u32)(s32)y;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#230: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:82:
+	default: printf("max_t!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'max_t', this function's name, in a string
#230: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:82:
+	default: printf("max_t!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#241: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:93:
+	default: printf("t_str!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_str', this function's name, in a string
#241: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:93:
+	default: printf("t_str!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#252: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:104:
+	default: printf("t_is_32!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_is_32', this function's name, in a string
#252: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:104:
+	default: printf("t_is_32!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#263: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:115:
+	default: printf("t_signed!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_signed', this function's name, in a string
#263: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:115:
+	default: printf("t_signed!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#274: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:126:
+	default: printf("t_unsigned!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_unsigned', this function's name, in a string
#274: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:126:
+	default: printf("t_unsigned!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#285: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:137:
+	default: printf("num_is_small!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'num_is_small', this function's name, in a string
#285: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:137:
+	default: printf("num_is_small!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#299: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:151:
+		default: printf("snprintf_num!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'snprintf_num', this function's name, in a string
#299: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:151:
+		default: printf("snprintf_num!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#339: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:191:
+		default: printf("snprintf_num!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'snprintf_num', this function's name, in a string
#339: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:191:
+		default: printf("snprintf_num!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#386: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:238:
+	default: printf("unkn_subreg!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'unkn_subreg', this function's name, in a string
#386: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:238:
+	default: printf("unkn_subreg!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#397: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:249:
+	default: printf("range!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range', this function's name, in a string
#397: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:249:
+	default: printf("range!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#454: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:306:
+	default: printf("range_cast_u64!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_u64', this function's name, in a string
#454: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:306:
+	default: printf("range_cast_u64!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#476: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:328:
+	default: printf("range_cast_s64!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_s64', this function's name, in a string
#476: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:328:
+	default: printf("range_cast_s64!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#493: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:345:
+	default: printf("range_cast_u32!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_u32', this function's name, in a string
#493: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:345:
+	default: printf("range_cast_u32!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#510: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:362:
+	default: printf("range_cast_s32!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_s32', this function's name, in a string
#510: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:362:
+	default: printf("range_cast_s32!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#526: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:378:
+	default: printf("range_cast!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast', this function's name, in a string
#526: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:378:
+	default: printf("range_cast!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#537: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:389:
+	default: printf("is_valid_num!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'is_valid_num', this function's name, in a string
#537: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:389:
+	default: printf("is_valid_num!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#551: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:403:
+	default: printf("is_valid_range!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'is_valid_range', this function's name, in a string
#551: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:403:
+	default: printf("is_valid_range!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#606: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:458:
+	default: printf("complement_op!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'complement_op', this function's name, in a string
#606: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:458:
+	default: printf("complement_op!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#619: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:471:
+	default: printf("op_str!\n"); exit(1);

WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'op_str', this function's name, in a string
#619: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:471:
+	default: printf("op_str!\n"); exit(1);

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#638: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:490:
+	default: printf("range_canbe op %d\n", op); exit(1);					\

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#643: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:495:
+	case U64: { range_canbe(u64); }

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#644: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:496:
+	case U32: { range_canbe(u32); }

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#645: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:497:
+	case S64: { range_canbe(s64); }

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#646: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:498:
+	case S32: { range_canbe(s32); }

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#647: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:499:
+	default: printf("range_canbe!\n"); exit(1);

WARNING:LINE_SPACING: Missing a blank line after declarations
#933: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:785:
+	struct bpf_insn insns[64];
+	LIBBPF_OPTS(bpf_prog_load_opts, opts,

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#1014: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:866:
+	case OP_LT: op_code = spec.compare_signed ? BPF_JSLT : BPF_JLT; break;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#1015: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:867:
+	case OP_LE: op_code = spec.compare_signed ? BPF_JSLE : BPF_JLE; break;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#1016: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:868:
+	case OP_GT: op_code = spec.compare_signed ? BPF_JSGT : BPF_JGT; break;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#1017: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:869:
+	case OP_GE: op_code = spec.compare_signed ? BPF_JSGE : BPF_JGE; break;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#1018: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:870:
+	case OP_EQ: op_code = BPF_JEQ; break;

ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
#1019: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:871:
+	case OP_NE: op_code = BPF_JNE; break;

WARNING:BRACES: braces {} are not necessary for single statement blocks
#1153: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1005:
+		for (t = MIN_T; t <= MAX_T; t++) {
+			reg->r[t] = range(t, sval, sval);
+		}

WARNING:BRACES: braces {} are not necessary for single statement blocks
#1559: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1411:
+		for (j = 0; j < ARRAY_SIZE(lower_seeds); j++) {
+			uvals[cnt++] = (((u64)upper_seeds[i]) << 32) | lower_seeds[j];
+		}

ERROR:OPEN_BRACE: that open brace { should be on the previous line
#1566: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1418:
+	for (i = 1, j = 0; i < cnt; i++)
+	{

WARNING:SUSPECT_CODE_INDENT: suspect code indent for conditional statements (8, 8)
#1665: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1517:
+	for (i = 0; i < val_cnt; i++)
+	for (j = 0; j < range_cnt; j++)

WARNING:SUSPECT_CODE_INDENT: suspect code indent for conditional statements (8, 8)
#1666: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1518:
+	for (j = 0; j < range_cnt; j++)
+	for (cond_t = MIN_T; cond_t <= MAX_T; cond_t++) {

-- 
0-DAY CI Kernel Test Service
https://github.com/intel/lkp-tests/wiki

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Shung-Hsi Yu]

On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> Add tests that validate correctness and completeness of BPF verifier's
> register range bounds.

Nitpick: in abstract-interpretation-speak, completeness seems to mean
something different. I believe what we're trying to check here is
soundness[1], again, in abstraction-interpretation-speak), so using
completeness here may be misleading to some. (I'll leave explanation to
other that understand this concept better than I do, rather than making an
ill attempt that would probably just make things worst)

> The main bulk is a lot of auto-generated tests based on a small set of
> seed values for lower and upper 32 bits of full 64-bit values.
> Currently we validate only range vs const comparisons, but the idea is
> to start validating range over range comparisons in subsequent patch set.

CC Langston Barrett who had previously send kunit-based tnum checks[2] a
while back. If this patch is merged, perhaps we can consider adding
validation for tnum as well in the future using similar framework.

More comments below

> When setting up initial register ranges we treat registers as one of
> u64/s64/u32/s32 numeric types, and then independently perform conditional
> comparisons based on a potentially different u64/s64/u32/s32 types. This
> tests lots of tricky cases of deriving bounds information across
> different numeric domains.
> 
> Given there are lots of auto-generated cases, we guard them behind
> SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> With current full set of upper/lower seed value, all supported
> comparison operators and all the combinations of u64/s64/u32/s32 number
> domains, we get about 7.7 million tests, which run in about 35 minutes
> on my local qemu instance. So it's something that can be run manually
> for exhaustive check in a reasonable time, and perhaps as a nightly CI
> test, but certainly is too slow to run as part of a default test_progs run.

FWIW an alternative approach that speeds things up is to use model checkers
like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
possible inputs takes less than 1.3 seconds[3] (based on code from [1]
paper, but I somehow lost the link to their GitHub repository).

One of the potential issue with [3] is that Z3Py is written in Python. So
there's the large over head of translating the C-implementation into Python
using Z3Py APIs each time we changed relevant code. This overhead could
potentially be removed with CBMC, which understand C, and we had a
precedence of using CBMC[4] within the kernel source code, though it was
later removed[5] due because SRCU changes are still happening too fast for
the format tests to keep up, so it looks like CBMC is not a silver-bullet.

I really meant to look into the CMBC approach for verification of ranges and
tnum, but fails to allocate time for it, so far.

Shung-Hsi

> ...

1: https://people.cs.rutgers.edu/~sn349/papers/cgo-2022.pdf
2: https://lore.kernel.org/bpf/20220430215727.113472-1-langston.barrett@gmail.com/
3: https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e
4: https://lore.kernel.org/all/1485295229-14081-3-git-send-email-paulmck@linux.vnet.ibm.com/

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Shung-Hsi Yu]

On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
> On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> > Add tests that validate correctness and completeness of BPF verifier's
> > register range bounds.
> 
> Nitpick: in abstract-interpretation-speak, completeness seems to mean
> something different. I believe what we're trying to check here is
> soundness[1], again, in abstraction-interpretation-speak), so using
> completeness here may be misleading to some. (I'll leave explanation to
> other that understand this concept better than I do, rather than making an
> ill attempt that would probably just make things worst)
> 
> > The main bulk is a lot of auto-generated tests based on a small set of
> > seed values for lower and upper 32 bits of full 64-bit values.
> > Currently we validate only range vs const comparisons, but the idea is
> > to start validating range over range comparisons in subsequent patch set.
> 
> CC Langston Barrett who had previously send kunit-based tnum checks[2] a
> while back. If this patch is merged, perhaps we can consider adding
> validation for tnum as well in the future using similar framework.
> 
> More comments below
> 
> > When setting up initial register ranges we treat registers as one of
> > u64/s64/u32/s32 numeric types, and then independently perform conditional
> > comparisons based on a potentially different u64/s64/u32/s32 types. This
> > tests lots of tricky cases of deriving bounds information across
> > different numeric domains.
> > 
> > Given there are lots of auto-generated cases, we guard them behind
> > SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> > With current full set of upper/lower seed value, all supported
> > comparison operators and all the combinations of u64/s64/u32/s32 number
> > domains, we get about 7.7 million tests, which run in about 35 minutes
> > on my local qemu instance. So it's something that can be run manually
> > for exhaustive check in a reasonable time, and perhaps as a nightly CI
> > test, but certainly is too slow to run as part of a default test_progs run.
> 
> FWIW an alternative approach that speeds things up is to use model checkers
> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> paper, but I somehow lost the link to their GitHub repository).

Found it. For reference, code used in "Sound, Precise, and Fast Abstract
Interpretation with Tristate Numbers"[1] can be found at
https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py

Below is a truncated form of the above that only check tnum_add(), requires
a package called python3-z3 on most distros:

  #!/usr/bin/python3
  from uuid import uuid4
  from z3 import And, BitVec, BitVecRef, BitVecVal, Implies, prove
  
  SIZE = 64 # Working with 64-bit integers
  
  class Tnum:
      """A model of tristate number use in Linux kernel's BPF verifier.
      https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c
      """
      val: BitVecRef
      mask: BitVecRef
  
      def __init__(self, val=None, mask=None):
          uid = uuid4() # Ensure that the BitVec are uniq, required by the Z3 solver
          self.val = BitVec(f'Tnum-val-{uid}', bv=SIZE) if val is None else val
          self.mask = BitVec(f'Tnum-mask-{uid}', bv=SIZE) if mask is None else mask
      
      def contains(self, bitvec: BitVecRef):
          # Simplified version of tnum_in()
          # https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c#L167-L173
          return (~self.mask & bitvec) == self.val
      
      def wellformed(self):
          # Bit cannot be set in both val and mask, such tnum is not valid
          return self.val & self.mask == BitVecVal(0, bv=SIZE)
  
  # The function that we want to check
  def tnum_add(a: Tnum, b: Tnum):
      # Unmodified tnum_add()
      # https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c#L62-L72
      sm = a.mask + b.mask
      sv = a.val + b.val
      sigma = sm + sv
      chi = sigma ^ sv
      mu = chi | a.mask | b.mask
      return Tnum(sv & ~mu, mu)
  
  t1 = Tnum()
  t2 = Tnum()
  
  x = BitVec('x', bv=SIZE) # Any possible 64-bit value
  y = BitVec('y', bv=SIZE) # same as above
  
  # Condition that needs to hold before we move forward to check tnum_add()
  premises = And(
      t1.wellformed(), # t1 and t2 is wellformed
      t2.wellformed(),
      t1.contains(x), # x is within t1, and y is within t2
      t2.contains(y),
  )
  
  # This ask Z3 solver to prove that tnum_add() work as intended
  prove(
      Implies(
          # Assuming that t1 and t2 is wellformed, x is within t1, and y is
          # within t2
          premises,
          # Below is what we'd like to check. Namely, for any random x whos
          # value is within t1, and any random y whos value is within t2,
          # (x+y) is always within the tnum produced by tnum_add(t1, t2)
          tnum_add(t1, t2).contains(x+y),
      )
  )

> One of the potential issue with [3] is that Z3Py is written in Python. So
> there's the large over head of translating the C-implementation into Python
> using Z3Py APIs each time we changed relevant code. This overhead could
> potentially be removed with CBMC, which understand C, and we had a
> precedence of using CBMC[4] within the kernel source code, though it was
> later removed[5] due because SRCU changes are still happening too fast for
> the format tests to keep up, so it looks like CBMC is not a silver-bullet.
> 
> I really meant to look into the CMBC approach for verification of ranges and
> tnum, but fails to allocate time for it, so far.
> 
> Shung-Hsi
> 
> > ...
> 
> 1: https://people.cs.rutgers.edu/~sn349/papers/cgo-2022.pdf
> 2: https://lore.kernel.org/bpf/20220430215727.113472-1-langston.barrett@gmail.com/
> 3: https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e
> 4: https://lore.kernel.org/all/1485295229-14081-3-git-send-email-paulmck@linux.vnet.ibm.com/

Also forgot to add the link to the removal of SRCU formal-verification tests

5: https://lore.kernel.org/all/20230717182337.1098991-2-paulmck@kernel.org/

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

On Thu, Oct 19, 2023 at 12:09 AM kernel test robot <lkp@intel.com> wrote:
>
> Hi Andrii,
>
> kernel test robot noticed the following build warnings:
>
> [auto build test WARNING on bpf-next/master]
>
> url:    https://github.com/intel-lab-lkp/linux/commits/Andrii-Nakryiko/bpf-improve-JEQ-JNE-branch-taken-logic/20231019-122550
> base:   https://git.kernel.org/pub/scm/linux/kernel/git/bpf/bpf-next.git master
> patch link:    https://lore.kernel.org/r/20231019042405.2971130-8-andrii%40kernel.org
> patch subject: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester
> reproduce: (https://download.01.org/0day-ci/archive/20231019/202310191409.pIIb2buD-lkp@intel.com/reproduce)
>
> If you fix the issue in a separate patch/commit (i.e. not just a new version of
> the same patch/commit), kindly add following tags
> | Reported-by: kernel test robot <lkp@intel.com>
> | Closes: https://lore.kernel.org/oe-kbuild-all/202310191409.pIIb2buD-lkp@intel.com/
>
> # many are suggestions rather than must-fix
>
> WARNING:NEW_TYPEDEFS: do not add new typedefs
> #169: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:21:
> +typedef unsigned long long ___u64;
>
> WARNING:NEW_TYPEDEFS: do not add new typedefs
> #170: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:22:
> +typedef unsigned int ___u32;
>
> WARNING:NEW_TYPEDEFS: do not add new typedefs
> #171: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:23:
> +typedef long long ___s64;
>
> WARNING:NEW_TYPEDEFS: do not add new typedefs
> #172: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:24:
> +typedef int ___s32;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #215: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:67:
> +       case U64: return (u64)x < (u64)y ? (u64)x : (u64)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #216: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:68:
> +       case U32: return (u32)x < (u32)y ? (u32)x : (u32)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #217: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:69:
> +       case S64: return (s64)x < (s64)y ? (s64)x : (s64)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #218: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:70:
> +       case S32: return (s32)x < (s32)y ? (s32)x : (s32)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #219: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:71:
> +       default: printf("min_t!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'min_t', this function's name, in a string
> #219: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:71:
> +       default: printf("min_t!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #226: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:78:
> +       case U64: return (u64)x > (u64)y ? (u64)x : (u64)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #227: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:79:
> +       case U32: return (u32)x > (u32)y ? (u32)x : (u32)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #228: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:80:
> +       case S64: return (s64)x > (s64)y ? (s64)x : (s64)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #229: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:81:
> +       case S32: return (s32)x > (s32)y ? (u32)(s32)x : (u32)(s32)y;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #230: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:82:
> +       default: printf("max_t!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'max_t', this function's name, in a string
> #230: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:82:
> +       default: printf("max_t!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #241: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:93:
> +       default: printf("t_str!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_str', this function's name, in a string
> #241: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:93:
> +       default: printf("t_str!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #252: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:104:
> +       default: printf("t_is_32!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_is_32', this function's name, in a string
> #252: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:104:
> +       default: printf("t_is_32!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #263: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:115:
> +       default: printf("t_signed!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_signed', this function's name, in a string
> #263: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:115:
> +       default: printf("t_signed!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #274: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:126:
> +       default: printf("t_unsigned!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 't_unsigned', this function's name, in a string
> #274: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:126:
> +       default: printf("t_unsigned!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #285: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:137:
> +       default: printf("num_is_small!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'num_is_small', this function's name, in a string
> #285: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:137:
> +       default: printf("num_is_small!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #299: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:151:
> +               default: printf("snprintf_num!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'snprintf_num', this function's name, in a string
> #299: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:151:
> +               default: printf("snprintf_num!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #339: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:191:
> +               default: printf("snprintf_num!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'snprintf_num', this function's name, in a string
> #339: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:191:
> +               default: printf("snprintf_num!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #386: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:238:
> +       default: printf("unkn_subreg!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'unkn_subreg', this function's name, in a string
> #386: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:238:
> +       default: printf("unkn_subreg!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #397: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:249:
> +       default: printf("range!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range', this function's name, in a string
> #397: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:249:
> +       default: printf("range!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #454: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:306:
> +       default: printf("range_cast_u64!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_u64', this function's name, in a string
> #454: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:306:
> +       default: printf("range_cast_u64!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #476: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:328:
> +       default: printf("range_cast_s64!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_s64', this function's name, in a string
> #476: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:328:
> +       default: printf("range_cast_s64!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #493: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:345:
> +       default: printf("range_cast_u32!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_u32', this function's name, in a string
> #493: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:345:
> +       default: printf("range_cast_u32!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #510: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:362:
> +       default: printf("range_cast_s32!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast_s32', this function's name, in a string
> #510: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:362:
> +       default: printf("range_cast_s32!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #526: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:378:
> +       default: printf("range_cast!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'range_cast', this function's name, in a string
> #526: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:378:
> +       default: printf("range_cast!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #537: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:389:
> +       default: printf("is_valid_num!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'is_valid_num', this function's name, in a string
> #537: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:389:
> +       default: printf("is_valid_num!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #551: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:403:
> +       default: printf("is_valid_range!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'is_valid_range', this function's name, in a string
> #551: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:403:
> +       default: printf("is_valid_range!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #606: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:458:
> +       default: printf("complement_op!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'complement_op', this function's name, in a string
> #606: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:458:
> +       default: printf("complement_op!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #619: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:471:
> +       default: printf("op_str!\n"); exit(1);
>
> WARNING:EMBEDDED_FUNCTION_NAME: Prefer using '"%s...", __func__' to using 'op_str', this function's name, in a string
> #619: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:471:
> +       default: printf("op_str!\n"); exit(1);
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #638: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:490:
> +       default: printf("range_canbe op %d\n", op); exit(1);                                    \
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #643: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:495:
> +       case U64: { range_canbe(u64); }
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #644: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:496:
> +       case U32: { range_canbe(u32); }
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #645: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:497:
> +       case S64: { range_canbe(s64); }
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #646: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:498:
> +       case S32: { range_canbe(s32); }
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #647: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:499:
> +       default: printf("range_canbe!\n"); exit(1);
>
> WARNING:LINE_SPACING: Missing a blank line after declarations
> #933: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:785:
> +       struct bpf_insn insns[64];
> +       LIBBPF_OPTS(bpf_prog_load_opts, opts,
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #1014: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:866:
> +       case OP_LT: op_code = spec.compare_signed ? BPF_JSLT : BPF_JLT; break;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #1015: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:867:
> +       case OP_LE: op_code = spec.compare_signed ? BPF_JSLE : BPF_JLE; break;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #1016: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:868:
> +       case OP_GT: op_code = spec.compare_signed ? BPF_JSGT : BPF_JGT; break;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #1017: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:869:
> +       case OP_GE: op_code = spec.compare_signed ? BPF_JSGE : BPF_JGE; break;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #1018: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:870:
> +       case OP_EQ: op_code = BPF_JEQ; break;
>
> ERROR:TRAILING_STATEMENTS: trailing statements should be on next line
> #1019: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:871:
> +       case OP_NE: op_code = BPF_JNE; break;
>
> WARNING:BRACES: braces {} are not necessary for single statement blocks
> #1153: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1005:
> +               for (t = MIN_T; t <= MAX_T; t++) {
> +                       reg->r[t] = range(t, sval, sval);
> +               }
>
> WARNING:BRACES: braces {} are not necessary for single statement blocks
> #1559: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1411:
> +               for (j = 0; j < ARRAY_SIZE(lower_seeds); j++) {
> +                       uvals[cnt++] = (((u64)upper_seeds[i]) << 32) | lower_seeds[j];
> +               }
>
> ERROR:OPEN_BRACE: that open brace { should be on the previous line
> #1566: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1418:
> +       for (i = 1, j = 0; i < cnt; i++)
> +       {
>
> WARNING:SUSPECT_CODE_INDENT: suspect code indent for conditional statements (8, 8)
> #1665: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1517:
> +       for (i = 0; i < val_cnt; i++)
> +       for (j = 0; j < range_cnt; j++)
>
> WARNING:SUSPECT_CODE_INDENT: suspect code indent for conditional statements (8, 8)
> #1666: FILE: tools/testing/selftests/bpf/prog_tests/reg_bounds.c:1518:
> +       for (j = 0; j < range_cnt; j++)
> +       for (cond_t = MIN_T; cond_t <= MAX_T; cond_t++) {

I think I'm going to ignore most of the above warnings and
suggestions, but let's see what comes up in the code review.
>
> --
> 0-DAY CI Kernel Test Service
> https://github.com/intel/lkp-tests/wiki

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

On Thu, Oct 19, 2023 at 12:30 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>
> On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> > Add tests that validate correctness and completeness of BPF verifier's
> > register range bounds.
>
> Nitpick: in abstract-interpretation-speak, completeness seems to mean
> something different. I believe what we're trying to check here is
> soundness[1], again, in abstraction-interpretation-speak), so using
> completeness here may be misleading to some. (I'll leave explanation to
> other that understand this concept better than I do, rather than making an
> ill attempt that would probably just make things worst)

I'll just say "Add test to validate BPF verifier's register range
bounds tracking logic." to avoid terminology hazards :)

>
> > The main bulk is a lot of auto-generated tests based on a small set of
> > seed values for lower and upper 32 bits of full 64-bit values.
> > Currently we validate only range vs const comparisons, but the idea is
> > to start validating range over range comparisons in subsequent patch set.
>
> CC Langston Barrett who had previously send kunit-based tnum checks[2] a
> while back. If this patch is merged, perhaps we can consider adding
> validation for tnum as well in the future using similar framework.
>
> More comments below
>
> > When setting up initial register ranges we treat registers as one of
> > u64/s64/u32/s32 numeric types, and then independently perform conditional
> > comparisons based on a potentially different u64/s64/u32/s32 types. This
> > tests lots of tricky cases of deriving bounds information across
> > different numeric domains.
> >
> > Given there are lots of auto-generated cases, we guard them behind
> > SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> > With current full set of upper/lower seed value, all supported
> > comparison operators and all the combinations of u64/s64/u32/s32 number
> > domains, we get about 7.7 million tests, which run in about 35 minutes
> > on my local qemu instance. So it's something that can be run manually
> > for exhaustive check in a reasonable time, and perhaps as a nightly CI
> > test, but certainly is too slow to run as part of a default test_progs run.
>
> FWIW an alternative approach that speeds things up is to use model checkers
> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> paper, but I somehow lost the link to their GitHub repository).
>
> One of the potential issue with [3] is that Z3Py is written in Python. So
> there's the large over head of translating the C-implementation into Python
> using Z3Py APIs each time we changed relevant code. This overhead could
> potentially be removed with CBMC, which understand C, and we had a
> precedence of using CBMC[4] within the kernel source code, though it was
> later removed[5] due because SRCU changes are still happening too fast for
> the format tests to keep up, so it looks like CBMC is not a silver-bullet.
>
> I really meant to look into the CMBC approach for verification of ranges and
> tnum, but fails to allocate time for it, so far.

It would be great if someone did a proper model checker-based
verification of range tracking logic of overall BPF verifier logic,
agreed. Until we have that (and depending on how easy it is to
integrate that approach into BPF CI), I think having something as part
of test_progs is a good practical step forward.

>
> Shung-Hsi
>
> > ...
>
> 1: https://people.cs.rutgers.edu/~sn349/papers/cgo-2022.pdf
> 2: https://lore.kernel.org/bpf/20220430215727.113472-1-langston.barrett@gmail.com/
> 3: https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e
> 4: https://lore.kernel.org/all/1485295229-14081-3-git-send-email-paulmck@linux.vnet.ibm.com/

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>
> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
> > On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> > > Add tests that validate correctness and completeness of BPF verifier's
> > > register range bounds.
> >
> > Nitpick: in abstract-interpretation-speak, completeness seems to mean
> > something different. I believe what we're trying to check here is
> > soundness[1], again, in abstraction-interpretation-speak), so using
> > completeness here may be misleading to some. (I'll leave explanation to
> > other that understand this concept better than I do, rather than making an
> > ill attempt that would probably just make things worst)
> >
> > > The main bulk is a lot of auto-generated tests based on a small set of
> > > seed values for lower and upper 32 bits of full 64-bit values.
> > > Currently we validate only range vs const comparisons, but the idea is
> > > to start validating range over range comparisons in subsequent patch set.
> >
> > CC Langston Barrett who had previously send kunit-based tnum checks[2] a
> > while back. If this patch is merged, perhaps we can consider adding
> > validation for tnum as well in the future using similar framework.
> >
> > More comments below
> >
> > > When setting up initial register ranges we treat registers as one of
> > > u64/s64/u32/s32 numeric types, and then independently perform conditional
> > > comparisons based on a potentially different u64/s64/u32/s32 types. This
> > > tests lots of tricky cases of deriving bounds information across
> > > different numeric domains.
> > >
> > > Given there are lots of auto-generated cases, we guard them behind
> > > SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> > > With current full set of upper/lower seed value, all supported
> > > comparison operators and all the combinations of u64/s64/u32/s32 number
> > > domains, we get about 7.7 million tests, which run in about 35 minutes
> > > on my local qemu instance. So it's something that can be run manually
> > > for exhaustive check in a reasonable time, and perhaps as a nightly CI
> > > test, but certainly is too slow to run as part of a default test_progs run.
> >
> > FWIW an alternative approach that speeds things up is to use model checkers
> > like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > paper, but I somehow lost the link to their GitHub repository).
>
> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> Interpretation with Tristate Numbers"[1] can be found at
> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
>
> Below is a truncated form of the above that only check tnum_add(), requires
> a package called python3-z3 on most distros:

Great! I'd be curious to see how range tracking logic can be encoded
using this approach, please give it a go!

>
>   #!/usr/bin/python3
>   from uuid import uuid4
>   from z3 import And, BitVec, BitVecRef, BitVecVal, Implies, prove
>
>   SIZE = 64 # Working with 64-bit integers
>
>   class Tnum:
>       """A model of tristate number use in Linux kernel's BPF verifier.
>       https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c
>       """
>       val: BitVecRef
>       mask: BitVecRef
>
>       def __init__(self, val=None, mask=None):
>           uid = uuid4() # Ensure that the BitVec are uniq, required by the Z3 solver
>           self.val = BitVec(f'Tnum-val-{uid}', bv=SIZE) if val is None else val
>           self.mask = BitVec(f'Tnum-mask-{uid}', bv=SIZE) if mask is None else mask
>
>       def contains(self, bitvec: BitVecRef):
>           # Simplified version of tnum_in()
>           # https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c#L167-L173
>           return (~self.mask & bitvec) == self.val
>
>       def wellformed(self):
>           # Bit cannot be set in both val and mask, such tnum is not valid
>           return self.val & self.mask == BitVecVal(0, bv=SIZE)
>
>   # The function that we want to check
>   def tnum_add(a: Tnum, b: Tnum):
>       # Unmodified tnum_add()
>       # https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c#L62-L72
>       sm = a.mask + b.mask
>       sv = a.val + b.val
>       sigma = sm + sv
>       chi = sigma ^ sv
>       mu = chi | a.mask | b.mask
>       return Tnum(sv & ~mu, mu)
>
>   t1 = Tnum()
>   t2 = Tnum()
>
>   x = BitVec('x', bv=SIZE) # Any possible 64-bit value
>   y = BitVec('y', bv=SIZE) # same as above
>
>   # Condition that needs to hold before we move forward to check tnum_add()
>   premises = And(
>       t1.wellformed(), # t1 and t2 is wellformed
>       t2.wellformed(),
>       t1.contains(x), # x is within t1, and y is within t2
>       t2.contains(y),
>   )
>
>   # This ask Z3 solver to prove that tnum_add() work as intended
>   prove(
>       Implies(
>           # Assuming that t1 and t2 is wellformed, x is within t1, and y is
>           # within t2
>           premises,
>           # Below is what we'd like to check. Namely, for any random x whos
>           # value is within t1, and any random y whos value is within t2,
>           # (x+y) is always within the tnum produced by tnum_add(t1, t2)
>           tnum_add(t1, t2).contains(x+y),
>       )
>   )
>
> > One of the potential issue with [3] is that Z3Py is written in Python. So
> > there's the large over head of translating the C-implementation into Python
> > using Z3Py APIs each time we changed relevant code. This overhead could
> > potentially be removed with CBMC, which understand C, and we had a
> > precedence of using CBMC[4] within the kernel source code, though it was
> > later removed[5] due because SRCU changes are still happening too fast for
> > the format tests to keep up, so it looks like CBMC is not a silver-bullet.
> >
> > I really meant to look into the CMBC approach for verification of ranges and
> > tnum, but fails to allocate time for it, so far.
> >
> > Shung-Hsi
> >
> > > ...
> >
> > 1: https://people.cs.rutgers.edu/~sn349/papers/cgo-2022.pdf
> > 2: https://lore.kernel.org/bpf/20220430215727.113472-1-langston.barrett@gmail.com/
> > 3: https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e
> > 4: https://lore.kernel.org/all/1485295229-14081-3-git-send-email-paulmck@linux.vnet.ibm.com/
>
> Also forgot to add the link to the removal of SRCU formal-verification tests
>
> 5: https://lore.kernel.org/all/20230717182337.1098991-2-paulmck@kernel.org/

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Shung-Hsi Yu]

On Thu, Oct 19, 2023 at 11:31:55AM -0700, Andrii Nakryiko wrote:
> On Thu, Oct 19, 2023 at 12:30 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> > > Add tests that validate correctness and completeness of BPF verifier's
> > > register range bounds.
> >
> > Nitpick: in abstract-interpretation-speak, completeness seems to mean
> > something different. I believe what we're trying to check here is
> > soundness[1], again, in abstraction-interpretation-speak), so using
> > completeness here may be misleading to some. (I'll leave explanation to
> > other that understand this concept better than I do, rather than making an
> > ill attempt that would probably just make things worst)
> 
> I'll just say "Add test to validate BPF verifier's register range
> bounds tracking logic." to avoid terminology hazards :)

Sounds good to me :)

> > > The main bulk is a lot of auto-generated tests based on a small set of
> > > seed values for lower and upper 32 bits of full 64-bit values.
> > > Currently we validate only range vs const comparisons, but the idea is
> > > to start validating range over range comparisons in subsequent patch set.
> >
> > CC Langston Barrett who had previously send kunit-based tnum checks[2] a
> > while back. If this patch is merged, perhaps we can consider adding
> > validation for tnum as well in the future using similar framework.
> >
> > More comments below
> >
> > > When setting up initial register ranges we treat registers as one of
> > > u64/s64/u32/s32 numeric types, and then independently perform conditional
> > > comparisons based on a potentially different u64/s64/u32/s32 types. This
> > > tests lots of tricky cases of deriving bounds information across
> > > different numeric domains.
> > >
> > > Given there are lots of auto-generated cases, we guard them behind
> > > SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> > > With current full set of upper/lower seed value, all supported
> > > comparison operators and all the combinations of u64/s64/u32/s32 number
> > > domains, we get about 7.7 million tests, which run in about 35 minutes
> > > on my local qemu instance. So it's something that can be run manually
> > > for exhaustive check in a reasonable time, and perhaps as a nightly CI
> > > test, but certainly is too slow to run as part of a default test_progs run.
> >
> > FWIW an alternative approach that speeds things up is to use model checkers
> > like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > paper, but I somehow lost the link to their GitHub repository).
> >
> > One of the potential issue with [3] is that Z3Py is written in Python. So
> > there's the large over head of translating the C-implementation into Python
> > using Z3Py APIs each time we changed relevant code. This overhead could
> > potentially be removed with CBMC, which understand C, and we had a
> > precedence of using CBMC[4] within the kernel source code, though it was
> > later removed[5] due because SRCU changes are still happening too fast for
> > the format tests to keep up, so it looks like CBMC is not a silver-bullet.
> >
> > I really meant to look into the CMBC approach for verification of ranges and
> > tnum, but fails to allocate time for it, so far.
> 
> It would be great if someone did a proper model checker-based
> verification of range tracking logic of overall BPF verifier logic,
> agreed. Until we have that (and depending on how easy it is to
> integrate that approach into BPF CI), I think having something as part
> of test_progs is a good practical step forward.

Agree, by no mean was I trying to suggest we shouldn't have this test.
Mainly want to bring up checker-based verification, and was glad to hear
that it is considered worth investigating.

> > Shung-Hsi
> >
> > > ...
> >
> > 1: https://people.cs.rutgers.edu/~sn349/papers/cgo-2022.pdf
> > 2: https://lore.kernel.org/bpf/20220430215727.113472-1-langston.barrett@gmail.com/
> > 3: https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e
> > 4: https://lore.kernel.org/all/1485295229-14081-3-git-send-email-paulmck@linux.vnet.ibm.com/

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Srinivas Narayana Ganapathy]

Hi all,

Thanks, @Shung-Hsi, for bringing up this conversation about
integrating formal verification approaches into the BPF CI and testing.

> On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
>
> On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>>
>> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
>>> On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
>>>> Add tests that validate correctness and completeness of BPF verifier's
>>>> register range bounds.
>>>
>>> Nitpick: in abstract-interpretation-speak, completeness seems to mean
>>> something different. I believe what we're trying to check here is
>>> soundness[1], again, in abstraction-interpretation-speak), so using
>>> completeness here may be misleading to some. (I'll leave explanation to
>>> other that understand this concept better than I do, rather than making an
>>> ill attempt that would probably just make things worst)
>>>
>>>> The main bulk is a lot of auto-generated tests based on a small set of
>>>> seed values for lower and upper 32 bits of full 64-bit values.
>>>> Currently we validate only range vs const comparisons, but the idea is
>>>> to start validating range over range comparisons in subsequent patch set.
>>>
>>> CC Langston Barrett who had previously send kunit-based tnum checks[2] a
>>> while back. If this patch is merged, perhaps we can consider adding
>>> validation for tnum as well in the future using similar framework.
>>>
>>> More comments below
>>>
>>>> When setting up initial register ranges we treat registers as one of
>>>> u64/s64/u32/s32 numeric types, and then independently perform conditional
>>>> comparisons based on a potentially different u64/s64/u32/s32 types. This
>>>> tests lots of tricky cases of deriving bounds information across
>>>> different numeric domains.
>>>>
>>>> Given there are lots of auto-generated cases, we guard them behind
>>>> SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
>>>> With current full set of upper/lower seed value, all supported
>>>> comparison operators and all the combinations of u64/s64/u32/s32 number
>>>> domains, we get about 7.7 million tests, which run in about 35 minutes
>>>> on my local qemu instance. So it's something that can be run manually
>>>> for exhaustive check in a reasonable time, and perhaps as a nightly CI
>>>> test, but certainly is too slow to run as part of a default test_progs run.
>>>
>>> FWIW an alternative approach that speeds things up is to use model checkers
>>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
>>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
>>> paper, but I somehow lost the link to their GitHub repository).
>>
>> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
>> Interpretation with Tristate Numbers"[1] can be found at
>> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
>>
>> Below is a truncated form of the above that only check tnum_add(), requires
>> a package called python3-z3 on most distros:
>
> Great! I'd be curious to see how range tracking logic can be encoded
> using this approach, please give it a go!
>

We have some recent work that applies formal verification approaches
to the entirety of range tracking in the eBPF verifier. We posted a
note to the eBPF mailing list about it sometime ago:

[1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u

Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.

[2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf

Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
are working to get our tooling into a form that is integrable into BPF
CI. We will look forward to your feedback when we post patches.

Thanks,

--
Srinivas
The fastest algorithm can frequently be replaced by one that is almost as fast and much easier to understand.

RE: [PATCH v2 bpf-next 0/7] BPF register bounds logic and testing improvements

[John Fastabend]

Andrii Nakryiko wrote:
> This patch set adds a big set of manual and auto-generated test cases
> validating BPF verifier's register bounds tracking and deduction logic. See
> details in the last patch.
> 
> To make this approach work, BPF verifier's logic needed a bunch of
> improvements to handle some cases that previously were not covered. This had
> no implications as to correctness of verifier logic, but it was incomplete
> enough to cause significant disagreements with alternative implementation of
> register bounds logic that tests in this patch set implement. So we need BPF
> verifier logic improvements to make all the tests pass.
> 
> This is a first part of work with the end goal intended to extend register
> bounds logic to cover range vs range comparisons, which will be submitted
> later assuming changes in this patch set land.
> 
> See individual patches for details.

Nice, I'm about half way through this I'll continue on Monday. The two rounds
of convergence was interesting I didn't expect that. Looks good to me though
so far.

Thanks for doing this I've wanted this cleaned up for awhile!

> 
> v1->v2:
>   - fix compilation when building selftests with llvm-16 toolchain (CI).
> 
> Andrii Nakryiko (7):
>   bpf: improve JEQ/JNE branch taken logic
>   bpf: derive smin/smax from umin/max bounds
>   bpf: enhance subregister bounds deduction logic
>   bpf: improve deduction of 64-bit bounds from 32-bit bounds
>   bpf: try harder to deduce register bounds from different numeric
>     domains
>   bpf: drop knowledge-losing __reg_combine_{32,64}_into_{64,32} logic
>   selftests/bpf: BPF register range bounds tester
> 
>  kernel/bpf/verifier.c                         |  175 +-
>  .../selftests/bpf/prog_tests/reg_bounds.c     | 1668 +++++++++++++++++
>  2 files changed, 1791 insertions(+), 52 deletions(-)
>  create mode 100644 tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> 
> -- 
> 2.34.1
> 
> 

Re: [PATCH v2 bpf-next 0/7] BPF register bounds logic and testing improvements

[Andrii Nakryiko]

On Fri, Oct 20, 2023 at 9:14 PM John Fastabend <john.fastabend@gmail.com> wrote:
>
> Andrii Nakryiko wrote:
> > This patch set adds a big set of manual and auto-generated test cases
> > validating BPF verifier's register bounds tracking and deduction logic. See
> > details in the last patch.
> >
> > To make this approach work, BPF verifier's logic needed a bunch of
> > improvements to handle some cases that previously were not covered. This had
> > no implications as to correctness of verifier logic, but it was incomplete
> > enough to cause significant disagreements with alternative implementation of
> > register bounds logic that tests in this patch set implement. So we need BPF
> > verifier logic improvements to make all the tests pass.
> >
> > This is a first part of work with the end goal intended to extend register
> > bounds logic to cover range vs range comparisons, which will be submitted
> > later assuming changes in this patch set land.
> >
> > See individual patches for details.
>
> Nice, I'm about half way through this I'll continue on Monday. The two rounds
> of convergence was interesting I didn't expect that. Looks good to me though
> so far.
>

Great, thanks for reviewing! I found an incompleteness in BPF_JEQ and
BPF_JNE handling in reg_bounds selftests, but it is not exposed on
range vs const comparisons (I found it only when I started testing
range vs range). So I might update this revision with slight changes
on selftest side, but kernel side so far looks good and I don't plan
any adjustments in this patch set.

I do have further generalization coming up that supports range vs
range comparisons and is_branch_taken() logic, so keep in mind that
this is just a first part :)

> Thanks for doing this I've wanted this cleaned up for awhile!

No problems, this was fun, and once range vs range logic lands I'll
have peace of mind :)

>
> >
> > v1->v2:
> >   - fix compilation when building selftests with llvm-16 toolchain (CI).
> >
> > Andrii Nakryiko (7):
> >   bpf: improve JEQ/JNE branch taken logic
> >   bpf: derive smin/smax from umin/max bounds
> >   bpf: enhance subregister bounds deduction logic
> >   bpf: improve deduction of 64-bit bounds from 32-bit bounds
> >   bpf: try harder to deduce register bounds from different numeric
> >     domains
> >   bpf: drop knowledge-losing __reg_combine_{32,64}_into_{64,32} logic
> >   selftests/bpf: BPF register range bounds tester
> >
> >  kernel/bpf/verifier.c                         |  175 +-
> >  .../selftests/bpf/prog_tests/reg_bounds.c     | 1668 +++++++++++++++++
> >  2 files changed, 1791 insertions(+), 52 deletions(-)
> >  create mode 100644 tools/testing/selftests/bpf/prog_tests/reg_bounds.c
> >
> > --
> > 2.34.1
> >
> >
>
>

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
<sn624@cs.rutgers.edu> wrote:
>
> Hi all,
>
> Thanks, @Shung-Hsi, for bringing up this conversation about
> integrating formal verification approaches into the BPF CI and testing.
>
> > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> >
> > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> >>
> >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
> >>> On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> >>>> Add tests that validate correctness and completeness of BPF verifier's
> >>>> register range bounds.
> >>>
> >>> Nitpick: in abstract-interpretation-speak, completeness seems to mean
> >>> something different. I believe what we're trying to check here is
> >>> soundness[1], again, in abstraction-interpretation-speak), so using
> >>> completeness here may be misleading to some. (I'll leave explanation to
> >>> other that understand this concept better than I do, rather than making an
> >>> ill attempt that would probably just make things worst)
> >>>
> >>>> The main bulk is a lot of auto-generated tests based on a small set of
> >>>> seed values for lower and upper 32 bits of full 64-bit values.
> >>>> Currently we validate only range vs const comparisons, but the idea is
> >>>> to start validating range over range comparisons in subsequent patch set.
> >>>
> >>> CC Langston Barrett who had previously send kunit-based tnum checks[2] a
> >>> while back. If this patch is merged, perhaps we can consider adding
> >>> validation for tnum as well in the future using similar framework.
> >>>
> >>> More comments below
> >>>
> >>>> When setting up initial register ranges we treat registers as one of
> >>>> u64/s64/u32/s32 numeric types, and then independently perform conditional
> >>>> comparisons based on a potentially different u64/s64/u32/s32 types. This
> >>>> tests lots of tricky cases of deriving bounds information across
> >>>> different numeric domains.
> >>>>
> >>>> Given there are lots of auto-generated cases, we guard them behind
> >>>> SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> >>>> With current full set of upper/lower seed value, all supported
> >>>> comparison operators and all the combinations of u64/s64/u32/s32 number
> >>>> domains, we get about 7.7 million tests, which run in about 35 minutes
> >>>> on my local qemu instance. So it's something that can be run manually
> >>>> for exhaustive check in a reasonable time, and perhaps as a nightly CI
> >>>> test, but certainly is too slow to run as part of a default test_progs run.
> >>>
> >>> FWIW an alternative approach that speeds things up is to use model checkers
> >>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> >>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> >>> paper, but I somehow lost the link to their GitHub repository).
> >>
> >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> >> Interpretation with Tristate Numbers"[1] can be found at
> >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> >>
> >> Below is a truncated form of the above that only check tnum_add(), requires
> >> a package called python3-z3 on most distros:
> >
> > Great! I'd be curious to see how range tracking logic can be encoded
> > using this approach, please give it a go!
> >
>
> We have some recent work that applies formal verification approaches
> to the entirety of range tracking in the eBPF verifier. We posted a
> note to the eBPF mailing list about it sometime ago:
>
> [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
>

Oh, I totally missed this, as I just went on a long vacation a few
days before that and declared email bankruptcy afterwards. I'll try to
give it a read, though I see lots of math symbols there and make no
promises ;)

> Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
>
> [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
>
> Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> are working to get our tooling into a form that is integrable into BPF
> CI. We will look forward to your feedback when we post patches.

If this could be integrated in a way that we can regularly run this
and validate latest version of verifier, that would be great. I have a
second part of verifier changes coming up that extends range tracking
logic further to support range vs range (as opposed to range vs const
that we do currently) comparisons and is_branch_taken, so having
independent and formal verification of these changes would be great!

>
> Thanks,
>
> --
> Srinivas
> The fastest algorithm can frequently be replaced by one that is almost as fast and much easier to understand.
>

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Shung-Hsi Yu]

On Sat, Oct 21, 2023 at 09:42:46PM -0700, Andrii Nakryiko wrote:
> On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
> <sn624@cs.rutgers.edu> wrote:
> >
> > Hi all,
> >
> > Thanks, @Shung-Hsi, for bringing up this conversation about
> > integrating formal verification approaches into the BPF CI and testing.
> >
> > > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
> > >>> On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> > >>>> Add tests that validate correctness and completeness of BPF verifier's
> > >>>> register range bounds.
> > >>>
> > >>> Nitpick: in abstract-interpretation-speak, completeness seems to mean
> > >>> something different. I believe what we're trying to check here is
> > >>> soundness[1], again, in abstraction-interpretation-speak), so using
> > >>> completeness here may be misleading to some. (I'll leave explanation to
> > >>> other that understand this concept better than I do, rather than making an
> > >>> ill attempt that would probably just make things worst)
> > >>>
> > >>>> The main bulk is a lot of auto-generated tests based on a small set of
> > >>>> seed values for lower and upper 32 bits of full 64-bit values.
> > >>>> Currently we validate only range vs const comparisons, but the idea is
> > >>>> to start validating range over range comparisons in subsequent patch set.
> > >>>
> > >>> CC Langston Barrett who had previously send kunit-based tnum checks[2] a
> > >>> while back. If this patch is merged, perhaps we can consider adding
> > >>> validation for tnum as well in the future using similar framework.
> > >>>
> > >>> More comments below
> > >>>
> > >>>> When setting up initial register ranges we treat registers as one of
> > >>>> u64/s64/u32/s32 numeric types, and then independently perform conditional
> > >>>> comparisons based on a potentially different u64/s64/u32/s32 types. This
> > >>>> tests lots of tricky cases of deriving bounds information across
> > >>>> different numeric domains.
> > >>>>
> > >>>> Given there are lots of auto-generated cases, we guard them behind
> > >>>> SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> > >>>> With current full set of upper/lower seed value, all supported
> > >>>> comparison operators and all the combinations of u64/s64/u32/s32 number
> > >>>> domains, we get about 7.7 million tests, which run in about 35 minutes
> > >>>> on my local qemu instance. So it's something that can be run manually
> > >>>> for exhaustive check in a reasonable time, and perhaps as a nightly CI
> > >>>> test, but certainly is too slow to run as part of a default test_progs run.
> > >>>
> > >>> FWIW an alternative approach that speeds things up is to use model checkers
> > >>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > >>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > >>> paper, but I somehow lost the link to their GitHub repository).
> > >>
> > >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> > >> Interpretation with Tristate Numbers"[1] can be found at
> > >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> > >>
> > >> Below is a truncated form of the above that only check tnum_add(), requires
> > >> a package called python3-z3 on most distros:
> > >
> > > Great! I'd be curious to see how range tracking logic can be encoded
> > > using this approach, please give it a go!
> >
> > We have some recent work that applies formal verification approaches
> > to the entirety of range tracking in the eBPF verifier. We posted a
> > note to the eBPF mailing list about it sometime ago:
> >
> > [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
> 
> Oh, I totally missed this, as I just went on a long vacation a few
> days before that and declared email bankruptcy afterwards. I'll try to
> give it a read, though I see lots of math symbols there and make no
> promises ;)

Feels the same when I start reading their previous work, but I can vouch
their work their work are definitely worth the read. (Though I had to admit
I secretly chant "math is easier than code, math is easier than code" to
convincing my mind to not go into flight mode when seeing math symbols ;D)

> > Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
> >
> > [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
> >
> > Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> > are working to get our tooling into a form that is integrable into BPF
> > CI. We will look forward to your feedback when we post patches.
> 
> If this could be integrated in a way that we can regularly run this
> and validate latest version of verifier, that would be great. I have a
> second part of verifier changes coming up that extends range tracking
> logic further to support range vs range (as opposed to range vs const
> that we do currently) comparisons and is_branch_taken, so having
> independent and formal verification of these changes would be great!

+1 (from a quick skim) this work is already great as-is, and it'd be even
better once it get's in the CI. From the paper there's this

  We conducted our experiments on ... a machine with two 10-core Intel
  Skylake CPUs running at 2.20 GHz with 192 GB of memory...

I suppose the memory requirement comes from the vast amount of state space
that the Z3 SMT solver have to go through, and perhaps that poses a
challenge for CI integration?

Just wondering is there are some low-hanging fruit the can make things
easier for the SMT solver.

> > Thanks,
> >
> > --
> > Srinivas
> > The fastest algorithm can frequently be replaced by one that is almost as fast and much easier to understand.
> >

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Paul Chaignon]

On Mon, Oct 23, 2023 at 10:05:41PM +0800, Shung-Hsi Yu wrote:
> On Sat, Oct 21, 2023 at 09:42:46PM -0700, Andrii Nakryiko wrote:
> > On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
> > <sn624@cs.rutgers.edu> wrote:
> > >
> > > Hi all,
> > >
> > > Thanks, @Shung-Hsi, for bringing up this conversation about
> > > integrating formal verification approaches into the BPF CI and testing.
> > >
> > > > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> > > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > > >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:

[...]

> > > >>> FWIW an alternative approach that speeds things up is to use model checkers
> > > >>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > > >>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > > >>> paper, but I somehow lost the link to their GitHub repository).
> > > >>
> > > >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> > > >> Interpretation with Tristate Numbers"[1] can be found at
> > > >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> > > >>
> > > >> Below is a truncated form of the above that only check tnum_add(), requires
> > > >> a package called python3-z3 on most distros:
> > > >
> > > > Great! I'd be curious to see how range tracking logic can be encoded
> > > > using this approach, please give it a go!
> > >
> > > We have some recent work that applies formal verification approaches
> > > to the entirety of range tracking in the eBPF verifier. We posted a
> > > note to the eBPF mailing list about it sometime ago:
> > >
> > > [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
> > 
> > Oh, I totally missed this, as I just went on a long vacation a few
> > days before that and declared email bankruptcy afterwards. I'll try to
> > give it a read, though I see lots of math symbols there and make no
> > promises ;)
> 
> Feels the same when I start reading their previous work, but I can vouch
> their work their work are definitely worth the read. (Though I had to admit
> I secretly chant "math is easier than code, math is easier than code" to
> convincing my mind to not go into flight mode when seeing math symbols ;D

Hari et al. did a great job at explaining the intuitions throughout the
paper. So even if you skip the math, you should be able to follow.

Having an understanding of abstract interpretation helps. The Mozilla
wiki has a great one [1] and I wrote a shorter BPF example of it [2].

1 - https://wiki.mozilla.org/Abstract_Interpretation
2 - https://pchaigno.github.io/abstract-interpretation.html

> 
> > > Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
> > >
> > > [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
> > >
> > > Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> > > are working to get our tooling into a form that is integrable into BPF
> > > CI. We will look forward to your feedback when we post patches.
> > 
> > If this could be integrated in a way that we can regularly run this
> > and validate latest version of verifier, that would be great. I have a
> > second part of verifier changes coming up that extends range tracking
> > logic further to support range vs range (as opposed to range vs const
> > that we do currently) comparisons and is_branch_taken, so having
> > independent and formal verification of these changes would be great!

The current goal is to have this running somewhere regularly (maybe
releases + manual triggers) in a semi-automated fashion. The two
challenges today are the time it takes to run verification (days without
parallelization) and whether the bit of conversion & glue code will be
maintanable long term.

I'm fairly optimistic on the first as we're already down to hours with
basic parallelization. The second is harder to predict, but I guess your
patches will be a good exercice :)

I've already ran the verification on v6.0 to v6.3; v6.4 is currently
running. Hari et al. had verified v4.14 to v5.19 before. I'll give it a
try on this patchset afterward.

> 
> +1 (from a quick skim) this work is already great as-is, and it'd be even
> better once it get's in the CI. From the paper there's this
> 
>   We conducted our experiments on ... a machine with two 10-core Intel
>   Skylake CPUs running at 2.20 GHz with 192 GB of memory...
> 
> I suppose the memory requirement comes from the vast amount of state space
> that the Z3 SMT solver have to go through, and perhaps that poses a
> challenge for CI integration?
> 
> Just wondering is there are some low-hanging fruit the can make things
> easier for the SMT solver.

This is how much memory the system had, but it didn't use it all :)
When running the solver on a single core, I saw around 1GB of memory
usage. With my changes to run on several cores, it can grow to a few
GBs depending on the number of cores.

--
Paul

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

On Mon, Oct 23, 2023 at 8:52 AM Paul Chaignon <paul@isovalent.com> wrote:
>
> On Mon, Oct 23, 2023 at 10:05:41PM +0800, Shung-Hsi Yu wrote:
> > On Sat, Oct 21, 2023 at 09:42:46PM -0700, Andrii Nakryiko wrote:
> > > On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
> > > <sn624@cs.rutgers.edu> wrote:
> > > >
> > > > Hi all,
> > > >
> > > > Thanks, @Shung-Hsi, for bringing up this conversation about
> > > > integrating formal verification approaches into the BPF CI and testing.
> > > >
> > > > > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> > > > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > > > >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
>
> [...]
>
> > > > >>> FWIW an alternative approach that speeds things up is to use model checkers
> > > > >>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > > > >>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > > > >>> paper, but I somehow lost the link to their GitHub repository).
> > > > >>
> > > > >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> > > > >> Interpretation with Tristate Numbers"[1] can be found at
> > > > >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> > > > >>
> > > > >> Below is a truncated form of the above that only check tnum_add(), requires
> > > > >> a package called python3-z3 on most distros:
> > > > >
> > > > > Great! I'd be curious to see how range tracking logic can be encoded
> > > > > using this approach, please give it a go!
> > > >
> > > > We have some recent work that applies formal verification approaches
> > > > to the entirety of range tracking in the eBPF verifier. We posted a
> > > > note to the eBPF mailing list about it sometime ago:
> > > >
> > > > [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
> > >
> > > Oh, I totally missed this, as I just went on a long vacation a few
> > > days before that and declared email bankruptcy afterwards. I'll try to
> > > give it a read, though I see lots of math symbols there and make no
> > > promises ;)
> >
> > Feels the same when I start reading their previous work, but I can vouch
> > their work their work are definitely worth the read. (Though I had to admit
> > I secretly chant "math is easier than code, math is easier than code" to
> > convincing my mind to not go into flight mode when seeing math symbols ;D
>
> Hari et al. did a great job at explaining the intuitions throughout the
> paper. So even if you skip the math, you should be able to follow.
>
> Having an understanding of abstract interpretation helps. The Mozilla
> wiki has a great one [1] and I wrote a shorter BPF example of it [2].
>
> 1 - https://wiki.mozilla.org/Abstract_Interpretation
> 2 - https://pchaigno.github.io/abstract-interpretation.html
>

thanks :)

> >
> > > > Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
> > > >
> > > > [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
> > > >
> > > > Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> > > > are working to get our tooling into a form that is integrable into BPF
> > > > CI. We will look forward to your feedback when we post patches.
> > >
> > > If this could be integrated in a way that we can regularly run this
> > > and validate latest version of verifier, that would be great. I have a
> > > second part of verifier changes coming up that extends range tracking
> > > logic further to support range vs range (as opposed to range vs const
> > > that we do currently) comparisons and is_branch_taken, so having
> > > independent and formal verification of these changes would be great!
>
> The current goal is to have this running somewhere regularly (maybe
> releases + manual triggers) in a semi-automated fashion. The two
> challenges today are the time it takes to run verification (days without
> parallelization) and whether the bit of conversion & glue code will be
> maintanable long term.
>
> I'm fairly optimistic on the first as we're already down to hours with
> basic parallelization. The second is harder to predict, but I guess your
> patches will be a good exercice :)
>
> I've already ran the verification on v6.0 to v6.3; v6.4 is currently
> running. Hari et al. had verified v4.14 to v5.19 before. I'll give it a
> try on this patchset afterward.

Cool, that's great! The second part of this work will be generalizing
this logic in kernel to support range vs range comparisons, so I'd
appreciate it if you could validate that one as well. I'm finalizing
it, but will wait for this patch set to land first before posting
second part to have a proper CI testing runs (and limit amount of code
review to be done).

BTW, I've since did some more changes to this "selftests" to be a bit
more parallelizable, so this range_vs_consts set of tests now can run
in about 5 minutes on 8+ core QEMU instance. In the second part we'll
have range-vs-range, so we have about 106 million cases and it takes
slightly more than 8 hours single-threaded. But with parallelization,
it's done in slightly more than one hour.

So, of course, still too slow to run as part of normal test_progs run,
but definitely easy to run locally to validate kernel changes (and
probably makes sense to enable on some nightly CI runs, when we have
them).

Regardless, my point is that both methods of verification are
complementary, I think, and it's good to have both available and
working on latest kernel versions.


>
> >
> > +1 (from a quick skim) this work is already great as-is, and it'd be even
> > better once it get's in the CI. From the paper there's this
> >
> >   We conducted our experiments on ... a machine with two 10-core Intel
> >   Skylake CPUs running at 2.20 GHz with 192 GB of memory...
> >
> > I suppose the memory requirement comes from the vast amount of state space
> > that the Z3 SMT solver have to go through, and perhaps that poses a
> > challenge for CI integration?
> >
> > Just wondering is there are some low-hanging fruit the can make things
> > easier for the SMT solver.
>
> This is how much memory the system had, but it didn't use it all :)
> When running the solver on a single core, I saw around 1GB of memory
> usage. With my changes to run on several cores, it can grow to a few
> GBs depending on the number of cores.
>
> --
> Paul

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

On Mon, Oct 23, 2023 at 3:50 PM Andrii Nakryiko
<andrii.nakryiko@gmail.com> wrote:
>
> On Mon, Oct 23, 2023 at 8:52 AM Paul Chaignon <paul@isovalent.com> wrote:
> >
> > On Mon, Oct 23, 2023 at 10:05:41PM +0800, Shung-Hsi Yu wrote:
> > > On Sat, Oct 21, 2023 at 09:42:46PM -0700, Andrii Nakryiko wrote:
> > > > On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
> > > > <sn624@cs.rutgers.edu> wrote:
> > > > >
> > > > > Hi all,
> > > > >
> > > > > Thanks, @Shung-Hsi, for bringing up this conversation about
> > > > > integrating formal verification approaches into the BPF CI and testing.
> > > > >
> > > > > > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> > > > > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > > > > >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
> >
> > [...]
> >
> > > > > >>> FWIW an alternative approach that speeds things up is to use model checkers
> > > > > >>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > > > > >>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > > > > >>> paper, but I somehow lost the link to their GitHub repository).
> > > > > >>
> > > > > >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> > > > > >> Interpretation with Tristate Numbers"[1] can be found at
> > > > > >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> > > > > >>
> > > > > >> Below is a truncated form of the above that only check tnum_add(), requires
> > > > > >> a package called python3-z3 on most distros:
> > > > > >
> > > > > > Great! I'd be curious to see how range tracking logic can be encoded
> > > > > > using this approach, please give it a go!
> > > > >
> > > > > We have some recent work that applies formal verification approaches
> > > > > to the entirety of range tracking in the eBPF verifier. We posted a
> > > > > note to the eBPF mailing list about it sometime ago:
> > > > >
> > > > > [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
> > > >
> > > > Oh, I totally missed this, as I just went on a long vacation a few
> > > > days before that and declared email bankruptcy afterwards. I'll try to
> > > > give it a read, though I see lots of math symbols there and make no
> > > > promises ;)
> > >
> > > Feels the same when I start reading their previous work, but I can vouch
> > > their work their work are definitely worth the read. (Though I had to admit
> > > I secretly chant "math is easier than code, math is easier than code" to
> > > convincing my mind to not go into flight mode when seeing math symbols ;D
> >
> > Hari et al. did a great job at explaining the intuitions throughout the
> > paper. So even if you skip the math, you should be able to follow.
> >
> > Having an understanding of abstract interpretation helps. The Mozilla
> > wiki has a great one [1] and I wrote a shorter BPF example of it [2].
> >
> > 1 - https://wiki.mozilla.org/Abstract_Interpretation
> > 2 - https://pchaigno.github.io/abstract-interpretation.html
> >
>
> thanks :)

Hey Paul,

I had a bunch of time on the plane to catch up on reading, so I read
your blog post about PREVAIL among other things. Hopefully you don't
mind some comments posted here.

> Observation 1. The analysis must track binary relations among registers.

It's curious that the BPF verifier in kernel actually doesn't track
relations in this sense, and yet it works for lots and lots of
practical programs. :)


(Speaking of kernel verifier implementation)

> Third, it does not currently support programs with loops.

It does, and I'm not even talking about bounded loops that are
basically unrolled as many times as necessary. We have bpf_loop()
helper calling given callback as many times as requested, but even
better we now have open-coded iterators. Please check selftests using
bpf_for() macro.

Note that Eduard is fixing discovered issues in open-coded iterators
convergence checks and logic, but other than that BPF does have real
loops.


And about a confusing bit at the end:

>  0: r0 = 0
>  1: if r1 > 10 goto pc+4  // r1 ∈ [0; 10]
>  2: if r2 > 10 goto pc+3  // r2 ∈ [0; 10]
>  3: r1 *= r2              // r1 ∈ [0; 100]
>  4: if r1 != 5 goto pc+1
>  5: r1 /= r0              // Division by zero!
>  6: exit
>
> After instruction 2, both r1 and r2 have abstract value [0; 10].
> After instruction 3, r1 holds the multiplication of r1 and r2 and
> therefore has abstract value [0; 100]. When considering the condition at
>  instruction 4, because 11 ∈ [0; 100], we will walk both paths and hit the
>  division by zero.
>
> Except we know that r1 can never take value 11. The number 11 is a prime
>  number, so it is not a multiple of any integers between 0 and 10.

This made me pause for a while. I think you meant to have `4: if r1 !=
11 goto pc+1` and then go on to explain that you can't get 11 by
multiplying numbers in range [0; 10], because 11 is greater than 10
(so can't be 1 x 11), but also it's a prime number, so you can't get
it from multiplication of two integers. So please consider fixing up
the code example, and perhaps elaborate a bit more on why 11 can't
happen in actuality. This example does look a bit academic, but, well,
formal methods and stuff, it's fitting! ;)


> It’s a bit disappointing that the paper doesn’t include any comparison with the Linux verifier on the same corpus of BPF programs.

Indeed, I concur. It would be interesting to have this comparison as
of the most recent version of PREVAIL and Linux's BPF verifier.


Either way, thanks a lot for the very approachable and informative
blog post, it was a pleasure to read! Great work!


>
> > >
> > > > > Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
> > > > >
> > > > > [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
> > > > >
> > > > > Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> > > > > are working to get our tooling into a form that is integrable into BPF
> > > > > CI. We will look forward to your feedback when we post patches.
> > > >
> > > > If this could be integrated in a way that we can regularly run this
> > > > and validate latest version of verifier, that would be great. I have a
> > > > second part of verifier changes coming up that extends range tracking
> > > > logic further to support range vs range (as opposed to range vs const
> > > > that we do currently) comparisons and is_branch_taken, so having
> > > > independent and formal verification of these changes would be great!
> >
> > The current goal is to have this running somewhere regularly (maybe
> > releases + manual triggers) in a semi-automated fashion. The two
> > challenges today are the time it takes to run verification (days without
> > parallelization) and whether the bit of conversion & glue code will be
> > maintanable long term.
> >
> > I'm fairly optimistic on the first as we're already down to hours with
> > basic parallelization. The second is harder to predict, but I guess your
> > patches will be a good exercice :)
> >
> > I've already ran the verification on v6.0 to v6.3; v6.4 is currently
> > running. Hari et al. had verified v4.14 to v5.19 before. I'll give it a
> > try on this patchset afterward.
>
> Cool, that's great! The second part of this work will be generalizing
> this logic in kernel to support range vs range comparisons, so I'd
> appreciate it if you could validate that one as well. I'm finalizing
> it, but will wait for this patch set to land first before posting
> second part to have a proper CI testing runs (and limit amount of code
> review to be done).
>
> BTW, I've since did some more changes to this "selftests" to be a bit
> more parallelizable, so this range_vs_consts set of tests now can run
> in about 5 minutes on 8+ core QEMU instance. In the second part we'll
> have range-vs-range, so we have about 106 million cases and it takes
> slightly more than 8 hours single-threaded. But with parallelization,
> it's done in slightly more than one hour.
>
> So, of course, still too slow to run as part of normal test_progs run,
> but definitely easy to run locally to validate kernel changes (and
> probably makes sense to enable on some nightly CI runs, when we have
> them).
>
> Regardless, my point is that both methods of verification are
> complementary, I think, and it's good to have both available and
> working on latest kernel versions.
>
>
> >
> > >
> > > +1 (from a quick skim) this work is already great as-is, and it'd be even
> > > better once it get's in the CI. From the paper there's this
> > >
> > >   We conducted our experiments on ... a machine with two 10-core Intel
> > >   Skylake CPUs running at 2.20 GHz with 192 GB of memory...
> > >
> > > I suppose the memory requirement comes from the vast amount of state space
> > > that the Z3 SMT solver have to go through, and perhaps that poses a
> > > challenge for CI integration?
> > >
> > > Just wondering is there are some low-hanging fruit the can make things
> > > easier for the SMT solver.
> >
> > This is how much memory the system had, but it didn't use it all :)
> > When running the solver on a single core, I saw around 1GB of memory
> > usage. With my changes to run on several cores, it can grow to a few
> > GBs depending on the number of cores.
> >
> > --
> > Paul

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Paul Chaignon]

On Mon, Oct 23, 2023 at 10:51:57PM -0700, Andrii Nakryiko wrote:
> On Mon, Oct 23, 2023 at 3:50 PM Andrii Nakryiko
> <andrii.nakryiko@gmail.com> wrote:
> >
> > On Mon, Oct 23, 2023 at 8:52 AM Paul Chaignon <paul@isovalent.com> wrote:
> > >
> > > On Mon, Oct 23, 2023 at 10:05:41PM +0800, Shung-Hsi Yu wrote:
> > > > On Sat, Oct 21, 2023 at 09:42:46PM -0700, Andrii Nakryiko wrote:
> > > > > On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
> > > > > <sn624@cs.rutgers.edu> wrote:
> > > > > >
> > > > > > Hi all,
> > > > > >
> > > > > > Thanks, @Shung-Hsi, for bringing up this conversation about
> > > > > > integrating formal verification approaches into the BPF CI and testing.
> > > > > >
> > > > > > > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> > > > > > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > > > > > >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
> > >
> > > [...]
> > >
> > > > > > >>> FWIW an alternative approach that speeds things up is to use model checkers
> > > > > > >>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > > > > > >>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > > > > > >>> paper, but I somehow lost the link to their GitHub repository).
> > > > > > >>
> > > > > > >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> > > > > > >> Interpretation with Tristate Numbers"[1] can be found at
> > > > > > >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> > > > > > >>
> > > > > > >> Below is a truncated form of the above that only check tnum_add(), requires
> > > > > > >> a package called python3-z3 on most distros:
> > > > > > >
> > > > > > > Great! I'd be curious to see how range tracking logic can be encoded
> > > > > > > using this approach, please give it a go!
> > > > > >
> > > > > > We have some recent work that applies formal verification approaches
> > > > > > to the entirety of range tracking in the eBPF verifier. We posted a
> > > > > > note to the eBPF mailing list about it sometime ago:
> > > > > >
> > > > > > [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
> > > > >
> > > > > Oh, I totally missed this, as I just went on a long vacation a few
> > > > > days before that and declared email bankruptcy afterwards. I'll try to
> > > > > give it a read, though I see lots of math symbols there and make no
> > > > > promises ;)
> > > >
> > > > Feels the same when I start reading their previous work, but I can vouch
> > > > their work their work are definitely worth the read. (Though I had to admit
> > > > I secretly chant "math is easier than code, math is easier than code" to
> > > > convincing my mind to not go into flight mode when seeing math symbols ;D
> > >
> > > Hari et al. did a great job at explaining the intuitions throughout the
> > > paper. So even if you skip the math, you should be able to follow.
> > >
> > > Having an understanding of abstract interpretation helps. The Mozilla
> > > wiki has a great one [1] and I wrote a shorter BPF example of it [2].
> > >
> > > 1 - https://wiki.mozilla.org/Abstract_Interpretation
> > > 2 - https://pchaigno.github.io/abstract-interpretation.html
> > >
> >
> > thanks :)
> 
> Hey Paul,
> 
> I had a bunch of time on the plane to catch up on reading, so I read
> your blog post about PREVAIL among other things. Hopefully you don't
> mind some comments posted here.
> 
> > Observation 1. The analysis must track binary relations among registers.
> 
> It's curious that the BPF verifier in kernel actually doesn't track
> relations in this sense, and yet it works for lots and lots of
> practical programs. :)

It kind of does, but only for the types where it's actually needed. For
example if we have:

  3: (bf) r3 = r1
  4: (07) r3 += 14
  5: (2d) if r3 > r2 goto pc+50
   R1_w=pkt(id=0,off=0,r=14,imm=0) R2_w=pkt_end(id=0,off=0,imm=0)
     R3_w=pkt(id=0,off=14,r=14,imm=0)

R1's range actually refers to the relationship to pkt_end, R2 at this
point. So, R1's r=14 carries the same information as R1 + 14 <= R2.

A big difference is that the Linux verifier is very tailored to eBPF. So
it doesn't perform this sort of more complicated tracking for all
registers and slack slots. I suspect that plays a bit role in the lower
performance of PREVAIL.

> 
> 
> (Speaking of kernel verifier implementation)
> 
> > Third, it does not currently support programs with loops.
> 
> It does, and I'm not even talking about bounded loops that are
> basically unrolled as many times as necessary. We have bpf_loop()
> helper calling given callback as many times as requested, but even
> better we now have open-coded iterators. Please check selftests using
> bpf_for() macro.
> 
> Note that Eduard is fixing discovered issues in open-coded iterators
> convergence checks and logic, but other than that BPF does have real
> loops.

I'll fix that. I also wasn't aware of the more recent bpf_for. Nice!

The larger point is that PREVAIL is able to fully verify free-form
loops. It doesn't impose a structure or rely on trusted code (helpers
and kfuncs).
In the end, I don't think it matters much. The amount of trusted code
for this is small and well understood. And we probably don't want
ill-structured loops in our C code anyway. But the lack of loop support
used to take a lot of attention when speaking of the BPF verifier, so I
guess that's why it ended up being a selling point in the paper.

> 
> 
> And about a confusing bit at the end:
> 
> >  0: r0 = 0
> >  1: if r1 > 10 goto pc+4  // r1 ∈ [0; 10]
> >  2: if r2 > 10 goto pc+3  // r2 ∈ [0; 10]
> >  3: r1 *= r2              // r1 ∈ [0; 100]
> >  4: if r1 != 5 goto pc+1
> >  5: r1 /= r0              // Division by zero!
> >  6: exit
> >
> > After instruction 2, both r1 and r2 have abstract value [0; 10].
> > After instruction 3, r1 holds the multiplication of r1 and r2 and
> > therefore has abstract value [0; 100]. When considering the condition at
> >  instruction 4, because 11 ∈ [0; 100], we will walk both paths and hit the
> >  division by zero.
> >
> > Except we know that r1 can never take value 11. The number 11 is a prime
> >  number, so it is not a multiple of any integers between 0 and 10.
> 
> This made me pause for a while. I think you meant to have `4: if r1 !=
> 11 goto pc+1` and then go on to explain that you can't get 11 by
> multiplying numbers in range [0; 10], because 11 is greater than 10
> (so can't be 1 x 11), but also it's a prime number, so you can't get
> it from multiplication of two integers. So please consider fixing up
> the code example, and perhaps elaborate a bit more on why 11 can't
> happen in actuality. This example does look a bit academic, but, well,
> formal methods and stuff, it's fitting! ;)

You're absolutely right. It should be 11 instead of 5. That's what I get
for changing the ranges from [0; 4] to [0; 10] at the last minute.

> 
> 
> > It’s a bit disappointing that the paper doesn’t include any comparison with the Linux verifier on the same corpus of BPF programs.
> 
> Indeed, I concur. It would be interesting to have this comparison as
> of the most recent version of PREVAIL and Linux's BPF verifier.
> 
> 
> Either way, thanks a lot for the very approachable and informative
> blog post, it was a pleasure to read! Great work!

Thanks for the read and the review! I like reading about what academia
is doing around BPF so certainly not my last post on those topics :)

> 
> 
> >
> > > >
> > > > > > Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
> > > > > >
> > > > > > [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
> > > > > >
> > > > > > Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> > > > > > are working to get our tooling into a form that is integrable into BPF
> > > > > > CI. We will look forward to your feedback when we post patches.
> > > > >
> > > > > If this could be integrated in a way that we can regularly run this
> > > > > and validate latest version of verifier, that would be great. I have a
> > > > > second part of verifier changes coming up that extends range tracking
> > > > > logic further to support range vs range (as opposed to range vs const
> > > > > that we do currently) comparisons and is_branch_taken, so having
> > > > > independent and formal verification of these changes would be great!
> > >
> > > The current goal is to have this running somewhere regularly (maybe
> > > releases + manual triggers) in a semi-automated fashion. The two
> > > challenges today are the time it takes to run verification (days without
> > > parallelization) and whether the bit of conversion & glue code will be
> > > maintanable long term.
> > >
> > > I'm fairly optimistic on the first as we're already down to hours with
> > > basic parallelization. The second is harder to predict, but I guess your
> > > patches will be a good exercice :)
> > >
> > > I've already ran the verification on v6.0 to v6.3; v6.4 is currently
> > > running. Hari et al. had verified v4.14 to v5.19 before. I'll give it a
> > > try on this patchset afterward.
> >
> > Cool, that's great! The second part of this work will be generalizing
> > this logic in kernel to support range vs range comparisons, so I'd
> > appreciate it if you could validate that one as well. I'm finalizing
> > it, but will wait for this patch set to land first before posting
> > second part to have a proper CI testing runs (and limit amount of code
> > review to be done).

Happy to!

> >
> > BTW, I've since did some more changes to this "selftests" to be a bit
> > more parallelizable, so this range_vs_consts set of tests now can run
> > in about 5 minutes on 8+ core QEMU instance. In the second part we'll
> > have range-vs-range, so we have about 106 million cases and it takes
> > slightly more than 8 hours single-threaded. But with parallelization,
> > it's done in slightly more than one hour.
> >
> > So, of course, still too slow to run as part of normal test_progs run,
> > but definitely easy to run locally to validate kernel changes (and
> > probably makes sense to enable on some nightly CI runs, when we have
> > them).
> >
> > Regardless, my point is that both methods of verification are
> > complementary, I think, and it's good to have both available and
> > working on latest kernel versions.

Completely agree!

> >
> >
> > >
> > > >
> > > > +1 (from a quick skim) this work is already great as-is, and it'd be even
> > > > better once it get's in the CI. From the paper there's this
> > > >
> > > >   We conducted our experiments on ... a machine with two 10-core Intel
> > > >   Skylake CPUs running at 2.20 GHz with 192 GB of memory...
> > > >
> > > > I suppose the memory requirement comes from the vast amount of state space
> > > > that the Z3 SMT solver have to go through, and perhaps that poses a
> > > > challenge for CI integration?
> > > >
> > > > Just wondering is there are some low-hanging fruit the can make things
> > > > easier for the SMT solver.
> > >
> > > This is how much memory the system had, but it didn't use it all :)
> > > When running the solver on a single core, I saw around 1GB of memory
> > > usage. With my changes to run on several cores, it can grow to a few
> > > GBs depending on the number of cores.
> > >
> > > --
> > > Paul

Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester

[Andrii Nakryiko]

On Tue, Oct 24, 2023 at 2:26 PM Paul Chaignon <paul.chaignon@gmail.com> wrote:
>
> On Mon, Oct 23, 2023 at 10:51:57PM -0700, Andrii Nakryiko wrote:
> > On Mon, Oct 23, 2023 at 3:50 PM Andrii Nakryiko
> > <andrii.nakryiko@gmail.com> wrote:
> > >
> > > On Mon, Oct 23, 2023 at 8:52 AM Paul Chaignon <paul@isovalent.com> wrote:
> > > >
> > > > On Mon, Oct 23, 2023 at 10:05:41PM +0800, Shung-Hsi Yu wrote:
> > > > > On Sat, Oct 21, 2023 at 09:42:46PM -0700, Andrii Nakryiko wrote:
> > > > > > On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
> > > > > > <sn624@cs.rutgers.edu> wrote:
> > > > > > >
> > > > > > > Hi all,
> > > > > > >
> > > > > > > Thanks, @Shung-Hsi, for bringing up this conversation about
> > > > > > > integrating formal verification approaches into the BPF CI and testing.
> > > > > > >
> > > > > > > > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> > > > > > > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > > > > > > >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu wrote:
> > > >
> > > > [...]
> > > >
> > > > > > > >>> FWIW an alternative approach that speeds things up is to use model checkers
> > > > > > > >>> like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > > > > > > >>> possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > > > > > > >>> paper, but I somehow lost the link to their GitHub repository).
> > > > > > > >>
> > > > > > > >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> > > > > > > >> Interpretation with Tristate Numbers"[1] can be found at
> > > > > > > >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> > > > > > > >>
> > > > > > > >> Below is a truncated form of the above that only check tnum_add(), requires
> > > > > > > >> a package called python3-z3 on most distros:
> > > > > > > >
> > > > > > > > Great! I'd be curious to see how range tracking logic can be encoded
> > > > > > > > using this approach, please give it a go!
> > > > > > >
> > > > > > > We have some recent work that applies formal verification approaches
> > > > > > > to the entirety of range tracking in the eBPF verifier. We posted a
> > > > > > > note to the eBPF mailing list about it sometime ago:
> > > > > > >
> > > > > > > [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
> > > > > >
> > > > > > Oh, I totally missed this, as I just went on a long vacation a few
> > > > > > days before that and declared email bankruptcy afterwards. I'll try to
> > > > > > give it a read, though I see lots of math symbols there and make no
> > > > > > promises ;)
> > > > >
> > > > > Feels the same when I start reading their previous work, but I can vouch
> > > > > their work their work are definitely worth the read. (Though I had to admit
> > > > > I secretly chant "math is easier than code, math is easier than code" to
> > > > > convincing my mind to not go into flight mode when seeing math symbols ;D
> > > >
> > > > Hari et al. did a great job at explaining the intuitions throughout the
> > > > paper. So even if you skip the math, you should be able to follow.
> > > >
> > > > Having an understanding of abstract interpretation helps. The Mozilla
> > > > wiki has a great one [1] and I wrote a shorter BPF example of it [2].
> > > >
> > > > 1 - https://wiki.mozilla.org/Abstract_Interpretation
> > > > 2 - https://pchaigno.github.io/abstract-interpretation.html
> > > >
> > >
> > > thanks :)
> >
> > Hey Paul,
> >
> > I had a bunch of time on the plane to catch up on reading, so I read
> > your blog post about PREVAIL among other things. Hopefully you don't
> > mind some comments posted here.
> >
> > > Observation 1. The analysis must track binary relations among registers.
> >
> > It's curious that the BPF verifier in kernel actually doesn't track
> > relations in this sense, and yet it works for lots and lots of
> > practical programs. :)
>
> It kind of does, but only for the types where it's actually needed. For
> example if we have:
>
>   3: (bf) r3 = r1
>   4: (07) r3 += 14
>   5: (2d) if r3 > r2 goto pc+50
>    R1_w=pkt(id=0,off=0,r=14,imm=0) R2_w=pkt_end(id=0,off=0,imm=0)
>      R3_w=pkt(id=0,off=14,r=14,imm=0)
>
> R1's range actually refers to the relationship to pkt_end, R2 at this
> point. So, R1's r=14 carries the same information as R1 + 14 <= R2.
>
> A big difference is that the Linux verifier is very tailored to eBPF. So
> it doesn't perform this sort of more complicated tracking for all
> registers and slack slots. I suspect that plays a bit role in the lower
> performance of PREVAIL.
>

Yes, PACKET_END is a special case, so you are right. I had
SCALAR_VALUE registers in mind, and for those we don't track
relationships (even if in some cases that could help with some
compiler optimizations).

> >
> >
> > (Speaking of kernel verifier implementation)
> >
> > > Third, it does not currently support programs with loops.
> >
> > It does, and I'm not even talking about bounded loops that are
> > basically unrolled as many times as necessary. We have bpf_loop()
> > helper calling given callback as many times as requested, but even
> > better we now have open-coded iterators. Please check selftests using
> > bpf_for() macro.
> >
> > Note that Eduard is fixing discovered issues in open-coded iterators
> > convergence checks and logic, but other than that BPF does have real
> > loops.
>
> I'll fix that. I also wasn't aware of the more recent bpf_for. Nice!
>
> The larger point is that PREVAIL is able to fully verify free-form
> loops. It doesn't impose a structure or rely on trusted code (helpers
> and kfuncs).
> In the end, I don't think it matters much. The amount of trusted code
> for this is small and well understood. And we probably don't want
> ill-structured loops in our C code anyway. But the lack of loop support
> used to take a lot of attention when speaking of the BPF verifier, so I
> guess that's why it ended up being a selling point in the paper.

Yeah, I get that. I only pointed this out because your blog post
written in September of 2023 will be read by someone and they will
think that BPF verifier still doesn't support loops, which is not true
:) So it would be nice to point out that this is possible.

>
> >
> >
> > And about a confusing bit at the end:
> >
> > >  0: r0 = 0
> > >  1: if r1 > 10 goto pc+4  // r1 ∈ [0; 10]
> > >  2: if r2 > 10 goto pc+3  // r2 ∈ [0; 10]
> > >  3: r1 *= r2              // r1 ∈ [0; 100]
> > >  4: if r1 != 5 goto pc+1
> > >  5: r1 /= r0              // Division by zero!
> > >  6: exit
> > >
> > > After instruction 2, both r1 and r2 have abstract value [0; 10].
> > > After instruction 3, r1 holds the multiplication of r1 and r2 and
> > > therefore has abstract value [0; 100]. When considering the condition at
> > >  instruction 4, because 11 ∈ [0; 100], we will walk both paths and hit the
> > >  division by zero.
> > >
> > > Except we know that r1 can never take value 11. The number 11 is a prime
> > >  number, so it is not a multiple of any integers between 0 and 10.
> >
> > This made me pause for a while. I think you meant to have `4: if r1 !=
> > 11 goto pc+1` and then go on to explain that you can't get 11 by
> > multiplying numbers in range [0; 10], because 11 is greater than 10
> > (so can't be 1 x 11), but also it's a prime number, so you can't get
> > it from multiplication of two integers. So please consider fixing up
> > the code example, and perhaps elaborate a bit more on why 11 can't
> > happen in actuality. This example does look a bit academic, but, well,
> > formal methods and stuff, it's fitting! ;)
>
> You're absolutely right. It should be 11 instead of 5. That's what I get
> for changing the ranges from [0; 4] to [0; 10] at the last minute.
>
> >
> >
> > > It’s a bit disappointing that the paper doesn’t include any comparison with the Linux verifier on the same corpus of BPF programs.
> >
> > Indeed, I concur. It would be interesting to have this comparison as
> > of the most recent version of PREVAIL and Linux's BPF verifier.
> >
> >
> > Either way, thanks a lot for the very approachable and informative
> > blog post, it was a pleasure to read! Great work!
>
> Thanks for the read and the review! I like reading about what academia
> is doing around BPF so certainly not my last post on those topics :)
>
> >
> >
> > >
> > > > >
> > > > > > > Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
> > > > > > >
> > > > > > > [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
> > > > > > >
> > > > > > > Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> > > > > > > are working to get our tooling into a form that is integrable into BPF
> > > > > > > CI. We will look forward to your feedback when we post patches.
> > > > > >
> > > > > > If this could be integrated in a way that we can regularly run this
> > > > > > and validate latest version of verifier, that would be great. I have a
> > > > > > second part of verifier changes coming up that extends range tracking
> > > > > > logic further to support range vs range (as opposed to range vs const
> > > > > > that we do currently) comparisons and is_branch_taken, so having
> > > > > > independent and formal verification of these changes would be great!
> > > >
> > > > The current goal is to have this running somewhere regularly (maybe
> > > > releases + manual triggers) in a semi-automated fashion. The two
> > > > challenges today are the time it takes to run verification (days without
> > > > parallelization) and whether the bit of conversion & glue code will be
> > > > maintanable long term.
> > > >
> > > > I'm fairly optimistic on the first as we're already down to hours with
> > > > basic parallelization. The second is harder to predict, but I guess your
> > > > patches will be a good exercice :)
> > > >
> > > > I've already ran the verification on v6.0 to v6.3; v6.4 is currently
> > > > running. Hari et al. had verified v4.14 to v5.19 before. I'll give it a
> > > > try on this patchset afterward.
> > >
> > > Cool, that's great! The second part of this work will be generalizing
> > > this logic in kernel to support range vs range comparisons, so I'd
> > > appreciate it if you could validate that one as well. I'm finalizing
> > > it, but will wait for this patch set to land first before posting
> > > second part to have a proper CI testing runs (and limit amount of code
> > > review to be done).
>
> Happy to!

I'm planning to post all my changes as one series in a few days, so
maybe you can take it for a spin at that point?

>
> > >
> > > BTW, I've since did some more changes to this "selftests" to be a bit
> > > more parallelizable, so this range_vs_consts set of tests now can run
> > > in about 5 minutes on 8+ core QEMU instance. In the second part we'll
> > > have range-vs-range, so we have about 106 million cases and it takes
> > > slightly more than 8 hours single-threaded. But with parallelization,
> > > it's done in slightly more than one hour.
> > >
> > > So, of course, still too slow to run as part of normal test_progs run,
> > > but definitely easy to run locally to validate kernel changes (and
> > > probably makes sense to enable on some nightly CI runs, when we have
> > > them).
> > >
> > > Regardless, my point is that both methods of verification are
> > > complementary, I think, and it's good to have both available and
> > > working on latest kernel versions.
>
> Completely agree!
>
> > >
> > >
> > > >
> > > > >
> > > > > +1 (from a quick skim) this work is already great as-is, and it'd be even
> > > > > better once it get's in the CI. From the paper there's this
> > > > >
> > > > >   We conducted our experiments on ... a machine with two 10-core Intel
> > > > >   Skylake CPUs running at 2.20 GHz with 192 GB of memory...
> > > > >
> > > > > I suppose the memory requirement comes from the vast amount of state space
> > > > > that the Z3 SMT solver have to go through, and perhaps that poses a
> > > > > challenge for CI integration?
> > > > >
> > > > > Just wondering is there are some low-hanging fruit the can make things
> > > > > easier for the SMT solver.
> > > >
> > > > This is how much memory the system had, but it didn't use it all :)
> > > > When running the solver on a single core, I saw around 1GB of memory
> > > > usage. With my changes to run on several cores, it can grow to a few
> > > > GBs depending on the number of cores.
> > > >
> > > > --
> > > > Paul