Adding a BTL record to help oracles

7 files changed, 265 insertions, 165 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 3daa40c4..44c25b75 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -23,24 +23,29 @@ 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 *)
 
+(* node_info is a ghost record to provide and transfert information through oracles *)
+Record node_info := {
+  _pos: node
+}.
+
 (** final instructions (that stops block execution) *)
 Inductive final: Type :=
   | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *)
-  | Breturn (res: option reg)
+  | Breturn (res: option reg) (ni: node_info)
       (** terminates the execution of the current function.  It returns the value of the given
           register, or [Vundef] if none is given. *)
-  | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit)
+  | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) (ni: node_info)
       (** invokes the function determined by [fn] (either a function pointer found in a register or a
           function name), giving it the values of registers [args] as arguments.
           It stores the return value in [dest] and branches to [succ]. *)
-  | Btailcall (sig:signature) (fn: reg + ident) (args: list reg)
+  | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) (ni: node_info)
       (**  performs a function invocation in tail-call position 
           (the current function terminates after the call, returning the result of the callee)  
       *)
-  | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit)
+  | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) (ni: node_info)
       (** calls the built-in function identified by [ef], giving it the values of [args] as arguments.
           It stores the return value in [dest] and branches to [succ]. *)
-  | Bjumptable (arg:reg) (tbl:list exit)
+  | Bjumptable (arg:reg) (tbl:list exit) (ni: node_info)
       (** [Bjumptable arg tbl] transitions to the node that is the [n]-th
           element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *)
   .
@@ -50,14 +55,14 @@ Inductive iblock: Type :=
 (* final instructions that stops block execution *)
   | BF (fi: final)
 (* basic instructions that continues block execution, except when aborting *)
-  | Bnop (* nop instruction *)
-  | Bop (op:operation) (args:list reg) (dest:reg) 
+  | Bnop (ni: node_info) (* nop instruction *)
+  | Bop (op:operation) (args:list reg) (dest:reg) (ni: node_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) (ni: node_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) (ni: node_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,7 +70,7 @@ 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) (info:option bool) (ni: node_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].
@@ -195,23 +200,23 @@ 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_nop rs m ni: iblock_istep sp rs m (Bnop ni) rs m None
+  | exec_op rs m op args res v ni
      (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 ni) (rs#res <- v) m None
+  | exec_load_TRAP rs m chunk addr args dst a v ni
      (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 ni) (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' ni
      (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 ni) 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 +224,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 i b rs' m' ofin ni
      (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 i ni) rs' m' ofin
   .
 Local Hint Constructors iblock_istep: core.
 
@@ -234,18 +239,18 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
   | 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 |}
@@ -256,7 +261,7 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
       | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m)
       | _ => Some out1 (* stop execution on the 1st final instruction *)
       end
-  | Bcond cond args ifso ifnot _ =>
+  | Bcond cond args ifso ifnot _ _ =>
       SOME b <- eval_condition cond rs##args m IN
       iblock_istep_run sp (if b then ifso else ifnot) rs m
   end.
@@ -275,32 +280,32 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
   | exec_Bgoto pc:
       final_step stack f sp rs m (Bgoto pc) E0
                  (State stack f sp pc rs m)
