diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 10:05:18 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 10:05:18 +0100 |
commit | f00b70b6a17fdfb4e8606df891f6becc8102ef12 (patch) | |
tree | 1d4542a2b371d9e1d158a9ccfcade58b28cc9774 | |
parent | d594c5da5e11fb10775c2b772961b8a2383887c7 (diff) | |
download | compcert-f00b70b6a17fdfb4e8606df891f6becc8102ef12.tar.gz compcert-f00b70b6a17fdfb4e8606df891f6becc8102ef12.zip |
Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.
Instead of assuming name uniqueness for all definitions in the program,
these variants only assume uniqueness for a particular name.
Use this approach to weaken the hypotheses for match_program
and transf_program_partial_augment.
-rw-r--r-- | common/Globalenvs.v | 192 |
1 files changed, 122 insertions, 70 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index db212685..30f03654 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -321,20 +321,47 @@ Proof. apply IHgl; auto. Qed. +Lemma add_globals_unique_preserves: + forall id gl ge, + (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. + auto. + destruct a. apply IHgl; auto. +Qed. + +Lemma add_globals_unique_ensures: + forall gl1 id g gl2 ge, + (forall ge id1 g1, P ge -> In (id1, g1) gl2 -> id1 <> id -> P (add_global ge (id1, g1))) -> + (forall ge, P (add_global ge (id, g))) -> + ~In id (map fst gl2) -> P (add_globals ge (gl1 ++ (id, g) :: gl2)). +Proof. + intros. rewrite add_globals_app. simpl. apply add_globals_unique_preserves with id; auto. +Qed. + +Remark in_norepet_unique: + forall id g (gl: list (ident * globdef F V)), + In (id, g) gl -> list_norepet (map fst gl) -> + exists gl1 gl2, gl = gl1 ++ (id, g) :: gl2 /\ ~In id (map fst gl2). +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. +Qed. + Lemma add_globals_norepet_ensures: forall id g gl ge, (forall ge id1 g1, P ge -> In (id1, g1) gl -> id1 <> id -> P (add_global ge (id1, g1))) -> (forall ge, P (add_global ge (id, g))) -> In (id, g) gl -> list_norepet (map fst gl) -> P (add_globals ge gl). Proof. - induction gl; simpl; intros. - contradiction. - inv H2. - destruct H1. subst a. simpl in H5. - apply add_globals_preserves; auto. - intros. apply H. auto. auto. red; intros; subst id0. elim H5. - change id with (fst (id, g0)). apply List.in_map; auto. - apply IHgl; auto. + 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. End GLOBALENV_PRINCIPLES. @@ -387,15 +414,14 @@ Proof. intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto. Qed. -Theorem find_funct_ptr_exists: - forall p id f, - list_norepet (prog_defs_names p) -> - In (id, Gfun f) (prog_defs p) -> +Theorem find_funct_ptr_exists_2: + forall p gl1 id f gl2, + prog_defs p = gl1 ++ (id, Gfun f) :: gl2 -> ~In id (map fst gl2) -> exists b, find_symbol (globalenv p) id = Some b /\ find_funct_ptr (globalenv p) b = Some f. Proof. - intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto. + intros; unfold globalenv. rewrite H. eapply add_globals_unique_ensures; eauto. (* preserves *) intros. unfold find_symbol, find_funct_ptr in *; simpl. destruct H1 as [b [A B]]. exists b; split. @@ -408,15 +434,26 @@ Proof. exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. Qed. -Theorem find_var_exists: - forall p id v, +Corollary find_funct_ptr_exists: + forall p id f, list_norepet (prog_defs_names p) -> - In (id, Gvar v) (prog_defs p) -> + In (id, Gfun f) (prog_defs p) -> + exists b, + 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. +Qed. + +Theorem find_var_exists_2: + forall p gl1 id v gl2, + prog_defs p = gl1 ++ (id, Gvar v) :: gl2 -> ~In id (map fst gl2) -> exists b, find_symbol (globalenv p) id = Some b /\ find_var_info (globalenv p) b = Some v. Proof. - intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto. + intros; unfold globalenv. rewrite H. eapply add_globals_unique_ensures; eauto. (* preserves *) intros. unfold find_symbol, find_var_info in *; simpl. destruct H1 as [b [A B]]. exists b; split. @@ -428,6 +465,18 @@ Proof. exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. Qed. +Corollary find_var_exists: + forall p id v, + list_norepet (prog_defs_names p) -> + In (id, Gvar v) (prog_defs p) -> + exists b, + 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. +Qed. + Lemma find_symbol_inversion : forall p x b, find_symbol (globalenv p) x = Some b -> In x (prog_defs_names p). @@ -1728,9 +1777,10 @@ Proof. destruct progmatch as (P & Q & R). rewrite R. auto. Qed. -Hypothesis new_ids_fresh : - forall s', find_symbol (globalenv p) s' <> None -> - ~In s' (map fst new_globs). +Hypothesis new_ids_fresh: + forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False. +Hypothesis new_ids_unique: + list_norepet (map fst new_globs). Lemma store_init_data_list_match: forall idl m b ofs m', @@ -1743,7 +1793,7 @@ Proof. 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. - apply new_ids_fresh. congruence. + 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. @@ -1780,6 +1830,32 @@ Proof. eapply alloc_globals_match; eauto. Qed. +Theorem find_new_funct_ptr_match: + 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. + 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. +Qed. + +Theorem find_new_var_match: + forall id v, In (id, Gvar v) new_globs -> + exists b, + find_symbol (globalenv p') id = Some b + /\ find_var_info (globalenv p') b = Some v. +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. +Qed. + End MATCH_PROGRAMS. Section TRANSF_PROGRAM_AUGMENT. @@ -1797,7 +1873,7 @@ Variable p': program B W. Hypothesis transf_OK: transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'. -Remark prog_match: +Let prog_match: match_program (fun fd tfd => transf_fun fd = OK tfd) (fun info tinfo => transf_var info = OK tinfo) @@ -1818,27 +1894,6 @@ Proof. intros [tf [X Y]]. exists tf; auto. Qed. -Theorem find_new_funct_ptr_exists: - list_norepet (List.map fst new_globs) -> - 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. destruct prog_match as [[tglob [P Q]] R]. - unfold globalenv. rewrite Q. rewrite add_globals_app. - eapply add_globals_norepet_ensures; eauto. -(* preserves *) - intros. unfold find_symbol, find_funct_ptr in *; simpl. - destruct H1 as [b [X Y]]. exists b; split. - rewrite PTree.gso; auto. - destruct g1 as [f1 | v1]. rewrite PTree.gso. auto. - apply Plt_ne. eapply genv_funs_range; eauto. - auto. -(* ensures *) - intros. unfold find_symbol, find_funct_ptr in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. -Qed. - Theorem find_funct_ptr_rev_transf_augment: forall (b: block) (tf: B), find_funct_ptr (globalenv p') b = Some tf -> @@ -1848,7 +1903,7 @@ Theorem find_funct_ptr_rev_transf_augment: In (Gfun tf) (map snd new_globs). Proof. intros. - exploit find_funct_ptr_rev_match; eauto. eexact prog_match; eauto. auto. + exploit find_funct_ptr_rev_match; eauto. Qed. Theorem find_funct_transf_augment: @@ -1883,26 +1938,6 @@ Proof. rewrite H0; simpl. auto. Qed. -Theorem find_new_var_exists: - list_norepet (List.map fst 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. destruct prog_match as [[tglob [P Q]] R]. - unfold globalenv. rewrite Q. rewrite add_globals_app. - eapply add_globals_norepet_ensures; eauto. -(* preserves *) - intros. unfold find_symbol, find_var_info in *; simpl. - destruct H1 as [b [X Y]]. exists b; split. - rewrite PTree.gso; auto. - destruct g1 as [f1 | v1]. auto. rewrite PTree.gso. auto. - red; intros; subst b. eelim Plt_strict. 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. -Qed. - Theorem find_var_info_rev_transf_augment: forall (b: block) (v': globvar W), find_var_info (globalenv p') b = Some v' -> @@ -1934,9 +1969,12 @@ Proof. intros. eapply public_symbol_match. eexact prog_match. auto. Qed. +Hypothesis new_ids_fresh: + forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False. +Hypothesis new_ids_unique: + list_norepet (map fst new_globs). + Theorem init_mem_transf_augment: - (forall s', find_symbol (globalenv p) s' <> None -> - ~ In s' (map fst new_globs)) -> forall m, init_mem p = Some m -> init_mem p' = alloc_globals (globalenv p') m new_globs. Proof. @@ -1944,18 +1982,32 @@ Proof. Qed. Theorem init_mem_inject_transf_augment: - (forall s', find_symbol (globalenv p) s' <> None -> - ~ In s' (map fst new_globs)) -> 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 H0). - erewrite init_mem_transf_augment in H1; eauto. + 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 -> + 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. +Qed. + +Theorem find_new_var_exists: + 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. +Qed. + End TRANSF_PROGRAM_AUGMENT. Section TRANSF_PROGRAM_PARTIAL2. |