diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
commit | 89a54eee40305a61d1c1c0b9c5e6ba039592507b (patch) | |
tree | 83cf2236e0cc161551cc025af531803547654270 /mppa_k1c | |
parent | 8bdfa912a9ba8cee569cb40bf2ec4c584095e402 (diff) | |
download | compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.tar.gz compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.zip |
MPPA - Onegf
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 8 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 12 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof1.v | 2 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 3 |
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 |