diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 17:13:41 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 17:13:41 +0200 |
commit | 9fd4e33a6dd2c2dc88103711af62a7214dbd4109 (patch) | |
tree | b39d6da151bd4c8d79a8009395afb2b54dbc6860 /mppa_k1c | |
parent | d407e23fe62ce837082820f777564c0050cf66c1 (diff) | |
download | compcert-kvx-9fd4e33a6dd2c2dc88103711af62a7214dbd4109.tar.gz compcert-kvx-9fd4e33a6dd2c2dc88103711af62a7214dbd4109.zip |
Osub and Omul
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 6 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 6 |
3 files changed, 14 insertions, 2 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index c2f145aa..72bbff69 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -197,6 +197,8 @@ Inductive instruction : Type := (** 32-bit integer register-register instructions *) | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) + | Psubw (rd: ireg) (rs1 rs2: ireg) (**r integer subition *) + | 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 *) @@ -740,6 +742,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** 32-bit integer register-register instructions *) | Paddw d s1 s2 => Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m + | Psubw d s1 s2 => + Next (nextinstr (rs#d <- (Val.sub rs##s1 rs##s2))) m + | Pmulw d s1 s2 => + Next (nextinstr (rs#d <- (Val.mul rs##s1 rs##s2))) m | Pandw d s1 s2 => Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m | Pnegw d s => diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index f3fccca8..3984c43f 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -265,13 +265,13 @@ Definition transl_op | Oneg, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pnegw rd rs :: k) -(*| Osub, a1 :: a2 :: nil => + | Osub, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubw rd rs1 rs2 :: k) | Omul, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulw rd rs1 rs2 :: k) - | Omulhs, a1 :: a2 :: nil => +(*| Omulhs, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulhw rd rs1 rs2 :: k) | Omulhu, a1 :: a2 :: nil => diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 00129c97..ca26dbbe 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -211,6 +211,12 @@ module Target : TARGET = | Paddl(rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Psubw(rd, rs1, rs2) -> + fprintf oc " sbfwd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + + | Pmulw(rd, rs1, rs2) -> + fprintf oc " mulw %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Psrliw (rd, rs, imm) -> fprintf oc " srlw %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm | Psrlil (rd, rs, imm) -> |