From 78fbb0e6f4c2065460a0ddb7e2e3ec94da21169f Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 31 May 2021 23:51:31 +0200 Subject: Dupmap bugfix and some advance in Livegen --- driver/Compiler.vexpand | 2 + scheduling/BTLRenumber.ml | 7 ++-- scheduling/BTL_Livecheck.v | 99 ++++++++++++++++++++++++++++++++++++---------- scheduling/BTLtoRTLaux.ml | 10 +++-- scheduling/RTLtoBTLaux.ml | 2 +- tools/compiler_expand.ml | 2 +- 6 files changed, 92 insertions(+), 30 deletions(-) diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 40ea0d68..1d218657 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -299,6 +299,8 @@ EXPAND_ASM_SEMANTICS EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. eapply RTLtoBTLproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply BTL_Schedulerproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply BTLtoRTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/scheduling/BTLRenumber.ml b/scheduling/BTLRenumber.ml index 58d4f7ac..6ff42a27 100644 --- a/scheduling/BTLRenumber.ml +++ b/scheduling/BTLRenumber.ml @@ -87,6 +87,7 @@ let regenerate_btl_tree btl entry = | Bseq (ib1, ib2) -> Bseq (renumber_iblock ib1, renumber_iblock ib2) | _ -> ib in + let dm = ref PTree.empty in let ord_btl = PTree.fold (fun ord_btl old_n old_ibf -> @@ -96,16 +97,16 @@ let regenerate_btl_tree btl entry = let bi = mk_binfo n in let ibf = { entry = ib; input_regs = old_ibf.input_regs; binfo = bi } in if old_n = entry then new_entry := n_pos; + dm := PTree.set old_n n_pos !dm; PTree.set n_pos ibf ord_btl) btl PTree.empty in debug "Renumbered BTL with new_entry=%d:\n" (p2i !new_entry); print_btl_code stderr ord_btl; - (ord_btl, !new_entry) + ((ord_btl, !new_entry), !dm) let renumber btl entry = (*debug_flag := true;*) let btl' = recompute_inumbs btl entry in - let ord_btl, new_entry = regenerate_btl_tree btl' entry in (*debug_flag := false;*) - (ord_btl, new_entry) + regenerate_btl_tree btl' entry diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 6064e4cd..4d556711 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -14,41 +14,98 @@ Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool := | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive end. -(* -Fixpoint iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option Regset.t := +Definition reg_option_mem (or: option reg) (alive: Regset.t) := + match or with None => true | Some r => Regset.mem r alive end. + +Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) := + match ros with inl r => Regset.mem r alive | inr s => true end. + +(* NB: definition following [regmap_setres] in [RTL.step] semantics *) +Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t := + match res with + | BR r => Regset.add r alive + | _ => alive + end. + +Definition exit_checker {A} (btl: code) (alive: Regset.t) (s: node) (v: A): option A := + SOME next <- btl!s IN + ASSERT Regset.subset next.(input_regs) alive IN + Some v. + +Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool := + match l with + | nil => true + | s :: l' => exit_checker btl alive s true &&& exit_list_checker btl alive l' + end. + +Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit := + match fin with + | Bgoto s => + exit_checker btl alive s tt + | Breturn oreg => + ASSERT reg_option_mem oreg alive IN Some tt + | Bcall _ ros args res s => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN + exit_checker btl (Regset.add res alive) s tt + | Btailcall _ ros args => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN Some tt + | Bbuiltin _ args res s => + ASSERT list_mem (params_of_builtin_args args) alive IN + exit_checker btl (reg_builtin_res res alive) s tt + | Bjumptable arg tbl => + ASSERT Regset.mem arg alive IN + ASSERT exit_list_checker btl alive tbl IN Some tt + end. + +Definition is_none {A} (oa: option A): bool := + match oa with + | Some _ => false + | None => true + end. + +Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (Regset.t*option final) := match ib with | Bseq ib1 ib2 => - SOME alive' <- iblock_checker btl ib1 alive IN - iblock_checker btl ib1 alive' (Some ib2) - | Bnop _ => - iblock_checker btl alive + SOME res <- body_checker btl ib1 alive IN + ASSERT is_none (snd res) IN + body_checker btl ib2 (fst res) + | Bnop _ => Some (alive, None) | Bop _ args dest _ => ASSERT list_mem args alive IN - iblock_checker btl (Regset.add dest alive) + Some (Regset.add dest alive, None) | Bload _ _ _ args dest _ => ASSERT list_mem args alive IN - iblock_checker btl (Regset.add dest alive) + Some (Regset.add dest alive, None) | Bstore _ _ args src _ => ASSERT Regset.mem src alive IN ASSERT list_mem args alive IN - iblock_checker btl alive - | Bcond _ args (BF (Bgoto s) _) ib2 _ => + Some (alive, None) + | Bcond _ args (BF (Bgoto s) _) (Bnop None) _ => ASSERT list_mem args alive IN - SOME _ <- iblock_checker btl ib2 alive None IN - SOME next <- btl!s IN - ASSERT Regset.subset next.(input_regs) alive IN - iblock_checker btl next.(entry) next.(input_regs) None - | Bcond _ _ _ _ _ => None - | BF _ _ => Some tt + exit_checker btl alive s (alive, None) + | BF fin _ => Some (alive, Some fin) + | _ => None + end. + +Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option unit := + SOME res <- body_checker btl ib alive IN + SOME fin <- snd res IN + final_inst_checker btl (fst res) fin. + +Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool := + match l with + | nil => true + | (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl l' end. Definition liveness_checker (f: BTL.function): res unit := - match f.(fn_code)!(f.(fn_entrypoint)) with - | Some ibf => iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) - | None => Error (msg "liveness_checker: empty function") + match list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) with + | true => OK tt + | false => Error (msg "BTL_Livecheck: liveness_checker failed") end. - *) -Definition liveness_checker (f: BTL.function): res unit := OK tt. + Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. (** TODO: adapt stuff RTLpathLivegenproof *) diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml index 8e728bd2..ddec991d 100644 --- a/scheduling/BTLtoRTLaux.ml +++ b/scheduling/BTLtoRTLaux.ml @@ -73,14 +73,16 @@ let btl2rtl (f : BTL.coq_function) = (*debug_flag := true;*) let btl = f.fn_code in let entry = f.fn_entrypoint in - let ordered_btl, new_entry = renumber btl entry in + let obne, dm = renumber btl entry in + let ordered_btl, new_entry = obne in let rtl = translate_function ordered_btl new_entry in - let dm = PTree.map (fun n i -> n) btl in - debug "Entry %d\n" (p2i entry); + debug "Entry %d\n" (p2i new_entry); + debug "BTL Code:\n"; + print_btl_code stderr ordered_btl; debug "RTL Code: "; print_code rtl; debug "Dupmap:\n"; print_ptree print_pint dm; debug "\n"; (*debug_flag := false;*) - ((rtl, entry), dm) + ((rtl, new_entry), dm) diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index e709d846..3de82d96 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -101,8 +101,8 @@ let rtl2btl (f : RTL.coq_function) = let btl = translate_function code entry join_points liveness in let dm = PTree.map (fun n i -> n) btl in (* TODO gourdinl move elsewhere *) - debug "Entry %d\n" (p2i entry); (*debug_flag := true;*) + debug "Entry %d\n" (p2i entry); debug "RTL Code: "; print_code code; debug "BTL Code:\n"; diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 29403c7e..5c90af6c 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -52,7 +52,7 @@ PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob" let post_rtl_passes = [| PARTIAL, Always, Require, (Some "BTL generation"), "RTLtoBTL", Noprint; - (*TODO gourdinl PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint;*) + PARTIAL, Always, Require, (Some "Prepass scheduling"), "BTL_Scheduler", Noprint; PARTIAL, Always, Require, (Some "Projection to RTL"), "BTLtoRTL", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1"); PARTIAL, Always, Require, (Some "Branch tunneling"), "Tunneling", (Print "LTL 2"); -- cgit