Big improvment in peephole, changing LDP/STP semantics

1 files changed, 49 insertions, 54 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index f12e8922..a4decae7 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -112,7 +112,7 @@ Inductive load_rd1_rd2_a: Type :=
 
 Inductive ld_instruction: Type :=
   | PLd_rd_a (ld: load_rd_a) (rd: dreg) (a: addressing)
-  | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: ireg) (a: addressing)   (**r load two int64 *)
+  | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two int64 *)
   .
 
 Inductive store_rs_a : Type :=
@@ -136,7 +136,7 @@ Inductive store_rs1_rs2_a : Type :=
 
 Inductive st_instruction : Type :=
   | PSt_rs_a (st: store_rs_a) (rs: dreg) (a: addressing)
-  | Pstp (st: store_rs1_rs2_a) (rs1 rs2: ireg) (a: addressing)  (**r store two int64 *)
+  | Pstp (st: store_rs1_rs2_a) (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)  (**r store two int64 *)
   .
 
 Inductive arith_p : Type :=
@@ -459,16 +459,16 @@ Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val)
   SOME v <- Mem.loadv chunk m (eval_addressing a rs) IN
   Next (rs#r <- (transf v)) m.
 
-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: dreg) (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 ((rs#rd1 <- (transf v1))#rd2 <- (transf v2)) m
@@ -482,16 +482,16 @@ Definition exec_store_rs_a (chunk: memory_chunk)
   SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN
   Next rs m'.
 
-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 rs m''
                    end
@@ -501,67 +501,62 @@ Definition exec_store_double (chunk: memory_chunk)
 (** execution of loads
 *)
 
-Definition chunk_load (ld: ld_instruction): memory_chunk :=
+Definition chunk_load (ld: load_rd_a): memory_chunk :=
   match ld with
-  | PLd_rd_a Pldrw _ _ => Mint32
-  | PLd_rd_a Pldrw_a _ _ => Many32
-  | PLd_rd_a Pldrx _ _ => Mint64
-  | PLd_rd_a Pldrx_a _ _ => Many64
-  | PLd_rd_a (Pldrb _) _ _ => Mint8unsigned
-  | PLd_rd_a (Pldrsb _) _ _ => Mint8signed
-  | PLd_rd_a (Pldrh _) _ _ => Mint16unsigned
-  | PLd_rd_a (Pldrsh _) _ _ => Mint16signed
-  | PLd_rd_a Pldrzw _ _ => Mint32
-  | PLd_rd_a Pldrsw _ _ => Mint32
-  | PLd_rd_a Pldrs _ _ => Mfloat32
-  | PLd_rd_a Pldrd _ _ => Mfloat64
-  | PLd_rd_a Pldrd_a _ _ =>  Many64
-  | Pldp Pldpw _ _ _ => Mint32
-  | Pldp Pldpx _ _ _ => Mint64
+  | Pldrw => Mint32
+  | Pldrw_a => Many32
+  | Pldrx => Mint64
+  | Pldrx_a => Many64
+  | Pldrb _ => Mint8unsigned
+  | Pldrsb _ => Mint8signed
+  | Pldrh _ => Mint16unsigned
+  | Pldrsh _ => Mint16signed
+  | Pldrzw => Mint32
+  | Pldrsw => Mint32
+  | Pldrs => Mfloat32
+  | Pldrd => Mfloat64
+  | Pldrd_a =>  Many64
   end.
 
-Definition chunk_store (st: st_instruction) : memory_chunk :=
+Definition chunk_store (st: store_rs_a) : memory_chunk :=
   match st with
-  | PSt_rs_a Pstrw _ _   => Mint32
-  | PSt_rs_a Pstrw_a _ _ => Many32
-  | PSt_rs_a Pstrx _ _   => Mint64
-  | PSt_rs_a Pstrx_a _ _ => Many64
-  | PSt_rs_a Pstrb _ _   => Mint8unsigned
-  | PSt_rs_a Pstrh _ _   => Mint16unsigned
-  | PSt_rs_a Pstrs _ _   => Mfloat32
-  | PSt_rs_a Pstrd _ _   => Mfloat64
-  | PSt_rs_a Pstrd_a _ _ => Many64
-  | Pstp Pstpw _ _ _ => Mint32
-  | Pstp Pstpx _ _ _ => Mint64
+  | Pstrw => Mint32
+  | Pstrw_a => Many32
+  | Pstrx => Mint64
+  | Pstrx_a => Many64
+  | Pstrb => Mint8unsigned
+  | Pstrh => Mint16unsigned
+  | Pstrs => Mfloat32
+  | Pstrd => Mfloat64
+  | Pstrd_a => Many64
   end.
 
-Definition interp_load (ld: ld_instruction): val -> val :=
+Definition interp_load (ld: load_rd_a): val -> val :=
   match ld with
-  | PLd_rd_a (Pldrb X) _ _ => Val.longofintu
-  | PLd_rd_a (Pldrsb X) _ _ => Val.longofint
-  | PLd_rd_a (Pldrh X) _ _ => Val.longofintu
-  | PLd_rd_a (Pldrsh X) _ _ => Val.longofint
-  | PLd_rd_a Pldrzw _ _ => Val.longofintu
-  | PLd_rd_a Pldrsw _ _ => Val.longofint
+  | Pldrb X => Val.longofintu
+  | Pldrsb X => Val.longofint
+  | Pldrh X => Val.longofintu
+  | Pldrsh X => Val.longofint
+  | Pldrzw => Val.longofintu
+  | Pldrsw => Val.longofint
   (* Changed to exhaustive list because I tend to forgot all the places I need
    * to check when changing things. *)
-  | PLd_rd_a (Pldrb W) _ _ | PLd_rd_a (Pldrsb W) _ _ | PLd_rd_a (Pldrh W) _ _ | PLd_rd_a (Pldrsh W) _ _ 
-  | PLd_rd_a Pldrw _ _   | PLd_rd_a Pldrw_a _ _ | PLd_rd_a Pldrx _ _
-  | PLd_rd_a Pldrx_a _ _ | PLd_rd_a Pldrs _ _   | PLd_rd_a Pldrd _ _
-  | PLd_rd_a Pldrd_a _ _
-  | Pldp _ _ _ _ => fun v => v
+  | Pldrb W | Pldrsb W | Pldrh W | Pldrsh W 
+  | Pldrw   | Pldrw_a | Pldrx 
+  | Pldrx_a | Pldrs   | Pldrd 
+  | Pldrd_a => fun v => v
   end.
 
 Definition exec_load (ldi: ld_instruction) (rs: regset) (m: mem) :=
   match ldi with
-  | PLd_rd_a ld rd a => exec_load_rd_a (chunk_load ldi) (interp_load ldi) a rd rs m
-  | Pldp ld rd1 rd2 a => exec_load_double (chunk_load ldi) (interp_load ldi) a rd1 rd2 rs m
+  | PLd_rd_a ld rd a => exec_load_rd_a (chunk_load ld) (interp_load ld) a rd rs m
+  | Pldp ld rd1 rd2 chk1 chk2 a => exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
   end.
 
 Definition exec_store (sti: st_instruction) (rs: regset) (m: mem) :=
   match sti with
-  | PSt_rs_a st rsr a => exec_store_rs_a (chunk_store sti) a rs#rsr rs m
-  | Pstp st rs1 rs2 a => exec_store_double (chunk_store sti) a rs#rs1 rs#rs2 rs m
+  | PSt_rs_a st rsr a => exec_store_rs_a (chunk_store st) a rs#rsr rs m
+  | Pstp st rs1 rs2 chk1 chk2 a => exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
   end.
 
 (** TODO: redundant w.r.t Machblock ?? *)