From 62277541b0ea1c687c64df79a543f776b9f58f29 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 9 Sep 2015 09:47:57 +0200
Subject: Added an builtin for the atomic exchange operation.

The new builtin __builtin_atomic_exchange(int *a, int *b, int *c)
stores *b in *a and sets *c to the old value of *a.
---
 powerpc/Asm.v            |  2 ++
 powerpc/Asmexpand.ml     | 21 ++++++++++++++++-----
 powerpc/CBuiltins.ml     |  5 ++++-
 powerpc/Machregs.v       |  8 +++++++-
 powerpc/TargetPrinter.ml |  2 ++
 5 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 3c7bdd15..66bb4607 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -153,6 +153,7 @@ Inductive instruction : Type :=
   | Pbdnz: label -> instruction                               (**r decrement CTR and branch if not zero *)
   | Pbf: crbit -> label -> instruction                        (**r branch if false *)
   | Pbl: ident -> signature -> instruction                    (**r branch and link *)
+  | Pbne: label -> instruction                                (**r branch not equal *)
   | Pbs: ident -> signature -> instruction                    (**r branch to symbol *)
   | Pblr: instruction                                         (**r branch to contents of register LR *)
   | Pbt: crbit -> label -> instruction                        (**r branch if true *)
@@ -873,6 +874,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   (** The following instructions and directives are not generated
       directly by [Asmgen], so we do not model them. *)
   | Pbdnz _
+  | Pbne _
   | Pcmpb _ _ _
   | Pcntlzw _ _
   | Pcreqv _ _ _
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 3fffc037..749d5afd 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -64,7 +64,7 @@ let expand_annot_val txt targ args res =
    Note that lfd and stfd cannot trap on ill-formed floats. *)
 
 let offset_in_range ofs =
-  Int.eq (Asmgen.high_s ofs) Int.zero
+  Int.eq (Asmgen.high_s ofs) _0
 
 let memcpy_small_arg sz arg tmp =
   match arg with
@@ -276,9 +276,9 @@ let expand_builtin_vstore chunk args =
       assert false
 
 (* Handling of varargs *)
-let linkregister_offset = ref  Int.zero
+let linkregister_offset = ref  _0
 
-let retaddr_offset = ref Int.zero
+let retaddr_offset = ref _0
 
 let current_function_stacksize = ref 0l
 
@@ -485,8 +485,19 @@ let expand_builtin_inline name args res =
       emit (Plwz (res, Cint! retaddr_offset,GPR1))
   (* isel *)
   | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) ->
-      emit (Pcmpwi (a1,Cint (Int.zero)));
+      emit (Pcmpwi (a1,Cint (_0)));
       emit (Pisel (res,a3,a2,CRbit_2))
+  (* atomic operations *)
+  | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ ->
+      emit (Plwz (GPR10,Cint _0,a2));
+      emit (Psync);
+      let lbl = new_label() in
+      emit (Plabel lbl);
+      emit (Plwarx (GPR11,GPR0,a1));
+      emit (Pstwcx_ (GPR10,GPR0,a1));
+      emit (Pbne lbl);
+      emit (Pisync);
+      emit (Pstw (GPR11,Cint _0,a3))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
@@ -517,7 +528,7 @@ let expand_instruction instr =
   | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
       let sz = camlint_of_coqint sz in
-      assert (ofs = Int.zero);
+      assert (ofs = _0);
       let sz = if variadic then Int32.add sz 96l else sz in
       let adj = Int32.neg sz in
       if adj >= -0x8000l then
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index e219a175..1c7a3086 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -118,7 +118,10 @@ let builtins = {
       (TPtr (TVoid [],[]),[],false);
     (* isel *)
     "__builtin_isel",
-      (TInt (IInt, []),[TInt(IInt, []);TInt(IInt, []);TInt(IInt, [])],false)
+      (TInt (IInt, []),[TInt(IInt, []);TInt(IInt, []);TInt(IInt, [])],false);
+    (* atomic operations *)
+    "__builtin_atomic_exchange",
+      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false)
   ]
 }
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index a2017dca..f07d488b 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -160,9 +160,14 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
       end
   end.
 
+Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange".
+
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
-  | EF_builtin _ _ => F13 :: nil
+  | EF_builtin id sg =>
+    if ident_eq id builtin_atomic_exchange then R10::R11::F13:: nil
+    else
+      F13 :: nil
   | EF_vload _ => R11 :: nil
   | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
   | EF_vstore _ => R11 :: R12 :: nil
@@ -183,6 +188,7 @@ Definition temp_for_parent_frame: mreg :=
 Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
   (nil, None).
 
+
 Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) :=
   (nil, nil).
 
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index eca7a1b8..f5295777 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -414,6 +414,8 @@ module Target (System : SYSTEM):TARGET =
           end
       | Pbl(s, sg) ->
           fprintf oc "	bl	%a\n" symbol s
+      | Pbne lbl ->
+          fprintf oc "	bne-	%a\n" label (transl_label lbl)
       | Pbs(s, sg) ->
           fprintf oc "	b	%a\n" symbol s
       | Pblr ->
-- 
cgit 


From 2dce91b8e2cae0b49c8870df6c727e25aaa180d8 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 9 Sep 2015 15:36:34 +0200
Subject: Add builtin for atomic load.

Implement the new __builtin_atomic_load(int *a, int *b); which stores
*a in *b. This differs from the atomic_load of the GCC, since the PPC
ISA manual states that you must jump before the load again if it fails.
---
 powerpc/Asmexpand.ml | 9 +++++++++
 powerpc/CBuiltins.ml | 5 ++++-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 749d5afd..c6bda75c 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -498,6 +498,15 @@ let expand_builtin_inline name args res =
       emit (Pbne lbl);
       emit (Pisync);
       emit (Pstw (GPR11,Cint _0,a3))
+  | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
+      let lbl = new_label() in
+      emit (Psync);
+      emit (Plabel lbl);
+      emit (Plwz (a1,Cint _0,a1));
+      emit (Pcmpw (a1,a1));
+      emit (Pbne lbl);
+      emit (Pisync);
+      emit (Pstw (a1,Cint _0, a2));
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 1c7a3086..2013c9cf 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -121,7 +121,10 @@ let builtins = {
       (TInt (IInt, []),[TInt(IInt, []);TInt(IInt, []);TInt(IInt, [])],false);
     (* atomic operations *)
     "__builtin_atomic_exchange",
-      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false)
+      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
+    "__builtin_atomic_load",
+      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false)
+
   ]
 }
 
-- 
cgit 


From 41655f6c8d38270cc50407b0141b443f6ee90100 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 10 Sep 2015 10:20:15 +0200
Subject: Added builtin for atomic compare and exchange.

The new __builtin_atomic_compare_exchange(int *ptr,int *exp,int *dsr);
writes dsr into ptr if ptr is equal to exp and returns true if
ptr is not equal to exp it writes ptr into exp and returns false.
---
 powerpc/AsmToJSON.ml | 1 +
 powerpc/Asmexpand.ml | 2 +-
 powerpc/CBuiltins.ml | 5 ++++-
 powerpc/Machregs.v   | 2 ++
 4 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 3ed36c4d..7cb41e69 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -163,6 +163,7 @@ let p_instruction oc ic =
   | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l 
   | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l
   | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}"  p_atom_constant i
+  | Pbne (lbl) -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}"  p_atom_constant lbl
   | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}"  p_atom_constant i
   | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}"
   | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index beaef42f..8cd123fe 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -527,7 +527,7 @@ let expand_builtin_inline name args res =
       and lblneq = new_label ()
       and lblsucc = new_label () in      
       emit (Plwz (GPR10,Cint _0,exp));
-      emit (Plwz (GPR11,Cint _0,exp));
+      emit (Plwz (GPR11,Cint _0,des));
       emit (Psync);
       emit (Plabel lbls);
       emit (Plwarx (GPR12,GPR0,dst));
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index b61028d3..5409e9ef 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -123,7 +123,10 @@ let builtins = {
     "__builtin_atomic_exchange",
       (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
     "__builtin_atomic_load",
-      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false)
+      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
+    "__builtin_atomic_compare_exchange",
+      (TInt (IBool, []), [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
+    
   ]
 }
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 4391d5a8..1699211d 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -162,12 +162,14 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
 
 Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange".
 Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_and_fetch".
+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
     else F13 :: nil
   | EF_vload _ => R11 :: nil
   | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
-- 
cgit 


From 2809e264a4c146b31b5009fba08f74d12126a1b3 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 10 Sep 2015 10:51:35 +0200
Subject: Type of argument for Pbne is label not atom.

---
 powerpc/AsmToJSON.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index c52c65c4..7064ebdd 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -163,7 +163,7 @@ let p_instruction oc ic =
   | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l 
   | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l
   | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}"  p_atom_constant i
-  | Pbne (lbl) -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}"  p_atom_constant lbl
+  | Pbne (lbl) -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl
   | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}"  p_atom_constant i
   | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}"
   | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l
-- 
cgit 


From 0de3d126e70dfedfd6f74710da31c4b9636f900a Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 11 Sep 2015 12:05:31 +0200
Subject: Use the gcc version of atomic load.

---
 powerpc/Asm.v            | 2 ++
 powerpc/AsmToJSON.ml     | 3 ++-
 powerpc/Asmexpand.ml     | 4 +---
 powerpc/TargetPrinter.ml | 5 +++++
 4 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 66bb4607..5fd40a27 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -154,6 +154,7 @@ Inductive instruction : Type :=
   | Pbf: crbit -> label -> instruction                        (**r branch if false *)
   | Pbl: ident -> signature -> instruction                    (**r branch and link *)
   | Pbne: label -> instruction                                (**r branch not equal *)
+  | Pbne_rel: int -> instruction                              (**r branch not equal with relative offset *)
   | Pbs: ident -> signature -> instruction                    (**r branch to symbol *)
   | Pblr: instruction                                         (**r branch to contents of register LR *)
   | Pbt: crbit -> label -> instruction                        (**r branch if true *)
@@ -875,6 +876,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       directly by [Asmgen], so we do not model them. *)
   | Pbdnz _
   | Pbne _
+  | Pbne_rel _
   | Pcmpb _ _ _
   | Pcntlzw _ _
   | Pcreqv _ _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 7064ebdd..d23beaad 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -163,7 +163,8 @@ let p_instruction oc ic =
   | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l 
   | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l
   | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}"  p_atom_constant i
-  | Pbne (lbl) -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl
+  | Pbne lbl -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl
+  | Pbne_rel ofs -> fprintf oc"{\"Instruction Name\":\"Pbne_rel\",\"Args\":[%a]}" p_int_constant ofs
   | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}"  p_atom_constant i
   | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}"
   | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 8cd123fe..5e26e8a6 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -499,12 +499,10 @@ let expand_builtin_inline name args res =
       emit (Pisync);
       emit (Pstw (GPR11,Cint _0,a3))
   | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
-      let lbl = new_label() in
       emit (Psync);
-      emit (Plabel lbl);
       emit (Plwz (a1,Cint _0,a1));
       emit (Pcmpw (a1,a1));
-      emit (Pbne lbl);
+      emit (Pbne_rel _4);
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index f5295777..1f1306c0 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -416,6 +416,11 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	bl	%a\n" symbol s
       | Pbne lbl ->
           fprintf oc "	bne-	%a\n" label (transl_label lbl)
+      | Pbne_rel ofs ->
+          let ofs = camlint_of_coqint ofs in
+          let sign = if ofs >= 0l then "+" else "-" in
+          let ofs = Int32.abs ofs in
+          fprintf oc "	bne-	$%s%ld\n" sign ofs 
       | Pbs(s, sg) ->
           fprintf oc "	b	%a\n" symbol s
       | Pblr ->
