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

Require Import Errors Linking BTLtoRTL.

Require Import Linking.


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

Inductive match_stackframes: BTL.stackframe -> RTL.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 (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).

Inductive match_states: BTL.state -> RTL.state -> Prop :=
  | match_states_intro 
      dupmap st f sp pc rs m st' f' pc'
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_function dupmap f f')
      (DUPLIC: dupmap!pc = Some pc')
      : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m)
  | match_states_call
      st st' f f' args m
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_fundef f f')
      : match_states (Callstate st f args m) (RTL.Callstate st' f' args m)
  | match_states_return
      st st' v m
      (STACKS: list_forall2 match_stackframes st st')
      : match_states (Returnstate st v m) (RTL.Returnstate st' v m)
   .

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.

Lemma find_function_preserved ri rs0 fd
  (FIND : find_function ge ri rs0 = Some fd)
  : exists fd', RTL.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.

(* variant of [star RTL.step] but requiring proposition [P] on the [refl] (stutttering) case. *)
Inductive cond_star_step (P: Prop): RTL.state -> trace -> RTL.state -> Prop :=
  | css_refl s: P -> cond_star_step P s E0 s
  | css_plus s1 t s2: plus RTL.step tge s1 t s2 -> cond_star_step P s1 t s2
  .

Lemma css_plus_trans P Q s0 s1 s2 t:
  plus RTL.step tge s0 E0 s1 ->
  cond_star_step P s1 t s2 ->
  cond_star_step Q s0 t s2.
Proof.
  intros PLUS STAR.
  eapply css_plus.
  inv STAR; auto.
  eapply plus_trans; eauto.
Qed.

Lemma css_E0_trans isfst isfst' s0 s1 s2:
  cond_star_step (isfst=false) s0 E0 s1 ->
  cond_star_step (false=isfst') s1 E0 s2 ->
  cond_star_step (isfst=isfst') s0 E0 s2.
Proof.
  intros S1 S2.
  inversion S1; subst; eauto.
  inversion S2; subst; eauto.
  eapply css_plus_trans; eauto.
Qed.

Lemma css_star P s0 s1 t:
  cond_star_step P s0 t s1 ->
  star RTL.step tge s0 t s1.
Proof.
  destruct 1.
  - eapply star_refl; eauto.
  - eapply plus_star; eauto.
Qed.

Local Hint Constructors RTL.step match_states: core.
Local Hint Resolve css_refl plus_one transf_fundef_correct: core.

Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
  (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
  forall pc0 opc isfst
  (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc),
   match ofin with 
   | None => exists pc1,(opc = Some pc1) /\ cond_star_step (isfst = false) (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
   | Some fin =>
      exists isfst' pc1 iinfo, match_iblock dupmap (RTL.fn_code f') isfst' pc1 (BF fin iinfo) None
                 /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
   end.
Proof.
  induction IBIS; simpl; intros.
  - (* exec_final *)
    assert (X: opc = None). { inv MIB; auto. }
    subst.
    repeat eexists; eauto.
  - (* exec_nop *)
    inv MIB; eexists; split; econstructor; eauto.
  - (* exec_op *)
    inv MIB. exists pc'; split; auto; constructor.
    apply plus_one. eapply exec_Iop; eauto.
    erewrite <- eval_operation_preserved; eauto.
    intros; rewrite symbols_preserved; trivial.
  - (* exec_load *)
    inv MIB. exists pc'; split; auto; constructor.
    apply plus_one. inversion LOAD; subst.
    + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
      rewrite <- EVAL; erewrite <- eval_addressing_preserved; eauto;
      intros; rewrite symbols_preserved; trivial).
    + destruct (eval_addressing) eqn:EVAL in LOAD0.
      * specialize (LOAD0 v).
        eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
        rewrite eval_addressing_preserved with (ge1:=ge).
        intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD0; auto.
        intros; rewrite symbols_preserved; trivial.
      * eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
        rewrite eval_addressing_preserved with (ge1:=ge).
        intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
        intros; rewrite symbols_preserved; trivial.
  - (* exec_store *)
    inv MIB. exists pc'; split; auto; constructor.
    apply plus_one. eapply exec_Istore; eauto.
    all: erewrite <- eval_addressing_preserved; eauto;
         intros; rewrite symbols_preserved; trivial.
  - (* exec_seq_stop *)
    inv MIB; eauto.
  - (* exec_seq_continue *)
    inv MIB.
    exploit IHIBIS1; eauto.
    intros (pc1 & EQpc1 & STEP1); inv EQpc1.
    exploit IHIBIS2; eauto.
    destruct ofin; simpl.
    + intros (ifst2 & pc2 & iinfo & M2 & STEP2).
      repeat eexists; eauto.
      eapply css_E0_trans; eauto. 
    + intros (pc2 & EQpc2 & STEP2); inv EQpc2.
      eexists; split; auto.
      eapply css_E0_trans; eauto.
  - (* exec_cond *)
    inv MIB.
    rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *)
    destruct b; exploit IHIBIS; eauto.
    + (* taking ifso *)
      destruct ofin; simpl.
      * (* ofin is Some final *)
        intros (isfst' & pc1 & iinfo' & MI & STAR).
        repeat eexists; eauto.
        eapply css_plus_trans; eauto.
      * (* ofin is None *)
        intros (pc1 & OPC & PLUS). inv OPC.
        inv JOIN; eexists; split; eauto.
        all:
          eapply css_plus_trans; eauto.
    + (* taking ifnot *)
      destruct ofin; simpl.
      * (* ofin is Some final *)
        intros (isfst' & pc1 & iinfo' & MI & STAR).
        repeat eexists; eauto.
        eapply css_plus_trans; eauto.
      * (* ofin is None *)
        intros (pc1 & OPC & PLUS). subst.
        inv JOIN; eexists; split; eauto.
        all:
          eapply css_plus_trans; eauto.
Qed.

Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s
  (STACKS : list_forall2 match_stackframes stack stack')
  (TRANSF : match_function dupmap f f')
  (FS : final_step tid ge stack f sp rs1 m1 fin t s)
  (i : instruction)
  (ATpc1 : (RTL.fn_code f') ! pc1 = Some i)
  (MF : match_final_inst dupmap fin i)
  : exists s', RTL.step tge (RTL.State stack' f' sp pc1 rs1 m1) t s' /\ match_states s s'.
Proof.
  inv MF; inv FS.
  - (* return *)
    eexists; split.
    eapply exec_Ireturn; eauto.
    erewrite <- preserv_fnstacksize; eauto.
    econstructor; eauto.
  - (* call *)
    rename H7 into FIND.
    exploit find_function_preserved; eauto.
    intros (fd' & FIND' & TRANSFU).
    eexists; split. eapply exec_Icall; eauto.
    apply function_sig_translated. assumption.
    repeat (econstructor; eauto).
  - (* tailcall *)
    rename H2 into FIND.
    exploit find_function_preserved; eauto.
    intros (fd' & FIND' & TRANSFU).
    eexists; split. eapply exec_Itailcall; eauto.
    apply function_sig_translated. assumption.
    erewrite <- preserv_fnstacksize; eauto.
    repeat (econstructor; eauto).
  - (* builtin *)
    pose symbols_preserved as SYMPRES.
    eexists. split.
    eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto.
    eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
    econstructor; eauto.
  - (* jumptable *)
    pose symbols_preserved as SYMPRES.
    exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM).
    eexists. split.
    eapply exec_Ijumptable; eauto.
    econstructor; eauto.
Qed.

Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
  (STACKS: list_forall2 match_stackframes stack stack')
  (TRANSF: match_function dupmap f f')
  (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
  (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
  (FS : final_step tid ge stack f sp rs1 m1 fin t s)
  : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
Proof.
  intros; exploit iblock_istep_simulation; eauto.
  simpl. intros (isfst' & pc1 & iinfo & MI & STAR). clear IBIS MIB.
  inv MI.
  - (* final inst except goto *)
    exploit final_simu_except_goto; eauto.
    intros (s' & STEP & MS). eexists; split.
    + eapply plus_right.
      eapply css_star; eauto.
      eapply STEP. econstructor.
    + eapply MS.
  - (* goto *)
    inv FS.
    inv STAR; try congruence.
    eexists; split. eauto.
    econstructor; eauto.
Qed.

Theorem plus_simulation s1 t s1':
  step tid ge s1 t s1' ->
  forall s2 (MS: match_states s1 s2),
  exists s2',
     plus RTL.step tge s2 t s2'
  /\ match_states s1' s2'.
Proof.
  destruct 1; intros; inv MS.
  - eapply dupmap_correct in DUPLIC; eauto.
    destruct DUPLIC as (ib' & FNC & MIB).
    try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS).
    intros; exploit iblock_step_simulation; eauto.
  (* exec_function_internal *)
  - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
    + eapply plus_one. apply RTL.exec_function_internal.
      erewrite <- preserv_fnstacksize; eauto.
    + erewrite <- preserv_fnparams; eauto.
      eapply match_states_intro; eauto.
      apply dupmap_entrypoint. assumption.
  (* exec_function_external *)
  - inversion TRANSF as [|]; subst. eexists. split.
    + eapply plus_one. econstructor.
      eapply external_call_symbols_preserved; eauto. apply senv_preserved.
    + constructor. assumption.
  (* exec_return *)
  - inversion STACKS as [|a1 al b1 bl H1 HL]; subst.
    destruct b1 as [res' f' sp' pc' rs'].
    eexists. split.
    + eapply plus_one. constructor.
    + inv H1. econstructor; eauto.
Qed.

Theorem transf_program_correct_cfg:
  forward_simulation (BTLmatchRTL.cfgsem 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.

Theorem transf_program_correct:
  forward_simulation (BTL.fsem prog) (RTL.semantics tprog).
Proof.
  eapply compose_forward_simulations.
  - eapply fsem2cfgsem.
  - eapply transf_program_correct_cfg.
Qed.

End RTL_SIMULATES_BTL.