preparing compiler passes and ml oracles

6 files changed, 37 insertions, 12 deletions

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: