[PATCH v2 bpf 0/4] Fix invariant violation for single-value tnums

[PATCH v2 bpf 0/4] Fix invariant violation for single-value tnums

[Paul Chaignon]

We're hitting an invariant violation in Cilium that sometimes leads to
BPF programs being rejected and Cilium failing to start [1]. As far as
I know this is the first case of invariant violation found in a real
program (i.e., not by a fuzzer). The following extract from verifier
logs shows what's happening:

  from 201 to 236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
  236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
  ; if (magic == MARK_MAGIC_HOST || magic == MARK_MAGIC_OVERLAY || magic == MARK_MAGIC_ENCRYPT) @ bpf_host.c:1337
  236: (16) if w9 == 0xe00 goto pc+45   ; R9=scalar(smin=umin=smin32=umin32=3585,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100))
  237: (16) if w9 == 0xf00 goto pc+1
  verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xe01, 0xe00] s64=[0xe01, 0xe00] u32=[0xe01, 0xe00] s32=[0xe01, 0xe00] var_off=(0xe00, 0x0)

More details are given in the second patch, but in short, the verifier
should be able to detect that the false branch of instruction 237 is
never true. After instruction 236, the u64 range and the tnum overlap
in a single value, 0xf00.

The long-term solution to invariant violation is likely to rely on the
refinement + invariant violation check to detect dead branches, as
started by Eduard. To fix the current issue, we need something with
less refactoring that we can backport to affected kernels.

The solution implemented in the second patch is to improve the bounds
refinement to avoid this case. It relies on a new tnum helper,
tnum_step, first sent as an RFC in [2]. The last two patches extend and
update the selftests.

Link: https://github.com/cilium/cilium/issues/44216 [1]
Link: https://lore.kernel.org/bpf/20251107192328.2190680-2-harishankar.vishwanathan@gmail.com/ [2]

Changes in v2:
  - Add guard suggested by Hari in tnum_step, to avoid undefined
    behavior spotted by AI code review.
  - Add explanation diagrams in code as suggested by Eduard.
  - Rework conditions for readability as suggested by Eduard.
  - Updated reference to SMT formula.
  - Rebased.

Harishankar Vishwanathan (1):
  bpf: Introduce tnum_step to step through tnum's members

Paul Chaignon (3):
  bpf: Improve bounds when tnum has a single possible value
  selftests/bpf: Test refinement of single-value tnum
  selftests/bpf: Avoid simplification of crafted bounds test

 include/linux/tnum.h                          |  3 +
 kernel/bpf/tnum.c                             | 56 ++++++++++++
 kernel/bpf/verifier.c                         | 30 ++++++
 .../selftests/bpf/prog_tests/reg_bounds.c     |  2 +-
 .../selftests/bpf/progs/verifier_bounds.c     | 91 +++++++++++++++++++
 5 files changed, 181 insertions(+), 1 deletion(-)

-- 
2.43.0

[PATCH v2 bpf 1/4] bpf: Introduce tnum_step to step through tnum's members

[Paul Chaignon]

From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>

This commit introduces tnum_step(), a function that, when given t, and a
number z returns the smallest member of t larger than z. The number z
must be greater or equal to the smallest member of t and less than the
largest member of t.

The first step is to compute j, a number that keeps all of t's known
bits, and matches all unknown bits to z's bits. Since j is a member of
the t, it is already a candidate for result. However, we want our result
to be (minimally) greater than z.

There are only two possible cases:

(1) Case j <= z. In this case, we want to increase the value of j and
make it > z.
(2) Case j > z. In this case, we want to decrease the value of j while
keeping it > z.

(Case 1) j <= z

t = xx11x0x0
z = 10111101 (189)
j = 10111000 (184)
         ^
         k

(Case 1.1) Let's first consider the case where j < z. We will address j
== z later.

Since z > j, there had to be a bit position that was 1 in z and a 0 in
j, beyond which all positions of higher significance are equal in j and
z. Further, this position could not have been unknown in a, because the
unknown positions of a match z. This position had to be a 1 in z and
known 0 in t.

Let k be position of the most significant 1-to-0 flip. In our example, k
= 3 (starting the count at 1 at the least significant bit).  Setting (to
1) the unknown bits of t in positions of significance smaller than
k will not produce a result > z. Hence, we must set/unset the unknown
bits at positions of significance higher than k. Specifically, we look
for the next larger combination of 1s and 0s to place in those
positions, relative to the combination that exists in z. We can achieve
this by concatenating bits at unknown positions of t into an integer,
adding 1, and writing the bits of that result back into the
corresponding bit positions previously extracted from z.

>From our example, considering only positions of significance greater
than k:

t =  xx..x
z =  10..1
    +    1
     -----
     11..0

This is the exact combination 1s and 0s we need at the unknown bits of t
in positions of significance greater than k. Further, our result must
only increase the value minimally above z. Hence, unknown bits in
positions of significance smaller than k should remain 0. We finally
have,

result = 11110000 (240)

(Case 1.2) Now consider the case when j = z, for example

t = 1x1x0xxx
z = 10110100 (180)
j = 10110100 (180)

Matching the unknown bits of the t to the bits of z yielded exactly z.
To produce a number greater than z, we must set/unset the unknown bits
in t, and *all* the unknown bits of t candidates for being set/unset. We
can do this similar to Case 1.1, by adding 1 to the bits extracted from
the masked bit positions of z. Essentially, this case is equivalent to
Case 1.1, with k = 0.

t =  1x1x0xxx
z =  .0.1.100
    +       1
    ---------
     .0.1.101

This is the exact combination of bits needed in the unknown positions of
t. After recalling the known positions of t, we get

result = 10110101 (181)

(Case 2) j > z

t = x00010x1
z = 10000010 (130)
j = 10001011 (139)
	^
	k

Since j > z, there had to be a bit position which was 0 in z, and a 1 in
j, beyond which all positions of higher significance are equal in j and
z. This position had to be a 0 in z and known 1 in t. Let k be the
position of the most significant 0-to-1 flip. In our example, k = 4.