-- 
cgit 


From 9dc0dd73f75875b301c886df40087192d0fad386 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 14 Sep 2015 19:41:39 +0200
Subject: 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.
---
 powerpc/Asmexpand.ml | 42 +++++++++++++++++++++++++++++++++---------
 powerpc/CBuiltins.ml |  3 ++-
 powerpc/Machregs.v   | 17 ++++++++++++-----
 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
-- 
cgit 


From fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 15 Sep 2015 12:32:09 +0200
Subject: Removed usage of bne and removed duplicated code for return values of
 atomics.

Instead of introducing a new bne instruction in Asm.v and the TargetPrinter.ml
I use the equivalent bf instruction. The duplicated code is due to unused return
values of builtins. Now we only emit the additional code for the return value if
the return value is used instead of duplicating the whole emiting sequence.
---
 powerpc/Asm.v            |  4 ----
 powerpc/AsmToJSON.ml     |  2 --
 powerpc/Asmexpand.ml     | 58 ++++++++++++++++--------------------------------
 powerpc/TargetPrinter.ml |  7 ------
 4 files changed, 19 insertions(+), 52 deletions(-)

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 5fd40a27..3c7bdd15 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -153,8 +153,6 @@ Inductive instruction : Type :=
   | Pbdnz: label -> instruction                               (**r decrement CTR and branch if not zero *)
   | Pbf: crbit -> label -> instruction                        (**r branch if false *)
   | Pbl: ident -> signature -> instruction                    (**r branch and link *)
-  | Pbne: label -> instruction                                (**r branch not equal *)
-  | Pbne_rel: int -> instruction                              (**r branch not equal with relative offset *)
   | Pbs: ident -> signature -> instruction                    (**r branch to symbol *)
   | Pblr: instruction                                         (**r branch to contents of register LR *)
   | Pbt: crbit -> label -> instruction                        (**r branch if true *)
@@ -875,8 +873,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   (** The following instructions and directives are not generated
       directly by [Asmgen], so we do not model them. *)
   | Pbdnz _
-  | Pbne _
-  | Pbne_rel _
   | Pcmpb _ _ _
   | Pcntlzw _ _
   | Pcreqv _ _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index d23beaad..a7e66701 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -163,8 +163,6 @@ let p_instruction oc ic =
   | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l 
   | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l
   | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}"  p_atom_constant i
-  | Pbne lbl -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl
-  | Pbne_rel ofs -> fprintf oc"{\"Instruction Name\":\"Pbne_rel\",\"Args\":[%a]}" p_int_constant ofs
   | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}"  p_atom_constant i
   | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}"
   | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 23c66382..098eb49d 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -495,57 +495,32 @@ let expand_builtin_inline name args res =
       emit (Plabel lbl);
       emit (Plwarx (GPR11,GPR0,a1));
       emit (Pstwcx_ (GPR10,GPR0,a1));
-      emit (Pbne lbl);
+      emit (Pbf (CRbit_2,lbl));
       emit (Pisync);
       emit (Pstw (GPR11,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 (Pbne_rel _4);
+      emit (Pbf (CRbit_2,lbl));
+      emit (Plabel lbl);
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
-  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
+  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], res ->
       let lbl = new_label() in
+      let res = (match res with
+      | BR (IR res) -> res
+      | BR_none -> GPR3
+      | _ ->   raise (Error ("unrecognized builtin " ^ name))) in
       emit (Psync);
       emit (Plabel lbl);
       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 (Pbf (CRbit_2, lbl));
       emit (Pisync);
-  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) ->
-      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);
-      emit (Pmr (res,dst));
-  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR_none ->
+  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], res ->
       let lbls = new_label ()
       and lblneq = new_label ()
       and lblsucc = new_label () in      
