Add test for NaNs

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 95 insertions, 4 deletions

diff --git a/test/regression/Makefile b/test/regression/Makefile
index b0663b1..a37f901 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -17,7 +17,12 @@ TESTS=int32 int64 floats floats-basics \
 
 TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
   bitfields5 bitfields6 bitfields7 bitfields8 \
-  builtins-$(ARCH) packedstruct1 packedstruct2 \
+  builtins-$(ARCH) packedstruct1 packedstruct2
+
+# Can run, both in compiled mode and in interpreter mode,
+# but produce processor-dependent results, so no reference output in Results
+
+TESTS_DIFF=NaNs
 
 # Other tests: should compile to .s without errors (but expect warnings)
 
@@ -28,9 +33,9 @@ EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 init1 \
 # Test known to fail
 FAILURES=funct1 varargs1
 
-all: $(TESTS:%=%.compcert) $(TESTS_COMP:%=%.compcert) $(EXTRAS:%=%.s)
+all: $(TESTS:%=%.compcert) $(TESTS_COMP:%=%.compcert) $(TESTS_DIFF:%=%.compcert) $(EXTRAS:%=%.s)
 
-all_s: $(TESTS:%=%.s) $(TESTS_COMP:%=%.s) $(EXTRAS:%=%.s)
+all_s: $(TESTS:%=%.s) $(TESTS_COMP:%=%.s) $(TESTS_DIFF:%=%.s) $(EXTRAS:%=%.s)
 
 %.compcert: %.c $(CCOMP)
 	$(CCOMP) $(CCOMPFLAGS) -o $*.compcert $*.c $(LIBS)
@@ -48,7 +53,7 @@ test:
            then echo "$$i: passed"; \
            else echo "$$i: FAILED"; \
 	   fi; \
-         done;
+         done
 	@for i in $(TESTS); do \
            if $(CCOMP) -fall -interp -quiet $$i.c > _cinterp.log; then \
              if cmp -s _cinterp.log Results/$$i; \
@@ -60,5 +65,16 @@ test:
            fi; \
            rm -f _cinterp.log; \
          done
+	@for i in $(TESTS_DIFF); do \
+           if $(CCOMP) -fall -interp -quiet $$i.c > _cinterp.log; then \
+             if ./$$i.compcert | cmp -s _cinterp.log -; \
+             then echo "$$i: compiler and interpreter agree"; \
+             else echo "$$i: compiler and interpreter DISAGREE"; \
+             fi; \
+           else \
+             echo "$$i: interpreter undefined behavior"; \
+           fi; \
+           rm -f _cinterp.log; \
+         done
 
 bench:
diff --git a/test/regression/NaNs.c b/test/regression/NaNs.c
new file mode 100644
index 0000000..45f1e7f
--- /dev/null
+++ b/test/regression/NaNs.c
@@ -0,0 +1,75 @@
+/* Validating the semantics of NaNs. 
+   This tests produces output that depend on the processor.
+   However, the same output must be obtained from compiled code
+   and from the reference interpreter. */
+
+#include<stdio.h>
+
+typedef unsigned long long u64;
+typedef unsigned int u32;
+
+inline u64 bits_of_double(double d)
+{
+  union { double d; u64 i; } u;
+  u.d = d; return u.i;
+}
+
+inline double double_of_bits(u64 i)
+{
+  union { double d; u64 i; } u;
+  u.i = i; return u.d; 
+}
+
+inline u32 bits_of_single(float f)
+{
+  union { float f; u32 i; } u;
+  u.f = f; return u.i;
+}
+
+inline float single_of_bits(u32 i)
+{
+  union { float f; u32 i; } u;
+  u.i = i; return u.f;
+}
+
+volatile double val[8];
+
+char * valname[8] = {
+  "+0", "-0", "+inf", "-inf",
+  "snan(5)", "qnan(6)", "snan(-9)", "qnan(-1)"
+};
+
+int main()
+{
+  int i, j;
+
+  val[0] = 0.0;
+  val[1] = - val[0];
+  val[2] = double_of_bits(0x7FF0000000000000);
+  val[3] = - val[2];
+
+  val[4] = double_of_bits(0x7FF0000000000005);
+  val[5] = double_of_bits(0x7FF8000000000006);
+  val[6] = double_of_bits(0xFFF0000000000009);
+  val[7] = double_of_bits(0xFFF8000000000001);
+
+  for (i = 0; i < 8; i++) {
+    printf("opp(%s) = 0x%016llx\n", valname[i], bits_of_double(- val[i]));
+    printf("single(%s) = 0x%08x\n", valname[i], bits_of_single((float)(val[i])));
+#if 0
+    /* The reference interpreter doesn't support __builtin_fabs */
+    printf("abs(%s) = 0x%016llx\n", valname[i], bits_of_double(__builtin_fabs(val[i])));
+#endif
+    for (j = 0; j < 8; j++) {
+      printf("%s + %s = 0x%016llx\n",
+             valname[i], valname[j], bits_of_double(val[i] + val[j]));
+      printf("%s - %s = 0x%016llx\n",
+             valname[i], valname[j], bits_of_double(val[i] - val[j]));
+      printf("%s * %s = 0x%016llx\n",
+             valname[i], valname[j], bits_of_double(val[i] * val[j]));
+      printf("%s / %s = 0x%016llx\n",
+             valname[i], valname[j], bits_of_double(val[i] / val[j]));
+    }
+  }
+  return 0;
+}