Simplifications in Peephole and size proof.

2 files changed, 48 insertions, 116 deletions

diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v
index 6cd2e110..a1bb6c6c 100644
--- a/aarch64/Peephole.v
+++ b/aarch64/Peephole.v
@@ -48,26 +48,43 @@ Definition is_valid_strx (b1 b2: iregsp) (n1 n2: int64) : bool :=
   then true else false.
 
 (* Try to find arguments of the next compatible ldrw to replace. *)
-Fixpoint get_next_comp_ldpw_args (ldb: basic) (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (ireg * iregsp * int64) :=
+Fixpoint get_next_comp_ldpw_args (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (ireg * iregsp * int64) :=
   match t1 with
   | nil => None
   | (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) :: t2 =>
       if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then Some (rd2, b2, n2)
       else None
-  | _ :: t2 => get_next_comp_ldpw_args ldb rd1 b1 n1 t2
+  | _ :: t2 => get_next_comp_ldpw_args rd1 b1 n1 t2
   end.
 
-(*Fixpoint ldpw_follow (ldb h1: basic) (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : list basic :=
-  match (get_next_comp_ldpw_args ldb rd1 b1 n1 t1) with
-  | None => ldb :: h1 :: t1
+(* Try to delete the next compatible ldrw to replace. *)
+Fixpoint del_next_comp_ldpw_args (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : list basic :=
+  match t1 with
+  | nil => nil
+  | (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) :: t2 =>
+      if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then t2
+      else t1
+  | h2 :: t2 => h2 :: del_next_comp_ldpw_args rd1 b1 n1 t2
+  end.
+
+Fixpoint ldpw_follow (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (basic * list basic) :=
+  match (get_next_comp_ldpw_args rd1 b1 n1 t1) with
+  | None => None
   | Some (rd2, b2, n2) =>
     match t1 with
-    | nil => ldb :: h1 :: nil
+    | nil => None
     | h2 :: t2 =>
         match h2 with
-        | (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) =>
-        | 
- *)
+        | (PStore _) => None
+        | (PLd_rd_a Pldrw (IR (RR1 rd')) (ADimm b' n')) =>
+            if (ireg_eq rd' rd2) && (iregsp_eq b' b2) && (Int64.eq n' n2) then
+              Some ((PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))),
+              (del_next_comp_ldpw_args rd1 b1 n1 t1))
+            else ldpw_follow rd1 b1 n1 t2
+        | _ => ldpw_follow rd1 b1 n1 t2
+        end
+    end
+  end.
 
 Fixpoint pair_rep (insns : list basic) : list basic :=
   match insns with
@@ -81,32 +98,30 @@ Fixpoint pair_rep (insns : list basic) : list basic :=
 
         | (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)),
           (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) =>
-          (* TODO This could be insteresting to add if compatible with the checker
-          When both load the same dest, and with no reuse of ld1 in ld2. *)
-          (* if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
+          (* When both load the same dest, and with no reuse of ld1 in ld2. *)
+          if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
             Pnop :: (pair_rep t0)
           (* When two consec mem addr are loading two different dest. *)
-             else*)
-
-          if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then
+          else if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then
             (PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
           (* When nothing can be optimized. *)
           else
             h0 :: (pair_rep t0)
         | (PLd_rd_a Pldrx (IR (RR1 rd1)) (ADimm b1 n1)),
           (PLd_rd_a Pldrx (IR (RR1 rd2)) (ADimm b2 n2)) =>
-          (*if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
+          if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
             Pnop :: (pair_rep t0)
-             else*)
-
-          if (is_valid_ldrx rd1 rd2 b1 b2 n1 n2) then
+          else if (is_valid_ldrx rd1 rd2 b1 b2 n1 n2) then
             (PLoad (Pldp Pldpx rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
           else
             h0 :: (pair_rep t0)
 
         (* When there are some insts between loads/stores *)
         (*| (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)), h1 =>*)
-            (*pair_rep (ldpw_follow h0 h1 rd1 b1 n1 t1)*)
+            (*match ldpw_follow rd1 b1 n1 t1 with*)
+            (*| None => h0 :: (pair_rep t0)*)
+            (*| Some (ldpw, l) => ldpw :: Pnop :: (pair_rep l)*)
+            (*end*)
         (*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*)
 
 
@@ -144,51 +159,6 @@ Fixpoint pair_rep (insns : list basic) : list basic :=
     end
   end.
 
-(*Fixpoint stp_rep (insns : list basic) : list basic :=
-  match insns with
-  | nil => nil
-  | h0 :: t0 =>
-    match t0 with
-    | h1 :: t1 =>
-        match h0, h1 with
-        | (PSt_rs_a Pstrw (IR (RR1 rs1)) (ADimm b1 n1)),
-          (PSt_rs_a Pstrw (IR (RR1 rs2)) (ADimm b2 n2)) =>
-          let z1 := Int64.signed n1 in
-          let z2 := Int64.signed n2 in
-
-          (* When both store at the same addr, same ofs. *)
-          (*if (iregsp_eq b1 b2) && (z2 =? z1) then
-            Pnop :: (stp_rep t0)
-          (* When two consec mem addr are targeted by two store. *)
-             else*)
-
-          if (iregsp_eq b1 b2) && (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then
-            (PStore (Pstp Pstpw rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1)
-          (* When nothing can be optimized. *)
-          else
-            h0 :: (stp_rep t0)
-        | (PSt_rs_a Pstrx (IR (RR1 rs1)) (ADimm b1 n1)),
-          (PSt_rs_a Pstrx (IR (RR1 rs2)) (ADimm b2 n2)) =>
-          let z1 := Int64.signed n1 in
-          let z2 := Int64.signed n2 in
-          
-          (*if (iregsp_eq b1 b2) && (z2 =? z1) then
-            Pnop :: (stp_rep t0)
-             else*)
-
-          if (iregsp_eq b1 b2) && (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then
-            (PStore (Pstp Pstpx rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1)
-          else
-            h0 :: (stp_rep t0)
-        (*| (PLd_rd_a Pldrw rd1 (ADimm b1 n1)), h1 => ldpw_follow rd1 b1 n1*)
-        (*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*)
-        | _, _ => h0 :: (stp_rep t0)
-        end   
-    | nil => h0 :: nil
-    end
-  end.
- *)
-
 Definition optimize_body (insns : list basic) :=
   (* TODO ADD A FLAG TO ENABLE PEEPHOLE *)
   if Compopts.optim_coalesce_mem tt
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index 19bed77b..b8c16131 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -68,66 +68,28 @@ Definition do_schedule (bb: bblock) : res bblock :=
   if (Z.eqb (size bb) 1) then OK (bb) 
   else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end.
 
+Definition do_peephole (bb: bblock) : bblock :=
+  let res := Peephole.optimize_bblock bb in
+  if (size res =? size bb) then res else bb.
+
 Definition verified_schedule (bb : bblock) : res bblock :=
   let nhbb  := no_header bb in
-  let nhbb' := Peephole.optimize_bblock nhbb in
-  do nhbb'' <- do_schedule nhbb';
-  let bb' := stick_header (header bb) nhbb'' in
+  let phbb := do_peephole nhbb in
+  do schbb <- do_schedule phbb;
+  let bb' := stick_header (header bb) schbb in
   do sizecheck <- verify_size bb bb';
   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.
-  (*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.*)
+  intros. unfold verified_schedule in H.
+  monadInv H.
+  unfold verify_size in EQ1.
+  destruct (size _ =? size _) eqn:ESIZE_H in EQ1; try discriminate.
+  rewrite Z.eqb_eq in ESIZE_H; rewrite ESIZE_H; reflexivity.
+Qed.
 
 Theorem verified_schedule_correct:
   forall ge f bb bb',