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

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 *)