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

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2026-04-20 at 18:35 -0400, Harishankar Vishwanathan wrote:
> On Fri, Apr 17, 2026 at 8:45 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Fri, 2026-04-17 at 20:38 -0400, Harishankar Vishwanathan wrote:
> > > On Fri, Apr 17, 2026 at 7:19 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > > > 
> > > > On Fri, 2026-04-17 at 14:17 -0700, Eduard Zingerman wrote:
> > > > > On Fri, 2026-04-17 at 01:34 -0400, Harishankar Vishwanathan wrote:
> > > > > 
> > > [...]
> > > > 
> 
> > Thank you for sharing the code. Indeed very similar logic.
> > I was under impression that you don't like the witness idea hence
> > proceeded on my own. Would have deferred to you if not for that.
> 
> I suppose I didn't look at it like "witness generation", but rather an
> "allwise intersection exists". Turns out of course, that both ideas
> are essentially similar. Also figured I should finish verifying and then
> share my implementation.
> 
> > Tbh, my version looks a bit shorter/simpler.
> 
> Agree yours is shorter. But I found the individual
> computations in my implementation easier to follow.

find_witness_aux() might be a bit packed, but I like the successive
subdivision into cases more than ranges accumulation into array.

> [...]
> 
> I can follow up with a v2, which includes ideas from both, probably closer
> to your version.

Sure, please follow-up.