diff options
| -rw-r--r-- | powerpc/AsmToJSON.ml | 1 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 5 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 2 |
4 files changed, 8 insertions, 2 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 3ed36c4d..7cb41e69 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -163,6 +163,7 @@ let p_instruction oc ic = | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}" p_atom_constant i + | Pbne (lbl) -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_atom_constant lbl | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}" p_atom_constant i | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}" | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index beaef42f..8cd123fe 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -527,7 +527,7 @@ let expand_builtin_inline name args res = and lblneq = new_label () and lblsucc = new_label () in emit (Plwz (GPR10,Cint _0,exp)); - emit (Plwz (GPR11,Cint _0,exp)); + emit (Plwz (GPR11,Cint _0,des)); emit (Psync); emit (Plabel lbls); emit (Plwarx (GPR12,GPR0,dst)); diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index b61028d3..5409e9ef 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -123,7 +123,10 @@ let builtins = { "__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) + (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); + "__builtin_atomic_compare_exchange", + (TInt (IBool, []), [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); + ] } diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 4391d5a8..1699211d 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -162,12 +162,14 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange". Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_and_fetch". +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 id sg => if ident_eq id builtin_atomic_exchange then R10::R11::F13:: nil else if ident_eq id builtin_sync_and_fetch then R11::F13::nil + else if ident_eq id builtin_atomic_compare_exchange then R10::R11::R12::F13:: nil else F13 :: nil | EF_vload _ => R11 :: nil | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil |