aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2015-09-21 17:51:38 +0200
committerBernhard Schommer <bschommer@users.noreply.github.com>2015-09-21 17:51:38 +0200
commit4365eedb2d7529e670af2ef22e38da6bed38fd1a (patch)
treedc53a02144d9c8c4faec7fa54a626db5e143f402
parentdb0a62a01bbf90617701b68917319767159bf039 (diff)
parent3174d685154a1e0febf305d305fc79422a1adcd3 (diff)
downloadcompcert-4365eedb2d7529e670af2ef22e38da6bed38fd1a.tar.gz
compcert-4365eedb2d7529e670af2ef22e38da6bed38fd1a.zip
Merge pull request #54 from AbsInt/atomic-builtins
Atomic builtins
-rw-r--r--powerpc/Asmexpand.ml61
-rw-r--r--powerpc/CBuiltins.ml11
-rw-r--r--powerpc/Machregs.v19
3 files changed, 83 insertions, 8 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index b9fe1d7f..1b9740b9 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,59 @@ 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 (GPR0,GPR0,a1));
+ emit (Pstwcx_ (GPR10,GPR0,a1));
+ emit (Pbf (CRbit_2,lbl));
+ emit (Pisync);
+ emit (Pstw (GPR0,Cint _0,a3))
+ | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
+ let lbl = new_label () in
+ emit (Psync);
+ emit (Plwz (GPR0,Cint _0,a1));
+ emit (Pcmpw (GPR0,GPR0));
+ emit (Pbf (CRbit_2,lbl));
+ emit (Plabel lbl);
+ emit (Pisync);
+ 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 (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) ->
+ 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 (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 (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)
(* Catch-all *)
| _ ->
raise (Error ("unrecognized builtin " ^ name))
@@ -517,7 +568,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 1bb8c6f7..a9e4f5e3 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -118,7 +118,16 @@ let builtins = {
(TPtr (TVoid [],[]),[],false);
(* isel *)
"__builtin_isel",
- (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false)
+ (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false);
+ (* atomic operations *)
+ "__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);
+ "__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 a2017dca..f94c3b64 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -160,9 +160,16 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
end
end.
+Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange".
+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 _ _ => F13 :: nil
+ | EF_builtin id sg =>
+ 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
| EF_vstore _ => R11 :: R12 :: nil
@@ -183,8 +190,16 @@ 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).
+ 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