From 626ea26cb58e50e7a42f90a6e23218d90df6dd5a Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 20 Aug 2014 14:24:42 +0000 Subject: 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 --- powerpc/PrintAsm.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'powerpc/PrintAsm.ml') 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) -> -- cgit v1.2.3