diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 14:38:06 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 14:38:06 +0200 |
commit | f73f3a4e5dda58408c82fe2657ddb251532ea894 (patch) | |
tree | c2357f7c06864719345ed6e3e9999ddf76cf6de4 | |
parent | 7b3d2c0ab46292a47256ff484b812d3d3b2846c2 (diff) | |
download | compcert-kvx-f73f3a4e5dda58408c82fe2657ddb251532ea894.tar.gz compcert-kvx-f73f3a4e5dda58408c82fe2657ddb251532ea894.zip |
MPPA - added remaining ops ; mult, div and floating point ops missing
-rw-r--r-- | mppa_k1c/Asm.v | 21 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 30 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 15 |
4 files changed, 57 insertions, 15 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d199495b..c0caed5d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -193,6 +193,8 @@ 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 *) + | Poriw (rd: ireg) (rs: ireg) (imm: int) (**r or immediate *) + | Pxoriw (rd: ireg) (rs: ireg) (imm: int) (**r xor 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 *) @@ -202,6 +204,8 @@ Inductive instruction : Type := | 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 *) + | Porw (rd: ireg) (rs1 rs2: ireg) (**r or word *) + | Pxorw (rd: ireg) (rs1 rs2: ireg) (**r xor word *) | 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 *) @@ -211,6 +215,7 @@ Inductive instruction : Type := | Paddil (rd: ireg) (rs: ireg) (imm: int64) (**r add immediate *) | Pandil (rd: ireg) (rs: ireg) (imm: int64) (**r and immediate *) | Poril (rd: ireg) (rs: ireg) (imm: int64) (**r or long immediate *) + | Pxoril (rd: ireg) (rs: ireg) (imm: int64) (**r xor long immediate *) | Psllil (rd: ireg) (rs: ireg) (imm: int) (**r shift left logical immediate long *) | Psrlil (rd: ireg) (rs: ireg) (imm: int) (**r shift right logical immediate long *) | Psrail (rd: ireg) (rs: ireg) (imm: int) (**r shift right arithmetic immediate long *) @@ -224,8 +229,10 @@ Inductive instruction : Type := (** 64-bit integer register-register instructions *) | Paddl (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) + | Psubl (rd: ireg) (rs1 rs2: ireg) (**r integer long subition *) | Pandl (rd: ireg) (rs1 rs2: ireg) (**r integer andition *) | Porl (rd: ireg) (rs1 rs2: ireg) (**r or long *) + | Pxorl (rd: ireg) (rs1 rs2: ireg) (**r xor 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 *) @@ -755,6 +762,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** 32-bit integer register-immediate instructions *) | Paddiw d s i => Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m + | Poriw d s i => + Next (nextinstr (rs#d <- (Val.or rs##s (Vint i)))) m + | Pxoriw d s i => + Next (nextinstr (rs#d <- (Val.xor rs##s (Vint i)))) m | Pandiw d s i => Next (nextinstr (rs#d <- (Val.and rs##s (Vint i)))) m | Psraiw d s i => @@ -773,6 +784,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out 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 + | Porw d s1 s2 => + Next (nextinstr (rs#d <- (Val.or rs##s1 rs##s2))) m + | Pxorw d s1 s2 => + Next (nextinstr (rs#d <- (Val.xor rs##s1 rs##s2))) m | Pnegw d s => Next (nextinstr (rs#d <- (Val.neg rs###s))) m | Psrlw d s1 s2 => @@ -789,6 +804,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m | Poril d s i => Next (nextinstr (rs#d <- (Val.orl rs###s (Vlong i)))) m + | Pxoril d s i => + Next (nextinstr (rs#d <- (Val.xorl rs###s (Vlong i)))) m | Psllil d s i => Next (nextinstr (rs#d <- (Val.shll rs###s (Vint i)))) m | Psrlil d s i => @@ -803,10 +820,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** 64-bit integer register-register instructions *) | Paddl d s1 s2 => Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m + | Psubl d s1 s2 => + Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m | Pandl d s1 s2 => Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m | Porl d s1 s2 => Next (nextinstr (rs#d <- (Val.orl rs###s1 rs###s2))) m + | Pxorl d s1 s2 => + Next (nextinstr (rs#d <- (Val.xorl rs###s1 rs###s2))) m | Pnegl d s => Next (nextinstr (rs#d <- (Val.negl rs###s))) m | Pmull d s1 s2 => diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 0adc41b5..744955de 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -83,9 +83,9 @@ Definition opimm32 (op: ireg -> ireg -> ireg -> instruction) Definition addimm32 := opimm32 Paddw Paddiw. Definition andimm32 := opimm32 Pandw Pandiw. -(* -Definition orimm32 := opimm32 Porw Poriw. +Definition orimm32 := opimm32 Porw Poriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. +(* Definition sltimm32 := opimm32 Psltw Psltiw. Definition sltuimm32 := opimm32 Psltuw Psltiuw. @@ -109,9 +109,9 @@ end. Definition addimm64 := opimm64 Paddl Paddil. Definition orimm64 := opimm64 Porl Poril. Definition andimm64 := opimm64 Pandl Pandil. +Definition xorimm64 := opimm64 Pxorl Pxoril. (* -Definition xorimm64 := opimm64 Pxorl Pxoril. Definition sltimm64 := opimm64 Psltl Psltil. Definition sltuimm64 := opimm64 Psltul Psltiul. *) @@ -310,13 +310,13 @@ Definition transl_op | Omodu, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Premuw rd rs1 rs2 :: k) - | Oand, a1 :: a2 :: nil => +*)| Oand, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandw rd rs1 rs2 :: k) -*)| Oandimm n, a1 :: nil => + | Oandimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (andimm32 rd rs n k) -(*| Oor, a1 :: a2 :: nil => + | Oor, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Porw rd rs1 rs2 :: k) | Oorimm n, a1 :: nil => @@ -328,7 +328,7 @@ 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 => @@ -374,10 +374,10 @@ Definition transl_op | Onegl, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pnegl rd rs :: k) -(*| Osubl, a1 :: a2 :: nil => + | 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 => @@ -398,25 +398,25 @@ Definition transl_op | Omodlu, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Premul rd rs1 rs2 :: k) - | Oandl, a1 :: a2 :: nil => +*)| Oandl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandl rd rs1 rs2 :: k) -*)| Oandlimm n, a1 :: nil => + | Oandlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (andimm64 rd rs n k) -(*| Oorl, a1 :: a2 :: nil => + | Oorl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Porl rd rs1 rs2 :: k) -*)| Oorlimm n, a1 :: nil => + | Oorlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (orimm64 rd rs n k) -(*| Oxorl, a1 :: a2 :: nil => + | Oxorl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pxorl rd rs1 rs2 :: k) | Oxorlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (xorimm64 rd rs n k) -*)| Oshll, a1 :: a2 :: nil => + | Oshll, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pslll rd rs1 rs2 :: k) | Oshllimm n, a1 :: nil => diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 04335726..32241542 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -323,6 +323,10 @@ Opaque Int.eq. - apply opimm32_label; intros; exact I. (* Oandimm32 *) - apply opimm32_label; intros; exact I. +(* Oorimm32 *) +- apply opimm32_label; intros; exact I. +(* Oxorimm32 *) +- apply opimm32_label; intros; exact I. (* Oshrximm *) - destruct (Int.eq n Int.zero); TailNoLabel. (* Oaddimm64 *) @@ -331,6 +335,8 @@ Opaque Int.eq. - apply opimm64_label; intros; exact I. (* Oorimm64 *) - apply opimm64_label; intros; exact I. +(* Oxorimm64 *) +- apply opimm64_label; intros; exact I. Qed. (* diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index b463a9c5..01a4e269 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -214,6 +214,8 @@ module Target : TARGET = fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 | Psubw(rd, rs1, rs2) -> + fprintf oc " sbfw %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Psubl(rd, rs1, rs2) -> fprintf oc " sbfwd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 | Pmulw(rd, rs1, rs2) -> @@ -250,6 +252,19 @@ module Target : TARGET = fprintf oc " ord %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm | Porl(rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " ord %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Poriw (rd, rs, imm) -> + fprintf oc " orw %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Porw(rd, rs1, rs2) -> + fprintf oc " orw %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + + | Pxoriw (rd, rs, imm) -> + fprintf oc " xorw %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Pxorw(rd, rs1, rs2) -> + fprintf oc " xorw %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Pxoril (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " xord %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Pxorl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " xord %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 | Pandiw (rd, rs, imm) -> fprintf oc " andd %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm |