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.

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