summaryrefslogtreecommitdiff
path: root/arm
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-20 13:02:53 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-20 13:02:53 +0000
commitac69dfdd1d7acc64035c70177f0c04b72627ed2e (patch)
tree054113b8d6a280c22903a62bf0925da7a734106b /arm
parenta350ca30d76323cd8c9957b3d70e2ee3f7562d1f (diff)
Add some more synchronization builtins
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
-rw-r--r--arm/CBuiltins.ml20
-rw-r--r--arm/PrintAsm.ml20
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