Use fix registers for atomic builtins.

In order to avoid clashes during register allocation etc. The
builtins now use fixed registers and mark additional registers as
destroyed for temporaries.

3 files changed, 47 insertions, 15 deletions

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 5e26e8a6..23c66382 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -506,20 +506,23 @@ let expand_builtin_inline name args res =
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
-      let tmpres = if a1 = res then
-        GPR11 
-      else
-        res in
       let lbl = new_label() in
       emit (Psync);
       emit (Plabel lbl);
-      emit (Plwarx (tmpres,GPR0,a1));
-      emit (Padd (a2,tmpres,a2));
-      emit (Pstwcx_ (a2,GPR0,a1));
+      emit (Plwarx (res,GPR0,a1));
+      emit (Padd (GPR10,res,a2));
+      emit (Pstwcx_ (GPR10,GPR0,a1));
+      emit (Pbne lbl);
+      emit (Pisync);
+  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR_none ->
+      let lbl = new_label() in
+      emit (Psync);
+      emit (Plabel lbl);
+      emit (Plwarx (GPR3,GPR0,a1));
+      emit (Padd (GPR10,GPR3,a2));
+      emit (Pstwcx_ (GPR10,GPR0,a1));
       emit (Pbne lbl);
       emit (Pisync);
-      if (tmpres <> res) then
-        emit (Pmr (res,tmpres))
   | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) ->
       let lbls = new_label ()
       and lblneq = new_label ()
@@ -542,6 +545,27 @@ let expand_builtin_inline name args res =
       emit (Pstw (GPR12,(Cint _0),exp));
       emit (Plabel lblsucc);
       emit (Pmr (res,dst));
+  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR_none ->
+      let lbls = new_label ()
+      and lblneq = new_label ()
+      and lblsucc = new_label () in      
+      emit (Plwz (GPR10,Cint _0,exp));
+      emit (Plwz (GPR11,Cint _0,des));
+      emit (Psync);
+      emit (Plabel lbls);
+      emit (Plwarx (GPR12,GPR0,dst));
+      emit (Pcmpw (GPR12,GPR10));
+      emit (Pbne lblneq);
+      emit (Pstwcx_ (GPR11,GPR0,dst));
+      emit (Pbne lbls);
+      emit (Plabel lblneq);
+      emit (Pisync);
+      emit (Pmfcr dst);
+      emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
+      emit (Pcmpwi (dst,(Cint _0)));
+      emit (Pbne lblsucc);
+      emit (Pstw (GPR12,(Cint _0),exp));
+      emit (Plabel lblsucc);
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 5409e9ef..a9e4f5e3 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -126,7 +126,8 @@ let builtins = {
       (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
     "__builtin_atomic_compare_exchange",
       (TInt (IBool, []), [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
-    
+    "__builtin_sync_fetch_and_add",
+      (TInt (IInt, []),  [TPtr (TInt(IInt, []),[]);TInt(IInt, [])],false);
   ]
 }
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 1699211d..c464ddd6 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -161,15 +161,15 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
   end.
 
 Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange".
-Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_and_fetch".
+Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_fetch_and_add".
 Definition builtin_atomic_compare_exchange := ident_of_string "__builtin_atomic_compare_exchange".
 
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_builtin id sg =>
-    if ident_eq id builtin_atomic_exchange then R10::R11::F13:: nil
-    else if ident_eq id builtin_sync_and_fetch then R11::F13::nil
-    else if ident_eq id builtin_atomic_compare_exchange then R10::R11::R12::F13:: nil
+    if ident_eq id builtin_atomic_exchange then R10::R11:: nil
+    else if ident_eq id builtin_atomic_compare_exchange then R10::R11::R12:: nil
+    else if ident_eq id builtin_sync_and_fetch then R3::R10::nil 
     else F13 :: nil
   | EF_vload _ => R11 :: nil
   | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
@@ -193,7 +193,14 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg
 
 
 Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) :=
-  (nil, nil).
+  match ef with
+    | EF_builtin id sg =>
+      if ident_eq id builtin_atomic_exchange then ((Some R3)::(Some R4)::(Some R5)::nil,nil)
+      else if ident_eq id builtin_sync_and_fetch then ((Some R4)::(Some R5)::nil,(Some R3)::nil)
+      else if ident_eq id builtin_atomic_compare_exchange then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil)
+      else (nil, nil)
+    | _ => (nil, nil)
+  end.
 
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store