|
From: John R. <jr...@bi...> - 2012-08-01 22:32:42
|
On 08/01/2012 12:08 PM, Julian Seward wrote:
>
>> I am interested in the accuracy of the V-Bit calculations
>
> So am I.
I consider that memcheck often generates incorrect V bits.
Memcheck does not understand word-wide binary integer inequality.
!!((a ^ b) & Va & Vb) ==> (a != b) [inequality at any position that has
two Valid bits determines Valid inequality for the whole operation.
http://bugs.kde.org/show_bug.cgi?id=117362
Summary: false positive uninit for bitfields or partial word.
This bug is nearing 7 years old (filed 2005-11-30) and includes
three suggested approaches for a fix.]
Memcheck does not understand binary integer addition.
If there is a place value [bit number] at which both operands
have a Valid zero bit, then a CarryIn which propagates into that bit gets stopped
(CarryOut is guaranteed to be zero), but memcheck will propagate an Undef Carry
through that bit position anyway. Memcheck propagates Undef "all the way
to the left" regardless of CarryStop.
-----
#include <stdlib.h>
#include <stdio.h>
main(int argc, char *argv[])
{
int *p = malloc(sizeof(int));
*p &= 0xff; /* top 24 bits of *p are Valid and zero */
int *q = malloc(sizeof(int));
*q &= 0xff; /* top 24 bits of *q are Valid and zero */
/* The top 23 bits of the sum are Valid and zero. */
if ((*p + *q) < 0) {
printf("Impossible.\n");
}
return 0;
}
----- The complaint from memcheck [below] is incorrect.
==15496== Conditional jump or move depends on uninitialised value(s)
==15496== at 0x400585: main (memcheck-add.c:11)
Memcheck does not understand unsigned integer remainder by 2**n-1.
(((a*256*256*256) + (b*256*256) + (c*256) + d) % 255) == ((a+b+c+d) % 255)
>From that it can be seen that Undef "middle" bits in each of a,b,c,d
do not affect the V bits for low bits of the remainder, as long as
(a+b+c+d) < 255.
But memcheck says that any Undef on input gives an Undef remainder.
Memcheck gives up if it encounters Undef bits in floating point arithmetic.
If either operand has any Undef bits, then all bits of all results are Undef.
In practice for floating point compare, often this is the worst thing to do.
It is very likely that the floating condition codes do not depend on a few
Undef bits in either input. [Numerical analysis wouldn't exist if it did.]
Almost the same can be said for floating point addition, subtraction, and
multiplication: the sign, exponent and more-significant fraction bits of many
particular results often do not depend on a few less-significant fraction bits.
Beyond individual operations, memcheck is blind with respect to
"re-convergent fan-out". If there is any common history between the
two operands, then memcheck does not care, even though the result may.
(a ^ a) ==> 0 regardless of Undef in 'a'; but memcheck ignores this
(x & ~x) ==> 0 regardless of Undef in 'x'; but memcheck ignores this
Generally, memcheck often ignores any contribution that the actual values
of Valid operand bits might make to the Valid bits of the result. That is,
memcheck often believes that the V bits of the result depend only on the
opcode and the V bits of the inputs, and not on the inputs themselves
(in particular, the actual values of input bits that are Valid.)
[If the actual shift count is all-Valid, then "shift by variable number
of bits" is an exception. But if the shift count itself has any Undef
bits, then memcheck says "all result bits are Undef" even though a
detailed analysis might not give such a pessimistic result. Shifting by
"either 2 or 3" (because of an Undef low bit in the count) need not
totally destroy the output, although in this case memcheck says "every bit
of the result is Undef, regardless of the actual bits and actual V bits
of the other operand."]
--
|