Module CminorC

Require Import CoqlibC.
Require Import Maps.
Require Import ASTC.
Require Import IntegersC.
Require Import Floats.
Require Import EventsC.
Require Import ValuesC.
Require Import Memory.
Require Import Globalenvs.
Require Import SmallstepC.
Require Import Switch.
newly added *
Require Export Simulation Cminor.
Require Import Skeleton Mod ModSem.

Set Implicit Arguments.

Local Obligation Tactic := ii; ss; des; inv_all_once; ss; clarify.

Definition get_mem (st: state): mem :=
  match st with
  | State _ _ _ _ _ m0 => m0
  | Callstate _ _ _ _ m0 => m0
  | Returnstate _ _ m0 => m0
  end.

Section MODSEM.

  Variable skenv_link: SkEnv.t.
  Variable p: program.
  Let skenv: SkEnv.t := skenv_link.(SkEnv.project) p.(Sk.of_program fn_sig).
  Let ge: genv := skenv.(SkEnv.revive) p.

  Inductive at_external: state -> Args.t -> Prop :=
  | at_external_intro
      fptr_arg sg_arg vs_arg k0 m0
      (EXTERNAL: ge.(Genv.find_funct) fptr_arg = None)
      (SIG: exists skd, skenv_link.(Genv.find_funct) fptr_arg = Some skd /\ Sk.get_csig skd = Some sg_arg):
      at_external (Callstate fptr_arg sg_arg vs_arg k0 m0) (Args.mk fptr_arg vs_arg m0).

  Inductive initial_frame (args: Args.t): state -> Prop :=
  | initial_frame_intro
      fd tvs
      (CSTYLE: Args.is_cstyle args /\ fd.(fn_sig).(sig_cstyle) = true)
      (FINDF: Genv.find_funct ge args.(Args.fptr) = Some (Internal fd))
      (TYP: typecheck args.(Args.vs) fd.(fn_sig) tvs)
      (LEN: args.(Args.vs).(length) = fd.(fn_sig).(sig_args).(length)):
      initial_frame args (Callstate args.(Args.fptr) fd.(fn_sig) tvs Kstop args.(Args.m)).

  Inductive final_frame: state -> Retv.t -> Prop :=
  | final_frame_intro
      v_ret m_ret:
      final_frame (Returnstate v_ret Kstop m_ret) (Retv.mk v_ret m_ret).

  Inductive after_external: state -> Retv.t -> state -> Prop :=
  | after_external_intro
      fptr_arg sg_arg vs_arg k m_arg
      retv tv
      (CSTYLE: Retv.is_cstyle retv)
      (TYP: typify retv.(Retv.v) sg_arg.(proj_sig_res) = tv):
      after_external (Callstate fptr_arg sg_arg vs_arg k m_arg)
                     retv
                     (Returnstate tv k retv.(Retv.m)).

  Program Definition modsem: ModSem.t :=
    {| ModSem.step := step;
       ModSem.at_external := at_external;
       ModSem.initial_frame := initial_frame;
       ModSem.final_frame := final_frame;
       ModSem.after_external := after_external;
       ModSem.globalenv := ge;
       ModSem.skenv := skenv;
       ModSem.skenv_link := skenv_link;
    |}.

  Lemma modsem_receptive: forall st, receptive_at modsem st.
Proof.
    econs; eauto.
    - ii; ss. inv H; try (exploit external_call_receptive; eauto; check_safe; intro T; des); inv_match_traces; try (by esplits; eauto; econs; eauto).
    - ii. inv H; try (exploit external_call_trace_length; eauto; check_safe; intro T; des); ss; try xomega.
  Qed.

  Let eval_expr_determ:
    forall sp e m a v, eval_expr ge sp e m a v -> forall v', eval_expr ge sp e m a v' -> v' = v.
Proof.
    induction 1; intros v' EV; inv EV; try congruence.
    - apply IHeval_expr in H3. unfold eval_unop in *; des_ifs.
    - apply IHeval_expr1 in H5. apply IHeval_expr2 in H7. subst. unfold eval_binop in *; des_ifs.
    - apply IHeval_expr in H3. subst. unfold Mem.loadv in *; des_ifs.
  Qed.

  Let eval_exprlist_determ:
    forall sp e m al vl, eval_exprlist ge sp e m al vl -> forall vl', eval_exprlist ge sp e m al vl' -> vl' = vl.
Proof.
    induction 1; intros v' EV; inv EV; f_equal; eauto using eval_expr_determ.
  Qed.

  Lemma modsem_determinate: forall st, determinate_at modsem st.
Proof.
    econs; eauto.
    - ii; ss. inv H; inv H0; clarify_meq;
                try (determ_tac eval_expr_determ; check_safe); try (determ_tac eval_exprlist_determ; check_safe);
                  try (determ_tac eval_builtin_args_determ; check_safe); try (determ_tac external_call_determ; check_safe);
                    esplits; eauto; try (econs; eauto); ii; eq_closure_tac; clarify_meq.
      + clear H1. determ_tac eval_expr_determ.
      + inv H2; inv H13; ss.
      + inv H2; inv H14; ss.
    - ii. inv H; try (exploit external_call_trace_length; eauto; check_safe; intro T; des); ss; try xomega.
  Qed.

End MODSEM.

Program Definition module (p: program): Mod.t :=
  {| Mod.data := p; Mod.get_sk := Sk.of_program fn_sig; Mod.get_modsem := modsem; |}.