bswap builtins: give semantics to them, support bswap64 on all targets

* Added semantic for byte swap builtins

The `__builtin_bswap`, `__builtin_bswap16`,  `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics.

The semantics  is given in terms of the decode/encode functions used for the memory model.

* Added bswap64 expansion to PowerPC 32 bits.

* Added bswap64 expansion for ARM.

6 files changed, 51 insertions, 7 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index d9424d11..a4ec0c5d 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -304,6 +304,11 @@ let expand_builtin_va_start r =
 let expand_builtin_inline name args res =
   match name, args, res with
   (* Integer arithmetic *)
+  | "__builtin_bswap64" , [BA_splitlong(BA(IR ah), BA(IR al))],
+                          BR_splitlong(BR(IR rh), BR(IR rl)) ->
+     expand_int64_arith (rl = al) rl (fun rl ->
+        emit (Prev (rl, ah));
+        emit (Prev (rh, al)))
   | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
      emit (Prev (res, a1))
   | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2e6bbe67..c1dfa9f4 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -161,7 +161,9 @@ let builtins_generic = {
       @
     [
     (* Integer arithmetic *)
-    "__builtin_bswap",
+    "__builtin_bswap64",
+    (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
+      "__builtin_bswap",
     (TInt(IUInt, []), [TInt(IUInt, [])], false);
     "__builtin_bswap32",
       (TInt(IUInt, []), [TInt(IUInt, [])], false);
diff --git a/common/Builtins0.v b/common/Builtins0.v
index c6a299d9..b78006dd 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -16,7 +16,7 @@
 (** Associating semantics to built-in functions *)
 
 Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+Require Import AST Integers Floats Values Memdata.
 
 (** This module provides definitions and mechanisms to associate semantics
   with names of built-in functions.
@@ -337,6 +337,9 @@ Inductive standard_builtin : Type :=
   | BI_addl
   | BI_subl
   | BI_mull
+  | BI_i16_bswap
+  | BI_i32_bswap
+  | BI_i64_bswap
   | BI_i64_umulh
   | BI_i64_smulh
   | BI_i64_sdiv
@@ -366,6 +369,10 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
  :: ("__builtin_addl", BI_addl)
  :: ("__builtin_subl", BI_subl)
  :: ("__builtin_mull", BI_mull)
+ :: ("__builtin_bswap16", BI_i16_bswap)
+ :: ("__builtin_bswap", BI_i32_bswap)
+ :: ("__builtin_bswap32", BI_i32_bswap)
+ :: ("__builtin_bswap64", BI_i64_bswap)
  :: ("__compcert_i64_umulh", BI_i64_umulh)
  :: ("__compcert_i64_smulh", BI_i64_smulh)
  :: ("__compcert_i64_sdiv", BI_i64_sdiv)
@@ -396,6 +403,12 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
       mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default
   | BI_mull =>
       mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
+  | BI_i32_bswap =>
+      mksignature (Tint :: nil) (Some Tint) cc_default
+  | BI_i64_bswap =>
+      mksignature (Tlong :: nil) (Some Tlong) cc_default
+  | BI_i16_bswap =>
+      mksignature (Tint :: nil) (Some Tint) cc_default
   | BI_i64_shl  | BI_i64_shr | BI_i64_sar =>
       mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default
   | BI_i64_dtos | BI_i64_dtou =>
@@ -420,6 +433,15 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (pro
   | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ 
   | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _
   | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _
+  | BI_i16_bswap =>
+    mkbuiltin_n1t Tint Tint
+                  (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n)))))
+  | BI_i32_bswap =>
+    mkbuiltin_n1t Tint Tint
+                  (fun n => Int.repr (decode_int (List.rev (encode_int 4%nat (Int.unsigned n)))))
+  | BI_i64_bswap =>
+    mkbuiltin_n1t Tlong Tlong
+                  (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n)))))
   | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
   | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
   | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 415b6651..5ca4c611 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -554,6 +554,26 @@ let expand_builtin_inline name args res =
       emit (Plabel lbl2)
   | "__builtin_cmpb",  [BA(IR a1); BA(IR a2)], BR(IR res) ->
       emit (Pcmpb (res,a1,a2))
+  |  "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))],
+                          BR_splitlong(BR(IR rh), BR(IR rl))->
+      assert (not Archi.ppc64);
+      emit (Pstwu(ah, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Pstwu(al, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Plwbrx(rh, GPR0, GPR1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8);
+      emit (Plwbrx(rl, GPR0, GPR1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8)
+  |  "__builtin_bswap64", [BA(IR a1)], BR(IR res) ->
+      assert (Archi.ppc64);
+      emit (Pstdu(a1, Cint _m8, GPR1));
+      emit (Pcfi_adjust _8);
+      emit (Pldbrx(res, GPR0, GPR1));
+      emit (Paddi(GPR1, GPR1, Cint _8));
+      emit (Pcfi_adjust _m8)
   | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
       emit (Pstwu(a1, Cint _m8, GPR1));
       emit (Pcfi_adjust _8);
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index edaf586d..a2087cb7 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -25,9 +25,6 @@ let builtins = {
     (* Synchronization *)
     "__builtin_fence",
       (TVoid [], [], false);
-    (* Integer arithmetic *)
-    "__builtin_bswap64",
-      (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
     (* Float arithmetic *)
     "__builtin_fmadd",
       (TFloat(FDouble, []),
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index 6fb8b697..f4f40a31 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -31,8 +31,6 @@ let builtins = {
   ];
   builtin_functions = [
     (* Integer arithmetic *)
-    "__builtin_bswap64",
-      (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
     "__builtin_clz",
       (TInt(IInt, []), [TInt(IUInt, [])], false);
     "__builtin_clzl",