From bc1fbdd0baaab41aa048b3214ec71bb0cc04dfcc Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 21 Sep 2015 16:17:44 +0200
Subject: Applied a few simplification for temporary registers.

---
 powerpc/Asmexpand.ml | 27 ++++++++++++++-------------
 powerpc/Machregs.v   |  5 ++---
 2 files changed, 16 insertions(+), 16 deletions(-)

(limited to 'powerpc')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 702b6a76..9a3804a0 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -493,27 +493,27 @@ let expand_builtin_inline name args res =
       emit (Psync);
       let lbl = new_label() in
       emit (Plabel lbl);
-      emit (Plwarx (GPR11,GPR0,a1));
+      emit (Plwarx (GPR0,GPR0,a1));
       emit (Pstwcx_ (GPR10,GPR0,a1));
       emit (Pbf (CRbit_2,lbl));
       emit (Pisync);
-      emit (Pstw (GPR11,Cint _0,a3))
+      emit (Pstw (GPR0,Cint _0,a3))
   | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
       let lbl = new_label () in
       emit (Psync);
-      emit (Plwz (a1,Cint _0,a1));
-      emit (Pcmpw (a1,a1));
+      emit (Plwz (GPR0,Cint _0,a1));
+      emit (Pcmpw (GPR0,GPR0));
       emit (Pbf (CRbit_2,lbl));
       emit (Plabel lbl);
       emit (Pisync);
-      emit (Pstw (a1,Cint _0, a2));
+      emit (Pstw (GPR0,Cint _0, a2))
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
       let lbl = new_label() in
       emit (Psync);
       emit (Plabel lbl);
       emit (Plwarx (res,GPR0,a1));
-      emit (Padd (GPR10,res,a2));
-      emit (Pstwcx_ (GPR10,GPR0,a1));
+      emit (Padd (GPR0,res,a2));
+      emit (Pstwcx_ (GPR0,GPR0,a1));
       emit (Pbf (CRbit_2, lbl));
       emit (Pisync);
   | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)],  BR (IR res) ->
@@ -524,18 +524,19 @@ let expand_builtin_inline name args res =
       emit (Plwz (GPR11,Cint _0,des));
       emit (Psync);
       emit (Plabel lbls);
-      emit (Plwarx (GPR12,GPR0,dst));
-      emit (Pcmpw (GPR12,GPR10));
+      emit (Plwarx (GPR0,GPR0,dst));
+      emit (Pcmpw (GPR0,GPR10));
       emit (Pbf (CRbit_2,lblneq));
       emit (Pstwcx_ (GPR11,GPR0,dst));
       emit (Pbf (CRbit_2,lbls));
       emit (Plabel lblneq);
+      (* Here, CR2 is true if the exchange succeeded, false if it failed *)
       emit (Pisync);
       emit (Pmfcr dst);
-      emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
-      emit (Pcmpwi (dst,(Cint _0)));
-      emit (Pbf (CRbit_2,lblsucc));
-      emit (Pstw (GPR12,(Cint _0),exp));
+      emit (Prlwinm (res,res,(Z.of_uint 3),_1));
+      (* Update exp with the current value of dst if the exchange failed *)
+      emit (Pbt (CRbit_2,lblsucc));
+      emit (Pstw (GPR0,Cint _0,exp));
       emit (Plabel lblsucc);
       emit (Pmr (res,dst))
   (* Catch-all *)
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index c464ddd6..f94c3b64 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -167,9 +167,8 @@ Definition builtin_atomic_compare_exchange := ident_of_string "__builtin_atomic_
 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:: 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 
+    if ident_eq id builtin_atomic_exchange then R10::nil
+    else if ident_eq id builtin_atomic_compare_exchange then R10::R11::nil
     else F13 :: nil
   | EF_vload _ => R11 :: nil
   | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
-- 
cgit