a first working draft on ldp/stp peephole

1 files changed, 26 insertions, 24 deletions

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;