Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work

1 files changed, 25 insertions, 0 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 4876f7ec..252a9270 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -899,6 +899,31 @@ Definition transl_op
       do r1 <- freg_of f1;
       do r2 <- freg_of f2;
       OK (Pfles rd r1 r2 :: k)
+
+  | Obits_of_single, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfmvxs rd rs :: k)
+  | Obits_of_float, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfmvxd rd rs :: k)
+  | Osingle_of_bits, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfmvsx rd rs :: k)
+  | Ofloat_of_bits, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfmvdx rd rs :: k)
+                               
+  | Ocmp cmp, _ =>
+      do rd <- ireg_of res;
+      transl_cond_op cmp rd args k
+
+  | Oselectl, b::t::f::nil =>
+      do rd <- ireg_of res;
+      do rb <- ireg_of b;
+      do rt <- ireg_of t;
+      do rf <- ireg_of f;
+      OK (Pselectl rd rb rt rf :: k)
+         
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.