Modify software pipelining for build

12 files changed, 198 insertions, 247 deletions

diff --git a/src/SoftwarePipelining/SPBase_types.ml b/src/SoftwarePipelining/SPBase_types.ml
index 3e339c3..ba92340 100644
--- a/src/SoftwarePipelining/SPBase_types.ml
+++ b/src/SoftwarePipelining/SPBase_types.ml
@@ -13,6 +13,7 @@
 open Camlcoq
 open Op
 open Registers
+open Memory
 open Mem
 open AST
 
@@ -20,14 +21,13 @@ type ('a,'b) sum = ('a,'b) Datatypes.sum
 
 type instruction =
   | Inop 
-  | Iop of operation * reg CList.list * reg 
-  | Iload of memory_chunk * addressing * reg CList.list * reg 
-  | Istore of memory_chunk * addressing * reg CList.list * reg 
-  | Icall of signature * (reg, ident) sum * reg CList.list * reg 
-  | Itailcall of signature * (reg, ident) sum * reg CList.list
-  | Ialloc of reg * reg 
-  | Icond of condition * reg CList.list 
-  | Ireturn of reg Datatypes.option
+  | Iop of operation * reg list * reg
+  | Iload of memory_chunk * addressing * reg list * reg
+  | Istore of memory_chunk * addressing * reg list * reg
+  | Icall of signature * (reg, ident) sum * reg list * reg
+  | Itailcall of signature * (reg, ident) sum * reg list
+  | Icond of condition * reg list
+  | Ireturn of reg option
 
 type resource = Reg of reg | Mem
 
@@ -38,8 +38,7 @@ let inst_coq_to_caml = function
   | RTL.Istore (chunk, mode, args, src, succ) -> Istore (chunk, mode, args, src)
   | RTL.Icall (sign, id, args, dst, succ) -> Icall (sign, id, args, dst)
   | RTL.Itailcall (sign, id, args) -> Itailcall (sign, id, args)
-  | RTL.Ialloc (dst, size, succ) -> Ialloc (dst, size)
-  | RTL.Icond (cond, args, succ1, succ2) -> Icond (cond, args)  
+  | RTL.Icond (cond, args, succ1, succ2) -> Icond (cond, args)
   | RTL.Ireturn (res) -> Ireturn (res)
  
 let inst_caml_to_coq i (links : RTL.node list) =
@@ -50,23 +49,22 @@ let inst_caml_to_coq i (links : RTL.node list) =
   | Istore (chunk, mode, args, src),[p] -> RTL.Istore (chunk, mode, args, src,p)  
   | Icall (sign, id, args, dst),[p] -> RTL.Icall (sign, id, args, dst,p) 
   | Itailcall (sign, id, args),[] -> RTL.Itailcall (sign, id, args) 
-  | Ialloc (dst, size),[p] -> RTL.Ialloc (dst, size,p) 
-  | Icond (cond, args),[p1;p2] -> RTL.Icond (cond,args,p1,p2)  
+  | Icond (cond, args),[p1;p2] -> RTL.Icond (cond,args,p1,p2)
   | Ireturn (res),[] -> RTL.Ireturn res 
   | _,_ -> failwith "Echec lors de la conversion des instrucitons internes vers compcert"
 
 
 let print_inst node = string_of_int (snd node)
 
-let to_int = fun n -> Int32.to_int (camlint_of_positive n)
-let to_binpos = fun n -> positive_of_camlint (Int32.of_int n)
+let to_int = fun n -> P.to_int n
+let to_binpos = fun n -> P.of_int n
 
 let rec string_of_args args =
   match args with
-    | CList.Coq_nil -> ""
-    | CList.Coq_cons (arg,args) -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args  
+    | [] -> ""
+    | arg :: args -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args
 
-let string_of_z z = string_of_int (Int32.to_int (Camlcoq.camlint_of_z z))
+let string_of_z z = string_of_int (Z.to_int z)
 
 let string_of_comparison = function
   | Integers.Ceq -> "eq"
@@ -89,17 +87,12 @@ let string_of_cond = function
 let string_of_op = function
   | Omove -> "move"
   | Ointconst i -> Printf.sprintf "intconst %s" (string_of_z i)
-  | Ofloatconst f -> Printf.sprintf "floatconst %s" (string_of_float f)  
-  | Oaddrsymbol (id,i) -> Printf.sprintf "addrsymbol %s %s" (string_of_int (to_int id)) (string_of_z i)
-  | Oaddrstack i -> Printf.sprintf "addrstack %s" (string_of_z i)
+  | Ofloatconst f -> Printf.sprintf "floatconst %s" (string_of_float (camlfloat_of_coqfloat32 f))
   | Ocast8signed -> "cast8signed"
   | Ocast8unsigned -> "cast8unsigned"
   | Ocast16signed -> "cast16signed"
   | Ocast16unsigned -> "cast16unsigned"
-  | Oadd -> "add"
-  | Oaddimm i -> Printf.sprintf "addimm %s" (string_of_z i)
   | Osub -> "sub"
-  | Osubimm i -> Printf.sprintf "subimm %s" (string_of_z i)
   | Omul -> "mul"
   | Omulimm i -> Printf.sprintf "mulimm %s" (string_of_z i)
   | Odiv -> "div"
@@ -110,34 +103,26 @@ let string_of_op = function
   | Oorimm i -> Printf.sprintf "orimm %s" (string_of_z i)
   | Oxor -> "xor"
   | Oxorimm i -> Printf.sprintf "xorimm %s" (string_of_z i)
-  | Onand -> "nand"
-  | Onor -> "nor"
-  | Onxor -> "nxor" 
   | Oshl -> "shl"
   | Oshr -> "shr"
   | Oshrimm i -> Printf.sprintf "shrimm %s" (string_of_z i)
   | Oshrximm i -> Printf.sprintf "shrximm %s" (string_of_z i)
   | Oshru -> "shru"
-  | Orolm (i,j) -> Printf.sprintf "rolm %s %s" (string_of_z i) (string_of_z j)
   | Onegf -> "negf"
   | Oabsf -> "absf"
   | Oaddf -> "addf"
   | Osubf -> "subf"
   | Omulf -> "mulf"
   | Odivf -> "divf"
-  | Omuladdf -> "muladdf"
-  | Omulsubf -> "mulsubf"
   | Osingleoffloat -> "singleoffloat"
-  | Ointoffloat -> "intoffloat"
-  | Ointuoffloat -> "intuoffloat"
   | Ofloatofint -> "floatofint"
-  | Ofloatofintu -> "floatofintu"
-  | Ocmp c -> Printf.sprintf "cmpcmpcmp" 
+  | Ocmp c -> Printf.sprintf "cmpcmpcmp"
+  | Olea _ -> "lea"
   
-let rec to_coq_list = function
-  | [] -> CList.Coq_nil
-  | e :: l -> CList.Coq_cons (e,(to_coq_list l))
+let to_coq_list = function
+  | [] -> []
+  | e :: l -> e :: l
 
-let rec to_caml_list = function
-  | CList.Coq_nil -> []
-  | CList.Coq_cons (e,l) -> e :: to_caml_list l 
+let to_caml_list = function
+  | [] -> []
+  | e :: l -> e :: l
diff --git a/src/SoftwarePipelining/SPBasic.ml b/src/SoftwarePipelining/SPBasic.ml
index b070e3c..1269faf 100644
--- a/src/SoftwarePipelining/SPBasic.ml
+++ b/src/SoftwarePipelining/SPBasic.ml
@@ -10,22 +10,23 @@
 (***********************************************************************)
 
 
-open Lengauer
 open RTL
 open Camlcoq
 open Graph.Pack.Digraph
 open Op
 open Registers
+open Memory
 open Mem
 open AST
-open Base_types
-open Symbolic_evaluation
+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 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 =
@@ -36,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
 
@@ -60,7 +61,7 @@ let dot_output g f =
   close_out oc
 
 let display g name =
-  let addr = Debug.name ^ name in
+  let addr = SPDebug.name ^ name in
   dot_output g addr  ;
   ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr  ^ ".png ; rm -f " ^ addr ^ ") & "))
 
@@ -68,7 +69,6 @@ let display g name =
  
 type cfg = {graph : G.t; start : G.V.t}
 
-
 (* convert traduit un graphe RTL compcert en un graphe RTL ocamlgraph*)
 
 let convert f  = 
@@ -84,13 +84,13 @@ let convert f  =
 		      ) f.fn_code (G.empty,Index.empty) 
   in
 
-  let succ = RTL.successors f in
+  let succ = RTL.successors_map f in
   let rec link n succs g =
     match succs with
-      | CList.Coq_nil -> g
-      | CList.Coq_cons (pos,CList.Coq_nil) -> 
+      | [] -> g
+      | pos::[] ->
 	  G.add_edge g (Index.find (to_int n) index) (Index.find (to_int pos) index)
-      | CList.Coq_cons (pos1, (CList.Coq_cons (pos2,CList.Coq_nil))) ->
+      | 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"
@@ -98,7 +98,8 @@ let convert f  =
   in
 
   let graph = Maps.PTree.fold ( fun g key inst ->
-				  link key (succ key) g
+				  link key (match Maps.PTree.get key succ with
+            Some x -> x | _ -> failwith "Could not index") g
 			      ) f.fn_code graph
   in
   
@@ -131,39 +132,19 @@ let convert_back g =
  
   
 
-(* dominator_tree calcule l arbre de domination grace au code de FP *)
+(* dominator_tree calcule l'arbre de domination grace au code de FP *)
 let dominator_tree f =
-    
-  let module X =
-    struct 
-      type node = G.V.t
-      let n = G.nb_vertex f.graph 
-      let index (node : G.V.t) = snd(G.V.label node) - 1
-      let successors fu n =
-	List.iter fu (G.succ f.graph n) 
-      let predecessors fu n = 
-	List.iter fu (G.pred f.graph n)
-      let start = f.start 
-    end
-  in 
-
-  let module Y = Lengauer.Run (X) 
-
-  in 
- 
-  Y.dominator
- 
+  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 dominates v2 *)
+  let rec is_dominating v1 v2 l = (* does v1 dominate v2 *)
     match dom_tree v2 with
-      | None -> None
-      | Some v -> if v1 = v then Some (v :: l) else is_dominating v1 v (v :: l)
+      | 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 -> 
@@ -171,7 +152,7 @@ let detect_loops graph dom_tree =
 		    | None -> loops
 		    | Some loop -> (v2,loop) :: loops
 	       ) graph []
-    
+
 let print_index node =
   Printf.printf "%i " (snd (G.V.label node))
 
@@ -183,7 +164,7 @@ let print_instruction node =
   | (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  
+  (*| (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   
  
@@ -195,7 +176,7 @@ let is_rewritten node r =
     | 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
+(*    | 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"
 
@@ -209,7 +190,7 @@ 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
+      | Icall _ | Itailcall _ | Ireturn _ | Icond _ (*| Ialloc _*) | Iop ((Ocmp _),_,_)-> false
       | _ -> true
   in
 	  
@@ -236,7 +217,7 @@ let is_pipelinable loop = (* true if loop is innermost and without control *)
 	  begin
 	    match args with 
 	      | [] -> false
-	      | r :: [] -> not (is_variant r loop) 
+	      | r :: [] -> is_variant r loop (* used to be not *)
 	      | r1 :: r2 :: [] ->
 		  begin
 		    match is_variant r1 loop, is_variant r2 loop with
@@ -250,8 +231,12 @@ let is_pipelinable loop = (* true if loop is innermost and without control *)
       | _ -> false
   in
 
-  match loop with
-    | v1 :: v2 :: l -> is_nop v1 && is_branching v2 && is_OK_aux l && is_bounded v2 loop
+  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 = 
@@ -275,8 +260,8 @@ let map_get key map =
 
 let rec to_res l = 
   match l with
-    | CList.Coq_nil -> []
-    | CList.Coq_cons (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
@@ -286,7 +271,7 @@ let resources_reads_of node =
     | 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] 
+    (*| Ialloc (dst, size) -> [Mem] *)
     | Icond (cond, args) -> to_res args
     | Ireturn (res) -> failwith "Resource read of return"
     
@@ -298,7 +283,7 @@ let resources_writes_of node =
     | 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]
+    (*| Ialloc (dst, size) -> (Reg dst) :: [Mem]*)
     | Icond (cond, args) -> []
     | Ireturn (res) -> failwith "Resource read of return"
  
@@ -429,7 +414,7 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
   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 ((Oaddimm (Camlcoq.z_of_camlint (Int32.of_int (-1)))),to_coq_list [r3],bound),next_pc) in (* retouchee, [r3],bound *)
+  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
@@ -478,7 +463,7 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
   let next_pc = next_pc + 1 in
   
   (* 7. Creation du ramp up *)
-  let ramp_up = List.map (fun (a,b) -> Iop (Omove,CList.Coq_cons (b,CList.Coq_nil),a)) ramp_up in
+  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)
@@ -486,7 +471,7 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
 
   let next_pc = next_pc + 1 in
 
-  let ramp_down = List.map (fun (a,b) -> Iop (Omove,CList.Coq_cons (b,CList.Coq_nil),a)) ramp_down 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)
@@ -501,7 +486,6 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog
   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
@@ -519,25 +503,25 @@ let regs_of_node node =
   | (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]
+  (*| (Ialloc (dst, size),n) -> [dst]*)
   | (Icond (cond, args),n) -> (to_caml_list args)
-  | (Ireturn (res),n) -> match res with Datatypes.Some res -> [res] | _ -> [] 
+  | (Ireturn (res),n) -> match res with Some res -> [res] | _ -> []
 
 let max_reg_of_graph graph params =
-  Printf.fprintf Debug.dc "Calcul du registre de depart.\n";
+  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 Debug.dc "%i " (Int32.to_int (Camlcoq.camlint_of_positive reg));
-				   if Int32.compare (Camlcoq.camlint_of_positive reg) max > 0 
-				   then (Camlcoq.camlint_of_positive reg)
+				   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 Debug.dc "MAX REG = %i\n" (Int32.to_int max_reg);
-  BinPos.coq_Psucc (Camlcoq.positive_of_camlint max_reg)
+  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
@@ -546,7 +530,7 @@ let get_bound node loop =
 	begin
 	  match args with 
 	    | [] -> failwith "get_bound: condition sans variables"
-	    | r :: [] -> if is_variant r loop then failwith "Pas de borene dans la boucle" else r
+	    | 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
@@ -568,20 +552,21 @@ let get_nextpc graph =
 
 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.coq_Psucc n1) in
-  let n3 = (BinPos.coq_Psucc n2) in
-  let n4 = (BinPos.coq_Psucc n3) 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 (List.hd (List.tl loop)) loop) in
-  let min = (Camlcoq.z_of_camlint (Int32.of_int min)) in
-  let unrolling = (Camlcoq.z_of_camlint (Int32.of_int unrolling)) 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 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
 
@@ -592,7 +577,7 @@ let delete_indexes l = List.map (fun e -> fst (G.V.label e) ) l
 
 type reg = Registers.reg 
 
-let fresh = ref BinPos.Coq_xH
+let fresh = ref BinNums.Coq_xH
 
 let distance e = 
   match G.E.label e with
@@ -617,15 +602,15 @@ let latency n = (* A raffiner *)
 	begin
 	  match op with
 	    | Omove -> 1
-	    | Oaddimm _ -> 1
-	    | Oadd -> 2
-	    | Omul -> 3 
+	    (*| Oaddimm _ -> 1*)
+	    (*| Oadd -> 2*)
+	    | Omul -> 3
 	    | Odiv -> 30
 	    | Omulimm _ -> 5
 	    | _ -> 2
 	end
     | Iload _ -> 10
-    | Ialloc _ -> 20
+(*    | Ialloc _ -> 20*)
     | _ -> 1
   
 let reforge_writes inst r = 
@@ -636,20 +621,20 @@ let reforge_writes inst 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)
+(*    | 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
-    | CList.Coq_nil -> CList.Coq_nil
-    | CList.Coq_cons (e,l) -> CList.Coq_cons ((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
-    | CList.Coq_nil -> false
-    | CList.Coq_cons (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
@@ -659,7 +644,7 @@ let check_read_exists inst 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
+    (*| Ialloc (dst, size) -> false*)
     | Icond (cond, args) -> mem_args args r
     | Ireturn (res) -> false
 
@@ -672,7 +657,7 @@ let reforge_reads inst oldr newr  =
     | 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)
+    (*| 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))
@@ -694,19 +679,19 @@ let written inst =
     | 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
+    (*| Ialloc (dst, size) -> Some dst*)
     | Icond (cond, args) -> None
     | Ireturn (res) -> failwith "written: return"
 
 let fresh_regs n =
-  let t = Array.make n (BinPos.Coq_xH) in
+  let t = Array.make n (BinNums.Coq_xH) in
   for i = 0 to (n - 1) do
     Array.set t i (!fresh);
-    fresh := BinPos.coq_Psucc !fresh 
+    fresh := BinPos.Pos.succ !fresh
   done;
   t
   
-let print_reg r = Printf.fprintf Debug.dc "%i " (Int32.to_int (Camlcoq.camlint_of_positive r))
+let print_reg r = Printf.fprintf SPDebug.dc "%i " (P.to_int r)
 
 let is_cond node =
   match fst (G.V.label node) with
@@ -720,7 +705,7 @@ 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,CList.Coq_cons (b,CList.Coq_nil),a))
+let make_moves = List.map (fun (a,b) -> Iop (Omove,[b],a))
 
 let rec repeat l n =
   match n with
@@ -730,38 +715,38 @@ let rec repeat l n =
 let fv = ref 0
 
 let apply_pipeliner f p ?(debug=false) = 
-  Printf.fprintf Debug.dc "******************** NEW FUNCTION ***********************\n";
+  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 Debug.dc "__________________ NEW LOOP ____________________\n";
+				 Printf.fprintf SPDebug.dc "__________________ NEW LOOP ____________________\n";
 				 Printf.printf "Pipelinable loop: ";
 				 incr lv;
-				 fresh := (BinPos.coq_Psucc 
-					     (BinPos.coq_Psucc 
-						(BinPos.coq_Psucc 
-						   (BinPos.coq_Psucc 
-						      (BinPos.coq_Psucc 
+				 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 Debug.dc "FRESH = %i \n" 
-				   (Int32.to_int (Camlcoq.camlint_of_positive !fresh));
+				 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.tl loop)) 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.tl loop))) 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
@@ -770,8 +755,8 @@ let apply_pipeliner f p ?(debug=false) =
 				       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 c2 = symbolic_condition cond2 p in
+				       let d2 = symbolic_condition cond2 ((make_moves pipe.ramp_up) @ bt) in*)
     
 				       
 
@@ -784,19 +769,19 @@ let apply_pipeliner f p ?(debug=false) =
 					 (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"
+				     (*  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 Debug.dc "pbte\n";
+				       Printf.fprintf SPDebug.dc "pbte\n";*)
 				       List.iter (fun e -> 
-						    Printf.fprintf Debug.dc "%s\n" 
+						    Printf.fprintf SPDebug.dc "%s\n"
 						      (string_of_node (G.V.create (e,0)))
 						 ) (p @ bt @ e);
-				       Printf.fprintf Debug.dc "bu\n";
-				       List.iter (fun e -> Printf.fprintf Debug.dc "%s\n" 
+				       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));
 
@@ -827,8 +812,8 @@ let apply_pipeliner f p ?(debug=false) =
 		    fn_stacksize = f.fn_stacksize;
 		    fn_code = tg; 
 		    fn_entrypoint = f.fn_entrypoint; 
-		    fn_nextpc = Camlcoq.positive_of_camlint (Int32.of_int (get_nextpc (graph)))
+		    (*fn_nextpc = P.of_int ((get_nextpc (graph)))*)
 		   } in
-  Typing.type_function tg_to_type;
+  (*SPTyping.type_function tg_to_type;*)
 
