Expansion of Ccompimm in RTL [Admitted checker]

1 files changed, 38 insertions, 2 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index b431d63d..8d1e3a5c 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -393,7 +393,14 @@ Definition transl_cond_op
 
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
-
+  
+Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) :=
+  match optR0 with
+  | None => sem r1 r2
+  | Some true => sem X0 r1
+  | Some false => sem r1 X0
+  end.
+  
 Definition transl_op
               (op: operation) (args: list mreg) (res: mreg) (k: code) :=
   match op, args with
@@ -708,7 +715,36 @@ Definition transl_op
   | Ocmp cmp, _ =>
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
-
+      
+  | OEseqw 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 (Pseqw rd) rs1 rs2 :: k)
+  | OEsnew 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 (Psnew rd) rs1 rs2 :: k)
+  | OEsltw 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 (Psltw rd) rs1 rs2 :: k)
+  | OEsltiw n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltiw rd rs n :: k)
+  | OExoriw n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Pxoriw rd rs n :: k)
+  | OEluiw n, nil =>
+      do rd <- ireg_of res;
+      OK (Pluiw rd n :: k)
+  | OEaddiwr0 n, nil =>
+      do rd <- ireg_of res;
+      OK (Paddiw rd X0 n :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.