a first working draft on ldp/stp peephole

1 files changed, 16 insertions, 16 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index abc9162b..137b5871 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -292,13 +292,13 @@ Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode)
 
 Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode) :=
   match ty, preg_of src with
-  | Tint,    IR rd => OK (indexed_memory_access_bc (PStore Pstrw rd) 4 base ofs k)
-  | Tlong,   IR rd => OK (indexed_memory_access_bc (PStore Pstrx rd) 8 base ofs k)
-  | Tsingle, FR rd => OK (indexed_memory_access_bc (PStore Pstrs rd) 4 base ofs k)
-  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PStore Pstrd rd) 8 base ofs k)
-  | Tany32,  IR rd => OK (indexed_memory_access_bc (PStore Pstrw_a rd) 4 base ofs k)
-  | Tany64,  IR rd => OK (indexed_memory_access_bc (PStore Pstrx_a rd) 8 base ofs k)
-  | Tany64,  FR rd => OK (indexed_memory_access_bc (PStore Pstrd_a rd) 8 base ofs k)
+  | Tint,    IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrw rd) 4 base ofs k)
+  | Tlong,   IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrx rd) 8 base ofs k)
+  | Tsingle, FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrs rd) 4 base ofs k)
+  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrd rd) 8 base ofs k)
+  | Tany32,  IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrw_a rd) 4 base ofs k)
+  | Tany64,  IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrx_a rd) 8 base ofs k)
+  | Tany64,  FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrd_a rd) 8 base ofs k)
   | _, _           => Error (msg "Asmgen.storeind")
   end.
 
@@ -306,7 +306,7 @@ Definition loadptr_bc (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bcode): bcode
   indexed_memory_access_bc (PLd_rd_a Pldrx dst) 8 base ofs k. 
 
 Definition storeptr_bc (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bcode): bcode :=
-  indexed_memory_access_bc (PStore Pstrx src) 8 base ofs k.
+  indexed_memory_access_bc (PSt_rs_a Pstrx src) 8 base ofs k.
 
 (** Function epilogue *)
 
@@ -1121,21 +1121,21 @@ Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
                         (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
   match chunk with
   | Mint8unsigned | Mint8signed =>
-      do r1 <- ireg_of src; transl_addressing 1 addr args (PStore Pstrb r1) k
+      do r1 <- ireg_of src; transl_addressing 1 addr args (PSt_rs_a Pstrb r1) k
   | Mint16unsigned | Mint16signed =>
-      do r1 <- ireg_of src; transl_addressing 2 addr args (PStore Pstrh r1) k
+      do r1 <- ireg_of src; transl_addressing 2 addr args (PSt_rs_a Pstrh r1) k
   | Mint32 =>
-      do r1 <- ireg_of src; transl_addressing 4 addr args (PStore Pstrw r1) k
+      do r1 <- ireg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrw r1) k
   | Mint64 =>
-      do r1 <- ireg_of src; transl_addressing 8 addr args (PStore Pstrx r1) k
+      do r1 <- ireg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrx r1) k
   | Mfloat32 =>
-      do r1 <- freg_of src; transl_addressing 4 addr args (PStore Pstrs r1) k
+      do r1 <- freg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrs r1) k
   | Mfloat64 =>
-      do r1 <- freg_of src; transl_addressing 8 addr args (PStore Pstrd r1) k
+      do r1 <- freg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrd r1) k
   | Many32 =>
-      do r1 <- ireg_of src; transl_addressing 4 addr args (PStore Pstrw_a r1) k
+      do r1 <- ireg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrw_a r1) k
   | Many64 =>
-      do r1 <- ireg_of src; transl_addressing 8 addr args (PStore Pstrx_a r1) k
+      do r1 <- ireg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrx_a r1) k
   end.
 
 (** Translation of a Machblock instruction. *)