- Extended traces so that pointers within globals are supported as event values.

- Revised handling of volatile reads: the execution environment
  dictates the value read, via the trace of events.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

32 files changed, 507 insertions, 351 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 13c2e57..7a3fe20 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -616,7 +616,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       extcall_arguments rs m ef.(ef_sig) args ->
       rs' = (rs#(loc_external_result ef.(ef_sig)) <- res
                #PC <- (rs IR14)) ->
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index eec0c65..0a1180c 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -1130,14 +1130,25 @@ Proof.
   econstructor; eauto with coqlib.
 Qed.
 
-Lemma exec_function_external_prop:
  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
         (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
         (ef : external_function) (args : list val) (res : val) (m': mem),
  Genv.find_funct_ptr ge fb = Some (External ef) ->
  external_call ef args m t0 res m' ->
  Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
  ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
  exec_instr_prop (Machconcr.Callstate s fb ms m)
               t0 (Machconcr.Returnstate s ms' m').
Proof.
+Lemma exec_function_external_prop:
+  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
+         (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
+         (ef : external_function) (args : list val) (res : val) (m': mem),
+  Genv.find_funct_ptr ge fb = Some (External ef) ->
+  external_call ef (Genv.find_symbol ge) args m t0 res m' ->
+  Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
+  ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
+  exec_instr_prop (Machconcr.Callstate s fb ms m)
+               t0 (Machconcr.Returnstate s ms' m').
+Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B. 
   left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14))
                 m'); split.
-  apply plus_one. eapply exec_step_external; eauto. 
-  eauto. eapply extcall_arguments_match; eauto. 
+  apply plus_one. eapply exec_step_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply extcall_arguments_match; eauto. 
   econstructor; eauto. 
   unfold loc_external_result. auto with ppcgen.
 Qed.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3f526aa..b845323 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -717,6 +717,7 @@ Proof.
   injection H7; intro EQ; inv EQ.
   econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   eapply match_states_return; eauto.
 
   (* return *)
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index fcc867a..ce577ac 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -935,6 +935,7 @@ Proof.
   (* external function *)
   simpl. econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
 
   (* return *)
diff --git a/backend/Cminor.v b/backend/Cminor.v
index f2f03c5..cc4afa5 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -496,7 +496,7 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
   | step_external_function: forall ef vargs k m t vres m',
-      external_call ef vargs m t vres m' ->
+      external_call ef (Genv.find_symbol ge) vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
          t (Returnstate vres k m')        
 
@@ -595,7 +595,7 @@ Inductive eval_funcall:
       eval_funcall m (Internal f) vargs t m3 vres
   | eval_funcall_external:
       forall ef m args t res m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       eval_funcall m (External ef) args t m' res
 
 (** Execution of a statement: [exec_stmt ge f sp e m s t e' m' out]
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 231af8f..65dd4de 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -354,7 +354,7 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
   | step_external_function: forall ef vargs k m t vres m',
-      external_call ef vargs m t vres m' ->
+      external_call ef (Genv.find_symbol ge) vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
          t (Returnstate vres k m')        
 
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 6671960..b5c3b1e 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -415,6 +415,7 @@ Proof.
   (* external function *)
   simpl. econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   constructor; auto.
 
   (* return *)
diff --git a/backend/LTL.v b/backend/LTL.v
index 2a1172a..4aa8afc 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -228,7 +228,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m')
   | exec_function_external:
       forall s ef t args res m m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       step (Callstate s (External ef) args m)
          t (Returnstate s res m')
   | exec_return:
diff --git a/backend/LTLin.v b/backend/LTLin.v
index c3b432b..64017c3 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -225,7 +225,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m')
   | exec_function_external:
       forall s ef args t res m m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       step (Callstate s (External ef) args m)
          t (Returnstate s res m')
   | exec_return:
diff --git a/backend/Linear.v b/backend/Linear.v
index be07b82..7d21651 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -314,7 +314,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk Int.zero) f.(fn_code) (call_regs rs) m')
   | exec_function_external:
       forall s ef args res rs1 rs2 m t m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) ->
       rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 ->
       step (Callstate s (External ef) rs1 m)
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 5d67065..fcb1acf 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -684,6 +684,7 @@ Proof.
   (* external function *)
   monadInv H6. econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
 
   (* return *)
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index ceaf9a6..bbc7e7d 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -303,7 +303,7 @@ Inductive step: state -> trace -> state -> Prop :=
                   f.(fn_code) rs empty_frame m')
   | exec_function_external:
       forall s ef args res rs1 rs2 m t m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args ->
       rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       step (Callstate s (External ef) rs1 m)
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index b766ed0..b823297 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -407,12 +407,12 @@ Qed.
 (** [frame_match] is preserved by external calls. *)
 
 Lemma frame_match_external_call:
-  forall fr sp base mm ms mm' ms' ef vargs vres t vargs' vres',
+  forall symb fr sp base mm ms mm' ms' ef vargs vres t vargs' vres',
   frame_match fr sp base mm ms ->
   Mem.extends mm ms ->
-  external_call ef vargs mm t vres mm' ->
+  external_call ef symb vargs mm t vres mm' ->
   Mem.extends mm' ms' ->
-  external_call ef vargs' ms t vres' ms' ->
+  external_call ef symb vargs' ms t vres' ms' ->
   mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
   frame_match fr sp base mm' ms'.
 Proof.
@@ -420,7 +420,7 @@ Proof.
   eapply external_call_valid_block; eauto.
   eapply external_call_valid_block; eauto.
   auto.
-  rewrite (external_call_bounds _ _ _ _ _ _ _ H1); auto.
+  rewrite (external_call_bounds _ _ _ _ _ _ _ _ H1); auto.
   red; intros. apply A; auto. red. omega.
   intros. exploit fm_contents_match0; eauto. intros [v [C D]].
   exists v; split; auto.
@@ -814,9 +814,9 @@ Lemma match_stacks_external_call:
   match_stacks s ts mm ms ->
   forall ef vargs t vres mm' ms' vargs' vres',
   Mem.extends mm ms ->
-  external_call ef vargs mm t vres mm' ->
+  external_call ef (Genv.find_symbol ge) vargs mm t vres mm' ->
   Mem.extends mm' ms' ->
-  external_call ef vargs' ms t vres' ms' ->
+  external_call ef (Genv.find_symbol ge) vargs' ms t vres' ms' ->
   mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
   match_stacks s ts mm' ms'.
 Proof.
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index a6be4bc..90d08f1 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -233,7 +233,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_function_external:
       forall s fb rs m t rs' ef args res m',
       Genv.find_funct_ptr ge fb = Some (External ef) ->
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       extcall_arguments rs m (parent_sp s) ef.(ef_sig) args ->
       rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       step (Callstate s fb rs m)
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index c2e797a..b0673ca 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -285,7 +285,7 @@ Proof.
   apply wt_empty_frame.
 
   econstructor; eauto. apply wt_setreg; auto.
-  generalize (external_call_well_typed _ _ _ _ _ _ H).  
+  generalize (external_call_well_typed _ _ _ _ _ _ _ H).  
   unfold proj_sig_res, Conventions.loc_result.
   destruct (sig_res (ef_sig ef)).
   destruct t0; simpl; auto.
diff --git a/backend/RTL.v b/backend/RTL.v
index c5d4d7d..c8220e5 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -282,7 +282,7 @@ Inductive step: state -> trace -> state -> Prop :=
                   m')
   | exec_function_external:
       forall s ef args res t m m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       step (Callstate s (External ef) args m)
          t (Returnstate s res m')
   | exec_return:
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index a15095b..92f4cc9 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1320,6 +1320,7 @@ Proof.
   monadInv TF. 
   econstructor; split.
   left; apply plus_one. eapply exec_function_external; eauto. 
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   constructor; auto.
 
   (* return *)
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index bf728fa..1fa000c 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -1310,6 +1310,7 @@ Proof.
   intros [res' [tm' [A [B [C D]]]]]. 
   left; econstructor; split.
   apply plus_one. eapply exec_function_external; eauto. 
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
   simpl. rewrite Locmap.gss. auto.
   intros. rewrite Locmap.gso. auto. 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 1da7884..0d1a1ee 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -469,6 +469,10 @@ Proof.
   econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut.
   rewrite H. simpl. reflexivity. 
   constructor; auto.
+  (* external call *)
+  econstructor; split.
+  econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. 
+  constructor; auto.
 Qed.
 
 Lemma sel_initial_states:
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index f44eac2..fbe4b68 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1574,6 +1574,7 @@ Proof.
   exploit transl_external_arguments; eauto. intro EXTARGS.
   econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
   intros. unfold Regmap.set. case (RegEq.eq r (loc_result (ef_sig ef))); intro.
   rewrite e. rewrite Locmap.gss; auto. rewrite Locmap.gso; auto.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 0ca4c02..0535cbf 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -557,6 +557,7 @@ Proof.
   intros [res' [m2' [A [B [C D]]]]].
   left. exists (Returnstate s' res' m2'); split.
   simpl. econstructor; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   constructor; auto. 
 
 (* returnstate *)
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 4cbcbd4..3f0a27d 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -335,6 +335,7 @@ Proof.
   (* external function *)
   simpl. left; econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   simpl. econstructor; eauto. 
   (* return *)
   inv H3. inv H1.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 19e13cb..9f572ed 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -481,19 +481,6 @@ Record match_env (f: meminj) (cenv: compilenv)
 
 Hint Resolve me_low_high.
 
-(** Global environments match if the memory injection [f] leaves unchanged
-  the references to global symbols and functions. *)
-
-Record match_globalenvs (f: meminj) : Prop := 
-  mk_match_globalenvs {
-    mg_symbols:
-      forall id b,
-      Genv.find_symbol ge id = Some b ->
-      f b = Some (b, 0) /\ Genv.find_symbol tge id = Some b;
-    mg_functions:
-      forall b, b < 0 -> f b = Some(b, 0)
-  }.
-
 (** The remainder of this section is devoted to showing preservation
   of the [match_en] invariant under various assignments and memory
   stores.  First: preservation by memory stores to ``mapped'' blocks
@@ -804,6 +791,16 @@ Inductive frame : Type :=
 
 Definition callstack : Type := list frame.
 
+(** Global environments match if the memory injection [f] leaves unchanged
+  the references to global symbols and functions. *)
+
+Inductive match_globalenvs (f: meminj) (bound: Z): Prop :=
+  | mk_match_globalenvs
+      (POS: bound > 0)
+      (DOMAIN: forall b, b < bound -> f b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound).
+
 (** Matching of call stacks imply:
 - matching of environments for each of the frames
 - matching of the global environments
@@ -824,8 +821,9 @@ Definition padding_freeable (f: meminj) (m: mem) (tm: mem) (sp: block) (sz: Z) :
 Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
                           callstack -> Z -> Z -> Prop :=
   | mcs_nil:
-      forall bound tbound,
-      match_globalenvs f ->
+      forall hi bound tbound,
+      match_globalenvs f hi ->
+      hi <= bound -> hi <= tbound ->
       match_callstack f m tm nil bound tbound 
   | mcs_cons:
       forall cenv tf e te sp lo hi cs bound tbound
@@ -841,7 +839,7 @@ Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
 Lemma match_callstack_match_globalenvs:
   forall f m tm cs bound tbound,
   match_callstack f m tm cs bound tbound ->
-  match_globalenvs f.
+  exists hi, match_globalenvs f hi.
 Proof.
   induction 1; eauto.
 Qed.
@@ -878,7 +876,7 @@ Lemma match_callstack_store_mapped:
   match_callstack f m' tm' cs lo hi.
 Proof.
   induction 4.
-  constructor; auto.
+  econstructor; eauto.
   constructor; auto. 
   eapply match_env_store_mapped; eauto. congruence.
   eapply padding_freeable_invariant; eauto. 
@@ -915,7 +913,7 @@ Lemma match_callstack_invariant:
   match_callstack f m' tm' cs bound tbound.
 Proof.
   induction 1; intros.
-  constructor; auto.
+  econstructor; eauto.
   constructor; auto.
   eapply padding_freeable_invariant; eauto. 
   intros. apply H1. omega.
@@ -973,7 +971,9 @@ Lemma match_callstack_incr_bound:
   bound <= bound' -> tbound <= tbound' ->
   match_callstack f m tm cs bound' tbound'.
 Proof.
-  intros. inversion H; constructor; auto. omega. omega.
+  intros. inv H.
+  econstructor; eauto. omega. omega. 
+  constructor; auto. omega. omega.
 Qed.
 
 (** Preservation of [match_callstack] by freeing all blocks allocated
@@ -1075,13 +1075,10 @@ Lemma match_callstack_alloc_below:
   match_callstack f2 m2 tm cs bound tbound.
 Proof.
   induction 4; intros.
-  constructor. 
-  inv H2. constructor. 
-  intros. exploit mg_symbols0; eauto. intros [A B]. auto. 
-  intros. rewrite H1; auto. 
-  exploit Mem.alloc_result; eauto. 
-  generalize (Mem.nextblock_pos m1).
-  unfold block; omega.
+  apply mcs_nil with hi; auto. 
+  inv H2. constructor; auto. 
+  intros. destruct (eq_block b1 b). subst. rewrite H2 in H6. omegaContradiction.
+  rewrite H1 in H2; eauto.
   constructor; auto.
   eapply match_env_alloc_other; eauto. omega. destruct (f2 b); auto. destruct p; omega.
   eapply padding_freeable_invariant; eauto. 
@@ -1223,15 +1220,15 @@ Proof.
   intros until m2'. 
   intros UNMAPPED OUTOFREACH INCR SEPARATED BOUNDS.
   destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2].
-  induction 1; intros; constructor.
+  induction 1; intros.
 (* base case *)
-  constructor; intros. 
-  exploit mg_symbols; eauto. intros [A B]. auto.
-  replace (f2 b) with (f1 b). eapply mg_functions; eauto.
-  symmetry. eapply inject_incr_separated_same; eauto. 
-  red. generalize (Mem.nextblock_pos m1); omega.
+  apply mcs_nil with hi; auto.
+  inv H. constructor; auto.
+  intros. case_eq (f1 b1). 
+  intros [b2' delta'] EQ. rewrite (INCR _ _ _ EQ) in H. inv H. eauto. 
+  intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. 
 (* inductive case *)
-  auto. auto. 
+  constructor. auto. auto. 
   eapply match_env_external_call; eauto. omega. omega. 
   (* padding-freeable *)
   red; intros.
@@ -1253,14 +1250,24 @@ Qed.
 
 Remark external_call_nextblock_incr:
   forall ef vargs m1 t vres m2,
-  external_call ef vargs m1 t vres m2 ->
+  external_call ef (Genv.find_symbol ge) vargs m1 t vres m2 ->
   Mem.nextblock m1 <= Mem.nextblock m2.
 Proof.
   intros. 
-  generalize (external_call_valid_block _ _ _ _ _ _ (Mem.nextblock m1 - 1) H).
+  generalize (external_call_valid_block _ _ _ _ _ _ _ (Mem.nextblock m1 - 1) H).
   unfold Mem.valid_block. omega. 
 Qed.
 
+Remark inj_preserves_globals:
+  forall f hi,
+  match_globalenvs f hi ->
+  meminj_preserves_globals (Genv.find_symbol ge) f.
+Proof.
+  intros. inv H. split; intros.
+  apply DOMAIN. eapply SYMBOLS. eauto.
+  symmetry. eapply IMAGE; eauto. 
+Qed.
+
 (** * Soundness of chunk and type inference. *)
 
 Lemma load_normalized:
@@ -1682,15 +1689,15 @@ Proof.
   auto.
   (* var_global_scalar *)
   simpl in *.
-  assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inv H2. exploit mg_symbols0; eauto. intros [A B].
+  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
   assert (chunk0 = chunk). congruence. subst chunk0.
   assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)).
-    econstructor; eauto.
+    econstructor; eauto. 
   exploit Mem.loadv_inject; eauto. simpl. eauto.   
   intros [tv [LOAD INJ]].
   exists tv; split. 
   eapply eval_Eload; eauto. eapply make_globaladdr_correct; eauto.
+  rewrite symbols_preserved; auto.
   auto.
 Qed.
 
@@ -1714,16 +1721,14 @@ Proof.
   exists (Vptr sp (Int.repr ofs)); split.
   eapply make_stackaddr_correct. congruence.
   (* var_global_scalar *)
-  assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inv H1. exploit mg_symbols0; eauto. intros [A B].
+  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
   exists (Vptr b Int.zero); split.
-  eapply make_globaladdr_correct. eauto.
+  eapply make_globaladdr_correct; eauto. rewrite symbols_preserved; auto.
   econstructor; eauto. 
   (* var_global_array *)
-  assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inv H1. exploit mg_symbols0; eauto. intros [A B].
+  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
   exists (Vptr b Int.zero); split.
-  eapply make_globaladdr_correct. eauto.
+  eapply make_globaladdr_correct; eauto. rewrite symbols_preserved; auto.
   econstructor; eauto. 
 Qed.
 
@@ -1791,11 +1796,10 @@ Proof.
   simpl in *.
   assert (chunk0 = chunk) by congruence. subst chunk0.  
   assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
-  assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  exploit mg_symbols; eauto. intros [A B].
+  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
   exploit make_store_correct.
     eapply make_globaladdr_correct; eauto.
-    eauto. eauto. eauto. eauto. eauto.
+    rewrite symbols_preserved; eauto. eauto. eauto. eauto. eauto. auto.
   intros [tm' [tvrhs' [EVAL' [STORE' TNEXTBLOCK]]]].
   exists te; exists tm'.
   split. eauto. split. auto. 
@@ -1874,11 +1878,10 @@ Proof.
   simpl in *.
   assert (chunk0 = chunk) by congruence. subst chunk0.  
   assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
-  assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  exploit mg_symbols; eauto. intros [A B].
+  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
   exploit make_store_correct.
     eapply make_globaladdr_correct; eauto.
-    eauto. eauto. eauto. eauto. eauto.
+    rewrite symbols_preserved; eauto. eauto. eauto. eauto. eauto. eauto.
   intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
   exists te'; exists tm'.
   split. eauto. split. auto. 
@@ -2601,16 +2604,16 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
                    (Returnstate tv tk tm).
 
 Remark val_inject_function_pointer:
-  forall v fd f tv,
+  forall bound v fd f tv,
   Genv.find_funct tge v = Some fd ->
-  match_globalenvs f ->
+  match_globalenvs f bound ->
   val_inject f v tv ->
   tv = v.
 Proof.
   intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v.
   rewrite Genv.find_funct_find_funct_ptr in H. 
   assert (b < 0). unfold tge in H. eapply Genv.find_funct_ptr_negative; eauto.
-  assert (f b = Some(b, 0)). eapply mg_functions; eauto. 
+  assert (f b = Some(b, 0)). inv H0. apply DOMAIN. omega.  
   inv H1. rewrite H3 in H6; inv H6. reflexivity.
 Qed.
 
@@ -3000,8 +3003,8 @@ Proof.
   exploit transl_expr_correct; eauto.
   intros [tvf [EVAL1 VINJ1]].
   assert (tvf = vf).
+    exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
     eapply val_inject_function_pointer; eauto.
-    eapply match_callstack_match_globalenvs; eauto.
   subst tvf.
   exploit transl_exprlist_correct; eauto.
   intros [tvargs [EVAL2 VINJ2]].
@@ -3020,8 +3023,8 @@ Proof.
   exploit transl_expr_correct; eauto.
   intros [tvf [EVAL1 VINJ1]].
   assert (tvf = vf).
+    exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
     eapply val_inject_function_pointer; eauto.
-    eapply match_callstack_match_globalenvs; eauto.
   subst tvf.
   exploit transl_exprlist_correct; eauto.
   intros [tvargs [EVAL2 VINJ2]].
@@ -3167,10 +3170,13 @@ Proof.
 
 (* external call *)
   monadInv TR. 
+  exploit match_callstack_match_globalenvs; eauto. intros [hi MG].
   exploit external_call_mem_inject; eauto. 
+  eapply inj_preserves_globals; eauto.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
-  apply plus_one. econstructor; eauto. 
+  apply plus_one. econstructor.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
   apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
@@ -3202,15 +3208,14 @@ Qed.
 Lemma match_globalenvs_init:
   forall m,
   Genv.init_mem prog = Some m ->
-  match_globalenvs (Mem.flat_inj (Mem.nextblock m)).
+  match_globalenvs (Mem.flat_inj (Mem.nextblock m)) (Mem.nextblock m).
 Proof.
   intros. constructor.
-  intros. split.
-  unfold Mem.flat_inj. rewrite zlt_true. auto.
-  eapply Genv.find_symbol_not_fresh; eauto.
-  rewrite <- H0. apply symbols_preserved.
-  intros. unfold Mem.flat_inj. rewrite zlt_true. auto.
-  generalize (Mem.nextblock_pos m). omega.
+  apply Mem.nextblock_pos.
+  intros. unfold Mem.flat_inj. apply zlt_true; auto. 
+  intros. unfold Mem.flat_inj in H0. 
+  destruct (zlt b1 (Mem.nextblock m)); congruence.
+  intros. eapply Genv.find_symbol_not_fresh; eauto.
 Qed.
 
 Lemma transl_initial_states:
@@ -3231,7 +3236,7 @@ Proof.
   eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame).
   auto.
   eapply Genv.initmem_inject; eauto.
-  constructor. apply match_globalenvs_init. auto.  
+  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. omega. omega.
   instantiate (1 := gce). constructor.
   red; auto. constructor. rewrite H2; simpl; auto. 
 Qed.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 5f8bbf1..4e4c379 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -901,7 +901,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f f.(fn_body) k e m2)
 
   | step_external_function: forall id targs tres vargs k m vres t m',
-      external_call (external_function id targs tres) vargs m t vres m' ->
+      external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' ->
       step (Callstate (External id targs tres) vargs k m)
          t (Returnstate vres k m')
 
@@ -1106,7 +1106,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       Mem.free_list m3 (blocks_of_env e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
   | eval_funcall_external: forall m id targs tres vargs t vres m',
-      external_call (external_function id targs tres) vargs m t vres m' ->
+      external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' ->
       eval_funcall m (External id targs tres) vargs t m' vres.
 
 Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 2fddc6c..4c61918 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -516,7 +516,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f f.(fn_body) k e m2)
 
   | step_external_function: forall ef vargs k m t vres m',
-      external_call ef vargs m t vres m' ->
+      external_call ef (Genv.find_symbol ge) vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
          t (Returnstate vres k m')        
 
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 7e3658b..99450de 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -1561,6 +1561,7 @@ Proof.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
   apply plus_one. constructor. eauto. 
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
 
 (* returnstate 0 *)
diff --git a/common/Determinism.v b/common/Determinism.v
index 862d5a5..02fb860 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -45,11 +45,21 @@ Axiom traceinf_extensionality:
   the world to [w]. *)
 
 Inductive world: Type :=
-  World: (ident -> list eventval -> option (eventval * world)) -> world.
+  World (io: ident -> list eventval -> option (eventval * world))
+        (vload: memory_chunk -> ident -> int -> option (eventval * world))
+        (vstore: memory_chunk -> ident -> int -> eventval -> option world).
 
-Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :
+Definition nextworld_io (w: world) (evname: ident) (evargs: list eventval) :
                      option (eventval * world) :=
-  match w with World f => f evname evargs end.
+  match w with World io vl vs => io evname evargs end.
+
+Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) :
+                     option (eventval * world) :=
+  match w with World io vl vs => vl chunk id ofs end.
+
+Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) (v: eventval):
+                     option world :=
+  match w with World io vl vs => vs chunk id ofs v end.
 
 (** A trace is possible in a given world if all events correspond
   to non-stuck external calls according to the given world.
@@ -63,12 +73,14 @@ Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :
 
 Inductive possible_event: world -> event -> world -> Prop :=
   | possible_event_syscall: forall w1 evname evargs evres w2,
-      nextworld w1 evname evargs = Some (evres, w2) ->
+      nextworld_io w1 evname evargs = Some (evres, w2) ->
       possible_event w1 (Event_syscall evname evargs evres) w2
-  | possible_event_load: forall w label,
-      possible_event w (Event_load label) w
-  | possible_event_store: forall w label,
-      possible_event w (Event_store label) w.
+  | possible_event_vload: forall w1 chunk id ofs evres w2,
+      nextworld_vload w1 chunk id ofs = Some (evres, w2) ->
+      possible_event w1 (Event_vload chunk id ofs evres) w2
+  | possible_event_vstore: forall w1 chunk id ofs evarg w2,
+      nextworld_vstore w1 chunk id ofs evarg = Some w2 ->
+      possible_event w1 (Event_vstore chunk id ofs evarg) w2.
 
 Inductive possible_trace: world -> trace -> world -> Prop :=
   | possible_trace_nil: forall w,
@@ -213,9 +225,9 @@ Proof.
   destruct t2; simpl; auto.
   destruct t2; simpl. destruct ev; auto. inv H1.
   inv H; inv H5; auto; intros.
-  subst. rewrite H in H1; inv H1. split; eauto.
-  eauto.
-  eauto.
+  destruct H2. subst. rewrite H in H1; inv H1. split; eauto.
+  destruct H2. destruct H3. subst. rewrite H in H1; inv H1. split; eauto.
+  destruct H2. destruct H3. destruct H4. subst. rewrite H in H1; inv H1. eauto.
 Qed.
 
 Lemma step_deterministic:
diff --git a/common/Events.v b/common/Events.v
index ad1fc51..a666b40 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -29,28 +29,38 @@ Require Import Memory.
   input/output events, which represent the actions of the program
   that the external world can observe.  CompCert leaves much flexibility as to
   the exact content of events: the only requirement is that they
-  do not expose pointer values nor memory states, because these
+  do not expose memory states nor pointer values 
+  (other than pointers to global variables), because these
   are not preserved literally during compilation.  For concreteness,
   we use the following type for events.  Each event represents either:
 
 - A system call (e.g. an input/output operation), recording the
-  name of the system call, its int-or-float parameters,
-  and its int-or-float result.
+  name of the system call, its parameters, and its result.
 
-- A volatile load from a memory location, recording a label
-  associated with the read (e.g. a global variable name or a source code position).
+- A volatile load from a global memory location, recording the chunk
+  and address being read and the value just read. 
 
-- A volatile store to a memory location, also recording a label.
+- A volatile store to a global memory location, recording the chunk
+  and address being written and the value stored there. 
+
+  The values attached to these events are of the following form.
+  As mentioned above, we do not expose pointer values directly.
+  Pointers relative to a global variable are shown with the name
+  of the variable instead of the block identifier.
+  Pointers within a dynamically-allocated block are collapsed
+  to the [EVptr_local] constant.
 *)
 
 Inductive eventval: Type :=
   | EVint: int -> eventval
-  | EVfloat: float -> eventval.
+  | EVfloat: float -> eventval
+  | EVptr_global: ident -> int -> eventval
+  | EVptr_local: eventval.
 
 Inductive event: Type :=
   | Event_syscall: ident -> list eventval -> eventval -> event
-  | Event_load: ident -> event
-  | Event_store: ident -> event.
+  | Event_vload: memory_chunk -> ident -> int -> eventval -> event
+  | Event_vstore: memory_chunk -> ident -> int -> eventval -> event.
 
 (** The dynamic semantics for programs collect traces of events.
   Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *)
@@ -236,6 +246,107 @@ Transparent Eappinf.
   simpl. f_equal. apply IHt. 
 Qed.
 
+(** * Relating values and event values *)
+
+Section EVENTVAL.
+
+(** Parameter to translate between global variable names and their block identifiers. *)
+Variable symb: ident -> option block.
+
+(** Translation from a value to an event value. *)
+
+Inductive eventval_of_val: val -> eventval -> Prop :=
+  | evofv_int: forall i,
+      eventval_of_val (Vint i) (EVint i)
+  | evofv_float: forall f,
+      eventval_of_val (Vfloat f) (EVfloat f)
+  | evofv_ptr_global: forall id b ofs,
+      symb id = Some b ->
+      eventval_of_val (Vptr b ofs) (EVptr_global id ofs)
+  | evofv_ptr_local: forall b ofs,
+      (forall id, symb id <> Some b) ->
+      eventval_of_val (Vptr b ofs) EVptr_local.
+
+(** Translation from an event value to a value.  To preserve determinism,
+  the translation is undefined if the event value is [EVptr_local]. *)
+
+Inductive val_of_eventval: eventval -> typ -> val -> Prop :=
+  | voffv_int: forall i,
+      val_of_eventval (EVint i) Tint (Vint i)
+  | voffv_float: forall f,
+      val_of_eventval (EVfloat f) Tfloat (Vfloat f)
+  | voffv_ptr_global: forall id b ofs,
+      symb id = Some b ->
+      val_of_eventval (EVptr_global id ofs) Tint (Vptr b ofs).
+
+(** Some properties of these translation predicates. *)
+
+Lemma val_of_eventval_type:
+  forall ev ty v,
+  val_of_eventval ev ty v -> Val.has_type v ty.
+Proof.
+  intros. inv H; constructor.
+Qed.
+
+Lemma eventval_of_val_lessdef:
+  forall v1 v2 ev,
+  eventval_of_val v1 ev -> Val.lessdef v1 v2 -> eventval_of_val v2 ev.
+Proof.
+  intros. inv H; inv H0; constructor; auto.
+Qed.
+
+Variable f: block -> option (block * Z).
+
+Definition meminj_preserves_globals : Prop :=
+     (forall id b, symb id = Some b -> f b = Some(b, 0))
+  /\ (forall id b1 b2 delta, symb id = Some b2 -> f b1 = Some(b2, delta) -> b2 = b1).
+
+Lemma eventval_of_val_inject:
+  forall v1 v2 ev,
+  meminj_preserves_globals ->
+  eventval_of_val v1 ev -> val_inject f v1 v2 -> eventval_of_val v2 ev.
+Proof.
+  intros. destruct H. inv H0; inv H1.
+  constructor. constructor. 
+  exploit H; eauto. intro EQ. rewrite H5 in EQ; inv EQ.
+  rewrite Int.add_zero. constructor; auto.
+  constructor. intros; red; intros. 
+  exploit H2; eauto. intro EQ. elim (H3 id). congruence.
+Qed.
+
+Lemma val_of_eventval_inject:
+  forall ev ty v,
+  meminj_preserves_globals ->
+  val_of_eventval ev ty v -> val_inject f v v.
+Proof.
+  intros. destruct H. inv H0. 
+  constructor. constructor.
+  apply val_inject_ptr with 0. eauto. rewrite Int.add_zero; auto.
+Qed.
+
+Definition symbols_injective: Prop :=
+  forall id1 id2 b, symb id1 = Some b -> symb id2 = Some b -> id1 = id2.
+
+Remark eventval_of_val_determ:
+  forall v ev1 ev2,
+  symbols_injective ->
+  eventval_of_val v ev1 -> eventval_of_val v ev2 -> ev1 = ev2.
+Proof.
+  intros. inv H0; inv H1; auto.
+  exploit (H id id0); eauto. congruence.
+  elim (H5 _ H2).
+  elim (H2 _ H5).
+Qed.
+
+Remark val_of_eventval_determ:
+  forall ev ty v1 v2,
+  val_of_eventval ev ty v1 -> val_of_eventval ev ty v2 -> v1 = v2.
+Proof.
+  intros. inv H; inv H0; auto. congruence.
+Qed.
+
+End EVENTVAL.
+
 (** * Semantics of external functions *)
 
 (** Each external function is of one of the following kinds: *)
@@ -245,15 +356,20 @@ Inductive extfun_kind: signature -> Type :=
      (** A system call.  Takes integer-or-float arguments, produces a
          result that is an integer or a float, does not modify
          the memory, and produces an [Event_syscall] event in the trace. *)
-  | EF_load (label: ident) (chunk: memory_chunk): extfun_kind (mksignature (Tint :: nil) (Some (type_of_chunk chunk)))
+  | EF_vload (chunk: memory_chunk): extfun_kind (mksignature (Tint :: nil) (Some (type_of_chunk chunk)))
      (** A volatile read operation.  Reads and returns the given memory
-         chunk from the address given as first argument.
-         Produces an [Event_load] event containing the given label. *)
-  | EF_store (label: ident) (chunk: memory_chunk): extfun_kind (mksignature (Tint :: type_of_chunk chunk :: nil) None)
+         chunk from the address given as first argument.  Since this is
+         a volatile access, the contents of this address may have changed
+         asynchronously since the last write we did at this address.
+         To account for this fact, we first update the given address
+         with a value that is provided by the outside world through
+         the trace of events.
+         Produces an [Event_load] event. *)
+  | EF_vstore (chunk: memory_chunk): extfun_kind (mksignature (Tint :: type_of_chunk chunk :: nil) None)
      (** A volatile store operation.  Store the value given as second
          argument at the address given as first argument, using the
          given memory chunk.  
-         Produces an [Event_store] event containing the given label. *)
+         Produces an [Event_store] event. *)
   | EF_malloc: extfun_kind (mksignature (Tint :: nil) (Some Tint))
      (** Dynamic memory allocation.  Takes the requested size in bytes
          as argument; returns a pointer to a fresh block of the given size.
@@ -268,15 +384,19 @@ Parameter classify_external_function:
   forall (ef: external_function), extfun_kind (ef.(ef_sig)).
 
 (** For each external function, its behavior is defined by a predicate relating:
+- the mapping from global variables to blocks
 - the values of the arguments passed to this function
 - the memory state before the call
 - the result value of the call
 - the memory state after the call
 - the trace generated by the call (can be empty).
-
-We now specify the expected properties of this predicate.
 *)
 
+Definition extcall_sem : Type :=
+  (ident -> option block) -> list val -> mem -> trace -> val -> mem -> Prop.
+
+(** We now specify the expected properties of this predicate. *)
+
 Definition mem_unchanged_on (P: block -> Z -> Prop) (m_before m_after: mem): Prop :=
   (forall b ofs p,
    P b ofs -> Mem.perm m_before b ofs p -> Mem.perm m_after b ofs p)
@@ -304,52 +424,52 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop :=
 Fixpoint matching_traces (t1 t2: trace) {struct t1} : Prop :=
   match t1, t2 with
   | Event_syscall name1 args1 res1 :: t1', Event_syscall name2 args2 res2 :: t2' =>
-      name1 = name2 -> args1 = args2 -> res1 = res2 /\ matching_traces t1' t2'
-  | Event_load name1 :: t1', Event_load name2 :: t2' =>
-      name1 = name2 -> matching_traces t1' t2'
-  | Event_store name1 :: t1', Event_store name2 :: t2' =>
-      name1 = name2 -> matching_traces t1' t2'
+      name1 = name2 /\ args1 = args2 -> res1 = res2 /\ matching_traces t1' t2'
+  | Event_vload chunk1 id1 ofs1 res1 :: t1', Event_vload chunk2 id2 ofs2 res2 :: t2' =>
+      chunk1 = chunk2 /\ id1 = id2 /\ ofs1 = ofs2 -> res1 = res2 /\ matching_traces t1' t2'
+  | Event_vstore chunk1 id1 ofs1 arg1 :: t1', Event_vstore chunk2 id2 ofs2 arg2 :: t2' =>
+      chunk1 = chunk2 /\ id1 = id2 /\ ofs1 = ofs2 /\ arg1 = arg2 -> matching_traces t1' t2'
   | _, _ =>
       True
   end.
 
-Record extcall_properties (sem: list val -> mem -> trace -> val -> mem -> Prop)
+Record extcall_properties (sem: extcall_sem)
                           (sg: signature) : Prop := mk_extcall_properties {
 
 (** The return value of an external call must agree with its signature. *)
   ec_well_typed:
-    forall vargs m1 t vres m2,
-    sem vargs m1 t vres m2 ->
+    forall symb vargs m1 t vres m2,
+    sem symb vargs m1 t vres m2 ->
     Val.has_type vres (proj_sig_res sg);
 
 (** The number of arguments of an external call must agree with its signature. *)
   ec_arity:
-    forall vargs m1 t vres m2,
-    sem vargs m1 t vres m2 ->
+    forall symb vargs m1 t vres m2,
+    sem symb vargs m1 t vres m2 ->
     List.length vargs = List.length sg.(sig_args);
 
 (** External calls cannot invalidate memory blocks.  (Remember that
   freeing a block does not invalidate its block identifier.) *)
   ec_valid_block:
-    forall vargs m1 t vres m2 b,
-    sem vargs m1 t vres m2 ->
+    forall symb vargs m1 t vres m2 b,
+    sem symb vargs m1 t vres m2 ->
     Mem.valid_block m1 b -> Mem.valid_block m2 b;
 
 (** External calls preserve the bounds of valid blocks. *)
   ec_bounds:
-    forall vargs m1 t vres m2 b,
-    sem vargs m1 t vres m2 ->
+    forall symb vargs m1 t vres m2 b,
+    sem symb vargs m1 t vres m2 ->
     Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b;
 
 (** External calls must commute with memory extensions, in the
   following sense. *)
   ec_mem_extends:
-    forall vargs m1 t vres m2 m1' vargs',
-    sem vargs m1 t vres m2 ->
+    forall symb vargs m1 t vres m2 m1' vargs',
+    sem symb vargs m1 t vres m2 ->
     Mem.extends m1 m1' ->
     Val.lessdef_list vargs vargs' ->
     exists vres', exists m2',
-       sem vargs' m1' t vres' m2'
+       sem symb vargs' m1' t vres' m2'
     /\ Val.lessdef vres vres'
     /\ Mem.extends m2 m2'
     /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2';
@@ -357,12 +477,13 @@ Record extcall_properties (sem: list val -> mem -> trace -> val -> mem -> Prop)
 (** External calls must commute with memory injections,
   in the following sense. *)
   ec_mem_inject:
-    forall vargs m1 t vres m2 f m1' vargs',
-    sem vargs m1 t vres m2 ->
+    forall symb vargs m1 t vres m2 f m1' vargs',
+    meminj_preserves_globals symb f ->
+    sem symb vargs m1 t vres m2 ->
     Mem.inject f m1 m1' ->
     val_list_inject f vargs vargs' ->
     exists f', exists vres', exists m2',
-       sem vargs' m1' t vres' m2'
+       sem symb vargs' m1' t vres' m2'
     /\ val_inject f' vres vres'
     /\ Mem.inject f' m2 m2'
     /\ mem_unchanged_on (loc_unmapped f) m1 m2
@@ -374,64 +495,111 @@ Record extcall_properties (sem: list val -> mem -> trace -> val -> mem -> Prop)
   if the observable traces match, the return states must be
   identical. *)
   ec_determ:
-    forall vargs m t1 vres1 m1 t2 vres2 m2,
-    sem vargs m t1 vres1 m1 -> sem vargs m t2 vres2 m2 ->
+    forall symb vargs m t1 vres1 m1 t2 vres2 m2,
+    symbols_injective symb ->
+    sem symb vargs m t1 vres1 m1 -> sem symb vargs m t2 vres2 m2 ->
     matching_traces t1 t2 -> t1 = t2 /\ vres1 = vres2 /\ m1 = m2
 }.
 
 (** ** Semantics of volatile loads *)
 
-Inductive extcall_load_sem (label: ident) (chunk: memory_chunk):
-      list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_load_sem_intro: forall b ofs m vres,
-      Mem.load chunk m b (Int.signed ofs) = Some vres ->
-      extcall_load_sem label chunk (Vptr b ofs :: nil) m (Event_load label :: nil) vres m.
-
-Lemma extcall_load_ok:
-  forall label chunk,
-  extcall_properties (extcall_load_sem label chunk) 
+Inductive volatile_load_sem (chunk: memory_chunk): extcall_sem :=
+  | volatile_load_sem_intro: forall symb b ofs m id ev v m' res,
+      symb id = Some b ->
+      val_of_eventval symb ev (type_of_chunk chunk) v ->
+      Mem.store chunk m b (Int.signed ofs) v = Some m' ->
+      Mem.load chunk m' b (Int.signed ofs) = Some res ->
+      volatile_load_sem chunk symb
+        (Vptr b ofs :: nil) m
+        (Event_vload chunk id ofs ev :: nil)
+        res m'.
+
+Lemma volatile_load_ok:
+  forall chunk,
+  extcall_properties (volatile_load_sem chunk) 
                      (mksignature (Tint :: nil) (Some (type_of_chunk chunk))).
 Proof.
   intros; constructor; intros.
 
-  inv H. unfold proj_sig_res. simpl. eapply Mem.load_type; eauto.
+  inv H. unfold proj_sig_res. simpl. eapply Mem.load_type; eauto. 
 
   inv H. simpl. auto.
 
-  inv H. auto.
+  inv H. eauto with mem. 
 
-  inv H. auto.
+  inv H. eapply Mem.bounds_store; eauto. 
 
-  inv H. inv H1. inv H6. inv H4. 
-  exploit Mem.load_extends; eauto. intros [v2 [A B]].
-  exists v2; exists m1'; intuition. 
-  constructor; auto. 
-  red. auto. 
-
-  inv H. inv H1. inv H6.
-  assert (Mem.loadv chunk m2 (Vptr b ofs) = Some vres). auto. 
-  exploit Mem.loadv_inject; eauto. intros [v2 [A B]].
-  inv H4. 
-  exists f; exists v2; exists m1'; intuition.
-  constructor. auto. 
-  red; auto.
-  red; auto.
+  inv H. inv H1. inv H7. inv H9.
+  exploit Mem.store_within_extends; eauto. intros [m2' [A B]].
+  exploit Mem.load_extends; eauto. intros [vres' [C D]].
+  exists vres'; exists m2'.
+  split. econstructor; eauto. 
+  split. auto.
+  split. auto.
+  red; split; intros.
+  eapply Mem.perm_store_1; eauto.
+  rewrite <- H1. eapply Mem.load_store_other; eauto.
+  destruct (eq_block b0 b); auto. subst b0; right. 
+  exploit Mem.valid_access_in_bounds. 
+  eapply Mem.store_valid_access_3. eexact H4.
+  intros [P Q].
+  generalize (size_chunk_pos chunk0). intro E.
+  generalize (size_chunk_pos chunk). intro F.
+  apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
+                              (Int.signed ofs, Int.signed ofs + size_chunk chunk)).
+  red; intros. generalize (H x H6). unfold loc_out_of_bounds, Intv.In; simpl. omega.
+  simpl; omega. simpl; omega.
+
+  inv H0. inv H2. inv H8. inv H10.
+  exploit val_of_eventval_inject; eauto. intro INJ.
+  exploit Mem.store_mapped_inject; eauto. intros [m2' [A B]].
+  exploit Mem.load_inject; eauto. intros [vres' [C D]].
+  exists f; exists vres'; exists m2'; intuition.
+  destruct H as [P Q].
+  rewrite (P _ _ H3) in H7. inv H7. rewrite Int.add_zero.
+  econstructor; eauto.
+  replace (Int.signed ofs) with (Int.signed ofs + 0) by omega; auto.  
+  replace (Int.signed ofs) with (Int.signed ofs + 0) by omega; auto.  
+  split; intros. eapply Mem.perm_store_1; eauto.
+  rewrite <- H2. eapply Mem.load_store_other; eauto. 
+  left. exploit (H0 ofs0). generalize (size_chunk_pos chunk0). omega. 
+  unfold loc_unmapped. congruence.
+  split; intros. eapply Mem.perm_store_1; eauto.
+  rewrite <- H2. eapply Mem.load_store_other; eauto.
+  destruct (eq_block b0 b2); auto. subst b0; right.
+  exploit Mem.valid_access_in_bounds. 
+  eapply Mem.store_valid_access_3. eexact H5.
+  intros [P Q].
+  generalize (size_chunk_pos chunk0). intro E.
+  generalize (size_chunk_pos chunk). intro F.
+  apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
+                              (Int.signed ofs + delta, Int.signed ofs + delta + size_chunk chunk)).
+  red; intros. exploit (H0 x H8). eauto. unfold Intv.In; simpl. omega.
+  simpl; omega. simpl; omega.
   red; intros. congruence.
 
-  inv H; inv H0. intuition congruence.
+  inv H0. inv H1. simpl in H2.
+  assert (id = id0) by (eapply H; eauto). subst id0.
+  assert (ev = ev0) by intuition. subst ev0.
+  exploit val_of_eventval_determ. eexact H4. eexact H9. intro. 
+  intuition congruence.
 Qed.
 
 (** ** Semantics of volatile stores *)
 
-Inductive extcall_store_sem (label: ident) (chunk: memory_chunk):
-      list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_store_sem_intro: forall b ofs v m m',
+Inductive volatile_store_sem (chunk: memory_chunk): extcall_sem :=
+  | volatile_store_sem_intro: forall symb b ofs v id ev m m',
+      symb id = Some b ->
+      eventval_of_val symb v ev ->
       Mem.store chunk m b (Int.signed ofs) v = Some m' ->
-      extcall_store_sem label chunk (Vptr b ofs :: v :: nil) m (Event_store label :: nil) Vundef m'.
-
-Lemma extcall_store_ok:
-  forall label chunk,
-  extcall_properties (extcall_store_sem label chunk) 
+      volatile_store_sem chunk symb
+        (Vptr b ofs :: v :: nil) m
+        (Event_vstore chunk id ofs ev :: nil)
+         Vundef m'.
+
+Lemma volatile_store_ok:
+  forall chunk,
+  extcall_properties (volatile_store_sem chunk) 
                      (mksignature (Tint :: type_of_chunk chunk :: nil) None).
 Proof.
   intros; constructor; intros.
@@ -444,63 +612,63 @@ Proof.
 
   inv H. eapply Mem.bounds_store; eauto. 
 
-  inv H. inv H1. inv H6. inv H7. inv H4.
+  inv H. inv H1. inv H6. inv H8. inv H7. 
   exploit Mem.store_within_extends; eauto. intros [m' [A B]].
   exists Vundef; exists m'; intuition.
-  constructor; auto.
+  constructor; auto. eapply eventval_of_val_lessdef; eauto. 
   red; split; intros.
   eapply Mem.perm_store_1; eauto.
   rewrite <- H1. eapply Mem.load_store_other; eauto.
   destruct (eq_block b0 b); auto. subst b0; right. 
   exploit Mem.valid_access_in_bounds. 
-  eapply Mem.store_valid_access_3. eexact H2.
+  eapply Mem.store_valid_access_3. eexact H4.
   intros [C D].
   generalize (size_chunk_pos chunk0). intro E.
   generalize (size_chunk_pos chunk). intro F.
   apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
                               (Int.signed ofs, Int.signed ofs + size_chunk chunk)).
-  red; intros. generalize (H x H4). unfold loc_out_of_bounds, Intv.In; simpl. omega.
+  red; intros. generalize (H x H6). unfold loc_out_of_bounds, Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
 
-  inv H. inv H1. inv H6. inv H7.
-  assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto.
-  exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]].
-  inv H4. 
+  inv H0. inv H2. inv H7. inv H9. inv H10.
+  exploit Mem.store_mapped_inject; eauto. intros [m2' [A B]].
   exists f; exists Vundef; exists m2'; intuition.
-  constructor; auto. 
+  elim H; intros P Q. 
+  rewrite (P _ _ H3) in H6. inv H6. rewrite Int.add_zero. econstructor; eauto.
+  eapply eventval_of_val_inject; eauto. 
+  replace (Int.signed ofs) with (Int.signed ofs + 0) by omega; auto.
   split; intros. eapply Mem.perm_store_1; eauto.
-  rewrite <- H4. eapply Mem.load_store_other; eauto. 
-  left. exploit (H1 ofs0). generalize (size_chunk_pos chunk0). omega. 
+  rewrite <- H2. eapply Mem.load_store_other; eauto. 
+  left. exploit (H0 ofs0). generalize (size_chunk_pos chunk0). omega. 
   unfold loc_unmapped. congruence.
   split; intros. eapply Mem.perm_store_1; eauto.
-  rewrite <- H4. eapply Mem.load_store_other; eauto.
+  rewrite <- H2. eapply Mem.load_store_other; eauto.
   destruct (eq_block b0 b2); auto. subst b0; right.
-  assert (EQ: Int.signed (Int.add ofs (Int.repr delta)) = Int.signed ofs + delta).
-    eapply Mem.address_inject; eauto with mem.
-  simpl in A. rewrite EQ in A. rewrite EQ.
   exploit Mem.valid_access_in_bounds. 
-  eapply Mem.store_valid_access_3. eexact H2.
+  eapply Mem.store_valid_access_3. eexact H5.
   intros [C D].
   generalize (size_chunk_pos chunk0). intro E.
   generalize (size_chunk_pos chunk). intro F.
   apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
                               (Int.signed ofs + delta, Int.signed ofs + delta + size_chunk chunk)).
-  red; intros. exploit (H1 x H5). eauto. unfold Intv.In; simpl. omega.
+  red; intros. exploit (H0 x H8). eauto. unfold Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
 
   red; intros. congruence.
 
-  inv H; inv H0. intuition congruence.
+  inv H0; inv H1.
+  assert (id = id0) by (eapply H; eauto).
+  exploit eventval_of_val_determ. eauto. eexact H4. eexact H14. intros.
+  intuition congruence.
 Qed.
 
 (** ** Semantics of dynamic memory allocation (malloc) *)
 
-Inductive extcall_malloc_sem:
-      list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_malloc_sem_intro: forall n m m' b m'',
+Inductive extcall_malloc_sem: extcall_sem :=
+  | extcall_malloc_sem_intro: forall symb n m m' b m'',
       Mem.alloc m (-4) (Int.signed n) = (m', b) ->
       Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
-      extcall_malloc_sem (Vint n :: nil) m E0 (Vptr b Int.zero) m''.
+      extcall_malloc_sem symb (Vint n :: nil) m E0 (Vptr b Int.zero) m''.
 
 Lemma extcall_malloc_ok:
   extcall_properties extcall_malloc_sem 
@@ -541,7 +709,7 @@ Proof.
   econstructor; eauto.
   eapply UNCHANGED; eauto.
 
-  inv H. inv H1. inv H5. inv H7.
+  inv H0. inv H2. inv H6. inv H8.
   exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. 
   intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
   exploit Mem.store_mapped_inject. eexact A. eauto. eauto. 
@@ -553,21 +721,20 @@ Proof.
   eapply UNCHANGED; eauto.
   eapply UNCHANGED; eauto.
   red; intros. destruct (eq_block b1 b). 
-  subst b1. rewrite C in H1. inv H1. eauto with mem. 
-  rewrite D in H1. congruence. auto. 
+  subst b1. rewrite C in H2. inv H2. eauto with mem. 
+  rewrite D in H2. congruence. auto. 
 
-  inv H; inv H0. intuition congruence. 
+  inv H0; inv H1. intuition congruence. 
 Qed.
 
 (** ** Semantics of dynamic memory deallocation (free) *)
 
-Inductive extcall_free_sem:
-      list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_free_sem_intro: forall b lo sz m m',
+Inductive extcall_free_sem: extcall_sem :=
+  | extcall_free_sem_intro: forall symb b lo sz m m',
       Mem.load Mint32 m b (Int.signed lo - 4) = Some (Vint sz) ->
       Int.signed sz > 0 ->
       Mem.free m b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) = Some m' ->
-      extcall_free_sem (Vptr b lo :: nil) m E0 Vundef m'.
+      extcall_free_sem symb (Vptr b lo :: nil) m E0 Vundef m'.
 
 Lemma extcall_free_ok:
   extcall_properties extcall_free_sem 
@@ -592,7 +759,7 @@ Proof.
 
   inv H. unfold proj_sig_res. simpl. auto.
 
-  inv H. auto. 
+  inv H. auto.
 
   inv H. eauto with mem.
 
@@ -609,19 +776,19 @@ Proof.
   exploit Mem.range_perm_in_bounds. 
   eapply Mem.free_range_perm. eexact H4. omega. omega.
 
-  inv H. inv H1. inv H8. inv H6.
+  inv H0. inv H2. inv H7. inv H9.
   exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. 
   assert (Mem.range_perm m1 b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) Freeable).
     eapply Mem.free_range_perm; eauto.
   exploit Mem.address_inject; eauto. 
     apply Mem.perm_implies with Freeable; auto with mem.
-    apply H. instantiate (1 := lo). omega. 
+    apply H0. instantiate (1 := lo). omega. 
   intro EQ.
   assert (Mem.range_perm m1' b2 (Int.signed lo + delta - 4) (Int.signed lo + delta + Int.signed sz) Freeable).
     red; intros. 
     replace ofs with ((ofs - delta) + delta) by omega.
-    eapply Mem.perm_inject; eauto. apply H. omega. 
-  destruct (Mem.range_perm_free _ _ _ _ H1) as [m2' FREE].
+    eapply Mem.perm_inject; eauto. apply H0. omega. 
+  destruct (Mem.range_perm_free _ _ _ _ H2) as [m2' FREE].
   exists f; exists Vundef; exists m2'; intuition.
 
   econstructor.
@@ -630,7 +797,7 @@ Proof.
   rewrite EQ. auto.
   
   assert (Mem.free_list m1 ((b, Int.signed lo - 4, Int.signed lo + Int.signed sz) :: nil) = Some m2).
-    simpl. rewrite H4. auto.
+    simpl. rewrite H5. auto.
   eapply Mem.free_inject; eauto. 
   intros. destruct (eq_block b b1).
   subst b. assert (delta0 = delta) by congruence. subst delta0. 
@@ -640,108 +807,30 @@ Proof.
   exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. 
   instantiate (1 := ofs + delta0 - delta). 
   apply Mem.perm_implies with Freeable; auto with mem.
-  apply H. omega. eauto with mem.
+  apply H0. omega. eauto with mem.
   unfold block; omega.
 
   eapply UNCHANGED; eauto. omega. intros.  
-  red in H6. left. congruence. 
+  red in H7. left. congruence. 
 
   eapply UNCHANGED; eauto. omega. intros.
   destruct (eq_block b' b2); auto. subst b'. right. 
-  red in H6. generalize (H6 _ _ H5). intros. 
-  exploit Mem.range_perm_in_bounds. eexact H. omega. intros. omega.
+  red in H7. generalize (H7 _ _ H6). intros. 
+  exploit Mem.range_perm_in_bounds. eexact H0. omega. intros. omega.
 
   red; intros. congruence.
 
-  inv H; inv H0. intuition congruence.
+  inv H0; inv H1. intuition congruence.
 Qed.
 
 (** ** Semantics of system calls. *)
 
-Inductive eventval_match: eventval -> typ -> val -> Prop :=
-  | ev_match_int:
-      forall i, eventval_match (EVint i) Tint (Vint i)
-  | ev_match_float:
-      forall f, eventval_match (EVfloat f) Tfloat (Vfloat f).
-
-Inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
-  | evl_match_nil:
-      eventval_list_match nil nil nil
-  | evl_match_cons:
-      forall ev1 evl ty1 tyl v1 vl,
-      eventval_match ev1 ty1 v1 ->
-      eventval_list_match evl tyl vl ->
-      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).
-
-Inductive extcall_io_sem (name: ident) (sg: signature):
-      list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_io_sem_intro: forall vargs m args res vres,
-      eventval_list_match args (sig_args sg) vargs ->
-      eventval_match res (proj_sig_res sg) vres ->
-      extcall_io_sem name sg vargs m (Event_syscall name args res :: E0) vres m.
-
-Remark eventval_match_lessdef:
-  forall ev ty v1 v2,
-  eventval_match ev ty v1 -> Val.lessdef v1 v2 -> eventval_match ev ty v2.
-Proof.
-  intros. inv H; inv H0; constructor.
-Qed.
-
-Remark eventval_list_match_lessdef:
-  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
-  forall vl2, Val.lessdef_list vl1 vl2 -> eventval_list_match evl tyl vl2.
-Proof.
-  induction 1; intros. inv H; constructor.
-  inv H1. constructor. eapply eventval_match_lessdef; eauto. eauto.
-Qed.
-
-Remark eventval_match_inject:
-  forall f ev ty v1 v2,
-  eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2.
-Proof.
-  intros. inv H; inv H0; constructor.
-Qed.
-
-Remark eventval_match_inject_2:
-  forall f ev ty v,
-  eventval_match ev ty v -> val_inject f v v.
-Proof.
-  induction 1; constructor.
-Qed.
-
-Remark eventval_list_match_inject:
-  forall f evl tyl vl1, eventval_list_match evl tyl vl1 ->
-  forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match evl tyl vl2.
-Proof.
-  induction 1; intros. inv H; constructor.
-  inv H1. constructor. eapply eventval_match_inject; eauto. eauto.
-Qed.
-
-Remark eventval_list_match_length:
-  forall evl tyl vl, eventval_list_match evl tyl vl -> List.length vl = List.length tyl.
-Proof.
-  induction 1; simpl; eauto.
-Qed.
-
-Remark eventval_match_determ_1:
-  forall ev ty v1 v2, eventval_match ev ty v1 -> eventval_match ev ty v2 -> v1 = v2.
-Proof.
-  intros. inv H; inv H0; auto.
-Qed.
-
-Remark eventval_match_determ_2:
-  forall ev1 ev2 ty v, eventval_match ev1 ty v -> eventval_match ev2 ty v -> ev1 = ev2.
-Proof.
-  intros. inv H; inv H0; auto.
-Qed.
-
-Remark eventval_list_match_determ_2:
-  forall evl1 tyl vl, eventval_list_match evl1 tyl vl ->
-  forall evl2, eventval_list_match evl2 tyl vl -> evl1 = evl2.
-Proof.
-  induction 1; intros. inv H. auto. inv H1. f_equal; eauto.
-  eapply eventval_match_determ_2; eauto.
-Qed.
+Inductive extcall_io_sem (name: ident) (sg: signature): extcall_sem :=
+  | extcall_io_sem_intro: forall symb vargs m args res vres,
+      length vargs = length (sig_args sg) ->
+      list_forall2 (eventval_of_val symb) vargs args ->
+      val_of_eventval symb res (proj_sig_res sg) vres ->
+      extcall_io_sem name sg symb vargs m (Event_syscall name args res :: E0) vres m.
 
 Lemma extcall_io_ok:
   forall name sg,
@@ -749,9 +838,9 @@ Lemma extcall_io_ok:
 Proof.
   intros; constructor; intros.
 
-  inv H. inv H1; constructor. 
+  inv H. eapply val_of_eventval_type; eauto.
 
-  inv H. eapply eventval_list_match_length; eauto.
+  inv H. auto.
 
   inv H; auto.
 
@@ -759,21 +848,34 @@ Proof.
 
   inv H.
   exists vres; exists m1'; intuition.
-  econstructor; eauto. eapply eventval_list_match_lessdef; eauto.
+  econstructor; eauto.
+  rewrite <- H2.
+  generalize vargs vargs' H1. induction 1; simpl; congruence.
+  generalize vargs vargs' H1 args H3. induction 1; intros.
+  inv H5. constructor.
+  inv H6. constructor; eauto. eapply eventval_of_val_lessdef; eauto. 
   red; auto.
 
-  inv H.
+  inv H0.
   exists f; exists vres; exists m1'; intuition.
-  econstructor; eauto. eapply eventval_list_match_inject; eauto. 
-  eapply eventval_match_inject_2; eauto. 
+  econstructor; eauto.
+  rewrite <- H3.
+  generalize vargs vargs' H2. induction 1; simpl; congruence.
+  generalize vargs vargs' H2 args H4. induction 1; intros.
+  inv H0. constructor.
+  inv H7. constructor; eauto. eapply eventval_of_val_inject; eauto. 
+  eapply val_of_eventval_inject; eauto.
   red; auto.
   red; auto.
   red; intros; congruence.
 
-  inv H; inv H0. simpl in H1.
-  assert (args = args0) by (eapply eventval_list_match_determ_2; eauto).
-  destruct H1; auto. subst.
-  intuition. eapply eventval_match_determ_1; eauto. 
+  inv H0; inv H1. simpl in H2.
+  assert (args = args0).
+    generalize vargs args H4 args0 H6. induction 1; intros.
+    inv H1; auto.
+    inv H9. decEq; eauto. eapply eventval_of_val_determ; eauto. 
+  destruct H2; auto. subst.
+  intuition. eapply val_of_eventval_determ; eauto. 
 Qed.
 
 (** ** Combined semantics of external calls *)
@@ -789,12 +891,11 @@ Qed.
 
 This predicate is used in the semantics of all CompCert languages. *)
 
-Definition external_call (ef: external_function):
-         list val -> mem -> trace -> val -> mem -> Prop :=
+Definition external_call (ef: external_function): extcall_sem :=
   match classify_external_function ef with
   | EF_syscall sg name   => extcall_io_sem name sg
-  | EF_load label chunk  => extcall_load_sem label chunk
-  | EF_store label chunk => extcall_store_sem label chunk
+  | EF_vload chunk       => volatile_load_sem chunk
+  | EF_vstore chunk      => volatile_store_sem chunk
   | EF_malloc            => extcall_malloc_sem 
   | EF_free              => extcall_free_sem
   end.
@@ -805,8 +906,8 @@ Theorem external_call_spec:
 Proof.
   intros. unfold external_call. destruct (classify_external_function ef). 
   apply extcall_io_ok.
-  apply extcall_load_ok.
-  apply extcall_store_ok.
+  apply volatile_load_ok.
+  apply volatile_store_ok.
   apply extcall_malloc_ok.
   apply extcall_free_ok.
 Qed.
@@ -818,3 +919,15 @@ Definition external_call_bounds ef := ec_bounds _ _ (external_call_spec ef).
 Definition external_call_mem_extends ef := ec_mem_extends _ _ (external_call_spec ef).
 Definition external_call_mem_inject ef := ec_mem_inject _ _ (external_call_spec ef).
 Definition external_call_determ ef := ec_determ _ _ (external_call_spec ef).
+
+(** The only dependency on the global environment is on the addresses of symbols. *)
+
+Lemma external_call_symbols_preserved:
+  forall ef symb1 symb2 vargs m1 t vres m2,
+  external_call ef symb1 vargs m1 t vres m2 ->
+  (forall id, symb2 id = symb1 id) ->
+  external_call ef symb2 vargs m1 t vres m2.
+Proof.
+  intros. replace symb2 with symb1; auto. 
+  symmetry. apply extensionality. auto.
+Qed.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 9dbf902..65ae06c 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -71,7 +71,9 @@ Record t: Type := mkgenv {
   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_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar;
+  genv_vars_inj: forall id1 id2 b, 
+    PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
 }.
 
 (** ** Lookup functions *)
@@ -111,7 +113,7 @@ Program Definition add_function (ge: t) (idf: ident * F) : t :=
     ge.(genv_vars)
     (ge.(genv_nextfun) - 1)
     ge.(genv_nextvar)
-    _ _ _ _ _.
+    _ _ _ _ _ _.
 Next Obligation.
   destruct ge; simpl; omega.
 Qed.
@@ -131,6 +133,15 @@ 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 * list init_data * V) : t :=
   @mkgenv
@@ -139,7 +150,7 @@ Program Definition add_variable (ge: t) (idv: ident * list init_data * V) : t :=
     (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars))
     ge.(genv_nextfun)
     (ge.(genv_nextvar) + 1)
-    _ _ _ _ _.
+    _ _ _ _ _ _.
 Next Obligation.
   destruct ge; auto.
 Qed.
@@ -159,9 +170,18 @@ Next Obligation.
   destruct (ZIndexed.eq b genv_nextvar0). subst; omega. 
   exploit genv_vars_range0; eauto. omega.
 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 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) 1 _ _ _ _ _ _.
 Next Obligation.
   omega.
 Qed.
@@ -177,6 +197,9 @@ Qed.
 Next Obligation.
   rewrite ZMap.gi in H. discriminate.
 Qed.
+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.
@@ -435,38 +458,13 @@ Proof.
 Qed.
 
 Theorem global_addresses_distinct:
-  forall p id1 id2 b1 b2,
-  id1<>id2 ->
-  find_symbol (globalenv p) id1 = Some b1 ->
-  find_symbol (globalenv p) id2 = Some b2 ->
-  b1<>b2.
-Proof.
-  intros until b2; intro DIFF. 
-  
-  set (P := fun ge => find_symbol ge id1 = Some b1 -> find_symbol ge id2 = Some b2 -> b1 <> b2).
-
-  assert (forall fl ge, P ge -> P (add_functions ge fl)).
-  induction fl; intros; simpl. auto. 
-  apply IHfl. red. unfold find_symbol; simpl. 
-  repeat rewrite PTree.gsspec. 
-  fold ident. destruct (peq id1 a#1); destruct (peq id2 a#1).
-  congruence.
-  intros. inversion H0. exploit genv_symb_range; eauto. unfold block; omega.
-  intros. inversion H1. exploit genv_symb_range; eauto. unfold block; omega.
-  auto. 
-
-  assert (forall vl ge, P ge -> P (add_variables ge vl)).
-  induction vl; intros; simpl. auto. 
-  apply IHvl. red. unfold find_symbol; simpl. 
-  repeat rewrite PTree.gsspec. 
-  fold ident. destruct (peq id1 a#1#1); destruct (peq id2 a#1#1).
-  congruence.
-  intros. inversion H1. exploit genv_symb_range; eauto. unfold block; omega.
-  intros. inversion H2. exploit genv_symb_range; eauto. unfold block; omega.
-  auto.
-
-  change (P (globalenv p)). unfold globalenv. apply H0. apply H. 
-  red; unfold find_symbol; simpl; intros. rewrite PTree.gempty in H1. congruence.
+  forall ge id1 id2 b1 b2,
+  id1 <> id2 ->
+  find_symbol ge id1 = Some b1 ->
+  find_symbol ge id2 = Some b2 ->
+  b1 <> b2.
+Proof.
+  intros. red; intros; subst. elim H. destruct ge. eauto. 
 Qed.
 
 (** * Construction of the initial memory state *)
diff --git a/driver/Complements.v b/driver/Complements.v
index b76a99f..a67d61e 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -64,7 +64,9 @@ Proof.
   congruence.
   assert (ef0 = ef) by congruence. subst ef0.
   assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0.
-  exploit external_call_determ. eexact H4. eexact H9. auto. 
+  exploit external_call_determ. 
+  instantiate (1 := Genv.find_symbol ge). exact (Genv.genv_vars_inj ge). 
+  eexact H4. eexact H9. auto. 
   intros [A [B C]]. subst. 
   intuition congruence.
 Qed.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index fe6cf86..f4a8a1f 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -881,7 +881,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       extcall_arguments rs m ef.(ef_sig) args ->
       rs' = (rs#(loc_external_result ef.(ef_sig)) <- res
                #PC <- (rs LR)) ->
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 5be4734..6a48451 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -1335,7 +1335,7 @@ Lemma exec_function_external_prop:
          (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
          (ef : external_function) (args : list val) (res : val) (m': mem),
   Genv.find_funct_ptr ge fb = Some (External ef) ->
-  external_call ef args m t0 res m' ->
+  external_call ef (Genv.find_symbol ge) args m t0 res m' ->
   Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
   ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
   exec_instr_prop (Machconcr.Callstate s fb ms m)
@@ -1347,6 +1347,7 @@ Proof.
   left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR))
                 m'); split.
   apply plus_one. eapply exec_step_external; eauto. 
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   eapply extcall_arguments_match; eauto. 
   econstructor; eauto.
   unfold loc_external_result. auto with ppcgen.