MPPA - Onegf

5 files changed, 17 insertions, 14 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index b988a156..db2f9ee2 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -286,8 +286,8 @@ Inductive instruction : Type :=
 *)| 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 *)
+*)| Pfnegd   (rd: freg) (rs: freg)                  (**r negation *)
+(*| Pfabsd   (rd: freg) (rs: freg)                  (**r absolute value *)
 
   | Pfaddd   (rd: freg) (rs1 rs2: freg)             (**r addition *)
   | Pfsubd   (rd: freg) (rs1 rs2: freg)             (**r subtraction *)
@@ -898,9 +898,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (*| Pfsd_a s a ofs =>
       exec_store Many64 rs m s a ofs
 
-  | Pfnegd d s =>
+*)| Pfnegd d s =>
       Next (nextinstr (rs#d <- (Val.negf rs#s))) m
-  | Pfabsd d s =>
+(*| Pfabsd d s =>
       Next (nextinstr (rs#d <- (Val.absf rs#s))) m
 
   | Pfaddd d s1 s2 =>
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 874ef101..9a4c2ba3 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -416,10 +416,10 @@ Definition transl_op
           Paddl GPR31 rs GPR31 ::
           Psrail rd GPR31 n :: k)
 
-  | Onegf, a1 :: nil =>
+*)| Onegf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfnegd rd rs :: k)
-  | Oabsf, a1 :: nil =>
+(*| Oabsf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfabsd rd rs :: k)
   | Oaddf, a1 :: a2 :: nil =>
@@ -612,7 +612,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (src: mreg) (k: code) : res (list instruction) :=
   match chunk with
-(*| Mint8signed | Mint8unsigned =>
+  | Mint8signed | Mint8unsigned =>
       do r <- ireg_of src;
       transl_memory_access (Psb r)  addr args k
   | Mint16signed | Mint16unsigned =>
@@ -630,7 +630,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
   | Mfloat64 =>
       do r <- freg_of src;
       transl_memory_access (Pfsd r) addr args k
-*)| _ =>
+  | _ =>
       Error (msg "Asmgen.transl_store")
   end.
 
@@ -658,9 +658,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       transl_op op args res k
   | Mload chunk addr args dst =>
       transl_load chunk addr args dst k
-(*| Mstore chunk addr args src =>
+  | Mstore chunk addr args src =>
       transl_store chunk addr args src k
-  | Mcall sig (inl r) =>
+(*| Mcall sig (inl r) =>
       do r1 <- ireg_of r; OK (Pjal_r r1 sig :: k)
 *)| Mcall sig (inr symb) =>
       OK ((Pcall symb) :: k)
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index d8080257..4809afcb 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -405,6 +405,8 @@ Proof.
 - eapply transl_op_label; eauto.
 (* transl_load *)
 - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
+(* transl store *)
+- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
 - destruct s0; monadInv H; TailNoLabel.
 - destruct s0; monadInv H; eapply tail_nolabel_trans
   ; [eapply make_epilogue_label|TailNoLabel].
@@ -797,11 +799,11 @@ Local Transparent destroyed_by_op.
   left; eapply exec_straight_steps; eauto.
   intros. simpl in TR.
   inversion TR.
-(*exploit transl_store_correct; eauto. intros [rs2 [P Q]].
+  exploit transl_store_correct; eauto. intros [rs2 [P Q]].
   exists rs2; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
   simpl; congruence.
-*)
+
 - (* Mcall *)
   assert (f0 = f) by congruence.  subst f0.
   inv AT.
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 55724239..e5d5af55 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -1534,10 +1534,8 @@ Proof.
    /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)).
   { unfold transl_store in TR; destruct chunk; ArgsInv;
     (econstructor; econstructor; split; [eassumption | split; [ intros; simpl; reflexivity | auto]]).
-(*
     destruct a; auto. apply Mem.store_signed_unsigned_8. 
     destruct a; auto. apply Mem.store_signed_unsigned_16. 
-*)
   }
   destruct A as (mk_instr & chunk' & B & C & D).
   rewrite D in STORE; clear D. 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index e93603a4..16d75df3 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -268,6 +268,9 @@ module Target : TARGET =
       | 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
 
+      | Pfnegd(rd, ra) ->
+         fprintf oc "	fnegd	%a = %a\n;;\n" ireg ra ireg rd
+
       (* Pseudo-instructions expanded in Asmexpand *)
       | Pallocframe(sz, ofs) ->
          assert false