[PATCH v2 bpf-next 0/6] Fix invariant violations and improve branch detection

[PATCH v2 bpf-next 0/6] Fix invariant violations and improve branch detection

[Paul Chaignon]

This patchset fixes invariant violations on register bounds. These
invariant violations cause a warning and happen when reg_bounds_sync is
trying to refine register bounds while walking an impossible branch.

This patchset takes this situation as an opportunity to improve
verification performance. That is, the verifier will use the invariant
violations as a signal that a branch cannot be taken and process it as
dead code.

This patchset implements this approach and covers it in selftests with
a new invariant violation case. Some of the logic in reg_bounds_sync
likely acts as a duplicate with logic from is_scalar_branch_taken. This
patchset does not attempt to remove superfluous logic from
is_scalar_branch_taken and leaves it to a future patchset (ex. once
syzbot has confirmed that all invariant violations are fixed).

In the future, there is also a potential opportunity to simplify
existing logic by merging reg_bounds_sync and range_bounds_violation
(have reg_bounds_sync error out on invariant violation). That is
however not needed to fix invariant violation, which we focus on in
this patchset.

Changes in v2:
  - Moved tmp registers to env in preparatory commit (Eduard).
  - Updated reg_bounds_sync to bail out in case of ill-formed
    registers, thus avoiding one set of invariant violation checks in
    simulate_both_branches_taken (Eduard).
  - Drop the Fixes tag to avoid misleading backporters (Shung-Hsi).
  - Improve wording of commit descriptions (Shung-Hsi, Hari).
  - Fix error in code comments (AI bot).
  - Rebased.

Harishankar Vishwanathan (3):
  bpf: Refactor reg_bounds_sanity_check
  bpf: Exit early if reg_bounds_sync gets invalid inputs
  bpf: Simulate branches to prune based on range violations

Paul Chaignon (3):
  bpf: Use bpf_verifier_env buffers for reg_set_min_max
  selftests/bpf: Cover invariant violation cases from syzbot
  selftests/bpf: Remove invariant violation flags

 include/linux/bpf_verifier.h                  |   4 +-
 kernel/bpf/verifier.c                         | 185 ++++++++++--------
 .../selftests/bpf/progs/verifier_bounds.c     |  46 +++--
 3 files changed, 136 insertions(+), 99 deletions(-)

-- 
2.43.0

[PATCH v2 bpf-next 1/6] bpf: Refactor reg_bounds_sanity_check

[Paul Chaignon]

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

This commit refactors reg_bounds_sanity_check to factor out the logic
that performs the sanity check from the logic that does the reporting.

Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 kernel/bpf/verifier.c | 50 ++++++++++++++++++++++++++++++-------------
 1 file changed, 35 insertions(+), 15 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 01c18f4268de..b638ab841c10 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2802,40 +2802,60 @@ static void reg_bounds_sync(struct bpf_reg_state *reg)
 	__update_reg_bounds(reg);
 }
 
-static int reg_bounds_sanity_check(struct bpf_verifier_env *env,
-				   struct bpf_reg_state *reg, const char *ctx)
+static bool range_bounds_violation(struct bpf_reg_state *reg)
 {
-	const char *msg;
-
-	if (reg->umin_value > reg->umax_value ||
-	    reg->smin_value > reg->smax_value ||
-	    reg->u32_min_value > reg->u32_max_value ||
-	    reg->s32_min_value > reg->s32_max_value) {
-		    msg = "range bounds violation";
-		    goto out;
-	}
+	return (reg->umin_value > reg->umax_value || reg->smin_value > reg->smax_value ||
+		reg->u32_min_value > reg->u32_max_value ||
+		reg->s32_min_value > reg->s32_max_value);
+}
 
+static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
+{
 	if (tnum_is_const(reg->var_off)) {
 		u64 uval = reg->var_off.value;
 		s64 sval = (s64)uval;
 
 		if (reg->umin_value != uval || reg->umax_value != uval ||
 		    reg->smin_value != sval || reg->smax_value != sval) {
-			msg = "const tnum out of sync with range bounds";
-			goto out;
+			return true;
 		}
 	}
+	return false;
+}
 
