[PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Paul Chaignon]

In the following toy program (reg states minimized for readability), R0
and R1 always have different values at instruction 6. This is obvious
when reading the program but cannot be guessed from ranges alone as
they overlap (R0 in [0; 0xc0000000], R1 in [1024; 0xc0000400]).

  0: call bpf_get_prandom_u32#7  ; R0_w=scalar()
  1: w0 = w0                     ; R0_w=scalar(var_off=(0x0; 0xffffffff))
  2: r0 >>= 30                   ; R0_w=scalar(var_off=(0x0; 0x3))
  3: r0 <<= 30                   ; R0_w=scalar(var_off=(0x0; 0xc0000000))
  4: r1 = r0                     ; R1_w=scalar(var_off=(0x0; 0xc0000000))
  5: r1 += 1024                  ; R1_w=scalar(var_off=(0x400; 0xc0000000))
  6: if r1 != r0 goto pc+1

Looking at tnums however, we can deduce that R1 is always different from
R0 because their tnums don't agree on known bits. This patch uses this
logic to improve is_scalar_branch_taken in case of BPF_JEQ and BPF_JNE.

This change has a tiny impact on complexity, which was measured with
the Cilium complexity CI test. That test covers 72 programs with
various build and load time configurations for a total of 970 test
cases. For 80% of test cases, the patch has no impact. On the other
test cases, the patch decreases complexity by only 0.08% on average. In
the best case, the verifier needs to walk 3% less instructions and, in
the worst case, 1.5% more. Overall, the patch has a small positive
impact, especially for our largest programs.

Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 include/linux/tnum.h  | 3 +++
 kernel/bpf/tnum.c     | 8 ++++++++
 kernel/bpf/verifier.c | 4 ++++
 3 files changed, 15 insertions(+)

diff --git a/include/linux/tnum.h b/include/linux/tnum.h
index 57ed3035cc30..06a41d070e75 100644
--- a/include/linux/tnum.h
+++ b/include/linux/tnum.h
@@ -51,6 +51,9 @@ struct tnum tnum_xor(struct tnum a, struct tnum b);
 /* Multiply two tnums, return @a * @b */
 struct tnum tnum_mul(struct tnum a, struct tnum b);
 
+/* Return true if the known bits of both tnums have the same value */
+bool tnum_agree(struct tnum a, struct tnum b);
+
 /* Return a tnum representing numbers satisfying both @a and @b */
 struct tnum tnum_intersect(struct tnum a, struct tnum b);
 
diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
index fa353c5d550f..8cb73d35196e 100644
--- a/kernel/bpf/tnum.c
+++ b/kernel/bpf/tnum.c
@@ -143,6 +143,14 @@ struct tnum tnum_mul(struct tnum a, struct tnum b)
 	return tnum_add(TNUM(acc_v, 0), acc_m);
 }
 
+bool tnum_agree(struct tnum a, struct tnum b)
+{
+	u64 mu;
+
+	mu = ~a.mask & ~b.mask;
+	return (a.value & mu) == (b.value & mu);
+}
+
 /* Note that if a and b disagree - i.e. one has a 'known 1' where the other has
  * a 'known 0' - this will return a 'known 1' for that bit.
  */
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 3a3982fe20d4..fa86833254e3 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -15891,6 +15891,8 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
 			return 0;
 		if (smin1 > smax2 || smax1 < smin2)
 			return 0;
+		if (!tnum_agree(t1, t2))
+			return 0;
 		if (!is_jmp32) {
 			/* if 64-bit ranges are inconclusive, see if we can
 			 * utilize 32-bit subrange knowledge to eliminate
@@ -15915,6 +15917,8 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
 			return 1;
 		if (smin1 > smax2 || smax1 < smin2)
 			return 1;
+		if (!tnum_agree(t1, t2))
+			return 1;
 		if (!is_jmp32) {
 			/* if 64-bit ranges are inconclusive, see if we can
 			 * utilize 32-bit subrange knowledge to eliminate
-- 
2.43.0

[PATCH bpf-next 2/2] selftests/bpf: Tests for is_scalar_branch_taken tnum logic

[Paul Chaignon]

This patch adds tests for the new jeq and jne logic in
is_scalar_branch_taken. The following shows the first test failing
before the previous patch is applied. Once the previous patch is
applied, the verifier can use the tnum values to deduce that instruction
7 is dead code.

  0: call bpf_get_prandom_u32#7  ; R0_w=scalar()
  1: w0 = w0                     ; R0_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
  2: r0 >>= 30                   ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=3,var_off=(0x0; 0x3))
  3: r0 <<= 30                   ; R0_w=scalar(smin=0,smax=umax=umax32=0xc0000000,smax32=0x40000000,var_off=(0x0; 0xc0000000))
  4: r1 = r0                     ; R0_w=scalar(id=1,smin=0,smax=umax=umax32=0xc0000000,smax32=0x40000000,var_off=(0x0; 0xc0000000)) R1_w=scalar(id=1,smin=0,smax=umax=umax32=0xc0000000,smax32=0x40000000,var_off=(0x0; 0xc0000000))
  5: r1 += 1024                  ; R1_w=scalar(smin=umin=umin32=1024,smax=umax=umax32=0xc0000400,smin32=0x80000400,smax32=0x40000400,var_off=(0x400; 0xc0000000))
  6: if r1 != r0 goto pc+1       ; R0_w=scalar(id=1,smin=umin=umin32=1024,smax=umax=umax32=0xc0000000,smin32=0x80000400,smax32=0x40000000,var_off=(0x400; 0xc0000000)) R1_w=scalar(smin=umin=umin32=1024,smax=umax=umax32=0xc0000000,smin32=0x80000400,smax32=0x40000400,var_off=(0x400; 0xc0000000))
  7: r10 = 0
  frame pointer is read only

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

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index 87a2c60d86e6..fbccc20555f4 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -1668,4 +1668,45 @@ l0_%=:	r0 = 0;				\
 	: __clobber_all);
 }
 
+SEC("socket")
+__description("dead jne branch due to disagreeing tnums")
+__success __log_level(2)
+__naked void jne_disagreeing_tnums(void *ctx)
+{
+	asm volatile("			\
+	call %[bpf_get_prandom_u32];	\
+	w0 = w0;			\
+	r0 >>= 30;			\
+	r0 <<= 30;			\
+	r1 = r0;			\
+	r1 += 1024;			\
+	if r1 != r0 goto +1;		\
+	r10 = 0;			\
+	exit;				\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("dead jeq branch due to disagreeing tnums")
+__success __log_level(2)
+__naked void jeq_disagreeing_tnums(void *ctx)
+{
+	asm volatile("			\
+	call %[bpf_get_prandom_u32];	\
+	w0 = w0;			\
+	r0 >>= 30;			\
+	r0 <<= 30;			\
+	r1 = r0;			\
+	r1 += 1024;			\
+	if r1 == r0 goto +1;		\
+	exit;				\
+	r10 = 0;			\
+	exit;				\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.43.0

Re: [PATCH bpf-next 2/2] selftests/bpf: Tests for is_scalar_branch_taken tnum logic

[Eduard Zingerman]

On Wed, 2025-08-13 at 17:35 +0200, Paul Chaignon wrote:
> This patch adds tests for the new jeq and jne logic in
> is_scalar_branch_taken. The following shows the first test failing
> before the previous patch is applied. Once the previous patch is
> applied, the verifier can use the tnum values to deduce that instruction
> 7 is dead code.
> 
>   0: call bpf_get_prandom_u32#7  ; R0_w=scalar()
>   1: w0 = w0                     ; R0_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
>   2: r0 >>= 30                   ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=3,var_off=(0x0; 0x3))
>   3: r0 <<= 30                   ; R0_w=scalar(smin=0,smax=umax=umax32=0xc0000000,smax32=0x40000000,var_off=(0x0; 0xc0000000))
>   4: r1 = r0                     ; R0_w=scalar(id=1,smin=0,smax=umax=umax32=0xc0000000,smax32=0x40000000,var_off=(0x0; 0xc0000000)) R1_w=scalar(id=1,smin=0,smax=umax=umax32=0xc0000000,smax32=0x40000000,var_off=(0x0; 0xc0000000))
>   5: r1 += 1024                  ; R1_w=scalar(smin=umin=umin32=1024,smax=umax=umax32=0xc0000400,smin32=0x80000400,smax32=0x40000400,var_off=(0x400; 0xc0000000))
>   6: if r1 != r0 goto pc+1       ; R0_w=scalar(id=1,smin=umin=umin32=1024,smax=umax=umax32=0xc0000000,smin32=0x80000400,smax32=0x40000000,var_off=(0x400; 0xc0000000)) R1_w=scalar(smin=umin=umin32=1024,smax=umax=umax32=0xc0000000,smin32=0x80000400,smax32=0x40000400,var_off=(0x400; 0xc0000000))
>   7: r10 = 0
>   frame pointer is read only
> 
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

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

[...]

Re: [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Eduard Zingerman]

On Wed, 2025-08-13 at 17:34 +0200, Paul Chaignon wrote:
> In the following toy program (reg states minimized for readability), R0
> and R1 always have different values at instruction 6. This is obvious
> when reading the program but cannot be guessed from ranges alone as
> they overlap (R0 in [0; 0xc0000000], R1 in [1024; 0xc0000400]).
> 
>   0: call bpf_get_prandom_u32#7  ; R0_w=scalar()
>   1: w0 = w0                     ; R0_w=scalar(var_off=(0x0; 0xffffffff))
>   2: r0 >>= 30                   ; R0_w=scalar(var_off=(0x0; 0x3))
>   3: r0 <<= 30                   ; R0_w=scalar(var_off=(0x0; 0xc0000000))
>   4: r1 = r0                     ; R1_w=scalar(var_off=(0x0; 0xc0000000))
>   5: r1 += 1024                  ; R1_w=scalar(var_off=(0x400; 0xc0000000))
>   6: if r1 != r0 goto pc+1
> 
> Looking at tnums however, we can deduce that R1 is always different from
> R0 because their tnums don't agree on known bits. This patch uses this
> logic to improve is_scalar_branch_taken in case of BPF_JEQ and BPF_JNE.
> 
> This change has a tiny impact on complexity, which was measured with
> the Cilium complexity CI test. That test covers 72 programs with
> various build and load time configurations for a total of 970 test
> cases. For 80% of test cases, the patch has no impact. On the other
> test cases, the patch decreases complexity by only 0.08% on average. In
> the best case, the verifier needs to walk 3% less instructions and, in
> the worst case, 1.5% more. Overall, the patch has a small positive
> impact, especially for our largest programs.
> 
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---

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

Note: CI reports verifier performance differences for Meta internal programs:
      https://github.com/kernel-patches/bpf/actions/runs/16942287206
      But I can't confirm the difference after running veristat for these programs,
      looks like a CI glitch.

[...]

Re: [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Shung-Hsi Yu]

On Wed, Aug 13, 2025 at 05:34:08PM +0200, Paul Chaignon wrote:
> In the following toy program (reg states minimized for readability), R0
> and R1 always have different values at instruction 6. This is obvious
> when reading the program but cannot be guessed from ranges alone as
> they overlap (R0 in [0; 0xc0000000], R1 in [1024; 0xc0000400]).
> 
>   0: call bpf_get_prandom_u32#7  ; R0_w=scalar()
>   1: w0 = w0                     ; R0_w=scalar(var_off=(0x0; 0xffffffff))
>   2: r0 >>= 30                   ; R0_w=scalar(var_off=(0x0; 0x3))
>   3: r0 <<= 30                   ; R0_w=scalar(var_off=(0x0; 0xc0000000))
>   4: r1 = r0                     ; R1_w=scalar(var_off=(0x0; 0xc0000000))
>   5: r1 += 1024                  ; R1_w=scalar(var_off=(0x400; 0xc0000000))
>   6: if r1 != r0 goto pc+1
> 
> Looking at tnums however, we can deduce that R1 is always different from
> R0 because their tnums don't agree on known bits. This patch uses this
> logic to improve is_scalar_branch_taken in case of BPF_JEQ and BPF_JNE.
> 
> This change has a tiny impact on complexity, which was measured with
> the Cilium complexity CI test. That test covers 72 programs with
> various build and load time configurations for a total of 970 test
> cases. For 80% of test cases, the patch has no impact. On the other
> test cases, the patch decreases complexity by only 0.08% on average. In
> the best case, the verifier needs to walk 3% less instructions and, in
> the worst case, 1.5% more. Overall, the patch has a small positive
> impact, especially for our largest programs.
> 
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> ---
>  include/linux/tnum.h  | 3 +++
>  kernel/bpf/tnum.c     | 8 ++++++++
>  kernel/bpf/verifier.c | 4 ++++
>  3 files changed, 15 insertions(+)
> 
> diff --git a/include/linux/tnum.h b/include/linux/tnum.h
> index 57ed3035cc30..06a41d070e75 100644
> --- a/include/linux/tnum.h
> +++ b/include/linux/tnum.h
> @@ -51,6 +51,9 @@ struct tnum tnum_xor(struct tnum a, struct tnum b);
>  /* Multiply two tnums, return @a * @b */
>  struct tnum tnum_mul(struct tnum a, struct tnum b);
>  
> +/* Return true if the known bits of both tnums have the same value */
> +bool tnum_agree(struct tnum a, struct tnum b);
> +
>  /* Return a tnum representing numbers satisfying both @a and @b */
>  struct tnum tnum_intersect(struct tnum a, struct tnum b);
>  
> diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
> index fa353c5d550f..8cb73d35196e 100644
> --- a/kernel/bpf/tnum.c
> +++ b/kernel/bpf/tnum.c
> @@ -143,6 +143,14 @@ struct tnum tnum_mul(struct tnum a, struct tnum b)
>  	return tnum_add(TNUM(acc_v, 0), acc_m);
>  }
>  
> +bool tnum_agree(struct tnum a, struct tnum b)
> +{
> +	u64 mu;
> +
> +	mu = ~a.mask & ~b.mask;
> +	return (a.value & mu) == (b.value & mu);
> +}

Nit: I finding the naming a bit unconventional compared to other tnum
helpers we have, with are either usually named after a BPF instruction
or set operation. tnum_overlap() would be my choice for the name of such
new helper.

One more comment below.

>  /* Note that if a and b disagree - i.e. one has a 'known 1' where the other has
>   * a 'known 0' - this will return a 'known 1' for that bit.
>   */
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 3a3982fe20d4..fa86833254e3 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -15891,6 +15891,8 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
>  			return 0;
>  		if (smin1 > smax2 || smax1 < smin2)
>  			return 0;
> +		if (!tnum_agree(t1, t2))
> +			return 0;

Could we reuse tnum_xor() here instead?

If xor of two register cannot be 0, then the two can never hold the same
value. Also we can use the tnum_xor() result in place of tnum_is_const()
checks.

case BPF_JEQ:
    t = tnum_xor(t1, t2);
    if (!t.mask) /* Equvalent of tnum_is_const(t1) && tnum_is_const(t2) */
        return t.value == 0;
    if (umin1 > umax2 || umax1 < umin2)
        return 0;
    if (smin1 > smax2 || smax1 < smin2)
        return 0;
    if (!t.value) /* Equvalent of !tnum_agree(t1, t2) */
      return 0;
    ...
case BPF_JNE:
    t = tnum_xor(t1, t2);
    if (!t.mask) /* Equvalent of tnum_is_const(t1) && tnum_is_const(t2) */
        return t.value != 0;
    /* non-overlapping ranges */
    if (umin1 > umax2 || umax1 < umin2)
        return 1;
    if (smin1 > smax2 || smax1 < smin2)
        return 1;
    if (!t.value) /* Equvalent of !tnum_agree(t1, t2) */
        return 1;

Looks slighly less readable though.

Re: [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Paul Chaignon]

On Thu, Aug 14, 2025 at 08:55:22PM +0800, Shung-Hsi Yu wrote:
> On Wed, Aug 13, 2025 at 05:34:08PM +0200, Paul Chaignon wrote:

Thanks for the review Shung-Hsi!

[...]

> > +bool tnum_agree(struct tnum a, struct tnum b)
> > +{
> > +	u64 mu;
> > +
> > +	mu = ~a.mask & ~b.mask;
> > +	return (a.value & mu) == (b.value & mu);
> > +}
> 
> Nit: I finding the naming a bit unconventional compared to other tnum
> helpers we have, with are either usually named after a BPF instruction
> or set operation. tnum_overlap() would be my choice for the name of such
> new helper.

Agree suggested name is better. Thanks!

> 
> One more comment below.
> 
> >  /* Note that if a and b disagree - i.e. one has a 'known 1' where the other has
> >   * a 'known 0' - this will return a 'known 1' for that bit.
> >   */
> > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > index 3a3982fe20d4..fa86833254e3 100644
> > --- a/kernel/bpf/verifier.c
> > +++ b/kernel/bpf/verifier.c
> > @@ -15891,6 +15891,8 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
> >  			return 0;
> >  		if (smin1 > smax2 || smax1 < smin2)
> >  			return 0;
> > +		if (!tnum_agree(t1, t2))
> > +			return 0;
> 
> Could we reuse tnum_xor() here instead?
> 
> If xor of two register cannot be 0, then the two can never hold the same
> value. Also we can use the tnum_xor() result in place of tnum_is_const()
> checks.
> 
> case BPF_JEQ:
>     t = tnum_xor(t1, t2);
>     if (!t.mask) /* Equvalent of tnum_is_const(t1) && tnum_is_const(t2) */
>         return t.value == 0;
>     if (umin1 > umax2 || umax1 < umin2)
>         return 0;
>     if (smin1 > smax2 || smax1 < smin2)
>         return 0;
>     if (!t.value) /* Equvalent of !tnum_agree(t1, t2) */
>       return 0;
>     ...
> case BPF_JNE:
>     t = tnum_xor(t1, t2);
>     if (!t.mask) /* Equvalent of tnum_is_const(t1) && tnum_is_const(t2) */
>         return t.value != 0;
>     /* non-overlapping ranges */
>     if (umin1 > umax2 || umax1 < umin2)
>         return 1;
>     if (smin1 > smax2 || smax1 < smin2)
>         return 1;
>     if (!t.value) /* Equvalent of !tnum_agree(t1, t2) */
>         return 1;
> 
> Looks slighly less readable though.

