From 972f6b9890ea3644626fc097e460035028b940eb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 4 Dec 2020 23:26:01 +0100 Subject: a first working draft on ldp/stp peephole --- aarch64/Asmblockdeps.v | 279 ++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 227 insertions(+), 52 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 059f234c..bdfb9ed3 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -166,14 +166,15 @@ Inductive arith_op := . Inductive store_op := - | Ostore1 (st: store_rs_a) (a: addressing) - | Ostore2 (st: store_rs_a) (a: addressing) - | OstoreU (st: store_rs_a) (a: addressing) + | Ostore1 (st: st_instruction) (a: addressing) + | Ostore2 (st: st_instruction) (a: addressing) + | OstoreU (st: st_instruction) (a: addressing) . Inductive load_op := | Oload1 (ld: ld_instruction) (a: addressing) | Oload2 (ld: ld_instruction) (a: addressing) + | OloadU (ld: ld_instruction) (a: addressing) . Inductive allocf_op := @@ -423,16 +424,16 @@ Definition call_ll_storev (c: memory_chunk) (m: mem) (v: option val) (vs: val) : | None => None (* should never occurs *) end. -Definition exec_store1 (n: store_rs_a) (m: mem) (a: addressing) (vr vs: val) := +Definition exec_store1 (n: st_instruction) (m: mem) (a: addressing) (vr vs: val) := let v := match a with | ADimm _ n => Some (Val.addl vs (Vlong n)) | ADadr _ id ofs => Some (Val.addl vs (symbol_low Ge.(_lk) id ofs)) | _ => None end in - call_ll_storev (chunk_store_rs_a n) m v vr. + call_ll_storev (chunk_store n) m v vr. -Definition exec_store2 (n: store_rs_a) (m: mem) (a: addressing) (vr vs1 vs2: val) := +Definition exec_store2 (n: st_instruction) (m: mem) (a: addressing) (vr vs1 vs2: val) := let v := match a with | ADreg _ _ => Some (Val.addl vs1 vs2) @@ -441,10 +442,10 @@ Definition exec_store2 (n: store_rs_a) (m: mem) (a: addressing) (vr vs1 vs2: val | ADuxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofintu vs2) (Vint n))) | _ => None end in - call_ll_storev (chunk_store_rs_a n) m v vr. + call_ll_storev (chunk_store n) m v vr. -Definition exec_storeU (n: store_rs_a) (m: mem) (a: addressing) (vr: val) := - call_ll_storev (chunk_store_rs_a n) m None vr. +Definition exec_storeU (n: st_instruction) (m: mem) (a: addressing) (vr: val) := + call_ll_storev (chunk_store n) m None vr. Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with @@ -537,10 +538,14 @@ Definition exec_load2 (ld: ld_instruction) (m: mem) (a: addressing) (vl1 vl2: va end in call_ll_loadv (chunk_load ld) (interp_load ld) m v. +Definition exec_loadU (n: ld_instruction) (m: mem) (a: addressing) := + call_ll_loadv (chunk_load n) (interp_load n) m None. + Definition load_eval (o: load_op) (l: list value) := match o, l with | Oload1 ld a, [Val vs; Memstate m] => exec_load1 ld m a vs | Oload2 ld a, [Val vs1; Val vs2; Memstate m] => exec_load2 ld m a vs1 vs2 + | OloadU st a, [Memstate m] => exec_loadU st m a | _, _ => None end. @@ -764,18 +769,18 @@ Opaque control_op_eq_correct. Definition store_op_eq (s1 s2: store_op): ?? bool := match s1 with | Ostore1 st1 a1 => - match s2 with Ostore1 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end + match s2 with Ostore1 st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end | Ostore2 st1 a1 => - match s2 with Ostore2 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end + match s2 with Ostore2 st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end | OstoreU st1 a1 => - match s2 with OstoreU st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end + match s2 with OstoreU st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end end. Lemma store_op_eq_correct s1 s2: WHEN store_op_eq s1 s2 ~> b THEN b = true -> s1 = s2. Proof. destruct s1, s2; wlp_simplify; try congruence. - all: rewrite H0 in H; rewrite H; reflexivity. + all: rewrite H1 in H0; rewrite H0, H; reflexivity. Qed. Hint Resolve store_op_eq_correct: wlp. Opaque store_op_eq_correct. @@ -783,16 +788,18 @@ Opaque store_op_eq_correct. Definition load_op_eq (l1 l2: load_op): ?? bool := match l1 with | Oload1 ld1 a1 => - match l2 with Oload1 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end + match l2 with Oload1 ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end | Oload2 ld1 a1 => - match l2 with Oload2 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end + match l2 with Oload2 ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end + | OloadU ld1 a1 => + match l2 with OloadU ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end end. Lemma load_op_eq_correct l1 l2: WHEN load_op_eq l1 l2 ~> b THEN b = true -> l1 = l2. Proof. destruct l1, l2; wlp_simplify; try congruence. - all: rewrite H0 in H; rewrite H; reflexivity. + all: rewrite H1 in H0; rewrite H, H0; reflexivity. Qed. Hint Resolve load_op_eq_correct: wlp. Opaque load_op_eq_correct. @@ -1120,7 +1127,7 @@ Definition trans_arith (ai: ar_instruction) : inst := | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))] end. -Definition eval_addressing_rlocs_st (st: store_rs_a) (rs: dreg) (a: addressing) := +Definition eval_addressing_rlocs_st (st: st_instruction) (rs: dreg) (a: addressing) := match a with | ADimm base n => Op (Store (Ostore1 st a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil) | ADreg base r => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) @@ -1147,10 +1154,42 @@ Definition trans_load (ldi: ld_instruction) := | PLd_rd_a ld r a => let lr := eval_addressing_rlocs_ld ldi a in [(#r, lr)] | Pldp ld r1 r2 a => - let lr := eval_addressing_rlocs_ld ldi a in + let ldi' := + match ld with + | Pldpw => Pldrw + | Pldpx => Pldrx + end in + let lr := eval_addressing_rlocs_ld (PLd_rd_a ldi' r1 a) a in + let ofs := match ld with | Pldpw => 4%Z | Pldpx => 8%Z end in + match a with + | ADimm base n => + let a' := (get_offset_addr a ofs) in + [(#r1, lr); + (#r2, Op (Load (Oload1 (PLd_rd_a ldi' r2 a') a')) + (Old(PReg (#base)) @ PReg (pmem) @ Enil))] + | _ => [(#PC, (Op (OError)) Enil)] + end + end. + +Definition trans_store (sti: st_instruction) := + match sti with + | PSt_rs_a st r a => + let lr := eval_addressing_rlocs_st sti r a in [(pmem, lr)] + | Pstp st r1 r2 a => + let sti' := + match st with + | Pstpw => Pstrw + | Pstpx => Pstrx + end in + let lr := eval_addressing_rlocs_st (PSt_rs_a sti' r1 a) r1 a in + let ofs := match st with | Pstpw => 4%Z | Pstpx => 8%Z end in match a with - | ADpostincr base n => [(#base, lr); (#r1, lr); (#r2, lr)] - | _ => [(#r1, lr); (#r2, lr)] + | ADimm base n => + let a' := (get_offset_addr a ofs) in + [(pmem, lr); + (pmem, Op (Store (Ostore1 (PSt_rs_a sti' r2 a') a')) + (PReg (#r2) @ Old(PReg (#base)) @ PReg (pmem) @ Enil))] + | _ => [(#PC, (Op (OError)) Enil)] end end. @@ -1158,8 +1197,7 @@ Definition trans_basic (b: basic) : inst := match b with | PArith ai => trans_arith ai | PLoad ld => trans_load ld - | PStore st r a => - let lr := eval_addressing_rlocs_st st r a in [(pmem, lr)] + | PStore st => trans_store st | Pallocframe sz linkofs => [(#X29, PReg(#SP)); (#SP, Op (Allocframe (OAllocf_SP sz linkofs)) (PReg (#SP) @ PReg pmem @ Enil)); @@ -1173,6 +1211,7 @@ Definition trans_basic (b: basic) : inst := | Pcvtsw2x rd r1 => [(#rd, Op (Cvtsw2x) (PReg (#r1) @ Enil))] | Pcvtuw2x rd r1 => [(#rd, Op (Cvtuw2x) (PReg (#r1) @ Enil))] | Pcvtx2w rd => [(#rd, Op (Cvtx2w) (PReg (#rd) @ Enil))] + | Pnop => [] end. Fixpoint trans_body (b: list basic) : list L.inst := @@ -1673,20 +1712,46 @@ Local Ltac preg_eq_discr r rd := 6,7,8,9: Simpl sr. - (* Arith *) exploit trans_arith_correct; eauto. - - (* Load *) admit. - (*unfold exec_load, eval_addressing_rlocs_ld, exp_eval;*) - (*destruct a; simpl; try destruct base; Simpl_exists sr; erewrite H;*) - (*unfold exec_load1, exec_load2, exec_loadU; unfold call_ll_loadv;*) - (*try destruct (Mem.loadv _ _ _); simpl; auto.*) - (*all: DDRM rd; Simpl_exists sr; try intros rr; Simpl_update.*) + - (* Load *) + destruct ld. + + unfold exec_load, exec_load_rd_a, eval_addressing_rlocs_ld, exp_eval; + destruct ld; destruct a; simpl; + try fold (ppos base); try fold (ppos r); + erewrite !H0, H; simpl; + unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv; + try destruct (Mem.loadv _ _ _); simpl; auto. + all: try (fold (ppos rd); Simpl_exists sr; auto; intros rr; Simpl_update). + + unfold exec_load, exec_load_double, eval_addressing_rlocs_ld, exp_eval; + destruct ld; destruct a; simpl; unfold control_eval; destruct Ge; auto; + try fold (ppos base); + try erewrite !H0, H; simpl; + unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv; + try destruct (Mem.loadv _ _ _); simpl; auto; + fold (ppos rd1); rewrite assign_diff; discriminate_ppos; rewrite H; + try destruct (Mem.loadv _ _ _); simpl; auto; Simpl_exists sr; + try (rewrite !assign_diff; discriminate_ppos; reflexivity); + try (destruct base; discriminate_ppos); + repeat (try fold (ppos r); intros; Simpl_update). - (* Store *) - admit. - (*unfold exec_store, eval_addressing_rlocs_st, exp_eval;*) - (*destruct a; simpl; DIRN1 r; try destruct base; Simpl_exists sr; erewrite H;*) - (*unfold exec_store1, exec_store2, exec_storeU; unfold call_ll_storev;*) - (*try destruct (Mem.storev _ _ _ _); simpl; auto.*) - (*all: eexists; split; [| split]; [ eauto | eauto |*) - (*intros rr; rewrite assign_diff; [ rewrite H0; auto | apply ppos_pmem_discr ]].*) + destruct st. + + unfold exec_store, exec_store_rs_a, eval_addressing_rlocs_st, exp_eval; + destruct st; destruct a; simpl; + try fold (ppos base); try fold (ppos rs); try fold (ppos r); + erewrite !H0, H; simpl; + unfold exec_store1, exec_store2, chunk_store; unfold call_ll_storev; + try destruct (Mem.storev _ _ _ _); simpl; auto. + all: eexists; split; [| split]; eauto; + intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos. + + unfold exec_store, exec_store_double, eval_addressing_rlocs_st, exp_eval; + destruct st; destruct a; simpl; unfold control_eval; destruct Ge; auto; + try fold (ppos base); try fold (ppos rs1); + erewrite !H0, H; simpl; + unfold exec_store1, exec_store2, chunk_store; unfold call_ll_storev; + try destruct (Mem.storev _ _ _ _); simpl; auto; + fold (ppos rs2); rewrite assign_diff; try congruence; try rewrite H0; simpl; + try destruct (Mem.storev _ _ _ _); simpl; auto. + all: eexists; split; [| split]; eauto; + repeat (try intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos). - (* Alloc *) destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. + eexists; repeat split. @@ -2052,6 +2117,21 @@ Definition freg_name (fr: freg) : pstring := end . +Definition iregsp_name (irsp: iregsp) : pstring := + match irsp with + | RR1 ir => ireg_name ir + | XSP => Str ("XSP") + end. + +Definition dreg_name (dr: dreg) : ?? pstring := + match dr with + | IR ir => match ir with + | XSP => RET (Str ("XSP")) + | RR1 irr => RET (ireg_name irr) + end + | FR fr => RET (freg_name fr) + end. + Definition string_of_name (x: P.R.t): ?? pstring := if (Pos.eqb x pmem) then RET (Str "MEM") @@ -2064,13 +2144,7 @@ Definition string_of_name (x: P.R.t): ?? pstring := | CV => RET (Str ("CV")) end | Some (PC) => RET (Str ("PC")) - | Some (DR dr) => match dr with - | IR ir => match ir with - | XSP => RET (Str ("XSP")) - | RR1 irr => RET (ireg_name irr) - end - | FR fr => RET (freg_name fr) - end + | Some (DR dr) => dreg_name dr | _ => RET (Str ("UNDEFINED")) end. @@ -2339,17 +2413,118 @@ Definition string_of_arith (op: arith_op): pstring := | Ofnmul _ => "Ofnmul" end. -Definition string_of_store (op: store_op) : pstring := - match op with - | Ostore1 _ _ => "Ostore1" - | Ostore2 _ _ => "Ostore2" - | OstoreU _ _ => "OstoreU" +Definition string_of_ofs (ofs: ptrofs) : ?? pstring := + (string_of_Z (Ptrofs.signed ofs)). + +Definition string_of_int (n: int) : ?? pstring := + (string_of_Z (Int.signed n)). + +Definition string_of_int64 (n: int64) : ?? pstring := + (string_of_Z (Int64.signed n)). + +Notation "x +; y" := (Concat x y). + +Definition string_of_addressing (a: addressing) : ?? pstring := + match a with + | ADimm base n => + DO n' <~ string_of_int64 n;; + RET ((Str "[ADimm ") +; (iregsp_name base) +; " " +; n' +; "]") + | ADreg base r => + RET ((Str "[ADreg ") +; (iregsp_name base) +; " " +; (ireg_name r) +; "]") + | ADlsl base r n => + DO n' <~ string_of_int n;; + RET ((Str "[ADlsl ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]") + | ADsxt base r n => + DO n' <~ string_of_int n;; + RET ((Str "[ADsxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]") + | ADuxt base r n => + DO n' <~ string_of_int n;; + RET ((Str "[ADuxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]") + | ADadr base id ofs => + DO id' <~ string_of_Z (Zpos id);; + DO ofs' <~ string_of_ofs ofs;; + RET ((Str "[ADadr ") +; (iregsp_name base) +; " " +; id' +; " " +; ofs' +; "]") + | ADpostincr base n => + DO n' <~ string_of_int64 n;; + RET ((Str "[ADpostincr ") +; (iregsp_name base) +; " " +; n' +; "]") + end. + +Definition string_of_ld_rd_a (ld: load_rd_a) : pstring := + match ld with + | Pldrw => Str "Pldrw" + | Pldrw_a => Str "Pldrw_a" + | Pldrx => Str "Pldrx" + | Pldrx_a => Str "Pldrx_a" + | Pldrb _ => Str "Pldrb" + | Pldrsb _ => Str "Pldrsb" + | Pldrh _ => Str "Pldrh" + | Pldrsh _ => Str "Pldrsh" + | Pldrzw => Str "Pldrzw" + | Pldrsw => Str "Pldrsw" + | Pldrs => Str "Pldrs" + | Pldrd => Str "Pldrd" + | Pldrd_a => Str "Pldrd_a" + end. + +Definition string_of_ldi (ldi: ld_instruction) : ?? pstring:= + match ldi with + | PLd_rd_a ld rd a => + DO a' <~ string_of_addressing a;; + DO rd' <~ dreg_name rd;; + RET (Str "PLd_rd_a (" +; (string_of_ld_rd_a ld) +; " " +; rd' +; " " +; a' +; ")") + | Pldp _ _ _ a => + DO a' <~ string_of_addressing a;; + RET (Str "Pldp (" +; a' +; ")") end. -Definition string_of_load (op: load_op) : pstring := +Definition string_of_load (op: load_op) : ?? pstring := + match op with + | Oload1 ld a => + DO a' <~ string_of_addressing a;; + DO ld' <~ string_of_ldi ld;; + RET((Str "Oload1 ") +; " " +; ld' +; " " +; a' +; " ") + | Oload2 ld a => + DO a' <~ string_of_addressing a;; + DO ld' <~ string_of_ldi ld;; + RET((Str "Oload2 ") +; " " +; ld' +; " " +; a' +; " ") + | OloadU _ _ => RET (Str "OloadU") + end. + +Definition string_of_st_rs_a (st: store_rs_a) : pstring := + match st with + | Pstrw => Str "Pstrw" + | Pstrw_a => Str "Pstrw_a" + | Pstrx => Str "Pstrx" + | Pstrx_a => Str "Pstrx_a" + | Pstrb => Str "Pstrb" + | Pstrh => Str "Pstrh" + | Pstrs => Str "Pstrs" + | Pstrd => Str "Pstrd" + | Pstrd_a => Str "Pstrd_a" + end. + +Definition string_of_sti (sti: st_instruction) : ?? pstring:= + match sti with + | PSt_rs_a st rs a => + DO a' <~ string_of_addressing a;; + DO rs' <~ dreg_name rs;; + RET (Str "PSt_rs_a (" +; (string_of_st_rs_a st) +; " " +; rs' +; " " +; a' +; ")") + | Pstp _ _ _ a => + DO a' <~ string_of_addressing a;; + RET (Str "Pstp (" +; a' +; ")") + end. + +Definition string_of_store (op: store_op) : ?? pstring := match op with - | Oload1 _ _ => "Oload1" - | Oload2 _ _ => "Oload2" + | Ostore1 st a => + DO a' <~ string_of_addressing a;; + DO st' <~ string_of_sti st;; + RET((Str "Ostore1 ") +; " " +; st' +; " " +; a' +; " ") + | Ostore2 st a => + DO a' <~ string_of_addressing a;; + DO st' <~ string_of_sti st;; + RET((Str "Ostore2 ") +; " " +; st' +; " " +; a' +; " ") + | OstoreU _ _ => RET (Str "OstoreU") end. Definition string_of_control (op: control_op) : pstring := @@ -2382,8 +2557,8 @@ Definition string_of_freef (op: freef_op) : pstring := Definition string_of_op (op: P.op): ?? pstring := match op with | Arith op => RET (string_of_arith op) - | Load op => RET (string_of_load op) - | Store op => RET (string_of_store op) + | Load op => string_of_load op + | Store op => string_of_store op | Control op => RET (string_of_control op) | Allocframe op => RET (string_of_allocf op) | Freeframe op => RET (string_of_freef op) -- cgit