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/Asmgenproof.v | 50 ++++++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 24 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 9d80f58f..d412b129 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -818,9 +818,10 @@ Proof. (*unfold exec_load in BASIC.*) (*destruct Mem.loadv. 2: { discriminate BASIC. }*) (*inv BASIC. rewrite Pregmap.gso; try discriminate; auto.*) - - unfold exec_store in BASIC. - destruct Mem.storev. 2: { discriminate BASIC. } - inv BASIC; reflexivity. + - admit. + (*unfold exec_store in BASIC.*) + (*destruct Mem.storev. 2: { discriminate BASIC. }*) + (*inv BASIC; reflexivity.*) - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. } inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity. - destruct Mem.loadv. 2: { discriminate BASIC. } @@ -979,7 +980,7 @@ Lemma eval_addressing_preserved a rs1 rs2: Proof. intros EQ. destruct a; simpl; try (rewrite !EQ; congruence). - (*auto. TODO *) + auto. Qed. Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence). @@ -1084,24 +1085,24 @@ Proof. Qed. *) -Lemma store_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk a: forall - (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) - (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) - (HSTORE: exec_store lk chk a rd rs1 m1 = Next rs1' m1'), - exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a rd rs2 m2 = Next rs2' m2' - /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). -Proof. - intros. - unfold exec_store, Asm.exec_store in *. - inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. - rewrite <- (eval_addressing_preserved a rs1 rs2); auto. - destruct (Mem.storev _ _ _ _). - + inversion HSTORE; auto. repeat (econstructor; eauto). - * eapply nextinstr_agree_but_pc; intros. - subst. apply EQR. auto. - * eapply ptrofs_nextinstr_agree; subst; eauto. - + next_stuck_cong. -Qed. +(*Lemma store_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk a: forall*) + (*(BOUNDED: 0 <= n <= Ptrofs.max_unsigned)*) + (*(MATCHI: match_internal n (State rs1 m1) (State rs2 m2))*) + (*(HSTORE: exec_store lk chk a rd rs1 m1 = Next rs1' m1'),*) + (*exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a rd rs2 m2 = Next rs2' m2'*) + (*/\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').*) +(*Proof.*) + (*intros.*) + (*unfold exec_store, Asm.exec_store in *.*) + (*inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.*) + (*rewrite <- (eval_addressing_preserved a rs1 rs2); auto.*) + (*destruct (Mem.storev _ _ _ _).*) + (*+ inversion HSTORE; auto. repeat (econstructor; eauto).*) + (** eapply nextinstr_agree_but_pc; intros.*) + (*subst. apply EQR. auto.*) + (** eapply ptrofs_nextinstr_agree; subst; eauto.*) + (*+ next_stuck_cong.*) +(*Qed.*) Lemma next_inst_preserved n rs1 m1 rs1' m1' rs2 m2 (x: dreg) v: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) @@ -1275,8 +1276,9 @@ Proof. (*destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto;*) (*intros; simpl in *; destruct sz; eauto. }*)} { (* PStore *) - destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto; - simpl in *; inv_matchi; find_rwrt_ag. } + admit. } + (*destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto;*) + (*simpl in *; inv_matchi; find_rwrt_ag. }*) { (* Pallocframe *) monadInv TRANSBI; inv_matchi; try pc_not_sp; -- cgit