aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmexpand.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-09 09:47:57 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-09 09:47:57 +0200
commit62277541b0ea1c687c64df79a543f776b9f58f29 (patch)
tree018b97b58a96f6c778db85ed16b382e295efee31 /powerpc/Asmexpand.ml
parentfc4af0aa2601b290ec62dceef11599171f056770 (diff)
downloadcompcert-kvx-62277541b0ea1c687c64df79a543f776b9f58f29.tar.gz
compcert-kvx-62277541b0ea1c687c64df79a543f776b9f58f29.zip
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.
Diffstat (limited to 'powerpc/Asmexpand.ml')
-rw-r--r--powerpc/Asmexpand.ml21
1 files changed, 16 insertions, 5 deletions
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