diff options
Diffstat (limited to 'scheduling/RTLpathLivegenaux.ml')
-rw-r--r-- | scheduling/RTLpathLivegenaux.ml | 85 |
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 |