From b279716c76c387c6c5eec96388c0c35629858b4c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 26 Nov 2014 14:46:07 +0100 Subject: Introduce symbol environments (type Senv.t) as a restricted view on global environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events). --- cfrontend/Cexec.v | 24 ++++++++++++------------ cfrontend/Cshmgenproof.v | 36 ++++++------------------------------ cfrontend/SimplExprproof.v | 4 ++-- 3 files changed, 20 insertions(+), 44 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 80748df1..5c062158 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -149,7 +149,7 @@ Lemma eventval_of_val_complete: forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev. Proof. induction 1; simpl; auto. - rewrite (Genv.find_invert_symbol _ _ H0). rewrite H. auto. + rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. auto. Qed. Lemma list_eventval_of_val_sound: @@ -181,14 +181,14 @@ Qed. Lemma val_of_eventval_complete: forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v. Proof. - induction 1; simpl; auto. rewrite H, H0; auto. + induction 1; simpl; auto. simpl in *. rewrite H, H0; auto. Qed. (** Volatile memory accesses. *) Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) : option (world * trace * val) := - if block_is_volatile ge b then + if Genv.block_is_volatile ge b then do id <- Genv.invert_symbol ge b; match nextworld_vload w chunk id ofs with | None => None @@ -202,7 +202,7 @@ Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) (v: val) : option (world * trace * mem) := - if block_is_volatile ge b then + if Genv.block_is_volatile ge b then do id <- Genv.invert_symbol ge b; do ev <- eventval_of_val (Val.load_result chunk v) (type_of_chunk chunk); do w' <- nextworld_vstore w chunk id ofs ev; @@ -239,7 +239,7 @@ Lemma do_volatile_load_complete: volatile_load ge chunk m b ofs t v -> possible_trace w t w' -> do_volatile_load w chunk m b ofs = Some(w', t, v). Proof. - unfold do_volatile_load; intros. inv H. + unfold do_volatile_load; intros. inv H; simpl in *. rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2). inv H0. inv H8. inv H6. rewrite H9. rewrite (val_of_eventval_complete _ _ _ H3). auto. rewrite H1. rewrite H2. inv H0. auto. @@ -262,7 +262,7 @@ Lemma do_volatile_store_complete: volatile_store ge chunk m b ofs v t m' -> possible_trace w t w' -> do_volatile_store w chunk m b ofs v = Some(w', t, m'). Proof. - unfold do_volatile_store; intros. inv H. + unfold do_volatile_store; intros. inv H; simpl in *. rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2). rewrite (eventval_of_val_complete _ _ _ H3). inv H0. inv H8. inv H6. rewrite H9. auto. @@ -387,7 +387,7 @@ Qed. (** External calls *) Variable do_external_function: - ident -> signature -> genv -> world -> list val -> mem -> option (world * trace * val * mem). + ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_external_function_sound: forall id sg ge vargs m t vres m' w w', @@ -401,7 +401,7 @@ Hypothesis do_external_function_complete: do_external_function id sg ge w vargs m = Some(w', t, vres, m'). Variable do_inline_assembly: - ident -> genv -> world -> list val -> mem -> option (world * trace * val * mem). + ident -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_inline_assembly_sound: forall txt ge vargs m t vres m' w w', @@ -573,11 +573,11 @@ Proof with try congruence. (* EF_vstore *) auto. (* EF_vload_global *) - rewrite volatile_load_global_charact. + rewrite volatile_load_global_charact; simpl. unfold do_ef_volatile_load_global. destruct (Genv.find_symbol ge)... intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto. (* EF_vstore_global *) - rewrite volatile_store_global_charact. + rewrite volatile_store_global_charact; simpl. unfold do_ef_volatile_store_global. destruct (Genv.find_symbol ge)... intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto. (* EF_malloc *) @@ -633,10 +633,10 @@ Proof. (* EF_vstore *) auto. (* EF_vload_global *) - rewrite volatile_load_global_charact in H. destruct H as [b [P Q]]. + rewrite volatile_load_global_charact in H; simpl in H. destruct H as [b [P Q]]. unfold do_ef_volatile_load_global. rewrite P. auto. (* EF_vstore *) - rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. + rewrite volatile_store_global_charact in H; simpl in H. destruct H as [b [P Q]]. unfold do_ef_volatile_store_global. rewrite P. auto. (* EF_malloc *) inv H; unfold do_ef_malloc. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 9cb112b0..dc47df04 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -759,29 +759,9 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar _ TRANSL). -Lemma var_info_translated: - forall b v, - Genv.find_var_info ge b = Some v -> - exists tv, Genv.find_var_info tge b = Some tv /\ transf_globvar transl_globvar v = OK tv. -Proof (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). - -Lemma var_info_rev_translated: - forall b tv, - Genv.find_var_info tge b = Some tv -> - exists v, Genv.find_var_info ge b = Some v /\ transf_globvar transl_globvar v = OK tv. -Proof (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). - Lemma block_is_volatile_preserved: - forall b, block_is_volatile tge b = block_is_volatile ge b. -Proof. - intros. unfold block_is_volatile. - destruct (Genv.find_var_info ge b) eqn:?. - exploit var_info_translated; eauto. intros [tv [A B]]. rewrite A. - unfold transf_globvar in B. monadInv B. auto. - destruct (Genv.find_var_info tge b) eqn:?. - exploit var_info_rev_translated; eauto. intros [tv [A B]]. congruence. - auto. -Qed. + forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b. +Proof (Genv.block_is_volatile_transf_partial2 transl_fundef transl_globvar _ TRANSL). (** * Matching between environments *) @@ -1288,10 +1268,8 @@ Proof. econstructor; split. apply plus_one. econstructor. eapply transl_arglist_correct; eauto. - eapply external_call_symbols_preserved_2; eauto. - exact symbols_preserved. exact public_preserved. - eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). - eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). + eapply external_call_symbols_preserved_gen with (ge1 := ge). + exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto. eapply match_states_skip; eauto. (* seq *) @@ -1469,10 +1447,8 @@ Proof. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. constructor. eauto. - eapply external_call_symbols_preserved_2; eauto. - exact symbols_preserved. exact public_preserved. - eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). - eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). + eapply external_call_symbols_preserved_gen with (ge1 := ge). + exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto. econstructor; eauto. (* returnstate *) diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 250f2b26..6d8b5c86 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -91,9 +91,9 @@ Proof. Qed. Lemma block_is_volatile_preserved: - forall b, block_is_volatile tge b = block_is_volatile ge b. + forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b. Proof. - intros. unfold block_is_volatile. rewrite varinfo_preserved. auto. + intros. unfold Genv.block_is_volatile. rewrite varinfo_preserved. auto. Qed. Lemma type_of_fundef_preserved: -- cgit