Because of the 0-to-1 flip at position k, a member of t can become
greater than z if the bits in positions greater than k are themselves >=
to z. To make that member *minimally* greater than z, the bits in
positions greater than k must be exactly = z. Hence, we simply match all
of t's unknown bits in positions more significant than k to z's bits. In
positions less significant than k, we set all t's unknown bits to 0
to retain minimality.

In our example, in positions of greater significance than k (=4),
t=x000. These positions are matched with z (1000) to produce 1000. In
positions of lower significance than k, t=10x1. All unknown bits are set
to 0 to produce 1001. The final result is:

result = 10001001 (137)

This concludes the computation for a result > z that is a member of t.

The procedure for tnum_step() in this commit implements the idea
described above. As a proof of correctness, we verified the algorithm
against a logical specification of tnum_step. The specification asserts
the following about the inputs t, z and output res that:

1. res is a member of t, and
2. res is strictly greater than z, and
3. there does not exist another value res2 such that
	3a. res2 is also a member of t, and
	3b. res2 is greater than z
	3c. res2 is smaller than res

We checked the implementation against this logical specification using
an SMT solver. The verification formula in SMTLIB format is available
at [1]. The verification returned an "unsat": indicating that no input
assignment exists for which the implementation and the specification
produce different outputs.

In addition, we also automatically generated the logical encoding of the
C implementation using Agni [2] and verified it against the same
specification. This verification also returned an "unsat", confirming
that the implementation is equivalent to the specification. The formula
for this check is also available at [3].

Link: https://pastebin.com/raw/2eRWbiit [1]
Link: https://github.com/bpfverif/agni [2]
Link: https://pastebin.com/raw/EztVbBJ2 [3]
Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
---
 include/linux/tnum.h |  3 +++
 kernel/bpf/tnum.c    | 56 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 59 insertions(+)

diff --git a/include/linux/tnum.h b/include/linux/tnum.h
index fa4654ffb621..ca2cfec8de08 100644
--- a/include/linux/tnum.h
+++ b/include/linux/tnum.h
@@ -131,4 +131,7 @@ static inline bool tnum_subreg_is_const(struct tnum a)
 	return !(tnum_subreg(a)).mask;
 }
 
+/* Returns the smallest member of t larger than z */
+u64 tnum_step(struct tnum t, u64 z);
+
 #endif /* _LINUX_TNUM_H */
diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
index 26fbfbb01700..4abc359b3db0 100644
--- a/kernel/bpf/tnum.c
+++ b/kernel/bpf/tnum.c
@@ -269,3 +269,59 @@ struct tnum tnum_bswap64(struct tnum a)
 {
 	return TNUM(swab64(a.value), swab64(a.mask));
 }
+
+/* Given tnum t, and a number z such that tmin <= z < tmax, where tmin
+ * is the smallest member of the t (= t.value) and tmax is the largest
+ * member of t (= t.value | t.mask), returns the smallest member of t
+ * larger than z.
+ *
+ * For example,
+ * t      = x11100x0
+ * z      = 11110001 (241)
+ * result = 11110010 (242)
+ *
+ * Note: if this function is called with z >= tmax, it just returns
+ * early with tmax; if this function is called with z < tmin, the
+ * algorithm already returns tmin.
+ */
+u64 tnum_step(struct tnum t, u64 z)
+{
+	u64 tmax, j, p, q, r, s, v, u, w, res;
+	u8 k;
+
+	tmax = t.value | t.mask;
+
+	/* if z >= largest member of t, return largest member of t */
+	if (z >= tmax)
+		return tmax;
+
+	/* if z < smallest member of t, return smallest member of t */
+	if (z < t.value)
+		return t.value;
+
+	/* keep t's known bits, and match all unknown bits to z */
+	j = t.value | (z & t.mask);
+
+	if (j > z) {
+		p = ~z & t.value & ~t.mask;
+		k = fls64(p); /* k is the most-significant 0-to-1 flip */
+		q = U64_MAX << k;
+		r = q & z; /* positions > k matched to z */
+		s = ~q & t.value; /* positions <= k matched to t.value */
+		v = r | s;
+		res = v;
+	} else {
+		p = z & ~t.value & ~t.mask;
+		k = fls64(p); /* k is the most-significant 1-to-0 flip */
+		q = U64_MAX << k;
+		r = q & t.mask & z; /* unknown positions > k, matched to z */
+		s = q & ~t.mask; /* known positions > k, set to 1 */
+		v = r | s;
+		/* add 1 to unknown positions > k to make value greater than z */
+		u = v + (1ULL << k);
+		/* extract bits in unknown positions > k from u, rest from t.value */
+		w = (u & t.mask) | t.value;
+		res = w;
+	}
+	return res;
+}
-- 
2.43.0

[PATCH v2 bpf 2/4] bpf: Improve bounds when tnum has a single possible value

[Paul Chaignon]

We're hitting an invariant violation in Cilium that sometimes leads to
BPF programs being rejected and Cilium failing to start [1]. The
following extract from verifier logs shows what's happening:

  from 201 to 236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
  236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
  ; if (magic == MARK_MAGIC_HOST || magic == MARK_MAGIC_OVERLAY || magic == MARK_MAGIC_ENCRYPT) @ bpf_host.c:1337
  236: (16) if w9 == 0xe00 goto pc+45   ; R9=scalar(smin=umin=smin32=umin32=3585,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100))
  237: (16) if w9 == 0xf00 goto pc+1
  verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xe01, 0xe00] s64=[0xe01, 0xe00] u32=[0xe01, 0xe00] s32=[0xe01, 0xe00] var_off=(0xe00, 0x0)

We reach instruction 236 with two possible values for R9, 0xe00 and
0xf00. This is perfectly reflected in the tnum, but of course the ranges
are less accurate and cover [0xe00; 0xf00]. Taking the fallthrough path
at instruction 236 allows the verifier to reduce the range to
[0xe01; 0xf00]. The tnum is however not updated.

