Rename pipelining

13 files changed, 2411 insertions, 0 deletions

diff --git a/src/pipelining/LICENSE b/src/pipelining/LICENSE
new file mode 100644
index 0000000..e275fa0
--- /dev/null
+++ b/src/pipelining/LICENSE
@@ -0,0 +1,19 @@
+Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/src/pipelining/SPBase_types.ml b/src/pipelining/SPBase_types.ml
new file mode 100644
index 0000000..ba92340
--- /dev/null
+++ b/src/pipelining/SPBase_types.ml
@@ -0,0 +1,128 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open Camlcoq
+open Op
+open Registers
+open Memory
+open Mem
+open AST
+
+type ('a,'b) sum = ('a,'b) Datatypes.sum
+
+type instruction =
+  | Inop 
+  | 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
+
+let inst_coq_to_caml = function 
+  | RTL.Inop succ -> Inop
+  | RTL.Iop (op, args, dst, succ) -> Iop (op, args, dst)
+  | RTL.Iload (chunk, mode, args, dst, succ) -> Iload (chunk, mode, args, dst)
+  | 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.Icond (cond, args, succ1, succ2) -> Icond (cond, args)
+  | RTL.Ireturn (res) -> Ireturn (res)
+ 
+let inst_caml_to_coq i (links : RTL.node list) =
+  match i,links with 
+  | Inop,[p] -> RTL.Inop p
+  | Iop (op, args, dst),[p] -> RTL.Iop (op, args, dst,p)  
+  | Iload (chunk, mode, args, dst),[p] -> RTL.Iload (chunk, mode, args,dst,p) 
+  | 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) 
+  | 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 -> P.to_int n
+let to_binpos = fun n -> P.of_int n
+
+let rec string_of_args args =
+  match args with
+    | [] -> ""
+    | arg :: args -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args
+
+let string_of_z z = string_of_int (Z.to_int z)
+
+let string_of_comparison = function
+  | Integers.Ceq -> "eq"
+  | Integers.Cne -> "ne"
+  | Integers.Clt -> "lt"
+  | Integers.Cle -> "le"
+  | Integers.Cgt -> "gt"
+  | Integers.Cge -> "ge"
+ 
+let string_of_cond = function
+  | Ccomp c -> Printf.sprintf "comp %s" (string_of_comparison c)
+  | Ccompu c -> Printf.sprintf "compu %s" (string_of_comparison c)
+  | Ccompimm (c,i) -> Printf.sprintf "compimm %s %s" (string_of_comparison c) (string_of_z i)
+  | Ccompuimm (c,i) -> Printf.sprintf "compuimm %s %s" (string_of_comparison c) (string_of_z i)
+  | Ccompf c -> Printf.sprintf "compf %s" (string_of_comparison c)
+  | Cnotcompf c -> Printf.sprintf "notcompf %s" (string_of_comparison c)
+  | Cmaskzero i -> Printf.sprintf "maskzero %s" (string_of_z i)
+  | Cmasknotzero i -> Printf.sprintf "masknotzero %s" (string_of_z i)
+
+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 (camlfloat_of_coqfloat32 f))
+  | Ocast8signed -> "cast8signed"
+  | Ocast8unsigned -> "cast8unsigned"
+  | Ocast16signed -> "cast16signed"
+  | Ocast16unsigned -> "cast16unsigned"
+  | Osub -> "sub"
+  | Omul -> "mul"
+  | Omulimm i -> Printf.sprintf "mulimm %s" (string_of_z i)
+  | Odiv -> "div"
+  | Odivu -> "divu"
+  | Oand -> "and"
+  | Oandimm i -> Printf.sprintf "andimm %s" (string_of_z i)
+  | Oor -> "or"
+  | Oorimm i -> Printf.sprintf "orimm %s" (string_of_z i)
+  | Oxor -> "xor"
+  | Oxorimm i -> Printf.sprintf "xorimm %s" (string_of_z i)
+  | 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"
+  | Onegf -> "negf"
+  | Oabsf -> "absf"
+  | Oaddf -> "addf"
+  | Osubf -> "subf"
+  | Omulf -> "mulf"
+  | Odivf -> "divf"
+  | Osingleoffloat -> "singleoffloat"
+  | Ofloatofint -> "floatofint"
+  | Ocmp c -> Printf.sprintf "cmpcmpcmp"
+  | Olea _ -> "lea"
+  
+let to_coq_list = function
+  | [] -> []
+  | e :: l -> e :: l
+
+let to_caml_list = function
+  | [] -> []
+  | e :: l -> e :: l
diff --git a/src/pipelining/SPBasic.ml b/src/pipelining/SPBasic.ml
new file mode 100644
index 0000000..32234b8
--- /dev/null
+++ b/src/pipelining/SPBasic.ml
@@ -0,0 +1,819 @@
+(***********************************************************************)
+ (*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open RTL
+open Camlcoq
+open Graph.Pack.Digraph
+open Op
+open Registers
+open Memory
+open Mem
+open AST
+open SPBase_types
+open SPSymbolic_evaluation
+
+type node = instruction * int
+module G = Graph.Persistent.Digraph.AbstractLabeled
+    (struct type t = node end)
+    (struct type t = int let compare = compare let default = 0 end)
+module Topo = Graph.Topological.Make (G)
+module Dom = Graph.Dominator.Make (G)
+module Index = Map.Make (struct type t = int let compare = compare end)
+
+let string_of_instruction node =
+  match G.V.label node with
+  | (Inop,n) -> Printf.sprintf "%i nop" n
+  | (Iop (op, args, dst),n) -> Printf.sprintf "%i r%i := %s %s" n (to_int dst) (string_of_op op) (string_of_args args)
+  | (Iload (chunk, mode, args, dst),n) -> Printf.sprintf "%i r%i := load %s" n (to_int dst) (string_of_args args)
+  | (Istore (chunk, mode, args, src),n) -> Printf.sprintf "%i store %i %s" n (to_int src) (string_of_args args)
+  | (Icall (sign, id, args, dst),n) -> Printf.sprintf "%i call" n
+  | (Itailcall (sign, id, args),n) -> Printf.sprintf "%i tailcall" n
+  (*  | (Ialloc (dst, size),n) -> Printf.sprintf "%i %i := alloc" n (to_int dst) *)
+  | (Icond (cond, args),n) -> Printf.sprintf "%i cond %s %s" n (string_of_cond cond) (string_of_args args)
+  | (Ireturn (res),n) -> Printf.sprintf "%i return" n
+
+let string_of_node = string_of_instruction
+
+module Display = struct
+  include G
+  let vertex_name v = print_inst (V.label v)
+  let graph_attributes _ = []
+  let default_vertex_attributes _ = []
+  let vertex_attributes v = [`Label (string_of_instruction v)]
+  let default_edge_attributes _ = []
+  let edge_attributes e = [`Label (string_of_int (G.E.label e))]
+  let get_subgraph _ = None
+end
+module Dot_ = Graph.Graphviz.Dot(Display)
+
+let dot_output g f = 
+  let oc = open_out f in
+  Dot_.output_graph oc g; 
+  close_out oc
+
+let display g name =
+  let addr = SPDebug.name ^ name in
+  dot_output g addr  ;
+  ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr  ^ ".png ; rm -f " ^ addr ^ ") & "))
+
+(******************************************)
+
+type cfg = {graph : G.t; start : G.V.t}
+
+(* convert traduit un graphe RTL compcert en un graphe RTL ocamlgraph*)
+
+let convert f  = 
+
+  let make_node inst key =
+    let inst = inst_coq_to_caml inst in
+    G.V.create (inst, to_int key)
+  in
+
+  let (graph, index) = Maps.PTree.fold (fun (g,m) key inst -> 
+      let node = make_node inst key in
+      (G.add_vertex g node, Index.add (to_int key) node m)
+    ) f.fn_code (G.empty,Index.empty)
+  in
+
+  let succ = RTL.successors_map f in
+  let rec link n succs g =
+    match succs with
+    | [] -> g
+    | pos::[] ->
+      G.add_edge g (Index.find (to_int n) index) (Index.find (to_int pos) index)
+    | pos1::pos2::[] ->
+      let g = G.add_edge_e g (G.E.create (Index.find (to_int n) index) 1 (Index.find (to_int pos1) index)) in
+      G.add_edge_e g (G.E.create (Index.find (to_int n) index) 2 (Index.find (to_int pos2) index))
+    | _ -> failwith "convert : trop de successeurs"
+
+  in
+
+  let graph = Maps.PTree.fold ( fun g key inst ->
+      link key (match Maps.PTree.get key succ with
+            Some x -> x | _ -> failwith "Could not index") g
+    ) f.fn_code graph
+  in
+
+  {graph = graph; start = Index.find (to_int (f.fn_entrypoint)) index}
+
+
+let convert_back g =
+
+  G.fold_vertex (fun node m ->
+      let v = G.V.label node in
+      match (fst v) with
+      | Icond (_,_) ->
+        begin
+          let l =
+            match G.succ_e g node with
+            | [e1;e2] ->
+              if G.E.label e1 > G.E.label e2
+              then [G.E.dst e2;G.E.dst e1]
+              else [G.E.dst e1;G.E.dst e2]
+            | _ -> failwith "convert_back: nombre de successeurs incoherent"
+          in
+          let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) l in
+          Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m
+        end
+      | _ ->
+        let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) (G.succ g node) in
+        Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m
+    ) g Maps.PTree.empty
+
+
+
+
+(* dominator_tree calcule l'arbre de domination grace au code de FP *)
+let dominator_tree f =
+  Dom.compute_idom f.graph f.start
+
+(* detect_loops, find the loops in the graph and returns the list of nodes in it,
+   in dominating order !!! This is of great importance, we suppose that it is ordered
+   when we build the dependency graph *)
+let detect_loops graph dom_tree =
+  let rec is_dominating v1 v2 l = (* does v1 dominate v2 *)
+    match dom_tree v2 with
+    | v -> if v1 = v then Some (v :: l)
+      else is_dominating v1 v (v :: l)
+    | exception (Not_found) -> None
+  in
+
+  G.fold_edges (fun v1 v2 loops -> 
+      match is_dominating v2 v1 [v1] with
+      | None -> loops
+      | Some loop -> (v2,loop) :: loops
+    ) graph []
+
+let print_index node =
+  Printf.printf "%i " (snd (G.V.label node))
+
+let print_instruction node = 
+  match G.V.label node with
+  | (Inop,n) -> Printf.printf "%i : Inop \n" n 
+  | (Iop (op, args, dst),n) -> Printf.printf "%i : Iop  \n" n  
+  | (Iload (chunk, mode, args, dst),n) -> Printf.printf "%i : Iload \n" n    
+  | (Istore (chunk, mode, args, src),n) -> Printf.printf "%i : Istore \n" n    
+  | (Icall (sign, id, args, dst),n) -> Printf.printf "%i : Icall \n" n   
+  | (Itailcall (sign, id, args),n) -> Printf.printf "%i : Itailcall \n" n   
+  (*| (Ialloc (dst, size),n) -> Printf.printf "%i : Ialloc \n" n  *)
+  | (Icond (cond, args),n) -> Printf.printf "%i : Icond \n" n    
+  | (Ireturn (res),n) -> Printf.printf "%i : Ireturn \n" n   
+
+let is_rewritten node r = 
+  match fst (G.V.label node) with
+  | Inop -> false
+  | Iop (op, args, dst) -> if dst = r then true else false
+  | Iload (chunk, mode, args, dst) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false
+  | Istore (chunk, mode, args, src) -> false
+  | Icall (sign, id, args, dst) -> failwith "call in a loop"
+  | Itailcall (sign, id, args) -> failwith "tailcall in a loop"
+  (*    | Ialloc (dst, size) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false *)
+  | Icond (cond, args) -> false
+  | Ireturn (res) -> failwith "return in a loop"
+
+let is_variant r loop = 
+  List.fold_right (fun node b -> 
+      is_rewritten node r || b
+    ) loop false
+
+
+let is_pipelinable loop = (* true if loop is innermost and without control *)
+
+  let is_acceptable node =
+    match fst (G.V.label node) with
+    | Icall _ | Itailcall _ | Ireturn _ | Icond _ (*| Ialloc _*) | Iop ((Ocmp _),_,_)-> false
+    | _ -> true
+  in
+
+  let is_branching node = 
+    match fst (G.V.label node) with
+    | Icond _ -> true
+    | _ -> false
+  in
+
+  let is_nop node = 
+    match fst (G.V.label node) with
+    | Inop -> true
+    | _ -> false
+  in
+
+  let is_OK_aux l =
+    List.fold_right (fun n b -> is_acceptable n && b) l true
+  in
+
+  let is_bounded node loop =
+    match G.V.label node with
+    | (Icond (cond, args),n) ->
+      let args = to_caml_list args in
+      begin
+        match args with
+        | [] -> false
+        | r :: [] -> is_variant r loop (* used to be not *)
+        | r1 :: r2 :: [] ->
+          begin
+            match is_variant r1 loop, is_variant r2 loop with
+            | true, true -> false
+            | false, true -> true
+            | true, false -> true
+            | false, false -> false
+          end
+        | _ -> false
+      end
+    | _ -> false
+  in
+
+  match List.rev loop with
+  | v2 :: v1 :: l -> ((*Printf.printf "is_nop: %s | " (is_nop v1 |> string_of_bool);*)
+      Printf.printf "is_branching: %s | " (is_branching v2 |> string_of_bool);
+      Printf.printf "is_OK_aux: %s | " (is_OK_aux l |> string_of_bool);
+      Printf.printf "is_bounded: %s\n" (is_bounded v2 loop |> string_of_bool);
+      (*is_nop v1 && *)is_branching v2 && is_OK_aux l && is_bounded v2 loop)
+  | _ -> false
+
+let print_loops loops = 
+  List.iter (fun loop -> print_index (fst(loop));
+              print_newline ();
+              List.iter print_index (snd(loop));
+              print_newline ();
+              if is_pipelinable (snd(loop)) then print_string "PIPELINABLE !" else print_string "WASTE";
+              print_newline ();
+              List.iter print_instruction (snd(loop));
+              print_newline ()
+            ) loops
+
+(* type resource = Reg of reg | Mem *)
+module Sim = Map.Make (struct type t = resource let compare = compare end)
+
+let map_get key map =
+  try Some (Sim.find key map) 
+  with
+  | Not_found -> None
+
+let rec to_res l = 
+  match l with
+  | [] -> []
+  | e :: l -> Reg e :: to_res l
+
+let resources_reads_of node = 
+  match fst (G.V.label node) with
+  | Inop -> []
+  | Iop (op, args, dst) -> to_res args
+  | Iload (chunk, mode, args, dst) -> Mem :: (to_res args)
+  | Istore (chunk, mode, args, src) -> Mem :: Reg src :: (to_res args)
+  | Icall (sign, id, args, dst) -> failwith "Resource read of call"
+  | Itailcall (sign, id, args) -> failwith "Resource read of tailcall"
+  (*| Ialloc (dst, size) -> [Mem] *)
+  | Icond (cond, args) -> to_res args
+  | Ireturn (res) -> failwith "Resource read of return"
+
+let resources_writes_of node = 
+  match fst (G.V.label node) with
+  | Inop -> []
+  | Iop (op, args, dst) -> [Reg dst]
+  | Iload (chunk, mode, args, dst) -> [Reg dst]
+  | Istore (chunk, mode, args, src) -> [Mem]
+  | Icall (sign, id, args, dst) -> failwith "Resource read of call"
+  | Itailcall (sign, id, args) -> failwith "Resource read of tailcall"
+  (*| Ialloc (dst, size) -> (Reg dst) :: [Mem]*)
+  | Icond (cond, args) -> []
+  | Ireturn (res) -> failwith "Resource read of return"
+
+let build_intra_dependency_graph loop =
+
+  let rec build_aux graph read write l = 
+    match l with
+    | [] -> (graph,(read,write))
+    | v :: l->
+      let g = G.add_vertex graph v in
+      let reads = resources_reads_of v in
+      let writes = resources_writes_of v in
+      (* dependances RAW *)
+      let g = List.fold_right (fun r g ->
+          match map_get r write with
+          | Some n -> G.add_edge_e g (G.E.create n 1 v)
+          | None -> g
+        ) reads g in
+      (* dependances WAR *)
+      let g = List.fold_right (fun r g ->
+          match map_get r read with
+          | Some l -> List.fold_right (fun n g -> G.add_edge_e g (G.E.create n 2 v)) l g
+          | None -> g
+        ) writes g in
+      (* dependances WAW *)
+      let g = List.fold_right (fun r g ->
+          match map_get r write with
+          | Some n -> G.add_edge_e g (G.E.create n 3 v)
+          | None -> g
+        ) writes g in
+      let write = List.fold_right (fun r m -> Sim.add r v m) writes write in
+      let read_tmp = List.fold_right (fun r m ->
+          match map_get r read with
+          | Some al -> Sim.add r (v :: al) m
+          | None -> Sim.add r (v :: []) m
+        ) reads read
+      in
+      let read = List.fold_right (fun r m -> Sim.add r [] m) writes read_tmp in
+
+      build_aux g read write l
+  in
+
+  build_aux G.empty Sim.empty Sim.empty (List.tl loop) 
+
+let build_inter_dependency_graph loop =
+
+  let rec build_aux2 graph read write l = 
+    match l with
+    | [] -> graph
+    | v :: l->
+      let g = graph in
+      let reads = resources_reads_of v in
+      let writes = resources_writes_of v in
+      (* dependances RAW *)
+      let g = List.fold_right (fun r g ->
+          match map_get r write with
+          | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 4 v)
+          | None -> g
+        ) reads g in
+      (* dependances WAR *)
+      let g = List.fold_right (fun r g ->
+          match map_get r read with
+          | Some l -> List.fold_right
+                        (fun n g -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 5 v)) l g
+          | None -> g
+        ) writes g in
+      (* dependances WAW *)
+      let g = List.fold_right (fun r g ->
+          match map_get r write with
+          | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 6 v)
+          | None -> g
+        ) writes g in
+      let write = List.fold_right (fun r m -> Sim.remove r m) writes write in
+      let read = List.fold_right (fun r m -> Sim.remove r m) writes read in
+
+
+      build_aux2 g read write l
+  in
+
+  let (g,(r,w)) = build_intra_dependency_graph loop in
+  build_aux2 g r w (List.tl loop)
+
+(* patch_graph prepare le graphe pour la boucle commencant au noeud entry 
+   qui a une borne de boucle bound et pour un software pipelining
+   de au minimum min tours et de deroulement ur *)
+(* this is rather technical so we give many comments *)
+
+(*   let n1 = G.V.create (Iop ((Ointconst ur),to_coq_list [],r1),next_pc) in *)
+(*   let next_pc = next_pc + 1 in *)
+(*   let n2 = G.V.create (Iop (Odiv,to_coq_list [bound;r1],r2),next_pc) in *)
+(*   let next_pc = next_pc + 1 in *)
+(*   let n3 = G.V.create (Iop ((Omulimm ur),to_coq_list [r2],r3),next_pc) in *)
+(*   let next_pc = next_pc + 1 in *)
+(*   let n4 = G.V.create (Iop (Osub,to_coq_list [bound;r3],r4),next_pc) in *)
+(*   let next_pc = next_pc + 1 in *)
+(*   let n5 = G.V.create (Iop (Omove,to_coq_list [r3],bound),next_pc) in (\* retouchee, [r3],bound *\) *)
+
+
+let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog epilog ramp_up ramp_down =
+
+  (* 1. Break the edge that enters the loop, except for the backedge *)
+  let preds_e = G.pred_e graph entry in
+  let wannabes = List.map G.E.src preds_e in 
+  let wannabes = List.filter (fun e -> not (e = lastone)) wannabes in
+  let graph = List.fold_right (fun e g -> G.remove_edge_e g e) preds_e graph in
+  let graph = G.add_edge graph lastone entry in
+
+  (* 2. Add the test for minimal iterations and link it*)
+
+  let cond = G.V.create (Icond ((Ccompimm (Integers.Cle,min)),to_coq_list [bound]), next_pc) in
+  let graph = G.add_vertex graph cond in
+  let next_pc = next_pc + 1 in
+
+  (* 3. Link its predecessors and successors *)
+  (* It is false in case there is a condition that points to the entry:
+     inthis case, the edge should not be labeled with 0 !*)
+
+  let graph = List.fold_right (fun n g -> G.add_edge g n cond) wannabes graph in
+  let graph = G.add_edge_e graph (G.E.create cond 1 entry) in
+
+
+  (* 4. Add the div and modulo code, link it *)
+  let n1 = G.V.create (Iop ((Ointconst ur),to_coq_list [],r1),next_pc) in
+  let next_pc = next_pc + 1 in
+  let n2 = G.V.create (Iop (Odiv,to_coq_list [bound;r1],r2),next_pc) in
+  let next_pc = next_pc + 1 in
+  let n3 = G.V.create (Iop (Omove,to_coq_list [bound],r4),next_pc) in
+  let next_pc = next_pc + 1 in
+  let n4 = G.V.create (Iop ((Omulimm ur ),to_coq_list [r2],r3),next_pc) in
+  let next_pc = next_pc + 1 in
+  let n5 = G.V.create (Iop ((Olea (Aindexed (Z.of_sint (-1)))),to_coq_list [r3],bound),next_pc) in (* retouchee, [r3],bound *)
+  let next_pc = next_pc + 1 in
+  let graph = G.add_vertex graph n1 in
+  let graph = G.add_vertex graph n2 in
+  let graph = G.add_vertex graph n3 in
+  let graph = G.add_vertex graph n4 in
+  let graph = G.add_vertex graph n5 in
+  let graph = G.add_edge_e graph (G.E.create cond 2 n1) in
+  let graph = G.add_edge graph n1 n2 in
+  let graph = G.add_edge graph n2 n3 in
+  let graph = G.add_edge graph n3 n4 in
+  let graph = G.add_edge graph n4 n5 in
+
+  (* 5. Fabriquer la pipelined loop et la linker, sans la condition d entree *)
+
+  let (graph,next_pc,l) = List.fold_right (fun e (g,npc,l) -> 
+      let n = G.V.create (e,npc) in
+      (G.add_vertex g n, npc+1, n :: l)
+    ) loop (graph,next_pc,[]) in
+
+  let pipe_cond = List.hd l in
+  let pipeline = List.tl l in
+
+  let rec link l graph node =
+    match l with
+    | n1 :: n2 :: l -> link (n2 :: l) (G.add_edge graph n1 n2) node
+    | n1 :: [] -> G.add_edge graph n1 node
+    | _ -> graph
+  in
+
+  let graph = link pipeline graph pipe_cond in
+
+  (* link de l entree de la boucle *)
+
+  let (graph,next_pc,prolog) = List.fold_right (fun e (g,npc,l) -> 
+      let n = G.V.create (e,npc) in
+      (G.add_vertex g n, npc+1, n :: l)
+    ) prolog (graph,next_pc,[]) in
+
+  let (graph,next_pc,epilog) = List.fold_right (fun e (g,npc,l) -> 
+      let n = G.V.create (e,npc) in
+      (G.add_vertex g n, npc+1, n :: l)
+    ) epilog (graph,next_pc,[]) in
+
+  (* 6. Creation du reste et branchement et la condition *)
+  let n6 = G.V.create (Iop (Omove,to_coq_list [r4],bound),next_pc) in (* Iop (Omove,to_coq_list [r4],bound) *)
+  let next_pc = next_pc + 1 in
+
+  (* 7. Creation du ramp up *)
+  let ramp_up = List.map (fun (a,b) -> Iop (Omove, [b], a)) ramp_up in
+  let (graph,next_pc,ramp_up) = List.fold_right (fun e (g,npc,l) -> 
+      let n = G.V.create (e,npc) in
+      (G.add_vertex g n, npc+1, n :: l)
+    ) ramp_up (graph,next_pc,[]) in
+
+  let next_pc = next_pc + 1 in
+
+  let ramp_down = List.map (fun (a,b) -> Iop (Omove,[b],a)) ramp_down in
+  let (graph,next_pc,ramp_down) = List.fold_right (fun e (g,npc,l) -> 
+      let n = G.V.create (e,npc) in
+      (G.add_vertex g n, npc+1, n :: l)
+    ) ramp_down (graph,next_pc,[]) in
+
+  (* let next_pc = next_pc + 1 in *)
+
+  (* Creation des proloque et epilogue *)
+
+  let graph = link prolog graph pipe_cond in
+  let graph = link ramp_up graph (List.hd prolog) in
+  let graph = link epilog graph (List.hd ramp_down) in
+  let graph = link ramp_down graph n6 in
+
+  let graph = G.add_edge graph n5 (List.hd ramp_up) in
+  let graph = G.add_edge_e graph (G.E.create pipe_cond 1 (List.hd epilog)) in
+  let graph = G.add_edge_e graph (G.E.create pipe_cond 2 (List.hd pipeline)) in
+
+  (* 8. Retour sur la boucle classique *)
+  let graph = G.add_edge graph n6 entry in
+
+  graph
+
+let regs_of_node node = 
+  match G.V.label node with
+  | (Inop,n) -> []
+  | (Iop (op, args, dst),n) -> dst :: (to_caml_list args)
+  | (Iload (chunk, mode, args, dst),n) -> dst :: (to_caml_list args)
+  | (Istore (chunk, mode, args, src),n) -> src :: (to_caml_list args)
+  | (Icall (sign, id, args, dst),n) -> dst :: (to_caml_list args)
+  | (Itailcall (sign, id, args),n) -> (to_caml_list args)
+  (*| (Ialloc (dst, size),n) -> [dst]*)
+  | (Icond (cond, args),n) -> (to_caml_list args)
+  | (Ireturn (res),n) -> match res with Some res -> [res] | _ -> []
+
+let max_reg_of_graph graph params =
+  Printf.fprintf SPDebug.dc "Calcul du registre de depart.\n";
+  let regs =  G.fold_vertex (fun node regs ->
+      (regs_of_node node) @ regs
+    ) graph [] in
+  let regs = regs @ params in
+  let max_reg = List.fold_right (fun reg max ->
+      Printf.fprintf SPDebug.dc "%i " (P.to_int reg);
+      if Int32.compare (P.to_int32 reg) max > 0
+      then (P.to_int32 reg)
+      else max
+    ) regs Int32.zero in
+
+  Printf.fprintf SPDebug.dc "MAX REG = %i\n" (Int32.to_int max_reg);
+  BinPos.Pos.succ (P.of_int32 max_reg)
+
+let get_bound node loop =
+  match G.V.label node with
+  | (Icond (cond, args),n) ->
+    let args = to_caml_list args in
+    begin
+      match args with
+      | [] -> failwith "get_bound: condition sans variables"
+      | r :: [] -> if is_variant r loop then failwith "Pas de borne dans la boucle"  else r (* Modified false to true condition. *)
+      | r1 :: r2 :: [] ->
+        begin
+          match is_variant r1 loop, is_variant r2 loop with
+          | true, true -> failwith "Pas de borne dans la boucle "
+          | false, true -> r1
+          | true, false -> r2
+          | false, false -> failwith "deux bornes possibles dans la boucle"
+        end
+      | _ -> failwith "get_bound: condition avec nombre de variables superieur a 2"
+    end
+  | _ -> failwith "get_bound: the node I was given is not a condition\n"
+
+let get_nextpc graph =
+  (G.fold_vertex (fun node max ->
+       if (snd (G.V.label node)) > max
+       then (snd (G.V.label node))
+       else max
+     ) graph 0) + 1
+
+let substitute_pipeline graph loop steady_state prolog epilog min unrolling ru rd params =
+  let n1 = max_reg_of_graph graph params in
+  let n2 = (BinPos.Pos.succ n1) in
+  let n3 = (BinPos.Pos.succ n2) in
+  let n4 = (BinPos.Pos.succ n3) in
+  let way_in = (List.hd loop) in
+  let way_out = (List.hd (List.rev loop)) in
+  let bound = (get_bound way_out loop) in
+  let min = Z.of_sint min in
+  let unrolling = Z.of_sint unrolling in
+  let next_pc = get_nextpc graph in
+  patch_graph graph way_in way_out steady_state bound min unrolling n1 n2 n3 n4 next_pc prolog epilog ru rd 
+
+let get_loops cfg =
+  let domi = dominator_tree cfg in
+  let loops = detect_loops cfg.graph domi in
+  print_loops loops;
+  let loops = List.filter (fun loop -> is_pipelinable (snd (loop))) loops in 
+  loops
+
+type pipeline = {steady_state : G.V.t list; prolog : G.V.t list; epilog : G.V.t list; 
+                 min : int; unrolling : int; ramp_up : (reg * reg) list; ramp_down : (reg * reg) list}
+
+let delete_indexes l = List.map (fun e -> fst (G.V.label e) ) l
+
+type reg = Registers.reg 
+
+let fresh = ref BinNums.Coq_xH
+
+let distance e = 
+  match G.E.label e with
+  | 1 | 2 | 3 -> 0
+  | _ -> 1
+
+type et = IntraRAW | IntraWAW | IntraWAR | InterRAW | InterWAW | InterWAR
+
+let edge_type e = 
+  match G.E.label e with
+  | 1 -> IntraRAW
+  | 2 -> IntraWAR
+  | 3 -> IntraWAW
+  | 4 -> InterRAW
+  | 5 -> InterWAR
+  | 6 -> InterWAW
+  | _ -> failwith "Unknown edge type"
+
+let latency n = (* A raffiner *) 
+  match fst (G.V.label n) with
+  | Iop (op,args, dst) ->
+    begin
+      match op with
+      | Omove -> 1
+      (*| Oaddimm _ -> 1*)
+      (*| Oadd -> 2*)
+      | Omul -> 4
+      | Odiv -> 30
+      | Omulimm _ -> 4
+      | _ -> 2
+    end
+  | Iload _ -> 1
+  (*    | Ialloc _ -> 20*)
+  | _ -> 1
+
+let reforge_writes inst r = 
+  G.V.create ((match fst (G.V.label inst) with
+      | Inop -> Inop
+      | Iop (op, args, dst) -> Iop (op, args, r)
+      | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, args, r)
+      | Istore (chunk, mode, args, src) -> Istore (chunk, mode, args, src)
+      | Icall (sign, id, args, dst) -> failwith "reforge_writes: call"
+      | Itailcall (sign, id, args) -> failwith "reforge_writes: tailcall"
+      (*    | Ialloc (dst, size) -> Ialloc (r, size)*)
+      | Icond (cond, args) -> Icond (cond, args)
+      | Ireturn (res) -> failwith "reforge_writes: return")
+             , snd (G.V.label inst))
+
+let rec reforge_args args oldr newr =
+  match args with
+  | [] -> []
+  | e :: l -> (if e = oldr then newr else e) :: (reforge_args l oldr newr)
+
+let rec mem_args args r =
+  match args with
+  | [] -> false
+  | e :: l -> if e = r then true else mem_args l r
+
+let check_read_exists inst r =
+  match fst (G.V.label inst) with
+  | Inop -> false
+  | Iop (op, args, dst) -> mem_args args r
+  | Iload (chunk, mode, args, dst) -> mem_args args r
+  | Istore (chunk, mode, args, src) -> src = r || mem_args args r
+  | Icall (sign, id, args, dst) -> mem_args args r
+  | Itailcall (sign, id, args) -> false
+  (*| Ialloc (dst, size) -> false*)
+  | Icond (cond, args) -> mem_args args r
+  | Ireturn (res) -> false
+
+let reforge_reads inst oldr newr  = 
+  assert (check_read_exists inst oldr);
+  G.V.create ((match fst (G.V.label inst) with
+      | Inop -> Inop
+      | Iop (op, args, dst) -> Iop (op, reforge_args args oldr newr, dst)
+      | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, reforge_args args oldr newr, dst)
+      | Istore (chunk, mode, args, src) -> Istore (chunk, mode, reforge_args args oldr newr , if src = oldr then newr else src)
+      | Icall (sign, id, args, dst) -> failwith "reforge_reads: call"
+      | Itailcall (sign, id, args) -> failwith "reforge_reads: tailcall"
+      (*| Ialloc (dst, size) -> Ialloc (dst, size)*)
+      | Icond (cond, args) -> Icond (cond, reforge_args args oldr newr)
+      | Ireturn (res) -> failwith "reforge_reads: return")
+             , snd (G.V.label inst))
+
+let get_succs_raw ddg node = 
+  let succs = G.succ_e ddg node in
+  let succs = List.filter (fun succ ->
+      match G.E.label succ with
+      | 1 | 4 -> true
+      | _ -> false
+    ) succs in
+  List.map (fun e -> G.E.dst e) succs
+
+let written inst = 
+  match fst (G.V.label inst) with
+  | Inop -> None
+  | Iop (op, args, dst) -> Some dst
+  | Iload (chunk, mode, args, dst) -> Some dst
+  | Istore (chunk, mode, args, src) -> None
+  | Icall (sign, id, args, dst) -> failwith "written: call"
+  | Itailcall (sign, id, args) -> failwith "written: tailcall"
+  (*| Ialloc (dst, size) -> Some dst*)
+  | Icond (cond, args) -> None
+  | Ireturn (res) -> failwith "written: return"
+
+let fresh_regs n =
+  let t = Array.make n (BinNums.Coq_xH) in
+  for i = 0 to (n - 1) do
+    Array.set t i (!fresh);
+    fresh := BinPos.Pos.succ !fresh
+  done;
+  t
+
+let print_reg r = Printf.fprintf SPDebug.dc "%i " (P.to_int r)
+
+let is_cond node =
+  match fst (G.V.label node) with
+  | Icond _ -> true
+  | _ -> false
+
+
+(*******************************************)
+
+let watch_regs l = List.fold_right (fun (a,b) l ->
+    if List.mem a l then l else a :: l
+  ) l []
+
+let make_moves = List.map (fun (a,b) -> Iop (Omove,[b],a))
+
+let rec repeat l n =
+  match n with
+  | 0 -> []
+  | n -> l @ repeat l (n-1)
+
+let fv = ref 0
+
+let apply_pipeliner f p ?(debug=false) = 
+  Printf.fprintf SPDebug.dc "******************** NEW FUNCTION ***********************\n";
+  let cfg = convert f in
+  incr fv;
+  if debug then display cfg.graph ("input" ^ (string_of_int !fv));
+  let loops = get_loops cfg in
+  Printf.fprintf SPDebug.dc "Loops: %d\n" (List.length loops);
+  let ddgs = List.map (fun (qqch,loop) -> (loop,build_inter_dependency_graph loop)) loops in
+
+  let lv = ref 0 in
+
+  let graph = List.fold_right (fun (loop,ddg) graph ->
+      Printf.fprintf SPDebug.dc "__________________ NEW LOOP ____________________\n";
+      Printf.printf "Pipelinable loop: ";
+      incr lv;
+      fresh := (BinPos.Pos.succ
+                  (BinPos.Pos.succ
+                     (BinPos.Pos.succ
+                        (BinPos.Pos.succ
+                           (BinPos.Pos.succ
+                              (max_reg_of_graph graph (to_caml_list f.fn_params)
+                              ))))));
+      Printf.fprintf SPDebug.dc "FRESH = %i \n"
+        (P.to_int !fresh);
+      match p ddg with
+      | Some pipe ->
+        Printf.printf "Rock On ! Min = %i - Unroll = %i\n" pipe.min pipe.unrolling;
+        let p = (make_moves pipe.ramp_up) @ (delete_indexes pipe.prolog) in
+        let e = (delete_indexes pipe.epilog) @ (make_moves pipe.ramp_down) in
+        let b = delete_indexes (List.tl (List.rev loop)) in
+        let bt = (List.tl (delete_indexes pipe.steady_state)) in
+        let cond1 = fst (G.V.label (List.hd (List.rev loop))) in
+        let cond2 = (List.hd (delete_indexes pipe.steady_state)) in
+
+        let bu = symbolic_evaluation (repeat b (pipe.min + 1)) in
+        let pe = symbolic_evaluation (p @ e) in
+        let bte = symbolic_evaluation (bt @ e) in
+        let ebu = symbolic_evaluation (e @ repeat b pipe.unrolling) in
+        let regs = watch_regs pipe.ramp_down in
+        let c1 = symbolic_condition cond1 (repeat b pipe.unrolling) in
+        let d1 = symbolic_condition cond1 (repeat b (pipe.min + 1)) in
+        (*let c2 = symbolic_condition cond2 p in
+          let d2 = symbolic_condition cond2 ((make_moves pipe.ramp_up) @ bt) in*)
+
+
+
+        let sbt = symbolic_evaluation (bt) in
+        let sep = symbolic_evaluation (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) in (* er @ pr *)
+
+        Printf.printf "Initialisation : %s \n"
+          (if symbolic_equivalence bu pe regs then "OK" else "FAIL");
+        Printf.printf "Etat stable : %s \n"
+          (if symbolic_equivalence bte ebu regs then "OK" else "FAIL");
+        Printf.printf "Egalite fondamentale : %s \n"
+          (if symbolic_equivalence sbt sep (watch_regs pipe.ramp_up) then "OK" else "FAIL");
+        (*  Printf.printf "Condition initiale : %s \n"
+            (if c1 = c2 then "OK" else "FAIL");
+            Printf.printf "Condition stable : %s \n"
+            (if d1 = d2 then "OK" else "FAIL");
+
+
+            Printf.fprintf SPDebug.dc "pbte\n";*)
+        List.iter (fun e ->
+            Printf.fprintf SPDebug.dc "%s\n"
+              (string_of_node (G.V.create (e,0)))
+          ) (p @ bt @ e);
+        Printf.fprintf SPDebug.dc "bu\n";
+        List.iter (fun e -> Printf.fprintf SPDebug.dc "%s\n"
+                      (string_of_node (G.V.create (e,0)))
+                  ) (repeat b (pipe.unrolling + pipe.min));
+
+
+
+        if debug then
+          display_st ("pbte"^ (string_of_int !fv) ^ (string_of_int !lv)) (p @ bt @ e) (watch_regs pipe.ramp_down);
+        if debug then
+          display_st ("bu"^ (string_of_int !fv) ^ (string_of_int !lv)) (repeat b (pipe.min + pipe.unrolling)) (watch_regs pipe.ramp_down);
+
+        if debug then display_st ("bt"^ (string_of_int !fv) ^ (string_of_int !lv)) (bt) (watch_regs pipe.ramp_up);
+        if debug then display_st ("ep"^ (string_of_int !fv) ^ (string_of_int !lv)) (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) (watch_regs pipe.ramp_up);
+
+        substitute_pipeline graph loop
+          (delete_indexes pipe.steady_state) (delete_indexes pipe.prolog)
+          (delete_indexes pipe.epilog) (pipe.min + pipe.unrolling)
+          pipe.unrolling pipe.ramp_up
+          pipe.ramp_down
+          (to_caml_list f.fn_params)
+      | None -> Printf.printf "Damn It ! \n"; graph
+    ) ddgs cfg.graph in
+
+  if debug then display graph ("output"^ (string_of_int !fv));
+  let tg = convert_back graph in
+
+  let tg_to_type = {fn_sig = f.fn_sig; 
+                    fn_params = f.fn_params;
+                    fn_stacksize = f.fn_stacksize;
+                    fn_code = tg;
+                    fn_entrypoint = f.fn_entrypoint;
+                    (*fn_nextpc = P.of_int ((get_nextpc (graph)))*)
+                   } in
+  (*SPTyping.type_function tg_to_type;*)
+
+  tg_to_type
diff --git a/src/pipelining/SPBasic.mli b/src/pipelining/SPBasic.mli
new file mode 100644
index 0000000..f16e524
--- /dev/null
+++ b/src/pipelining/SPBasic.mli
@@ -0,0 +1,57 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open Graph.Pack.Digraph
+
+(* DATA DEPENDENCY GRAPHS *)
+module G : Graph.Sig.P 
+
+(* We abstract the register type to make sure that the user won't mess up *)
+type reg
+
+(* The scheduling should return a value of type pipeline *)
+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
+}
+
+(* Operations on ddg *)
+
+val display : G.t -> string -> unit
+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 *)
+
+val string_of_node : G.V.t -> string
+val latency : G.V.t -> int
+val reforge_reads : G.V.t -> reg -> reg -> G.V.t
+val reforge_writes : G.V.t -> reg -> G.V.t
+val written : G.V.t -> reg option
+val is_cond : G.V.t -> bool
+
+(* Operations on dependencies, the edges of the data dependency graph *)
+ 
+type et = IntraRAW | IntraWAW | IntraWAR | InterRAW | InterWAW | InterWAR
+
+val edge_type : G.E.t -> et
+val distance : G.E.t -> int
+
+(* Getting fresh registers, int is the number of required registers *)
+
+val fresh_regs : int -> reg array 
+val print_reg : reg -> unit
diff --git a/src/pipelining/SPDebug.ml b/src/pipelining/SPDebug.ml
new file mode 100644
index 0000000..34d1c0c
--- /dev/null
+++ b/src/pipelining/SPDebug.ml
@@ -0,0 +1,21 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open Unix
+
+let tm = localtime (time ());;
+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/pipelining/SPIMS.ml b/src/pipelining/SPIMS.ml
new file mode 100644
index 0000000..0e19dec
--- /dev/null
+++ b/src/pipelining/SPIMS.ml
@@ -0,0 +1,189 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open Graph.Pack.Digraph
+open SPBasic
+
+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
+
+let unpack v = 
+  match v with
+  | Some v -> v
+  | None -> failwith "unpack abusif"
+
+let dep_latency edge = 
+  match edge_type edge with
+  | 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
+  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
+
+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
+
+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
+  (* 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*)
+  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 []
+
+let get_condition ddg =
+  let cond = G.fold_vertex (fun node cond ->
+      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"
+
+(* Perform iterative modulo scheduling, using a heuristic for the next instruction to schedule
+ * [heightr], the data dependency graph to schedule [ddg], the minimum II [min_ii] and the maximum
+ * II [max_interval].
+ *)
+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
+
+  let cond = get_condition ddg in
+
+  while (!ii < max_interval && !notfound) do
+    (* Printf.printf "."; flush stdout;  *)
+    ii := !ii + 1;
+    (* Printf.printf "NOUVEAU II %i \n" !ii; *)
+    let budget = ref (G.nb_vertex ddg * 10) in
+    let lasttime = ref NI.empty in
+    (* Create the map with schedules, and add the schedule for the condition.  This should go at the
+     * end, but in this case is set to the start. *)
+    let schedtime = ref (NI.add cond (Some 0) NI.empty) in
+    (* Create an array that is as large as the current II, which will determine where each
+     * instruction will be placed. *)
+    let mrt = Array.make !ii None in
+    (* Set the condition to be the initial instruction at time 0. *)
+    Array.set mrt 0 (Some cond);
+
+    while (!budget > 0 && not (finished ddg !schedtime)) do (* Pretty inefficient *)
+      budget := !budget - 1;
+      (* Get next instruction to schedule. *)
+      let h = heightr ddg !schedtime in
+      let mintime = estart ddg !schedtime h !ii in
+      (* 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)
+      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
+      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
+
+    if success then (notfound := false; sched := !schedtime);
+
+  done;
+
+  if (not !notfound) 
+  then (!sched,!ii)
+  else failwith "IMS failure"
+
+(* Take the number of vertices as the minimum resource-constrained II.  However, the II might
+   actually be less than that in some cases, so this should be adjusted accordingly. *)
+let res_m_ii ddg =
+  G.nb_vertex ddg
+
+let pipeliner ddg heightr =
+  let mii = res_m_ii ddg in
+  Printf.fprintf SPDebug.dc "MII: %i\n" mii;
+  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)
+
+let print_schedule sched =
+  NI.iter (fun node time ->
+      Printf.fprintf SPDebug.dc "%s |---> %i \n" (string_of_node node) time
+    ) sched
diff --git a/src/pipelining/SPIMS.mli b/src/pipelining/SPIMS.mli
new file mode 100644
index 0000000..7c1d9a7
--- /dev/null
+++ b/src/pipelining/SPIMS.mli
@@ -0,0 +1,22 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open Graph.Pack.Digraph
+open SPBasic
+
+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 *)
+val pipeliner : G.t -> (G.t -> int option NI.t -> G.V.t) -> int NI.t * int
+
+val print_schedule : int NI.t -> unit
diff --git a/src/pipelining/SPMVE.ml b/src/pipelining/SPMVE.ml
new file mode 100644
index 0000000..28381c1
--- /dev/null
+++ b/src/pipelining/SPMVE.ml
@@ -0,0 +1,299 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+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
+
+let size_of_map2 m = 
+  Mult.fold (fun key v size -> size + 1) m 0
+
+let sched_max_time sched = 
+  NI.fold (fun node time max ->
+      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 -> "_"
+  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
+
+let minimizer qi ur =
+
+  let rec fill n = 
+    if n <= ur then n :: fill (n + 1) else []
+  in
+
+  let l = fill qi in
+  let l = List.map (fun e -> (e,ur mod e)) l in
+  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; *)
+  let unroll = Mult.fold (fun reg mult max ->
+      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
+  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
+    Array.iter print_reg  fregs;
+    Printf.fprintf SPDebug.dc "\n";
+    Array.set regs i fregs
+  done;
+
+  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 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"
+  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;
+  (* 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 steady = Array.make (ii * ur) None in
+  for i = 0 to (ur - 1) do
+    for time = 0 to (ii - 1) do
+      Array.set steady (time + i * ii) (steady_s.(time)) 
+    done
+  done;
+  steady
+
+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;
+  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"
+    done;
+
+    prolog := List.rev (!prolog_piece) @ !prolog
+  done;
+
+  !prolog
+
+
+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"
+    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
+  in
+
+  way_out_rec l []
+
+let mve ddg sched ii =
+  assert (size_of_map1 sched = G.nb_vertex ddg);
+  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 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 SPDebug.dc "min : %i \n" min;
+  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;
+  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 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/pipelining/SPMVE.mli b/src/pipelining/SPMVE.mli
new file mode 100644
index 0000000..2da367d
--- /dev/null
+++ b/src/pipelining/SPMVE.mli
@@ -0,0 +1,17 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+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/pipelining/SPSymbolic_evaluation.ml b/src/pipelining/SPSymbolic_evaluation.ml
new file mode 100644
index 0000000..c99afc8
--- /dev/null
+++ b/src/pipelining/SPSymbolic_evaluation.ml
@@ -0,0 +1,226 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open Registers
+open Op
+open AST
+open SPBase_types
+open Camlcoq
+
+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
+
+module State = Map.Make (struct type t = reg let compare = compare end)
+
+module Cons = Set.Make (struct type t = symbolic_value let compare = compare end)
+
+type symbolic_state = symbolic_value State.t * Cons.t
+
+let initial_state = State.empty 
+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
+
+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
+
+  | 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
+
+  | 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
+
+  | 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
+
+  | _ :: l -> raise Not_straight
+
+type osv =
+  | Oresource of resource
+  | Oop of operation 
+  | Oload of memory_chunk * addressing 
+  | Ostore of memory_chunk * addressing 
+
+let string_of_osv = function
+  | Oresource (Reg r) -> Printf.sprintf "reg %i" (P.to_int r)
+  | Oresource Mem -> "mem" 
+  | Oop op -> string_of_op op
+  | Oload (mc,addr) -> "load" 
+  | Ostore (mc,addr) -> "store"
+
+type ident = int
+
+module S = Graph.Persistent.Digraph.Abstract
+    (struct type t = osv * ident end)
+
+let name_of_vertex v = 
+  let (osv,id) = S.V.label v in
+  Printf.sprintf "%i" id 
+
+let string_of_vertex v = 
+  let (osv,_) = S.V.label v in
+  Printf.sprintf "%s" (string_of_osv osv)
+
+module DisplayTree = struct
+  include S
+  let vertex_name v =  name_of_vertex v
+  let graph_attributes _ = [] 
+  let default_vertex_attributes _ = []
+  let vertex_attributes v = [`Label (string_of_vertex v)]
+  let default_edge_attributes _ = []
+  let edge_attributes _ = []
+  let get_subgraph _ = None
+end
+module DotTree = Graph.Graphviz.Dot(DisplayTree)
+
+let dot_output_ss g f = 
+  let oc = open_out f in
+  DotTree.output_graph oc g; 
+  close_out oc
+
+module Build = Graph.Builder.P (S)
+module Op = Graph.Oper.Make (Build)
+
+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)
+
+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)
+
+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
+  in 
+  let graph' = 
+    let (graph,head) = convert_sm sm in
+    incr counter;
+    let src = S.V.create (Oresource Mem, !counter) in
+    let graph = S.add_vertex graph src in
+    let graph = S.add_edge graph src head in
+    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)
+
+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"
diff --git a/src/pipelining/SPTyping.ml b/src/pipelining/SPTyping.ml
new file mode 100644
index 0000000..9b9c679
--- /dev/null
+++ b/src/pipelining/SPTyping.ml
@@ -0,0 +1,526 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+(*open Datatypes
+open List
+open Camlcoq
+open Maps
+open AST
+open Op
+open Registers
+open RTL
+
+open Conventions
+open Coqlib
+open Errors
+open Specif
+
+exception Type_error of string
+
+let env = ref (PTree.empty : typ PTree.t)
+
+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 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
+  | [], [] -> ()
+  | 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 (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 (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)
+  | Istore(chunk, addr, args, src, _) ->
+      set_types args (type_of_addressing addr);
+      set_type src (type_of_chunk chunk)
+  | Icall(sg, ros, args, res, _) ->
+      begin try
+        begin match ros with
+        | Coq_inl r -> set_type r Tint
+        | Coq_inr _ -> ()
+        end;
+        set_types args sg.sig_args;
+        set_type res (match sg.sig_res with Tret t -> t | _ -> Tint);
+      with Type_error msg ->
+        let name =
+          match ros with
+          | Coq_inl _ -> "<reg>"
+          | Coq_inr id -> extern_atom id in
+        raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s"
+                                         name msg))
+      end
+  | Itailcall(sg, ros, args) ->
+      begin try
+        begin match ros with
+        | Coq_inl r -> set_type r Tint
+        | Coq_inr _ -> ()
+        end;
+        set_types args sg.sig_args;
+        if sg.sig_res <> retty then
+          raise (Type_error "mismatch on return type")
+      with Type_error msg ->
+        let name =
+          match ros with
+          | Coq_inl _ -> "<reg>"
+          | Coq_inr id -> extern_atom id in
+        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*)
+  | Icond(cond, args, _, _) ->
+      set_types args (type_of_condition cond)
+  | Ireturn(optres) ->
+      begin match optres, retty with
+      | None, Tvoid -> ()
+      | Some r, Tret ty -> set_type r ty
+      | _, _ -> raise (Type_error "type mismatch in Ireturn")
+      end
+
+let type_pass1 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
+  | [] -> []
+  | (pc, i) :: rem ->
+      match i with
+      | Iop(Omove, [r1], r2, _) ->
+          (r1, r2) :: extract_moves rem
+      | Iop(Omove, _, _, _) ->
+          raise (Type_error "wrong Omove")
+      | _ ->
+          extract_moves rem
+
+let changed = ref false
+
+let rec solve_moves = function
+  | [] -> []
+  | (r1, r2) :: rem ->
+      match (PTree.get r1 !env, PTree.get r2 !env) with
+      | Some ty1, Some ty2 ->
+          if ty1 = ty2 
+          then (changed := true; solve_moves rem)
+          else raise (Type_error "type mismatch in Omove")
+      | Some ty1, None ->
+          env := PTree.set r2 ty1 !env; changed := true; solve_moves rem
+      | None, Some ty2 ->
+          env := PTree.set r1 ty2 !env; changed := true; solve_moves rem
+      | None, None ->
+          (r1, r2) :: solve_moves rem
+
+let rec iter_solve_moves mvs =
+  changed := false;
+  let mvs' = solve_moves mvs in
+  if !changed then iter_solve_moves mvs'
+
+let type_pass2 instrs =
+  iter_solve_moves (extract_moves instrs)
+
+let typeof e r =
+  match PTree.get r e with Some ty -> ty | None -> Tint
+
+let infer_type_environment f instrs =
+  try
+    env := PTree.empty;
+    set_types f.fn_params f.fn_sig.sig_args;
+    type_pass1 f.fn_sig.sig_res instrs;
+    type_pass2 instrs;
+    let e = !env in
+    env := PTree.empty;
+    Some(typeof e)
+  with Type_error msg ->
+    Printf.eprintf "Error during RTL type inference: %s\n" msg;
+    None
+
+(** val typ_eq : typ -> typ -> bool **)
+
+let typ_eq t1 t2 =
+  match t1 with
+    | Tint -> (match t2 with
+                 | Tint -> true
+                 | Tfloat -> false)
+    | Tfloat -> (match t2 with
+                   | Tint -> false
+                   | Tfloat -> true)
+
+(** val opt_typ_eq : typ option -> typ option -> bool **)
+
+let opt_typ_eq t1 t2 =
+  match t1 with
+    | Some x -> (match t2 with
+                   | Some t -> typ_eq x t
+                   | None -> false)
+    | None -> (match t2 with
+                 | Some t -> false
+                 | None -> true)
+
+(** val check_reg : regenv -> reg -> typ -> bool **)
+
+let check_reg env r ty =
+  match typ_eq (env r) ty with
+    | true -> true
+    | false -> false
+
+(** val check_regs : regenv -> reg list -> typ list -> bool **)
+
+let rec check_regs env rl tyl =
+  match rl with
+    | [] ->
+        (match tyl with
+           | [] -> true
+           | (t :: l) -> false)
+    | r1 :: rs ->
+        (match tyl with
+           | [] -> false
+           | (ty :: tys) ->
+               (match typ_eq (env r1) ty with
+                  | true -> check_regs env rs tys
+                  | false -> false))
+
+(** val check_op : regenv -> operation -> reg list -> reg -> bool **)
+
+let check_op env op args res0 =
+  let (targs, tres) = type_of_operation op in
+  (match check_regs env args targs with
+     | true ->
+         (match typ_eq (env res0) tres with
+            | true -> true
+            | false -> false)
+     | false -> false)
+
+(** val check_successor : coq_function -> node -> bool **)
+
+let check_successor funct s =
+  match Maps.PTree.get s funct.fn_code with
+    | Some i -> true
+    | None -> false
+
+(** val check_instr : coq_function -> regenv -> instruction -> bool **)
+
+let check_instr funct env = function
+  | Inop s -> check_successor funct s
+  | Iop (op, args, res0, s) ->
+      (match op with
+         | Omove ->
+             (match args with
+                | Coq_nil -> false
+                | Coq_cons (arg, l) ->
+                    (match l with
+                       | Coq_nil ->
+                           (match typ_eq (env arg) (env res0) with
+                              | true -> check_successor funct s
+                              | false -> false)
+                       | Coq_cons (r, l0) -> false))
+         | Ointconst i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ofloatconst f ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+(*         | Oaddrsymbol (i0, i1) ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)*)
+(*         | Oaddrstack i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)*)
+         | Ocast8signed ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ocast8unsigned ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ocast16signed ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ocast16unsigned ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+(*         | 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)*)
+         | Osub ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Osubimm i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Omul ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Omulimm i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Odiv ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Odivu ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oand ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oandimm i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oor ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oorimm i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oxor ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oxorimm i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Onand ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Onor ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Onxor ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oshl ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oshr ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oshrimm i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oshrximm i0 ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oshru ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Orolm (i0, i1) ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Onegf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oabsf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Oaddf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Osubf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Omulf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Odivf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Omuladdf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Omulsubf ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Osingleoffloat ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ointoffloat ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ointuoffloat ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ofloatofint ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ofloatofintu ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false)
+         | Ocmp c ->
+             (match check_op env op args res0 with
+                | true -> check_successor funct s
+                | false -> false))
+  | Iload (chunk, addr, args, dst, s) ->
+      (match check_regs env args (type_of_addressing addr) with
+         | true ->
+             (match typ_eq (env dst) (type_of_chunk chunk) with
+                | true -> check_successor funct s
+                | false -> false)
+         | false -> false)
+  | Istore (chunk, addr, args, src, s) ->
+      (match check_regs env args (type_of_addressing addr) with
+         | true ->
+             (match typ_eq (env src) (type_of_chunk chunk) with
+                | true -> check_successor funct s
+                | false -> false)
+         | false -> false)
+  | Icall (sig0, ros, args, res0, s) ->
+      (match match ros with
+               | Coq_inl r ->
+                   (match typ_eq (env r) Tint with
+                      | true -> check_regs env args sig0.sig_args
+                      | false -> false)
+               | Coq_inr s0 -> check_regs env args sig0.sig_args with
+         | true ->
+             (match typ_eq (env res0) (proj_sig_res sig0) with
+                | true -> check_successor funct s
+                | false -> false)
+         | false -> false)
+  | Itailcall (sig0, ros, args) ->
+      (match match match ros with
+                     | Coq_inl r ->
+                         (match typ_eq (env r) Tint with
+                            | true -> check_regs env args sig0.sig_args
+                            | false -> false)
+                     | Coq_inr s -> check_regs env args sig0.sig_args with
+               | true ->
+                   proj_sumbool
+                     (opt_typ_eq sig0.sig_res funct.fn_sig.sig_res)
+               | false -> false with
+         | true -> tailcall_is_possible sig0
+         | false -> false)
+(*  | 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)*)
+  | Icond (cond, args, s1, s2) ->
+      (match match check_regs env args (type_of_condition cond) with
+               | true -> check_successor funct s1
+               | false -> false with
+         | true -> check_successor funct s2
+         | false -> false)
+  | Ireturn optres ->
+      (match optres with
+         | Some r ->
+             (match funct.fn_sig.sig_res with
+                | Some t ->
+                    (match typ_eq (env r) t with
+                       | true -> true
+                       | false -> false)
+                | None -> false)
+         | None ->
+             (match funct.fn_sig.sig_res with
+                | Some t -> false
+                | None -> true))
+
+(** val check_params_norepet : reg list -> bool **)
+
+let check_params_norepet params =
+  match list_norepet_dec Registers.Reg.eq params with
+    | true -> true
+    | false -> false
+
+(** val check_instrs : coq_function -> regenv -> (node, instruction) prod
+                       list -> bool **)
+
+let rec check_instrs funct env = function
+  | Coq_nil -> true
+  | Coq_cons (p, rem) ->
+      let Coq_pair (pc, i) = p in
+      (match check_instr funct env i with
+         | true -> check_instrs funct env rem
+         | false -> false)
+
+(** val type_function : coq_function -> unit **)
+
+let type_function f =
+  let instrs = Maps.PTree.elements f.fn_code in
+  match infer_type_environment f instrs with
+    | Some env ->
+        (match match match match check_regs env f.fn_params
+           f.fn_sig.sig_args with
+             | true -> check_params_norepet f.fn_params
+             | false -> false with
+                 | true -> check_instrs f env instrs
+                 | 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")
+    | None -> failwith "Type inference failure\n"
+*)
diff --git a/src/pipelining/SPTyping.mli b/src/pipelining/SPTyping.mli
new file mode 100644
index 0000000..dd27875
--- /dev/null
+++ b/src/pipelining/SPTyping.mli
@@ -0,0 +1,14 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+
+(*val type_function : RTL.coq_function -> unit*)
diff --git a/src/pipelining/SoftwarePipelining.ml b/src/pipelining/SoftwarePipelining.ml
new file mode 100644
index 0000000..0ba6d9d
--- /dev/null
+++ b/src/pipelining/SoftwarePipelining.ml
@@ -0,0 +1,74 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open SPBasic
+open SPIMS
+open SPMVE
+open RTL
+
+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
+  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
+
+(* A random heuristic is used to pick the next instruction to be scheduled from the unscheduled
+ * instructions.  The scheduled instructions are given to the function, and the unscheduled
+ * instructions are created by taking all the instructions that are not in the scheduled list.
+ *)
+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
+  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)
+
+let order = ref []
+
+let pipeliner ddg =
+  order := List.flatten (Scc.scc_list ddg);
+  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
+    Some {steady_state = steady_state; prolog = prolog; epilog = epilog; min = min; unrolling = unroll;
+          ramp_up = entrance; ramp_down = way_out}
+
+
+let pipeline f =
+  SPBasic.apply_pipeliner f pipeliner ~debug:false