From 49342474c19558709c8cea6d70eaba9a4dd7a150 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 15 Apr 2019 17:50:30 +0200
Subject: Implement a `Osel` operation for ARM

The operation comples down to conditional moves.
Both integer and floating-point conditional moves are supported.
---
 arm/Asmgen.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'arm/Asmgen.v')

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index f12ea870..1a1e7f2f 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -555,6 +555,19 @@ Definition transl_op
       do r <- ireg_of res;
       transl_cond cmp args
         (Pmovite (cond_for_cond cmp) r (SOimm Int.one) (SOimm Int.zero) :: k)
+  | Osel cmp ty, a1 :: a2 :: args =>
+      match preg_of res with
+      | IR r => 
+          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+          transl_cond cmp args
+            (Pmovite (cond_for_cond cmp) r (SOreg r1) (SOreg r2) :: k)
+      | FR r =>
+          do r1 <- freg_of a1; do r2 <- freg_of a2;
+          transl_cond cmp args
+            (Pfmovite (cond_for_cond cmp) r r1 r2 :: k)
+      | _ =>
+          Error(msg "Asmgen.Osel")
+      end
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
-- 
cgit