Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

13 files changed, 550 insertions, 165 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 10a000a8..ca727f82 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -23,6 +23,14 @@ Require Import RTL Op Registers OptionMonad.
 Definition exit := node.  (* we may generalize this with register renamings at exit, 
                              like in "phi" nodes of SSA-form *)
 
+(* inst_info is a ghost record to provide instruction information through oracles *)
+Parameter inst_info: Set.
+Extract Constant inst_info => "BTLaux.inst_info".
+
+(* block_info is a ghost record to provide block information through oracles *)
+Parameter block_info: Set.
+Extract Constant block_info => "BTLaux.block_info".
+
 (** final instructions (that stops block execution) *)
 Inductive final: Type :=
   | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *)
@@ -48,16 +56,16 @@ Inductive final: Type :=
 (* instruction block *)
 Inductive iblock: Type :=
 (* final instructions that stops block execution *)
-  | BF (fi: final)
+  | BF (fi: final) (iinfo: inst_info)
 (* basic instructions that continues block execution, except when aborting *)
-  | Bnop (* nop instruction *)
-  | Bop (op:operation) (args:list reg) (dest:reg) 
+  | Bnop (iinfo: inst_info) (* nop instruction *)
+  | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info)
       (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *)
-  | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg)
+  | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (iinfo: inst_info)
       (** loads a [chunk] quantity from the address determined by the addressing mode [addr] 
           and the values of the [args] registers, stores the quantity just read into [dest].
           If trap=NOTRAP, then failures lead to a default value written to [dest]. *)
-  | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg)
+  | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) (iinfo: inst_info)
       (** stores the value of register [src] in the [chunk] quantity at the
           the address determined by the addressing mode [addr] and the
           values of the [args] registers. *)
@@ -65,13 +73,13 @@ Inductive iblock: Type :=
   | Bseq (b1 b2: iblock)
       (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted
           or continue with [b2] otherwise *)
-  | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool)
+  | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (iinfo: inst_info)
       (** evaluates the boolean condition [cond] over the values of registers [args].  
           If the condition is true, it continues on [ifso].
           If the condition is false, it continues on [ifnot].
           [info] is a ghost field there to provide information relative to branch prediction. *)
   .
