diff options
Diffstat (limited to 'common/Globalenvs.v')
| -rw-r--r-- | common/Globalenvs.v | 144 |
1 files changed, 72 insertions, 72 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 9affd634..dd8a1eb9 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -259,7 +259,7 @@ Lemma add_globals_app: forall gl2 gl1 ge, add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2. Proof. - intros. apply fold_left_app. + intros. apply fold_left_app. Qed. Program Definition empty_genv (pub: list ident): t := @@ -429,17 +429,17 @@ Proof. { induction l as [ | [id1 g1] l]; intros; simpl. - auto. - apply IHl. unfold P, add_global, find_symbol, find_def; simpl. - rewrite ! PTree.gsspec. destruct (peq id id1). + rewrite ! PTree.gsspec. destruct (peq id id1). + subst id1. split; intros. inv H0. exists (genv_next ge); split; auto. apply PTree.gss. destruct H0 as (b & A & B). inv A. rewrite PTree.gss in B. auto. + red in H; rewrite H. split. - intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto. - apply Plt_ne. eapply genv_symb_range; eauto. - intros (b & A & B). rewrite PTree.gso in B. exists b; auto. - apply Plt_ne. eapply genv_symb_range; eauto. + intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto. + apply Plt_ne. eapply genv_symb_range; eauto. + intros (b & A & B). rewrite PTree.gso in B. exists b; auto. + apply Plt_ne. eapply genv_symb_range; eauto. } - apply REC. unfold P, find_symbol, find_def; simpl. + apply REC. unfold P, find_symbol, find_def; simpl. rewrite ! PTree.gempty. split. congruence. intros (b & A & B); congruence. @@ -770,12 +770,12 @@ Remark store_init_data_perm: store_init_data m b p i = Some m' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - intros. + intros. assert (forall chunk v, Mem.store chunk m b p v = Some m' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm)). intros; split; eauto with mem. - destruct i; simpl in H; eauto. + destruct i; simpl in H; eauto. inv H; tauto. destruct (find_symbol ge i); try discriminate. eauto. Qed. @@ -788,7 +788,7 @@ Proof. induction idl as [ | i1 idl]; simpl; intros. - inv H; tauto. - destruct (store_init_data m b p i1) as [m1|] eqn:S1; try discriminate. - transitivity (Mem.perm m1 b' q k prm). + transitivity (Mem.perm m1 b' q k prm). eapply store_init_data_perm; eauto. eapply IHidl; eauto. Qed. @@ -849,8 +849,8 @@ Proof. intros until n. functional induction (store_zeros m b p n); intros. - inv H; apply Mem.unchanged_on_refl. - apply Mem.unchanged_on_trans with m'. -+ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. -+ apply IHo; auto. intros; apply H0; omega. ++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. ++ apply IHo; auto. intros; apply H0; omega. - discriminate. Qed. @@ -878,7 +878,7 @@ Proof. - inv H. apply Mem.unchanged_on_refl. - destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. apply Mem.unchanged_on_trans with m1. - eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. + eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega. Qed. @@ -947,8 +947,8 @@ Proof. intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). - inv H. simpl. assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0). - { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } - rewrite <- EQ. apply H0. omega. simpl. omega. + { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } + rewrite <- EQ. apply H0. omega. simpl. omega. - rewrite init_data_size_addrof. simpl. destruct (find_symbol ge i) as [b'|]; try discriminate. rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H). @@ -976,14 +976,14 @@ Proof. eapply store_init_data_list_unchanged; eauto. intros; omega. intros; omega. - eapply store_init_data_loadbytes; eauto. + eapply store_init_data_loadbytes; eauto. red; intros; apply H0. omega. omega. apply IHil with m1; auto. - red; intros. + red; intros. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1). - eapply store_init_data_unchanged; eauto. + eapply store_init_data_unchanged; eauto. + intros; omega. intros; omega. - intros; omega. apply H0. omega. omega. auto. auto. Qed. @@ -1010,9 +1010,9 @@ Remark read_as_zero_unchanged: (forall i, ofs <= i < ofs + len -> P b i) -> read_as_zero m' b ofs len. Proof. - intros; red; intros. eapply Mem.load_unchanged_on; eauto. - intros; apply H1. omega. -Qed. + intros; red; intros. eapply Mem.load_unchanged_on; eauto. + intros; apply H1. omega. +Qed. Lemma store_zeros_read_as_zero: forall m b p n m', @@ -1078,7 +1078,7 @@ Proof. exploit IHil; eauto. set (P := fun (b': block) ofs' => p + init_data_size a <= ofs'). apply read_as_zero_unchanged with (m := m) (P := P). - red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. + red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. eapply store_init_data_unchanged with (P := P); eauto. intros; unfold P. omega. intros; unfold P. omega. @@ -1094,7 +1094,7 @@ Proof. set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)). inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P). red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. - eapply store_init_data_list_unchanged; eauto. + eapply store_init_data_list_unchanged; eauto. intros; unfold P. omega. intros; unfold P. simpl; xomega. + rewrite init_data_size_addrof in *. @@ -1118,7 +1118,7 @@ Proof. apply Mem.unchanged_on_implies with Q. apply Mem.unchanged_on_trans with m1. eapply Mem.alloc_unchanged_on; eauto. - eapply Mem.drop_perm_unchanged_on; eauto. + eapply Mem.drop_perm_unchanged_on; eauto. intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem. - (* variable *) set (init := gvar_init v) in *. @@ -1133,8 +1133,8 @@ Proof. apply Mem.unchanged_on_trans with m2. eapply store_zeros_unchanged; eauto. apply Mem.unchanged_on_trans with m3. - eapply store_init_data_list_unchanged; eauto. - eapply Mem.drop_perm_unchanged_on; eauto. + eapply store_init_data_list_unchanged; eauto. + eapply Mem.drop_perm_unchanged_on; eauto. intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem. Qed. @@ -1147,7 +1147,7 @@ Proof. - inv H. apply Mem.unchanged_on_refl. - destruct (alloc_global m a) as [m''|] eqn:?; try discriminate. destruct a as [id g]. - apply Mem.unchanged_on_trans with m''. + apply Mem.unchanged_on_trans with m''. eapply alloc_global_unchanged; eauto. apply IHgl; auto. Qed. @@ -1196,7 +1196,7 @@ Proof. exploit Mem.alloc_result; eauto. intros RES. rewrite H, <- RES. split. eapply Mem.perm_drop_1; eauto. omega. - intros. + intros. assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. } exploit Mem.perm_drop_2; eauto. intros ORD. split. omega. inv ORD; auto. @@ -1210,35 +1210,35 @@ Proof. split. red; intros. eapply Mem.perm_drop_1; eauto. split. intros. assert (0 <= ofs < sz). - { eapply Mem.perm_alloc_3; eauto. + { eapply Mem.perm_alloc_3; eauto. erewrite store_zeros_perm by eauto. - erewrite store_init_data_list_perm by eauto. + erewrite store_init_data_list_perm by eauto. eapply Mem.perm_drop_4; eauto. } split; auto. eapply Mem.perm_drop_2; eauto. split. intros NOTVOL. apply load_store_init_data_invariant with m3. - intros. eapply Mem.load_drop; eauto. right; right; right. + intros. eapply Mem.load_drop; eauto. right; right; right. unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem. - eapply store_init_data_list_charact; eauto. + eapply store_init_data_list_charact; eauto. eapply store_zeros_read_as_zero; eauto. - intros NOTVOL. - transitivity (Mem.loadbytes m3 b 0 sz). + intros NOTVOL. + transitivity (Mem.loadbytes m3 b 0 sz). eapply Mem.loadbytes_drop; eauto. right; right; right. unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem. eapply store_init_data_list_loadbytes; eauto. eapply store_zeros_loadbytes; eauto. + assert (U: Mem.unchanged_on (fun _ _ => True) m m') by (eapply alloc_global_unchanged; eauto). assert (VALID: Mem.valid_block m b). - { red. rewrite <- H. eapply genv_defs_range; eauto. } + { red. rewrite <- H. eapply genv_defs_range; eauto. } exploit H1; eauto. destruct gd0 as [f|v]. * intros [A B]; split; intros. eapply Mem.perm_unchanged_on; eauto. exact I. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I. -* intros (A & B & C & D). split; [| split; [| split]]. +* intros (A & B & C & D). split; [| split; [| split]]. red; intros. eapply Mem.perm_unchanged_on; eauto. exact I. intros. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I. - intros. apply load_store_init_data_invariant with m; auto. + intros. apply load_store_init_data_invariant with m; auto. intros. eapply Mem.load_unchanged_on_1; eauto. intros; exact I. intros. eapply Mem.loadbytes_unchanged_on; eauto. intros; exact I. - simpl. congruence. @@ -1312,7 +1312,7 @@ Lemma init_mem_characterization_gen: init_mem p = Some m -> globals_initialized (globalenv p) (globalenv p) m. Proof. - intros. apply alloc_globals_initialized with Mem.empty. + intros. apply alloc_globals_initialized with Mem.empty. auto. rewrite Mem.nextblock_empty. auto. red; intros. unfold find_def in H0; simpl in H0; rewrite PTree.gempty in H0; discriminate. @@ -1499,7 +1499,7 @@ Proof. { intros. apply Mem.store_valid_access_3 in H0. destruct H0. congruence. } destruct i; simpl in H; eauto. simpl. apply Z.divide_1_l. - destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption. + destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption. unfold Mptr, init_data_alignment; destruct Archi.ptr64; auto. Qed. @@ -1537,14 +1537,14 @@ Theorem init_mem_inversion: init_data_list_aligned 0 v.(gvar_init) /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b. Proof. - intros until v. unfold init_mem. set (ge := globalenv p). - revert m. generalize Mem.empty. generalize (prog_defs p). + intros until v. unfold init_mem. set (ge := globalenv p). + revert m. generalize Mem.empty. generalize (prog_defs p). induction l as [ | idg1 defs ]; simpl; intros m m'; intros. - contradiction. - destruct (alloc_global ge m idg1) as [m''|] eqn:A; try discriminate. destruct H0. -+ subst idg1; simpl in A. - set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *. ++ subst idg1; simpl in A. + set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *. destruct (Mem.alloc m 0 sz) as [m1 b]. destruct (store_zeros m1 b 0 sz) as [m2|]; try discriminate. destruct (store_init_data_list ge m2 b 0 il) as [m3|] eqn:B; try discriminate. @@ -1565,7 +1565,7 @@ Proof. - exists m; auto. - apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega. - destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE). - split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. + split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. simpl. apply Z.divide_1_l. congruence. Qed. @@ -1577,17 +1577,17 @@ Lemma store_init_data_exists: (forall id ofs, i = Init_addrof id ofs -> exists b, find_symbol ge id = Some b) -> exists m', store_init_data ge m b p i = Some m'. Proof. - intros. + intros. assert (DFL: forall chunk v, init_data_size i = size_chunk chunk -> init_data_alignment i = align_chunk chunk -> exists m', Mem.store chunk m b p v = Some m'). { intros. destruct (Mem.valid_access_store m chunk b p v) as (m' & STORE). - split. rewrite <- H2; auto. rewrite <- H3; auto. + split. rewrite <- H2; auto. rewrite <- H3; auto. exists m'; auto. } destruct i; eauto. simpl. exists m; auto. - simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL. + simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL. unfold init_data_size, Mptr. destruct Archi.ptr64; auto. unfold init_data_alignment, Mptr. destruct Archi.ptr64; auto. Qed. @@ -1601,11 +1601,11 @@ Lemma store_init_data_list_exists: Proof. induction il as [ | i1 il ]; simpl; intros. - exists m; auto. -- destruct H0. +- destruct H0. destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto. red; intros. apply H. generalize (init_data_list_size_pos il); omega. - rewrite S1. - apply IHil; eauto. + rewrite S1. + apply IHil; eauto. red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega. Qed. @@ -1622,7 +1622,7 @@ Proof. intros m [id [f|v]]; intros; simpl. - destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC. destruct (Mem.range_perm_drop_2 m1 b 0 1 Nonempty) as [m2 DROP]. - red; intros; eapply Mem.perm_alloc_2; eauto. + red; intros; eapply Mem.perm_alloc_2; eauto. exists m2; auto. - destruct H as [P Q]. set (sz := init_data_list_size (gvar_init v)). @@ -1651,14 +1651,14 @@ Theorem init_mem_exists: /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b) -> exists m, init_mem p = Some m. Proof. - intros. set (ge := globalenv p) in *. + intros. set (ge := globalenv p) in *. unfold init_mem. revert H. generalize (prog_defs p) Mem.empty. induction l as [ | idg l]; simpl; intros. - exists m; auto. - destruct (@alloc_global_exists ge m idg) as [m1 A1]. destruct idg as [id [f|v]]; eauto. - fold ge. rewrite A1. eapply IHl; eauto. -Qed. + fold ge. rewrite A1. eapply IHl; eauto. +Qed. End GENV. @@ -1685,8 +1685,8 @@ Lemma add_global_match: Proof. intros. destruct H. constructor; simpl; intros. - congruence. -- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto. -- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)). +- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto. +- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)). constructor; auto. auto. Qed. @@ -1718,7 +1718,7 @@ Hypothesis progmatch: match_program_gen match_fundef match_varinfo ctx p tp. Lemma globalenvs_match: match_genvs (match_globdef match_fundef match_varinfo ctx) (globalenv p) (globalenv tp). Proof. - intros. apply add_globals_match. apply progmatch. + intros. apply add_globals_match. apply progmatch. constructor; simpl; intros; auto. rewrite ! PTree.gempty. constructor. Qed. @@ -1734,7 +1734,7 @@ Theorem find_def_match: find_def (globalenv tp) b = Some tg /\ match_globdef match_fundef match_varinfo ctx g tg. Proof. intros. generalize (find_def_match_2 b). rewrite H; intros R; inv R. - exists y; auto. + exists y; auto. Qed. Theorem find_funct_ptr_match: @@ -1743,8 +1743,8 @@ Theorem find_funct_ptr_match: exists cunit tf, find_funct_ptr (globalenv tp) b = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx. Proof. - intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H. - destruct H as (tg & P & Q). inv Q. + intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H. + destruct H as (tg & P & Q). inv Q. exists ctx', f2; intuition auto. apply find_funct_ptr_iff; auto. Qed. @@ -1766,8 +1766,8 @@ Theorem find_var_info_match: exists tv, find_var_info (globalenv tp) b = Some tv /\ match_globvar match_varinfo v tv. Proof. - intros. rewrite find_var_info_iff in *. apply find_def_match in H. - destruct H as (tg & P & Q). inv Q. + intros. rewrite find_var_info_iff in *. apply find_def_match in H. + destruct H as (tg & P & Q). inv Q. exists v2; split; auto. apply find_var_info_iff; auto. Qed. @@ -1783,10 +1783,10 @@ Theorem senv_match: Proof. red; simpl. repeat split. - apply find_symbol_match. -- intros. unfold public_symbol. rewrite find_symbol_match. - rewrite ! globalenv_public. +- intros. unfold public_symbol. rewrite find_symbol_match. + rewrite ! globalenv_public. destruct progmatch as (P & Q & R). rewrite R. auto. -- intros. unfold block_is_volatile. +- intros. unfold block_is_volatile. destruct globalenvs_match as [P Q R]. specialize (R b). unfold find_var_info, find_def. inv R; auto. @@ -1820,7 +1820,7 @@ Proof. { destruct a1 as [id1 g1]; destruct b1 as [id2 g2]; destruct H; simpl in *. subst id2. inv H2. - auto. - - inv H; simpl in *. + - inv H; simpl in *. set (sz := init_data_list_size init) in *. destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?. destruct (store_zeros m2 b 0 sz) as [m3|] eqn:?; try discriminate. @@ -1853,7 +1853,7 @@ Theorem find_funct_ptr_transf_partial: exists tf, find_funct_ptr (globalenv tp) b = Some tf /\ transf f = OK tf. Proof. - intros. exploit (find_funct_ptr_match progmatch); eauto. + intros. exploit (find_funct_ptr_match progmatch); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -1863,7 +1863,7 @@ Theorem find_funct_transf_partial: exists tf, find_funct (globalenv tp) v = Some tf /\ transf f = OK tf. Proof. - intros. exploit (find_funct_match progmatch); eauto. + intros. exploit (find_funct_match progmatch); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -1871,7 +1871,7 @@ Theorem find_symbol_transf_partial: forall (s : ident), find_symbol (globalenv tp) s = find_symbol (globalenv p) s. Proof. - intros. eapply (find_symbol_match progmatch). + intros. eapply (find_symbol_match progmatch). Qed. Theorem senv_transf_partial: @@ -1901,7 +1901,7 @@ Theorem find_funct_ptr_transf: find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv tp) b = Some (transf f). Proof. - intros. exploit (find_funct_ptr_match progmatch); eauto. + intros. exploit (find_funct_ptr_match progmatch); eauto. intros (cu & tf & P & Q & R). congruence. Qed. @@ -1910,7 +1910,7 @@ Theorem find_funct_transf: find_funct (globalenv p) v = Some f -> find_funct (globalenv tp) v = Some (transf f). Proof. - intros. exploit (find_funct_match progmatch); eauto. + intros. exploit (find_funct_match progmatch); eauto. intros (cu & tf & P & Q & R). congruence. Qed. |