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 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.  Since we already are
talking about an approximation, it might be fine to do additional
simplifications.

For example, given the current implementations for
is_scalar_branch_taken(), regs_refine_cond_op(),
deduce_bounds_64_from_64() is it ever possible for u64 range not to
intersect with s64 range?

After spending some time with pen and paper for BPF_JLE operation I
suspect that it is not possible. I also encoded this as a small cbmc
test: https://github.com/eddyz87/intersection-check.
I suspect that same reasoning applies for other operations.

I'd suggest to drop the u32/s32 and u64/s64 checks, unless a counter
example can be found. I'm not sure about 64/32-bit checks.
Wdyt?

[...]