From 807b07dce1f41dc885d7671e8567ba112966ba7b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 15:48:11 +0200 Subject: begin load.xs --- mppa_k1c/Asm.v | 12 ++++++++++++ mppa_k1c/Asmblock.v | 2 ++ mppa_k1c/Asmblockdeps.v | 20 ++++++++++++++++++++ mppa_k1c/Asmvliw.v | 23 +++++++++++++++++++++++ mppa_k1c/PostpassSchedulingOracle.ml | 8 ++++---- mppa_k1c/PostpassSchedulingproof.v | 12 ++++++++++++ mppa_k1c/TargetPrinter.ml | 18 +++++++++++------- mppa_k1c/lib/Asmblockgenproof0.v | 1 + 8 files changed, 85 insertions(+), 11 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d1ac8a67..0e217d36 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -42,6 +42,7 @@ Definition preg := preg. Inductive addressing : Type := | AOff (ofs: offset) | AReg (ro: ireg) + | ARegXS (ro: ireg) . (** Syntax *) @@ -444,6 +445,17 @@ Definition basic_to_instruction (b: basic) := | PLoadRRR Asmvliw.Pfls rd ra ro => Pfls rd ra (AReg ro) | PLoadRRR Asmvliw.Pfld rd ra ro => Pfld rd ra (AReg ro) + | PLoadRRRXS Asmvliw.Plb rd ra ro => Plb rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Plbu rd ra ro => Plbu rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Plh rd ra ro => Plh rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Plhu rd ra ro => Plhu rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Plw rd ra ro => Plw rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Plw_a rd ra ro => Plw_a rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Pld rd ra ro => Pld rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Pld_a rd ra ro => Pld_a rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Pfls rd ra ro => Pfls rd ra (ARegXS ro) + | PLoadRRRXS Asmvliw.Pfld rd ra ro => Pfld rd ra (ARegXS ro) + (** Store *) | PStoreRRO Asmvliw.Psb rd ra ofs => Psb rd ra (AOff ofs) | PStoreRRO Asmvliw.Psh rd ra ofs => Psh rd ra (AOff ofs) diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index ed145f21..3aec4e11 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -268,6 +268,8 @@ Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ir Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro. +Definition exec_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_regxs chunk rs rs m m d a ro. + Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset ge chunk rs rs m m s a ofs. Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 2e83fb44..32a5fa04 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -75,6 +75,7 @@ Coercion OArithRRI64: arith_name_rri64 >-> Funclass. Inductive load_op := | OLoadRRO (n: load_name) (ofs: offset) | OLoadRRR (n: load_name) + | OLoadRRRXS (n: load_name) . Coercion OLoadRRO: load_name >-> Funclass. @@ -146,10 +147,17 @@ Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) := | Some vl => Some (Val vl) end. +Definition exec_load_deps_regxs (chunk: memory_chunk) (m: mem) (v vo: val) := + match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with + | None => None + | Some vl => Some (Val vl) + end. + Definition load_eval (lo: load_op) (l: list value) := match lo, l with | OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps_offset (load_chunk n) m v ofs | OLoadRRR n, [Val v; Val vo; Memstate m] => exec_load_deps_reg (load_chunk n) m v vo + | OLoadRRRXS n, [Val v; Val vo; Memstate m] => exec_load_deps_regxs (load_chunk n) m v vo | _, _ => None end. @@ -355,6 +363,8 @@ Definition load_op_eq (o1 o2: load_op): ?? bool := match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end | OLoadRRR n1 => match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end + | OLoadRRRXS n1 => + match o2 with OLoadRRRXS n2 => phys_eq n1 n2 | _ => RET false end end. Lemma load_op_eq_correct o1 o2: @@ -363,6 +373,7 @@ Proof. destruct o1, o2; wlp_simplify; try discriminate. - congruence. - congruence. + - congruence. Qed. Hint Resolve load_op_eq_correct: wlp. Opaque load_op_eq_correct. @@ -612,6 +623,7 @@ Definition trans_basic (b: basic) : inst := | PArith ai => trans_arith ai | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (PReg (#a) @ PReg pmem @ Enil))] | PLoadRRR n d a ro => [(#d, Op (Load (OLoadRRR n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PLoadRRRXS n d a ro => [(#d, Op (Load (OLoadRRRXS n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | 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))] | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil); @@ -828,6 +840,13 @@ Proof. eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + (* Load Reg XS *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs); + destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + (* Store *) - destruct i. (* Store Offset *) @@ -1408,6 +1427,7 @@ Definition string_of_load (op: load_op): pstring := match op with | OLoadRRO n _ => string_of_load_name n | OLoadRRR n => string_of_load_name n + | OLoadRRRXS n => string_of_load_name n end. Definition string_of_store_name (n: store_name) : pstring := diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index cf827818..d7311272 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -270,6 +270,7 @@ Inductive load_name : Type := Inductive ld_instruction : Type := | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) . Coercion PLoadRRO: load_name >-> Funclass. @@ -1123,6 +1124,27 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) | Some v => Next (rsw#d <- v) mw end. +Definition scale_of_chunk (chunk: memory_chunk) := + Vint (Int.repr + (match chunk with + | Mint8signed => 0 + | Mint8unsigned => 0 + | Mint16signed => 1 + | Mint16unsigned => 1 + | Mint32 => 2 + | Mint64 => 3 + | Mfloat32 => 2 + | Mfloat64 => 3 + | Many32 => 2 + | Many64 => 3 + end)). + +Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := + match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with + | None => Stuck + | Some v => Next (rsw#d <- v) mw + end. + Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) := match (eval_offset ofs) with | OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with @@ -1172,6 +1194,7 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := | PLoadRRO n d a ofs => parexec_load_offset (load_chunk n) rsr rsw mr mw d a ofs | PLoadRRR n d a ro => parexec_load_reg (load_chunk n) rsr rsw mr mw d a ro + | PLoadRRRXS n d a ro => parexec_load_regxs (load_chunk n) rsr rsw mr mw d a ro | 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 diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index f931b64b..ef5e325a 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -216,10 +216,10 @@ let arith_rec i = | PArithR (i, rd) -> arith_r_rec i (IR rd) let load_rec i = match i with - | PLoadRRO (i, rs1, rs2, imm) -> { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) - ; is_control = false} - | PLoadRRR (i, rs1, rs2, rs3) -> { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None - ; is_control = false} + | PLoadRRO (i, rs1, rs2, imm) -> + { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false} + | PLoadRRR (i, rs1, rs2, rs3) | PLoadRRRXS (i, rs1, rs2, rs3) -> + { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false} let store_rec i = match i with | PStoreRRO (i, rs1, rs2, imm) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2)]; imm = (Some (Off imm)) diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index bc90dd4c..3f3cb19c 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -117,6 +117,17 @@ Proof. - discriminate. Qed. +Lemma exec_load_regxs_pc_var: + forall t rs m rd ra ro rs' m' v, + exec_load_regxs t rs m rd ra ro = Next rs' m' -> + exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. + destruct (Mem.loadv _ _ _). + - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. + - discriminate. +Qed. + Lemma exec_store_offset_pc_var: forall ge t rs m rd ra ofs rs' m' v, exec_store_offset ge t rs m rd ra ofs = Next rs' m' -> @@ -155,6 +166,7 @@ Proof. - destruct i. + exploreInst; apply exec_load_offset_pc_var; auto. + exploreInst; apply exec_load_reg_pc_var; auto. + + exploreInst; apply exec_load_regxs_pc_var; auto. - destruct i. + exploreInst; apply exec_store_offset_pc_var; auto. + exploreInst; apply exec_store_reg_pc_var; auto. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 506faa1c..47927364 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -166,7 +166,11 @@ module Target (*: TARGET*) = let addressing oc = function | AOff ofs -> offset oc ofs - | AReg ro -> ireg oc ro + | AReg ro | ARegXS ro -> ireg oc ro + + let xscale oc = function + | ARegXS _ -> fprintf oc ".xs" + | _ -> () let icond_name = let open Asmvliw in function | ITne | ITneu -> "ne" @@ -342,17 +346,17 @@ module Target (*: TARGET*) = (* Load/Store instructions *) | Plb(rd, ra, adr) -> - fprintf oc " lbs %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lbs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plbu(rd, ra, adr) -> - fprintf oc " lbz %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lbz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plh(rd, ra, adr) -> - fprintf oc " lhs %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lhs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plhu(rd, ra, adr) -> - fprintf oc " lhz %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lhz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plw(rd, ra, adr) | Plw_a(rd, ra, adr) | Pfls(rd, ra, adr) -> - fprintf oc " lws %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lws%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Pld(rd, ra, adr) | Pfld(rd, ra, adr) | Pld_a(rd, ra, adr) -> assert Archi.ptr64; - fprintf oc " ld %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " ld%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Psb(rd, ra, adr) -> fprintf oc " sb %a[%a] = %a\n" addressing adr ireg ra ireg rd diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index eb336edc..ab0d2964 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -946,6 +946,7 @@ Proof. all: try (inv H; Simpl). 1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). 1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). 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. - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. -- cgit