From b3d0a01117d5a5e1fac748387fa517617b88c645 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 27 Oct 2020 20:11:28 +0100 Subject: Epilogue OK and loadimm --- aarch64/Asmblockgen.v | 154 +++++++++++++++++++++++++++++++------------------- 1 file changed, 96 insertions(+), 58 deletions(-) (limited to 'aarch64/Asmblockgen.v') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 2bab1927..aa6df96f 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -25,8 +25,6 @@ Local Open Scope string_scope. Local Open Scope list_scope. Local Open Scope error_monad_scope. -Import PArithCoercions. - (** Extracting integer or float registers. *) Definition ireg_of (r: mreg) : res ireg := @@ -153,37 +151,23 @@ Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks := Notation "ctl ::c k" := (insert_ctl ctl k) (at level 49, right associativity). +(* TODO: Coercions to move in Asmblock ? *) +Coercion PArithP: arith_p >-> Funclass. +Coercion PArithPP: arith_pp >-> Funclass. +Coercion PArithRR0: arith_rr0 >-> Funclass. +Coercion PArithRR0R: arith_rr0r >-> Funclass. +Coercion PArith: ar_instruction >-> basic. + +Definition bcode := list basic. +Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity). +(* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *) (** Alignment check for symbols *) Parameter symbol_is_aligned : ident -> Z -> bool. (** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) (***************************************************************************************) -(* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *) - -Definition indexed_memory_access (insn: addressing -> basic) - (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks := - let ofs := Ptrofs.to_int64 ofs in - insn (ADimm base ofs) ::b k. (* STUB: change me ! See Asmgen below *) - - -Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks := - indexed_memory_access (PLoad Pldrx dst) 8 base ofs k. - -Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bblocks): bblocks := - indexed_memory_access (PStore Pstrx src) 8 base ofs k. - -(** Function epilogue *) - -Definition make_epilogue (f: Machblock.function) (k: bblocks) : bblocks := - (* FIXME - Cannot be used because memcpy destroys X30; - issue being discussed with X. Leroy *) - (* if is_leaf_function f - then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k - else*) loadptr XSP f.(fn_retaddr_ofs) RA - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::b k). (** Decompose integer literals into 16-bit fragments *) @@ -201,18 +185,6 @@ Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) := Definition negate_decomposition (l: list (Z * Z)) := List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l. -(* TODO: Coercions to move in Asmblock ? *) -Coercion PArithP: arith_p >-> Funclass. -Coercion PArithPP: arith_pp >-> Funclass. -Coercion PArithRR0: arith_rr0 >-> Funclass. -Coercion PArith: ar_instruction >-> basic. - -Definition bcode := list basic. - -Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity). -(* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *) - - Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode := List.fold_right (fun np k => Pmovk sz (fst np) (snd np) rd rd ::bi k) k l. @@ -246,6 +218,68 @@ Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode := then Porrimm X (Int64.unsigned n) rd XZR ::bi k else loadimm X rd (Int64.unsigned n) k. +(* 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 + insn (ADimm base ofs) ::b k. (* STUB: change me ! See Asmgen below *) + +Definition indexed_memory_access_bc (insn: addressing -> basic) + (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bcode) : bcode := + let ofs := Ptrofs.to_int64 ofs in + insn (ADimm base ofs) :: k. + +Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks := + indexed_memory_access (PLoad Pldrx dst) 8 base ofs k. + +Definition loadptr_bc (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bcode): bcode := + indexed_memory_access_bc (PLoad Pldrx dst) 8 base ofs k. + +Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bblocks): bblocks := + indexed_memory_access (PStore Pstrx src) 8 base ofs k. + +(*Definition storeptr_bc (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bcode): bcode :=*) + (*indexed_memory_access_bc (PStore Pstrx src) 8 base ofs k.*) + +(** Function epilogue *) + +(*Definition make_epilogue (f: Machblock.function) (k: bblocks) : bblocks :=*) + (*(* FIXME*) + (*Cannot be used because memcpy destroys X30;*) + (*issue being discussed with X. Leroy *)*) + (*(* if is_leaf_function f*) + (*then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k*) + (*else*) loadptr XSP f.(fn_retaddr_ofs) RA*) + (*(Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::b k).*) + +Definition make_epilogue (f: Machblock.function) : bcode := + loadptr_bc XSP f.(fn_retaddr_ofs) RA + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs)::nil). + +(** Add immediate *) + +Definition addimm32 (rd r1: ireg) (n: int) (k: bcode) : bcode := + let m := Int.neg n in + if Int.eq n (Int.zero_ext 24 n) then + Paddimm W (Int.unsigned n) rd r1 ::bi k + else if Int.eq m (Int.zero_ext 24 m) then + Psubimm W (Int.unsigned m) rd r1 ::bi k + else if Int.lt n Int.zero then + loadimm32 X16 m (Psub W SOnone rd r1 X16 ::bi k) + else + loadimm32 X16 n (Padd W SOnone rd r1 X16 ::bi k). + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -255,6 +289,9 @@ Definition transl_op | Ointconst n, nil => do rd <- ireg_of res; OK (loadimm32 rd n k) + | Oaddimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (addimm32 rd rs n k) | _, _ => Error(msg "Not implemented yet") end. @@ -304,22 +341,6 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool := | _ => false end. -(** This is an equivalent definition in continuation-passing style - that runs in constant stack space. *) -(* -Fixpoint transl_code_rec (f: Machblock.function) (il: list Machblock.basic_inst) - (it1p: bool) (k: bcode -> res bcode) := - match il with - | nil => k nil - | i1 :: il' => - transl_code_rec f il' (it1_is_parent it1p i1) - (fun c1 => do c2 <- transl_instr_basic f i1 it1p c1; k c2) - end. - -Definition transl_code' (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := - transl_code_rec f il it1p (fun c => OK c). -*) - Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):= match il with | nil => OK nil @@ -365,12 +386,26 @@ Obligation 1. rewrite <- Heq_anonymous. constructor. Qed. -Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) := - Error (msg ("not yet implemented")). +Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*option 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)") + | 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 => Error (msg "NYI MBgoto lbl") + | MBcond cond args lbl => Error (msg "NYI MBcond cond args lbl") + | MBreturn => OK (make_epilogue f, Some (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. Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) (ep: bool) : res (bcode*option control) := match ext with - Some ctl => do (b,c) <- transl_control f ctl ep; OK (b, Some c) + Some ctl => do (b,c) <- transl_control f ctl ep; OK (b, c) | None => OK (nil, None) end. @@ -378,7 +413,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' ex k) + OK (cons_bblocks fb.(Machblock.header) (bdy' ++ bdy) ex k) . Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks := @@ -392,6 +427,9 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): (* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *) Program Definition make_prologue (f: Machblock.function) (k:bblocks) := + (*({| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::*) + (*storeptr_bc RA XSP f.(fn_retaddr_ofs) nil;*) + (*exit := None |} :: k).*) Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b storeptr RA XSP f.(fn_retaddr_ofs) k. -- cgit