Fix whitespace

6 files changed, 748 insertions, 752 deletions

diff --git a/src/SoftwarePipelining/SPBasic.ml b/src/SoftwarePipelining/SPBasic.ml
index 1269faf..dd2b5c1 100644
--- a/src/SoftwarePipelining/SPBasic.ml
+++ b/src/SoftwarePipelining/SPBasic.ml
@@ -23,8 +23,8 @@ 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)
+    (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)
@@ -37,7 +37,7 @@ let string_of_instruction node =
   | (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) *)
+  (*  | (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
 
@@ -66,7 +66,7 @@ let display g name =
   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*)
@@ -79,58 +79,58 @@ let convert f  =
   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) 
+      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"
-	 
+    | [] -> 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
+      link key (match Maps.PTree.get key succ with
             Some x -> x | _ -> failwith "Could not index") g
-			      ) f.fn_code graph
+    ) 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
-
- 
-  
+
+  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 =
@@ -142,16 +142,16 @@ let dominator_tree f =
 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
+    | 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 []
+      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))
@@ -167,43 +167,43 @@ let print_instruction node =
   (*| (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"
+  | 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
+      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
+    | Icall _ | Itailcall _ | Ireturn _ | Icond _ (*| Ialloc _*) | Iop ((Ocmp _),_,_)-> false
+    | _ -> true
   in
-	  
+
   let is_branching node = 
     match fst (G.V.label node) with
-      | Icond _ -> true
-      | _ -> false
+    | Icond _ -> true
+    | _ -> false
   in
 
   let is_nop node = 
     match fst (G.V.label node) with
-      | Inop -> true
-      | _ -> false
+    | Inop -> true
+    | _ -> false
   in
 
   let is_OK_aux l =
@@ -212,160 +212,160 @@ let is_pipelinable loop = (* true if loop is innermost and without control *)
 
   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
+    | (Icond (cond, args),n) ->
+      let args = to_caml_list args in
+      begin
+        match args with
+        | [] -> false
+        | r :: [] -> not (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
- 
+  | 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
- 
+              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
+  | Not_found -> None
 
 let rec to_res l = 
   match l with
-    | [] -> []
-    | e :: l -> Reg e :: to_res l
+  | [] -> []
+  | 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"
-    
+  | 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"
- 
+  | 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
+    | [] -> (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
+    | [] -> 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 *)
@@ -390,7 +390,7 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
   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
@@ -400,11 +400,11 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
   (* 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
@@ -426,56 +426,56 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
   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 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
+    | 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 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
+      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 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 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 *)
 
@@ -494,7 +494,7 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
   let graph = G.add_edge graph n6 entry in
 
   graph
-       
+
 let regs_of_node node = 
   match G.V.label node with
   | (Inop,n) -> []
@@ -510,45 +510,45 @@ let regs_of_node node =
 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
+      (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 "%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
-	    | 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" 
+  | (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
+      | 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
+       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
@@ -562,7 +562,7 @@ let substitute_pipeline graph loop steady_state prolog epilog min unrolling ru r
   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
@@ -571,7 +571,7 @@ let get_loops cfg =
   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}
+                 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
 
@@ -581,107 +581,107 @@ let fresh = ref BinNums.Coq_xH
 
 let distance e = 
   match G.E.label e with
-    | 1 | 2 | 3 -> 0
-    | _ -> 1
+  | 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"
+  | 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 -> 3
-	    | Odiv -> 30
-	    | Omulimm _ -> 5
-	    | _ -> 2
-	end
-    | Iload _ -> 10
-(*    | Ialloc _ -> 20*)
-    | _ -> 1
-  
+  | Iop (op,args, dst) ->
+    begin
+      match op with
+      | Omove -> 1
+      (*| Oaddimm _ -> 1*)
+      (*| Oadd -> 2*)
+      | Omul -> 3
+      | Odiv -> 30
+      | Omulimm _ -> 5
+      | _ -> 2
+    end
+  | Iload _ -> 10
+  (*    | 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))
+      | 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)
+  | [] -> []
+  | 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
+  | [] -> 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
+  | 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))
+      | 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
+      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"
+  | 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
@@ -690,27 +690,27 @@ let fresh_regs n =
     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
-    
-  
+  | 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 []
+    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)
+  | 0 -> []
+  | n -> l @ repeat l (n-1)
 
 let fv = ref 0
 
@@ -722,98 +722,98 @@ let apply_pipeliner f p ?(debug=false) =
   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
+      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
+                    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
diff --git a/src/SoftwarePipelining/SPIMS.ml b/src/SoftwarePipelining/SPIMS.ml
index 48e7339..1933268 100644
--- a/src/SoftwarePipelining/SPIMS.ml
+++ b/src/SoftwarePipelining/SPIMS.ml
@@ -18,80 +18,80 @@ module NI = Map.Make (struct type t = G.V.t let compare = compare end)
 let find key map def =
   try NI.find key map 
   with
-    | Not_found -> def
+  | Not_found -> def
 
 let unpack v = 
   match v with
-    | Some v -> v
-    | None -> failwith "unpack abusif"
- 
+  | Some v -> v
+  | None -> failwith "unpack abusif"
+
 let dep_latency edge = 
   match edge_type edge with
-    | IntraRAW | InterRAW -> latency (G.E.src edge)
-    | _ -> 1
+  | IntraRAW | InterRAW -> latency (G.E.src edge)
+  | _ -> 1
 
 let estart ddg schedule node ii =
   let preds = G.pred_e ddg node in
   let starts = List.map (fun edge ->
-			   match find (G.E.src edge) schedule None with
-			     | Some t -> 
-				 let start = t + dep_latency edge - ii * distance edge in
-				 (*Printf.printf "start : %i \n" start;*)
-				 if start < 0 then 0 else start 
-			     | None -> 0
-			) preds in
+      match find (G.E.src edge) schedule None with
+      | Some t ->
+        let start = t + dep_latency edge - ii * distance edge in
+        (*Printf.printf "start : %i \n" start;*)
+        if start < 0 then 0 else start
+      | None -> 0
+    ) preds in
   List.fold_left (fun max e -> if max > e then max else e) 0 starts
-    
+
 let resource_conflict time mrt ii =
   match Array.get mrt (time mod ii) with 
-    | None -> false
-    | Some v -> true
-	 
+  | None -> false
+  | Some v -> true
+
 let rec scan_time time maxtime mrt ii =
-    if time <= maxtime
-    then 
-      begin
-	if resource_conflict time mrt ii
-	then scan_time (time + 1) maxtime mrt ii
-	else Some time
-      end
-    else None
-      
+  if time <= maxtime
+  then
+    begin
+      if resource_conflict time mrt ii
+      then scan_time (time + 1) maxtime mrt ii
+      else Some time
+    end
+  else None
+
 let finished ddg schedule = 
   let unscheduled = G.fold_vertex (fun node l ->
-				     match find node schedule None with
-				       | Some v -> l
-				       | None -> node :: l
-				  ) ddg [] in
+      match find node schedule None with
+      | Some v -> l
+      | None -> node :: l
+    ) ddg [] in
   (* Printf.printf "R %i R \n" (List.length unscheduled); *)
   if List.length unscheduled = 0 then true else false
 
 let bad_successors ddg schedule node ii =
   let succs = G.succ_e ddg node in (* Le succs_ddg initial *) 
-(*   let reftime = NI.find node schedule in *)
-(*   let succs_sched = NI.fold (fun node time succs ->  *)
-(* 			 if time > reftime then node :: succs else succs *)
-(* 		      ) schedule [] in *)
-(*  let succs = List.filter (fun edge -> List.mem (G.E.dst edge) succs_sched) succs_ddg in*)
+  (*   let reftime = NI.find node schedule in *)
+  (*   let succs_sched = NI.fold (fun node time succs ->  *)
+  (*               if time > reftime then node :: succs else succs *)
+  (*                ) schedule [] in *)
+  (*  let succs = List.filter (fun edge -> List.mem (G.E.dst edge) succs_sched) succs_ddg in*)
   List.fold_right (fun edge bad ->
-		     match find (G.E.dst edge) schedule None with
-		       | Some t ->
-			   if unpack (NI.find node schedule) + dep_latency edge - ii * distance edge > t
-			   then (G.E.dst edge) :: bad
-			   else bad
-		       | None -> bad
-		  ) succs []
-    
+      match find (G.E.dst edge) schedule None with
+      | Some t ->
+        if unpack (NI.find node schedule) + dep_latency edge - ii * distance edge > t
+        then (G.E.dst edge) :: bad
+        else bad
+      | None -> bad
+    ) succs []
+
 let get_condition ddg = 
   let cond = G.fold_vertex (fun node cond ->
-			      if is_cond node then Some node else cond
-			   ) ddg None in
+      if is_cond node then Some node else cond
+    ) ddg None in
   match cond with
-    | Some cond -> cond
-    | None -> failwith "The loop does not contain a condition. Aborting\n"
+  | Some cond -> cond
+  | None -> failwith "The loop does not contain a condition. Aborting\n"
 
 let modulo_schedule heightr ddg min_ii max_interval =
-  
+
   let ii = ref (min_ii - 1) in 
   let notfound = ref true in
   let sched = ref NI.empty in
@@ -115,50 +115,50 @@ let modulo_schedule heightr ddg min_ii max_interval =
       (* Printf.printf "tmin (%s) = %i \n" (string_of_node h) mintime; *)
       let maxtime = mintime + !ii -1 in
       let time =  
-	match scan_time mintime maxtime mrt !ii with
-	  | Some t -> t
-	  | None -> (*Printf.printf "backtrack" ; *)
-	      if mintime = 0 then 1 + find h !lasttime 0
-	      else max mintime (1 + find h !lasttime 0)
+        match scan_time mintime maxtime mrt !ii with
+        | Some t -> t
+        | None -> (*Printf.printf "backtrack" ; *)
+          if mintime = 0 then 1 + find h !lasttime 0
+          else max mintime (1 + find h !lasttime 0)
       in
       (* Printf.printf "Chosen time for %s : %i \n" (string_of_node h) time; *)
       schedtime := NI.add h (Some time) !schedtime;
       lasttime := NI.add h time !lasttime; 
-      
+
       let killed = bad_successors ddg !schedtime h !ii in
       List.iter (fun n -> (* Printf.printf "Killing %s" (string_of_node n) ; *)schedtime := NI.add n None !schedtime) killed;
-      
+
       begin
-	match Array.get mrt (time mod !ii) with
-	  | None -> Array.set mrt (time mod !ii) (Some h)
-	  | Some n -> 
-	      begin
-		(*Printf.printf "Deleting : %s \n" (string_of_node n); *)
-		(* Printf.printf "."; *)
-		schedtime := NI.add n None !schedtime;
-		Array.set mrt (time mod !ii) (Some h)
-	      end
+        match Array.get mrt (time mod !ii) with
+        | None -> Array.set mrt (time mod !ii) (Some h)
+        | Some n ->
+          begin
+            (*Printf.printf "Deleting : %s \n" (string_of_node n); *)
+            (* Printf.printf "."; *)
+            schedtime := NI.add n None !schedtime;
+            Array.set mrt (time mod !ii) (Some h)
+          end
       end;
       (* if finished ddg !schedtime then Printf.printf "Fini ! \n" *)
-    
+
     done;
-    
+
     let success = G.fold_vertex (fun node b ->
-				   b &&
-				     match find node !schedtime None with
-				       | Some _ -> true
-				       | None -> false
-				) ddg true in
-    
+        b &&
+        match find node !schedtime None with
+        | Some _ -> true
+        | None -> false
+      ) ddg true in
+
     if success then (notfound := false; sched := !schedtime);
-    
+
   done;
-  
+
   if (not !notfound) 
   then (!sched,!ii)
   else failwith "IMS failure"
-    
-  
+
+
 let res_m_ii ddg =
   G.nb_vertex ddg
 
@@ -166,13 +166,12 @@ let pipeliner ddg heightr =
   let mii = res_m_ii ddg in
   let (schedule,ii) = modulo_schedule heightr ddg mii (10 * mii) in
   (NI.fold (fun n v map -> 
-	     match v with
-	       | Some v -> NI.add n v map
-	       | None -> failwith "pipeliner: schedule unfinished"
-	  ) schedule NI.empty,ii)
+       match v with
+       | Some v -> NI.add n v map
+       | None -> failwith "pipeliner: schedule unfinished"
+     ) schedule NI.empty,ii)
 
 let print_schedule sched =
   NI.iter (fun node time ->
-	      Printf.fprintf SPDebug.dc "%s |---> %i \n" (string_of_node node) time
-	   ) sched
-    
+      Printf.fprintf SPDebug.dc "%s |---> %i \n" (string_of_node node) time
+    ) sched
diff --git a/src/SoftwarePipelining/SPMVE.ml b/src/SoftwarePipelining/SPMVE.ml
index 2eb4929..28381c1 100644
--- a/src/SoftwarePipelining/SPMVE.ml
+++ b/src/SoftwarePipelining/SPMVE.ml
@@ -14,7 +14,7 @@ open SPBasic
 open SPIMS
 
 module Mult = Map.Make (struct type t = reg let compare = compare end)
- 
+
 let size_of_map1 m = 
   NI.fold (fun key v size -> size + 1) m 0
 
@@ -23,36 +23,36 @@ let size_of_map2 m =
 
 let sched_max_time sched = 
   NI.fold (fun node time max ->
-	     if time > max then time else max
-	  ) sched 0 
+      if time > max then time else max
+    ) sched 0
 
 let print_table t s =
   Printf.fprintf SPDebug.dc "%s : \n" s;
   let string_of_node_ev node = 
     match node with
-      | Some node -> string_of_node node
-      | None -> "_"
+    | Some node -> string_of_node node
+    | None -> "_"
   in
   Array.iteri (fun i node -> Printf.fprintf SPDebug.dc "%i :: %s \n" i (string_of_node_ev node)) t
 
 let durations ddg sched ii =
-  
+
   G.fold_vertex (fun node mult ->
-		   match written node with 
-		     | None -> mult
-		     | Some r -> 
-			 let raw_succs = get_succs_raw ddg node in
-			 let durations = List.map (fun succ -> 
-						     let d = NI.find succ sched - NI.find node sched in
-						     if d >= 0 then d 
-						     else ((sched_max_time sched - NI.find node sched) + NI.find succ sched)
-						  ) raw_succs in
-			 let duration = List.fold_left (fun max e -> if max > e then max else e) 0 durations in
-			 Mult.add r ((duration / ii) + 1) mult (* cette division est surement fdausse*)
-		) ddg Mult.empty
+      match written node with
+      | None -> mult
+      | Some r ->
+        let raw_succs = get_succs_raw ddg node in
+        let durations = List.map (fun succ ->
+            let d = NI.find succ sched - NI.find node sched in
+            if d >= 0 then d
+            else ((sched_max_time sched - NI.find node sched) + NI.find succ sched)
+          ) raw_succs in
+        let duration = List.fold_left (fun max e -> if max > e then max else e) 0 durations in
+        Mult.add r ((duration / ii) + 1) mult (* cette division est surement fdausse*)
+    ) ddg Mult.empty
 
 let minimizer qi ur =
-  
+
   let rec fill n = 
     if n <= ur then n :: fill (n + 1) else []
   in
@@ -62,22 +62,22 @@ let minimizer qi ur =
   let l = List.filter (fun e -> snd e = 0) l in
   let l = List.map fst l in
   List.fold_left (fun min e -> if min < e then min else e) ur l
-  
+
 let multiplicity ddg sched ii =
   let qs = durations ddg sched ii in
-(*   Printf.printf "Quantite de variables necessaires : \n"; *)
-(*   Mult.iter (fun key mu -> print_reg key ; Printf.printf " |-> %i\n" mu) qs; *)
+  (*   Printf.printf "Quantite de variables necessaires : \n"; *)
+  (*   Mult.iter (fun key mu -> print_reg key ; Printf.printf " |-> %i\n" mu) qs; *)
   let unroll = Mult.fold (fun reg mult max ->
-			    if mult > max then mult else max
-			 ) qs 0 in
+      if mult > max then mult else max
+    ) qs 0 in
   let mult = Mult.fold (fun reg mult mult -> 
-			 Mult.add reg (minimizer (Mult.find reg qs) unroll) mult 
-		      ) qs Mult.empty 
+      Mult.add reg (minimizer (Mult.find reg qs) unroll) mult
+    ) qs Mult.empty
   in
   (mult,unroll)
- 
+
 let mve_kernel t ddg sched ii mult unroll =
-  
+
   let regs = Array.make ii (fresh_regs 0) in  
   for i = 0 to (ii - 1) do
     let fregs = fresh_regs unroll in
@@ -89,103 +89,103 @@ let mve_kernel t ddg sched ii mult unroll =
   let used_regs = ref [] in
 
   let index r i = Mult.find r mult - ( ((i / ii) + 1) mod Mult.find r mult) in
-(*   let pos i node inst =  *)
-(*     let separation =  *)
-(*       let b= NI.find node sched - NI.find inst sched in *)
-(*       if b >= 0 then b *)
-(*       else ((sched_max_time sched - NI.find inst sched) + NI.find node sched)  *)
-(*     in *)
-(*     (i + separation) mod (ii * unroll) in   *)
+  (*   let pos i node inst =  *)
+  (*     let separation =  *)
+  (*       let b= NI.find node sched - NI.find inst sched in *)
+  (*       if b >= 0 then b *)
+  (*       else ((sched_max_time sched - NI.find inst sched) + NI.find node sched)  *)
+  (*     in *)
+  (*     (i + separation) mod (ii * unroll) in   *)
 
   let new_t = Array.copy t in
 
   for i = 0 to (Array.length t - 1) do
     (* print_table new_t "Nouvelle table"; *)
     match t.(i),new_t.(i) with
-      | Some insti, Some insti_mod ->
-	  begin 
-	    match written insti with
-	      | None -> ()
-	      | Some r -> 
-		  begin
-		    let new_reg = 
-		      if Mult.find r mult = 0 then r 
-		      else regs.(i mod ii).(index r i - 1) in
-		    if (not (List.mem (r,new_reg) !used_regs)) then used_regs := (r,new_reg) :: !used_regs;
-		    let inst = reforge_writes insti_mod new_reg in 
-		    Printf.fprintf SPDebug.dc "Reecriture : %s --> %s \n" (string_of_node insti) (string_of_node inst);
-		    Array.set new_t i (Some inst);
-		    let succs = get_succs_raw ddg insti in 
-		    List.iter (fun node ->
-
-		(* 		 let lifetime =  *)
-(* 				   let d = NI.find node sched - NI.find insti sched in *)
-(* 				   if d >= 0 then d  *)
-(* 				   else ((sched_max_time sched - NI.find insti sched) + 1 + NI.find node sched) *)
-(* 				 in *)
-				 
-
-				 (* ___Version 1___ *)
-				 (* let lifetime = lifetime / ii in *)
-(* 				 let schedtime =  *)
-(* 				   ((NI.find node sched) mod ii) (\* Position dans le premier bloc *\) *)
-(* 				   + (ii * (i / ii))           (\* Commencement du bloc ou on travail *\) *)
-(* 				   + (ii * lifetime )     (\* Decalage (Mult.find r mult - 1)  *\) *)
-(* 				   + ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 0 else 0) * ii) *)
-(* 				 in *)
-
-				 (* Printf.printf "seed = %i - bloc = %i - slide = %i - corr = %i - id = %i \n" *)
-(* 				    ((NI.find node sched) mod ii) *)
-(* 			 	   (ii * (i / ii)) (ii * lifetime) *)
-(* 				 ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 1 else 0 ) * ii)  *)
-(* 				 id; *)
-(* 			 	 Printf.printf "Successeur a traiter : %s ooo %i ooo\n" (string_of_node node) (Mult.find r mult); *)
-
-				 (* ___Version 2___ *)
-	 			 let schedtime = 
-				   if (NI.find node sched > NI.find insti sched)
-				   then i + (NI.find node sched - NI.find insti sched) 
-				   else i - NI.find insti sched + ii + NI.find node sched
-				     (* let delta = NI.find insti sched - NI.find node sched in *)
-(* 				     (i - delta) + (((delta / ii) + 1) * ii) (\* (i - delta) + ii*\) *)
-				 in
-
-				 (*   then  *)
-
-				 Printf.fprintf SPDebug.dc "i = %i - def = %i - use = %i - time = %i \n"
-				   i (NI.find insti sched) (NI.find node sched) schedtime;
-				 
-
- 				 (* let id = pos i node insti in *)
-				 let id = schedtime mod (unroll * ii) (* le tout modulo la tabl *) in
-				 let id = (id + (unroll * ii)) mod (unroll * ii) in 
- 			 	 Printf.fprintf SPDebug.dc "Positions to treat : %i \n" id;
-				 let insttt = match new_t.(id) with
-				   | Some inst -> inst
-				   | None -> failwith "There should be an instruction" 
-				 in
-				 let inst = reforge_reads insttt r new_reg in
-				 Array.set new_t id (Some inst)
-			      ) succs
-		  end
-	  end
-      | None, _ -> ()
-      | _, None -> failwith "MVE : qqch mal compris"
+    | Some insti, Some insti_mod ->
+      begin
+        match written insti with
+        | None -> ()
+        | Some r ->
+          begin
+            let new_reg =
+              if Mult.find r mult = 0 then r
+              else regs.(i mod ii).(index r i - 1) in
+            if (not (List.mem (r,new_reg) !used_regs)) then used_regs := (r,new_reg) :: !used_regs;
+            let inst = reforge_writes insti_mod new_reg in
+            Printf.fprintf SPDebug.dc "Reecriture : %s --> %s \n" (string_of_node insti) (string_of_node inst);
+            Array.set new_t i (Some inst);
+            let succs = get_succs_raw ddg insti in
+            List.iter (fun node ->
+
+                (*           let lifetime =  *)
+                (*                     let d = NI.find node sched - NI.find insti sched in *)
+                (*                     if d >= 0 then d  *)
+                (*                     else ((sched_max_time sched - NI.find insti sched) + 1 + NI.find node sched) *)
+                (*                   in *)
+
+
+                (* ___Version 1___ *)
+                (* let lifetime = lifetime / ii in *)
+                (*                   let schedtime =  *)
+                (*                     ((NI.find node sched) mod ii) (\* Position dans le premier bloc *\) *)
+                (*                     + (ii * (i / ii))           (\* Commencement du bloc ou on travail *\) *)
+                (*                     + (ii * lifetime )     (\* Decalage (Mult.find r mult - 1)  *\) *)
+                (*                     + ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 0 else 0) * ii) *)
+                (*                   in *)
+
+                (* Printf.printf "seed = %i - bloc = %i - slide = %i - corr = %i - id = %i \n" *)
+                (*                      ((NI.find node sched) mod ii) *)
+                (*                     (ii * (i / ii)) (ii * lifetime) *)
+                (*                   ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 1 else 0 ) * ii)  *)
+                (*                   id; *)
+                (*                   Printf.printf "Successeur a traiter : %s ooo %i ooo\n" (string_of_node node) (Mult.find r mult); *)
+
+                (* ___Version 2___ *)
+                let schedtime =
+                  if (NI.find node sched > NI.find insti sched)
+                  then i + (NI.find node sched - NI.find insti sched)
+                  else i - NI.find insti sched + ii + NI.find node sched
+                  (* let delta = NI.find insti sched - NI.find node sched in *)
+                  (*                       (i - delta) + (((delta / ii) + 1) * ii) (\* (i - delta) + ii*\) *)
+                in
+
+                (*   then  *)
+
+                Printf.fprintf SPDebug.dc "i = %i - def = %i - use = %i - time = %i \n"
+                  i (NI.find insti sched) (NI.find node sched) schedtime;
+
+
+                (* let id = pos i node insti in *)
+                let id = schedtime mod (unroll * ii) (* le tout modulo la tabl *) in
+                let id = (id + (unroll * ii)) mod (unroll * ii) in
+                Printf.fprintf SPDebug.dc "Positions to treat : %i \n" id;
+                let insttt = match new_t.(id) with
+                  | Some inst -> inst
+                  | None -> failwith "There should be an instruction"
+                in
+                let inst = reforge_reads insttt r new_reg in
+                Array.set new_t id (Some inst)
+              ) succs
+          end
+      end
+    | None, _ -> ()
+    | _, None -> failwith "MVE : qqch mal compris"
   done;
   new_t,!used_regs
 
 let crunch_and_unroll sched ii ur =
   let steady_s = Array.make ii None in
   NI.iter (fun inst time -> 
-	     Array.set steady_s (time mod ii) (Some inst) 
-	  ) sched;
+      Array.set steady_s (time mod ii) (Some inst)
+    ) sched;
   (* Printf.printf "Etat stable : \n"; *)
-(*   let string_of_node_ev node =  *)
-(*     match node with *)
-(*       | Some node -> string_of_node node *)
-(*       | None -> "_" *)
-(*   in   *)
-(*   Array.iteri (fun i node -> Printf.printf "%i :: %s \n" i (string_of_node_ev node)) steady_s; *)
+  (*   let string_of_node_ev node =  *)
+  (*     match node with *)
+  (*       | Some node -> string_of_node node *)
+  (*       | None -> "_" *)
+  (*   in   *)
+  (*   Array.iteri (fun i node -> Printf.printf "%i :: %s \n" i (string_of_node_ev node)) steady_s; *)
   let steady = Array.make (ii * ur) None in
   for i = 0 to (ur - 1) do
     for time = 0 to (ii - 1) do
@@ -197,27 +197,27 @@ let crunch_and_unroll sched ii ur =
 let compute_iteration_table sched ii =
   let t = Array.make ii None in
   NI.iter (fun node time ->
-	     Array.set t (NI.find node sched mod ii) (Some ((NI.find node sched / ii) + 1))
-	  ) sched;
+      Array.set t (NI.find node sched mod ii) (Some ((NI.find node sched / ii) + 1))
+    ) sched;
   t
 
 let compute_prolog steady min ii unroll schedule it =
- 
+
   let prolog = ref [] in
   let prolog_piece = ref [] in
 
   for i = (min - 1) downto 0 do
-    
+
     let index = ((ii * (unroll - (min - i)))) mod (unroll * ii)  in
     prolog_piece := [];
 
     for j = 0 to (ii - 1) do (* copie du sous tableau *)
       (* Printf.printf "i : %i - j : %i - index : %i \n" i j index; *)
       match steady.(index + j), it.(j) with
-	| Some inst , Some iter ->
-	    if iter <= (i + 1) then prolog_piece := inst :: !prolog_piece; (* i + 1 au lieu de i *)
-	| None, _ -> ()
-	| _, _ -> failwith "compute_prolog: quelquechose est mal compris"
+      | Some inst , Some iter ->
+        if iter <= (i + 1) then prolog_piece := inst :: !prolog_piece; (* i + 1 au lieu de i *)
+      | None, _ -> ()
+      | _, _ -> failwith "compute_prolog: quelquechose est mal compris"
     done;
 
     prolog := List.rev (!prolog_piece) @ !prolog
@@ -227,41 +227,41 @@ let compute_prolog steady min ii unroll schedule it =
 
 
 let compute_epilog steady min ii unroll schedule it = 
- 
+
   let epilog = ref [] in 
 
   for i = 0 to (min - 1) do
     let index = (i mod unroll) * ii in
     for j = 0 to (ii - 1) do 
       match steady.(index + j), it.(j) with
-	| Some inst , Some iter ->
-	    if iter > (i + 1) then epilog := inst :: !epilog;  
-	| None, _ -> ()
-	| _, _ -> failwith "compute_prolog: quelquechose est mal compris"
+      | Some inst , Some iter ->
+        if iter > (i + 1) then epilog := inst :: !epilog;
+      | None, _ -> ()
+      | _, _ -> failwith "compute_prolog: quelquechose est mal compris"
     done;
   done;
   List.rev (!epilog)
-      
+
 let entrance = List.map (fun (a,b) -> (b,a)) 
 
 let way_out prolog epilog used_regs =
   let l = List.rev (prolog @ epilog) in
-  
+
   let rec way_out_rec l wo =
     match l with
-      | [] -> wo
-      | i :: l -> 
-	  begin
-	    match written i with
-	      | Some r -> 
-		  let mov = List.find (fun (a,b) -> r = b) used_regs in
-		  if List.mem mov wo 
-		  then way_out_rec l wo
-		  else way_out_rec l (mov :: wo)
-	      | None -> way_out_rec l wo
-	  end
+    | [] -> wo
+    | i :: l ->
+      begin
+        match written i with
+        | Some r ->
+          let mov = List.find (fun (a,b) -> r = b) used_regs in
+          if List.mem mov wo
+          then way_out_rec l wo
+          else way_out_rec l (mov :: wo)
+        | None -> way_out_rec l wo
+      end
   in
-  
+
   way_out_rec l []
 
 let mve ddg sched ii =
@@ -282,11 +282,11 @@ let mve ddg sched ii =
   let iteration_table = compute_iteration_table sched ii in
   Printf.fprintf SPDebug.dc "Table d'iteration \n";
   Array.iteri (fun i elt ->
-		 match elt with
-		   | Some elt ->
-		       Printf.fprintf SPDebug.dc "%i : %i\n" i elt
-		   | None -> Printf.fprintf SPDebug.dc "%i : _ \n" i
-	      ) iteration_table;
+      match elt with
+      | Some elt ->
+        Printf.fprintf SPDebug.dc "%i : %i\n" i elt
+      | None -> Printf.fprintf SPDebug.dc "%i : _ \n" i
+    ) iteration_table;
   let prolog = compute_prolog steady_state min ii unroll sched iteration_table in
   let prolog = List.filter (fun e -> not (is_cond e)) prolog in
   let epilog = compute_epilog steady_state min ii unroll sched iteration_table in
@@ -297,6 +297,3 @@ let mve ddg sched ii =
   List.iter (fun node -> Printf.fprintf SPDebug.dc "%s \n" (string_of_node node)) epilog;
   let way_out = way_out prolog epilog used_regs in
   (steady_state,prolog,epilog,min - 1,unroll,entrance used_regs, way_out)
-
-
-  
diff --git a/src/SoftwarePipelining/SPSymbolic_evaluation.ml b/src/SoftwarePipelining/SPSymbolic_evaluation.ml
index 450cda7..c99afc8 100644
--- a/src/SoftwarePipelining/SPSymbolic_evaluation.ml
+++ b/src/SoftwarePipelining/SPSymbolic_evaluation.ml
@@ -20,7 +20,7 @@ type symbolic_value =
   | Sreg of reg
   | Sop of operation * symbolic_value list
   | Sload of memory_chunk * addressing * symbolic_value list * symbolic_mem
-      
+
 and symbolic_mem =
   | Smem 
   | Sstore of memory_chunk * addressing * symbolic_value list * symbolic_value * symbolic_mem
@@ -36,34 +36,34 @@ let initial_mem = Smem
 let initial_cons = Cons.empty
 
 exception Not_straight
-  	
+
 let find res st =
   try State.find res st
   with 
-    | Not_found -> Sreg res
+  | Not_found -> Sreg res
 
 let rec get_args st = function
   | [] -> []
   | arg::args -> find arg st :: get_args st args
-      
+
 let rec symbolic_evaluation st sm cs = function
   | [] -> (st,sm,cs)
   | Inop :: l -> symbolic_evaluation st sm cs l
 
   | Iop (Omove, [src], dst) :: l ->
-      symbolic_evaluation (State.add dst (find src st) st) sm cs l      
+    symbolic_evaluation (State.add dst (find src st) st) sm cs l
 
   | Iop (op, args, dst) :: l -> 
-      let sym_val = Sop (op,get_args st args) in
-      symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l
+    let sym_val = Sop (op,get_args st args) in
+    symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l
 
   | Iload (chunk, mode, args, dst) :: l  -> 
-      let sym_val = Sload (chunk, mode, get_args st args, sm) in
-      symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l
+    let sym_val = Sload (chunk, mode, get_args st args, sm) in
+    symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l
 
   | Istore (chunk, mode, args, src) :: l -> 
