More faithful semantics for volatile reads and writes.

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

1 files changed, 363 insertions, 247 deletions

diff --git a/common/Events.v b/common/Events.v
index a666b40..329f31c 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -22,6 +22,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 Require Import Memory.
+Require Import Globalenvs.
 
 (** * Events and traces *)
 
@@ -47,15 +48,12 @@ Require Import Memory.
   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
-  | EVptr_global: ident -> int -> eventval
-  | EVptr_local: eventval.
+  | EVptr_global: ident -> int -> eventval.
 
 Inductive event: Type :=
   | Event_syscall: ident -> list eventval -> eventval -> event
@@ -248,105 +246,155 @@ Qed.
 
 (** * Relating values and event values *)
 
+Set Implicit Arguments.
+
 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).
+(** Global environment used to translate between global variable names and their block identifiers. *)
+Variables F V: Type.
+Variable ge: Genv.t F V.
+
+(** Translation between values and event values. *)
+
+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)
+  | ev_match_ptr: forall id b ofs,
+      Genv.find_symbol ge id = Some b ->
+      eventval_match (EVptr_global id ofs) Tint (Vptr b ofs).
+
+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).
 
 (** Some properties of these translation predicates. *)
 
-Lemma val_of_eventval_type:
+Lemma eventval_match_type:
   forall ev ty v,
-  val_of_eventval ev ty v -> Val.has_type v ty.
+  eventval_match 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.
+Lemma 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.
+
+Lemma 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; auto.
 Qed.
 
+Lemma 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.
+
+(** Compatibility with memory injections *)
+
 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).
+     (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0))
+  /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0))
+  /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> 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.
+Hypothesis glob_pres: meminj_preserves_globals.
+
+Lemma eventval_match_inject:
+  forall ev ty v1 v2,
+  eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2.
 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.
+  intros. inv H; inv H0. constructor. constructor.
+  destruct glob_pres as [A [B C]].
+  exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ.
+  rewrite Int.add_zero. econstructor; eauto. 
 Qed.
 
-Lemma val_of_eventval_inject:
+Lemma eventval_match_inject_2:
   forall ev ty v,
-  meminj_preserves_globals ->
-  val_of_eventval ev ty v -> val_inject f v v.
+  eventval_match 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.
+  induction 1. constructor. constructor.
+  destruct glob_pres as [A [B C]].
+  exploit A; eauto. intro EQ.
+  econstructor; 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.
+Lemma eventval_list_match_inject:
+  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
+  forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match evl tyl vl2.
 Proof.
-  intros. inv H0; inv H1; auto.
-  exploit (H id id0); eauto. congruence.
-  elim (H5 _ H2).
-  elim (H2 _ H5).
+  induction 1; intros. inv H; constructor.
+  inv H1. constructor. eapply eventval_match_inject; eauto. eauto.
 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.
+(** Determinism *)
+
+Lemma 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. congruence.
 Qed.
 
+Lemma 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.
+  decEq. eapply Genv.genv_vars_inj; eauto. 
+Qed.
+
+Lemma 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.
+
 End EVENTVAL.
 
+(** Invariance under changes to the global environment *)
+
+Section EVENTVAL_INV.
+
+Variables F1 V1 F2 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
+
+Hypothesis symbols_preserved:
+  forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id.
+
+Lemma eventval_match_preserved:
+  forall ev ty v,
+  eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v.
+Proof.
+  induction 1; constructor. rewrite symbols_preserved; auto. 
+Qed.
+
+Lemma eventval_list_match_preserved:
+  forall evl tyl vl,
+  eventval_list_match ge1 evl tyl vl -> eventval_list_match ge2 evl tyl vl.
+Proof.
+  induction 1; constructor; auto. eapply eventval_match_preserved; eauto.
+Qed.
+
+End EVENTVAL_INV.
+
 (** * Semantics of external functions *)
 
 (** Each external function is of one of the following kinds: *)
@@ -357,19 +405,14 @@ Inductive extfun_kind: signature -> Type :=
          result that is an integer or a float, does not modify
          the memory, and produces an [Event_syscall] event in the trace. *)
   | 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.  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. *)
+     (** A volatile read operation.  If the adress given as first argument
+         points within a volatile global variable, generate an [Event_vload]
+         event and return the value found in this event.  Otherwise,
+         produce no event and behave like a regular memory load. *)
   | 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. *)
+     (** A volatile store operation.   If the adress given as first argument
+         points within a volatile global variable, generate an [Event_vstore]
+         event.  Otherwise, produce no event and behave like a regular memory store. *)
   | 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.
