gcc strength-reduces floating-point expressions such as x * 1.0 into the identity function. This is correct if x is a finite or infinite value, but if x is a signaling NaN, x * 1.0 will be a "quietified" version of it. Thus, the outcomes differ depending on whether this strength-reduction has been applied.

I was wondering whether this optimization, which changes observable behavior of the program (the NaN payload is changed), is allowed. Annex F of the C standard says that the behavior of signaling NaN is unspecified, but it's unclear to me if this allows replacing a value by a different one.

This is observable by executing the following program depending on the EXTERN_MUL macro:

#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>

#ifdef __COMPCERT__
#define float_of_bits(x) __builtin_float_of_bits(x)
#define bits_of_float(x) __builtin_bits_of_float(x)
#else
union float_bits {
  float f;
  uint32_t i32;
};

float float_of_bits(uint32_t x) {
  union float_bits u;
  u.i32 = x;
  return u.f;
}
uint32_t bits_of_float(float x) {
  union float_bits u;
  u.f = x;
  return u.i32;
}
#endif

extern float mul(float, float);

int main() {
  float s = float_of_bits(UINT32_C(0xFF8FFFFF));
#ifdef EXTERN_MUL
  float q = mul(s, 1.0f);
#else
  float q = s * 1.0f;
#endif
  uint32_t s1 = bits_of_float(s);
  uint32_t q1 = bits_of_float(q);
  printf("%d\t%" PRIx32 "\t%" PRIx32 "\n", s1 == q1, s1, q1);
  return 0;
}

linked with

float mul(float x, float y) { return x*y; }

(two separate modules to prevent function inlining).