diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:28:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:28:51 +0200 |
| commit | eb3fd167668695c33f776cbb381c7664c3ec1858 (patch) | |
| tree | e7bcfaa9fc18a8755d8fa983d3e8a8d18f1d89f1 /mppa_k1c | |
| parent | 139595171a98e6722503202a2a8fb7c000f267c2 (diff) | |
| download | compcert-kvx-eb3fd167668695c33f776cbb381c7664c3ec1858.tar.gz compcert-kvx-eb3fd167668695c33f776cbb381c7664c3ec1858.zip | |
MPPA - Added Pmull -> now able to run the sort test
Diffstat (limited to 'mppa_k1c')
| -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 b2272f7a..f8ab1e8d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -226,6 +226,7 @@ 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 *) + | Pmull (rd: ireg) (rs1 rs2: ireg) (**r integer mulition long (low part) *) | 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 *) @@ -807,6 +808,8 @@ 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 + | Pmull d s1 s2 => + Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m | Pslll d s1 s2 => Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m | Psrll d s1 s2 => diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 9025a00d..d17ba14b 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -377,10 +377,10 @@ Definition transl_op (*| Osubl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubl rd rs1 rs2 :: k) - | Omull, a1 :: a2 :: nil => +*)| Omull, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmull rd rs1 rs2 :: k) - | Omullhs, a1 :: a2 :: nil => +(*| Omullhs, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulhl rd rs1 rs2 :: k) | Omullhu, a1 :: a2 :: nil => diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index cb3b558c..4c3bf3c6 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -216,6 +216,8 @@ module Target : TARGET = | Pmulw(rd, rs1, rs2) -> fprintf oc " mulw %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Pmull(rd, rs1, rs2) -> + fprintf oc " muld %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 |