diff options
Diffstat (limited to 'cfrontend/SimplExprproof.v')
-rw-r--r-- | cfrontend/SimplExprproof.v | 81 |
1 files changed, 45 insertions, 36 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index a2b8e615..dfe1c8ab 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -44,29 +44,44 @@ Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof - (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). +Proof. + intros. eapply Genv.find_symbol_match. eapply transl_program_spec; eauto. + simpl. tauto. +Qed. Lemma function_ptr_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. -Proof - (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). + Genv.find_funct_ptr tge b = Some tf /\ tr_fundef f tf. +Proof. + intros. eapply Genv.find_funct_ptr_match. + eapply transl_program_spec; eauto. + assumption. +Qed. Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. -Proof - (Genv.find_funct_transf_partial transl_fundef _ TRANSL). + Genv.find_funct tge v = Some tf /\ tr_fundef f tf. +Proof. + intros. eapply Genv.find_funct_match. + eapply transl_program_spec; eauto. + assumption. +Qed. Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof - (Genv.find_var_info_transf_partial transl_fundef _ TRANSL). +Proof. + intros. destruct (Genv.find_var_info ge b) as [v|] eqn:V. +- exploit Genv.find_var_info_match. eapply transl_program_spec; eauto. eassumption. + intros [tv [A B]]. inv B. assumption. +- destruct (Genv.find_var_info tge b) as [v'|] eqn:V'; auto. + exploit Genv.find_var_info_rev_match. eapply transl_program_spec; eauto. eassumption. + simpl. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try tauto. + intros [v [A B]]. inv B. fold ge in A. congruence. +Qed. Lemma block_is_volatile_preserved: forall b, block_is_volatile tge b = block_is_volatile ge b. @@ -75,22 +90,19 @@ Proof. Qed. Lemma type_of_fundef_preserved: - forall f tf, transl_fundef f = OK tf -> + forall f tf, tr_fundef f tf -> type_of_fundef tf = Csyntax.type_of_fundef f. Proof. - intros. destruct f; monadInv H. - exploit transl_function_spec; eauto. intros [A [B [C D]]]. - simpl. unfold type_of_function, Csyntax.type_of_function. congruence. + intros. inv H. + inv H0; simpl. unfold type_of_function, Csyntax.type_of_function. congruence. auto. Qed. Lemma function_return_preserved: - forall f tf, transl_function f = OK tf -> + forall f tf, tr_function f tf -> fn_return tf = Csyntax.fn_return f. Proof. - intros. unfold transl_function in H. - destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); inv H. - auto. + intros. inv H; auto. Qed. Lemma type_of_global_preserved: @@ -893,7 +905,7 @@ Inductive match_cont : Csem.cont -> cont -> Prop := match_cont k tk -> match_cont (Csem.Kswitch2 k) (Kswitch tk) | match_Kcall: forall f e C ty k optid tf le sl tk a dest tmps, - transl_function f = Errors.OK tf -> + tr_function f tf -> leftcontext RV RV C -> (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (Csyntax.Eval v ty)) sl a tmps) -> match_cont_exp dest a k tk -> @@ -961,19 +973,19 @@ Qed. Inductive match_states: Csem.state -> state -> Prop := | match_exprstates: forall f r k e m tf sl tk le dest a tmps, - transl_function f = Errors.OK tf -> + tr_function f tf -> tr_top tge e le m dest r sl a tmps -> match_cont_exp dest a k tk -> match_states (Csem.ExprState f r k e m) (State tf Sskip (Kseqlist sl tk) e le m) | match_regularstates: forall f s k e m tf ts tk le, - transl_function f = Errors.OK tf -> + tr_function f tf -> tr_stmt s ts -> match_cont k tk -> match_states (Csem.State f s k e m) (State tf ts tk e le m) | match_callstates: forall fd args k m tfd tk, - transl_fundef fd = Errors.OK tfd -> + tr_fundef fd tfd -> match_cont k tk -> match_states (Csem.Callstate fd args k m) (Callstate tfd args tk m) @@ -2089,8 +2101,7 @@ Proof. inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left. eapply plus_two. constructor. econstructor. eauto. - replace (fn_return tf) with (Csyntax.fn_return f). eauto. - exploit transl_function_spec; eauto. intuition congruence. + erewrite function_return_preserved; eauto. eauto. traceEq. constructor. apply match_cont_call; auto. (* skip return *) @@ -2133,8 +2144,8 @@ Proof. (* goto *) inv H7. - exploit transl_function_spec; eauto. intros [A [B [C D]]]. - exploit tr_find_label. eexact A. apply match_cont_call. eauto. + inversion H6; subst. + exploit tr_find_label. eauto. apply match_cont_call. eauto. instantiate (1 := lbl). rewrite H. intros [ts' [tk' [P [Q R]]]]. econstructor; split. @@ -2142,18 +2153,17 @@ Proof. econstructor; eauto. (* internal function *) - monadInv H7. - exploit transl_function_spec; eauto. intros [A [B [C D]]]. + inv H7. inversion H3; subst. econstructor; split. left; apply plus_one. eapply step_internal_function. econstructor. - rewrite C; rewrite D; auto. - rewrite C; rewrite D. eapply alloc_variables_preserved; eauto. - rewrite C. eapply bind_parameters_preserved; eauto. + rewrite H5; rewrite H6; auto. + rewrite H5; rewrite H6. eapply alloc_variables_preserved; eauto. + rewrite H5. eapply bind_parameters_preserved; eauto. eauto. constructor; auto. (* external function *) - monadInv H5. + inv H5. econstructor; split. left; apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. @@ -2188,14 +2198,13 @@ Lemma transl_initial_states: exists S', Clight.initial_state tprog S' /\ match_states S S'. Proof. intros. inv H. + exploit transl_program_spec; eauto. intros MP. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. - apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto. + exploit Genv.init_mem_match; eauto. simpl. fold tge. rewrite symbols_preserved. - replace (prog_main tprog) with (prog_main prog). eexact H1. - symmetry. unfold transl_program in TRANSL. - eapply transform_partial_program_main; eauto. + destruct MP as [A B]. rewrite B; eexact H1. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. |