ARM: added reversed load/store builtins + bswap builtin (to be tested)

IA32: added bswap builtin
Updated Changelog


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

5 files changed, 84 insertions, 7 deletions

diff --git a/Changelog b/Changelog
index 56fcb61..a2677f7 100644
--- a/Changelog
+++ b/Changelog
@@ -1,7 +1,14 @@
-- Fixed two omissions in the semantics of CompCert C (reported by Brian Campbell):
-  . Functions calls through a function pointer had undefined semantics.
-  . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different
-    types were missing a cast to their common type.
+Release 1.9, 2011-xx-xx
+=======================
+
+- The reduction semantics of CompCert C was made executable and turned
+  into a reference interpreter for CompCert C, enabling animation of
+  the semantics.  (Thanks to Brian Campbell for suggesting this approach.)
+  Usage is:  ccomp -interp [options] source.c
+  Options include:
+    -trace      to print a detailed trace of reduction steps
+    -random     to randomize execution order
+    -all        to explore all possible execution orders in parallel
 
 - Revised and strengthened the top-level statements of semantic preservation.
   In particular, we now show:
@@ -11,6 +18,11 @@
     the compiled code performs at least these I/O before continuing
     with an arbitrary behavior.
 
+- Fixed two omissions in the semantics of CompCert C (reported by Brian Campbell):
+  . Functions calls through a function pointer had undefined semantics.
+  . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different
+    types were missing a cast to their common type.
+
 - Revised handling of annotation statements.  Now they come in two forms:
     1. __builtin_annot("format", x1, ..., xN)
        (arbitrarily many arguments; no code generated, even if some
@@ -22,6 +34,13 @@
 - Related clean-ups in the handling of external functions and 
   compiler built-ins.
 
+- ARM code generator was ported to the new ABI (EABI in ARM parlance,
+  armel in Debian parlance), using VFD instructions for floating-point.
+  (Successfully tested on a Trimslice platform running Ubuntu 11.04.)
+
+- IA32 code generator: added -fno-sse option to prevent generation of
+  SSE instructions for memory copy operations.
+
 	
 Release 1.8.2, 2011-05-24
 =========================
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 2e49388..dc4ca60 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -18,10 +18,24 @@
 open Cparser
 open C
 
-(* No ARM builtins for the moment *)
-
 let builtins = {
   Builtins.typedefs = [];
-  Builtins.functions = []
+  Builtins.functions = [
+    (* Integer arithmetic *)
+    "__builtin_bswap",
+      (TInt(IUInt, []), [TInt(IUInt, [])], false);
+    (* Float arithmetic *)
+    "__builtin_fsqrt",
+      (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/arm/PrintAsm.ml b/arm/PrintAsm.ml
index f1beded..c50acba 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -370,14 +370,50 @@ let print_builtin_vstore oc chunk args =
     end in
   fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n
 
+(* Magic sequence for byte-swapping *)
+
+let print_bswap oc src dst tmp =
+  (* 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
   (* Float arithmetic *)
   | "__builtin_fabs", [FR a1], FR res ->
       fprintf oc "	fabsd	%a, %a\n" freg res freg a1; 1
+  | "__builtin_fsqrt", [FR a1], FR res ->
+      fprintf oc "	fsqrtd	%a, %a\n" freg res freg a1; 1
+  (* Memory accesses *)
+  | "__builtin_read_int16_reversed", [IR a1], IR res ->
+      fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg a1;
+      fprintf oc "	mov	%a, %a, lsr #8\n" ireg IR14 ireg res;
+      fprintf oc "	orr	%a, %a, %a, lsl #8\n" ireg res ireg IR14 ireg res; 3
+  | "__builtin_read_int32_reversed", [IR a1], IR res ->
+      fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg a1;
+      print_bswap oc res IR14 res; 5
+  | "__builtin_write_int16_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_write_int32_reversed", [IR a1; IR a2], _ ->
+      let tmp = if a1 = IR10 then IR12 else IR10 in
+      print_bswap oc a2 IR14 tmp;
+      fprintf oc "	str	%a, [%a, #0]\n" ireg tmp ireg a1; 5
   (* Catch-all *)
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index 9cd31da..3b94744 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -21,6 +21,9 @@ open C
 let builtins = {
   Builtins.typedefs = [];
   Builtins.functions = [
+    (* Integer arithmetic *)
+    "__builtin_bswap",
+      (TInt(IUInt, []), [TInt(IUInt, [])], false);
     (* Float arithmetic *)
     "__builtin_fsqrt",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 842957f..6f02a8a 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -412,6 +412,11 @@ let print_builtin_inline oc name args res =
         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
+  (* Integer arithmetic *)
+  | "__builtin_bswap", [IR a1], IR res ->
+      if a1 <> res then
+        fprintf oc "	movl	%a, %a\n" ireg a1 ireg res;
+      fprintf oc "	bswap	%a\n" ireg res
   (* Float arithmetic *)
   | "__builtin_fabs", [FR a1], FR res ->
       need_masks := true;