diff options
Diffstat (limited to 'backend/LICMaux.ml')
-rw-r--r-- | backend/LICMaux.ml | 332 |
1 files changed, 332 insertions, 0 deletions
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml new file mode 100644 index 00000000..82e4629f --- /dev/null +++ b/backend/LICMaux.ml @@ -0,0 +1,332 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +open RTL;; +open Camlcoq;; +open Maps;; +open Kildall;; +open HashedSet;; +open Inject;; +open DebugPrint;; +open RTLcommonaux;; + +type reg = P.t;; + +(** get_loop_headers moved from Duplicateaux.ml to LICMaux.ml to prevent cycle dependencies *) +type vstate = Unvisited | Processed | Visited + +let rtl_successors = function +| Itailcall _ | Ireturn _ -> [] +| Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n) +| Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> [n] +| Icond (_,_,n1,n2,_) -> [n1; n2] +| Ijumptable (_,ln) -> ln + +(** Getting loop branches with a DFS visit : + * Each node is either Unvisited, Visited, or Processed + * pre-order: node becomes Processed + * post-order: node becomes Visited + * + * If we come accross an edge to a Processed node, it's a loop! + *) +let get_loop_backedges code entrypoint = begin + debug "get_loop_backedges\n"; + let visited = ref (PTree.map (fun n i -> Unvisited) code) + and loop_backedge = ref (PTree.map (fun n i -> None) code) + in let rec dfs_visit code origin = function + | [] -> () + | node :: ln -> + debug "ENTERING node %d, REM are %a\n" (P.to_int node) print_intlist ln; + match (get_some @@ PTree.get node !visited) with + | Visited -> begin + debug "\tNode %d is already Visited, skipping\n" (P.to_int node); + dfs_visit code origin ln + end + | Processed -> begin + debug "Node %d is a loop header\n" (P.to_int node); + debug "The backedge is from %d\n" (P.to_int @@ get_some origin); + loop_backedge := PTree.set node origin !loop_backedge; + visited := PTree.set node Visited !visited; + dfs_visit code origin ln + end + | Unvisited -> begin + visited := PTree.set node Processed !visited; + debug "Node %d is Processed\n" (P.to_int node); + (match PTree.get node code with + | None -> failwith "No such node" + | Some i -> let next_visits = rtl_successors i in begin + debug "About to visit: %a\n" print_intlist next_visits; + dfs_visit code (Some node) next_visits + end); + debug "Node %d is Visited!\n" (P.to_int node); + visited := PTree.set node Visited !visited; + dfs_visit code origin ln + end + in begin + dfs_visit code None [entrypoint]; + debug "LOOP BACKEDGES: %a\n" print_ptree_opint !loop_backedge; + !loop_backedge + end +end + +let get_loop_headers code entrypoint = + let backedges = get_loop_backedges code entrypoint in + PTree.map (fun _ ob -> + match ob with + | None -> false + | Some _ -> true + ) backedges + +module Dominator = + struct + type t = Unreachable | Dominated of int | Multiple + let bot = Unreachable and top = Multiple + let beq a b = + match a, b with + | Unreachable, Unreachable + | Multiple, Multiple -> true + | (Dominated x), (Dominated y) -> x = y + | _ -> false + let lub a b = + match a, b with + | Multiple, _ + | _, Multiple -> Multiple + | Unreachable, x + | x, Unreachable -> x + | (Dominated x), (Dominated y) when x=y -> a + | (Dominated _), (Dominated _) -> Multiple + + let pp oc = function + | Unreachable -> output_string oc "unreachable" + | Multiple -> output_string oc "multiple" + | Dominated x -> Printf.fprintf oc "%d" x;; + end + +module Dominator_Solver = Dataflow_Solver(Dominator)(NodeSetForward) + +let apply_dominator (is_marked : node -> bool) (pc : node) + (before : Dominator.t) : Dominator.t = + match before with + | Dominator.Unreachable -> before + | _ -> + if is_marked pc + then Dominator.Dominated (P.to_int pc) + else before;; + +let dominated_parts1 (f : coq_function) : + (bool PTree.t) * (Dominator.t PMap.t option) = + let headers = get_loop_headers f.fn_code f.fn_entrypoint in + let dominated = Dominator_Solver.fixpoint f.fn_code RTL.successors_instr + (apply_dominator (fun pc -> match PTree.get pc headers with + | Some x -> x + | None -> false)) f.fn_entrypoint + Dominator.top in + (headers, dominated);; + +let dominated_parts (f : coq_function) : Dominator.t PMap.t * PSet.t PTree.t = + let (headers, dominated) = dominated_parts1 f in + match dominated with + | None -> failwith "dominated_parts 1" + | Some dominated -> + let singletons = + PTree.fold (fun before pc flag -> + if flag + then PTree.set pc (PSet.add pc PSet.empty) before + else before) headers PTree.empty in + (dominated, + PTree.fold (fun before pc ii -> + match PMap.get pc dominated with + | Dominator.Dominated x -> + let px = P.of_int x in + (match PTree.get px before with + | None -> failwith "dominated_parts 2" + | Some old -> + PTree.set px (PSet.add pc old) before) + | _ -> before) f.fn_code singletons);; + +let graph_traversal (initial_node : P.t) + (successor_iterator : P.t -> (P.t -> unit) -> unit) : PSet.t = + let seen = ref PSet.empty + and stack = Stack.create () in + Stack.push initial_node stack; + while not (Stack.is_empty stack) + do + let vertex = Stack.pop stack in + if not (PSet.contains !seen vertex) + then + begin + seen := PSet.add vertex !seen; + successor_iterator vertex (fun x -> Stack.push x stack) + end + done; + !seen;; + +let filter_dominated_part (predecessors : P.t list PTree.t) + (header : P.t) (dominated_part : PSet.t) = + graph_traversal header + (fun (vertex : P.t) (f : P.t -> unit) -> + match PTree.get vertex predecessors with + | None -> () + | Some l -> + List.iter + (fun x -> + if PSet.contains dominated_part x + then f x) l + );; + +let inner_loops (f : coq_function) = + let (dominated, parts) = dominated_parts f + and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in + (dominated, predecessors, PTree.map (filter_dominated_part predecessors) parts);; + +let map_reg mapper r = + match PTree.get r mapper with + | None -> r + | Some x -> x;; + +let rewrite_loop_body (last_alloc : reg ref) + (insns : RTL.code) (header : P.t) (loop_body : PSet.t) = + let seen = ref PSet.empty + and stack = Stack.create () + and rewritten = ref [] in + let add_inj ii = rewritten := ii::!rewritten in + Stack.push (header, PTree.empty) stack; + while not (Stack.is_empty stack) + do + let (pc, mapper) = Stack.pop stack in + if not (PSet.contains !seen pc) + then + begin + seen := PSet.add pc !seen; + match PTree.get pc insns with + | None -> () + | Some ii -> + let mapper' = + match ii with + | Iop(op, args, res, pc') when not (Op.is_trapping_op op) -> + let new_res = P.succ !last_alloc in + last_alloc := new_res; + add_inj (INJop(op, + (List.map (map_reg mapper) args), + new_res)); + PTree.set res new_res mapper + | Iload(_, chunk, addr, args, v, pc') + | Istore(chunk, addr, args, v, pc') + when Archi.has_notrap_loads && + !Clflags.option_fnontrap_loads -> + let new_res = P.succ !last_alloc in + last_alloc := new_res; + add_inj (INJload(chunk, addr, + (List.map (map_reg mapper) args), + new_res)); + PTree.set v new_res mapper + | _ -> mapper in + List.iter (fun x -> + if PSet.contains loop_body x + then Stack.push (x, mapper') stack) + (successors_instr ii) + end + done; + List.rev !rewritten;; + +let pp_inj_instr (oc : out_channel) (ii : inj_instr) = + match ii with + | INJnop -> output_string oc "nop" + | INJop(op, args, res) -> + Printf.fprintf oc "%a = %a" + PrintRTL.reg res (PrintOp.print_operation PrintRTL.reg) (op, args) + | INJload(chunk, addr, args, dst) -> + Printf.fprintf oc "%a = %s[%a]" + PrintRTL.reg dst (PrintAST.name_of_chunk chunk) + (PrintOp.print_addressing PrintRTL.reg) (addr, args);; + +let pp_inj_list (oc : out_channel) (l : inj_instr list) = + List.iter (Printf.fprintf oc "%a; " pp_inj_instr) l;; + +let pp_injections (oc : out_channel) (injections : inj_instr list PTree.t) = + List.iter + (fun (pc, injl) -> + Printf.fprintf oc "%d : %a\n" (P.to_int pc) pp_inj_list injl) + (PTree.elements injections);; + +let compute_injections1 (f : coq_function) = + let (dominated, predecessors, loop_bodies) = inner_loops f + and last_alloc = ref (max_reg_function f) in + (dominated, predecessors, + PTree.map (fun header body -> + (body, rewrite_loop_body last_alloc f.fn_code header body)) loop_bodies);; + +let compute_injections (f : coq_function) : inj_instr list PTree.t = + let (dominated, predecessors, injections) = compute_injections1 f in + let output_map = ref PTree.empty in + List.iter + (fun (header, (body, inj)) -> + match PTree.get header predecessors with + | None -> failwith "compute_injections" + | Some l -> + List.iter (fun predecessor -> + if (PMap.get predecessor dominated)<>Dominator.Unreachable && + not (PSet.contains body predecessor) + then output_map := PTree.set predecessor inj !output_map) l) + (PTree.elements injections); + !output_map;; + +let pp_list pp_item oc l = + output_string oc "{ "; + let first = ref true in + List.iter (fun x -> + (if !first + then first := false + else output_string oc ", "); + pp_item oc x) l; + output_string oc " }";; + +let pp_pset oc s = + pp_list (fun oc -> Printf.fprintf oc "%d") oc + (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s)));; + +let print_dominated_parts oc f = + List.iter (fun (header, nodes) -> + Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) + (PTree.elements (snd (dominated_parts f)));; + +let print_inner_loops oc f = + List.iter (fun (header, nodes) -> + Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) + (PTree.elements (let (_,_,l) = (inner_loops f) in l));; + +let print_dominated_parts1 oc f = + match snd (dominated_parts1 f) with + | None -> output_string oc "error\n" + | Some parts -> + List.iter + (fun (pc, instr) -> + Printf.fprintf oc "%d : %a\n" (P.to_int pc) Dominator.pp + (PMap.get pc parts) + ) + (PTree.elements f.fn_code);; + +let loop_headers (f : coq_function) : RTL.node list = + List.map fst (List.filter snd (PTree.elements (get_loop_headers f.fn_code f.fn_entrypoint)));; + +let print_loop_headers f = + print_endline "Loop headers"; + List.iter + (fun i -> Printf.printf "%d " (P.to_int i)) + (loop_headers f); + print_newline ();; + +let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): + (Inject.inj_instr list) PTree.t = + let injections = compute_injections f in + (* let () = pp_injections stdout injections in *) + injections;; |