8 files changed, 42 insertions, 21 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand
index a751b232..40ea0d68 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -298,13 +298,9 @@ EXPAND_ASM_SEMANTICS
     eapply RTLgenproof.transf_program_correct; eassumption.
 EXPAND_RTL_FORWARD_SIMULATIONS
   eapply compose_forward_simulations.
-    eapply RTLpathLivegenproof.transf_program_correct; eassumption.
-  pose proof RTLpathLivegenproof.all_fundef_liveness_ok as X.
-    refine (modusponens _ _ (X _ _ _) _); eauto. intro.
+    eapply RTLtoBTLproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
-    eapply RTLpathSchedulerproof.transf_program_correct; eassumption.
-  eapply compose_forward_simulations.
-    eapply RTLpathproof.transf_program_correct; eassumption.
+    eapply BTLtoRTLproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply Allocationproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 10a000a8..9fdf39be 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -463,8 +463,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 +472,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.
 
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..3d8d44d0
--- /dev/null
+++ b/scheduling/BTLtoRTLaux.ml
@@ -0,0 +1,5 @@
+open Maps
+open BinNums
+
+let btl2rtl f =
+  ((PTree.empty, Coq_xH), PTree.empty)
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..8ace6e2a
--- /dev/null
+++ b/scheduling/RTLtoBTLaux.ml
@@ -0,0 +1,17 @@
+open RTLpathLivegenaux
+open Maps
+open RTL
+open BinNums
+open DebugPrint
+
+let rtl2btl (f: RTL.coq_function) =
+  let code = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let join_points = get_join_points code entry in
+  Printf.eprintf "test";
+  debug_flag := true;
+  debug "Join points: ";
+  print_true_nodes join_points;
+  debug "\n";
+  debug_flag := false;
+  ((PTree.empty, Coq_xH), PTree.empty)
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 633e1b8e..5cebd33c 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -231,6 +231,7 @@ 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.
@@ -244,12 +245,10 @@ 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 H4.
 Qed.
 
 Lemma list_nth_z_rev_dupmap:
diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml
index ddb3c21a..be3c6e19 100644
--- a/tools/compiler_expand.ml
+++ b/tools/compiler_expand.ml
@@ -51,9 +51,9 @@ PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob"
 
 let post_rtl_passes =
 [|
-  PARTIAL, Always, Require, (Some "RTLpath generation"), "RTLpathLivegen", Noprint;
-  PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint;
-  TOTAL, Always, Require,  (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1)));
+  PARTIAL, Always, Require, (Some "BTL generation"), "RTLtoBTL", Noprint;
+  (*PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint;*)
+  PARTIAL, Always, Require,  (Some "Projection to RTL"), "BTLtoRTL", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1)));
   PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1");
   PARTIAL, Always, Require, (Some "Branch tunneling"), "Tunneling", (Print "LTL 2");
   PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint;