[PATCH bpf-next 0/2] Detect and prune dead branches using intersection checks

[PATCH bpf-next 0/2] Detect and prune dead branches using intersection checks

[Harishankar Vishwanathan]

This patchset improves the BPF verifier's dead branch detection and pruning by
introducing intersection checks for the verifier's abstract domains (u64, s64,
u32, s32, and tnum). 

Previously, the verifier could detect only ill-formed ranges (e.g., umin > umax)
to detect dead branches during simulation [1]. This patchset expands upon that
by identifying situations where the abstract values across different domains for
a given register no longer intersect. If there is no concrete integer value that
simultaneously satisfies the bounds of all tracked domains, the verifier can
safely deduce that the branch is dead code. As a proof of correctness, the C
implementation for each of the 10 domain intersection checks has been formally
verified against a logical specification using the Agni framework [2].

Patch 1 introduces reg_bounds_intersect() which implements intersection checks
for all 10 domain pairs and uses this in simulate_both_branches_taken() to
improve dead branch detection, and in reg_bounds_sync() to exit early on invalid
inputs that have no intersection. 

Patch 2 (Paul) adds an accompanying selftest that relies on an empty
intersection between tnum and u64 state, something that is detectable only by
the new logic. 

[1] commit b254c6d816e5 ("bpf: Simulate branches to prune based on range violations")
[2] https://github.com/bpfverif/agni

Harishankar Vishwanathan (1):
  bpf/verifier: Use intersection checks when simulating to detect dead
    branches

Paul Chaignon (1):
  selftests/bpf: Test for empty intersection of tnum and u64

 kernel/bpf/verifier.c                         | 224 +++++++++++++++++-
 .../selftests/bpf/progs/verifier_bounds.c     |  25 ++
 2 files changed, 244 insertions(+), 5 deletions(-)

-- 
2.51.0

[PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Harishankar Vishwanathan]

This commit introduces checks to detect if the ranges and/or tnums have
intersections between them, and uses the checks in
simulate_both_branches_taken and reg_bounds_sync.

The verifier is known to evolve the reg_states correctly (i.e. soundly)
on a live branch. In a previous commit [1], we used the ill-formedness
of a range (e.g. umin > umax), identified by range_bounds_violation, to
detect dead branches and prune the branch along which the ill-formedness
occurs.

Another opportunity to prune branches is when the ranges and/or tnums
have don't intersect. When the verifier evolves the reg_state along a
dead branch, it is possible that abstract value in one domain (e.g tnum)
doesn't match with the abstract value in the other domain (e.g. u64), so
that there is no single value x, that is contained in both the abstract
values.

First, we introduce intersection checks for each of the 5 domains (for a
total of 10 domain pairs), and wrap it in reg_bounds_intersect.

Next, in simulate_both_branches_taken, we use reg_bounds_intersect
instead of the existing range_bounds_violation to detect dead branches.
Because the new check in reg_bounds_intersect also checks for
range_bounds_violation, we are strictly increasing the detection of dead
branches when using the new check.

Finally, this commit also replaces the early exit in reg_bounds_sync. In
an older commit [2] we detected invalid inputs to reg_bounds_sync using
range_bounds_violation, i.e. checking for ill-formed ranges (e.g. umin >
umax), and exited early. If the inputs to reg_bounds_sync do not have
any intersection, they are also invalid. This way, we ensure that
subsequent operations in reg_bounds_sync don't inadvertently "fix" the
reg_state to become valid. This is important for example, when we
simulate_both_branches_taken; the call to reg_bounds_sync won't fix the
reg_state bounds, so we can still detect dead branches using
reg_bounds_intersect.

As a proof of correctness, for each domain pair, we individually
verified the C implementation against a logical specification. For each
pair, we used Agni [3] to encode the C implementation in logic. The
logical specification for a given pair asserts that an intersection
exists if and only if there is at least one concrete integer value that
is simultaneously a valid member of both abstract domains. All 10
verifications returned an "unsat", confirming the C implementation is
equivalent to the specification.

[1] commit b254c6d816e5 ("bpf: Simulate branches to prune based on range violations")
[2] commit a2a14e874b4e ("bpf: Exit early if reg_bounds_sync gets invalid inputs")
[3] https://github.com/bpfverif/agni

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>
---
 kernel/bpf/verifier.c | 224 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 219 insertions(+), 5 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 9e4980128151..3f0d24ed2acc 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2345,12 +2345,15 @@ static void __reg_bound_offset(struct bpf_reg_state *reg)
 	reg->var_off = tnum_or(tnum_clear_subreg(var64_off), var32_off);
 }
 
-static bool range_bounds_violation(struct bpf_reg_state *reg);
+static bool reg_bounds_intersect(struct bpf_reg_state *reg);
 
 static void reg_bounds_sync(struct bpf_reg_state *reg)
 {
-	/* If the input reg_state is invalid, we can exit early */
-	if (range_bounds_violation(reg))
+	/* If the input reg_state has no intersection between abstract values, it is
+	 * invalid. We can exit early, ensuring that subsequent operations don't
+	 * inadvertently fix the reg_state.
+	 */
+	if (!reg_bounds_intersect(reg))
 		return;
 	/* We might have learned new bounds from the var_off. */
 	__update_reg_bounds(reg);
@@ -2397,6 +2400,217 @@ static bool const_tnum_range_mismatch_32(struct bpf_reg_state *reg)
 	       reg->s32_min_value != sval32 || reg->s32_max_value != sval32;
 }
 
