diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:35:01 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:35:01 +0200 |
| commit | 1ecd47e848d3073c7317dc39c4fa72dbac66dd60 (patch) | |
| tree | 5b3d09bd9d1481fd09c1e97f9e3f8d5f75e96c95 | |
| parent | a6c79438ae754d969558bd37eb3a7676be6e66aa (diff) | |
| download | compcert-kvx-1ecd47e848d3073c7317dc39c4fa72dbac66dd60.tar.gz compcert-kvx-1ecd47e848d3073c7317dc39c4fa72dbac66dd60.zip | |
MPPA - Oshr
| -rw-r--r-- | mppa_k1c/Asm.v | 3 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 |
3 files changed, 7 insertions, 2 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d7007102..c2f145aa 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -193,6 +193,7 @@ 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 *) @@ -743,6 +744,8 @@ 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 + | Psraw d s1 s2 => + Next (nextinstr (rs#d <- (Val.shr 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 828073f7..f3fccca8 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -313,10 +313,10 @@ Definition transl_op | 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 => diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 3e4c3ff6..00129c97 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -215,6 +215,8 @@ 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 + | Psraw (rd, rs1, rs2) -> + fprintf oc " sraw %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 | Poril (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " ord %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm |