Asmgen proof completely proved with ldp/stp

1 files changed, 120 insertions, 46 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index d412b129..eac406a1 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -814,14 +814,24 @@ Lemma exec_basic_dont_move_PC bi rs m rs' m': forall
 Proof.
   destruct bi; simpl; intros.
   - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto.
-  - admit.
-    (*unfold exec_load in BASIC.*)
-    (*destruct Mem.loadv. 2: { discriminate BASIC. }*)
-    (*inv BASIC. rewrite Pregmap.gso; try discriminate; auto.*)
-  - admit.
-    (*unfold exec_store in BASIC.*)
-    (*destruct Mem.storev. 2: { discriminate BASIC. }*)
-    (*inv BASIC; reflexivity.*)
+  - unfold exec_load in BASIC.
+    destruct ld.
+    + unfold exec_load_rd_a in BASIC.
+      destruct Mem.loadv. 2: { discriminate BASIC. }
+      inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
+    + unfold exec_load_double, is_pair_addressing_mode_correct in BASIC.
+      destruct a; try discriminate BASIC.
+      do 2 (destruct Mem.loadv; try discriminate BASIC).
+      inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
+  - unfold exec_store in BASIC.
+    destruct st.
+    + unfold exec_store_rs_a in BASIC.
+      destruct Mem.storev. 2: { discriminate BASIC. }
+      inv BASIC; reflexivity.
+    + unfold exec_store_double in BASIC.
+      destruct a; try discriminate BASIC.
+      do 2 (destruct Mem.storev; try 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. }
@@ -831,8 +841,8 @@ Proof.
   - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
   - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
   - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-(*Qed.*)
-Admitted.
+  - inv BASIC; auto.
+Qed.
 
 Lemma exec_body_dont_move_PC_aux:
   forall bis rs m rs' m'
@@ -1064,16 +1074,15 @@ Proof.
   rewrite <- Ptrofs.add_unsigned; rewrite <- Val.offset_ptr_assoc; rewrite AGPC; eauto.
 Qed.
 
-(* TODO
-Lemma load_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall
+Lemma load_rd_a_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall
   (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
   (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
-  (HLOAD: exec_load lk chk f a rd rs1 m1 = Next rs1' m1'),
+  (HLOAD: exec_load_rd_a lk chk f a rd rs1 m1 = Next rs1' m1'),
   exists (rs2' : regset) (m2' : mem), Asm.exec_load tge chk f a rd rs2 m2 = Next rs2' m2'
   /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
 Proof.
   intros.
-  unfold exec_load, Asm.exec_load in *.
+  unfold exec_load_rd_a, Asm.exec_load in *.
   inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
   rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
   destruct (Mem.loadv _ _ _).
@@ -1083,26 +1092,81 @@ Proof.
     * eapply ptrofs_nextinstr_agree; eauto.
   + next_stuck_cong.
 Qed.
- *)
+ 
+Lemma load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk f a: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (HLOAD: exec_load_double lk chk f a rd1 rd2 rs1 m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk f a rd1 rd2 rs2 m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  unfold exec_load_double, Asm.exec_load_double in *.
+  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+  erewrite <- !eval_addressing_preserved; eauto.
+  destruct (is_pair_addressing_mode_correct a); try discriminate.
+  destruct (Mem.loadv _ _ _);
+  destruct (Mem.loadv chk m2
+      (eval_addressing lk
+         (get_offset_addr a match chk with
+                            | Mint32 => 4
+                            | _ => 8
+                            end) rs1));
+  inversion HLOAD; auto.
+  repeat (econstructor; eauto).
+  * eapply nextinstr_agree_but_pc; intros.
+    destruct (PregEq.eq r rd2); destruct (PregEq.eq r rd1).
+    - try update_x_access_x. 
+    - try update_x_access_x.
+    - subst; repeat rewrite Pregmap.gso, Pregmap.gss; auto.
+    - try update_x_access_r.
+  * eapply ptrofs_nextinstr_agree; eauto.
+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_rs_a_preserved n rs1 m1 rs1' m1' rs2 m2 v chk a: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (HSTORE: exec_store_rs_a lk chk a v rs1 m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a v rs2 m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  unfold exec_store_rs_a, 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_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk a: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (HSTORE: exec_store_double lk chk a v1 v2 rs1 m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk a v1 v2 rs2 m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  unfold exec_store_double, Asm.exec_store_double in *.
+  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+  erewrite <- !eval_addressing_preserved; eauto.
+  destruct (is_pair_addressing_mode_correct a); try discriminate.
+  destruct (Mem.storev _ _ _ _);
+  try destruct (Mem.storev chk m
+          (eval_addressing lk
+             (get_offset_addr a match chk with
+                                | Mint32 => 4
+                                | _ => 8
+                                end) rs1) v2);
+  inversion HSTORE; auto.
+  repeat (econstructor; eauto).
+  * eapply nextinstr_agree_but_pc; intros.
+    subst. apply EQR. auto.
+  * eapply ptrofs_nextinstr_agree; subst; eauto.
+Qed.
 
 Lemma next_inst_preserved n rs1 m1 rs1' m1' rs2 m2 (x: dreg) v: forall
   (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
@@ -1271,14 +1335,17 @@ Proof.
       try (destruct_reg_size);
       try (exploit next_inst_preserved; eauto);
       try (find_rwrt_ag). } }
-  { (* PLoad TODO *)
-    admit.
-    (*destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto;*)
-    (*intros; simpl in *; destruct sz; eauto. }*)}
+  { (* PLoad *)
+    destruct ld.
+    - destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_rd_a_preserved; eauto;
+      intros; simpl in *; destruct sz; eauto.
+    - destruct ld; monadInv TRANSBI; exploit load_double_preserved; eauto. }
   { (* PStore *)
-    admit. }
-    (*destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto;*)
-    (*simpl in *; inv_matchi; find_rwrt_ag. }*)
+    destruct st.
+    - destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_rs_a_preserved; eauto;
+      simpl in *; inv_matchi; find_rwrt_ag.
+    - destruct st; monadInv TRANSBI; exploit store_double_preserved; eauto;
+      simpl in *; inv_matchi; find_rwrt_ag. }
   { (* Pallocframe *)
     monadInv TRANSBI;
     inv_matchi; try pc_not_sp;
@@ -1309,8 +1376,15 @@ Proof.
     try (exploit next_inst_preserved; eauto);
     rewrite symbol_addresses_preserved; eauto;
     try (find_rwrt_ag).
-(*Qed.*)
-Admitted.
+  { (* Pnop *)
+    monadInv TRANSBI; inv_matchi. 
+    inversion BASIC.
+    repeat (econstructor; eauto).
+    eapply nextinstr_agree_but_pc; intros;
+    try rewrite <- H0, AG; auto.
+    try eapply ptrofs_nextinstr_agree; auto; rewrite <- H0;
+    assumption. }
+Qed.
 
 Lemma find_basic_instructions b ofs f bb tc: forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
@@ -1592,11 +1666,11 @@ Lemma no_label_in_basic_inst: forall a lbl x,
 Proof.
   intros.
   destruct a; simpl in *;
-  repeat destruct i; simpl in *;
+  repeat destruct i;
+  repeat destruct ld; repeat destruct st;
+  simpl in *;
   try (try destruct_reg_inv; monadInv H; simpl in *; reflexivity).
-  admit.
-(*Qed.*)
-Admitted.
+Qed.
 
 Lemma label_pos_body bdy: forall c1 c2 z ex lbl
   (HUNF : unfold_body bdy = OK c2),