Rename pipelining

1 files changed, 0 insertions, 819 deletions

diff --git a/src/SoftwarePipelining/SPBasic.ml b/src/SoftwarePipelining/SPBasic.ml
deleted file mode 100644
index 32234b8..0000000
--- a/src/SoftwarePipelining/SPBasic.ml
+++ /dev/null
@@ -1,819 +0,0 @@
-(***********************************************************************)
- (*                                                                     *)
-(*                        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