Revert "Remove more OCaml files to compile successfully without admits."

This reverts commit 9a4122dba9bdc33a8e912d5a45bae35e05afb229.

5 files changed, 1085 insertions, 0 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 1ea580f..aa5309a 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -65,6 +65,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintClight.destination option_dclight ".light.c";
   set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
+  set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
new file mode 100644
index 0000000..19c6048
--- /dev/null
+++ b/src/hls/Partition.ml
@@ -0,0 +1,124 @@
+ (*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+open Printf
+open Clflags
+open Camlcoq
+open Datatypes
+open Coqlib
+open Maps
+open AST
+open Kildall
+open Op
+open RTLBlockInstr
+open RTLBlock
+
+(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
+   [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *)
+let find_edge i n =
+  let succ = RTL.successors_instr i in
+  let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in
+  ((match filt with [] -> [] | _ -> [n]), filt)
+
+let find_edges c =
+  PTree.fold (fun l n i ->
+      let f = find_edge i n in
+      (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], [])
+
+let prepend_instr i = function
+  | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
+
+let translate_inst = function
+  | RTL.Inop _ -> Some RBnop
+  | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst))
+  | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst))
+  | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src))
+  | _ -> None
+
+let translate_cfi = function
+  | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n))
+  | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls))
+  | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n))
+  | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2))
+  | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls))
+  | RTL.Ireturn r -> Some (RBreturn r)
+  | _ -> None
+
+let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
+  let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in
+  let trans_inst = (translate_inst i, translate_cfi i) in
+  match trans_inst, succ with
+  | (None, Some i'), _ ->
+    if List.exists (fun x -> x = s) (snd e) && not is_start then
+      Errors.OK { bb_body = []; bb_exit = RBgoto s }
+    else
+      Errors.OK { bb_body = []; bb_exit = i' }
+  | (Some i', None), (s', Some i_n)::[] ->
+    if List.exists (fun x -> x = s) (fst e) then
+      Errors.OK { bb_body = [i']; bb_exit = RBgoto s' }
+    else if List.exists (fun x -> x = s) (snd e) && not is_start then
+      Errors.OK { bb_body = []; bb_exit = RBgoto s }
+    else begin
+      match next_bblock_from_RTL false e c s' i_n with
+      | Errors.OK bb ->
+        Errors.OK (prepend_instr i' bb)
+      | Errors.Error msg -> Errors.Error msg
+    end
+  | _, _ ->
+    Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong."))
+
+let rec traverseacc f l c =
+  match l with
+  | [] -> Errors.OK c
+  | x::xs ->
+    match f x c with
+    | Errors.Error msg -> Errors.Error msg
+    | Errors.OK x' ->
+      match traverseacc f xs x' with
+      | Errors.Error msg -> Errors.Error msg
+      | Errors.OK xs' -> Errors.OK xs'
+
+let rec translate_all edge c s res =
+  let c_bb, translated = res in
+  if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else
+    (match PTree.get s c with
+     | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all."))
+     | Some i ->
+       match next_bblock_from_RTL true edge c s i with
+       | Errors.Error msg -> Errors.Error msg
+       | Errors.OK {bb_body = bb; bb_exit = e} ->
+         let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in
+         (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with
+          | Errors.Error msg -> Errors.Error msg
+          | Errors.OK (c', t') ->
+            Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t')))
+
+(* Partition a function and transform it into RTLBlock. *)
+let function_from_RTL f =
+  let e = find_edges f.RTL.fn_code in
+  match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with
+  | Errors.Error msg -> Errors.Error msg
+  | Errors.OK (c, _) ->
+    Errors.OK { fn_sig = f.RTL.fn_sig;
+                fn_stacksize = f.RTL.fn_stacksize;
+                fn_params = f.RTL.fn_params;
+                fn_entrypoint = f.RTL.fn_entrypoint;
+                fn_code = c
+              }
+
+let partition = function_from_RTL
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
new file mode 100644
index 0000000..8fef401
--- /dev/null
+++ b/src/hls/PrintRTLBlock.ml
@@ -0,0 +1,72 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printers for RTL code *)
+
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlockInstr
+open RTLBlock
+open PrintAST
+open PrintRTLBlockInstr
+
+(* Printing of RTL code *)
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_bblock pp (pc, i) =
+  fprintf pp "%5d:{\n" pc;
+  List.iter (print_bblock_body pp) i.bb_body;
+  print_bblock_exit pp i.bb_exit;
+  fprintf pp "\t}\n\n"
+
+let print_function pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+  let instrs =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.fn_code)) in
+  List.iter (print_bblock pp) instrs;
+  fprintf pp "}\n\n"
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_function pp id f
+  | _ -> ()
+
+let print_program pp (prog: program) =
+  List.iter (print_globdef pp) prog.prog_defs
+
+let destination : string option ref = ref None
+
+let print_if passno prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+     let oc = open_out (f ^ "." ^ Z.to_string passno) in
+     print_program oc prog;
+     close_out oc
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
new file mode 100644
index 0000000..ba7241b
--- /dev/null
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -0,0 +1,87 @@
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlockInstr
+open PrintAST
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let pred pp r =
+  fprintf pp "p%d" (Nat.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let rec print_pred_op pp = function
+  | Pvar p -> pred pp p
+  | Pnot p -> fprintf pp "(~ %a)" print_pred_op p
+  | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2
+  | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2
+
+let print_pred_option pp = function
+  | Some x -> fprintf pp "(%a)" print_pred_op x
+  | None -> ()
+
+let print_bblock_body pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBnop -> fprintf pp "nop\n"
+  | RBop(p, op, ls, dst) ->
+     fprintf pp "%a %a = %a\n"
+       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
+  | RBload(p, chunk, addr, args, dst) ->
+     fprintf pp "%a %a = %s[%a]\n"
+       print_pred_option p reg dst (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+  | RBstore(p, chunk, addr, args, src) ->
+     fprintf pp "%a %s[%a] = %a\n"
+       print_pred_option p
+       (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+       reg src
+  | RBsetpred (c, args, p) ->
+    fprintf pp "%a = %a\n"
+      pred p
+      (PrintOp.print_condition reg) (c, args)
+
+let rec print_bblock_exit pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBcall(_, fn, args, res, _) ->
+      fprintf pp "%a = %a(%a)\n"
+        reg res ros fn regs args;
+  | RBtailcall(_, fn, args) ->
+      fprintf pp "tailcall %a(%a)\n"
+        ros fn regs args
+  | RBbuiltin(ef, args, res, _) ->
+      fprintf pp "%a = %s(%a)\n"
+        (print_builtin_res reg) res
+        (name_of_external ef)
+        (print_builtin_args reg) args
+  | RBcond(cond, args, s1, s2) ->
+      fprintf pp "if (%a) goto %d else goto %d\n"
+        (PrintOp.print_condition reg) (cond, args)
+        (P.to_int s1) (P.to_int s2)
+  | RBjumptable(arg, tbl) ->
+      let tbl = Array.of_list tbl in
+      fprintf pp "jumptable (%a)\n" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
+  | RBreturn None ->
+      fprintf pp "return\n"
+  | RBreturn (Some arg) ->
+      fprintf pp "return %a\n" reg arg
+  | RBgoto n ->
+     fprintf pp "goto %d\n" (P.to_int n)
+  | RBpred_cf (p, c1, c2) ->
+    fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
new file mode 100644
index 0000000..c6c8bf4
--- /dev/null
+++ b/src/hls/Schedule.ml
@@ -0,0 +1,801 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+open Printf
+open Clflags
+open Camlcoq
+open Datatypes
+open Coqlib
+open Maps
+open AST
+open Kildall
+open Op
+open RTLBlockInstr
+open RTLBlock
+open HTL
+open Verilog
+open HTLgen
+open HTLMonad
+open HTLMonadExtra
+
+module SS = Set.Make(P)
+
+type svtype =
+  | BBType of int
+  | VarType of int * int
+
+type sv = {
+  sv_type: svtype;
+  sv_num: int;
+}
+
+let print_sv v =
+  match v with
+  | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n
+  | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n
+
+module G = Graph.Persistent.Digraph.ConcreteLabeled(struct
+  type t = sv
+  let compare = compare
+  let equal = (=)
+  let hash = Hashtbl.hash
+end)(struct
+  type t = int
+  let compare = compare
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let default = 0
+end)
+
+module GDot = Graph.Graphviz.Dot(struct
+    let graph_attributes _ = []
+    let default_vertex_attributes _ = []
+    let vertex_name = print_sv
+    let vertex_attributes _ = []
+    let get_subgraph _ = None
+    let default_edge_attributes _ = []
+    let edge_attributes _ = []
+
+    include G
+  end)
+
+module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct
+  type t = int * instr
+  let compare = compare
+  let equal = (=)
+  let hash = Hashtbl.hash
+end)(struct
+  type t = int
+  let compare = compare
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let default = 0
+end)
+
+let reg r = sprintf "r%d" (P.to_int r)
+let print_pred r = sprintf "p%d" (Nat.to_int r)
+
+let print_instr = function
+  | RBnop -> ""
+  | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r)
+  | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r)
+  | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p)
+  | RBop (_, op, args, d) ->
+    (match op, args with
+    | Omove, _ -> "mov"
+    | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n)
+    | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n)
+    | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n)
+    | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n)
+    | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id)
+    | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1)
+    | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1)
+    | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1)
+    | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1)
+    | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1)
+    | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2)
+    | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2)
+    | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2)
+    | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2)
+    | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2)
+    | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2)
+    | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2)
+    | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2)
+    | Oorimm n, [r1] ->  sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2)
+    | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1)
+    | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2)
+    | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2)
+    | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2)
+    | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n)
+    | Olea addr, args -> sprintf "%s=addr" (reg d)
+    | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1)
+    | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1)
+    | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1)
+    | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1)
+    | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1)
+    | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2)
+    | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2)
+    | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2)
+    | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2)
+    | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2)
+    | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2)
+    | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2)
+    | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2)
+    | Oorlimm n, [r1] ->  sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2)
+    | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1)
+    | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2)
+    | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2)
+    | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2)
+    | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oleal addr, args -> sprintf "%s=addr" (reg d)
+    | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1)
+    | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1)
+    | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2)
+    | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2)
+    | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2)
+    | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2)
+    | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1)
+    | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1)
+    | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2)
+    | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2)
+    | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2)
+    | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2)
+    | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1)
+    | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1)
+    | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1)
+    | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1)
+    | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1)
+    | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1)
+    | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1)
+    | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1)
+    | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1)
+    | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1)
+    | Ocmp c, args -> sprintf "%s=cmp" (reg d)
+    | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d)
+    | _, _ -> sprintf "N/a")
+
+module DFGDot = Graph.Graphviz.Dot(struct
+    let graph_attributes _ = []
+    let default_vertex_attributes _ = []
+    let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr)
+    let vertex_attributes _ = []
+    let get_subgraph _ = None
+    let default_edge_attributes _ = []
+    let edge_attributes _ = []
+
+    include DFG
+  end)
+
+module IMap = Map.Make (struct
+  type t = int
+
+  let compare = compare
+end)
+
+let gen_vertex instrs i = (i, List.nth instrs i)
+
+(** The DFG type defines a list of instructions with their data dependencies as [edges], which are
+   the pairs of integers that represent the index of the instruction in the [nodes].  The edges
+   always point from left to right. *)
+
+let print_list f out_chan a =
+  fprintf out_chan "[ ";
+  List.iter (fprintf out_chan "%a " f) a;
+  fprintf out_chan "]"
+
+let print_tuple out_chan a =
+  let l, r = a in
+  fprintf out_chan "(%d,%d)" l r
+
+(*let print_dfg out_chan dfg =
+  fprintf out_chan "{ nodes = %a, edges = %a }"
+    (print_list PrintRTLBlockInstr.print_bblock_body)
+    dfg.nodes (print_list print_tuple) dfg.edges*)
+
+let print_dfg = DFGDot.output_graph
+
+let read_process command =
+  let buffer_size = 2048 in
+  let buffer = Buffer.create buffer_size in
+  let string = Bytes.create buffer_size in
+  let in_channel = Unix.open_process_in command in
+  let chars_read = ref 1 in
+  while !chars_read <> 0 do
+    chars_read := input in_channel string 0 buffer_size;
+    Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read
+  done;
+  ignore (Unix.close_process_in in_channel);
+  Buffer.contents buffer
+
+let comb_delay = function
+  | RBnop -> 0
+  | RBop (_, op, _, _) ->
+    (match op with
+     | Omove -> 0
+     | Ointconst _ -> 0
+     | Olongconst _ -> 0
+     | Ocast8signed -> 0
+     | Ocast8unsigned -> 0
+     | Ocast16signed -> 0
+     | Ocast16unsigned -> 0
+     | Oneg -> 0
+     | Onot -> 0
+     | Oor -> 0
+     | Oorimm _ -> 0
+     | Oand -> 0
+     | Oandimm _ -> 0
+     | Oxor -> 0
+     | Oxorimm _ -> 0
+     | Omul -> 8
+     | Omulimm _ -> 8
+     | Omulhs -> 8
+     | Omulhu -> 8
+     | Odiv -> 72
+     | Odivu -> 72
+     | Omod -> 72
+     | Omodu -> 72
+     | _ -> 1)
+  | _ -> 1
+
+let pipeline_stages = function
+  | RBop (_, op, _, _) ->
+    (match op with
+     | Odiv -> 32
+     | Odivu -> 32
+     | Omod -> 32
+     | Omodu -> 32
+     | _ -> 0)
+  | _ -> 0
+
+(** Add a dependency if it uses a register that was written to previously. *)
+let add_dep map i tree dfg curr =
+  match PTree.get curr tree with
+  | None -> dfg
+  | Some ip ->
+    let ipv = (List.nth map ip) in
+    DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i)
+
+(** This function calculates the dependencies of each instruction.  The nodes correspond to previous
+   registers that were allocated and show which instruction caused it.
+
+   This function only gathers the RAW constraints, and will therefore only be active for operations
+   that modify registers, which is this case only affects loads and operations. *)
+let accumulate_RAW_deps map dfg curr =
+  let i, dst_map, graph = dfg in
+  let acc_dep_instruction rs dst =
+    ( i + 1,
+      PTree.set dst i dst_map,
+      List.fold_left (add_dep map i dst_map) graph rs
+    )
+  in
+  let acc_dep_instruction_nodst rs =
+    ( i + 1,
+      dst_map,
+    List.fold_left (add_dep map i dst_map) graph rs)
+  in
+  match curr with
+  | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst
+  | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst
+  | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
+  | _ -> (i + 1, dst_map, graph)
+
+(** Finds the next write to the [dst] register.  This is a small optimisation so that only one
+   dependency is generated for a data dependency. *)
+let rec find_next_dst_write i dst i' curr =
+  let check_dst dst' curr' =
+    if dst = dst' then Some (i, i')
+    else find_next_dst_write i dst (i' + 1) curr'
+  in
+  match curr with
+  | [] -> None
+  | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr'
+  | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr'
+  | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr'
+
+let rec find_all_next_dst_read i dst i' curr =
+  let check_dst rs curr' =
+    if List.exists (fun x -> x = dst) rs
+    then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr'
+    else find_all_next_dst_read i dst (i' + 1) curr'
+  in
+  match curr with
+  | [] -> []
+  | RBop (_, _, rs, _) :: curr' -> check_dst rs curr'
+  | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr'
+  | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
+  | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
+  | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr'
+
+let drop i lst =
+  let rec drop' i' lst' =
+    match lst' with
+    | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls
+    | [] -> []
+  in
+  if i = 0 then lst else drop' 1 lst
+
+let take i lst =
+  let rec take' i' lst' =
+    match lst' with
+    | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls
+    | [] -> []
+  in
+  if i = 0 then [] else take' 1 lst
+
+let rec next_store i = function
+  | [] -> None
+  | RBstore (_, _, _, _, _) :: _ -> Some i
+  | _ :: rst -> next_store (i + 1) rst
+
+let rec next_load i = function
+  | [] -> None
+  | RBload (_, _, _, _, _) :: _ -> Some i
+  | _ :: rst -> next_load (i + 1) rst
+
+let accumulate_RAW_mem_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBload (_, _, _, _, _) -> (
+      match next_store 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAR_mem_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBstore (_, _, _, _, _) -> (
+      match next_load 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAW_mem_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBstore (_, _, _, _, _) -> (
+      match next_store 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+(** Predicate dependencies. *)
+
+let rec in_predicate p p' =
+  match p' with
+  | Pvar p'' -> Nat.to_int p = Nat.to_int p''
+  | Pnot p'' -> in_predicate p p''
+  | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
+  | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
+
+let get_predicate = function
+  | RBop (p, _, _, _) -> p
+  | RBload (p, _, _, _, _) -> p
+  | RBstore (p, _, _, _, _) -> p
+  | _ -> None
+
+let rec next_setpred p i = function
+  | [] -> None
+  | RBsetpred (_, _, p') :: rst ->
+    if in_predicate p' p then
+      Some i
+    else
+      next_setpred p (i + 1) rst
+  | _ :: rst -> next_setpred p (i + 1) rst
+
+let rec next_preduse p i instr=
+  let next p' rst =
+    if in_predicate p p' then
+      Some i
+    else
+      next_preduse p (i + 1) rst
+  in
+  match instr with
+  | [] -> None
+  | RBload (Some p', _, _, _, _) :: rst -> next p' rst
+  | RBstore (Some p', _, _, _, _) :: rst -> next p' rst
+  | RBop (Some p', _, _, _) :: rst -> next p' rst
+  | _ :: rst -> next_load (i + 1) rst
+
+let accumulate_RAW_pred_deps instrs dfg curri =
+  let i, curr = curri in
+  match get_predicate curr with
+  | Some p -> (
+      match next_setpred p 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAR_pred_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBsetpred (_, _, p) -> (
+      match next_preduse p 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAW_pred_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBsetpred (_, _, p) -> (
+      match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+(** This function calculates the WAW dependencies, which happen when two writes are ordered one
+   after another and therefore have to be kept in that order.  This accumulation might be redundant
+   if register renaming is done before hand, because then these dependencies can be avoided. *)
+let accumulate_WAW_deps instrs dfg curri =
+  let i, curr = curri in
+  let dst_dep dst =
+    match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with
+    | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b)
+    | _ -> dfg
+  in
+  match curr with
+  | RBop (_, _, _, dst) -> dst_dep dst
+  | RBload (_, _, _, _, dst) -> dst_dep dst
+  | RBstore (_, _, _, _, _) -> (
+      match next_store (i + 1) (drop (i + 1) instrs) with
+      | None -> dfg
+      | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') )
+  | _ -> dfg
+
+let accumulate_WAR_deps instrs dfg curri =
+  let i, curr = curri in
+  let dst_dep dst =
+    let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev)
+        |> List.map (function (d, d') -> (i - d' - 1, d))
+    in
+    List.fold_left (fun g ->
+        function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list
+  in
+  match curr with
+  | RBop (_, _, _, dst) -> dst_dep dst
+  | RBload (_, _, _, _, dst) -> dst_dep dst
+  | _ -> dfg
+
+let assigned_vars vars = function
+  | RBnop -> vars
+  | RBop (_, _, _, dst) -> dst :: vars
+  | RBload (_, _, _, _, dst) -> dst :: vars
+  | RBstore (_, _, _, _, _) -> vars
+  | RBsetpred (_, _, _) -> vars
+
+let get_pred = function
+  | RBnop -> None
+  | RBop (op, _, _, _) -> op
+  | RBload (op, _, _, _, _) -> op
+  | RBstore (op, _, _, _, _) -> op
+  | RBsetpred (_, _, _) -> None
+
+let independant_pred p p' =
+  match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with
+  | Some None -> true
+  | _ -> false
+
+let check_dependent op1 op2 =
+  match op1, op2 with
+  | Some p, Some p' -> not (independant_pred p p')
+  | _, _ -> true
+
+let remove_unnecessary_deps graph =
+  let is_dependent v1 v2 g =
+    let (_, instr1) = v1 in
+    let (_, instr2) = v2 in
+    if check_dependent (get_pred instr1) (get_pred instr2)
+    then g
+    else DFG.remove_edge g v1 v2
+  in
+  DFG.fold_edges is_dependent graph graph
+
+(** All the nodes in the DFG have to come after the source of the basic block, and should terminate
+   before the sink of the basic block.  After that, there should be constraints for data
+   dependencies between nodes. *)
+let gather_bb_constraints debug bb =
+  let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in
+  let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in
+  let _, _, dfg' =
+    List.fold_left (accumulate_RAW_deps ibody)
+      (0, PTree.empty, dfg)
+      bb.bb_body
+  in
+  let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg'
+      [ accumulate_WAW_deps;
+        accumulate_WAR_deps;
+        accumulate_RAW_mem_deps;
+        accumulate_WAR_mem_deps;
+        accumulate_WAW_mem_deps;
+        accumulate_RAW_pred_deps;
+        accumulate_WAR_pred_deps;
+        accumulate_WAW_pred_deps
+      ]
+  in
+  let dfg''' = remove_unnecessary_deps dfg'' in
+  (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit)
+
+let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i }
+let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i }
+
+let add_super_nodes n dfg =
+  DFG.fold_vertex (function v1 -> fun g ->
+      (if DFG.in_degree dfg v1 = 0
+       then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0)
+       else g) |>
+      (fun g' ->
+         if DFG.out_degree dfg v1 = 0
+         then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1)
+         else g')) dfg
+
+let add_data_deps n =
+  DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g ->
+      G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0)
+    )
+
+let add_ctrl_deps n succs constr =
+  List.fold_left (fun g n' ->
+      G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0)
+    ) constr succs
+
+module BFDFG = Graph.Path.BellmanFord(DFG)(struct
+    include DFG
+    type t = int
+    let weight = DFG.E.label
+    let compare = compare
+    let add = (+)
+    let zero = 0
+  end)
+
+module TopoDFG = Graph.Topological.Make(DFG)
+
+let negate_graph constr =
+  DFG.fold_edges_e (function (v1, e, v2) -> fun g ->
+      DFG.add_edge_e g (v1, -e, v2)
+    ) constr DFG.empty
+
+let add_cycle_constr max n dfg constr =
+  let negated_dfg = negate_graph dfg in
+  let longest_path v = BFDFG.all_shortest_paths negated_dfg v
+                       |> BFDFG.H.to_seq |> List.of_seq in
+  let constrained_paths = List.filter (function (v, m) -> - m > max) in
+  List.fold_left (fun g -> function (v, v', w) ->
+      G.add_edge_e g (encode_var n (fst v) 0,
+                      - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1),
+                      encode_var n (fst v') 0)
+    ) constr (DFG.fold_vertex (fun v l ->
+      List.append l (longest_path v |> constrained_paths
+                     |> List.map (function (v', w) -> (v, v', - w)))
+    ) dfg [])
+
+type resource =
+  | Mem
+  | SDiv
+  | UDiv
+
+type resources = {
+  res_mem: DFG.V.t list;
+  res_udiv: DFG.V.t list;
+  res_sdiv: DFG.V.t list;
+}
+
+let find_resource = function
+  | RBload _ -> Some Mem
+  | RBstore _ -> Some Mem
+  | RBop (_, op, _, _) ->
+    ( match op with
+      | Odiv -> Some SDiv
+      | Odivu -> Some UDiv
+      | Omod -> Some SDiv
+      | Omodu -> Some UDiv
+      | _ -> None )
+  | _ -> None
+
+let add_resource_constr n dfg constr =
+  let res = TopoDFG.fold (function (i, instr) ->
+    function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r ->
+    match find_resource instr with
+    | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl}
+    | Some UDiv -> {r with res_udiv = (i, instr) :: udl}
+    | Some Mem -> {r with res_mem = (i, instr) :: ml}
+    | None -> r
+    ) dfg {res_mem = []; res_sdiv = []; res_udiv = []}
+  in
+  let get_constraints l g = List.fold_left (fun gv v' ->
+      match gv with
+      | (g, None) -> (g, Some v')
+      | (g, Some v) ->
+        (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v')
+    ) (g, None) l |> fst
+  in
+  get_constraints (List.rev res.res_mem) constr
+  |> get_constraints (List.rev res.res_udiv)
+  |> get_constraints (List.rev res.res_sdiv)
+
+let gather_cfg_constraints c constr curr =
+  let (n, dfg) = curr in
+  match PTree.get (P.of_int n) c with
+  | None -> assert false
+  | Some { bb_exit = ctrl; _ } ->
+    add_super_nodes n dfg constr
+    |> add_data_deps n dfg
+    |> add_ctrl_deps n (successors_instr ctrl
+                        |> List.map P.to_int
+                        |> List.filter (fun n' -> n' < n))
+    |> add_cycle_constr 8 n dfg
+    |> add_resource_constr n dfg
+
+let rec intersperse s = function
+  | [] -> []
+  | [ a ] -> [ a ]
+  | x :: xs -> x :: s :: intersperse s xs
+
+let print_objective constr =
+  let vars = G.fold_vertex (fun v1 l ->
+      match v1 with
+      | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l
+      | _ -> l
+    ) constr []
+  in
+  "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n"
+
+let print_lp constr =
+  print_objective constr ^
+  (G.fold_edges_e (function (e1, w, e2) -> fun s ->
+       s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w
+     ) constr "" |>
+   G.fold_vertex (fun v1 s ->
+       s ^ sprintf "int %s;\n" (print_sv v1)
+     ) constr)
+
+let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ]
+
+let parse_soln tree s =
+  let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in
+  if Str.string_match r s 0 then
+    IMap.update
+      (Str.matched_group 1 s |> int_of_string)
+      (update_schedule
+         ( Str.matched_group 2 s |> int_of_string,
+           Str.matched_group 3 s |> int_of_string ))
+      tree
+  else tree
+
+let solve_constraints constr =
+  let oc = open_out "lpsolve.txt" in
+  fprintf oc "%s\n" (print_lp constr);
+  close_out oc;
+
+  Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt")
+  |> drop 3
+  |> List.fold_left parse_soln IMap.empty
+
+let subgraph dfg l =
+  let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in
+  List.fold_left (fun g v ->
+      List.fold_left (fun g' v' ->
+          let edges = DFG.find_all_edges dfg v v' in
+          List.fold_left (fun g'' e ->
+              DFG.add_edge_e g'' e
+            ) g' edges
+        ) g l
+    ) dfg' l
+
+let rec all_successors dfg v =
+  List.concat (List.fold_left (fun l v ->
+      all_successors dfg v :: l
+    ) [] (DFG.succ dfg v))
+
+let order_instr dfg =
+  DFG.fold_vertex (fun v li ->
+      if DFG.in_degree dfg v = 0
+      then (List.map snd (v :: all_successors dfg v)) :: li
+      else li
+    ) dfg []
+
+let combine_bb_schedule schedule s =
+  let i, st = s in
+  IMap.update st (update_schedule i) schedule
+
+(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *)
+let transf_rtlpar c c' (schedule : (int * int) list IMap.t) =
+  let f i bb : RTLPar.bblock =
+    match bb with
+    | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c }
+    | { bb_body = bb_body'; bb_exit = ctrl_flow } ->
+      let dfg = match PTree.get i c' with None -> assert false | Some x -> x in
+      let i_sched = IMap.find (P.to_int i) schedule in
+      let i_sched_tree =
+        List.fold_left combine_bb_schedule IMap.empty i_sched
+      in
+      let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd
+                 |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
+      in
+      (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*)
+      let final_body2 = List.map (fun x -> subgraph dfg x
+                                           |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
+                                           |> List.rev) body
+      in
+      { bb_body = List.map (fun x -> [x]) final_body2;
+        bb_exit = ctrl_flow
+      }
+  in
+  PTree.map f c
+
+let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
+  let debug = true in
+  let transf_graph (_, dfg, _) = dfg in
+  let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in
+  (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*)
+  let cgraph = PTree.elements c'
+               |> List.map (function (x, y) -> (P.to_int x, y))
+               |> List.fold_left (gather_cfg_constraints c) G.empty
+  in
+  let graph = open_out "constr_graph.dot" in
+  fprintf graph "%a\n" GDot.output_graph cgraph;
+  close_out graph;
+  let schedule' = solve_constraints cgraph in
+  (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
+  (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
+  transf_rtlpar c c' schedule'
+
+let rec find_reachable_states c e =
+  match PTree.get e c with
+  | Some { bb_exit = ex; _ } ->
+    e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) []
+      (successors_instr ex |> List.filter (fun x -> P.lt x e))
+  | None -> assert false
+
+let add_to_tree c nt i =
+  match PTree.get i c with
+  | Some p -> PTree.set i p nt
+  | None -> assert false
+
+let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
+  let scheduled = schedule f.fn_entrypoint f.fn_code in
+  let reachable = find_reachable_states scheduled f.fn_entrypoint
+                  |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in
+  { fn_sig = f.fn_sig;
+    fn_params = f.fn_params;
+    fn_stacksize = f.fn_stacksize;
+    fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable;
+    fn_entrypoint = f.fn_entrypoint
+  }