a first working draft on ldp/stp peephole

1 files changed, 227 insertions, 52 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 059f234c..bdfb9ed3 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -166,14 +166,15 @@ Inductive arith_op :=
 .
 
 Inductive store_op :=
-  | Ostore1 (st: store_rs_a) (a: addressing)
-  | Ostore2 (st: store_rs_a) (a: addressing)
-  | OstoreU (st: store_rs_a) (a: addressing)
+  | Ostore1 (st: st_instruction) (a: addressing)
+  | Ostore2 (st: st_instruction) (a: addressing)
+  | OstoreU (st: st_instruction) (a: addressing)
 .
 
 Inductive load_op :=
   | Oload1 (ld: ld_instruction) (a: addressing)
   | Oload2 (ld: ld_instruction) (a: addressing)
+  | OloadU (ld: ld_instruction) (a: addressing)
 .
 
 Inductive allocf_op :=
@@ -423,16 +424,16 @@ Definition call_ll_storev (c: memory_chunk) (m: mem) (v: option val) (vs: val) :
   | None => None (* should never occurs *)
   end.
 
-Definition exec_store1 (n: store_rs_a) (m: mem) (a: addressing) (vr vs: val) :=
+Definition exec_store1 (n: st_instruction) (m: mem) (a: addressing) (vr vs: val) :=
   let v :=
     match a with
     | ADimm _ n => Some (Val.addl vs (Vlong n))
     | ADadr _ id ofs => Some (Val.addl vs (symbol_low Ge.(_lk) id ofs))
     | _ => None
     end in
-  call_ll_storev (chunk_store_rs_a n) m v vr.
+  call_ll_storev (chunk_store n) m v vr.
 
-Definition exec_store2 (n: store_rs_a) (m: mem) (a: addressing) (vr vs1 vs2: val) :=
+Definition exec_store2 (n: st_instruction) (m: mem) (a: addressing) (vr vs1 vs2: val) :=
   let v :=
     match a with
     | ADreg _ _ => Some (Val.addl vs1 vs2)
@@ -441,10 +442,10 @@ Definition exec_store2 (n: store_rs_a) (m: mem) (a: addressing) (vr vs1 vs2: val
     | ADuxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofintu vs2) (Vint n)))
     | _ => None
     end in
-  call_ll_storev (chunk_store_rs_a n) m v vr.
+  call_ll_storev (chunk_store n) m v vr.
   
-Definition exec_storeU (n: store_rs_a) (m: mem) (a: addressing) (vr: val) :=
-  call_ll_storev (chunk_store_rs_a n) m None vr.
+Definition exec_storeU (n: st_instruction) (m: mem) (a: addressing) (vr: val) :=
+  call_ll_storev (chunk_store n) m None vr.
 
 Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
   match label_pos lbl 0 (fn_blocks f) with
