Nicer printing of annotations.

ia32: support builtins for reversed reads and writes (facilitates testing).


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

5 files changed, 45 insertions, 19 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index ed6d3f3..4f5d1cd 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -319,10 +319,6 @@ let print_builtin_inlined oc name args res =
       let sz = int_of_string (Str.matched_group 3 name) in
       let al = try int_of_string (Str.matched_group 2 name) with Not_found -> 1 in
       print_builtin_memcpy oc sz al dst src
-  (* Annotations *)
-  | name, args, res when Str.string_match re_builtin_annotation name 0 ->
-      let annot = Str.matched_group 1 name in
-      print_annotation oc annot args res
   (* Catch-all *)
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
@@ -533,7 +529,9 @@ let print_instruction oc = function
       2 + List.length tbl
   | Pbuiltin(ef, args, res) ->
       let name = extern_atom ef.ef_id in
-      print_builtin_inlined oc name args res
+      if Str.string_match re_builtin_annotation name 0
+      then print_annotation oc (Str.matched_group 1 name) args res
+      else print_builtin_inlined oc name args res
 
 let no_fallthrough = function
   | Pb _ -> true
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index 14a2f10..9cd31da 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -28,5 +28,14 @@ let builtins = {
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmin",
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+    (* Memory accesses *)
+    "__builtin_read_int16_reversed",
+      (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
+    "__builtin_read_int32_reversed",
+      (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
+    "__builtin_write_int16_reversed",
+      (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
+    "__builtin_write_int32_reversed",
+      (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
   ]
 }
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 35195b6..9facf85 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -85,6 +85,10 @@ let int8_reg_name = function
   | EAX -> "%al"  | EBX -> "%bl"  | ECX -> "%cl"  | EDX -> "%dl"
   | _ -> assert false
 
+let high_int8_reg_name = function
+  | EAX -> "%ah"  | EBX -> "%bh"  | ECX -> "%ch"  | EDX -> "%dh"
+  | _ -> assert false
+
 let int16_reg_name = function
   | EAX -> "%ax"  | EBX -> "%bx"  | ECX -> "%cx"  | EDX -> "%dx"
   | ESI -> "%si"  | EDI -> "%di"  | EBP -> "%bp"  | ESP -> "%sp"
@@ -95,6 +99,7 @@ let float_reg_name = function
 
 let ireg oc r = output_string oc (int_reg_name r)
 let ireg8 oc r = output_string oc (int8_reg_name r)
+let high_ireg8 oc r = output_string oc (high_int8_reg_name r)
 let ireg16 oc r = output_string oc (int16_reg_name r)
 let freg oc r = output_string oc (float_reg_name r)
 
@@ -327,6 +332,28 @@ let print_builtin_inlined oc name args res =
       fprintf oc "	movss	%%xmm7, 0(%a)\n" ireg addr
   | "__builtin_volatile_write_float64", [IR addr; FR src], _ ->
       fprintf oc "	movsd	%a, 0(%a)\n" freg src ireg addr
+  (* Memory accesses *)
+  | "__builtin_read_int16_reversed", [IR a1], IR res ->
+      let tmp = if Asmgen.low_ireg res then res else ECX in
+      fprintf oc "	movzwl	0(%a), %a\n" ireg a1 ireg tmp;
+      fprintf oc "	xchg	%a, %a\n" ireg8 tmp high_ireg8 tmp;
+      if tmp <> res then
+        fprintf oc "	movl	%a, %a\n" ireg tmp ireg res
+  | "__builtin_read_int32_reversed", [IR a1], IR res ->
+      fprintf oc "	movl	0(%a), %a\n" ireg a1 ireg res;
+      fprintf oc "	bswap	%a\n" ireg res
+  | "__builtin_write_int16_reversed", [IR a1; IR a2], _ ->
+      let tmp = if a1 = ECX then EDX else ECX in
+      if a2 <> tmp then
+        fprintf oc "	movl	%a, %a\n" ireg a2 ireg tmp;
+      fprintf oc "	xchg	%a, %a\n" ireg8 tmp high_ireg8 tmp;
+      fprintf oc "	movw	%a, 0(%a)\n" ireg16 tmp ireg a1
+  | "__builtin_write_int32_reversed", [IR a1; IR a2], _ ->
+      let tmp = if a1 = ECX then EDX else ECX in
+      if a2 <> tmp then
+        fprintf oc "	movl	%a, %a\n" ireg a2 ireg tmp;
+      fprintf oc "	bswap	%a\n" ireg tmp;
+      fprintf oc "	movl	%a, 0(%a)\n" ireg tmp ireg a1
   (* Float arithmetic *)
   | "__builtin_fabs", [FR a1], FR res ->
       need_masks := true;
@@ -357,10 +384,6 @@ let print_builtin_inlined oc name args res =
   | name, [IR dst; IR src], _ when Str.string_match re_builtin_memcpy name 0 ->
       let sz = int_of_string (Str.matched_group 3 name) in
       print_builtin_memcpy oc sz dst src
-  (* Annotations *)
-  | name, args, res when Str.string_match re_builtin_annotation name 0 ->
-      let annot = Str.matched_group 1 name in
-      print_annotation oc annot args res
   (* Catch-all *)  
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
@@ -633,7 +656,9 @@ let print_instruction oc = function
       fprintf oc "	addl	$%ld, %%esp\n" sz
   | Pbuiltin(ef, args, res) ->
       let name = extern_atom ef.ef_id in
-      print_builtin_inlined oc name args res
+      if Str.string_match re_builtin_annotation name 0
+      then print_annotation oc (Str.matched_group 1 name) args res
+      else print_builtin_inlined oc name args res
 
 let print_literal oc (lbl, n) =
   fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 56e3c36..ef53411 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -412,10 +412,6 @@ let print_builtin_inlined oc name args res =
       let sz = int_of_string (Str.matched_group 3 name) in
       let al = try int_of_string (Str.matched_group 2 name) with Not_found -> 1 in
       print_builtin_memcpy oc sz al dst src
-  (* Annotations *)
-  | name, args, res when Str.string_match re_builtin_annotation name 0 ->
-      let annot = Str.matched_group 1 name in
-      print_annotation oc annot args res
   (* Catch-all *)
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
@@ -712,7 +708,9 @@ let print_instruction oc = function
       fprintf oc "%a:\n" label (transl_label lbl)
   | Pbuiltin(ef, args, res) ->
       let name = extern_atom ef.ef_id in
-      print_builtin_inlined oc name args res
+      if Str.string_match re_builtin_annotation name 0
+      then print_annotation oc (Str.matched_group 1 name) args res
+      else print_builtin_inlined oc name args res
 
 let print_literal oc (lbl, n) =
   let nlo = Int64.to_int32 n
diff --git a/test/regression/packedstruct1.c b/test/regression/packedstruct1.c
index 01f6b46..1bde780 100644
--- a/test/regression/packedstruct1.c
+++ b/test/regression/packedstruct1.c
@@ -42,11 +42,7 @@ void test2(void)
 
 /* Now with byte-swapped fields */
 
-#if defined(__COMPCERT__) && defined(_ARCH_PPC)
 #pragma pack(1,1,1)
-#else
-#pragma pack(1,1,0)
-#endif
 
 struct s3 {
   unsigned char x;