diff options
-rw-r--r-- | powerpc/Asmexpand.ml | 37 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 3 | ||||
-rw-r--r-- | powerpc/Machregs.v | 5 |
3 files changed, 41 insertions, 4 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index c6bda75c..beaef42f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -507,6 +507,43 @@ let expand_builtin_inline name args res = emit (Pbne lbl); emit (Pisync); emit (Pstw (a1,Cint _0, a2)); + | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> + let tmpres = if a1 = res then + GPR11 + else + res in + let lbl = new_label() in + emit (Psync); + emit (Plabel lbl); + emit (Plwarx (tmpres,GPR0,a1)); + emit (Padd (a2,tmpres,a2)); + emit (Pstwcx_ (a2,GPR0,a1)); + emit (Pbne lbl); + emit (Pisync); + if (tmpres <> res) then + emit (Pmr (res,tmpres)) + | "__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,exp)); + 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)); (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 2013c9cf..b61028d3 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -118,13 +118,12 @@ let builtins = { (TPtr (TVoid [],[]),[],false); (* isel *) "__builtin_isel", - (TInt (IInt, []),[TInt(IInt, []);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) - ] } diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index f07d488b..4391d5a8 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -161,13 +161,14 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := end. Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange". +Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_and_fetch". Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin id sg => if ident_eq id builtin_atomic_exchange then R10::R11::F13:: nil - else - F13 :: nil + else if ident_eq id builtin_sync_and_fetch then R11::F13::nil + else F13 :: nil | EF_vload _ => R11 :: nil | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil | EF_vstore _ => R11 :: R12 :: nil |