On Fri, Oct 27, 2023 at 01:49:34PM -0700, Andrii Nakryiko wrote:
> On Thu, Oct 26, 2023 at 9:57 PM Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> wrote:
> > On Mon, Oct 23, 2023 at 09:50:59AM -0700, Andrii Nakryiko wrote:
[...]
> > > > The way around this is that we can slightly change how we track the bounds,
> > > > and instead use
> > > >
> > > > struct bounds {
> > > > u64 base; /* base = umin */
> > > > /* Maybe there's a better name other than "size" */
> > > > u64 size; /* size = umax - umin */
> > > > }
> > > >
> > > > Using this base + size approach, previous old bound would have looked like
> > > >
> > > > <----------> base = A
> > > > |----------********************--|
> > > > <------------------> size = B - A
> > > >
> > > > Looking at the bounds this way means we can now capture the union of bound
> > > > #1 and bound #2 above. Here it is again for reference
> > > >
> > > > |**************------------******| union of bound #1 and bound #2
> > > >
> > > > Because registers are u64-sized, they wraps, and if we extend the u64 number
> > > > line, it would look like this due to wrapping
> > > >
> > > > u64 same u64 wrapped
> > > > |**************------------******|*************------------******|
> > > >
> > > > Which can be capture with the base + size semantic
> > > >
> > > > <--------------------------> base = (u64) A + 2^63
> > > > |**************------------******|*************------------******|
> > > > <------------------> size = B - A,
> > > > doesn't change after add
> > > >
> > > > Or looking it with just a single u64 number line again
> > > >
> > > > <--------------------------> base = (u64) A + 2^63
> > > > |**************------------******|
> > > > <-------------> base + size = (u64) (B + 2^32)
> > > >
> > > > This would mean that umin and umax is no longer readily available, we now
> > > > have to detect whether base + size wraps to determin whether umin = 0 or
> > > > base (and similar for umax). But the verifier already have the code to do
> > > > that in the existing scalar_min_max_add(), so it can be done by reusing
> > > > existing code.
[...]
> > > > Now back to the topic of unification of signed and unsigned range. Using the
> > > > union of bound #1 and bound #2 again as an example (size = B - A, and
> > > > base = (u64) A + 2^63)
> > > >
> > > > |**************------------******| union of bound #1 and bound #2
> > > >
> > > > And look at it's wrapped number line form again
> > > >
> > > > u64 same u64 wrapped
> > > > <--------------------------> base
> > > > |**************------------******|*************------------******|
> > > > <------------------> size
> > > >
> > > > Now add in the s64 range and align both u64 range and s64 at 0, we can see
> > > > what previously was a bound that umin/umax cannot track is simply a valid
> > > > smin/smax bound (idea drawn from patch [2]).
> > > >
> > > > 0
> > > > |**************------------******|*************------------******|
> > > > |----------********************--|
> > > > s64
> > > >
> > > > The question now is be what is the "signed" base so we proceed to calculate
> > > > the smin/smax. Note that base starts at 0, so for s64 the line that
> > > > represents base doesn't start from the left-most location.
> > > > (OTOH size stays the same, so we know it already)
> > > >
> > > > s64
> > > > 0
> > > > <-----> signed base = ?
> > > > |----------********************--|
> > > > <------------------> size is the same
> > > >
> > > > If we put u64 range back into the picture again, we can see that the "signed
> > > > base" was, in fact, just base casted into s64, so there's really no need for
> > > > a "signed" base at all
> > > >
> > > > <--------------------------> base
> > > > |**************------------******|
> > > > 0
> > > > <-----> signed base = (s64) base
> > > > |----------********************--|
> > > >
> > > > Which shows base + size approach capture signed and unsigned bounds at the
> > > > same time. Or at least its the best attempt I can make to show it.
> > > >
> > > > One way to look at this is that base + size is just a generalization of
> > > > umin/umax, taking advantage of the fact that the similar underlying hardware
> > > > is used both for the execution of BPF program and bound tracking.
> > > >
> > > > I wonder whether this is already being done elsewhere, e.g. by PREVAIL or
> > > > some of static code analyzer, and I can just borrow the code from there
> > > > (where license permits).
> > >
> > > A slight alternative, but the same idea, that I had (though after
> > > looking at reg_bounds_sync() I became less enthusiastic about this)
> > > was to unify signed/unsigned ranges by allowing umin u64> umax. That
> > > is, invalid range where umin is greater than umax would mean the wrap
> > > around case (which is also basically smin/smax case when it covers
> > > negative and positive parts of s64/s32 range).
> > >
> > > Taking your diagram and annotating it a bit differently:
> > >
> > > |**************------------******|
> > > umax umin
> >
> > Yes, that was exactly that's how I look at it at first (not that
> > surprisingly given I was drawing ideas from you patchset :) ), and it
> > certainly has the benefit of preserving both bounds, where as the base +
> > size approach only preserve one of the bounds, leaving the other to be
> > calculated.
> >
> > The problem I have with allowing umin u64> umax is mostly a naming one, that
> > it would be rather error prone and too easy to assume umin is always smaller
> > than umax (after all, that how it works now); and I can't come up with a
> > better name for them in that form.
>
> min64/max64 and min32/max32 would be my proposal if/when we unify them.
i'm going with start/end for now since it go along quite well with the
number line analogy, where the number line start at at one point and
ends at another; and it should be less assuming about how the values
compares.
Following this logic, `end - start` would be call the length, rather
than size that I've proposed above. Calling size is not that great
because it implies this is the number of values between the two bounds,
but in fact it is off by one, (borrowing from Eduard's email[1]) the
actual number of values N between two bounds is
N = end - start + 1
1: https://lore.kernel.org/bpf/d7af631802f0cfae20df77fe70068702d24bbd31.camel@xxxxxxxxx/
> > But as you've pointed out both approach are the same idea, if one works so
> > will the other.
> >
> > > It will make everything more tricky, but if someone is enthusiastic
> > > enough to try it out and see if we can make this still understandable,
> > > why not?
> >
> > I'll blindly assume reg_bounds_sync() can be worked out eventually to keep
> > my enthusiasm and look at just the u64/s64 case for now, let see how that
> > goes...
> >
>
> probably, yes
>
> > > > The glaring questions left to address are:
> > > > 1. Lots of talk with no code at all:
> > > > Will try to work on this early November and send some result as RFC. In
> > > > the meantime if someone is willing to give it a try I'll do my best to
> > > > help.
> > > >
> > > > 2. Whether the same trick applied to scalar_min_max_add() can be applied to
> > > > other arithmetic operations such as BPF_MUL or BPF_DIV:
> > > > Maybe not, but we should be able to keep on using most of the existing
> > > > bound inferring logic we have scalar_min_max_{mul,div}() since base +
> > > > size can be viewed as a generalization of umin/umax/smin/smax.
> > > >
> > > > 3. (Assuming this base + size approach works) how to integrate it into our
> > > > existing codebase:
> > > > I think we may need to refactor out code that touches
> > > > umin/umax/smin/smax and provide set-operation API where possible. (i.e.
> > > > like tnum's APIs)
> > > >
> > > > 4. Whether the verifier loss to ability to track certain range that comes
> > > > out of mixed u64 and s64 BPF operations, and this loss cause some BPF
> > > > program that passes the verfier to now be rejected.
> > >
> > > Very well might be, I've seen some crazy combinations in my testing.
> > > Good thing is that I'm adding a quite exhaustive tests that try all
> > > different boundary conditions. If you check seeds values I used, most
> > > of them are some sort of boundary for signed/unsigned 32/64 bit
> > > numbers. Add to that abstract interpretation model checking, and you
> > > should be able to validate your ideas pretty easily.
> >
> > Thanks for the heads up. Would be glad to see the exhaustive tests being
> > added!
>
> Check [0]. You can run range vs consts (7.7mln cases) with
>
> sudo SLOW_TESTS=1 ./test_progs -a 'reg_bounds_gen_consts*' -j
>
> And range vs range (106mln cases right now) with
>
> sudo SLOW_TESTS=1 ./test_progs -a 'reg_bounds_gen_ranges*' -j
>
> The latter might take a bit, it runs for about 1.5 hours for me.
>
> It's not exhaustive in a strict sense of this word, as we can't really
> try all possible u64/s64 ranges, ever. But it tests a lot of edge
> values on the border between min/max values for u32/s32 and u64/s32.
> Give it a try.
>
> [0] https://patchwork.kernel.org/project/netdevbpf/list/?series=797178&state=*
Finally gave it a better look today. It looks good. With this I should
be able to easily see how the unified range tracking differs from the
latest implementation once I have conditional jump logic implemented.
I've only got to add/sub/mul so far[2].
2: https://lore.kernel.org/bpf/20231108054611.19531-1-shung-hsi.yu@xxxxxxxx/
[...]
