Adding semantics for Pldp

This commit prepare the backend for a peephole optimization in Asmblock.

1 files changed, 18 insertions, 18 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index b25a95da..abc9162b 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -280,13 +280,13 @@ Definition indexed_memory_access_bc (insn: addressing -> basic)
 
 Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
   match ty, preg_of dst with
-  | Tint,    IR rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k)
-  | Tlong,   IR rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k)
-  | Tsingle, FR rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k)
-  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k)
-  | Tany32,  IR rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k)
-  | Tany64,  IR rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k)
-  | Tany64,  FR rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k)
+  | Tint,    IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw rd) 4 base ofs k)
+  | Tlong,   IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx rd) 8 base ofs k)
+  | Tsingle, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrs rd) 4 base ofs k)
+  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd rd) 8 base ofs k)
+  | Tany32,  IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw_a rd) 4 base ofs k)
+  | Tany64,  IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx_a rd) 8 base ofs k)
+  | Tany64,  FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd_a rd) 8 base ofs k)
   | _, _           => Error (msg "Asmgen.loadind")
   end.
 
@@ -303,7 +303,7 @@ Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode
   end.
 
 Definition loadptr_bc (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bcode): bcode :=
-  indexed_memory_access_bc (PLoad Pldrx dst) 8 base ofs k. 
+  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.
@@ -1096,25 +1096,25 @@ Definition transl_load (chunk: memory_chunk) (addr: Op.addressing)
                        (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
   match chunk with
   | Mint8unsigned =>
-      do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrb W) rd) k
+      do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrb W) rd) k
   | Mint8signed =>
-      do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrsb W) rd) k
+      do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrsb W) rd) k
   | Mint16unsigned =>
-      do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrh W) rd) k
+      do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrh W) rd) k
   | Mint16signed =>
-      do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrsh W) rd) k
+      do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrsh W) rd) k
   | Mint32 =>
-      do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw rd) k
+      do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw rd) k
   | Mint64 =>
-      do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx rd) k
+      do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx rd) k
   | Mfloat32 =>
-      do rd <- freg_of dst; transl_addressing 4 addr args (PLoad Pldrs rd) k
+      do rd <- freg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrs rd) k
   | Mfloat64 =>
-      do rd <- freg_of dst; transl_addressing 8 addr args (PLoad Pldrd rd) k
+      do rd <- freg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrd rd) k
   | Many32 =>
-      do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw_a rd) k
+      do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw_a rd) k
   | Many64 =>
-      do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx_a rd) k
+      do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx_a rd) k
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)