Add some more synchronization builtins

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

2 files changed, 39 insertions, 1 deletions

diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 4446ab2..daeabda 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -44,10 +44,28 @@ let builtins = {
     "__builtin_write32_reversed",
       (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
     (* Synchronization *)
+    "__builtin_dmb",
+      (TVoid [], [], false);
     "__builtin_dsb",
       (TVoid [], [], false);
     "__builtin_isb",
-      (TVoid [], [], false)
+      (TVoid [], [], false);
+    "__builtin_ldrex",
+      (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
+    "__builtin_ldrexb",
+      (TInt(IUChar, []), [TPtr(TInt(IUChar, [AConst]), [])], false);
+    "__builtin_ldrexh",
+      (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
+    "__builtin_ldrexd",
+      (TInt(IULongLong, []), [TPtr(TInt(IULongLong, [AConst]), [])], false);
+    "__builtin_strex",
+      (TInt(IInt, []), [TPtr(TInt(IUInt, [AConst]), []); TInt(IUInt, [])], false);
+    "__builtin_strexb",
+      (TInt(IInt, []), [TPtr(TInt(IUChar, [AConst]), []); TInt(IUChar, [])], false);
+    "__builtin_strexh",
+      (TInt(IInt, []), [TPtr(TInt(IUShort, [AConst]), []); TInt(IUShort, [])], false);
+    "__builtin_strexd",
+      (TInt(IInt, []), [TPtr(TInt(IULongLong, [AConst]), []); TInt(IULongLong, [])], false);
   ]
 }
 
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 530a8f7..7ae4508 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -592,10 +592,30 @@ let print_builtin_inline oc name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
       0
+  | "__builtin_dmb", [], _ ->
+      fprintf oc "	dmb\n"; 1
   | "__builtin_dsb", [], _ ->
       fprintf oc "	dsb\n"; 1
   | "__builtin_isb", [], _ ->
       fprintf oc "	isb\n"; 1
+  | "__builtin_ldrex", [IR addr], [IR dst] ->
+      fprintf oc "	ldrex	%a, [%a]\n" dst addr
+  | "__builtin_ldrexb", [IR addr], [IR dst] ->
+      fprintf oc "	ldrexb	%a, [%a]\n" dst addr
+  | "__builtin_ldrexd", [IR addr], [IR dsth; IR dstl] ->
+      fprintf oc "	ldrexd	%a, %a, [%a]\n" dstl dsth addr
+  | "__builtin_ldrexh", [IR addr], [IR dst] ->
+      fprintf oc "	ldrexh	%a, [%a]\n" dst addr
+  | "__builtin_strex", [IR addr; IR src], [IR res] ->
+      fprintf oc "	strex	%a, %a, [%a]\n" res src addr; 1
+  | "__builtin_strexb", [IR addr; IR src], [IR res] ->
+      fprintf oc "	strexb	%a, %a, [%a]\n" res src addr; 1
+  | "__builtin_strexd", [IR addr; IR srch; IR srcl], [IR res] ->
+      fprintf oc "	strexd	%a, %a, %a, [%a]\n" res srcl srch addr; 1
+  | "__builtin_strexh", [IR addr; IR src], [IR res] ->
+      fprintf oc "	strexh	%a, %a, [%a]\n" res src addr; 1
+
+
   (* Vararg stuff *)
   | "__builtin_va_start", [IR a], _ ->
       print_builtin_va_start oc a