From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- common/Globalenvs.v | 564 ++++++++++++++++++++++++++-------------------------- 1 file changed, 282 insertions(+), 282 deletions(-) (limited to 'common/Globalenvs.v') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 30f03654..5f78ea6b 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -14,11 +14,11 @@ (* *) (* *********************************************************************) -(** Global environments are a component of the dynamic semantics of +(** Global environments are a component of the dynamic semantics of all languages involved in the compiler. A global environment maps symbol names (names of functions and of global variables) to the corresponding memory addresses. It also maps memory addresses - of functions to the corresponding function descriptions. + of functions to the corresponding function descriptions. Global environments, along with the initial memory state at the beginning of program execution, are built from the program of interest, as follows: @@ -110,7 +110,7 @@ Theorem shift_symbol_address: forall ge id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). Proof. - intros. unfold symbol_address. destruct (find_symbol ge id); auto. + intros. unfold symbol_address. destruct (find_symbol ge id); auto. Qed. End Senv. @@ -137,7 +137,7 @@ Record t: Type := mkgenv { genv_vars_range: forall b v, PTree.get b genv_vars = Some v -> Plt b genv_next; genv_funs_vars: forall b1 b2 f v, PTree.get b1 genv_funs = Some f -> PTree.get b2 genv_vars = Some v -> b1 <> b2; - genv_vars_inj: forall id1 id2 b, + genv_vars_inj: forall id1 id2 b, PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2 }. @@ -225,18 +225,18 @@ Next Obligation. apply Plt_trans_succ; eauto. Qed. Next Obligation. - destruct ge; simpl in *. - destruct g. - rewrite PTree.gsspec in H. + destruct ge; simpl in *. + destruct g. + rewrite PTree.gsspec in H. destruct (peq b genv_next0). inv H. apply Plt_succ. apply Plt_trans_succ; eauto. apply Plt_trans_succ; eauto. Qed. Next Obligation. - destruct ge; simpl in *. + destruct ge; simpl in *. destruct g. apply Plt_trans_succ; eauto. - rewrite PTree.gsspec in H. + rewrite PTree.gsspec in H. destruct (peq b genv_next0). inv H. apply Plt_succ. apply Plt_trans_succ; eauto. Qed. @@ -253,8 +253,8 @@ Next Obligation. eauto. Qed. Next Obligation. - destruct ge; simpl in *. - rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. + destruct ge; simpl in *. + rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. destruct (peq id1 i); destruct (peq id2 i). congruence. inv H. eelim Plt_strict. eapply genv_symb_range0; eauto. @@ -304,9 +304,9 @@ Lemma add_globals_preserves: (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) -> P ge -> P (add_globals ge gl). Proof. - induction gl; simpl; intros. + induction gl; simpl; intros. auto. - destruct a. apply IHgl; auto. + destruct a. apply IHgl; auto. Qed. Lemma add_globals_ensures: @@ -317,8 +317,8 @@ Lemma add_globals_ensures: Proof. induction gl; simpl; intros. contradiction. - destruct H1. subst a. apply add_globals_preserves; auto. - apply IHgl; auto. + destruct H1. subst a. apply add_globals_preserves; auto. + apply IHgl; auto. Qed. Lemma add_globals_unique_preserves: @@ -326,9 +326,9 @@ Lemma add_globals_unique_preserves: (forall ge id1 g, P ge -> In (id1, g) gl -> id1 <> id -> P (add_global ge (id1, g))) -> ~In id (map fst gl) -> P ge -> P (add_globals ge gl). Proof. - induction gl; simpl; intros. + induction gl; simpl; intros. auto. - destruct a. apply IHgl; auto. + destruct a. apply IHgl; auto. Qed. Lemma add_globals_unique_ensures: @@ -347,10 +347,10 @@ Remark in_norepet_unique: Proof. induction gl as [|[id1 g1] gl]; simpl; intros. contradiction. - inv H0. destruct H. - inv H. exists nil, gl. auto. - exploit IHgl; eauto. intros (gl1 & gl2 & X & Y). - exists ((id1, g1) :: gl1), gl2; split; auto. rewrite X; auto. + inv H0. destruct H. + inv H. exists nil, gl. auto. + exploit IHgl; eauto. intros (gl1 & gl2 & X & Y). + exists ((id1, g1) :: gl1), gl2; split; auto. rewrite X; auto. Qed. Lemma add_globals_norepet_ensures: @@ -359,8 +359,8 @@ Lemma add_globals_norepet_ensures: (forall ge, P (add_global ge (id, g))) -> In (id, g) gl -> list_norepet (map fst gl) -> P (add_globals ge gl). Proof. - intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). - subst gl. apply add_globals_unique_ensures; auto. intros. eapply H; eauto. + intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). + subst gl. apply add_globals_unique_ensures; auto. intros. eapply H; eauto. apply in_or_app; simpl; auto. Qed. @@ -371,7 +371,7 @@ End GLOBALENV_PRINCIPLES. Theorem public_symbol_exists: forall ge id, public_symbol ge id = true -> exists b, find_symbol ge id = Some b. Proof. - unfold public_symbol; intros. destruct (find_symbol ge id) as [b|]. + unfold public_symbol; intros. destruct (find_symbol ge id) as [b|]. exists b; auto. discriminate. Qed. @@ -380,15 +380,15 @@ Theorem shift_symbol_address: forall ge id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). Proof. - intros. unfold symbol_address. destruct (find_symbol ge id); auto. + intros. unfold symbol_address. destruct (find_symbol ge id); auto. Qed. Theorem find_funct_inv: forall ge v f, find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. Proof. - intros until f; unfold find_funct. - destruct v; try congruence. + intros until f; unfold find_funct. + destruct v; try congruence. destruct (Int.eq_dec i Int.zero); try congruence. intros. exists b; congruence. Qed. @@ -428,7 +428,7 @@ Proof. rewrite PTree.gso; auto. destruct g1 as [f1 | v1]. rewrite PTree.gso. auto. apply Plt_ne. eapply genv_funs_range; eauto. - auto. + auto. (* ensures *) intros. unfold find_symbol, find_funct_ptr in *; simpl. exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. @@ -442,8 +442,8 @@ Corollary find_funct_ptr_exists: find_symbol (globalenv p) id = Some b /\ find_funct_ptr (globalenv p) b = Some f. Proof. - intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). - eapply find_funct_ptr_exists_2; eauto. + intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). + eapply find_funct_ptr_exists_2; eauto. Qed. Theorem find_var_exists_2: @@ -462,7 +462,7 @@ Proof. apply Plt_ne. eapply genv_vars_range; eauto. (* ensures *) intros. unfold find_symbol, find_var_info in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. + exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. Qed. Corollary find_var_exists: @@ -473,8 +473,8 @@ Corollary find_var_exists: find_symbol (globalenv p) id = Some b /\ find_var_info (globalenv p) b = Some v. Proof. - intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). - eapply find_var_exists_2; eauto. + intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). + eapply find_var_exists_2; eauto. Qed. Lemma find_symbol_inversion : forall p x b, @@ -483,7 +483,7 @@ Lemma find_symbol_inversion : forall p x b, Proof. intros until b; unfold globalenv. eapply add_globals_preserves. (* preserves *) - unfold find_symbol; simpl; intros. rewrite PTree.gsspec in H1. + unfold find_symbol; simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x id). subst x. change id with (fst (id, g)). apply List.in_map; auto. auto. (* base *) @@ -495,9 +495,9 @@ Theorem find_funct_ptr_inversion: find_funct_ptr (globalenv p) b = Some f -> exists id, In (id, Gfun f) (prog_defs p). Proof. - intros until f. unfold globalenv. apply add_globals_preserves. + intros until f. unfold globalenv. apply add_globals_preserves. (* preserves *) - unfold find_funct_ptr; simpl; intros. destruct g; auto. + unfold find_funct_ptr; simpl; intros. destruct g; auto. rewrite PTree.gsspec in H1. destruct (peq b (genv_next ge)). inv H1. exists id; auto. auto. @@ -510,7 +510,7 @@ Theorem find_funct_inversion: find_funct (globalenv p) v = Some f -> exists id, In (id, Gfun f) (prog_defs p). Proof. - intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. + intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. rewrite find_funct_find_funct_ptr in H. eapply find_funct_ptr_inversion; eauto. Qed. @@ -539,9 +539,9 @@ Theorem find_funct_ptr_symbol_inversion: find_funct_ptr (globalenv p) b = Some f -> In (id, Gfun f) p.(prog_defs). Proof. - intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves. + intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves. (* preserves *) - intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0). + intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0). inv H1. destruct g as [f1|v1]. rewrite PTree.gss in H2. inv H2. auto. eelim Plt_strict. eapply genv_funs_range; eauto. destruct g as [f1|v1]. rewrite PTree.gso in H2. auto. @@ -559,7 +559,7 @@ Theorem global_addresses_distinct: find_symbol ge id2 = Some b2 -> b1 <> b2. Proof. - intros. red; intros; subst. elim H. destruct ge. eauto. + intros. red; intros; subst. elim H. destruct ge. eauto. Qed. Theorem invert_find_symbol: @@ -568,9 +568,9 @@ Theorem invert_find_symbol: Proof. intros until b; unfold find_symbol, invert_symbol. apply PTree_Properties.fold_rec. - intros. rewrite H in H0; auto. + intros. rewrite H in H0; auto. congruence. - intros. destruct (eq_block b v). inv H2. apply PTree.gss. + intros. destruct (eq_block b v). inv H2. apply PTree.gss. rewrite PTree.gsspec. destruct (peq id k). subst. assert (m!k = Some b) by auto. congruence. auto. @@ -588,9 +588,9 @@ Proof. rewrite PTree.gempty; congruence. intros. destruct (eq_block b v). exists k; auto. rewrite PTree.gsspec in H2. destruct (peq id k). - inv H2. congruence. auto. + inv H2. congruence. auto. - intros; exploit H; eauto. intros [id' A]. + intros; exploit H; eauto. intros [id' A]. assert (id = id'). eapply genv_vars_inj; eauto. apply invert_find_symbol; auto. congruence. Qed. @@ -604,14 +604,14 @@ Remark genv_next_add_globals: Proof. induction gl; simpl; intros. auto. - rewrite IHgl. auto. + rewrite IHgl. auto. Qed. Remark genv_public_add_globals: forall gl ge, genv_public (add_globals ge gl) = genv_public ge. Proof. - induction gl; simpl; intros. + induction gl; simpl; intros. auto. rewrite IHgl; auto. Qed. @@ -619,7 +619,7 @@ Qed. Theorem globalenv_public: forall p, genv_public (globalenv p) = prog_public p. Proof. - unfold globalenv; intros. rewrite genv_public_add_globals. auto. + unfold globalenv; intros. rewrite genv_public_add_globals. auto. Qed. Theorem block_is_volatile_below: @@ -765,11 +765,11 @@ Remark store_init_data_list_nextblock: Proof. induction idl; simpl; intros until m'. intros. congruence. - caseEq (store_init_data m b p a); try congruence. intros. - transitivity (Mem.nextblock m0). eauto. + caseEq (store_init_data m b p a); try congruence. intros. + transitivity (Mem.nextblock m0). eauto. destruct a; simpl in H; try (eapply Mem.nextblock_store; eauto; fail). congruence. - destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. + destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. Qed. Remark alloc_global_nextblock: @@ -778,10 +778,10 @@ Remark alloc_global_nextblock: Mem.nextblock m' = Psucc(Mem.nextblock m). Proof. unfold alloc_global. intros. - destruct g as [id [f|v]]. + destruct g as [id [f|v]]. (* function *) destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. - erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto. + erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. @@ -824,13 +824,13 @@ Remark store_init_data_list_perm: (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. induction idl; simpl; intros until m'. - intros. inv H. tauto. + intros. inv H. tauto. caseEq (store_init_data m b p a); try congruence. intros. rewrite <- (IHidl _ _ _ _ H0). assert (forall chunk v, Mem.store chunk m b p v = Some m0 -> (Mem.perm m b' q k prm <-> Mem.perm m0 b' q k prm)). - intros; split; eauto with mem. + intros; split; eauto with mem. destruct a; simpl in H; eauto. inv H; tauto. destruct (find_symbol ge i). eauto. discriminate. @@ -842,13 +842,13 @@ Remark alloc_global_perm: Mem.valid_block m b' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - intros. destruct idg as [id [f|v]]; simpl in H. + intros. destruct idg as [id [f|v]]; simpl in H. (* function *) - destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. + destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. split; intros. - eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto. - eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_drop_4; eauto. + eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto. + eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_drop_4; eauto. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. @@ -860,11 +860,11 @@ Proof. eapply Mem.perm_drop_3; eauto. erewrite <- store_init_data_list_perm; [idtac|eauto]. erewrite <- store_zeros_perm; [idtac|eauto]. - eapply Mem.perm_alloc_1; eauto. + eapply Mem.perm_alloc_1; eauto. eapply Mem.perm_alloc_4; eauto. erewrite store_zeros_perm; [idtac|eauto]. - erewrite store_init_data_list_perm; [idtac|eauto]. - eapply Mem.perm_drop_4; eauto. + erewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. Qed. Remark alloc_globals_perm: @@ -876,7 +876,7 @@ Proof. induction gl. simpl; intros. inv H. tauto. simpl; intros. destruct (alloc_global m a) as [m1|] eqn:?; try discriminate. - erewrite alloc_global_perm; eauto. eapply IHgl; eauto. + erewrite alloc_global_perm; eauto. eapply IHgl; eauto. unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. apply Plt_trans_succ; auto. Qed. @@ -892,9 +892,9 @@ Remark store_zeros_load_outside: Proof. intros until n. functional induction (store_zeros m b p n); intros. inv H; auto. - transitivity (Mem.load chunk m' b' p'). - apply IHo. auto. intuition omega. - eapply Mem.load_store_other; eauto. simpl. intuition omega. + transitivity (Mem.load chunk m' b' p'). + apply IHo. auto. intuition omega. + eapply Mem.load_store_other; eauto. simpl. intuition omega. discriminate. Qed. @@ -907,15 +907,15 @@ Remark store_zeros_loadbytes_outside: Proof. intros until n. functional induction (store_zeros m b p n); intros. inv H; auto. - transitivity (Mem.loadbytes m' b' p' n'). + transitivity (Mem.loadbytes m' b' p' n'). apply IHo. auto. intuition omega. - eapply Mem.loadbytes_store_other; eauto. simpl. intuition omega. + eapply Mem.loadbytes_store_other; eauto. simpl. intuition omega. discriminate. Qed. Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := forall chunk p, - ofs <= p -> p + size_chunk chunk <= ofs + len -> + ofs <= p -> p + size_chunk chunk <= ofs + len -> (align_chunk chunk | p) -> Mem.load chunk m b p = Some (match chunk with @@ -938,18 +938,18 @@ Proof. rewrite inj_S in H1. omegaContradiction. - destruct (zeq p' p). + subst p'. destruct n'. simpl. apply Mem.loadbytes_empty. omega. - rewrite inj_S in H1. rewrite inj_S. + rewrite inj_S in H1. rewrite inj_S. replace (Z.succ (Z.of_nat n')) with (1 + Z.of_nat n') by omega. change (list_repeat (S n') (Byte Byte.zero)) with ((Byte Byte.zero :: nil) ++ list_repeat n' (Byte Byte.zero)). - apply Mem.loadbytes_concat. + apply Mem.loadbytes_concat. erewrite store_zeros_loadbytes_outside; eauto. change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). change 1 with (size_chunk Mint8unsigned). - eapply Mem.loadbytes_store_same; eauto. + eapply Mem.loadbytes_store_same; eauto. right; omega. - eapply IHo; eauto. omega. omega. omega. omega. - + eapply IHo; eauto. omega. omega. + eapply IHo; eauto. omega. omega. omega. omega. + + eapply IHo; eauto. omega. omega. - discriminate. Qed. @@ -960,9 +960,9 @@ Lemma store_zeros_read_as_zero: Proof. intros; red; intros. transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))). - apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. - eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. - f_equal. destruct chunk; reflexivity. + apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. + eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. + f_equal. destruct chunk; reflexivity. Qed. Remark store_init_data_outside: @@ -974,8 +974,8 @@ Remark store_init_data_outside: Proof. intros. destruct i; simpl in *; try (eapply Mem.load_store_other; eauto; fail). - inv H; auto. - destruct (find_symbol ge i); try congruence. + inv H; auto. + destruct (find_symbol ge i); try congruence. eapply Mem.load_store_other; eauto; intuition. Qed. @@ -991,7 +991,7 @@ Proof. intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. transitivity (Mem.load chunk m1 b' q). eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega. - eapply store_init_data_outside; eauto. tauto. + eapply store_init_data_outside; eauto. tauto. Qed. Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop := @@ -1041,17 +1041,17 @@ Proof. Mem.load chunk m' b p = Some(Val.load_result chunk v)). { intros. transitivity (Mem.load chunk m1 b p). - eapply store_init_data_list_outside; eauto. right. omega. - eapply Mem.load_store_same; eauto. + eapply store_init_data_list_outside; eauto. right. omega. + eapply Mem.load_store_same; eauto. } induction il; simpl. auto. intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. exploit IHil; eauto. - red; intros. transitivity (Mem.load chunk m b p0). - eapply store_init_data_outside. eauto. auto. - apply H0. generalize (init_data_size_pos a); omega. omega. auto. - intro D. + red; intros. transitivity (Mem.load chunk m b p0). + eapply store_init_data_outside. eauto. auto. + apply H0. generalize (init_data_size_pos a); omega. omega. auto. + intro D. destruct a; simpl in Heqo; intuition. eapply (A Mint8unsigned (Vint i)); eauto. eapply (A Mint16unsigned (Vint i)); eauto. @@ -1059,11 +1059,11 @@ Proof. eapply (A Mint64 (Vlong i)); eauto. eapply (A Mfloat32 (Vsingle f)); eauto. eapply (A Mfloat64 (Vfloat f)); eauto. - inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0). - eapply store_init_data_list_outside; eauto. right. simpl. xomega. + inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0). + eapply store_init_data_list_outside; eauto. right. simpl. xomega. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. - destruct (find_symbol ge i); try congruence. exists b0; split; auto. - eapply (A Mint32 (Vptr b0 i0)); eauto. + destruct (find_symbol ge i); try congruence. exists b0; split; auto. + eapply (A Mint32 (Vptr b0 i0)); eauto. Qed. Remark load_alloc_global: @@ -1074,10 +1074,10 @@ Remark load_alloc_global: Proof. intros. destruct g as [f|v]; simpl in H. (* function *) - destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. + destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. - transitivity (Mem.load chunk m1 b p). - eapply Mem.load_drop; eauto. + transitivity (Mem.load chunk m1 b p). + eapply Mem.load_drop; eauto. eapply Mem.load_alloc_unchanged; eauto. (* variable *) set (init := gvar_init v) in *. @@ -1086,10 +1086,10 @@ Proof. destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate. destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate. assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. - transitivity (Mem.load chunk m3 b p). + transitivity (Mem.load chunk m3 b p). eapply Mem.load_drop; eauto. transitivity (Mem.load chunk m2 b p). - eapply store_init_data_list_outside; eauto. + eapply store_init_data_list_outside; eauto. transitivity (Mem.load chunk m1 b p). eapply store_zeros_load_outside; eauto. eapply Mem.load_alloc_unchanged; eauto. @@ -1104,11 +1104,11 @@ Proof. induction gl; simpl; intros. congruence. destruct (alloc_global m a) as [m''|] eqn:?; try discriminate. - transitivity (Mem.load chunk m'' b p). - apply IHgl; auto. unfold Mem.valid_block in *. - erewrite alloc_global_nextblock; eauto. + transitivity (Mem.load chunk m'' b p). + apply IHgl; auto. unfold Mem.valid_block in *. + erewrite alloc_global_nextblock; eauto. apply Plt_trans with (Mem.nextblock m); auto. apply Plt_succ. - destruct a as [id g]. eapply load_alloc_global; eauto. + destruct a as [id g]. eapply load_alloc_global; eauto. Qed. Remark load_store_init_data_invariant: @@ -1119,7 +1119,7 @@ Remark load_store_init_data_invariant: Proof. induction il; intro p; simpl. auto. - repeat rewrite H. destruct a; intuition. red; intros; rewrite H; auto. + repeat rewrite H. destruct a; intuition. red; intros; rewrite H; auto. Qed. Definition variables_initialized (g: t) (m: mem) := @@ -1146,19 +1146,19 @@ Lemma alloc_global_initialized: /\ functions_initialized (add_global ge (id, g)) m' /\ genv_next (add_global ge (id, g)) = Mem.nextblock m'. Proof. - intros. + intros. exploit alloc_global_nextblock; eauto. intros NB. split. (* variables-initialized *) destruct g as [f|v]. (* function *) - red; intros. unfold find_var_info in H3. simpl in H3. + red; intros. unfold find_var_info in H3. simpl in H3. exploit H1; eauto. intros [A [B C]]. - assert (D: Mem.valid_block m b). + assert (D: Mem.valid_block m b). red. exploit genv_vars_range; eauto. rewrite H; auto. - split. red; intros. erewrite <- alloc_global_perm; eauto. - split. intros. eapply B. erewrite alloc_global_perm; eauto. - intros. apply load_store_init_data_invariant with m; auto. - intros. eapply load_alloc_global; eauto. + split. red; intros. erewrite <- alloc_global_perm; eauto. + split. intros. eapply B. erewrite alloc_global_perm; eauto. + intros. apply load_store_init_data_invariant with m; auto. + intros. eapply load_alloc_global; eauto. (* variable *) red; intros. unfold find_var_info in H3. simpl in H3. rewrite PTree.gsspec in H3. destruct (peq b (genv_next ge0)). @@ -1169,29 +1169,29 @@ Proof. destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?. destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate. destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate. - exploit Mem.alloc_result; eauto. intro RES. + exploit Mem.alloc_result; eauto. intro RES. replace (genv_next ge0) with b' by congruence. split. red; intros. eapply Mem.perm_drop_1; eauto. split. intros. assert (0 <= ofs < sz). eapply Mem.perm_alloc_3; eauto. erewrite store_zeros_perm; [idtac|eauto]. - erewrite store_init_data_list_perm; [idtac|eauto]. + erewrite store_init_data_list_perm; [idtac|eauto]. eapply Mem.perm_drop_4; eauto. split. auto. eapply Mem.perm_drop_2; eauto. - intros. apply load_store_init_data_invariant with m3. - intros. eapply Mem.load_drop; eauto. - right; right; right. unfold perm_globvar. rewrite H3. + intros. apply load_store_init_data_invariant with m3. + intros. eapply Mem.load_drop; eauto. + right; right; right. unfold perm_globvar. rewrite H3. destruct (gvar_readonly gv); auto with mem. eapply store_init_data_list_charact; eauto. - eapply store_zeros_read_as_zero; eauto. + eapply store_zeros_read_as_zero; eauto. (* older var *) exploit H1; eauto. intros [A [B C]]. - assert (D: Mem.valid_block m b). - red. exploit genv_vars_range; eauto. rewrite H; auto. - split. red; intros. erewrite <- alloc_global_perm; eauto. - split. intros. eapply B. erewrite alloc_global_perm; eauto. - intros. apply load_store_init_data_invariant with m; auto. + assert (D: Mem.valid_block m b). + red. exploit genv_vars_range; eauto. rewrite H; auto. + split. red; intros. erewrite <- alloc_global_perm; eauto. + split. intros. eapply B. erewrite alloc_global_perm; eauto. + intros. apply load_store_init_data_invariant with m; auto. intros. eapply load_alloc_global; eauto. (* functions-initialized *) split. destruct g as [f|v]. @@ -1199,11 +1199,11 @@ Proof. red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite PTree.gsspec in H3. destruct (peq b (genv_next ge0)). (* same *) - inv H3. simpl in H0. - destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. - exploit Mem.alloc_result; eauto. intro RES. + inv H3. simpl in H0. + destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. + exploit Mem.alloc_result; eauto. intro RES. replace (genv_next ge0) with b' by congruence. - split. eapply Mem.perm_drop_1; eauto. omega. + split. eapply Mem.perm_drop_1; eauto. omega. intros. assert (0 <= ofs < 1). eapply Mem.perm_alloc_3; eauto. @@ -1211,16 +1211,16 @@ Proof. split. omega. eapply Mem.perm_drop_2; eauto. (* older function *) exploit H2; eauto. intros [A B]. - assert (D: Mem.valid_block m b). + assert (D: Mem.valid_block m b). red. exploit genv_funs_range; eauto. rewrite H; auto. - split. erewrite <- alloc_global_perm; eauto. + split. erewrite <- alloc_global_perm; eauto. intros. eapply B. erewrite alloc_global_perm; eauto. (* variables *) - red; intros. unfold find_funct_ptr in H3. simpl in H3. + red; intros. unfold find_funct_ptr in H3. simpl in H3. exploit H2; eauto. intros [A B]. - assert (D: Mem.valid_block m b). + assert (D: Mem.valid_block m b). red. exploit genv_funs_range; eauto. rewrite H; auto. - split. erewrite <- alloc_global_perm; eauto. + split. erewrite <- alloc_global_perm; eauto. intros. eapply B. erewrite alloc_global_perm; eauto. (* nextblock *) rewrite NB. simpl. rewrite H. auto. @@ -1238,7 +1238,7 @@ Proof. inv H0; auto. destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|] eqn:?; try discriminate. exploit alloc_global_initialized; eauto. intros [P [Q R]]. - eapply IHgl; eauto. + eapply IHgl; eauto. Qed. End INITMEM. @@ -1247,12 +1247,12 @@ Definition init_mem (p: program F V) := alloc_globals (globalenv p) Mem.empty p.(prog_defs). Lemma init_mem_genv_next: forall p m, - init_mem p = Some m -> + init_mem p = Some m -> genv_next (globalenv p) = Mem.nextblock m. Proof. unfold init_mem; intros. exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))). + generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))). fold (globalenv p). simpl genv_next. intros. congruence. Qed. @@ -1261,7 +1261,7 @@ Theorem find_symbol_not_fresh: init_mem p = Some m -> find_symbol (globalenv p) id = Some b -> Mem.valid_block m b. Proof. - intros. red. erewrite <- init_mem_genv_next; eauto. + intros. red. erewrite <- init_mem_genv_next; eauto. eapply genv_symb_range; eauto. Qed. @@ -1270,7 +1270,7 @@ Theorem find_funct_ptr_not_fresh: init_mem p = Some m -> find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b. Proof. - intros. red. erewrite <- init_mem_genv_next; eauto. + intros. red. erewrite <- init_mem_genv_next; eauto. eapply genv_funs_range; eauto. Qed. @@ -1279,7 +1279,7 @@ Theorem find_var_info_not_fresh: init_mem p = Some m -> find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b. Proof. - intros. red. erewrite <- init_mem_genv_next; eauto. + intros. red. erewrite <- init_mem_genv_next; eauto. eapply genv_vars_range; eauto. Qed. @@ -1293,7 +1293,7 @@ Theorem init_mem_characterization: /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)). Proof. intros. eapply alloc_globals_initialized; eauto. - rewrite Mem.nextblock_empty. auto. + rewrite Mem.nextblock_empty. auto. red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. Qed. @@ -1328,7 +1328,7 @@ Lemma store_zeros_neutral: Proof. intros until n. functional induction (store_zeros m b p n); intros. inv H1; auto. - apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor. + apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor. inv H1. Qed. @@ -1343,9 +1343,9 @@ Proof. destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail). congruence. destruct (find_symbol ge i) as [b'|] eqn:E; try discriminate. - eapply Mem.store_inject_neutral; eauto. - econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto. - rewrite Int.add_zero. auto. + eapply Mem.store_inject_neutral; eauto. + econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto. + rewrite Int.add_zero. auto. Qed. Lemma store_init_data_list_neutral: @@ -1358,7 +1358,7 @@ Proof. induction idl; simpl; intros. congruence. destruct (store_init_data ge m b p a) as [m1|] eqn:E; try discriminate. - eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. + eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. Qed. Lemma alloc_global_neutral: @@ -1372,7 +1372,7 @@ Proof. (* function *) destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. - eapply Mem.drop_inject_neutral; eauto. + eapply Mem.drop_inject_neutral; eauto. eapply Mem.alloc_inject_neutral; eauto. (* variable *) set (init := gvar_init v) in *. @@ -1381,9 +1381,9 @@ Proof. destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate. destruct (store_init_data_list ge m2 b 0 init) as [m3|] eqn:?; try discriminate. assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. - eapply Mem.drop_inject_neutral; eauto. + eapply Mem.drop_inject_neutral; eauto. eapply store_init_data_list_neutral with (m := m2) (b := b); eauto. - eapply store_zeros_neutral with (m := m1); eauto. + eapply store_zeros_neutral with (m := m1); eauto. eapply Mem.alloc_inject_neutral; eauto. Qed. @@ -1403,7 +1403,7 @@ Lemma alloc_globals_neutral: Proof. induction gl; intros. simpl in *. congruence. - exploit alloc_globals_nextblock; eauto. intros EQ. + exploit alloc_globals_nextblock; eauto. intros EQ. simpl in *. destruct (alloc_global ge m a) as [m1|] eqn:E; try discriminate. exploit alloc_global_neutral; eauto. assert (Ple (Psucc (Mem.nextblock m)) (Mem.nextblock m')). @@ -1419,14 +1419,14 @@ Theorem initmem_inject: Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m. Proof. unfold init_mem; intros. - apply Mem.neutral_inject. - eapply alloc_globals_neutral; eauto. + apply Mem.neutral_inject. + eapply alloc_globals_neutral; eauto. intros. exploit find_symbol_not_fresh; eauto. apply Mem.empty_inject_neutral. apply Ple_refl. Qed. -Section INITMEM_AUGMENT_INJ. +Section INITMEM_AUGMENT_INJ. Variable ge: t. Variable thr: block. @@ -1440,58 +1440,58 @@ Lemma store_zeros_augment: Proof. intros until n. functional induction (store_zeros m2 b p n); intros. inv H1; auto. - apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. - intros. exfalso. unfold Mem.flat_inj in H2. destruct (plt b' thr). + apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. + intros. exfalso. unfold Mem.flat_inj in H2. destruct (plt b' thr). inv H2. unfold Plt, Ple in *. zify; omega. discriminate. discriminate. Qed. -Lemma store_init_data_augment: - forall m1 m2 b p id m2', - Mem.inject (Mem.flat_inj thr) m1 m2 -> - Ple thr b -> +Lemma store_init_data_augment: + forall m1 m2 b p id m2', + Mem.inject (Mem.flat_inj thr) m1 m2 -> + Ple thr b -> store_init_data ge m2 b p id = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2'. -Proof. - intros until m2'. intros INJ BND ST. - assert (P: forall chunk ofs v m2', - Mem.store chunk m2 b ofs v = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2'). - intros. eapply Mem.store_outside_inject; eauto. +Proof. + intros until m2'. intros INJ BND ST. + assert (P: forall chunk ofs v m2', + Mem.store chunk m2 b ofs v = Some m2' -> + Mem.inject (Mem.flat_inj thr) m1 m2'). + intros. eapply Mem.store_outside_inject; eauto. intros. unfold Mem.flat_inj in H0. destruct (plt b' thr); inv H0. unfold Plt, Ple in *. zify; omega. destruct id; simpl in ST; try (eapply P; eauto; fail). congruence. - revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. + revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. Qed. Lemma store_init_data_list_augment: - forall b idl m1 m2 p m2', - Mem.inject (Mem.flat_inj thr) m1 m2 -> - Ple thr b -> + forall b idl m1 m2 p m2', + Mem.inject (Mem.flat_inj thr) m1 m2 -> + Ple thr b -> store_init_data_list ge m2 b p idl = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2'. -Proof. +Proof. induction idl; simpl. intros; congruence. intros until m2'; intros INJ FB. - caseEq (store_init_data ge m2 b p a); try congruence. intros. - eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. + caseEq (store_init_data ge m2 b p a); try congruence. intros. + eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. Qed. Lemma alloc_global_augment: forall idg m1 m2 m2', alloc_global ge m2 idg = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2 -> - Ple thr (Mem.nextblock m2) -> + Mem.inject (Mem.flat_inj thr) m1 m2 -> + Ple thr (Mem.nextblock m2) -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. intros. destruct idg as [id [f|v]]; simpl in H. (* function *) destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?. assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. - eapply Mem.drop_outside_inject. 2: eauto. + eapply Mem.drop_outside_inject. 2: eauto. eapply Mem.alloc_right_inject; eauto. intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3. unfold Plt, Ple in *. zify; omega. @@ -1502,7 +1502,7 @@ Proof. destruct (store_zeros m3 b 0 sz) as [m4|] eqn:?; try discriminate. destruct (store_init_data_list ge m4 b 0 init) as [m5|] eqn:?; try discriminate. assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. - eapply Mem.drop_outside_inject. 2: eauto. + eapply Mem.drop_outside_inject. 2: eauto. eapply store_init_data_list_augment. 3: eauto. 2: eauto. eapply store_zeros_augment. 3: eauto. 2: eauto. eapply Mem.alloc_right_inject; eauto. @@ -1520,13 +1520,13 @@ Proof. induction gl; simpl. intros. congruence. intros until m2'. caseEq (alloc_global ge m2 a); try congruence. intros. - eapply IHgl with (m2 := m); eauto. - eapply alloc_global_augment; eauto. - rewrite (alloc_global_nextblock _ _ _ H). + eapply IHgl with (m2 := m); eauto. + eapply alloc_global_augment; eauto. + rewrite (alloc_global_nextblock _ _ _ H). apply Ple_trans with (Mem.nextblock m2); auto. apply Ple_succ. Qed. -End INITMEM_AUGMENT_INJ. +End INITMEM_AUGMENT_INJ. End GENV. @@ -1545,7 +1545,7 @@ Inductive match_globvar: globvar V -> globvar W -> Prop := match_varinfo info1 info2 -> match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo). -Record match_genvs (new_globs : list (ident * globdef B W)) +Record match_genvs (new_globs : list (ident * globdef B W)) (ge1: t A V) (ge2: t B W): Prop := { mge_next: genv_next ge2 = advance_next new_globs (genv_next ge1); @@ -1557,9 +1557,9 @@ Record match_genvs (new_globs : list (ident * globdef B W)) exists tf, PTree.get b (genv_funs ge2) = Some tf /\ match_fun f tf; mge_rev_funs: forall b tf, PTree.get b (genv_funs ge2) = Some tf -> - if plt b (genv_next ge1) then + if plt b (genv_next ge1) then exists f, PTree.get b (genv_funs ge1) = Some f /\ match_fun f tf - else + else In (Gfun tf) (map snd new_globs); mge_vars: forall b v, PTree.get b (genv_vars ge1) = Some v -> @@ -1583,43 +1583,43 @@ Proof. (* two functions *) constructor; simpl. congruence. - intros. rewrite mge_next0. + intros. rewrite mge_next0. repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. - destruct (peq b (genv_next ge1)). + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + destruct (peq b (genv_next ge1)). exists f2; split; congruence. eauto. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. - destruct (peq b (genv_next ge1)). + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + destruct (peq b (genv_next ge1)). subst b. rewrite pred_dec_true. exists f1; split; congruence. apply Plt_succ. - pose proof (mge_rev_funs0 b tf H0). + pose proof (mge_rev_funs0 b tf H0). destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. contradiction. eauto. intros. - pose proof (mge_rev_vars0 b tv H0). + pose proof (mge_rev_vars0 b tv H0). destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans with (genv_next ge1); auto. apply Plt_succ. contradiction. (* two variables *) constructor; simpl. congruence. - intros. rewrite mge_next0. + intros. rewrite mge_next0. repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. eauto. intros. - pose proof (mge_rev_funs0 b tf H0). + pose proof (mge_rev_funs0 b tf H0). destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. contradiction. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. destruct (peq b (genv_next ge1)). - econstructor; split. eauto. inv H0. constructor; auto. + econstructor; split. eauto. inv H0. constructor; auto. eauto. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. - destruct (peq b (genv_next ge1)). + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + destruct (peq b (genv_next ge1)). subst b. rewrite pred_dec_true. econstructor; split. eauto. inv H0. constructor; auto. apply Plt_succ. - pose proof (mge_rev_vars0 b tv H0). + pose proof (mge_rev_vars0 b tv H0). destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. contradiction. Qed. @@ -1629,56 +1629,56 @@ Lemma add_globals_match: forall ge1 ge2, match_genvs nil ge1 ge2 -> match_genvs nil (add_globals ge1 gl1) (add_globals ge2 gl2). Proof. - induction 1; intros; simpl. + induction 1; intros; simpl. auto. apply IHlist_forall2. apply add_global_match; auto. Qed. -Lemma add_global_augment_match: +Lemma add_global_augment_match: forall new_globs ge1 ge2 idg, match_genvs new_globs ge1 ge2 -> match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg). Proof. - intros. destruct H. + intros. destruct H. assert (LE: Ple (genv_next ge1) (genv_next ge2)). { rewrite mge_next0; apply advance_next_le. } constructor; simpl. rewrite mge_next0. unfold advance_next. rewrite fold_left_app. simpl. auto. - intros. rewrite map_app in H. rewrite in_app in H. simpl in H. - destruct (peq id idg#1). subst. intuition. rewrite PTree.gso. - apply mge_symb0. intuition. auto. + intros. rewrite map_app in H. rewrite in_app in H. simpl in H. + destruct (peq id idg#1). subst. intuition. rewrite PTree.gso. + apply mge_symb0. intuition. auto. intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. rewrite PTree.gso. eauto. exploit genv_funs_range; eauto. intros. unfold Plt, Ple in *; zify; omega. intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. - rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). + rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence. subst b. unfold Plt, Ple in *; zify; omega. - exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. + exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. - exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. + exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. - rewrite PTree.gso. eauto. exploit genv_vars_range; eauto. + rewrite PTree.gso. eauto. exploit genv_vars_range; eauto. unfold Plt, Ple in *; zify; omega. intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. - exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. + exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. - rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). + rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence. subst b. unfold Plt, Ple in *; zify; omega. - exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. + exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. Qed. -Lemma add_globals_augment_match: +Lemma add_globals_augment_match: forall gl new_globs ge1 ge2, match_genvs new_globs ge1 ge2 -> match_genvs (new_globs ++ gl) ge1 (add_globals ge2 gl). Proof. - induction gl; simpl. - intros. rewrite app_nil_r. auto. + induction gl; simpl. + intros. rewrite app_nil_r. auto. intros. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass. apply IHgl. apply add_global_augment_match. auto. Qed. @@ -1688,15 +1688,15 @@ Variable new_main : ident. Variable p: program A V. Variable p': program B W. -Hypothesis progmatch: +Hypothesis progmatch: match_program match_fun match_varinfo new_globs new_main p p'. Lemma globalenvs_match: match_genvs new_globs (globalenv p) (globalenv p'). Proof. unfold globalenv. destruct progmatch as [[tglob [P Q]] R]. - rewrite Q. rewrite add_globals_app. - change new_globs with (nil ++ new_globs) at 1. + rewrite Q. rewrite add_globals_app. + change new_globs with (nil ++ new_globs) at 1. apply add_globals_augment_match. apply add_globals_match; auto. constructor; simpl; auto; intros; rewrite PTree.gempty in H; congruence. @@ -1712,9 +1712,9 @@ Proof (mge_funs globalenvs_match). Theorem find_funct_ptr_rev_match: forall (b : block) (tf : B), find_funct_ptr (globalenv p') b = Some tf -> - if plt b (genv_next (globalenv p)) then + if plt b (genv_next (globalenv p)) then exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf - else + else In (Gfun tf) (map snd new_globs). Proof (mge_rev_funs globalenvs_match). @@ -1723,8 +1723,8 @@ Theorem find_funct_match: find_funct (globalenv p) v = Some f -> exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf. Proof. - intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. - rewrite find_funct_find_funct_ptr in H. + intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. + rewrite find_funct_find_funct_ptr in H. rewrite find_funct_find_funct_ptr. apply find_funct_ptr_match. auto. Qed. @@ -1732,13 +1732,13 @@ Qed. Theorem find_funct_rev_match: forall (v : val) (tf : B), find_funct (globalenv p') v = Some tf -> - (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf) + (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf) \/ (In (Gfun tf) (map snd new_globs)). Proof. - intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. - rewrite find_funct_find_funct_ptr in H. + intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. + rewrite find_funct_find_funct_ptr in H. rewrite find_funct_find_funct_ptr. - apply find_funct_ptr_rev_match in H. + apply find_funct_ptr_rev_match in H. destruct (plt b (genv_next (globalenv p))); auto. Qed. @@ -1752,7 +1752,7 @@ Proof (mge_vars globalenvs_match). Theorem find_var_info_rev_match: forall (b : block) (tv : globvar W), find_var_info (globalenv p') b = Some tv -> - if plt b (genv_next (globalenv p)) then + if plt b (genv_next (globalenv p)) then exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv else In (Gvar tv) (map snd new_globs). @@ -1763,7 +1763,7 @@ Theorem find_symbol_match: ~In s (map fst new_globs) -> find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. - intros. destruct globalenvs_match. unfold find_symbol. auto. + intros. destruct globalenvs_match. unfold find_symbol. auto. Qed. Theorem public_symbol_match: @@ -1771,11 +1771,11 @@ Theorem public_symbol_match: ~In s (map fst new_globs) -> public_symbol (globalenv p') s = public_symbol (globalenv p) s. Proof. - intros. unfold public_symbol. rewrite find_symbol_match by auto. + intros. unfold public_symbol. rewrite find_symbol_match by auto. destruct (find_symbol (globalenv p) s); auto. - rewrite ! globalenv_public. - destruct progmatch as (P & Q & R). rewrite R. auto. -Qed. + rewrite ! globalenv_public. + destruct progmatch as (P & Q & R). rewrite R. auto. +Qed. Hypothesis new_ids_fresh: forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False. @@ -1787,47 +1787,47 @@ Lemma store_init_data_list_match: store_init_data_list (globalenv p) m b ofs idl = Some m' -> store_init_data_list (globalenv p') m b ofs idl = Some m'. Proof. - induction idl; simpl; intros. + induction idl; simpl; intros. auto. assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' -> store_init_data (globalenv p') m b ofs a = Some m'). destruct a; simpl; auto. rewrite find_symbol_match. auto. simpl in H. destruct (find_symbol (globalenv p) i) as [b'|] eqn:?; try discriminate. - red; intros. exploit find_symbol_inversion; eauto. - case_eq (store_init_data (globalenv p) m b ofs a); intros. - rewrite H1 in H. - pose proof (H0 _ H1). rewrite H2. auto. - rewrite H1 in H. inversion H. + red; intros. exploit find_symbol_inversion; eauto. + case_eq (store_init_data (globalenv p) m b ofs a); intros. + rewrite H1 in H. + pose proof (H0 _ H1). rewrite H2. auto. + rewrite H1 in H. inversion H. Qed. Lemma alloc_globals_match: forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 -> forall m m', - alloc_globals (globalenv p) m gl1 = Some m' -> + alloc_globals (globalenv p) m gl1 = Some m' -> alloc_globals (globalenv p') m gl2 = Some m'. Proof. induction 1; simpl; intros. auto. destruct (alloc_global (globalenv p) m a1) as [m1|] eqn:?; try discriminate. assert (alloc_global (globalenv p') m b1 = Some m1). - inv H; simpl in *. + inv H; simpl in *. auto. 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. destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|] eqn:?; try discriminate. - erewrite store_init_data_list_match; eauto. + erewrite store_init_data_list_match; eauto. rewrite H2. eauto. Qed. Theorem init_mem_match: - forall m, init_mem p = Some m -> + forall m, init_mem p = Some m -> init_mem p' = alloc_globals (globalenv p') m new_globs. Proof. unfold init_mem; intros. destruct progmatch as [[tglob [P Q]] R]. - rewrite Q. erewrite <- alloc_globals_app; eauto. - eapply alloc_globals_match; eauto. + rewrite Q. erewrite <- alloc_globals_app; eauto. + eapply alloc_globals_match; eauto. Qed. Theorem find_new_funct_ptr_match: @@ -1838,9 +1838,9 @@ Theorem find_new_funct_ptr_match: Proof. intros. destruct progmatch as [[tglob [P Q]] R]. - exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). - rewrite S in Q. rewrite <- app_ass in Q. - eapply find_funct_ptr_exists_2; eauto. + exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). + rewrite S in Q. rewrite <- app_ass in Q. + eapply find_funct_ptr_exists_2; eauto. Qed. Theorem find_new_var_match: @@ -1851,9 +1851,9 @@ Theorem find_new_var_match: Proof. intros. destruct progmatch as [[tglob [P Q]] R]. - exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). - rewrite S in Q. rewrite <- app_ass in Q. - eapply find_var_exists_2; eauto. + exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). + rewrite S in Q. rewrite <- app_ass in Q. + eapply find_var_exists_2; eauto. Qed. End MATCH_PROGRAMS. @@ -1889,8 +1889,8 @@ Theorem find_funct_ptr_transf_augment: exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. Proof. - intros. - exploit find_funct_ptr_match. eexact prog_match. eauto. + intros. + exploit find_funct_ptr_match. eexact prog_match. eauto. intros [tf [X Y]]. exists tf; auto. Qed. @@ -1899,10 +1899,10 @@ Theorem find_funct_ptr_rev_transf_augment: find_funct_ptr (globalenv p') b = Some tf -> if plt b (genv_next (globalenv p)) then (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf) - else + else In (Gfun tf) (map snd new_globs). Proof. - intros. + intros. exploit find_funct_ptr_rev_match; eauto. Qed. @@ -1912,18 +1912,18 @@ Theorem find_funct_transf_augment: exists f', find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Proof. - intros. - exploit find_funct_match. eexact prog_match. eauto. auto. + intros. + exploit find_funct_match. eexact prog_match. eauto. auto. Qed. -Theorem find_funct_rev_transf_augment: +Theorem find_funct_rev_transf_augment: forall (v: val) (tf: B), find_funct (globalenv p') v = Some tf -> (exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf) \/ In (Gfun tf) (map snd new_globs). Proof. - intros. - exploit find_funct_rev_match. eexact prog_match. eauto. auto. + intros. + exploit find_funct_rev_match. eexact prog_match. eauto. auto. Qed. Theorem find_var_info_transf_augment: @@ -1932,8 +1932,8 @@ Theorem find_var_info_transf_augment: exists v', find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'. Proof. - intros. - exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]]. + intros. + exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]]. exists tv; split; auto. inv Y. unfold transf_globvar; simpl. rewrite H0; simpl. auto. Qed. @@ -1946,23 +1946,23 @@ Theorem find_var_info_rev_transf_augment: else (In (Gvar v') (map snd new_globs)). Proof. - intros. + intros. exploit find_var_info_rev_match. eexact prog_match. eauto. destruct (plt b (genv_next (globalenv p))); auto. - intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. + intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. rewrite H0; simpl. auto. Qed. -Theorem find_symbol_transf_augment: - forall (s: ident), +Theorem find_symbol_transf_augment: + forall (s: ident), ~ In s (map fst new_globs) -> find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. intros. eapply find_symbol_match. eexact prog_match. auto. Qed. -Theorem public_symbol_transf_augment: - forall (s: ident), +Theorem public_symbol_transf_augment: + forall (s: ident), ~ In s (map fst new_globs) -> public_symbol (globalenv p') s = public_symbol (globalenv p) s. Proof. @@ -1974,38 +1974,38 @@ Hypothesis new_ids_fresh: Hypothesis new_ids_unique: list_norepet (map fst new_globs). -Theorem init_mem_transf_augment: - forall m, init_mem p = Some m -> +Theorem init_mem_transf_augment: + forall m, init_mem p = Some m -> init_mem p' = alloc_globals (globalenv p') m new_globs. Proof. intros. eapply init_mem_match. eexact prog_match. auto. auto. Qed. - + Theorem init_mem_inject_transf_augment: forall m, init_mem p = Some m -> - forall m', init_mem p' = Some m' -> + forall m', init_mem p' = Some m' -> Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'. Proof. - intros. - pose proof (initmem_inject p H). - erewrite init_mem_transf_augment in H0; eauto. - eapply alloc_globals_augment; eauto. apply Ple_refl. + intros. + pose proof (initmem_inject p H). + erewrite init_mem_transf_augment in H0; eauto. + eapply alloc_globals_augment; eauto. apply Ple_refl. Qed. -Theorem find_new_funct_ptr_exists: - forall id f, In (id, Gfun f) new_globs -> +Theorem find_new_funct_ptr_exists: + forall id f, In (id, Gfun f) new_globs -> exists b, find_symbol (globalenv p') id = Some b /\ find_funct_ptr (globalenv p') b = Some f. Proof. - intros. eapply find_new_funct_ptr_match; eauto. + intros. eapply find_new_funct_ptr_match; eauto. Qed. Theorem find_new_var_exists: - forall id gv, In (id, Gvar gv) new_globs -> + forall id gv, In (id, Gvar gv) new_globs -> exists b, find_symbol (globalenv p') id = Some b /\ find_var_info (globalenv p') b = Some gv. Proof. - intros. eapply find_new_var_match; eauto. + intros. eapply find_new_var_match; eauto. Qed. End TRANSF_PROGRAM_AUGMENT. @@ -2041,7 +2041,7 @@ Theorem find_funct_ptr_rev_transf_partial2: exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. Proof. pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). - intros. pose proof (H b tf H0). + intros. pose proof (H b tf H0). destruct (plt b (genv_next (globalenv p))). auto. contradiction. Qed. @@ -2060,7 +2060,7 @@ Theorem find_funct_rev_transf_partial2: exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf. Proof. pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). - intros. pose proof (H v tf H0). + intros. pose proof (H v tf H0). destruct H1. auto. contradiction. Qed. @@ -2080,7 +2080,7 @@ Theorem find_var_info_rev_transf_partial2: find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'. Proof. pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). - intros. pose proof (H b v' H0). + intros. pose proof (H b v' H0). destruct (plt b (genv_next (globalenv p))). auto. contradiction. Qed. @@ -2104,10 +2104,10 @@ Theorem block_is_volatile_transf_partial2: forall (b: block), block_is_volatile (globalenv p') b = block_is_volatile (globalenv p) b. Proof. - unfold block_is_volatile; intros. + unfold block_is_volatile; intros. destruct (find_var_info (globalenv p) b) as [v|] eqn:FV. exploit find_var_info_transf_partial2; eauto. intros (v' & P & Q). - rewrite P. monadInv Q. auto. + rewrite P. monadInv Q. auto. destruct (find_var_info (globalenv p') b) as [v'|] eqn:FV'. exploit find_var_info_rev_transf_partial2; eauto. intros (v & P & Q). congruence. auto. @@ -2117,7 +2117,7 @@ Theorem init_mem_transf_partial2: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). - intros. simpl in H. apply H; auto. + intros. simpl in H. apply H; auto. Qed. End TRANSF_PROGRAM_PARTIAL2. @@ -2183,11 +2183,11 @@ Theorem find_var_info_transf_partial: find_var_info (globalenv p') b = find_var_info (globalenv p) b. Proof. intros. case_eq (find_var_info (globalenv p) b); intros. - exploit find_var_info_transf_partial2. eexact transf_OK. eauto. - intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto. + exploit find_var_info_transf_partial2. eexact transf_OK. eauto. + intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto. case_eq (find_var_info (globalenv p') b); intros. exploit find_var_info_rev_transf_partial2. eexact transf_OK. eauto. - intros [v' [P Q]]. monadInv Q. inv EQ. congruence. + intros [v' [P Q]]. monadInv Q. inv EQ. congruence. auto. Qed. @@ -2216,7 +2216,7 @@ Let tp := transform_program transf p. Remark transf_OK: transform_partial_program (fun x => OK (transf x)) p = OK tp. Proof. - unfold tp. apply transform_program_partial_program. + unfold tp. apply transform_program_partial_program. Qed. Theorem find_funct_ptr_transf: @@ -2224,7 +2224,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. + intros. destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H) as [f' [X Y]]. congruence. Qed. @@ -2243,7 +2243,7 @@ Theorem find_funct_transf: find_funct (globalenv p) v = Some f -> find_funct (globalenv tp) v = Some (transf f). Proof. - intros. + intros. destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H) as [f' [X Y]]. congruence. Qed. -- cgit