Added builtin for isel.

The builtin_isel function takes a _Bool as first argument and returns
either the second or the third depending on the value of the _Bool.

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) ->