From f57103ff244a72201e12864e998eae791681e68f Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 29 Oct 2020 09:00:42 +0100 Subject: Some tests and load/store instr --- aarch64/Asmblockgen.v | 171 ++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 145 insertions(+), 26 deletions(-) (limited to 'aarch64/Asmblockgen.v') 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 := -- cgit