diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-10 10:20:15 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-10 10:20:15 +0200 |
| commit | 41655f6c8d38270cc50407b0141b443f6ee90100 (patch) | |
| tree | 838b8432f9a66123ca876579298e2eb34b51d407 /powerpc | |
| parent | be6dc9e64912901b8217f56656d770f957d15cb4 (diff) | |
| download | compcert-kvx-41655f6c8d38270cc50407b0141b443f6ee90100.tar.gz compcert-kvx-41655f6c8d38270cc50407b0141b443f6ee90100.zip | |
Added builtin for atomic compare and exchange.
The new __builtin_atomic_compare_exchange(int *ptr,int *exp,int *dsr);
writes dsr into ptr if ptr is equal to exp and returns true if
ptr is not equal to exp it writes ptr into exp and returns false.
Diffstat (limited to 'powerpc')
| -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 |