1 files changed, 4 insertions, 45 deletions

diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index 2a20a15d..c9bb94d3 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -7,31 +7,7 @@ open Datatypes
 open Kildall
 open Lattice
 open DebugPrint
-
-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
-
-let non_predicted_successors i =
-  match predicted_successor i with
-  | None -> successors_inst i
-  | Some n -> List.filter (fun n' -> n != n') (successors_inst i)
+open AuxTools
 
 let rec list_to_regset = function
   | [] -> Regset.empty
@@ -59,24 +35,6 @@ let get_output_reg i =
   | Iop (_, _, r, _) | Iload (_, _, _, _, r, _) | Icall (_, _, _, r, _) -> Some r
   | Ibuiltin (_, _, brr, _) -> (match brr with AST.BR r -> Some r | _ -> None)
 
-(* 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 begin
-      if not (get_some @@ PTree.get pc !reached_twice) then
-        reached_twice := PTree.set pc true !reached_twice
-    end else begin
-      reached := PTree.set pc true !reached;
-      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
-    end
-  and traverse_succs = function
-    | [] -> ()
-    | [pc] -> traverse pc
-    | pc :: l -> traverse pc; traverse_succs l
-  in traverse entry; !reached_twice
-
 (* Does not set the input_regs and liveouts field *)
 let get_path_map code entry join_points =
   let visited = ref (PTree.map (fun n i -> false) code) in
@@ -92,12 +50,13 @@ let get_path_map code entry join_points =
         let inst = get_some @@ PTree.get n code in
         begin
           psize := !psize + 1;
-          let successor = match predicted_successor inst with
+          let psucc = predicted_successor inst in
+          let successor = match psucc with
           | None -> None
           | Some n' -> if get_some @@ PTree.get n' join_points then None else Some n'
           in match successor with
           | Some n' -> begin
-                path_successors := !path_successors @ non_predicted_successors inst;
+                path_successors := !path_successors @ non_predicted_successors inst psucc;
                 dig_path_rec n'
               end
           | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize);