All targets: add __builtin_membar

ARM: add __builtin_dsb __builtin_isb


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

5 files changed, 53 insertions, 29 deletions

diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index b9b54e4..4446ab2 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -43,6 +43,11 @@ let builtins = {
       (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
     "__builtin_write32_reversed",
       (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
+    (* Synchronization *)
+    "__builtin_dsb",
+      (TVoid [], [], false);
+    "__builtin_isb",
+      (TVoid [], [], false)
   ]
 }
 
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index bb738a1..7dd7e48 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -515,6 +515,21 @@ let print_builtin_va_start oc r =
   fprintf oc "	str	r14, [%a, #0]\n" ireg r;
   n + 1
 
+(* Auxiliary for 64-bit integer arithmetic built-ins.  They expand to
+   two instructions, one computing the low 32 bits of the result,
+   followed by another computing the high 32 bits.  In cases where
+   the first instruction would overwrite arguments to the second
+   instruction, we must go through IR14 to hold the low 32 bits of the result.
+*)
+
+let print_int64_arith oc conflict rl fn =
+  if conflict then begin
+    let n = fn IR14 in
+    fprintf oc "	mov%t	%a, %a\n" thumbS ireg rl ireg IR14;
+    n + 1
+  end else
+    fn rl
+
 (* Handling of compiler-inlined builtins *)
 
 let print_builtin_inline oc name args res =
@@ -534,38 +549,25 @@ let print_builtin_inline oc name args res =
       fprintf oc "	vsqrt.f64 %a, %a\n" freg res freg a1; 1
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
-        fprintf oc "	rsbs	%a, %a, #0\n"
-                ireg (if rl = ah then IR14 else rl) ireg al;
+      print_int64_arith oc (rl = ah) rl (fun rl ->
+        fprintf oc "	rsbs	%a, %a, #0\n" ireg rl ireg al;
         (* No "rsc" instruction in Thumb2.  Emulate based on
              rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry)
                           == mvn a, b; adc a, a, #0 *)
         if !Clflags.option_fthumb then begin
           fprintf oc "	mvn	%a, %a\n" ireg rh ireg ah;
-          fprintf oc "	adc	%a, %a, #0\n" ireg rh ireg rh
+          fprintf oc "	adc	%a, %a, #0\n" ireg rh ireg rh; 3
         end else begin
-          fprintf oc "	rsc	%a, %a, #0\n" ireg rh ireg ah
-        end;
-        if rl = ah then
-          fprintf oc "	mov%t	%a, %a\n" thumbS ireg rl ireg IR14;
-        4
+          fprintf oc "	rsc	%a, %a, #0\n" ireg rh ireg ah; 2
+        end)
   | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      if rl = ah || rl = bh then begin
-        fprintf oc "	adds	%a, %a, %a\n" ireg IR14 ireg al ireg bl;
-        fprintf oc "	adc	%a, %a, %a\n" ireg rh ireg ah ireg bh;
-        fprintf oc "	mov%t	%a, %a\n" thumbS ireg rl ireg IR14; 3
-      end else begin
+      print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
         fprintf oc "	adds	%a, %a, %a\n" ireg rl ireg al ireg bl;
-        fprintf oc "	adc	%a, %a, %a\n" ireg rh ireg ah ireg bh; 2
-      end
+        fprintf oc "	adc	%a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
   | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      if rl = ah || rl = bh then begin
-        fprintf oc "	subs	%a, %a, %a\n" ireg IR14 ireg al ireg bl;
-        fprintf oc "	sbc	%a, %a, %a\n" ireg rh ireg ah ireg bh;
-        fprintf oc "	mov%t	%a, %a\n" thumbS ireg rl ireg IR14; 3
-      end else begin
+      print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
         fprintf oc "	subs	%a, %a, %a\n" ireg rl ireg al ireg bl;
-        fprintf oc "	sbc	%a, %a, %a\n" ireg rh ireg ah ireg bh; 2
-      end
+        fprintf oc "	sbc	%a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
   | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
       fprintf oc "	umull   %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1
   (* Memory accesses *)
@@ -581,6 +583,13 @@ let print_builtin_inline oc name args res =
   | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
       fprintf oc "	rev	%a, %a\n" ireg IR14 ireg a2;
       fprintf oc "	str	%a, [%a, #0]\n" ireg IR14 ireg a1; 2
+  (* Synchronization *)
+  | "__builtin_membar", [], _ ->
+      0
+  | "__builtin_dsb", [], _ ->
+      fprintf oc "	dsb\n"; 1
+  | "__builtin_isb", [], _ ->
+      fprintf oc "	isb\n"; 1
   (* Vararg stuff *)
   | "__builtin_va_start", [IR a], _ ->
       print_builtin_va_start oc a
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index e7d8337..6ee217c 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -92,6 +92,11 @@ let builtins_generic = {
         (TInt(IInt, []),
           [TPtr(TInt(IChar, [AConst]), []); TInt(IInt, [])],
           false);
+    (* Software memory barrier *)
+    "__builtin_membar",
+        (TVoid [],
+          [],
+          false);
     (* Variable arguments *)
 (* va_start(ap,n)
       (preprocessing) --> __builtin_va_start(ap, arg)
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index d30c856..56e837d 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -529,6 +529,9 @@ 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
+  (* Synchronization *)
+  | "__builtin_membar", [], _ ->
+      ()
   (* Vararg stuff *)
   | "__builtin_va_start", [IR a], _ ->
       print_builtin_va_start oc a
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 243a4d9..07cc50b 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -369,19 +369,19 @@ let expand_builtin_inline name args res =
       emit (Pcfi_adjust _m8)
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
-      expand_int64_arith (rl = ah) rl (fun rl' ->
-        emit (Psubfic(rl', al, Cint _0));
+      expand_int64_arith (rl = ah) rl (fun rl ->
+        emit (Psubfic(rl, al, Cint _0));
         emit (Psubfze(rh, ah)))
   | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      expand_int64_arith (rl = ah || rl = bh) rl (fun rl' ->
-        emit (Paddc(rl', al, bl));
+      expand_int64_arith (rl = ah || rl = bh) rl (fun rl ->
+        emit (Paddc(rl, al, bl));
         emit (Padde(rh, ah, bh)))
   | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      expand_int64_arith (rl = ah || rl = bh) rl (fun rl' ->
-        emit (Psubfc(rl', bl, al));
+      expand_int64_arith (rl = ah || rl = bh) rl (fun rl ->
+        emit (Psubfc(rl, bl, al));
         emit (Psubfe(rh, bh, ah)))
   | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
-      expand_int64_arith (rl = a || rl = b) rl (fun rl' ->
+      expand_int64_arith (rl = a || rl = b) rl (fun rl ->
         emit (Pmullw(rl, a, b));
         emit (Pmulhwu(rh, a, b)))
   (* Memory accesses *)
@@ -394,6 +394,8 @@ let expand_builtin_inline name args res =
   | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
       emit (Pstwbrx(a2, GPR0, a1))
   (* Synchronization *)
+  | "__builtin_membar", [], _ ->
+      ()
   | "__builtin_eieio", [], _ ->
       emit (Peieio)
   | "__builtin_sync", [], _ ->