Module CstrategyC

Require Import Axioms.
Require Import Classical.
Require Import CoqlibC.
Require Import Errors.
Require Import MapsC.
Require Import IntegersC.
Require Import Floats.
Require Import ValuesC.
Require Import ASTC.
Require Import MemoryC.
Require Import EventsC.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
Require Import Csyntax.
Require Import CsemC.
Require Import sflib.
newly added *
Require Export Simulation Cstrategy CopC Ctypes Ctyping Csyntax Cexec.
Require Import Skeleton Mod ModSem.
Require Import CtypesC.
Require Import Conventions.
Require Import CtypingC.

Set Implicit Arguments.

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

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

Section MODSEM.

  Variable skenv_link: SkEnv.t.
  Variable p: program.
  Let skenv: SkEnv.t := skenv_link.(SkEnv.project) p.(CSk.of_program signature_of_function).
  Let ce_ge: composite_env := prog_comp_env p.
  Let ge_ge: Genv.t fundef type := SkEnv.revive skenv p.
  Let ge: genv := Build_genv ge_ge ce_ge.

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

  Inductive initial_frame (args: Args.t): state -> Prop :=
  | initial_frame_intro
      fd tyf
      (CSTYLE: Args.is_cstyle args)
      (FINDF: Genv.find_funct ge args.(Args.fptr) = Some (Internal fd))
      (TYPE: type_of_fundef (Internal fd) = tyf)
      (TYP: typecheck args.(Args.vs) (type_of_params (fn_params fd))):
      initial_frame args (Callstate args.(Args.fptr) tyf args.(Args.vs) 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 vs_arg m_arg k retv tv targs tres cconv
      (CSTYLE: Retv.is_cstyle retv)
      (TYP: typify_c retv.(Retv.v) tres tv):
      after_external (Callstate fptr_arg (Tfunction targs tres cconv) 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_strongly_receptive: forall st, strongly_receptive_at modsem st.
Proof.
    i. econs; ss; i.
    - inversion H; subst. inv H1.
      + (* valof volatile *)
        exploit deref_loc_receptive; eauto. intros [A [v' B]].
        econstructor; econstructor. left; eapply step_rvalof_volatile; eauto.
      + (* assign *)
        exploit assign_loc_receptive; eauto. intro EQ; rewrite EQ in H.
        econstructor; econstructor; eauto.
      + (* assignop *)
        destruct t0 as [ | ev0 t0]; simpl in H10.
        subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
        econstructor; econstructor; eauto.
        inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
        destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
        destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
        destruct (classic (exists t2', exists m'', assign_loc skenv_link ge (typeof l) m b ofs v4' t2' m'')).
        destruct H1 as [t2' [m'' P]].
        econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
        econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto.
        econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0; auto.
        econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
        rewrite Heqo; auto.
      + (* assignop stuck *)
        exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
        destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
        destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
        destruct (classic (exists t2', exists m'', assign_loc skenv_link ge (typeof l) m b ofs v4' t2' m'')).
        destruct H1 as [t2' [m'' P]].
        econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
        econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto.
        econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0; auto.
        econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
        rewrite Heqo; auto.
      + (* postincr *)
        destruct t0 as [ | ev0 t0]; simpl in H9.
        subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
        econstructor; econstructor; eauto.
        inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
        destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
        destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
        destruct (classic (exists t2', exists m'', assign_loc skenv_link ge (typeof l) m b ofs v3' t2' m'')).
        destruct H1 as [t2' [m'' P]].
        econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
        econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto.
        econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0; auto.
        econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
        rewrite Heqo; auto.
      + (* postincr stuck *)
        exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
        destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
        destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
        destruct (classic (exists t2', exists m'', assign_loc skenv_link ge (typeof l) m b ofs v3' t2' m'')).
        destruct H1 as [t2' [m'' P]].
        econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
        econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto.
        econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
        rewrite Heqo; rewrite Heqo0; auto.
        econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
        rewrite Heqo; auto.
      + (* builtin *)
        exploit external_call_trace_length; eauto. destruct t1; simpl; intros.
        exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
        econstructor; econstructor. left; eapply step_builtin; eauto.
        omegaContradiction.
      + (* external calls *)
        inv H1.
        exploit external_call_trace_length; eauto. destruct t1; simpl; intros.
        exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
        exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto.
        omegaContradiction.
    - red; intros. inv H; inv H0; ss.
      + (* valof volatile *)
        exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
      + (* assign *)
        exploit assign_loc_trace; eauto. destruct t; auto. destruct t; simpl; tauto.
      + (* assignop *)
        exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto.
        destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto.
        destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto.
        tauto.
      + (* assignop stuck *)
        exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
      + (* postincr *)
        exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto.
        destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto.
        destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto.
        tauto.
      + (* postincr stuck *)
        exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
      + (* builtins *)
        exploit external_call_trace_length; eauto.
        destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction.
      + (* external calls *)
        exploit external_call_trace_length; eauto.
        destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction.
  Qed.

End MODSEM.



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