Add builtins for load with reservation and conditional store.

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

5 files changed, 39 insertions, 1 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index a9a5f02..f175f16 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -1664,6 +1664,16 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Plwarx(rd, r1, r2) ->
+          begin match ecode with
+          | LWARX(rD, rA, rB):: es ->
+              OK(fw)
+              >>= match_iregs rd rD
+              >>= match_iregs r1 rA
+              >>= match_iregs r2 rB
+              >>= recur_simpl
+          | _ -> error
+          end
       | Plwbrx(rd, r1, r2) ->
           begin match ecode with
           | LWBRX(rD, rA, rB):: es ->
@@ -2121,6 +2131,16 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pstwcx_(rd, r1, r2) ->
+          begin match ecode with
+          | STWCX_(rS, rA, rB) :: es ->
+              OK(fw)
+              >>= match_iregs rd rS
+              >>= match_iregs r1 rA
+              >>= match_iregs r2 rB
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pstwxu(rd, r1, r2) ->
           begin match ecode with
           | STWUX(rS, rA, rB) :: es ->
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index fc8c2d9..18316fb 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -221,6 +221,7 @@ Inductive instruction : Type :=
   | Plwzx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plwz_a: ireg -> constant -> ireg -> instruction           (**r load 32-bit quantity to int reg *)
   | Plwzx_a: ireg -> ireg -> ireg -> instruction              (**r same, with 2 index regs *)
+  | Plwarx: ireg -> ireg -> ireg -> instruction               (**r load with reservation *)
   | Plwbrx: ireg -> ireg -> ireg -> instruction               (**r load 32-bit int and reverse endianness *)
   | Pmfcr: ireg -> instruction                                (**r move condition register to reg *)
   | Pmfcrbit: ireg -> crbit -> instruction                    (**r move condition bit to reg (pseudo) *)
@@ -263,6 +264,7 @@ Inductive instruction : Type :=
   | Pstw_a: ireg -> constant -> ireg -> instruction           (**r store 32-bit quantity from int reg *)
   | Pstwx_a: ireg -> ireg -> ireg -> instruction              (**r same, with 2 index regs *)
   | Pstwbrx: ireg -> ireg -> ireg -> instruction              (**r store 32-bit int with reverse endianness *)
+  | Pstwcx_: ireg -> ireg -> ireg -> instruction              (**r store conditional *)
   | Psubfc: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction *)
   | Psubfe: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction with carry *)
   | Psubfze: ireg -> ireg -> instruction                      (**r integer opposite with carry *)
@@ -869,12 +871,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfrsqrte _ _
   | Pfres _ _
   | Pfsel _ _ _ _
+  | Plwarx _ _ _
   | Plwbrx _ _ _
   | Pisync
   | Plhbrx _ _ _
   | Plwzu _ _ _
   | Pmfcr _
   | Pstwbrx _ _ _
+  | Pstwcx_ _ _ _
   | Pstfdu _ _ _
   | Psthbrx _ _ _
   | Pstwu _ _ _
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index bec4daa..3554de8 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -418,6 +418,12 @@ 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 db01ae1..f28ff8b 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -84,7 +84,11 @@ let builtins = {
     "__builtin_isync",
       (TVoid [], [], false);
     "__builtin_trap",
-      (TVoid [], [], false)
+      (TVoid [], [], false);
+    "__builtin_lwar",
+      (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
+    "__builtin_stwc",
+      (TInt(IInt, []), [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false)
   ]
 }
 
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 0192747..d2ec561 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -512,6 +512,8 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	addis	%a, 0, %a\n" ireg GPR12 label_high lbl;
       fprintf oc "	lfs	%a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c);
       float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals;
+  | Plwarx(r1, r2, r3) ->
+      fprintf oc "	lwarx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plwbrx(r1, r2, r3) ->
       fprintf oc "	lwbrx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) ->
@@ -600,6 +602,8 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	stwxu	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstwbrx(r1, r2, r3) ->
       fprintf oc "	stwbrx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pstwcx_(r1, r2, r3) ->
+      fprintf oc "	stwcx.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfc(r1, r2, r3) ->
       fprintf oc "	subfc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfe(r1, r2, r3) ->