Re: [Valgrind-developers] [PATCH] Valgrind for PowerPC

[Paul M. <pa...@sa...>]

Julian Seward writes:

> >   reported errors a lot.  Glibc seems to like using the add-fefefeff
> >   and or-7f7f7f7f tricks a lot.  I have a formula for getting the
> >   valid bits for the result of an ADD exactly without too much effort.
> 
> Ha!  Tell me what it is (pretty please).  I have been wondering how to do
> that for a long time, without success, since it would also improve accuracy
> on x86.

If you have values A and B, with valid bits QA and QB, let

A_min = A & ~QA
A_max = A | QA
B_min = B & ~QB
B_max = B | QB

If we then let the sum S = A + B, then

QS = QA | QB | ((A_min + B_min) ^ (A_max + B_max))

Proof:

Let C be the carry-in to each bit of the sum.  Then

S = A ^ B ^ C

Thus QS = QA | QB | QC.  If we can work out QC, we are set.

Now, C is monotonic in A and B, in the sense that if you change a bit
in A or B from 0 to 1, you may get bits in C changing from 0 to 1, but
you won't get bits changing from 1 to 0.  (I can give a proof of this
if you like; it involves looking at which bit positions of the sum
generate or propagate carries.)

If we consider the range of possible A and B values from A_min to
A_max and B_min to B_max, we therefore have the smallest C value (in
an unsigned sense) for A_min + B_min, and the largest C value for
A_max + B_max.  In other words

C_min = (A_min + B_min) ^ A_min ^ B_min
C_max = (A_max + B_max) ^ A_max ^ B_max

so

QC = C_min ^ C_max
   = (A_min + B_min) ^ (A_max + B_max) ^ A_min ^ A_max ^ B_min ^ B_max
   = (A_min + B_min) ^ (A_max + B_max) ^ QA ^ QB

since QA = A_max ^ A_min and similarly for QB.

Then

QS = QA | QB | ((A_min + B_min) ^ (A_max + B_max) ^ QA ^ QB)

However, the only time the value of a bit of QC matters is when we
have 0 in the corresponding bits of QA and QB.  Therefore we can drop
the "^ QA ^ QB" in the QC term of this expression, yielding:

QS = QA | QB | ((A_min + B_min) ^ (A_max + B_max))

Regards,
Paul.