diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-09 15:36:34 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-09 15:36:34 +0200 |
| commit | 2dce91b8e2cae0b49c8870df6c727e25aaa180d8 (patch) | |
| tree | 1b8bab698f77feb32bd2997911523cccd1e2924a /powerpc | |
| parent | 62277541b0ea1c687c64df79a543f776b9f58f29 (diff) | |
| download | compcert-kvx-2dce91b8e2cae0b49c8870df6c727e25aaa180d8.tar.gz compcert-kvx-2dce91b8e2cae0b49c8870df6c727e25aaa180d8.zip | |
Add builtin for atomic load.
Implement the new __builtin_atomic_load(int *a, int *b); which stores
*a in *b. This differs from the atomic_load of the GCC, since the PPC
ISA manual states that you must jump before the load again if it fails.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asmexpand.ml | 9 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 5 |
2 files changed, 13 insertions, 1 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 749d5afd..c6bda75c 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -498,6 +498,15 @@ let expand_builtin_inline name args res = emit (Pbne lbl); emit (Pisync); emit (Pstw (GPR11,Cint _0,a3)) + | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> + let lbl = new_label() in + emit (Psync); + emit (Plabel lbl); + emit (Plwz (a1,Cint _0,a1)); + emit (Pcmpw (a1,a1)); + emit (Pbne lbl); + emit (Pisync); + emit (Pstw (a1,Cint _0, a2)); (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 1c7a3086..2013c9cf 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -121,7 +121,10 @@ let builtins = { (TInt (IInt, []),[TInt(IInt, []);TInt(IInt, []);TInt(IInt, [])],false); (* atomic operations *) "__builtin_atomic_exchange", - (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false) + (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); + "__builtin_atomic_load", + (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false) + ] } |