-Coercion BF: final >-> iblock.
+Coercion BF: final >-> Funclass.
 
 
 (** NB: - a RTL [(Inop pc)] ending a branch of block is encoded by [(Bseq Bnop (Bgoto pc))].
@@ -83,7 +91,8 @@ Coercion BF: final >-> iblock.
 
 Record iblock_info := { 
   entry: iblock;
-  input_regs: Regset.t (* extra liveness information ignored by BTL semantics *)
+  input_regs: Regset.t; (* extra liveness information ignored by BTL semantics *)
+  binfo: block_info (* Ghost field used in oracles *)
 }.
 
 Definition code: Type := PTree.t iblock_info.
@@ -194,24 +203,24 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
 
 (** internal big-step execution of one iblock *)
 Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop :=
-  | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin)
-  | exec_nop rs m: iblock_istep sp rs m Bnop rs m None
-  | exec_op rs m op args res v
+  | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin)
+  | exec_nop rs m iinfo: iblock_istep sp rs m (Bnop iinfo) rs m None
+  | exec_op rs m op args res v iinfo
      (EVAL: eval_operation ge sp op rs##args m = Some v)
-     : iblock_istep sp rs m (Bop op args res) (rs#res <- v) m None
-  | exec_load_TRAP rs m chunk addr args dst a v
+     : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None
+  | exec_load_TRAP rs m chunk addr args dst a v iinfo
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (LOAD: Mem.loadv chunk m a = Some v)
-     : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None
+     : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None
 (* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above
   | exec_load rs m trap chunk addr args dst v
       (LOAD: has_loaded sp rs m chunk addr args v trap)
      : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None
 *)
-  | exec_store rs m chunk addr args src a m' 
+  | exec_store rs m chunk addr args src a m' iinfo
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (STORE: Mem.storev chunk m a rs#src = Some m')
-     : iblock_istep sp rs m (Bstore chunk addr args src) rs m' None
+     : iblock_istep sp rs m (Bstore chunk addr args src iinfo) rs m' None
   | exec_seq_stop rs m b1 b2 rs' m' fin
      (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin))
      : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin)
@@ -219,10 +228,10 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi
      (EXEC1: iblock_istep sp rs m b1 rs1 m1 None)
      (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin)
      : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin
-  | exec_cond rs m cond args ifso ifnot i b rs' m' ofin
+  | exec_cond rs m cond args ifso ifnot b rs' m' ofin iinfo
      (EVAL: eval_condition cond rs##args m = Some b)
      (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin)
-     : iblock_istep sp rs m (Bcond cond args ifso ifnot i) rs' m' ofin
+     : iblock_istep sp rs m (Bcond cond args ifso ifnot iinfo) rs' m' ofin
   .
 Local Hint Constructors iblock_istep: core.
 
@@ -231,21 +240,21 @@ Lemma [iblock_istep_run_equiv] below provides a proof that "relation" [iblock_is
 *)
 Fixpoint iblock_istep_run sp ib rs m: option outcome := 
   match ib with
-  | BF fin =>
+  | BF fin _ =>
       Some {| _rs := rs; _m := m; _fin := Some fin |}
   (* basic instructions *)
-  | Bnop =>
+  | Bnop _ =>
       Some {| _rs := rs; _m:= m; _fin := None |}
-  | Bop op args res =>
+  | Bop op args res _ =>
       SOME v <- eval_operation ge sp op rs##args m IN
       Some {| _rs := rs#res <- v; _m:= m; _fin := None |}
-  | Bload TRAP chunk addr args dst =>
+  | Bload TRAP chunk addr args dst _ =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME v <- Mem.loadv chunk m a IN
       Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
-  | Bload NOTRAP chunk addr args dst =>
+  | Bload NOTRAP chunk addr args dst _ =>
       None (* TODO *)
-  | Bstore chunk addr args src =>
+  | Bstore chunk addr args src _ =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME m' <- Mem.storev chunk m a rs#src IN
       Some {| _rs := rs; _m:= m'; _fin := None |}
@@ -412,25 +421,25 @@ Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop :=
    - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc'].
 *)
 Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop :=
-  | mib_BF isfst fi pc i:
+  | mib_BF isfst fi pc i iinfo:
       cfg!pc = Some i ->
       match_final_inst dupmap fi i ->
-      match_iblock dupmap cfg isfst pc (BF fi) None
-  | mib_nop isfst pc pc':
+      match_iblock dupmap cfg isfst pc (BF fi iinfo) None
+  | mib_nop isfst pc pc' iinfo:
       cfg!pc = Some (Inop pc') ->
-      match_iblock dupmap cfg isfst pc Bnop (Some pc')
-  | mib_op isfst pc pc' op lr r:
+      match_iblock dupmap cfg isfst pc (Bnop iinfo) (Some pc')
+  | mib_op isfst pc pc' op lr r iinfo:
       cfg!pc = Some (Iop op lr r pc') ->
-      match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc')
-  | mib_load isfst pc pc' m a lr r:
+      match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc')
+  | mib_load isfst pc pc' m a lr r iinfo:
       cfg!pc = Some (Iload TRAP m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r) (Some pc')
-  | mib_store isfst pc pc' m a lr r:
+      match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc')
+  | mib_store isfst pc pc' m a lr r iinfo:
       cfg!pc = Some (Istore m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc')
-  | mib_exit pc pc': 
+      match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc')
+  | mib_exit pc pc' iinfo: 
       dupmap!pc = (Some pc') ->
-      match_iblock dupmap cfg false pc' (Bgoto pc) None
+      match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) None
       (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). 
          Thus some step should have been executed before [pc'] in the RTL code *)
   | mib_seq_Some isfst b1 b2 pc1 pc2 opc:
@@ -445,12 +454,12 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i
          And the verifier could fail if there is such dead code!
       *)
 *)
-  | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i':
-      cfg!pc = Some (Icond c lr pcso pcnot i') ->
+  | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo:
+      cfg!pc = Some (Icond c lr pcso pcnot i) ->
       match_iblock dupmap cfg false pcso bso opc1 ->
       match_iblock dupmap cfg false pcnot bnot opc2 ->
       is_join_opt opc1 opc2 opc ->
-      match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc
+      match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc
   .
 
 Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop :=
@@ -463,8 +472,8 @@ Local Open Scope error_monad_scope.
 
 Definition verify_is_copy dupmap n n' :=
   match dupmap!n with
-  | None => Error(msg "verify_is_copy None")
-  | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
+  | None => Error(msg "BTL.verify_is_copy None")
+  | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end
   end.
 
 Fixpoint verify_is_copy_list dupmap ln ln' :=
@@ -472,9 +481,9 @@ Fixpoint verify_is_copy_list dupmap ln ln' :=
   | n::ln => match ln' with
              | n'::ln' => do _ <- verify_is_copy dupmap n n';
                           verify_is_copy_list dupmap ln ln'
-             | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end
+             | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end
   | nil => match ln' with
-          | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'")
+          | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'")
           | nil => OK tt end
   end.
 
@@ -523,19 +532,19 @@ Global Opaque builtin_res_eq_pos.
 
 Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) :=
   match ib with
-  | BF fi =>
+  | BF fi _ =>
       match fi with
       | Bgoto pc1 =>
           do u <- verify_is_copy dupmap pc1 pc;
           if negb isfst then
             OK None
-          else Error (msg "verify_block: isfst is true Bgoto")
+          else Error (msg "BTL.verify_block: isfst is true Bgoto")
       | Breturn or =>
           match cfg!pc with
           | Some (Ireturn or') =>
               if option_eq Pos.eq_dec or or' then OK None
-              else Error (msg "verify_block: different opt reg in Breturn")
-          | _ => Error (msg "verify_block: incorrect cfg Breturn")
+              else Error (msg "BTL.verify_block: different opt reg in Breturn")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn")
           end
       | Bcall s ri lr r pc1 =>
           match cfg!pc with
@@ -545,11 +554,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
                 if (product_eq Pos.eq_dec ident_eq ri ri') then
                   if (list_eq_dec Pos.eq_dec lr lr') then
                     if (Pos.eq_dec r r') then OK None
-                    else Error (msg "verify_block: different r r' in Bcall")
-                  else Error (msg "verify_block: different lr in Bcall")
-                else Error (msg "verify_block: different ri in Bcall")
-              else Error (msg "verify_block: different signatures in Bcall")
-          | _ => Error (msg "verify_block: incorrect cfg Bcall")
+                    else Error (msg "BTL.verify_block: different r r' in Bcall")
+                  else Error (msg "BTL.verify_block: different lr in Bcall")
+                else Error (msg "BTL.verify_block: different ri in Bcall")
+              else Error (msg "BTL.verify_block: different signatures in Bcall")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall")
           end
       | Btailcall s ri lr =>
           match cfg!pc with
@@ -557,10 +566,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               if (signature_eq s s') then
                 if (product_eq Pos.eq_dec ident_eq ri ri') then
                   if (list_eq_dec Pos.eq_dec lr lr') then OK None
-                  else Error (msg "verify_block: different lr in Btailcall")
-                else Error (msg "verify_block: different ri in Btailcall")
-              else Error (msg "verify_block: different signatures in Btailcall")
-          | _ => Error (msg "verify_block: incorrect cfg Btailcall")
+                  else Error (msg "BTL.verify_block: different lr in Btailcall")
+                else Error (msg "BTL.verify_block: different ri in Btailcall")
+              else Error (msg "BTL.verify_block: different signatures in Btailcall")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall")
           end
       | Bbuiltin ef la br pc1 =>
           match cfg!pc with
@@ -569,38 +578,38 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               if (external_function_eq ef ef') then
                 if (list_eq_dec builtin_arg_eq_pos la la') then
                   if (builtin_res_eq_pos br br') then OK None
-                  else Error (msg "verify_block: different brr in Bbuiltin")
-                else Error (msg "verify_block: different lbar in Bbuiltin")
-              else Error (msg "verify_block: different ef in Bbuiltin")
-          | _ => Error (msg "verify_block: incorrect cfg Bbuiltin")
+                  else Error (msg "BTL.verify_block: different brr in Bbuiltin")
+                else Error (msg "BTL.verify_block: different lbar in Bbuiltin")
+              else Error (msg "BTL.verify_block: different ef in Bbuiltin")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin")
           end
       | Bjumptable r ln =>
           match cfg!pc with
           | Some (Ijumptable r' ln') =>
               do u <- verify_is_copy_list dupmap ln ln';
               if (Pos.eq_dec r r') then OK None
-              else Error (msg "verify_block: different r in Bjumptable")
-          | _ => Error (msg "verify_block: incorrect cfg Bjumptable")
+              else Error (msg "BTL.verify_block: different r in Bjumptable")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable")
           end
       end
-  | Bnop =>
+  | Bnop _ =>
       match cfg!pc with
       | Some (Inop pc') => OK (Some pc')
-      | _ => Error (msg "verify_block: incorrect cfg Bnop")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop")
       end
-  | Bop op lr r =>
+  | Bop op lr r _ =>
       match cfg!pc with
       | Some (Iop op' lr' r' pc') =>
           if (eq_operation op op') then
             if (list_eq_dec Pos.eq_dec lr lr') then
               if (Pos.eq_dec r r') then
                 OK (Some pc')
-              else Error (msg "verify_block: different r in Bop")
-            else Error (msg "verify_block: different lr in Bop")
-          else Error (msg "verify_block: different operations in Bop")
-      | _ => Error (msg "verify_block: incorrect cfg Bop")
+              else Error (msg "BTL.verify_block: different r in Bop")
+            else Error (msg "BTL.verify_block: different lr in Bop")
+          else Error (msg "BTL.verify_block: different operations in Bop")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bop")
       end
-  | Bload tm m a lr r =>
+  | Bload tm m a lr r _ =>
       match cfg!pc with
       | Some (Iload tm' m' a' lr' r' pc') =>
           if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then
@@ -609,34 +618,34 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
                 if (list_eq_dec Pos.eq_dec lr lr') then
                   if (Pos.eq_dec r r') then
                     OK (Some pc')
-                  else Error (msg "verify_block: different r in Bload")
-                else Error (msg "verify_block: different lr in Bload")
-              else Error (msg "verify_block: different addressing in Bload")
-            else Error (msg "verify_block: different mchunk in Bload")
-          else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload")
-      | _ => Error (msg "verify_block: incorrect cfg Bload")
+                  else Error (msg "BTL.verify_block: different r in Bload")
+                else Error (msg "BTL.verify_block: different lr in Bload")
+              else Error (msg "BTL.verify_block: different addressing in Bload")
+            else Error (msg "BTL.verify_block: different mchunk in Bload")
+          else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bload")
       end
-  | Bstore m a lr r =>
+  | Bstore m a lr r _ =>
       match cfg!pc with
       | Some (Istore m' a' lr' r' pc') =>
           if (chunk_eq m m') then
             if (eq_addressing a a') then
               if (list_eq_dec Pos.eq_dec lr lr') then
                 if (Pos.eq_dec r r') then OK (Some pc')
-                else Error (msg "verify_block: different r in Bstore")
-              else Error (msg "verify_block: different lr in Bstore")
-            else Error (msg "verify_block: different addressing in Bstore")
-          else Error (msg "verify_block: different mchunk in Bstore")
-      | _ => Error (msg "verify_block: incorrect cfg Bstore")
+                else Error (msg "BTL.verify_block: different r in Bstore")
+              else Error (msg "BTL.verify_block: different lr in Bstore")
+            else Error (msg "BTL.verify_block: different addressing in Bstore")
+          else Error (msg "BTL.verify_block: different mchunk in Bstore")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore")
       end
   | Bseq b1 b2 =>
       do opc <- verify_block dupmap cfg isfst pc b1;
       match opc with
       | Some pc' =>
           verify_block dupmap cfg false pc' b2
-      | None => Error (msg "verify_block: None next pc in Bseq (deadcode)")
+      | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)")
       end
-  | Bcond c lr bso bnot i =>
+  | Bcond c lr bso bnot _ =>
       match cfg!pc with
       | Some (Icond c' lr' pcso pcnot i') =>
           if (list_eq_dec Pos.eq_dec lr lr') then
@@ -648,11 +657,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               | o, None => OK o
               | Some x, Some x' =>
                   if Pos.eq_dec x x' then OK (Some x)
-                  else Error (msg "verify_block: is_join_opt incorrect for Bcond")
+                  else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond")
               end
-            else Error (msg "verify_block: incompatible conditions in Bcond")
-          else Error (msg "verify_block: different lr in Bcond")
-      | _ => Error (msg "verify_block: incorrect cfg Bcond")
+            else Error (msg "BTL.verify_block: incompatible conditions in Bcond")
+          else Error (msg "BTL.verify_block: different lr in Bcond")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond")
       end
   end.
 
@@ -753,9 +762,9 @@ Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit :=
     | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry);
                  match o with
                  | None => verify_blocks dupmap cfg cfg' l
-                 | _ => Error(msg "verify_blocks.end")
+                 | _ => Error(msg "BTL.verify_blocks.end")
                  end
-    | _ => Error(msg "verify_blocks.entry")
+    | _ => Error(msg "BTL.verify_blocks.entry")
     end
   end.
 
@@ -788,7 +797,7 @@ Definition verify_function dupmap f f' : res unit :=
 
 Definition is_goto (ib: iblock): bool :=
   match ib with
-  | Bgoto _ => true
+  | BF (Bgoto _) _ => true
   | _ => false
   end.
 
@@ -804,10 +813,10 @@ Inductive is_expand: iblock -> Prop :=
      is_atom ib1 = true ->
      is_expand ib2 -> 
      is_expand (Bseq ib1 ib2)
-  | exp_Bcond cond args ib1 ib2 i:
+  | exp_Bcond cond args ib1 ib2 iinfo:
      is_expand ib1 ->
      is_expand ib2 -> 
-     is_expand (Bcond cond args ib1 ib2 i)
+     is_expand (Bcond cond args ib1 ib2 iinfo)
   | exp_others ib:
      is_atom ib = true ->
      is_expand ib
@@ -817,9 +826,9 @@ Local Hint Constructors is_expand: core.
 Fixpoint expand (ib: iblock) (k: option iblock): iblock :=
   match ib with
   | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k))
-  | Bcond cond args ib1 ib2 i => 
-     Bcond cond args (expand ib1 k) (expand ib2 k) i
-  | BF fin => fin
+  | Bcond cond args ib1 ib2 iinfo => 
+     Bcond cond args (expand ib1 k) (expand ib2 k) iinfo
+  | BF fin iinfo => BF fin iinfo
   | ib => 
     match k with 
     | None => ib
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index b9a05a8a..cd69cd37 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -770,13 +770,13 @@ pour représenter l'ensemble des chemins.
 
 Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := 
   match ib with
-  | BF fin => Sfinal sis (sexec_final_sfv fin sis)
+  | BF fin _ => Sfinal sis (sexec_final_sfv fin sis)
   (* basic instructions *)
-  | Bnop => k sis
-  | Bop op args res => k (sexec_op op args res sis)
-  | Bload TRAP chunk addr args dst => k (sexec_load TRAP chunk addr args dst sis)
-  | Bload NOTRAP chunk addr args dst => Sabort (* TODO *)
-  | Bstore chunk addr args src => k (sexec_store chunk addr args src sis)
+  | Bnop _ => k sis
+  | Bop op args res _ => k (sexec_op op args res sis)
+  | Bload TRAP chunk addr args dst _ => k (sexec_load TRAP chunk addr args dst sis)
+  | Bload NOTRAP chunk addr args dst _ => Sabort (* TODO *)
+  | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
       sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml
new file mode 100644
index 00000000..863afdf0
--- /dev/null
+++ b/scheduling/BTLaux.ml
@@ -0,0 +1,3 @@
+type inst_info = { mutable inumb : int; mutable pcond : bool option }
+
+type block_info = { mutable bnumb : int; mutable visited: bool }
diff --git a/scheduling/BTLrenumber.ml b/scheduling/BTLrenumber.ml
new file mode 100644
index 00000000..dd6baa89
--- /dev/null
+++ b/scheduling/BTLrenumber.ml
@@ -0,0 +1,50 @@
+(* XXX uncomment
+open !BTL
+open DebugPrint
+open AuxTools
+open Maps*)
+
+(** A quick note on the BTL renumber algorithm
+    This is a simple first version where we try to reuse the entry numbering from RTL.
+    In the futur, it would be great to implement a strongly connected components partitionning.
+    The numbering is done by a postorder traversal.
+    TODO gourdinl : note perso
+    - faire un comptage global du nombre d'instructions rtl à générer
+    - utiliser la structure d'info créée lors de la génération pour tenter de préserver au max
+    la relation d'ordre, avec une heuristique genre (1 + max des succs) pour l'insertion
+    - quand il y a un branchement conditionnel, privilégier le parcour du fils gauche en premier
+    (afin d'avoir de plus petits numéros à gauche)
+*)
+(*
+let rec get_max_rtl_ninsts code entry =
+let rec postorder_blk ib =
+*)
+
+(* XXX uncomment
+let postorder code entry =
+  let renumbered_code = ref PTree.empty in
+  let rec renum_ibf e =
+    let ibf = get_some @@ PTree.get e code in
+    if ibf.binfo.visited then ()
+    else (
+      ibf.binfo.visited <- true;
+      let next_nodes = ref [] in
+      let ib = ibf.entry in
+      let rec renum_iblock ib =
+        match ib with
+      in
+      let rib = renum_iblock ib in
+      ibf.entry <- rib;
+      renumbered_code := PTree.set e ibf !renumbered_code;
+      let succs = !next_nodes in
+      List.iter renum_ibf succs)
+  in
+  renum_ibf entry
+
+let renumber (f: BTL.coq_function) =
+  debug_flag := true;
+  let code = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let renumbered_code = postorder code entry in
+  debug_flag := false;
+  renumbered_code*)
diff --git a/scheduling/BTLtoRTL.v b/scheduling/BTLtoRTL.v
index b64fd87a..82ad47b1 100644
--- a/scheduling/BTLtoRTL.v
+++ b/scheduling/BTLtoRTL.v
@@ -5,7 +5,9 @@ Require Import RTL Op Registers OptionMonad BTL.
 Require Import Errors Linking.
 
 (** External oracle *)
-Parameter btl2rtl: function -> RTL.code * node * (PTree.t node).
+Axiom btl2rtl: function -> RTL.code * node * (PTree.t node).
+
+Extract Constant btl2rtl => "BTLtoRTLaux.btl2rtl".
 
 Local Open Scope error_monad_scope.
 
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
new file mode 100644
index 00000000..b4833b2c
--- /dev/null
+++ b/scheduling/BTLtoRTLaux.ml
@@ -0,0 +1,115 @@
+open Maps
+open BTL
+open RTL
+open Camlcoq
+open AuxTools
+open DebugPrint
+open BTLaux
+
+let is_atom = function
+  | Bseq (_, _) | Bcond (_, _, _, _, _) -> false
+  | _ -> true
+
+let get_inumb iinfo = P.of_int iinfo.inumb
+
+let rec get_ib_num = function
+  | BF (Bgoto s, _) -> s
+  | Bnop iinfo
+  | Bop (_, _, _, iinfo)
+  | Bload (_, _, _, _, _, iinfo)
+  | Bstore (_, _, _, _, iinfo)
+  | Bcond (_, _, _, _, iinfo)
+  | BF (_, iinfo) ->
+      get_inumb iinfo
+  | Bseq (ib1, _) -> get_ib_num ib1
+
+let translate_function code entry =
+  let rtl_code = ref PTree.empty in
+  let code =
+    PTree.map
+      (fun n ibf ->
+        ibf.binfo.visited <- false;
+        ibf)
+      code
+  in
+  let rec build_rtl_tree e =
+    let ibf = get_some @@ PTree.get e code in
+    if ibf.binfo.visited then ()
+    else (
+      ibf.binfo.visited <- true;
+      let ib = ibf.entry in
+      let next_nodes = ref [] in
+      let rec translate_btl_block ib k =
+        let rtli =
+          match ib with
+          | Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) ->
+              next_nodes := s1 :: s2 :: !next_nodes;
+              Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo)
+          | Bcond (cond, lr, BF (Bgoto s1, _), ib2, iinfo) ->
+              assert (iinfo.pcond = Some false);
+              next_nodes := s1 :: !next_nodes;
+              translate_btl_block ib2 None;
+              Some
+                ( Icond (cond, lr, s1, get_ib_num ib2, iinfo.pcond),
+                  get_inumb iinfo )
+          (* TODO gourdinl remove dynamic check *)
+          | Bcond (_, _, _, _, _) ->
+              failwith "translate_function: invalid Bcond"
+          | Bseq (ib1, ib2) ->
+              (* TODO gourdinl remove dynamic check *)
+              assert (is_atom ib1);
+              translate_btl_block ib1 (Some ib2);
+              translate_btl_block ib2 None;
+              None
+          | Bnop iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
+          | Bop (op, lr, rd, iinfo) ->
+              Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo)
+          | Bload (trap, chk, addr, lr, rd, iinfo) ->
+              Some
+                ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)),
+                  get_inumb iinfo )
+          | Bstore (chk, addr, lr, rd, iinfo) ->
+              Some
+                ( Istore (chk, addr, lr, rd, get_ib_num (get_some k)),
+                  get_inumb iinfo )
+          | BF (Bcall (sign, fn, lr, rd, s), iinfo) ->
+              next_nodes := s :: !next_nodes;
+              Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo)
+          | BF (Btailcall (sign, fn, lr), iinfo) ->
+              Some (Itailcall (sign, fn, lr), get_inumb iinfo)
+          | BF (Bbuiltin (ef, lr, rd, s), iinfo) ->
+              next_nodes := s :: !next_nodes;
+              Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
+          | BF (Bjumptable (arg, tbl), iinfo) ->
+              next_nodes := !next_nodes @ tbl;
+              Some (Ijumptable (arg, tbl), get_inumb iinfo)
+          | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo)
+          | BF (Bgoto s, iinfo) ->
+              next_nodes := s :: !next_nodes;
+              None
+        in
+        match rtli with
+        | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code
+        | None -> ()
+      in
+      translate_btl_block ib None;
+      let succs = !next_nodes in
+      List.iter build_rtl_tree succs)
+  in
+  build_rtl_tree entry;
+  !rtl_code
+
+let btl2rtl (f : BTL.coq_function) =
+  (*debug_flag := true;*)
+  let code = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let rtl = translate_function code entry in
+  let dm = PTree.map (fun n i -> n) code in
+  debug "Entry %d\n" (p2i entry);
+  debug "RTL Code: ";
+  (*print_code rtl;*)
+  debug "Dupmap:\n";
+  print_ptree print_pint dm;
+  debug "\n";
+  (*debug_flag := false;*)
+  ((rtl, entry), dm)
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 08a77ae4..9b37d8fa 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -221,7 +221,7 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
    match ofin with 
    | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
    | Some fin =>
-      exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None
+      exists isfst' pc1 iinfo, match_iblock dupmap (RTL.fn_code f') isfst' pc1 (BF fin iinfo) None
                  /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
    end.
 Proof.
@@ -255,7 +255,7 @@ Proof.
     intros (pc1 & EQpc1 & STEP1); inv EQpc1.
     exploit IHIBIS2; eauto.
     destruct ofin; simpl.
-    + intros (ifst2 & pc2 & M2 & STEP2).
+    + intros (ifst2 & pc2 & iinfo & M2 & STEP2).
       repeat eexists; eauto.
       eapply css_plus_trans; eauto.
     + intros (pc2 & EQpc2 & STEP2); inv EQpc2.
@@ -268,7 +268,7 @@ Proof.
     + (* taking ifso *)
       destruct ofin; simpl.
       * (* ofin is Some final *)
-        intros (isfst' & pc1 & MI & STAR).
+        intros (isfst' & pc1 & iinfo' & MI & STAR).
         repeat eexists; eauto.
         eapply css_plus_trans; eauto.
       * (* ofin is None *)
@@ -279,7 +279,7 @@ Proof.
     + (* taking ifnot *)
       destruct ofin; simpl.
       * (* ofin is Some final *)
-        intros (isfst' & pc1 & MI & STAR).
+        intros (isfst' & pc1 & iinfo' & MI & STAR).
         repeat eexists; eauto.
         eapply css_plus_trans; eauto.
       * (* ofin is None *)
@@ -342,7 +342,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi
   : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
 Proof.
   intros; exploit iblock_istep_simulation; eauto.
-  simpl. intros (isfst' & pc1 & MI & STAR). clear IBIS MIB.
+  simpl. intros (isfst' & pc1 & iinfo & MI & STAR). clear IBIS MIB.
   inv MI.
   - (* final inst except goto *)
     exploit final_simu_except_goto; eauto.
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
new file mode 100644
index 00000000..0ed3981d
--- /dev/null
+++ b/scheduling/PrintBTL.ml
@@ -0,0 +1,122 @@
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open BTL
+open PrintAST
+open BTLaux
+open DebugPrint
+
+(* Printing of BTL 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_succ pp s = fprintf pp "\tsucc %d\n" (P.to_int s)
+
+let print_pref pp pref = fprintf pp "%s" pref
+
+let rec print_iblock pp is_rec pref ib =
+  match ib with
+  | Bnop _ ->
+      print_pref pp pref;
+      fprintf pp "Bnop\n"
+  | Bop (op, args, res, _) ->
+      print_pref pp pref;
+      fprintf pp "Bop: %a = %a\n" reg res
+        (PrintOp.print_operation reg)
+        (op, args)
+  | Bload (trap, chunk, addr, args, dst, _) ->
+      print_pref pp pref;
+      fprintf pp "Bload: %a = %s[%a]%a\n" reg dst (name_of_chunk chunk)
+        (PrintOp.print_addressing reg)
+        (addr, args) print_trapping_mode trap
+  | Bstore (chunk, addr, args, src, _) ->
+      print_pref pp pref;
+      fprintf pp "Bstore: %s[%a] = %a\n" (name_of_chunk chunk)
+        (PrintOp.print_addressing reg)
+        (addr, args) reg src
+  | BF (Bcall (sg, fn, args, res, s), _) ->
+      print_pref pp pref;
+      fprintf pp "Bcall: %a = %a(%a)\n" reg res ros fn regs args;
+      print_succ pp s
+  | BF (Btailcall (sg, fn, args), _) ->
+      print_pref pp pref;
+      fprintf pp "Btailcall: %a(%a)\n" ros fn regs args
+  | BF (Bbuiltin (ef, args, res, s), _) ->
+      print_pref pp pref;
+      fprintf pp "Bbuiltin: %a = %s(%a)\n" (print_builtin_res reg) res
+        (name_of_external ef) (print_builtin_args reg) args;
+      print_succ pp s
+  | Bcond (cond, args, ib1, ib2, iinfo) ->
+      print_pref pp pref;
+      fprintf pp "Bcond: (%a) (prediction: %s)\n"
+        (PrintOp.print_condition reg)
+        (cond, args)
+        (match iinfo.pcond with
+        | None -> "none"
+        | Some true -> "branch"
+        | Some false -> "fallthrough");
+      let pref' = pref ^ "  " in
+      fprintf pp "%sifso = [\n" pref;
+      if is_rec then print_iblock pp is_rec pref' ib1 else fprintf pp "...\n";
+      fprintf pp "%s]\n" pref;
+      fprintf pp "%sifnot = [\n" pref;
+      if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n";
+      fprintf pp "%s]\n" pref
+  | BF (Bjumptable (arg, tbl), _) ->
+      let tbl = Array.of_list tbl in
+      print_pref pp pref;
+      fprintf pp "Bjumptable: (%a)\n" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
+  | BF (Breturn None, _) ->
+      print_pref pp pref;
+      fprintf pp "Breturn\n"
+  | BF (Breturn (Some arg), _) ->
+      print_pref pp pref;
+      fprintf pp "Breturn: %a\n" reg arg
+  | BF (Bgoto s, _) ->
+      print_pref pp pref;
+      fprintf pp "Bgoto: %d\n" (P.to_int s)
+  | Bseq (ib1, ib2) ->
+      if is_rec then (
+        print_iblock pp is_rec pref ib1;
+        print_iblock pp is_rec pref ib2)
+      else fprintf pp "Bseq...\n"
+
+let print_btl_inst pp ib = print_iblock pp false "  " ib
+
+let print_btl_code pp btl is_rec =
+  if !debug_flag then (
+    fprintf pp "\n";
+    List.iter
+      (fun (n, ibf) ->
+        fprintf pp "[BTL block %d]\n" (P.to_int n);
+        print_iblock pp is_rec "  " ibf.entry;
+        fprintf pp "\n")
+      (PTree.elements btl);
+    fprintf pp "\n")
+  else ()
+
+(* TODO gourdinl remove or adapt this?
+let print_function pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+  let instrs = List.map (fun (n, i) -> i.entry) (PTree.elements f.fn_code) in
+  List.iter (print_iblock pp true "") 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 : BTL.program) =
+  List.iter (print_globdef pp) prog.prog_defs*)
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index 2a20a15d..c9bb94d3 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -7,31 +7,7 @@ open Datatypes
 open Kildall
 open Lattice
 open DebugPrint
-
-let get_some = function
-| None -> failwith "Got None instead of Some _"
-| Some thing -> thing
-
-let successors_inst = function
-| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n]
-| Icond (_,_,n1,n2,_) -> [n1; n2]
-| Ijumptable (_,l) -> l
-| Itailcall _ | Ireturn _ -> []
-
-let predicted_successor = function
-| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n
-| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None
-| Icond (_,_,n1,n2,p) -> (
-    match p with
-    | Some true -> Some n1
-    | Some false -> Some n2
-    | None -> None )
-| Ijumptable _ | Itailcall _ | Ireturn _ -> None
-
-let non_predicted_successors i =
-  match predicted_successor i with
-  | None -> successors_inst i
-  | Some n -> List.filter (fun n' -> n != n') (successors_inst i)
+open AuxTools
 
 let rec list_to_regset = function
   | [] -> Regset.empty
@@ -59,24 +35,6 @@ let get_output_reg i =
   | Iop (_, _, r, _) | Iload (_, _, _, _, r, _) | Icall (_, _, _, r, _) -> Some r
   | Ibuiltin (_, _, brr, _) -> (match brr with AST.BR r -> Some r | _ -> None)
 
-(* adapted from Linearizeaux.get_join_points *)
-let get_join_points code entry =
-  let reached = ref (PTree.map (fun n i -> false) code) in
-  let reached_twice = ref (PTree.map (fun n i -> false) code) in
-  let rec traverse pc =
-    if get_some @@ PTree.get pc !reached then begin
-      if not (get_some @@ PTree.get pc !reached_twice) then
-        reached_twice := PTree.set pc true !reached_twice
-    end else begin
-      reached := PTree.set pc true !reached;
-      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
-    end
-  and traverse_succs = function
-    | [] -> ()
-    | [pc] -> traverse pc
-    | pc :: l -> traverse pc; traverse_succs l
-  in traverse entry; !reached_twice
-
 (* Does not set the input_regs and liveouts field *)
 let get_path_map code entry join_points =
   let visited = ref (PTree.map (fun n i -> false) code) in
@@ -92,12 +50,13 @@ let get_path_map code entry join_points =
         let inst = get_some @@ PTree.get n code in
         begin
           psize := !psize + 1;
-          let successor = match predicted_successor inst with
+          let psucc = predicted_successor inst in
+          let successor = match psucc with
           | None -> None
           | Some n' -> if get_some @@ PTree.get n' join_points then None else Some n'
           in match successor with
           | Some n' -> begin
-                path_successors := !path_successors @ non_predicted_successors inst;
+                path_successors := !path_successors @ non_predicted_successors inst psucc;
                 dig_path_rec n'
               end
           | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize);
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index aeed39df..70a0c507 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -7,6 +7,7 @@ open RTL
 open Maps
 open Registers
 open ExpansionOracle
+open AuxTools
 
 let config = Machine.config
 
diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v
index e9319315..b3585157 100644
--- a/scheduling/RTLtoBTL.v
+++ b/scheduling/RTLtoBTL.v
@@ -5,7 +5,9 @@ Require Import RTL Op Registers OptionMonad BTL.
 Require Import Errors Linking.
 
 (** External oracle *)
-Parameter rtl2btl: RTL.function -> BTL.code * node * (PTree.t node).
+Axiom rtl2btl: RTL.function -> BTL.code * node * (PTree.t node).
+
+Extract Constant rtl2btl => "RTLtoBTLaux.rtl2btl".
 
 Local Open Scope error_monad_scope.
 
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
new file mode 100644
index 00000000..43556150
--- /dev/null
+++ b/scheduling/RTLtoBTLaux.ml
@@ -0,0 +1,123 @@
+open Maps
+open RTL
+open BTL
+open Registers
+open DebugPrint
+open PrintBTL
+open AuxTools
+open BTLaux
+
+let undef_node = -1
+
+let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond }
+
+let def_iinfo = { inumb = undef_node; pcond = None }
+
+let mk_binfo _bnumb = { bnumb = _bnumb; visited = false }
+
+let encaps_final inst osucc =
+  match inst with
+  | BF _ | Bcond _ -> inst
+  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo))
+
+let translate_inst iinfo inst is_final =
+  let osucc = ref None in
+  let btli =
+    match inst with
+    | Inop s ->
+        osucc := Some s;
+        Bnop iinfo
+    | Iop (op, lr, rd, s) ->
+        osucc := Some s;
+        Bop (op, lr, rd, iinfo)
+    | Iload (trap, chk, addr, lr, rd, s) ->
+        osucc := Some s;
+        Bload (trap, chk, addr, lr, rd, iinfo)
+    | Istore (chk, addr, lr, rd, s) ->
+        osucc := Some s;
+        Bstore (chk, addr, lr, rd, iinfo)
+    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo)
+    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo)
+    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo)
+    | Icond (cond, lr, ifso, ifnot, info) ->
+        iinfo.pcond <- info;
+        Bcond
+          ( cond,
+            lr,
+            BF (Bgoto ifso, def_iinfo),
+            BF (Bgoto ifnot, def_iinfo),
+            iinfo )
+    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo)
+    | Ireturn oreg -> BF (Breturn oreg, iinfo)
+  in
+  if is_final then encaps_final btli !osucc else btli
+
+let translate_function code entry join_points =
+  let reached = ref (PTree.map (fun n i -> false) code) in
+  let btl_code = ref PTree.empty in
+  let rec build_btl_tree e =
+    if get_some @@ PTree.get e !reached then ()
+    else (
+      reached := PTree.set e true !reached;
+      let next_nodes = ref [] in
+      let rec build_btl_block n =
+        let inst = get_some @@ PTree.get n code in
+        let psucc = predicted_successor inst in
+        let iinfo = mk_iinfo (p2i n) None in
+        let succ =
+          match psucc with
+          | Some ps ->
+              if get_some @@ PTree.get ps join_points then (
+                None)
+              else Some ps
+          | None -> None
+        in
+        match succ with
+        | Some s -> (
+            match inst with
+            | Icond (cond, lr, ifso, ifnot, info) ->
+                (* TODO gourdinl remove this *)
+                assert (s = ifnot);
+                next_nodes := !next_nodes @ non_predicted_successors inst psucc;
+                iinfo.pcond <- info;
+                Bcond
+                  ( cond,
+                    lr,
+                    BF (Bgoto ifso, def_iinfo),
+                    build_btl_block s,
+                    iinfo )
+            | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
+        | None ->
+            debug "BLOCK END.\n";
+            next_nodes := !next_nodes @ successors_inst inst;
+            translate_inst iinfo inst true
+      in
+      let ib = build_btl_block e in
+      let succs = !next_nodes in
+      let bi = mk_binfo (p2i e) in
+      let ibf = { entry = ib; input_regs = Regset.empty; binfo = bi } in
+      btl_code := PTree.set e ibf !btl_code;
+      List.iter build_btl_tree succs)
+  in
+  build_btl_tree entry;
+  !btl_code
+
+let rtl2btl (f : RTL.coq_function) =
+  (*debug_flag := true;*)
+  let code = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let join_points = get_join_points code entry in
+  let btl = translate_function code entry join_points in
+  let dm = PTree.map (fun n i -> n) btl in
+  debug "Entry %d\n" (p2i entry);
+  debug "RTL Code: ";
+  (*print_code code;*)
+  debug "BTL Code: ";
+  print_btl_code stderr btl true;
+  debug "Dupmap:\n";
+  print_ptree print_pint dm;
+  debug "Join points: ";
+  print_true_nodes join_points;
+  debug "\n";
+  (*debug_flag := false;*)
+  ((btl, entry), dm)
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 633e1b8e..7ad1472b 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -231,25 +231,24 @@ Proof.
   induction ib; simpl; auto; lia.
 Qed.
 
+(* TODO gourdinl remove useless lemma? *)
 Lemma entry_isnt_goto dupmap f pc ib:
   match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None ->
   is_goto (entry ib) = false.
 Proof.
   intros.
   destruct (entry ib); trivial.
-  destruct fi; trivial. inv H. inv H4.
+  destruct fi; trivial. inv H. inv H5.
 Qed.
 
 Lemma expand_entry_isnt_goto dupmap f pc ib:
   match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None ->
   is_goto (expand (entry ib) None) = false.
 Proof.
-  destruct (is_goto (expand (entry ib) None))eqn:EQG.
-  - destruct (expand (entry ib) None);
-    try destruct fi; try discriminate; trivial.
-    intros; inv H; inv H4.
-  - destruct (expand (entry ib) None);
-    try destruct fi; try discriminate; trivial.
+  destruct (is_goto (expand (entry ib) None))eqn:EQG;
+  destruct (expand (entry ib) None);
+  try destruct fi; try discriminate; trivial.
+  intros; inv H; inv H5.
 Qed.
 
 Lemma list_nth_z_rev_dupmap:
@@ -315,7 +314,7 @@ Proof.
   destruct ofin; simpl; auto.
 Qed.
 
-(* TODO useless? *)
+(* TODO gourdinl useless? *)
 Lemma expand_iblock_istep_run_Some_rec sp ib rs0 m0 rs1 m1 ofin1:
   forall (ISTEP: iblock_istep_run tge sp ib rs0 m0 =
   Some {| _rs := rs1; _m := m1; _fin := ofin1 |})
@@ -500,10 +499,10 @@ Proof.
   destruct (is_goto ib2) eqn:GT.
   destruct ib2; try destruct fi; try discriminate.
   - (* Bgoto *)
-    inv MSS2. inversion MIB; subst; try inv H3.
-    remember H0 as ODUPLIC; clear HeqODUPLIC.
+    inv MSS2. inversion MIB; subst; try inv H4.
+    remember H2 as ODUPLIC; clear HeqODUPLIC.
     eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-    apply DMC in H0 as [ib [FNC MI]]; clear DMC.
+    apply DMC in H2 as [ib [FNC MI]]; clear DMC.
     eexists; left; eexists; split.
     + repeat econstructor; eauto.
       apply iblock_istep_run_equiv in BTL_RUN; eauto.