diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 16:30:26 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 16:30:26 +0200 |
commit | 3997c0bc61ddbbceefd449a8007e7212add8ac4a (patch) | |
tree | f75c6a9409ee76b6f628f012a88f1c4e293b7f85 /mppa_k1c | |
parent | 8a77a2d41eb560ce9dbc3669971ccbc342743784 (diff) | |
download | compcert-kvx-3997c0bc61ddbbceefd449a8007e7212add8ac4a.tar.gz compcert-kvx-3997c0bc61ddbbceefd449a8007e7212add8ac4a.zip |
MPPA - added all shifts
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 17 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 10 |
3 files changed, 28 insertions, 3 deletions
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 |