Big improvment in peephole, changing LDP/STP semantics

1 files changed, 20 insertions, 20 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 719c3b61..5d9cf601 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -193,16 +193,16 @@ Inductive instruction: Type :=
   | Pldrsh (sz: isize) (rd: ireg) (a: addressing)                     (**r load int16, sign-extend *)
   | Pldrzw (rd: ireg) (a: addressing)                                 (**r load int32, zero-extend to int64 *)
   | Pldrsw (rd: ireg) (a: addressing)                                 (**r load int32, sign-extend to int64 *)
-  | Pldpw (rd1 rd2: ireg) (a: addressing)                               (**r load two int32 *)
-  | Pldpx (rd1 rd2: ireg) (a: addressing)                               (**r load two int64 *)
+  | Pldpw (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two int32 *)
+  | Pldpx (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two int64 *)
   | Pstrw (rs: ireg) (a: addressing)                                  (**r store int32 *)
   | Pstrw_a (rs: ireg) (a: addressing)                                (**r store int32 as any32 *)
   | Pstrx (rs: ireg) (a: addressing)                                  (**r store int64 *)
   | Pstrx_a (rs: ireg) (a: addressing)                                (**r store int64 as any64 *)
   | Pstrb (rs: ireg) (a: addressing)                                  (**r store int8 *)
   | Pstrh (rs: ireg) (a: addressing)                                  (**r store int16 *)
-  | Pstpw (rs1 rs2: ireg) (a: addressing)                              (**r store two int64 *)
-  | Pstpx (rs1 rs2: ireg) (a: addressing)                              (**r store two int64 *)
+  | Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)                              (**r store two int64 *)
+  | Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)                              (**r store two int64 *)
   (** Integer arithmetic, immediate *)
   | Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r addition *)
   | Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r subtraction *)
@@ -845,16 +845,16 @@ Definition exec_load (chunk: memory_chunk) (transf: val -> val)
   | Some v => Next (nextinstr (rs#r <- (transf v))) m
   end.
 
-Definition exec_load_double (chunk: memory_chunk) (transf: val -> val)
+Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val)
                      (a: addressing) (rd1 rd2: preg) (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
+    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
-        match Mem.loadv chunk m addr with
+        match Mem.loadv chk1 m addr with
         | None => Stuck
         | Some v1 =>
-            match Mem.loadv chunk m addr' with
+            match Mem.loadv chk2 m addr' with
             | None => Stuck
             | Some v2 =>
                 Next (nextinstr ((rs#rd1 <- (transf v1))#rd2 <- (transf v2))) m
@@ -870,16 +870,16 @@ Definition exec_store (chunk: memory_chunk)
   | Some m' => Next (nextinstr rs) m'
   end.
 
-Definition exec_store_double (chunk: memory_chunk)
+Definition exec_store_double (chk1 chk2: memory_chunk)
                       (a: addressing) (v1 v2: val)
                       (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
+    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
-      match Mem.storev chunk m addr v1 with
+      match Mem.storev chk1 m addr v1 with
       | None => Stuck
-      | Some m' => match Mem.storev chunk m' addr' v2 with
+      | Some m' => match Mem.storev chk2 m' addr' v2 with
                    | None => Stuck
                    | Some m'' => Next (nextinstr rs) m''
                    end
@@ -1311,15 +1311,15 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pbuiltin ef args res => Stuck    (**r treated specially below *)
   (** The following instructions and directives are not generated directly
       by Asmgen, so we do not model them. *)
-  | Pldpw rd1 rd2 a =>
-      exec_load_double Mint32 (fun v => v) a rd1 rd2 rs m
-  | Pldpx rd1 rd2 a =>
-      exec_load_double Mint64 (fun v => v) a rd1 rd2 rs m
+  | Pldpw rd1 rd2 chk1 chk2 a =>
+      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
+  | Pldpx rd1 rd2 chk1 chk2 a =>
+      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
   | Pnop => Next (nextinstr rs) m
-  | Pstpw rs1 rs2 a =>
-      exec_store_double Mint32 a rs#rs1 rs#rs2 rs m
-  | Pstpx rs1 rs2 a =>
-      exec_store_double Mint64 a rs#rs1 rs#rs2 rs m
+  | Pstpw rs1 rs2 chk1 chk2 a =>
+      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
+  | Pstpx rs1 rs2 chk1 chk2 a =>
+      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
   | Pcls _ _ _
   | Pclz _ _ _
   | Prev _ _ _