diff options
Diffstat (limited to 'src/pipelining/SPBasic.ml')
| -rw-r--r-- | src/pipelining/SPBasic.ml | 819 |
1 files changed, 819 insertions, 0 deletions
diff --git a/src/pipelining/SPBasic.ml b/src/pipelining/SPBasic.ml new file mode 100644 index 0000000..32234b8 --- /dev/null +++ b/src/pipelining/SPBasic.ml @@ -0,0 +1,819 @@ +(***********************************************************************) + (* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open RTL +open Camlcoq +open Graph.Pack.Digraph +open Op +open Registers +open Memory +open Mem +open AST +open SPBase_types +open SPSymbolic_evaluation + +type node = instruction * int +module G = Graph.Persistent.Digraph.AbstractLabeled + (struct type t = node end) + (struct type t = int let compare = compare let default = 0 end) +module Topo = Graph.Topological.Make (G) +module Dom = Graph.Dominator.Make (G) +module Index = Map.Make (struct type t = int let compare = compare end) + +let string_of_instruction node = + match G.V.label node with + | (Inop,n) -> Printf.sprintf "%i nop" n + | (Iop (op, args, dst),n) -> Printf.sprintf "%i r%i := %s %s" n (to_int dst) (string_of_op op) (string_of_args args) + | (Iload (chunk, mode, args, dst),n) -> Printf.sprintf "%i r%i := load %s" n (to_int dst) (string_of_args args) + | (Istore (chunk, mode, args, src),n) -> Printf.sprintf "%i store %i %s" n (to_int src) (string_of_args args) + | (Icall (sign, id, args, dst),n) -> Printf.sprintf "%i call" n + | (Itailcall (sign, id, args),n) -> Printf.sprintf "%i tailcall" n + (* | (Ialloc (dst, size),n) -> Printf.sprintf "%i %i := alloc" n (to_int dst) *) + | (Icond (cond, args),n) -> Printf.sprintf "%i cond %s %s" n (string_of_cond cond) (string_of_args args) + | (Ireturn (res),n) -> Printf.sprintf "%i return" n + +let string_of_node = string_of_instruction + +module Display = struct + include G + let vertex_name v = print_inst (V.label v) + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_attributes v = [`Label (string_of_instruction v)] + let default_edge_attributes _ = [] + let edge_attributes e = [`Label (string_of_int (G.E.label e))] + let get_subgraph _ = None +end +module Dot_ = Graph.Graphviz.Dot(Display) + +let dot_output g f = + let oc = open_out f in + Dot_.output_graph oc g; + close_out oc + +let display g name = + let addr = SPDebug.name ^ name in + dot_output g addr ; + ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr ^ ".png ; rm -f " ^ addr ^ ") & ")) + +(******************************************) + +type cfg = {graph : G.t; start : G.V.t} + +(* convert traduit un graphe RTL compcert en un graphe RTL ocamlgraph*) + +let convert f = + + let make_node inst key = + let inst = inst_coq_to_caml inst in + G.V.create (inst, to_int key) + in + + let (graph, index) = Maps.PTree.fold (fun (g,m) key inst -> + let node = make_node inst key in + (G.add_vertex g node, Index.add (to_int key) node m) + ) f.fn_code (G.empty,Index.empty) + in + + let succ = RTL.successors_map f in + let rec link n succs g = + match succs with + | [] -> g + | pos::[] -> + G.add_edge g (Index.find (to_int n) index) (Index.find (to_int pos) index) + | pos1::pos2::[] -> + let g = G.add_edge_e g (G.E.create (Index.find (to_int n) index) 1 (Index.find (to_int pos1) index)) in + G.add_edge_e g (G.E.create (Index.find (to_int n) index) 2 (Index.find (to_int pos2) index)) + | _ -> failwith "convert : trop de successeurs" + + in + + let graph = Maps.PTree.fold ( fun g key inst -> + link key (match Maps.PTree.get key succ with + Some x -> x | _ -> failwith "Could not index") g + ) f.fn_code graph + in + + {graph = graph; start = Index.find (to_int (f.fn_entrypoint)) index} + + +let convert_back g = + + G.fold_vertex (fun node m -> + let v = G.V.label node in + match (fst v) with + | Icond (_,_) -> + begin + let l = + match G.succ_e g node with + | [e1;e2] -> + if G.E.label e1 > G.E.label e2 + then [G.E.dst e2;G.E.dst e1] + else [G.E.dst e1;G.E.dst e2] + | _ -> failwith "convert_back: nombre de successeurs incoherent" + in + let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) l in + Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m + end + | _ -> + let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) (G.succ g node) in + Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m + ) g Maps.PTree.empty + + + + +(* dominator_tree calcule l'arbre de domination grace au code de FP *) +let dominator_tree f = + Dom.compute_idom f.graph f.start + +(* detect_loops, find the loops in the graph and returns the list of nodes in it, + in dominating order !!! This is of great importance, we suppose that it is ordered + when we build the dependency graph *) +let detect_loops graph dom_tree = + let rec is_dominating v1 v2 l = (* does v1 dominate v2 *) + match dom_tree v2 with + | v -> if v1 = v then Some (v :: l) + else is_dominating v1 v (v :: l) + | exception (Not_found) -> None + in + + G.fold_edges (fun v1 v2 loops -> + match is_dominating v2 v1 [v1] with + | None -> loops + | Some loop -> (v2,loop) :: loops + ) graph [] + +let print_index node = + Printf.printf "%i " (snd (G.V.label node)) + +let print_instruction node = + match G.V.label node with + | (Inop,n) -> Printf.printf "%i : Inop \n" n + | (Iop (op, args, dst),n) -> Printf.printf "%i : Iop \n" n + | (Iload (chunk, mode, args, dst),n) -> Printf.printf "%i : Iload \n" n + | (Istore (chunk, mode, args, src),n) -> Printf.printf "%i : Istore \n" n + | (Icall (sign, id, args, dst),n) -> Printf.printf "%i : Icall \n" n + | (Itailcall (sign, id, args),n) -> Printf.printf "%i : Itailcall \n" n + (*| (Ialloc (dst, size),n) -> Printf.printf "%i : Ialloc \n" n *) + | (Icond (cond, args),n) -> Printf.printf "%i : Icond \n" n + | (Ireturn (res),n) -> Printf.printf "%i : Ireturn \n" n + +let is_rewritten node r = + match fst (G.V.label node) with + | Inop -> false + | Iop (op, args, dst) -> if dst = r then true else false + | Iload (chunk, mode, args, dst) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false + | Istore (chunk, mode, args, src) -> false + | Icall (sign, id, args, dst) -> failwith "call in a loop" + | Itailcall (sign, id, args) -> failwith "tailcall in a loop" + (* | Ialloc (dst, size) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false *) + | Icond (cond, args) -> false + | Ireturn (res) -> failwith "return in a loop" + +let is_variant r loop = + List.fold_right (fun node b -> + is_rewritten node r || b + ) loop false + + +let is_pipelinable loop = (* true if loop is innermost and without control *) + + let is_acceptable node = + match fst (G.V.label node) with + | Icall _ | Itailcall _ | Ireturn _ | Icond _ (*| Ialloc _*) | Iop ((Ocmp _),_,_)-> false + | _ -> true + in + + let is_branching node = + match fst (G.V.label node) with + | Icond _ -> true + | _ -> false + in + + let is_nop node = + match fst (G.V.label node) with + | Inop -> true + | _ -> false + in + + let is_OK_aux l = + List.fold_right (fun n b -> is_acceptable n && b) l true + in + + let is_bounded node loop = + match G.V.label node with + | (Icond (cond, args),n) -> + let args = to_caml_list args in + begin + match args with + | [] -> false + | r :: [] -> is_variant r loop (* used to be not *) + | r1 :: r2 :: [] -> + begin + match is_variant r1 loop, is_variant r2 loop with + | true, true -> false + | false, true -> true + | true, false -> true + | false, false -> false + end + | _ -> false + end + | _ -> false + in + + match List.rev loop with + | v2 :: v1 :: l -> ((*Printf.printf "is_nop: %s | " (is_nop v1 |> string_of_bool);*) + Printf.printf "is_branching: %s | " (is_branching v2 |> string_of_bool); + Printf.printf "is_OK_aux: %s | " (is_OK_aux l |> string_of_bool); + Printf.printf "is_bounded: %s\n" (is_bounded v2 loop |> string_of_bool); + (*is_nop v1 && *)is_branching v2 && is_OK_aux l && is_bounded v2 loop) + | _ -> false + +let print_loops loops = + List.iter (fun loop -> print_index (fst(loop)); + print_newline (); + List.iter print_index (snd(loop)); + print_newline (); + if is_pipelinable (snd(loop)) then print_string "PIPELINABLE !" else print_string "WASTE"; + print_newline (); + List.iter print_instruction (snd(loop)); + print_newline () + ) loops + +(* type resource = Reg of reg | Mem *) +module Sim = Map.Make (struct type t = resource let compare = compare end) + +let map_get key map = + try Some (Sim.find key map) + with + | Not_found -> None + +let rec to_res l = + match l with + | [] -> [] + | e :: l -> Reg e :: to_res l + +let resources_reads_of node = + match fst (G.V.label node) with + | Inop -> [] + | Iop (op, args, dst) -> to_res args + | Iload (chunk, mode, args, dst) -> Mem :: (to_res args) + | Istore (chunk, mode, args, src) -> Mem :: Reg src :: (to_res args) + | Icall (sign, id, args, dst) -> failwith "Resource read of call" + | Itailcall (sign, id, args) -> failwith "Resource read of tailcall" + (*| Ialloc (dst, size) -> [Mem] *) + | Icond (cond, args) -> to_res args + | Ireturn (res) -> failwith "Resource read of return" + +let resources_writes_of node = + match fst (G.V.label node) with + | Inop -> [] + | Iop (op, args, dst) -> [Reg dst] + | Iload (chunk, mode, args, dst) -> [Reg dst] + | Istore (chunk, mode, args, src) -> [Mem] + | Icall (sign, id, args, dst) -> failwith "Resource read of call" + | Itailcall (sign, id, args) -> failwith "Resource read of tailcall" + (*| Ialloc (dst, size) -> (Reg dst) :: [Mem]*) + | Icond (cond, args) -> [] + | Ireturn (res) -> failwith "Resource read of return" + +let build_intra_dependency_graph loop = + + let rec build_aux graph read write l = + match l with + | [] -> (graph,(read,write)) + | v :: l-> + let g = G.add_vertex graph v in + let reads = resources_reads_of v in + let writes = resources_writes_of v in + (* dependances RAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> G.add_edge_e g (G.E.create n 1 v) + | None -> g + ) reads g in + (* dependances WAR *) + let g = List.fold_right (fun r g -> + match map_get r read with + | Some l -> List.fold_right (fun n g -> G.add_edge_e g (G.E.create n 2 v)) l g + | None -> g + ) writes g in + (* dependances WAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> G.add_edge_e g (G.E.create n 3 v) + | None -> g + ) writes g in + let write = List.fold_right (fun r m -> Sim.add r v m) writes write in + let read_tmp = List.fold_right (fun r m -> + match map_get r read with + | Some al -> Sim.add r (v :: al) m + | None -> Sim.add r (v :: []) m + ) reads read + in + let read = List.fold_right (fun r m -> Sim.add r [] m) writes read_tmp in + + build_aux g read write l + in + + build_aux G.empty Sim.empty Sim.empty (List.tl loop) + +let build_inter_dependency_graph loop = + + let rec build_aux2 graph read write l = + match l with + | [] -> graph + | v :: l-> + let g = graph in + let reads = resources_reads_of v in + let writes = resources_writes_of v in + (* dependances RAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 4 v) + | None -> g + ) reads g in + (* dependances WAR *) + let g = List.fold_right (fun r g -> + match map_get r read with + | Some l -> List.fold_right + (fun n g -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 5 v)) l g + | None -> g + ) writes g in + (* dependances WAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 6 v) + | None -> g + ) writes g in + let write = List.fold_right (fun r m -> Sim.remove r m) writes write in + let read = List.fold_right (fun r m -> Sim.remove r m) writes read in + + + build_aux2 g read write l + in + + let (g,(r,w)) = build_intra_dependency_graph loop in + build_aux2 g r w (List.tl loop) + +(* patch_graph prepare le graphe pour la boucle commencant au noeud entry + qui a une borne de boucle bound et pour un software pipelining + de au minimum min tours et de deroulement ur *) +(* this is rather technical so we give many comments *) + +(* let n1 = G.V.create (Iop ((Ointconst ur),to_coq_list [],r1),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n2 = G.V.create (Iop (Odiv,to_coq_list [bound;r1],r2),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n3 = G.V.create (Iop ((Omulimm ur),to_coq_list [r2],r3),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n4 = G.V.create (Iop (Osub,to_coq_list [bound;r3],r4),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n5 = G.V.create (Iop (Omove,to_coq_list [r3],bound),next_pc) in (\* retouchee, [r3],bound *\) *) + + +let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog epilog ramp_up ramp_down = + + (* 1. Break the edge that enters the loop, except for the backedge *) + let preds_e = G.pred_e graph entry in + let wannabes = List.map G.E.src preds_e in + let wannabes = List.filter (fun e -> not (e = lastone)) wannabes in + let graph = List.fold_right (fun e g -> G.remove_edge_e g e) preds_e graph in + let graph = G.add_edge graph lastone entry in + + (* 2. Add the test for minimal iterations and link it*) + + let cond = G.V.create (Icond ((Ccompimm (Integers.Cle,min)),to_coq_list [bound]), next_pc) in + let graph = G.add_vertex graph cond in + let next_pc = next_pc + 1 in + + (* 3. Link its predecessors and successors *) + (* It is false in case there is a condition that points to the entry: + inthis case, the edge should not be labeled with 0 !*) + + let graph = List.fold_right (fun n g -> G.add_edge g n cond) wannabes graph in + let graph = G.add_edge_e graph (G.E.create cond 1 entry) in + + + (* 4. Add the div and modulo code, link it *) + let n1 = G.V.create (Iop ((Ointconst ur),to_coq_list [],r1),next_pc) in + let next_pc = next_pc + 1 in + let n2 = G.V.create (Iop (Odiv,to_coq_list [bound;r1],r2),next_pc) in + let next_pc = next_pc + 1 in + let n3 = G.V.create (Iop (Omove,to_coq_list [bound],r4),next_pc) in + let next_pc = next_pc + 1 in + let n4 = G.V.create (Iop ((Omulimm ur ),to_coq_list [r2],r3),next_pc) in + let next_pc = next_pc + 1 in + let n5 = G.V.create (Iop ((Olea (Aindexed (Z.of_sint (-1)))),to_coq_list [r3],bound),next_pc) in (* retouchee, [r3],bound *) + let next_pc = next_pc + 1 in + let graph = G.add_vertex graph n1 in + let graph = G.add_vertex graph n2 in + let graph = G.add_vertex graph n3 in + let graph = G.add_vertex graph n4 in + let graph = G.add_vertex graph n5 in + let graph = G.add_edge_e graph (G.E.create cond 2 n1) in + let graph = G.add_edge graph n1 n2 in + let graph = G.add_edge graph n2 n3 in + let graph = G.add_edge graph n3 n4 in + let graph = G.add_edge graph n4 n5 in + + (* 5. Fabriquer la pipelined loop et la linker, sans la condition d entree *) + + let (graph,next_pc,l) = List.fold_right (fun e (g,npc,l) -> + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) loop (graph,next_pc,[]) in + + let pipe_cond = List.hd l in + let pipeline = List.tl l in + + let rec link l graph node = + match l with + | n1 :: n2 :: l -> link (n2 :: l) (G.add_edge graph n1 n2) node + | n1 :: [] -> G.add_edge graph n1 node + | _ -> graph + in + + let graph = link pipeline graph pipe_cond in + + (* link de l entree de la boucle *) + + let (graph,next_pc,prolog) = List.fold_right (fun e (g,npc,l) -> + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) prolog (graph,next_pc,[]) in + + let (graph,next_pc,epilog) = List.fold_right (fun e (g,npc,l) -> + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) epilog (graph,next_pc,[]) in + + (* 6. Creation du reste et branchement et la condition *) + let n6 = G.V.create (Iop (Omove,to_coq_list [r4],bound),next_pc) in (* Iop (Omove,to_coq_list [r4],bound) *) + let next_pc = next_pc + 1 in + + (* 7. Creation du ramp up *) + let ramp_up = List.map (fun (a,b) -> Iop (Omove, [b], a)) ramp_up in + let (graph,next_pc,ramp_up) = List.fold_right (fun e (g,npc,l) -> + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) ramp_up (graph,next_pc,[]) in + + let next_pc = next_pc + 1 in + + let ramp_down = List.map (fun (a,b) -> Iop (Omove,[b],a)) ramp_down in + let (graph,next_pc,ramp_down) = List.fold_right (fun e (g,npc,l) -> + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) ramp_down (graph,next_pc,[]) in + + (* let next_pc = next_pc + 1 in *) + + (* Creation des proloque et epilogue *) + + let graph = link prolog graph pipe_cond in + let graph = link ramp_up graph (List.hd prolog) in + let graph = link epilog graph (List.hd ramp_down) in + let graph = link ramp_down graph n6 in + + let graph = G.add_edge graph n5 (List.hd ramp_up) in + let graph = G.add_edge_e graph (G.E.create pipe_cond 1 (List.hd epilog)) in + let graph = G.add_edge_e graph (G.E.create pipe_cond 2 (List.hd pipeline)) in + + (* 8. Retour sur la boucle classique *) + let graph = G.add_edge graph n6 entry in + + graph + +let regs_of_node node = + match G.V.label node with + | (Inop,n) -> [] + | (Iop (op, args, dst),n) -> dst :: (to_caml_list args) + | (Iload (chunk, mode, args, dst),n) -> dst :: (to_caml_list args) + | (Istore (chunk, mode, args, src),n) -> src :: (to_caml_list args) + | (Icall (sign, id, args, dst),n) -> dst :: (to_caml_list args) + | (Itailcall (sign, id, args),n) -> (to_caml_list args) + (*| (Ialloc (dst, size),n) -> [dst]*) + | (Icond (cond, args),n) -> (to_caml_list args) + | (Ireturn (res),n) -> match res with Some res -> [res] | _ -> [] + +let max_reg_of_graph graph params = + Printf.fprintf SPDebug.dc "Calcul du registre de depart.\n"; + let regs = G.fold_vertex (fun node regs -> + (regs_of_node node) @ regs + ) graph [] in + let regs = regs @ params in + let max_reg = List.fold_right (fun reg max -> + Printf.fprintf SPDebug.dc "%i " (P.to_int reg); + if Int32.compare (P.to_int32 reg) max > 0 + then (P.to_int32 reg) + else max + ) regs Int32.zero in + + Printf.fprintf SPDebug.dc "MAX REG = %i\n" (Int32.to_int max_reg); + BinPos.Pos.succ (P.of_int32 max_reg) + +let get_bound node loop = + match G.V.label node with + | (Icond (cond, args),n) -> + let args = to_caml_list args in + begin + match args with + | [] -> failwith "get_bound: condition sans variables" + | r :: [] -> if is_variant r loop then failwith "Pas de borne dans la boucle" else r (* Modified false to true condition. *) + | r1 :: r2 :: [] -> + begin + match is_variant r1 loop, is_variant r2 loop with + | true, true -> failwith "Pas de borne dans la boucle " + | false, true -> r1 + | true, false -> r2 + | false, false -> failwith "deux bornes possibles dans la boucle" + end + | _ -> failwith "get_bound: condition avec nombre de variables superieur a 2" + end + | _ -> failwith "get_bound: the node I was given is not a condition\n" + +let get_nextpc graph = + (G.fold_vertex (fun node max -> + if (snd (G.V.label node)) > max + then (snd (G.V.label node)) + else max + ) graph 0) + 1 + +let substitute_pipeline graph loop steady_state prolog epilog min unrolling ru rd params = + let n1 = max_reg_of_graph graph params in + let n2 = (BinPos.Pos.succ n1) in + let n3 = (BinPos.Pos.succ n2) in + let n4 = (BinPos.Pos.succ n3) in + let way_in = (List.hd loop) in + let way_out = (List.hd (List.rev loop)) in + let bound = (get_bound way_out loop) in + let min = Z.of_sint min in + let unrolling = Z.of_sint unrolling in + let next_pc = get_nextpc graph in + patch_graph graph way_in way_out steady_state bound min unrolling n1 n2 n3 n4 next_pc prolog epilog ru rd + +let get_loops cfg = + let domi = dominator_tree cfg in + let loops = detect_loops cfg.graph domi in + print_loops loops; + let loops = List.filter (fun loop -> is_pipelinable (snd (loop))) loops in + loops + +type pipeline = {steady_state : G.V.t list; prolog : G.V.t list; epilog : G.V.t list; + min : int; unrolling : int; ramp_up : (reg * reg) list; ramp_down : (reg * reg) list} + +let delete_indexes l = List.map (fun e -> fst (G.V.label e) ) l + +type reg = Registers.reg + +let fresh = ref BinNums.Coq_xH + +let distance e = + match G.E.label e with + | 1 | 2 | 3 -> 0 + | _ -> 1 + +type et = IntraRAW | IntraWAW | IntraWAR | InterRAW | InterWAW | InterWAR + +let edge_type e = + match G.E.label e with + | 1 -> IntraRAW + | 2 -> IntraWAR + | 3 -> IntraWAW + | 4 -> InterRAW + | 5 -> InterWAR + | 6 -> InterWAW + | _ -> failwith "Unknown edge type" + +let latency n = (* A raffiner *) + match fst (G.V.label n) with + | Iop (op,args, dst) -> + begin + match op with + | Omove -> 1 + (*| Oaddimm _ -> 1*) + (*| Oadd -> 2*) + | Omul -> 4 + | Odiv -> 30 + | Omulimm _ -> 4 + | _ -> 2 + end + | Iload _ -> 1 + (* | Ialloc _ -> 20*) + | _ -> 1 + +let reforge_writes inst r = + G.V.create ((match fst (G.V.label inst) with + | Inop -> Inop + | Iop (op, args, dst) -> Iop (op, args, r) + | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, args, r) + | Istore (chunk, mode, args, src) -> Istore (chunk, mode, args, src) + | Icall (sign, id, args, dst) -> failwith "reforge_writes: call" + | Itailcall (sign, id, args) -> failwith "reforge_writes: tailcall" + (* | Ialloc (dst, size) -> Ialloc (r, size)*) + | Icond (cond, args) -> Icond (cond, args) + | Ireturn (res) -> failwith "reforge_writes: return") + , snd (G.V.label inst)) + +let rec reforge_args args oldr newr = + match args with + | [] -> [] + | e :: l -> (if e = oldr then newr else e) :: (reforge_args l oldr newr) + +let rec mem_args args r = + match args with + | [] -> false + | e :: l -> if e = r then true else mem_args l r + +let check_read_exists inst r = + match fst (G.V.label inst) with + | Inop -> false + | Iop (op, args, dst) -> mem_args args r + | Iload (chunk, mode, args, dst) -> mem_args args r + | Istore (chunk, mode, args, src) -> src = r || mem_args args r + | Icall (sign, id, args, dst) -> mem_args args r + | Itailcall (sign, id, args) -> false + (*| Ialloc (dst, size) -> false*) + | Icond (cond, args) -> mem_args args r + | Ireturn (res) -> false + +let reforge_reads inst oldr newr = + assert (check_read_exists inst oldr); + G.V.create ((match fst (G.V.label inst) with + | Inop -> Inop + | Iop (op, args, dst) -> Iop (op, reforge_args args oldr newr, dst) + | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, reforge_args args oldr newr, dst) + | Istore (chunk, mode, args, src) -> Istore (chunk, mode, reforge_args args oldr newr , if src = oldr then newr else src) + | Icall (sign, id, args, dst) -> failwith "reforge_reads: call" + | Itailcall (sign, id, args) -> failwith "reforge_reads: tailcall" + (*| Ialloc (dst, size) -> Ialloc (dst, size)*) + | Icond (cond, args) -> Icond (cond, reforge_args args oldr newr) + | Ireturn (res) -> failwith "reforge_reads: return") + , snd (G.V.label inst)) + +let get_succs_raw ddg node = + let succs = G.succ_e ddg node in + let succs = List.filter (fun succ -> + match G.E.label succ with + | 1 | 4 -> true + | _ -> false + ) succs in + List.map (fun e -> G.E.dst e) succs + +let written inst = + match fst (G.V.label inst) with + | Inop -> None + | Iop (op, args, dst) -> Some dst + | Iload (chunk, mode, args, dst) -> Some dst + | Istore (chunk, mode, args, src) -> None + | Icall (sign, id, args, dst) -> failwith "written: call" + | Itailcall (sign, id, args) -> failwith "written: tailcall" + (*| Ialloc (dst, size) -> Some dst*) + | Icond (cond, args) -> None + | Ireturn (res) -> failwith "written: return" + +let fresh_regs n = + let t = Array.make n (BinNums.Coq_xH) in + for i = 0 to (n - 1) do + Array.set t i (!fresh); + fresh := BinPos.Pos.succ !fresh + done; + t + +let print_reg r = Printf.fprintf SPDebug.dc "%i " (P.to_int r) + +let is_cond node = + match fst (G.V.label node) with + | Icond _ -> true + | _ -> false + + +(*******************************************) + +let watch_regs l = List.fold_right (fun (a,b) l -> + if List.mem a l then l else a :: l + ) l [] + +let make_moves = List.map (fun (a,b) -> Iop (Omove,[b],a)) + +let rec repeat l n = + match n with + | 0 -> [] + | n -> l @ repeat l (n-1) + +let fv = ref 0 + +let apply_pipeliner f p ?(debug=false) = + Printf.fprintf SPDebug.dc "******************** NEW FUNCTION ***********************\n"; + let cfg = convert f in + incr fv; + if debug then display cfg.graph ("input" ^ (string_of_int !fv)); + let loops = get_loops cfg in + Printf.fprintf SPDebug.dc "Loops: %d\n" (List.length loops); + let ddgs = List.map (fun (qqch,loop) -> (loop,build_inter_dependency_graph loop)) loops in + + let lv = ref 0 in + + let graph = List.fold_right (fun (loop,ddg) graph -> + Printf.fprintf SPDebug.dc "__________________ NEW LOOP ____________________\n"; + Printf.printf "Pipelinable loop: "; + incr lv; + fresh := (BinPos.Pos.succ + (BinPos.Pos.succ + (BinPos.Pos.succ + (BinPos.Pos.succ + (BinPos.Pos.succ + (max_reg_of_graph graph (to_caml_list f.fn_params) + )))))); + Printf.fprintf SPDebug.dc "FRESH = %i \n" + (P.to_int !fresh); + match p ddg with + | Some pipe -> + Printf.printf "Rock On ! Min = %i - Unroll = %i\n" pipe.min pipe.unrolling; + let p = (make_moves pipe.ramp_up) @ (delete_indexes pipe.prolog) in + let e = (delete_indexes pipe.epilog) @ (make_moves pipe.ramp_down) in + let b = delete_indexes (List.tl (List.rev loop)) in + let bt = (List.tl (delete_indexes pipe.steady_state)) in + let cond1 = fst (G.V.label (List.hd (List.rev loop))) in + let cond2 = (List.hd (delete_indexes pipe.steady_state)) in + + let bu = symbolic_evaluation (repeat b (pipe.min + 1)) in + let pe = symbolic_evaluation (p @ e) in + let bte = symbolic_evaluation (bt @ e) in + let ebu = symbolic_evaluation (e @ repeat b pipe.unrolling) in + let regs = watch_regs pipe.ramp_down in + let c1 = symbolic_condition cond1 (repeat b pipe.unrolling) in + let d1 = symbolic_condition cond1 (repeat b (pipe.min + 1)) in + (*let c2 = symbolic_condition cond2 p in + let d2 = symbolic_condition cond2 ((make_moves pipe.ramp_up) @ bt) in*) + + + + let sbt = symbolic_evaluation (bt) in + let sep = symbolic_evaluation (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) in (* er @ pr *) + + Printf.printf "Initialisation : %s \n" + (if symbolic_equivalence bu pe regs then "OK" else "FAIL"); + Printf.printf "Etat stable : %s \n" + (if symbolic_equivalence bte ebu regs then "OK" else "FAIL"); + Printf.printf "Egalite fondamentale : %s \n" + (if symbolic_equivalence sbt sep (watch_regs pipe.ramp_up) then "OK" else "FAIL"); + (* Printf.printf "Condition initiale : %s \n" + (if c1 = c2 then "OK" else "FAIL"); + Printf.printf "Condition stable : %s \n" + (if d1 = d2 then "OK" else "FAIL"); + + + Printf.fprintf SPDebug.dc "pbte\n";*) + List.iter (fun e -> + Printf.fprintf SPDebug.dc "%s\n" + (string_of_node (G.V.create (e,0))) + ) (p @ bt @ e); + Printf.fprintf SPDebug.dc "bu\n"; + List.iter (fun e -> Printf.fprintf SPDebug.dc "%s\n" + (string_of_node (G.V.create (e,0))) + ) (repeat b (pipe.unrolling + pipe.min)); + + + + if debug then + display_st ("pbte"^ (string_of_int !fv) ^ (string_of_int !lv)) (p @ bt @ e) (watch_regs pipe.ramp_down); + if debug then + display_st ("bu"^ (string_of_int !fv) ^ (string_of_int !lv)) (repeat b (pipe.min + pipe.unrolling)) (watch_regs pipe.ramp_down); + + if debug then display_st ("bt"^ (string_of_int !fv) ^ (string_of_int !lv)) (bt) (watch_regs pipe.ramp_up); + if debug then display_st ("ep"^ (string_of_int !fv) ^ (string_of_int !lv)) (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) (watch_regs pipe.ramp_up); + + substitute_pipeline graph loop + (delete_indexes pipe.steady_state) (delete_indexes pipe.prolog) + (delete_indexes pipe.epilog) (pipe.min + pipe.unrolling) + pipe.unrolling pipe.ramp_up + pipe.ramp_down + (to_caml_list f.fn_params) + | None -> Printf.printf "Damn It ! \n"; graph + ) ddgs cfg.graph in + + if debug then display graph ("output"^ (string_of_int !fv)); + let tg = convert_back graph in + + let tg_to_type = {fn_sig = f.fn_sig; + fn_params = f.fn_params; + fn_stacksize = f.fn_stacksize; + fn_code = tg; + fn_entrypoint = f.fn_entrypoint; + (*fn_nextpc = P.of_int ((get_nextpc (graph)))*) + } in + (*SPTyping.type_function tg_to_type;*) + + tg_to_type |