diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:03:52 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:03:52 +0200 |
| commit | b63085295d8495ff640f5eaff8b8ad52fc5c43d1 (patch) | |
| tree | fb854f158307f9a5185e92959e63df470566d538 /mppa_k1c | |
| parent | b17acc2e5f9c31a93164897c64c698fe8e490765 (diff) | |
| download | compcert-kvx-b63085295d8495ff640f5eaff8b8ad52fc5c43d1.tar.gz compcert-kvx-b63085295d8495ff640f5eaff8b8ad52fc5c43d1.zip | |
MPPA - More shifts
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 12 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 8 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 8 |
3 files changed, 24 insertions, 4 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f11a8cbe..b2272f7a 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -192,7 +192,9 @@ Inductive instruction : Type := (** 32-bit integer register-immediate instructions *) | Paddiw (rd: ireg) (rs: ireg) (imm: int) (**r add immediate *) | Pandiw (rd: ireg) (rs: ireg) (imm: int) (**r and immediate *) + | Psraiw (rd: ireg) (rs: ireg) (imm: int) (**r shift right arithmetic immediate *) | Psrliw (rd: ireg) (rs: ireg) (imm: int) (**r shift right logical immediate *) + | Pslliw (rd: ireg) (rs: ireg) (imm: int) (**r shift left logical immediate *) (** 32-bit integer register-register instructions *) | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) @@ -201,6 +203,8 @@ Inductive instruction : Type := | 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 *) + | Psrlw (rd: ireg) (rs1 rs2: ireg) (**r shift right logical *) + | Psllw (rd: ireg) (rs1 rs2: ireg) (**r shift left logical word *) (** 64-bit integer register-immediate instructions *) | Paddil (rd: ireg) (rs: ireg) (imm: int64) (**r add immediate *) @@ -751,8 +755,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m | Pandiw d s i => Next (nextinstr (rs#d <- (Val.and rs##s (Vint i)))) m + | Psraiw d s i => + Next (nextinstr (rs#d <- (Val.shr rs##s (Vint i)))) m | Psrliw d s i => Next (nextinstr (rs#d <- (Val.shru rs##s (Vint i)))) m + | Pslliw d s i => + Next (nextinstr (rs#d <- (Val.shl rs##s (Vint i)))) m (** 32-bit integer register-register instructions *) | Paddw d s1 s2 => @@ -765,8 +773,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m | Pnegw d s => Next (nextinstr (rs#d <- (Val.neg rs###s))) m + | Psrlw d s1 s2 => + Next (nextinstr (rs#d <- (Val.shru rs##s1 rs##s2))) m | Psraw d s1 s2 => Next (nextinstr (rs#d <- (Val.shr rs##s1 rs##s2))) m + | Psllw d s1 s2 => + Next (nextinstr (rs#d <- (Val.shl rs##s1 rs##s2))) m (** 64-bit integer register-immediate instructions *) | Paddil d s i => diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 12cdb114..98253ab3 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -328,22 +328,22 @@ Definition transl_op | Oxorimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (xorimm32 rd rs n k) - | Oshl, a1 :: a2 :: nil => +*)| Oshl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psllw rd rs1 rs2 :: k) | Oshlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pslliw rd rs n :: k) -*)| Oshr, a1 :: a2 :: nil => + | Oshr, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psraw rd rs1 rs2 :: k) -(*| Oshrimm n, a1 :: nil => + | Oshrimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psraiw rd rs n :: k) | Oshru, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psrlw rd rs1 rs2 :: k) -*)| Oshruimm n, a1 :: nil => + | Oshruimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psrliw rd rs n :: k) (*| Oshrximm n, a1 :: nil => diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 0f242eda..977d3019 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -223,12 +223,20 @@ module Target : TARGET = 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 + | Psrlw (rd, rs1, rs2) -> + fprintf oc " srlw %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Pslliw (rd, rs, imm) -> + fprintf oc " sllw %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Psllw (rd, rs1, rs2) -> + fprintf oc " sllw %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 + | Psraiw (rd, rs1, imm) -> + fprintf oc " sraw %a = %a, %a\n;;\n" ireg rd ireg rs1 coqint64 imm | Psral (rd, rs1, rs2) -> fprintf oc " srad %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 | Psrail (rd, rs1, imm) -> |