Some tests and load/store instr

1 files changed, 145 insertions, 26 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index c7170edc..8e095553 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -235,16 +235,6 @@ Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode :=
 
 (* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *)
 
-(** Translation of addressing modes *)
-
-(*Definition offset_representable (sz: Z) (ofs: int64) : bool :=*)
-  (*let isz := Int64.repr sz in*)
-  (*[>* either unscaled 9-bit signed <]*)
-  (*Int64.eq ofs (Int64.sign_ext 9 ofs) ||*)
-  (*[>* or scaled 12-bit unsigned <]*)
-  (*(Int64.eq (Int64.modu ofs isz) Int64.zero*)
-   (*&& Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).*)
-
 Definition indexed_memory_access (insn: addressing -> basic)
                                  (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks :=
   let ofs := Ptrofs.to_int64 ofs in
@@ -255,6 +245,30 @@ Definition indexed_memory_access_bc (insn: addressing -> basic)
   let ofs := Ptrofs.to_int64 ofs in
   insn (ADimm base ofs) :: k.
 
+Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
+  match ty, preg_of dst with
+  | Tint,    IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k)
+  | Tlong,   IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k)
+  | Tsingle, FR' rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k)
+  | Tfloat,  FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k)
+  | Tany32,  IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k)
+  | Tany64,  IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k)
+  | Tany64,  FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k)
+  | _, _           => Error (msg "Asmgen.loadind")
+  end.
+
+Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode) :=
+  match ty, preg_of src with
+  | Tint,    IR' rd => OK (indexed_memory_access_bc (PStore Pstrw rd) 4 base ofs k)
+  | Tlong,   IR' rd => OK (indexed_memory_access_bc (PStore Pstrx rd) 8 base ofs k)
+  | Tsingle, FR' rd => OK (indexed_memory_access_bc (PStore Pstrs rd) 4 base ofs k)
+  | Tfloat,  FR' rd => OK (indexed_memory_access_bc (PStore Pstrd rd) 8 base ofs k)
+  | Tany32,  IR' rd => OK (indexed_memory_access_bc (PStore Pstrw_a rd) 4 base ofs k)
+  | Tany64,  IR' rd => OK (indexed_memory_access_bc (PStore Pstrx_a rd) 8 base ofs k)
+  | Tany64,  FR' rd => OK (indexed_memory_access_bc (PStore Pstrd_a rd) 8 base ofs k)
+  | _, _           => Error (msg "Asmgen.storeind")
+  end.
+
 Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks :=
   indexed_memory_access (PLoad Pldrx dst) 8 base ofs k.
 
@@ -594,6 +608,12 @@ Definition transl_cond_branch
 Definition transl_op
               (op: operation) (args: list mreg) (res: mreg) (k: bcode) :=
   match op, args with
+  | Omove, a1 :: nil =>
+      match preg_of res, preg_of a1 with
+      | IR' r, IR' a => OK (Pmov r a ::bi k)
+      | FR' r, FR' a => OK (Pfmov r a ::bi k)
+      |  _  ,  _   => Error(msg "Asmgenblock.Omove")
+      end
   | Ointconst n, nil =>
       do rd <- ireg_of res;
       OK (loadimm32 rd n k)
@@ -990,18 +1010,123 @@ Definition transl_op
   | _, _ => Error(msg "Asmgenblock.transl_op")
   end.
 
+(** Translation of addressing modes *)
+
+Definition offset_representable (sz: Z) (ofs: int64) : bool :=
+  let isz := Int64.repr sz in
+  (** either unscaled 9-bit signed *)
+  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
+  (** or scaled 12-bit unsigned *)
+  (Int64.eq (Int64.modu ofs isz) Int64.zero
+   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
+ 
+Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
+                             (insn: Asm.addressing -> basic) (k: bcode) : res bcode :=
+  match addr, args with
+  | Aindexed ofs, a1 :: nil =>
+      do r1 <- ireg_of a1;
+       if offset_representable sz ofs then
+        OK (insn (ADimm r1 ofs) ::bi k)
+      else
+        OK (loadimm64 X16 ofs (insn (ADreg r1 X16) ::bi k))
+  | Aindexed2, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (insn (ADreg r1 r2) ::bi k)
+  | Aindexed2shift a, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Int.eq a Int.zero then
+        OK (insn (ADreg r1 r2) ::bi k)
+      else if Int.eq (Int.shl Int.one a) (Int.repr sz) then
+        OK (insn (ADlsl r1 r2 a) ::bi k)
+      else
+        OK (Padd X (SOlsl a) X16 r1 r2 ::bi insn (ADimm X16 Int64.zero) ::bi k)
+  | Aindexed2ext x a, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then
+        OK (insn (match x with Xsgn32 => ADsxt r1 r2 a
+                             | Xuns32 => ADuxt r1 r2 a end) ::bi k)
+      else
+        OK (arith_extended Paddext (Padd X) X16 r1 r2 x a
+                           (insn (ADimm X16 Int64.zero) ::bi k))
+  | Aglobal id ofs, nil =>
+      assertion (negb (Archi.pic_code tt));
+      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
+      then OK (Padrp id ofs X16 ::bi insn (ADadr X16 id ofs) ::bi k)
+      else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) ::bi k))
+  | Ainstack ofs, nil =>
+      let ofs := Ptrofs.to_int64 ofs in
+      if offset_representable sz ofs then
+        OK (insn (ADimm XSP ofs) ::bi k)
+      else
+        OK (loadimm64 X16 ofs (insn (ADreg XSP X16) ::bi k))
+  | _, _ =>
+      Error(msg "Asmgen.transl_addressing")
+  end.
+
+(** Translation of loads and stores *)
+
+Definition transl_load (chunk: memory_chunk) (addr: Op.addressing)
+                       (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+  match chunk with
+  | Mint8unsigned =>
+      do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrb W) rd) k
+  | Mint8signed =>
+      do rd <- ireg_of dst; transl_addressing 1 addr args (PLoad (Pldrsb W) rd) k
+  | Mint16unsigned =>
+      do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrh W) rd) k
+  | Mint16signed =>
+      do rd <- ireg_of dst; transl_addressing 2 addr args (PLoad (Pldrsh W) rd) k
+  | Mint32 =>
+      do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw rd) k
+  | Mint64 =>
+      do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx rd) k
+  | Mfloat32 =>
+      do rd <- freg_of dst; transl_addressing 4 addr args (PLoad Pldrs rd) k
+  | Mfloat64 =>
+      do rd <- freg_of dst; transl_addressing 8 addr args (PLoad Pldrd rd) k
+  | Many32 =>
+      do rd <- ireg_of dst; transl_addressing 4 addr args (PLoad Pldrw_a rd) k
+  | Many64 =>
+      do rd <- ireg_of dst; transl_addressing 8 addr args (PLoad Pldrx_a rd) k
+  end.
+
+Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
+                        (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
+  match chunk with
+  | Mint8unsigned | Mint8signed =>
+      do r1 <- ireg_of src; transl_addressing 1 addr args (PStore Pstrb r1) k
+  | Mint16unsigned | Mint16signed =>
+      do r1 <- ireg_of src; transl_addressing 2 addr args (PStore Pstrh r1) k
+  | Mint32 =>
+      do r1 <- ireg_of src; transl_addressing 4 addr args (PStore Pstrw r1) k
+  | Mint64 =>
+      do r1 <- ireg_of src; transl_addressing 8 addr args (PStore Pstrx r1) k
+  | Mfloat32 =>
+      do r1 <- freg_of src; transl_addressing 4 addr args (PStore Pstrs r1) k
+  | Mfloat64 =>
+      do r1 <- freg_of src; transl_addressing 8 addr args (PStore Pstrd r1) k
+  | Many32 =>
+      do r1 <- ireg_of src; transl_addressing 4 addr args (PStore Pstrw_a r1) k
+  | Many64 =>
+      do r1 <- ireg_of src; transl_addressing 8 addr args (PStore Pstrx_a r1) k
+  end.
+
 (** Translation of a Machblock instruction. *)
 
 Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                               (ep: bool) (k: bcode) :=
   match i with
+  | MBgetstack ofs ty dst =>
+      loadind XSP ofs ty dst k
+  | MBsetstack src ofs ty =>
+      storeind src XSP ofs ty k
   | MBop op args res =>
       transl_op op args res k
+  | MBload _ chunk addr args dst =>
+      transl_load chunk addr args dst k
+  (*| MBstore chunk addr args src =>*)
+      (*transl_store chunk addr args src k*)
   | _ => Error(msg "Not implemented yet")
-  (*| MBgetstack ofs ty dst =>*)
-      (*loadind SP ofs ty dst k*)
-  (*| MBsetstack src ofs ty =>*)
-      (*storeind src SP ofs ty k*)
   (*| MBgetparam ofs ty dst =>*)
       (*[> load via the frame pointer if it is valid <]*)
       (*do c <- loadind FP ofs ty dst k;*)
@@ -1009,10 +1134,6 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                 (*else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c)*)
   (*| MBop op args res =>*)
       (*transl_op op args res k*)
-  (*| MBload trap chunk addr args dst =>*)
-      (*transl_load trap chunk addr args dst k*)
-  (*| MBstore chunk addr args src =>*)
-      (*transl_store chunk addr args src k*)
   end.
 
 (** Translation of a code sequence *)
@@ -1030,15 +1151,17 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
 
 Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
   match i with
+  | MBgetstack ofs ty dst => before && negb (mreg_eq dst R29)
   (*| Msetstack src ofs ty => before*)
   (*| Mgetparam ofs ty dst => negb (mreg_eq dst R29)*)
   | MBop op args res => before && negb (mreg_eq res R29)
+  | MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst R29)
   | _ => false
   end.
 
 Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):=
   match il with
-  | nil => OK nil
+  | nil => OK (k)
   | i1 :: il' =>
       do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k;
       transl_instr_basic f i1 it1p k1
@@ -1083,18 +1206,14 @@ Qed.
 
 Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) :=
   match ctl with
-  | MBcall sig (inl r) => Error (msg "NYI MBcall sig (inl r)")
-  | MBcall sig (inr symb) => Error (msg "NYI MBcall sig (inr symb)")
+  | MBcall sig (inl r) => do r1 <- ireg_of r; OK (nil, PCtlFlow (Pblr r1 sig))
+  | MBcall sig (inr symb) => OK (nil, PCtlFlow (Pbl symb sig))
   | MBtailcall sig (inr symb) => Error (msg "NYI MBtailcall sig (inr symb)")
   | MBtailcall sig (inl r) => Error (msg "NYI MBtailcall sig (inl r)")
   | MBbuiltin ef args res => Error (msg "NYI MBbuiltin ef args res")
   | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl))
   | MBcond cond args lbl => transl_cond_branch cond args lbl nil
   | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA))
-      (*match make_epilogue f (Pret RA ::c nil) with*)
-      (*| nil => OK(nil,None)*)
-      (*| b :: k  => OK(body b,exit b)*)
-      (*end*)
   | MBjumptable arg tbl => Error (msg "NYI MBjumptable arg tbl")
   end.
 
@@ -1108,7 +1227,7 @@ Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool
   let stub := false in (* TODO: FIXME *) 
   do (bdy, ex) <- transl_exit f fb.(Machblock.exit) stub;
   do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
-  OK (cons_bblocks fb.(Machblock.header) (bdy' ++ bdy) ex k) 
+  OK (cons_bblocks fb.(Machblock.header) bdy' ex k) 
   .
 
 Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=