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.

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