a first working draft on ldp/stp peephole

1 files changed, 66 insertions, 43 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 329c889e..3ad1d7f8 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -130,14 +130,16 @@ Inductive store_rs_a : Type :=
   | Pstrd                                   (**r store float64 *)
   | Pstrd_a                                 (**r store float64 as any64 *)
   .
-(* Actually, Pstp is not used in the aarch64/Asm semantics!
- * Thus we skip this particular case:
- *   Inductive st_instruction : Type :=
- *     | PSt_rs_a (st : store_rs_a) (rs : ireg) (a : addressing)
- *     | Pstp (rs1 rs2: ireg) (a: addressing)  (**r store two int64 *)
- *     .
- *   Coercion PStore : st_instruction >-> basic.
- *)
+
+Inductive store_rs1_rs2_a : Type :=
+  | Pstpw
+  | Pstpx
+  .
+
+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 *)
+  .
 
 Inductive arith_p : Type :=
   (** PC-relative addressing *)
@@ -318,23 +320,23 @@ Inductive ar_instruction : Type :=
 
 Inductive basic : Type :=
   | PArith (i: ar_instruction)                                        (**r TODO *)
-  (*| PLoad (ld: load_rd_a) (rd: dreg) (a: addressing)                  [>*r TODO <]*)
   | PLoad (ld: ld_instruction)
-  | PStore (st: store_rs_a) (r: dreg) (a: addressing)                 (**r TODO *)
+  | PStore (st: st_instruction)
   | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
   | Pfreeframe (sz: Z) (linkofs: ptrofs)                              (**r deallocate stack frame and restore previous frame *)
   | Ploadsymbol (rd: ireg) (id: ident)                                (**r load the address of [id] *)
   | Pcvtsw2x (rd: ireg) (r1: ireg)                                    (**r sign-extend 32-bit int to 64-bit *)
   | Pcvtuw2x (rd: ireg) (r1: ireg)                                    (**r zero-extend 32-bit int to 64-bit *)
   | Pcvtx2w (rd: ireg)                                                (**r retype a 64-bit int as a 32-bit int *)
-(* NOT USED IN THE SEMANTICS !
   | Pnop                                                              (**r no operation *)
+(* NOT USED IN THE SEMANTICS !
   | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
   | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
 *)
 .
 
 Coercion PLoad: ld_instruction >-> basic.
+Coercion PStore : st_instruction >-> basic.
 
 (* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml
 Inductive instruction : Type :=
@@ -591,13 +593,7 @@ 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 lk id ofs)
-  | ADpostincr base n => rs#base
-  end.
-
-Definition eval_addressing_update (a: addressing) (rs: regset): regset :=
-  match a with
-  | ADpostincr base n => rs#base <- (Vlong n)
-  | _ => rs
+  | ADpostincr base n => Vundef
   end.
 
 (** Auxiliaries for memory accesses *)
@@ -609,24 +605,42 @@ Definition exec_load_rd_a (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.
-
-Definition exec_store (chunk: memory_chunk)
+  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 ((rs#rd1 <- (transf v1))#rd2 <- (transf v2)) m
+            end
+        end
+  else Stuck.
+
+Definition exec_store_rs_a (chunk: memory_chunk)
                       (a: addressing) (v: val)
                       (rs: regset) (m: mem) :=
   SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN
   Next rs m'.
 
+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 rs m''
+                   end
+      end
+  else Stuck.
 
 (** execution of loads
 *)
@@ -647,20 +661,22 @@ Definition chunk_load (ld: ld_instruction): memory_chunk :=
   | PLd_rd_a Pldrd _ _ => Mfloat64
   | PLd_rd_a Pldrd_a _ _ =>  Many64
   | Pldp Pldpw _ _ _ => Mint32
-  | Pldp Pldpx _ _ _ => Mint32
+  | Pldp Pldpx _ _ _ => Mint64
   end.
 
-Definition chunk_store_rs_a (st: store_rs_a) : memory_chunk :=
+Definition chunk_store (st: st_instruction) : memory_chunk :=
   match st with
-  | Pstrw   => Mint32
-  | Pstrw_a => Many32
-  | Pstrx   => Mint64
-  | Pstrx_a => Many64
-  | Pstrb   => Mint8unsigned
-  | Pstrh   => Mint16unsigned
-  | Pstrs   => Mfloat32
-  | Pstrd   => Mfloat64
-  | Pstrd_a => Many64
+  | 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
   end.
 
 Definition interp_load (ld: ld_instruction): val -> val :=
@@ -686,6 +702,12 @@ Definition exec_load (ldi: ld_instruction) (rs: regset) (m: mem) :=
   | Pldp ld rd1 rd2 a => exec_load_double (chunk_load ldi) (interp_load ldi) 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
+  end.
+
 (** TODO: redundant w.r.t Machblock ?? *)
 Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
 Proof.
@@ -1022,7 +1044,7 @@ Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
   match b with
   | PArith ai => Next (exec_arith_instr ai rs) m
   | PLoad ldi => exec_load ldi rs m
-  | PStore st r a => exec_store (chunk_store_rs_a st) a rs#r rs m
+  | PStore sti => exec_store sti rs m
   | Pallocframe sz pos =>
       let (m1, stk) := Mem.alloc m 0 sz in
       let sp := (Vptr stk Ptrofs.zero) in
@@ -1044,6 +1066,7 @@ Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
       Next (rs#rd <- (Val.longofintu rs#r1)) m
   | Pcvtx2w rd =>
       Next (rs#rd <- (Val.loword rs#rd)) m
+  | Pnop => Next rs m
   end.
 
 (* TODO: ORIGINAL EXECUTION OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !