MPPA - Activated Paddw and Paddiw + ops

4 files changed, 22 insertions, 21 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 4693975b..42b5f85f 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -144,8 +144,8 @@ Inductive instruction : Type :=
   | Pmv     (rd: ireg) (rs: ireg)                    (**r integer move *)
 
 (** 32-bit integer register-immediate instructions *)
-(*| Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add immediate *)
-  | Psltiw  (rd: ireg) (rs: ireg) (imm: int)        (**r set-less-than immediate *)
+  | Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add immediate *)
+(*| Psltiw  (rd: ireg) (rs: ireg) (imm: int)        (**r set-less-than immediate *)
   | Psltiuw (rd: ireg) (rs: ireg) (imm: int)        (**r set-less-than unsigned immediate *)
   | Pandiw  (rd: ireg) (rs: ireg) (imm: int)        (**r and immediate *)
   | Poriw   (rd: ireg) (rs: ireg) (imm: int)        (**r or immediate *)
@@ -155,8 +155,8 @@ Inductive instruction : Type :=
   | Psraiw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift-right-arith immediate *)
   | Pluiw   (rd: ireg)             (imm: int)        (**r load upper-immediate *)
 (** 32-bit integer register-register instructions *)
-  | Paddw   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
-  | Psubw   (rd: ireg) (rs1 rs2: ireg)              (**r integer subtraction *)
+*)| Paddw   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
+(*| Psubw   (rd: ireg) (rs1 rs2: ireg)              (**r integer subtraction *)
 
   | Pmulw   (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply low *)
   | Pmulhw  (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply high signed *)
@@ -629,9 +629,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (rs#s))) m
 
 (** 32-bit integer register-immediate instructions *)
-(*| Paddiw d s i =>
+  | Paddiw d s i =>
       Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m
-  | Psltiw d s i =>
+(*| Psltiw d s i =>
       Next (nextinstr (rs#d <- (Val.cmp Clt rs##s (Vint i)))) m
   | Psltiuw d s i =>
       Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Clt rs##s (Vint i)))) m
@@ -651,9 +651,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Vint (Int.shl i (Int.repr 12))))) m
 
 (** 32-bit integer register-register instructions *)
-  | Paddw d s1 s2 =>
+*)| Paddw d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m
-  | Psubw d s1 s2 =>
+(*| 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
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 82779bf4..96246bc2 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -73,16 +73,16 @@ Definition loadimm32 (r: ireg) (n: int) (k: code) :=
   match make_immed32 n with
   | Imm32_single imm => Pmake r imm :: k
   end.
-(*
+
 Definition opimm32 (op: ireg -> ireg -> ireg -> instruction)
                    (opimm: ireg -> ireg -> int -> instruction)
                    (rd rs: ireg) (n: int) (k: code) :=
   match make_immed32 n with
   | Imm32_single imm => opimm rd rs imm :: k
-  | Imm32_pair hi lo => load_hilo32 GPR31 hi lo (op rd rs GPR31 :: k)
   end.
 
 Definition addimm32 := opimm32 Paddw Paddiw.
+(*
 Definition andimm32 := opimm32 Pandw Pandiw.
 Definition orimm32  := opimm32 Porw  Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
@@ -414,13 +414,13 @@ Definition transl_op
   | Ocast16signed, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Pslliw rd rs (Int.repr 16) :: Psraiw rd rd (Int.repr 16) :: k)
-  | Oadd, a1 :: a2 :: nil =>
+*)| Oadd, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Paddw rd rs1 rs2 :: k)
   | Oaddimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (addimm32 rd rs n k)
-  | Oneg, a1 :: nil =>
+(*| Oneg, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Psubw rd GPR0 rs :: k)
   | Osub, a1 :: a2 :: nil =>
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 45531e00..414527ad 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -122,7 +122,7 @@ Proof.
 (*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)
 Qed.
 Hint Resolve loadimm32_label: labels.
-(*
+
 Remark opimm32_label:
   forall op opimm r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
@@ -130,10 +130,10 @@ Remark opimm32_label:
   tail_nolabel k (opimm32 op opimm r1 r2 n k).
 Proof.
   intros; unfold opimm32. destruct (make_immed32 n); TailNoLabel.
-  unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.
+(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)
 Qed.
 Hint Resolve opimm32_label: labels.
-*)
+
 Remark loadimm64_label:
   forall r n k, tail_nolabel k (loadimm64 r n k).
 Proof.
@@ -277,6 +277,7 @@ Remark transl_op_label:
 Proof.
 Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
+- apply opimm32_label; intros; exact I.
 - apply opimm64_label; intros; exact I.
 Qed.
 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index e51ad51f..71d2f22d 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -168,9 +168,9 @@ module Target : TARGET =
          fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
 
       (* 32-bit integer register-immediate instructions *)
-    (*| Paddiw (rd, rs, imm) ->
-         fprintf oc "	addi%t	%a, %a, %a\n" w ireg rd ireg rs coqint imm
-      | Psltiw (rd, rs, imm) ->
+      | Paddiw (rd, rs, imm) ->
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+    (*| Psltiw (rd, rs, imm) ->
          fprintf oc "	slti	%a, %a, %a\n" ireg rd ireg rs coqint imm
       | Psltiuw (rd, rs, imm) ->
          fprintf oc "	sltiu	%a, %a, %a\n" ireg rd ireg rs coqint imm
@@ -190,9 +190,9 @@ module Target : TARGET =
          fprintf oc "	lui	%a, %a\n"     ireg rd coqint imm
 
       (* 32-bit integer register-register instructions *)
-      | Paddw(rd, rs1, rs2) ->
-         fprintf oc "	add%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-      | Psubw(rd, rs1, rs2) ->
+    *)| Paddw(rd, rs1, rs2) ->
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+    (*| Psubw(rd, rs1, rs2) ->
          fprintf oc "	sub%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
 
       | Pmulw(rd, rs1, rs2) ->