diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-20 13:02:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-20 13:02:53 +0000 |
| commit | ac69dfdd1d7acc64035c70177f0c04b72627ed2e (patch) | |
| tree | 054113b8d6a280c22903a62bf0925da7a734106b /arm | |
| parent | a350ca30d76323cd8c9957b3d70e2ee3f7562d1f (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.ml | 20 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 20 |
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 |