1 files changed, 4 insertions, 81 deletions

diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index 2a20a15d..976ddc16 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -4,34 +4,8 @@ open Registers
 open Maps
 open Camlcoq
 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 RTLcommonaux
 
 let rec list_to_regset = function
   | [] -> Regset.empty
@@ -59,24 +33,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 +48,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);
@@ -118,40 +75,6 @@ let get_path_map code entry join_points =
     !path_map
   end
 
-let transfer f pc after = let open Liveness in
-  match PTree.get pc f.fn_code with
-  | Some i ->
-    (match i with
-    | Inop _ -> after
-    | Iop (_, args, res, _) ->
-        reg_list_live args (Regset.remove res after)
-    | Iload (_, _, _, args, dst, _) ->
-        reg_list_live args (Regset.remove dst after)
-    | Istore (_, _, args, src, _) ->
-        reg_list_live args (Regset.add src after)
-    | Icall (_, ros, args, res, _) ->
-        reg_list_live args (reg_sum_live ros (Regset.remove res after))
-    | Itailcall (_, ros, args) ->
-        reg_list_live args (reg_sum_live ros Regset.empty)
-    | Ibuiltin (_, args, res, _) ->
-        reg_list_live (AST.params_of_builtin_args args)
-          (reg_list_dead (AST.params_of_builtin_res res) after)
-    | Icond (_, args, _, _, _) ->
-        reg_list_live args after
-    | Ijumptable (arg, _) ->
-        Regset.add arg after
-    | Ireturn optarg ->
-        reg_option_live optarg Regset.empty)
-  | None -> Regset.empty
-
-module RegsetLat = LFSet(Regset)
-
-module DS = Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward)
-
-let analyze f =
-  let liveouts = get_some @@ DS.fixpoint f.fn_code successors_instr (transfer f) in
-  PTree.map (fun n _ -> let lo = PMap.get n liveouts in transfer f n lo) f.fn_code
-
 (** OLD CODE - If needed to have our own kildall
 
 let transfer after = let open Liveness in function