summaryrefslogtreecommitdiff
path: root/test/regression
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-08-02 09:27:04 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-08-02 09:27:04 +0000
commitf7d64b71170e0694c5c4fb38ab7d1a23a4bd4c2a (patch)
treec1bb3c1893407207139b48e49970476318d8b093 /test/regression
parent4ee0544a157090ddd087b36109d292cd174bae7c (diff)
Add test for NaNs
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'test/regression')
-rw-r--r--test/regression/Makefile24
-rw-r--r--test/regression/NaNs.c75
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;
+}