@@ -555,17 +530,22 @@ let expand_builtin_inline name args res =
       emit (Plabel lbls);
       emit (Plwarx (GPR12,GPR0,dst));
       emit (Pcmpw (GPR12,GPR10));
-      emit (Pbne lblneq);
+      emit (Pbf (CRbit_2,lblneq));
       emit (Pstwcx_ (GPR11,GPR0,dst));
-      emit (Pbne lbls);
+      emit (Pbf (CRbit_2,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 (Pbf (CRbit_2,lblsucc));
       emit (Pstw (GPR12,(Cint _0),exp));
       emit (Plabel lblsucc);
+      (match res with
+      | BR_none -> ()
+      | BR (IR res) ->
+          emit (Pmr (res,dst))
+      | _ ->raise (Error ("unrecognized builtin " ^ name)))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 1f1306c0..eca7a1b8 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -414,13 +414,6 @@ module Target (System : SYSTEM):TARGET =
           end
       | Pbl(s, sg) ->
           fprintf oc "	bl	%a\n" symbol s
-      | Pbne lbl ->
-          fprintf oc "	bne-	%a\n" label (transl_label lbl)
-      | Pbne_rel ofs ->
-          let ofs = camlint_of_coqint ofs in
-          let sign = if ofs >= 0l then "+" else "-" in
-          let ofs = Int32.abs ofs in
-          fprintf oc "	bne-	$%s%ld\n" sign ofs 
       | Pbs(s, sg) ->
           fprintf oc "	b	%a\n" symbol s
       | Pblr ->
-- 
cgit 


From 435dc0e6fe74f0ab06737360e1dc49b42b95f1e4 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 17 Sep 2015 19:20:57 +0200
Subject: Integrated the fix of commit de40fce9c16ced8d23389cbcfc55ef6d99466fe8
 for the atomics.

---
 powerpc/Asmexpand.ml | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 098eb49d..702b6a76 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -507,12 +507,8 @@ let expand_builtin_inline name args res =
       emit (Plabel lbl);
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
-  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], res ->
+  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
       let lbl = new_label() in
-      let res = (match res with
-      | BR (IR res) -> res
-      | BR_none -> GPR3
-      | _ ->   raise (Error ("unrecognized builtin " ^ name))) in
       emit (Psync);
       emit (Plabel lbl);
       emit (Plwarx (res,GPR0,a1));
@@ -520,7 +516,7 @@ let expand_builtin_inline name args res =
       emit (Pstwcx_ (GPR10,GPR0,a1));
       emit (Pbf (CRbit_2, lbl));
       emit (Pisync);
-  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], res ->
+  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)],  BR (IR res) ->
       let lbls = new_label ()
       and lblneq = new_label ()
       and lblsucc = new_label () in      
@@ -541,11 +537,7 @@ let expand_builtin_inline name args res =
       emit (Pbf (CRbit_2,lblsucc));
       emit (Pstw (GPR12,(Cint _0),exp));
       emit (Plabel lblsucc);
-      (match res with
-      | BR_none -> ()
-      | BR (IR res) ->
-          emit (Pmr (res,dst))
-      | _ ->raise (Error ("unrecognized builtin " ^ name)))
+      emit (Pmr (res,dst))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
-- 
cgit 


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(-)

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 


From 3174d685154a1e0febf305d305fc79422a1adcd3 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 21 Sep 2015 17:49:22 +0200
Subject: Removed unnecessary move register and use the correct register as
 base value for the rlwinm.

---
 powerpc/Asmexpand.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 9a3804a0..23704feb 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -533,12 +533,11 @@ let expand_builtin_inline name args res =
       (* Here, CR2 is true if the exchange succeeded, false if it failed *)
       emit (Pisync);
       emit (Pmfcr dst);
-      emit (Prlwinm (res,res,(Z.of_uint 3),_1));
+      emit (Prlwinm (res,dest,(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))
+      emit (Plabel lblsucc)
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
-- 
cgit