diff options
Diffstat (limited to 'scheduling/RTLpathLivegenaux.ml')
| -rw-r--r-- | scheduling/RTLpathLivegenaux.ml | 309 |
1 files changed, 309 insertions, 0 deletions
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml new file mode 100644 index 00000000..dd971db8 --- /dev/null +++ b/scheduling/RTLpathLivegenaux.ml @@ -0,0 +1,309 @@ +open RTL +open RTLpath +open Registers +open Maps +open Camlcoq +open Datatypes +open Kildall +open Lattice + +let debug_flag = ref false + +let dprintf fmt = let open Printf in + match !debug_flag with + | true -> printf fmt + | false -> ifprintf stdout fmt + +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) + +let rec list_to_regset = function + | [] -> Regset.empty + | r::l -> Regset.add r (list_to_regset l) + +let get_input_regs i = + let empty = Regset.empty in + match i with + | Inop _ -> empty + | Iop (_,lr,_,_) | Iload (_,_,_,lr,_,_) | Icond (_,lr,_,_,_) -> list_to_regset lr + | Istore (_,_,lr,r,_) -> Regset.add r (list_to_regset lr) + | Icall (_, ri, lr, _, _) | Itailcall (_, ri, lr) -> begin + let rs = list_to_regset lr in + match ri with + | Coq_inr _ -> rs + | Coq_inl r -> Regset.add r rs + end + | Ibuiltin (_, lbr, _, _) -> list_to_regset @@ AST.params_of_builtin_args lbr + | Ijumptable (r, _) -> Regset.add r empty + | Ireturn opr -> (match opr with Some r -> Regset.add r empty | None -> empty) + +let get_output_reg i = + match i with + | Inop _ | Istore _ | Icond _ | Itailcall _ | Ijumptable _ | Ireturn _ -> None + | 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 + let path_map = ref PTree.empty in + let rec dig_path e = + let psize = ref (-1) in + let path_successors = ref [] in + let rec dig_path_rec n : (path_info * node list) option = + if not (get_some @@ PTree.get n !visited) then + let inst = get_some @@ PTree.get n code in + begin + visited := PTree.set n true !visited; + psize := !psize + 1; + let successor = match predicted_successor inst 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; + dig_path_rec n' + end + | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize); + input_regs = Regset.empty; output_regs = Regset.empty }, + !path_successors @ successors_inst inst) + end + else None + in match dig_path_rec e with + | None -> () + | Some ret -> + let (path_info, succs) = ret in + begin + path_map := PTree.set e path_info !path_map; + List.iter dig_path succs + end + in begin + dig_path entry; + !path_map + end + +let print_regset rs = begin + dprintf "["; + List.iter (fun n -> dprintf "%d " (P.to_int n)) (Regset.elements rs); + dprintf "]" +end + +let print_ptree_regset pt = begin + dprintf "["; + List.iter (fun (n, rs) -> + dprintf "\n\t"; + dprintf "%d: " (P.to_int n); + print_regset rs + ) (PTree.elements pt); + dprintf "]" +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 + | 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 + +let get_last_nodes f = + let visited = ref (PTree.map (fun n i -> false) f.fn_code) in + let rec step n = + let inst = get_some @@ PTree.get n f.fn_code in + let successors = successors_inst inst in + if get_some @@ PTree.get n !visited then [] + else begin + +let analyze f = + let liveness = ref (PTree.map (fun n i -> None) f.fn_code) in + let predecessors = Duplicateaux.get_predecessors_rtl f.fn_code in + let last_nodes = get_last_nodes f in + let rec step liveout n = (* liveout is the input_regs from the successor *) + let inst = get_some @@ PTree.get n f.fn_code in + let continue = ref true in + let alive = match get_some @@ PTree.get n !liveness with + | None -> transfer liveout inst + | Some pre_alive -> begin + let union = Regset.union pre_alive liveout in + let new_alive = transfer union inst in + (if Regset.equal pre_alive new_alive then continue := false); + new_alive + end + in begin + liveness := PTree.set n (Some alive) !liveness; + if !continue then + let preds = get_some @@ PTree.get n predecessors in + List.iter (step alive) preds + end + in begin + List.iter (step Regset.empty) last_nodes; + let liveness_noopt = PTree.map (fun n i -> get_some i) !liveness in + begin + debug_flag := true; + dprintf "Liveness: "; print_ptree_regset liveness_noopt; dprintf "\n"; + debug_flag := false; + liveness_noopt + end + end +*) + +let rec traverse code n size = + let inst = get_some @@ PTree.get n code in + if (size == 0) then inst + else + let n' = get_some @@ predicted_successor inst in + traverse code n' (size-1) + +let get_outputs liveness code n pi = + let last_instruction = traverse code n (Camlcoq.Nat.to_int pi.psize) in + let path_last_successors = successors_inst last_instruction in + let list_input_regs = List.map ( + fun n -> get_some @@ PTree.get n liveness + ) path_last_successors in + List.fold_left Regset.union Regset.empty list_input_regs + +let set_pathmap_liveness f pm = + let liveness = analyze f in + let new_pm = ref PTree.empty in + let code = f.fn_code in + begin + dprintf "Liveness: "; print_ptree_regset liveness; dprintf "\n"; + List.iter (fun (n, pi) -> + let inputs = get_some @@ PTree.get n liveness in + let outputs = get_outputs liveness code n pi in + new_pm := PTree.set n + {psize=pi.psize; input_regs=inputs; output_regs=outputs} !new_pm + ) (PTree.elements pm); + !new_pm + end + +let print_true_nodes booltree = begin + dprintf "["; + List.iter (fun (n,b) -> + if b then dprintf "%d " (P.to_int n) + ) (PTree.elements booltree); + dprintf "]"; +end + +let print_path_info pi = begin + dprintf "(psize=%d; " (Camlcoq.Nat.to_int pi.psize); + dprintf "input_regs="; + print_regset pi.input_regs; + dprintf "; output_regs="; + print_regset pi.output_regs; + dprintf ")" +end + +let print_path_map path_map = begin + dprintf "["; + List.iter (fun (n,pi) -> + dprintf "\n\t"; + dprintf "%d: " (P.to_int n); + print_path_info pi + ) (PTree.elements path_map); + dprintf "]" +end + +let build_path_map f = + let code = f.fn_code in + let entry = f.fn_entrypoint in + let join_points = get_join_points code entry in + let path_map = set_pathmap_liveness f @@ get_path_map code entry join_points in + begin + dprintf "Join points: "; + print_true_nodes join_points; + dprintf "\nPath map: "; + print_path_map path_map; + dprintf "\n"; + path_map + end |