aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-04-11 17:13:41 +0200
committerCyril SIX <cyril.six@kalray.eu>2018-04-11 17:13:41 +0200
commit9fd4e33a6dd2c2dc88103711af62a7214dbd4109 (patch)
treeb39d6da151bd4c8d79a8009395afb2b54dbc6860 /mppa_k1c
parentd407e23fe62ce837082820f777564c0050cf66c1 (diff)
downloadcompcert-kvx-9fd4e33a6dd2c2dc88103711af62a7214dbd4109.tar.gz
compcert-kvx-9fd4e33a6dd2c2dc88103711af62a7214dbd4109.zip
Osub and Omul
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asm.v6
-rw-r--r--mppa_k1c/Asmgen.v4
-rw-r--r--mppa_k1c/TargetPrinter.ml6
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) ->