From 271f87ba08f42340900378c0797511d4071fc1b8 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 31 May 2021 16:55:18 +0200 Subject: BTL Scheduler oracle and some drafts --- scheduling/BTL_Livecheck.v | 47 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 45 insertions(+), 2 deletions(-) (limited to 'scheduling/BTL_Livecheck.v') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 2baba025..6064e4cd 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -4,8 +4,51 @@ Require Import Errors RTL BTL BTLmatchRTL. (** TODO: adapt stuff RTLpathLivegen *) -Definition liveness_checker (f: BTL.function): res unit := OK tt. (* TODO: implement this ! *) - +Local Open Scope lazy_bool_scope. + +Local Open Scope option_monad_scope. + +Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool := + match rl with + | nil => true + | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive + end. + +(* +Fixpoint iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option Regset.t := + 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 + | Bop _ args dest _ => + ASSERT list_mem args alive IN + iblock_checker btl (Regset.add dest alive) + | Bload _ _ _ args dest _ => + ASSERT list_mem args alive IN + iblock_checker btl (Regset.add dest alive) + | 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 _ => + 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 + 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") + 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 *) -- cgit