Asmgen proof completely proved with ldp/stp

6 files changed, 198 insertions, 133 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 3ad1d7f8..16f8e0c0 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -604,7 +604,7 @@ Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val)
   Next (rs#r <- (transf v)) m.
 
 Definition exec_load_double (chunk: memory_chunk) (transf: val -> val)
-                     (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) :=
+                     (a: addressing) (rd1 rd2: dreg) (rs: regset) (m: mem) :=
   if is_pair_addressing_mode_correct a then
     let addr := (eval_addressing a rs) in
     let ofs := match chunk with | Mint32 => 4 | _ => 8 end in
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index bdfb9ed3..e2d788a5 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -1781,8 +1781,9 @@ Local Ltac preg_eq_discr r rd :=
       * rewrite e; rewrite Pregmap.gss, sr_gss; auto.
       * rewrite Pregmap.gso, !assign_diff; auto; apply ppos_discr in n; auto.
     + rewrite <- sp_xsp; rewrite MLOAD; reflexivity.
-(*Qed.*)
-Admitted.
+  - (* Nop *)
+    Simpl sr.
+Qed.
 
 Theorem bisimu_body:
   forall bdy rsr mr sr,
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),
diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v
index 2282326a..167def44 100644
--- a/aarch64/Peephole.v
+++ b/aarch64/Peephole.v
@@ -17,39 +17,6 @@ Require Import Integers.
 Require Import AST.
 Require Compopts.
 
-(*Fixpoint gpreg_q_search_rec r0 r1 l :=
-  match l with
-  | h :: t =>
-    let (s0, s1) := gpreg_q_expand h in
-    if (gpreg_eq r0 s0) && (gpreg_eq r1 s1)
-    then Some h
-    else gpreg_q_search_rec r0 r1 t
-  | nil => None
-  end.
-
-Fixpoint gpreg_o_search_rec r0 r1 r2 r3 l :=
-  match l with
-  | h :: t =>
-    match gpreg_o_expand h with
-    | (((s0, s1), s2), s3) =>
-      if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) &&
-         (gpreg_eq r2 s2) && (gpreg_eq r3 s3)
-      then Some h
-      else gpreg_o_search_rec r0 r1 r2 r3 t
-    end
-  | nil => None
-  end.
-
-Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q :=
-  gpreg_q_search_rec r0 r1 gpreg_q_list.
-
-Definition gpreg_o_search r0 r1 r2 r3 : option gpreg_o :=
-  gpreg_o_search_rec r0 r1 r2 r3 gpreg_o_list.
-
-Parameter print_found_store: forall A, Z -> A -> A.
-
-   Definition coalesce_octuples := true.*)
-
 Definition is_valid_immofs_32 (z: Z) : bool :=
   if (zle z 252) && (zle (-256) z) && ((Z.modulo z 4) =? 0) then true else false.
 
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index 548976c9..19bed77b 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -77,45 +77,69 @@ Definition verified_schedule (bb : bblock) : res bblock :=
   do schedcheck <- verify_schedule bb bb';
   OK (bb').
 
+(*Lemma size_peephole_unchanged: forall bb,*)
+  (*size (Peephole.optimize_bblock (no_header bb)) = size (no_header bb).*)
+(*Proof.*)
+  (*intros.*)
+  (*unfold Peephole.optimize_bblock, size in *. simpl in *.*)
+  (*destruct non_empty_bblockb eqn:NEMPTY; auto.*)
+  (*apply inj_eq. rewrite Nat.add_cancel_r.*)
+  (*unfold Peephole.optimize_body.*)
+  (*remember (body bb) as l.*)
+  (*generalize dependent l.*)
+  (*induction l.*)
+  (*- simpl. reflexivity.*)
+  (*- intros.*)
+    (*simpl.*)
+  (*unfold Peephole.stp_rep, Peephole.ldp_rep.*)
+
 Lemma verified_schedule_size:
   forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'.
 Proof.
 Admitted.
-(* TODO
-  intros. unfold verified_schedule in H.
-  monadInv H.
-  unfold do_schedule in EQ.
-  destruct schedule in EQ.
-  destruct (size (no_header bb) =? 1) eqn:TRIVB.
-  - inv EQ. unfold size. simpl. reflexivity.
-  - unfold schedule_to_bblock in EQ.
-  destruct o in EQ.
-  + inv EQ. unfold verify_size in EQ1. unfold size in *. simpl in *.
-    rewrite Z.eqb_neq in TRIVB.
-    destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?
-    Z.of_nat (Datatypes.length (header bb) + Datatypes.length l + 1)) eqn:ESIZE; try discriminate.
-    rewrite Z.eqb_eq in ESIZE; repeat rewrite Nat2Z.inj_add in *;
-    rewrite ESIZE. reflexivity.
-  + unfold make_bblock_from_basics in EQ. destruct l in EQ; try discriminate.
-    inv EQ. unfold verify_size in EQ1; unfold size in *; simpl in *.
-    destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?
-    Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate.
-    rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *.
-    rewrite ESIZE. reflexivity.
-   Qed.*)
+  (*intros. unfold verified_schedule in H.*)
+  (*monadInv H.*)
+  (*unfold do_schedule in EQ.*)
+  (*destruct schedule in EQ.*)
+  (*destruct Peephole.optimize_bblock eqn:PEEP.*)
+  (*destruct (size (_) =? 1) eqn:TRIVB in EQ.*)
+  (*[>destruct (size (Peephole.optimize_bblock (no_header bb)) =? 1) eqn:TRIVB.<]*)
+  (*-*)
+    (*inv EQ. *)
+    (*unfold Peephole.optimize_bblock in PEEP. simpl in *.*)
+
+    (*unfold size. *)
+    (*simpl in *.*)
+
+    (*simpl. unfold non_empty_bblockb, non_empty_exit, non_empty_body.*)
+    (*reflexivity.*)
+  (*- unfold schedule_to_bblock in EQ.*)
+  (*destruct o in EQ.*)
+  (*+ inv EQ. unfold verify_size in EQ1. unfold size in *. simpl in *.*)
+    (*rewrite Z.eqb_neq in TRIVB.*)
+    (*destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?*)
+    (*Z.of_nat (Datatypes.length (header bb) + Datatypes.length l + 1)) eqn:ESIZE; try discriminate.*)
+    (*rewrite Z.eqb_eq in ESIZE; repeat rewrite Nat2Z.inj_add in *;*)
+    (*rewrite ESIZE. reflexivity.*)
+  (*+ unfold make_bblock_from_basics in EQ. destruct l in EQ; try discriminate.*)
+    (*inv EQ. unfold verify_size in EQ1; unfold size in *; simpl in *.*)
+    (*destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?*)
+    (*Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate.*)
+    (*rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *.*)
+    (*rewrite ESIZE. reflexivity.*)
+(*Qed.*)
 
 Theorem verified_schedule_correct:
   forall ge f bb bb',
   verified_schedule bb = OK bb' ->
   bblock_simu lk ge f bb bb'.
 Proof.
-Admitted.
-  (* TODO intros.*)
-  (*monadInv H.*)
-  (*eapply bblock_simub_correct.*)
-  (*unfold verify_schedule in EQ0.*)
-  (*destruct (bblock_simub _ _) in *; try discriminate; auto.*)
-(*Qed.*)
+  intros.
+  monadInv H.
+  eapply bblock_simub_correct.
+  unfold verify_schedule in EQ0.
+  destruct (bblock_simub _ _) in *; try discriminate; auto.
+Qed.
 
 End verify_schedule.
 
diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v
index 140b3aa2..48840602 100644
--- a/aarch64/PostpassSchedulingproof.v
+++ b/aarch64/PostpassSchedulingproof.v
@@ -99,28 +99,27 @@ Lemma transf_find_bblock:
      verified_schedule bb = OK tbb
      /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb.
 Proof.
-Admitted.
-  (*intros.*)
-  (*monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.*)
-  (*monadInv EQ. simpl in *.*)
-  (*generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0.*)
-  (*induction (fn_blocks f).*)
-  (*- intros. simpl in *. discriminate.*)
-  (*- intros. simpl in *.*)
-    (*monadInv EQ0. simpl.*)
-    (*destruct (zlt z 0); try discriminate.*)
-    (*destruct (zeq z 0).*)
-    (*+ inv H. eauto.*)
-    (*+ monadInv EQ0.*)
-      (*exploit IHb; eauto.*)
-      (*intros (tbb & SCH & FIND).*)
-      (*eexists; split; eauto.*)
-      (*inv FIND.*)
-      (*unfold verify_size in EQ0.*)
-      (*destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.*)
-      (*rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.*)
-      (*reflexivity.*)
-(*Qed.*)
+  intros.
+  monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.
+  monadInv EQ. simpl in *.
+  generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0.
+  induction (fn_blocks f).
+  - intros. simpl in *. discriminate.
+  - intros. simpl in *.
+    monadInv EQ0. simpl.
+    destruct (zlt z 0); try discriminate.
+    destruct (zeq z 0).
+    + inv H. eauto.
+    + monadInv EQ0.
+      exploit IHb; eauto.
+      intros (tbb & SCH & FIND).
+      eexists; split; eauto.
+      inv FIND.
+      unfold verify_size in EQ0.
+      destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.
+      rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.
+      reflexivity.
+Qed.
 
 Lemma stick_header_neutral: forall a,
   a = (stick_header (header a) (no_header a)).