Dupmap bugfix and some advance in Livegen

4 files changed, 89 insertions, 29 deletions

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";