diff options
-rw-r--r-- | powerpc/Asm.v | 2 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 1 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 4 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 5 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 2 |
5 files changed, 13 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 796bad3d..3c7bdd15 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -207,6 +207,7 @@ Inductive instruction : Type := | Pfrsqrte: freg -> freg -> instruction (**r approximate reciprocal of square root *) | Pfres: freg -> freg -> instruction (**r approximate inverse *) | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) + | Pisel: ireg -> ireg -> ireg -> crbit -> instruction (**r integer select *) | Pisync: instruction (**r ISYNC barrier *) | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) | Picbtls: int -> ireg -> ireg -> instruction (**r instruction cache block touch and lock set *) @@ -893,6 +894,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfrsqrte _ _ | Pfres _ _ | Pfsel _ _ _ _ + | Pisel _ _ _ _ | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 8f2b4dc2..3ed36c4d 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -217,6 +217,7 @@ let p_instruction oc ic = | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pisel (ir1,ir2,ir3,cr) -> fprintf oc "{\"Instruction Name\":\"Pisel\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 p_crbit cr | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Picbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2 | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 929e6325..3fffc037 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -483,6 +483,10 @@ let expand_builtin_inline name args res = emit (Plwz(res, Cint ofs, GPR1)) | "__builtin_return_address",_,BR (IR res) -> emit (Plwz (res, Cint! retaddr_offset,GPR1)) + (* isel *) + | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> + emit (Pcmpwi (a1,Cint (Int.zero))); + emit (Pisel (res,a3,a2,CRbit_2)) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 6d7b2aff..e219a175 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -115,7 +115,10 @@ let builtins = { "__builtin_call_frame", (TPtr (TVoid [],[]),[],false); "__builtin_return_address", - (TPtr (TVoid [],[]),[],false) + (TPtr (TVoid [],[]),[],false); + (* isel *) + "__builtin_isel", + (TInt (IInt, []),[TInt(IInt, []);TInt(IInt, []);TInt(IInt, [])],false) ] } diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index cdb7aa97..eca7a1b8 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -538,6 +538,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fres %a, %a\n" freg r1 freg r2 | Pfsel(r1, r2, r3, r4) -> fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pisel (r1,r2,r3,cr) -> + fprintf oc " isel %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 crbit cr | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 | Picbtls (n,r1,r2) -> |