@@ -384,7 +427,7 @@ 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 global environment
 - the values of the arguments passed to this function
 - the memory state before the call
 - the result value of the call
@@ -393,7 +436,7 @@ Parameter classify_external_function:
 *)
 
 Definition extcall_sem : Type :=
-  (ident -> option block) -> list val -> mem -> trace -> val -> mem -> Prop.
+  forall (F V: Type), Genv.t F V -> list val -> mem -> trace -> val -> mem -> Prop.
 
 (** We now specify the expected properties of this predicate. *)
 
@@ -433,43 +476,57 @@ Fixpoint matching_traces (t1 t2: trace) {struct t1} : Prop :=
       True
   end.
 
+Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool :=
+  match Genv.find_var_info ge b with
+  | None => false
+  | Some gv => gv.(gvar_volatile)
+  end.
+
 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 symb vargs m1 t vres m2,
-    sem symb vargs m1 t vres m2 ->
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2,
+    sem F V ge 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 symb vargs m1 t vres m2,
-    sem symb vargs m1 t vres m2 ->
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2,
+    sem F V ge vargs m1 t vres m2 ->
     List.length vargs = List.length sg.(sig_args);
 
+(** The semantics is invariant under change of global environment that preserves symbols. *)
+  ec_symbols_preserved:
+    forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) vargs m1 t vres m2,
+    (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
+    (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) ->
+    sem F1 V1 ge1 vargs m1 t vres m2 ->
+    sem F2 V2 ge2 vargs m1 t vres m2;
+
 (** External calls cannot invalidate memory blocks.  (Remember that
   freeing a block does not invalidate its block identifier.) *)
   ec_valid_block:
-    forall symb vargs m1 t vres m2 b,
-    sem symb vargs m1 t vres m2 ->
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2 b,
+    sem F V ge 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 symb vargs m1 t vres m2 b,
-    sem symb vargs m1 t vres m2 ->
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2 b,
+    sem F V ge 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 symb vargs m1 t vres m2 m1' vargs',
-    sem symb vargs m1 t vres m2 ->
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2 m1' vargs',
+    sem F V ge vargs m1 t vres m2 ->
     Mem.extends m1 m1' ->
     Val.lessdef_list vargs vargs' ->
     exists vres', exists m2',
-       sem symb vargs' m1' t vres' m2'
+       sem F V ge vargs' m1' t vres' m2'
     /\ Val.lessdef vres vres'
     /\ Mem.extends m2 m2'
     /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2';
@@ -477,13 +534,13 @@ Record extcall_properties (sem: extcall_sem)
 (** External calls must commute with memory injections,
   in the following sense. *)
   ec_mem_inject:
-    forall symb vargs m1 t vres m2 f m1' vargs',
-    meminj_preserves_globals symb f ->
-    sem symb vargs m1 t vres m2 ->
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs',
+    meminj_preserves_globals ge f ->
+    sem F V ge vargs m1 t vres m2 ->
     Mem.inject f m1 m1' ->
     val_list_inject f vargs vargs' ->
     exists f', exists vres', exists m2',
-       sem symb vargs' m1' t vres' m2'
+       sem F V ge vargs' m1' t vres' m2'
     /\ val_inject f' vres vres'
     /\ Mem.inject f' m2 m2'
     /\ mem_unchanged_on (loc_unmapped f) m1 m2
@@ -495,24 +552,43 @@ Record extcall_properties (sem: extcall_sem)
   if the observable traces match, the return states must be
   identical. *)
   ec_determ:
-    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 ->
+    forall F V ge vargs m t1 vres1 m1 t2 vres2 m2,
+    sem F V ge vargs m t1 vres1 m1 -> sem F V ge vargs m t2 vres2 m2 ->
     matching_traces t1 t2 -> t1 = t2 /\ vres1 = vres2 /\ m1 = m2
 }.
 
 (** ** Semantics of volatile loads *)
 
