|
From: John R. <jr...@bi...> - 2012-01-12 21:03:30
|
On 01/12/2012 12:02 PM, Christian Borntraeger wrote:
>> For binary floating point, memcheck currently tracks undefined bits very coarsely.
>> If at least one bit of input is Undefined, then every bit of output is Undefined.
>
> Being not an expert on floating point, isnt that exactly what we want? I would consider
> any undefined bit in floating point input a bug, no?
No, that is only the least possible "good" property. I want the best possible
good property: An output bit is marked Undefined if and only if that bit is
Undefined after bit-by-bit examination using the value tables for one-bit
operations involving 0,1, and U. The one-bit table for addition is:
A B Ci Sum Cout
-------------------
0 0 0 0 0
0 0 U U 0 *
0 0 1 1 0
0 U 0 U 0 *
0 U U U U
0 U 1 U U
0 1 0 1 0
0 1 U U U
0 1 1 0 1
U 0 0 U 0 *
U 0 U U U
U 0 1 U U
U U 0 U U
U U U U U
U U 1 U U
U 1 0 U U
U 1 U U U
U 1 1 U 1 *
1 0 0 1 0
1 0 U U U
1 0 1 0 1
1 U 0 U U
1 U U U U
1 U 1 U 1 *
1 1 0 0 1
1 1 U U 1 *
1 1 1 1 1
The rows marked with '*' are cases where CarryOut (Cout) is Defined
even though exactly one input from {A, B, Ci} is Undefined. Currently
memcheck pessimizes these cases by assuming that Cout also is Undefined.
For example, if the inputs to a Decimal Floating Point ADD are
12.34 with all bits Defined except the 00.20 bit,
and 65.65 with all bits Defined
+ ----- then the result of ADD is
77.99 with all bits Defined except the 00.60 bits
(the 00.20 bit, also the 00.40 bit because of Carry)
Thus in particular the sum has no possible Undefined in the
integer part (77.) nor in the "low 5 bits" (the 00.19).
If DFP were to inherit its Undefined behavior from current binary FP,
then the sum would be marked as "all bits undefined", i.e., worthless.
Yet we know that only 2 of its bits can be bad.
--
|