MPPA - Ocast32signed

6 files changed, 53 insertions, 8 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index db2f9ee2..d7007102 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -209,6 +209,8 @@ Inductive instruction : Type :=
 
 (** Conversions *)
   | Pcvtl2w (rd: ireg) (rs: ireg)                   (**r Convert Long to Word *)
+  | Pcvtw2l (r : ireg)                              (**r Convert Word to Long *)
+  | Pmvw2l  (rd: ireg) (rs: ireg)                   (**r Move Convert Word to Long *)
 
 (** 64-bit integer register-register instructions *)
   | Paddl   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
@@ -769,6 +771,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (** Conversions *)
   | Pcvtl2w d s =>
       Next (nextinstr (rs#d <- (Val.loword rs###s))) m
+  | Pcvtw2l r   =>
+      Next (nextinstr (rs#r <- (Val.longofint rs#r))) m
+  | Pmvw2l d s =>
+      Next (nextinstr (rs#d <- (Val.longofint rs#s))) m
 
 (** Unconditional jumps. *)
   | Pj_l l =>
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index d24383a7..51d63da5 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -551,11 +551,12 @@ let expand_instruction instr =
 *)| Pcvtl2w(rd, rs) ->
       assert Archi.ptr64;
       emit (Paddiw(rd, rs, Int.zero))  (* 32-bit sign extension *)
-(*| Pcvtw2l(r) ->
+  | Pcvtw2l(r) ->
       assert Archi.ptr64
       (* no-operation because the 32-bit integer was kept sign extended already *)
+      (* FIXME - is it really the case on the MPPA ? *)
 
-  | Pjal_r(r, sg) ->
+(*| Pjal_r(r, sg) ->
       fixup_call sg; emit instr
   | Pjal_s(symb, sg) ->
       fixup_call sg; emit instr
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 9a4c2ba3..828073f7 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -116,6 +116,12 @@ Definition sltimm64 := opimm64 Psltl Psltil.
 Definition sltuimm64 := opimm64 Psltul Psltiul.
 *)
 
+Definition cast32signed (rd rs: ireg) (k: code) := 
+  if (ireg_eq rd rs)
+    then Pcvtw2l rd :: k
+    else Pmvw2l rd rs :: k
+  .
+
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
     Pmv rd rs :: k
@@ -331,11 +337,10 @@ Definition transl_op
 *)| Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Pcvtl2w rd rs :: k)  
-(*| Ocast32signed, a1 :: nil =>
+  | Ocast32signed, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      assertion (ireg_eq rd rs);
-      OK (Pcvtw2l rd :: k)
-  | Ocast32unsigned, a1 :: nil =>
+      OK (cast32signed rd rs k)
+(*| Ocast32unsigned, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       assertion (ireg_eq rd rs);
       OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k)
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 4809afcb..905bb85c 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -142,6 +142,13 @@ Proof.
 Qed.
 Hint Resolve loadimm64_label: labels.
 
+Remark cast32signed_label:
+  forall rd rs k, tail_nolabel k (cast32signed rd rs k).
+Proof.
+  intros; unfold cast32signed. destruct (ireg_eq rd rs); TailNoLabel.
+Qed.
+Hint Resolve cast32signed_label: labels.
+
 Remark opimm64_label:
   forall op opimm r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index e5d5af55..ef70cec4 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -1080,6 +1080,26 @@ Proof.
   destruct (zlt i0 32). auto. apply Int.bits_above. auto.
 Qed.
 
+Lemma cast32signed_correct:
+  forall (d s: ireg) (k: code) (rs: regset) (m: mem),
+  exists rs': regset,
+    exec_straight ge fn (cast32signed d s k) rs m k rs' m
+ /\ Val.lessdef (Val.longofint (rs s)) (rs' d)
+ /\ (forall r: preg, r <> PC -> r <> d -> rs' r = rs r).
+Proof.
+  intros. unfold cast32signed. destruct (ireg_eq d s).
+- econstructor; split.
+  + apply exec_straight_one. simpl. eauto with asmgen. Simpl.
+  + split.
+    * rewrite e. Simpl.
+    * intros. destruct r; Simpl.
+- econstructor; split.
+  + apply exec_straight_one. simpl. eauto with asmgen. Simpl.
+  + split.
+    * Simpl.
+    * intros. destruct r; Simpl.
+Qed.
+
 (* Translation of arithmetic operations *)
 
 Ltac SimplEval H :=
@@ -1109,6 +1129,11 @@ Opaque Int.eq.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
 - (* move *)
   destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl.
+- (* Ocast32signed *)
+  exploit cast32signed_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. split. apply B.
+  intros. assert (r <> PC). { destruct r; auto; contradict H; discriminate. }
+  apply C; auto.
 (*
 - (* intconst *)
   exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
@@ -1233,6 +1258,7 @@ Opaque Int.eq.
 *)
 Qed.
 
+
 (** Memory accesses *)
 
 Lemma indexed_memory_access_correct:
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 16d75df3..3e4c3ff6 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -199,7 +199,7 @@ module Target : TARGET =
          fprintf oc "	get	%a = %a\n;;\n" ireg rd preg rs
       | Pset (rd, rs) ->
          fprintf oc "	set	%a = %a\n;;\n" preg rd ireg rs
-      | Pmv(rd, rs) ->
+      | Pmv(rd, rs) | Pmvw2l(rd, rs) ->
          fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
 
       | Paddiw (rd, rs, imm) ->
@@ -276,7 +276,7 @@ module Target : TARGET =
          assert false
       | Pfreeframe(sz, ofs) ->
          assert false
-      | Pcvtl2w _ -> assert false
+      | Pcvtl2w _ | Pcvtw2l _ -> assert false
 
       (* Pseudo-instructions that remain *)
       | Plabel lbl ->