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

2 files changed, 979 insertions, 1227 deletions

diff --git a/common/AST.v b/common/AST.v
index 6425cb0..ccc9dbf 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -118,44 +118,29 @@ Record globvar (V: Type) : Type := mkglobvar {
 }.
 
 (** Whole programs consist of:
-- a collection of function definitions (name and description);
-- the name of the ``main'' function that serves as entry point in the program;
-- a collection of global variable declarations (name and information).
+- a collection of global definitions (name and description);
+- the name of the ``main'' function that serves as entry point in the program.
 
+A global definition is either a global function or a global variable.
 The type of function descriptions and that of additional information
 for variables vary among the various intermediate languages and are
 taken as parameters to the [program] type.  The other parts of whole
 programs are common to all languages. *)
 
-Record program (F V: Type) : Type := mkprogram {
-  prog_funct: list (ident * F);
-  prog_main: ident;
-  prog_vars: list (ident * globvar V)
-}.
+Inductive globdef (F V: Type) : Type :=
+  | Gfun (f: F)
+  | Gvar (v: globvar V).
 
-Definition funct_names (F: Type) (fl: list (ident * F)) : list ident :=
-  map (@fst ident F) fl. 
+Implicit Arguments Gfun [F V].
+Implicit Arguments Gvar [F V].
 
-Lemma funct_names_app : forall (F: Type) (fl1 fl2 : list (ident * F)),
-  funct_names (fl1 ++ fl2) = funct_names fl1 ++ funct_names fl2. 
-Proof.
-  intros; unfold funct_names; apply list_append_map.
-Qed.
-  
-Definition var_names (V: Type) (vl: list (ident * globvar V)) : list ident :=
-  map (@fst ident (globvar V)) vl. 
-
-Lemma var_names_app : forall (V: Type) (vl1 vl2 : list (ident * globvar V)),
-  var_names (vl1 ++ vl2) = var_names vl1 ++ funct_names vl2. 
-Proof.
-  intros; unfold var_names; apply list_append_map.
-Qed.
-  
-Definition prog_funct_names (F V: Type) (p: program F V) : list ident :=
-  funct_names p.(prog_funct).
+Record program (F V: Type) : Type := mkprogram {
+  prog_defs: list (ident * globdef F V);
+  prog_main: ident
+}.
 
-Definition prog_var_names (F V: Type) (p: program F V) : list ident :=
-  var_names p.(prog_vars).
+Definition prog_defs_names (F V: Type) (p: program F V) : list ident :=
+  List.map fst p.(prog_defs).
 
 (** * Generic transformations over programs *)
 
@@ -168,253 +153,195 @@ Section TRANSF_PROGRAM.
 Variable A B V: Type.
 Variable transf: A -> B.
 
-Definition transf_program (l: list (ident * A)) : list (ident * B) :=
-  List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l.
+Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V :=
+  match idg with
+  | (id, Gfun f) => (id, Gfun (transf f))
+  | (id, Gvar v) => (id, Gvar v)
+  end.
 
 Definition transform_program (p: program A V) : program B V :=
   mkprogram
-    (transf_program p.(prog_funct))
-    p.(prog_main)
-    p.(prog_vars).
+    (List.map transform_program_globdef p.(prog_defs))
+    p.(prog_main).
 
 Lemma transform_program_function:
   forall p i tf,
-  In (i, tf) (transform_program p).(prog_funct) ->
-  exists f, In (i, f) p.(prog_funct) /\ transf f = tf.
+  In (i, Gfun tf) (transform_program p).(prog_defs) ->
+  exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf.
 Proof.
-  simpl. unfold transf_program. intros.
+  simpl. unfold transform_program. intros.
   exploit list_in_map_inv; eauto. 
-  intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst. 
-  exists f; split; auto.
+  intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. 
+  exists f; auto.
 Qed.
 
 End TRANSF_PROGRAM.
 
-(** The following is a variant of [transform_program] where the
-  code transformation function can fail and therefore returns an
-  option type. *)
+(** The following is a more general presentation of [transform_program] where 
+  global variable information can be transformed, in addition to function
+  definitions.  Moreover, the transformation functions can fail and
+  return an error message. *)
 
 Open Local Scope error_monad_scope.
 Open Local Scope string_scope.
 
-Section MAP_PARTIAL.
+Section TRANSF_PROGRAM_GEN.
 
-Variable A B C: Type.
-Variable prefix_errmsg: A -> errmsg.
-Variable f: B -> res C.
+Variables A B V W: Type.
+Variable transf_fun: A -> res B.
+Variable transf_var: V -> res W.
+
+Definition transf_globvar (g: globvar V) : res (globvar W) :=
+  do info' <- transf_var g.(gvar_info);
+  OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
 
-Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
+Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
   match l with
   | nil => OK nil
-  | (a, b) :: rem =>
-      match f b with
-      | Error msg => Error (prefix_errmsg a ++ msg)%list
-      | OK c =>
-          do rem' <- map_partial rem; 
-          OK ((a, c) :: rem')
+  | (id, Gfun f) :: l' =>
+      match transf_fun f with
+      | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
+      | OK tf =>
+          do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl')
+      end
+  | (id, Gvar v) :: l' =>
+      match transf_globvar v with
+      | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
+      | OK tv =>
+          do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl')
       end
   end.
 
-Remark In_map_partial:
-  forall l l' a c,
-  map_partial l = OK l' ->
-  In (a, c) l' ->
-  exists b, In (a, b) l /\ f b = OK c.
-Proof.
-  induction l; simpl.
-  intros. inv H. elim H0.
-  intros until c. destruct a as [a1 b1].
-  caseEq (f b1); try congruence.
-  intro c1; intros. monadInv H0. 
-  elim H1; intro. inv H0. exists b1; auto. 
-  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
-Qed.
+Definition transform_partial_program2 (p: program A V) : res (program B W) :=
+  do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)).
 
-Remark map_partial_forall2:
-  forall l l',
-  map_partial l = OK l' ->
-  list_forall2
-    (fun (a_b: A * B) (a_c: A * C) =>
-       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
-    l l'.
+Lemma transform_partial_program2_function:
+  forall p tp i tf,
+  transform_partial_program2 p = OK tp ->
+  In (i, Gfun tf) tp.(prog_defs) ->
+  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf.
 Proof.
-  induction l; simpl.
-  intros. inv H. constructor.
-  intro l'. destruct a as [a b].
-  caseEq (f b). 2: congruence. intro c; intros. monadInv H0.  
-  constructor. simpl. auto. auto. 
+  intros. monadInv H. simpl in H0. 
+  revert x EQ H0. induction (prog_defs p); simpl; intros.
+  inv EQ. contradiction.
+  destruct a as [id [f|v]].
+  destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ.
+  simpl in H0; destruct H0. inv H. exists f; auto. 
+  exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
+  destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ.
+  simpl in H0; destruct H0. inv H.
+  exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
 Qed.
 
-End MAP_PARTIAL.
-
-Remark map_partial_total:
-  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
-  map_partial prefix (fun b => OK (f b)) l =
-  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
+Lemma transform_partial_program2_variable:
+  forall p tp i tv,
+  transform_partial_program2 p = OK tp ->
+  In (i, Gvar tv) tp.(prog_defs) ->
+  exists v,
+     In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
+  /\ transf_var v = OK tv.(gvar_info).
 Proof.
-  induction l; simpl.
-  auto.
-  destruct a as [a1 b1]. rewrite IHl. reflexivity.
+  intros. monadInv H. simpl in H0. 
+  revert x EQ H0. induction (prog_defs p); simpl; intros.
+  inv EQ. contradiction.
+  destruct a as [id [f|v]].
+  destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ.
+  simpl in H0; destruct H0. inv H.
+  exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
+  destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ.
+  simpl in H0; destruct H0. inv H.
+  monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto.
+  exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
 Qed.
 
-Remark map_partial_identity:
-  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
-  map_partial prefix (fun b => OK b) l = OK l.
+Lemma transform_partial_program2_main:
+  forall p tp,
+  transform_partial_program2 p = OK tp ->
+  tp.(prog_main) = p.(prog_main).
 Proof.
-  induction l; simpl.
-  auto.
-  destruct a as [a1 b1]. rewrite IHl. reflexivity.
+  intros. monadInv H. reflexivity.
 Qed.
 
-Section TRANSF_PARTIAL_PROGRAM.
+(** Additionally, we can also "augment" the program with new global definitions
+  and a different "main" function. *)
 
-Variable A B V: Type.
-Variable transf_partial: A -> res B.
-
-Definition prefix_name (id: ident) : errmsg :=
-  MSG "In function " :: CTX id :: MSG ": " :: nil.
+Section AUGMENT.
 
-Definition transform_partial_program (p: program A V) : res (program B V) :=
-  do fl <- map_partial prefix_name transf_partial p.(prog_funct);
-  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
+Variable new_globs: list(ident * globdef B W).
+Variable new_main: ident.
 
-Lemma transform_partial_program_function:
-  forall p tp i tf,
-  transform_partial_program p = OK tp ->
-  In (i, tf) tp.(prog_funct) ->
-  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
-Proof.
-  intros. monadInv H. simpl in H0.  
-  eapply In_map_partial; eauto.
-Qed.
+Definition transform_partial_augment_program (p: program A V) : res (program B W) :=
+  do gl' <- transf_globdefs p.(prog_defs);
+  OK(mkprogram (gl' ++ new_globs) new_main).
 
-Lemma transform_partial_program_main:
+Lemma transform_partial_augment_program_main:
   forall p tp,
-  transform_partial_program p = OK tp ->
-  tp.(prog_main) = p.(prog_main).
+  transform_partial_augment_program p = OK tp ->
+  tp.(prog_main) = new_main.
 Proof.
   intros. monadInv H. reflexivity.
 Qed.
 
-Lemma transform_partial_program_vars:
-  forall p tp,
-  transform_partial_program p = OK tp ->
-  tp.(prog_vars) = p.(prog_vars).
+End AUGMENT.
+
+Remark transform_partial_program2_augment:
+  forall p,
+  transform_partial_program2 p =
+  transform_partial_augment_program nil p.(prog_main) p.
 Proof.
-  intros. monadInv H. reflexivity.
+  unfold transform_partial_program2, transform_partial_augment_program; intros.
+  destruct (transf_globdefs (prog_defs p)); auto.
+  simpl. f_equal. f_equal. rewrite <- app_nil_end. auto.
 Qed.
 
-End TRANSF_PARTIAL_PROGRAM.
+End TRANSF_PROGRAM_GEN.
 
-(** The following is a variant of [transform_program_partial] where
-  both the program functions and the additional variable information
-  are transformed by functions that can fail. *)
+(** The following is a special case of [transform_partial_program2],
+  where only function definitions are transformed, but not variable definitions. *)
 
-Section TRANSF_PARTIAL_PROGRAM2.
-
-Variable A B V W: Type.
-Variable transf_partial_function: A -> res B.
-Variable transf_partial_variable: V -> res W.
-
-Definition transf_globvar (g: globvar V) : res (globvar W) :=
-  do info' <- transf_partial_variable g.(gvar_info);
-  OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
-
-Definition transform_partial_program2 (p: program A V) : res (program B W) :=
-  do fl <- map_partial prefix_name transf_partial_function p.(prog_funct);
-  do vl <- map_partial prefix_name transf_globvar p.(prog_vars);
-  OK (mkprogram fl p.(prog_main) vl).
+Section TRANSF_PARTIAL_PROGRAM.
 
-Lemma transform_partial_program2_function:
-  forall p tp i tf,
-  transform_partial_program2 p = OK tp ->
-  In (i, tf) tp.(prog_funct) ->
-  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
-Proof.
-  intros. monadInv H.  
-  eapply In_map_partial; eauto. 
-Qed.
+Variable A B V: Type.
+Variable transf_partial: A -> res B.
 
-Lemma transform_partial_program2_variable:
-  forall p tp i tg,
-  transform_partial_program2 p = OK tp ->
-  In (i, tg) tp.(prog_vars) ->
-  exists v,
-     In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars)
-  /\ transf_partial_variable v = OK tg.(gvar_info).
-Proof.
-  intros. monadInv H. exploit In_map_partial; eauto. intros [g [P Q]].
-  monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto.
- Qed.
+Definition transform_partial_program (p: program A V) : res (program B V) :=
+  transform_partial_program2 transf_partial (fun v => OK v) p.
 
-Lemma transform_partial_program2_main:
+Lemma transform_partial_program_main:
   forall p tp,
-  transform_partial_program2 p = OK tp ->
+  transform_partial_program p = OK tp ->
   tp.(prog_main) = p.(prog_main).
 Proof.
-  intros. monadInv H. reflexivity.
+  apply transform_partial_program2_main.
 Qed.
 
-End TRANSF_PARTIAL_PROGRAM2.
-
-(** The following is a variant of [transform_partial_program2] where the
-     where the set of functions and global data is augmented, and
-     the main function is potentially changed. *)
-
-Section TRANSF_PARTIAL_AUGMENT_PROGRAM.
-
-Variable A B V W: Type.
-Variable transf_partial_function: A -> res B.
-Variable transf_partial_variable: V -> res W.
-
-Variable new_functs : list (ident * B).
-Variable new_vars : list (ident * globvar W).
-Variable new_main : ident.
-
-Definition transform_partial_augment_program (p: program A V) : res (program B W)  :=
-  do fl <- map_partial prefix_name transf_partial_function p.(prog_funct);
-  do vl <- map_partial prefix_name (transf_globvar transf_partial_variable) p.(prog_vars);
-  OK (mkprogram (fl ++ new_functs) new_main (vl ++ new_vars)).
-
-Lemma transform_partial_augment_program_function:
+Lemma transform_partial_program_function:
   forall p tp i tf,
-  transform_partial_augment_program p = OK tp ->
-  In (i, tf) tp.(prog_funct) ->
-  (exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf)
-  \/ In (i,tf) new_functs.
-Proof.
-  intros. monadInv H. simpl in H0.  
-  rewrite in_app in H0.  destruct H0. 
-  left. eapply In_map_partial; eauto.
-  right. auto. 
-Qed.
-
-Lemma transform_partial_augment_program_main:
-  forall p tp,
-  transform_partial_augment_program p = OK tp ->
-  tp.(prog_main) = new_main.
+  transform_partial_program p = OK tp ->
+  In (i, Gfun tf) tp.(prog_defs) ->
+  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf.
 Proof.
-  intros. monadInv H. reflexivity.
+  apply transform_partial_program2_function. 
 Qed.
 
+End TRANSF_PARTIAL_PROGRAM.
 
-Lemma transform_partial_augment_program_variable:
-  forall p tp i tg,
-  transform_partial_augment_program p = OK tp ->
-  In (i, tg) tp.(prog_vars) ->
-  (exists v, In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) /\ transf_partial_variable v = OK tg.(gvar_info))
-  \/ In (i,tg) new_vars.
+Lemma transform_program_partial_program:
+  forall (A B V: Type) (transf: A -> B) (p: program A V),
+  transform_partial_program (fun f => OK(transf f)) p = OK(transform_program transf p).
 Proof.
-  intros. monadInv H. 
-  simpl in H0.  rewrite in_app in H0.  inversion H0. 
-  left. exploit In_map_partial; eauto.  intros [g [P Q]]. 
-  monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto. 
-  right. auto.
+  intros.
+  unfold transform_partial_program, transform_partial_program2, transform_program; intros.
+  replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs))
+     with (OK (map (transform_program_globdef transf) p.(prog_defs))).
+  auto. 
+  induction (prog_defs p); simpl.
+  auto.
+  destruct a as [id [f|v]]; rewrite <- IHl.
+    auto.
+    destruct v; auto.
 Qed.
 