@@ -537,10 +538,14 @@ Definition exec_load2 (ld: ld_instruction) (m: mem) (a: addressing) (vl1 vl2: va
     end in
   call_ll_loadv (chunk_load ld) (interp_load ld) m v.
   
+Definition exec_loadU (n: ld_instruction) (m: mem) (a: addressing) :=
+  call_ll_loadv (chunk_load n) (interp_load n) m None.
+
 Definition load_eval (o: load_op) (l: list value) :=
   match o, l with
   | Oload1 ld a, [Val vs; Memstate m] => exec_load1 ld m a vs
   | Oload2 ld a, [Val vs1; Val vs2; Memstate m] => exec_load2 ld m a vs1 vs2
+  | OloadU st a, [Memstate m] => exec_loadU st m a
   | _, _ => None
   end.
 
@@ -764,18 +769,18 @@ Opaque control_op_eq_correct.
 Definition store_op_eq (s1 s2: store_op): ?? bool :=
   match s1 with
   | Ostore1 st1 a1 =>
-      match s2 with Ostore1 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
+      match s2 with Ostore1 st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
   | Ostore2 st1 a1 =>
-      match s2 with Ostore2 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
+      match s2 with Ostore2 st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
   | OstoreU st1 a1 =>
-      match s2 with OstoreU st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
+      match s2 with OstoreU st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
   end.
 
 Lemma store_op_eq_correct s1 s2:
   WHEN store_op_eq s1 s2 ~> b THEN b = true -> s1 = s2.
 Proof.
   destruct s1, s2; wlp_simplify; try congruence.
-  all: rewrite H0 in H; rewrite H; reflexivity.
+  all: rewrite H1 in H0; rewrite H0, H; reflexivity.
 Qed.
 Hint Resolve store_op_eq_correct: wlp.
 Opaque store_op_eq_correct.
@@ -783,16 +788,18 @@ Opaque store_op_eq_correct.
 Definition load_op_eq (l1 l2: load_op): ?? bool :=
   match l1 with
   | Oload1 ld1 a1 =>
-      match l2 with Oload1 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
+      match l2 with Oload1 ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
   | Oload2 ld1 a1 =>
-      match l2 with Oload2 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
+      match l2 with Oload2 ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
+  | OloadU ld1 a1 =>
+      match l2 with OloadU ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
   end.
 
 Lemma load_op_eq_correct l1 l2:
   WHEN load_op_eq l1 l2 ~> b THEN b = true -> l1 = l2.
 Proof.
   destruct l1, l2; wlp_simplify; try congruence.
-  all: rewrite H0 in H; rewrite H; reflexivity.
+  all: rewrite H1 in H0; rewrite H, H0; reflexivity.
 Qed.
 Hint Resolve load_op_eq_correct: wlp.
 Opaque load_op_eq_correct.
@@ -1120,7 +1127,7 @@ Definition trans_arith (ai: ar_instruction) : inst :=
   | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))]
   end.
 
-Definition eval_addressing_rlocs_st (st: store_rs_a) (rs: dreg) (a: addressing) :=
+Definition eval_addressing_rlocs_st (st: st_instruction) (rs: dreg) (a: addressing) :=
   match a with
   | ADimm base n => Op (Store (Ostore1 st a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil)
   | ADreg base r => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
@@ -1147,10 +1154,42 @@ Definition trans_load (ldi: ld_instruction) :=
   | PLd_rd_a ld r a =>
       let lr := eval_addressing_rlocs_ld ldi a in [(#r, lr)]
   | Pldp ld r1 r2 a =>
-      let lr := eval_addressing_rlocs_ld ldi a in
+      let ldi' :=
+        match ld with
+        | Pldpw => Pldrw
+        | Pldpx => Pldrx
+        end in
+      let lr := eval_addressing_rlocs_ld (PLd_rd_a ldi' r1 a) a in
+      let ofs := match ld with | Pldpw => 4%Z | Pldpx => 8%Z end in
+      match a with
+      | ADimm base n =>
+        let a' := (get_offset_addr a ofs) in
+          [(#r1, lr);
+           (#r2, Op (Load (Oload1 (PLd_rd_a ldi' r2 a') a'))
+            (Old(PReg (#base)) @ PReg (pmem) @ Enil))]
+      | _ => [(#PC, (Op (OError)) Enil)]
+      end
+  end.
+
+Definition trans_store (sti: st_instruction) :=
+  match sti with
+  | PSt_rs_a st r a =>
+      let lr := eval_addressing_rlocs_st sti r a in [(pmem, lr)]
+  | Pstp st r1 r2 a =>
+      let sti' :=
+        match st with
+        | Pstpw => Pstrw
+        | Pstpx => Pstrx
+        end in
+      let lr := eval_addressing_rlocs_st (PSt_rs_a sti' r1 a) r1 a in
+      let ofs := match st with | Pstpw => 4%Z | Pstpx => 8%Z end in
       match a with
-      | ADpostincr base n => [(#base, lr); (#r1, lr); (#r2, lr)]
-      | _ => [(#r1, lr); (#r2, lr)]
+      | ADimm base n =>
+        let a' := (get_offset_addr a ofs) in
+          [(pmem, lr);
+           (pmem, Op (Store (Ostore1 (PSt_rs_a sti' r2 a') a'))
+            (PReg (#r2) @ Old(PReg (#base)) @ PReg (pmem) @ Enil))]
+      | _ => [(#PC, (Op (OError)) Enil)]
       end
   end.
 
@@ -1158,8 +1197,7 @@ Definition trans_basic (b: basic) : inst :=
   match b with
   | PArith ai => trans_arith ai
   | PLoad ld => trans_load ld
-  | PStore st r a => 
-      let lr := eval_addressing_rlocs_st st r a in [(pmem, lr)]
+  | PStore st => trans_store st
   | Pallocframe sz linkofs =>
       [(#X29, PReg(#SP));
        (#SP, Op (Allocframe (OAllocf_SP sz linkofs)) (PReg (#SP) @ PReg pmem @ Enil));
@@ -1173,6 +1211,7 @@ Definition trans_basic (b: basic) : inst :=
   | Pcvtsw2x rd r1 => [(#rd, Op (Cvtsw2x) (PReg (#r1) @ Enil))]
   | Pcvtuw2x rd r1 => [(#rd, Op (Cvtuw2x) (PReg (#r1) @ Enil))]
   | Pcvtx2w rd => [(#rd, Op (Cvtx2w) (PReg (#rd) @ Enil))]
+  | Pnop => []
   end.
 
 Fixpoint trans_body (b: list basic) : list L.inst :=
@@ -1673,20 +1712,46 @@ Local Ltac preg_eq_discr r rd :=
   6,7,8,9: Simpl sr.
   - (* Arith *)
     exploit trans_arith_correct; eauto.
-  - (* Load *) admit.
-    (*unfold exec_load, eval_addressing_rlocs_ld, exp_eval;*)
-    (*destruct a; simpl; try destruct base; Simpl_exists sr; erewrite H;*)
-    (*unfold exec_load1, exec_load2, exec_loadU; unfold call_ll_loadv;*)
-    (*try destruct (Mem.loadv _ _ _); simpl; auto.*)
-    (*all: DDRM rd; Simpl_exists sr; try intros rr; Simpl_update.*)
+  - (* Load *)
+    destruct ld.
+    + unfold exec_load, exec_load_rd_a, eval_addressing_rlocs_ld, exp_eval;
+      destruct ld; destruct a; simpl;
+      try fold (ppos base); try fold (ppos r);
+      erewrite !H0, H; simpl;
+      unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv;
+      try destruct (Mem.loadv _ _ _); simpl; auto.
+      all: try (fold (ppos rd); Simpl_exists sr; auto; intros rr; Simpl_update).
+    + unfold exec_load, exec_load_double, eval_addressing_rlocs_ld, exp_eval;
+      destruct ld; destruct a; simpl; unfold control_eval; destruct Ge; auto;
+      try fold (ppos base);
+      try erewrite !H0, H; simpl;
+      unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv;
+      try destruct (Mem.loadv _ _ _); simpl; auto;
+      fold (ppos rd1); rewrite assign_diff; discriminate_ppos; rewrite H;
+      try destruct (Mem.loadv _ _ _); simpl; auto; Simpl_exists sr;
+      try (rewrite !assign_diff; discriminate_ppos; reflexivity);
+      try (destruct base; discriminate_ppos);
+      repeat (try fold (ppos r); intros; Simpl_update).
   - (* Store *)
-    admit.
-    (*unfold exec_store, eval_addressing_rlocs_st, exp_eval;*)
-    (*destruct a; simpl; DIRN1 r; try destruct base; Simpl_exists sr; erewrite H;*)
-    (*unfold exec_store1, exec_store2, exec_storeU; unfold call_ll_storev;*)
-    (*try destruct (Mem.storev _ _ _ _); simpl; auto.*)
-    (*all: eexists; split; [| split]; [ eauto | eauto |*)
-    (*intros rr; rewrite assign_diff; [ rewrite H0; auto | apply ppos_pmem_discr ]].*)
+    destruct st.
+    + unfold exec_store, exec_store_rs_a, eval_addressing_rlocs_st, exp_eval;
+      destruct st; destruct a; simpl;
+      try fold (ppos base); try fold (ppos rs); try fold (ppos r);
+      erewrite !H0, H; simpl;
+      unfold exec_store1, exec_store2, chunk_store; unfold call_ll_storev;
+      try destruct (Mem.storev _ _ _ _); simpl; auto.
+      all: eexists; split; [| split]; eauto;
+      intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos.
+    + unfold exec_store, exec_store_double, eval_addressing_rlocs_st, exp_eval;
+      destruct st; destruct a; simpl; unfold control_eval; destruct Ge; auto;
+      try fold (ppos base); try fold (ppos rs1);
+      erewrite !H0, H; simpl;
+      unfold exec_store1, exec_store2, chunk_store; unfold call_ll_storev;
+      try destruct (Mem.storev _ _ _ _); simpl; auto;
+      fold (ppos rs2); rewrite assign_diff; try congruence; try rewrite H0; simpl;
+      try destruct (Mem.storev _ _ _ _); simpl; auto.
+      all: eexists; split; [| split]; eauto;
+      repeat (try intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos).
   - (* Alloc *)
     destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
     + eexists; repeat split. 
@@ -2052,6 +2117,21 @@ Definition freg_name (fr: freg) : pstring :=
   end
 .
 
+Definition iregsp_name (irsp: iregsp) : pstring :=
+  match irsp with
+  | RR1 ir => ireg_name ir
+  | XSP => Str ("XSP")
+  end.
+
+Definition dreg_name (dr: dreg) : ?? pstring :=
+  match dr with
+  | IR ir => match ir with
+             | XSP => RET (Str ("XSP"))
+             | RR1 irr => RET (ireg_name irr)
+             end
+  | FR fr => RET (freg_name fr)
+  end.
+
 Definition string_of_name (x: P.R.t): ?? pstring := 
   if (Pos.eqb x pmem) then 
     RET (Str "MEM")
@@ -2064,13 +2144,7 @@ Definition string_of_name (x: P.R.t): ?? pstring :=
                       | CV => RET (Str ("CV"))
                       end
     | Some (PC) => RET (Str ("PC"))
-    | Some (DR dr) => match dr with
-                      | IR ir => match ir with
-                                 | XSP => RET (Str ("XSP"))
-                                 | RR1 irr => RET (ireg_name irr)
-                                 end
-                      | FR fr => RET (freg_name fr)
-                      end
+    | Some (DR dr) => dreg_name dr
     | _ => RET (Str ("UNDEFINED"))
     end.
 
@@ -2339,17 +2413,118 @@ Definition string_of_arith (op: arith_op): pstring :=
   | Ofnmul _ => "Ofnmul"
   end.
 
-Definition string_of_store (op: store_op) : pstring :=
-  match op with
-  | Ostore1 _ _ => "Ostore1"
-  | Ostore2 _ _ => "Ostore2"
-  | OstoreU _ _ => "OstoreU"
+Definition string_of_ofs (ofs: ptrofs) : ?? pstring :=
+  (string_of_Z (Ptrofs.signed ofs)).
+
+Definition string_of_int (n: int) : ?? pstring :=
+  (string_of_Z (Int.signed n)).
+
+Definition string_of_int64 (n: int64) : ?? pstring :=
+  (string_of_Z (Int64.signed n)).
+
+Notation "x +; y" := (Concat x y).
+
+Definition string_of_addressing (a: addressing) : ?? pstring :=
+  match a with
+  | ADimm base n =>
+      DO n' <~ string_of_int64 n;;
+      RET ((Str "[ADimm ") +; (iregsp_name base) +; " " +; n' +; "]")
+  | ADreg base r =>
+      RET ((Str "[ADreg ") +; (iregsp_name base) +; " " +; (ireg_name r) +; "]")
+  | ADlsl base r n =>
+      DO n' <~ string_of_int n;;
+      RET ((Str "[ADlsl ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]")
+  | ADsxt base r n =>
+      DO n' <~ string_of_int n;;
+      RET ((Str "[ADsxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]")
+  | ADuxt base r n =>
+      DO n' <~ string_of_int n;;
+      RET ((Str "[ADuxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]")
+  | ADadr base id ofs =>
+      DO id' <~ string_of_Z (Zpos id);;
+      DO ofs' <~ string_of_ofs ofs;;
+      RET ((Str "[ADadr ") +; (iregsp_name base) +; " " +; id' +; " " +; ofs' +; "]")
+  | ADpostincr base n =>
+      DO n' <~ string_of_int64 n;;
+      RET ((Str "[ADpostincr ") +; (iregsp_name base) +; " " +; n' +; "]")
+  end.
+
+Definition string_of_ld_rd_a (ld: load_rd_a) : pstring :=
+  match ld with
+  | Pldrw => Str "Pldrw"
+  | Pldrw_a => Str "Pldrw_a"
+  | Pldrx => Str "Pldrx"
+  | Pldrx_a => Str "Pldrx_a"
+  | Pldrb _ => Str "Pldrb"
+  | Pldrsb _ => Str "Pldrsb"
+  | Pldrh _ => Str "Pldrh"
+  | Pldrsh _ => Str "Pldrsh"
+  | Pldrzw => Str "Pldrzw"
+  | Pldrsw => Str "Pldrsw"
+  | Pldrs => Str "Pldrs"
+  | Pldrd => Str "Pldrd"
+  | Pldrd_a => Str "Pldrd_a"
+  end.
+
+Definition string_of_ldi (ldi: ld_instruction) : ?? pstring:=
+  match ldi with
+  | PLd_rd_a ld rd a =>
+      DO a' <~ string_of_addressing a;;
+      DO rd' <~ dreg_name rd;;
+      RET (Str "PLd_rd_a (" +; (string_of_ld_rd_a ld) +; " " +; rd' +; " " +; a' +; ")")
+  | Pldp _ _ _ a =>
+      DO a' <~ string_of_addressing a;;
+      RET (Str "Pldp (" +; a' +; ")")
   end.
 
-Definition string_of_load (op: load_op) : pstring :=
+Definition string_of_load (op: load_op) : ?? pstring :=
+  match op with
+  | Oload1 ld a =>
+      DO a' <~ string_of_addressing a;;
+      DO ld' <~ string_of_ldi ld;;
+      RET((Str "Oload1 ") +; " " +; ld' +; " " +; a' +; " ")
+  | Oload2 ld a =>
+      DO a' <~ string_of_addressing a;;
+      DO ld' <~ string_of_ldi ld;;
+      RET((Str "Oload2 ") +; " " +; ld' +; " " +; a' +; " ")
+  | OloadU _ _ => RET (Str "OloadU")
+  end.
+
+Definition string_of_st_rs_a (st: store_rs_a) : pstring :=
+  match st with
+  | Pstrw => Str "Pstrw"
+  | Pstrw_a => Str "Pstrw_a"
+  | Pstrx => Str "Pstrx"
+  | Pstrx_a => Str "Pstrx_a"
+  | Pstrb => Str "Pstrb"
+  | Pstrh => Str "Pstrh"
+  | Pstrs => Str "Pstrs"
+  | Pstrd => Str "Pstrd"
+  | Pstrd_a => Str "Pstrd_a"
+  end.
+
+Definition string_of_sti (sti: st_instruction) : ?? pstring:=
+  match sti with
+  | PSt_rs_a st rs a =>
+      DO a' <~ string_of_addressing a;;
+      DO rs' <~ dreg_name rs;;
+      RET (Str "PSt_rs_a (" +; (string_of_st_rs_a st) +; " " +; rs' +; " " +; a' +; ")")
+  | Pstp _ _ _ a =>
+      DO a' <~ string_of_addressing a;;
+      RET (Str "Pstp (" +; a' +; ")")
+  end.
+
+Definition string_of_store (op: store_op) : ?? pstring :=
   match op with
-  | Oload1 _ _ => "Oload1"
-  | Oload2 _ _ => "Oload2"
+  | Ostore1 st a =>
+      DO a' <~ string_of_addressing a;;
+      DO st' <~ string_of_sti st;;
+      RET((Str "Ostore1 ") +; " " +; st' +; " " +; a' +; " ")
+  | Ostore2 st a =>
+      DO a' <~ string_of_addressing a;;
+      DO st' <~ string_of_sti st;;
+      RET((Str "Ostore2 ") +; " " +; st' +; " " +; a' +; " ")
+  | OstoreU _ _ => RET (Str "OstoreU")
   end.
 
 Definition string_of_control (op: control_op) : pstring :=
@@ -2382,8 +2557,8 @@ Definition string_of_freef (op: freef_op) : pstring :=
 Definition string_of_op (op: P.op): ?? pstring := 
   match op with
   | Arith op => RET (string_of_arith op)
-  | Load op => RET (string_of_load op)
-  | Store op => RET (string_of_store op)
+  | Load op => string_of_load op
+  | Store op => string_of_store op
   | Control op => RET (string_of_control op)
   | Allocframe op => RET (string_of_allocf op)
   | Freeframe op => RET (string_of_freef op)