Nice find on the xor-based equivalent version! I lean a bit toward
keeping the slightly more readable version though. The xor version is
probably a bit more efficient, but I'm unsure that matters much for this
piece of code, whereas I think readability matters a lot here. That
said, if others prefer the xor version, I don't mind much :)

Re: [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Shung-Hsi Yu]

On Mon, Aug 18, 2025 at 07:44:05PM +0200, Paul Chaignon wrote:
> On Thu, Aug 14, 2025 at 08:55:22PM +0800, Shung-Hsi Yu wrote:
> > On Wed, Aug 13, 2025 at 05:34:08PM +0200, Paul Chaignon wrote:
[...]
> > > @@ -15891,6 +15891,8 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
> > >  			return 0;
> > >  		if (smin1 > smax2 || smax1 < smin2)
> > >  			return 0;
> > > +		if (!tnum_agree(t1, t2))
> > > +			return 0;
> > 
> > Could we reuse tnum_xor() here instead?
> > 
> > If xor of two register cannot be 0, then the two can never hold the same
> > value. Also we can use the tnum_xor() result in place of tnum_is_const()
> > checks.
> > 
> > case BPF_JEQ:
> >     t = tnum_xor(t1, t2);
> >     if (!t.mask) /* Equvalent of tnum_is_const(t1) && tnum_is_const(t2) */
> >         return t.value == 0;
> >     if (umin1 > umax2 || umax1 < umin2)
> >         return 0;
> >     if (smin1 > smax2 || smax1 < smin2)
> >         return 0;
> >     if (!t.value) /* Equvalent of !tnum_agree(t1, t2) */
> >       return 0;
> >     ...
[...]
> > Looks slighly less readable though.
> 
> Nice find on the xor-based equivalent version! I lean a bit toward
> keeping the slightly more readable version though. The xor version is
> probably a bit more efficient, but I'm unsure that matters much for this
> piece of code, whereas I think readability matters a lot here.

True, I probably had jump a bit too quickly to optimization. Thinking
about this over again adding a new helper does make more sense (someone
probably will try to add it in the future anyway), so let's take the
readability preference. You can add

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

Maybe add the check right after 'tnum_is_const(t1) && tnum_is_const(t2)'
check, and before 'umin/umax/smin/smax' check though? Bunching tnum
usage together for aesthetic.

> ... That
> said, if others prefer the xor version, I don't mind much :)

FWIW I'd ideally would like tnum_intersect to return 'false' if no
intersection can be found (similar to check_add_overflow), then we can
use it here. And forcing check to always be done should help avoid
running into some of the register bound violations. But such change felt
too intrusive for the purpose of this patchset, maybe for a future
refactor.

  __must_check bool tnum_intersect(struct tnum a, struct tnum b, struct tnum *out)

Re: [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Paul Chaignon]

On Wed, Aug 20, 2025 at 01:09:22PM +0800, Shung-Hsi Yu wrote:
> On Mon, Aug 18, 2025 at 07:44:05PM +0200, Paul Chaignon wrote:
> > On Thu, Aug 14, 2025 at 08:55:22PM +0800, Shung-Hsi Yu wrote:
> > > On Wed, Aug 13, 2025 at 05:34:08PM +0200, Paul Chaignon wrote:
> [...]

[...]

> Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> 
> Maybe add the check right after 'tnum_is_const(t1) && tnum_is_const(t2)'
> check, and before 'umin/umax/smin/smax' check though? Bunching tnum
> usage together for aesthetic.

Done in the v2. Thanks again for the review!

> 
> > ... That
> > said, if others prefer the xor version, I don't mind much :)
> 
> FWIW I'd ideally would like tnum_intersect to return 'false' if no
> intersection can be found (similar to check_add_overflow), then we can
> use it here. And forcing check to always be done should help avoid
> running into some of the register bound violations. But such change felt
> too intrusive for the purpose of this patchset, maybe for a future
> refactor.
> 
>   __must_check bool tnum_intersect(struct tnum a, struct tnum b, struct tnum *out)

I like the idea :) When checking the returned value in reg_bounds_sync
and regs_refine_cond_op, we would probably want to throw a verifier bug,
but that doesn't look too invasive.

[syzbot ci] Re: bpf: Use tnums for JEQ/JNE is_branch_taken logic

[syzbot ci]

syzbot ci has tested the following series