-End TRANSF_PARTIAL_AUGMENT_PROGRAM.
-
-
 (** The following is a relational presentation of 
   [transform_partial_augment_preogram].  Given relations between function
   definitions and between variable information, it defines a relation
@@ -429,61 +356,50 @@ Variable A B V W: Type.
 Variable match_fundef: A -> B -> Prop.
 Variable match_varinfo: V -> W -> Prop.
 
-Inductive match_funct_entry: ident * A -> ident * B -> Prop :=
-  | match_funct_entry_intro: forall id fn1 fn2,
-      match_fundef fn1 fn2 ->
-      match_funct_entry (id, fn1) (id, fn2).
-
-Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop :=
-  | match_var_entry_intro: forall id info1 info2 init ro vo,
+Inductive match_globdef: ident * globdef A V -> ident * globdef B W -> Prop :=
+  | match_glob_fun: forall id f1 f2,
+      match_fundef f1 f2 ->
+      match_globdef (id, Gfun f1) (id, Gfun f2)
+  | match_glob_var: forall id init ro vo info1 info2,
       match_varinfo info1 info2 ->
-      match_var_entry (id, mkglobvar info1 init ro vo)
-                      (id, mkglobvar info2 init ro vo).
+      match_globdef (id, Gvar (mkglobvar info1 init ro vo)) (id, Gvar (mkglobvar info2 init ro vo)).
 
-Definition match_program (new_functs : list (ident * B))
-                         (new_vars : list (ident * globvar W))
+Definition match_program (new_globs : list (ident * globdef B W))
                          (new_main : ident)
                          (p1: program A V)  (p2: program B W) : Prop :=
-  (exists tfuncts, list_forall2 match_funct_entry p1.(prog_funct) tfuncts /\
-                                (p2.(prog_funct) = tfuncts ++ new_functs)) /\
-  (exists tvars, list_forall2 match_var_entry p1.(prog_vars) tvars /\
-                                (p2.(prog_vars) = tvars ++ new_vars)) /\
+  (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\
+                 p2.(prog_defs) = tglob ++ new_globs) /\
   p2.(prog_main) = new_main.
 
 End MATCH_PROGRAM.
 
-Remark transform_partial_augment_program_match:
+Lemma transform_partial_augment_program_match:
   forall (A B V W: Type)
-         (transf_partial_function: A -> res B)
-         (transf_partial_variable : V -> res W)
+         (transf_fun: A -> res B)
+         (transf_var: V -> res W)
          (p: program A V) 
-         (new_functs : list (ident * B))
-         (new_vars : list (ident * globvar W))
+         (new_globs : list (ident * globdef B W))
          (new_main : ident)
          (tp: program B W),
-  transform_partial_augment_program transf_partial_function transf_partial_variable new_functs new_vars new_main p = OK tp ->
+  transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp ->
   match_program 
-    (fun fd tfd => transf_partial_function fd = OK tfd)
-    (fun info tinfo => transf_partial_variable info = OK tinfo)
-    new_functs new_vars new_main
+    (fun fd tfd => transf_fun fd = OK tfd)
+    (fun info tinfo => transf_var info = OK tinfo)
+    new_globs new_main
     p tp.
 Proof.
-  intros. unfold transform_partial_augment_program in H. monadInv H. split.
-  exists x. split. 
-  apply list_forall2_imply with
-    (fun (ab: ident * A) (ac: ident * B) =>
-       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
-  eapply map_partial_forall2. eauto. 
-  intros. destruct v1; destruct v2; simpl in *.
-  destruct H1; subst. constructor. auto. 
-  auto. 
-  split. exists x0.  split.
-  apply list_forall2_imply with
-    (fun (ab: ident * globvar V) (ac: ident * globvar W) =>
-       fst ab = fst ac /\ transf_globvar transf_partial_variable (snd ab) = OK (snd ac)).
-  eapply map_partial_forall2. eauto.
-  intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. 
-  monadInv H2. destruct g; simpl in *.  constructor. auto.  auto.  auto. 
+  unfold transform_partial_augment_program; intros. monadInv H. 
+  red; simpl. split; auto. exists x; split; auto.
+  revert x EQ. generalize (prog_defs p). induction l; simpl; intros.
+  monadInv EQ. constructor.
+  destruct a as [id [f|v]]. 
+  (* function *)
+  destruct (transf_fun f) as [tf|?]_eqn; monadInv EQ. 
+  constructor; auto. constructor; auto.
+  (* variable *)
+  unfold transf_globvar in EQ.
+  destruct (transf_var (gvar_info v)) as [tinfo|?]_eqn; simpl in EQ; monadInv EQ.
+  constructor; auto. destruct v; simpl in *. constructor; auto.
 Qed.
 
 (** * External functions *)
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index ba038f8..8565ae6 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -69,13 +69,13 @@ Record t: Type := mkgenv {
   genv_symb: PTree.t block;             (**r mapping symbol -> block *)
   genv_funs: ZMap.t (option F);         (**r mapping function pointer -> definition *)
   genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *)
-  genv_nextfun: block;                  (**r next function pointer *)
-  genv_nextvar: block;                  (**r next variable pointer *)
-  genv_nextfun_neg: genv_nextfun < 0;
-  genv_nextvar_pos: genv_nextvar > 0;
-  genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> b <> 0 /\ genv_nextfun < b /\ b < genv_nextvar;
-  genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> genv_nextfun < b < 0;
-  genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar;
+  genv_next: block;                     (**r next symbol pointer *)
+  genv_next_pos: genv_next > 0;
+  genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> 0 < b < genv_next;
+  genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> 0 < b < genv_next;
+  genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_next;
+  genv_funs_vars: forall b1 b2 f v,
+    ZMap.get b1 genv_funs = Some f -> ZMap.get b2 genv_vars = Some v -> b1 <> b2;
   genv_vars_inj: forall id1 id2 b, 
     PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
 }.
@@ -117,69 +117,53 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) :=
 
 (** ** Constructing the global environment *)
 
-Program Definition add_function (ge: t) (idf: ident * F) : t :=
+Program Definition add_global (ge: t) (idg: ident * globdef F V) : t :=
   @mkgenv
-    (PTree.set idf#1 ge.(genv_nextfun) ge.(genv_symb))
-    (ZMap.set ge.(genv_nextfun) (Some idf#2) ge.(genv_funs))
-    ge.(genv_vars)
-    (ge.(genv_nextfun) - 1)
-    ge.(genv_nextvar)
+    (PTree.set idg#1 ge.(genv_next) ge.(genv_symb))
+    (match idg#2 with
+     | Gfun f => ZMap.set ge.(genv_next) (Some f) ge.(genv_funs)
+     | Gvar v => ge.(genv_funs)
+     end)
+    (match idg#2 with
+     | Gfun f => ge.(genv_vars)
+     | Gvar v => ZMap.set ge.(genv_next) (Some v) ge.(genv_vars)
+     end)
+    (ge.(genv_next) + 1)
     _ _ _ _ _ _.
 Next Obligation.
   destruct ge; simpl; omega.
 Qed.
 Next Obligation.
-  destruct ge; auto.
-Qed.
-Next Obligation.
   destruct ge; simpl in *.
   rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega.
   exploit genv_symb_range0; eauto. unfold block; omega.
 Qed.
 Next Obligation.
-  destruct ge; simpl in *. rewrite ZMap.gsspec in H. 
-  destruct (ZIndexed.eq b genv_nextfun0). subst; omega. 
+  destruct ge; simpl in *. 
+  destruct g. 
+  rewrite ZMap.gsspec in H. 
+  destruct (ZIndexed.eq b genv_next0). subst; omega. 
+  exploit genv_funs_range0; eauto. omega.
   exploit genv_funs_range0; eauto. omega.
-Qed.
-Next Obligation.
-  destruct ge; eauto. 
 Qed.
 Next Obligation.
   destruct ge; simpl in *. 
-  rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. 
-  destruct (peq id1 i); destruct (peq id2 i).
-  congruence.
-  exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction.
-  exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction.
-  eauto.
-Qed.
-
-Program Definition add_variable (ge: t) (idv: ident * globvar V) : t :=
-  @mkgenv
-    (PTree.set idv#1 ge.(genv_nextvar) ge.(genv_symb))
-    ge.(genv_funs)
-    (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars))
-    ge.(genv_nextfun)
-    (ge.(genv_nextvar) + 1)
-    _ _ _ _ _ _.
-Next Obligation.
-  destruct ge; auto.
-Qed.
-Next Obligation.
-  destruct ge; simpl; omega.
-Qed.
-Next Obligation.
-  destruct ge; simpl in *.
-  rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega.
-  exploit genv_symb_range0; eauto. unfold block; omega.
-Qed.
-Next Obligation.
-  destruct ge; eauto. 
+  destruct g. 
+  exploit genv_vars_range0; eauto. omega.
+  rewrite ZMap.gsspec in H. 
+  destruct (ZIndexed.eq b genv_next0). subst; omega. 
+  exploit genv_vars_range0; eauto. omega.
 Qed.
 Next Obligation.
-  destruct ge; simpl in *. rewrite ZMap.gsspec in H. 
-  destruct (ZIndexed.eq b genv_nextvar0). subst; omega. 
-  exploit genv_vars_range0; eauto. omega.
+  destruct ge; simpl in *. destruct g.
+  rewrite ZMap.gsspec in H.
+  destruct (ZIndexed.eq b1 genv_next0). inv H. 
+  exploit genv_vars_range0; eauto. unfold ZIndexed.t; omega.
+  eauto.
+  rewrite ZMap.gsspec in H0.
+  destruct (ZIndexed.eq b2 genv_next0). inv H. 
+  exploit genv_funs_range0; eauto. unfold ZIndexed.t; omega.
+  eauto.
 Qed.
 Next Obligation.
   destruct ge; simpl in *. 
@@ -191,16 +175,26 @@ Next Obligation.
   eauto.
 Qed.
 
+Definition add_globals (ge: t) (gl: list (ident * globdef F V)) : t :=
+  List.fold_left add_global gl ge.
+
+Lemma add_globals_app:
+  forall gl2 gl1 ge,
+  add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2.
+Proof.
+  induction gl1; simpl; intros. auto. rewrite IHgl1; auto.
+Qed.
+
 Program Definition empty_genv : t :=
-  @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) (-1) 1 _ _ _ _ _ _.
+  @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) 1 _ _ _ _ _ _.
 Next Obligation.
   omega.
 Qed.
 Next Obligation.
-  omega.
+  rewrite PTree.gempty in H. discriminate.
 Qed.
 Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
+  rewrite ZMap.gi in H. discriminate.
 Qed.
 Next Obligation.
   rewrite ZMap.gi in H. discriminate.
@@ -212,27 +206,54 @@ Next Obligation.
   rewrite PTree.gempty in H. discriminate.
 Qed.
 
-Definition add_functions (ge: t) (fl: list (ident * F)) : t :=
-  List.fold_left add_function fl ge.
+Definition globalenv (p: program F V) :=
+  add_globals empty_genv p.(prog_defs).
 
-Lemma add_functions_app : forall ge fl1 fl2,
-  add_functions ge (fl1 ++ fl2) = add_functions (add_functions ge fl1) fl2.
-Proof. 
-  intros. unfold add_functions. rewrite fold_left_app. auto.
-Qed.
+(** Proof principles *)
 
+Section GLOBALENV_PRINCIPLES.
 
-Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t :=
-  List.fold_left add_variable vl ge.
+Variable P: t -> Prop.
 
-Lemma add_variables_app : forall ge vl1 vl2 ,
-  add_variables ge (vl1 ++ vl2) = add_variables (add_variables ge vl1) vl2.
-Proof. 
-  intros. unfold add_variables. rewrite fold_left_app. auto.
+Lemma add_globals_preserves:
+  forall gl ge,
+  (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. 
+  auto.
+  destruct a. apply IHgl; auto. 
 Qed.
 
-Definition globalenv (p: program F V) :=
-  add_variables (add_functions empty_genv p.(prog_funct)) p.(prog_vars).
+Lemma add_globals_ensures:
+  forall id g gl ge,
+  (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) ->
+  (forall ge, P (add_global ge (id, g))) ->
+  In (id, g) gl -> P (add_globals ge gl).
+Proof.
+  induction gl; simpl; intros.
+  contradiction.
+  destruct H1. subst a. apply add_globals_preserves; auto. 
+  apply IHgl; 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. 
+Qed.
+
+End GLOBALENV_PRINCIPLES.
 
 (** ** Properties of the operations over global environments *)
 
@@ -254,298 +275,132 @@ Proof.
 Qed.
 
 Theorem find_symbol_exists:
-  forall p id gv,
-  In (id, gv) (prog_vars p) ->
+  forall p id g,
+  In (id, g) (prog_defs p) ->
   exists b, find_symbol (globalenv p) id = Some b.
 Proof.
-  intros until gv.
-  assert (forall vl ge,
-          (exists b, find_symbol ge id = Some b) ->
-          exists b, find_symbol (add_variables ge vl) id = Some b).
-  unfold find_symbol; induction vl; simpl; intros. auto. apply IHvl.
-  simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1).
-  exists (genv_nextvar ge); auto. auto.
-
-  assert (forall vl ge, In (id, gv) vl ->
-          exists b, find_symbol (add_variables ge vl) id = Some b).
-  unfold find_symbol; induction vl; simpl; intros. contradiction.
-  destruct H0. apply H. subst; unfold find_symbol; simpl.
-  rewrite PTree.gss. exists (genv_nextvar ge); auto.
-  eauto.
+  intros. unfold globalenv. eapply add_globals_ensures; eauto.
+(* preserves *)
+  intros. unfold find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id0).
+  econstructor; eauto.
+  auto.
+(* ensures *)
+  intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto.
+Qed.
 
-  intros. unfold globalenv; eauto. 
+Theorem find_funct_ptr_exists:
+  forall p id f,
+  list_norepet (prog_defs_names 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; unfold globalenv. eapply add_globals_norepet_ensures; eauto.
+(* preserves *)
+  intros. unfold find_symbol, find_funct_ptr in *; simpl.
+  destruct H1 as [b [A B]]. exists b; split.
+  rewrite PTree.gso; auto.
+  destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. 
+  exploit genv_funs_range; eauto. unfold ZIndexed.t; omega.
+  auto. 
+(* ensures *)
+  intros. unfold find_symbol, find_funct_ptr in *; simpl.
+  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
 Qed.
 
 Theorem find_var_exists:
-  forall p id gv,
-  list_norepet (prog_var_names p) ->
-  In (id, gv) (prog_vars p) ->
+  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 gv.
-Proof.
-  intros until gv.
-  assert (forall vl ge,
-    ~In id (var_names vl) ->
-    (exists b, find_symbol ge id = Some b /\ find_var_info ge b = Some gv) ->
-    (exists b, find_symbol (add_variables ge vl) id = Some b
-           /\  find_var_info (add_variables ge vl) b = Some gv)).
-  induction vl; simpl; intros.
-  auto.
-  apply IHvl. tauto. destruct a as [id1 gv1]. destruct H0 as [b [P Q]].
-  unfold add_variable, find_symbol, find_var_info; simpl. 
-  exists b; split. rewrite PTree.gso. auto. intuition. 
-  rewrite ZMap.gso. auto. exploit genv_vars_range; eauto.
-  unfold ZIndexed.t; omega.
-
-  unfold globalenv, prog_var_names.
-  generalize (prog_vars p) (add_functions empty_genv (prog_funct p)).
-  induction l; simpl; intros.
-  contradiction.
-  destruct a as [id1 gv1]; simpl in *. inv H0.
-  destruct H1. inv H0.
-  apply H; auto.
-  exists (genv_nextvar t0); split.
-  unfold find_symbol, add_variable; simpl. apply PTree.gss.
-  unfold find_var_info, add_variable; simpl. apply ZMap.gss.
-  apply IHl; auto. 
-Qed.  
-
-Remark add_variables_inversion : forall vs e x b,
-  find_symbol (add_variables e vs) x = Some b ->
-  In x (var_names vs) \/ find_symbol e x = Some b. 
-Proof.
-  induction vs; intros. 
-    simpl in H.  intuition.
-    simpl in H. destruct (IHvs _ _ _ H).
-       left. simpl. intuition.
-       destruct a as [y ?]. 
-       unfold add_variable, find_symbol in H0. simpl in H0. 
-       rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition.
-Qed.
-
-Remark add_functions_inversion : forall fs e x b,
-  find_symbol (add_functions e fs) x = Some b -> 
-  In x (funct_names fs) \/ find_symbol e x = Some b. 
-Proof.
-  induction fs; intros. 
-    simpl in H.  intuition.
-    simpl in H. destruct (IHfs _ _ _ H).
-       left. simpl. intuition.
-       destruct a as [y ?]. 
-       unfold add_variable, find_symbol in H0. simpl in H0. 
-       rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition.
+  /\ find_var_info (globalenv p) b = Some v.
+Proof.
+  intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto.
+(* preserves *)
+  intros. unfold find_symbol, find_var_info in *; simpl.
+  destruct H1 as [b [A B]]. exists b; split.
+  rewrite PTree.gso; auto.
+  destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. 
+  exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
+(* ensures *)
+  intros. unfold find_symbol, find_var_info in *; simpl.
+  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
 Qed.
 
 Lemma find_symbol_inversion : forall p x b,
   find_symbol (globalenv p) x = Some b ->
-  In x (prog_var_names p ++ prog_funct_names p). 
-Proof.
- unfold prog_var_names, prog_funct_names, globalenv. 
- intros.
- apply in_app.
- apply add_variables_inversion in H. intuition.
- apply add_functions_inversion in H0. inversion H0. intuition. 
- unfold find_symbol in H. 
- rewrite PTree.gempty in H. inversion H.
-Qed.
- 
-
-Remark add_functions_same_symb:
-  forall id fl ge, 
-  ~In id (funct_names fl) ->
-  find_symbol (add_functions ge fl) id = find_symbol ge id.
-Proof.
-  induction fl; simpl; intros. auto. 
-  rewrite IHfl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition.
-Qed.
-
-Remark add_functions_same_address:
-  forall b fl ge,
-  b > ge.(genv_nextfun) ->
-  find_funct_ptr (add_functions ge fl) b = find_funct_ptr ge b.
-Proof.
-  induction fl; simpl; intros. auto. 
-  rewrite IHfl. unfold find_funct_ptr; simpl. apply ZMap.gso. 
-  red; intros; subst b; omegaContradiction.
-  simpl. omega. 
-Qed.
-
-Remark add_variables_same_symb:
-  forall id vl ge, 
-  ~In id (var_names vl) -> 
-  find_symbol (add_variables ge vl) id = find_symbol ge id.
+  In x (prog_defs_names p).
 Proof.
-  induction vl; simpl; intros. auto. 
-  rewrite IHvl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition.
-Qed.
-
-Remark add_variables_same_address:
-  forall b vl ge,
-  b < ge.(genv_nextvar) ->
-  find_var_info (add_variables ge vl) b = find_var_info ge b.
-Proof.
-  induction vl; simpl; intros. auto. 
-  rewrite IHvl. unfold find_var_info; simpl. apply ZMap.gso. 
-  red; intros; subst b; omegaContradiction.
-  simpl. omega. 
-Qed.
-
-Remark add_variables_same_funs:
-  forall b vl ge, find_funct_ptr (add_variables ge vl) b = find_funct_ptr ge b.
-Proof.
-  induction vl; simpl; intros. auto. rewrite IHvl. auto.
+  intros until b; unfold globalenv. eapply add_globals_preserves.
+(* preserves *)
+  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 *)
+  unfold find_symbol; simpl; intros. rewrite PTree.gempty in H. discriminate.
 Qed.
 
-Remark add_functions_nextvar:
-  forall fl ge, genv_nextvar (add_functions ge fl) = genv_nextvar ge.
+Theorem find_funct_ptr_inversion:
+  forall p b f,
+  find_funct_ptr (globalenv p) b = Some f ->
+  exists id, In (id, Gfun f) (prog_defs p).
 Proof.
-  induction fl; simpl; intros. auto. rewrite IHfl. auto. 
+  intros until f. unfold globalenv. apply add_globals_preserves. 
+(* preserves *)
+  unfold find_funct_ptr; simpl; intros. destruct g; auto. 
+  rewrite ZMap.gsspec in H1. destruct (ZIndexed.eq b (genv_next ge)).
+  inv H1. exists id; auto.
+  auto.
+(* base *)
+  unfold find_funct_ptr; simpl; intros. rewrite ZMap.gi in H. discriminate.
 Qed.
 
-Remark add_variables_nextvar:
-  forall vl ge, genv_nextvar (add_variables ge vl) = genv_nextvar ge + Z_of_nat(List.length vl).
+Theorem find_funct_inversion:
+  forall p v f,
+  find_funct (globalenv p) v = Some f ->
+  exists id, In (id, Gfun f) (prog_defs p).
 Proof.
-  induction vl; intros.
-  simpl. unfold block; omega.
-  simpl length; rewrite inj_S; simpl. rewrite IHvl. simpl. unfold block; omega.
-Qed.
-
-Theorem find_funct_ptr_exists:
-  forall p id f,
-  list_norepet (prog_funct_names p) ->
-  list_disjoint (prog_funct_names p) (prog_var_names p) ->
-  In (id, f) (prog_funct p) ->
-  exists b, find_symbol (globalenv p) id = Some b
-         /\ find_funct_ptr (globalenv p) b = Some f.
-Proof.
-  intros until f.
-
-  assert (forall fl ge, In (id, f) fl -> list_norepet (funct_names fl) ->
-          exists b, find_symbol (add_functions ge fl) id = Some b
-                 /\ find_funct_ptr (add_functions ge fl) b = Some f).
-  induction fl; simpl; intros. contradiction. inv H0. 
-  destruct H. subst a. exists (genv_nextfun ge); split.
-  rewrite add_functions_same_symb; auto. unfold find_symbol; simpl. apply PTree.gss.
-  rewrite add_functions_same_address. unfold find_funct_ptr; simpl. apply ZMap.gss. 
-  simpl; omega.
-  apply IHfl; auto. 
-
-  intros. exploit (H p.(prog_funct) empty_genv); eauto. intros [b [A B]].
-  unfold globalenv; exists b; split.
-  rewrite add_variables_same_symb. auto. eapply list_disjoint_notin; eauto. 
-  unfold prog_funct_names. change id with (fst (id, f)). apply in_map; auto. 
-  rewrite add_variables_same_funs. auto.
+  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.
 
 Theorem find_funct_ptr_prop:
   forall (P: F -> Prop) p b f,
-  (forall id f, In (id, f) (prog_funct p) -> P f) ->
+  (forall id f, In (id, Gfun f) (prog_defs p) -> P f) ->
   find_funct_ptr (globalenv p) b = Some f ->
   P f.
 Proof.
-  intros until f. intros PROP.
-  assert (forall fl ge,
-          List.incl fl (prog_funct p) ->
-          match find_funct_ptr ge b with None => True | Some f => P f end ->
-          match find_funct_ptr (add_functions ge fl) b with None => True | Some f => P f end).
-  induction fl; simpl; intros. auto.
-  apply IHfl. eauto with coqlib. unfold find_funct_ptr; simpl.
-  destruct a as [id' f']; simpl. 
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (genv_nextfun ge)). 
-  apply PROP with id'. apply H. auto with coqlib. 
-  assumption.
-
-  unfold globalenv. rewrite add_variables_same_funs. intro. 
-  exploit (H p.(prog_funct) empty_genv). auto with coqlib. 
-  unfold find_funct_ptr; simpl. rewrite ZMap.gi. auto.
-  rewrite H0. auto.
+  intros. exploit find_funct_ptr_inversion; eauto. intros [id IN]. eauto.
 Qed.
 
 Theorem find_funct_prop:
   forall (P: F -> Prop) p v f,
-  (forall id f, In (id, f) (prog_funct p) -> P f) ->
+  (forall id f, In (id, Gfun f) (prog_defs p) -> P f) ->
   find_funct (globalenv p) v = Some f ->
   P f.
 Proof.
