Commit a6c79438 authored by Cyril SIX's avatar Cyril SIX
Browse files

MPPA - Ocast32signed

parent 5e35117f
......@@ -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 =>
......
......@@ -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
......
......@@ -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)
......
......@@ -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)) ->
......
......@@ -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:
......
......@@ -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 ->
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment