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

[Eduard Zingerman <eddyz87@gmail.com>]

On Wed, 2026-04-15 at 18:10 -0700, Eduard Zingerman wrote:
> On Wed, 2026-04-15 at 12:07 -0400, Harishankar Vishwanathan wrote:
> > This commit introduces checks to detect if the ranges and/or tnums have
> > intersections between them, and uses the checks in
> > simulate_both_branches_taken and reg_bounds_sync.
> > 
> > The verifier is known to evolve the reg_states correctly (i.e. soundly)
> > on a live branch. In a previous commit [1], we used the ill-formedness
> > of a range (e.g. umin > umax), identified by range_bounds_violation, to
> > detect dead branches and prune the branch along which the ill-formedness
> > occurs.
> > 
> > Another opportunity to prune branches is when the ranges and/or tnums
> > have don't intersect. When the verifier evolves the reg_state along a
> > dead branch, it is possible that abstract value in one domain (e.g tnum)
> > doesn't match with the abstract value in the other domain (e.g. u64), so
> > that there is no single value x, that is contained in both the abstract
> > values.
> > 
> > First, we introduce intersection checks for each of the 5 domains (for a
> > total of 10 domain pairs), and wrap it in reg_bounds_intersect.
> 
> Hi Harishankar,
> 
> I thought some more on the topic if checks for all 10 domain pairs are
> necessary and now have some doubts. Ideally, what one wants to check
> is that there exist a value included in all 5 domains.  Unfortunately,
> it is too complicated to encode such a check, so the patch-set
> approximates this doing pairwise intersections.

Speaking of which, how hard would it be to figure out the witness value?
Assuming that __update_reg64_bounds() happened would it be sufficient
to check tmin, tnum_step(..., tmin) and tmax?

[...]