+/*
+ * Check if a reg_state's bounds in all domains (u64, s64, u32, s32, tnum)
+ * intersect. This ensures that for every pair of abstract values, there is
+ * *at least one* value x, such that x is a member of both abstract values.
+ * If there is no intersection between *any* pair of abstract values (10 pairs
+ * from the five domains), return false. Otherwise, return true.
+ */
+static bool reg_bounds_intersect(struct bpf_reg_state *reg)
+{
+	u64 umin = reg->umin_value, umax = reg->umax_value;
+	s64 smin = reg->smin_value, smax = reg->smax_value;
+	u32 u32_min = reg->u32_min_value, u32_max = reg->u32_max_value;
+	s32 s32_min = reg->s32_min_value, s32_max = reg->s32_max_value;
+	struct tnum t = reg->var_off;
+	struct tnum t32 = tnum_subreg(t);
+	u64 tmin = t.value, tmax = t.value | t.mask;
+	u32 t32_min = t32.value, t32_max = t32.value | t32.mask;
+
+	/*
+	 * If the min > max, then the range itself is ill-formed, so there can be no
+	 * intersection in abstract values across domains.
+	 */
+	if (range_bounds_violation(reg))
+		return false;
+
+	/*
+	 * If the var_off is ill-formed, there can be no intersection in abstract
+	 * values across domains.
+	 */
+	if ((t.value & t.mask) != 0)
+		return false;
+
+	/*
+	 * Intersect u64 with s64. We map the s64 range to u64 domain and check if
+	 * there is an intersection. If s64 range does not cross the sign boundary,
+	 * then we can treat it as a u64 range and check if its bounding values are
+	 * outside the u64 range. If s64 range crosses the sign boundary, then it
+	 * spans the u64 intervals [0, smax] and [smin, U64_MAX]. Intersection
+	 * exists if the u64 range overlaps either of these components, which is
+	 * equivalent to checking that the u64 range is not trapped between
+	 * (u64)smax and (u64)smin.
+	 */
+	if ((u64)smin <= (u64)smax) { /* s64 does not cross the sign boundary */
+		if ((u64)smax < umin || umax < (u64)smin)
+			return false;
+	} else { /* s64 crosses the sign boundary */
+		if ((u64)smin > umax && (u64)smax < umin)
+			return false;
+	}
+
+	/*
+	 * Intersect u32 with s32. This case is similar to u64-s64, but we map
+	 * the s32 range to the u32 domain.
+	 */
+	if ((u32)s32_min <= (u32)s32_max) {
+		if ((u32)s32_max < u32_min || u32_max < (u32)s32_min)
+			return false;
+	} else {
+		if ((u32)s32_min > u32_max && (u32)s32_max < u32_min)
+			return false;
+	}
+
+	/*
+	 * Intersect u64 with tnum. When we map the tnum to the u64 domain, the
+	 * bounding values of tnum might be outside the bounding values of u64.
+	 * In this case, there is no intersection. For example:
+	 *
+	 * u64:  --[xxxxxx]--------------
+	 * tnum: -----------xx-x-x----x--
+	 *               tmin         tmax
+	 *
+	 * However, it is also possible that the tnum "jumps over" the
+	 * u64, making the u64 range lie entirely "in-between" the tnum, and
+	 * in this case as well, there is no intersection. For example:
+	 *
+	 * u64:  ----[xxxxxx]------
+	 * tnum: -x-----------x----
+	 *      tmin         tmax
+	 *
+	 * We can check for intersection by checking if the next tnum value after
+	 * umin is beyond umax. If it is, there is no intersection.
+	 */
+	if (tmax < umin || tmin > umax)
+		return false;
+	if (t.value != (umin & ~t.mask)) {
+		if (tnum_step(t, umin) > umax)
+			return false;
+	}
+
+	/*
+	 * Intersect u32 with tnum. This case is similar to u64-tnum, but we map
+	 * the tnum to the u32 domain.
+	 */
+	if (t32_max < u32_min || t32_min > u32_max)
+		return false;
+	if (t32.value != (u32_min & ~t32.mask)) {
+		if (tnum_step(t32, u32_min) > u32_max)
+			return false;
+	}
+
+	/*
+	 * Intersect s64 with tnum. Similar to u64-tnum, but we map s64 and tnum to
+	 * the u64 domain. If s64 range does not cross the sign boundary, we can
+	 * treat it as a normal u64 range and check intersection with the tnum as
+	 * above. If s64 range crosses the sign boundary, it spans the u64 intervals
+	 * [0, smax] and [smin, U64_MAX]. Intersection exists if the tnum overlaps
+	 * either of these components. The tnum cannot "jump over" either of these
+	 * two intervals, because they contain endpoints 0 and U64_MAX respectively.
+	 * So it is sufficient to check if the bounding values of tnum are outside
+	 * the bounding values of the mapped s64.
+	 */
+	if ((u64)smin <= (u64)smax) { /* s64 does not cross sign boundary */
+		if (tmax < (u64)smin || tmin > (u64)smax)
+			return false;
+		if (t.value != ((u64)smin & ~t.mask)) {
+			if (tnum_step(t, (u64)smin) > (u64)smax)
+				return false;
+		}
+	} else { /* s64 crosses sign boundary */
+		if (tmin > (u64)smax && tmax < (u64)smin)
+			return false;
+	}
+
+	/*
+	 * Intersect s32 with tnum. This case is similar to s64-tnum, but we map
+	 * s32 and tnum to the u32 domain.
+	 */
+	if ((u32)s32_min <= (u32)s32_max) { /* s32 does not cross sign boundary */
+		if (t32_min > (u32)s32_max || t32_max < (u32)s32_min)
+			return false;
+		if (t32.value != ((u32)s32_min & ~t32.mask)) {
+			if (tnum_step(t32, (u32)s32_min) > (u32)s32_max)
+				return false;
+		}
+	} else { /* s32 crosses sign boundary */
+		if (t32_min > (u32)s32_max && t32_max < (u32)s32_min)
+			return false;
+	}
+
+	/*
+	 * Intersect u64 with u32. If the u64 range spans >=U32_MAX values then an
+	 * intersection is guaranteed, so we skip that case. Otherwise, we map the
+	 * u64 bounds to the u32 domain. When mapped, the u64 range might cross the
+	 * U32_MAX boundary. If it doesn't cross the boundary, it forms a single
+	 * contiguous range: [(u32)umin, (u32)umax] that we check intersection with
+	 * u32 bounds. If it does cross the U32_MAX boundary, we get two contiguous
+	 * ranges: [0, (u32)umax] and [(u32)umin, U32_MAX]. We check if any part of
+	 * the u32 bounds overlaps with either segment, which is equivalent to
+	 * ensuring the u32 bounds are not trapped between (u32)umax and (u32)umin.
+	 */
+	if (umax - umin < U32_MAX) { /* u64 range does not span entire 32-bit domain */
+		if ((u32)umin <= (u32)umax) { /* mapped u32 range is a single contiguous range */
+			if ((u32)umax < u32_min || u32_max < (u32)umin)
+				return false;
+		} else { /* mapped u32 range crosses U32_MAX boundary */
+			if ((u32)umin > u32_max && (u32)umax < u32_min)
+				return false;
+		}
+	}
+
+	/*
+	 * Intersect s64 with u32. This case is similar to u64-u32, but the s64
+	 * range is mapped to the u32 domain.
+	 */
+	if ((u64)smax - (u64)smin < U32_MAX) { /* s64 range does not span entire 32-bit domain */
+		if ((u32)smin <= (u32)smax) { /* mapped u32 range is a single contiguous range */
+			if ((u32)smax < u32_min || u32_max < (u32)smin)
+				return false;
+		} else { /* mapped u32 range crosses U32_MAX boundary */
+			if ((u32)smin > u32_max && (u32)smax < u32_min)
+				return false;
+		}
+	}
+
+	/*
+	 * Intersect u64 with s32. We map the u64 range to the s32 domain, where it
+	 * might cross the S32_MIN/S32_MAX boundary. If it doesn't cross the
+	 * boundary (it might still cross the -1/0 boundary), we check for overlap
+	 * in the standard way. Otherwise, we get two contiguous ranges (one of
+	 * which might cross the -1/0 boundary): [S32_MIN, (s32)umax] and
+	 * [(s32)umin, S32_MAX]. Intersection exists if the s32 bounds overlap with
+	 * either segment, which is equivalent to ensuring the s32 bounds are not
+	 * trapped between (s32)umax and (s32)umin.
+	 */
+	if (umax - umin < U32_MAX) { /* u64 range does not span entire 32-bit domain */
+		if ((s32)umin <= (s32)umax) { /* mapped s32 range is a single contiguous range */
+			if ((s32)umax < s32_min || s32_max < (s32)umin)
+				return false;
+		} else { /* mapped s32 range crosses S32_MIN/S32_MAX boundary */
+			if ((s32)umin > s32_max && (s32)umax < s32_min)
+				return false;
+		}
+	}
+
+	/*
+	 * Intersect s64 with s32. This case is similar to u64-s32, but the s64
+	 * range is mapped to the s32 domain.
+	 */
+	if ((u64)smax - (u64)smin < U32_MAX) { /* s64 range does not span entire 32-bit domain */
+		if ((s32)smin <= (s32)smax) { /* mapped s32 range is a single contiguous range */
+			if ((s32)smax < s32_min || s32_max < (s32)smin)
+				return false;
+		} else { /* mapped s32 range crosses S32_MAX/S32_MIN boundary */
+			if ((s32)smin > s32_max && (s32)smax < s32_min)
+				return false;
+		}
+	}
+
+	return true;
+}
+
 static int reg_bounds_sanity_check(struct bpf_verifier_env *env,
 				   struct bpf_reg_state *reg, const char *ctx)
 {
@@ -15493,7 +15707,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
 	 * reg_states in the FALSE branch (i.e. reg1, reg2), the FALSE branch must be dead. Only
 	 * TRUE branch will be taken.
 	 */
-	if (range_bounds_violation(&env->false_reg1) || range_bounds_violation(&env->false_reg2))
+	if (!reg_bounds_intersect(&env->false_reg1) || !reg_bounds_intersect(&env->false_reg2))
 		return 1;
 
 	/* Jump (TRUE) branch */
@@ -15505,7 +15719,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
 	 * reg_states in the TRUE branch (i.e. true_reg1, true_reg2), the TRUE branch must be dead.
 	 * Only FALSE branch will be taken.
 	 */
-	if (range_bounds_violation(&env->true_reg1) || range_bounds_violation(&env->true_reg2))
+	if (!reg_bounds_intersect(&env->true_reg1) || !reg_bounds_intersect(&env->true_reg2))
 		return 0;
 
 	/* Both branches are possible, we can't determine which one will be taken. */
-- 
2.51.0

[PATCH bpf-next 2/2] selftests/bpf: Test for empty intersection of tnum and u64

[Harishankar Vishwanathan]

From: Paul Chaignon <paul.chaignon@gmail.com>

Thanks to the previous patch, if the tnum and u64 don't intersect on a
branch, we can deduce the branch is dead code. This patch adds a
verifier selftest for that case, with an invalid r10 write on the dead
branch.

Without the previous patch, this selftest fails as follows:

  0: call bpf_get_prandom_u32#7  ; R0=scalar()
  1: r6 = r0                     ; R0=scalar(id=1) R6=scalar(id=1)
  2: r1 = 0xe00000002            ; R1=0xe00000002
  4: r2 = 0xf00000000            ; R2=0xf00000000
  6: if r6 s< r1 goto pc+2       ; R1=0xe00000002 R6=scalar(id=1,smin=umin=0xe00000002,umax=0x7fffffffffffffff,var_off=(0x0; 0x7fffffffffffffff))
  7: if r6 s> r2 goto pc+1       ; R2=0xf00000000 R6=scalar(id=1,smin=umin=0xe00000002,smax=umax=0xf00000000,var_off=(0xe00000000; 0x1ffffffff))
  8: if w6 == 0x1 goto pc+1      ; R6=scalar(id=1,smin=umin=0xe00000002,smax=umax=0xf00000000,var_off=(0xe00000000; 0x1ffffffff))
  9: exit

  from 8 to 10: R0=scalar(id=1,smin=umin=0xe00000002,smax=umax=0xf00000000,smin32=umin32=1,smax32=umax32=1,var_off=(0xe00000001; 0x100000000)) R1=0xe00000002 R2=0xf00000000 R6=scalar(id=1,smin=umin=0xe00000002,smax=umax=0xf00000000,smin32=umin32=1,smax32=umax32=1,var_off=(0xe00000001; 0x100000000)) R10=fp0
  10: R0=scalar(id=1,smin=umin=0xe00000002,smax=umax=0xf00000000,smin32=umin32=1,smax32=umax32=1,var_off=(0xe00000001; 0x100000000)) R1=0xe00000002 R2=0xf00000000 R6=scalar(id=1,smin=umin=0xe00000002,smax=umax=0xf00000000,smin32=umin32=1,smax32=umax32=1,var_off=(0xe00000001; 0x100000000)) R10=fp0
  10: (b7) r10 = 0
  frame pointer is read only

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

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index c1ae013dee29..151c7a479a6b 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -2184,4 +2184,29 @@ __naked void tnums_equal_impossible_constant(void *ctx)
 	: __clobber_all);
 }
 
+SEC("socket")
+__description("dead branch: tnum and u64 don't intersect on true branch")
+__success
+__naked void empty_tnum_u64_intersection(void *ctx)
+{
+	asm volatile("									\
+	call %[bpf_get_prandom_u32];							\
+	r6 = r0;									\
+	r1 = 0xe00000002 ll;								\
+	r2 = 0xf00000000 ll;								\
+	if r6 s< r1 goto +2;								\
+	/* On fallthrough, r6's u64=[0xe00000002;0xf00000000] */			\
+	/*                      tnum=(0xe00000000; 0x1ffffffff) */			\
+	if r6 s> r2 goto +1;								\
+	/* On fallthrough, r6's tnum=(0xe00000001; 0x100000000) */			\
+	/* It doesn't intersect with the u64 so the condition is always false */	\
+	if w6 == 1 goto +1;								\
+	exit;										\
+	r10 = 0;									\
+	exit;										\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.51.0

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[bot+bpf-ci]

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

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2345,12 +2345,15 @@ static void __reg_bound_offset(struct bpf_reg_state *reg)
>  	reg->var_off = tnum_or(tnum_clear_subreg(var64_off), var32_off);
>  }
>
> -static bool range_bounds_violation(struct bpf_reg_state *reg);
> +static bool reg_bounds_intersect(struct bpf_reg_state *reg);
>
>  static void reg_bounds_sync(struct bpf_reg_state *reg)
>  {
> -	/* If the input reg_state is invalid, we can exit early */
> -	if (range_bounds_violation(reg))
> +	/* If the input reg_state has no intersection between abstract values, it is
> +	 * invalid. We can exit early, ensuring that subsequent operations don't
> +	 * inadvertently fix the reg_state.
> +	 */
> +	if (!reg_bounds_intersect(reg))
>  		return;

This multi-line comment has text on the same line as the opening /*.
The BPF subsystem convention is to place the opening /* on its own
line for multi-line comments:

    /*
     * If the input reg_state has no intersection between abstract
     * values, it is invalid. ...
     */

[ ... ]

> @@ -15493,7 +15707,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
>  	 * If there is a range bounds violation in *any* of the abstract values in either
>  	 * reg_states in the FALSE branch (i.e. reg1, reg2), the FALSE branch must be dead. Only
>  	 * TRUE branch will be taken.
>  	 */
> -	if (range_bounds_violation(&env->false_reg1) || range_bounds_violation(&env->false_reg2))
> +	if (!reg_bounds_intersect(&env->false_reg1) || !reg_bounds_intersect(&env->false_reg2))
>  		return 1;

The comment above still says "range bounds violation" but the check
is now reg_bounds_intersect(), which tests all 10 pairwise domain
intersections -- a strictly broader check than range bounds violation
alone. Should this comment be updated to reflect the new semantics,
e.g., "If there is no intersection between abstract values..."?

> @@ -15505,7 +15719,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
>  	 * If there is a range bounds violation in *any* of the abstract values in either
>  	 * reg_states in the TRUE branch (i.e. true_reg1, true_reg2), the TRUE branch must be dead.
>  	 * Only FALSE branch will be taken.
>  	 */
> -	if (range_bounds_violation(&env->true_reg1) || range_bounds_violation(&env->true_reg2))
> +	if (!reg_bounds_intersect(&env->true_reg1) || !reg_bounds_intersect(&env->true_reg2))
>  		return 0;

Same stale "range bounds violation" wording here in the TRUE branch
comment.


---
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/24465659578

Re: [PATCH bpf-next 2/2] selftests/bpf: Test for empty intersection of tnum and u64

[sashiko-bot]

Sashiko AI review found 2 potential issue(s):
- [Medium] The test relies on the verifier treating the return value of `bpf_get_prandom_u32()` as a completely unbounded 64-bit scalar. If the verifier is improved to track its true 32-bit bounds, the test will silently stop testing the intended logic.
- [Medium] The inline comments in `empty_tnum_u64_intersection` incorrectly describe the verifier state at the wrong instruction boundaries and use incorrect terminology.
--

commit f07d8c6131ab63ef38acb708d393fc328146ef7c
Author: Paul Chaignon <paul.chaignon@gmail.com>

selftests/bpf: Test for empty intersection of tnum and u64

This commit adds a verifier selftest for a scenario where the tnum and u64
values don't intersect on a branch. It uses bpf_get_prandom_u32() and
conditional jumps to test if the verifier correctly deduces that the branch
is dead code.

> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> index c1ae013dee29c..151c7a479a6b8 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c

[ ... ]

> @@ -2184,4 +2184,29 @@ __naked void tnums_equal_impossible_constant(void *ctx)
>  	: __clobber_all);
>  }
>  
> +SEC("socket")
> +__description("dead branch: tnum and u64 don't intersect on true branch")
> +__success
> +__naked void empty_tnum_u64_intersection(void *ctx)
> +{
> +	asm volatile("									\
> +	call %[bpf_get_prandom_u32];							\
> +	r6 = r0;									\

Since bpf_get_prandom_u32() returns a u32, its runtime value is strictly
within [0, 0xffffffff]. If a future verifier update bounds prandom_u32() to
this range, the verifier will accurately determine that the jump
(r6 s< 0xe00000002) is always taken and prune the fallthrough path as dead
code.

Would this cause the test to silently pass while no longer providing any test
coverage for the tnum intersection logic? Could a truly unknown 64-bit value
be constructed instead to prevent this test fragility?

> +	r1 = 0xe00000002 ll;								\
> +	r2 = 0xf00000000 ll;								\
> +	if r6 s< r1 goto +2;								\
> +	/* On fallthrough, r6's u64=[0xe00000002;0xf00000000] */			\

Are these inline comments describing the verifier state accurately? The upper
bound of 0xf00000000 does not seem to be established until the fallthrough of
the next instruction (if r6 s> r2 goto +1).

> +	/*                      tnum=(0xe00000000; 0x1ffffffff) */			\
> +	if r6 s> r2 goto +1;								\
> +	/* On fallthrough, r6's tnum=(0xe00000001; 0x100000000) */			\

Does this tnum state actually describe the fallthrough path? It appears to
describe the mathematically deduced state on the jump target (true branch) of
the w6 == 1 check, making the term "fallthrough" incorrect here.

> +	/* It doesn't intersect with the u64 so the condition is always false */	\
> +	if w6 == 1 goto +1;								\

-- 
Sashiko AI review · https://sashiko.dev/#/patchset/20260415160728.657270-1-harishankar.vishwanathan@gmail.com?part=2

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Paul Chaignon]

On Wed, Apr 15, 2026 at 12:07:27PM -0400, Harishankar Vishwanathan wrote:
> This commit introduces checks to detect if the ranges and/or tnums have
> intersections between them, and uses the checks in
> simulate_both_branches_taken and reg_bounds_sync.
> 
> The verifier is known to evolve the reg_states correctly (i.e. soundly)
> on a live branch. In a previous commit [1], we used the ill-formedness
> of a range (e.g. umin > umax), identified by range_bounds_violation, to
> detect dead branches and prune the branch along which the ill-formedness
> occurs.
> 
> Another opportunity to prune branches is when the ranges and/or tnums
> have don't intersect. When the verifier evolves the reg_state along a
> dead branch, it is possible that abstract value in one domain (e.g tnum)
> doesn't match with the abstract value in the other domain (e.g. u64), so
> that there is no single value x, that is contained in both the abstract
> values.
> 
> First, we introduce intersection checks for each of the 5 domains (for a
> total of 10 domain pairs), and wrap it in reg_bounds_intersect.
> 
> Next, in simulate_both_branches_taken, we use reg_bounds_intersect
> instead of the existing range_bounds_violation to detect dead branches.
> Because the new check in reg_bounds_intersect also checks for
> range_bounds_violation, we are strictly increasing the detection of dead
> branches when using the new check.
> 
> Finally, this commit also replaces the early exit in reg_bounds_sync. In
> an older commit [2] we detected invalid inputs to reg_bounds_sync using
> range_bounds_violation, i.e. checking for ill-formed ranges (e.g. umin >
> umax), and exited early. If the inputs to reg_bounds_sync do not have
> any intersection, they are also invalid. This way, we ensure that
> subsequent operations in reg_bounds_sync don't inadvertently "fix" the
> reg_state to become valid. This is important for example, when we
> simulate_both_branches_taken; the call to reg_bounds_sync won't fix the
> reg_state bounds, so we can still detect dead branches using
> reg_bounds_intersect.
> 
> As a proof of correctness, for each domain pair, we individually
> verified the C implementation against a logical specification. For each
> pair, we used Agni [3] to encode the C implementation in logic. The
> logical specification for a given pair asserts that an intersection
> exists if and only if there is at least one concrete integer value that
> is simultaneously a valid member of both abstract domains. All 10
> verifications returned an "unsat", confirming the C implementation is
> equivalent to the specification.
> 
> [1] commit b254c6d816e5 ("bpf: Simulate branches to prune based on range violations")
> [2] commit a2a14e874b4e ("bpf: Exit early if reg_bounds_sync gets invalid inputs")
> [3] https://github.com/bpfverif/agni
> 
> 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>

I tested this with the Cilium complexity test suite [1]. I wanted to
check the impact on the verification time so I ran it on my host (no VM)
and disabled parallelism.

First, there is almost no impact on the number of instructions processed
(< 13 insns). That makes sense since reports of invariant violations
have been rare in Cilium. Now, the impact on the verification time also
seems null. Even running on the host, there are a few outliers, but the
mean difference is consistently reported to be null.

Considering that and the consistent veristat results:

Tested-by: Paul Chaignon <paul.chaignon@gmail.com>
Acked-by: Paul Chaignon <paul.chaignon@gmail.com>

1: https://pchaigno.github.io/test-verifier-complexity.html

> ---
>  kernel/bpf/verifier.c | 224 +++++++++++++++++++++++++++++++++++++++++-
>  1 file changed, 219 insertions(+), 5 deletions(-)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 9e4980128151..3f0d24ed2acc 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2345,12 +2345,15 @@ static void __reg_bound_offset(struct bpf_reg_state *reg)
>  	reg->var_off = tnum_or(tnum_clear_subreg(var64_off), var32_off);
>  }
>  
> -static bool range_bounds_violation(struct bpf_reg_state *reg);
> +static bool reg_bounds_intersect(struct bpf_reg_state *reg);
>  
>  static void reg_bounds_sync(struct bpf_reg_state *reg)
>  {
> -	/* If the input reg_state is invalid, we can exit early */
> -	if (range_bounds_violation(reg))
> +	/* If the input reg_state has no intersection between abstract values, it is
> +	 * invalid. We can exit early, ensuring that subsequent operations don't
> +	 * inadvertently fix the reg_state.
> +	 */
> +	if (!reg_bounds_intersect(reg))
>  		return;
>  	/* We might have learned new bounds from the var_off. */
>  	__update_reg_bounds(reg);
> @@ -2397,6 +2400,217 @@ static bool const_tnum_range_mismatch_32(struct bpf_reg_state *reg)
>  	       reg->s32_min_value != sval32 || reg->s32_max_value != sval32;
>  }
>  
> +/*
> + * Check if a reg_state's bounds in all domains (u64, s64, u32, s32, tnum)
> + * intersect. This ensures that for every pair of abstract values, there is
> + * *at least one* value x, such that x is a member of both abstract values.
> + * If there is no intersection between *any* pair of abstract values (10 pairs
> + * from the five domains), return false. Otherwise, return true.
> + */
> +static bool reg_bounds_intersect(struct bpf_reg_state *reg)
> +{
> +	u64 umin = reg->umin_value, umax = reg->umax_value;
> +	s64 smin = reg->smin_value, smax = reg->smax_value;
> +	u32 u32_min = reg->u32_min_value, u32_max = reg->u32_max_value;
> +	s32 s32_min = reg->s32_min_value, s32_max = reg->s32_max_value;
> +	struct tnum t = reg->var_off;
> +	struct tnum t32 = tnum_subreg(t);
> +	u64 tmin = t.value, tmax = t.value | t.mask;
> +	u32 t32_min = t32.value, t32_max = t32.value | t32.mask;
> +
> +	/*
> +	 * If the min > max, then the range itself is ill-formed, so there can be no
> +	 * intersection in abstract values across domains.
> +	 */
> +	if (range_bounds_violation(reg))
> +		return false;
> +
> +	/*
> +	 * If the var_off is ill-formed, there can be no intersection in abstract
> +	 * values across domains.
> +	 */
> +	if ((t.value & t.mask) != 0)
> +		return false;
> +
> +	/*
> +	 * Intersect u64 with s64. We map the s64 range to u64 domain and check if
> +	 * there is an intersection. If s64 range does not cross the sign boundary,
> +	 * then we can treat it as a u64 range and check if its bounding values are
> +	 * outside the u64 range. If s64 range crosses the sign boundary, then it
> +	 * spans the u64 intervals [0, smax] and [smin, U64_MAX]. Intersection
> +	 * exists if the u64 range overlaps either of these components, which is
> +	 * equivalent to checking that the u64 range is not trapped between
> +	 * (u64)smax and (u64)smin.
> +	 */
> +	if ((u64)smin <= (u64)smax) { /* s64 does not cross the sign boundary */
> +		if ((u64)smax < umin || umax < (u64)smin)
> +			return false;
> +	} else { /* s64 crosses the sign boundary */
> +		if ((u64)smin > umax && (u64)smax < umin)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u32 with s32. This case is similar to u64-s64, but we map
> +	 * the s32 range to the u32 domain.
> +	 */
> +	if ((u32)s32_min <= (u32)s32_max) {
> +		if ((u32)s32_max < u32_min || u32_max < (u32)s32_min)
> +			return false;
> +	} else {
> +		if ((u32)s32_min > u32_max && (u32)s32_max < u32_min)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u64 with tnum. When we map the tnum to the u64 domain, the
> +	 * bounding values of tnum might be outside the bounding values of u64.
> +	 * In this case, there is no intersection. For example:
> +	 *
> +	 * u64:  --[xxxxxx]--------------
> +	 * tnum: -----------xx-x-x----x--
> +	 *               tmin         tmax
> +	 *
> +	 * However, it is also possible that the tnum "jumps over" the
> +	 * u64, making the u64 range lie entirely "in-between" the tnum, and
> +	 * in this case as well, there is no intersection. For example:
> +	 *
> +	 * u64:  ----[xxxxxx]------
> +	 * tnum: -x-----------x----
> +	 *      tmin         tmax
> +	 *
> +	 * We can check for intersection by checking if the next tnum value after
> +	 * umin is beyond umax. If it is, there is no intersection.
> +	 */
> +	if (tmax < umin || tmin > umax)
> +		return false;
> +	if (t.value != (umin & ~t.mask)) {
> +		if (tnum_step(t, umin) > umax)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u32 with tnum. This case is similar to u64-tnum, but we map
> +	 * the tnum to the u32 domain.
> +	 */
> +	if (t32_max < u32_min || t32_min > u32_max)
> +		return false;
> +	if (t32.value != (u32_min & ~t32.mask)) {
> +		if (tnum_step(t32, u32_min) > u32_max)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect s64 with tnum. Similar to u64-tnum, but we map s64 and tnum to
> +	 * the u64 domain. If s64 range does not cross the sign boundary, we can
> +	 * treat it as a normal u64 range and check intersection with the tnum as
> +	 * above. If s64 range crosses the sign boundary, it spans the u64 intervals
> +	 * [0, smax] and [smin, U64_MAX]. Intersection exists if the tnum overlaps
> +	 * either of these components. The tnum cannot "jump over" either of these
> +	 * two intervals, because they contain endpoints 0 and U64_MAX respectively.
> +	 * So it is sufficient to check if the bounding values of tnum are outside
> +	 * the bounding values of the mapped s64.
> +	 */
> +	if ((u64)smin <= (u64)smax) { /* s64 does not cross sign boundary */
> +		if (tmax < (u64)smin || tmin > (u64)smax)
> +			return false;
> +		if (t.value != ((u64)smin & ~t.mask)) {
> +			if (tnum_step(t, (u64)smin) > (u64)smax)
> +				return false;
> +		}
> +	} else { /* s64 crosses sign boundary */
> +		if (tmin > (u64)smax && tmax < (u64)smin)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect s32 with tnum. This case is similar to s64-tnum, but we map
> +	 * s32 and tnum to the u32 domain.
> +	 */
> +	if ((u32)s32_min <= (u32)s32_max) { /* s32 does not cross sign boundary */
> +		if (t32_min > (u32)s32_max || t32_max < (u32)s32_min)
> +			return false;
> +		if (t32.value != ((u32)s32_min & ~t32.mask)) {
> +			if (tnum_step(t32, (u32)s32_min) > (u32)s32_max)
> +				return false;
> +		}
> +	} else { /* s32 crosses sign boundary */
> +		if (t32_min > (u32)s32_max && t32_max < (u32)s32_min)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u64 with u32. If the u64 range spans >=U32_MAX values then an
> +	 * intersection is guaranteed, so we skip that case. Otherwise, we map the
> +	 * u64 bounds to the u32 domain. When mapped, the u64 range might cross the
> +	 * U32_MAX boundary. If it doesn't cross the boundary, it forms a single
> +	 * contiguous range: [(u32)umin, (u32)umax] that we check intersection with
> +	 * u32 bounds. If it does cross the U32_MAX boundary, we get two contiguous
> +	 * ranges: [0, (u32)umax] and [(u32)umin, U32_MAX]. We check if any part of
> +	 * the u32 bounds overlaps with either segment, which is equivalent to
> +	 * ensuring the u32 bounds are not trapped between (u32)umax and (u32)umin.
> +	 */
> +	if (umax - umin < U32_MAX) { /* u64 range does not span entire 32-bit domain */
> +		if ((u32)umin <= (u32)umax) { /* mapped u32 range is a single contiguous range */
> +			if ((u32)umax < u32_min || u32_max < (u32)umin)
> +				return false;
> +		} else { /* mapped u32 range crosses U32_MAX boundary */
> +			if ((u32)umin > u32_max && (u32)umax < u32_min)
> +				return false;
> +		}
> +	}
> +
> +	/*
> +	 * Intersect s64 with u32. This case is similar to u64-u32, but the s64
> +	 * range is mapped to the u32 domain.
> +	 */
> +	if ((u64)smax - (u64)smin < U32_MAX) { /* s64 range does not span entire 32-bit domain */
> +		if ((u32)smin <= (u32)smax) { /* mapped u32 range is a single contiguous range */
> +			if ((u32)smax < u32_min || u32_max < (u32)smin)
> +				return false;
> +		} else { /* mapped u32 range crosses U32_MAX boundary */
> +			if ((u32)smin > u32_max && (u32)smax < u32_min)
> +				return false;
> +		}
> +	}
> +
> +	/*
> +	 * Intersect u64 with s32. We map the u64 range to the s32 domain, where it
> +	 * might cross the S32_MIN/S32_MAX boundary. If it doesn't cross the
> +	 * boundary (it might still cross the -1/0 boundary), we check for overlap
> +	 * in the standard way. Otherwise, we get two contiguous ranges (one of
> +	 * which might cross the -1/0 boundary): [S32_MIN, (s32)umax] and
> +	 * [(s32)umin, S32_MAX]. Intersection exists if the s32 bounds overlap with
> +	 * either segment, which is equivalent to ensuring the s32 bounds are not
> +	 * trapped between (s32)umax and (s32)umin.
> +	 */
> +	if (umax - umin < U32_MAX) { /* u64 range does not span entire 32-bit domain */
> +		if ((s32)umin <= (s32)umax) { /* mapped s32 range is a single contiguous range */
> +			if ((s32)umax < s32_min || s32_max < (s32)umin)
> +				return false;
> +		} else { /* mapped s32 range crosses S32_MIN/S32_MAX boundary */
> +			if ((s32)umin > s32_max && (s32)umax < s32_min)
> +				return false;
> +		}
> +	}
> +
> +	/*
> +	 * Intersect s64 with s32. This case is similar to u64-s32, but the s64
> +	 * range is mapped to the s32 domain.
> +	 */
> +	if ((u64)smax - (u64)smin < U32_MAX) { /* s64 range does not span entire 32-bit domain */
> +		if ((s32)smin <= (s32)smax) { /* mapped s32 range is a single contiguous range */
> +			if ((s32)smax < s32_min || s32_max < (s32)smin)
> +				return false;
> +		} else { /* mapped s32 range crosses S32_MAX/S32_MIN boundary */
> +			if ((s32)smin > s32_max && (s32)smax < s32_min)
> +				return false;
> +		}
> +	}
> +
> +	return true;
> +}
> +
>  static int reg_bounds_sanity_check(struct bpf_verifier_env *env,
>  				   struct bpf_reg_state *reg, const char *ctx)
>  {
> @@ -15493,7 +15707,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
>  	 * reg_states in the FALSE branch (i.e. reg1, reg2), the FALSE branch must be dead. Only
>  	 * TRUE branch will be taken.
>  	 */
> -	if (range_bounds_violation(&env->false_reg1) || range_bounds_violation(&env->false_reg2))
> +	if (!reg_bounds_intersect(&env->false_reg1) || !reg_bounds_intersect(&env->false_reg2))
>  		return 1;
>  
>  	/* Jump (TRUE) branch */
> @@ -15505,7 +15719,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
>  	 * reg_states in the TRUE branch (i.e. true_reg1, true_reg2), the TRUE branch must be dead.
>  	 * Only FALSE branch will be taken.
>  	 */
> -	if (range_bounds_violation(&env->true_reg1) || range_bounds_violation(&env->true_reg2))
> +	if (!reg_bounds_intersect(&env->true_reg1) || !reg_bounds_intersect(&env->true_reg2))
>  		return 0;
>  
>  	/* Both branches are possible, we can't determine which one will be taken. */
> -- 
> 2.51.0
> 

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Eduard Zingerman]

On Wed, 2026-04-15 at 12:07 -0400, Harishankar Vishwanathan wrote:
> This commit introduces checks to detect if the ranges and/or tnums have
> intersections between them, and uses the checks in
> simulate_both_branches_taken and reg_bounds_sync.
> 
> The verifier is known to evolve the reg_states correctly (i.e. soundly)
> on a live branch. In a previous commit [1], we used the ill-formedness
> of a range (e.g. umin > umax), identified by range_bounds_violation, to
> detect dead branches and prune the branch along which the ill-formedness
> occurs.
> 
> Another opportunity to prune branches is when the ranges and/or tnums
> have don't intersect. When the verifier evolves the reg_state along a
> dead branch, it is possible that abstract value in one domain (e.g tnum)
> doesn't match with the abstract value in the other domain (e.g. u64), so
> that there is no single value x, that is contained in both the abstract
> values.
> 
> First, we introduce intersection checks for each of the 5 domains (for a
> total of 10 domain pairs), and wrap it in reg_bounds_intersect.

Hi Harishankar,

I thought some more on the topic if checks for all 10 domain pairs are
necessary and now have some doubts. Ideally, what one wants to check
is that there exist a value included in all 5 domains.  Unfortunately,
it is too complicated to encode such a check, so the patch-set
approximates this doing pairwise intersections.  Since we already are
talking about an approximation, it might be fine to do additional
simplifications.

For example, given the current implementations for
is_scalar_branch_taken(), regs_refine_cond_op(),
deduce_bounds_64_from_64() is it ever possible for u64 range not to
intersect with s64 range?

After spending some time with pen and paper for BPF_JLE operation I
suspect that it is not possible. I also encoded this as a small cbmc
test: https://github.com/eddyz87/intersection-check.
I suspect that same reasoning applies for other operations.

I'd suggest to drop the u32/s32 and u64/s64 checks, unless a counter
example can be found. I'm not sure about 64/32-bit checks.
Wdyt?

[...]

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Eduard Zingerman]

On Wed, 2026-04-15 at 18:10 -0700, Eduard Zingerman wrote:
> On Wed, 2026-04-15 at 12:07 -0400, Harishankar Vishwanathan wrote:
> > This commit introduces checks to detect if the ranges and/or tnums have
> > intersections between them, and uses the checks in
> > simulate_both_branches_taken and reg_bounds_sync.
> > 
> > The verifier is known to evolve the reg_states correctly (i.e. soundly)
> > on a live branch. In a previous commit [1], we used the ill-formedness
> > of a range (e.g. umin > umax), identified by range_bounds_violation, to
> > detect dead branches and prune the branch along which the ill-formedness
> > occurs.
> > 
> > Another opportunity to prune branches is when the ranges and/or tnums
> > have don't intersect. When the verifier evolves the reg_state along a
> > dead branch, it is possible that abstract value in one domain (e.g tnum)
> > doesn't match with the abstract value in the other domain (e.g. u64), so
> > that there is no single value x, that is contained in both the abstract
> > values.
> > 
> > First, we introduce intersection checks for each of the 5 domains (for a
> > total of 10 domain pairs), and wrap it in reg_bounds_intersect.
> 
> Hi Harishankar,
> 
> I thought some more on the topic if checks for all 10 domain pairs are
> necessary and now have some doubts. Ideally, what one wants to check
> is that there exist a value included in all 5 domains.  Unfortunately,
> it is too complicated to encode such a check, so the patch-set
> approximates this doing pairwise intersections.

Speaking of which, how hard would it be to figure out the witness value?
Assuming that __update_reg64_bounds() happened would it be sufficient
to check tmin, tnum_step(..., tmin) and tmax?

[...]

Re: [PATCH bpf-next 2/2] selftests/bpf: Test for empty intersection of tnum and u64

[Paul Chaignon]

On Wed, Apr 15, 2026 at 06:29:52PM +0000, sashiko-bot@kernel.org wrote:
> Sashiko AI review found 2 potential issue(s):
> - [Medium] The test relies on the verifier treating the return value of `bpf_get_prandom_u32()` as a completely unbounded 64-bit scalar. If the verifier is improved to track its true 32-bit bounds, the test will silently stop testing the intended logic.
> - [Medium] The inline comments in `empty_tnum_u64_intersection` incorrectly describe the verifier state at the wrong instruction boundaries and use incorrect terminology.
> --
> 
> commit f07d8c6131ab63ef38acb708d393fc328146ef7c
> Author: Paul Chaignon <paul.chaignon@gmail.com>
> 
> selftests/bpf: Test for empty intersection of tnum and u64
> 
> This commit adds a verifier selftest for a scenario where the tnum and u64
> values don't intersect on a branch. It uses bpf_get_prandom_u32() and
> conditional jumps to test if the verifier correctly deduces that the branch
> is dead code.
> 
> > diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > index c1ae013dee29c..151c7a479a6b8 100644
> > --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> > +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> 
> [ ... ]
> 
> > @@ -2184,4 +2184,29 @@ __naked void tnums_equal_impossible_constant(void *ctx)
> >  	: __clobber_all);
> >  }
> >  
> > +SEC("socket")
> > +__description("dead branch: tnum and u64 don't intersect on true branch")
> > +__success
> > +__naked void empty_tnum_u64_intersection(void *ctx)
> > +{
> > +	asm volatile("									\
> > +	call %[bpf_get_prandom_u32];							\
> > +	r6 = r0;									\
> 
> Since bpf_get_prandom_u32() returns a u32, its runtime value is strictly
> within [0, 0xffffffff]. If a future verifier update bounds prandom_u32() to
> this range, the verifier will accurately determine that the jump
> (r6 s< 0xe00000002) is always taken and prune the fallthrough path as dead
> code.
> 
> Would this cause the test to silently pass while no longer providing any test
> coverage for the tnum intersection logic? Could a truly unknown 64-bit value
> be constructed instead to prevent this test fragility?

That's not a bad comment, but I would expect bpf_get_prandom_u32_proto
to be part of the API at this point. Many other selftests use it to
retrieve a RET_INTEGER from the verifier's point of view. If we were to
ever change that, we'd likely get more than one failure.

> 
> > +	r1 = 0xe00000002 ll;								\
> > +	r2 = 0xf00000000 ll;								\
> > +	if r6 s< r1 goto +2;								\
> > +	/* On fallthrough, r6's u64=[0xe00000002;0xf00000000] */			\
> 
> Are these inline comments describing the verifier state accurately? The upper
> bound of 0xf00000000 does not seem to be established until the fallthrough of
> the next instruction (if r6 s> r2 goto +1).

The convention seems to be that comments explain the next line, not the
previous (cf. other tests and [1]).

1: https://lore.kernel.org/bpf/CAADnVQJ2hX6E1_p557MYJOQLxXROzDxezwr-x79A7MyZZLzJuA@mail.gmail.com/

> 
> > +	/*                      tnum=(0xe00000000; 0x1ffffffff) */			\
> > +	if r6 s> r2 goto +1;								\
> > +	/* On fallthrough, r6's tnum=(0xe00000001; 0x100000000) */			\
> 
> Does this tnum state actually describe the fallthrough path? It appears to
> describe the mathematically deduced state on the jump target (true branch) of
> the w6 == 1 check, making the term "fallthrough" incorrect here.

Same here.

> 
> > +	/* It doesn't intersect with the u64 so the condition is always false */	\
> > +	if w6 == 1 goto +1;								\
> 
> -- 
> Sashiko AI review · https://sashiko.dev/#/patchset/20260415160728.657270-1-harishankar.vishwanathan@gmail.com?part=2
> 

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Harishankar Vishwanathan]

On Wed, Apr 15, 2026 at 9:10 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Wed, 2026-04-15 at 12:07 -0400, Harishankar Vishwanathan wrote:
[...]
>
> For example, given the current implementations for
> is_scalar_branch_taken(), regs_refine_cond_op(),
> deduce_bounds_64_from_64() is it ever possible for u64 range not to
> intersect with s64 range?

> After spending some time with pen and paper for BPF_JLE operation I
> suspect that it is not possible. I also encoded this as a small cbmc
> test: https://github.com/eddyz87/intersection-check.
> I suspect that same reasoning applies for other operations.

Hi Eduard,

First to confirm if I am reading the CBMC code
correctly, the precondition for the verification is that the inputs to the
BPF_JLE code are
1) register states are valid initial states (at least one concrete
value satisfying both its u64 and s64 bounds)
2) the input register states have been passed through
deduce_bounds_64_from_64()

Without the 2), the verification fails.
I am assuming the rationale is that any inputs to the BPF_JLE code in
actual verifier will have passed through reg_bounds_sync()
in a previous instruction.

If the understanding is correct, then, I had the following questions:

1) Other reg_bounds_sync() functions.
What if the other reg_bounds_sync() functions update the
abstract register values in a way that makes the jump operators
produce no intersection between u64 and s64 (when reg_bound_offset
and update_reg_bounds are run at the end)? Is this not possible?

