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

4 files changed, 522 insertions, 358 deletions

diff --git a/common/AST.v b/common/AST.v
index 2d20276..861795c 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -93,11 +93,19 @@ Inductive init_data: Type :=
   | Init_space: Z -> init_data
   | Init_addrof: ident -> int -> init_data.  (**r address of symbol + offset *)
 
+(** Information attached to global variables. *)
+
+Record globvar (V: Type) : Type := mkglobvar {
+  gvar_info: V;                    (**r language-dependent info, e.g. a type *)
+  gvar_init: list init_data;       (**r initialization data *)
+  gvar_readonly: bool;             (**r read-only variable? (const) *)
+  gvar_volatile: bool              (**r volatile variable? *)
+}.
+
 (** Whole programs consist of:
 - a collection of function definitions (name and description);
 - the name of the ``main'' function that serves as entry point in the program;
-- a collection of global variable declarations, consisting of
-  a name, initialization data, and additional information.
+- a collection of global variable declarations (name and information).
 
 The type of function descriptions and that of additional information
 for variables vary among the various intermediate languages and are
@@ -107,14 +115,14 @@ programs are common to all languages. *)
 Record program (F V: Type) : Type := mkprogram {
   prog_funct: list (ident * F);
   prog_main: ident;
-  prog_vars: list (ident * list init_data * V)
+  prog_vars: list (ident * globvar V)
 }.
 
 Definition prog_funct_names (F V: Type) (p: program F V) : list ident :=
   map (@fst ident F) p.(prog_funct).
 
 Definition prog_var_names (F V: Type) (p: program F V) : list ident :=
-  map (fun x: ident * list init_data * V => fst(fst x)) p.(prog_vars).
+  map (@fst ident (globvar V)) p.(prog_vars).
 
 (** * Generic transformations over programs *)
 
@@ -230,11 +238,11 @@ Section TRANSF_PARTIAL_PROGRAM.
 Variable A B V: Type.
 Variable transf_partial: A -> res B.
 
-Definition prefix_funct_name (id: ident) : errmsg :=
+Definition prefix_name (id: ident) : errmsg :=
   MSG "In function " :: CTX id :: MSG ": " :: nil.
 
 Definition transform_partial_program (p: program A V) : res (program B V) :=
-  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
+  do fl <- map_partial prefix_name transf_partial p.(prog_funct);
   OK (mkprogram fl p.(prog_main) p.(prog_vars)).
 
 Lemma transform_partial_program_function:
@@ -275,12 +283,13 @@ Variable A B V W: Type.
 Variable transf_partial_function: A -> res B.
 Variable transf_partial_variable: V -> res W.
 
-Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
-  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
+Definition transf_globvar (g: globvar V) : res (globvar W) :=
+  do info' <- transf_partial_variable g.(gvar_info);
+  OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
 
 Definition transform_partial_program2 (p: program A V) : res (program B W) :=
-  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
-  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
+  do fl <- map_partial prefix_name transf_partial_function p.(prog_funct);
+  do vl <- map_partial prefix_name transf_globvar p.(prog_vars);
   OK (mkprogram fl p.(prog_main) vl).
 
 Lemma transform_partial_program2_function:
@@ -294,14 +303,16 @@ Proof.
 Qed.
 
 Lemma transform_partial_program2_variable:
-  forall p tp i tv,
+  forall p tp i tg,
   transform_partial_program2 p = OK tp ->
-  In (i, tv) tp.(prog_vars) ->
-  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
+  In (i, tg) tp.(prog_vars) ->
+  exists v,
+     In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars)
+  /\ transf_partial_variable v = OK tg.(gvar_info).
 Proof.
-  intros. monadInv H. 
-  eapply In_map_partial; eauto. 
-Qed.
+  intros. monadInv H. exploit In_map_partial; eauto. intros [g [P Q]].
+  monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto.
+ Qed.
 
 Lemma transform_partial_program2_main:
   forall p tp,
@@ -326,15 +337,16 @@ Variable A B V W: Type.
 Variable match_fundef: A -> B -> Prop.
 Variable match_varinfo: V -> W -> Prop.
 
-Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
-  match x1, x2 with
-  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
-  end.
+Inductive match_funct_entry: ident * A -> ident * B -> Prop :=
+  | match_funct_entry_intro: forall id fn1 fn2,
+      match_fundef fn1 fn2 ->
+      match_funct_entry (id, fn1) (id, fn2).
 
-Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
-  match x1, x2 with
-  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
-  end.
+Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop :=
+  | match_var_entry_intro: forall id info1 info2 init ro vo,
+      match_varinfo info1 info2 ->
+      match_var_entry (id, mkglobvar info1 init ro vo)
+                      (id, mkglobvar info2 init ro vo).
 
 Definition match_program (p1: program A V) (p2: program B W) : Prop :=
   list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
@@ -359,13 +371,14 @@ Proof.
     (fun (ab: ident * A) (ac: ident * B) =>
        fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
   eapply map_partial_forall2. eauto. 
-  intros. destruct v1; destruct v2; simpl in *. auto.
+  intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. constructor. auto.
   split. auto.
   apply list_forall2_imply with
-    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
-       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
+    (fun (ab: ident * globvar V) (ac: ident * globvar W) =>
+       fst ab = fst ac /\ transf_globvar transf_partial_variable (snd ab) = OK (snd ac)).
   eapply map_partial_forall2. eauto. 
-  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
+  intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. 
+  monadInv H2. destruct g; simpl in *. constructor. auto.
 Qed.
 
 (** * External functions *)
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.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 65ae06c..b540ad1 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -64,7 +64,7 @@ Variable V: Type.  (**r The type of information attached to variables *)
 Record t: Type := mkgenv {
   genv_symb: PTree.t block;             (**r mapping symbol -> block *)
   genv_funs: ZMap.t (option F);         (**r mapping function pointer -> definition *)
-  genv_vars: ZMap.t (option V);         (**r mapping variable pointer -> info *)
+  genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *)
   genv_nextfun: block;                  (**r next function pointer *)
   genv_nextvar: block;                  (**r next variable pointer *)
   genv_nextfun_neg: genv_nextfun < 0;
@@ -101,7 +101,7 @@ Definition find_funct (ge: t) (v: val) : option F :=
 (** [find_var_info ge b] returns the information attached to the variable
    at address [b]. *)
 
-Definition find_var_info (ge: t) (b: block) : option V :=
+Definition find_var_info (ge: t) (b: block) : option (globvar V) :=
   ZMap.get b ge.(genv_vars).
 
 (** ** Constructing the global environment *)
@@ -143,9 +143,9 @@ Next Obligation.
   eauto.
 Qed.
 
-Program Definition add_variable (ge: t) (idv: ident * list init_data * V) : t :=
+Program Definition add_variable (ge: t) (idv: ident * globvar V) : t :=
   @mkgenv
-    (PTree.set idv#1#1 ge.(genv_nextvar) ge.(genv_symb))
+    (PTree.set idv#1 ge.(genv_nextvar) ge.(genv_symb))
     ge.(genv_funs)
     (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars))
     ge.(genv_nextfun)
@@ -204,7 +204,7 @@ Qed.
 Definition add_functions (ge: t) (fl: list (ident * F)) : t :=
   List.fold_left add_function fl ge.
 
-Definition add_variables (ge: t) (vl: list (ident * list init_data * V)) : t :=
+Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t :=
   List.fold_left add_variable vl ge.
 
 Definition globalenv (p: program F V) :=
@@ -230,19 +230,19 @@ Proof.
 Qed.
 
 Theorem find_symbol_exists:
-  forall p id init v,
-  In (id, init, v) (prog_vars p) ->
+  forall p id gv,
+  In (id, gv) (prog_vars p) ->
   exists b, find_symbol (globalenv p) id = Some b.
 Proof.
-  intros until v.
+  intros until gv.
   assert (forall vl ge,
           (exists b, find_symbol ge id = Some b) ->
           exists b, find_symbol (add_variables ge vl) id = Some b).
   unfold find_symbol; induction vl; simpl; intros. auto. apply IHvl.
-  simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1#1).
+  simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1).
   exists (genv_nextvar ge); auto. auto.
 
-  assert (forall vl ge, In (id, init, v) vl ->
+  assert (forall vl ge, In (id, gv) vl ->
           exists b, find_symbol (add_variables ge vl) id = Some b).
   unfold find_symbol; induction vl; simpl; intros. contradiction.
   destruct H0. apply H. subst; unfold find_symbol; simpl.
@@ -274,7 +274,7 @@ Qed.
 
 Remark add_variables_same_symb:
   forall id vl ge, 
-  ~In id (map (fun idv => idv#1#1) vl) ->
+  ~In id (map (@fst ident (globvar V)) vl) ->
   find_symbol (add_variables ge vl) id = find_symbol ge id.
 Proof.
   induction vl; simpl; intros. auto. 
@@ -415,7 +415,7 @@ Remark add_variables_symb_neg:
 Proof.
   induction vl; simpl; intros. auto.
   exploit IHvl; eauto. unfold find_symbol; simpl. rewrite PTree.gsspec. 
-  fold ident. destruct (peq id (a#1#1)); auto. intros. inv H1. 
+  fold ident. destruct (peq id (a#1)); auto. intros. inv H1. 
   generalize (genv_nextvar_pos ge). intros. omegaContradiction.
 Qed.
 
@@ -522,11 +522,12 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
   | i :: il' => init_data_size i + init_data_list_size il'
   end.
 
-Definition alloc_variable (m: mem) (idv: ident * list init_data * V) : option mem :=
-  let (m', b) := Mem.alloc m 0 (init_data_list_size idv#1#2) in
-  store_init_data_list m' b 0 idv#1#2.
+Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem :=
+  let init := idv#2.(gvar_init) in
+  let (m', b) := Mem.alloc m 0 (init_data_list_size init) in
+  store_init_data_list m' b 0 init.
 
-Fixpoint alloc_variables (m: mem) (vl: list (ident * list init_data * V))
+Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V))
                          {struct vl} : option mem :=
   match vl with
   | nil => Some m
@@ -560,8 +561,9 @@ Proof.
   simpl; intros. inv H; unfold block; omega.
   simpl length; rewrite inj_S; simpl. intros m m'. 
   unfold alloc_variable. 
-  caseEq (Mem.alloc m 0 (init_data_list_size (a#1)#2)). intros m1 b ALLOC.
-  caseEq (store_init_data_list m1 b 0 a#1#2); try congruence. intros m2 STORE REC.
+  set (init := gvar_init a#2).
+  caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
+  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC.
   rewrite (IHvl _ _ REC). 
   rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
   rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
@@ -590,8 +592,9 @@ Proof.
   induction vl.
   simpl; intros. congruence.
   intros until m'. simpl. unfold alloc_variable. 
-  caseEq (Mem.alloc m 0 (init_data_list_size (a#1)#2)). intros m1 b ALLOC.
-  caseEq (store_init_data_list m1 b 0 a#1#2); try congruence. intros m2 STORE REC PERM.
+  set (init := gvar_init a#2).
+  caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
+  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC PERM.
   eapply IHvl; eauto. 
   eapply store_init_data_list_perm; eauto. 
   eauto with mem.
@@ -616,24 +619,6 @@ Proof.
   eapply Mem.load_store_other; eauto; intuition.
 Qed.
 
-(*
-Remark alloc_variables_nextblock:
-  forall vl g m m',
-  alloc_variables m vl = Some m' ->
-  Mem.nextblock m = genv_nextvar g ->
-  Mem.nextblock m' = genv_nextvar (add_variables g vl).
-Proof.
-  induction vl; simpl; intros until m'.
-  intros. congruence.
-  unfold alloc_variable. 
-  caseEq (Mem.alloc m 0 (init_data_list_size (a#1)#2)). intros m1 b ALLOC.
-  caseEq (store_init_data_list m1 b 0 a#1#2); try congruence. intros m2 STORE REC EQ.
-  eapply IHvl; eauto. 
-  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
-  rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
-  simpl. unfold block in *; omega.
-Qed.
-*)
 Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop :=
   match il with
   | nil => True
@@ -697,8 +682,9 @@ Proof.
   induction vl; simpl; intros until m'.
   congruence.
   unfold alloc_variable. 
-  caseEq (Mem.alloc m 0 (init_data_list_size a#1#2)); intros m1 b1 ALLOC.
-  caseEq (store_init_data_list m1 b1 0 a#1#2); try congruence. intros m2 STO REC VAL.
+  set (init := gvar_init a#2).
+  caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC.
+  caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO REC VAL.
   transitivity (Mem.load chunk m2 b p). 
   apply IHvl; auto. red. rewrite (store_init_data_list_nextblock _ _ _ _ STO).
   change (Mem.valid_block m1 b). eauto with mem. 
@@ -720,23 +706,23 @@ Proof.
 Qed.
 
 Lemma alloc_variables_charact:
-  forall id init v vl g m m',
+  forall id gv vl g m m',
   genv_nextvar g = Mem.nextblock m ->
   alloc_variables m vl = Some m' ->
-  list_norepet (map (fun v => v#1#1) vl) ->
-  In (id, init, v) vl ->
+  list_norepet (map (@fst ident (globvar V)) vl) ->
+  In (id, gv) vl ->
   exists b, find_symbol (add_variables g vl) id = Some b 
-         /\ find_var_info (add_variables g vl) b = Some v
-         /\ Mem.range_perm m' b 0 (init_data_list_size init) Writable
-         /\ load_store_init_data m' b 0 init.
+         /\ find_var_info (add_variables g vl) b = Some gv
+         /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) Writable
+         /\ load_store_init_data m' b 0 gv.(gvar_init).
 Proof.
   induction vl; simpl.
   contradiction.
   intros until m'; intro NEXT.
-  unfold alloc_variable. destruct a as [[id' init'] v']. simpl.
-  caseEq (Mem.alloc m 0 (init_data_list_size init')); try congruence.
+  unfold alloc_variable. destruct a as [id' gv']. simpl.
+  caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence.
   intros m1 b ALLOC. 
-  caseEq (store_init_data_list m1 b 0 init'); try congruence.
+  caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence.
   intros m2 STORE REC NOREPET IN. inv NOREPET.
   exploit Mem.alloc_result; eauto. intro BEQ. 
   destruct IN. inv H.
@@ -778,15 +764,28 @@ Proof.
   red. rewrite H1. rewrite <- H3. intuition.
 Qed.
 
+Theorem find_var_info_not_fresh:
+  forall p b gv m,
+  init_mem p = Some m ->
+  find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b.
+Proof.
+  unfold init_mem; intros.
+  exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro.
+  exploit genv_vars_range; eauto. intros.
+  generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))).
+  rewrite add_functions_nextvar. simpl genv_nextvar. intro.
+  red. rewrite H1. rewrite <- H3. intuition.
+Qed.
+
 Theorem find_var_exists:
-  forall p id init v m,
+  forall p id gv m,
   list_norepet (prog_var_names p) ->
-  In (id, init, v) (prog_vars p) ->
+  In (id, gv) (prog_vars p) ->
   init_mem p = Some m ->
   exists b, find_symbol (globalenv p) id = Some b
-         /\ find_var_info (globalenv p) b = Some v
-         /\ Mem.range_perm m b 0 (init_data_list_size init) Writable
-         /\ load_store_init_data (globalenv p) m b 0 init.
+         /\ find_var_info (globalenv p) b = Some gv
+         /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Writable
+         /\ load_store_init_data (globalenv p) m b 0 gv.(gvar_init).
 Proof.
   intros. exploit alloc_variables_charact; eauto. 
   instantiate (1 := Mem.empty). rewrite add_functions_nextvar. rewrite Mem.nextblock_empty; auto.
@@ -839,7 +838,7 @@ Lemma alloc_variable_neutral:
   Mem.inject_neutral thr m'.
 Proof.
   intros until m'. unfold alloc_variable. 
-  caseEq (Mem.alloc m 0 (init_data_list_size (id#1)#2)); intros m1 b; intros.
+  caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b; intros.
   eapply store_init_data_list_neutral with (b := b).
   eapply Mem.alloc_inject_neutral; eauto.
   rewrite (Mem.alloc_result _ _ _ _ _ H). auto.
@@ -887,7 +886,12 @@ Section MATCH_PROGRAMS.
 
 Variables A B V W: Type.
 Variable match_fun: A -> B -> Prop.
-Variable match_var: V -> W -> Prop.
+Variable match_varinfo: V -> W -> Prop.
+
+Inductive match_globvar: globvar V -> globvar W -> Prop :=
+  | match_globvar_intro: forall info1 info2 init ro vo,
+      match_varinfo info1 info2 ->
+      match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo).
 
 Record match_genvs (ge1: t A V) (ge2: t B W): Prop := {
   mge_nextfun: genv_nextfun ge1 = genv_nextfun ge2;
@@ -901,10 +905,10 @@ Record match_genvs (ge1: t A V) (ge2: t B W): Prop := {
     exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf;
   mge_vars:
     forall b v, ZMap.get b (genv_vars ge1) = Some v ->
-    exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_var v tv;
+    exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv;
   mge_rev_vars:
     forall b tv, ZMap.get b (genv_vars ge2) = Some tv ->
-    exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_var v tv
+    exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv
 }.
 
 Lemma add_function_match:
@@ -939,10 +943,10 @@ Proof.
 Qed.
 
 Lemma add_variable_match:
-  forall ge1 ge2 id idl v1 v2,
+  forall ge1 ge2 id v1 v2,
   match_genvs ge1 ge2 ->
-  match_var v1 v2 ->
-  match_genvs (add_variable ge1 (id, idl, v1)) (add_variable ge2 (id, idl, v2)).
+  match_globvar v1 v2 ->
+  match_genvs (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)).
 Proof.
   intros. destruct H. constructor; simpl. 
   congruence. congruence. congruence.
@@ -959,19 +963,18 @@ Proof.
 Qed.
 
 Lemma add_variables_match:
-  forall vl1 vl2, list_forall2 (match_var_entry match_var) vl1 vl2 ->
+  forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
   forall ge1 ge2, match_genvs ge1 ge2 ->
   match_genvs (add_variables ge1 vl1) (add_variables ge2 vl2).
 Proof.
   induction 1; intros; simpl. 
   auto.
-  destruct a1 as [[id1 init1] f1]; destruct b1 as [[id2 init2] f2].
-  destruct H. destruct H2. subst. apply IHlist_forall2. apply add_variable_match; auto.
+  inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; auto.
 Qed.
 
 Variable p: program A V.
 Variable p': program B W.
-Hypothesis progmatch: match_program match_fun match_var p p'.
+Hypothesis progmatch: match_program match_fun match_varinfo p p'.
 
 Lemma globalenvs_match:
   match_genvs (globalenv p) (globalenv p').
@@ -1018,17 +1021,17 @@ Proof.
 Qed.
 
 Theorem find_var_info_match:
-  forall (b : block) (v : V),
+  forall (b : block) (v : globvar V),
   find_var_info (globalenv p) b = Some v ->
   exists tv,
-  find_var_info (globalenv p') b = Some tv /\ match_var v tv.
+  find_var_info (globalenv p') b = Some tv /\ match_globvar v tv.
 Proof (mge_vars globalenvs_match).
 
 Theorem find_var_info_rev_match:
-  forall (b : block) (tv : W),
+  forall (b : block) (tv : globvar W),
   find_var_info (globalenv p') b = Some tv ->
   exists v,
-  find_var_info (globalenv p) b = Some v /\ match_var v tv.
+  find_var_info (globalenv p) b = Some v /\ match_globvar v tv.
 Proof (mge_rev_vars globalenvs_match).
 
 Theorem find_symbol_match:
@@ -1052,18 +1055,17 @@ Proof.
 Qed.
 
 Lemma alloc_variables_match:
-  forall vl1 vl2, list_forall2 (match_var_entry match_var) vl1 vl2 ->
+  forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 ->
   forall m,
   alloc_variables (globalenv p') m vl2 = alloc_variables (globalenv p) m vl1.
 Proof.
   induction 1; intros; simpl.
   auto.
-  destruct a1 as [[id1 init1] v1]; destruct b1 as [[id2 init2] v2].
-  destruct H. destruct H1. subst.
+  inv H. 
   unfold alloc_variable; simpl. 
-  destruct (Mem.alloc m 0 (init_data_list_size init2)). 
+  destruct (Mem.alloc m 0 (init_data_list_size init)). 
   rewrite store_init_data_list_match. 
-  destruct (store_init_data_list (globalenv p) m0 b 0 init2); auto.
+  destruct (store_init_data_list (globalenv p) m0 b 0 init); auto.
 Qed.
 
 Theorem init_mem_match:
@@ -1135,25 +1137,27 @@ Proof.
 Qed.
 
 Theorem find_var_info_transf_partial2:
-  forall (b: block) (v: V),
+  forall (b: block) (v: globvar V),
   find_var_info (globalenv p) b = Some v ->
   exists v',
-  find_var_info (globalenv p') b = Some v' /\ transf_var v = OK v'.
+  find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
 Proof.
   intros. 
   exploit find_var_info_match. eexact prog_match. eauto. 
-  intros [tv [X Y]]. exists tv; auto.
+  intros [tv [X Y]]. exists tv; split; auto. inv Y. unfold transf_globvar; simpl.
+  rewrite H0; simpl. auto.
 Qed.
 
 Theorem find_var_info_rev_transf_partial2:
-  forall (b: block) (v': W),
+  forall (b: block) (v': globvar W),
   find_var_info (globalenv p') b = Some v' ->
   exists v,
-  find_var_info (globalenv p) b = Some v /\ transf_var v = OK v'.
+  find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'.
 Proof.
   intros. 
   exploit find_var_info_rev_match. eexact prog_match. eauto. 
-  intros [v [X Y]]. exists v; auto.
+  intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl.
+  rewrite H0; simpl. auto.
 Qed.
 
 Theorem find_symbol_transf_partial2:
@@ -1182,9 +1186,12 @@ Hypothesis transf_OK: transform_partial_program transf p = OK p'.
 Remark transf2_OK:
   transform_partial_program2 transf (fun x => OK x) p = OK p'.
 Proof.
-  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
-  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
-  rewrite map_partial_identity; auto. 
+  rewrite <- transf_OK. 
+  unfold transform_partial_program2, transform_partial_program.
+  destruct (map_partial prefix_name transf (prog_funct p)); auto.
+  simpl. replace (transf_globvar (fun (x : V) => OK x)) with (fun (v: globvar V) => OK v).
+  rewrite map_partial_identity; auto.
+  apply extensionality; intros. destruct x; auto.
 Qed.
 
 Theorem find_funct_ptr_transf_partial:
@@ -1228,6 +1235,19 @@ Proof.
   exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
 Qed.
 
+Theorem find_var_info_transf_partial:
+  forall (b: block),
+  find_var_info (globalenv p') b = find_var_info (globalenv p) b.
+Proof.
+  intros. case_eq (find_var_info (globalenv p) b); intros.
+  exploit find_var_info_transf_partial2. eexact transf2_OK. eauto. 
+  intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto. 
+  case_eq (find_var_info (globalenv p') b); intros.
+  exploit find_var_info_rev_transf_partial2. eexact transf2_OK. eauto.
+  intros [v' [P Q]]. monadInv Q. inv EQ. congruence. 
+  auto.
+Qed.
+
 Theorem init_mem_transf_partial:
   forall m, init_mem p = Some m -> init_mem p' = Some m.
 Proof.
@@ -1295,6 +1315,13 @@ Proof.
   exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
 Qed.
 
+Theorem find_var_info_transf:
+  forall (b: block),
+  find_var_info (globalenv tp) b = find_var_info (globalenv p) b.
+Proof.
+  exact (@find_var_info_transf_partial _ _ _ _ _ _ transf_OK).
+Qed.
+
 Theorem init_mem_transf:
   forall m, init_mem p = Some m -> init_mem tp = Some m.
 Proof.
diff --git a/common/Values.v b/common/Values.v
index 056cffb..236a5ae 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1029,6 +1029,14 @@ Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:=
 
 Hint Resolve val_nil_inject val_cons_inject.
 
+Lemma val_load_result_inject:
+  forall f chunk v1 v2,
+  val_inject f v1 v2 ->
+  val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
+Proof.
+  intros. inv H; destruct chunk; simpl; econstructor; eauto.
+Qed.
+
 (** Monotone evolution of a memory injection. *)
 
 Definition inject_incr (f1 f2: meminj) : Prop :=