[v1] bpf: Use tnums for JEQ/JNE is_branch_taken logic
https://lore.kernel.org/all/ba9baf9f73d51d9bce9ef13778bd39408d67db79.1755098817.git.paul.chaignon@gmail.com
* [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic
* [PATCH bpf-next 2/2] selftests/bpf: Tests for is_scalar_branch_taken tnum logic

and found the following issue:
WARNING in reg_bounds_sanity_check

Full report is available here:
https://ci.syzbot.org/series/fd950b40-1da8-44b1-bd12-4366e4a354b1

***

WARNING in reg_bounds_sanity_check

tree:      bpf-next
URL:       https://kernel.googlesource.com/pub/scm/linux/kernel/git/bpf/bpf-next.git
base:      07866544e410e4c895a729971e4164861b41fad5
arch:      amd64
compiler:  Debian clang version 20.1.7 (++20250616065708+6146a88f6049-1~exp1~20250616065826.132), Debian LLD 20.1.7
config:    https://ci.syzbot.org/builds/c4af872a-9b42-4821-a832-941921acc063/config
C repro:   https://ci.syzbot.org/findings/8dfae15e-cda5-4fa6-8f95-aab106ebd860/c_repro
syz repro: https://ci.syzbot.org/findings/8dfae15e-cda5-4fa6-8f95-aab106ebd860/syz_repro

verifier bug: REG INVARIANTS VIOLATION (true_reg1): range bounds violation u64=[0xffffdfcd, 0xffffffffffffdfcc] s64=[0x80000000ffffdfcd, 0x7fffffffffffdfcc] u32=[0xffffdfcd, 0xffffdfcc] s32=[0xffffdfcd, 0xffffdfcc] var_off=(0xffffdfcc, 0xffffffff00000000)
WARNING: CPU: 0 PID: 6007 at kernel/bpf/verifier.c:2728 reg_bounds_sanity_check+0x6e6/0xc20 kernel/bpf/verifier.c:2722
Modules linked in:
CPU: 0 UID: 0 PID: 6007 Comm: syz.0.17 Not tainted 6.17.0-rc1-syzkaller-00022-g07866544e410-dirty #0 PREEMPT(full) 
Hardware name: QEMU Standard PC (Q35 + ICH9, 2009), BIOS 1.16.2-debian-1.16.2-1 04/01/2014
RIP: 0010:reg_bounds_sanity_check+0x6e6/0xc20 kernel/bpf/verifier.c:2722
Code: 24 20 4c 8b 44 24 60 4c 8b 4c 24 58 41 ff 75 00 53 41 57 55 ff 74 24 38 ff 74 24 70 ff 74 24 40 e8 1f 30 aa ff 48 83 c4 38 90 <0f> 0b 90 90 48 bb 00 00 00 00 00 fc ff df 4d 89 f7 4c 8b 74 24 08
RSP: 0018:ffffc9000294ef08 EFLAGS: 00010282
RAX: 98d8a1179b385100 RBX: 00000000ffffdfcc RCX: ffff888020fb5640
RDX: 0000000000000000 RSI: 0000000000000001 RDI: 0000000000000002
RBP: 00000000ffffdfcd R08: 0000000000000003 R09: 0000000000000004
R10: dffffc0000000000 R11: fffffbfff1bfa1ec R12: ffff88803dbe4258
R13: ffff88803dbe4278 R14: ffff88803dbe4290 R15: 00000000ffffdfcc
FS:  000055557043b500(0000) GS:ffff8880b861c000(0000) knlGS:0000000000000000
CS:  0010 DS: 0000 ES: 0000 CR0: 0000000080050033
CR2: 00007f985e5b7dac CR3: 000000010f3be000 CR4: 00000000000006f0
Call Trace:
 <TASK>
 reg_set_min_max+0x214/0x300 kernel/bpf/verifier.c:16338
 check_cond_jmp_op+0x1625/0x2910 kernel/bpf/verifier.c:16772
 do_check_insn kernel/bpf/verifier.c:19960 [inline]
 do_check+0x6751/0xe520 kernel/bpf/verifier.c:20097
 do_check_common+0x1949/0x24f0 kernel/bpf/verifier.c:23265
 do_check_main kernel/bpf/verifier.c:23348 [inline]
 bpf_check+0x1746a/0x1d2e0 kernel/bpf/verifier.c:24708
 bpf_prog_load+0x1318/0x1930 kernel/bpf/syscall.c:2979
 __sys_bpf+0x528/0x870 kernel/bpf/syscall.c:6029
 __do_sys_bpf kernel/bpf/syscall.c:6139 [inline]
 __se_sys_bpf kernel/bpf/syscall.c:6137 [inline]
 __x64_sys_bpf+0x7c/0x90 kernel/bpf/syscall.c:6137
 do_syscall_x64 arch/x86/entry/syscall_64.c:63 [inline]
 do_syscall_64+0xfa/0x3b0 arch/x86/entry/syscall_64.c:94
 entry_SYSCALL_64_after_hwframe+0x77/0x7f
RIP: 0033:0x7f985e38ebe9
Code: ff ff c3 66 2e 0f 1f 84 00 00 00 00 00 0f 1f 40 00 48 89 f8 48 89 f7 48 89 d6 48 89 ca 4d 89 c2 4d 89 c8 4c 8b 4c 24 08 0f 05 <48> 3d 01 f0 ff ff 73 01 c3 48 c7 c1 a8 ff ff ff f7 d8 64 89 01 48
RSP: 002b:00007ffd45036968 EFLAGS: 00000246 ORIG_RAX: 0000000000000141
RAX: ffffffffffffffda RBX: 00007f985e5b5fa0 RCX: 00007f985e38ebe9
RDX: 0000000000000048 RSI: 00002000000054c0 RDI: 0000000000000005
RBP: 00007f985e411e19 R08: 0000000000000000 R09: 0000000000000000
R10: 0000000000000000 R11: 0000000000000246 R12: 0000000000000000
R13: 00007f985e5b5fa0 R14: 00007f985e5b5fa0 R15: 0000000000000003
 </TASK>


***

If these findings have caused you to resend the series or submit a
separate fix, please add the following tag to your commit message:
Tested-by: syzbot@syzkaller.appspotmail.com

---
This report is generated by a bot. It may contain errors.
syzbot ci engineers can be reached at syzkaller@googlegroups.com.

Re: [syzbot ci] Re: bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Paul Chaignon]

On Fri, Aug 15, 2025 at 01:24:40AM -0700, syzbot ci wrote:
> syzbot ci has tested the following series
> 
> [v1] bpf: Use tnums for JEQ/JNE is_branch_taken logic
> https://lore.kernel.org/all/ba9baf9f73d51d9bce9ef13778bd39408d67db79.1755098817.git.paul.chaignon@gmail.com
> * [PATCH bpf-next 1/2] bpf: Use tnums for JEQ/JNE is_branch_taken logic
> * [PATCH bpf-next 2/2] selftests/bpf: Tests for is_scalar_branch_taken tnum logic
> 
> and found the following issue:
> WARNING in reg_bounds_sanity_check
> 
> Full report is available here:
> https://ci.syzbot.org/series/fd950b40-1da8-44b1-bd12-4366e4a354b1
> 
> ***
> 
> WARNING in reg_bounds_sanity_check
> 
> tree:      bpf-next
> URL:       https://kernel.googlesource.com/pub/scm/linux/kernel/git/bpf/bpf-next.git
> base:      07866544e410e4c895a729971e4164861b41fad5
> arch:      amd64
> compiler:  Debian clang version 20.1.7 (++20250616065708+6146a88f6049-1~exp1~20250616065826.132), Debian LLD 20.1.7
> config:    https://ci.syzbot.org/builds/c4af872a-9b42-4821-a832-941921acc063/config
> C repro:   https://ci.syzbot.org/findings/8dfae15e-cda5-4fa6-8f95-aab106ebd860/c_repro
> syz repro: https://ci.syzbot.org/findings/8dfae15e-cda5-4fa6-8f95-aab106ebd860/syz_repro
> 
> verifier bug: REG INVARIANTS VIOLATION (true_reg1): range bounds violation u64=[0xffffdfcd, 0xffffffffffffdfcc] s64=[0x80000000ffffdfcd, 0x7fffffffffffdfcc] u32=[0xffffdfcd, 0xffffdfcc] s32=[0xffffdfcd, 0xffffdfcc] var_off=(0xffffdfcc, 0xffffffff00000000)

My is_branch_taken patch fixes some invariant violations. The test from
the second patch is even adapted from a syzkaller reproduction manually
extracted from logs at [1]. Ironically, by improving the branch
detection, we can also sometimes degrade state pruning (as discussed in
the first patch) which causes the exploration of new branches.

