diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-09 09:47:57 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-09 09:47:57 +0200 |
commit | 62277541b0ea1c687c64df79a543f776b9f58f29 (patch) | |
tree | 018b97b58a96f6c778db85ed16b382e295efee31 /powerpc/Asmexpand.ml | |
parent | fc4af0aa2601b290ec62dceef11599171f056770 (diff) | |
download | compcert-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.ml | 21 |
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 |