aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--powerpc/Asm.v4
-rw-r--r--powerpc/AsmToJSON.ml2
-rw-r--r--powerpc/Asmexpand.ml58
-rw-r--r--powerpc/TargetPrinter.ml7
4 files changed, 19 insertions, 52 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 5fd40a27..3c7bdd15 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -153,8 +153,6 @@ Inductive instruction : Type :=
| Pbdnz: label -> instruction (**r decrement CTR and branch if not zero *)
| Pbf: crbit -> label -> instruction (**r branch if false *)
| Pbl: ident -> signature -> instruction (**r branch and link *)
- | Pbne: label -> instruction (**r branch not equal *)
- | Pbne_rel: int -> instruction (**r branch not equal with relative offset *)
| Pbs: ident -> signature -> instruction (**r branch to symbol *)
| Pblr: instruction (**r branch to contents of register LR *)
| Pbt: crbit -> label -> instruction (**r branch if true *)
@@ -875,8 +873,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
(** The following instructions and directives are not generated
directly by [Asmgen], so we do not model them. *)
| Pbdnz _
- | Pbne _
- | Pbne_rel _
| Pcmpb _ _ _
| Pcntlzw _ _
| Pcreqv _ _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index d23beaad..a7e66701 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -163,8 +163,6 @@ 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_label lbl
- | Pbne_rel ofs -> fprintf oc"{\"Instruction Name\":\"Pbne_rel\",\"Args\":[%a]}" p_int_constant ofs
| 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 23c66382..098eb49d 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -495,57 +495,32 @@ let expand_builtin_inline name args res =
emit (Plabel lbl);
emit (Plwarx (GPR11,GPR0,a1));
emit (Pstwcx_ (GPR10,GPR0,a1));
- emit (Pbne lbl);
+ emit (Pbf (CRbit_2,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 (Plwz (a1,Cint _0,a1));
emit (Pcmpw (a1,a1));
- emit (Pbne_rel _4);
+ emit (Pbf (CRbit_2,lbl));
+ emit (Plabel lbl);
emit (Pisync);
emit (Pstw (a1,Cint _0, a2));
- | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
+ | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], res ->
let lbl = new_label() in
+ let res = (match res with
+ | BR (IR res) -> res
+ | BR_none -> GPR3
+ | _ -> raise (Error ("unrecognized builtin " ^ name))) in
emit (Psync);
emit (Plabel lbl);
emit (Plwarx (res,GPR0,a1));
emit (Padd (GPR10,res,a2));
emit (Pstwcx_ (GPR10,GPR0,a1));
- emit (Pbne lbl);
- emit (Pisync);
- | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR_none ->
- let lbl = new_label() in
- emit (Psync);
- emit (Plabel lbl);
- emit (Plwarx (GPR3,GPR0,a1));
- emit (Padd (GPR10,GPR3,a2));
- emit (Pstwcx_ (GPR10,GPR0,a1));
- emit (Pbne lbl);
+ emit (Pbf (CRbit_2, lbl));
emit (Pisync);
- | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) ->
- let lbls = new_label ()
- and lblneq = new_label ()
- and lblsucc = new_label () in
- emit (Plwz (GPR10,Cint _0,exp));
- emit (Plwz (GPR11,Cint _0,des));
- emit (Psync);
- emit (Plabel lbls);
- emit (Plwarx (GPR12,GPR0,dst));
- emit (Pcmpw (GPR12,GPR10));
- emit (Pbne lblneq);
- emit (Pstwcx_ (GPR11,GPR0,dst));
- emit (Pbne lbls);
- emit (Plabel lblneq);
- emit (Pisync);
- emit (Pmfcr dst);
- emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
- emit (Pcmpwi (dst,(Cint _0)));
- emit (Pbne lblsucc);
- emit (Pstw (GPR12,(Cint _0),exp));
- emit (Plabel lblsucc);
- emit (Pmr (res,dst));
- | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR_none ->
+ | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], res ->
let lbls = new_label ()
and lblneq = new_label ()
and lblsucc = new_label () in
@@ -555,17 +530,22 @@ let expand_builtin_inline name args res =
emit (Plabel lbls);
emit (Plwarx (GPR12,GPR0,dst));
emit (Pcmpw (GPR12,GPR10));
- emit (Pbne lblneq);
+ emit (Pbf (CRbit_2,lblneq));
emit (Pstwcx_ (GPR11,GPR0,dst));
- emit (Pbne lbls);
+ emit (Pbf (CRbit_2,lbls));
emit (Plabel lblneq);
emit (Pisync);
emit (Pmfcr dst);
emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
emit (Pcmpwi (dst,(Cint _0)));
- emit (Pbne lblsucc);
+ emit (Pbf (CRbit_2,lblsucc));
emit (Pstw (GPR12,(Cint _0),exp));
emit (Plabel lblsucc);
+ (match res with
+ | BR_none -> ()
+ | BR (IR res) ->
+ emit (Pmr (res,dst))
+ | _ ->raise (Error ("unrecognized builtin " ^ name)))
(* Catch-all *)
| _ ->
raise (Error ("unrecognized builtin " ^ name))
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 1f1306c0..eca7a1b8 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -414,13 +414,6 @@ module Target (System : SYSTEM):TARGET =
end
| Pbl(s, sg) ->
fprintf oc " bl %a\n" symbol s
- | Pbne lbl ->
- fprintf oc " bne- %a\n" label (transl_label lbl)
- | Pbne_rel ofs ->
- let ofs = camlint_of_coqint ofs in
- let sign = if ofs >= 0l then "+" else "-" in
- let ofs = Int32.abs ofs in
- fprintf oc " bne- $%s%ld\n" sign ofs
| Pbs(s, sg) ->
fprintf oc " b %a\n" symbol s
| Pblr ->
generated by cgit (git 2.34.1) at 2024-07-06 03:46:11 +0000