1 files changed, 363 insertions, 0 deletions

diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
new file mode 100644
index 00000000..4ba197b0
--- /dev/null
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -0,0 +1,363 @@
+Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
+Require Import Coqlib Maps Events Errors Op.
+Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory.
+Require Import RTLpathScheduler.
+
+Definition match_prog (p tp: 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 PRESERVATION.
+
+Variable prog: program.
+Variable tprog: program.
+
+Hypothesis TRANSL: match_prog prog tprog.
+
+Let pge := Genv.globalenv prog.
+Let tpge := Genv.globalenv tprog.
+
+Hypothesis all_fundef_liveness_ok: forall b fd, Genv.find_funct_ptr pge b = Some fd -> liveness_ok_fundef fd.
+
+Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s.
+Proof.
+  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
+Qed.
+
+Lemma senv_preserved:
+  Senv.equiv pge tpge.
+Proof.
+  eapply (Genv.senv_match TRANSL).
+Qed.
+
+Lemma functions_preserved:
+  forall (v: val) (f: fundef),
+  Genv.find_funct pge v = Some f ->
+  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tpge 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_preserved:
+  forall v f,
+  Genv.find_funct_ptr pge v = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf.
+Proof.
+  intros.
+  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
+Qed.
+
+Lemma function_sig_preserved:
+  forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f.
+Proof.
+  intros. destruct f.
+  - simpl in H. monadInv H.
+    destruct (transf_function f) as [res H]; simpl in * |- *; auto.
+    destruct (H _ EQ).
+    intuition subst; auto.
+    symmetry.
+    eapply match_function_preserves.
+    eassumption.
+  - simpl in H. monadInv H. reflexivity.
+Qed.
+
+Theorem transf_initial_states:
+  forall s1, initial_state prog s1 ->
+  exists s2, initial_state tprog s2 /\ match_states s1 s2.
+Proof.
+  intros. inv H.
+  exploit function_ptr_preserved; eauto. intros (tf & FIND &  TRANSF).
+  exists (Callstate nil tf nil m0).
+  split.
+  - econstructor; eauto.
+    + intros; apply (Genv.init_mem_match TRANSL); assumption.
+    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
+      symmetry. eapply match_program_main. eauto.
+    + destruct f.
+      * monadInv TRANSF. rewrite <- H3.
+        destruct (transf_function f) as [res H]; simpl in * |- *; auto.
+        destruct (H _ EQ).
+        intuition subst; auto.
+        symmetry; eapply match_function_preserves. eassumption.
+      * monadInv TRANSF. assumption.
+  - constructor; eauto.
+    + constructor.
+    + apply transf_fundef_correct; auto.
+(*     + eapply all_fundef_liveness_ok; eauto. *)
+Qed.
+
+Theorem transf_final_states s1 s2 r:
+  final_state s1 r -> match_states s1 s2 -> final_state s2 r.
+Proof.
+  unfold final_state.
+  intros H; inv H.
+  intros H; inv H; simpl in * |- *; try congruence.
+  inv H1.
+  destruct st; simpl in * |- *; try congruence.
+  inv STACKS. constructor.
+Qed.
+
+
+Let ge := Genv.globalenv (RTLpath.transf_program prog).
+Let tge := Genv.globalenv (RTLpath.transf_program tprog).
+
+Lemma senv_sym x y: Senv.equiv x y -> Senv.equiv y x.
+Proof.
+  unfold Senv.equiv. intuition congruence.
+Qed.
+
+Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
+Proof.
+  unfold Senv.equiv. intuition congruence.
+Qed.
+
+Lemma senv_preserved_RTL:
+  Senv.equiv ge tge.
+Proof.
+  eapply senv_transitivity. { eapply senv_sym; eapply RTLpath.senv_preserved. }
+  eapply senv_transitivity. { eapply senv_preserved. }
+  eapply RTLpath.senv_preserved.
+Qed.
+
+Lemma symbols_preserved_RTL s: Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  unfold tge, ge. erewrite RTLpath.symbols_preserved; eauto.
+  rewrite symbols_preserved.
+  erewrite RTLpath.symbols_preserved; eauto.
+Qed.
+
+Program Definition mkctx sp rs0 m0 {f1: RTLpath.function} (hyp: liveness_ok_function f1)
+   :  simu_proof_context f1
+   := {| the_ge1:= ge; the_ge2 := tge; the_sp:=sp; the_rs0:=rs0; the_m0:=m0 |}.
+Obligation 2.
+  erewrite symbols_preserved_RTL. eauto.
+Qed.
+
+Lemma s_find_function_preserved f sp svos1 svos2 rs0 m0 fd
+  (LIVE: liveness_ok_function f):
+  (svident_simu f (mkctx sp rs0 m0 LIVE) svos1 svos2) ->
+  sfind_function pge ge sp svos1 rs0 m0 = Some fd ->
+  exists fd', sfind_function tpge tge sp svos2 rs0 m0 = Some fd'
+              /\ transf_fundef fd = OK fd'
+              /\ liveness_ok_fundef fd.
+Proof.
+  Local Hint Resolve symbols_preserved_RTL: core.
+  unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *.
+  + rewrite !(seval_preserved ge tge) in *; eauto.
+    destruct (seval_sval _ _ _ _); try congruence.
+    erewrite <- SIMU; try congruence. clear SIMU.
+    intros; exploit functions_preserved; eauto.
+    intros (fd' & cunit & (X1 & X2 & X3)). eexists.
+    repeat split; eauto.
+    eapply find_funct_liveness_ok; eauto.
+(*     intros. eapply all_fundef_liveness_ok; eauto. *)
+  + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
+    intros; exploit function_ptr_preserved; eauto.
+    intros (fd' & X). eexists. intuition eauto.
+(*     intros. eapply all_fundef_liveness_ok; eauto. *)
+Qed.
+
+Lemma sistate_simu f dupmap sp st st' rs m is 
+  (LIVE: liveness_ok_function f):
+  ssem_internal ge sp st rs m is ->
+  sistate_simu dupmap f st st' (mkctx sp rs m LIVE)->
+  exists is',
+    ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap is is'.
+Proof.
+  intros SEM X; eapply X; eauto.
+Qed.
+
+Lemma seval_builtin_sval_preserved sp rs m:
+  forall bs, seval_builtin_sval ge sp bs rs m = seval_builtin_sval tge sp bs rs m.
+Proof.
+  induction bs.
+  all: try (simpl; try reflexivity; erewrite seval_preserved by eapply symbols_preserved_RTL; reflexivity).
+  all: simpl; rewrite IHbs1; rewrite IHbs2; reflexivity.
+Qed.
+
+Lemma seval_list_builtin_sval_preserved sp rs m:
+  forall lbs,
+  seval_list_builtin_sval ge sp lbs rs m = seval_list_builtin_sval tge sp lbs rs m.
+Proof.
+  induction lbs; [simpl; reflexivity|].
+  simpl. rewrite seval_builtin_sval_preserved. rewrite IHlbs.
+  reflexivity.
+Qed.
+
+Lemma ssem_final_simu dm f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s
+  (LIVE: liveness_ok_function f):
+  match_function dm f f' ->
+  list_forall2 match_stackframes stk stk' ->
+  (* s_istate_simu f dupmap st st' -> *)
+  sfval_simu dm f st.(si_pc) st'.(si_pc) (mkctx sp rs0 m0 LIVE) sv sv' ->
+  ssem_final pge ge sp st.(si_pc) stk f rs0 m0 sv rs m t s ->
+  exists s', ssem_final tpge tge sp st'.(si_pc) stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
+Proof.
+  Local Hint Resolve transf_fundef_correct: core.
+  intros FUN STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl in *.
+  - (* Snone *)
+    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
+    intros (path & PATH).
+    eexists; split; econstructor; eauto.
+    eapply eqlive_reg_refl.
+  - (* Scall *)
+    exploit s_find_function_preserved; eauto.
+    intros (fd' & FIND & TRANSF & LIVE').
+    erewrite <- function_sig_preserved; eauto.
+    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
+    intros (path & PATH).
+    eexists; split; econstructor; eauto.
+    + eapply eq_trans; try eassumption; auto.
+    + simpl. repeat (econstructor; eauto).
+  - (* Stailcall *)
+    exploit s_find_function_preserved; eauto.
+    intros (fd' & FIND & TRANSF & LIVE').
+    erewrite <- function_sig_preserved; eauto.
+    eexists; split; econstructor; eauto.
+    + erewrite <- preserv_fnstacksize; eauto.
+    + eapply eq_trans; try eassumption; auto.
+  - (* Sbuiltin *)
+    pose senv_preserved_RTL as SRTL.
+    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
+    intros (path & PATH).
+    eexists; split; econstructor; eauto.
+    + eapply seval_builtin_args_preserved; eauto.
+      eapply seval_list_builtin_sval_correct; eauto.
+      rewrite H0.
+      erewrite seval_list_builtin_sval_preserved; eauto.
+    + eapply external_call_symbols_preserved; eauto.
+    + eapply eqlive_reg_refl.
+  - (* Sjumptable *)
+    exploit ptree_get_list_nth_rev; eauto. intros (p2 & LNZ & DM).
+    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
+    intros (path & PATH).
+    eexists; split; econstructor; eauto.
+    + eapply eq_trans; try eassumption; auto.
+    + eapply eqlive_reg_refl.
+  - (* Sreturn *)
+    eexists; split; econstructor; eauto.
+    erewrite <- preserv_fnstacksize; eauto.
+  - (* Sreturn bis *)
+    eexists; split; econstructor; eauto.
+    + erewrite <- preserv_fnstacksize; eauto.
+    + rewrite <- H. erewrite <- seval_preserved; eauto.
+Qed.
+
+(* The main theorem on simulation of symbolic states ! *)
+Theorem ssem_sstate_simu dm f f' stk stk' sp st st' rs m t s:
+  match_function dm f f' ->
+  liveness_ok_function f ->
+  list_forall2 match_stackframes stk stk' ->
+  ssem pge ge sp st stk f rs m t s ->
+  (forall ctx: simu_proof_context f, sstate_simu dm f st st' ctx) ->
+  exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
+Proof.
+  intros MFUNC LIVE STACKS SEM SIMU.
+  destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU.
+  destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl.
+  - (* sem_early *)
+    exploit sistate_simu; eauto.
+    unfold istate_simu; rewrite CONT.
+    intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')).
+    exists (State stk' f' sp (ipc is') (irs is') (imem is')).
+    split.
+    + eapply ssem_early; auto. congruence.
+    + rewrite M'. econstructor; eauto.
+  - (* sem_normal *)
+    exploit sistate_simu; eauto.
+    unfold istate_simu; rewrite CONT.
+    intros (is' & SEM' & (CONT' & RS' & M')(*  & DMEQ *)).
+    rewrite <- eqlive_reg_triv in RS'.
+    exploit ssem_final_simu; eauto.
+    clear SEM2; intros (s0 & SEM2 & MATCH0).
+    exploit ssem_final_equiv; eauto.
+    clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2).
+    exists s1; split.
+    + eapply ssem_normal; eauto.
+    + eapply match_states_equiv; eauto.
+Qed.
+
+Lemma exec_path_simulation dupmap path stk stk' f f' sp rs m pc pc' t s:
+  (fn_path f)!pc = Some path ->
+  path_step ge pge path.(psize) stk f sp rs m pc t s ->
+  list_forall2 match_stackframes stk stk' ->
+  dupmap ! pc' = Some pc ->
+  match_function dupmap f f' ->
+  liveness_ok_function f ->
+  exists path' s', (fn_path f')!pc' = Some path' /\ path_step tge tpge path'.(psize) stk' f' sp rs m pc' t s' /\ match_states s s'.
+Proof.
+  intros PATH STEP STACKS DUPPC MATCHF LIVE.
+  exploit initialize_path. { eapply dupmap_path_entry2; eauto. }
+  intros (path' & PATH').
+  exists path'.
+  exploit (sexec_correct f pc pge ge sp path stk rs m t s); eauto.
+  intros (st & SYMB & SEM); clear STEP.
+  exploit dupmap_correct; eauto.
+  clear SYMB; intros (st' & SYMB & SIMU).
+  exploit ssem_sstate_simu; eauto.
+  intros (s0 & SEM0 & MATCH). 
+  exploit sexec_exact; eauto.
+  intros (s' & STEP' & EQ).
+  exists s'; intuition.
+  eapply match_states_equiv; eauto.
+Qed.
+
+Lemma step_simulation s1 t s1' s2:
+  step ge pge s1 t s1' ->
+  match_states s1 s2 ->
+  exists s2',
+     step tge tpge s2 t s2'
+  /\ match_states s1' s2'.
+Proof.
+  Local Hint Resolve eqlive_stacks_refl transf_fundef_correct: core.
+  destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]; intros MS; inv MS.
+(* exec_path *)
+  - try_simplify_someHyps. intros.
+    exploit path_step_eqlive; eauto. (* { intros. eapply all_fundef_liveness_ok; eauto. } *)
+    clear STEP EQUIV rs; intros (s2 & STEP & EQLIVE).
+    exploit exec_path_simulation; eauto.
+    clear STEP; intros (path' & s' & PATH' & STEP' & MATCH').
+    exists s'; split.
+    + eapply exec_path; eauto.
+    + eapply eqlive_match_states; eauto.
+(* exec_function_internal *)
+  - inv LIVE.
+    exploit initialize_path. { eapply (fn_entry_point_wf f). }
+    destruct 1 as (path & PATH).
+    inversion TRANSF as [f0 xf tf MATCHF|]; subst. eexists. split.
+    + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto.
+    + erewrite preserv_fnparams; eauto.
+      econstructor; eauto. 
+      { apply preserv_entrypoint; auto. }
+      { apply eqlive_reg_refl. }
+(* exec_function_external *)
+  - inversion TRANSF as [|]; subst. eexists. split.
+    + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved_RTL.
+    + constructor. assumption.
+(* exec_return *)
+  - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split.
+    + constructor.
+    + inv H1. econstructor; eauto.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (semantics prog) (semantics tprog).
+Proof.
+  eapply forward_simulation_step with match_states.
+  - eapply senv_preserved.
+  - eapply transf_initial_states.
+  - intros; eapply transf_final_states; eauto.
+  - intros; eapply step_simulation; eauto.
+Qed.
+
+End PRESERVATION.