From 3997c0bc61ddbbceefd449a8007e7212add8ac4a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 17 Apr 2018 16:30:26 +0200 Subject: MPPA - added all shifts --- .gitignore | 2 ++ mppa_k1c/Asm.v | 17 ++++++++++++++++- mppa_k1c/Asmgen.v | 4 ++-- mppa_k1c/TargetPrinter.ml | 10 ++++++++++ test/mppa/.gitignore | 1 + test/mppa/general/.gitignore | 1 + test/mppa/lib/.gitignore | 2 ++ test/mppa/sort/.gitignore | 8 ++++++++ 8 files changed, 42 insertions(+), 3 deletions(-) create mode 100644 test/mppa/.gitignore create mode 100644 test/mppa/general/.gitignore create mode 100644 test/mppa/lib/.gitignore create mode 100644 test/mppa/sort/.gitignore 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 -- cgit