32-bit rotate finished

7 files changed, 27 insertions, 6 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 31bc855d..5ed54a2b 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -171,7 +171,7 @@ Inductive instruction : Type :=
   | Psraiw              (rd rs: ireg) (imm: int)    (**r shift right arithmetic imm word *)

   | Psrliw              (rd rs: ireg) (imm: int)    (**r shift right logical imm word *)

   | Pslliw              (rd rs: ireg) (imm: int)    (**r shift left logical imm word *)

-

+  | Proriw              (rd rs: ireg) (imm: int)    (**r rotate right imm word *) 

   | Psllil              (rd rs: ireg) (imm: int)    (**r shift left logical immediate long *)

   | Psrlil              (rd rs: ireg) (imm: int)    (**r shift right logical immediate long *)

   | Psrail              (rd rs: ireg) (imm: int)    (**r shift right arithmetic immediate long *)

@@ -291,6 +291,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI32 Asmblock.Psraiw rd rs imm       => Psraiw rd rs imm

   | PArithRRI32 Asmblock.Psrliw rd rs imm       => Psrliw rd rs imm

   | PArithRRI32 Asmblock.Pslliw rd rs imm       => Pslliw rd rs imm

+  | PArithRRI32 Asmblock.Proriw rd rs imm       => Proriw rd rs imm

   | PArithRRI32 Asmblock.Psllil rd rs imm       => Psllil rd rs imm

   | PArithRRI32 Asmblock.Psrlil rd rs imm       => Psrlil rd rs imm

   | PArithRRI32 Asmblock.Psrail rd rs imm       => Psrail rd rs imm

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 621ed8a7..883cfb94 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -372,7 +372,7 @@ Inductive arith_name_rri32 : Type :=
   | Psraiw                                          (**r shift right arithmetic imm word *)
   | Psrliw                                          (**r shift right logical imm word *)
   | Pslliw                                          (**r shift left logical imm word *)
-
+  | Proriw                                          (**r rotate right imm word *)
   | Psllil                                          (**r shift left logical immediate long *)
   | Psrlil                                          (**r shift right logical immediate long *)
   | Psrail                                          (**r shift right arithmetic immediate long *)
@@ -1125,6 +1125,7 @@ Definition arith_eval_rri32 n v i :=
   | Psraiw  => Val.shr   v (Vint i)
   | Psrliw  => Val.shru  v (Vint i)
   | Pslliw  => Val.shl   v (Vint i)
+  | Proriw  => Val.ror   v (Vint i)
   | Psllil  => Val.shll  v (Vint i)
   | Psrlil  => Val.shrlu v (Vint i)
   | Psrail  => Val.shrl  v (Vint i)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index c6052337..19fca6c1 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1332,6 +1332,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   | Psraiw => "Psraiw"
   | Psrliw => "Psrliw"
   | Pslliw => "Pslliw"
+  | Proriw => "Proriw"
   | Psllil => "Psllil"
   | Psrlil => "Psrlil"
   | Psrail => "Psrail"
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 1c176538..26b1c6c1 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -471,7 +471,10 @@ Definition transl_op
           Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i
           Paddw RTMP rs RTMP ::i
           Psraiw rd RTMP n ::i k)
-
+  | Ororimm n, a1 :: nil =>
+    do rd <- ireg_of res; do rs <- ireg_of a1;
+      OK (Proriw rd rs n ::i k)
+         
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 9700776c..97108a90 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -91,6 +91,7 @@ let arith_rri32_str = function
   | Psraiw -> "Psraiw"
   | Psrliw -> "Psrliw"
   | Pslliw -> "Pslliw"
+  | Proriw -> "Proriw"
   | Psllil -> "Psllil"
   | Psrlil -> "Psrlil"
   | Psrail -> "Psrail"
@@ -375,7 +376,7 @@ let lsu_data_y : int array = let resmap = fun r -> match r with
 
 type real_instruction = 
   (* ALU *) 
-  | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
+  | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
@@ -409,6 +410,7 @@ let ab_inst_to_real = function
   | "Psrlw" | "Psrliw" -> Srlw
   | "Psrll" | "Psrlil" -> Srld
   | "Psllw" | "Pslliw" -> Sllw
+  | "Proriw" -> Rorw
   | "Pslll" | "Psllil" -> Slld
   | "Pxorw" | "Pxoriw" -> Xorw
   | "Pxorl" | "Pxoril" -> Xord
@@ -504,7 +506,7 @@ let rec_to_usage r =
                                 | Some U27L5 | Some U27L10 -> mau_x
                                 | Some E27U27L10 -> mau_y)
   | Nop -> alu_nop
-  | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
+  | Sraw | Srlw | Sllw | Rorw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
   | Sxwd | Zxwd -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
   | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 
@@ -523,7 +525,7 @@ let rec_to_usage r =
 
 let real_inst_to_latency = function
   | Nop -> 0 (* Only goes through ID *)
-  | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
+  | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw | Rorw
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
   | Sxwd | Zxwd | Fcompw | Fcompd
         -> 1
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 70d9ff6c..810808c2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -430,6 +430,9 @@ module Target (*: TARGET*) =
          fprintf oc "	srlw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pslliw (rd, rs, imm) ->
          fprintf oc "	sllw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Proriw (rd, rs, imm) ->
+         fprintf oc "	rorw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+
       | Psllil (rd, rs, imm) ->
          fprintf oc "	slld	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Psrlil (rd, rs, imm) ->
diff --git a/test/monniaux/rotate/rotate.c b/test/monniaux/rotate/rotate.c
new file mode 100644
index 00000000..96f20c49
--- /dev/null
+++ b/test/monniaux/rotate/rotate.c
@@ -0,0 +1,10 @@
+#include <stdio.h>
+
+unsigned rotate(unsigned x) {
+  return (x << 4) | (x >> (32-4));
+}
+
+int main() {
+  unsigned x = 0x12345678U;
+  printf("%X %X\n", x, rotate(x));
+}