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(-)

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;
-- 
2.17.0

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

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

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

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~

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

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

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

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

On Tue, Apr 17, 2018 at 21:54:03 +0100, Peter Maydell wrote:
> 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.

Yes, you're reading it right.

> 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.)

Yes sometimes the input files don't make much sense -- that's why
I ended up whitelisting some of them.

BTW I just checked with -t host on an IBM Power8, and we get
the same 1049 flag errors we get with -t soft plus two additional ones:

+A 0xffb00000, expected: 0x7fa00000, returned: 0x7fa00000, \
  expected exceptions: i, returned: none
+error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:382:
+b32A =0 S -> S i
(...)
+cff 0xffb00000, expected: 0x7ff8000000000000, returned: 0x7ff4000000000000, \
  expected exceptions: i, returned: none
+error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:26170:
+b32b64cff =0 S -> Q i

On x86 with -t host we again get a strict superset of what we get
with -t soft.

So yeah, I don't know what these test cases are about.

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

Given the above, whitelisting the 1049 cases and forcing the flag
checks for all tests (as below) seems reasonable to me.

--- a/tests/fp/fp-test.c
+++ b/tests/fp/fp-test.c
@@ -247,7 +247,7 @@ static enum error tester_check(const struct test_op *t, uint64_t res64,
             goto out;
         }
     }