2) Other jump operators.
The CBMC code currently doesn't check for, i.e. JEQ, JNE, JSLE,
JSLT, JSGE, JSGT, JSET. Could they produce an u64-s64 empty
intersection?

> I'd suggest to drop the u32/s32 and u64/s64 checks, unless a counter
> example can be found. I'm not sure about 64/32-bit checks.
> Wdyt?

Given Paul's tests [1] on the Cilium suite revealed almost no performance
impact of these checks, should we keep them all to stay on the safe side?

[1] https://lore.kernel.org/bpf/ad_g2QwAfJh64Ba7@mail.gmail.com/

> [...]

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Eduard Zingerman]

On Thu, 2026-04-16 at 19:13 -0400, Harishankar Vishwanathan wrote:
> On Wed, Apr 15, 2026 at 9:10 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Wed, 2026-04-15 at 12:07 -0400, Harishankar Vishwanathan wrote:
> [...]
> > 
> > For example, given the current implementations for
> > is_scalar_branch_taken(), regs_refine_cond_op(),
> > deduce_bounds_64_from_64() is it ever possible for u64 range not to
> > intersect with s64 range?
> 
> > After spending some time with pen and paper for BPF_JLE operation I
> > suspect that it is not possible. I also encoded this as a small cbmc
> > test: https://github.com/eddyz87/intersection-check.
> > I suspect that same reasoning applies for other operations.
> 
> Hi Eduard,
> 
> First to confirm if I am reading the CBMC code
> correctly, the precondition for the verification is that the inputs to the
> BPF_JLE code are
> 1) register states are valid initial states (at least one concrete
> value satisfying both its u64 and s64 bounds)
> 2) the input register states have been passed through
> deduce_bounds_64_from_64()

Yes, that's what I tried to check.

> Without the 2), the verification fails.
> I am assuming the rationale is that any inputs to the BPF_JLE code in
> actual verifier will have passed through reg_bounds_sync()
> in a previous instruction.
> 
> If the understanding is correct, then, I had the following questions:
> 
> 1) Other reg_bounds_sync() functions.
> What if the other reg_bounds_sync() functions update the
> abstract register values in a way that makes the jump operators
> produce no intersection between u64 and s64 (when reg_bound_offset
> and update_reg_bounds are run at the end)? Is this not possible?
> 
> 2) Other jump operators.
> The CBMC code currently doesn't check for, i.e. JEQ, JNE, JSLE,
> JSLT, JSGE, JSGT, JSET. Could they produce an u64-s64 empty
> intersection?

To answer both your questions: this needs additional investigation.
In general, I think it would be nice for the parts of reg_bounds_sync()
to have the following properties:
- valid register remains valid
- invalid register remains invalid

This would need some modifications and proofing to work.

> 
> > I'd suggest to drop the u32/s32 and u64/s64 checks, unless a counter
> > example can be found. I'm not sure about 64/32-bit checks.
> > Wdyt?
> 
> Given Paul's tests [1] on the Cilium suite revealed almost no performance
> impact of these checks, should we keep them all to stay on the safe side?

What I don't like is that we go through all the trouble to intersect
the ranges and still have an incomplete result, because we still don't
know if all ranges intersect at some common point (that's true for 5
arbitrary sets, here we have connected domains, so maybe there are
some additional constraints that make pairwise comparison guarantee
common intersection, but that requires additional reasoning).

Could you please comment about the witness idea?
Suppose reg_bounds_sync() is modified to preserve the properties I
described above, would it be sufficient to check two candidates:
tmin and tnum_step(tmin) to identify a register in an invalid state?

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Eduard Zingerman]

On Thu, 2026-04-16 at 16:33 -0700, Eduard Zingerman wrote:

[...]

> Could you please comment about the witness idea?
> Suppose reg_bounds_sync() is modified to preserve the properties I
> described above, would it be sufficient to check two candidates:
> tmin and tnum_step(tmin) to identify a register in an invalid state?

Actually, the witness search procedure is probably more involved than that.
Something along the following lines (ignoring 32-bit ranges for now):

- case a. s64 range does not cross the sign boundary:
  - w := min(umin_value, (u64)smin_value)
  - w := w if w in tnum else tnum_step(tnum, w)
- case b. s64 range crosses the sign boundary:
  - if u64 range intersects with lower half of s64 range [0, (u64)smax_value]:
    - w := umin_value
    - w := w if w in tnum else tnum_step(tnum, w)
  - otherwise:
    - w := min((u64)smin_value, umax_value)
    - w := w if w in tnum else tnum_step(tnum, w)

And then check again if w still belongs to each range
(it belongs to tnum by construction).

'w' refinement for 32-bit ranges needs more thought.
It would probably be similar to 32-bit -> 64-bit from lower bound
refinement described in [1] or [2].

Wdyt?

[1] https://lore.kernel.org/bpf/20260410124035.297632-1-koike@igalia.com/
[2] https://lore.kernel.org/bpf/b2a0346a5b0818008503b721c62621918d84ad0a.1776344897.git.paul.chaignon@gmail.com/

It is much simpler with cnums [3] because sync of non-intersecting
ranges produces an empty range, and one would only need to apply the
tnum range logic from your patch-set. I really need to wrap-up that RFC.

[3] https://github.com/eddyz87/bpf/tree/cnums-everywhere

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Harishankar Vishwanathan]

On Thu, Apr 16, 2026 at 7:33 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Thu, 2026-04-16 at 19:13 -0400, Harishankar Vishwanathan wrote:
> > On Wed, Apr 15, 2026 at 9:10 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > >
[...]
> In general, I think it would be nice for the parts of reg_bounds_sync()
> to have the following properties:
> - valid register remains valid
> - invalid register remains invalid

Here do you mean "valid" in the sense that there is a concrete value
across all domains? If yes, reg_bounds_sync() already holds the
first property.

As I understand, the second property is a bit nuanced as you have
referenced below.
Assuming "invalid" means there is no single concrete value common
across all domains. One way to check that is the intersection check,
if any of the input domain pairs have empty intersection, the input is invalid.
But it is also possible that the pairwise intersections say "true" but there
still doesn't exist a global intersection across all the 5 abstract values.

> What I don't like is that we go through all the trouble to intersect
> the ranges and still have an incomplete result, because we still don't
> know if all ranges intersect at some common point (that's true for 5
> arbitrary sets, here we have connected domains, so maybe there are
> some additional constraints that make pairwise comparison guarantee
> common intersection, but that requires additional reasoning).

We were thinking about this. You are right that the
pairwise comparison does not guarantee a common
intersection point. We have counterexamples showing that.

However, no pairwise intersection (in any of the domain pairs) guarantees
that there can be no common intersection point.

> Could you please comment about the witness idea?
> Suppose reg_bounds_sync() is modified to preserve the properties I
> described above, would it be sufficient to check two candidates:
> tmin and tnum_step(tmin) to identify a register in an invalid state?

IIUC, your idea is, if there is a witness, it should be one
of tmin, tnum_step(tmin).

- I don't think tmin, tnum_step(tmin) works, because you might
need several applications of tnum_step from tmin to reach umin.

- Assuming tnum_step(umin) to reach the first intersection of umin
with the tnum (let's say x), x might not intersect with the s64.

-  I think one of tnum_step(umin), tnum_step(smin), smin, umin works
to find the common intersection point among u64, s64 and tnum.

- But even then that particular intersection point must also intersect
with the u32 and s32 (when mapped to those domains). That
complicates the reasoning.

Also how would you ensure property 2 described above
in reg_bounds_sync()?

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Eduard Zingerman]

On Fri, 2026-04-17 at 01:34 -0400, Harishankar Vishwanathan wrote:

[...]

> > Could you please comment about the witness idea?
> > Suppose reg_bounds_sync() is modified to preserve the properties I
> > described above, would it be sufficient to check two candidates:
> > tmin and tnum_step(tmin) to identify a register in an invalid state?
> 
> IIUC, your idea is, if there is a witness, it should be one
> of tmin, tnum_step(tmin).
> 
> - I don't think tmin, tnum_step(tmin) works, because you might
> need several applications of tnum_step from tmin to reach umin.
> 
> - Assuming tnum_step(umin) to reach the first intersection of umin
> with the tnum (let's say x), x might not intersect with the s64.
> 
> -  I think one of tnum_step(umin), tnum_step(smin), smin, umin works
> to find the common intersection point among u64, s64 and tnum.
> 
> - But even then that particular intersection point must also intersect
> with the u32 and s32 (when mapped to those domains). That
> complicates the reasoning.
> 
> Also how would you ensure property 2 described above
> in reg_bounds_sync()?

Continuing this train of thoughts, consider the function
find_witness_aux() from [1]:

    /* pre-conditions:
     * - (u32)a_min <= b_min
     * - b_max <= (u32)a_max
     */
    static bool find_witness_aux(u64 a_min, u64 a_max, u32 b_min, u32 b_max,
                                struct tnum tnum, u64 *out)

If there is a tnum T, a 64-bit range A and a 32-bit range B, such that
`(u32)a_min <= b_min && b_max <= (u32)a_max`,
it can find a value that belongs to A, B and T if such value exist.

I believe that this function can be used as a basis for complete
witness check including signed and unsigned ranges:
- Each intersection between signed and unsigned ranges produces one or
  two unsigned ranges. 
- If e.g. (u32)a_min <= b_min does not hold, further subdivision is
  possible.

Meaning that final witness check will need to enumerate several ranges
and call find_witness_aux() several times.

Wdyt?

[1] https://github.com/eddyz87/find-witness

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Eduard Zingerman]

On Fri, 2026-04-17 at 14:17 -0700, Eduard Zingerman wrote:
> On Fri, 2026-04-17 at 01:34 -0400, Harishankar Vishwanathan wrote:
> 
> [...]
> 
> > > Could you please comment about the witness idea?
> > > Suppose reg_bounds_sync() is modified to preserve the properties I
> > > described above, would it be sufficient to check two candidates:
> > > tmin and tnum_step(tmin) to identify a register in an invalid state?
> > 
> > IIUC, your idea is, if there is a witness, it should be one
> > of tmin, tnum_step(tmin).
> > 
> > - I don't think tmin, tnum_step(tmin) works, because you might
> > need several applications of tnum_step from tmin to reach umin.
> > 
> > - Assuming tnum_step(umin) to reach the first intersection of umin
> > with the tnum (let's say x), x might not intersect with the s64.
> > 
> > -  I think one of tnum_step(umin), tnum_step(smin), smin, umin works
> > to find the common intersection point among u64, s64 and tnum.
> > 
> > - But even then that particular intersection point must also intersect
> > with the u32 and s32 (when mapped to those domains). That
> > complicates the reasoning.
> > 
> > Also how would you ensure property 2 described above
> > in reg_bounds_sync()?
> 
> Continuing this train of thoughts, consider the function
> find_witness_aux() from [1]:
> 
>     /* pre-conditions:
>      * - (u32)a_min <= b_min
>      * - b_max <= (u32)a_max
>      */
>     static bool find_witness_aux(u64 a_min, u64 a_max, u32 b_min, u32 b_max,
>                                 struct tnum tnum, u64 *out)
> 
> If there is a tnum T, a 64-bit range A and a 32-bit range B, such that
> `(u32)a_min <= b_min && b_max <= (u32)a_max`,
> it can find a value that belongs to A, B and T if such value exist.
> 
> I believe that this function can be used as a basis for complete
> witness check including signed and unsigned ranges:
> - Each intersection between signed and unsigned ranges produces one or
>   two unsigned ranges. 
> - If e.g. (u32)a_min <= b_min does not hold, further subdivision is
>   possible.
> 
> Meaning that final witness check will need to enumerate several ranges
> and call find_witness_aux() several times.
> 
> Wdyt?
> 
> [1] https://github.com/eddyz87/find-witness

Pushed complete find_witness() implementation in [1].
cbmc verification passes.

    bool find_witness(struct bpf_reg_state *reg, u64 *out)

Takes a register as an input and produces a value satisfying all
domains if such value exist. Assumes that register is well-formed:
- min < max
- tnum.mask & tnum.value == 0

Required some incantations to make cbmc understand function contracts,
I might want to switch to some more mainstream checker.

In any case, please let me know what you think.

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Harishankar Vishwanathan]

On Fri, Apr 17, 2026 at 5:17 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Fri, 2026-04-17 at 01:34 -0400, Harishankar Vishwanathan wrote:
>
> [...]
>
> > > Could you please comment about the witness idea?
> > > Suppose reg_bounds_sync() is modified to preserve the properties I
> > > described above, would it be sufficient to check two candidates:
> > > tmin and tnum_step(tmin) to identify a register in an invalid state?
> >
> > IIUC, your idea is, if there is a witness, it should be one
> > of tmin, tnum_step(tmin).
> >
> > - I don't think tmin, tnum_step(tmin) works, because you might
> > need several applications of tnum_step from tmin to reach umin.
> >
> > - Assuming tnum_step(umin) to reach the first intersection of umin
> > with the tnum (let's say x), x might not intersect with the s64.
> >
> > -  I think one of tnum_step(umin), tnum_step(smin), smin, umin works
> > to find the common intersection point among u64, s64 and tnum.
> >
> > - But even then that particular intersection point must also intersect
> > with the u32 and s32 (when mapped to those domains). That
> > complicates the reasoning.
> >
> > Also how would you ensure property 2 described above
> > in reg_bounds_sync()?
>
> Continuing this train of thoughts, consider the function
> find_witness_aux() from [1]:
>
>     /* pre-conditions:
>      * - (u32)a_min <= b_min
>      * - b_max <= (u32)a_max
>      */
>     static bool find_witness_aux(u64 a_min, u64 a_max, u32 b_min, u32 b_max,
>                                 struct tnum tnum, u64 *out)
>
> If there is a tnum T, a 64-bit range A and a 32-bit range B, such that
> `(u32)a_min <= b_min && b_max <= (u32)a_max`,
> it can find a value that belongs to A, B and T if such value exist.
>
> I believe that this function can be used as a basis for complete
> witness check including signed and unsigned ranges:
> - Each intersection between signed and unsigned ranges produces one or
>   two unsigned ranges.
> - If e.g. (u32)a_min <= b_min does not hold, further subdivision is
>   possible.

This is very similar to what we were thinking about. I was coding
it up before you shared your implementation.
I have uploaded an implementation at [1]

The main problem is solving the intersection of the u64 and tnum with u32.
The other domains can be reduced to this.

A single u64 interval [x, y] can span
a) A single interval smaller than the 32-bit space
b) Three intervals, [x, k], [k, j], [j, y], where the middle interval [k, j]
can include one or more full 32-bit spaces.

In the second case, any one of these intervals could
intersect with the tnum, depending on the higher order bits of the
intervals. To figure out which, we can intersect these 3 intervals
with the tnum (using the tnum_step check), and can discard any
intervals that don't match the tnum.

The procedure at [1] follows this approach.
1) We intersect u64 with s64, to get at most 2 u64 intervals.
2) For each u64 interval, we break them down into at most 3
intervals as described above, to obtain at most 6 u64 intervals.
3) For each u64 interval, we run a u64-tnum intersection to discard
intervals which don't match the tnum. The rest are used to
form (at most 6) u32 intervals.
4). For each u32 interval we intersect it with the tnum32, u32, and
s32. If at any point, if any of the u32 intervals intersects with all
tnum32, u32 and s32, we have a valid allwise intersection.
If none of the u32 candidates intersect entirely, the allwise intersection
is empty.

There are more details in the README about the implementation
and in the code comments. Please let me know what you think.

[1]: https://github.com/bpfverif/ebpf-domains-intersection/blob/main/intersection_allwise.c




>
> Meaning that final witness check will need to enumerate several ranges
> and call find_witness_aux() several times.
>
> Wdyt?
>
> [1] https://github.com/eddyz87/find-witness

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Harishankar Vishwanathan]

On Fri, Apr 17, 2026 at 7:19 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Fri, 2026-04-17 at 14:17 -0700, Eduard Zingerman wrote:
> > On Fri, 2026-04-17 at 01:34 -0400, Harishankar Vishwanathan wrote:
> >
[...]
>
> Pushed complete find_witness() implementation in [1].
> cbmc verification passes.

Just saw this. I shared my complete implementation in another email reply
as well.

> In any case, please let me know what you think.

I think the ideas are essentially similar. We can decide which one to
proceed with.

Alternatively, might we also consider continuing with the pairwise
intersection?

Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Eduard Zingerman]

On Fri, 2026-04-17 at 20:38 -0400, Harishankar Vishwanathan wrote:
> On Fri, Apr 17, 2026 at 7:19 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Fri, 2026-04-17 at 14:17 -0700, Eduard Zingerman wrote:
> > > On Fri, 2026-04-17 at 01:34 -0400, Harishankar Vishwanathan wrote:
> > > 
> [...]
> > 
> > Pushed complete find_witness() implementation in [1].
> > cbmc verification passes.
> 
> Just saw this. I shared my complete implementation in another email reply
> as well.
> 
> > In any case, please let me know what you think.
> 
> I think the ideas are essentially similar. We can decide which one to
> proceed with.

Thank you for sharing the code. Indeed very similar logic.
I was under impression that you don't like the witness idea hence
proceeded on my own. Would have deferred to you if not for that.
Tbh, my version looks a bit shorter/simpler.

> Alternatively, might we also consider continuing with the pairwise
> intersection?

Since we have the complete intersection logic now and it is about the
same size as pairwise, I think we should use the complete intersection
version.