Commit 89a54eee authored by Cyril SIX's avatar Cyril SIX
Browse files

MPPA - Onegf

parent 8bdfa912
......@@ -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 =>
......
......@@ -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)
......
......@@ -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.
......
......@@ -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.
......
......@@ -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
......
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