start the new "BTL" IR.

1 files changed, 127 insertions, 0 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
new file mode 100644
index 00000000..26b5bae6
--- /dev/null
+++ b/scheduling/BTLtoRTLproof.v
@@ -0,0 +1,127 @@
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import RTL Op Registers OptionMonad BTL.
+
+Require Import Errors Linking BTLtoRTL.
+
+
+(*****************************)
+(* Put this in an other file *)
+
+Require Import Linking.
+
+Lemma transf_function_correct f f':
+  transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
+Proof.
+  unfold transf_function; unfold bind. repeat autodestruct.
+  intros H _ _ X. inversion X; subst; clear X.
+  eexists; eapply verify_function_correct; simpl; eauto.
+Qed.
+
+Lemma transf_fundef_correct f f':
+  transf_fundef f = OK f' -> match_fundef f f'.
+Proof.
+  intros TRANSF; destruct f; simpl; monadInv TRANSF.
+  + exploit transf_function_correct; eauto.
+    intros (dupmap & MATCH_F).
+    eapply match_Internal; eauto.
+  + eapply match_External.
+Qed.
+
+Definition match_prog (p: program) (tp: RTL.program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. eapply match_transform_partial_program_contextual; eauto.
+Qed.
+
+Section RTL_SIMULATES_BTL.
+
+Variable prog: program.
+Variable tprog: RTL.program.
+
+Hypothesis TRANSL: match_prog prog tprog.
+
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
+Qed.
+
+Lemma senv_preserved: Senv.equiv ge tge.
+Proof.
+  eapply (Genv.senv_match TRANSL).
+Qed.
+
+Lemma functions_translated (v: val) (f: fundef):
+  Genv.find_funct ge v = Some f ->
+  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog.
+Proof.
+  intros. exploit (Genv.find_funct_match TRANSL); eauto.
+  intros (cu & tf & A & B & C).
+  repeat eexists; intuition eauto.
+  + unfold incl; auto.
+  + eapply linkorder_refl.
+Qed.
+
+Lemma function_ptr_translated v f:
+  Genv.find_funct_ptr ge v = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
+Proof.
+  intros.
+  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
+Qed.
+
+Lemma function_sig_translated f tf: transf_fundef f = OK tf -> RTL.funsig tf = funsig f.
+Proof.
+  intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
+  erewrite preserv_fnsig; eauto.
+Qed.
+
+Lemma transf_initial_states s1:
+  initial_state prog s1 ->
+  exists s2, RTL.initial_state tprog s2 /\ match_states s1 s2.
+Proof.
+  intros. inv H.
+  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
+  eexists. split.
+  - econstructor; eauto.
+    + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
+      symmetry. eapply match_program_main. eauto.
+    + erewrite function_sig_translated; eauto.
+  - constructor; eauto.
+    constructor.
+    apply transf_fundef_correct; auto.
+Qed.
+
+Lemma transf_final_states s1 s2 r:
+  match_states s1 s2 -> final_state s1 r -> RTL.final_state s2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem plus_simulation s1 t s1':
+  step ge s1 t s1' ->
+  forall s2 (MS: match_states s1 s2),
+  exists s2',
+     plus RTL.step tge s2 t s2'
+  /\ match_states s1' s2'.
+Admitted. (* TODO: première étape *)
+
+Theorem transf_program_correct:
+  forward_simulation (semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_plus with match_states.
+  - eapply senv_preserved.
+  - eapply transf_initial_states.
+  - eapply transf_final_states.
+  - eapply plus_simulation.
+Qed.
+
+End RTL_SIMULATES_BTL.