Generate both Pcsel and Pfsel

In Asmblock, Pcsel is used for both integer and floating-point
conditional selection.
A previous commit (c764ff84) had incorrectly reverted the merging of
Pfsel into Pcsel.

1 files changed, 12 insertions, 1 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index dae9004d..ec680478 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -217,7 +217,18 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
 
   | PArith (Pcset rd c) => OK (Asm.Pcset rd c)
   | PArith (Pfmovi fsz rd r1) => OK (Asm.Pfmovi fsz rd r1)
-  | PArith (Pcsel rd r1 r2 c) => OK (Asm.Pcsel rd r1 r2 c)
+  | PArith (Pcsel rd r1 r2 c) =>
+      match r1, r2 with
+      | IR r1', IR r2' => do rd' <- ireg_of_preg rd;
+                          do r1'' <- ireg_of_preg r1';
+                          do r2'' <- ireg_of_preg r2';
+                          OK (Asm.Pcsel rd' r1'' r2'' c)
+      | FR r1', IR r2' => do rd' <- freg_of_preg rd;
+                          do r1'' <- freg_of_preg r1';
+                          do r2'' <- freg_of_preg r2';
+                          OK (Asm.Pfsel rd' r1'' r2'' c)
+      | _, _ => Error (msg "Asmgen.basic_to_instruction: Pcsel is only defind on iregs and fregs.")
+      end
   | PArith (Pfnmul fsz rd r1 r2) => OK (Asm.Pfnmul fsz rd r1 r2)
 
   | PLoad Pldrw       rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw     rd' a)