diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
commit | ce4951549999f403446415c135ad1403a16a15c3 (patch) | |
tree | cac9bbb2fea29fce331916b277c38ed8fe29e471 /backend/Inliningspec.v | |
parent | dcb9f48f51cec5e864565862a700c27df2a1a7e6 (diff) | |
download | compcert-ce4951549999f403446415c135ad1403a16a15c3.tar.gz compcert-ce4951549999f403446415c135ad1403a16a15c3.zip |
Globalenvs: allocate one-byte block with permissions Nonempty for each
function definition, so that comparisons between function pointers
are correctly defined.
AST, Globalenvs, and many other files:
represent programs as a list of (function or variable) definitions
instead of two lists, one for functions and the other for variables.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Inliningspec.v')
-rw-r--r-- | backend/Inliningspec.v | 51 |
1 files changed, 16 insertions, 35 deletions
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index ec722900..84bcdcd9 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -35,43 +35,30 @@ Definition fenv_compat (ge: genv) (fenv: funenv) : Prop := fenv!id = Some f -> Genv.find_symbol ge id = Some b -> Genv.find_funct_ptr ge b = Some (Internal f). -Remark add_fundef_compat: - forall ge fenv idf, +Remark add_globdef_compat: + forall ge fenv idg, fenv_compat ge fenv -> - fenv_compat (Genv.add_function ge idf) (Inlining.add_fundef fenv idf). + fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg). Proof. - intros. destruct idf as [id fd]. red; simpl; intros. + intros. destruct idg as [id gd]. red; simpl; intros. unfold Genv.find_symbol in H1; simpl in H1. unfold Genv.find_funct_ptr; simpl. rewrite PTree.gsspec in H1. destruct (peq id0 id). (* same *) - subst id0. inv H1. rewrite ZMap.gss. - destruct fd. destruct (should_inline id f0). - rewrite PTree.gss in H0. inv H0; auto. + subst id0. inv H1. destruct gd. destruct f0. + destruct (should_inline id f0). + rewrite PTree.gss in H0. rewrite ZMap.gss. inv H0; auto. + rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. (* different *) - rewrite ZMap.gso. eapply H; eauto. - destruct fd. destruct (should_inline id f0). + destruct gd. rewrite ZMap.gso. eapply H; eauto. + destruct f0. destruct (should_inline id f0). rewrite PTree.gso in H0; auto. rewrite PTree.gro in H0; auto. rewrite PTree.gro in H0; auto. - exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega. -Qed. - -Remark remove_vardef_compat: - forall ge fenv idv, - fenv_compat ge fenv -> - fenv_compat (Genv.add_variable ge idv) (Inlining.remove_vardef fenv idv). -Proof. - intros. destruct idv as [id vi]. red; simpl; intros. - unfold Genv.find_symbol in H1; simpl in H1. - unfold Genv.find_funct_ptr; simpl. - unfold remove_vardef in H0; simpl in H0. - rewrite PTree.gsspec in H1. rewrite PTree.grspec in H0. - unfold PTree.elt_eq in H0. destruct (peq id0 id). - discriminate. - eapply H; eauto. + exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega. + rewrite PTree.gro in H0; auto. eapply H; eauto. Qed. Lemma funenv_program_compat: @@ -79,17 +66,11 @@ Lemma funenv_program_compat: Proof. intros. unfold Genv.globalenv, funenv_program. - assert (forall funs ge fenv, - fenv_compat ge fenv -> - fenv_compat (Genv.add_functions ge funs) (fold_left add_fundef funs fenv)). - unfold Genv.add_functions. induction funs; simpl; intros. - auto. apply IHfuns. apply add_fundef_compat; auto. - assert (forall vars ge fenv, + assert (forall gl ge fenv, fenv_compat ge fenv -> - fenv_compat (Genv.add_variables ge vars) (fold_left remove_vardef vars fenv)). - unfold Genv.add_variables. induction vars; simpl; intros. - auto. apply IHvars. apply remove_vardef_compat; auto. - apply H0. apply H. red; intros. rewrite PTree.gempty in H1; discriminate. + fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)). + induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto. + apply H. red; intros. rewrite PTree.gempty in H0; discriminate. Qed. (** ** Soundness of the computed bounds over function resources *) |