-  tg
+  tg_to_type
diff --git a/src/SoftwarePipelining/SPBasic.mli b/src/SoftwarePipelining/SPBasic.mli
index 03b3a97..f16e524 100644
--- a/src/SoftwarePipelining/SPBasic.mli
+++ b/src/SoftwarePipelining/SPBasic.mli
@@ -32,7 +32,7 @@ type pipeline = {
 (* Operations on ddg *)
 
 val display : G.t -> string -> unit
-val apply_pipeliner : RTL.coq_function -> (G.t -> pipeline option) -> ?debug:bool -> RTL.code
+val apply_pipeliner : RTL.coq_function -> (G.t -> pipeline option) -> ?debug:bool -> RTL.coq_function
 val get_succs_raw : G.t -> G.V.t -> G.V.t list
 
 (* Operations on instructions, the nodes of the data dependency graph *)
@@ -55,13 +55,3 @@ val distance : G.E.t -> int
 
 val fresh_regs : int -> reg array 
 val print_reg : reg -> unit
-
-
-
-
-
-
-
-
-
-
diff --git a/src/SoftwarePipelining/SPDebug.ml b/src/SoftwarePipelining/SPDebug.ml
index b2ea257..34d1c0c 100644
--- a/src/SoftwarePipelining/SPDebug.ml
+++ b/src/SoftwarePipelining/SPDebug.ml
@@ -13,13 +13,9 @@
 open Unix
 
 let tm = localtime (time ());;
-let name = "../tmp/" ^ (string_of_int tm.tm_year) ^ "-" ^(string_of_int tm.tm_mon) ^ "-" ^(string_of_int tm.tm_mday) ^ 
+let name = "debug/" ^ (string_of_int tm.tm_year) ^ "-" ^(string_of_int tm.tm_mon) ^ "-" ^(string_of_int tm.tm_mday) ^
   "-" ^(string_of_int tm.tm_hour) ^"-" ^(string_of_int tm.tm_min) ^ "-" ^(string_of_int tm.tm_sec) ^ "/";;
 mkdir name 0o777;;
 Printf.printf "Debug informations: %s \n" name  ;;
 let dc = open_out (name ^ "debug.log");;   
 let () = at_exit(fun () -> close_out dc);;
-
-
-
-  
diff --git a/src/SoftwarePipelining/SPIMS.ml b/src/SoftwarePipelining/SPIMS.ml
index a31f3d2..48e7339 100644
--- a/src/SoftwarePipelining/SPIMS.ml
+++ b/src/SoftwarePipelining/SPIMS.ml
@@ -11,7 +11,7 @@
 
 
 open Graph.Pack.Digraph
-open Basic
+open SPBasic
 
 module NI = Map.Make (struct type t = G.V.t let compare = compare end)
 
@@ -173,6 +173,6 @@ let pipeliner ddg heightr =
 
 let print_schedule sched =
   NI.iter (fun node time ->
-	      Printf.fprintf Debug.dc "%s |---> %i \n" (string_of_node node) time
+	      Printf.fprintf SPDebug.dc "%s |---> %i \n" (string_of_node node) time
 	   ) sched
     
diff --git a/src/SoftwarePipelining/SPIMS.mli b/src/SoftwarePipelining/SPIMS.mli
index bcd9ede..7c1d9a7 100644
--- a/src/SoftwarePipelining/SPIMS.mli
+++ b/src/SoftwarePipelining/SPIMS.mli
@@ -11,9 +11,9 @@
 
 
 open Graph.Pack.Digraph
-open Basic
+open SPBasic
 
-module NI : Map.S with type key = Basic.G.V.t 
+module NI : Map.S with type key = SPBasic.G.V.t
 
 (* piepeliner takes a data dependency graph and returns a schedule with an initiation interval
    fails if cannot find any schedule *)
diff --git a/src/SoftwarePipelining/SPMVE.ml b/src/SoftwarePipelining/SPMVE.ml
index a4efb49..2eb4929 100644
--- a/src/SoftwarePipelining/SPMVE.ml
+++ b/src/SoftwarePipelining/SPMVE.ml
@@ -10,8 +10,8 @@
 (***********************************************************************)
 
 
-open Basic
-open IMS
+open SPBasic
+open SPIMS
 
 module Mult = Map.Make (struct type t = reg let compare = compare end)
  
@@ -27,13 +27,13 @@ let sched_max_time sched =
 	  ) sched 0 
 
 let print_table t s =
-  Printf.fprintf Debug.dc "%s : \n" s;
+  Printf.fprintf SPDebug.dc "%s : \n" s;
   let string_of_node_ev node = 
     match node with
       | Some node -> string_of_node node
       | None -> "_"
   in
-  Array.iteri (fun i node -> Printf.fprintf Debug.dc "%i :: %s \n" i (string_of_node_ev node)) t
+  Array.iteri (fun i node -> Printf.fprintf SPDebug.dc "%i :: %s \n" i (string_of_node_ev node)) t
 
 let durations ddg sched ii =
   
@@ -82,7 +82,7 @@ let mve_kernel t ddg sched ii mult unroll =
   for i = 0 to (ii - 1) do
     let fregs = fresh_regs unroll in
     Array.iter print_reg  fregs;
-    Printf.fprintf Debug.dc "\n"; 
+    Printf.fprintf SPDebug.dc "\n";
     Array.set regs i fregs
   done;
 
@@ -113,7 +113,7 @@ let mve_kernel t ddg sched ii mult unroll =
 		      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 Debug.dc "Reecriture : %s --> %s \n" (string_of_node insti) (string_of_node inst);  
+		    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 ->
@@ -152,14 +152,14 @@ let mve_kernel t ddg sched ii mult unroll =
 
 				 (*   then  *)
 
-				 Printf.fprintf Debug.dc "i = %i - def = %i - use = %i - time = %i \n"
+				 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 Debug.dc "Positions to treat : %i \n" id; 
+ 			 	 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" 
@@ -266,35 +266,35 @@ let way_out prolog epilog used_regs =
 
 let mve ddg sched ii =
   assert (size_of_map1 sched = G.nb_vertex ddg);
-  Printf.fprintf Debug.dc "L'intervalle d'initiation est de : %i \n" ii;
-  Printf.fprintf Debug.dc "L'ordonnancement est le suivant : \n";
+  Printf.fprintf SPDebug.dc "L'intervalle d'initiation est de : %i \n" ii;
+  Printf.fprintf SPDebug.dc "L'ordonnancement est le suivant : \n";
   print_schedule sched;
   let (mult,unroll) = multiplicity ddg sched ii in  
   let unroll = unroll in  (* changer pour tester, default doit etre egal a unroll *)
-  Printf.fprintf Debug.dc "Table de multiplicite : \n";
-  Mult.iter (fun key mu -> print_reg key ; Printf.fprintf Debug.dc " |-> %i\n" mu) mult;
-  Printf.fprintf Debug.dc "Taux de deroulement de : %i \n" unroll;
+  Printf.fprintf SPDebug.dc "Table de multiplicite : \n";
+  Mult.iter (fun key mu -> print_reg key ; Printf.fprintf SPDebug.dc " |-> %i\n" mu) mult;
+  Printf.fprintf SPDebug.dc "Taux de deroulement de : %i \n" unroll;
   let steady_state = crunch_and_unroll sched ii unroll in
   let (steady_state,used_regs) = mve_kernel steady_state ddg sched ii mult unroll in
   print_table steady_state "Table finale"; 
   let min = ((sched_max_time sched) / ii) + 1 in
-  Printf.fprintf Debug.dc "min : %i \n" min; 
+  Printf.fprintf SPDebug.dc "min : %i \n" min;
   let iteration_table = compute_iteration_table sched ii in
-  Printf.fprintf Debug.dc "Table d'iteration \n";
+  Printf.fprintf SPDebug.dc "Table d'iteration \n";
   Array.iteri (fun i elt ->
 		 match elt with
 		   | Some elt ->
-		       Printf.fprintf Debug.dc "%i : %i\n" i elt
-		   | None -> Printf.fprintf Debug.dc "%i : _ \n" i
+		       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
   let epilog = List.filter (fun e -> not (is_cond e)) epilog in
-  Printf.fprintf Debug.dc "Prologue: \n"; 
-  List.iter (fun node -> Printf.fprintf Debug.dc "%s \n" (string_of_node node)) prolog; 
-  Printf.fprintf Debug.dc "Epilogue: \n"; 
-  List.iter (fun node -> Printf.fprintf Debug.dc "%s \n" (string_of_node node)) epilog;  
+  Printf.fprintf SPDebug.dc "Prologue: \n";
+  List.iter (fun node -> Printf.fprintf SPDebug.dc "%s \n" (string_of_node node)) prolog;
+  Printf.fprintf SPDebug.dc "Epilogue: \n";
+  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/SPMVE.mli b/src/SoftwarePipelining/SPMVE.mli
index 418a3ab..2da367d 100644
--- a/src/SoftwarePipelining/SPMVE.mli
+++ b/src/SoftwarePipelining/SPMVE.mli
@@ -10,8 +10,8 @@
 (***********************************************************************)
 
 
-open Basic
-open IMS
+open SPBasic
+open SPIMS
 
 val mve : G.t -> int NI.t -> int -> 
   (G.V.t option) array * G.V.t list * G.V.t list * int * int * (reg * reg) list * (reg * reg) list
diff --git a/src/SoftwarePipelining/SPSymbolic_evaluation.ml b/src/SoftwarePipelining/SPSymbolic_evaluation.ml
index eba5707..450cda7 100644
--- a/src/SoftwarePipelining/SPSymbolic_evaluation.ml
+++ b/src/SoftwarePipelining/SPSymbolic_evaluation.ml
@@ -13,7 +13,8 @@
 open Registers
 open Op
 open AST
-open Base_types
+open SPBase_types
+open Camlcoq
 
 type symbolic_value =
   | Sreg of reg
@@ -42,14 +43,14 @@ let find res st =
     | Not_found -> Sreg res
 
 let rec get_args st = function
-  | CList.Coq_nil -> []
-  | CList.Coq_cons (arg,args) -> find arg st :: get_args st args
+  | [] -> []
+  | 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, CList.Coq_cons (src,CList.Coq_nil), dst) :: l ->  
+  | Iop (Omove, [src], dst) :: l ->
       symbolic_evaluation (State.add dst (find src st) st) sm cs l      
 
   | Iop (op, args, dst) :: l -> 
@@ -73,7 +74,7 @@ type osv =
   | Ostore of memory_chunk * addressing 
 
 let string_of_osv = function
-  | Oresource (Reg r) -> Printf.sprintf "reg %i" (Int32.to_int (Camlcoq.camlint_of_positive r))
+  | Oresource (Reg r) -> Printf.sprintf "reg %i" (P.to_int r)
   | Oresource Mem -> "mem" 
   | Oop op -> string_of_op op
   | Oload (mc,addr) -> "load" 
@@ -201,7 +202,7 @@ let convert_sym st sm regs =
 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 = Debug.name ^ name in
+  let addr = SPDebug.name ^ name in
   dot_output_ss g addr  ;
   ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr  ^ ".png ; rm -f " ^ addr ^ ") & ")) (* & *)
   
diff --git a/src/SoftwarePipelining/SPTyping.ml b/src/SoftwarePipelining/SPTyping.ml
index f4e1f51..16c9b01 100644
--- a/src/SoftwarePipelining/SPTyping.ml
+++ b/src/SoftwarePipelining/SPTyping.ml
@@ -10,8 +10,8 @@
 (***********************************************************************)
 
 
-open Datatypes
-open CList
+(*open Datatypes
+open List
 open Camlcoq
 open Maps
 open AST
@@ -24,8 +24,6 @@ open Coqlib
 open Errors
 open Specif
 
-
-
 exception Type_error of string
 
 let env = ref (PTree.empty : typ PTree.t)
@@ -34,29 +32,29 @@ let set_type r ty =
   match PTree.get r !env with
   | None -> env := PTree.set r ty !env
   | Some ty' -> if ty <> ty' then 
-      begin 
-	Printf.fprintf Debug.dc "Failed to type register : %i " (Int32.to_int (Camlcoq.camlint_of_positive r));
-	raise (Type_error "type mismatch")
+      begin
+        Printf.fprintf SPDebug.dc "Failed to type register : %i " (P.to_int r);
+        raise (Type_error "type mismatch")
       end
 
 let rec set_types rl tyl =
   match rl, tyl with
-  | Coq_nil, Coq_nil -> ()
-  | Coq_cons(r1, rs), Coq_cons(ty1, tys) -> set_type r1 ty1; set_types rs tys
+  | [], [] -> ()
+  | r1 :: rs, ty1 :: tys -> set_type r1 ty1; set_types rs tys
   | _, _ -> raise (Type_error "arity mismatch")
 
 (* First pass: process constraints of the form typeof(r) = ty *)
 
-let type_instr retty (Coq_pair(pc, i)) =
-  Printf.fprintf Debug.dc "typage de l'instruction : %i \n" (Int32.to_int (Camlcoq.camlint_of_positive pc)); 
+let type_instr retty (pc, i) =
+  Printf.fprintf SPDebug.dc "typage de l'instruction : %i \n" (P.to_int pc);
   match i with
   | Inop(_) ->
       ()
   | Iop(Omove, _, _, _) -> 
       ()
   | Iop(op, args, res, _) ->
-      let (Coq_pair(targs, tres)) = type_of_operation op in
-      set_types args targs; set_type res tres
+    let (targs, tres) = type_of_operation op in
+    set_types args targs; set_type res tres
   | Iload(chunk, addr, args, dst, _) ->
       set_types args (type_of_addressing addr);
       set_type dst (type_of_chunk chunk)
@@ -70,7 +68,7 @@ let type_instr retty (Coq_pair(pc, i)) =
         | Coq_inr _ -> ()
         end;
         set_types args sg.sig_args;
-        set_type res (match sg.sig_res with None -> Tint | Some ty -> ty)
+        set_type res (match sg.sig_res with Tret t -> t | _ -> Tint);
       with Type_error msg ->
         let name =
           match ros with
@@ -96,28 +94,28 @@ let type_instr retty (Coq_pair(pc, i)) =
         raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s"
                                          name msg))
       end
-  | Ialloc(arg, res, _) ->
-      set_type arg Tint; set_type res Tint
+(*  | Ialloc(arg, res, _) ->
+      set_type arg Tint; set_type res Tint*)
   | Icond(cond, args, _, _) ->
       set_types args (type_of_condition cond)
   | Ireturn(optres) ->
       begin match optres, retty with
-      | None, None -> ()
-      | Some r, Some ty -> set_type r ty
+      | None, Tvoid -> ()
+      | Some r, Tret ty -> set_type r ty
       | _, _ -> raise (Type_error "type mismatch in Ireturn")
       end
 
 let type_pass1 retty instrs = 
-  coqlist_iter (type_instr retty) instrs
+  List.iter (type_instr retty) instrs
 
 (* Second pass: extract move constraints typeof(r1) = typeof(r2)
    and solve them iteratively *)
 
 let rec extract_moves = function
-  | Coq_nil -> []
-  | Coq_cons(Coq_pair(pc, i), rem) ->
+  | [] -> []
+  | (pc, i) :: rem ->
       match i with
-      | Iop(Omove, Coq_cons(r1, Coq_nil), r2, _) ->
+      | Iop(Omove, [r1], r2, _) ->
           (r1, r2) :: extract_moves rem
       | Iop(Omove, _, _, _) ->
           raise (Type_error "wrong Omove")
@@ -198,14 +196,14 @@ let check_reg env r ty =
 
 let rec check_regs env rl tyl =
   match rl with
-    | Coq_nil ->
+    | [] ->
         (match tyl with
-           | Coq_nil -> true
-           | Coq_cons (t, l) -> false)
-    | Coq_cons (r1, rs) ->
+           | [] -> true
+           | (t :: l) -> false)
+    | r1 :: rs ->
         (match tyl with
-           | Coq_nil -> false
-           | Coq_cons (ty, tys) ->
+           | [] -> false
+           | (ty :: tys) ->
                (match typ_eq (env r1) ty with
                   | true -> check_regs env rs tys
                   | false -> false))
@@ -213,7 +211,7 @@ let rec check_regs env rl tyl =
 (** val check_op : regenv -> operation -> reg list -> reg -> bool **)
 
 let check_op env op args res0 =
-  let Coq_pair (targs, tres) = type_of_operation op in
+  let (targs, tres) = type_of_operation op in
   (match check_regs env args targs with
      | true ->
          (match typ_eq (env res0) tres with
@@ -252,14 +250,14 @@ let check_instr funct env = function
              (match check_op env op args res0 with
                 | true -> check_successor funct s
                 | false -> false)
-         | Oaddrsymbol (i0, i1) ->
+(*         | Oaddrsymbol (i0, i1) ->
              (match check_op env op args res0 with
                 | true -> check_successor funct s
-                | false -> false)
-         | Oaddrstack i0 ->
+                | false -> false)*)
+(*         | Oaddrstack i0 ->
              (match check_op env op args res0 with
                 | true -> check_successor funct s
-                | false -> false)
+                | false -> false)*)
          | Ocast8signed ->
              (match check_op env op args res0 with
                 | true -> check_successor funct s
@@ -276,14 +274,14 @@ let check_instr funct env = function
              (match check_op env op args res0 with
                 | true -> check_successor funct s
                 | false -> false)
-         | Oadd ->
+(*         | Oadd ->
              (match check_op env op args res0 with
                 | true -> check_successor funct s
                 | false -> false)
          | Oaddimm i0 ->
              (match check_op env op args res0 with
                 | true -> check_successor funct s
-                | false -> false)
+                | false -> false)*)
          | Osub ->
              (match check_op env op args res0 with
                 | true -> check_successor funct s
@@ -463,13 +461,13 @@ let check_instr funct env = function
                | false -> false with
          | true -> tailcall_is_possible sig0
          | false -> false)
-  | Ialloc (arg, res0, s) ->
+(*  | Ialloc (arg, res0, s) ->
       (match typ_eq (env arg) Tint with
          | true ->
              (match typ_eq (env res0) Tint with
                 | true -> check_successor funct s
                 | false -> false)
-         | false -> false)
+         | false -> false)*)
   | Icond (cond, args, s1, s2) ->
       (match match check_regs env args (type_of_condition cond) with
                | true -> check_successor funct s1
@@ -522,7 +520,7 @@ let type_function f =
                  | false -> false with
                      | true -> check_successor f f.fn_entrypoint
                      | false -> false with
-			 | true -> Printf.fprintf Debug.dc "The code is well typed\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/SPTyping.mli b/src/SoftwarePipelining/SPTyping.mli
index c231ddd..dd27875 100644
--- a/src/SoftwarePipelining/SPTyping.mli
+++ b/src/SoftwarePipelining/SPTyping.mli
@@ -11,5 +11,4 @@
 
 
 
-val type_function : RTL.coq_function -> unit
-
+(*val type_function : RTL.coq_function -> unit*)
diff --git a/src/SoftwarePipelining/SoftwarePipelining.ml b/src/SoftwarePipelining/SoftwarePipelining.ml
index eeb2dfd..12ab783 100644
--- a/src/SoftwarePipelining/SoftwarePipelining.ml
+++ b/src/SoftwarePipelining/SoftwarePipelining.ml
@@ -10,9 +10,9 @@
 (***********************************************************************)
 
 
-open Basic
-open IMS
-open MVE
+open SPBasic
+open SPIMS
+open SPMVE
 open RTL
 
 let clean t = 
@@ -57,8 +57,8 @@ let order = ref []
 
 let pipeliner ddg =  
   order := List.flatten (Scc.scc_list ddg);
-  let (sched,ii) = IMS.pipeliner ddg random in
-  let (steady,prolog,epilog,min,unroll,entrance,way_out) = MVE.mve ddg sched ii in
+  let (sched,ii) = SPIMS.pipeliner ddg random in
+  let (steady,prolog,epilog,min,unroll,entrance,way_out) = SPMVE.mve ddg sched ii in
   let steady_state = clean steady in
   if min <= 0 then None 
   else
@@ -66,8 +66,5 @@ let pipeliner ddg =
 	 ramp_up = entrance; ramp_down = way_out}
       
 
-let main f = 
-  Basic.apply_pipeliner f pipeliner ~debug:false
-
-  
-
+let pipeline f =
+  SPBasic.apply_pipeliner f pipeliner ~debug:true