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

[Eduard Zingerman <eddyz87@gmail.com>]

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

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

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

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