+static bool const_subreg_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
+{
 	if (tnum_subreg_is_const(reg->var_off)) {
 		u32 uval32 = tnum_subreg(reg->var_off).value;
 		s32 sval32 = (s32)uval32;
 
 		if (reg->u32_min_value != uval32 || reg->u32_max_value != uval32 ||
 		    reg->s32_min_value != sval32 || reg->s32_max_value != sval32) {
-			msg = "const subreg tnum out of sync with range bounds";
-			goto out;
+			return true;
 		}
 	}
+	return false;
+}
+
+static int reg_bounds_sanity_check(struct bpf_verifier_env *env,
+				   struct bpf_reg_state *reg, const char *ctx)
+{
+	const char *msg;
+
+	if (range_bounds_violation(reg)) {
+		msg = "range bounds violation";
+		goto out;
+	}
+
+	if (const_tnum_out_of_sync_with_range_bounds(reg)) {
+		msg = "const tnum out of sync with range bounds";
+		goto out;
+	}
+
+	if (const_subreg_tnum_out_of_sync_with_range_bounds(reg)) {
+		msg = "const subreg tnum out of sync with range bounds";
+		goto out;
+	}
 
 	return 0;
 out:
-- 
2.43.0

[PATCH v2 bpf-next 2/6] bpf: Use bpf_verifier_env buffers for reg_set_min_max

[Paul Chaignon]

In a subsequent patch, the regs_refine_cond_op and reg_bounds_sync
functions will be called in is_branch_taken instead of reg_set_min_max,
to simulate each branch's outcome. Since they will run before we branch
out, these two functions will need to work on temporary registers for
the two branches.

This refactoring patch prepares for that change, by introducing the
temporary registers on bpf_verifier_env and using them in
reg_set_min_max.

This change also allows us to save one fake_reg slot as we don't need to
allocate an additional temporary buffer in case of a BPF_K condition.

Finally, you may notice that this patch removes the check for
"false_reg1 == false_reg2" in reg_set_min_max. That check was introduced
in commit d43ad9da8052 ("bpf: Skip bounds adjustment for conditional
jumps on same scalar register") to avoid an invariant violation. Given
that "env->false_reg1 == env->false_reg2" doesn't make sense and
invariant violations are addressed in a subsequent commit, this patch
just removes the check.

Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
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>
---
 include/linux/bpf_verifier.h |  4 ++-
 kernel/bpf/verifier.c        | 64 +++++++++++++-----------------------
 2 files changed, 26 insertions(+), 42 deletions(-)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index 090aa26d1c98..b129e0aaee20 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -837,7 +837,9 @@ struct bpf_verifier_env {
 	u64 scratched_stack_slots;
 	u64 prev_log_pos, prev_insn_print_pos;
 	/* buffer used to temporary hold constants as scalar registers */
-	struct bpf_reg_state fake_reg[2];
+	struct bpf_reg_state fake_reg[1];
+	/* buffers used to save updated reg states while simulating branches */
+	struct bpf_reg_state true_reg1, true_reg2, false_reg1, false_reg2;
 	/* buffer used to generate temporary string representations,
 	 * e.g., in reg_type_str() to generate reg_type string
 	 */
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index b638ab841c10..fbc29fb96a60 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -17184,10 +17184,6 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
  * but we don't support that right now.
  */
 static int reg_set_min_max(struct bpf_verifier_env *env,
-			   struct bpf_reg_state *true_reg1,
-			   struct bpf_reg_state *true_reg2,
-			   struct bpf_reg_state *false_reg1,
-			   struct bpf_reg_state *false_reg2,
 			   u8 opcode, bool is_jmp32)
 {
 	int err;
@@ -17196,30 +17192,23 @@ static int reg_set_min_max(struct bpf_verifier_env *env,
 	 * variable offset from the compare (unless they were a pointer into
 	 * the same object, but we don't bother with that).
 	 */
-	if (false_reg1->type != SCALAR_VALUE || false_reg2->type != SCALAR_VALUE)
-		return 0;
-
-	/* We compute branch direction for same SCALAR_VALUE registers in
-	 * is_scalar_branch_taken(). For unknown branch directions (e.g., BPF_JSET)
-	 * on the same registers, we don't need to adjust the min/max values.
-	 */
-	if (false_reg1 == false_reg2)
+	if (env->false_reg1.type != SCALAR_VALUE || env->false_reg2.type != SCALAR_VALUE)
 		return 0;
 
 	/* fallthrough (FALSE) branch */
-	regs_refine_cond_op(false_reg1, false_reg2, rev_opcode(opcode), is_jmp32);
-	reg_bounds_sync(false_reg1);
-	reg_bounds_sync(false_reg2);
+	regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
+	reg_bounds_sync(&env->false_reg1);
+	reg_bounds_sync(&env->false_reg2);
 
 	/* jump (TRUE) branch */
-	regs_refine_cond_op(true_reg1, true_reg2, opcode, is_jmp32);
-	reg_bounds_sync(true_reg1);
-	reg_bounds_sync(true_reg2);
-
-	err = reg_bounds_sanity_check(env, true_reg1, "true_reg1");
-	err = err ?: reg_bounds_sanity_check(env, true_reg2, "true_reg2");
-	err = err ?: reg_bounds_sanity_check(env, false_reg1, "false_reg1");
-	err = err ?: reg_bounds_sanity_check(env, false_reg2, "false_reg2");
+	regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
+	reg_bounds_sync(&env->true_reg1);
+	reg_bounds_sync(&env->true_reg2);
+
+	err = reg_bounds_sanity_check(env, &env->true_reg1, "true_reg1");
+	err = err ?: reg_bounds_sanity_check(env, &env->true_reg2, "true_reg2");
+	err = err ?: reg_bounds_sanity_check(env, &env->false_reg1, "false_reg1");
+	err = err ?: reg_bounds_sanity_check(env, &env->false_reg2, "false_reg2");
 	return err;
 }
 
@@ -17597,6 +17586,10 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
 	}
 
 	is_jmp32 = BPF_CLASS(insn->code) == BPF_JMP32;
+	copy_register_state(&env->false_reg1, dst_reg);
+	copy_register_state(&env->false_reg2, src_reg);
+	copy_register_state(&env->true_reg1, dst_reg);
+	copy_register_state(&env->true_reg2, src_reg);
 	pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
 	if (pred >= 0) {
 		/* If we get here with a dst_reg pointer type it is because
@@ -17661,27 +17654,16 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
 		return PTR_ERR(other_branch);
 	other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
 
-	if (BPF_SRC(insn->code) == BPF_X) {
-		err = reg_set_min_max(env,
-				      &other_branch_regs[insn->dst_reg],
-				      &other_branch_regs[insn->src_reg],
-				      dst_reg, src_reg, opcode, is_jmp32);
-	} else /* BPF_SRC(insn->code) == BPF_K */ {
-		/* reg_set_min_max() can mangle the fake_reg. Make a copy
-		 * so that these are two different memory locations. The
-		 * src_reg is not used beyond here in context of K.
-		 */
-		memcpy(&env->fake_reg[1], &env->fake_reg[0],
-		       sizeof(env->fake_reg[0]));
-		err = reg_set_min_max(env,
-				      &other_branch_regs[insn->dst_reg],
-				      &env->fake_reg[0],
-				      dst_reg, &env->fake_reg[1],
-				      opcode, is_jmp32);
-	}
+	err = reg_set_min_max(env, opcode, is_jmp32);
 	if (err)
 		return err;
 
+	copy_register_state(dst_reg, &env->false_reg1);
+	copy_register_state(src_reg, &env->false_reg2);
+	copy_register_state(&other_branch_regs[insn->dst_reg], &env->true_reg1);
+	if (BPF_SRC(insn->code) == BPF_X)
+		copy_register_state(&other_branch_regs[insn->src_reg], &env->true_reg2);
+
 	if (BPF_SRC(insn->code) == BPF_X &&
 	    src_reg->type == SCALAR_VALUE && src_reg->id &&
 	    !WARN_ON_ONCE(src_reg->id != other_branch_regs[insn->src_reg].id)) {
-- 
2.43.0

[PATCH v2 bpf-next 3/6] bpf: Exit early if reg_bounds_sync gets invalid inputs

[Paul Chaignon]

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

In the subsequent commit, to prune dead branches we will rely on
detecting ill-formed ranges using range_bounds_violations()
(e.g., umin > umax) after refining register bounds using
regs_refine_cond_op().

However, reg_bounds_sync() can sometimes "repair" ill-formed bounds,
potentially masking a violation that was produced by
regs_refine_cond_op().

This commit modifies reg_bounds_sync() to exit early if an invariant
violation is already present in the input.

This ensures ill-formed reg_states remain ill-formed after
reg_bounds_sync(), allowing simulate_both_branches_taken() to correctly
identify dead branches with a single check to range_bounds_violation().

Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 kernel/bpf/verifier.c | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index fbc29fb96a60..8d7ad5f21ed6 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2786,8 +2786,13 @@ 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 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))
+		return;
 	/* We might have learned new bounds from the var_off. */
 	__update_reg_bounds(reg);
 	/* We might have learned something about the sign bit. */
-- 
2.43.0

[PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Paul Chaignon]

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

This patch fixes the invariant violations that can happen after we
refine ranges & tnum based on an incorrectly-detected branch condition.
For example, the branch is always true, but we miss it in
is_branch_taken; we then refine based on the branch being false and end
up with incoherent ranges (e.g. umax < umin).

To avoid this, we can simulate the refinement on both branches. More
specifically, this patch simulates both branches taken using
regs_refine_cond_op and reg_bounds_sync. If the resulting register
states are ill-formed on one of the branches, is_branch_taken can mark
that branch as "never taken".

On a more formal note, we can deduce a branch is not taken when
regs_refine_cond_op or reg_bounds_sync returns an ill-formed state
because the branch operators are sound (formally verified). Soundness
means that the verifier is guaranteed to produce sound outputs on the
taken branches. On the non-taken branch (explored because of
imprecision in the bounds), the verifier is free to produce any output.
We use ill-formedness as a signal that the branch is dead and prune
that branch.

This patch moves the refinement logic for both branches from
reg_set_min_max to their own function, simulate_both_branches_taken,
which is called from is_scalar_branch_taken. As a result,
reg_set_min_max now only runs sanity checks and has been renamed to
reg_bounds_sanity_check_branches to reflect that.

We have had five patches fixing specific cases of invariant violations
in the past, all added with selftests:
- commit fbc7aef517d8 ("bpf: Fix u32/s32 bounds when ranges cross
  min/max boundary")
- commit efc11a667878 ("bpf: Improve bounds when tnum has a single
  possible value")
- commit f41345f47fb2 ("bpf: Use tnums for JEQ/JNE is_branch_taken
  logic")
- commit 00bf8d0c6c9b ("bpf: Improve bounds when s64 crosses sign
  boundary")
- commit 6279846b9b25 ("bpf: Forget ranges when refining tnum after
  JSET")

To confirm that this patch addresses all invariant violations, we have
also reverted those five commits and verified that their related
selftests don't cause any invariant violation warnings anymore. Those
selftests still fail but only because of mis-detected branches or
less-precise bounds than expected. This demonstrates that the current
patch is enough to avoid the invariant violation warning AND that the
previous five patches are still useful to improve branch detection.

In addition to the selftests, this change was also tested with the
Cilium complexity test suite: all programs were successfully loaded and
it didn't change the number of processed instructions.

Reported-by: syzbot+c950cc277150935cc0b5@syzkaller.appspotmail.com
Closes: https://syzkaller.appspot.com/bug?extid=c950cc277150935cc0b5
Co-developed-by: Paul Chaignon <paul.chaignon@gmail.com>
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
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 | 84 +++++++++++++++++++++++++------------------
 1 file changed, 49 insertions(+), 35 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 8d7ad5f21ed6..0b4f622efec1 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -16717,11 +16717,48 @@ static void find_good_pkt_pointers(struct bpf_verifier_state *vstate,
 	}));
 }
 
+static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
+				u8 opcode, bool is_jmp32);
+static u8 rev_opcode(u8 opcode);
+
+/* Learn more information about live branches by simulating both branches being
+ * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when
+ * the branch is taken, if it produces ill-formed register bounds, it must mean
+ * that the branch is dead.
+ */
+static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
+{
+	/* Fallthrough (FALSE) branch */
+	regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
+	reg_bounds_sync(&env->false_reg1);
+	reg_bounds_sync(&env->false_reg2);
+	/* 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))
+		return 1;
+
+	/* Jump (TRUE) branch */
+	regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
+	reg_bounds_sync(&env->true_reg1);
+	reg_bounds_sync(&env->true_reg2);
+	/* 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))
+		return 0;
+
+	/* Both branches are possible, we can't determine which one will be taken. */
+	return -1;
+}
+
 /*
  * <reg1> <op> <reg2>, currently assuming reg2 is a constant
  */
-static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
-				  u8 opcode, bool is_jmp32)
+static int is_scalar_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
+				  struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
 {
 	struct tnum t1 = is_jmp32 ? tnum_subreg(reg1->var_off) : reg1->var_off;
 	struct tnum t2 = is_jmp32 ? tnum_subreg(reg2->var_off) : reg2->var_off;
@@ -16873,7 +16910,7 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
 		break;
 	}
 
-	return -1;
+	return simulate_both_branches_taken(env, opcode, is_jmp32);
 }
 
 static int flip_opcode(u32 opcode)
@@ -16944,8 +16981,8 @@ static int is_pkt_ptr_branch_taken(struct bpf_reg_state *dst_reg,
  * -1 - unknown. Example: "if (reg1 < 5)" is unknown when register value
  *      range [0,10]
  */
-static int is_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
-			   u8 opcode, bool is_jmp32)
+static int is_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
+			   struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
 {
 	if (reg_is_pkt_pointer_any(reg1) && reg_is_pkt_pointer_any(reg2) && !is_jmp32)
 		return is_pkt_ptr_branch_taken(reg1, reg2, opcode);
@@ -16983,7 +17020,7 @@ static int is_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg
 	}
 
 	/* now deal with two scalars, but not necessarily constants */
-	return is_scalar_branch_taken(reg1, reg2, opcode, is_jmp32);
+	return is_scalar_branch_taken(env, reg1, reg2, opcode, is_jmp32);
 }
 
 /* Opcode that corresponds to a *false* branch condition.
@@ -17074,8 +17111,8 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
 			/* u32_min_value is not equal to 0xffffffff at this point,
 			 * because otherwise u32_max_value is 0xffffffff as well,
 			 * in such a case both reg1 and reg2 would be constants,
-			 * jump would be predicted and reg_set_min_max() won't
-			 * be called.
+			 * jump would be predicted and regs_refine_cond_op()
+			 * wouldn't be called.
 			 *
 			 * Same reasoning works for all {u,s}{min,max}{32,64} cases
 			 * below.
@@ -17182,34 +17219,11 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
 	}
 }
 
-/* Adjusts the register min/max values in the case that the dst_reg and
- * src_reg are both SCALAR_VALUE registers (or we are simply doing a BPF_K
- * check, in which case we have a fake SCALAR_VALUE representing insn->imm).
- * Technically we can do similar adjustments for pointers to the same object,
- * but we don't support that right now.
- */
-static int reg_set_min_max(struct bpf_verifier_env *env,
-			   u8 opcode, bool is_jmp32)
+/* Check for invariant violations on the registers for both branches of a condition */
+static int regs_bounds_sanity_check_branches(struct bpf_verifier_env *env)
 {
 	int err;
 
-	/* If either register is a pointer, we can't learn anything about its
-	 * variable offset from the compare (unless they were a pointer into
-	 * the same object, but we don't bother with that).
-	 */
-	if (env->false_reg1.type != SCALAR_VALUE || env->false_reg2.type != SCALAR_VALUE)
-		return 0;
-
-	/* fallthrough (FALSE) branch */
-	regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
-	reg_bounds_sync(&env->false_reg1);
-	reg_bounds_sync(&env->false_reg2);
-
-	/* jump (TRUE) branch */
-	regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
-	reg_bounds_sync(&env->true_reg1);
-	reg_bounds_sync(&env->true_reg2);
-
 	err = reg_bounds_sanity_check(env, &env->true_reg1, "true_reg1");
 	err = err ?: reg_bounds_sanity_check(env, &env->true_reg2, "true_reg2");
 	err = err ?: reg_bounds_sanity_check(env, &env->false_reg1, "false_reg1");
@@ -17595,7 +17609,7 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
 	copy_register_state(&env->false_reg2, src_reg);
 	copy_register_state(&env->true_reg1, dst_reg);
 	copy_register_state(&env->true_reg2, src_reg);
-	pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
+	pred = is_branch_taken(env, dst_reg, src_reg, opcode, is_jmp32);
 	if (pred >= 0) {
 		/* If we get here with a dst_reg pointer type it is because
 		 * above is_branch_taken() special cased the 0 comparison.
@@ -17659,7 +17673,7 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
 		return PTR_ERR(other_branch);
 	other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
 
-	err = reg_set_min_max(env, opcode, is_jmp32);
+	err = regs_bounds_sanity_check_branches(env);
 	if (err)
 		return err;
 
-- 
2.43.0

[PATCH v2 bpf-next 5/6] selftests/bpf: Cover invariant violation cases from syzbot

[Paul Chaignon]

This patch adds a selftest for the change in the previous patch. The
selftest is derived from a syzbot reproducer from [1] (among the 22
reproducers on that page, only 4 still reproduced on latest bpf tree,
all being small variants of the same invariant violation).

The test case failure without the previous patch is shown below.

  0: R1=ctx() R10=fp0
  0: (85) call bpf_get_prandom_u32#7    ; R0=scalar()
  1: (bf) r5 = r0                       ; R0=scalar(id=1) R5=scalar(id=1)
  2: (57) r5 &= -4                      ; R5=scalar(smax=0x7ffffffffffffffc,umax=0xfffffffffffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; 0xfffffffffffffffc))
  3: (bf) r7 = r0                       ; R0=scalar(id=1) R7=scalar(id=1)
  4: (57) r7 &= 1                       ; R7=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
  5: (07) r7 += -43                     ; R7=scalar(smin=smin32=-43,smax=smax32=-42,umin=0xffffffffffffffd5,umax=0xffffffffffffffd6,umin32=0xffffffd5,umax32=0xffffffd6,var_off=(0xffffffffffffffd4; 0x3))
  6: (5e) if w5 != w7 goto pc+1
  verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xffffffd5, 0xffffffffffffffd4] s64=[0x80000000ffffffd5, 0x7fffffffffffffd4] u32=[0xffffffd5, 0xffffffd4] s32=[0xffffffd5, 0xffffffd4] var_off=(0xffffffd4, 0xffffffff00000000)

R5 and R7 are prepared such that their tnums intersection results in a
known constant but that constant isn't within R7's u32 bounds.
is_branch_taken isn't able to detect this case today, so the verifier
walks the impossible fallthrough branch. After regs_refine_cond_op and
reg_bounds_sync refine R5 on the assumption that the branch is taken,
the impossibility becomes apparent and results in an invariant violation
for R5: umin32 is greater than umax32.

The previous patch fixes this by using regs_refine_cond_op and
reg_bounds_sync in is_branch_taken to detect the impossible branch. The
fallthrough branch is therefore correctly detected as dead code.

Link: https://syzkaller.appspot.com/bug?extid=c950cc277150935cc0b5 [1]
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 .../selftests/bpf/progs/verifier_bounds.c     | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index 3724d5e5bcb3..818efa08404d 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -2070,4 +2070,28 @@ __naked void refinement_32bounds_not_overwriting_64bounds(void *ctx)
 	: __clobber_all);
 }
 
+/* Last jump can be detected as always taken because the intersection of R5 and
+ * R7 32bit tnums produces a constant that isn't within R7's s32 bounds.
+ */
+SEC("socket")
+__description("dead branch: tnums give impossible constant if equal")
+__success
+__flag(BPF_F_TEST_REG_INVARIANTS)
+__naked void tnums_equal_impossible_constant(void *ctx)
+{
+	asm volatile("										\
+	call %[bpf_get_prandom_u32];								\
+	r5 = r0;										\
+	r5 &= 0xfffffffffffffffc;	/* var_off32=(0; 0xfffffffc) */				\
+	r7 = r0;										\
+	r7 &= 0x1;			/* var_off32=(0x0; 0x1) */				\
+	r7 += -43;			/* s32=[-43; -42] & var_off32=(0xffffffd4; 0x3) */	\
+	if w5 != w7 goto +1;		/* on fallthrough var_off32=-44, not in s32 */		\
+	r10 = 0;										\
+	exit;											\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.43.0

[PATCH v2 bpf-next 6/6] selftests/bpf: Remove invariant violation flags

[Paul Chaignon]

With the changes to the verifier in previous commits, we're not
expecting any invariant violations anymore. We should therefore always
enable BPF_F_TEST_REG_INVARIANTS to fail on invariant violations. Turns
out that's already the case and we've been explicitly setting this flag
in selftests when it wasn't necessary. This commit removes those flags
from selftests, which should hopefully make clearer that it's always
enabled.

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

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index 818efa08404d..1ebc99d75862 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -1066,7 +1066,6 @@ l0_%=:	r0 = 0;						\
 SEC("xdp")
 __description("bound check with JMP_JSLT for crossing 64-bit signed boundary")
 __success __retval(0)
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void crossing_64_bit_signed_boundary_2(void)
 {
 	asm volatile ("					\
@@ -1148,7 +1147,6 @@ l0_%=:	r0 = 0;						\
 SEC("xdp")
 __description("bound check with JMP32_JSLT for crossing 32-bit signed boundary")
 __success __retval(0)
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void crossing_32_bit_signed_boundary_2(void)
 {
 	asm volatile ("					\
@@ -1536,7 +1534,7 @@ __naked void sub32_partial_overflow(void)
 SEC("socket")
 __description("dead branch on jset, does not result in invariants violation error")
 __success __log_level(2)
-__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
+__retval(0)
 __naked void jset_range_analysis(void)
 {
 	asm volatile ("			\
@@ -1572,7 +1570,7 @@ l0_%=:	r0 = 0;				\
  */
 SEC("socket")
 __description("bounds deduction cross sign boundary, negative overlap")
-__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
+__success __log_level(2)
 __msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=smin32=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,umin32=0xfffffd71,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")
 __retval(0)
 __naked void bounds_deduct_negative_overlap(void)
@@ -1616,7 +1614,7 @@ l0_%=:	r0 = 0;				\
  */
 SEC("socket")
 __description("bounds deduction cross sign boundary, positive overlap")
-__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
+__success __log_level(2)
 __msg("3: (2d) if r0 > r1 {{.*}} R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=127,var_off=(0x0; 0x7f))")
 __retval(0)
 __naked void bounds_deduct_positive_overlap(void)
@@ -1649,7 +1647,7 @@ l0_%=:	r0 = 0;				\
  */
 SEC("socket")
 __description("bounds deduction cross sign boundary, two overlaps")
-__failure __flag(BPF_F_TEST_REG_INVARIANTS)
+__failure
 __msg("3: (2d) if r0 > r1 {{.*}} R0=scalar(smin=smin32=-128,smax=smax32=127,umax=0xffffffffffffff80)")
 __msg("frame pointer is read only")
 __naked void bounds_deduct_two_overlaps(void)
@@ -1713,7 +1711,7 @@ SEC("socket")
 __description("conditional jump on same register, branch taken")
 __not_msg("20: (b7) r0 = 1 {{.*}} R0=1")
 __success __log_level(2)
-__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
+__retval(0)
 __naked void condition_jump_on_same_register(void *ctx)
 {
 	asm volatile("			\
@@ -1748,7 +1746,7 @@ SEC("socket")
 __description("jset on same register, constant value branch taken")
 __not_msg("7: (b7) r0 = 1 {{.*}} R0=1")
 __success __log_level(2)
-__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
+__retval(0)
 __naked void jset_on_same_register_1(void *ctx)
 {
 	asm volatile("			\
@@ -1770,7 +1768,7 @@ SEC("socket")
 __description("jset on same register, scalar value branch taken")
 __not_msg("12: (b7) r0 = 1 {{.*}} R0=1")
 __success __log_level(2)
-__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
+__retval(0)
 __naked void jset_on_same_register_2(void *ctx)
 {
 	asm volatile("			\
@@ -1800,7 +1798,6 @@ __description("jset on same register, scalar value unknown branch 1")
 __msg("3: (b7) r0 = 0 {{.*}} R0=0")
 __msg("5: (b7) r0 = 1 {{.*}} R0=1")
 __success __log_level(2)
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void jset_on_same_register_3(void *ctx)
 {
 	asm volatile("			\
@@ -1822,7 +1819,6 @@ __description("jset on same register, scalar value unknown branch 2")
 __msg("4: (b7) r0 = 0 {{.*}} R0=0")
 __msg("6: (b7) r0 = 1 {{.*}} R0=1")
 __success __log_level(2)
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void jset_on_same_register_4(void *ctx)
 {
 	asm volatile("			\
@@ -1845,7 +1841,6 @@ __description("jset on same register, scalar value unknown branch 3")
 __msg("4: (b7) r0 = 0 {{.*}} R0=0")
 __msg("6: (b7) r0 = 1 {{.*}} R0=1")
 __success __log_level(2)
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void jset_on_same_register_5(void *ctx)
 {
 	asm volatile("			\
@@ -1877,7 +1872,6 @@ SEC("socket")
 __description("bounds refinement with single-value tnum on umax")
 __msg("3: (15) if r0 == 0xe0 {{.*}} R0=240")
 __success __log_level(2)
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void bounds_refinement_tnum_umax(void *ctx)
 {
 	asm volatile("			\
@@ -1907,7 +1901,6 @@ SEC("socket")
 __description("bounds refinement with single-value tnum on umin")
 __msg("3: (15) if r0 == 0xf0 {{.*}} R0=224")
 __success __log_level(2)
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void bounds_refinement_tnum_umin(void *ctx)
 {
 	asm volatile("			\
@@ -2002,7 +1995,6 @@ __naked void bounds_refinement_multiple_overlaps(void *ctx)
 
 SEC("socket")
 __success
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void signed_unsigned_intersection32_case1(void *ctx)
 {
 	asm volatile("									\
@@ -2020,7 +2012,6 @@ __naked void signed_unsigned_intersection32_case1(void *ctx)
 
 SEC("socket")
 __success
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void signed_unsigned_intersection32_case2(void *ctx)
 {
 	asm volatile("									\
@@ -2076,7 +2067,6 @@ __naked void refinement_32bounds_not_overwriting_64bounds(void *ctx)
 SEC("socket")
 __description("dead branch: tnums give impossible constant if equal")
 __success
-__flag(BPF_F_TEST_REG_INVARIANTS)
 __naked void tnums_equal_impossible_constant(void *ctx)
 {
 	asm volatile("										\
-- 
2.43.0

Re: [PATCH v2 bpf-next 1/6] bpf: Refactor reg_bounds_sanity_check

[Shung-Hsi Yu]

On Fri, Mar 20, 2026 at 05:47:45PM +0100, Paul Chaignon wrote:
> From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> 
> This commit refactors reg_bounds_sanity_check to factor out the logic
> that performs the sanity check from the logic that does the reporting.
> 
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

> ---
>  kernel/bpf/verifier.c | 50 ++++++++++++++++++++++++++++++-------------
>  1 file changed, 35 insertions(+), 15 deletions(-)
...
> +static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
> +{
>  	if (tnum_is_const(reg->var_off)) {
>  		u64 uval = reg->var_off.value;
>  		s64 sval = (s64)uval;
>  
>  		if (reg->umin_value != uval || reg->umax_value != uval ||
>  		    reg->smin_value != sval || reg->smax_value != sval) {
> -			msg = "const tnum out of sync with range bounds";
> -			goto out;
> +			return true;

Off topic: despite I acked the addition of these check, I can no longer
recall the exact rational. This now just seems to me to report when the
bounds have not converge (in reg_bounds_sync?).

Anyway, good to keep it as-is for now.

...

Re: [PATCH v2 bpf-next 2/6] bpf: Use bpf_verifier_env buffers for reg_set_min_max

[Shung-Hsi Yu]

On Fri, Mar 20, 2026 at 05:49:09PM +0100, Paul Chaignon wrote:
> In a subsequent patch, the regs_refine_cond_op and reg_bounds_sync
> functions will be called in is_branch_taken instead of reg_set_min_max,
> to simulate each branch's outcome. Since they will run before we branch
> out, these two functions will need to work on temporary registers for
> the two branches.
> 
> This refactoring patch prepares for that change, by introducing the
> temporary registers on bpf_verifier_env and using them in
> reg_set_min_max.
> 
> This change also allows us to save one fake_reg slot as we don't need to
> allocate an additional temporary buffer in case of a BPF_K condition.
> 
> Finally, you may notice that this patch removes the check for
> "false_reg1 == false_reg2" in reg_set_min_max. That check was introduced
> in commit d43ad9da8052 ("bpf: Skip bounds adjustment for conditional
> jumps on same scalar register") to avoid an invariant violation. Given
> that "env->false_reg1 == env->false_reg2" doesn't make sense and
> invariant violations are addressed in a subsequent commit, this patch
> just removes the check.
> 
> Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
> 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>

LGTM. Cleanup around the (to-be-removed) reg_set_min_max() looks nice.

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

...

Re: [PATCH v2 bpf-next 3/6] bpf: Exit early if reg_bounds_sync gets invalid inputs

[Shung-Hsi Yu]

On Fri, Mar 20, 2026 at 05:49:30PM +0100, Paul Chaignon wrote:
> From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> 
> In the subsequent commit, to prune dead branches we will rely on
> detecting ill-formed ranges using range_bounds_violations()
> (e.g., umin > umax) after refining register bounds using
> regs_refine_cond_op().
> 
> However, reg_bounds_sync() can sometimes "repair" ill-formed bounds,
> potentially masking a violation that was produced by
> regs_refine_cond_op().
> 
> This commit modifies reg_bounds_sync() to exit early if an invariant
> violation is already present in the input.
> 
> This ensures ill-formed reg_states remain ill-formed after
> reg_bounds_sync(), allowing simulate_both_branches_taken() to correctly
> identify dead branches with a single check to range_bounds_violation().
> 
> Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

Thought given reg_bounds_sync() is used if various different places, I
wonder how this will affect current syzbot reporting. In comparison the
rest of the patchset seems to try to preserve current behavior.

Being nosey, I also look at the Sashiko review[1], which gave the
following review:

  Does returning early here expose invalid bounds to
  reg_bounds_sanity_check()?
  When regs_refine_cond_op() produces overlapping bounds for logically dead
  branches (e.g., umin > umax), reg_bounds_sync() previously repaired them.
  With this early exit, the invalid bounds remain.
  Will the subsequent call to reg_bounds_sanity_check() detect this violation
  and trigger a kernel warning via verifier_bug() and BPF_WARN_ONCE?
  Additionally, since reg_bounds_sanity_check() handles failures by marking
  the register as unbounded, could this cause the verifier to explore dead
  branches with unconstrained registers and falsely reject valid programs?
  While this is resolved in the subsequent commit "bpf: Simulate branches to
  prune based on range violations", could this intermediate state break
  git bisectability?

Given if we get invalid bounds in reg_bounds_sync() to begin with, then
there is no guarantee that what the BPF verifier ended up with can be
trusted at all, so returning early shouldn't introduce new safety issue,
and the rest about falsely rejecting valid program doesn't seem like a
concern, too, for similar reason.

1: https://sashiko.dev/#/patchset/cover.1774025082.git.paul.chaignon%40gmail.com

...

Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Shung-Hsi Yu]

On Fri, Mar 20, 2026 at 05:49:44PM +0100, Paul Chaignon wrote:
> From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> 
> This patch fixes the invariant violations that can happen after we
> refine ranges & tnum based on an incorrectly-detected branch condition.
> For example, the branch is always true, but we miss it in
> is_branch_taken; we then refine based on the branch being false and end
> up with incoherent ranges (e.g. umax < umin).
> 
> To avoid this, we can simulate the refinement on both branches. More
> specifically, this patch simulates both branches taken using
> regs_refine_cond_op and reg_bounds_sync. If the resulting register
> states are ill-formed on one of the branches, is_branch_taken can mark
> that branch as "never taken".
> 
> On a more formal note, we can deduce a branch is not taken when
> regs_refine_cond_op or reg_bounds_sync returns an ill-formed state
> because the branch operators are sound (formally verified). Soundness

Nit1: would be nice to get a link or at least mentioning of Agni,
otherwise it is not obvious where this claim comes from. And that seems
like a healthy dose of project promotion, too.

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

...
> +/* Learn more information about live branches by simulating both branches being
> + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when

Nit2: while this statement is very specific, "sound" is a rather
uncommon vocabulary in current codebase, I see no such usage.

  $ git grep -A1 -ie sound -- kernel/bpf/ Documentation/bpf/
  Documentation/bpf/kfuncs.rst:   no warning will not be a common occurrence or take place without sound
  Documentation/bpf/kfuncs.rst-   justification, but it is a possibility that must be accepted if one is to

> + * the branch is taken, if it produces ill-formed register bounds, it must mean
> + * that the branch is dead.
> + */
> +static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
> +{
...

Re: [PATCH v2 bpf-next 1/6] bpf: Refactor reg_bounds_sanity_check

[Mykyta Yatsenko]

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

> From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
>
> This commit refactors reg_bounds_sanity_check to factor out the logic
> that performs the sanity check from the logic that does the reporting.
>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---
>  kernel/bpf/verifier.c | 50 ++++++++++++++++++++++++++++++-------------
>  1 file changed, 35 insertions(+), 15 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 01c18f4268de..b638ab841c10 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2802,40 +2802,60 @@ static void reg_bounds_sync(struct bpf_reg_state *reg)
>  	__update_reg_bounds(reg);
>  }
>  
> -static int reg_bounds_sanity_check(struct bpf_verifier_env *env,
> -				   struct bpf_reg_state *reg, const char *ctx)
> +static bool range_bounds_violation(struct bpf_reg_state *reg)
>  {
> -	const char *msg;
> -
> -	if (reg->umin_value > reg->umax_value ||
> -	    reg->smin_value > reg->smax_value ||
> -	    reg->u32_min_value > reg->u32_max_value ||
> -	    reg->s32_min_value > reg->s32_max_value) {
> -		    msg = "range bounds violation";
> -		    goto out;
> -	}
> +	return (reg->umin_value > reg->umax_value || reg->smin_value > reg->smax_value ||
> +		reg->u32_min_value > reg->u32_max_value ||
> +		reg->s32_min_value > reg->s32_max_value);
> +}
>  
> +static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
> +{
>  	if (tnum_is_const(reg->var_off)) {
>  		u64 uval = reg->var_off.value;
>  		s64 sval = (s64)uval;
>  
>  		if (reg->umin_value != uval || reg->umax_value != uval ||
>  		    reg->smin_value != sval || reg->smax_value != sval) {
> -			msg = "const tnum out of sync with range bounds";
> -			goto out;
> +			return true;
nit: maybe it's going to look simpler if you rewrite it with early return?
static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
{
	u64 uval = reg->var_off.value;
	s64 sval = (s64)uval;

  	if (!tnum_is_const(reg->var_off))
                return false;

        return reg->umin_value != uval || reg->umax_value != uval ||
               reg->smin_value != sval || reg->smax_value != sval;
}

same principle can be applied to
const_subreg_tnum_out_of_sync_with_range_bounds(), which looks like a
very long function name, will something like
subreg_tnum_range_mismatch() capture the idea?
>  
> +static bool const_subreg_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
> +{
>  	if (tnum_subreg_is_const(reg->var_off)) {
>  		u32 uval32 = tnum_subreg(reg->var_off).value;
>  		s32 sval32 = (s32)uval32;
>  
>  		if (reg->u32_min_value != uval32 || reg->u32_max_value != uval32 ||
>  		    reg->s32_min_value != sval32 || reg->s32_max_value != sval32) {
> -			msg = "const subreg tnum out of sync with range bounds";
> -			goto out;
> +			return true;
>  		}
>  	}
> +	return false;
> +}
> +
> +static int reg_bounds_sanity_check(struct bpf_verifier_env *env,
> +				   struct bpf_reg_state *reg, const char *ctx)
> +{
> +	const char *msg;
> +
> +	if (range_bounds_violation(reg)) {
> +		msg = "range bounds violation";
> +		goto out;
> +	}
> +
> +	if (const_tnum_out_of_sync_with_range_bounds(reg)) {
> +		msg = "const tnum out of sync with range bounds";
> +		goto out;
> +	}
> +
> +	if (const_subreg_tnum_out_of_sync_with_range_bounds(reg)) {
> +		msg = "const subreg tnum out of sync with range bounds";
> +		goto out;
> +	}
Other than those few nits, the change looks good.
>  
>  	return 0;
>  out:
> -- 
> 2.43.0

Re: [PATCH v2 bpf-next 2/6] bpf: Use bpf_verifier_env buffers for reg_set_min_max

[Mykyta Yatsenko]

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

> In a subsequent patch, the regs_refine_cond_op and reg_bounds_sync
> functions will be called in is_branch_taken instead of reg_set_min_max,
> to simulate each branch's outcome. Since they will run before we branch
> out, these two functions will need to work on temporary registers for
> the two branches.
>
> This refactoring patch prepares for that change, by introducing the
> temporary registers on bpf_verifier_env and using them in
> reg_set_min_max.
>
> This change also allows us to save one fake_reg slot as we don't need to
> allocate an additional temporary buffer in case of a BPF_K condition.
>
> Finally, you may notice that this patch removes the check for
> "false_reg1 == false_reg2" in reg_set_min_max. That check was introduced
> in commit d43ad9da8052 ("bpf: Skip bounds adjustment for conditional
> jumps on same scalar register") to avoid an invariant violation. Given
> that "env->false_reg1 == env->false_reg2" doesn't make sense and
> invariant violations are addressed in a subsequent commit, this patch
> just removes the check.
>
> Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
> 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>
> ---
>  include/linux/bpf_verifier.h |  4 ++-
>  kernel/bpf/verifier.c        | 64 +++++++++++++-----------------------
>  2 files changed, 26 insertions(+), 42 deletions(-)
>
> diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
> index 090aa26d1c98..b129e0aaee20 100644
> --- a/include/linux/bpf_verifier.h
> +++ b/include/linux/bpf_verifier.h
> @@ -837,7 +837,9 @@ struct bpf_verifier_env {
>  	u64 scratched_stack_slots;
>  	u64 prev_log_pos, prev_insn_print_pos;
>  	/* buffer used to temporary hold constants as scalar registers */
> -	struct bpf_reg_state fake_reg[2];
> +	struct bpf_reg_state fake_reg[1];
> +	/* buffers used to save updated reg states while simulating branches */
> +	struct bpf_reg_state true_reg1, true_reg2, false_reg1, false_reg2;
I can see Eduard suggested to store this in env to reduce stack usage by
the verifier. The rest of the refactoring looks like a correct
alignment. The only difference with the base version is removal of the
if (false_reg1 == false_reg2) condition, which is explained in the
commit message.
Acked-by: Mykyta Yatsenko <yatsenko@meta.com>
>  	/* buffer used to generate temporary string representations,
>  	 * e.g., in reg_type_str() to generate reg_type string
>  	 */
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index b638ab841c10..fbc29fb96a60 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -17184,10 +17184,6 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
>   * but we don't support that right now.
>   */
>  static int reg_set_min_max(struct bpf_verifier_env *env,
> -			   struct bpf_reg_state *true_reg1,
> -			   struct bpf_reg_state *true_reg2,
> -			   struct bpf_reg_state *false_reg1,
> -			   struct bpf_reg_state *false_reg2,
>  			   u8 opcode, bool is_jmp32)
>  {
>  	int err;
> @@ -17196,30 +17192,23 @@ static int reg_set_min_max(struct bpf_verifier_env *env,
>  	 * variable offset from the compare (unless they were a pointer into
>  	 * the same object, but we don't bother with that).
>  	 */
> -	if (false_reg1->type != SCALAR_VALUE || false_reg2->type != SCALAR_VALUE)
> -		return 0;
> -
> -	/* We compute branch direction for same SCALAR_VALUE registers in
> -	 * is_scalar_branch_taken(). For unknown branch directions (e.g., BPF_JSET)
> -	 * on the same registers, we don't need to adjust the min/max values.
> -	 */
> -	if (false_reg1 == false_reg2)
> +	if (env->false_reg1.type != SCALAR_VALUE || env->false_reg2.type != SCALAR_VALUE)
>  		return 0;
>  
>  	/* fallthrough (FALSE) branch */
> -	regs_refine_cond_op(false_reg1, false_reg2, rev_opcode(opcode), is_jmp32);
> -	reg_bounds_sync(false_reg1);
> -	reg_bounds_sync(false_reg2);
> +	regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
> +	reg_bounds_sync(&env->false_reg1);
> +	reg_bounds_sync(&env->false_reg2);
>  
>  	/* jump (TRUE) branch */
> -	regs_refine_cond_op(true_reg1, true_reg2, opcode, is_jmp32);
> -	reg_bounds_sync(true_reg1);
> -	reg_bounds_sync(true_reg2);
> -
> -	err = reg_bounds_sanity_check(env, true_reg1, "true_reg1");
> -	err = err ?: reg_bounds_sanity_check(env, true_reg2, "true_reg2");
> -	err = err ?: reg_bounds_sanity_check(env, false_reg1, "false_reg1");
> -	err = err ?: reg_bounds_sanity_check(env, false_reg2, "false_reg2");
> +	regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
> +	reg_bounds_sync(&env->true_reg1);
> +	reg_bounds_sync(&env->true_reg2);
> +
> +	err = reg_bounds_sanity_check(env, &env->true_reg1, "true_reg1");
> +	err = err ?: reg_bounds_sanity_check(env, &env->true_reg2, "true_reg2");
> +	err = err ?: reg_bounds_sanity_check(env, &env->false_reg1, "false_reg1");
> +	err = err ?: reg_bounds_sanity_check(env, &env->false_reg2, "false_reg2");
>  	return err;
>  }
>  
> @@ -17597,6 +17586,10 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>  	}
>  
>  	is_jmp32 = BPF_CLASS(insn->code) == BPF_JMP32;
> +	copy_register_state(&env->false_reg1, dst_reg);
> +	copy_register_state(&env->false_reg2, src_reg);
> +	copy_register_state(&env->true_reg1, dst_reg);
> +	copy_register_state(&env->true_reg2, src_reg);
>  	pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
>  	if (pred >= 0) {
>  		/* If we get here with a dst_reg pointer type it is because
> @@ -17661,27 +17654,16 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>  		return PTR_ERR(other_branch);
>  	other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
>  
> -	if (BPF_SRC(insn->code) == BPF_X) {
> -		err = reg_set_min_max(env,
> -				      &other_branch_regs[insn->dst_reg],
> -				      &other_branch_regs[insn->src_reg],
> -				      dst_reg, src_reg, opcode, is_jmp32);
> -	} else /* BPF_SRC(insn->code) == BPF_K */ {
> -		/* reg_set_min_max() can mangle the fake_reg. Make a copy
> -		 * so that these are two different memory locations. The
> -		 * src_reg is not used beyond here in context of K.
> -		 */
> -		memcpy(&env->fake_reg[1], &env->fake_reg[0],
> -		       sizeof(env->fake_reg[0]));
> -		err = reg_set_min_max(env,
> -				      &other_branch_regs[insn->dst_reg],
> -				      &env->fake_reg[0],
> -				      dst_reg, &env->fake_reg[1],
> -				      opcode, is_jmp32);
> -	}
> +	err = reg_set_min_max(env, opcode, is_jmp32);
>  	if (err)
>  		return err;
>  
> +	copy_register_state(dst_reg, &env->false_reg1);
> +	copy_register_state(src_reg, &env->false_reg2);
> +	copy_register_state(&other_branch_regs[insn->dst_reg], &env->true_reg1);
> +	if (BPF_SRC(insn->code) == BPF_X)
> +		copy_register_state(&other_branch_regs[insn->src_reg], &env->true_reg2);
> +
>  	if (BPF_SRC(insn->code) == BPF_X &&
>  	    src_reg->type == SCALAR_VALUE && src_reg->id &&
>  	    !WARN_ON_ONCE(src_reg->id != other_branch_regs[insn->src_reg].id)) {
> -- 
> 2.43.0

Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Mykyta Yatsenko]

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

> From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
>
> This patch fixes the invariant violations that can happen after we
> refine ranges & tnum based on an incorrectly-detected branch condition.
> For example, the branch is always true, but we miss it in
> is_branch_taken; we then refine based on the branch being false and end
> up with incoherent ranges (e.g. umax < umin).
>
> To avoid this, we can simulate the refinement on both branches. More
> specifically, this patch simulates both branches taken using
> regs_refine_cond_op and reg_bounds_sync. If the resulting register
> states are ill-formed on one of the branches, is_branch_taken can mark
> that branch as "never taken".
>
> On a more formal note, we can deduce a branch is not taken when
> regs_refine_cond_op or reg_bounds_sync returns an ill-formed state
> because the branch operators are sound (formally verified). Soundness
> means that the verifier is guaranteed to produce sound outputs on the
> taken branches. On the non-taken branch (explored because of
> imprecision in the bounds), the verifier is free to produce any output.
> We use ill-formedness as a signal that the branch is dead and prune
> that branch.
>
> This patch moves the refinement logic for both branches from
> reg_set_min_max to their own function, simulate_both_branches_taken,
> which is called from is_scalar_branch_taken. As a result,
> reg_set_min_max now only runs sanity checks and has been renamed to
> reg_bounds_sanity_check_branches to reflect that.
>
> We have had five patches fixing specific cases of invariant violations
> in the past, all added with selftests:
> - commit fbc7aef517d8 ("bpf: Fix u32/s32 bounds when ranges cross
>   min/max boundary")
> - commit efc11a667878 ("bpf: Improve bounds when tnum has a single
>   possible value")
> - commit f41345f47fb2 ("bpf: Use tnums for JEQ/JNE is_branch_taken
>   logic")
> - commit 00bf8d0c6c9b ("bpf: Improve bounds when s64 crosses sign
>   boundary")
> - commit 6279846b9b25 ("bpf: Forget ranges when refining tnum after
>   JSET")
>
> To confirm that this patch addresses all invariant violations, we have
> also reverted those five commits and verified that their related
> selftests don't cause any invariant violation warnings anymore. Those
> selftests still fail but only because of mis-detected branches or
> less-precise bounds than expected. This demonstrates that the current
> patch is enough to avoid the invariant violation warning AND that the
> previous five patches are still useful to improve branch detection.
>
> In addition to the selftests, this change was also tested with the
> Cilium complexity test suite: all programs were successfully loaded and
> it didn't change the number of processed instructions.
>
> Reported-by: syzbot+c950cc277150935cc0b5@syzkaller.appspotmail.com
> Closes: https://syzkaller.appspot.com/bug?extid=c950cc277150935cc0b5
> Co-developed-by: Paul Chaignon <paul.chaignon@gmail.com>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> 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 | 84 +++++++++++++++++++++++++------------------
>  1 file changed, 49 insertions(+), 35 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 8d7ad5f21ed6..0b4f622efec1 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -16717,11 +16717,48 @@ static void find_good_pkt_pointers(struct bpf_verifier_state *vstate,
>  	}));
>  }
>  
> +static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> +				u8 opcode, bool is_jmp32);
> +static u8 rev_opcode(u8 opcode);
> +
> +/* Learn more information about live branches by simulating both branches being
> + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when
> + * the branch is taken, if it produces ill-formed register bounds, it must mean
> + * that the branch is dead.
> + */
Sorry for being nit-picky, could you please use kernel style comment style +
maybe reword it a little bit, instead of:

/*
 * Because regs_refine_cond_op is sound when
 * the branch is taken, if it produces ill-formed register bounds, it must mean
 * that the branch is dead.
 */
Something like:
/*
 * regs_refine_cond_op() is sound, so producing ill-formed register
 * bounds for the branch means that branch is dead.
 */

> +static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
> +{
> +	/* Fallthrough (FALSE) branch */
> +	regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
> +	reg_bounds_sync(&env->false_reg1);
> +	reg_bounds_sync(&env->false_reg2);
This is probably more related to patch 2: is it necessary to have both
true/false_reg1/2 pairs, it looks like we process false branch before
the true branch and they never intersect, don't they? So it worth
removing a pair of bpf_reg_states from env?
> +	/* 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))
> +		return 1;
> +
> +	/* Jump (TRUE) branch */
> +	regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
> +	reg_bounds_sync(&env->true_reg1);
> +	reg_bounds_sync(&env->true_reg2);
> +	/* 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))
> +		return 0;
> +
> +	/* Both branches are possible, we can't determine which one will be taken. */
> +	return -1;
> +}
> +
>  /*
>   * <reg1> <op> <reg2>, currently assuming reg2 is a constant
>   */
> -static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> -				  u8 opcode, bool is_jmp32)
> +static int is_scalar_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
> +				  struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
>  {
>  	struct tnum t1 = is_jmp32 ? tnum_subreg(reg1->var_off) : reg1->var_off;
>  	struct tnum t2 = is_jmp32 ? tnum_subreg(reg2->var_off) : reg2->var_off;
> @@ -16873,7 +16910,7 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
>  		break;
>  	}
>  
> -	return -1;
> +	return simulate_both_branches_taken(env, opcode, is_jmp32);
>  }
>  
>  static int flip_opcode(u32 opcode)
> @@ -16944,8 +16981,8 @@ static int is_pkt_ptr_branch_taken(struct bpf_reg_state *dst_reg,
>   * -1 - unknown. Example: "if (reg1 < 5)" is unknown when register value
>   *      range [0,10]
>   */
> -static int is_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> -			   u8 opcode, bool is_jmp32)
> +static int is_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
> +			   struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
>  {
>  	if (reg_is_pkt_pointer_any(reg1) && reg_is_pkt_pointer_any(reg2) && !is_jmp32)
>  		return is_pkt_ptr_branch_taken(reg1, reg2, opcode);
> @@ -16983,7 +17020,7 @@ static int is_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg
>  	}
>  
>  	/* now deal with two scalars, but not necessarily constants */
> -	return is_scalar_branch_taken(reg1, reg2, opcode, is_jmp32);
> +	return is_scalar_branch_taken(env, reg1, reg2, opcode, is_jmp32);
>  }
>  
>  /* Opcode that corresponds to a *false* branch condition.
> @@ -17074,8 +17111,8 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
>  			/* u32_min_value is not equal to 0xffffffff at this point,
>  			 * because otherwise u32_max_value is 0xffffffff as well,
>  			 * in such a case both reg1 and reg2 would be constants,
> -			 * jump would be predicted and reg_set_min_max() won't
> -			 * be called.
> +			 * jump would be predicted and regs_refine_cond_op()
> +			 * wouldn't be called.
>  			 *
>  			 * Same reasoning works for all {u,s}{min,max}{32,64} cases
>  			 * below.
> @@ -17182,34 +17219,11 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
>  	}
>  }
>  
> -/* Adjusts the register min/max values in the case that the dst_reg and
> - * src_reg are both SCALAR_VALUE registers (or we are simply doing a BPF_K
> - * check, in which case we have a fake SCALAR_VALUE representing insn->imm).
> - * Technically we can do similar adjustments for pointers to the same object,
> - * but we don't support that right now.
> - */
> -static int reg_set_min_max(struct bpf_verifier_env *env,
> -			   u8 opcode, bool is_jmp32)
> +/* Check for invariant violations on the registers for both branches of a condition */
> +static int regs_bounds_sanity_check_branches(struct bpf_verifier_env *env)
>  {
>  	int err;
>  
> -	/* If either register is a pointer, we can't learn anything about its
> -	 * variable offset from the compare (unless they were a pointer into
> -	 * the same object, but we don't bother with that).
> -	 */
> -	if (env->false_reg1.type != SCALAR_VALUE || env->false_reg2.type != SCALAR_VALUE)
> -		return 0;
> -
> -	/* fallthrough (FALSE) branch */
> -	regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
> -	reg_bounds_sync(&env->false_reg1);
> -	reg_bounds_sync(&env->false_reg2);
> -
> -	/* jump (TRUE) branch */
> -	regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
> -	reg_bounds_sync(&env->true_reg1);
> -	reg_bounds_sync(&env->true_reg2);
> -
>  	err = reg_bounds_sanity_check(env, &env->true_reg1, "true_reg1");
>  	err = err ?: reg_bounds_sanity_check(env, &env->true_reg2, "true_reg2");
>  	err = err ?: reg_bounds_sanity_check(env, &env->false_reg1, "false_reg1");
> @@ -17595,7 +17609,7 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>  	copy_register_state(&env->false_reg2, src_reg);
>  	copy_register_state(&env->true_reg1, dst_reg);
>  	copy_register_state(&env->true_reg2, src_reg);
> -	pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
> +	pred = is_branch_taken(env, dst_reg, src_reg, opcode, is_jmp32);
>  	if (pred >= 0) {
>  		/* If we get here with a dst_reg pointer type it is because
>  		 * above is_branch_taken() special cased the 0 comparison.
> @@ -17659,7 +17673,7 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>  		return PTR_ERR(other_branch);
>  	other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
>  
> -	err = reg_set_min_max(env, opcode, is_jmp32);
> +	err = regs_bounds_sanity_check_branches(env);
>  	if (err)
>  		return err;
>  
> -- 
> 2.43.0

Re: [PATCH v2 bpf-next 5/6] selftests/bpf: Cover invariant violation cases from syzbot

[Mykyta Yatsenko]

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

> This patch adds a selftest for the change in the previous patch. The
> selftest is derived from a syzbot reproducer from [1] (among the 22
> reproducers on that page, only 4 still reproduced on latest bpf tree,
> all being small variants of the same invariant violation).
>
> The test case failure without the previous patch is shown below.
>
>   0: R1=ctx() R10=fp0
>   0: (85) call bpf_get_prandom_u32#7    ; R0=scalar()
>   1: (bf) r5 = r0                       ; R0=scalar(id=1) R5=scalar(id=1)
>   2: (57) r5 &= -4                      ; R5=scalar(smax=0x7ffffffffffffffc,umax=0xfffffffffffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; 0xfffffffffffffffc))
>   3: (bf) r7 = r0                       ; R0=scalar(id=1) R7=scalar(id=1)
>   4: (57) r7 &= 1                       ; R7=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
>   5: (07) r7 += -43                     ; R7=scalar(smin=smin32=-43,smax=smax32=-42,umin=0xffffffffffffffd5,umax=0xffffffffffffffd6,umin32=0xffffffd5,umax32=0xffffffd6,var_off=(0xffffffffffffffd4; 0x3))
>   6: (5e) if w5 != w7 goto pc+1
>   verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xffffffd5, 0xffffffffffffffd4] s64=[0x80000000ffffffd5, 0x7fffffffffffffd4] u32=[0xffffffd5, 0xffffffd4] s32=[0xffffffd5, 0xffffffd4] var_off=(0xffffffd4, 0xffffffff00000000)
>
> R5 and R7 are prepared such that their tnums intersection results in a
> known constant but that constant isn't within R7's u32 bounds.
> is_branch_taken isn't able to detect this case today, so the verifier
> walks the impossible fallthrough branch. After regs_refine_cond_op and
> reg_bounds_sync refine R5 on the assumption that the branch is taken,
> the impossibility becomes apparent and results in an invariant violation
> for R5: umin32 is greater than umax32.
>
> The previous patch fixes this by using regs_refine_cond_op and
> reg_bounds_sync in is_branch_taken to detect the impossible branch. The
> fallthrough branch is therefore correctly detected as dead code.
>
> Link: https://syzkaller.appspot.com/bug?extid=c950cc277150935cc0b5 [1]
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---
>  .../selftests/bpf/progs/verifier_bounds.c     | 24 +++++++++++++++++++
>  1 file changed, 24 insertions(+)
>
> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> index 3724d5e5bcb3..818efa08404d 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> @@ -2070,4 +2070,28 @@ __naked void refinement_32bounds_not_overwriting_64bounds(void *ctx)
>  	: __clobber_all);
>  }
>  
> +/* Last jump can be detected as always taken because the intersection of R5 and
> + * R7 32bit tnums produces a constant that isn't within R7's s32 bounds.
> + */
> +SEC("socket")
> +__description("dead branch: tnums give impossible constant if equal")
> +__success
> +__flag(BPF_F_TEST_REG_INVARIANTS)
> +__naked void tnums_equal_impossible_constant(void *ctx)
> +{
> +	asm volatile("										\
> +	call %[bpf_get_prandom_u32];								\
> +	r5 = r0;										\
> +	r5 &= 0xfffffffffffffffc;	/* var_off32=(0; 0xfffffffc) */				\
> +	r7 = r0;										\
> +	r7 &= 0x1;			/* var_off32=(0x0; 0x1) */				\
> +	r7 += -43;			/* s32=[-43; -42] & var_off32=(0xffffffd4; 0x3) */	\
> +	if w5 != w7 goto +1;		/* on fallthrough var_off32=-44, not in s32 */		\
w5 has bits 0,1 zero, rest unknown
w7 has top bits known as 0xffffffd4, and bits 0,1 unknown
If w5 == w7, their tnums must intersect to a single
value = 0xffffffd4(-44). Which is outside of w7's range [-43; 42]. So
the r10 = 0 branch should be unreachable.
I guess the comment should be updated to the kernel style as well.
Acked-by: Mykyta Yatsenko <yatsenko@meta.com>
> +	r10 = 0;										\
> +	exit;											\
> +"	:
> +	: __imm(bpf_get_prandom_u32)
> +	: __clobber_all);
> +}
> +
>  char _license[] SEC("license") = "GPL";
> -- 
> 2.43.0

Re: [PATCH v2 bpf-next 6/6] selftests/bpf: Remove invariant violation flags

[Mykyta Yatsenko]

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

> With the changes to the verifier in previous commits, we're not
> expecting any invariant violations anymore. We should therefore always
> enable BPF_F_TEST_REG_INVARIANTS to fail on invariant violations. Turns
> out that's already the case and we've been explicitly setting this flag
> in selftests when it wasn't necessary. This commit removes those flags
> from selftests, which should hopefully make clearer that it's always
> enabled.
>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---
BPF_F_TEST_REG_INVARIANTS is included in testing_prog_flags() from
testing_helpers.c which is used for loading verifier test programs, the
change looks good.
Acked-by: Mykyta Yatsenko <yatsenko@meta.com>
>  .../selftests/bpf/progs/verifier_bounds.c     | 24 ++++++-------------
>  1 file changed, 7 insertions(+), 17 deletions(-)
>
> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> index 818efa08404d..1ebc99d75862 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> @@ -1066,7 +1066,6 @@ l0_%=:	r0 = 0;						\
>  SEC("xdp")
>  __description("bound check with JMP_JSLT for crossing 64-bit signed boundary")
>  __success __retval(0)
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void crossing_64_bit_signed_boundary_2(void)
>  {
>  	asm volatile ("					\
> @@ -1148,7 +1147,6 @@ l0_%=:	r0 = 0;						\
>  SEC("xdp")
>  __description("bound check with JMP32_JSLT for crossing 32-bit signed boundary")
>  __success __retval(0)
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void crossing_32_bit_signed_boundary_2(void)
>  {
>  	asm volatile ("					\
> @@ -1536,7 +1534,7 @@ __naked void sub32_partial_overflow(void)
>  SEC("socket")
>  __description("dead branch on jset, does not result in invariants violation error")
>  __success __log_level(2)
> -__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__retval(0)
>  __naked void jset_range_analysis(void)
>  {
>  	asm volatile ("			\
> @@ -1572,7 +1570,7 @@ l0_%=:	r0 = 0;				\
>   */
>  SEC("socket")
>  __description("bounds deduction cross sign boundary, negative overlap")
> -__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__success __log_level(2)
>  __msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=smin32=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,umin32=0xfffffd71,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")
>  __retval(0)
>  __naked void bounds_deduct_negative_overlap(void)
> @@ -1616,7 +1614,7 @@ l0_%=:	r0 = 0;				\
>   */
>  SEC("socket")
>  __description("bounds deduction cross sign boundary, positive overlap")
> -__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__success __log_level(2)
>  __msg("3: (2d) if r0 > r1 {{.*}} R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=127,var_off=(0x0; 0x7f))")
>  __retval(0)
>  __naked void bounds_deduct_positive_overlap(void)
> @@ -1649,7 +1647,7 @@ l0_%=:	r0 = 0;				\
>   */
>  SEC("socket")
>  __description("bounds deduction cross sign boundary, two overlaps")
> -__failure __flag(BPF_F_TEST_REG_INVARIANTS)
> +__failure
>  __msg("3: (2d) if r0 > r1 {{.*}} R0=scalar(smin=smin32=-128,smax=smax32=127,umax=0xffffffffffffff80)")
>  __msg("frame pointer is read only")
>  __naked void bounds_deduct_two_overlaps(void)
> @@ -1713,7 +1711,7 @@ SEC("socket")
>  __description("conditional jump on same register, branch taken")
>  __not_msg("20: (b7) r0 = 1 {{.*}} R0=1")
>  __success __log_level(2)
> -__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__retval(0)
>  __naked void condition_jump_on_same_register(void *ctx)
>  {
>  	asm volatile("			\
> @@ -1748,7 +1746,7 @@ SEC("socket")
>  __description("jset on same register, constant value branch taken")
>  __not_msg("7: (b7) r0 = 1 {{.*}} R0=1")
>  __success __log_level(2)
> -__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__retval(0)
>  __naked void jset_on_same_register_1(void *ctx)
>  {
>  	asm volatile("			\
> @@ -1770,7 +1768,7 @@ SEC("socket")
>  __description("jset on same register, scalar value branch taken")
>  __not_msg("12: (b7) r0 = 1 {{.*}} R0=1")
>  __success __log_level(2)
> -__retval(0) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__retval(0)
>  __naked void jset_on_same_register_2(void *ctx)
>  {
>  	asm volatile("			\
> @@ -1800,7 +1798,6 @@ __description("jset on same register, scalar value unknown branch 1")
>  __msg("3: (b7) r0 = 0 {{.*}} R0=0")
>  __msg("5: (b7) r0 = 1 {{.*}} R0=1")
>  __success __log_level(2)
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void jset_on_same_register_3(void *ctx)
>  {
>  	asm volatile("			\
> @@ -1822,7 +1819,6 @@ __description("jset on same register, scalar value unknown branch 2")
>  __msg("4: (b7) r0 = 0 {{.*}} R0=0")
>  __msg("6: (b7) r0 = 1 {{.*}} R0=1")
>  __success __log_level(2)
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void jset_on_same_register_4(void *ctx)
>  {
>  	asm volatile("			\
> @@ -1845,7 +1841,6 @@ __description("jset on same register, scalar value unknown branch 3")
>  __msg("4: (b7) r0 = 0 {{.*}} R0=0")
>  __msg("6: (b7) r0 = 1 {{.*}} R0=1")
>  __success __log_level(2)
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void jset_on_same_register_5(void *ctx)
>  {
>  	asm volatile("			\
> @@ -1877,7 +1872,6 @@ SEC("socket")
>  __description("bounds refinement with single-value tnum on umax")
>  __msg("3: (15) if r0 == 0xe0 {{.*}} R0=240")
>  __success __log_level(2)
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void bounds_refinement_tnum_umax(void *ctx)
>  {
>  	asm volatile("			\
> @@ -1907,7 +1901,6 @@ SEC("socket")
>  __description("bounds refinement with single-value tnum on umin")
>  __msg("3: (15) if r0 == 0xf0 {{.*}} R0=224")
>  __success __log_level(2)
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void bounds_refinement_tnum_umin(void *ctx)
>  {
>  	asm volatile("			\
> @@ -2002,7 +1995,6 @@ __naked void bounds_refinement_multiple_overlaps(void *ctx)
>  
>  SEC("socket")
>  __success
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void signed_unsigned_intersection32_case1(void *ctx)
>  {
>  	asm volatile("									\
> @@ -2020,7 +2012,6 @@ __naked void signed_unsigned_intersection32_case1(void *ctx)
>  
>  SEC("socket")
>  __success
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void signed_unsigned_intersection32_case2(void *ctx)
>  {
>  	asm volatile("									\
> @@ -2076,7 +2067,6 @@ __naked void refinement_32bounds_not_overwriting_64bounds(void *ctx)
>  SEC("socket")
>  __description("dead branch: tnums give impossible constant if equal")
>  __success
> -__flag(BPF_F_TEST_REG_INVARIANTS)
>  __naked void tnums_equal_impossible_constant(void *ctx)
>  {
>  	asm volatile("										\
> -- 
> 2.43.0

Re: [PATCH v2 bpf-next 2/6] bpf: Use bpf_verifier_env buffers for reg_set_min_max

[Eduard Zingerman]

On Fri, 2026-03-20 at 17:49 +0100, Paul Chaignon wrote:
> In a subsequent patch, the regs_refine_cond_op and reg_bounds_sync
> functions will be called in is_branch_taken instead of reg_set_min_max,
> to simulate each branch's outcome. Since they will run before we branch
> out, these two functions will need to work on temporary registers for
> the two branches.
> 
> This refactoring patch prepares for that change, by introducing the
> temporary registers on bpf_verifier_env and using them in
> reg_set_min_max.
> 
> This change also allows us to save one fake_reg slot as we don't need to
> allocate an additional temporary buffer in case of a BPF_K condition.
> 
> Finally, you may notice that this patch removes the check for
> "false_reg1 == false_reg2" in reg_set_min_max. That check was introduced
> in commit d43ad9da8052 ("bpf: Skip bounds adjustment for conditional
> jumps on same scalar register") to avoid an invariant violation. Given
> that "env->false_reg1 == env->false_reg2" doesn't make sense and
> invariant violations are addressed in a subsequent commit, this patch
> just removes the check.
> 
> Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
> 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>

[...]

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index b638ab841c10..fbc29fb96a60 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -17184,10 +17184,6 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
>   * but we don't support that right now.
>   */
>  static int reg_set_min_max(struct bpf_verifier_env *env,
> -			   struct bpf_reg_state *true_reg1,
> -			   struct bpf_reg_state *true_reg2,
> -			   struct bpf_reg_state *false_reg1,
> -			   struct bpf_reg_state *false_reg2,
>  			   u8 opcode, bool is_jmp32)
>  {
>  	int err;
> @@ -17196,30 +17192,23 @@ static int reg_set_min_max(struct bpf_verifier_env *env,
>  	 * variable offset from the compare (unless they were a pointer into
>  	 * the same object, but we don't bother with that).
>  	 */
> -	if (false_reg1->type != SCALAR_VALUE || false_reg2->type != SCALAR_VALUE)
> -		return 0;
> -
> -	/* We compute branch direction for same SCALAR_VALUE registers in
> -	 * is_scalar_branch_taken(). For unknown branch directions (e.g., BPF_JSET)
> -	 * on the same registers, we don't need to adjust the min/max values.
> -	 */
> -	if (false_reg1 == false_reg2)

A side note:

The above hunk was added as a part of [1] to mitigate some invariant
violation errors. Surprisingly, none of the tests added in [1] fail
on current master if above hunk is commented out. Probably due to
recent improvements in bounds deduction. Should we remove these
tests as a part of the series?

[1] https://lore.kernel.org/all/20251103063108.1111764-3-kafai.wan@linux.dev/

[...]

Re: [PATCH v2 bpf-next 3/6] bpf: Exit early if reg_bounds_sync gets invalid inputs

[Eduard Zingerman]

On Fri, 2026-03-20 at 17:49 +0100, Paul Chaignon wrote:

[...]

> @@ -2786,8 +2786,13 @@ 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 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))
> +		return;
>  	/* We might have learned new bounds from the var_off. */
>  	__update_reg_bounds(reg);
>  	/* We might have learned something about the sign bit. */

Is it possible for the invariants violation to manifest after
__update_reg{32,64}_bounds() calls, once cross domain boundaries are
propagated?

Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Eduard Zingerman]

On Fri, 2026-03-20 at 17:49 +0100, Paul Chaignon wrote:

[...]

> @@ -16717,11 +16717,48 @@ static void find_good_pkt_pointers(struct bpf_verifier_state *vstate,
>  	}));
>  }
>  
> +static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> +				u8 opcode, bool is_jmp32);
> +static u8 rev_opcode(u8 opcode);
> +
> +/* Learn more information about live branches by simulating both branches being
> + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when
> + * the branch is taken, if it produces ill-formed register bounds, it must mean
> + * that the branch is dead.
> + */
> +static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
> +{
> +	/* Fallthrough (FALSE) branch */
> +	regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
> +	reg_bounds_sync(&env->false_reg1);
> +	reg_bounds_sync(&env->false_reg2);
> +	/* 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))
> +		return 1;
> +
> +	/* Jump (TRUE) branch */
> +	regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
> +	reg_bounds_sync(&env->true_reg1);
> +	reg_bounds_sync(&env->true_reg2);
> +	/* 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))
> +		return 0;

Why did you chose to limit these checks to range_bounds_violation(),
excluding const_{subreg_,}tnum_out_of_sync_with_range_bounds()?

Also, it appears that tnum bounds checking functions are unnecessarily
restricted and should be implemented as follows:

  static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
  {

        u64 tnum_umin = reg->var_off.value;
        u64 tnum_umax = reg->var_off.value | reg->var_off.mask;
        s64 tnum_smin = (s64)tnum_umin;
        s64 tnum_smax = (s64)tnum_smax;

	// check that [tnum_umin, tnum_umax] and [reg->umin_value, reg->umax_value] intersect
	// check that [tnum_smin, tnum_smax] and [reg->smin_value, reg->smax_value] intersect
        return ...;
  }

Wdyt?

> +
> +	/* Both branches are possible, we can't determine which one will be taken. */
> +	return -1;
> +}
> +
>  /*
>   * <reg1> <op> <reg2>, currently assuming reg2 is a constant
>   */
> -static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> -				  u8 opcode, bool is_jmp32)
> +static int is_scalar_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
> +				  struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
>  {
>  	struct tnum t1 = is_jmp32 ? tnum_subreg(reg1->var_off) : reg1->var_off;
>  	struct tnum t2 = is_jmp32 ? tnum_subreg(reg2->var_off) : reg2->var_off;

[...]

Re: [PATCH v2 bpf-next 1/6] bpf: Refactor reg_bounds_sanity_check

[Harishankar Vishwanathan]

On Mon, Mar 23, 2026 at 10:16 AM Mykyta Yatsenko
<mykyta.yatsenko5@gmail.com> wrote:
>
> Paul Chaignon <paul.chaignon@gmail.com> writes:
>
> > From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> >
[...]
> nit: maybe it's going to look simpler if you rewrite it with early return?
> static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
> {
>         u64 uval = reg->var_off.value;
>         s64 sval = (s64)uval;
>
>         if (!tnum_is_const(reg->var_off))
>                 return false;
>
>         return reg->umin_value != uval || reg->umax_value != uval ||
>                reg->smin_value != sval || reg->smax_value != sval;
> }

Sounds good, this makes sense!

> same principle can be applied to
> const_subreg_tnum_out_of_sync_with_range_bounds(), which looks like a
> very long function name, will something like
> subreg_tnum_range_mismatch() capture the idea?

It is specifically checking for a *const* tnum and range mismatch, not
just any tnum,
so I'd assume we want to capture that when naming.
Perhaps we call these const_tnum_range_mismatch and
const_tnum_range_mismatch_32?

[...]
> Other than those few nits, the change looks good.
> >
> >       return 0;
> >  out:
> > --
> > 2.43.0

Re: [PATCH v2 bpf-next 3/6] bpf: Exit early if reg_bounds_sync gets invalid inputs

[Harishankar Vishwanathan]

On Mon, Mar 23, 2026 at 8:12 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>
> On Fri, Mar 20, 2026 at 05:49:30PM +0100, Paul Chaignon wrote:
> > From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
[...]
> Thought given reg_bounds_sync() is used if various different places, I
> wonder how this will affect current syzbot reporting. In comparison the
> rest of the patchset seems to try to preserve current behavior.
>
> Being nosey, I also look at the Sashiko review[1], which gave the
> following review:
>
>   Does returning early here expose invalid bounds to
>   reg_bounds_sanity_check()?
>   When regs_refine_cond_op() produces overlapping bounds for logically dead
>   branches (e.g., umin > umax), reg_bounds_sync() previously repaired them.
>   With this early exit, the invalid bounds remain.
>   Will the subsequent call to reg_bounds_sanity_check() detect this violation
>   and trigger a kernel warning via verifier_bug() and BPF_WARN_ONCE?
>   Additionally, since reg_bounds_sanity_check() handles failures by marking
>   the register as unbounded, could this cause the verifier to explore dead
>   branches with unconstrained registers and falsely reject valid programs?
>   While this is resolved in the subsequent commit "bpf: Simulate branches to
>   prune based on range violations", could this intermediate state break
>   git bisectability?
>
> Given if we get invalid bounds in reg_bounds_sync() to begin with, then
> there is no guarantee that what the BPF verifier ended up with can be
> trusted at all, so returning early shouldn't introduce new safety issue,
> and the rest about falsely rejecting valid program doesn't seem like a
> concern, too, for similar reason.

Thanks for taking a look at the review!

As you know, the main reason for this commit is to allow the next
commit to identify dead branches
with a single call to range_bounds_violation(), instead of two calls
(one after regs_refine_cond_op(),
and one after sync()).

You are right, if the inputs to sync() itself are invalid, then
whatever "fixes" sync()
can come up with don't make sense anyway. So it should be okay to exit early.

One argument to keep sync() unchanged is, as you say, to "preserve
existing behavior".

I'm okay either way. If it makes sense to keep sync() unchanged + use
two calls to range_bounds_violation(), please advise.
Otherwise will continue with this commit.

> 1: https://sashiko.dev/#/patchset/cover.1774025082.git.paul.chaignon%40gmail.com
>
> ...

Re: [PATCH v2 bpf-next 1/6] bpf: Refactor reg_bounds_sanity_check

[Mykyta Yatsenko]

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

> On Mon, Mar 23, 2026 at 10:16 AM Mykyta Yatsenko
> <mykyta.yatsenko5@gmail.com> wrote:
>>
>> Paul Chaignon <paul.chaignon@gmail.com> writes:
>>
>> > From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
>> >
> [...]
>> nit: maybe it's going to look simpler if you rewrite it with early return?
>> static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
>> {
>>         u64 uval = reg->var_off.value;
>>         s64 sval = (s64)uval;
>>
>>         if (!tnum_is_const(reg->var_off))
>>                 return false;
>>
>>         return reg->umin_value != uval || reg->umax_value != uval ||
>>                reg->smin_value != sval || reg->smax_value != sval;
>> }
>
> Sounds good, this makes sense!
>
>> same principle can be applied to
>> const_subreg_tnum_out_of_sync_with_range_bounds(), which looks like a
>> very long function name, will something like
>> subreg_tnum_range_mismatch() capture the idea?
>
> It is specifically checking for a *const* tnum and range mismatch, not
> just any tnum,
> so I'd assume we want to capture that when naming.
> Perhaps we call these const_tnum_range_mismatch and
> const_tnum_range_mismatch_32?
Something like that should do, thanks!
>
> [...]
>> Other than those few nits, the change looks good.
>> >
>> >       return 0;
>> >  out:
>> > --
>> > 2.43.0

Re: [PATCH v2 bpf-next 3/6] bpf: Exit early if reg_bounds_sync gets invalid inputs

[Harishankar Vishwanathan]

On Mon, Mar 23, 2026 at 2:47 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Fri, 2026-03-20 at 17:49 +0100, Paul Chaignon wrote:
>
> [...]
>
> > @@ -2786,8 +2786,13 @@ 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 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))
> > +             return;
> >       /* We might have learned new bounds from the var_off. */
> >       __update_reg_bounds(reg);
> >       /* We might have learned something about the sign bit. */
>
> Is it possible for the invariants violation to manifest after
> __update_reg{32,64}_bounds() calls, once cross domain boundaries are
> propagated?

The short answer is yes.

The sub-sync functions, i.e. __update_reg_bounds, __reg_deduce_bounds,
__reg_bound_offset are individually sound (checked by Agni).
This means that they preserve any concrete value x that is contained in all
the range bounds and tnum inputs, after refinement.

But if in the input, there is no concrete value x that is contained in
ALL the range bounds and tnum, then an invariant violation can
manifest. Note that this can happen in the presence
of the current early exit commit, i.e., even if
range_bounds_violation(reg) is false.

For example,

before reg_bounds_sync: s64=[1, 1], tnum=0
after reg_bounds_sync: s64=[1, 0] tnum=0

Could you elaborate on your concern? Did you perhaps imply that we should
be checking for reg_bounds_violation in
simulate_both_branches_taken after each sub-sync function?

Re: [PATCH v2 bpf-next 3/6] bpf: Exit early if reg_bounds_sync gets invalid inputs

[Eduard Zingerman]

On Tue, 2026-03-24 at 15:28 -0400, Harishankar Vishwanathan wrote:
> On Mon, Mar 23, 2026 at 2:47 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Fri, 2026-03-20 at 17:49 +0100, Paul Chaignon wrote:
> > 
> > [...]
> > 
> > > @@ -2786,8 +2786,13 @@ 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 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))
> > > +             return;
> > >       /* We might have learned new bounds from the var_off. */
> > >       __update_reg_bounds(reg);
> > >       /* We might have learned something about the sign bit. */
> > 
> > Is it possible for the invariants violation to manifest after
> > __update_reg{32,64}_bounds() calls, once cross domain boundaries are
> > propagated?
> 
> The short answer is yes.
> 
> The sub-sync functions, i.e. __update_reg_bounds, __reg_deduce_bounds,
> __reg_bound_offset are individually sound (checked by Agni).
> This means that they preserve any concrete value x that is contained in all
> the range bounds and tnum inputs, after refinement.
> 
> But if in the input, there is no concrete value x that is contained in
> ALL the range bounds and tnum, then an invariant violation can
> manifest. Note that this can happen in the presence
> of the current early exit commit, i.e., even if
> range_bounds_violation(reg) is false.
> 
> For example,
> 
> before reg_bounds_sync: s64=[1, 1], tnum=0
> after reg_bounds_sync: s64=[1, 0] tnum=0
> 
> Could you elaborate on your concern? Did you perhaps imply that we should
> be checking for reg_bounds_violation in
> simulate_both_branches_taken after each sub-sync function?

My main concern is that we might loose useful signal.
It would be nice to adjust reg_bounds_sync() such
that it would stop (e.g. return false, as you suggested previously)
if it hits invariant violation mid-step.

Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Harishankar Vishwanathan]

On Mon, Mar 23, 2026 at 12:19 PM Mykyta Yatsenko
<mykyta.yatsenko5@gmail.com> wrote:
>
> Paul Chaignon <paul.chaignon@gmail.com> writes:
>
> > From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> >
[...]
> > +static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> > +                             u8 opcode, bool is_jmp32);
> > +static u8 rev_opcode(u8 opcode);
> > +
> > +/* Learn more information about live branches by simulating both branches being
> > + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when
> > + * the branch is taken, if it produces ill-formed register bounds, it must mean
> > + * that the branch is dead.
> > + */
> Sorry for being nit-picky, could you please use kernel style comment style +

Thanks for the suggestion. To clarify, by kernel-style did you mean
keeping the beginning line empty?
Or something else that I might have missed.

> maybe reword it a little bit, instead of:
>
> /*
>  * Because regs_refine_cond_op is sound when
>  * the branch is taken, if it produces ill-formed register bounds, it must mean
>  * that the branch is dead.
>  */
> Something like:
> /*
>  * regs_refine_cond_op() is sound, so producing ill-formed register
>  * bounds for the branch means that branch is dead.
>  */
>
This sounds good.

> > +static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
> > +{
> > +     /* Fallthrough (FALSE) branch */
> > +     regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
> > +     reg_bounds_sync(&env->false_reg1);
> > +     reg_bounds_sync(&env->false_reg2);
> This is probably more related to patch 2: is it necessary to have both
> true/false_reg1/2 pairs, it looks like we process false branch before
> the true branch and they never intersect, don't they? So it worth
> removing a pair of bpf_reg_states from env?

We do process the false branch before the true branch in
is_branch_taken->simulate_both_branches. But when both branches are possible
(we return -1), we need all the four env buffers to hold the updated results
of both branch simulations simultaneously.

The new verifier state for other_branch hasn't been created at the time
simulate_both_branches is called, so we cannot copy the results to their
final destinations immediately. We must hold them in the buffers until
after push_stack,
after which we can copy them back into their corresponding register states:

copy_register_state(dst_reg, &env->false_reg1);
copy_register_state(src_reg, &env->false_reg2);
copy_register_state(&other_branch_regs[insn->dst_reg], &env->true_reg1);
if (BPF_SRC(insn->code) == BPF_X)
        copy_register_state(&other_branch_regs[insn->src_reg], &env->true_reg2);

[...]

Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Harishankar Vishwanathan]

On Mon, Mar 23, 2026 at 3:05 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Fri, 2026-03-20 at 17:49 +0100, Paul Chaignon wrote:
>
> [...]
>
> > @@ -16717,11 +16717,48 @@ static void find_good_pkt_pointers(struct bpf_verifier_state *vstate,
> >       }));
> >  }
> >
> > +static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> > +                             u8 opcode, bool is_jmp32);
> > +static u8 rev_opcode(u8 opcode);
> > +
> > +/* Learn more information about live branches by simulating both branches being
> > + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when
> > + * the branch is taken, if it produces ill-formed register bounds, it must mean
> > + * that the branch is dead.
> > + */
> > +static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
> > +{
> > +     /* Fallthrough (FALSE) branch */
> > +     regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
> > +     reg_bounds_sync(&env->false_reg1);
> > +     reg_bounds_sync(&env->false_reg2);
> > +     /* 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))
> > +             return 1;
> > +
> > +     /* Jump (TRUE) branch */
> > +     regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
> > +     reg_bounds_sync(&env->true_reg1);
> > +     reg_bounds_sync(&env->true_reg2);
> > +     /* 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))
> > +             return 0;
>
> Why did you chose to limit these checks to range_bounds_violation(),
> excluding const_{subreg_,}tnum_out_of_sync_with_range_bounds()?

The main reason was because the invariant violations were typically
only detected by
range_bounds_violations().

> Also, it appears that tnum bounds checking functions are unnecessarily
> restricted and should be implemented as follows:
>
>   static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
>   {
>
>         u64 tnum_umin = reg->var_off.value;
>         u64 tnum_umax = reg->var_off.value | reg->var_off.mask;
>         s64 tnum_smin = (s64)tnum_umin;
>         s64 tnum_smax = (s64)tnum_smax;
>
>         // check that [tnum_umin, tnum_umax] and [reg->umin_value, reg->umax_value] intersect
>         // check that [tnum_smin, tnum_smax] and [reg->smin_value, reg->smax_value] intersect
>         return ...;
>   }
>
> Wdyt?

I like the idea! If we do this, we should also rename the function to simply
"tnum_range_mismatch" or something along those lines (as mentioned in
the other thread),
dropping the "const".

Technically, the verifier should maintain the invariant that all domain
pairs always have intersections. There are 10 domain pairs:
u64_s64, u64_tnum, s64_tnum, u32_s32, u32_tnum, s32_tnum,
u64_u32, u64_s32, u32_s64, s64_s32. We can have intersection checks
for each of these pairs, or we can stick to the major ones, i.e. the top 6
in this list.

Checking for intersections was part of the original idea in the RFC
for tnum_step()
I had sent a while back [1], which was about detecting intersection between
tnum and u64.

Generally a simple check will be
if (tmin > umax) || (tmax < umin) // no intersection

The original idea in the RFC was to use tnum_step to make this check
complete. Particularly, for cases like:

        t = x0x1 {1, 3, 9, 11}
        r = [4, 8] {4, 5, 6, 7, 8}

The above check won't suffice. We can add the following check:

if tnum_step(t, umin) > umax) // no intersection

Since tnum_step() has been upstreamed, maybe it is a good time to
revisit the idea, and have a sound and complete intersection check?
Or do you think that is overkill for this patch?

Also, then, should this patch introduce domain checks for all 10 domain pairs?

[1]: https://lore.kernel.org/bpf/20251107192328.2190680-1-harishankar.vishwanathan@gmail.com/

> > +
> > +     /* Both branches are possible, we can't determine which one will be taken. */
> > +     return -1;
> > +}
> > +
> >  /*
> >   * <reg1> <op> <reg2>, currently assuming reg2 is a constant
> >   */
> > -static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
> > -                               u8 opcode, bool is_jmp32)
> > +static int is_scalar_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
> > +                               struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
> >  {
> >       struct tnum t1 = is_jmp32 ? tnum_subreg(reg1->var_off) : reg1->var_off;
> >       struct tnum t2 = is_jmp32 ? tnum_subreg(reg2->var_off) : reg2->var_off;
>
> [...]

Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Eduard Zingerman]

On Tue, 2026-03-24 at 19:59 -0400, Harishankar Vishwanathan wrote:

[...]

> > Also, it appears that tnum bounds checking functions are unnecessarily
> > restricted and should be implemented as follows:
> > 
> >   static bool const_tnum_out_of_sync_with_range_bounds(struct bpf_reg_state *reg)
> >   {
> > 
> >         u64 tnum_umin = reg->var_off.value;
> >         u64 tnum_umax = reg->var_off.value | reg->var_off.mask;
> >         s64 tnum_smin = (s64)tnum_umin;
> >         s64 tnum_smax = (s64)tnum_smax;
> > 
> >         // check that [tnum_umin, tnum_umax] and [reg->umin_value, reg->umax_value] intersect
> >         // check that [tnum_smin, tnum_smax] and [reg->smin_value, reg->smax_value] intersect
> >         return ...;
> >   }
> > 
> > Wdyt?
> 
> I like the idea! If we do this, we should also rename the function to simply
> "tnum_range_mismatch" or something along those lines (as mentioned in
> the other thread),
> dropping the "const".
> 
> Technically, the verifier should maintain the invariant that all domain
> pairs always have intersections. There are 10 domain pairs:
> u64_s64, u64_tnum, s64_tnum, u32_s32, u32_tnum, s32_tnum,
> u64_u32, u64_s32, u32_s64, s64_s32. We can have intersection checks
> for each of these pairs, or we can stick to the major ones, i.e. the top 6
> in this list.
> 
> Checking for intersections was part of the original idea in the RFC
> for tnum_step()
> I had sent a while back [1], which was about detecting intersection between
> tnum and u64.
> 
> Generally a simple check will be
> if (tmin > umax) || (tmax < umin) // no intersection
> 
> The original idea in the RFC was to use tnum_step to make this check
> complete. Particularly, for cases like:
> 
>         t = x0x1 {1, 3, 9, 11}
>         r = [4, 8] {4, 5, 6, 7, 8}
> 
> The above check won't suffice. We can add the following check:
> 
> if tnum_step(t, umin) > umax) // no intersection

Yes, this makes sense.

> Since tnum_step() has been upstreamed, maybe it is a good time to
> revisit the idea, and have a sound and complete intersection check?
> Or do you think that is overkill for this patch?
> 
> Also, then, should this patch introduce domain checks for all 10 domain pairs?

I'd say we should check each and every but 10 sounds a bit scary.
Maybe do it in a straightforward way and see if it shows in perf
profile? Trying on a few large programs?

[...]

Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Mykyta Yatsenko]

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

> On Mon, Mar 23, 2026 at 12:19 PM Mykyta Yatsenko
> <mykyta.yatsenko5@gmail.com> wrote:
>>
>> Paul Chaignon <paul.chaignon@gmail.com> writes:
>>
>> > From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
>> >
> [...]
>> > +static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
>> > +                             u8 opcode, bool is_jmp32);
>> > +static u8 rev_opcode(u8 opcode);
>> > +
>> > +/* Learn more information about live branches by simulating both branches being
>> > + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when
>> > + * the branch is taken, if it produces ill-formed register bounds, it must mean
>> > + * that the branch is dead.
>> > + */
>> Sorry for being nit-picky, could you please use kernel style comment style +
>
> Thanks for the suggestion. To clarify, by kernel-style did you mean
> keeping the beginning line empty?
> Or something else that I might have missed.
Yes, first line just /*, then text goes next line.
>
>> maybe reword it a little bit, instead of:
>>
>> /*
>>  * Because regs_refine_cond_op is sound when
>>  * the branch is taken, if it produces ill-formed register bounds, it must mean
>>  * that the branch is dead.
>>  */
>> Something like:
>> /*
>>  * regs_refine_cond_op() is sound, so producing ill-formed register
>>  * bounds for the branch means that branch is dead.
>>  */
>>
> This sounds good.
>
>> > +static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
>> > +{
>> > +     /* Fallthrough (FALSE) branch */
>> > +     regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
>> > +     reg_bounds_sync(&env->false_reg1);
>> > +     reg_bounds_sync(&env->false_reg2);
>> This is probably more related to patch 2: is it necessary to have both
>> true/false_reg1/2 pairs, it looks like we process false branch before
>> the true branch and they never intersect, don't they? So it worth
>> removing a pair of bpf_reg_states from env?
>
> We do process the false branch before the true branch in
> is_branch_taken->simulate_both_branches. But when both branches are possible
> (we return -1), we need all the four env buffers to hold the updated results
> of both branch simulations simultaneously.
>
> The new verifier state for other_branch hasn't been created at the time
> simulate_both_branches is called, so we cannot copy the results to their
> final destinations immediately. We must hold them in the buffers until
> after push_stack,
> after which we can copy them back into their corresponding register states:
>
> copy_register_state(dst_reg, &env->false_reg1);
> copy_register_state(src_reg, &env->false_reg2);
> copy_register_state(&other_branch_regs[insn->dst_reg], &env->true_reg1);
> if (BPF_SRC(insn->code) == BPF_X)
>         copy_register_state(&other_branch_regs[insn->src_reg], &env->true_reg2);
>
> [...]

Re: [PATCH v2 bpf-next 5/6] selftests/bpf: Cover invariant violation cases from syzbot

[Paul Chaignon]

On Mon, Mar 23, 2026 at 05:46:41PM +0000, Mykyta Yatsenko wrote:
> Paul Chaignon <paul.chaignon@gmail.com> writes:

[...]

> > +/* Last jump can be detected as always taken because the intersection of R5 and
> > + * R7 32bit tnums produces a constant that isn't within R7's s32 bounds.
> > + */
> > +SEC("socket")
> > +__description("dead branch: tnums give impossible constant if equal")
> > +__success
> > +__flag(BPF_F_TEST_REG_INVARIANTS)
> > +__naked void tnums_equal_impossible_constant(void *ctx)
> > +{
> > +	asm volatile("										\
> > +	call %[bpf_get_prandom_u32];								\
> > +	r5 = r0;										\
> > +	r5 &= 0xfffffffffffffffc;	/* var_off32=(0; 0xfffffffc) */				\
> > +	r7 = r0;										\
> > +	r7 &= 0x1;			/* var_off32=(0x0; 0x1) */				\
> > +	r7 += -43;			/* s32=[-43; -42] & var_off32=(0xffffffd4; 0x3) */	\
> > +	if w5 != w7 goto +1;		/* on fallthrough var_off32=-44, not in s32 */		\
> w5 has bits 0,1 zero, rest unknown
> w7 has top bits known as 0xffffffd4, and bits 0,1 unknown
> If w5 == w7, their tnums must intersect to a single
> value = 0xffffffd4(-44). Which is outside of w7's range [-43; 42]. So
> the r10 = 0 branch should be unreachable.
> I guess the comment should be updated to the kernel style as well.

Thanks for the review! We already have a lot of end-of-line comments on
the BPF assembly in selftests (including two tests above) so I assumed
that was fine.

(Unrelated: On some mail clients, your comments are hard to spot. It
might help if you could include a blank line before and after them :) )

> Acked-by: Mykyta Yatsenko <yatsenko@meta.com>
> > +	r10 = 0;										\
> > +	exit;											\
> > +"	:
> > +	: __imm(bpf_get_prandom_u32)
> > +	: __clobber_all);
> > +}
> > +
> >  char _license[] SEC("license") = "GPL";
> > -- 
> > 2.43.0

Re: [PATCH v2 bpf-next 5/6] selftests/bpf: Cover invariant violation cases from syzbot

[Alexei Starovoitov]

On Sat, Mar 28, 2026 at 9:20 AM Paul Chaignon <paul.chaignon@gmail.com> wrote:
>
> On Mon, Mar 23, 2026 at 05:46:41PM +0000, Mykyta Yatsenko wrote:
> > Paul Chaignon <paul.chaignon@gmail.com> writes:
>
> [...]
>
> > > +/* Last jump can be detected as always taken because the intersection of R5 and
> > > + * R7 32bit tnums produces a constant that isn't within R7's s32 bounds.
> > > + */
> > > +SEC("socket")
> > > +__description("dead branch: tnums give impossible constant if equal")
> > > +__success
> > > +__flag(BPF_F_TEST_REG_INVARIANTS)
> > > +__naked void tnums_equal_impossible_constant(void *ctx)
> > > +{
> > > +   asm volatile("                                                                          \
> > > +   call %[bpf_get_prandom_u32];                                                            \
> > > +   r5 = r0;                                                                                \
> > > +   r5 &= 0xfffffffffffffffc;       /* var_off32=(0; 0xfffffffc) */                         \
> > > +   r7 = r0;                                                                                \
> > > +   r7 &= 0x1;                      /* var_off32=(0x0; 0x1) */                              \
> > > +   r7 += -43;                      /* s32=[-43; -42] & var_off32=(0xffffffd4; 0x3) */      \
> > > +   if w5 != w7 goto +1;            /* on fallthrough var_off32=-44, not in s32 */          \
> > w5 has bits 0,1 zero, rest unknown
> > w7 has top bits known as 0xffffffd4, and bits 0,1 unknown
> > If w5 == w7, their tnums must intersect to a single
> > value = 0xffffffd4(-44). Which is outside of w7's range [-43; 42]. So
> > the r10 = 0 branch should be unreachable.
> > I guess the comment should be updated to the kernel style as well.
>
> Thanks for the review! We already have a lot of end-of-line comments on
> the BPF assembly in selftests (including two tests above) so I assumed
> that was fine.

btw we have two comment styles in bpf progs.
I personally prefer this one:
        /*
         * Checkpoint at function entry should not fire, as caller
         * stack fp[0]-8 is alive at this point.
         */
        "r6 = r2;"
        "r1 = *(u64 *)(r6 + 0);"
        "*(u64*)(r10 - 8) = 7;"
        "r2 = r10;"

because of color highlighting.
But some prefer the other one:

        asm volatile ("                                 \
        /* spill R1(ctx) into stack */                  \
        *(u64*)(r10 - 8) = r1;                          \
        /* fill it back into R2 */                      \
        r2 = *(u64*)(r10 - 8);                          \

The comments have the same color as asm, but
no " " marks.


> (Unrelated: On some mail clients, your comments are hard to spot. It
> might help if you could include a blank line before and after them :) )

+1