With these ranges, at instruction 237, the verifier is not able to
deduce that R9 is always equal to 0xf00. Hence the fallthrough pass is
explored first, the verifier refines the bounds using the assumption
that R9 != 0xf00, and ends up with an invariant violation.

This pattern of impossible branch + bounds refinement is common to all
invariant violations seen so far. The long-term solution is likely to
rely on the refinement + invariant violation check to detect dead
branches, as started by Eduard. To fix the current issue, we need
something with less refactoring that we can backport.

This patch uses the tnum_step helper introduced in the previous patch to
detect the above situation. In particular, three cases are now detected
in the bounds refinement:

1. The u64 range and the tnum only overlap in umin.
   u64:  ---[xxxxxx]-----
   tnum: --xx----------x-

2. The u64 range and the tnum only overlap in the maximum value
   represented by the tnum, called tmax.
   u64:  ---[xxxxxx]-----
   tnum: xx-----x--------

3. The u64 range and the tnum only overlap in between umin (excluded)
   and umax.
   u64:  ---[xxxxxx]-----
   tnum: xx----x-------x-

To detect these three cases, we call tnum_step(tnum, umin), which
returns the largest member of the tnum greater than umin, called
tnum_next here. We're in case (1) if umin is part of the tnum and
tnum_next is greater than umax. We're in case (2) if umin is not part of
the tnum and tnum_next is equal to tmax. Finally, we're in case (3) if
umin is not part of the tnum, tnum_next is inferior or equal to umax,
and calling tnum_step a second time gives us a value past umax.

This change implements these three cases. With it, the above bytecode
looks as follows:

  0: (85) call bpf_get_prandom_u32#7    ; R0=scalar()
  1: (47) r0 |= 3584                    ; R0=scalar(smin=0x8000000000000e00,umin=umin32=3584,smin32=0x80000e00,var_off=(0xe00; 0xfffffffffffff1ff))
  2: (57) r0 &= 3840                    ; R0=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100))
  3: (15) if r0 == 0xe00 goto pc+2      ; R0=3840
  4: (15) if r0 == 0xf00 goto pc+1
  4: R0=3840
  6: (95) exit

In addition to the new selftests, this change was also verified with
Agni [3]. For the record, the raw SMT is available at [4]. The property
it verifies is that: If a concrete value x is contained in all input
abstract values, after __update_reg_bounds, it will continue to be
contained in all output abstract values.

Link: https://github.com/cilium/cilium/issues/44216 [1]
Link: https://pchaigno.github.io/test-verifier-complexity.html [2]
Link: https://github.com/bpfverif/agni [3]
Link: https://pastebin.com/raw/naCfaqNx [4]
Fixes: 0df1a55afa83 ("bpf: Warn on internal verifier errors")
Co-developed-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 kernel/bpf/verifier.c | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index dbaafb64d3bd..7eb6b94dfa11 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2379,6 +2379,9 @@ static void __update_reg32_bounds(struct bpf_reg_state *reg)
 
 static void __update_reg64_bounds(struct bpf_reg_state *reg)
 {
+	u64 tnum_next, tmax;
+	bool umin_in_tnum;
+
 	/* min signed is max(sign bit) | min(other bits) */
 	reg->smin_value = max_t(s64, reg->smin_value,
 				reg->var_off.value | (reg->var_off.mask & S64_MIN));
@@ -2388,6 +2391,33 @@ static void __update_reg64_bounds(struct bpf_reg_state *reg)
 	reg->umin_value = max(reg->umin_value, reg->var_off.value);
 	reg->umax_value = min(reg->umax_value,
 			      reg->var_off.value | reg->var_off.mask);
+
+	/* Check if u64 and tnum overlap in a single value */
+	tnum_next = tnum_step(reg->var_off, reg->umin_value);
+	umin_in_tnum = (reg->umin_value & ~reg->var_off.mask) == reg->var_off.value;
+	tmax = reg->var_off.value | reg->var_off.mask;
+	if (umin_in_tnum && tnum_next > reg->umax_value) {
+		/* The u64 range and the tnum only overlap in umin.
+		 * u64:  ---[xxxxxx]-----
+		 * tnum: --xx----------x-
+		 */
+		___mark_reg_known(reg, reg->umin_value);
+	} else if (!umin_in_tnum && tnum_next == tmax) {
+		/* The u64 range and the tnum only overlap in the maximum value
+		 * represented by the tnum, called tmax.
+		 * u64:  ---[xxxxxx]-----
+		 * tnum: xx-----x--------
+		 */
+		___mark_reg_known(reg, tmax);
+	} else if (!umin_in_tnum && tnum_next <= reg->umax_value &&
+		   tnum_step(reg->var_off, tnum_next) > reg->umax_value) {
+		/* The u64 range and the tnum only overlap in between umin
+		 * (excluded) and umax.
+		 * u64:  ---[xxxxxx]-----
+		 * tnum: xx----x-------x-
+		 */
+		___mark_reg_known(reg, tnum_next);
+	}
 }
 
 static void __update_reg_bounds(struct bpf_reg_state *reg)
-- 
2.43.0

[PATCH v2 bpf 3/4] selftests/bpf: Test refinement of single-value tnum

[Paul Chaignon]

This patch introduces selftests to cover the new bounds refinement
logic introduced in the previous patch. Without the previous patch,
the first two tests fail because of the invariant violation they
trigger. The last test fails because the R10 access is not detected as
dead code. In addition, all tests fail because of R0 having a
non-constant value in the verifier logs.

Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 .../selftests/bpf/progs/verifier_bounds.c     | 91 +++++++++++++++++++
 1 file changed, 91 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index 560531404bce..41dd249faadd 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -1863,4 +1863,95 @@ l1_%=:	r0 = 1;				\
 	: __clobber_all);
 }
 