All that to say the current syzkaller repro is not directly caused by
my patch. It simply causes a new branch to be explored, and there is a
different kind of invariant violation on that branch. The full (sk_skb)
program is below [2], but the end of verifier logs are enough to
understand what's happening:

    12: (2f) r5 *= r6                  ; R5_w=scalar(smax=0x7ffffffffffffffc,umax=0xfffffffffffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; 0xfffffffffffffffc)) R6_w=0x9fe719f2
    13: (65) if r7 s> 0x1 goto pc-7    ; R7_w=scalar(id=67,smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
    14: (07) r7 += -8243               ; R7=scalar(smin=smin32=-8243,smax=smax32=-8242,umin=0xffffffffffffdfcd,umax=0xffffffffffffdfce,umin32=0xffffdfcd,umax32=0xffffdfce,var_off=(0xffffffffffffdfcc; 0x3))
    15: (1e) if w5 == w7 goto pc+0
    verifier bug: REG INVARIANTS VIOLATION (true_reg1): range bounds violation u64=[0xffffdfcd, 0xffffffffffffdfcc] s64=[0x80000000ffffdfcd, 0x7fffffffffffdfcc] u32=[0xffffdfcd, 0xffffdfcc] s32=[0xffffdfcd, 0xffffdfcc] var_off=(0xffffdfcc, 0xffffffff00000000)

The invariant violation follows the same pattern as usual: the verifier
walks a dead branch, uses it to improve ranges, and ends up with
inconsistent ranges. In this case, the u32 min value is larger than the
u32 max value. We can notice that the condition at instruction 15 is
always false because, if w5 and w7 were equal, the intersection of their
tnums would give us a constant (0xffffdfcc) that isn't within R7's u32
range. Hence, w5 and w7 can't be equal.

I have a patch to potentially fix this, but I'm still testing it and
would prefer to send it separately as it doesn't really relate to my
current patchset.

1 - https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf
2 - syzkaller program:

    r5 = *(u32 *)(r1 +112)
    r3 = *(u32 *)(r1 +108)
    r0 = r10
    r0 += 85328110
    if w3 != w0 goto +1
    if w5 == 0x0 goto +0
    r6 = *(u16 *)(r1 +62)
    r7 = r0
    if w5 > 0x2007ff0f goto +7
    r6 <<= 32
    w6 -= 1612244494
    r0 = r5
    r5 *= r6
    if r7 s> 0x1 goto -7
    r7 += -8243
    if w5 == w7 goto +0
    r4 = r5
    r4 += -458748
    if r3 < r4 goto +1
    exit
    if r0 == 0x0 goto +0

[...]

Re: [syzbot ci] Re: bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Eduard Zingerman]

On Wed, 2025-08-20 at 13:34 +0200, Paul Chaignon wrote:

[...]

> I have a patch to potentially fix this, but I'm still testing it and
> would prefer to send it separately as it doesn't really relate to my
> current patchset.

I'd like to bring this point again: this is a cat-and-mouse game.
is_scalar_branch_taken() and regs_refine_cond_op() are essentially
same operation and should be treated as such: produce register states
for both branches and prune those that result in an impossible state.
There is nothing wrong with this logically and we haven't got a single
real bug from the invariant violations check if I remember correctly.

Comparing the two functions, it looks like tricky cases are BPF_JE/JNE
and BPF_JSET/JSET|BPF_X. However, given that regs_refine_cond_op() is
called for a false branch with opcode reversed it looks like there is
no issues with these cases.

I'll give this a try.

[...]

Re: [syzbot ci] Re: bpf: Use tnums for JEQ/JNE is_branch_taken logic

[Paul Chaignon]

On Wed, Aug 20, 2025 at 12:37:46PM -0700, Eduard Zingerman wrote:
> On Wed, 2025-08-20 at 13:34 +0200, Paul Chaignon wrote:
> 
> [...]
> 
> > I have a patch to potentially fix this, but I'm still testing it and
> > would prefer to send it separately as it doesn't really relate to my
> > current patchset.
> 
> I'd like to bring this point again: this is a cat-and-mouse game.
> is_scalar_branch_taken() and regs_refine_cond_op() are essentially
> same operation and should be treated as such: produce register states
> for both branches and prune those that result in an impossible state.

I agree. I've been slowly convincing myself of the same :)
So far, the syzkaller invariant violation reports have been useful to
retrieve examples of where the two functions diverge and to deduce
improvements. But syzkaller now seems to be iterating between the same
three different cases of violations, so maybe it's time to look at a
more generic solution.

I assume you would call regs_refine_cond_op() then reg_bounds_sync()
and use the result in is_scalar_branch_taken()? Most of the impossible
states are only exposed once passed through reg_bounds_sync().

> There is nothing wrong with this logically and we haven't got a single
> real bug from the invariant violations check if I remember correctly.

That's correct. We also have pretty good coverage of this logic in
selftests and now it seems in syzkaller as well. Agni is also
continuously verifying reg_bounds_sync(). So I think the risk of relying
on regs_refine_cond_op() and reg_bounds_sync() in
is_scalar_branch_taken() would be low.

> 
> Comparing the two functions, it looks like tricky cases are BPF_JE/JNE
> and BPF_JSET/JSET|BPF_X. However, given that regs_refine_cond_op() is
> called for a false branch with opcode reversed it looks like there is
> no issues with these cases.
> 
> I'll give this a try.

I'd be happy to contribute selftests extracted from the syzkaller logs.
It's still hitting three different kinds of invariant violations: the
one reported here, the one addressed by my patch, and another one.

And I'm of course interested to run any patch through Cilium's CI to
check the complexity impact.

> 
> [...]