Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.

Require Import Errors Linking RTLtoBTL.

Require Import Linking.

(* TODO: remplacer "right_assoc" par "expand" ci-dessous *)

Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
  dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
  dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
  code_right_assoc: forall pc ib, (fn_code tf)!pc=Some ib -> is_right_assoc ib.(entry);
  preserv_fnsig: fn_sig tf = RTL.fn_sig f;
  preserv_fnparams: fn_params tf = RTL.fn_params f;
  preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
}.

Inductive match_fundef: RTL.fundef -> fundef -> Prop :=
  | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf)
  | match_External ef: match_fundef (External ef) (External ef).

Inductive match_stackframes: RTL.stackframe -> stackframe -> Prop :=
  | match_stackframe_intro 
      dupmap res f sp pc rs f' pc'
      (TRANSF: match_function dupmap f f')
      (DUPLIC: dupmap!pc' = Some pc)
      : match_stackframes (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).

Lemma verify_function_correct dupmap f f' tt:
  verify_function dupmap f' f = OK tt ->
  fn_sig f' = RTL.fn_sig f ->
  fn_params f' = RTL.fn_params f ->
  fn_stacksize f' = RTL.fn_stacksize f ->
  (forall pc ib, (fn_code f')!pc=Some ib -> is_right_assoc ib.(entry)) ->
  match_function dupmap f f'.
Proof.
  unfold verify_function; intro VERIF. monadInv VERIF.
  constructor; eauto.
  - eapply verify_cfg_correct; eauto.
  - eapply verify_is_copy_correct; eauto.
Qed.

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.
  eapply right_assoc_code_correct; 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: RTL.program) (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 BTL_SIMULATES_RTL.

Variable prog: RTL.program.
Variable tprog: program.

Hypothesis TRANSL: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Local Open Scope nat_scope.

(** * Match relation from a RTL state to a BTL state

The "option iblock" parameter represents the current BTL execution state.
Thus, each RTL single step is symbolized by a new BTL "option iblock"
starting at the equivalent PC.

The simulation diagram for match_states_intro is as follows:

<<

        RTL state       match_states_intro        BTL state
      [pcR0,rs0,m0 ---------------------------- [pcB0,rs0,m0]
           |                                         |
           |                                         |
   RTL_RUN | *E0                                     | BTL_RUN
           |                                         |
           |                   MIB                   |
      [pcR1,rs,m] -------------------------------- [ib]

>>
*)

Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
  | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
      ib dupmap st f sp rs m st' f' pcB0 pcR0 pcR1 rs0 m0 isfst ib0
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_function dupmap f f')
      (ATpc0: (fn_code f')!pcB0 = Some ib0)
      (DUPLIC: dupmap!pcB0 = Some pcR0)
      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
      (RIGHTA: is_right_assoc ib)
      (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs m))
      (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
      : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
  | match_states_call
      st st' f f' args m
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_fundef f f')
      : match_states None (RTL.Callstate st f args m) (Callstate st' f' args m)
  | match_states_return
      st st' v m
      (STACKS: list_forall2 match_stackframes st st')
      : match_states None (RTL.Returnstate st v m) (Returnstate st' v m)
   .

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: RTL.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 -> funsig tf = RTL.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:
  RTL.initial_state prog s1 ->
  exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
  eexists. 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 ib s1 s2 r:
  match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r.
Proof.
  intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Lemma find_function_preserved ri rs0 fd
  (FIND : RTL.find_function ge ri rs0 = Some fd)
  : exists fd', find_function tge ri rs0 = Some fd'
                /\ transf_fundef fd = OK fd'.
Proof.
  pose symbols_preserved as SYMPRES.
  destruct ri.
  + simpl in FIND; apply functions_translated in FIND.
    destruct FIND as (tf & cunit & TFUN & GFIND & LO).
    eexists; split. eauto. assumption.
  + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
    apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
    eexists; split. simpl. rewrite symbols_preserved.
    rewrite GFS. eassumption. assumption.
Qed.

(* Inspired from Duplicateproof.v *)
Lemma list_nth_z_dupmap:
  forall dupmap ln ln' (pc pc': node) val,
  list_nth_z ln val = Some pc ->
  list_forall2 (fun n n' => dupmap!n = Some n') ln ln' ->
  exists (pc': node),
     list_nth_z ln' val = Some pc'
  /\ dupmap!pc = Some pc'.
Proof.
  induction ln; intros until val; intros LNZ LFA.
  - inv LNZ.
  - inv LNZ. destruct (zeq val 0) eqn:ZEQ.
    + inv H0. destruct ln'; inv LFA.
      simpl. exists n. split; auto.
    + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
Qed.

(* TODO: definir une measure sur les iblocks.
Cette mesure décroit strictement quand on exécute un "petit-pas" de iblock.
Par exemple, le nombre de noeuds (ou d'instructions "RTL") dans le iblock devrait convenir.
La hauteur de l'arbre aussi.
*)
(** Representing an intermediate BTL state

We keep a measure of code that remains to be executed with the omeasure
type defined below. Intuitively, each RTL step corresponds to either
   - a single BTL step if we are on the last instruction of the block
   - no BTL step (as we use a "big step" semantics) but a change in
     the measure which represents the new intermediate state of the BTL code
 *)
Fixpoint measure ib: nat :=
  match ib with
  | Bseq ib1 ib2
  | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2
  | ib => 1
  end.

Definition omeasure (oib: option iblock): nat :=
 match oib with
 | None => 0
 | Some ib => measure ib
 end.

Lemma opt_simu_intro
  sp f f' st st' dupmap isfst pcR0 pcR1 pcB0 ib ib0 rs m rs0 m0 t s1'
  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1')
  (STACKS : list_forall2 match_stackframes st st')
  (TRANSF : match_function dupmap f f')
  (ATpc0 : (fn_code f') ! pcB0 = Some ib0)
  (DUPLIC : dupmap ! pcB0 = Some pcR0)
  (MIB : match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
  (RIGHTA : is_right_assoc ib)
  (RTL_RUN : star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0
              (RTL.State st f sp pcR1 rs m))
  (BTL_RUN : iblock_istep_run tge sp (entry ib0) rs0 m0 =
            iblock_istep_run tge sp ib rs m)
  : exists (oib' : option iblock),
     (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
  \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
Proof.
  inv MIB.
  - (* mib_BF *)
    admit.
  - (* mib_exit *)
    (*
      simpl in *.
      eapply iblock_istep_run_equiv in BTL_RUN.
      inv BTL_RUN.
    eexists; left. eexists; split.
    + eapply exec_iblock; eauto.
      econstructor; repeat eexists.
      inv STEP.
       eapply exec_Bgoto.*) admit.
  - (* mib_seq *)
    inv H.
    + (* Bnop *)
      inversion STEP; subst; try_simplify_someHyps. (* TODO maybe move that for each subcase *)
      exists (Some b2); right; repeat (split; auto).
      econstructor; eauto. inv RIGHTA; auto; discriminate.
      eapply star_right; eauto.
    + (* Bop *)
      inversion STEP; subst; try_simplify_someHyps.
      exists (Some b2); right; repeat (split; auto).
      econstructor; eauto. inv RIGHTA; auto; discriminate.
      eapply star_right; eauto.
      erewrite eval_operation_preserved in H10.
      erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto.
      intros; rewrite <- symbols_preserved; trivial.
    + (* Bload *)
      inversion STEP; subst; try_simplify_someHyps.
      exists (Some (b2)); right; repeat (split; auto).
      econstructor; eauto. inv RIGHTA; auto; discriminate.
      eapply star_right; eauto.
      erewrite eval_addressing_preserved in H10.
      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
      intros; rewrite <- symbols_preserved; trivial.
    + (* Bstore *)
      inversion STEP; subst; try_simplify_someHyps.
      exists (Some b2); right; repeat (split; auto).
      econstructor; eauto. inv RIGHTA; auto; discriminate.
      eapply star_right; eauto.
      erewrite eval_addressing_preserved in H10.
      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
      intros; rewrite <- symbols_preserved; trivial.
    + (* Absurd case *)
      inv RIGHTA. inv H4. inv H.
    + (* Bcond *)
      admit.
  - (* mib_cond *)
    admit.
Admitted.

Theorem opt_simu s1 t s1' oib s2:
 RTL.step ge s1 t s1' ->
 match_states oib s1 s2 ->
 exists (oib' : option iblock),
     (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
  \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
 .
Proof.
  inversion 2; subst; clear H0.
  - (* State *)
    exploit opt_simu_intro; eauto.
  - (* Callstate *)
    inv H.
    + (* Internal function *)
      inv TRANSF.
      rename H0 into TRANSF.
      eapply dupmap_entrypoint in TRANSF as ENTRY.
      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
      apply DMC in ENTRY as DMC'.
      destruct DMC' as [ib [CENTRY MI]]; clear DMC.
      eexists; left; eexists; split.
      * eapply exec_function_internal.
        erewrite preserv_fnstacksize; eauto.
      * econstructor; eauto.
        eapply code_right_assoc; eauto.
        all: erewrite preserv_fnparams; eauto.
        constructor.
    + (* External function *)
      inv TRANSF.
      eexists; left; eexists; split.
      * eapply exec_function_external.
        eapply external_call_symbols_preserved.
        eapply senv_preserved. eauto.
      * econstructor; eauto.
  - (* Returnstate *)
    inv H. inv STACKS. inv H1.
    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
    remember DUPLIC as ODUPLIC; clear HeqODUPLIC.
    apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
    eexists; left; eexists; split.
    + eapply exec_return.
    + econstructor; eauto.
      eapply code_right_assoc; eauto.
      constructor.
Qed.

Local Hint Resolve plus_one star_refl: core.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (BTL.semantics tprog).
Proof.
  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states).
  constructor 1; simpl.
  - apply well_founded_ltof.
  - eapply transf_initial_states.
  - eapply transf_final_states.
  - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP.
    destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]).
    + repeat eexists; eauto.
    + subst. repeat eexists; eauto.
  - eapply senv_preserved.
Qed.

End BTL_SIMULATES_RTL.