Now a more general way to perform imm operations

1 files changed, 9 insertions, 6 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index d4c6b73a..54c7a7c0 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -219,6 +219,12 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
   | Some false => sem r1 X0
   end.
 
+Definition get_opimmR0 (rd: ireg) (opi: opimm) :=
+  match opi with
+  | OPimmADD i => Paddiw rd X0 i
+  | OPimmADDL i => Paddil rd X0 i
+  end.
+
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
@@ -770,6 +776,9 @@ Definition transl_op
   | Ocmp cmp, _ =>
       do rd <- ireg_of res;
      transl_cond_op cmp rd args k
+  | OEimmR0 opi, nil =>
+      do rd <- ireg_of res;
+      OK (get_opimmR0 rd opi :: k)
   | OEseqw optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
       do rs1 <- ireg_of a1;
@@ -819,9 +828,6 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Paddiw rd rs n :: k)
-  | OEaddiwr0 n, nil =>
-      do rd <- ireg_of res;
-      OK (Paddiw rd X0 n :: k)
   | OEandiw n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
@@ -879,9 +885,6 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Paddil rd rs n :: k)
-  | OEaddilr0 n, nil =>
-      do rd <- ireg_of res;
-      OK (Paddil rd X0 n :: k)
   | OEandil n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;