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

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