From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Jul 2011 08:26:16 +0000 Subject: Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 51 +++++++++--------------------------------------- 1 file changed, 9 insertions(+), 42 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 49d3ff3..28e6dad 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1846,14 +1846,14 @@ Proof. Qed. Lemma transl_initial_states: - forall S t S', Clight.initial_state prog S -> Clight.step ge S t S' -> + forall S, Clight.initial_state prog S -> exists R, initial_state tprog R /\ match_states S R. Proof. intros. inv H. exploit function_ptr_translated; eauto. intros [tf [A B]]. assert (C: Genv.find_symbol tge (prog_main tprog) = Some b). rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). - exact H2. symmetry. unfold transl_program in TRANSL. + auto. symmetry. unfold transl_program in TRANSL. eapply transform_partial_program2_main; eauto. assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). eapply transl_fundef_sig2; eauto. @@ -1870,46 +1870,13 @@ Proof. Qed. Theorem transl_program_correct: - forall (beh: program_behavior), - not_wrong beh -> Clight.exec_program prog beh -> - Csharpminor.exec_program tprog beh. -Proof. - set (order := fun (S1 S2: Clight.state) => False). - assert (WF: well_founded order). - unfold order; red. intros. constructor; intros. contradiction. - assert (transl_step': - forall S1 t S2, Clight.step ge S1 t S2 -> - forall T1, match_states S1 T1 -> - exists T2, - (plus step tge T1 t T2 \/ star step tge T1 t T2 /\ order S2 S1) - /\ match_states S2 T2). - intros. exploit transl_step; eauto. intros [T2 [A B]]. - exists T2; split. auto. auto. - intros. inv H0. -(* Terminates *) - assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). - inv H3. inv H2. inv H1. exists t1; exists s2; auto. - destruct H0 as [t1 [s1 ST]]. - exploit transl_initial_states; eauto. intros [R [A B]]. - exploit simulation_star_star; eauto. intros [R' [C D]]. - econstructor; eauto. eapply transl_final_states; eauto. -(* Diverges *) - assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). - inv H2. inv H3. exists E0; exists s2; auto. exists t1; exists s2; auto. - destruct H0 as [t1 [s1 ST]]. - exploit transl_initial_states; eauto. intros [R [A B]]. - exploit simulation_star_star; eauto. intros [R' [C D]]. - econstructor; eauto. eapply simulation_star_forever_silent; eauto. -(* Reacts *) - assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). - inv H2. inv H0. congruence. exists t1; exists s0; auto. - destruct H0 as [t1 [s1 ST]]. - exploit transl_initial_states; eauto. intros [R [A B]]. - exploit simulation_star_forever_reactive; eauto. - intro C. - econstructor; eauto. -(* Goes wrong *) - contradiction. contradiction. + forward_simulation (Clight.semantics prog) (Csharpminor.semantics tprog). +Proof. + eapply forward_simulation_plus. + eexact symbols_preserved. + eexact transl_initial_states. + eexact transl_final_states. + eexact transl_step. Qed. End CORRECTNESS. -- cgit v1.2.3