Commit f73f3a4e authored by Cyril SIX's avatar Cyril SIX
Browse files

MPPA - added remaining ops ; mult, div and floating point ops missing

parent 7b3d2c0a
......@@ -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 =>
......
......@@ -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 =>
......
......@@ -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.
(*
......
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment