From ac69dfdd1d7acc64035c70177f0c04b72627ed2e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 20 Aug 2014 13:02:53 +0000
Subject: Add some more synchronization builtins

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/PrintAsm.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'arm/PrintAsm.ml')

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 530a8f71..7ae45088 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
-- 
cgit