-    if (t->exceptions && flags != (t->exceptions | default_exceptions)) {
+    if (flags != (t->exceptions | default_exceptions)) {
         err = ERROR_EXCEPTIONS;
         goto out;
     }

Thanks,

		E.

On 17 April 2018 at 22:27, Emilio G. Cota <cota@braap.org> wrote:
> BTW I just checked with -t host on an IBM Power8, and we get
> the same 1049 flag errors we get with -t soft plus two additional ones:
>
> +A 0xffb00000, expected: 0x7fa00000, returned: 0x7fa00000, \
>   expected exceptions: i, returned: none
> +error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:382:
> +b32A =0 S -> S i

That's Abs of an SNaN; the test expects Invalid, which is wrong,
because IEEE754 says absolute-value is a "quiet-computational
operation" that never signals an exception.

What's odd is that we don't report that error for the softfloat
implementation! I also don't understand why the expected value
isn't just the input value with the sign bit flipped.

> (...)
> +cff 0xffb00000, expected: 0x7ff8000000000000, returned: 0x7ff4000000000000, \
>   expected exceptions: i, returned: none
> +error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:26170:
> +b32b64cff =0 S -> Q i

SNaN conversion from 32 bit to 64 bit. Here I agree
with the test -- we should quieten the NaN and raise
Invalid -- which implies that the hardware is wrong ?!?

thanks
-- PMM

On Tue, Apr 17, 2018 at 22:45:51 +0100, Peter Maydell wrote:
> On 17 April 2018 at 22:27, Emilio G. Cota <cota@braap.org> wrote:
> > BTW I just checked with -t host on an IBM Power8, and we get
> > the same 1049 flag errors we get with -t soft plus two additional ones:
> >
> > +A 0xffb00000, expected: 0x7fa00000, returned: 0x7fa00000, \
> >   expected exceptions: i, returned: none
> > +error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:382:
> > +b32A =0 S -> S i
> 
> That's Abs of an SNaN; the test expects Invalid, which is wrong,
> because IEEE754 says absolute-value is a "quiet-computational
> operation" that never signals an exception.
> 
> What's odd is that we don't report that error for the softfloat
> implementation! I also don't understand why the expected value
> isn't just the input value with the sign bit flipped.

With -t soft we don't handle "abs" and we don't get the error -- we get
a "not handled" instead.
Is there a function that we could use for abs? The only ones I've seen
are floatX_abs() which mask out the sign bit and do nothing else.

> > (...)
> > +cff 0xffb00000, expected: 0x7ff8000000000000, returned: 0x7ff4000000000000, \
> >   expected exceptions: i, returned: none
> > +error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:26170:
> > +b32b64cff =0 S -> Q i
> 
> SNaN conversion from 32 bit to 64 bit. Here I agree
> with the test -- we should quieten the NaN and raise
> Invalid -- which implies that the hardware is wrong ?!?

This passes on an Intel host, and fails on both Power7 and 8 hosts I have
access to. I don't have the Power ISA spec in front of me, but I hope
there's something about this specified in it.

		E.

On 04/17/2018 12:38 PM, Emilio G. Cota wrote:
> On Tue, Apr 17, 2018 at 22:45:51 +0100, Peter Maydell wrote:
>> On 17 April 2018 at 22:27, Emilio G. Cota <cota@braap.org> wrote:
>>> BTW I just checked with -t host on an IBM Power8, and we get
>>> the same 1049 flag errors we get with -t soft plus two additional ones:
>>>
>>> +A 0xffb00000, expected: 0x7fa00000, returned: 0x7fa00000, \
>>>   expected exceptions: i, returned: none
>>> +error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:382:
>>> +b32A =0 S -> S i
>>
>> That's Abs of an SNaN; the test expects Invalid, which is wrong,
>> because IEEE754 says absolute-value is a "quiet-computational
>> operation" that never signals an exception.
>>
>> What's odd is that we don't report that error for the softfloat
>> implementation! I also don't understand why the expected value
>> isn't just the input value with the sign bit flipped.
> 
> With -t soft we don't handle "abs" and we don't get the error -- we get
> a "not handled" instead.
> Is there a function that we could use for abs? The only ones I've seen
> are floatX_abs() which mask out the sign bit and do nothing else.

Both abs and neg are pure bit operations.  So, yes, floatX_abs (and floatX_chs)
are the softfloat functions for these.

And if fp-test thinks Invalid should be raised, it's wrong.

>>> (...)
>>> +cff 0xffb00000, expected: 0x7ff8000000000000, returned: 0x7ff4000000000000, \
>>>   expected exceptions: i, returned: none
>>> +error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:26170:
>>> +b32b64cff =0 S -> Q i
>>
>> SNaN conversion from 32 bit to 64 bit. Here I agree
>> with the test -- we should quieten the NaN and raise
>> Invalid -- which implies that the hardware is wrong ?!?
> 
> This passes on an Intel host, and fails on both Power7 and 8 hosts I have
> access to. I don't have the Power ISA spec in front of me, but I hope
> there's something about this specified in it.

IIRC this is unspecified and does vary by implementation.


r~

On 17 April 2018 at 23:49, Richard Henderson
<richard.henderson@linaro.org> wrote:
> On 04/17/2018 12:38 PM, Emilio G. Cota wrote:
>> On Tue, Apr 17, 2018 at 22:45:51 +0100, Peter Maydell wrote:
>>> On 17 April 2018 at 22:27, Emilio G. Cota <cota@braap.org> wrote:
>>>> (...)
>>>> +cff 0xffb00000, expected: 0x7ff8000000000000, returned: 0x7ff4000000000000, \
>>>>   expected exceptions: i, returned: none
>>>> +error: flags mismatch for input @ ibm/Basic-Types-Inputs.fptest:26170:
>>>> +b32b64cff =0 S -> Q i
>>>
>>> SNaN conversion from 32 bit to 64 bit. Here I agree
>>> with the test -- we should quieten the NaN and raise
>>> Invalid -- which implies that the hardware is wrong ?!?
>>
>> This passes on an Intel host, and fails on both Power7 and 8 hosts I have
>> access to. I don't have the Power ISA spec in front of me, but I hope
>> there's something about this specified in it.
>
> IIRC this is unspecified and does vary by implementation.

I think 754-2008 does specify it: s6.2 says that you get
'set Invalid and return a QNaN if an input is an SNaN' for
"every general-computational and signaling-computational
operation except for the conversions described in 5.12".
So the only exceptions are:
 1) the s5.12 conversions, which are to/from strings-of-characters
 2) quiet-computational operations, which are just
    copy, abs, negate, copySign, and some re-encoding
    operations involving decimal formats

float-to-float conversions are general-computational.

I don't have the original IEEE754 spec to hand though;
that may have left this unspecified.

thanks
-- PMM

On 18 April 2018 at 00:01, Peter Maydell <peter.maydell@linaro.org> wrote:
> I don't have the original IEEE754 spec to hand though;
> that may have left this unspecified.

Having located a copy of 754-1985 I think that also is
clear enough that float-float conversion is an operation
that must quieten SNaN and raise Invalid.

thanks
-- PMM

On 04/17/2018 01:08 PM, Peter Maydell wrote:
> On 18 April 2018 at 00:01, Peter Maydell <peter.maydell@linaro.org> wrote:
>> I don't have the original IEEE754 spec to hand though;
>> that may have left this unspecified.
> 
> Having located a copy of 754-1985 I think that also is
> clear enough that float-float conversion is an operation
> that must quieten SNaN and raise Invalid.

That does seem to match actual processor behaviour.
The attached test case produces

7fa00000
7ffc000000000000 - 1
7ff4000000000000
7fe00000 - 1

on both x86_64 and aarch64.

For ppc64, I believe there's a compiler bug:

7fa00000
7ff4000000000000 - 0
7ff4000000000000
7fe00000 - 536870912

convert float to double:
    1000074c:   60 00 01 c0     lfs     f0,96(r1)
    10000750:   68 00 01 d8     stfd    f0,104(r1)

convert double to float:
    100007a8:   68 00 01 c8     lfd     f0,104(r1)
    100007ac:   18 00 00 fc     frsp    f0,f0
    100007b0:   60 00 01 d0     stfs    f0,96(r1)

Floating point numbers are held in a "register" format that largely corresponds
to double-precision.  Thus the compiler believes that loading a
single-precision value and then storing it out again as a double is sufficient.
 However, as we can see above that does not consider SNaN.

There is no ppc "convert single to double" instruction, there is only a "round
to single precision" instruction -- frsp.  However, if we assume that the
single precision number is already properly rounded, then we can add an extra
frsp and it will not normally affect the value at all; it will only change the
contents for snan.

If I manually add the frsp insn to the code generated for the test case I get

7fa00000
7ffc000000000000 - 536870912
7ff4000000000000
7fe00000 - 536870912

exactly as we expect.  I'll file a bug vs gcc.


r~

On 04/19/2018 09:06 AM, Richard Henderson wrote:
> For ppc64, I believe there's a compiler bug:

Bah.  Apparently one must now use -fsignalling-nans.
With that option we do generate the conversion insn.


r~

On 19 April 2018 at 20:12, Richard Henderson
<richard.henderson@linaro.org> wrote:
> On 04/19/2018 09:06 AM, Richard Henderson wrote:
>> For ppc64, I believe there's a compiler bug:
>
> Bah.  Apparently one must now use -fsignalling-nans.
> With that option we do generate the conversion insn.

"This option is experimental", the gcc docs say :-)

thanks
-- PMM

Richard Henderson <richard.henderson@linaro.org> writes:

> On 04/17/2018 01:08 PM, Peter Maydell wrote:
>> On 18 April 2018 at 00:01, Peter Maydell <peter.maydell@linaro.org> wrote:
>>> I don't have the original IEEE754 spec to hand though;
>>> that may have left this unspecified.
>>
>> Having located a copy of 754-1985 I think that also is
>> clear enough that float-float conversion is an operation
>> that must quieten SNaN and raise Invalid.
>
> That does seem to match actual processor behaviour.
> The attached test case produces
>
> 7fa00000
> 7ffc000000000000 - 1
> 7ff4000000000000
> 7fe00000 - 1
>
> on both x86_64 and aarch64.
>
> For ppc64, I believe there's a compiler bug:
>
> 7fa00000
> 7ff4000000000000 - 0
> 7ff4000000000000
> 7fe00000 - 536870912
>
> convert float to double:
>     1000074c:   60 00 01 c0     lfs     f0,96(r1)
>     10000750:   68 00 01 d8     stfd    f0,104(r1)
>
> convert double to float:
>     100007a8:   68 00 01 c8     lfd     f0,104(r1)
>     100007ac:   18 00 00 fc     frsp    f0,f0
>     100007b0:   60 00 01 d0     stfs    f0,96(r1)
>
> Floating point numbers are held in a "register" format that largely corresponds
> to double-precision.  Thus the compiler believes that loading a
> single-precision value and then storing it out again as a double is sufficient.
>  However, as we can see above that does not consider SNaN.
>
> There is no ppc "convert single to double" instruction, there is only a "round
> to single precision" instruction -- frsp.  However, if we assume that the
> single precision number is already properly rounded, then we can add an extra
> frsp and it will not normally affect the value at all; it will only change the
> contents for snan.
>
> If I manually add the frsp insn to the code generated for the test case I get
>
> 7fa00000
> 7ffc000000000000 - 536870912
> 7ff4000000000000
> 7fe00000 - 536870912
>
> exactly as we expect.  I'll file a bug vs gcc.

It does seem to be floating point is a rabbit hole that everyone gets
something wrong if you look too closely!

--
Alex Bennée