-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'.
+Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | volatile_load_sem_vol: forall b ofs m id ev v,
+      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true ->
+      eventval_match ge ev (type_of_chunk chunk) v ->
+      volatile_load_sem chunk ge
+          (Vptr b ofs :: nil) m
+          (Event_vload chunk id ofs ev :: nil)
+          (Val.load_result chunk v) m
+  | volatile_load_sem_nonvol: forall b ofs m v,
+      block_is_volatile ge b = false ->
+      Mem.load chunk m b (Int.signed ofs) = Some v ->
+      volatile_load_sem chunk ge
+          (Vptr b ofs :: nil) m
+          E0
+          v m.
+
+Remark meminj_preserves_block_is_volatile:
+  forall F V (ge: Genv.t F V) f b1 b2 delta,
+  meminj_preserves_globals ge f ->
+  f b1 = Some (b2, delta) ->
+  block_is_volatile ge b2 = block_is_volatile ge b1.
+Proof.
+  intros. destruct H as [A [B C]]. unfold block_is_volatile. 
+  case_eq (Genv.find_var_info ge b1); intros.
+  exploit B; eauto. intro EQ; rewrite H0 in EQ; inv EQ. rewrite H; auto.
+  case_eq (Genv.find_var_info ge b2); intros.
+  exploit C; eauto. intro EQ. congruence.
+  auto.
+Qed.
 
 Lemma volatile_load_ok:
   forall chunk,
@@ -521,81 +597,77 @@ Lemma volatile_load_ok:
 Proof.
   intros; constructor; intros.
 
-  inv H. unfold proj_sig_res. simpl. eapply Mem.load_type; eauto. 
+  unfold proj_sig_res; simpl. destruct H.
+  destruct chunk; destruct v; simpl; constructor.
+  eapply Mem.load_type; eauto. 
 
-  inv H. simpl. auto.
+  destruct H; simpl; auto.
 
-  inv H. eauto with mem. 
+  destruct H1. 
+  econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto. 
+  econstructor; eauto.
 
-  inv H. eapply Mem.bounds_store; eauto. 
+  destruct H; 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.
+  destruct H; auto.
 