+/* This test covers the bounds deduction when the u64 range and the tnum
+ * overlap only at umax. After instruction 3, the ranges look as follows:
+ *
+ * 0    umin=0xe01     umax=0xf00                              U64_MAX
+ * |    [xxxxxxxxxxxxxx]                                       |
+ * |----------------------------|------------------------------|
+ * |   x               x                                       | tnum values
+ *
+ * The verifier can therefore deduce that the R0=0xf00=3840.
+ */
+SEC("socket")
+__description("bounds refinement with single-value tnum on umax")
+__msg("3: (15) if r0 == 0xe00 {{.*}} R0=3840")
+__success __log_level(2)
+__flag(BPF_F_TEST_REG_INVARIANTS)
+__naked void bounds_refinement_tnum_umax(void *ctx)
+{
+	asm volatile("			\
+	call %[bpf_get_prandom_u32];	\
+	r0 |= 0xe00;			\
+	r0 &= 0xf00;			\
+	if r0 == 0xe00 goto +2;		\
+	if r0 == 0xf00 goto +1;		\
+	r0 = 0;				\
+	exit;				\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
+/* This test covers the bounds deduction when the u64 range and the tnum
+ * overlap only at umin. After instruction 3, the ranges look as follows:
+ *
+ * 0    umin=0xe00     umax=0xeff                              U64_MAX
+ * |    [xxxxxxxxxxxxxx]                                       |
+ * |----------------------------|------------------------------|
+ * |    x               x                                      | tnum values
+ *
+ * The verifier can therefore deduce that the R0=0xe00=3584.
+ */
+SEC("socket")
+__description("bounds refinement with single-value tnum on umin")
+__msg("3: (15) if r0 == 0xf00 {{.*}} R0=3584")
+__success __log_level(2)
+__flag(BPF_F_TEST_REG_INVARIANTS)
+__naked void bounds_refinement_tnum_umin(void *ctx)
+{
+	asm volatile("			\
+	call %[bpf_get_prandom_u32];	\
+	r0 |= 0xe00;			\
+	r0 &= 0xf00;			\
+	if r0 == 0xf00 goto +2;		\
+	if r0 == 0xe00 goto +1;		\
+	r0 = 0;				\
+	exit;				\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
+/* This test covers the bounds deduction when the only possible tnum value is
+ * in the middle of the u64 range. After instruction 3, the ranges look as
+ * follows:
+ *
+ * 0    umin=0x7cf     umax=0x7df                              U64_MAX
+ * |    [xxxxxxxxxxxxxx]                                       |
+ * |----------------------------|------------------------------|
+ * |      x            x            x            x            x| tnum values
+ *
+ * The verifier can therefore deduce that the R0=0x7d0=2000. Instruction 5 is
+ * therefore dead code.
+ */
+SEC("socket")
+__description("bounds refinement with single-value tnum in middle of range")
+__msg("3: (a5) if r0 < 0x7cf {{.*}} R0=2000")
+__success __log_level(2)
+__naked void bounds_refinement_tnum_middle(void *ctx)
+{
+	asm volatile("			\
+	call %[bpf_get_prandom_u32];	\
+	if r0 & 0x0f goto +4;		\
+	if r0 > 0x7df goto +3;		\
+	if r0 < 0x7cf goto +2;		\
+	if r0 == 0x7d0 goto +1;		\
+	r10 = 0;			\
+	exit;				\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.43.0

[PATCH v2 bpf 4/4] selftests/bpf: Avoid simplification of crafted bounds test

[Paul Chaignon]

The reg_bounds_crafted tests validate the verifier's range analysis
logic. They focus on the actual ranges and thus ignore the tnum. As a
consequence, they carry the assumption that the tested cases can be
reproduced in userspace without using the tnum information.

Unfortunately, the previous change the refinement logic breaks that
assumption for one test case:

  (u64)2147483648 (u32)<op> [4294967294; 0x100000000]

The tested bytecode is shown below. Without our previous improvement, on
the false branch of the condition, R7 is only known to have u64 range
[0xfffffffe; 0x100000000]. With our improvement, and using the tnum
information, we can deduce that R7 equals 0x100000000.

  19: (bc) w0 = w6                ; R6=0x80000000
  20: (bc) w0 = w7                ; R7=scalar(smin=umin=0xfffffffe,smax=umax=0x100000000,smin32=-2,smax32=0,var_off=(0x0; 0x1ffffffff))
  21: (be) if w6 <= w7 goto pc+3  ; R6=0x80000000 R7=0x100000000

R7's tnum is (0; 0x1ffffffff). On the false branch, regs_refine_cond_op
refines R7's u32 range to [0; 0x7fffffff]. Then, __reg32_deduce_bounds
refines the s32 range to 0 using u32 and finally also sets u32=0.
From this, __reg_bound_offset improves the tnum to (0; 0x100000000).
Finally, our previous patch uses this new tnum to deduce that it only
intersect with u64=[0xfffffffe; 0x100000000] in a single value:
0x100000000.

Because the verifier uses the tnum to reach this constant value, the
selftest is unable to reproduce it by only simulating ranges. The
solution implemented in this patch is to change the test case such that
there is more than one overlap value between u64 and the tnum. The max.
u64 value is thus changed from 0x100000000 to 0x300000000.

Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 tools/testing/selftests/bpf/prog_tests/reg_bounds.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
index d93a0c7b1786..0322f817d07b 100644
--- a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
+++ b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c
@@ -2091,7 +2091,7 @@ static struct subtest_case crafted_cases[] = {
 	{U64, S64, {0, 0xffffffffULL}, {0x7fffffff, 0x7fffffff}},
 
 	{U64, U32, {0, 0x100000000}, {0, 0}},
-	{U64, U32, {0xfffffffe, 0x100000000}, {0x80000000, 0x80000000}},
+	{U64, U32, {0xfffffffe, 0x300000000}, {0x80000000, 0x80000000}},
 
 	{U64, S32, {0, 0xffffffff00000000ULL}, {0, 0}},
 	/* these are tricky cases where lower 32 bits allow to tighten 64
-- 
2.43.0

Re: [PATCH v2 bpf 2/4] bpf: Improve bounds when tnum has a single possible value

[bot+bpf-ci]

[-- Attachment #1: Type: text/plain, Size: 1065 bytes --]

> To detect these three cases, we call tnum_step(tnum, umin), which
> returns the largest member of the tnum greater than umin, called
          ^^^^^^^
The tnum_step() comment in tnum.c and the header in tnum.h both say
"returns the smallest member of t larger than z."  Should "largest" be
"smallest" here?


---
AI reviewed your patch. Please fix the bug or email reply why it's not a bug.
See: https://github.com/kernel-patches/vmtest/blob/master/ci/claude/README.md

CI run summary: https://github.com/kernel-patches/bpf/actions/runs/22227142197

AI-authorship-score: low
AI-authorship-explanation: Detailed real-world bug context from Cilium, co-developed with academic researchers at Rutgers using formal SMT verification, domain-specific verifier terminology used naturally; consistent with experienced kernel developer.
issues-found: 1
issue-severity-score: low
issue-severity-explanation: Commit message incorrectly describes tnum_step as returning the largest member when it returns the smallest; documentation error only with no code or runtime impact.

Re: [PATCH v2 bpf 0/4] Fix invariant violation for single-value tnums

[Marco Schirrmeister]

On Fri, Feb 20, 2026 at 02:55:04PM +0100, Paul Chaignon wrote:
> We're hitting an invariant violation in Cilium that sometimes leads to
> BPF programs being rejected and Cilium failing to start [1]. As far as
> I know this is the first case of invariant violation found in a real
> program (i.e., not by a fuzzer). The following extract from verifier
> logs shows what's happening:
> 
>   verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xe01, 0xe00] s64=[0xe01, 0xe00] u32=[0xe01, 0xe00] s32=[0xe01, 0xe00] var_off=(0xe00, 0x0)
> 

I have tested this patchset (v2) on an ARM64 system (NanoPi R76S / RK3588)
running Void Linux (glibc) with Kernel 6.18.13.

Before applying the patches, I was hitting the "REG INVARIANTS VIOLATION"
stack trace and BPF program rejections during Cilium 1.19.1 startup.

After applying this series, the Cilium agent starts successfully and
the previously rejected BPF programs now pass verification and are
successfully loaded. There are no further invariant violation warnings
in dmesg.

If there are any specific BPF tests or additional scenarios you would
like me to run, please let me know.

Tested-by: Marco Schirrmeister <mschirrmeister@gmail.com>

Re: [PATCH v2 bpf 2/4] bpf: Improve bounds when tnum has a single possible value

[Eduard Zingerman]

On Fri, 2026-02-20 at 14:57 +0100, Paul Chaignon wrote:
> We're hitting an invariant violation in Cilium that sometimes leads to
> BPF programs being rejected and Cilium failing to start [1]. The
> following extract from verifier logs shows what's happening:
> 
>   from 201 to 236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
>   236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
>   ; if (magic == MARK_MAGIC_HOST || magic == MARK_MAGIC_OVERLAY || magic == MARK_MAGIC_ENCRYPT) @ bpf_host.c:1337
>   236: (16) if w9 == 0xe00 goto pc+45   ; R9=scalar(smin=umin=smin32=umin32=3585,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100))
>   237: (16) if w9 == 0xf00 goto pc+1
>   verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xe01, 0xe00] s64=[0xe01, 0xe00] u32=[0xe01, 0xe00] s32=[0xe01, 0xe00] var_off=(0xe00, 0x0)
> 
> We reach instruction 236 with two possible values for R9, 0xe00 and
> 0xf00. This is perfectly reflected in the tnum, but of course the ranges
> are less accurate and cover [0xe00; 0xf00]. Taking the fallthrough path
> at instruction 236 allows the verifier to reduce the range to
> [0xe01; 0xf00]. The tnum is however not updated.
> 
> With these ranges, at instruction 237, the verifier is not able to
> deduce that R9 is always equal to 0xf00. Hence the fallthrough pass is
> explored first, the verifier refines the bounds using the assumption
> that R9 != 0xf00, and ends up with an invariant violation.
> 
> This pattern of impossible branch + bounds refinement is common to all
> invariant violations seen so far. The long-term solution is likely to
> rely on the refinement + invariant violation check to detect dead
> branches, as started by Eduard. To fix the current issue, we need
> something with less refactoring that we can backport.
> 
> This patch uses the tnum_step helper introduced in the previous patch to
> detect the above situation. In particular, three cases are now detected
> in the bounds refinement:
> 
> 1. The u64 range and the tnum only overlap in umin.
>    u64:  ---[xxxxxx]-----
>    tnum: --xx----------x-
> 
> 2. The u64 range and the tnum only overlap in the maximum value
>    represented by the tnum, called tmax.
>    u64:  ---[xxxxxx]-----
>    tnum: xx-----x--------
> 
> 3. The u64 range and the tnum only overlap in between umin (excluded)
>    and umax.
>    u64:  ---[xxxxxx]-----
>    tnum: xx----x-------x-
> 
> To detect these three cases, we call tnum_step(tnum, umin), which
> returns the largest member of the tnum greater than umin, called
> tnum_next here. We're in case (1) if umin is part of the tnum and
> tnum_next is greater than umax. We're in case (2) if umin is not part of
> the tnum and tnum_next is equal to tmax. Finally, we're in case (3) if
> umin is not part of the tnum, tnum_next is inferior or equal to umax,
> and calling tnum_step a second time gives us a value past umax.
> 
> This change implements these three cases. With it, the above bytecode
> looks as follows:
> 
>   0: (85) call bpf_get_prandom_u32#7    ; R0=scalar()
>   1: (47) r0 |= 3584                    ; R0=scalar(smin=0x8000000000000e00,umin=umin32=3584,smin32=0x80000e00,var_off=(0xe00; 0xfffffffffffff1ff))
>   2: (57) r0 &= 3840                    ; R0=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100))
>   3: (15) if r0 == 0xe00 goto pc+2      ; R0=3840
>   4: (15) if r0 == 0xf00 goto pc+1
>   4: R0=3840
>   6: (95) exit
> 
> In addition to the new selftests, this change was also verified with
> Agni [3]. For the record, the raw SMT is available at [4]. The property
> it verifies is that: If a concrete value x is contained in all input
> abstract values, after __update_reg_bounds, it will continue to be
> contained in all output abstract values.
> 
> Link: https://github.com/cilium/cilium/issues/44216 [1]
> Link: https://pchaigno.github.io/test-verifier-complexity.html [2]
> Link: https://github.com/bpfverif/agni [3]
> Link: https://pastebin.com/raw/naCfaqNx [4]
> Fixes: 0df1a55afa83 ("bpf: Warn on internal verifier errors")
> Co-developed-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

Re: [PATCH v2 bpf 3/4] selftests/bpf: Test refinement of single-value tnum

[Eduard Zingerman]

On Fri, 2026-02-20 at 14:57 +0100, Paul Chaignon wrote:
> This patch introduces selftests to cover the new bounds refinement
> logic introduced in the previous patch. Without the previous patch,
> the first two tests fail because of the invariant violation they
> trigger. The last test fails because the R10 access is not detected as
> dead code. In addition, all tests fail because of R0 having a
> non-constant value in the verifier logs.
>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

Hi Paul,

I have a few nitpicks, sorry for not commenting about it in v1.

>  .../selftests/bpf/progs/verifier_bounds.c     | 91 +++++++++++++++++++
>  1 file changed, 91 insertions(+)
>
> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> index 560531404bce..41dd249faadd 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> @@ -1863,4 +1863,95 @@ l1_%=:	r0 = 1;				\
>  	: __clobber_all);
>  }
>
> +/* This test covers the bounds deduction when the u64 range and the tnum
> + * overlap only at umax. After instruction 3, the ranges look as follows:
> + *
> + * 0    umin=0xe01     umax=0xf00                              U64_MAX
> + * |    [xxxxxxxxxxxxxx]                                       |
> + * |----------------------------|------------------------------|
> + * |   x               x                                       | tnum values
> + *
> + * The verifier can therefore deduce that the R0=0xf00=3840.
> + */
> +SEC("socket")
> +__description("bounds refinement with single-value tnum on umax")
> +__msg("3: (15) if r0 == 0xe00 {{.*}} R0=3840")
> +__success __log_level(2)
> +__flag(BPF_F_TEST_REG_INVARIANTS)
> +__naked void bounds_refinement_tnum_umax(void *ctx)
> +{
> +	asm volatile("			\
> +	call %[bpf_get_prandom_u32];	\
> +	r0 |= 0xe00;			\
> +	r0 &= 0xf00;			\
> +	if r0 == 0xe00 goto +2;		\
> +	if r0 == 0xf00 goto +1;		\
> +	r0 = 0;				\

Nit: make this `r10 = 0;`, just like in the last test?
     (and in the next test).

Also, the test works the same if I replace 0xe00 -> 0xe, 0xf00 -> 0xf.
Maybe pick the smaller constants to ease the readability?

> +	exit;				\
> +"	:
> +	: __imm(bpf_get_prandom_u32)
> +	: __clobber_all);
> +}
> +
> +/* This test covers the bounds deduction when the u64 range and the tnum
> + * overlap only at umin. After instruction 3, the ranges look as follows:
> + *
> + * 0    umin=0xe00     umax=0xeff                              U64_MAX
> + * |    [xxxxxxxxxxxxxx]                                       |
> + * |----------------------------|------------------------------|
> + * |    x               x                                      | tnum values
> + *
> + * The verifier can therefore deduce that the R0=0xe00=3584.
> + */
> +SEC("socket")
> +__description("bounds refinement with single-value tnum on umin")
> +__msg("3: (15) if r0 == 0xf00 {{.*}} R0=3584")
> +__success __log_level(2)
> +__flag(BPF_F_TEST_REG_INVARIANTS)
> +__naked void bounds_refinement_tnum_umin(void *ctx)
> +{
> +	asm volatile("			\
> +	call %[bpf_get_prandom_u32];	\
> +	r0 |= 0xe00;			\
> +	r0 &= 0xf00;			\
> +	if r0 == 0xf00 goto +2;		\
> +	if r0 == 0xe00 goto +1;		\
> +	r0 = 0;				\
> +	exit;				\
> +"	:
> +	: __imm(bpf_get_prandom_u32)
> +	: __clobber_all);
> +}
> +
> +/* This test covers the bounds deduction when the only possible tnum value is
> + * in the middle of the u64 range. After instruction 3, the ranges look as
> + * follows:
> + *
> + * 0    umin=0x7cf     umax=0x7df                              U64_MAX
> + * |    [xxxxxxxxxxxxxx]                                       |
> + * |----------------------------|------------------------------|
> + * |      x            x            x            x            x| tnum values
> + *
> + * The verifier can therefore deduce that the R0=0x7d0=2000. Instruction 5 is
> + * therefore dead code.
> + */
> +SEC("socket")
> +__description("bounds refinement with single-value tnum in middle of range")
> +__msg("3: (a5) if r0 < 0x7cf {{.*}} R0=2000")
> +__success __log_level(2)
> +__naked void bounds_refinement_tnum_middle(void *ctx)
> +{
> +	asm volatile("			\
> +	call %[bpf_get_prandom_u32];	\
> +	if r0 & 0x0f goto +4;		\
> +	if r0 > 0x7df goto +3;		\
> +	if r0 < 0x7cf goto +2;		\

Could you please add comment here saying something like:

  r0 is now in a range [0x7cf..0x7df] with lower 4 bits known to be 0,
  first number > 0x7cf with lower 4 bits set to 0 is 0x7d0 with 0x7e0
  following it. Only 0x7d0 fits in the above range, hence that's the
  value of r0. (Or add labels for tnum 'x' on the diagram above?)

> +	if r0 == 0x7d0 goto +1;		\
> +	r10 = 0;			\
> +	exit;				\
> +"	:
> +	: __imm(bpf_get_prandom_u32)
> +	: __clobber_all);
> +}
> +
>  char _license[] SEC("license") = "GPL";

Also, I think a few more tests are necessary, there are three cases:

         if (umin_in_tnum && tnum_next > reg->umax_value) {  // A
	 	...
         } else if (!umin_in_tnum && tnum_next == tmax) {    // B
	 	...
         } else if (!umin_in_tnum && tnum_next <= reg->umax_value && // C
	 	...
         }

If I remove 'umin_in_tnum &&' from A no tests fail.
If I remove '!umin_in_tnum &&' from B or C test cases
'verifier_bounds/verifier_bounds/bounds check based on reg_off + var_off + insn_off. test{1,2}' fail,
but these seem unrelated.
Maybe craft a few test cases covering these conditions?

Re: [PATCH v2 bpf 4/4] selftests/bpf: Avoid simplification of crafted bounds test

[Eduard Zingerman]

On Fri, 2026-02-20 at 14:58 +0100, Paul Chaignon wrote:
> The reg_bounds_crafted tests validate the verifier's range analysis
> logic. They focus on the actual ranges and thus ignore the tnum. As a
> consequence, they carry the assumption that the tested cases can be
> reproduced in userspace without using the tnum information.
> 
> Unfortunately, the previous change the refinement logic breaks that
> assumption for one test case:
> 
>   (u64)2147483648 (u32)<op> [4294967294; 0x100000000]
> 
> The tested bytecode is shown below. Without our previous improvement, on
> the false branch of the condition, R7 is only known to have u64 range
> [0xfffffffe; 0x100000000]. With our improvement, and using the tnum
> information, we can deduce that R7 equals 0x100000000.
> 
>   19: (bc) w0 = w6                ; R6=0x80000000
>   20: (bc) w0 = w7                ; R7=scalar(smin=umin=0xfffffffe,smax=umax=0x100000000,smin32=-2,smax32=0,var_off=(0x0; 0x1ffffffff))
>   21: (be) if w6 <= w7 goto pc+3  ; R6=0x80000000 R7=0x100000000
> 
> R7's tnum is (0; 0x1ffffffff). On the false branch, regs_refine_cond_op
> refines R7's u32 range to [0; 0x7fffffff]. Then, __reg32_deduce_bounds
> refines the s32 range to 0 using u32 and finally also sets u32=0.
> From this, __reg_bound_offset improves the tnum to (0; 0x100000000).
> Finally, our previous patch uses this new tnum to deduce that it only
> intersect with u64=[0xfffffffe; 0x100000000] in a single value:
> 0x100000000.
> 
> Because the verifier uses the tnum to reach this constant value, the
> selftest is unable to reproduce it by only simulating ranges. The
> solution implemented in this patch is to change the test case such that
> there is more than one overlap value between u64 and the tnum. The max.
> u64 value is thus changed from 0x100000000 to 0x300000000.
> 
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

The change seem to preserve the original test case intent.

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

Re: [PATCH v2 bpf 3/4] selftests/bpf: Test refinement of single-value tnum

[Paul Chaignon]

On Fri, Feb 20, 2026 at 04:20:55PM -0800, Eduard Zingerman wrote:
> On Fri, 2026-02-20 at 14:57 +0100, Paul Chaignon wrote:
> > This patch introduces selftests to cover the new bounds refinement
> > logic introduced in the previous patch. Without the previous patch,
> > the first two tests fail because of the invariant violation they
> > trigger. The last test fails because the R10 access is not detected as
> > dead code. In addition, all tests fail because of R0 having a
> > non-constant value in the verifier logs.
> >
> > Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> > ---
> 
> Hi Paul,

Hi Eduard,

Sorry for the late answer, I've been travelling.

> 
> I have a few nitpicks, sorry for not commenting about it in v1.

No worries. The AI bot also found a new small thing :')

I noticed you haven't acked the first patch. I think it's a bit thougher
to follow, so is there anything we could do to ease review?

> 
> >  .../selftests/bpf/progs/verifier_bounds.c     | 91 +++++++++++++++++++
> >  1 file changed, 91 insertions(+)
> >
> > diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > index 560531404bce..41dd249faadd 100644
> > --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > @@ -1863,4 +1863,95 @@ l1_%=:	r0 = 1;				\
> >  	: __clobber_all);
> >  }
> >
> > +/* This test covers the bounds deduction when the u64 range and the tnum
> > + * overlap only at umax. After instruction 3, the ranges look as follows:
> > + *
> > + * 0    umin=0xe01     umax=0xf00                              U64_MAX
> > + * |    [xxxxxxxxxxxxxx]                                       |
> > + * |----------------------------|------------------------------|
> > + * |   x               x                                       | tnum values
> > + *
> > + * The verifier can therefore deduce that the R0=0xf00=3840.
> > + */
> > +SEC("socket")
> > +__description("bounds refinement with single-value tnum on umax")
> > +__msg("3: (15) if r0 == 0xe00 {{.*}} R0=3840")
> > +__success __log_level(2)
> > +__flag(BPF_F_TEST_REG_INVARIANTS)
> > +__naked void bounds_refinement_tnum_umax(void *ctx)
> > +{
> > +	asm volatile("			\
> > +	call %[bpf_get_prandom_u32];	\
> > +	r0 |= 0xe00;			\
> > +	r0 &= 0xf00;			\
> > +	if r0 == 0xe00 goto +2;		\
> > +	if r0 == 0xf00 goto +1;		\
> > +	r0 = 0;				\
> 
> Nit: make this `r10 = 0;`, just like in the last test?
>      (and in the next test).
> 
> Also, the test works the same if I replace 0xe00 -> 0xe, 0xf00 -> 0xf.
> Maybe pick the smaller constants to ease the readability?

If we switch to 0xe and 0xf, the test won't validate the changes
anymore: it will pass regardless of the second patch. That's because
the range would only contain two values. We can however change it to
0xe0 and 0xf0.

[...]

> Also, I think a few more tests are necessary, there are three cases:
> 
>          if (umin_in_tnum && tnum_next > reg->umax_value) {  // A
> 	 	...
>          } else if (!umin_in_tnum && tnum_next == tmax) {    // B
> 	 	...
>          } else if (!umin_in_tnum && tnum_next <= reg->umax_value && // C
> 	 	...
>          }
> 
> If I remove 'umin_in_tnum &&' from A no tests fail.

That would be expected. As you pointed out in the v1, this part of the
condition is not strictly necessary because it should be implied by the
second part. We ended up adding it just for readability.

> If I remove '!umin_in_tnum &&' from B or C test cases
> 'verifier_bounds/verifier_bounds/bounds check based on reg_off + var_off + insn_off. test{1,2}' fail,
> but these seem unrelated.
> Maybe craft a few test cases covering these conditions?

Ack. I'll include the two cases I mentioned when discussing this in the
v1.

Thanks for the review!

Re: [PATCH v2 bpf 3/4] selftests/bpf: Test refinement of single-value tnum

[Eduard Zingerman]

On Wed, 2026-02-25 at 11:21 +0100, Paul Chaignon wrote:
> On Fri, Feb 20, 2026 at 04:20:55PM -0800, Eduard Zingerman wrote:
> > On Fri, 2026-02-20 at 14:57 +0100, Paul Chaignon wrote:
> > > This patch introduces selftests to cover the new bounds refinement
> > > logic introduced in the previous patch. Without the previous patch,
> > > the first two tests fail because of the invariant violation they
> > > trigger. The last test fails because the R10 access is not detected as
> > > dead code. In addition, all tests fail because of R0 having a
> > > non-constant value in the verifier logs.
> > > 
> > > Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> > > ---
> > 
> > Hi Paul,
> 
> Hi Eduard,
> 
> Sorry for the late answer, I've been travelling.
> 
> > 
> > I have a few nitpicks, sorry for not commenting about it in v1.
> 
> No worries. The AI bot also found a new small thing :')
> 
> I noticed you haven't acked the first patch. I think it's a bit thougher
> to follow, so is there anything we could do to ease review?

It made sense on the first pass, comments help.
Let me re-read it tomorrow, but I assume this patch works.

> > 
> > >  .../selftests/bpf/progs/verifier_bounds.c     | 91 +++++++++++++++++++
> > >  1 file changed, 91 insertions(+)
> > > 
> > > diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > > b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > > index 560531404bce..41dd249faadd 100644
> > > --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > > +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > > @@ -1863,4 +1863,95 @@ l1_%=:	r0 = 1;				\
> > >  	: __clobber_all);
> > >  }
> > > 
> > > +/* This test covers the bounds deduction when the u64 range and the tnum
> > > + * overlap only at umax. After instruction 3, the ranges look as follows:
> > > + *
> > > + * 0    umin=0xe01     umax=0xf00                              U64_MAX
> > > + * |    [xxxxxxxxxxxxxx]                                       |
> > > + * |----------------------------|------------------------------|
> > > + * |   x               x                                       | tnum values
> > > + *
> > > + * The verifier can therefore deduce that the R0=0xf00=3840.
> > > + */
> > > +SEC("socket")
> > > +__description("bounds refinement with single-value tnum on umax")
> > > +__msg("3: (15) if r0 == 0xe00 {{.*}} R0=3840")
> > > +__success __log_level(2)
> > > +__flag(BPF_F_TEST_REG_INVARIANTS)
> > > +__naked void bounds_refinement_tnum_umax(void *ctx)
> > > +{
> > > +	asm volatile("			\
> > > +	call %[bpf_get_prandom_u32];	\
> > > +	r0 |= 0xe00;			\
> > > +	r0 &= 0xf00;			\
> > > +	if r0 == 0xe00 goto +2;		\
> > > +	if r0 == 0xf00 goto +1;		\
> > > +	r0 = 0;				\
> > 
> > Nit: make this `r10 = 0;`, just like in the last test?
> >      (and in the next test).
> > 
> > Also, the test works the same if I replace 0xe00 -> 0xe, 0xf00 -> 0xf.
> > Maybe pick the smaller constants to ease the readability?
> 
> If we switch to 0xe and 0xf, the test won't validate the changes
> anymore: it will pass regardless of the second patch. That's because
> the range would only contain two values. We can however change it to
> 0xe0 and 0xf0.

You mean that min/max logic for 'r0 == 0xe' will adjust the range, right?
Makes sense, no changes necessary then.

> 
> [...]
> 
> > Also, I think a few more tests are necessary, there are three cases:
> > 
> >          if (umin_in_tnum && tnum_next > reg->umax_value) {  // A
> > 	 	...
> >          } else if (!umin_in_tnum && tnum_next == tmax) {    // B
> > 	 	...
> >          } else if (!umin_in_tnum && tnum_next <= reg->umax_value && // C
> > 	 	...
> >          }
> > 
> > If I remove 'umin_in_tnum &&' from A no tests fail.
> 
> That would be expected. As you pointed out in the v1, this part of the
> condition is not strictly necessary because it should be implied by the
> second part. We ended up adding it just for readability.

Wellp, that's a bit embarrassing, sorry for the noise.

> > If I remove '!umin_in_tnum &&' from B or C test cases
> > 'verifier_bounds/verifier_bounds/bounds check based on reg_off + var_off + insn_off. test{1,2}'
> > fail,
> > but these seem unrelated.
> > Maybe craft a few test cases covering these conditions?
> 
> Ack. I'll include the two cases I mentioned when discussing this in the
> v1.
> 
> Thanks for the review!