Verification of the Unusedglob pass (removal of unreferenced static global definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.

1 files changed, 1256 insertions, 0 deletions

diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
new file mode 100644
index 00000000..5be9344f
--- /dev/null
+++ b/backend/Unusedglobproof.v
@@ -0,0 +1,1256 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Elimination of unreferenced static definitions *)
+
+Require Import FSets.
+Require Import Coqlib.
+Require Import Ordered.
+Require Import Maps.
+Require Import Iteration.
+Require Import AST.
+Require Import Errors.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Unusedglob.
+
+Module ISF := FSetFacts.Facts(IS).
+Module ISP := FSetProperties.Properties(IS).
+
+(** * Properties of the analysis *)
+
+(** Monotonic evolution of the workset. *)
+
+Inductive workset_incl (w1 w2: workset) : Prop := 
+  workset_incl_intro:
+    forall (SEEN: IS.Subset w1.(w_seen) w2.(w_seen))
+           (TODO: List.incl w1.(w_todo) w2.(w_todo))
+           (TRACK: forall id, IS.In id w2.(w_seen) ->
+                      IS.In id w1.(w_seen) \/ List.In id w2.(w_todo)),
+    workset_incl w1 w2.
+
+Lemma seen_workset_incl:
+  forall w1 w2 id, workset_incl w1 w2 -> IS.In id w1 -> IS.In id w2.
+Proof.
+  intros. destruct H. auto.
+Qed.
+
+Lemma workset_incl_refl: forall w, workset_incl w w.
+Proof.
+  intros; split. red; auto. red; auto. auto. 
+Qed.
+
+Lemma workset_incl_trans:
+  forall w1 w2 w3, workset_incl w1 w2 -> workset_incl w2 w3 -> workset_incl w1 w3.
+Proof.
+  intros. destruct H, H0; split.
+  red; eauto.
+  red; eauto.
+  intros. edestruct TRACK0; eauto. edestruct TRACK; eauto. 
+Qed.
+
+Lemma add_workset_incl:
+  forall id w, workset_incl w (add_workset id w).
+Proof.
+  unfold add_workset; intros. destruct (IS.mem id w) eqn:MEM.
+- apply workset_incl_refl.
+- split; simpl.
+  + red; intros. apply IS.add_2; auto.
+  + red; simpl; auto.
+  + intros. destruct (ident_eq id id0); auto. apply IS.add_3 in H; auto. 
+Qed.
+
+Lemma addlist_workset_incl:
+  forall l w, workset_incl w (addlist_workset l w).
+Proof.
+  induction l; simpl; intros. 
+  apply workset_incl_refl.
+  eapply workset_incl_trans. apply add_workset_incl. eauto.
+Qed.
+
+Lemma add_ref_function_incl:
+  forall f w, workset_incl w (add_ref_function f w).
+Proof.
+  unfold add_ref_function; intros. apply PTree_Properties.fold_rec.
+- auto.
+- apply workset_incl_refl.
+- intros. apply workset_incl_trans with a; auto. 
+  unfold add_ref_instruction. apply addlist_workset_incl.
+Qed.
+
+Lemma add_ref_globvar_incl:
+  forall gv w, workset_incl w (add_ref_globvar gv w).
+Proof.
+  unfold add_ref_globvar; intros. 
+  revert w. induction (gvar_init gv); simpl; intros.
+  apply workset_incl_refl.
+  eapply workset_incl_trans; [ | eauto ].
+  unfold add_ref_init_data.
+  destruct a; (apply workset_incl_refl || apply add_workset_incl).
+Qed.
+
+Lemma add_ref_definition_incl:
+  forall pm id w, workset_incl w (add_ref_definition pm id w).
+Proof.
+  unfold add_ref_definition; intros. 
+  destruct (pm!id) as [[[] | ? ] | ].
+  apply add_ref_function_incl.
+  apply addlist_workset_incl. 
+  apply add_ref_globvar_incl.
+  apply workset_incl_refl.
+Qed.
+
+Lemma initial_workset_incl:
+  forall p, workset_incl {| w_seen := IS.empty; w_todo := nil |} (initial_workset p).
+Proof.
+  unfold initial_workset; intros.
+  eapply workset_incl_trans. 2: apply add_workset_incl. 
+  generalize {| w_seen := IS.empty; w_todo := nil |}. induction (prog_public p); simpl; intros.
+  apply workset_incl_refl.
+  eapply workset_incl_trans. eapply add_workset_incl. eapply IHl. 
+Qed.
+
+(** Soundness properties for functions that add identifiers to the workset *)
+
+Lemma seen_add_workset:
+  forall id (w: workset), IS.In id (add_workset id w).
+Proof.
+  unfold add_workset; intros.
+  destruct (IS.mem id w) eqn:MEM.
+  apply IS.mem_2; auto.
+  simpl. apply IS.add_1; auto.
+Qed.
+
+Lemma seen_addlist_workset:
+  forall id l (w: workset),
+  In id l -> IS.In id (addlist_workset l w).
+Proof.
+  induction l; simpl; intros. 
+  tauto.
+  destruct H. subst a.
+  eapply seen_workset_incl. apply addlist_workset_incl. apply seen_add_workset.
+  apply IHl; auto.
+Qed.
+
+Definition ref_function (f: function) (id: ident) : Prop :=
+  exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i).
+
+Lemma seen_add_ref_function:
+  forall id f w,
+  ref_function f id -> IS.In id (add_ref_function f w).
+Proof.
+  intros until w. unfold ref_function, add_ref_function. apply PTree_Properties.fold_rec; intros.
+- destruct H1 as (pc & i & A & B). apply H0; auto. exists pc, i; split; auto. rewrite H; auto.
+- destruct H as (pc & i & A & B). rewrite PTree.gempty in A; discriminate.
+- destruct H2 as (pc & i & A & B). rewrite PTree.gsspec in A. destruct (peq pc k).
+  + inv A. unfold add_ref_instruction. apply seen_addlist_workset; auto. 
+  + unfold add_ref_instruction. eapply seen_workset_incl. apply addlist_workset_incl. 
+    apply H1. exists pc, i; auto. 
+Qed.
+
+Definition ref_fundef (fd: fundef) (id: ident) : Prop :=
+  match fd with Internal f => ref_function f id | External ef => In id (globals_external ef) end.
+
+Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop :=
+  match gd with
+  | Gfun fd => ref_fundef fd id
+  | Gvar gv => exists ofs, List.In (Init_addrof id ofs) gv.(gvar_init)
+  end.
+
+Lemma seen_add_ref_definition:
+  forall pm id gd id' w,
+  pm!id = Some gd -> ref_def gd id' -> IS.In id' (add_ref_definition pm id w).
+Proof.
+  unfold add_ref_definition; intros. rewrite H. red in H0; destruct gd as [[f|ef]|gv].
+  apply seen_add_ref_function; auto.
+  apply seen_addlist_workset; auto.
+  destruct H0 as (ofs & IN).
+  unfold add_ref_globvar.
+  assert (forall l (w: workset),
+          IS.In id' w \/ In (Init_addrof id' ofs) l ->
+          IS.In id' (fold_left add_ref_init_data l w)).
+  {
+    induction l; simpl; intros. 
+    tauto.
+    apply IHl. intuition auto.
+    left. destruct a; simpl; auto. eapply seen_workset_incl. apply add_workset_incl. auto. 
+    subst; left; simpl. apply seen_add_workset.
+  }
+  apply H0; auto. 
+Qed.
+
+Lemma seen_main_initial_workset:
+  forall p, IS.In p.(prog_main) (initial_workset p).
+Proof.
+  unfold initial_workset; intros. apply seen_add_workset. 
+Qed.
+
+Lemma seen_public_initial_workset:
+  forall p id, In id p.(prog_public) -> IS.In id (initial_workset p).
+Proof.
+  intros. unfold initial_workset. eapply seen_workset_incl. apply add_workset_incl. 
+  assert (forall l (w: workset),
+          IS.In id w \/ In id l -> IS.In id (fold_left (fun w id => add_workset id w) l w)).
+  {
+    induction l; simpl; intros.
+    tauto.
+    apply IHl. intuition auto; left.
+    eapply seen_workset_incl. apply add_workset_incl. auto. 
+    subst a. apply seen_add_workset. 
+  }
+  apply H0. auto. 
+Qed.
+
+(** * Semantic preservation *)
+
+Section SOUNDNESS.
+Variable p: program.
+Variable tp: program.
+Hypothesis TRANSF: transform_program p = OK tp.
+Let ge := Genv.globalenv p.
+Let tge := Genv.globalenv tp.
+
+Let pm := program_map p.
+
+
+(** Correctness of the dependency graph traversal. *)
+
+Definition workset_invariant (w: workset) : Prop :=
+  forall id gd id',
+  IS.In id w -> ~List.In id (w_todo w) -> pm!id = Some gd -> ref_def gd id' ->
+  IS.In id' w.
+
+Definition used_set_closed (u: IS.t) : Prop :=
+  forall id gd id',
+  IS.In id u -> pm!id = Some gd -> ref_def gd id' -> IS.In id' u.
+
+Lemma iter_step_invariant:
+  forall w,
+  workset_invariant w ->
+  match iter_step pm w with
+  | inl u => used_set_closed u
+  | inr w' => workset_invariant w'
+  end.
+Proof.
+  unfold iter_step, workset_invariant, used_set_closed; intros. 
+  destruct (w_todo w) as [ | id rem ]; intros.
+- eapply H; eauto.
+- set (w' := {| w_seen := w.(w_seen); w_todo := rem |}) in *.
+  destruct (add_ref_definition_incl pm id w').
+  destruct (ident_eq id id0).
+  + subst id0. eapply seen_add_ref_definition; eauto. 
+  + exploit TRACK; eauto. intros [A|A].
+    * apply SEEN. eapply H; eauto. simpl. 
+      assert (~ In id0 rem). 
+      { change rem with (w_todo w'). red; intros. elim H1; auto. }
+      tauto.
+    * contradiction.
+Qed.
+
+Theorem used_globals_sound:
+  forall u, used_globals p = Some u -> used_set_closed u.
+Proof.
+  unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := workset_invariant); eauto.
+- intros. apply iter_step_invariant; auto. 
+- destruct (initial_workset_incl p). 
+  red; intros. edestruct TRACK; eauto. 
+  simpl in H4. eelim IS.empty_1; eauto. 
+  contradiction.
+Qed.
+
+Theorem used_globals_incl:
+  forall u, used_globals p = Some u -> IS.Subset (initial_workset p) u.
+Proof.
+  unfold used_globals; intros.
+  eapply PrimIter.iterate_prop with (P := fun (w: workset) => IS.Subset (initial_workset p) w); eauto.
+- fold pm; unfold iter_step; intros. destruct (w_todo a) as [ | id rem ].
+  auto.
+  destruct (add_ref_definition_incl pm id {| w_seen := a; w_todo := rem |}).
+  red; auto.
+- red; auto.
+Qed.
+
+Definition used: IS.t := 
+  match used_globals p with Some u => u | None => IS.empty end.
+
+Remark USED_GLOBALS: used_globals p = Some used.
+Proof.
+  unfold used. unfold transform_program in TRANSF. destruct (used_globals p). auto. discriminate.
+Qed.
+
+Definition kept (id: ident) : Prop := IS.In id used.
+
+Theorem kept_closed:
+  forall id gd id',
+  kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'.
+Proof.
+  intros. assert (UC: used_set_closed used) by (apply used_globals_sound; apply USED_GLOBALS).
+  eapply UC; eauto.
+Qed.
+
+Theorem kept_main:
+  kept p.(prog_main).
+Proof.
+  unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_main_initial_workset.
+Qed.
+
+Theorem kept_public:
+  forall id, In id p.(prog_public) -> kept id.
+Proof.
+  intros. unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_public_initial_workset; auto.
+Qed.
+
+Remark filter_globdefs_accu:
+  forall defs accu1 accu2 u,
+  filter_globdefs u (accu1 ++ accu2) defs = filter_globdefs u accu1 defs ++ accu2.
+Proof.
+  induction defs; simpl; intros.
+  auto.
+  destruct a as [id gd]. destruct (IS.mem id u); auto. 
+  rewrite <- IHdefs. auto.
+Qed.
+
+Remark filter_globdefs_nil:
+  forall u accu defs,
+  filter_globdefs u accu defs = filter_globdefs u nil defs ++ accu.
+Proof.
+  intros. rewrite <- filter_globdefs_accu. auto. 
+Qed.
+
+Theorem transform_program_charact:
+  forall id, (program_map tp)!id = if IS.mem id used then pm!id else None.
+Proof.
+  intros. 
+  assert (X: forall l u m1 m2,
+             IS.In id u ->
+             m1!id = m2!id ->
+             (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id =
+             (fold_left add_def_prog_map (List.rev l) m2)!id).
+  {
+    induction l; simpl; intros. 
+    auto.
+    destruct a as [id1 gd1]. rewrite fold_left_app. simpl. 
+    destruct (IS.mem id1 u) eqn:MEM.
+    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. 
+    unfold add_def_prog_map at 1 3. simpl. 
+    rewrite ! PTree.gsspec. destruct (peq id id1). auto.
+    apply IHl; auto. apply IS.remove_2; auto. 
+    unfold add_def_prog_map at 2. simpl. rewrite PTree.gso. apply IHl; auto. 
+    red; intros; subst id1.
+    assert (IS.mem id u = true) by (apply IS.mem_1; auto). congruence.
+  }
+  assert (Y: forall l u m1,
+             IS.mem id u = false ->
+             m1!id = None ->
+             (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = None).
+  {
+    induction l; simpl; intros.
+    auto.
+    destruct a as [id1 gd1].
+    destruct (IS.mem id1 u) eqn:MEM.
+    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. 
+    unfold add_def_prog_map at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto.
+    rewrite ISF.remove_b. rewrite H; auto. 
+    eapply IHl; eauto.
+  }
+  unfold pm, program_map.
+  unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF. inversion TRANSF.
+  simpl. destruct (IS.mem id used) eqn: MEM.
+  erewrite X. rewrite List.rev_involutive. eauto. apply IS.mem_2; auto. auto.
+  apply Y. auto. apply PTree.gempty.
+Qed.
+
+(** Program map and Genv operations *)
+
+Definition genv_progmap_match (ge: genv) (pm: prog_map) : Prop :=
+  forall id,
+  match Genv.find_symbol ge id with
+  | None => pm!id = None
+  | Some b =>
+      match pm!id with
+      | None => False
+      | Some (Gfun fd) => Genv.find_funct_ptr ge b = Some fd
+      | Some (Gvar gv) => Genv.find_var_info ge b = Some gv
+      end
+  end.
+
+Lemma genv_program_map:
+  forall p, genv_progmap_match (Genv.globalenv p) (program_map p).
+Proof.
+  intros. unfold Genv.globalenv, program_map. 
+  assert (REC: forall defs g m, 
+               genv_progmap_match g m ->
+               genv_progmap_match (Genv.add_globals g defs) (fold_left add_def_prog_map defs m)).
+  {
+    induction defs; simpl; intros.
+    auto.
+    apply IHdefs. red; intros. specialize (H id).
+    destruct a as [id1 [fd|gv]];
+    unfold Genv.add_global, Genv.find_symbol, Genv.find_funct_ptr, Genv.find_var_info, add_def_prog_map in *;
+    simpl.
+  - rewrite PTree.gsspec. destruct (peq id id1); subst.
+    + rewrite ! PTree.gss. auto.
+    + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto.
+      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. 
+      * auto.
+  - rewrite PTree.gsspec. destruct (peq id id1); subst.
+    + rewrite ! PTree.gss. auto.
+    + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto.
+      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. 
+      * auto.
+  }
+  apply REC. red; intros. unfold Genv.find_symbol, Genv.empty_genv; simpl. rewrite ! PTree.gempty; auto.
+Qed.
+
+Lemma transform_program_kept:
+  forall id b, Genv.find_symbol tge id = Some b -> kept id.
+Proof.
+  intros. generalize (genv_program_map tp id). fold tge; rewrite H. 
+  rewrite transform_program_charact. intros. destruct (IS.mem id used) eqn:U.
+  unfold kept; apply IS.mem_2; auto.
+  contradiction.
+Qed.
+
+(** Injections that preserve used globals. *)
+
+Record meminj_preserves_globals (f: meminj) : Prop := {
+  symbols_inject_1: forall id b b' delta,
+    f b = Some(b', delta) -> Genv.find_symbol ge id = Some b ->
+    delta = 0 /\ Genv.find_symbol tge id = Some b';
+  symbols_inject_2: forall id b,
+    kept id -> Genv.find_symbol ge id = Some b ->
+    exists b', Genv.find_symbol tge id = Some b' /\ f b = Some(b', 0);
+  symbols_inject_3: forall id b',
+    Genv.find_symbol tge id = Some b' ->
+    exists b, Genv.find_symbol ge id = Some b /\ f b = Some(b', 0);
+  funct_ptr_inject: forall b b' delta fd,
+    f b = Some(b', delta) -> Genv.find_funct_ptr ge b = Some fd ->
+    Genv.find_funct_ptr tge b' = Some fd /\ delta = 0 /\
+    (forall id, ref_fundef fd id -> kept id);
+  var_info_inject: forall b b' delta gv,
+    f b = Some(b', delta) -> Genv.find_var_info ge b = Some gv ->
+    Genv.find_var_info tge b' = Some gv /\ delta = 0;
+  var_info_rev_inject: forall b b' delta gv,
+    f b = Some(b', delta) -> Genv.find_var_info tge b' = Some gv ->
+    Genv.find_var_info ge b = Some gv /\ delta = 0
+}.
+
+Definition init_meminj : meminj :=
+  fun b =>
+    match Genv.invert_symbol ge b with
+    | Some id => 
+        match Genv.find_symbol tge id with
+        | Some b' => Some (b', 0)
+        | None => None
+        end
+    | None => None
+    end.
+
+Remark init_meminj_invert:
+  forall b b' delta,
+  init_meminj b = Some(b', delta) ->
+  delta = 0 /\ exists id, Genv.find_symbol ge id = Some b /\ Genv.find_symbol tge id = Some b'.
+Proof.
+  unfold init_meminj; intros.
+  destruct (Genv.invert_symbol ge b) as [id|] eqn:S; try discriminate.
+  destruct (Genv.find_symbol tge id) as [b''|] eqn:F; inv H.
+  split. auto. exists id. split. apply Genv.invert_find_symbol; auto. auto.
+Qed. 
+
+Lemma init_meminj_preserves_globals:
+  meminj_preserves_globals init_meminj.
+Proof.
+  constructor; intros.
+- exploit init_meminj_invert; eauto. intros (A & id1 & B & C).
+  assert (id1 = id) by (eapply (Genv.genv_vars_inj ge); eauto). subst id1.
+  auto.
+- unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. apply IS.mem_1 in H.
+  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
+  rewrite transform_program_charact. rewrite H, H0.
+  destruct (Genv.find_symbol tge id) as [b'|]; intros.
+  exists b'; auto. rewrite H2 in H1; contradiction.
+- generalize (genv_program_map tp id). fold tge. rewrite H. intros.
+  destruct (program_map tp)!id as [gd|] eqn:PM; try contradiction.
+  generalize (transform_program_charact id). rewrite PM. 
+  destruct (IS.mem id used) eqn:USED; intros; try discriminate.
+  generalize (genv_program_map p id). fold ge; fold pm.
+  destruct (Genv.find_symbol ge id) as [b|] eqn:FS; intros; try congruence.
+  exists b; split; auto. unfold init_meminj. 
+  erewrite Genv.find_invert_symbol by eauto. rewrite H. auto.
+- exploit init_meminj_invert; eauto. intros (A & id & B & C).
+  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
+  rewrite transform_program_charact. rewrite B, C. intros.
+  destruct (IS.mem id used) eqn:KEPT; try contradiction.
+  destruct (pm!id) as [gd|] eqn:PM; try contradiction. 
+  destruct gd as [fd'|gv'].
+  + assert (fd' = fd) by congruence. subst fd'. split. auto. split. auto. 
+    intros. eapply kept_closed; eauto. red; apply IS.mem_2; auto. 
+  + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence.
+- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto.
+  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
+  rewrite transform_program_charact. rewrite B, C. intros.
+  destruct (IS.mem id used); try contradiction.
+  destruct (pm!id) as [gd|]; try contradiction. 
+  destruct gd as [fd'|gv']. 
+  + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence.
+  + congruence.
+- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto.
+  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
+  rewrite transform_program_charact. rewrite B, C. intros.
+  destruct (IS.mem id used); try contradiction.
+  destruct (pm!id) as [gd|]; try contradiction. 
+  destruct gd as [fd'|gv']. 
+  + assert (b' <> b') by (eapply Genv.genv_funs_vars; eassumption). congruence.
+  + congruence.
+Qed.
+
+Lemma globals_symbols_inject:
+  forall j, meminj_preserves_globals j -> symbols_inject j ge tge.
+Proof.
+  intros. 
+  assert (E1: Genv.genv_public ge = p.(prog_public)).
+  { apply Genv.globalenv_public. }
+  assert (E2: Genv.genv_public tge = p.(prog_public)).
+  { unfold tge; rewrite Genv.globalenv_public. 
+    unfold transform_program in TRANSF. rewrite USED_GLOBALS in TRANSF. inversion TRANSF. auto. }
+  split; [|split;[|split]]; intros.
+  + unfold Genv.public_symbol; rewrite E1, E2.
+    destruct (Genv.find_symbol tge id) as [b'|] eqn:TFS.
+    exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto. 
+    destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
+    destruct (in_dec ident_eq id (prog_public p)); simpl; auto.
+    exploit symbols_inject_2; eauto. apply kept_public; auto. 
+    intros (b' & TFS' & INJ). congruence.
+  + eapply symbols_inject_1; eauto. 
+  + unfold Genv.public_symbol in H0. 
+    destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
+    rewrite E1 in H0. 
+    destruct (in_dec ident_eq id (prog_public p)); try discriminate. inv H1.
+    exploit symbols_inject_2; eauto. apply kept_public; auto. 
+    intros (b' & A & B); exists b'; auto.
+  + unfold block_is_volatile. 
+    destruct (Genv.find_var_info ge b1) as [gv|] eqn:V1.
+    exploit var_info_inject; eauto. intros [A B]. rewrite A. auto.
+    destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto.
+    exploit var_info_rev_inject; eauto. intros [A B]. congruence.
+Qed.
+
+Lemma symbol_address_inject:
+  forall j id ofs, 
+  meminj_preserves_globals j -> kept id ->
+  val_inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).
+Proof.
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
+  exploit symbols_inject_2; eauto. intros (b' & TFS & INJ). rewrite TFS. 
+  econstructor; eauto. rewrite Int.add_zero; auto.
+Qed. 
+
+(** Semantic preservation *)
+
+Definition regset_inject (f: meminj) (rs rs': regset): Prop :=
+  forall r, val_inject f rs#r rs'#r.
+
+Lemma regs_inject:
+  forall f rs rs', regset_inject f rs rs' -> forall l, val_list_inject f rs##l rs'##l.
+Proof.
+  induction l; simpl. constructor. constructor; auto. 
+Qed.
+
+Lemma set_reg_inject:
+  forall f rs rs' r v v',
+  regset_inject f rs rs' -> val_inject f v v' ->
+  regset_inject f (rs#r <- v) (rs'#r <- v').
+Proof.
+  intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto. 
+Qed.
+
+Lemma regset_inject_incr:
+  forall f f' rs rs', regset_inject f rs rs' -> inject_incr f f' -> regset_inject f' rs rs'.
+Proof.
+  intros; red; intros. apply val_inject_incr with f; auto. 
+Qed.
+
+Lemma regset_undef_inject:
+  forall f, regset_inject f (Regmap.init Vundef) (Regmap.init Vundef).
+Proof.
+  intros; red; intros. rewrite Regmap.gi. auto.
+Qed.
+
+Lemma init_regs_inject:
+  forall f args args', val_list_inject f args args' ->
+  forall params,
+  regset_inject f (init_regs args params) (init_regs args' params).
+Proof.
+  induction 1; intros; destruct params; simpl; try (apply regset_undef_inject).
+  apply set_reg_inject; auto. 
+Qed.
+
+Inductive match_stacks (j: meminj):
+        list stackframe -> list stackframe -> block -> block -> Prop :=
+  | match_stacks_nil: forall bound tbound,
+      meminj_preserves_globals j ->
+      Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next tge) tbound ->
+      match_stacks j nil nil bound tbound
+  | match_stacks_cons: forall res f sp pc rs s tsp trs ts bound tbound
+         (STACKS: match_stacks j s ts sp tsp)
+         (KEPT: forall id, ref_function f id -> kept id)
+         (SPINJ: j sp = Some(tsp, 0))
+         (REGINJ: regset_inject j rs trs)
+         (BELOW: Plt sp bound)
+         (TBELOW: Plt tsp tbound),
+      match_stacks j (Stackframe res f (Vptr sp Int.zero) pc rs :: s)
+                     (Stackframe res f (Vptr tsp Int.zero) pc trs :: ts)
+                     bound tbound.
+
+Lemma match_stacks_preserves_globals:
+  forall j s ts bound tbound,
+  match_stacks j s ts bound tbound ->
+  meminj_preserves_globals j.
+Proof.
+  induction 1; auto. 
+Qed.
+
+Lemma match_stacks_incr:
+  forall j j', inject_incr j j' ->
+  forall s ts bound tbound, match_stacks j s ts bound tbound ->
+  (forall b1 b2 delta,
+      j b1 = None -> j' b1 = Some(b2, delta) -> Ple bound b1 /\ Ple tbound b2) ->
+  match_stacks j' s ts bound tbound.
+Proof.
+  induction 2; intros.
+- assert (SAME: forall b b' delta, Plt b (Genv.genv_next ge) ->
+                                   j' b = Some(b', delta) -> j b = Some(b', delta)).
+  { intros. destruct (j b) as [[b1 delta1] | ] eqn: J.
+    exploit H; eauto. congruence. 
+    exploit H3; eauto. intros [A B]. elim (Plt_strict b).
+    eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. }
+  assert (SAME': forall b b' delta, Plt b' (Genv.genv_next tge) ->
+                                   j' b = Some(b', delta) -> j b = Some (b', delta)).
+  { intros. destruct (j b) as [[b1 delta1] | ] eqn: J.
+    exploit H; eauto. congruence.
+    exploit H3; eauto. intros [A B]. elim (Plt_strict b').
+    eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. }
+  constructor; auto.  constructor; intros.
+  + exploit symbols_inject_1; eauto. apply SAME; auto. 
+    eapply Genv.genv_symb_range; eauto. 
+  + exploit symbols_inject_2; eauto. intros (b' & A & B). 
+    exists b'; auto.
+  + exploit symbols_inject_3; eauto. intros (b & A & B).
+    exists b; auto.
+  + eapply funct_ptr_inject; eauto. apply SAME; auto. 
+    eapply Genv.genv_funs_range; eauto.
+  + eapply var_info_inject; eauto. apply SAME; auto. 
+    eapply Genv.genv_vars_range; eauto.
+  + eapply var_info_rev_inject; eauto. apply SAME'; auto. 
+    eapply Genv.genv_vars_range; eauto.
+- econstructor; eauto. 
+  apply IHmatch_stacks.
+  intros. exploit H1; eauto. intros [A B]. split; eapply Ple_trans; eauto.
+  apply Plt_Ple; auto. apply Plt_Ple; auto.
+  apply regset_inject_incr with j; auto.
+Qed.
+
+Lemma match_stacks_bound:
+  forall j s ts bound tbound bound' tbound',
+  match_stacks j s ts bound tbound ->
+  Ple bound bound' -> Ple tbound tbound' ->
+  match_stacks j s ts bound' tbound'.
+Proof.
+  induction 1; intros.
+- constructor; auto. eapply Ple_trans; eauto. eapply Ple_trans; eauto.  
+- econstructor; eauto. eapply Plt_Ple_trans; eauto. eapply Plt_Ple_trans; eauto. 
+Qed.
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_regular: forall s f sp pc rs m ts tsp trs tm j
+         (STACKS: match_stacks j s ts sp tsp)
+         (KEPT: forall id, ref_function f id -> kept id)
+         (SPINJ: j sp = Some(tsp, 0))
+         (REGINJ: regset_inject j rs trs)
+         (MEMINJ: Mem.inject j m tm),
+      match_states (State s f (Vptr sp Int.zero) pc rs m)
+                   (State ts f (Vptr tsp Int.zero) pc trs tm)
+  | match_states_call: forall s fd args m ts targs tm j
+         (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm))
+         (KEPT: forall id, ref_fundef fd id -> kept id)
+         (ARGINJ: val_list_inject j args targs)
+         (MEMINJ: Mem.inject j m tm),
+      match_states (Callstate s fd args m)
+                   (Callstate ts fd targs tm)
+  | match_states_return: forall s res m ts tres tm j
+         (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm))
+         (RESINJ: val_inject j res tres)
+         (MEMINJ: Mem.inject j m tm),
+      match_states (Returnstate s res m)
+                   (Returnstate ts tres tm).
+
+Lemma external_call_inject:
+  forall ef vargs m1 t vres m2 f m1' vargs',
+  meminj_preserves_globals f ->
+  external_call ef ge vargs m1 t vres m2 ->
+  (forall id, In id (globals_external ef) -> kept id) ->
+  Mem.inject f m1 m1' ->
+  val_list_inject f vargs vargs' ->
+  exists f', exists vres', exists m2',
+    external_call ef tge vargs' m1' t vres' m2'
+    /\ val_inject f' vres vres'
+    /\ Mem.inject f' m2 m2'
+    /\ Mem.unchanged_on (loc_unmapped f) m1 m2
+    /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
+    /\ inject_incr f f'
+    /\ inject_separated f f' m1 m1'.
+Proof.
+  intros. eapply external_call_mem_inject_gen; eauto.
+- apply globals_symbols_inject; auto.
+- intros. exploit symbols_inject_2; eauto. 
+  intros (b' & A & B); exists b'; auto.
+Qed.
+
+Lemma find_function_inject:
+  forall j ros rs fd trs,
+  meminj_preserves_globals j ->
+  find_function ge ros rs = Some fd ->
+  match ros with inl r => regset_inject j rs trs | inr id => kept id end ->
+  find_function tge ros trs = Some fd /\ (forall id, ref_fundef fd id -> kept id).
+Proof.
+  intros. destruct ros as [r|id]; simpl in *.
+- exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0. 
+  rewrite Genv.find_funct_find_funct_ptr in H0. 
+  specialize (H1 r). rewrite R in H1. inv H1. 
+  exploit funct_ptr_inject; eauto. intros (A & B & C). 
+  rewrite B; auto.
+- destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
+  exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P. 
+  exploit funct_ptr_inject; eauto. intros (A & B & C). 
+  auto.
+Qed.
+
+Theorem step_simulation:
+  forall S1 t S2, step ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  exists S2', step tge S1' t S2' /\ match_states S2 S2'.
+Proof.
+  induction 1; intros; inv MS.
+
+- (* nop *)
+  econstructor; split. 
+  eapply exec_Inop; eauto. 
+  econstructor; eauto. 
+
+- (* op *)
+  assert (A: exists tv, 
+               eval_operation tge (Vptr tsp Int.zero) op trs##args tm = Some tv
+            /\ val_inject j v tv).
+  { apply eval_operation_inj with (ge1 := ge) (m1 := m) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
+    intros; eapply Mem.valid_pointer_inject_val; eauto.
+    intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+    intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+    intros; eapply Mem.different_pointers_inject; eauto.
+    intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+    apply KEPT. red. exists pc, (Iop op args res pc'); auto.
+    econstructor; eauto. 
+    apply regs_inject; auto.
+    assumption. }
+  destruct A as (tv & B & C).
+  econstructor; split. eapply exec_Iop; eauto.
+  econstructor; eauto. apply set_reg_inject; auto. 
+
+- (* load *)
+  assert (A: exists ta, 
+               eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta
+            /\ val_inject j a ta).
+  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
+    intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+    apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto.
+    econstructor; eauto. 
+    apply regs_inject; auto.
+    assumption. }
+  destruct A as (ta & B & C).
+  exploit Mem.loadv_inject; eauto. intros (tv & D & E).
+  econstructor; split. eapply exec_Iload; eauto.
+  econstructor; eauto. apply set_reg_inject; auto.
+
+- (* store *)
+  assert (A: exists ta, 
+               eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta
+            /\ val_inject j a ta).
+  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
+    intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+    apply KEPT. red. exists pc, (Istore chunk addr args src pc'); auto.
+    econstructor; eauto. 
+    apply regs_inject; auto.
+    assumption. }
+  destruct A as (ta & B & C).
+  exploit Mem.storev_mapped_inject; eauto. intros (tm' & D & E).
+  econstructor; split. eapply exec_Istore; eauto.
+  econstructor; eauto.
+
+- (* call *)
+  exploit find_function_inject. 
+  eapply match_stacks_preserves_globals; eauto. eauto. 
+  destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto.
+  intros (A & B).
+  econstructor; split. eapply exec_Icall; eauto. 
+  econstructor; eauto. 
+  econstructor; eauto.
+  change (Mem.valid_block m sp0). eapply Mem.valid_block_inject_1; eauto. 
+  change (Mem.valid_block tm tsp). eapply Mem.valid_block_inject_2; eauto. 
+  apply regs_inject; auto.
+
+- (* tailcall *)
+  exploit find_function_inject. 
+  eapply match_stacks_preserves_globals; eauto. eauto. 
+  destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto.
+  intros (A & B).
+  exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D).
+  econstructor; split.
+  eapply exec_Itailcall; eauto. 
+  econstructor; eauto. 
+  apply match_stacks_bound with stk tsp; auto.
+  apply Plt_Ple. 
+  change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto.
+  apply Plt_Ple. 
+  change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto.
+  apply regs_inject; auto.
+
+- (* builtin *)
+  exploit external_call_inject; eauto. 
+  eapply match_stacks_preserves_globals; eauto.
+  intros. apply KEPT. red. econstructor; econstructor; eauto. 
+  apply regs_inject; eauto.
+  intros (j' & tv & tm' & A & B & C & D & E & F & G).
+  econstructor; split.
+  eapply exec_Ibuiltin; eauto.
+  eapply match_states_regular with (j := j'); eauto. 
+  apply match_stacks_incr with j; auto. 
+  intros. exploit G; eauto. intros [P Q].
+  assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto).
+  assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto).
+  unfold Mem.valid_block in *; xomega.
+  apply set_reg_inject; auto. apply regset_inject_incr with j; auto.
+
+- (* cond *)
+  assert (C: eval_condition cond trs##args tm = Some b).
+  { eapply eval_condition_inject; eauto. apply regs_inject; auto. }
+  econstructor; split.
+  eapply exec_Icond with (pc' := if b then ifso else ifnot); eauto. 
+  econstructor; eauto.
+
+- (* jumptbl *)
+  generalize (REGINJ arg); rewrite H0; intros INJ; inv INJ.
+  econstructor; split.
+  eapply exec_Ijumptable; eauto. 
+  econstructor; eauto.
+
+- (* return *)
+  exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D).
+  econstructor; split.
+  eapply exec_Ireturn; eauto. 
+  econstructor; eauto. 
+  apply match_stacks_bound with stk tsp; auto.
+  apply Plt_Ple. 
+  change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto.
+  apply Plt_Ple. 
+  change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto.
+  destruct or; simpl; auto. 
+
+- (* internal function *)
+  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  intros (j' & tm' & tstk & C & D & E & F & G).
+  assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). 
+  assert (TSTK: tstk = Mem.nextblock tm) by (eapply Mem.alloc_result; eauto). 
+  assert (STACKS': match_stacks j' s ts stk tstk).
+  { rewrite STK, TSTK. 
+    apply match_stacks_incr with j; auto. 
+    intros. destruct (eq_block b1 stk). 
+    subst b1. rewrite F in H1; inv H1. subst b2. split; apply Ple_refl. 
+    rewrite G in H1 by auto. congruence. }
+  econstructor; split. 
+  eapply exec_function_internal; eauto.
+  eapply match_states_regular with (j := j'); eauto.
+  apply init_regs_inject; auto. apply val_list_inject_incr with j; auto. 
+
+- (* external function *)
+  exploit external_call_inject; eauto. 
+  eapply match_stacks_preserves_globals; eauto.
+  intros (j' & tres & tm' & A & B & C & D & E & F & G).
+  econstructor; split.
+  eapply exec_function_external; eauto.
+  eapply match_states_return with (j := j'); eauto.
+  apply match_stacks_bound with (Mem.nextblock m) (Mem.nextblock tm).
+  apply match_stacks_incr with j; auto. 
+  intros. exploit G; eauto. intros [P Q].
+  unfold Mem.valid_block in *; xomega.
+  eapply external_call_nextblock; eauto.
+  eapply external_call_nextblock; eauto.
+
+- (* return *)
+  inv STACKS. econstructor; split.
+  eapply exec_return. 
+  econstructor; eauto. apply set_reg_inject; auto. 
+Qed.
+
+(** Relating initial memory states *)
+
+Remark init_meminj_no_overlap:
+  forall m, Mem.meminj_no_overlap init_meminj m.
+Proof.
+  intros; red; intros. 
+  exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1).
+  exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2).
+  left; red; intros; subst b2'. 
+  assert (id1 = id2) by (eapply Genv.genv_vars_inj; eauto). 
+  congruence.
+Qed.
+
+Lemma store_zeros_unmapped_inj:
+  forall m1 b1 i n m1',
+  store_zeros m1 b1 i n = Some m1' ->
+  forall m2,
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj b1 = None ->
+  Mem.mem_inj init_meminj m1' m2.
+Proof.
+  intros until m1'. functional induction (store_zeros m1 b1 i n); intros.
+  inv H. auto.
+  eapply IHo; eauto. eapply Mem.store_unmapped_inj; eauto. 
+  discriminate.
+Qed.
+
+Lemma store_zeros_mapped_inj:
+  forall m1 b1 i n m1',
+  store_zeros m1 b1 i n = Some m1' ->
+  forall m2 b2,
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj b1 = Some(b2, 0) ->
+  exists m2', store_zeros m2 b2 i n = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
+Proof.
+  intros until m1'. functional induction (store_zeros m1 b1 i n); intros.
+  inv H. exists m2; split; auto. rewrite store_zeros_equation, e; auto. 
+  exploit Mem.store_mapped_inj; eauto. apply init_meminj_no_overlap. instantiate (1 := Vzero); constructor. 
+  intros (m2' & A & B). rewrite Zplus_0_r in A.
+  exploit IHo; eauto. intros (m3' & C & D). 
+  exists m3'; split; auto. rewrite store_zeros_equation, e, A, C; auto.
+  discriminate.
+Qed.
+
+Lemma store_init_data_unmapped_inj:
+  forall m1 b1 i id m1' m2,
+  Genv.store_init_data ge m1 b1 i id = Some m1' ->
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj b1 = None ->
+  Mem.mem_inj init_meminj m1' m2.
+Proof.
+  intros. destruct id; simpl in H; try (eapply Mem.store_unmapped_inj; now eauto). 
+  inv H; auto.
+  destruct (Genv.find_symbol ge i0); try discriminate. eapply Mem.store_unmapped_inj; now eauto.
+Qed.
+
+Lemma store_init_data_mapped_inj:
+  forall m1 b1 i init m1' b2 m2,
+  Genv.store_init_data ge m1 b1 i init = Some m1' ->
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj b1 = Some(b2, 0) ->
+  (forall id ofs, init = Init_addrof id ofs -> kept id) ->
+  exists m2', Genv.store_init_data tge m2 b2 i init = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
+Proof.
+  intros. replace i with (i + 0) by omega. pose proof (init_meminj_no_overlap m1).
+  destruct init; simpl in *; try (eapply Mem.store_mapped_inj; now eauto).
+  inv H. exists m2; auto.
+  destruct (Genv.find_symbol ge i0) as [bi|] eqn:FS1; try discriminate.
+  exploit symbols_inject_2. eapply init_meminj_preserves_globals. eapply H2; eauto. eauto. 
+  intros (bi' & A & B). rewrite A. eapply Mem.store_mapped_inj; eauto. 
+  econstructor; eauto. rewrite Int.add_zero; auto.
+Qed.
+
+ Lemma store_init_data_list_unmapped_inj:
+  forall initlist m1 b1 i m1' m2,
+  Genv.store_init_data_list ge m1 b1 i initlist = Some m1' ->
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj b1 = None ->
+  Mem.mem_inj init_meminj m1' m2.
+Proof.
+  induction initlist; simpl; intros. 
+- inv H; auto.
+- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate.
+  eapply IHinitlist; eauto. eapply store_init_data_unmapped_inj; eauto.
+Qed.
+
+Lemma store_init_data_list_mapped_inj:
+  forall initlist m1 b1 i m1' b2 m2,
+  Genv.store_init_data_list ge m1 b1 i initlist = Some m1' ->
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj b1 = Some(b2, 0) ->
+  (forall id ofs, In (Init_addrof id ofs) initlist -> kept id) ->
+  exists m2', Genv.store_init_data_list tge m2 b2 i initlist = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
+Proof.
+  induction initlist; simpl; intros.
+- inv H. exists m2; auto.
+- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate.
+  exploit store_init_data_mapped_inj; eauto. intros (m2'' & A & B).
+  exploit IHinitlist; eauto. intros (m2' & C & D).
+  exists m2'; split; auto. rewrite A; auto. 
+Qed.
+
+Lemma alloc_global_unmapped_inj:
+  forall m1 id g m1' m2,
+  Genv.alloc_global ge m1 (id, g) = Some m1' ->
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj (Mem.nextblock m1) = None ->
+  Mem.mem_inj init_meminj m1' m2.
+Proof.
+  unfold Genv.alloc_global; intros. destruct g as [fd|gv].
+- destruct (Mem.alloc m1 0 1) as (m1a, b) eqn:ALLOC.
+  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. 
+  eapply Mem.drop_unmapped_inj with (m1 := m1a); eauto. 
+  eapply Mem.alloc_left_unmapped_inj; eauto.
+- set (sz := Genv.init_data_list_size (gvar_init gv)) in *.
+  destruct (Mem.alloc m1 0 sz) as (m1a, b) eqn:ALLOC.
+  destruct (store_zeros m1a b 0 sz) as [m1b|] eqn: STZ; try discriminate.
+  destruct (Genv.store_init_data_list ge m1b b 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate.
+  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. 
+  eapply Mem.drop_unmapped_inj with (m1 := m1c); eauto.
+  eapply store_init_data_list_unmapped_inj with (m1 := m1b); eauto. 
+  eapply store_zeros_unmapped_inj with (m1 := m1a); eauto.
+  eapply Mem.alloc_left_unmapped_inj; eauto.
+Qed.
+
+Lemma alloc_global_mapped_inj:
+  forall m1 id g m1' m2,
+  Genv.alloc_global ge m1 (id, g) = Some m1' ->
+  Mem.mem_inj init_meminj m1 m2 ->
+  init_meminj (Mem.nextblock m1) = Some(Mem.nextblock m2, 0) ->
+  (forall id, ref_def g id -> kept id) ->
+  exists m2',
+    Genv.alloc_global tge m2 (id, g) = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
+Proof.
+  unfold Genv.alloc_global; intros. destruct g as [fd|gv].
+- destruct (Mem.alloc m1 0 1) as (m1a, b1) eqn:ALLOC.
+  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
+  destruct (Mem.alloc m2 0 1) as (m2a, b2) eqn:ALLOC2.
+  exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1.
+  assert (Mem.mem_inj init_meminj m1a m2a).
+  { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0).
+    eapply Mem.alloc_right_inj; eauto.
+    eauto.
+    eauto with mem. 
+    red; intros; apply Z.divide_0_r.
+    intros. apply Mem.perm_implies with Freeable; auto with mem. 
+    eapply Mem.perm_alloc_2; eauto. omega. 
+    auto.
+  }
+  exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap.
+- set (sz := Genv.init_data_list_size (gvar_init gv)) in *.
+  destruct (Mem.alloc m1 0 sz) as (m1a, b1) eqn:ALLOC.
+  destruct (store_zeros m1a b1 0 sz) as [m1b|] eqn: STZ; try discriminate.
+  destruct (Genv.store_init_data_list ge m1b b1 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate.
+  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
+  destruct (Mem.alloc m2 0 sz) as (m2a, b2) eqn:ALLOC2.
+  exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1.
+  assert (Mem.mem_inj init_meminj m1a m2a).
+  { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0).
+    eapply Mem.alloc_right_inj; eauto.
+    eauto.
+    eauto with mem. 
+    red; intros; apply Z.divide_0_r.
+    intros. apply Mem.perm_implies with Freeable; auto with mem. 
+    eapply Mem.perm_alloc_2; eauto. omega. 
+    auto.
+  }
+  exploit store_zeros_mapped_inj; eauto. intros (m2b & A & B).
+  exploit store_init_data_list_mapped_inj; eauto. 
+  intros. apply H2. red. exists ofs; auto. intros (m2c & C & D).
+  exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. intros (m2' & E & F).
+  exists m2'; split; auto. rewrite ! Zplus_0_r in E. rewrite A, C, E. auto.
+Qed.
+
+Lemma alloc_globals_app:
+  forall F V (g: Genv.t F V) defs1 m defs2,
+  Genv.alloc_globals g m (defs1 ++ defs2) =
+  match Genv.alloc_globals g m defs1 with
+  | None => None
+  | Some m1 => Genv.alloc_globals g m1 defs2
+  end.
+Proof.
+  induction defs1; simpl; intros. auto. 
+  destruct (Genv.alloc_global g m a); auto. 
+Qed.
+
+Lemma alloc_globals_snoc:
+  forall F V (g: Genv.t F V) m defs1 id_def,
+  Genv.alloc_globals g m (defs1 ++ id_def :: nil) =
+  match Genv.alloc_globals g m defs1 with
+  | None => None
+  | Some m1 => Genv.alloc_global g m1 id_def
+  end.
+Proof.
+  intros. rewrite alloc_globals_app.
+  destruct (Genv.alloc_globals g m defs1); auto. unfold Genv.alloc_globals. 
+  destruct (Genv.alloc_global g m0 id_def); auto.
+Qed.
+
+Lemma alloc_globals_inj:
+  forall pubs defs m1 u g1 g2,
+  Genv.alloc_globals ge Mem.empty (List.rev defs) = Some m1 ->
+  g1 = Genv.add_globals (Genv.empty_genv _ _ pubs) (List.rev defs) ->
+  g2 = Genv.add_globals (Genv.empty_genv _ _ pubs) (filter_globdefs u nil defs) ->
+  Mem.nextblock m1 = Genv.genv_next g1 ->
+  (forall id, IS.In id u -> Genv.find_symbol g1 id = Genv.find_symbol ge id) ->
+  (forall id, IS.In id u -> Genv.find_symbol g2 id = Genv.find_symbol tge id) ->
+  (forall b id, Genv.find_symbol ge id = Some b -> Plt b (Mem.nextblock m1) -> kept id -> IS.In id u) ->
+  (forall id, IS.In id u -> (fold_left add_def_prog_map (List.rev defs) (PTree.empty _))!id = pm!id) ->
+  exists m2,
+     Genv.alloc_globals tge Mem.empty (filter_globdefs u nil defs) = Some m2
+  /\ Mem.nextblock m2 = Genv.genv_next g2
+  /\ Mem.mem_inj init_meminj m1 m2.
+Proof.
+  induction defs; simpl; intros until g2; intros ALLOC GE1 GE2 NEXT1 SYMB1 SYMB2 SYMB3 PROGMAP.
+- inv ALLOC. exists Mem.empty. intuition auto. constructor; intros.
+  eelim Mem.perm_empty; eauto. 
+  exploit init_meminj_invert; eauto. intros [A B]. subst delta. apply Z.divide_0_r. 
+  eelim Mem.perm_empty; eauto.
+- rewrite Genv.add_globals_app in GE1. simpl in GE1. 
+  set (g1' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (rev defs)) in *.
+  rewrite alloc_globals_snoc in ALLOC.
+  destruct (Genv.alloc_globals ge Mem.empty (rev defs)) as [m1'|] eqn:ALLOC1'; try discriminate.
+  exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK1.
+  assert (NEXTGE1: Genv.genv_next g1 = Pos.succ (Genv.genv_next g1')) by (rewrite GE1; reflexivity). 
+  assert (NEXT1': Mem.nextblock m1' = Genv.genv_next g1') by (unfold block in *; xomega).
+  rewrite fold_left_app in PROGMAP. simpl in PROGMAP.
+  destruct a as [id gd]. unfold add_def_prog_map at 1 in PROGMAP. simpl in PROGMAP.
+  destruct (IS.mem id u) eqn:MEM.
+  + rewrite filter_globdefs_nil in *. rewrite alloc_globals_snoc. 
+    rewrite Genv.add_globals_app in GE2. simpl in GE2.
+    set (g2' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (filter_globdefs (IS.remove id u) nil defs)) in *.
+    assert (NEXTGE2: Genv.genv_next g2 = Pos.succ (Genv.genv_next g2')) by (rewrite GE2; reflexivity).
+    assert (FS1: Genv.find_symbol ge id = Some (Mem.nextblock m1')).
+    { rewrite <- SYMB1 by (apply IS.mem_2; auto).
+      rewrite GE1. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. }
+    exploit (IHdefs m1' (IS.remove id u) g1' g2'); eauto.
+      intros. rewrite ISF.remove_iff in H; destruct H.
+      rewrite <- SYMB1 by auto. rewrite GE1. unfold Genv.find_symbol; simpl. 
+      rewrite PTree.gso; auto.
+      intros. rewrite ISF.remove_iff in H; destruct H.
+      rewrite <- SYMB2 by auto. rewrite GE2. unfold Genv.find_symbol; simpl. 
+      rewrite PTree.gso; auto.
+      intros. rewrite ISF.remove_iff. destruct (ident_eq id id0).
+      subst id0. rewrite FS1 in H. inv H. eelim Plt_strict; eauto.
+      exploit SYMB3. eexact H. unfold block in *; xomega. auto. tauto. 
+      intros. rewrite ISF.remove_iff in H; destruct H. 
+      rewrite <- PROGMAP by auto. rewrite PTree.gso by auto. auto.
+    intros (m2' & A & B & C). fold g2' in B.
+    assert (FS2: Genv.find_symbol tge id = Some (Mem.nextblock m2')).
+    { rewrite <- SYMB2 by (apply IS.mem_2; auto).
+      rewrite GE2. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. }
+    assert (INJ: init_meminj (Mem.nextblock m1') = Some (Mem.nextblock m2', 0)).
+    { apply Genv.find_invert_symbol in FS1. unfold init_meminj. rewrite FS1, FS2. auto. }
+    exploit alloc_global_mapped_inj. eexact ALLOC. eexact C. exact INJ.
+    intros. apply kept_closed with id gd. eapply transform_program_kept; eauto. 
+    rewrite <- PROGMAP by (apply IS.mem_2; auto). apply PTree.gss. auto. 
+    intros (m2 & D & E).
+    exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK2. 
+    exists m2; split. rewrite A, D. auto. 
+    split. unfold block in *; xomega.
+    auto.
+  + exploit (IHdefs m1' u g1' g2); auto. 
+    intros. rewrite <- SYMB1 by auto. rewrite GE1. 
+    unfold Genv.find_symbol; simpl. rewrite PTree.gso; auto. 
+    red; intros; subst id0. apply IS.mem_1 in H. congruence.
+    intros. eapply SYMB3; eauto. unfold block in *; xomega.
+    intros. rewrite <- PROGMAP by auto. rewrite PTree.gso; auto.
+    apply IS.mem_1 in H. congruence.
+    intros (m2 & A & B & C).
+    assert (NOTINJ: init_meminj (Mem.nextblock m1') = None).
+    { destruct (init_meminj (Mem.nextblock m1')) as [[b' delta]|] eqn:J; auto.
+      exploit init_meminj_invert; eauto. intros (U & id1 & V & W).
+      exploit SYMB3; eauto. unfold block in *; xomega.
+      eapply transform_program_kept; eauto.
+      intros P.
+      revert V. rewrite <- SYMB1, GE1 by auto. unfold Genv.find_symbol; simpl.
+      rewrite PTree.gsspec. rewrite NEXT1'. destruct (peq id1 id); intros Q. 
+      subst id1. apply IS.mem_1 in P. congruence. 
+      eelim Plt_strict. eapply Genv.genv_symb_range; eauto. }
+    exists m2; intuition auto. eapply alloc_global_unmapped_inj; eauto.
+Qed.
+
+Theorem init_mem_inject:
+  forall m,
+  Genv.init_mem p = Some m ->
+  exists f tm, Genv.init_mem tp = Some tm /\ Mem.inject f m tm /\ meminj_preserves_globals f.
+Proof.
+  intros.
+  unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; injection TRANSF. intros EQ.
+  destruct (alloc_globals_inj (prog_public p) (List.rev (prog_defs p)) m used ge tge) as (tm & A & B & C).
+  rewrite rev_involutive; auto. 
+  rewrite rev_involutive; auto.
+  unfold tge; rewrite <- EQ; auto.
+  symmetry. apply Genv.init_mem_genv_next; auto. 
+  auto. auto. auto.
+  intros. rewrite rev_involutive. auto.
+  assert (D: Genv.init_mem tp = Some tm).
+  { unfold Genv.init_mem. fold tge. rewrite <- EQ. exact A. }
+  pose proof (init_meminj_preserves_globals). 
+  exists init_meminj, tm; intuition auto.
+  constructor; intros.
+  + auto.
+  + destruct (init_meminj b) as [[b1 delta1]|] eqn:INJ; auto.
+    exploit init_meminj_invert; eauto. intros (P & id & Q & R).
+    elim H1. eapply Genv.find_symbol_not_fresh; eauto.
+  + exploit init_meminj_invert; eauto. intros (P & id & Q & R).
+    eapply Genv.find_symbol_not_fresh; eauto.
+  + apply init_meminj_no_overlap.
+  + exploit init_meminj_invert; eauto. intros (P & id & Q & R). 
+    split. omega. generalize (Int.unsigned_range_2 ofs). omega.
+Qed.
+
+Lemma transf_initial_states:
+  forall S1, initial_state p S1 -> exists S2, initial_state tp S2 /\ match_states S1 S2.
+Proof.
+  intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C).
+  exploit symbols_inject_2. eauto. apply kept_main. eexact H1. intros (tb & P & Q).
+  exploit funct_ptr_inject. eauto. eexact Q. exact H2. 
+  intros (R & S & T).
+  exists (Callstate nil f nil tm); split.
+  econstructor; eauto.
+    fold tge. unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; inversion TRANSF; auto. 
+  econstructor; eauto.
+  constructor. auto. 
+  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. 
+  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. 
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r,
+  match_states S1 S2 -> final_state S1 r -> final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. inv RESINJ. constructor. 
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (semantics p) (semantics tp).
+Proof.
+  intros. 
+  eapply forward_simulation_step.
+  exploit globals_symbols_inject. apply init_meminj_preserves_globals. intros [A B]. exact A.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  eexact step_simulation.
+Qed.
+
+End SOUNDNESS.