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_fundef f sp svos rs0 m0 fd
  (LIVE: liveness_ok_function f):
  sfind_function pge ge sp svos rs0 m0 = Some fd ->
  liveness_ok_fundef fd.
Proof.
  unfold sfind_function. destruct svos; simpl.
  + destruct (seval_sval _ _ _ _); try congruence.
    eapply find_funct_liveness_ok; eauto.
  + destruct (Genv.find_symbol _ _); try congruence.
    intros. eapply all_fundef_liveness_ok; eauto.
Qed.
Local Hint Resolve s_find_function_fundef: core.

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'.
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.
  + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
    intros; exploit function_ptr_preserved; eauto.
Qed.

Lemma sistate_simu f dupmap outframe sp st st' rs m is 
  (LIVE: liveness_ok_function f):
  ssem_internal ge sp st rs m is ->
  sistate_simu dupmap f outframe st st' (mkctx sp rs m LIVE)->
  exists is',
    ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap outframe 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' ->
  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 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).
    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).
    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.

Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
  (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
          (irs is) (imem is) t s)
  (SIEXEC : siexec_inst i st0 = Some s0)
  (ICHK : inst_checker (fn_path f) alive (pre_output_regs path0) i = Some tt),
  (liveness_ok_function f) ->
  list_forall2 match_stackframes stk stk' ->
  eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
  exists s' : state,
    ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone rs' (imem is) t s' /\
    eqlive_states s s'.
Proof.
  Local Hint Resolve eqlive_stacks_refl: core.
  intros ? ? ? LIVE STK EQLIVE.
  inversion SSEM2; subst; clear SSEM2.
  eexists; split.
  * econstructor.
  * generalize ICHK.
    unfold inst_checker. destruct i; simpl in *;
    unfold exit_checker; try discriminate.
    all:
      try destruct (list_mem _ _); simpl;
      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence; fail).
    4,5:
      destruct (Regset.mem _ _); destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
    1,2,3,4: assert (NPC: n=(si_pc s0)).
    all: try (inv SIEXEC; simpl; auto; fail).
    1,2,3,4:
      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence);
      simpl; inversion_SOME p;
      destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence;
      intros NPATH _; econstructor; eauto;
      try (instantiate (1:=p); rewrite <- NPC; auto; fail).
    1,2,3,4:
      eapply eqlive_reg_monotonic; eauto; simpl;
      intros; apply Regset.subset_2 in SUB_PATH;
      unfold Regset.Subset in SUB_PATH;
      apply SUB_PATH in H; auto.
    assert (NPC: n0=(si_pc s0)). { inv SIEXEC; simpl; auto. }
    inversion_SOME p.
    2: { destruct (Regset.subset _ _) eqn:?; try congruence. }
    destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
    2: { destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence. }
    simpl.
    destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence.
    inversion_SOME p'.
    destruct (Regset.subset (input_regs p') (pre_output_regs path0)) eqn:SUB_PATH; try congruence.
    intros NPATH NPATH' _. econstructor; eauto.
    instantiate (1:=p'). rewrite <- NPC; auto.
    eapply eqlive_reg_monotonic; eauto; simpl.
    intros. apply Regset.subset_2 in SUB_PATH.
    unfold Regset.Subset in SUB_PATH.
    apply SUB_PATH in H; auto.
Qed.

Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
  (liveness_ok_function f) ->
  (fn_path f) ! pc0 = Some path0 ->
  sexec f pc0 = Some st -> 
  list_forall2 match_stackframes stk stk' ->
  ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s ->
  eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
  exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'.
Proof.
  Local Hint Resolve eqlive_stacks_refl: core.
  intros LIVE PATH0 SEXEC STK SSEM2 EQLIVE.
  (* start decomposing path_checker *)
  generalize (LIVE pc0 path0 PATH0).
  unfold path_checker.
  inversion_SOME res; intros IPCHK.
  inversion_SOME i; intros INST ICHK.
  exploit ipath_checker_default_succ; eauto. intros DEFSUCC.
  (* start decomposing SEXEC *)
  generalize SEXEC; clear SEXEC.
  unfold sexec; rewrite PATH0.
  inversion_SOME st0; intros SEXEC_PATH.
  exploit siexec_path_default_succ; eauto.
  simpl. rewrite DEFSUCC.
  clear DEFSUCC. destruct res as [alive pc1]. simpl in *.
  try_simplify_someHyps.
  destruct (siexec_inst i st0) eqn: SIEXEC; try_simplify_someHyps; intros.
  (* Snone *)
  eapply siexec_snone_por_correct; eauto.
  destruct i; try_simplify_someHyps; try congruence;
  inversion SSEM2; subst; clear SSEM2; simpl in *.
 + (* Scall *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
      econstructor; eauto.
      (* wf *)
      generalize ICHK.
      unfold inst_checker; simpl in *.
      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
      destruct (list_mem _ _); try congruence.
      destruct (reg_sum_mem _ _); try congruence.
      intros EXIT.
      exploit exit_checker_eqlive_ext1; eauto.
      intros. destruct H as [p [PATH EQLIVE']].
      econstructor; eauto.
 + (* Stailcall *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
 + (* Sbuiltin *)
    eexists; split.
    * econstructor; eauto.
    * (* wf *)
      generalize ICHK.
      unfold inst_checker; simpl in *.
      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
      destruct (list_mem _ _); try congruence.
      intros EXIT.
      exploit exit_checker_eqlive_builtin_res; eauto.
      intros. destruct H as [p [PATH EQLIVE']].
      econstructor; eauto.
 + (* Sjumptable *)
    eexists; split.
    * econstructor; eauto.
    * (* wf *)
      generalize ICHK.
      unfold inst_checker; simpl in *.
      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
      destruct (Regset.mem _ _); try congruence.
      destruct (exit_list_checker _ _ _) eqn:EQL; try congruence.
      exploit exit_list_checker_eqlive; eauto.
      intros. destruct H as [p [PATH EQLIVE']].
      econstructor; eauto.
 + (* Sreturn *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
Qed.

(* The main theorem on simulation of symbolic states ! *)
Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
  (fn_path f) ! pc0 = Some path0 ->
  sexec f pc0 = Some st -> 
  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 (pre_output_regs path0) st st' ctx) ->
  exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
Proof.
  intros PATH0 SEXEC 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 in *.
  - (* 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')).
    exploit pre_output_regs_correct; eauto.
    clear SEM2; intros (s0 & SEM2 & EQLIVE).
    exploit ssem_final_simu; eauto.
    clear SEM2; intros (s1 & SEM2 & MATCH0).
    exploit ssem_final_equiv; eauto.
    clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s2 & EQ & SEM2).
    exists s2; split.
    + eapply ssem_normal; eauto.
    + eapply eqlive_match_states; 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).
  exploit dupmap_correct; eauto.
  intros (path0 & st' & PATH0 & SYMB' & SIMU).
  rewrite PATH0 in PATH; inversion PATH; subst.
  exploit ssem_sstate_simu; eauto.
  intros (s0 & SEM0 & MATCH). 
  exploit (sexec_exact f'); 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.