From 02a86fb0cd2dcb63b8346c48ca78056b30c7fef6 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 26 Nov 2020 09:12:52 +0100 Subject: This commit fix the issue #226 - adding two functions to manage special bblock case - adding movz size specifications --- aarch64/Asmblockgen.v | 107 +++++++++++++++++++++++++++----------------------- 1 file changed, 57 insertions(+), 50 deletions(-) (limited to 'aarch64/Asmblockgen.v') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 0a21485c..268cd7fc 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -139,6 +139,8 @@ Definition is_arith_imm64 (x: int64) : bool := Int64.eq x (Int64.zero_ext 12 x) || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)). +Definition bcode := list basic. + Program Definition single_basic (bi: basic): bblock := {| header := nil; body:= bi::nil; exit := None |}. @@ -155,12 +157,6 @@ Program Definition insert_basic (bi: basic) (k:bblocks): bblocks := Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity). -(* insert [ctl] at the head of [k] *) -Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks := - {| header := nil; body := nil; exit := Some ctl |}::k. - -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. @@ -173,11 +169,45 @@ Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass. Coercion PArithComparisonR0R: arith_comparison_r0r >-> 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 *) +Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity). + +(* The pop_bc and push_bc functions are used to adapt the output of some definitions + in bblocks format and avoid some redefinitions. *) + +(* pop_bc takes the body of the first bblock in the list if it does not have a header. *) +Definition pop_bc (k: bblocks): bcode := + match k with + | bb :: k' => match bb.(header) with + | nil => (body bb) + | _ => nil + end + | _ => nil + end. + +(* push_bc tries to overwrite code in the first bblock if it does not have a header, + otherwise, a new bblock is created and appended to the list. *) +Program Definition push_bc (bc: bcode) (k:bblocks): bblocks := + match bc with + | bi :: bc' => match k with + | bb :: k' => match bb.(header) with + | nil => {| header := nil; body := bc; exit := exit bb |} :: k' + | _ => {| header := nil; body := bc; exit := None |} :: k + end + | _ => {| header := nil; body := bc; exit := None |} :: nil + end + | nil => k + end. +Next Obligation. + simpl; auto. +Qed. +Next Obligation. + simpl; auto. +Qed. +Next Obligation. + simpl; auto. +Qed. Parameter symbol_is_aligned : ident -> Z -> bool. (** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) @@ -233,17 +263,20 @@ 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) *) - -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 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_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. + if offset_representable sz ofs + then insn (ADimm base ofs) :: k + else loadimm64 X16 ofs (insn (ADreg base X16) :: k). Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with @@ -269,32 +302,17 @@ Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode | _, _ => 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. - 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.*) +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). + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs)::nil). (** Add immediate *) @@ -1022,14 +1040,6 @@ Definition 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 := @@ -1222,7 +1232,7 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) : end. Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) := - let stub := false in (* TODO: FIXME *) + let stub := false in do (bdy, ex) <- transl_exit f fb.(Machblock.exit); do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy; OK (cons_bblocks fb.(Machblock.header) bdy' ex k) @@ -1232,18 +1242,15 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): match lmb with | nil => OK nil | mb :: lmb => - do lb <- transl_blocks f lmb false; (* TODO: check [false] here *) - transl_block f mb (if Machblock.header mb then ep else false) lb (* TODO: check this *) + do lb <- transl_blocks f lmb false; + transl_block f mb (if Machblock.header mb then ep else false) lb end. - (* OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *)*) + (* OK (make_epilogue f ((Pret X0)::c nil))*) (* 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. + push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k. Definition transl_function (f: Machblock.function) : res Asmblock.function := do lb <- transl_blocks f f.(Machblock.fn_code) true; -- cgit