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, 8 insertions, 0 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index e821c6c4..b9300fd7 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -231,6 +231,7 @@ Inductive instruction : Type :=
   | 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 *)
+  | Pfsel_gen: freg -> freg -> freg -> crbit -> instruction   (**r floating point 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 *)
@@ -867,6 +868,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
           | _ => Vundef
           end in
       Next (nextinstr (rs #rd <- v #GPR0 <- Vundef)) m
+  | Pfsel_gen rd r1 r2 bit =>
+      let v :=
+          match rs#(reg_of_crbit bit) with
+          | Vint n => if Int.eq n Int.zero then rs#r2 else rs#r1
+          | _ => Vundef
+          end in
+      Next (nextinstr (rs #rd <- v #GPR0 <- Vundef)) m
   | Plbz rd cst r1 =>
       load1 Mint8unsigned rd cst r1 rs m
   | Plbzx rd r1 r2 =>