Require compcert.cfrontend.Cminorgenproof.
Require CminorX.
Require CsharpminorX.
Require SmallstepX.
Require EventsX.
Import Coqlib.
Import Errors.
Import Values.
Import Globalenvs.
Import EventsX.
Import SmallstepX.
Import Cminorgen.
Export Cminorgenproof.
Section WITHCONFIG.
Context `{
external_calls_prf:
ExternalCalls}.
Variable prog:
Csharpminor.program.
Variable tprog:
Cminor.program.
Hypothesis TRANSL:
transl_program prog =
OK tprog.
Let ge :
Csharpminor.genv :=
Genv.globalenv prog.
Let tge:
Cminor.genv :=
Genv.globalenv tprog.
Variable fn_stack_requirements:
AST.ident ->
Z.
Let MATCH_PROG:
match_prog prog tprog.
Proof.
apply transf_program_match; auto. Qed.
Variable init_m:
mem.
Hypothesis init_m_inject_neutral:
Mem.inject_neutral (
Mem.nextblock init_m)
init_m.
Hypothesis genv_next_init_m:
Ple (
Genv.genv_next ge) (
Mem.nextblock init_m).
Variable args:
list val.
Hypothesis args_inj:
Val.inject_list (
Mem.flat_inj (
Mem.nextblock init_m))
args args.
Lemma transl_initial_states:
forall i sg,
forall S,
CsharpminorX.initial_state fn_stack_requirements prog i init_m sg args S ->
exists R,
CminorX.initial_state fn_stack_requirements tprog i init_m sg args R /\
match_states prog init_m S R.
Proof.
intros.
inv H.
exploit function_ptr_translated; eauto.
destruct 1 as [? [? ?]].
esplit.
split.
econstructor; eauto.
erewrite symbols_preserved; eauto.
symmetry. eapply sig_preserved; eauto.
econstructor; eauto.
rewrite_stack_blocks. simpl. apply Mem.push_new_stage_inject.
eapply Mem.neutral_inject; eauto.
rewrite_stack_blocks. simpl. unfold flat_frameinj. simpl.
apply stack_equiv_refl; auto.
econstructor.
econstructor.
apply Ple_refl.
intros. unfold Mem.flat_inj. destruct (plt b0 (Mem.nextblock init_m)); try contradiction. reflexivity.
unfold Mem.flat_inj. intros. destruct (plt b1 (Mem.nextblock init_m)); congruence.
intros. exploit Genv.genv_symb_range; eauto. unfold ge in *; xomega.
intros. apply Genv.find_funct_ptr_iff in H1. exploit Genv.genv_defs_range; eauto. unfold ge in *; xomega.
intros. apply Genv.find_var_info_iff in H1. exploit Genv.genv_defs_range; eauto. unfold ge in *; xomega.
rewnb; apply Ple_refl.
rewnb; apply Ple_refl.
econstructor.
constructor.
Grab Existential Variables. constructor.
Qed.
Lemma transl_final_states:
forall sg,
forall S R r,
match_states prog init_m S R ->
CsharpminorX.final_state sg S r ->
final_state_with_inject (
CminorX.final_state sg)
init_m R r.
Proof.
inversion 2; subst. inv H. inv MK. inv MCS.
edestruct Mem.unrecord_stack_block_inject_parallel_flat as (m2' & USB' & EXT'); eauto.
econstructor.
econstructor. eauto.
eapply match_globalenvs_inject_incr; eassumption.
eapply match_globalenvs_inject_separated; eassumption.
eassumption.
assumption.
Qed.
Theorem transl_program_correct:
forall i sg,
forward_simulation
(
CsharpminorX.semantics fn_stack_requirements prog i init_m sg args)
(
semantics_with_inject (
CminorX.semantics fn_stack_requirements tprog i init_m sg args)
init_m).
Proof.
intros.
eapply forward_simulation_star with (match_states := fun s1 s2 => match_states prog init_m s1 s2 /\ Cminor.stack_inv s2); eauto.
- apply senv_preserved; auto.
- simpl; intros s1 IS. edestruct transl_initial_states as (s2 & IS2 & MS); eauto.
eexists; split; eauto. split; auto.
eapply CminorX.stack_inv_initial; eauto.
- intros s1 s2 r (MS & SI); apply transl_final_states; auto.
- instantiate (1 := measure).
simpl. intros s1 t s1' STEP s2 (MS & SI).
exploit transl_step_correct; eauto. intros [(s2' & STEPS & MS')|(LT & EQ & MS')]; [left|right].
eexists; split; eauto. split; auto.
eapply inv_plus; eauto. eapply Cminor.stack_inv_inv; eauto.
auto.
Qed.
End WITHCONFIG.