Edward Cree wrote:
> On 09/03/2020 23:58, Alexei Starovoitov wrote:> Thinking about it differently... var_off is a bit representation of
> > 64-bit register. So that bit representation doesn't really have
> > 32 or 16-bit chunks. It's a full 64-bit register. I think all alu32
> > and jmp32 ops can update var_off without losing information.
> Agreed; AFAICT the 32-bit var_off should always just be the bottom
> 32 bits of the full var_off.
This seems to work.
> In fact, it seems like the only situations where 32-bit bounds are
> needed are (a) the high and low halves of a 64-bit register are
> being used separately, so e.g. r0 = (x << 32) | y with small known
> bounds on y you want to track, or (b) 32-bit signed arithmetic.
> (a) doesn't seem like it's in scope to be supported, and (b) should
> (I'm naïvely imagining) only need the s32 bounds, not the u32 or
> var32.
I guess I'm not opposed to supporting (a) it seems like it should
be doable.
For (b) the primary reason is to keep symmetry between 32-bit and
64-bit cases. But also we could have mixed signed 32-bit comparisons
which this helps with.
Example tracking bounds with [x,y] being signed 32-bit
bounds and [x',y'] being unsigned 32-bit bounds.
r1 = # [x,y],[x',y']
w1 > 0 goto pc+y [x,y],[1 ,y']
w1 s> -10 goto pc+x [-10,y],[1 ,y']
We can't really deduce much from that in __reg_deduce_bounds so
we get stuck with different bounds on signed and unsigned space.
Same case as 64-bit world fwiw. I guess we could do more work
and use 64-bit/32-bit together and deduce something but I find
this more work than its worth. Keeping separate signed/unsigned
makes things easy.
>
> John Fastabend wrote:
> > For example, BPF_ADD will do a tnum_add() this is a different
> > operation when overflows happen compared to tnum32_add(). Simply
> > truncating tnum_add result to 32-bits is not the same operation.
> I don't see why. Overflows from the low (tracked) 32 bits can only
> affect the high 32.
> Truncation should be a homomorphism from
> Z_2^n to Z_2^m wrt. both addition and multiplication, and tnums
> are just (a particular class of) subsets of those rings.
Agreed, no need for 32bit ops on tnums.
> Can you construct an example of a tnum addition that breaks the
> homomorphism?
no, I'm convinced. There seems to be a proof that the above is
true if n>m.
>
> -ed
