- 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

3 files changed, 384 insertions, 261 deletions

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