-      let sym_mem = Sstore (chunk, mode, get_args st args, find src st, sm) in
-      symbolic_evaluation st sym_mem cs l
+    let sym_mem = Sstore (chunk, mode, get_args st args, find src st, sm) in
+    symbolic_evaluation st sym_mem cs l
 
   | _ :: l -> raise Not_straight
 
@@ -83,7 +83,7 @@ let string_of_osv = function
 type ident = int
 
 module S = Graph.Persistent.Digraph.Abstract
-  (struct type t = osv * ident end)
+    (struct type t = osv * ident end)
 
 let name_of_vertex v = 
   let (osv,id) = S.V.label v in
@@ -118,76 +118,76 @@ let counter = ref 0
 let rec convert_sv_rec sv graph = 
   incr counter;
   match sv with
-    | Sreg res ->
-	let node = S.V.create (Oresource (Reg res), !counter) in
-	let graph = S.add_vertex graph node in
-	(graph,node)
-	  
-    | Sop (op, svl) ->
-	let node = S.V.create (Oop op, !counter) in
-	let (graph, node_l) = List.fold_right (fun sv (graph,node_l) ->
-						 let (graph,node) = convert_sv_rec sv graph in
-						 graph, node :: node_l
-					      ) svl (graph,[]) in
-	let graph = S.add_vertex graph node in
-	let graph = List.fold_right (fun n graph ->
-				       S.add_edge graph node n
-				    ) node_l graph in
-	(graph,node)
-	  
-	  
-    | Sload (mc,addr,svl,sm) -> 
-	let node = S.V.create (Oload (mc, addr), !counter) in
-	let (graph, node_l) = List.fold_right (fun sv (graph,node_l) ->
-						 let (graph,node) = convert_sv_rec sv graph in
-						 graph, node :: node_l
-					      ) svl (graph,[]) in
-	let (graph,node_m) = convert_sm_rec sm graph in  
-	let graph = S.add_vertex graph node in
-	let graph = List.fold_right (fun n graph ->
-				       S.add_edge graph node n
-				    ) node_l graph in
-	let graph = S.add_edge graph node node_m in 
-	(graph,node)
-	  	  	  
+  | Sreg res ->
+    let node = S.V.create (Oresource (Reg res), !counter) in
+    let graph = S.add_vertex graph node in
+    (graph,node)
+
+  | Sop (op, svl) ->
+    let node = S.V.create (Oop op, !counter) in
+    let (graph, node_l) = List.fold_right (fun sv (graph,node_l) ->
+        let (graph,node) = convert_sv_rec sv graph in
+        graph, node :: node_l
+      ) svl (graph,[]) in
+    let graph = S.add_vertex graph node in
+    let graph = List.fold_right (fun n graph ->
+        S.add_edge graph node n
+      ) node_l graph in
+    (graph,node)
+
+
+  | Sload (mc,addr,svl,sm) ->
+    let node = S.V.create (Oload (mc, addr), !counter) in
+    let (graph, node_l) = List.fold_right (fun sv (graph,node_l) ->
+        let (graph,node) = convert_sv_rec sv graph in
+        graph, node :: node_l
+      ) svl (graph,[]) in
+    let (graph,node_m) = convert_sm_rec sm graph in
+    let graph = S.add_vertex graph node in
+    let graph = List.fold_right (fun n graph ->
+        S.add_edge graph node n
+      ) node_l graph in
+    let graph = S.add_edge graph node node_m in
+    (graph,node)
+
 and convert_sm_rec sm graph =
   incr counter;
   match sm with 
-    | Smem ->
-	let node = S.V.create (Oresource Mem, !counter) in
-	let graph = S.add_vertex graph node in
-	(graph,node)
-	    
-    | Sstore (mc,addr,svl,sv,sm) ->
-	let node = S.V.create (Ostore (mc, addr), !counter) in
-	let (graph, node_l) = List.fold_right (fun sv (graph,node_l) ->
-						 let (graph,node) = convert_sv_rec sv graph in
-						 graph, node :: node_l
-					      ) svl (graph,[]) in
-	let (graph, n) = convert_sv_rec sv graph in
-	let (graph, node_m) = convert_sm_rec sm graph in
-	let graph = S.add_vertex graph node in
-	let graph = List.fold_right (fun n graph ->
-				       S.add_edge graph node n
-				    ) node_l graph in
-	let graph = S.add_edge graph node n in
-	let graph = S.add_edge graph node node_m in
-	(graph,node)
-	  	  
+  | Smem ->
+    let node = S.V.create (Oresource Mem, !counter) in
+    let graph = S.add_vertex graph node in
+    (graph,node)
+
+  | Sstore (mc,addr,svl,sv,sm) ->
+    let node = S.V.create (Ostore (mc, addr), !counter) in
+    let (graph, node_l) = List.fold_right (fun sv (graph,node_l) ->
+        let (graph,node) = convert_sv_rec sv graph in
+        graph, node :: node_l
+      ) svl (graph,[]) in
+    let (graph, n) = convert_sv_rec sv graph in
+    let (graph, node_m) = convert_sm_rec sm graph in
+    let graph = S.add_vertex graph node in
+    let graph = List.fold_right (fun n graph ->
+        S.add_edge graph node n
+      ) node_l graph in
+    let graph = S.add_edge graph node n in
+    let graph = S.add_edge graph node node_m in
+    (graph,node)
+
 let convert_sv sv = convert_sv_rec sv S.empty
 let convert_sm sm = convert_sm_rec sm S.empty
 
 let convert_sym st sm regs =
   let graph = State.fold (fun res sv g ->
-			    if (not (List.mem res regs)) then g
-			    else 
-			      let (graph,head) = convert_sv sv in
-			      incr counter;
-			      let src = S.V.create (Oresource (Reg res), !counter) in
-			      let graph = S.add_vertex graph src in
-			      let graph = S.add_edge graph src head in
-			      Op.union g graph
-			 ) st S.empty
+      if (not (List.mem res regs)) then g
+      else
+        let (graph,head) = convert_sv sv in
+        incr counter;
+        let src = S.V.create (Oresource (Reg res), !counter) in
+        let graph = S.add_vertex graph src in
+        let graph = S.add_edge graph src head in
+        Op.union g graph
+    ) st S.empty
   in 
   let graph' = 
     let (graph,head) = convert_sm sm in
@@ -198,29 +198,29 @@ let convert_sym st sm regs =
     graph
   in
   Op.union graph graph'
-    
+
 let display_st name l regs =
   let (st,sm,_) = symbolic_evaluation initial_state initial_mem initial_cons l in
   let g = convert_sym st sm regs in
   let addr = SPDebug.name ^ name in
   dot_output_ss g addr  ;
   ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr  ^ ".png ; rm -f " ^ addr ^ ") & ")) (* & *)
-  
+
 
 let symbolic_equivalence (st1,sm1,cs1) (st2,sm2,cs2) regs =
   Printf.printf "|cs1| = %i - |cs2| = %i \n" (Cons.cardinal cs1) (Cons.cardinal cs2);
   (List.fold_right (fun res b ->
-		     find res st1 = find res st2 && b
-		  ) regs true
-  && sm1 = sm2
-  && Cons.equal cs1 cs2)
+       find res st1 = find res st2 && b
+     ) regs true
+   && sm1 = sm2
+   && Cons.equal cs1 cs2)
 
 let symbolic_evaluation = symbolic_evaluation initial_state initial_mem initial_cons
 
 let symbolic_condition i l =
   match i with
-    | Icond (cond,args) ->
-	let args = to_caml_list args in
-	let (st,sm,cs) = symbolic_evaluation l in
-	(cond,List.map (fun r -> find r st) args)
-    | _ -> failwith "Not a condition !\n"  
+  | Icond (cond,args) ->
+    let args = to_caml_list args in
+    let (st,sm,cs) = symbolic_evaluation l in
+    (cond,List.map (fun r -> find r st) args)
+  | _ -> failwith "Not a condition !\n"
diff --git a/src/SoftwarePipelining/SPTyping.ml b/src/SoftwarePipelining/SPTyping.ml
index 16c9b01..9b9c679 100644
--- a/src/SoftwarePipelining/SPTyping.ml
+++ b/src/SoftwarePipelining/SPTyping.ml
@@ -520,7 +520,7 @@ let type_function f =
                  | false -> false with
                      | true -> check_successor f f.fn_entrypoint
                      | false -> false with
-			 | true -> Printf.fprintf SPDebug.dc "The code is well typed\n"
-			 | false -> failwith "Type checking failure\n")
+             | true -> Printf.fprintf SPDebug.dc "The code is well typed\n"
+             | false -> failwith "Type checking failure\n")
     | None -> failwith "Type inference failure\n"
 *)
diff --git a/src/SoftwarePipelining/SoftwarePipelining.ml b/src/SoftwarePipelining/SoftwarePipelining.ml
index 12ab783..fd95134 100644
--- a/src/SoftwarePipelining/SoftwarePipelining.ml
+++ b/src/SoftwarePipelining/SoftwarePipelining.ml
@@ -19,37 +19,37 @@ let clean t =
 
   let rec clean_rec i =
     match i with 
-      | 0 -> []
-      | n -> 
-	  begin
-	    match t.(i - 1) with
-	      | None -> clean_rec (i - 1)
-	      | Some inst -> inst :: clean_rec (i - 1) 
-	  end
+    | 0 -> []
+    | n ->
+      begin
+        match t.(i - 1) with
+        | None -> clean_rec (i - 1)
+        | Some inst -> inst :: clean_rec (i - 1)
+      end
   in
   let l = List.rev (clean_rec (Array.length t)) in
   List.hd l :: (List.filter (fun e -> not (is_cond e)) (List.tl l))
 
 let print_nodes = List.iter (fun n -> Printf.printf "%s \n" (string_of_node n))  
- 
+
 (* random heuristic *)
- 
+
 let find node schedule opt =
   try NI.find node schedule with
-    | Not_found -> opt
+  | Not_found -> opt
 
 let random ddg schedule = 
   let unscheduled = G.fold_vertex (fun node l ->
-				     match find node schedule None with 
-				       | Some v -> l
-				       | None -> node :: l 
-				  ) ddg [] in
+      match find node schedule None with
+      | Some v -> l
+      | None -> node :: l
+    ) ddg [] in
   let bound = List.length unscheduled in 
   Random.self_init (); 
   List.nth unscheduled (Random.int bound)
 
 (* tought heuristics *)
- 
+
 module Topo = Graph.Topological.Make (G)
 module Scc = Graph.Components.Make (G)
 
@@ -63,8 +63,8 @@ let pipeliner ddg =
   if min <= 0 then None 
   else
     Some {steady_state = steady_state; prolog = prolog; epilog = epilog; min = min; unrolling = unroll;
-	 ramp_up = entrance; ramp_down = way_out}
-      
+          ramp_up = entrance; ramp_down = way_out}
+
 
 let pipeline f =
-  SPBasic.apply_pipeliner f pipeliner ~debug:true
+  SPBasic.apply_pipeliner f pipeliner ~debug:false