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 14:17 -0700, Eduard Zingerman wrote:
> On Fri, 2026-04-17 at 01:34 -0400, Harishankar Vishwanathan 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?
> > 
> > IIUC, your idea is, if there is a witness, it should be one
> > of tmin, tnum_step(tmin).
> > 
> > - I don't think tmin, tnum_step(tmin) works, because you might
> > need several applications of tnum_step from tmin to reach umin.
> > 
> > - Assuming tnum_step(umin) to reach the first intersection of umin
> > with the tnum (let's say x), x might not intersect with the s64.
> > 
> > -  I think one of tnum_step(umin), tnum_step(smin), smin, umin works
> > to find the common intersection point among u64, s64 and tnum.
> > 
> > - But even then that particular intersection point must also intersect
> > with the u32 and s32 (when mapped to those domains). That
> > complicates the reasoning.
> > 
> > Also how would you ensure property 2 described above
> > in reg_bounds_sync()?
> 
> Continuing this train of thoughts, consider the function
> find_witness_aux() from [1]:
> 
>     /* pre-conditions:
>      * - (u32)a_min <= b_min
>      * - b_max <= (u32)a_max
>      */
>     static bool find_witness_aux(u64 a_min, u64 a_max, u32 b_min, u32 b_max,
>                                 struct tnum tnum, u64 *out)
> 
> If there is a tnum T, a 64-bit range A and a 32-bit range B, such that
> `(u32)a_min <= b_min && b_max <= (u32)a_max`,
> it can find a value that belongs to A, B and T if such value exist.
> 
> I believe that this function can be used as a basis for complete
> witness check including signed and unsigned ranges:
> - Each intersection between signed and unsigned ranges produces one or
>   two unsigned ranges. 
> - If e.g. (u32)a_min <= b_min does not hold, further subdivision is
>   possible.
> 
> Meaning that final witness check will need to enumerate several ranges
> and call find_witness_aux() several times.
> 
> Wdyt?
> 
> [1] https://github.com/eddyz87/find-witness

Pushed complete find_witness() implementation in [1].
cbmc verification passes.

    bool find_witness(struct bpf_reg_state *reg, u64 *out)

Takes a register as an input and produces a value satisfying all
domains if such value exist. Assumes that register is well-formed:
- min < max
- tnum.mask & tnum.value == 0

Required some incantations to make cbmc understand function contracts,
I might want to switch to some more mainstream checker.

In any case, please let me know what you think.