public inbox for bpf@vger.kernel.org
 help / color / mirror / Atom feed
From: Paul Chaignon <paul.chaignon@gmail.com>
To: sashiko@lists.linux.dev
Cc: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>,
	bpf@vger.kernel.org
Subject: Re: [PATCH bpf-next 2/2] selftests/bpf: Test for empty intersection of tnum and u64
Date: Thu, 16 Apr 2026 19:51:53 +0200	[thread overview]
Message-ID: <aeEhua0q1C8xCO0F@mail.gmail.com> (raw)
In-Reply-To: <20260415182952.C7B77C19424@smtp.kernel.org>

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

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

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

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

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

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

Same here.

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

      reply	other threads:[~2026-04-16 17:51 UTC|newest]

Thread overview: 18+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2026-04-15 16:07 [PATCH bpf-next 0/2] Detect and prune dead branches using intersection checks Harishankar Vishwanathan
2026-04-15 16:07 ` [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches Harishankar Vishwanathan
2026-04-15 17:04   ` bot+bpf-ci
2026-04-15 19:02   ` Paul Chaignon
2026-04-16  1:10   ` Eduard Zingerman
2026-04-16 17:23     ` Eduard Zingerman
2026-04-16 23:13     ` Harishankar Vishwanathan
2026-04-16 23:33       ` Eduard Zingerman
2026-04-17  5:24         ` Eduard Zingerman
2026-04-17  5:34         ` Harishankar Vishwanathan
2026-04-17 21:17           ` Eduard Zingerman
2026-04-17 23:19             ` Eduard Zingerman
2026-04-18  0:38               ` Harishankar Vishwanathan
2026-04-18  0:45                 ` Eduard Zingerman
2026-04-18  0:22             ` Harishankar Vishwanathan
2026-04-15 16:07 ` [PATCH bpf-next 2/2] selftests/bpf: Test for empty intersection of tnum and u64 Harishankar Vishwanathan
2026-04-15 18:29   ` sashiko-bot
2026-04-16 17:51     ` Paul Chaignon [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=aeEhua0q1C8xCO0F@mail.gmail.com \
    --to=paul.chaignon@gmail.com \
    --cc=bpf@vger.kernel.org \
    --cc=harishankar.vishwanathan@gmail.com \
    --cc=sashiko@lists.linux.dev \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox