MPPA - Added Mgetstack, loadind, a bunch of loads

5 files changed, 33 insertions, 32 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 59b1a139..521027ae 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -242,12 +242,12 @@ Inductive instruction : Type :=
   | Plbu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load unsigned int8 *)
   | Plh     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load signed int16 *)
   | Plhu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load unsigned int16 *)
-  | Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)
+*)| Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)
   | Plw_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any32 *)
-*)| Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)
-(*| Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)
+  | Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)
+  | Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)
 
-  | Psb     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int8 *)
+(*| Psb     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int8 *)
   | Psh     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int16 *)
   | Psw     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)
   | Psw_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any32 *)
@@ -263,8 +263,8 @@ Inductive instruction : Type :=
   | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
 
   (* 32-bit (single-precision) floating point *)
-  | Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
-  | Pfss     (rs: freg) (ra: ireg) (ofs: offset)    (**r store float *)
+*)| Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
+(*| Pfss     (rs: freg) (ra: ireg) (ofs: offset)    (**r store float *)
 
   | Pfnegs   (rd: freg) (rs: freg)                  (**r negation *)
   | Pfabss   (rd: freg) (rs: freg)                  (**r absolute value *)
@@ -298,8 +298,8 @@ Inductive instruction : Type :=
   | Pfcvtslu (rd: freg) (rs: ireg)                 (**r unsigned int 64-> float32 conversion *)
 
   (* 64-bit (double-precision) floating point *)
-  | Pfld     (rd: freg) (ra: ireg) (ofs: offset)    (**r load 64-bit float *)
-  | Pfld_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r load any64 *)
+*)| Pfld     (rd: freg) (ra: ireg) (ofs: offset)    (**r load 64-bit float *)
+(*| Pfld_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r load any64 *)
   | Pfsd     (rd: freg) (ra: ireg) (ofs: offset)    (**r store 64-bit float *)
   | Pfsd_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r store any64 *)
 
@@ -825,15 +825,15 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_load Mint16signed rs m d a ofs
   | Plhu d a ofs =>
       exec_load Mint16unsigned rs m d a ofs
-  | Plw d a ofs =>
+*)| Plw d a ofs =>
       exec_load Mint32 rs m d a ofs
   | Plw_a d a ofs =>
       exec_load Many32 rs m d a ofs
-*)| Pld d a ofs =>
+  | Pld d a ofs =>
       exec_load Mint64 rs m d a ofs
-(*| Pld_a d a ofs =>
+  | Pld_a d a ofs =>
       exec_load Many64 rs m d a ofs
-  | Psb s a ofs =>
+(*| Psb s a ofs =>
       exec_store Mint8unsigned rs m s a ofs
   | Psh s a ofs =>
       exec_store Mint16unsigned rs m s a ofs
@@ -851,9 +851,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (rs#s))) m
 
 (** 32-bit (single-precision) floating point *)
-  | Pfls d a ofs =>
+*)| Pfls d a ofs =>
       exec_load Mfloat32 rs m d a ofs
-  | Pfss s a ofs =>
+(*| Pfss s a ofs =>
       exec_store Mfloat32 rs m s a ofs
 
   | Pfnegs d s =>
@@ -895,9 +895,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.maketotal (Val.singleoflongu rs###s)))) m
 
 (** 64-bit (double-precision) floating point *)
-  | Pfld d a ofs =>
+*)| Pfld d a ofs =>
       exec_load Mfloat64 rs m d a ofs
-  | Pfld_a d a ofs =>
+(*| Pfld_a d a ofs =>
       exec_load Many64 rs m d a ofs
   | Pfsd s a ofs =>
       exec_store Mfloat64 rs m s a ofs
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 300f21a2..33442dd0 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -696,7 +696,7 @@ Definition indexed_memory_access
   | Imm64_large imm =>
       Pmake GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k
 *)end.
-(*
+
 Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
   match ty, preg_of dst with
   | Tint,    IR rd => OK (indexed_memory_access (Plw rd) base ofs k)
@@ -707,7 +707,7 @@ Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
   | Tany64,  IR rd => OK (indexed_memory_access (Pld_a rd) base ofs k)
   | _, _           => Error (msg "Asmgen.loadind")
   end.
-
+(*
 Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :=
   match ty, preg_of src with
   | Tint,    IR rd => OK (indexed_memory_access (Psw rd) base ofs k)
@@ -810,9 +810,9 @@ Definition make_epilogue (f: Mach.function) (k: code) :=
 Definition transl_instr (f: Mach.function) (i: Mach.instruction)
                         (ep: bool) (k: code) :=
   match i with
-(*| Mgetstack ofs ty dst =>
+  | Mgetstack ofs ty dst =>
       loadind SP ofs ty dst k
-  | Msetstack src ofs ty =>
+(*| Msetstack src ofs ty =>
       storeind src SP ofs ty k
   | Mgetparam ofs ty dst =>
       (* load via the frame pointer if it is valid *)
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 213cb5d6..d3fcc7f7 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -311,7 +311,7 @@ Proof.
   destruct (make_immed64 (Ptrofs.to_int64 ofs)); TailNoLabel.
   (* destruct (make_immed32 (Ptrofs.to_int ofs)); TailNoLabel. *)
 Qed.
-(*
+
 Remark loadind_label:
   forall base ofs ty dst k c,
   loadind base ofs ty dst k = OK c -> tail_nolabel k c.
@@ -319,7 +319,7 @@ Proof.
   unfold loadind; intros.
   destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I.
 Qed.
-
+(*
 Remark storeind_label:
   forall src base ofs ty k c,
   storeind src base ofs ty k = OK c -> tail_nolabel k c.
@@ -361,13 +361,13 @@ Lemma transl_instr_label:
   match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end.
 Proof.
   unfold transl_instr; intros; destruct i; TailNoLabel.
+- eapply loadind_label; eauto.
 - eapply transl_op_label; eauto.
 - destruct s0; monadInv H; eapply tail_nolabel_trans
   ; [eapply make_epilogue_label|TailNoLabel]. 
 - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
 Qed.
 (*
-- eapply loadind_label; eauto.
 - eapply storeind_label; eauto.
 - destruct ep. eapply loadind_label; eauto.
   eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. 
@@ -661,15 +661,15 @@ Proof.
   exploit Mem.loadv_extends; eauto. intros [v' [A B]].
   rewrite (sp_val _ _ _ AG) in A.
   left; eapply exec_straight_steps; eauto. intros. simpl in TR.
+(*  
   inversion TR.
-(*
   intros [rs' [P [Q R]]].
-
+*)
   exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
   exists rs'; split. eauto.
   split. eapply agree_set_mreg; eauto with asmgen. congruence.
   simpl; congruence.
-*)
+
 
 - (* Msetstack *)
   unfold store_stack in H.
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 91cee038..e339a4c9 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -1196,7 +1196,7 @@ Proof.
   unfold exec_store. rewrite B, C, STORE by auto. eauto. auto. 
   intros; Simpl.
 Qed.
-(*
+
 Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k c (rs: regset) m v,
   loadind base ofs ty dst k = OK c ->
@@ -1213,11 +1213,12 @@ Proof.
              /\ forall base' ofs' rs',
                    exec_instr ge fn (mk_instr base' ofs') rs' m =
                    exec_load ge (chunk_of_type ty) rs' m (preg_of dst) base' ofs').
-  { unfold loadind in TR. destruct ty, (preg_of dst); inv TR; econstructor; split; eauto. }
+  { unfold loadind in TR. 
+    destruct ty, (preg_of dst); inv TR; econstructor; split; eauto. }
   destruct A as (mk_instr & B & C). subst c. 
   eapply indexed_load_access_correct; eauto with asmgen. 
 Qed.
-
+(*
 Lemma storeind_correct:
   forall (base: ireg) ofs ty src k c (rs: regset) m m',
   storeind src base ofs ty k = OK c ->
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index b25804d2..5852b7f5 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -348,9 +348,9 @@ module Target : TARGET =
          fprintf oc "	lh	%a, %a(%a)\n" ireg rd offset ofs ireg ra
       | Plhu(rd, ra, ofs) ->
          fprintf oc "	lhu	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) ->
-         fprintf oc "	lw	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-    *)| Pld(rd, ra, ofs) (*| Pld_a(rd, ra, ofs)*) -> assert Archi.ptr64;
+    *)| Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
+         fprintf oc "	lws	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+      | Pld(rd, ra, ofs) | Pfld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64;
          fprintf oc "	ld	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
 
     (*| Psb(rd, ra, ofs) ->