Ccompu expansion

1 files changed, 9 insertions, 0 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 8d1e3a5c..17a2d3bb 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -731,10 +731,19 @@ Definition transl_op
       do rs1 <- ireg_of a1;
       do rs2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0 optR0 (Psltw rd) rs1 rs2 :: k)
+  | OEsltuw 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 (Psltuw rd) rs1 rs2 :: k)
   | OEsltiw n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Psltiw rd rs n :: k)
+  | OEsltiuw n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltiuw rd rs n :: k)
   | OExoriw n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;