MPPA - Added Msetstack + bunch of store --> on a des call !

5 files changed, 35 insertions, 32 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 8657bc44..7603a1f9 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -250,13 +250,13 @@ Inductive instruction : Type :=
 
 (*| 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     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)
   | Psw_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any32 *)
-*)| Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)
-(*| Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)
+  | Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)
+  | Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)
 
   (* Synchronization *)
-  | Pfence                                          (**r fence *)
+(*| Pfence                                          (**r fence *)
 
   (* floating point register move *)
   | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
@@ -265,9 +265,9 @@ Inductive instruction : Type :=
 
   (* 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 *)
+  | Pfss     (rs: freg) (ra: ireg) (ofs: offset)    (**r store float *)
 
-  | Pfnegs   (rd: freg) (rs: freg)                  (**r negation *)
+(*| Pfnegs   (rd: freg) (rs: freg)                  (**r negation *)
   | Pfabss   (rd: freg) (rs: freg)                  (**r absolute value *)
 
   | Pfadds   (rd: freg) (rs1 rs2: freg)             (**r addition *)
@@ -301,8 +301,8 @@ Inductive instruction : Type :=
   (* 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 *)
-  | Pfsd     (rd: freg) (ra: ireg) (ofs: offset)    (**r store 64-bit float *)
-  | Pfsd_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r store any64 *)
+*)| Pfsd     (rd: freg) (ra: ireg) (ofs: offset)    (**r store 64-bit float *)
+(*| Pfsd_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r store any64 *)
 
   | Pfnegd   (rd: freg) (rs: freg)                  (**r negation *)
   | Pfabsd   (rd: freg) (rs: freg)                  (**r absolute value *)
@@ -841,26 +841,26 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_store Mint8unsigned rs m s a ofs
   | Psh s a ofs =>
       exec_store Mint16unsigned rs m s a ofs
-  | Psw s a ofs =>
+*)| Psw s a ofs =>
       exec_store Mint32 rs m s a ofs
   | Psw_a s a ofs =>
       exec_store Many32 rs m s a ofs
-*)| Psd s a ofs =>
+  | Psd s a ofs =>
       exec_store Mint64 rs m s a ofs
-(*| Psd_a s a ofs =>
+  | Psd_a s a ofs =>
       exec_store Many64 rs m s a ofs
 
 (** Floating point register move *)
-  | Pfmv d s =>
+(*| Pfmv d s =>
       Next (nextinstr (rs#d <- (rs#s))) m
 
 (** 32-bit (single-precision) floating point *)
 *)| 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 =>
+(*| Pfnegs d s =>
       Next (nextinstr (rs#d <- (Val.negfs rs#s))) m
   | Pfabss d s =>
       Next (nextinstr (rs#d <- (Val.absfs rs#s))) m
@@ -903,9 +903,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_load Mfloat64 rs m d a ofs
 (*| Pfld_a d a ofs =>
       exec_load Many64 rs m d a ofs
-  | Pfsd s a ofs =>
+*)| Pfsd s a ofs =>
       exec_store Mfloat64 rs m s a ofs
-  | Pfsd_a s a ofs =>
+(*| Pfsd_a s a ofs =>
       exec_store Many64 rs m s a ofs
 
   | Pfnegd d s =>
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 3445c898..8dd23041 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -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)
@@ -719,7 +719,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :
   | _, _           => Error (msg "Asmgen.storeind")
   end.
 
-*)
+  
 Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) :=
   indexed_memory_access (Pld dst) base ofs k.
 
@@ -812,9 +812,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   match i with
   | 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 =>
+(*| Mgetparam ofs ty dst =>
       (* load via the frame pointer if it is valid *)
       do c <- loadind GPR30 ofs ty dst k;
       OK (if ep then c
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index afbb2e3f..5d6c21c8 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -323,7 +323,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.
@@ -331,7 +331,7 @@ Proof.
   unfold storeind; intros.
   destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I.
 Qed.
-*)
+
 Remark loadind_ptr_label:
   forall base ofs dst k, tail_nolabel k (loadind_ptr base ofs dst k).
 Proof.
@@ -365,7 +365,10 @@ 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.
+(* loadind *)
 - eapply loadind_label; eauto.
+(* storeind *)
+- eapply storeind_label; eauto.
 - eapply transl_op_label; eauto.
 - destruct s0; monadInv H; TailNoLabel.
 - destruct s0; monadInv H; eapply tail_nolabel_trans
@@ -373,7 +376,7 @@ Proof.
 - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
 Qed.
 (*
-- eapply storeind_label; eauto.
+
 - destruct ep. eapply loadind_label; eauto.
   eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. 
 - eapply transl_op_label; eauto.
@@ -683,11 +686,11 @@ Proof.
   left; eapply exec_straight_steps; eauto.
   rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
   inversion TR.
-(*exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
+  exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
   exists rs'; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
   simpl; intros. rewrite Q; auto with asmgen.
-*)
+
 - (* Mgetparam *)
   assert (f0 = f) by congruence; subst f0.
   unfold load_stack in *.
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 23c0478c..635f37dc 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -1218,7 +1218,7 @@ Proof.
   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 ->
@@ -1238,7 +1238,7 @@ Proof.
   destruct A as (mk_instr & B & C). subst c. 
   eapply indexed_store_access_correct; eauto with asmgen. 
 Qed.
-*)
+
 
 Lemma Pget_correct:
   forall (dst: gpreg) (src: preg) k (rs: regset) m,
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index fe3a57ac..913127df 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -159,9 +159,9 @@ module Target : TARGET =
 (* Printing of instructions *)
     let print_instruction oc = function
       | Pcall(s) ->
-         fprintf oc "	call	%a\n" symbol s
+         fprintf oc "	call	%a\n;;\n" symbol s
       | Pgoto(s) ->
-         fprintf oc "	goto	%a\n" symbol s
+         fprintf oc "	goto	%a\n;;\n" symbol s
       | Pret ->
          fprintf oc "	ret\n;;\n"
       | Pget (rd, rs) ->
@@ -359,9 +359,9 @@ module Target : TARGET =
          fprintf oc "	sb	%a, %a(%a)\n" ireg rd offset ofs ireg ra
       | Psh(rd, ra, ofs) ->
          fprintf oc "	sh	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) ->
-         fprintf oc "	sw	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-    *)| Psd(rd, ra, ofs) (*| Psd_a(rd, ra, ofs)*) -> assert Archi.ptr64;
+    *)| Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
+         fprintf oc "	sw	%a[%a] = %a\n" offset ofs ireg ra ireg rd
+      | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) | Pfsd(rd, ra, ofs) -> assert Archi.ptr64;
          fprintf oc "	sd	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd