Adding semantics for Pldp

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

1 files changed, 67 insertions, 37 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 6ea592dd..329c889e 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -107,19 +107,16 @@ Inductive load_rd_a: Type :=
   | Pldrd_a                                 (**r load float64 as any64 *)
   .
 
-(* Actually, Pldp is not used in the aarch64/Asm semantics!
-
-Thus we skip this particular case:
+Inductive load_rd1_rd2_a: Type :=
+  | Pldpw
+  | Pldpx
+  .
 
 Inductive ld_instruction: Type :=
-  | PLd_rd_a (ld: load_rd_a) (rd: ireg) (a: addressing)
-  | Pldp (rd1 rd2: ireg) (a: addressing)   (**r load two int64 *)
+  | 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 *)
   .
 
-Coercion PLoad: ld_instruction >-> basic.
-
-*)
-
 Inductive store_rs_a : Type :=
   (* Integer store *)
   | Pstrw                                   (**r store int32 *)
@@ -321,7 +318,8 @@ 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: load_rd_a) (rd: dreg) (a: addressing)                  [>*r TODO <]*)
+  | PLoad (ld: ld_instruction)
   | PStore (st: store_rs_a) (r: dreg) (a: addressing)                 (**r TODO *)
   | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
   | Pfreeframe (sz: Z) (linkofs: ptrofs)                              (**r deallocate stack frame and restore previous frame *)
@@ -336,6 +334,8 @@ Inductive basic : Type :=
 *)
 .
 
+Coercion PLoad: ld_instruction >-> basic.
+
 (* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml
 Inductive instruction : Type :=
   | PBasic    (i: basic)
@@ -591,16 +591,36 @@ 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 => Vundef (* not modeled yet *)
+  | 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
   end.
 
 (** Auxiliaries for memory accesses *)
 
-Definition exec_load (chunk: memory_chunk) (transf: val -> val)
+Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val)
                      (a: addressing) (r: dreg) (rs: regset) (m: mem) :=
   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)
+                     (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)
                       (a: addressing) (v: val)
                       (rs: regset) (m: mem) :=
@@ -611,21 +631,23 @@ Definition exec_store (chunk: memory_chunk)
 (** execution of loads
 *)
 
-Definition chunk_load_rd_a (ld: load_rd_a): memory_chunk :=
+Definition chunk_load (ld: ld_instruction): memory_chunk :=
   match ld with
-  | 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
+  | 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 _ _ _ => Mint32
   end.
 
 Definition chunk_store_rs_a (st: store_rs_a) : memory_chunk :=
@@ -641,19 +663,27 @@ Definition chunk_store_rs_a (st: store_rs_a) : memory_chunk :=
   | Pstrd_a => Many64
   end.
 
-Definition interp_load_rd_a (ld: load_rd_a): val -> val :=
+Definition interp_load (ld: ld_instruction): val -> val :=
   match ld with
-  | Pldrb X => Val.longofintu
-  | Pldrsb X => Val.longofint
-  | Pldrh X => Val.longofintu
-  | Pldrsh X => Val.longofint
-  | Pldrzw => Val.longofintu
-  | Pldrsw => Val.longofint
+  | 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
   (* Changed to exhaustive list because I tend to forgot all the places I need
    * to check when changing things. *)
-  | Pldrb W | Pldrsb W | Pldrh W | Pldrsh W
-  | Pldrw   | Pldrw_a  | Pldrx   | Pldrx_a
-  | Pldrs   | Pldrd    | Pldrd_a => fun v => v
+  | 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
+  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
   end.
 
 (** TODO: redundant w.r.t Machblock ?? *)
@@ -991,7 +1021,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
 Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
   match b with
   | PArith ai => Next (exec_arith_instr ai rs) m
-  | PLoad ld rd a => exec_load (chunk_load_rd_a ld) (interp_load_rd_a ld) a rd 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
   | Pallocframe sz pos =>
       let (m1, stk) := Mem.alloc m 0 sz in