Module DebugvarproofC

Require Import Axioms CoqlibC Maps Iteration .
Require Import Integers Floats AST Linking.
Require Import ValuesC Memory Events Globalenvs Smallstep.
Require Import Machregs LocationsC Conventions Op LinearC.
Require Import Debugvar.
newly added *
Require Export Debugvarproof.
Require Import Simulation.
Require Import Skeleton Mod ModSem SimMod SimModSem SimSymb SimMem AsmregsC MatchSimModSem.
Require SimMemId.
Require SoundTop.
Require Import LiftDummy.

Set Implicit Arguments.



Definition strong_wf_tgt (st_tgt0: Linear.state): Prop :=
  exists sg_init ls_init, last_option st_tgt0.(LinearC.get_stack) = Some (Linear.dummy_stack sg_init ls_init).

Section SIMMODSEM.

Variable skenv_link: SkEnv.t.
Variable sm_link: SimMem.t.
Variables prog tprog: program.
Let md_src: Mod.t := (LinearC.module prog).
Let md_tgt: Mod.t := (LinearC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (WF: SkEnv.wf skenv_link).
Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) tt sm_link.

Inductive match_states (sm_init: SimMem.t)
          (idx: nat) (st_src0: Linear.state) (st_tgt0: Linear.state) (sm0: SimMem.t): Prop :=
| match_states_intro
    (MATCHST: Debugvarproof.match_states st_src0 st_tgt0)
    (MCOMPATSRC: st_src0.(get_mem) = sm0.(SimMem.src))
    (MCOMPATTGT: st_tgt0.(get_mem) = sm0.(SimMem.tgt))
    (DUMMYTGT: strong_wf_tgt st_tgt0).

Theorem make_match_genvs :
  SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk))
                      (SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
  Genv.match_genvs (match_globdef (fun _ f tf => transf_fundef f = Errors.OK tf) eq prog) ge tge.
Proof.
subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Theorem sim_modsem: ModSemPair.sim msp.
Proof.
  eapply match_states_sim with (match_states := match_states) (match_states_at := top4) (sound_state := SoundTop.sound_state);
    eauto; ii; ss.
  - instantiate (1:= Nat.lt). apply lt_wf.
  - eapply SoundTop.sound_state_local_preservation.
  - (* init bsim *)
    inv INITTGT. destruct sm_arg; ss. clarify.
    inv SIMARGS; ss. clarify. inv TYP.
    exploit (fill_arguments_progress ls_init (typify_list vs_tgt (sig_args (fn_sig fd)))
                                     (Conventions1.loc_arguments (fn_sig fd))); eauto.
    { apply (f_equal (@length _)) in TYP0. rewrite map_length in *. etrans; try apply TYP0; eauto. }
    intro P; des.
    hexploit (@fill_arguments_spec); et. intro Q; des.
    exploit make_match_genvs; eauto. { apply SIMSKENV. } intro SIMGE. des.
    eexists. eexists (SimMemId.mk _ _). esplits; ss; cycle 1.
    + econs; eauto; ss.
      * rpapply match_states_call.
        { econs; eauto.
          - instantiate (1:= (dummy_stack (fn_sig fd) ls_init)). unfold dummy_stack, dummy_function.
            rpapply match_stackframe_intro; eauto; swap 1 2.
            + econs; eauto.
            + econs; eauto. ss. econs; eauto. econs; eauto.
            + ss. f_equal; ss.
              * instantiate (1:= None). instantiate (1:= None). ss.
              * instantiate (1:= None). instantiate (1:= None). ss.
          - econs; et.
        }
      * rr. esplits; ss; eauto.
    + inv SAFESRC. folder. inv TYP.
      exploit (Genv.find_funct_transf_partial_genv SIMGE); eauto. intro FINDFSRC; des; clarify.
      unfold transf_fundef; ss. unfold Errors.bind in *. des_ifs.
      econs; swap 1 3.
      { folder; ss. eauto. }
      all: ss.
      unfold transf_function in *. des_ifs.
  - (* init progress *)
    des. inv SAFESRC. inv SIMARGS; ss.
    exploit make_match_genvs; eauto. { apply SIMSKENV. } intro SIMGE.
    exploit (Genv.find_funct_match_genv SIMGE); eauto. i; des. ss. clarify. folder.
    inv TYP. unfold Errors.bind in *. des_ifs.
    destruct sm_arg; ss. clarify.
    exploit (Genv.find_funct_match_genv SIMGE); eauto. i; des. ss. clarify.
    exploit (fill_arguments_progress (Locmap.init Vundef) (typify_list vs_tgt (sig_args (fn_sig fd)))
                                     (Conventions1.loc_arguments (fn_sig fd))); eauto.
    { apply (f_equal (@length _)) in TYP0. rewrite map_length in *. etrans; try apply TYP0; eauto. }
    intro P; des.
    hexploit (fill_arguments_spec); eauto. intro Q; des.
    assert(SGEQ: fn_sig fd = fn_sig f).
    { unfold transf_function in *; des_ifs. }
    esplits; eauto. econs; swap 1 3.
    { ss. folder. eauto. }
    all: ss; eauto with congruence.
    + econs; ss; eauto with congruence.
  - (* call wf *)
    inv MATCH; ss. destruct sm0; ss. clarify.
    inv CALLSRC. inv MATCHST; ss.
  - (* call fsim *)
    inv MATCH; ss. destruct sm0; ss. clarify.
    inv CALLSRC. inv MATCHST; ss.
    folder. esplits; eauto.
    + econs; eauto.
      * folder. des.
        r in TRANSL. r in TRANSL.
        exploit (SimSymbId.sim_skenv_revive TRANSL); eauto.
        { apply SIMSKENV. }
        intro GE.
        apply (fsim_external_funct_id GE); ss.
    + econs; ss; eauto.
      * instantiate (1:= SimMemId.mk _ _). ss.
      * ss.
    + ss.
  - (* after fsim *)
    inv AFTERSRC. inv SIMRET; ss. exists sm_ret. destruct sm_ret; ss. clarify.
    inv MATCH; ss. inv MATCHST; ss. esplits; eauto.
    + econs; eauto.
    + econs; ss; eauto. econs; eauto.
      { inv H5; ss. - econs; eauto. - des_ifs. econs; eauto. inv H. econs; eauto. }
      { clear - DUMMYTGT. unfold strong_wf_tgt in *. des. destruct ts; ss. unfold dummy_stack, dummy_function in *. des_ifs; ss; clarify; esplits; et. }
  - (* final fsim *)
    inv MATCH. inv FINALSRC; inv MATCHST; ss.
    inv H3; ss. inv H4; ss. rr in DUMMYTGT. des. ss. clarify. destruct sm0; ss. clarify.
    eexists (SimMemId.mk _ _). esplits; ss; eauto.
    econs; ss; eauto. inv H1; ss. inv H2; ss.
  - left; i. esplits; eauto.
    { apply modsem_receptive; et. }
    inv MATCH.
    ii. rr in STEPSRC. des. hexploit (@transf_step_correct prog skenv_link); eauto.
    { inv SIMSKENV. ss. }
    { apply make_match_genvs; eauto. apply SIMSKENV. }
    i; des.
    exploit (lift_plus Linear.step (fun st => get_stack st <> []) strong_wf_tgt); ss; et.
    { intros st X Y. rr in X. des. rewrite Y in *. ss. }
    { i. folder. unfold strong_wf_tgt in *. des. inv HSTEP; ss; eauto.
      - des_ifs; ss; eauto.
      - des_ifs; ss; eauto. right. ii. inv HSTEP0; ss. }
    { ii. unfold strong_wf_tgt in *; des. inv HSTEP; try inv STACKS; ss; clarify; et; des_ifs; et. }
    { intro T. inv H0; ss; clarify; try inv STACKS; ss; try inv H1; ss. }
    intro TT; des.
    esplits; eauto.
    * left. eapply ModSemProps.spread_dplus; eauto.
      { eapply modsem_determinate; eauto. }
    * instantiate (1:= SimMemId.mk _ _). econs; ss.
Unshelve.
  all: ss; try (by econs).
Qed.

End SIMMODSEM.




Section SIMMOD.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Definition mp: ModPair.t := ModPair.mk (LinearC.module prog) (LinearC.module tprog) tt.

Theorem sim_mod: ModPair.sim mp.
Proof.
  econs; ss.
  - r. eapply Sk.match_program_eq; eauto.
    ii. destruct f1; ss.
    + clarify. right. unfold Errors.bind, transf_function in *. des_ifs. esplits; eauto.
    + clarify. left. esplits; eauto.
  - ii. inv SIMSKENVLINK. eapply sim_modsem; eauto.
Qed.

End SIMMOD.