diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 5 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 11 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 27 | ||||
-rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 7 |
4 files changed, 40 insertions, 10 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d73d00c7..8b1c9a81 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -122,7 +122,9 @@ Inductive instruction : Type := | Psd (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int64 *)
| Psd_a (rs: ireg) (ra: ireg) (ofs: addressing) (**r store any64 *)
| Pfss (rs: freg) (ra: ireg) (ofs: addressing) (**r store float *)
- | Pfsd (rd: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
+ | Pfsd (rs: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
+
+ | Psq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
(** Arith RR *)
| Pmv (rd rs: ireg) (**r register move *)
@@ -484,6 +486,7 @@ Definition basic_to_instruction (b: basic) := | PStoreRRRXS Asmvliw.Pfss rd ra ro => Pfss rd ra (ARegXS ro)
| PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro)
+ | PStoreQRRO qrs ra ofs => Psq qrs ra (AOff ofs)
end.
Section RELSEM.
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 1ee5002c..04f02a80 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -639,6 +639,10 @@ Definition trans_basic (b: basic) : inst := | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))] | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PStoreQRRO qs a ofs => + let (s0, s1) := gpreg_q_expand qs in + [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))] | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil); (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))] | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil)); @@ -884,7 +888,10 @@ Proof. eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. -(* Allocframe *) + + unfold parexec_store_q_offset. + destruct (gpreg_q_expand rs) as [s0 s1]. + simpl. + (* Allocframe *) - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. * eexists; repeat split. { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl. @@ -1529,5 +1536,3 @@ Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bbloc Definition bblock_equiv_eq := pure_bblock_eq_test_correct true. End SECT_BBLOCK_EQUIV. - - diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 0cbe27e1..fb1575f9 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -236,9 +236,6 @@ Definition label := positive. *) Inductive ex_instruction : Type := (* Pseudo-instructions *) -(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *) - | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) - | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) . @@ -341,6 +338,7 @@ Inductive st_instruction : Type := | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset) | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) | PStoreRRRXS(i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) + | PStoreQRRO (rs: gpreg_q) (ra: ireg) (ofs: offset) . (** Arithmetic instructions **) @@ -355,7 +353,6 @@ Inductive arith_name_rr : Type := | Pcvtl2w (**r Convert Long to Word *) | Psxwd (**r Sign Extend Word to Double Word *) | Pzxwd (**r Zero Extend Word to Double Word *) -(* | Pextfs (stop : int) (start : int) (**r extract bit field, signed *) *) | Pextfz (stop : Z) (start : Z) (**r extract bit field, unsigned *) | Pextfs (stop : Z) (start : Z) (**r extract bit field, signed *) | Pextfzl (stop : Z) (start : Z) (**r extract bit field, unsigned *) @@ -693,7 +690,7 @@ Variable ge: genv. from the current state (a register set + a memory state) to either [Next rs' m'] where [rs'] and [m'] are the updated register set and memory state after execution of the instruction at [rs#PC], or [Stuck] if the processor is stuck. - + The parallel semantics of each instructions handles two states in input: - the actual input state of the bundle which is only read - and the other on which every "write" is performed: @@ -1198,6 +1195,23 @@ Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: m | Some m' => Next rsw m' end. +Definition parexec_store_q_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_q) (a: ireg) (ofs: offset) := + let (s0, s1) := gpreg_q_expand s in + match eval_offset ofs with + | OK eofs => + let base := Val.offset_ptr (rsr a) eofs in + match Mem.storev Many64 mr base (rsr s0) with + | None => Stuck + | Some m1 => + match Mem.storev Many64 m1 base (rsr s1) with + | None => Stuck + | Some m2 => Next rsw m2 + end + end + | _ => Stuck + end. + + Definition load_chunk n := match n with | Plb => Mint8signed @@ -1237,7 +1251,8 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := | PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs | PStoreRRR n s a ro => parexec_store_reg (store_chunk n) rsr rsw mr mw s a ro | PStoreRRRXS n s a ro => parexec_store_regxs (store_chunk n) rsr rsw mr mw s a ro - + | PStoreQRRO s a ofs => + parexec_store_q_offset rsr rsw mr mw s a ofs | Pallocframe sz pos => let (mw, stk) := Mem.alloc mr 0 sz in let sp := (Vptr stk Ptrofs.zero) in diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 0a83a903..a93cb28a 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -950,6 +950,13 @@ Proof. 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). 1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. 1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. + - (* PStoreQRRO *) + unfold parexec_store_q_offset in H1. + destruct (gpreg_q_expand _) as [r0 r1] in H1. + destruct (eval_offset _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + inv H1. Simpl. reflexivity. - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. |