BTL Scheduler oracle and some drafts

1 files changed, 45 insertions, 2 deletions

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 *)