Add __builtin_bswap16 and __builtin_bswap32 to all ports.

Remove __builtin_{read,write}_reversed from IA32 and ARM ports.
Machregs: tighten destroyed_by_builtin
Packedstructs: use bswap if read/write-reversed not available.


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

5 files changed, 56 insertions, 26 deletions

diff --git a/test/regression/Makefile b/test/regression/Makefile
index 454bcef..643fba4 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -17,7 +17,7 @@ TESTS=int32 int64 floats floats-basics \
 
 TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
   bitfields5 bitfields6 bitfields7 bitfields8 \
-  packedstruct1 packedstruct2 \
+  builtins-$(ARCH) packedstruct1 packedstruct2 \
 
 # Other tests: should compile to .s without errors (but expect warnings)
 
diff --git a/test/regression/Results/builtins-ia32 b/test/regression/Results/builtins-ia32
new file mode 100644
index 0000000..52d6daf
--- /dev/null
+++ b/test/regression/Results/builtins-ia32
@@ -0,0 +1,5 @@
+bswap(12345678) = 78563412
+bswap16(1234) = 3412
+fsqrt(3.141590) = 1.772453
+fmin(3.141590, 2.718000) = 2.718000
+fmax(3.141590, 2.718000) = 3.141590
diff --git a/test/regression/builtins-arm.c b/test/regression/builtins-arm.c
new file mode 100644
index 0000000..41ea88b
--- /dev/null
+++ b/test/regression/builtins-arm.c
@@ -0,0 +1,23 @@
+/* Fun with builtins */
+
+#include <stdio.h>
+
+int main(int argc, char ** argv)
+{
+  unsigned int x = 0x12345678;
+  unsigned int y = 0xDEADBEEF;
+  double a = 3.14159;
+  unsigned short s = 0x1234;
+
+  printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
+  printf("bswap16(%x) = %x\n", s, __builtin_bswap16(s));
+  printf("cntlz(%x) = %d\n", x, __builtin_cntlz(x));
+  printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
+  
+  return 0;
+}
+
+
+  
+
+
diff --git a/test/regression/builtins-ia32.c b/test/regression/builtins-ia32.c
new file mode 100644
index 0000000..43e4566
--- /dev/null
+++ b/test/regression/builtins-ia32.c
@@ -0,0 +1,25 @@
+/* Fun with builtin functions */
+
+#include <stdio.h>
+
+int main(int argc, char ** argv)
+{
+  unsigned int x = 0x12345678;
+  double a = 3.14159;
+  double b = 2.718;
+  unsigned short s = 0x1234;
+
+  printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
+  printf("bswap16(%x) = %x\n", s, __builtin_bswap16(s));
+
+  printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
+  printf("fmin(%f, %f) = %f\n", a, b, __builtin_fmin(a, b));
+  printf("fmax(%f, %f) = %f\n", a, b, __builtin_fmax(a, b));
+
+  return 0;
+}
+
+
+  
+
+
diff --git a/test/regression/builtins.c b/test/regression/builtins-powerpc.c
index f548fd8..9f0d410 100644
--- a/test/regression/builtins.c
+++ b/test/regression/builtins-powerpc.c
@@ -4,19 +4,18 @@
 
 int main(int argc, char ** argv)
 {
-  int x = 0x12345678;
+  unsigned int x = 0x12345678;
   unsigned int y = 0xDEADBEEF;
   double a = 3.14159;
   double b = 2.718;
   double c = 1.414;
   unsigned short s = 0x1234;
 
-#if defined(__PPC__) || defined(__ppc__)
-
   printf("mulhw(%x, %x) = %x\n", x, y, __builtin_mulhw(x, y));
   printf("mulhwu(%x, %x) = %x\n", x, y, __builtin_mulhwu(x, y));
   printf("cntlz(%x) = %d\n", x, __builtin_cntlz(x));
   printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
+  printf("bswap16(%x) = %x\n", s, __builtin_bswap16(s));
 
   printf("fmadd(%f, %f, %f) = %f\n", a, b, c, __builtin_fmadd(a, b, c));
   printf("fmsub(%f, %f, %f) = %f\n", a, b, c, __builtin_fmsub(a, b, c));
@@ -33,28 +32,6 @@ int main(int argc, char ** argv)
   __builtin_eieio();
   __builtin_sync();
   __builtin_isync();
-
-#endif
-
-#ifdef __arm__
-
-  printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
-  printf("cntlz(%x) = %d\n", x, __builtin_cntlz(x));
-
-  printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
-  
-#endif
-
-#ifdef __i386__
-
-  printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
-
-  printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
-  printf("fmin(%f, %f) = %f\n", a, b, __builtin_fmin(a, b));
-  printf("fmax(%f, %f) = %f\n", a, b, __builtin_fmax(a, b));
-
-#endif
-
   printf ("read_16_rev = %x\n", __builtin_read16_reversed(&s));
   printf ("read_32_rev = %x\n", __builtin_read32_reversed(&y));
   __builtin_write16_reversed(&s, 0x789A);