Remove more OCaml files to compile successfully without admits.

5 files changed, 0 insertions, 1085 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index aa5309a..1ea580f 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -65,7 +65,6 @@ 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
deleted file mode 100644
index 19c6048..0000000
--- a/src/hls/Partition.ml
+++ /dev/null
@@ -1,124 +0,0 @@
- (*
- * 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
deleted file mode 100644
index 8fef401..0000000
--- a/src/hls/PrintRTLBlock.ml
+++ /dev/null
@@ -1,72 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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
deleted file mode 100644
index ba7241b..0000000
--- a/src/hls/PrintRTLBlockInstr.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-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
deleted file mode 100644
index c6c8bf4..0000000
--- a/src/hls/Schedule.ml
+++ /dev/null
@@ -1,801 +0,0 @@
-(*
- * 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
-  }