-  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. 
-  rewrite find_funct_find_funct_ptr in H0. 
-  eapply find_funct_ptr_prop; eauto.
-Qed.
-
-Theorem find_funct_ptr_inversion:
-  forall p b f,
-  find_funct_ptr (globalenv p) b = Some f ->
-  exists id, In (id, f) (prog_funct p).
-Proof.
-  intros. pattern f. apply find_funct_ptr_prop with p b; auto.
-  intros. exists id; auto.
-Qed.
-
-Theorem find_funct_inversion:
-  forall p v f,
-  find_funct (globalenv p) v = Some f ->
-  exists id, In (id, f) (prog_funct p).
-Proof.
-  intros. pattern f. apply find_funct_prop with p v; auto.
-  intros. exists id; auto.
-Qed.
-
-Theorem find_funct_ptr_negative:
-  forall p b f,
-  find_funct_ptr (globalenv p) b = Some f -> b < 0.
-Proof.
-  unfold find_funct_ptr. intros. destruct (globalenv p). simpl in H. 
-  exploit genv_funs_range0; eauto. omega. 
-Qed.
-
-Theorem find_var_info_positive:
-  forall p b v,
-  find_var_info (globalenv p) b = Some v -> b > 0.
-Proof.
-  unfold find_var_info. intros. destruct (globalenv p). simpl in H. 
-  exploit genv_vars_range0; eauto. omega. 
-Qed.
-
-Remark add_variables_symb_neg:
-  forall id b vl ge,
-  find_symbol (add_variables ge vl) id = Some b -> b < 0 ->
-  find_symbol ge id = Some b.
-Proof.
-  induction vl; simpl; intros. auto.
-  exploit IHvl; eauto. unfold find_symbol; simpl. rewrite PTree.gsspec. 
-  fold ident. destruct (peq id (a#1)); auto. intros. inv H1. 
-  generalize (genv_nextvar_pos ge). intros. omegaContradiction.
+  intros. exploit find_funct_inversion; eauto. intros [id IN]. eauto.
 Qed.
 
 Theorem find_funct_ptr_symbol_inversion:
   forall p id b f,
   find_symbol (globalenv p) id = Some b ->
   find_funct_ptr (globalenv p) b = Some f ->
-  In (id, f) p.(prog_funct).
-Proof.
-  intros until f.
-
-  assert (forall fl ge,
-          find_symbol (add_functions ge fl) id = Some b ->
-          find_funct_ptr (add_functions ge fl) b = Some f ->
-          In (id, f) fl \/ (find_symbol ge id = Some b /\ find_funct_ptr ge b = Some f)).
-  induction fl; simpl; intros.
+  In (id, Gfun f) p.(prog_defs).
+Proof.
+  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). 
+  inv H1. destruct g as [f1|v1]. rewrite ZMap.gss in H2. inv H2. auto. 
+  exploit genv_funs_range; eauto. intros. omegaContradiction.
+  destruct g as [f1|v1]. rewrite ZMap.gso in H2. auto. 
+  exploit genv_symb_range; eauto. unfold ZIndexed.t; omega. 
   auto.
-  exploit IHfl; eauto. intros [A | [A B]]. auto.
-  destruct a as [id' f'].
-  unfold find_symbol in A; simpl in A.
-  unfold find_funct_ptr in B; simpl in B.
-  rewrite PTree.gsspec in A. destruct (peq id id'). inv A. 
-  rewrite ZMap.gss in B. inv B. auto.
-  rewrite ZMap.gso in B. right; auto. 
-  exploit genv_symb_range; eauto. unfold block, ZIndexed.t; omega.
-
-  intros. assert (b < 0) by (eapply find_funct_ptr_negative; eauto). 
-  unfold globalenv in *. rewrite add_variables_same_funs in H1.
-  exploit (H (prog_funct p) empty_genv). 
-  eapply add_variables_symb_neg; eauto. auto. 
-  intuition. unfold find_symbol in H3; simpl in H3. rewrite PTree.gempty in H3. discriminate.
+(* initial *)
+  intros. simpl in *. rewrite PTree.gempty in H. discriminate.
 Qed.
 
 Theorem find_symbol_not_nullptr:
@@ -553,7 +408,7 @@ Theorem find_symbol_not_nullptr:
   find_symbol (globalenv p) id = Some b -> b <> Mem.nullptr.
 Proof.
   intros until b. unfold find_symbol. destruct (globalenv p); simpl. 
-  intros. exploit genv_symb_range0; eauto. intuition.
+  intros. exploit genv_symb_range0; eauto. unfold Mem.nullptr, block. omega. 
 Qed.
 
 Theorem global_addresses_distinct:
@@ -599,6 +454,16 @@ Proof.
   congruence.
 Qed.
 
+Remark genv_next_add_globals:
+  forall gl ge,
+  genv_next (add_globals ge gl) = genv_next ge + Z_of_nat (length gl).
+Proof.
+  induction gl; intros.
+  simpl. unfold block; omega.
+  simpl add_globals; simpl length; rewrite inj_S. 
+  rewrite IHgl. simpl. unfold block; omega.
+Qed.
+
 (** * Construction of the initial memory state *)
 
 Section INITMEM.
@@ -622,6 +487,18 @@ Proof.
   destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega.
 Qed.
 
+Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
+  if zle n 0 then Some m else
+    let n' := n - 1 in
+    match Mem.store Mint8unsigned m b p Vzero with
+    | Some m' => store_zeros m' b (p + 1) n'
+    | None => None
+    end.
+Proof.
+  intros. red. omega.
+  apply Zwf_well_founded.
+Qed.
+
 Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem :=
   match id with
   | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)
@@ -648,18 +525,6 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data)
       end
   end.
 
-Function store_zeros (m: mem) (b: block) (n: Z) {wf (Zwf 0) n}: option mem :=
-  if zle n 0 then Some m else
-    let n' := n - 1 in
-    match Mem.store Mint8unsigned m b n' Vzero with
-    | Some m' => store_zeros m' b n'
-    | None => None
-    end.
-Proof.
-  intros. red. omega.
-  apply Zwf_well_founded.
-Qed.
-
 Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
   match il with
   | nil => 0
@@ -671,37 +536,54 @@ Definition perm_globvar (gv: globvar V) : permission :=
   else if gv.(gvar_readonly) then Readable
   else Writable.
 
-Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem :=
-  let init := idv#2.(gvar_init) in
-  let sz := init_data_list_size init in
-  let (m1, b) := Mem.alloc m 0 sz in
-  match store_zeros m1 b sz with
-  | None => None
-  | Some m2 =>
-      match store_init_data_list m2 b 0 init with
+Definition alloc_global (m: mem) (idg: ident * globdef F V): option mem :=
+  match idg with
+  | (id, Gfun f) =>
+      let (m1, b) := Mem.alloc m 0 1 in
+      Mem.drop_perm m1 b 0 1 Nonempty
+  | (id, Gvar v) =>
+      let init := v.(gvar_init) in
+      let sz := init_data_list_size init in
+      let (m1, b) := Mem.alloc m 0 sz in
+      match store_zeros m1 b 0 sz with
       | None => None
-      | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar idv#2)
+      | Some m2 =>
+          match store_init_data_list m2 b 0 init with
+          | None => None
+          | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar v)
+          end
       end
   end.
 
-Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V))
-                         {struct vl} : option mem :=
-  match vl with
+Fixpoint alloc_globals (m: mem) (gl: list (ident * globdef F V))
+                       {struct gl} : option mem :=
+  match gl with
   | nil => Some m
-  | v :: vl' =>
-      match alloc_variable m v with
+  | g :: gl' =>
+      match alloc_global m g with
       | None => None
-      | Some m' => alloc_variables m' vl'
+      | Some m' => alloc_globals m' gl'
       end
   end.
 
-Lemma alloc_variables_app : forall vl1 vl2 m m1,
-  alloc_variables m vl1 = Some m1 ->
-  alloc_variables m1 vl2 = alloc_variables m (vl1 ++ vl2).
+Lemma alloc_globals_app : forall gl1 gl2 m m1,
+  alloc_globals m gl1 = Some m1 ->
+  alloc_globals m1 gl2 = alloc_globals m (gl1 ++ gl2).
+Proof.
+  induction gl1.
+  simpl. intros.  inversion H; subst. auto.
+  simpl. intros. destruct (alloc_global m a); eauto. inversion H.
+Qed.
+
+(** Next-block properties *)
+
+Remark store_zeros_nextblock:
+  forall m b p n m', store_zeros m b p n = Some m' -> Mem.nextblock m' = Mem.nextblock m.
 Proof.
-  induction vl1.
-    simpl. intros.  inversion H; subst. auto.
-    simpl. intros. destruct (alloc_variable m a); eauto. inversion H.
+  intros until n. functional induction (store_zeros m b p n); intros.
+  inv H; auto.
+  rewrite IHo; eauto with mem.
+  congruence.
 Qed.
 
 Remark store_init_data_list_nextblock:
@@ -714,71 +596,52 @@ Proof.
   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. 
-Qed.
-
-Remark store_zeros_nextblock:
-  forall m b n m', store_zeros m b n = Some m' -> Mem.nextblock m' = Mem.nextblock m.
-Proof.
-  intros until n. functional induction (store_zeros m b n); intros.
-  inv H; auto.
-  rewrite IHo; eauto with mem.
   congruence.
+  destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. 
 Qed.
 
-Remark alloc_variable_nextblock:
-  forall v m m',
-  alloc_variable m v = Some m' ->
+Remark alloc_global_nextblock:
+  forall g m m',
+  alloc_global m g = Some m' ->
   Mem.nextblock m' = Zsucc(Mem.nextblock m).
 Proof.
-  unfold alloc_variable.
-  intros until m'.   
-  set (init := gvar_init v#2).
-  set (sz := init_data_list_size init).
-  caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
-  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
-  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
-  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar v#2)); try congruence. intros m4 DROP REC. 
-  inv REC; subst.
-  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
-  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
-  rewrite (store_zeros_nextblock _ _ _ STZ). 
-  rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). 
-  auto.
-Qed.
-
-
-Remark alloc_variables_nextblock:
-  forall vl m m',
-  alloc_variables m vl = Some m' ->
-  Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length vl).
-Proof.
-  induction vl.
+  unfold alloc_global. intros.
+  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. 
+  (* variable *)
+  set (init := gvar_init v) in *.
+  set (sz := init_data_list_size init) in *.
+  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.
+  erewrite Mem.nextblock_drop; eauto.
+  erewrite store_init_data_list_nextblock; eauto.
+  erewrite store_zeros_nextblock; eauto.
+  erewrite Mem.nextblock_alloc; eauto.
+Qed.
+
+Remark alloc_globals_nextblock:
+  forall gl m m',
+  alloc_globals m gl = Some m' ->
+  Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length gl).
+Proof.
+  induction gl.
   simpl; intros. inv H; unfold block; omega.
-  simpl length; rewrite inj_S; simpl. intros m m'. 
-  unfold alloc_variable. 
-  set (init := gvar_init a#2).
-  set (sz := init_data_list_size init).
-  caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
-  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
-  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
-  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC.
-  rewrite (IHvl _ _ REC).
-  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
-  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
-  rewrite (store_zeros_nextblock _ _ _ STZ).
-  rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
-  unfold block in *; omega.
+  simpl length; rewrite inj_S; simpl; intros.
+  destruct (alloc_global m a) as [m1|]_eqn; try discriminate.
+  erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega.
 Qed.
 
+(** Permissions *)
 
 Remark store_zeros_perm:
-  forall k prm b' q m b n m',
-  store_zeros m b n = Some m' ->
+  forall k prm b' q m b p n m',
+  store_zeros m b p n = Some m' ->
   (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
-  intros until n. functional induction (store_zeros m b n); intros.
+  intros until n. functional induction (store_zeros m b p n); intros.
   inv H; tauto.
   destruct (IHo _ H); intros. split; eauto with mem.
   congruence.
@@ -793,56 +656,74 @@ Proof.
   intros. inv H. tauto. 
   caseEq (store_init_data m b p a); try congruence. intros.
   rewrite <- (IHidl _ _ _ _ H0).
-  destruct a; simpl in H; split; eauto with mem.
-  inv H; auto. inv H; auto. 
-  destruct (find_symbol ge i); try congruence. eauto with mem.
-  destruct (find_symbol ge i); try congruence. eauto with mem.
+  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. 
+  destruct a; simpl in H; eauto.
+  inv H; tauto.
+  destruct (find_symbol ge i). eauto. discriminate.
 Qed.
 
-Remark alloc_variables_perm:
-  forall k prm b' q vl m m',
-  alloc_variables m vl = Some m' ->
+Remark alloc_global_perm:
+  forall k prm b' q idg m m',
+  alloc_global m idg = Some m' ->
   Mem.valid_block m b' ->
   (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
-  induction vl.
-  simpl; intros. inv H. tauto. 
-  intros until m'. simpl. unfold alloc_variable. 
-  set (init := gvar_init a#2).
-  set (sz := init_data_list_size init).
-  caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
-  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
-  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
-  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID.
+  intros. destruct idg as [id [f|v]]; simpl in H. 
+  (* function *)
+  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. 
+  (* variable *)
+  set (init := gvar_init v) in *.
+  set (sz := init_data_list_size init) in *.
+  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.
   assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  assert (VALID': Mem.valid_block m4 b').
-    unfold Mem.valid_block. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
-    rewrite (store_init_data_list_nextblock _ _ _ _ STORE).  
-    rewrite (store_zeros_nextblock _ _ _ STZ).  
-    change (Mem.valid_block m1 b'). eauto with mem.
-  rewrite <- (IHvl _ _ REC VALID').
   split; intros.
   eapply Mem.perm_drop_3; eauto.
-  rewrite <- store_init_data_list_perm; [idtac|eauto].
-  rewrite <- store_zeros_perm; [idtac|eauto].
-  eauto with mem.
-  assert (Mem.perm m1 b' q k prm).
-    rewrite store_zeros_perm; [idtac|eauto].
-    rewrite store_init_data_list_perm; [idtac|eauto].
-    eapply Mem.perm_drop_4; eauto.
-  exploit Mem.perm_alloc_inv; eauto. rewrite zeq_false; auto.
+  erewrite <- store_init_data_list_perm; [idtac|eauto].
+  erewrite <- store_zeros_perm; [idtac|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. 
+Qed.
+
+Remark alloc_globals_perm:
+  forall k prm b' q gl m m',
+  alloc_globals m gl = Some m' ->
+  Mem.valid_block m b' ->
+  (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
+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. 
+  unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. 
 Qed.
 
+(** Data preservation properties *)
+
 Remark store_zeros_outside:
-  forall m b n m',
-  store_zeros m b n = Some m' ->
-  forall chunk b' p,
-  b' <> b -> Mem.load chunk m' b' p = Mem.load chunk m b' p.
+  forall m b p n m',
+  store_zeros m b p n = Some m' ->
+  forall chunk b' p',
+  b' <> b \/ p' + size_chunk chunk <= p \/ p + n <= p' ->
+  Mem.load chunk m' b' p' = Mem.load chunk m b' p'.
 Proof.
-  intros until n. functional induction (store_zeros m b n); intros.
+  intros until n. functional induction (store_zeros m b p n); intros.
   inv H; auto.
-  rewrite IHo; auto. eapply Mem.load_store_other; eauto. 
-  inv H.
+  transitivity (Mem.load chunk m' b' p'). 
+  apply IHo. auto. unfold block in *; omega. 
+  eapply Mem.load_store_other; eauto. simpl. unfold block in *; omega.
+  discriminate.
 Qed.
 
 Remark store_init_data_list_outside:
@@ -854,12 +735,12 @@ Remark store_init_data_list_outside:
 Proof.
   induction il; simpl.
   intros; congruence.
-  intros until m'. caseEq (store_init_data m b p a); try congruence. 
-  intros m1 A B chunk b' q C. transitivity (Mem.load chunk m1 b' q).
+  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.
-  destruct a; simpl in A;
+  destruct a; simpl in Heqo;
   try (eapply Mem.load_store_other; eauto; intuition; fail).
-  congruence.
+  inv Heqo. auto.
   destruct (find_symbol ge i); try congruence. 
   eapply Mem.load_store_other; eauto; intuition.
 Qed.
@@ -904,10 +785,9 @@ Proof.
 
   induction il; simpl.
   auto.
-  intros until m'. caseEq (store_init_data m b p a); try congruence. 
-  intros m1 B C.
+  intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence.
   exploit IHil; eauto. intro D. 
-  destruct a; simpl in B; intuition.
+  destruct a; simpl in Heqo; intuition.
   eapply (A Mint8unsigned (Vint i)); eauto.
   eapply (A Mint16unsigned (Vint i)); eauto.
   eapply (A Mint32 (Vint i)); eauto.
@@ -917,36 +797,49 @@ Proof.
   eapply (A Mint32 (Vptr b0 i0)); eauto. 
 Qed.
 
-Remark load_alloc_variables:
-  forall chunk b p vl m m',
-  alloc_variables m vl = Some m' ->
+Remark load_alloc_global:
+  forall chunk b p id g m m',
+  alloc_global m (id, g) = Some m' ->
   Mem.valid_block m b ->
   Mem.load chunk m' b p = Mem.load chunk m b p.
 Proof.
-  induction vl; simpl; intros until m'.
-  congruence.
-  unfold alloc_variable. 
-  set (init := gvar_init a#2).
-  set (sz := init_data_list_size init).
-  caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC.
-  caseEq (store_zeros m1 b1 sz); try congruence. intros m2 STZ.
-  caseEq (store_init_data_list m2 b1 0 init); try congruence. intros m3 STORE.
-  caseEq (Mem.drop_perm m3 b1 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID.
-  assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  transitivity (Mem.load chunk m4 b p).
-  apply IHvl; auto. red.
-  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
-  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
-  rewrite (store_zeros_nextblock _ _ _ STZ).
-  change (Mem.valid_block m1 b). eauto with mem.
-  transitivity (Mem.load chunk m3 b p). 
+  intros. destruct g as [f|v]; simpl in H.
+  (* function *)
+  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. 
+  eapply Mem.load_alloc_unchanged; eauto.
+  (* variable *)
+  set (init := gvar_init v) in *.
+  set (sz := init_data_list_size init) in *.
+  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.
+  assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
+  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_outside; eauto.
   eapply Mem.load_alloc_unchanged; eauto.
-Qed. 
+Qed.
+
+Remark load_alloc_globals:
+  forall chunk b p gl m m',
+  alloc_globals m gl = Some m' ->
+  Mem.valid_block m b ->
+  Mem.load chunk m' b p = Mem.load chunk m b p.
+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. omega.
+  destruct a as [id g]. eapply load_alloc_global; eauto. 
+Qed.
 
 Remark load_store_init_data_invariant:
   forall m m' b,
@@ -967,114 +860,147 @@ Definition variables_initialized (g: t) (m: mem) :=
         0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
   /\ (gv.(gvar_volatile) = false -> load_store_init_data m b 0 gv.(gvar_init)).
 
-Lemma alloc_variable_initialized:
-  forall g m id v m',
-  genv_nextvar g = Mem.nextblock m ->
-  alloc_variable m (id, v) = Some m' ->
-  variables_initialized g m ->
-  variables_initialized (add_variable g (id, v)) m'
-  /\ genv_nextvar (add_variable g (id,v)) = Mem.nextblock m'.
-Proof.
-  intros. revert H0. unfold alloc_variable. simpl. 
-  set (il := gvar_init v).
-  set (sz := init_data_list_size il).
-  caseEq (Mem.alloc m 0 sz).   intros m1 b1 ALLOC.
-  caseEq (store_zeros m1 b1 sz); try congruence. intros m2 ZEROS.
-  caseEq (store_init_data_list m2 b1 0 il); try congruence. intros m3 INIT DROP.
-  exploit Mem.nextblock_alloc; eauto.  intros NB1.
-  assert (Mem.nextblock m' = Mem.nextblock m1).
-    rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
-    rewrite (store_init_data_list_nextblock _ _ _ _ INIT).
-    eapply store_zeros_nextblock; eauto.
-  exploit Mem.alloc_result; eauto. intro RES.
-  split.
-  (* var-init *)
-  red; intros. revert H2.
-  unfold add_variable, find_var_info; simpl.
-  rewrite H; rewrite <- RES.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b b1); intros VI.
-  (* new var *)
-  injection VI; intro EQ. subst b gv. clear VI.
-  fold il. fold sz.
-  split. red; intros. eapply Mem.perm_drop_1; eauto.
-  split. intros. 
-    assert (0 <= ofs < sz).
-      eapply Mem.perm_alloc_3; eauto. 
-      rewrite store_zeros_perm; [idtac|eauto].
-      rewrite store_init_data_list_perm; [idtac|eauto].
-      eapply Mem.perm_drop_4; eauto.
-  split; auto. eapply Mem.perm_drop_2; eauto.
+Definition functions_initialized (g: t) (m: mem) :=
+  forall b fd,
+  find_funct_ptr g b = Some fd ->
+  Mem.perm m b 0 Cur Nonempty
+  /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p).
+
+Lemma alloc_global_initialized:
+  forall ge m id g m',
+  genv_next ge = Mem.nextblock m ->
+  alloc_global m (id, g) = Some m' ->
+  variables_initialized ge m ->
+  functions_initialized ge m ->
+  variables_initialized (add_global ge (id, g)) m'
+  /\ functions_initialized (add_global ge (id, g)) m'
+  /\ genv_next (add_global ge (id, g)) = Mem.nextblock m'.
+Proof.
   intros. 
-  apply load_store_init_data_invariant with m3.
-  intros. eapply Mem.load_drop; eauto. right; right; right.
-  unfold perm_globvar. destruct (gvar_volatile v); try discriminate.
-  destruct (gvar_readonly v); auto with mem.
+  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. 
+  exploit H1; eauto. intros [A [B C]].
+  assert (D: Mem.valid_block m b). 
+    red. exploit genv_vars_range; eauto. rewrite H; omega. 
+  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 ZMap.gsspec in H3.
+  destruct (ZIndexed.eq b (genv_next ge0)).
+  (* same *)
+  inv H3. simpl in H0.
+  set (init := gvar_init gv) in *.
+  set (sz := init_data_list_size init) in *.
+  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. 
+  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]. 
+    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. 
+  destruct (gvar_readonly gv); auto with mem.
   eapply store_init_data_list_charact; eauto.
-  (* older vars *)
+  (* older var *)
   exploit H1; eauto. intros [A [B C]].
-  split. red; intros. eapply Mem.perm_drop_3; eauto. 
-  rewrite <- store_init_data_list_perm; [idtac|eauto].
-  rewrite <- store_zeros_perm; [idtac|eauto].
-  eapply Mem.perm_alloc_1; eauto.
-  split. intros. eapply B. 
-  eapply Mem.perm_alloc_4; eauto.   
-  rewrite store_zeros_perm; [idtac|eauto].
-  rewrite store_init_data_list_perm; [idtac|eauto].
-  eapply Mem.perm_drop_4; eauto.
-  intros. apply load_store_init_data_invariant with m; auto.
-  intros. transitivity (Mem.load chunk m3 b ofs). 
-  eapply Mem.load_drop; eauto. 
-  transitivity (Mem.load chunk m2 b ofs). 
-  eapply store_init_data_list_outside; eauto.
-  transitivity (Mem.load chunk m1 b ofs). 
-  eapply store_zeros_outside; eauto.
-  eapply Mem.load_alloc_unchanged; eauto.
-  red. exploit genv_vars_range; eauto. rewrite <- H. omega.
-  rewrite H0; rewrite NB1; rewrite H; auto.
-Qed.
-
-Lemma alloc_variables_initialized:
-  forall vl g m m',
-  genv_nextvar g = Mem.nextblock m ->
-  alloc_variables m vl = Some m' ->
-  variables_initialized g m ->
-  variables_initialized (add_variables g vl) m'.
-Proof.
-  induction vl; simpl; intros.
+  assert (D: Mem.valid_block m b). 
+    red. exploit genv_vars_range; eauto. rewrite H; omega. 
+  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].
+(* function *)
+  red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite ZMap.gsspec in H3.
+  destruct (ZIndexed.eq 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. 
+  replace (genv_next ge0) with b' by congruence.
+  split. eapply Mem.perm_drop_1; eauto. omega. 
+  intros.
+  assert (0 <= ofs < 1).
+    eapply Mem.perm_alloc_3; eauto.
+    eapply Mem.perm_drop_4; eauto.
+  split. omega. eapply Mem.perm_drop_2; eauto.
+  (* older function *)
+  exploit H2; eauto. intros [A B].
+  assert (D: Mem.valid_block m b). 
+    red. exploit genv_funs_range; eauto. rewrite H; omega. 
+  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. 
+  exploit H2; eauto. intros [A B].
+  assert (D: Mem.valid_block m b). 
+    red. exploit genv_funs_range; eauto. rewrite H; omega. 
+  split. erewrite <- alloc_global_perm; eauto. 
+  intros. eapply B. erewrite alloc_global_perm; eauto.
+(* nextblock *)
+  rewrite NB. simpl. rewrite H. unfold block; omega. 
+Qed.
+
+Lemma alloc_globals_initialized:
+  forall gl ge m m',
+  genv_next ge = Mem.nextblock m ->
+  alloc_globals m gl = Some m' ->
+  variables_initialized ge m ->
+  functions_initialized ge m ->
+  variables_initialized (add_globals ge gl) m' /\ functions_initialized (add_globals ge gl) m'.
+Proof.
+  induction gl; simpl; intros.
   inv H0; auto.
-  destruct (alloc_variable m a) as [m1|]_eqn; try discriminate.
-  destruct a as [id gv].
-  exploit alloc_variable_initialized; eauto. intros [P Q].
-  eapply IHvl; eauto. 
+  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. 
 Qed.
 
 End INITMEM.
 
 Definition init_mem (p: program F V) :=
-  alloc_variables (globalenv p) Mem.empty p.(prog_vars).
+  alloc_globals (globalenv p) Mem.empty p.(prog_defs).
+
+Lemma init_mem_genv_next: forall p 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). 
+  fold (globalenv p). simpl genv_next. intros. congruence.
+Qed.
 
 Theorem find_symbol_not_fresh:
   forall p id b m,
   init_mem p = Some m ->
   find_symbol (globalenv p) id = Some b -> Mem.valid_block m b.
 Proof.
-  unfold init_mem; intros.
-  exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro.
-  exploit genv_symb_range; eauto. intros.
-  generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))).
-  rewrite add_functions_nextvar. simpl genv_nextvar. intro.
-  red. rewrite H1. rewrite <- H3. intuition.
+  intros. red. erewrite <- init_mem_genv_next; eauto. 
+  exploit genv_symb_range; eauto. omega.
 Qed.
 
-Lemma init_mem_genv_vars : forall p m,
-    init_mem p = Some m -> 
-    genv_nextvar (globalenv p) = Mem.nextblock m.
+Theorem find_funct_ptr_not_fresh:
+  forall p b f m,
+  init_mem p = Some m ->
+  find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b.
 Proof.
-    clear. unfold globalenv, init_mem.  intros.
-    exploit alloc_variables_nextblock; eauto.
-    simpl (Mem.nextblock Mem.empty). 
-    rewrite add_variables_nextvar.  rewrite add_functions_nextvar.
-    simpl (genv_nextvar empty_genv).  auto.
+  intros. red. erewrite <- init_mem_genv_next; eauto. 
+  exploit genv_funs_range; eauto. omega.
 Qed.
 
 Theorem find_var_info_not_fresh:
@@ -1082,12 +1008,8 @@ 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.
-  unfold init_mem; intros.
-  exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro.
-  exploit genv_vars_range; eauto. intros.
-  generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))).
-  rewrite add_functions_nextvar. simpl genv_nextvar. intro.
-  red. rewrite H1. rewrite <- H3. intuition.
+  intros. red. erewrite <- init_mem_genv_next; eauto. 
+  exploit genv_vars_range; eauto. omega.
 Qed.
 
 Theorem init_mem_characterization:
@@ -1099,10 +1021,23 @@ Theorem init_mem_characterization:
         0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
   /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)).
 Proof.
-  intros. eapply alloc_variables_initialized; eauto. 
-  rewrite add_functions_nextvar; auto. 
-  red; intros. exploit genv_vars_range; eauto. rewrite add_functions_nextvar. 
-  simpl. intros. omegaContradiction.
+  intros. eapply alloc_globals_initialized; eauto.
+  rewrite Mem.nextblock_empty. auto. 
+  red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction.
+  red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction.
+Qed.
+
+Theorem init_mem_characterization_2:
+  forall p b fd m,
+  find_funct_ptr (globalenv p) b = Some fd ->
+  init_mem p = Some m ->
+  Mem.perm m b 0 Cur Nonempty
+  /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p).
+Proof.
+  intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto.
+  rewrite Mem.nextblock_empty. auto. 
+  red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction.
+  red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction.
 Qed.
 
 (** ** Compatibility with memory injections *)
@@ -1113,6 +1048,19 @@ Variable ge: t.
 Variable thr: block.
 Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> b < thr.
 
+Lemma store_zeros_neutral:
+  forall m b p n m',
+  Mem.inject_neutral thr m ->
+  b < thr ->
+  store_zeros m b p n = Some m' ->
+  Mem.inject_neutral thr m'.
+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.  
+  inv H1.
+Qed.
+
 Lemma store_init_data_neutral:
   forall m b p id m',
   Mem.inject_neutral thr m ->
@@ -1122,7 +1070,7 @@ Lemma store_init_data_neutral:
 Proof.
   intros.
   destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail).
-  inv H1; auto.
+  congruence.
   revert H1. caseEq (find_symbol ge i); try congruence. intros b' FS ST. 
   eapply Mem.store_inject_neutral; eauto. 
   econstructor. unfold Mem.flat_inj. apply zlt_true; eauto. 
@@ -1143,54 +1091,46 @@ Proof.
   eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. 
 Qed.
 
-Lemma store_zeros_neutral:
-  forall m b n m',
-  Mem.inject_neutral thr m ->
-  b < thr ->
-  store_zeros m b n = Some m' ->
-  Mem.inject_neutral thr m'.
-Proof.
-  intros until n. functional induction (store_zeros m b n); intros.
-  inv H1; auto.
-  apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor.  
-  inv H1.
-Qed.
-
-Lemma alloc_variable_neutral:
-  forall id m m',
-  alloc_variable ge m id = Some m' ->
+Lemma alloc_global_neutral:
+  forall idg m m',
+  alloc_global ge m idg = Some m' ->
   Mem.inject_neutral thr m ->
   Mem.nextblock m < thr ->
   Mem.inject_neutral thr m'.
 Proof.
-  intros until m'. unfold alloc_variable.
-  set (init := gvar_init id#2).
-  set (sz := init_data_list_size init).
-  caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC.
-  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
-  caseEq (store_init_data_list ge m2 b 0 init); try congruence.
-  intros m3 STORE DROP NEUTRAL NEXT.
-  assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
+  intros. destruct idg as [id [f|v]]; simpl in H.
+  (* function *)
+  destruct (Mem.alloc m 0 1) as [m1 b]_eqn.
+  assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  eapply Mem.drop_inject_neutral; eauto. 
+  eapply Mem.alloc_inject_neutral; eauto.
+  (* variable *)
+  set (init := gvar_init v) in *.
+  set (sz := init_data_list_size init) in *.
+  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 ge m2 b 0 init) as [m3|]_eqn; try discriminate.
+  assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   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 Mem.alloc_inject_neutral; eauto.
 Qed.
 
-Lemma alloc_variables_neutral:
-  forall idl m m',
-  alloc_variables ge m idl = Some m' ->
+Lemma alloc_globals_neutral:
+  forall gl m m',
+  alloc_globals ge m gl = Some m' ->
   Mem.inject_neutral thr m ->
   Mem.nextblock m' <= thr ->
   Mem.inject_neutral thr m'.
 Proof.
-  induction idl; simpl.
+  induction gl; simpl.
   intros. congruence.
-  intros until m'. caseEq (alloc_variable ge m a); try congruence. intros.
-  assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: idl))).
-  eapply alloc_variables_nextblock with ge. simpl. rewrite H. auto. 
+  intros until m'. caseEq (alloc_global ge m a); try congruence. intros.
+  assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: gl))).
+  eapply alloc_globals_nextblock with ge. simpl. rewrite H. auto. 
   simpl length in H3. rewrite inj_S in H3. 
-  exploit alloc_variable_neutral; eauto. unfold block in *; omega.
+  exploit alloc_global_neutral; eauto. unfold block in *; omega.
 Qed.
 
 End INITMEM_INJ.
@@ -1202,7 +1142,7 @@ Theorem initmem_inject:
 Proof.
   unfold init_mem; intros.
   apply Mem.neutral_inject. 
-  eapply alloc_variables_neutral; eauto. 
+  eapply alloc_globals_neutral; eauto. 
   intros. exploit find_symbol_not_fresh; eauto.
   apply Mem.empty_inject_neutral.
   omega.
@@ -1213,6 +1153,22 @@ Section INITMEM_AUGMENT_INJ.
 Variable ge: t.
 Variable thr: block.
 
+Lemma store_zeros_augment:
+  forall m1 m2 b p n m2',
+  Mem.inject (Mem.flat_inj thr) m1 m2 ->
+  b >= thr ->
+  store_zeros m2 b p n = Some m2' ->
+  Mem.inject (Mem.flat_inj thr) m1 m2'.
+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 (zlt b' thr). 
+    inversion H2; subst; omega.  
+    discriminate.
+  inv H1.
+Qed.
+
 Lemma store_init_data_augment: 
   forall m1 m2 b p id m2', 
   Mem.inject (Mem.flat_inj thr) m1 m2 -> 
@@ -1228,7 +1184,7 @@ Proof.
     intros. unfold Mem.flat_inj in H0.
     destruct (zlt b' thr); inversion H0; subst. omega. 
   destruct id; simpl in ST; try (eapply P; eauto; fail).
-  inv ST; auto. 
+  congruence.
   revert ST.  caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. 
 Qed.
 
@@ -1246,59 +1202,49 @@ Proof.
   eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. 
 Qed.
 
-Lemma store_zeros_augment:
-  forall m1 m2 b n m2',
-  Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  b >= thr ->
-  store_zeros m2 b n = Some m2' ->
-  Mem.inject (Mem.flat_inj thr) m1 m2'.
-Proof.
-  intros until n. functional induction (store_zeros m2 b n); intros.
-  inv H1; auto.
-  apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. 
-  intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). 
-    inversion H2; subst; omega.  
-    discriminate.
-  inv H1.
-Qed.
-
-Lemma alloc_variable_augment:
-  forall id m1 m2 m2',
-  alloc_variable ge m2 id = Some m2' ->
+Lemma alloc_global_augment:
+  forall idg m1 m2 m2',
+  alloc_global ge m2 idg = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2 -> 
   Mem.nextblock m2 >= thr -> 
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof.
-  intros until m2'. unfold alloc_variable. 
-  set (sz := init_data_list_size (gvar_init id#2)).
-  caseEq (Mem.alloc m2 0 sz); try congruence. intros m3 b ALLOC.
-  caseEq (store_zeros m3 b sz); try congruence. intros m4 STZ.
-  caseEq (store_init_data_list ge m4 b 0 (gvar_init id#2)); try congruence.
-  intros m5 STORE DROP INJ NEXT.
-  assert (b >= thr). 
-     pose proof (Mem.fresh_block_alloc _ _ _ _ _ ALLOC).  
-     unfold Mem.valid_block in H.  unfold block in *; omega. 
-  eapply Mem.drop_outside_inject. 2: eauto.  
-  eapply store_init_data_list_augment. 2: eauto. 2: eauto. 
-  eapply store_zeros_augment. 2: eauto. 2: eauto.
-  eapply Mem.alloc_right_inject; eauto. 
-  intros. unfold Mem.flat_inj in H0. destruct (zlt b' thr); inversion H0. 
+  intros. destruct idg as [id [f|v]]; simpl in H.
+  (* function *)
+  destruct (Mem.alloc m2 0 1) as [m3 b]_eqn.
+  assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  eapply Mem.drop_outside_inject. 2: eauto. 
+  eapply Mem.alloc_right_inject; eauto.
+  intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. 
+     subst; exfalso; omega.
+  (* variable *)
+  set (init := gvar_init v) in *.
+  set (sz := init_data_list_size init) in *.
+  destruct (Mem.alloc m2 0 sz) as [m3 b]_eqn.
+  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 (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  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.
+  intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. 
      subst; exfalso; omega.
 Qed.
 
-Lemma alloc_variables_augment:
-  forall idl m1 m2 m2',
-  alloc_variables ge m2 idl = Some m2' ->
+Lemma alloc_globals_augment:
+  forall gl m1 m2 m2',
+  alloc_globals ge m2 gl = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2 ->
   Mem.nextblock m2 >= thr ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof.
-  induction idl; simpl.
+  induction gl; simpl.
   intros. congruence.
-  intros until m2'. caseEq (alloc_variable ge m2 a); try congruence. intros.
-  eapply IHidl with (m2 := m); eauto.  
-    eapply alloc_variable_augment; eauto. 
-    rewrite (alloc_variable_nextblock _ _ _ H). 
+  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). 
     unfold block in *; omega. 
 Qed.
 
@@ -1321,216 +1267,156 @@ 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_functs : list (ident * B)) (new_vars : list (ident * globvar W)) 
+Record match_genvs (new_globs : list (ident * globdef B W)) 
                    (ge1: t A V) (ge2: t B W): Prop := {
-  mge_nextfun: genv_nextfun ge2 = genv_nextfun ge1 - Z_of_nat(length new_functs);
-  mge_nextvar: genv_nextvar ge2 = genv_nextvar ge1 + Z_of_nat(length new_vars);
-  mge_symb:    forall id,  ~ In id ((funct_names new_functs) ++ (var_names new_vars)) -> 
+  mge_next:
+    genv_next ge2 = genv_next ge1 + Z_of_nat(length new_globs);
+  mge_symb:
+    forall id, ~ In id (map fst new_globs) ->
                    PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1);
   mge_funs:
     forall b f, ZMap.get b (genv_funs ge1) = Some f ->
     exists tf, ZMap.get b (genv_funs ge2) = Some tf /\ match_fun f tf;
   mge_rev_funs:
     forall b tf, ZMap.get b (genv_funs ge2) = Some tf ->
-    if zlt (genv_nextfun ge1) b then 
+    if zlt b (genv_next ge1) then 
       exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf
     else 
-      In tf (map (@snd ident B) new_functs);
+      In (Gfun tf) (map snd new_globs);
   mge_vars:
     forall b v, ZMap.get b (genv_vars ge1) = Some v ->
     exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv;
   mge_rev_vars:
     forall b tv, ZMap.get b (genv_vars ge2) = Some tv ->
-    if zlt b (genv_nextvar ge1) then
+    if zlt b (genv_next ge1) then
       exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv
     else
-      In tv (map (@snd ident (globvar W)) new_vars)
+      In (Gvar tv) (map snd new_globs)
 }.
 
-Lemma add_function_match:
-  forall ge1 ge2 id f1 f2,
-  match_genvs nil nil ge1 ge2 ->
-  match_fun f1 f2 ->
-  match_genvs nil nil (add_function ge1 (id, f1)) (add_function ge2 (id, f2)).
+Lemma add_global_match:
+  forall ge1 ge2 idg1 idg2,
+  match_genvs nil ge1 ge2 ->
+  match_globdef match_fun match_varinfo idg1 idg2 ->
+  match_genvs nil (add_global ge1 idg1) (add_global ge2 idg2).
 Proof.
   intros. destruct H. 
-     simpl in mge_nextfun0. rewrite Zminus_0_r in mge_nextfun0. 
-     simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. 
-  constructor; simpl. 
-  rewrite Zminus_0_r. congruence.
+     simpl in mge_next0. rewrite Zplus_0_r in mge_next0.
+  inv H0.
+(* two functions *)
+  constructor; simpl.
   rewrite Zplus_0_r. congruence.
-  intros. rewrite mge_nextfun0. 
-    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. 
-    rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-    destruct (ZIndexed.eq b (genv_nextfun ge1)). 
+  intros. rewrite mge_next0. 
+    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
+  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
+    destruct (ZIndexed.eq b (genv_next ge1)). 
      exists f2; split; congruence.
      eauto.
-  rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-   destruct (ZIndexed.eq b (genv_nextfun ge1)). 
-    subst b. destruct (zlt (genv_nextfun ge1 - 1) (genv_nextfun ge1)). 
-      exists f1; split; congruence. omega. 
-    pose proof (mge_rev_funs0 b tf H). 
-    destruct (zlt (genv_nextfun ge1) b); 
-      destruct (zlt (genv_nextfun ge1 - 1) b).  auto. omega. exfalso; omega. intuition.
-  auto.
-  auto.
-Qed.
-
-Lemma add_functions_match:
-  forall fl1 fl2, list_forall2 (match_funct_entry match_fun) fl1 fl2 ->
-  forall ge1 ge2, match_genvs nil nil ge1 ge2 ->
-  match_genvs nil nil (add_functions ge1 fl1) (add_functions ge2 fl2).
-Proof.
-  induction 1; intros; simpl. 
-  auto.
-  destruct a1 as [id1 f1]; destruct b1 as [id2 f2].
-  destruct H. subst. apply IHlist_forall2. apply add_function_match; auto.
-Qed.
-
-Lemma add_function_augment_match: 
-  forall new_functs new_vars ge1 ge2 id f2,
-  match_genvs new_functs new_vars ge1 ge2 ->
-  match_genvs (new_functs++((id,f2)::nil)) new_vars ge1 (add_function ge2 (id, f2)).
-Proof.
-  intros. destruct H. constructor; simpl. 
-  rewrite mge_nextfun0. rewrite app_length. 
-       simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *)
-  auto.
-  intros. unfold funct_names in H. rewrite map_app in H. rewrite in_app in H.  rewrite in_app in H. simpl in H. 
-     destruct (peq id id0). subst. intuition. rewrite PTree.gso. 
-     apply mge_symb0. intro.  apply H. rewrite in_app in H0. inversion H0; intuition. intuition. 
-  intros. rewrite ZMap.gso. auto. 
-     rewrite mge_nextfun0. pose proof (genv_funs_range ge1 b H). intro; subst; omega.
-  intros. rewrite ZMap.gsspec in H. 
-     destruct (ZIndexed.eq b (genv_nextfun ge2)). 
-       destruct (zlt (genv_nextfun ge1) b). 
-          exfalso.  rewrite mge_nextfun0 in e.  unfold block; omega. 
-          rewrite map_app. rewrite in_app.  simpl.  inversion H; intuition.
-       pose proof (mge_rev_funs0 b tf H). 
-          destruct (zlt (genv_nextfun ge1) b). 
-            auto.
-            rewrite map_app. rewrite in_app. intuition. 
-  auto.
-  auto.
-Qed.
-
-
-Lemma add_functions_augment_match:
-  forall fl new_functs new_vars ge1 ge2, 
-    match_genvs new_functs new_vars ge1 ge2 ->
-    match_genvs (new_functs++fl) new_vars ge1 (add_functions ge2 fl).
-Proof.
-  induction fl; simpl. 
-    intros. rewrite app_nil_r. auto. 
-    intros. replace (new_functs ++ a :: fl) with ((new_functs ++ (a::nil)) ++ fl) 
-       by (rewrite app_ass; auto). 
-     apply IHfl. destruct a. apply add_function_augment_match. auto.
-Qed.
-
-
-Lemma add_variable_match:
-  forall new_functs ge1 ge2 id v1 v2,
-  match_genvs new_functs nil ge1 ge2 ->
-  match_globvar v1 v2 ->
-  match_genvs new_functs nil (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)).
-Proof.
-  intros. destruct H. 
-     simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. 
-  constructor; simpl. 
-  auto. 
-    rewrite Zplus_0_r. rewrite mge_nextvar0. auto. 
-  intros. rewrite mge_nextvar0. 
-    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. 
-  auto.
-  auto.
-  rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-    destruct (ZIndexed.eq b (genv_nextvar ge1)). 
-     exists v2; split; congruence.
-     eauto.
-  rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. 
-   destruct (ZIndexed.eq b (genv_nextvar ge1)). 
-    subst b. inversion H; subst. 
-      destruct (zlt (genv_nextvar ge1) (genv_nextvar ge1 + 1)). 
-        exists v1; split; congruence. omega. 
-      pose proof (mge_rev_vars0 _ _ H).
-        destruct (zlt b (genv_nextvar ge1));
-          destruct (zlt b (genv_nextvar ge1 + 1)).  auto. omega. exfalso; omega. intuition.
+  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
+   destruct (ZIndexed.eq b (genv_next ge1)). 
+    subst b. rewrite zlt_true. exists f1; split; congruence. omega.
+    pose proof (mge_rev_funs0 b tf H0). 
+    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    contradiction.
+  eauto.
+  intros.
+    pose proof (mge_rev_vars0 b tv H0). 
+    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    contradiction.
+(* two variables *)
+  constructor; simpl.
+  rewrite Zplus_0_r. congruence.
+  intros. rewrite mge_next0. 
+    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
+  eauto.
+  intros.
+    pose proof (mge_rev_funs0 b tf H0). 
+    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    contradiction.
+  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
+    destruct (ZIndexed.eq b (genv_next ge1)).
+    econstructor; split. eauto. inv H0. constructor; auto. 
+    eauto.
+  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
+   destruct (ZIndexed.eq b (genv_next ge1)). 
+    subst b. rewrite zlt_true.
+    econstructor; split. eauto. inv H0. constructor; auto.
+    omega.
+    pose proof (mge_rev_vars0 b tv H0). 
+    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    contradiction.
 Qed.
 
-Lemma add_variables_match:
-  forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
-  forall new_functs ge1 ge2, match_genvs new_functs nil ge1 ge2 ->
-  match_genvs new_functs nil (add_variables ge1 vl1) (add_variables ge2 vl2).
+Lemma add_globals_match:
+  forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 ->
+  forall ge1 ge2, match_genvs nil ge1 ge2 ->
+  match_genvs nil (add_globals ge1 gl1) (add_globals ge2 gl2).
 Proof.
   induction 1; intros; simpl. 
   auto.
-  inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; auto.
+  apply IHlist_forall2. apply add_global_match; auto.
 Qed.
 
-
-Lemma add_variable_augment_match:
-  forall ge1 new_functs new_vars ge2 id v2,
-  match_genvs new_functs new_vars ge1 ge2 ->
-  match_genvs new_functs (new_vars++((id,v2)::nil)) ge1 (add_variable ge2 (id, v2)).
+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. constructor; simpl. 
-  auto.
-  rewrite mge_nextvar0. rewrite app_length. 
-       simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *)
-  intros. unfold funct_names, var_names in H. rewrite map_app in H. rewrite in_app in H.  rewrite in_app in H. simpl in H. 
-     destruct (peq id id0). subst. intuition. rewrite PTree.gso. 
-     apply mge_symb0. intro.  apply H. rewrite in_app in H0. inversion H0; intuition. intuition. 
-  auto.
-  auto.
-  intros. rewrite ZMap.gso. auto. 
-     rewrite mge_nextvar0. pose proof (genv_vars_range ge1 b H). intro; subst; omega.
-  intros. rewrite ZMap.gsspec in H. 
-     destruct (ZIndexed.eq b (genv_nextvar ge2)). 
-       destruct (zlt b (genv_nextvar ge1)). 
-          exfalso.  rewrite mge_nextvar0 in e.  unfold block; omega. 
-          rewrite map_app. rewrite in_app.  simpl.  inversion H; intuition.
-       pose proof (mge_rev_vars0 b tv H). 
-          destruct (zlt b (genv_nextvar ge1)). 
-            auto.
-            rewrite map_app. rewrite in_app. intuition. 
-
-Qed.
-
-Lemma add_variables_augment_match:
-  forall vl ge1 new_functs new_vars ge2, 
-    match_genvs new_functs new_vars ge1 ge2 ->
-    match_genvs new_functs (new_vars++vl) ge1  (add_variables ge2 vl).
-Proof.
-  induction vl; simpl. 
+  rewrite mge_next0. rewrite app_length. 
+    simpl. rewrite inj_plus. change (Z_of_nat 1) with 1. unfold block; omega.
+  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 ZMap.gso. eauto. exploit genv_funs_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. 
+  intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
+    rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). 
+    rewrite zlt_false. rewrite in_app. simpl; right; left. congruence.
+    subst b. rewrite mge_next0. omega.
+    exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    rewrite in_app. tauto.
+    exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    rewrite in_app. tauto.
+  intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
+    rewrite ZMap.gso. eauto. exploit genv_vars_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. 
+  intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
+    exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    rewrite in_app. tauto.
+    rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). 
+    rewrite zlt_false. rewrite in_app. simpl; right; left. congruence.
+    subst b. rewrite mge_next0. omega.
+    exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    rewrite in_app. tauto.
+Qed.
+
+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. 
-    intros. replace (new_vars ++ a :: vl) with ((new_vars ++ (a::nil)) ++ vl) 
-       by (rewrite app_ass; auto). 
-     apply IHvl. destruct a. apply add_variable_augment_match. auto.
+    intros. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass.
+      apply IHgl. apply add_global_augment_match. auto.
 Qed.
 
-Variable new_functs : list (ident * B).
-Variable new_vars : list (ident * globvar W).
+Variable new_globs : list (ident * globdef B W).
 Variable new_main : ident.
 
 Variable p: program A V.
 Variable p': program B W.
 Hypothesis progmatch: 
-  match_program match_fun match_varinfo new_functs new_vars new_main p p'.
+  match_program match_fun match_varinfo new_globs new_main p p'.
 
 Lemma globalenvs_match:
-  match_genvs new_functs new_vars (globalenv p) (globalenv p').
-Proof.
-  unfold globalenv. destruct progmatch. clear progmatch.
-  destruct H as [tfuncts [P1 P2]]. destruct H0.  clear H0. destruct H as [tvars [Q1 Q2]]. 
-  rewrite P2.  rewrite Q2. clear P2 Q2.
-  rewrite add_variables_app. 
-  rewrite add_functions_app. 
-  pattern new_vars at 1. replace new_vars with (nil++new_vars) by auto.
-  apply add_variables_augment_match.
-  apply add_variables_match; auto. 
-  pattern new_functs at 1. replace new_functs with (nil++new_functs) by auto. 
-  apply add_functions_augment_match.
-  apply add_functions_match; auto. 
+  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. 
+  apply add_globals_augment_match.
+  apply add_globals_match; auto.
   constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence.
 Qed.
 
@@ -1544,10 +1430,10 @@ 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 zlt (genv_nextfun (globalenv p)) b then 
+  if zlt b (genv_next (globalenv p)) then 
       exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf
   else 
-      In tf (map (@snd ident B) new_functs).
+      In (Gfun tf) (map snd new_globs).
 Proof (mge_rev_funs globalenvs_match).
 
 Theorem find_funct_match:
@@ -1565,13 +1451,13 @@ 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) 
-  \/ (In tf (map (@snd ident B) new_functs)).
+  \/ (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. 
   rewrite find_funct_find_funct_ptr.
   apply find_funct_ptr_rev_match in H. 
-   destruct (zlt (genv_nextfun (globalenv p)) b); intuition. 
+   destruct (zlt b (genv_next (globalenv p))); auto.
 Qed.
 
 Theorem find_var_info_match:
@@ -1584,23 +1470,23 @@ 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 zlt b (genv_nextvar (globalenv p)) then 
+  if zlt b (genv_next (globalenv p)) then 
     exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv
   else
-    In tv (map (@snd ident (globvar W)) new_vars).  
+    In (Gvar tv) (map snd new_globs).
 Proof (mge_rev_vars globalenvs_match).
 
 Theorem find_symbol_match:
   forall (s : ident),
-  ~In s (funct_names new_functs ++ var_names new_vars) -> 
+  ~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. 
 Qed.
 
 Hypothesis new_ids_fresh : 
-  (forall s', find_symbol (globalenv p) s' <> None  -> 
-             ~In s' (funct_names new_functs ++ var_names new_vars)).
+  forall s', find_symbol (globalenv p) s' <> None  -> 
+             ~In s' (map fst new_globs).
 
 Lemma store_init_data_list_match:
   forall idl m b ofs m',
@@ -1611,46 +1497,43 @@ Proof.
   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. 
-     inversion H.  case_eq (find_symbol (globalenv p) i). 
-       intros. apply new_ids_fresh. intro. rewrite H0 in H2; inversion H2. 
-       intro. rewrite H0 in H1. inversion H1. 
+   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.
   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_variables_match:
-  forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
+Lemma alloc_globals_match:
+  forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 ->
   forall m m',
-  alloc_variables (globalenv p) m vl1 = Some m' -> 
-  alloc_variables (globalenv p') m vl2 = Some m'.
+  alloc_globals (globalenv p) m gl1 = Some m' -> 
+  alloc_globals (globalenv p') m gl2 = Some m'.
 Proof.
-  induction 1; intros until m'; simpl.
+  induction 1; simpl; intros.
   auto.
-  inv H. 
-  unfold alloc_variable; simpl. 
-  destruct (Mem.alloc m 0 (init_data_list_size init)). 
-  destruct (store_zeros m0 b (init_data_list_size init)); auto. 
-  case_eq (store_init_data_list (globalenv p) m1 b 0 init); intros m2 P. 
-  rewrite (store_init_data_list_match _ _ _ _ P). 
-  change (perm_globvar (mkglobvar info2 init ro vo))
-    with (perm_globvar (mkglobvar info1 init ro vo)).
-  destruct (Mem.drop_perm m2 b 0 (init_data_list_size init)
-    (perm_globvar (mkglobvar info1 init ro vo))); auto. 
-  inversion P. 
+  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 *. 
+    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. 
+  rewrite H2. eauto.
 Qed.
 
 Theorem init_mem_match:
   forall m, init_mem p = Some m -> 
-  init_mem p' = alloc_variables (globalenv p') m new_vars.
+  init_mem p' = alloc_globals (globalenv p') m new_globs.
 Proof.
-  unfold init_mem. destruct progmatch. destruct H0.  destruct H0 as [tvars [P1 P2]].
-  rewrite P2. 
-  intros. 
-  erewrite <- alloc_variables_app; eauto. 
-  eapply alloc_variables_match; eauto. 
+  unfold init_mem; intros.
+  destruct progmatch as [[tglob [P Q]] R].
+  rewrite Q. erewrite <- alloc_globals_app; eauto. 
+  eapply alloc_globals_match; eauto. 
 Qed.
 
 End MATCH_PROGRAMS.
@@ -1661,21 +1544,20 @@ Variable A B V W: Type.
 Variable transf_fun: A -> res B.
 Variable transf_var: V -> res W.
 
-Variable new_functs : list (ident * B).
-Variable new_vars : list (ident * globvar W).
+Variable new_globs : list (ident * globdef B W).
 Variable new_main : ident.
 
 Variable p: program A V.
 Variable p': program B W.
 
 Hypothesis transf_OK:
-  transform_partial_augment_program transf_fun transf_var new_functs new_vars new_main p = OK p'.
+  transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'.
 
 Remark prog_match:
   match_program
     (fun fd tfd => transf_fun fd = OK tfd)
     (fun info tinfo => transf_var info = OK tinfo)
-    new_functs new_vars new_main
+    new_globs new_main
     p p'.
 Proof.
   apply transform_partial_augment_program_match; auto.
@@ -1692,51 +1574,39 @@ Proof.
   intros [tf [X Y]]. exists tf; auto.
 Qed.
 
-
-
-(* This may not yet be in the ideal form for easy use .*)
 Theorem find_new_funct_ptr_exists: 
-  list_norepet (prog_funct_names p ++ funct_names new_functs) ->
-  list_disjoint (prog_funct_names p ++ funct_names new_functs)  (prog_var_names p ++ var_names new_vars) ->
-  forall id f, In (id, f) new_functs -> 
+  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 p. 
-  unfold transform_partial_augment_program in transf_OK. 
-  monadInv transf_OK. rename x into prog_funct'.  rename x0 into prog_vars'. simpl in *.
-  assert (funct_names prog_funct = funct_names prog_funct').
-   clear - EQ.  generalize dependent prog_funct'. induction prog_funct; intros.
-      simpl in EQ. inversion EQ; subst; auto.
-      simpl in EQ. destruct a. destruct (transf_fun a); try discriminate. monadInv EQ.
-      simpl; f_equal; auto.
-  assert (var_names prog_vars = var_names prog_vars').
-   clear - EQ1.  generalize dependent prog_vars'. induction prog_vars; intros.
-      simpl in EQ1. inversion EQ1; subst; auto.
-      simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1.
-      simpl; f_equal; auto.
-  apply find_funct_ptr_exists. 
-  unfold prog_funct_names in *; simpl in *. 
-  rewrite funct_names_app. rewrite <- H2. auto.
-  unfold prog_funct_names, prog_var_names in *; simpl in *.  
-  rewrite funct_names_app. rewrite var_names_app. rewrite <- H2. rewrite <- H3.  auto.
-  simpl. intuition.
+  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 ZMap.gso. auto. 
+  exploit genv_funs_range; eauto. unfold ZIndexed.t; omega.
+  auto. 
+(* ensures *)
+  intros. unfold find_symbol, find_funct_ptr in *; simpl.
+  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
 Qed.
 
 Theorem find_funct_ptr_rev_transf_augment:
   forall (b: block) (tf: B),
   find_funct_ptr (globalenv p') b = Some tf ->
-  if (zlt (genv_nextfun (globalenv p)) b) then
+  if zlt b (genv_next (globalenv p)) then
    (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf)
   else 
-   In tf (map (@snd ident B) new_functs).
+   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. eexact prog_match; eauto. auto. 
 Qed.
 
-
 Theorem find_funct_transf_augment:
   forall (v: val) (f: A),
   find_funct (globalenv p) v = Some f ->
@@ -1744,15 +1614,14 @@ Theorem find_funct_transf_augment:
   find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
 Proof.
   intros. 
-  exploit find_funct_match. eexact prog_match. eauto. 
-  intros [tf [X Y]]. exists tf; auto.
+  exploit find_funct_match. eexact prog_match. eauto. auto. 
 Qed.
 
 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 tf (map (@snd ident B) new_functs). 
+  In (Gfun tf) (map snd new_globs).
 Proof.
   intros. 
   exploit find_funct_rev_match. eexact prog_match. eauto. auto. 
@@ -1765,65 +1634,49 @@ Theorem find_var_info_transf_augment:
   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]]. exists tv; split; auto. inv Y. unfold transf_globvar; simpl.
+  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.
 
 Theorem find_new_var_exists:
-  forall id gv,
-  list_norepet (var_names new_vars) ->
-  In (id, gv) new_vars ->
-  exists b, find_symbol (globalenv p') id = Some b /\ find_var_info (globalenv p') b = Some gv.
-Proof.
-  intros. 
-  assert (P: forall b vars (ge: t B W),
-          ~In id (var_names vars) ->
-          find_symbol ge id = Some b
-          /\ find_var_info ge b = Some gv ->
-          find_symbol (add_variables ge vars) id = Some b
-          /\ find_var_info (add_variables ge vars) b = Some gv).
-  induction vars; simpl; intros. auto. apply IHvars. tauto.
-  destruct a as [id1 gv1]; unfold add_variable, find_symbol, find_var_info; simpl in *.
-  destruct H2; split. rewrite PTree.gso. auto. intuition. 
-  rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
-
-  assert (Q: forall vars (ge: t B W),
-          list_norepet (var_names vars) ->
-          In (id, gv) vars ->
-          exists b, find_symbol (add_variables ge vars) id = Some b
-                 /\ find_var_info (add_variables ge vars) b = Some gv).
-    induction vars; simpl; intros.
-    contradiction.
-    destruct a as [id1 gv1]; simpl in *. inv H1. destruct H2. inv H1. 
-    exists (genv_nextvar ge). apply P; auto. 
-    unfold add_variable, find_symbol, find_var_info; simpl in *.
-    split. apply PTree.gss. apply ZMap.gss. 
-    apply IHvars; auto. 
-
-  unfold transform_partial_augment_program in transf_OK. 
-  monadInv transf_OK. rename x into prog_funct'.  rename x0 into prog_vars'. simpl in *.
-  unfold globalenv; simpl. repeat rewrite add_variables_app. apply Q; auto.
+  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 ZMap.gso. auto. 
+  exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
+(* ensures *)
+  intros. unfold find_symbol, find_var_info in *; simpl.
+  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
 Qed.
 
 Theorem find_var_info_rev_transf_augment:
   forall (b: block) (v': globvar W),
   find_var_info (globalenv p') b = Some v' ->
-  if zlt b (genv_nextvar (globalenv p)) then
+  if zlt b (genv_next (globalenv p)) then
     (exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v')
   else
-    (In v' (map (@snd ident (globvar W)) new_vars)).
+    (In (Gvar v') (map snd new_globs)).
 Proof.
   intros. 
   exploit find_var_info_rev_match. eexact prog_match. eauto.
-  destruct (zlt b (genv_nextvar (globalenv p))); auto.
+  destruct (zlt b (genv_next (globalenv p))); auto.
   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), 
-  ~ In s (funct_names new_functs ++ var_names new_vars) -> 
+  ~ 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.
@@ -1831,16 +1684,16 @@ Qed.
 
 Theorem init_mem_transf_augment: 
    (forall s', find_symbol (globalenv p) s' <> None -> 
-     ~ In s' (funct_names new_functs ++ var_names new_vars)) -> 
+     ~ In s' (map fst new_globs)) ->
    forall m, init_mem p = Some m -> 
-   init_mem p' = alloc_variables (globalenv p') m new_vars.
+   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 s', find_symbol (globalenv p) s' <> None -> 
-     ~ In s' (funct_names new_functs ++ var_names new_vars)) -> 
+     ~ 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'.
@@ -1848,10 +1701,9 @@ Proof.
   intros. 
   pose proof (initmem_inject p H0). 
   erewrite init_mem_transf_augment in H1; eauto. 
-  eapply alloc_variables_augment; eauto. omega.
+  eapply alloc_globals_augment; eauto. omega.
 Qed.
 
-
 End TRANSF_PROGRAM_AUGMENT.
 
 Section TRANSF_PROGRAM_PARTIAL2.
@@ -1865,13 +1717,9 @@ Hypothesis transf_OK:
   transform_partial_program2 transf_fun transf_var p = OK p'.
 
 Remark transf_augment_OK:
-  transform_partial_augment_program transf_fun transf_var nil nil p.(prog_main) p = OK p'.
+  transform_partial_augment_program transf_fun transf_var nil p.(prog_main) p = OK p'.
 Proof.
-  rewrite <- transf_OK. 
-  unfold transform_partial_augment_program, transform_partial_program2. 
-  destruct (map_partial prefix_name transf_fun (prog_funct p)); auto. simpl. 
-  destruct (map_partial prefix_name (transf_globvar transf_var) (prog_vars p)); simpl. 
-  repeat rewrite app_nil_r. auto. auto.
+  rewrite <- transf_OK. apply symmetry. apply transform_partial_program2_augment.
 Qed.
 
 Theorem find_funct_ptr_transf_partial2:
@@ -1880,7 +1728,7 @@ Theorem find_funct_ptr_transf_partial2:
   exists f',
   find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
 Proof.
-  exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
 Qed.
 
 Theorem find_funct_ptr_rev_transf_partial2:
@@ -1888,9 +1736,9 @@ Theorem find_funct_ptr_rev_transf_partial2:
   find_funct_ptr (globalenv p') b = Some tf ->
   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).
+  pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
   intros.  pose proof (H b tf H0). 
-  destruct (zlt (genv_nextfun (globalenv p)) b).  auto. inversion H1. 
+  destruct (zlt b (genv_next (globalenv p))).  auto. contradiction.
 Qed.
 
 Theorem find_funct_transf_partial2:
@@ -1899,7 +1747,7 @@ Theorem find_funct_transf_partial2:
   exists f',
   find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
 Proof.
-  exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
 Qed.
 
 Theorem find_funct_rev_transf_partial2:
@@ -1907,9 +1755,9 @@ Theorem find_funct_rev_transf_partial2:
   find_funct (globalenv p') v = Some tf ->
   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).
+  pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
   intros. pose proof (H v tf H0). 
-  destruct H1. auto. inversion H1. 
+  destruct H1. auto. contradiction.
 Qed.
 
 Theorem find_var_info_transf_partial2:
@@ -1918,7 +1766,7 @@ Theorem find_var_info_transf_partial2:
   exists v',
   find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
 Proof.
-  exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
 Qed.
 
 Theorem find_var_info_rev_transf_partial2:
@@ -1927,23 +1775,23 @@ Theorem find_var_info_rev_transf_partial2:
   exists v,
   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).
+  pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
   intros.  pose proof (H b v' H0). 
-  destruct (zlt b (genv_nextvar (globalenv p))).  auto. inversion H1. 
+  destruct (zlt b (genv_next (globalenv p))).  auto. contradiction.
 Qed.
 
 Theorem find_symbol_transf_partial2:
   forall (s: ident),
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
 Proof.
-  pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
+  pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
   auto.
 Qed.
 
 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).
+  pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
   intros. simpl in H. apply H; auto.  
 Qed.
 
@@ -1957,24 +1805,13 @@ Variable p: program A V.
 Variable p': program B V.
 Hypothesis transf_OK: transform_partial_program transf p = OK p'.
 
-Remark transf2_OK:
-  transform_partial_program2 transf (fun x => OK x) p = OK p'.
-Proof.
-  rewrite <- transf_OK. 
-  unfold transform_partial_program2, transform_partial_program.
-  destruct (map_partial prefix_name transf (prog_funct p)); auto.
-  simpl. replace (transf_globvar (fun (x : V) => OK x)) with (fun (v: globvar V) => OK v).
-  rewrite map_partial_identity; auto.
-  apply extensionality; intros. destruct x; auto.
-Qed.
-
 Theorem find_funct_ptr_transf_partial:
   forall (b: block) (f: A),
   find_funct_ptr (globalenv p) b = Some f ->
   exists f',
   find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.
 Proof.
-  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
 Qed.
 
 Theorem find_funct_ptr_rev_transf_partial:
@@ -1982,7 +1819,7 @@ Theorem find_funct_ptr_rev_transf_partial:
   find_funct_ptr (globalenv p') b = Some tf ->
   exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.
 Proof.
-  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
 Qed.
 
 Theorem find_funct_transf_partial:
@@ -1991,7 +1828,7 @@ Theorem find_funct_transf_partial:
   exists f',
   find_funct (globalenv p') v = Some f' /\ transf f = OK f'.
 Proof.
-  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
 Qed.
 
 Theorem find_funct_rev_transf_partial:
@@ -1999,14 +1836,14 @@ Theorem find_funct_rev_transf_partial:
   find_funct (globalenv p') v = Some tf ->
   exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf.
 Proof.
-  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
 Qed.
 
 Theorem find_symbol_transf_partial:
   forall (s: ident),
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
 Proof.
-  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
 Qed.
 
 Theorem find_var_info_transf_partial:
@@ -2014,10 +1851,10 @@ 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 transf2_OK. eauto. 
+  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 transf2_OK. eauto.
+  exploit find_var_info_rev_transf_partial2. eexact transf_OK. eauto.
   intros [v' [P Q]]. monadInv Q. inv EQ. congruence. 
   auto.
 Qed.
@@ -2025,7 +1862,7 @@ Qed.
 Theorem init_mem_transf_partial:
   forall m, init_mem p = Some m -> init_mem p' = Some m.
 Proof.
-  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
 Qed.
 
 End TRANSF_PROGRAM_PARTIAL.
@@ -2040,8 +1877,7 @@ Let tp := transform_program transf p.
 Remark transf_OK:
   transform_partial_program (fun x => OK (transf x)) p = OK tp.
 Proof.
-  unfold tp, transform_program, transform_partial_program.
-  rewrite map_partial_total. reflexivity.
+  unfold tp. apply transform_program_partial_program. 
 Qed.
 
 Theorem find_funct_ptr_transf: