MPPA - added all shifts

8 files changed, 42 insertions, 3 deletions

diff --git a/.gitignore b/.gitignore
index 99ec0c72..eeec81f8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,6 @@
 # Object files, in general
+**#*#
+**.swp
 **.bin
 **.out
 **.tok
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index bc8c07e4..f11a8cbe 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -193,7 +193,6 @@ Inductive instruction : Type :=
   | Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add immediate *)
   | Pandiw  (rd: ireg) (rs: ireg) (imm: int)        (**r and immediate *)
   | Psrliw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right logical immediate *)
-  | Psraw   (rd: ireg) (rs1 rs2: ireg)              (**r shift right arithmetic *)
 
 (** 32-bit integer register-register instructions *)
   | Paddw   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
@@ -201,12 +200,15 @@ Inductive instruction : Type :=
   | Pmulw   (rd: ireg) (rs1 rs2: ireg)              (**r integer mulition *)
   | Pandw   (rd: ireg) (rs1 rs2: ireg)              (**r integer andition *)
   | Pnegw   (rd: ireg) (rs: ireg)                   (**r negate word *)
+  | Psraw   (rd: ireg) (rs1 rs2: ireg)              (**r shift right arithmetic *)
 
 (** 64-bit integer register-immediate instructions *)
   | Paddil  (rd: ireg) (rs: ireg) (imm: int64)      (**r add immediate *) 
   | Pandil  (rd: ireg) (rs: ireg) (imm: int64)      (**r and immediate *) 
   | Poril   (rd: ireg) (rs: ireg) (imm: int64)      (**r or long immediate *) 
+  | Psllil  (rd: ireg) (rs: ireg) (imm: int)        (**r shift left logical immediate long *)
   | Psrlil  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right logical immediate long *)
+  | Psrail  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right arithmetic immediate long *)
   | Pmake   (rd: ireg)            (imm: int)        (**r load immediate *)
   | Pmakel  (rd: ireg)            (imm: int64)      (**r load immediate long *)
 
@@ -220,6 +222,9 @@ Inductive instruction : Type :=
   | Pandl   (rd: ireg) (rs1 rs2: ireg)              (**r integer andition *)
   | Porl    (rd: ireg) (rs1 rs2: ireg)              (**r or long *)
   | Pnegl   (rd: ireg) (rs: ireg)                   (**r negate long *)
+  | Pslll   (rd: ireg) (rs1 rs2: ireg)              (**r shift left logical long *)
+  | Psrll   (rd: ireg) (rs1 rs2: ireg)              (**r shift right logical long *)
+  | Psral   (rd: ireg) (rs1 rs2: ireg)              (**r shift right arithmetic long *)
 
   (* Unconditional jumps.  Links are always to X1/RA. *)
   | Pj_l    (l: label)                              (**r jump to label *)
@@ -770,8 +775,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m
   | Poril  d s i =>
       Next (nextinstr (rs#d <- (Val.orl  rs###s (Vlong i)))) m
+  | Psllil  d s i =>
+      Next (nextinstr (rs#d <- (Val.shll  rs###s (Vint i)))) m
   | Psrlil  d s i =>
       Next (nextinstr (rs#d <- (Val.shrlu  rs###s (Vint i)))) m
+  | Psrail d s i =>
+      Next (nextinstr (rs#d <- (Val.shrl rs###s (Vint i)))) m
   | Pmakel d i =>
       Next (nextinstr (rs#d <- (Vlong i))) m
   | Pmake d i =>
@@ -786,6 +795,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.orl  rs###s1 rs###s2))) m
   | Pnegl d s =>
       Next (nextinstr (rs#d <- (Val.negl rs###s))) m
+  | Pslll d s1 s2 =>
+      Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m
+  | Psrll d s1 s2 =>
+      Next (nextinstr (rs#d <- (Val.shrlu rs###s1 rs###s2))) m
+  | Psral d s1 s2 =>
+      Next (nextinstr (rs#d <- (Val.shrl rs###s1 rs###s2))) m
 
 (** Conversions *)
   | Pcvtl2w d s =>
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 0f0d3e41..12cdb114 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -416,7 +416,7 @@ Definition transl_op
   | Oxorlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (xorimm64 rd rs n k)
-  | Oshll, a1 :: a2 :: nil =>
+*)| Oshll, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pslll rd rs1 rs2 :: k)
   | Oshllimm n, a1 :: nil =>
@@ -431,7 +431,7 @@ Definition transl_op
   | Oshrlu, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psrll rd rs1 rs2 :: k)
-*)| Oshrluimm n, a1 :: nil =>
+  | Oshrluimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Psrlil rd rs n :: k)
 (*| Oshrxlimm n, a1 :: nil =>
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index af7b7b30..0f242eda 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -221,8 +221,18 @@ module Target : TARGET =
          fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Psrlil (rd, rs, imm) ->
          fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Psrll (rd, rs1, rs2) ->
+         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psllil (rd, rs, imm) ->
+         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pslll (rd, rs1, rs2) ->
+         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psraw  (rd, rs1, rs2) ->
          fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psral  (rd, rs1, rs2) ->
+         fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psrail  (rd, rs1, imm) ->
+         fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs1 coqint64 imm
 
       | Poril (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
diff --git a/test/mppa/.gitignore b/test/mppa/.gitignore
new file mode 100644
index 00000000..f03fc12c
--- /dev/null
+++ b/test/mppa/.gitignore
@@ -0,0 +1 @@
+check
diff --git a/test/mppa/general/.gitignore b/test/mppa/general/.gitignore
new file mode 100644
index 00000000..ea1472ec
--- /dev/null
+++ b/test/mppa/general/.gitignore
@@ -0,0 +1 @@
+output/
diff --git a/test/mppa/lib/.gitignore b/test/mppa/lib/.gitignore
new file mode 100644
index 00000000..1879eaee
--- /dev/null
+++ b/test/mppa/lib/.gitignore
@@ -0,0 +1,2 @@
+prng-test-k1c
+prng-test-x86
diff --git a/test/mppa/sort/.gitignore b/test/mppa/sort/.gitignore
new file mode 100644
index 00000000..e7dc9aa0
--- /dev/null
+++ b/test/mppa/sort/.gitignore
@@ -0,0 +1,8 @@
+insertion-test-k1c
+insertion-test-x86
+merge-test-k1c
+selection-test-k1c
+test-k1c
+merge-test-x86
+selection-test-x86
+test-x86