-  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.
+  destruct H. 
+  inv H1. inv H8. inv H6. 
+  exists (Val.load_result chunk v); exists m1'; intuition.
+  constructor; auto.
+  red; auto.
+  inv H1. inv H7. inv H5. 
+  exploit Mem.load_extends; eauto. intros [v' [A B]]. 
+  exists v'; exists m1'; intuition.
   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; auto.
+
+  destruct H0.
+  inv H2. inv H9. inv H7.
+  generalize H; intros [P [Q R]].
+  exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ.
+  exists f; exists (Val.load_result chunk v); exists m1'; intuition.
+  rewrite Int.add_zero. constructor; auto.
+  apply val_load_result_inject. eapply eventval_match_inject_2; eauto.
+  red; auto.
+  red; auto.
+  red; intros. congruence.
+  inv H2. inv H8.
+  exploit Mem.loadv_inject; eauto. simpl. eauto. intros [v1 [A B]].
+  inv H6; simpl in *.
+  exists f; exists v1; exists m1'; intuition.
+  econstructor; eauto.
+  rewrite <- H0. eapply meminj_preserves_block_is_volatile; eauto.
+  red; auto.
+  red; auto.
   red; intros. 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. 
+  inv H; inv H0; try congruence.
+  assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0.
+  assert (ev = ev0) by (red in H1; tauto). subst ev0.
+  assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0.
+  auto.
   intuition congruence.
 Qed.
 
 (** ** Semantics of volatile stores *)
 
-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 ->
+Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | volatile_store_sem_vol: forall b ofs m id ev v,
+      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true ->
+      eventval_match ge ev (type_of_chunk chunk) v ->
+      volatile_store_sem chunk ge
+          (Vptr b ofs :: v :: nil) m
+          (Event_vstore chunk id ofs ev :: nil)
+          Vundef m
+  | volatile_store_sem_nonvol: forall b ofs m v m',
+      block_is_volatile ge b = false ->
       Mem.store chunk m b (Int.signed ofs) v = Some m' ->
-      volatile_store_sem chunk symb
-        (Vptr b ofs :: v :: nil) m
-        (Event_vstore chunk id ofs ev :: nil)
-         Vundef m'.
+      volatile_store_sem chunk ge
+          (Vptr b ofs :: v :: nil) m
+          E0
+          Vundef m'.
 
 Lemma volatile_store_ok:
   forall chunk,
@@ -604,71 +676,93 @@ Lemma volatile_store_ok:
 Proof.
   intros; constructor; intros.
 
-  inv H. unfold proj_sig_res. simpl. auto.
+  unfold proj_sig_res; simpl. inv H; constructor.
+
+  inv H; simpl; auto.
 
-  inv H. simpl. auto.
+  inv H1. 
+  constructor. rewrite H; auto. rewrite H0; auto. eapply eventval_match_preserved; eauto.
+  constructor; auto. rewrite H0; auto.
 
-  inv H. eauto with mem. 
+  inv H. auto. eauto with mem.
 
-  inv H. eapply Mem.bounds_store; eauto. 
+  inv H. auto. eapply Mem.bounds_store; eauto.
 
-  inv H. inv H1. inv H6. inv H8. inv H7. 
+  inv H.
+  inv H1. inv H6. inv H8. inv H7.
+  exists Vundef; exists m1'; intuition.
+  constructor; auto. eapply eventval_match_lessdef; eauto.
+  red; auto.
+  inv H1. inv H5. inv H7. inv H6.
   exploit Mem.store_within_extends; eauto. intros [m' [A B]].
   exists Vundef; exists m'; intuition.
-  constructor; auto. eapply eventval_of_val_lessdef; eauto. 
+  constructor; 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.
+  eapply Mem.store_valid_access_3. eexact H3.
   intros [C D].
   generalize (size_chunk_pos chunk0). intro E.
-  generalize (size_chunk_pos chunk). intro F.
+  generalize (size_chunk_pos chunk). intro G.
   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.
+  red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
 
-  inv H0. inv H2. inv H7. inv H9. inv H10.
-  exploit Mem.store_mapped_inject; eauto. intros [m2' [A B]].
+  inv H0.
+  inv H2. inv H7. inv H9. inv H10.
+  generalize H; intros [P [Q R]].
+  exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ.
+  exists f; exists Vundef; exists m1'; intuition.
+  rewrite Int.add_zero. constructor; auto. 
+  eapply eventval_match_inject; eauto. 
+  red; auto.
+  red; auto.
+  red; intros; congruence.
+  inv H2. inv H8. inv H9. inv H6.
+  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. 
   exists f; exists Vundef; exists m2'; intuition.
-  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.
+  constructor; auto. rewrite <- H3. eapply meminj_preserves_block_is_volatile; eauto.  
   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. 
+  rewrite <- H4. eapply Mem.load_store_other; eauto. 
+  left. exploit (H2 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.
+  rewrite <- H4. 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 H5.
+  eapply Mem.store_valid_access_3. eexact H0.
   intros [C D].
   generalize (size_chunk_pos chunk0). intro E.
-  generalize (size_chunk_pos chunk). intro F.
+  generalize (size_chunk_pos chunk). intro G.
   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.
+  red; intros. exploit (H2 x H8). eauto. unfold Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
+  red; intros; congruence.
 
-  red; intros. congruence.
-
-  inv H0; inv H1.
-  assert (id = id0) by (eapply H; eauto).
-  exploit eventval_of_val_determ. eauto. eexact H4. eexact H14. intros.
+  inv H; inv H0; try congruence.
+  assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0.
+  assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0.
+  auto.
   intuition congruence.
 Qed.
 
 (** ** Semantics of dynamic memory allocation (malloc) *)
 
-Inductive extcall_malloc_sem: extcall_sem :=
-  | extcall_malloc_sem_intro: forall symb n m m' b m'',
+Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | extcall_malloc_sem_intro: forall 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 symb (Vint n :: nil) m E0 (Vptr b Int.zero) m''.
+      extcall_malloc_sem ge (Vint n :: nil) m E0 (Vptr b Int.zero) m''.
 
 Lemma extcall_malloc_ok:
   extcall_properties extcall_malloc_sem 
@@ -692,6 +786,8 @@ Proof.
 
   inv H. auto.
 
+  inv H1; econstructor; eauto.
+
   inv H. eauto with mem.
 
   inv H. transitivity (Mem.bounds m' b).
@@ -714,7 +810,7 @@ Proof.
   intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
   exploit Mem.store_mapped_inject. eexact A. eauto. eauto. 
   instantiate (1 := Vint n). auto. 
-  intros [m2' [E F]].
+  intros [m2' [E G]].
   exists f'; exists (Vptr b' Int.zero); exists m2'; intuition.
   econstructor; eauto.
   econstructor. eauto. auto.
@@ -724,17 +820,18 @@ Proof.
   subst b1. rewrite C in H2. inv H2. eauto with mem. 
   rewrite D in H2. congruence. auto. 
 
-  inv H0; inv H1. intuition congruence. 
+  inv H; inv H0. intuition congruence. 
 Qed.
 
 (** ** Semantics of dynamic memory deallocation (free) *)
 
-Inductive extcall_free_sem: extcall_sem :=
-  | extcall_free_sem_intro: forall symb b lo sz m m',
+Inductive extcall_free_sem  (F V: Type) (ge: Genv.t F V):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | extcall_free_sem_intro: forall 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 symb (Vptr b lo :: nil) m E0 Vundef m'.
+      extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'.
 
 Lemma extcall_free_ok:
   extcall_properties extcall_free_sem 
@@ -761,6 +858,8 @@ Proof.
 
   inv H. auto.
 
+  inv H1; econstructor; eauto.
+
   inv H. eauto with mem.
 
   inv H. eapply Mem.bounds_free; eauto.
@@ -820,17 +919,17 @@ Proof.
 
   red; intros. congruence.
 
-  inv H0; inv H1. intuition congruence.
+  inv H; inv H0. intuition congruence.
 Qed.
 
 (** ** Semantics of system calls. *)
 
-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.
+Inductive extcall_io_sem (name: ident) (sg: signature) (F V: Type) (ge: Genv.t F V):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | extcall_io_sem_intro: forall vargs m args res vres,
+      eventval_list_match ge args (sig_args sg) vargs ->
+      eventval_match ge res (proj_sig_res sg) vres ->
+      extcall_io_sem name sg ge vargs m (Event_syscall name args res :: E0) vres m.
 
 Lemma extcall_io_ok:
   forall name sg,
@@ -838,9 +937,13 @@ Lemma extcall_io_ok:
 Proof.
   intros; constructor; intros.
 
-  inv H. eapply val_of_eventval_type; eauto.
+  inv H. eapply eventval_match_type; eauto.
 
-  inv H. auto.
+  inv H. eapply eventval_list_match_length; eauto.
+
+  inv H1. econstructor; eauto. 
+  eapply eventval_list_match_preserved; eauto.
+  eapply eventval_match_preserved; eauto. 
 
   inv H; auto.
 
@@ -849,33 +952,22 @@ Proof.
   inv H.
   exists vres; exists m1'; intuition.
   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. 
+  eapply eventval_list_match_lessdef; eauto.
   red; auto.
 
   inv H0.
   exists f; exists vres; exists m1'; intuition.
   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.
+  eapply eventval_list_match_inject; eauto.
+  eapply eventval_match_inject_2; eauto.
   red; auto.
   red; auto.
   red; intros; congruence.
 
-  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. 
+  inv H; inv H0. simpl in H1.
+  assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0.
+  assert (res = res0). tauto. subst res0.
+  intuition. eapply eventval_match_determ_1; eauto.
 Qed.
 
 (** ** Combined semantics of external calls *)
@@ -912,22 +1004,46 @@ Proof.
   apply extcall_free_ok.
 Qed.
 
-Definition external_call_well_typed ef := ec_well_typed _ _ (external_call_spec ef).
-Definition external_call_arity ef := ec_arity _ _ (external_call_spec ef).
-Definition external_call_valid_block ef := ec_valid_block _ _ (external_call_spec ef).
-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).
+Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).
+Definition external_call_arity ef := ec_arity (external_call_spec ef).
+Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef).
+Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef).
+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. *)
+(** Special cases of [external_call_symbols_preserved_gen]. *)
 
 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.
+  forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
+  external_call ef ge1 vargs m1 t vres m2 ->
+  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
+  (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
+  external_call ef ge2 vargs m1 t vres m2.
+Proof.
+  intros. eapply external_call_symbols_preserved_gen; eauto.
+  intros. unfold block_is_volatile. rewrite H1. auto.
+Qed.
+
+Require Import Errors.
+
+Lemma external_call_symbols_preserved_2:
+  forall ef F1 V1 F2 V2 (tvar: V1 -> res V2)
+         (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2,
+  external_call ef ge1 vargs m1 t vres m2 ->
+  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
+  (forall b gv1, Genv.find_var_info ge1 b = Some gv1 ->
+     exists gv2, Genv.find_var_info ge2 b = Some gv2 /\ transf_globvar tvar gv1 = OK gv2) ->
+  (forall b gv2, Genv.find_var_info ge2 b = Some gv2 ->
+     exists gv1, Genv.find_var_info ge1 b = Some gv1 /\ transf_globvar tvar gv1 = OK gv2) ->
+  external_call ef ge2 vargs m1 t vres m2.
 Proof.
-  intros. replace symb2 with symb1; auto. 
-  symmetry. apply extensionality. auto.
+  intros. eapply external_call_symbols_preserved_gen; eauto.
+  intros. unfold block_is_volatile.
+  case_eq (Genv.find_var_info ge1 b); intros.
+  exploit H1; eauto. intros [g2 [A B]]. rewrite A. monadInv B. destruct g; auto.
+  case_eq (Genv.find_var_info ge2 b); intros.
+  exploit H2; eauto. intros [g1 [A B]]. congruence.
+  auto.
 Qed.