diff mbox

fpu/softfloat: check for Inf / x or 0 / x before /0

Message ID 20180416135442.30606-1-alex.bennee@linaro.org (mailing list archive)
State New, archived
Headers show

Commit Message

Alex Bennée April 16, 2018, 1:54 p.m. UTC
The re-factoring of div_floats changed the order of checking meaning
an operation like -inf/0 erroneously raises the divbyzero flag.
IEEE-754 (2008) specifies this should only occur for operations on
finite operands.

We fix this by moving the check on the dividend being Inf/0 to before
the divisor is zero check.

Signed-off-by: Alex Bennée <alex.bennee@linaro.org>
Cc: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
---
 fpu/softfloat.c | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

Comments

Bastian Koppelmann April 16, 2018, 2:16 p.m. UTC | #1
On 04/16/2018 03:54 PM, Alex Bennée wrote:
> The re-factoring of div_floats changed the order of checking meaning
> an operation like -inf/0 erroneously raises the divbyzero flag.
> IEEE-754 (2008) specifies this should only occur for operations on
> finite operands.
> 
> We fix this by moving the check on the dividend being Inf/0 to before
> the divisor is zero check.
> 
> Signed-off-by: Alex Bennée <alex.bennee@linaro.org>
> Cc: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
> ---
>  fpu/softfloat.c | 10 +++++-----
>  1 file changed, 5 insertions(+), 5 deletions(-)

Reviewed-by: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
Tested-by: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>

Cheers,
Bastian
Alex Bennée April 16, 2018, 2:42 p.m. UTC | #2
Bastian Koppelmann <kbastian@mail.uni-paderborn.de> writes:

> On 04/16/2018 03:54 PM, Alex Bennée wrote:
>> The re-factoring of div_floats changed the order of checking meaning
>> an operation like -inf/0 erroneously raises the divbyzero flag.
>> IEEE-754 (2008) specifies this should only occur for operations on
>> finite operands.
>>
>> We fix this by moving the check on the dividend being Inf/0 to before
>> the divisor is zero check.
>>
>> Signed-off-by: Alex Bennée <alex.bennee@linaro.org>
>> Cc: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
>> ---
>>  fpu/softfloat.c | 10 +++++-----
>>  1 file changed, 5 insertions(+), 5 deletions(-)
>
> Reviewed-by: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
> Tested-by: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>

Peter are you going to grab these tags or do you want me to re-spin?


--
Alex Bennée
Peter Maydell April 16, 2018, 2:45 p.m. UTC | #3
On 16 April 2018 at 15:42, Alex Bennée <alex.bennee@linaro.org> wrote:
>
> Bastian Koppelmann <kbastian@mail.uni-paderborn.de> writes:
>
>> On 04/16/2018 03:54 PM, Alex Bennée wrote:
>>> The re-factoring of div_floats changed the order of checking meaning
>>> an operation like -inf/0 erroneously raises the divbyzero flag.
>>> IEEE-754 (2008) specifies this should only occur for operations on
>>> finite operands.
>>>
>>> We fix this by moving the check on the dividend being Inf/0 to before
>>> the divisor is zero check.
>>>
>>> Signed-off-by: Alex Bennée <alex.bennee@linaro.org>
>>> Cc: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
>>> ---
>>>  fpu/softfloat.c | 10 +++++-----
>>>  1 file changed, 5 insertions(+), 5 deletions(-)
>>
>> Reviewed-by: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
>> Tested-by: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>
>
> Peter are you going to grab these tags or do you want me to re-spin?

'patches' will grab them automatically when it applies the patch.

thanks
-- PMM
Richard Henderson April 16, 2018, 7:39 p.m. UTC | #4
On 04/16/2018 03:54 AM, Alex Bennée wrote:
> +    /* Inf / x or 0 / x */
> +    if (a.cls == float_class_inf || a.cls == float_class_zero) {
> +        a.sign = sign;
> +        return a;
> +    }

0/0 should raise an exception.

I find inf/0 non-intuitive, but there ya go.

r~
Peter Maydell April 17, 2018, 8:56 a.m. UTC | #5
On 16 April 2018 at 20:39, Richard Henderson
<richard.henderson@linaro.org> wrote:
> On 04/16/2018 03:54 AM, Alex Bennée wrote:
>> +    /* Inf / x or 0 / x */
>> +    if (a.cls == float_class_inf || a.cls == float_class_zero) {
>> +        a.sign = sign;
>> +        return a;
>> +    }
>
> 0/0 should raise an exception.

It does -- we check for 0/0 and Inf/Inf first, just before this check.

thanks
-- PMM
Peter Maydell April 17, 2018, 8:57 a.m. UTC | #6
On 16 April 2018 at 14:54, Alex Bennée <alex.bennee@linaro.org> wrote:
> The re-factoring of div_floats changed the order of checking meaning
> an operation like -inf/0 erroneously raises the divbyzero flag.
> IEEE-754 (2008) specifies this should only occur for operations on
> finite operands.
>
> We fix this by moving the check on the dividend being Inf/0 to before
> the divisor is zero check.
>
> Signed-off-by: Alex Bennée <alex.bennee@linaro.org>
> Cc: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>

Applied, thanks.

-- PMM
Emilio Cota April 17, 2018, 7:04 p.m. UTC | #7
On Mon, Apr 16, 2018 at 14:54:42 +0100, Alex Bennée wrote:
> The re-factoring of div_floats changed the order of checking meaning
> an operation like -inf/0 erroneously raises the divbyzero flag.
> IEEE-754 (2008) specifies this should only occur for operations on
> finite operands.
> 
> We fix this by moving the check on the dividend being Inf/0 to before
> the divisor is zero check.
> 
> Signed-off-by: Alex Bennée <alex.bennee@linaro.org>
> Cc: Bastian Koppelmann <kbastian@mail.uni-paderborn.de>

I can confirm this fixes the issue -- just checked with a modified
version of fp-test, see below.

Note that in fp-test I am not checking for flags that are raised
when none are expected, because doing so gives quite a few errors.
Just noticed that enabling this check yields 1049 of these errors for
v2.11, and before this patch that number was 1087. After this
patch, it is again brought down to 1049. IOW, the test cases in
fp-test raise exactly the same flags as v2.11, which is good to know.

The 1049 errors are probably false positives -- at least a big
chunk of them should be, given that "-t host" gives even more errors.
I am tempted to keep the flag check and whitelist these errors
though, which would catch regressions such as the one we're fixing here.

Here is the report file with the 1049 failing test cases:
  http://www.cs.columbia.edu/~cota/qemu/fp-test-after-inf-patch.txt

Thanks,

		Emilio
Peter Maydell April 17, 2018, 8:54 p.m. UTC | #8
On 17 April 2018 at 20:04, Emilio G. Cota <cota@braap.org> wrote:
> Note that in fp-test I am not checking for flags that are raised
> when none are expected, because doing so gives quite a few errors.
> Just noticed that enabling this check yields 1049 of these errors for
> v2.11, and before this patch that number was 1087. After this
> patch, it is again brought down to 1049. IOW, the test cases in
> fp-test raise exactly the same flags as v2.11, which is good to know.
>
> The 1049 errors are probably false positives -- at least a big
> chunk of them should be, given that "-t host" gives even more errors.
> I am tempted to keep the flag check and whitelist these errors
> though, which would catch regressions such as the one we're fixing here.

I strongly suspect we do have a few cases where we get the answers
wrong and/or don't report the flags right, so ideally we'd have
a look at them in more detail...

> Here is the report file with the 1049 failing test cases:
>   http://www.cs.columbia.edu/~cota/qemu/fp-test-after-inf-patch.txt

Syntax for interpreting the report:
https://www.research.ibm.com/haifa/projects/verification/fpgen/syntax.txt

Here's the first one, am I reading it right?

+ 0xffc00000 0xffb00000, expected: 0xffc00000, returned: 0xffc00000,
expected exceptions: none, returned: i
error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:1346:
b32+ =0 Q S -> Q

That's a float32 addition where the first input is a QNaN
and the second an SNaN (presumably the test is configured
for what in QEMU is snan_bit_is_one == 0), and it expects
the result to be the QNaN, with no exceptions set. But
we raise Invalid.
=0 is the rounding mode, not relevant here.

IEEE754-2008 s6.2 seems pretty clear that if there's
an SNaN as an operand then operations like addition should
signal Invalid. So this looks like a bug in the test case
input. (Which is weird, because IBM must have tested this,
so it's odd to see an obvious error in it.)

Most of the "expected none, returned i" lines look
like the same thing. We should look at the others, though.

thanks
-- PMM
diff mbox

Patch

diff --git a/fpu/softfloat.c b/fpu/softfloat.c
index b46dccc63e..a7d0f3ff56 100644
--- a/fpu/softfloat.c
+++ b/fpu/softfloat.c
@@ -1146,6 +1146,11 @@  static FloatParts div_floats(FloatParts a, FloatParts b, float_status *s)
         a.cls = float_class_dnan;
         return a;
     }
+    /* Inf / x or 0 / x */
+    if (a.cls == float_class_inf || a.cls == float_class_zero) {
+        a.sign = sign;
+        return a;
+    }
     /* Div 0 => Inf */
     if (b.cls == float_class_zero) {
         s->float_exception_flags |= float_flag_divbyzero;
@@ -1153,11 +1158,6 @@  static FloatParts div_floats(FloatParts a, FloatParts b, float_status *s)
         a.sign = sign;
         return a;
     }
-    /* Inf / x or 0 / x */
-    if (a.cls == float_class_inf || a.cls == float_class_zero) {
-        a.sign = sign;
-        return a;
-    }
     /* Div by Inf */
     if (b.cls == float_class_inf) {
         a.cls = float_class_zero;