Dupmap bugfix and some advance in Livegen

1 files changed, 78 insertions, 21 deletions

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