Ccomp for long

1 files changed, 44 insertions, 3 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 17a2d3bb..f702d11a 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -347,7 +347,7 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
 Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
   match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
+  (* TODO | 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 =>
@@ -364,13 +364,13 @@ Definition transl_cond_op
       OK (transl_cond_int64s c rd r1 r2 k)
   | Ccomplu c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64u c rd r1 r2 k)
+     OK (transl_cond_int64u c rd r1 r2 k)
   | Ccomplimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       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
@@ -754,6 +754,47 @@ Definition transl_op
   | OEaddiwr0 n, nil =>
       do rd <- ireg_of res;
       OK (Paddiw rd X0 n :: k)
+  | OEseql optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Pseql rd) rs1 rs2 :: k)
+  | OEsnel optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k)
+  | OEsltl optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psltl rd) rs1 rs2 :: k)
+  | OEsltul optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psltul rd) rs1 rs2 :: k)
+  | OEsltil n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltil rd rs n :: k)
+  | OEsltiul n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltiul rd rs n :: k)
+  | OExoril n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Pxoril rd rs n :: k)
+  | OEluil n, nil =>
+      do rd <- ireg_of res;
+      OK (Pluil rd n :: k)
+  | OEaddilr0 n, nil =>
+      do rd <- ireg_of res;
+      OK (Paddil rd X0 n :: k)
+  | OEloadli n, nil =>
+      do rd <- ireg_of res;
+      OK (Ploadli rd n :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.