diff options
-rw-r--r-- | powerpc/Asm.v | 4 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 2 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 58 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 7 |
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 -> |