summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-20 14:24:42 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-20 14:24:42 +0000
commit626ea26cb58e50e7a42f90a6e23218d90df6dd5a (patch)
treee8214df04ff25411e435210beb8e9e188683b113 /powerpc
parente2fa973a4bfea5d47b0d9f41b8734a7b6744dc18 (diff)
Add builtins for load with reservation and conditional store.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asm.v4
-rw-r--r--powerpc/Asmexpand.ml6
-rw-r--r--powerpc/CBuiltins.ml6
-rw-r--r--powerpc/PrintAsm.ml4
4 files changed, 19 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index fc8c2d9..18316fb 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -221,6 +221,7 @@ Inductive instruction : Type :=
| Plwzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *)
| Plwz_a: ireg -> constant -> ireg -> instruction (**r load 32-bit quantity to int reg *)
| Plwzx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *)
+ | Plwarx: ireg -> ireg -> ireg -> instruction (**r load with reservation *)
| Plwbrx: ireg -> ireg -> ireg -> instruction (**r load 32-bit int and reverse endianness *)
| Pmfcr: ireg -> instruction (**r move condition register to reg *)
| Pmfcrbit: ireg -> crbit -> instruction (**r move condition bit to reg (pseudo) *)
@@ -263,6 +264,7 @@ Inductive instruction : Type :=
| Pstw_a: ireg -> constant -> ireg -> instruction (**r store 32-bit quantity from int reg *)
| Pstwx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *)
| Pstwbrx: ireg -> ireg -> ireg -> instruction (**r store 32-bit int with reverse endianness *)
+ | Pstwcx_: ireg -> ireg -> ireg -> instruction (**r store conditional *)
| Psubfc: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction *)
| Psubfe: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction with carry *)
| Psubfze: ireg -> ireg -> instruction (**r integer opposite with carry *)
@@ -869,12 +871,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfrsqrte _ _
| Pfres _ _
| Pfsel _ _ _ _
+ | Plwarx _ _ _
| Plwbrx _ _ _
| Pisync
| Plhbrx _ _ _
| Plwzu _ _ _
| Pmfcr _
| Pstwbrx _ _ _
+ | Pstwcx_ _ _ _
| Pstfdu _ _ _
| Psthbrx _ _ _
| Pstwu _ _ _
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index bec4daa..3554de8 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -418,6 +418,12 @@ let expand_builtin_inline name args res =
emit (Pisync)
| "__builtin_trap", [], _ ->
emit (Ptrap)
+ | "__builtin_lwar", [IR addr], [IR res] ->
+ emit (Plwarx(res, GPR0, addr))
+ | "__builtin_stwc", [IR addr; IR src], [IR res] ->
+ emit (Pstwcx_(src, GPR0, addr));
+ emit (Pmfcr res);
+ emit (Prlwinm(res, res, Z.of_uint 3, _1))
(* Vararg stuff *)
| "__builtin_va_start", [IR a], _ ->
expand_builtin_va_start a
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index db01ae1..f28ff8b 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -84,7 +84,11 @@ let builtins = {
"__builtin_isync",
(TVoid [], [], false);
"__builtin_trap",
- (TVoid [], [], false)
+ (TVoid [], [], false);
+ "__builtin_lwar",
+ (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
+ "__builtin_stwc",
+ (TInt(IInt, []), [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false)
]
}
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 0192747..d2ec561 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -512,6 +512,8 @@ let print_instruction oc tbl pc fallthrough = function
fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl;
fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c);
float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals;
+ | Plwarx(r1, r2, r3) ->
+ fprintf oc " lwarx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Plwbrx(r1, r2, r3) ->
fprintf oc " lwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Plwz(r1, c, r2) | Plwz_a(r1, c, r2) ->
@@ -600,6 +602,8 @@ let print_instruction oc tbl pc fallthrough = function
fprintf oc " stwxu %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pstwbrx(r1, r2, r3) ->
fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
+ | Pstwcx_(r1, r2, r3) ->
+ fprintf oc " stwcx. %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Psubfc(r1, r2, r3) ->
fprintf oc " subfc %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Psubfe(r1, r2, r3) ->