From 8de1a1f5811470bc1d7d1a7b2f0e5193de40698e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 29 Oct 2020 14:15:19 +0100 Subject: End of Asmblock translation --- aarch64/Asmblockgen.v | 74 +++++++++++++++++++++++++-------------------------- 1 file changed, 36 insertions(+), 38 deletions(-) (limited to 'aarch64/Asmblockgen.v') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 8e095553..fc356d52 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -298,12 +298,23 @@ Definition make_epilogue (f: Machblock.function) : bcode := (** Add immediate *) +Definition addimm_aux (insn: Z -> arith_pp) + (rd r1: iregsp) (n: Z) (k: bcode) := + let nlo := Zzero_ext 12 n in + let nhi := n - nlo in + if Z.eqb nhi 0 then + insn nlo rd r1 ::bi k + else if Z.eqb nlo 0 then + insn nhi rd r1 ::bi k + else + insn nhi rd r1 ::bi insn nlo rd rd ::bi k. + 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 + addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k else if Int.eq m (Int.zero_ext 24 m) then - Psubimm W (Int.unsigned m) rd r1 ::bi k + addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k else if Int.lt n Int.zero then loadimm32 X16 m (Psub W SOnone rd r1 X16 ::bi k) else @@ -312,9 +323,9 @@ Definition addimm32 (rd r1: ireg) (n: int) (k: bcode) : bcode := Definition addimm64 (rd r1: iregsp) (n: int64) (k: bcode) : bcode := let m := Int64.neg n in if Int64.eq n (Int64.zero_ext 24 n) then - Paddimm X (Int64.unsigned n) rd r1 ::bi k + addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k else if Int64.eq m (Int64.zero_ext 24 m) then - Psubimm X (Int64.unsigned m) rd r1 ::bi k + addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k else if Int64.lt n Int64.zero then loadimm64 X16 m (Psubext (EOuxtx Int.zero) rd r1 X16 ::bi k) else @@ -1120,42 +1131,26 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) loadind XSP ofs ty dst k | MBsetstack src ofs ty => storeind src XSP ofs ty k + | MBgetparam ofs ty dst => + do c <- loadind X29 ofs ty dst k; + OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c) | 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") - (*| MBgetparam ofs ty dst =>*) - (*[> load via the frame pointer if it is valid <]*) - (*do c <- loadind FP ofs ty dst k;*) - (*OK (if ep then c*) - (*else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c)*) - (*| MBop op args res =>*) - (*transl_op op args res k*) + | MBstore chunk addr args src => + transl_store chunk addr args src k end. (** Translation of a code sequence *) -(* TODO to remove ? *) -(*Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=*) - (*match i with*) - (*| MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP)*) - (*| MBsetstack src ofs ty => before*) - (*| MBgetparam ofs ty dst => negb (mreg_eq dst MFP)*) - (*| MBop op args res => before && negb (mreg_eq res MFP)*) - (*| MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst MFP)*) - (*| MBstore chunk addr args res => before*) - (*end.*) - 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)*) + (*| MBgetstack ofs ty dst => before && negb (mreg_eq dst R29)*) + | MBsetstack src ofs ty => before + | MBgetparam 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) + (*| MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst R29)*) | _ => false end. @@ -1204,28 +1199,31 @@ Obligation 1. rewrite <- Heq_anonymous. constructor. Qed. -Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) := +Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) := match ctl with - | MBcall sig (inl r) => do r1 <- ireg_of r; OK (nil, PCtlFlow (Pblr r1 sig)) + | 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") + | MBtailcall sig (inr symb) => OK(make_epilogue f, PCtlFlow (Pbs symb sig)) + | MBtailcall sig (inl r) => do r1 <- ireg_of r; + OK (make_epilogue f, PCtlFlow (Pbr r1 sig)) + | MBbuiltin ef args res => OK (nil, Pbuiltin ef (List.map (map_builtin_arg dreg_of) args) (map_builtin_res dreg_of 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)) - | MBjumptable arg tbl => Error (msg "NYI MBjumptable arg tbl") + | MBjumptable arg tbl => do r <- ireg_of arg; + OK (nil, PCtlFlow (Pbtbl r tbl)) end. -Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) (ep: bool) : res (bcode*option control) := +Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) : 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; OK (b, Some c) | None => OK (nil, None) end. Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) := let stub := false in (* TODO: FIXME *) - do (bdy, ex) <- transl_exit f fb.(Machblock.exit) stub; + 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) . -- cgit