Created attachment 48601 [details]
Reduced testcase of the fmaxf issue

I've been creating some floating point benchmarks for SMT-LIB. I have noticed that gcc (or something else) does not produce the same result in some specific examples. I am on amd64 Debian, but I've also reproduced this on a recent amd64 Ubuntu. Below is a reduced test-case showing this:

#include <stdio.h>
#include <stdint.h>
#include <math.h>
#include <string.h>

int main()
{
  uint32_t bv = 0x7FACBA7E;
  // (0 11111111 01011001011101001111110)

  float a, b;
  a = -INFINITY;
  memcpy(&b, &bv, 4);

  printf("max(%f, %f) = %f\n", a, b, fmaxf(a, b));

  b = NAN;
  printf("max(%f, %f) = %f\n", a, b, fmaxf(a, b));
}

When compiling and running this program you get:

max(-inf, nan) = nan
max(-inf, nan) = -inf

I've tried with both:
  gcc bug.c -lm
and
  gcc -std=c99 -frounding-math -fsignaling-nans -ffp-contract=off -mfma -mno-fma4 -pedantic -Wall -W -msse2 -mfpmath=sse -fstrict-aliasing bug.c -lm


However, IEEE-754 says that max(something not NaN, NaN) should get you the
thing that is not NaN. With the built-in constant it works, but with my hand-crafted NaN it does not.

I've also tried replacing fmaxf by __builtin_fmaxf, with no success.


I also realise this likely may not be a gcc bug, but something deeper down in libm or elsewhere. I do note that with clang-9 this works though. However I
suspect you guys will know where exactly this report needs to go to.