Cold feet: suppress builtins for load with reservation/store conditional, use case is unclear.

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

5 files changed, 2 insertions, 47 deletions

diff --git a/Changelog b/Changelog
index ef9ae30..ec31f0e 100644
--- a/Changelog
+++ b/Changelog
@@ -29,7 +29,6 @@ ARM port:
 - Exploit some VFPv3 instructions when available.
 - Built-in function '__builtin_cntlz' (count leading zeros)
   renamed '__builtin_clz' for GCC / Clang compatibility.
-- Added built-in functions for load with reservation / store conditional.
 
 PowerPC port:
 - Refactored the expansion of built-in functions and
@@ -39,7 +38,6 @@ PowerPC port:
 - More efficient code generated for volatile accesses to small data areas.
 - Built-in function '__builtin_cntlz' (count leading zeros)
   renamed '__builtin_clz' for GCC / Clang compatibility.
-- Added built-in functions for load with reservation / store conditional.
 
 IA32 port:
 - Added built-in functions __builtin_clz and __builtin_ctz
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 6f62bed..17aa511 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -49,23 +49,7 @@ let builtins = {
     "__builtin_dsb",
       (TVoid [], [], false);
     "__builtin_isb",
-      (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, []), []); TInt(IUInt, [])], false);
-    "__builtin_strexb",
-      (TInt(IInt, []), [TPtr(TInt(IUChar, []), []); TInt(IUChar, [])], false);
-    "__builtin_strexh",
-      (TInt(IInt, []), [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
-    "__builtin_strexd",
-      (TInt(IInt, []), [TPtr(TInt(IULongLong, []), []); TInt(IULongLong, [])], false);
+      (TVoid [], [], false)
   ]
 }
 
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 01ec716..e9b20d4 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -603,23 +603,6 @@ let print_builtin_inline oc name args res =
       fprintf oc "	dsb\n"; 1
   | "__builtin_isb", [], _ ->
       fprintf oc "	isb\n"; 1
-  | "__builtin_ldrex", [IR addr], [IR dst] ->
-      fprintf oc "	ldrex	%a, [%a]\n" ireg dst ireg addr; 1
-  | "__builtin_ldrexb", [IR addr], [IR dst] ->
-      fprintf oc "	ldrexb	%a, [%a]\n" ireg dst ireg addr; 1
-  | "__builtin_ldrexd", [IR addr], [IR dsth; IR dstl] ->
-      fprintf oc "	ldrexd	%a, %a, [%a]\n" ireg dstl ireg dsth ireg addr; 1
-  | "__builtin_ldrexh", [IR addr], [IR dst] ->
-      fprintf oc "	ldrexh	%a, [%a]\n" ireg dst ireg addr; 1
-  | "__builtin_strex", [IR addr; IR src], [IR res] ->
-      fprintf oc "	strex	%a, %a, [%a]\n" ireg res ireg src ireg addr; 1
-  | "__builtin_strexb", [IR addr; IR src], [IR res] ->
-      fprintf oc "	strexb	%a, %a, [%a]\n" ireg res ireg src ireg addr; 1
-  | "__builtin_strexd", [IR addr; IR srch; IR srcl], [IR res] ->
-      fprintf oc "	strexd	%a, %a, %a, [%a]\n" ireg res ireg srcl ireg srch ireg addr; 1
-  | "__builtin_strexh", [IR addr; IR src], [IR res] ->
-      fprintf oc "	strexh	%a, %a, [%a]\n" ireg res ireg src ireg addr; 1
-
 
   (* Vararg stuff *)
   | "__builtin_va_start", [IR a], _ ->
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 7a45452..c003bcd 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -418,12 +418,6 @@ let expand_builtin_inline name args res =
       emit (Pisync)
   | "__builtin_trap", [], _ ->
       emit (Ptrap)
-  | "__builtin_lwar", [IR addr], [IR res] ->
-      emit (Plwarx(res, GPR0, addr))
-  | "__builtin_stwc", [IR addr; IR src], [IR res] ->
-      emit (Pstwcx_(src, GPR0, addr));
-      emit (Pmfcr res);
-      emit (Prlwinm(res, res, Z.of_uint 3, _1))
   (* Vararg stuff *)
   | "__builtin_va_start", [IR a], _ ->
       expand_builtin_va_start a
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 53d84f7..8840d2c 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -84,11 +84,7 @@ let builtins = {
     "__builtin_isync",
       (TVoid [], [], false);
     "__builtin_trap",
-      (TVoid [], [], false);
-    "__builtin_lwar",
-      (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
-    "__builtin_stwc",
-      (TInt(IInt, []), [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false)
+      (TVoid [], [], false)
   ]
 }