Grouping common RTL functions, printer improvement

1 files changed, 6 insertions, 62 deletions

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 9a61f55e..e14e0ab3 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -3,62 +3,9 @@ open RTL
 open BTL
 open Registers
 open DebugPrint
-open PrintRTL
 open PrintBTL
 open Camlcoq
-
-(* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
-        This should be accessible everywhere. *)
-let get_some = function
-  | None -> failwith "Got None instead of Some _"
-  | Some thing -> thing
-
-let successors_inst = function
-  | Inop n
-  | Iop (_, _, _, n)
-  | Iload (_, _, _, _, _, n)
-  | Istore (_, _, _, _, n)
-  | Icall (_, _, _, _, n)
-  | Ibuiltin (_, _, _, n) ->
-      [ n ]
-  | Icond (_, _, n1, n2, _) -> [ n1; n2 ]
-  | Ijumptable (_, l) -> l
-  | Itailcall _ | Ireturn _ -> []
-
-let predicted_successor = function
-  | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n)
-    ->
-      Some n
-  | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None
-  | Icond (_, _, n1, n2, p) -> (
-      match p with Some true -> Some n1 | Some false -> Some n2 | None -> None)
-  | Ijumptable _ | Itailcall _ | Ireturn _ -> None
-
-(* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *)
-let non_predicted_successors i = function
-  | None -> successors_inst i
-  | Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
-
-(* adapted from Linearizeaux.get_join_points *)
-let get_join_points code entry =
-  let reached = ref (PTree.map (fun n i -> false) code) in
-  let reached_twice = ref (PTree.map (fun n i -> false) code) in
-  let rec traverse pc =
-    if get_some @@ PTree.get pc !reached then (
-      if not (get_some @@ PTree.get pc !reached_twice) then
-        reached_twice := PTree.set pc true !reached_twice)
-    else (
-      reached := PTree.set pc true !reached;
-      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code))
-  and traverse_succs = function
-    | [] -> ()
-    | [ pc ] -> traverse pc
-    | pc :: l ->
-        traverse pc;
-        traverse_succs l
-  in
-  traverse entry;
-  !reached_twice
+open AuxTools
 
 let encaps_final inst osucc =
   match inst with
@@ -94,7 +41,7 @@ let translate_inst inst is_final =
 let translate_function code entry join_points =
   let reached = ref (PTree.map (fun n i -> false) code) in
   let btl_code = ref PTree.empty in
-  (* SEPARATE IN A BETTER WAY!! *)
+  (* TODO gourdinl SEPARATE IN A BETTER WAY!! *)
   let rec build_btl_tree e =
     if get_some @@ PTree.get e !reached then ()
     else (
@@ -102,9 +49,6 @@ let translate_function code entry join_points =
       let next_nodes = ref [] in
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
-        debug "Inst is : ";
-        print_instruction stderr (0, inst);
-        debug "\n";
         let psucc = predicted_successor inst in
         let succ =
           match psucc with
@@ -148,7 +92,7 @@ let print_dm dm =
   (PTree.elements dm)
 
 let rtl2btl (f : RTL.coq_function) =
-  (*debug_flag := true;*)
+  debug_flag := true;
   let code = f.fn_code in
   let entry = f.fn_entrypoint in
   let join_points = get_join_points code entry in
@@ -157,12 +101,12 @@ let rtl2btl (f : RTL.coq_function) =
   debug "Entry %d\n" (P.to_int entry);
   debug "RTL Code: ";
   print_code code;
+  debug_flag := false;
   debug "BTL Code: ";
   print_btl_code stderr btl true;
-  debug "BTL Dupmap:\n";
-  print_dm dm;
+  debug "Dupmap:\n";
+  print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  debug_flag := false;
   ((btl, entry), dm)