-  | exec_Breturn or stk m':
+  | exec_Breturn or stk m' ni:
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      final_step stack f sp rs m (Breturn or)
+      final_step stack f sp rs m (Breturn or ni)
         E0 (Returnstate stack (regmap_optget or Vundef rs) m')
-  | exec_Bcall sig ros args res pc' fd:
+  | exec_Bcall sig ros args res pc' fd ni:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      final_step stack f sp rs m (Bcall sig ros args res pc')
+      final_step stack f sp rs m (Bcall sig ros args res pc' ni)
         E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
-  | exec_Btailcall sig ros args stk m' fd:
+  | exec_Btailcall sig ros args stk m' fd ni:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      final_step stack f sp rs m (Btailcall sig ros args)
+      final_step stack f sp rs m (Btailcall sig ros args ni)
         E0 (Callstate stack fd rs##args m')
-  | exec_Bbuiltin ef args res pc' vargs t vres m':
+  | exec_Bbuiltin ef args res pc' vargs t vres m' ni:
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
-      final_step stack f sp rs m (Bbuiltin ef args res pc')
+      final_step stack f sp rs m (Bbuiltin ef args res pc' ni)
          t (State stack f sp pc' (regmap_setres res vres rs) m')
-  | exec_Bjumptable arg tbl n pc':
+  | exec_Bjumptable arg tbl n pc' ni:
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      final_step stack f sp rs m (Bjumptable arg tbl)
+      final_step stack f sp rs m (Bjumptable arg tbl ni)
         E0 (State stack f sp pc' rs m)
 .
 
@@ -388,16 +393,16 @@ Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop
   | mfi_goto pc pc':
       dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc')
 *)
-  | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or)
-  | mfi_call pc pc' s ri lr r:
-      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc')
-  | mfi_tailcall s ri lr:
-      match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr)
-  | mfi_builtin pc pc' ef la br:
-      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc')
-  | mfi_jumptable ln ln' r:
+  | mfi_return or ni: match_final_inst dupmap (Breturn or ni) (Ireturn or)
+  | mfi_call pc pc' s ri lr r ni:
+      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc ni) (Icall s ri lr r pc')
+  | mfi_tailcall s ri lr ni:
+      match_final_inst dupmap (Btailcall s ri lr ni) (Itailcall s ri lr)
+  | mfi_builtin pc pc' ef la br ni:
+      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc ni) (Ibuiltin ef la br pc')
+  | mfi_jumptable ln ln' r ni:
       list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' ->
-      match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln')
+      match_final_inst dupmap (Bjumptable r ln ni) (Ijumptable r ln')
 .
 
 Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop :=
@@ -416,18 +421,18 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i
       cfg!pc = Some i ->
       match_final_inst dupmap fi i ->
       match_iblock dupmap cfg isfst pc (BF fi) None
-  | mib_nop isfst pc pc':
+  | mib_nop isfst pc pc' ni:
       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 ni) (Some pc')
+  | mib_op isfst pc pc' op lr r ni:
       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 ni) (Some pc')
+  | mib_load isfst pc pc' m a lr r ni:
       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 ni) (Some pc')
+  | mib_store isfst pc pc' m a lr r ni:
       cfg!pc = Some (Istore m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc')
+      match_iblock dupmap cfg isfst pc (Bstore m a lr r ni) (Some pc')
   | mib_exit pc pc': 
       dupmap!pc = (Some pc') ->
       match_iblock dupmap cfg false pc' (Bgoto pc) None
@@ -445,12 +450,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':
+  | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i' ni:
       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 i ni) opc
   .
 
 Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop :=
@@ -530,14 +535,14 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           if negb isfst then
             OK None
           else Error (msg "BTL.verify_block: isfst is true Bgoto")
-      | Breturn or =>
+      | Breturn or _ =>
           match cfg!pc with
           | Some (Ireturn or') =>
               if option_eq Pos.eq_dec or or' then OK None
               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 =>
+      | Bcall s ri lr r pc1 _ =>
           match cfg!pc with
           | Some (Icall s' ri' lr' r' pc2) =>
               do u <- verify_is_copy dupmap pc1 pc2;
@@ -551,7 +556,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               else Error (msg "BTL.verify_block: different signatures in Bcall")
           | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall")
           end
-      | Btailcall s ri lr =>
+      | Btailcall s ri lr _ =>
           match cfg!pc with
           | Some (Itailcall s' ri' lr') =>
               if (signature_eq s s') then
@@ -562,7 +567,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               else Error (msg "BTL.verify_block: different signatures in Btailcall")
           | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall")
           end
-      | Bbuiltin ef la br pc1 =>
+      | Bbuiltin ef la br pc1 _ =>
           match cfg!pc with
           | Some (Ibuiltin ef' la' br' pc2) =>
               do u <- verify_is_copy dupmap pc1 pc2;
@@ -574,7 +579,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               else Error (msg "BTL.verify_block: different ef in Bbuiltin")
           | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin")
           end
-      | Bjumptable r ln =>
+      | Bjumptable r ln _ =>
           match cfg!pc with
           | Some (Ijumptable r' ln') =>
               do u <- verify_is_copy_list dupmap ln ln';
@@ -583,12 +588,12 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable")
           end
       end
-  | Bnop =>
+  | Bnop _ =>
       match cfg!pc with
       | Some (Inop pc') => OK (Some pc')
       | _ => 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
@@ -600,7 +605,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           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
@@ -616,7 +621,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           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
@@ -636,7 +641,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           verify_block dupmap cfg false pc' b2
       | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)")
       end
-  | Bcond c lr bso bnot i =>
+  | Bcond c lr bso bnot i _ =>
       match cfg!pc with
       | Some (Icond c' lr' pcso pcnot i') =>
           if (list_eq_dec Pos.eq_dec lr lr') then
@@ -794,7 +799,7 @@ Definition is_goto (ib: iblock): bool :=
 
 Definition is_atom (ib: iblock): bool :=
  match ib with
- | Bseq _ _ | Bcond _ _ _ _ _ => false 
+ | Bseq _ _ | Bcond _ _ _ _ _ _ => false 
  | _ => true
  end.
 
@@ -804,10 +809,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 i ni:
      is_expand ib1 ->
      is_expand ib2 -> 
-     is_expand (Bcond cond args ib1 ib2 i)
+     is_expand (Bcond cond args ib1 ib2 i ni)
   | exp_others ib:
      is_atom ib = true ->
      is_expand ib
@@ -817,8 +822,8 @@ 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
+  | Bcond cond args ib1 ib2 i ni => 
+     Bcond cond args (expand ib1 k) (expand ib2 k) i ni
   | BF fin => fin
   | ib => 
     match k with 
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index b9a05a8a..94d299e7 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -557,21 +557,21 @@ Qed.
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
   match i with
   | Bgoto pc => Sgoto pc
-  | Bcall sig ros args res pc => 
+  | Bcall sig ros args res pc _ => 
     let svos := sum_left_map sis.(si_sreg) ros in
     let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
     Scall sig svos sargs res pc
-  | Btailcall sig ros args =>
+  | Btailcall sig ros args _ =>
     let svos := sum_left_map sis.(si_sreg) ros in
     let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
     Stailcall sig svos sargs
-  | Bbuiltin ef args res pc =>
+  | Bbuiltin ef args res pc _ =>
     let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
     Sbuiltin ef sargs res pc
-  | Breturn or => 
+  | Breturn or _ => 
     let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
     Sreturn sor
-  | Bjumptable reg tbl =>
+  | Bjumptable reg tbl _ =>
     let sv := sis.(si_sreg) reg in
     Sjumptable sv tbl
   end.
@@ -772,15 +772,15 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
   match ib with
   | 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) 
-  | Bcond cond args ifso ifnot _ =>
+  | Bcond cond args ifso ifnot _ _ =>
       let args := list_sval_inj (List.map sis.(si_sreg) args) in
       let ifso := sexec_rec ifso sis k in
       let ifnot := sexec_rec ifnot sis k in
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index 3d8d44d0..dd7ba4c7 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -1,5 +1,103 @@
 open Maps
-open BinNums
+open BTL
+open RTL
+open Camlcoq
+open AuxTools
+open DebugPrint
+open PrintBTL
 
-let btl2rtl f =
-  ((PTree.empty, Coq_xH), PTree.empty)
+let is_atom = function
+  | Bseq (_, _) | Bcond (_, _, _, _, _, _) -> false
+  | _ -> true
+
+let rec get_nn = function
+  | Bnop ni
+  | Bop (_, _, _, ni)
+  | Bload (_, _, _, _, _, ni)
+  | Bstore (_, _, _, _, ni)
+  | Bcond (_, _, _, _, _, ni)
+  | BF (Breturn (_, ni))
+  | BF (Bcall (_, _, _, _, _, ni))
+  | BF (Btailcall (_, _, _, ni))
+  | BF (Bbuiltin (_, _, _, _, ni))
+  | BF (Bjumptable (_, _, ni)) ->
+      ni
+  | BF (Bgoto s) -> s
+  | Bseq (ib1, _) -> get_nn ib1
+
+let translate_function code entry =
+  let reached = ref (PTree.map (fun n i -> false) code) in
+  let rtl_code = ref PTree.empty in
+  let rec build_rtl_tree e =
+    if get_some @@ PTree.get e !reached then ()
+    else (
+      reached := PTree.set e true !reached;
+      let next_nodes = ref [] in
+      let ib = (get_some @@ PTree.get e code).entry in
+      let rec translate_btl_block ib k =
+        print_btl_inst stderr ib;
+        let rtli =
+          match ib with
+          | Bcond (cond, lr, BF (Bgoto s1), BF (Bgoto s2), info, ni) ->
+              next_nodes := s1 :: s2 :: !next_nodes;
+              Some (Icond (cond, lr, s1, s2, info), ni)
+          | Bcond (cond, lr, BF (Bgoto s1), ib2, info, ni) ->
+              assert (info = Some false);
+              next_nodes := s1 :: !next_nodes;
+              translate_btl_block ib2 None;
+              Some (Icond (cond, lr, s1, get_nn ib2, info), ni)
+          (* 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 ni -> Some (Inop (get_nn (get_some k)), ni)
+          | Bop (op, lr, rd, ni) ->
+              Some (Iop (op, lr, rd, get_nn (get_some k)), ni)
+          | Bload (trap, chk, addr, lr, rd, ni) ->
+              Some (Iload (trap, chk, addr, lr, rd, get_nn (get_some k)), ni)
+          | Bstore (chk, addr, lr, rd, ni) ->
+              Some (Istore (chk, addr, lr, rd, get_nn (get_some k)), ni)
+          | BF (Bcall (sign, fn, lr, rd, s, ni)) ->
+              next_nodes := s :: !next_nodes;
+              Some (Icall (sign, fn, lr, rd, s), ni)
+          | BF (Btailcall (sign, fn, lr, ni)) ->
+              Some (Itailcall (sign, fn, lr), ni)
+          | BF (Bbuiltin (ef, lr, rd, s, ni)) ->
+              next_nodes := s :: !next_nodes;
+              Some (Ibuiltin (ef, lr, rd, s), ni)
+          | BF (Bjumptable (arg, tbl, ni)) -> Some (Ijumptable (arg, tbl), ni)
+          | BF (Breturn (oreg, ni)) -> Some (Ireturn oreg, ni)
+          | BF (Bgoto s) ->
+              next_nodes := s :: !next_nodes;
+              None
+        in
+        match rtli with
+        | Some (inst, ni) -> rtl_code := PTree.set ni 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" (P.to_int 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..6c894b78 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -263,7 +263,7 @@ Proof.
       eapply plus_trans; eauto.
   - (* exec_cond *)
     inv MIB.
-    rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *)
+    rename H11 into JOIN. (* is_join_opt opc1 opc2 opc *)
     destruct b; exploit IHIBIS; eauto.
     + (* taking ifso *)
       destruct ofin; simpl.
@@ -305,14 +305,14 @@ Proof.
     erewrite <- preserv_fnstacksize; eauto.
     econstructor; eauto.
   - (* call *)
-    rename H7 into FIND.
+    rename H8 into FIND.
     exploit find_function_preserved; eauto.
     intros (fd' & FIND' & TRANSFU).
     eexists; split. eapply exec_Icall; eauto.
     apply function_sig_translated. assumption.
     repeat (econstructor; eauto).
   - (* tailcall *)
-    rename H2 into FIND.
+    rename H3 into FIND.
     exploit find_function_preserved; eauto.
     intros (fd' & FIND' & TRANSFU).
     eexists; split. eapply exec_Itailcall; eauto.
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
index b461e3f1..4b14d28e 100644
--- a/scheduling/PrintBTL.ml
+++ b/scheduling/PrintBTL.ml
@@ -8,84 +8,80 @@ open PrintAST
 
 (* Printing of BTL code *)
 
-let reg pp r =
-  fprintf pp "x%d" (P.to_int r)
+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
+  | [ 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_succ pp s = fprintf pp "\tsucc %d\n" (P.to_int s)
 
-let print_pref pp pref =
-  fprintf pp "%s" pref
+let print_pref pp pref = fprintf pp "%s" pref
 
 let rec print_iblock pp is_rec pref ib =
   match ib with
-  | Bnop ->
+  | Bnop _ ->
       print_pref pp pref;
       fprintf pp "Bnop\n"
-  | Bop(op, args, res) ->
+  | 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) ->
+      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) ->
+      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)) ->
+      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;
+      fprintf pp "Bcall: %a = %a(%a)\n" reg res ros fn regs args;
       print_succ pp s
-  | BF (Btailcall(sg, fn, args)) ->
+  | 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)) ->
+      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;
+      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, info) ->
+  | Bcond (cond, args, ib1, ib2, info, _) ->
       print_pref pp pref;
       fprintf pp "Bcond: (%a) (prediction: %s)\n"
-        (PrintOp.print_condition reg) (cond, args)
-        (match info 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)) ->
+        (PrintOp.print_condition reg)
+        (cond, args)
+        (match info 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) ->
+  | BF (Breturn (None, _)) ->
       print_pref pp pref;
       fprintf pp "Breturn\n"
-  | BF (Breturn (Some arg)) ->
+  | BF (Breturn (Some arg, _)) ->
       print_pref pp pref;
       fprintf pp "Breturn: %a\n" reg arg
   | BF (Bgoto s) ->
@@ -97,28 +93,26 @@ let rec print_iblock pp is_rec pref ib =
         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_inst pp ib = print_iblock pp false "  " ib
 
 let print_btl_code pp btl is_rec =
   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);
+  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"
 
 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
+  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
-  | _ -> ()
+  match gd with Gfun (Internal f) -> print_function pp id f | _ -> ()
 
-let print_program pp (prog: BTL.program) =
+let print_program pp (prog : BTL.program) =
   List.iter (print_globdef pp) prog.prog_defs
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index e14e0ab3..859bbf07 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -7,34 +7,36 @@ open PrintBTL
 open Camlcoq
 open AuxTools
 
+let mk_ni n = n
+
 let encaps_final inst osucc =
   match inst with
   | BF _ | Bcond _ -> inst
   | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
 
-let translate_inst inst is_final =
+let translate_inst ni inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
     | Inop s ->
         osucc := Some s;
-        Bnop
+        Bnop ni
     | Iop (op, lr, rd, s) ->
         osucc := Some s;
-        Bop (op, lr, rd)
+        Bop (op, lr, rd, ni)
     | Iload (trap, chk, addr, lr, rd, s) ->
         osucc := Some s;
-        Bload (trap, chk, addr, lr, rd)
+        Bload (trap, chk, addr, lr, rd, ni)
     | Istore (chk, addr, lr, rd, s) ->
         osucc := Some s;
-        Bstore (chk, addr, lr, rd)
-    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s))
-    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr))
-    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s))
+        Bstore (chk, addr, lr, rd, ni)
+    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s, ni))
+    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr, ni))
+    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s, ni))
     | Icond (cond, lr, ifso, ifnot, info) ->
-        Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info)
-    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl))
-    | Ireturn oreg -> BF (Breturn oreg)
+        Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info, ni)
+    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl, ni))
+    | Ireturn oreg -> BF (Breturn (oreg, ni))
   in
   if is_final then encaps_final btli !osucc else btli
 
@@ -50,6 +52,7 @@ let translate_function code entry join_points =
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
         let psucc = predicted_successor inst in
+        let ni = mk_ni n in
         let succ =
           match psucc with
           | Some ps ->
@@ -67,12 +70,12 @@ let translate_function code entry join_points =
                 (* TODO gourdinl remove this *)
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
-                Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info)
-            | _ -> Bseq (translate_inst inst false, build_btl_block s))
+                Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info, ni)
+            | _ -> Bseq (translate_inst ni inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
             next_nodes := !next_nodes @ successors_inst inst;
-            translate_inst inst true
+            translate_inst ni inst true
       in
       let ib = build_btl_block e in
       let succs = !next_nodes in
@@ -84,12 +87,12 @@ let translate_function code entry join_points =
   !btl_code
 
 let print_dm dm =
-  List.iter (fun (n,n') ->
-    debug "%d -> %d" (P.to_int n) (P.to_int n');
-    (*print_btl_inst stderr ib.entry;*)
-    debug "\n"
-    )
-  (PTree.elements dm)
+  List.iter
+    (fun (n, n') ->
+      debug "%d -> %d" (P.to_int n) (P.to_int n');
+      (*print_btl_inst stderr ib.entry;*)
+      debug "\n")
+    (PTree.elements dm)
 
 let rtl2btl (f : RTL.coq_function) =
   debug_flag := true;
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index f89ea5cf..6681d691 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -215,7 +215,7 @@ type defined below. Intuitively, each RTL step corresponds to either
 Fixpoint measure ib: nat :=
   match ib with
   | Bseq ib1 ib2
-  | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2
+  | Bcond _ _ ib1 ib2 _ _ => measure ib1 + measure ib2
   | ib => 1
   end.