diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-20 14:24:42 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-20 14:24:42 +0000 |
commit | 626ea26cb58e50e7a42f90a6e23218d90df6dd5a (patch) | |
tree | e8214df04ff25411e435210beb8e9e188683b113 /powerpc/PrintAsm.ml | |
parent | e2fa973a4bfea5d47b0d9f41b8734a7b6744dc18 (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/PrintAsm.ml')
-rw-r--r-- | powerpc/PrintAsm.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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) -> |