a first working draft on ldp/stp peephole

1 files changed, 46 insertions, 18 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 33f1013a..719c3b61 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -201,7 +201,8 @@ Inductive instruction: Type :=
   | 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 *)
-  | Pstp (rs1 rs2: ireg) (a: addressing)                              (**r store two int64 *)
+  | Pstpw (rs1 rs2: ireg) (a: addressing)                              (**r store two int64 *)
+  | Pstpx (rs1 rs2: ireg) (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 *)
@@ -820,13 +821,19 @@ Definition eval_addressing (a: addressing) (rs: regset): val :=
   | ADsxt base r n => Val.addl rs#base (Val.shll (Val.longofint rs#r) (Vint n))
   | ADuxt base r n => Val.addl rs#base (Val.shll (Val.longofintu rs#r) (Vint n))
   | ADadr base id ofs => Val.addl rs#base (symbol_low ge id ofs)
-  | ADpostincr base n => rs#base
+  | ADpostincr base n => Vundef
   end.
 
-Definition eval_addressing_update (a: addressing) (rs: regset): regset :=
+Definition is_pair_addressing_mode_correct (a: addressing): bool :=
   match a with
-  | ADpostincr base n => rs#base <- (Vlong n)
-  | _ => rs
+  | ADimm _ _ => true
+  | _ => false
+  end.
+
+Definition get_offset_addr (a: addressing) (ofs: Z) : addressing :=
+  match a with
+  | ADimm base n => (ADimm base (Int64.add n (Int64.repr ofs)))
+  | _ => a
   end.
 
 (** Auxiliaries for memory accesses *)
@@ -840,17 +847,20 @@ Definition exec_load (chunk: memory_chunk) (transf: val -> val)
 
 Definition exec_load_double (chunk: memory_chunk) (transf: val -> val)
                      (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) :=
-  let addr := (eval_addressing a rs) in
-  let ofs := match chunk with | Mint32 => 4 | _ => 8 end in
-      match Mem.loadv Mint32 m addr with
-      | None => Stuck
-      | Some v1 =>
-          match Mem.loadv Mint32 m (Val.offset_ptr addr (Ptrofs.repr ofs)) with
-          | None => Stuck
-          | Some v2 =>
-              Next (nextinstr (((eval_addressing_update a rs)#rd1 <- (transf v1))#rd2 <- (transf v2))) m
-          end
-      end.
+  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 addr' := (eval_addressing (get_offset_addr a ofs) rs) in
+        match Mem.loadv chunk m addr with
+        | None => Stuck
+        | Some v1 =>
+            match Mem.loadv chunk m addr' with
+            | None => Stuck
+            | Some v2 =>
+                Next (nextinstr ((rs#rd1 <- (transf v1))#rd2 <- (transf v2))) m
+            end
+        end
+  else Stuck.
 
 Definition exec_store (chunk: memory_chunk)
                       (a: addressing) (v: val)
@@ -860,6 +870,21 @@ Definition exec_store (chunk: memory_chunk)
   | Some m' => Next (nextinstr rs) m'
   end.
 
+Definition exec_store_double (chunk: 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 addr' := (eval_addressing (get_offset_addr a ofs) rs) in
+      match Mem.storev chunk m addr v1 with
+      | None => Stuck
+      | Some m' => match Mem.storev chunk m' addr' v2 with
+                   | None => Stuck
+                   | Some m'' => Next (nextinstr rs) m''
+                   end
+      end
+  else Stuck.
 
 Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
@@ -1290,7 +1315,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       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
-  | Pstp _ _ _
+  | 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
   | Pcls _ _ _
   | Pclz _ _ _
   | Prev _ _ _
@@ -1300,7 +1329,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfmsub _ _ _ _ _
   | Pfnmadd _ _ _ _ _
   | Pfnmsub _ _ _ _ _
-  | Pnop
   | Pcfi_adjust _ 
   | Pcfi_rel_offset _ =>
       Stuck