From 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 3 Feb 2021 17:14:23 +0100
Subject: All Ocmp expanded in RTL

---
 riscV/Asmgen.v | 44 +++++++++++++++++++++++++++++++++++++-------
 1 file changed, 37 insertions(+), 7 deletions(-)

(limited to 'riscV/Asmgen.v')

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index f702d11a..b3fb2350 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -344,10 +344,10 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
   | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
   end.
 
-Definition transl_cond_op
+(* TODO Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
   match cond, args with
-  (* TODO | Ccomp c, a1 :: a2 :: nil =>
+  | Ccomp c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (transl_cond_int32s c rd r1 r2 k)
   | Ccompu c, a1 :: a2 :: nil =>
@@ -370,7 +370,7 @@ Definition transl_cond_op
       OK (transl_condimm_int64s c rd r1 n k)
   | Ccompluimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
-     OK (transl_condimm_int64u c rd r1 n k)*)
+     OK (transl_condimm_int64u c rd r1 n k)
   | Ccompf c, f1 :: f2 :: nil =>
       do r1 <- freg_of f1; do r2 <- freg_of f2;
       let (insn, normal) := transl_cond_float c rd r1 r2 in
@@ -386,10 +386,10 @@ Definition transl_cond_op
   | Cnotcompfs c, f1 :: f2 :: nil =>
       do r1 <- freg_of f1; do r2 <- freg_of f2;
       let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
+     OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
   | _, _ =>
       Error(msg "Asmgen.transl_cond_op")
-  end.
+              end.*)
 
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
@@ -712,9 +712,9 @@ Definition transl_op
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
 
-  | Ocmp cmp, _ =>
+      (* TODO | Ocmp cmp, _ =>
       do rd <- ireg_of res;
-      transl_cond_op cmp rd args k
+         transl_cond_op cmp rd args k*)
       
   | OEseqw optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
@@ -795,6 +795,36 @@ Definition transl_op
   | OEloadli n, nil =>
       do rd <- ireg_of res;
       OK (Ploadli rd n :: k)
+  | OEfeqd, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfeqd rd r1 r2 :: k)
+  | OEfltd, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfltd rd r1 r2 :: k)
+  | OEfled, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfled rd r1 r2 :: k)
+  | OEfeqs, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfeqs rd r1 r2 :: k)
+  | OEflts, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pflts rd r1 r2 :: k)
+  | OEfles, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfles rd r1 r2 :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
-- 
cgit