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

3 files changed, 12 insertions, 55 deletions

diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 3be32e4..771243f 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -23,20 +23,15 @@ let builtins = {
     (* Integer arithmetic *)
     "__builtin_bswap",
       (TInt(IUInt, []), [TInt(IUInt, [])], false);
+    "__builtin_bswap32",
+      (TInt(IUInt, []), [TInt(IUInt, [])], false);
+    "__builtin_bswap16",
+      (TInt(IUShort, []), [TInt(IUShort, [])], false);
     "__builtin_cntlz",
       (TInt(IUInt, []), [TInt(IUInt, [])], false);
     (* Float arithmetic *)
     "__builtin_fsqrt",
-      (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
-    (* Memory accesses *)
-    "__builtin_read16_reversed",
-      (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
-    "__builtin_read32_reversed",
-      (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
-    "__builtin_write16_reversed",
-      (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
-    "__builtin_write32_reversed",
-      (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
+      (TFloat(FDouble, []), [TFloat(FDouble, [])], false)
   ]
 }
 
diff --git a/arm/Machregs.v b/arm/Machregs.v
index 4906eb0..50535f0 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -104,7 +104,9 @@ Definition destroyed_by_jumptable: list mreg :=
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil
-  | _ => R12 :: F6 :: nil
+  | EF_vstore Mfloat32 => F6 :: nil
+  | EF_vstore_global Mfloat32 _ _ => F6 :: nil
+  | _ => nil
   end.
 
 Definition destroyed_at_function_entry: list mreg :=
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 1bac715..fc7c987 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -336,28 +336,16 @@ let print_builtin_vstore_global oc chunk id ofs args =
   let n = print_builtin_vstore_common oc chunk (IR IR14 :: args) in
   fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n + 1
 
-(* Magic sequence for byte-swapping *)
-
-let print_bswap oc src tmp dst =
-  (* tmp <> src, tmp <> dst, but can have dst = src *)
-  (* src = A . B .C . D *)
-  fprintf oc "	eor	%a, %a, %a, ror #16\n" ireg tmp ireg src ireg src;
-  (* tmp = A^C . B^D . C^A . D^B *)
-  fprintf oc "	bic	%a, %a, #0x00FF0000\n" ireg tmp ireg tmp;
-  (* tmp = A^C . 000 . C^A . D^B *)
-  fprintf oc "	mov	%a, %a, ror #8\n" ireg dst ireg src;
-  (* dst = D . A . B . C *)
-  fprintf oc "	eor	%a, %a, %a, lsr #8\n" ireg dst ireg dst ireg tmp
-  (* dst = D . A^A^C . B . C^C^A = D . C . B . A *)
-
 (* Handling of compiler-inlined builtins *)
 
 let print_builtin_inline oc name args res =
   fprintf oc "%s begin %s\n" comment name;
   let n = match name, args, res with
   (* Integer arithmetic *)
-  | "__builtin_bswap", [IR a1], [IR res] ->
-      print_bswap oc a1 IR14 res; 4
+  | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
+      fprintf oc "	rev	%a, %a\n" ireg res ireg a1; 1
+  | "__builtin_bswap16", [IR a1], [IR res] ->
+      fprintf oc "	rev16	%a, %a\n" ireg res ireg a1; 1
   | "__builtin_cntlz", [IR a1], [IR res] ->
       fprintf oc "	clz	%a, %a\n" ireg res ireg a1; 1
   (* Float arithmetic *)
@@ -400,34 +388,6 @@ let print_builtin_inline oc name args res =
       end else begin
         fprintf oc "	umull   %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1
       end
-  (* Memory accesses *)
-  | "__builtin_read16_reversed", [IR a1], [IR res] ->
-      fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg a1;
-      fprintf oc "	mov	%a, %a, lsl #8\n" ireg IR14 ireg res;
-      fprintf oc "	and	%a, %a, #0xFF00\n" ireg IR14 ireg IR14;
-      fprintf oc "	orr	%a, %a, %a, lsr #8\n" ireg res ireg IR14 ireg res; 4
-  | "__builtin_read32_reversed", [IR a1], [IR res] ->
-      fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg a1;
-      print_bswap oc res IR14 res; 5
-  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
-      fprintf oc "	mov	%a, %a, lsr #8\n" ireg IR14 ireg a2;
-      fprintf oc "	and	%a, %a, #0xFF\n" ireg IR14 ireg IR14;
-      fprintf oc "	orr	%a, %a, %a, lsl #8\n" ireg IR14 ireg IR14 ireg a2;
-      fprintf oc "	strh	%a, [%a, #0]\n" ireg IR14 ireg a1; 4
-  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
-      if a1 <> IR12 then begin
-        print_bswap oc a2 IR14 IR12;
-        fprintf oc "	str	%a, [%a, #0]\n" ireg IR12 ireg a1; 5
-      end else begin
-        fprintf oc "	mov	%a, %a, lsr #24\n" ireg IR14 ireg a2;
-        fprintf oc "	str     %a, [%a, #0]\n" ireg IR14 ireg a1;
-        fprintf oc "	mov	%a, %a, lsr #16\n" ireg IR14 ireg a2;
-        fprintf oc "	str     %a, [%a, #1]\n" ireg IR14 ireg a1;
-        fprintf oc "	mov	%a, %a, lsr #8\n" ireg IR14 ireg a2;
-        fprintf oc "	str     %a, [%a, #2]\n" ireg IR14 ireg a1;
-        fprintf oc "	str     %a, [%a, #3]\n" ireg IR14 ireg a1;
-        7
-      end
   (* Catch-all *)
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)