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

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2026-04-16 at 16:33 -0700, Eduard Zingerman wrote:

[...]

> Could you please comment about the witness idea?
> Suppose reg_bounds_sync() is modified to preserve the properties I
> described above, would it be sufficient to check two candidates:
> tmin and tnum_step(tmin) to identify a register in an invalid state?

Actually, the witness search procedure is probably more involved than that.
Something along the following lines (ignoring 32-bit ranges for now):

- case a. s64 range does not cross the sign boundary:
  - w := min(umin_value, (u64)smin_value)
  - w := w if w in tnum else tnum_step(tnum, w)
- case b. s64 range crosses the sign boundary:
  - if u64 range intersects with lower half of s64 range [0, (u64)smax_value]:
    - w := umin_value
    - w := w if w in tnum else tnum_step(tnum, w)
  - otherwise:
    - w := min((u64)smin_value, umax_value)
    - w := w if w in tnum else tnum_step(tnum, w)

And then check again if w still belongs to each range
(it belongs to tnum by construction).

'w' refinement for 32-bit ranges needs more thought.
It would probably be similar to 32-bit -> 64-bit from lower bound
refinement described in [1] or [2].

Wdyt?

[1] https://lore.kernel.org/bpf/20260410124035.297632-1-koike@igalia.com/
[2] https://lore.kernel.org/bpf/b2a0346a5b0818008503b721c62621918d84ad0a.1776344897.git.paul.chaignon@gmail.com/

It is much simpler with cnums [3] because sync of non-intersecting
ranges produces an empty range, and one would only need to apply the
tnum range logic from your patch-set. I really need to wrap-up that RFC.

[3] https://github.com/eddyz87/bpf/tree/cnums-everywhere