Provide a float select operation for PowerPC. (#173)

The FP select for PowerPC stores both addresses in two
subsequent stack slots and loads them using an offset created
from the result of the comparison.

1 files changed, 18 insertions, 1 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 62efc17f..a686414a 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -416,6 +416,16 @@ Definition transl_select_op
     let r2' := if snd p then r2 else r1 in
     transl_cond cond args (Pisel rd r1' r2' (fst p) :: k)).
 
+Definition transl_fselect_op
+              (cond: condition) (args: list mreg) (r1 r2 rd: freg) (k: code) :=
+  if freg_eq r1 r2 then
+    OK (Pfmr rd r1 :: k)
+  else
+   (let p := crbit_for_cond cond in
+    let r1' := if snd p then r1 else r2 in
+    let r2' := if snd p then r2 else r1 in
+    transl_cond cond args (Pfsel_gen rd r1' r2' (fst p) :: k)).
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -623,9 +633,16 @@ Definition transl_op
   | Ocmp cmp, _ =>
       transl_cond_op cmp args res k
   | Osel cmp ty, a1 :: a2 :: args =>
-      assertion (typ_eq ty Tint || typ_eq ty Tlong);
+      match preg_of res with
+      | IR r1 =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
       transl_select_op cmp args r1 r2 r k
+      | FR r =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      transl_fselect_op cmp args r1 r2 r k
+      | _ =>
+        Error (msg "Asmgen.Osel")
+      end
 (*c PPC64 operations *)
   | Olongconst n, nil =>
       do r <- ireg_of res; OK (loadimm64 r n k)