We also hit this regression when testing CompCert for e5500 with qemu 3.1.0.
The minimal example
> #include <stdio.h>
> #include <math.h>
>
> union C { float f; unsigned long l; };
> int main (void) {
> union C c;
> c.f = NAN;
> printf("Float: %f\n Hex: 0x%x\n", c.f, c.l);
> printf("The above float is %s NAN\n", c.f == NAN ? "==" : "!=");
> return 0;
> }
does not exhibit the error with GCC 6.3.0, since that statically optimizes the c.f == NAN to always be false. But CompCert doesn't do this optimization and thus triggers the regression in the float compare.
With qemu 3.0.0 the example outputs (whether built with compcert or gcc):
> Float: nan
> Hex: 0x7fc00000
> The above float is != NAN
The example works well with qemu 3.0.0 and we stumbled over this with qemu 3.1.0; both build from the released source tarballs. My native system is a x86_64 GNU/Linux (openSUSE Tumbleweed with Kernel 4.20.13-1-default).
Output with qemu 3.1.0 and built with GCC:
> $ ./qemu-ppc64abi32-3.1.0 bug25310.gcc.elf
> Float: 510423550381407695195061911147652317184.000000
> Hex: 0x7fc00000
> The above float is != NAN
qemu 3.1.0 and example built with CompCert:
> $ ./qemu-ppc64abi32-3.1.0 bug25310.ccomp.elf
> Float: 510423550381407695195061911147652317184.000000
> Hex: 0x7fc00000
> The above float is == NAN
We also hit this regression when testing CompCert for e5500 with qemu 3.1.0.
The minimal example
> #include <stdio.h>
> #include <math.h>
>
> union C { float f; unsigned long l; };
> int main (void) {
> union C c;
> c.f = NAN;
> printf("Float: %f\n Hex: 0x%x\n", c.f, c.l);
> printf("The above float is %s NAN\n", c.f == NAN ? "==" : "!=");
> return 0;
> }
does not exhibit the error with GCC 6.3.0, since that statically optimizes the c.f == NAN to always be false. But CompCert doesn't do this optimization and thus triggers the regression in the float compare.
With qemu 3.0.0 the example outputs (whether built with compcert or gcc):
> Float: nan
> Hex: 0x7fc00000
> The above float is != NAN
The example works well with qemu 3.0.0 and we stumbled over this with qemu 3.1.0; both build from the released source tarballs. My native system is a x86_64 GNU/Linux (openSUSE Tumbleweed with Kernel 4.20.13-1-default).
Output with qemu 3.1.0 and built with GCC: ppc64abi32- 3.1.0 bug25310.gcc.elf 695195061911147 652317184. 000000
> $ ./qemu-
> Float: 510423550381407
> Hex: 0x7fc00000
> The above float is != NAN
qemu 3.1.0 and example built with CompCert: ppc64abi32- 3.1.0 bug25310.ccomp.elf 695195061911147 652317184. 000000
> $ ./qemu-
> Float: 510423550381407
> Hex: 0x7fc00000
> The above float is == NAN
I attached example binaries (statically built): internal_ ppc/bin/ ccomp --version 02/11/1924 internal_ ppc/bin/ ccomp -target e5500-linux -g -static bug25310.c -o bug25310.ccomp.elf internal_ ppc/gcc/ bin/powerpc- unknown- linux-gnu- gcc --version unknown- linux-gnu- gcc (crosstool-NG crosstool- ng-1.23. 0) 6.3.0 internal_ ppc/gcc/ bin/powerpc- unknown- linux-gnu- gcc bug25310.c -g -static -O0 -o bug25310.gcc.elf -mcpu=e5500
> $ ../../compcert_
> The CompCert C verified compiler, Release: 18.10i, Build: 4503984, Tag: auto/2019/
> $ ../../compcert_
>
> $ ../../compcert_
> powerpc-
> $ ../../compcert_