Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


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

30 files changed, 951 insertions, 842 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 10eaa5b1..3f526aa4 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -21,7 +21,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Smallstep.
 Require Import Globalenvs.
@@ -423,14 +423,14 @@ Lemma functions_translated:
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial transf_fundef TRANSF).
+Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
+Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
 
 Lemma sig_function_translated:
   forall f tf,
@@ -482,7 +482,7 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> Prop
               (rs#res <- rv)
               (Locmap.set (assign res) rv ls)) ->
       match_stackframes
-        (RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s)
+        (RTL.Stackframe res f sp pc rs :: s)
         (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts).
 
 Inductive match_states: RTL.state -> LTL.state -> Prop :=
@@ -493,7 +493,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
       (ANL: analyze f = Some live)
       (ASG: regalloc f live (live0 f live) env = Some assign)
       (AG: agree assign (transfer f pc live!!pc) rs ls),
-      match_states (RTL.State s (RTL.fn_code f) sp pc rs m)
+      match_states (RTL.State s f sp pc rs m)
                    (LTL.State ts (transf_fun f live assign) sp pc ls m)
   | match_states_call:
       forall s f args m ts tf,
@@ -532,7 +532,7 @@ Ltac WellTypedHyp :=
 Ltac TranslInstr :=
   match goal with
   | H: (PTree.get _ _ = Some _) |- _ =>
-      simpl; rewrite PTree.gmap; rewrite H; simpl; auto
+      simpl in H; simpl; rewrite PTree.gmap; rewrite H; simpl; auto
   end.
 
 Ltac MatchStates :=
@@ -646,7 +646,7 @@ Proof.
 
   (* Icall *)
   exploit transl_find_function; eauto.  intros [tf [TFIND TF]].
-  generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
  unfold correct_alloc_instr. intros [CORR1 [CORR2 CORR3]].
+  generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
  unfold correct_alloc_instr. intros [CORR1 [CORR2 CORR3]].
   assert (rs##args = map ls (map assign args)).
     eapply agree_eval_regs; eauto. 
   econstructor; split. 
@@ -735,14 +735,13 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
-  assert (MEM: (Genv.init_mem tprog) = (Genv.init_mem prog)).
-    exact (Genv.init_mem_transf_partial _ _ TRANSF).
-  exists (LTL.Callstate nil tf nil (Genv.init_mem tprog)); split.
+  exists (LTL.Callstate nil tf nil m0); split.
   econstructor; eauto.
+  eapply Genv.init_mem_transf_partial; eauto. 
   rewrite symbols_preserved. 
   rewrite (transform_partial_program_main _ _ TRANSF).  auto.
-  rewrite <- H2. apply sig_function_translated; auto. 
-  rewrite MEM. constructor; auto. constructor.
+  rewrite <- H3. apply sig_function_translated; auto. 
+  constructor; auto. constructor.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/CSE.v b/backend/CSE.v
index 98b7bbf5..ff79be54 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -19,7 +19,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
@@ -265,7 +265,7 @@ Definition equation_holds
   | Load chunk addr vl =>
       exists a,
       eval_addressing ge sp addr (List.map valuation vl) = Some a /\
-      loadv chunk m a = Some (valuation vres)
+      Mem.loadv chunk m a = Some (valuation vres)
   end.
 
 Definition numbering_holds
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 7f942464..fcc867af 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -18,7 +18,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -404,7 +404,7 @@ Definition rhs_evals_to
   | Load chunk addr vl =>
       exists a,
       eval_addressing ge sp addr (List.map valu vl) = Some a /\
-      loadv chunk m a = Some v
+      Mem.loadv chunk m a = Some v
   end.
 
 Lemma equation_evals_to_holds_1:
@@ -510,7 +510,7 @@ Lemma add_load_satisfiable:
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
   eval_addressing ge sp addr rs##args = Some a ->
-  loadv chunk m a = Some v ->
+  Mem.loadv chunk m a = Some v ->
   numbering_satisfiable ge sp 
      (rs#dst <- v)
      m (add_load n dst chunk addr args).
@@ -668,7 +668,7 @@ Lemma find_load_correct:
   find_load n chunk addr args = Some r ->
   exists a,
   eval_addressing ge sp addr rs##args = Some a /\
-  loadv chunk m a = Some rs#r.
+  Mem.loadv chunk m a = Some rs#r.
 Proof.
   intros until r. intros WF [valu NH].
   unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND.
@@ -783,21 +783,19 @@ Qed.
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   match_stackframes_intro:
-    forall res c sp pc rs f,
-    c = f.(RTL.fn_code) ->
+    forall res sp pc rs f,
     (forall v m, numbering_satisfiable ge sp (rs#res <- v) m (analyze f)!!pc) ->
     match_stackframes
-      (Stackframe res c sp pc rs)
-      (Stackframe res (transf_code (analyze f) c) sp pc rs).
+      (Stackframe res f sp pc rs)
+      (Stackframe res (transf_function f) sp pc rs).
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
-      forall s c sp pc rs m s' f
-             (CF: c = f.(RTL.fn_code))
+      forall s sp pc rs m s' f
              (SAT: numbering_satisfiable ge sp rs m (analyze f)!!pc)
              (STACKS: list_forall2 match_stackframes s s'),
-      match_states (State s c sp pc rs m)
-                   (State s' (transf_code (analyze f) c) sp pc rs m)
+      match_states (State s f sp pc rs m)
+                   (State s' (transf_function f) sp pc rs m)
   | match_states_call:
       forall s f args m s',
       list_forall2 match_stackframes s s' ->
@@ -812,9 +810,9 @@ Inductive match_states: state -> state -> Prop :=
 Ltac TransfInstr :=
   match goal with
   | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr));
-      [ simpl
-      | unfold transf_code; rewrite PTree.gmap; 
+      cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr));
+      [ simpl transf_instr
+      | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
         unfold option_map; rewrite H1; reflexivity ]
   end.
 
@@ -829,14 +827,14 @@ Proof.
   induction 1; intros; inv MS; try (TransfInstr; intro C).
 
   (* Inop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
+  exists (State s' (transf_function f) sp pc' rs m); split.
   apply exec_Inop; auto.
   econstructor; eauto. 
   eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H; auto.
 
   (* Iop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
+  exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
   assert (eval_operation tge sp op rs##args = Some v).
     rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
   generalize C; clear C.
@@ -855,14 +853,14 @@ Proof.
   eapply add_op_satisfiable; eauto. apply wf_analyze.
 
   (* Iload *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
+  exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split.
   assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   generalize C; clear C.
   caseEq (find_load (analyze f)!!pc chunk addr args). intros r FIND CODE.
   eapply exec_Iop'; eauto. simpl. 
   assert (exists a, eval_addressing ge sp addr rs##args = Some a
-                 /\ loadv chunk m a = Some rs#r).
+                 /\ Mem.loadv chunk m a = Some rs#r).
     eapply find_load_correct; eauto.
     eapply wf_analyze; eauto.
   elim H3; intros a' [A B].
@@ -874,7 +872,7 @@ Proof.
   eapply add_load_satisfiable; eauto. apply wf_analyze.
 
   (* Istore *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
+  exists (State s' (transf_function f) sp pc' rs m'); split.
   assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Istore; eauto.
@@ -886,7 +884,7 @@ Proof.
   (* Icall *)
   exploit find_function_translated; eauto. intro FIND'.
   econstructor; split.
-  eapply exec_Icall with (f := transf_fundef f); eauto.
+  eapply exec_Icall; eauto.
   apply sig_preserved. 
   econstructor; eauto. 
   constructor; auto. 
@@ -898,7 +896,7 @@ Proof.
   (* Itailcall *)
   exploit find_function_translated; eauto. intro FIND'.
   econstructor; split.
-  eapply exec_Itailcall with (f := transf_fundef f); eauto.
+  eapply exec_Itailcall; eauto.
   apply sig_preserved. 
   econstructor; eauto. 
 
@@ -951,15 +949,14 @@ Lemma transf_initial_states:
   exists st2, initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. 
-  exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split.
+  exists (Callstate nil (transf_fundef f) nil m0); split.
   econstructor; eauto.
+  apply Genv.init_mem_transf; auto.
   change (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
   apply funct_ptr_translated; auto.
-  rewrite <- H2. apply sig_preserved. 
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
-  constructor. constructor. auto.
-  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf.
+  rewrite <- H3. apply sig_preserved. 
+  constructor. constructor.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/Cminor.v b/backend/Cminor.v
index aa9c5116..094bef73 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -22,7 +22,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Events.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Switch.
@@ -144,7 +144,7 @@ Definition funsig (fd: fundef) :=
 - [env]: local environments, map local variables to values.
 *)
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 Definition env := PTree.t val.
 
 (** The following functions build the initial local environment at
@@ -402,11 +402,12 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_skip_block: forall f k sp e m,
       step (State f Sskip (Kblock k) sp e m)
         E0 (State f Sskip k sp e m)
-  | step_skip_call: forall f k sp e m,
+  | step_skip_call: forall f k sp e m m',
       is_call_cont k ->
       f.(fn_sig).(sig_res) = None ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f Sskip k (Vptr sp Int.zero) e m)
-        E0 (Returnstate Vundef k (Mem.free m sp))
+        E0 (Returnstate Vundef k m')
 
   | step_assign: forall f id a k sp e m v,
       eval_expr sp e m a v ->
@@ -428,13 +429,14 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid sig a bl) k sp e m)
         E0 (Callstate fd vargs (Kcall optid f sp e k) m)
 
-  | step_tailcall: forall f sig a bl k sp e m vf vargs fd,
+  | step_tailcall: forall f sig a bl k sp e m vf vargs fd m',
       eval_expr (Vptr sp Int.zero) e m a vf ->
       eval_exprlist (Vptr sp Int.zero) e m bl vargs ->
       Genv.find_funct ge vf = Some fd ->
       funsig fd = sig ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
-        E0 (Callstate fd vargs (call_cont k) (Mem.free m sp))
+        E0 (Callstate fd vargs (call_cont k) m')
 
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)
@@ -469,13 +471,15 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sswitch a cases default) k sp e m)
         E0 (State f (Sexit (switch_target n default cases)) k sp e m)
 
-  | step_return_0: forall f k sp e m,
+  | step_return_0: forall f k sp e m m',
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f (Sreturn None) k (Vptr sp Int.zero) e m)
-        E0 (Returnstate Vundef (call_cont k) (Mem.free m sp))
-  | step_return_1: forall f a k sp e m v,
+        E0 (Returnstate Vundef (call_cont k) m')
+  | step_return_1: forall f a k sp e m v m',
       eval_expr (Vptr sp Int.zero) e m a v ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m)
-        E0 (Returnstate v (call_cont k) (Mem.free m sp))
+        E0 (Returnstate v (call_cont k) m')
 
   | step_label: forall f lbl s k sp e m,
       step (State f (Slabel lbl s) k sp e m)
@@ -491,10 +495,10 @@ Inductive step: state -> trace -> state -> Prop :=
       set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
-  | step_external_function: forall ef vargs k m t vres,
-      event_match ef vargs t vres ->
+  | step_external_function: forall ef vargs k m t vres m',
+      external_call ef vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
-         t (Returnstate vres k m)        
+         t (Returnstate vres k m')        
 
   | step_return: forall v optid f sp e k m,
       step (Returnstate v (Kcall optid f sp e k) m)
@@ -508,9 +512,9 @@ End RELSEM.
   without arguments and with an empty continuation. *)
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
@@ -560,12 +564,16 @@ Definition outcome_result_value
   end.
 
 Definition outcome_free_mem
-    (out: outcome) (m: mem) (sp: block) : mem :=
+    (out: outcome) (m: mem) (sp: block) (sz: Z) (m': mem) :=
   match out with
-  | Out_tailcall_return _ => m
-  | _ => Mem.free m sp
+  | Out_tailcall_return _ => m' = m
+  | _ => Mem.free m sp 0 sz = Some m'
   end.
 
+(***** REVISE - PROBLEMS WITH free *)
+
+(******************************
+
 Section NATURALSEM.
 
 Variable ge: genv.
@@ -580,16 +588,17 @@ Inductive eval_funcall:
         mem -> fundef -> list val -> trace ->
         mem -> val -> Prop :=
   | eval_funcall_internal:
-      forall m f vargs m1 sp e t e2 m2 out vres,
+      forall m f vargs m1 sp e t e2 m2 out vres m3,
       Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
       set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
       exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out ->
       outcome_result_value out f.(fn_sig).(sig_res) vres ->
-      eval_funcall m (Internal f) vargs t (outcome_free_mem out m2 sp) vres
+      outcome_free_mem out m2 sp f.(fn_stackspace) m3 ->
+      eval_funcall m (Internal f) vargs t m3 vres
   | eval_funcall_external:
-      forall ef m args t res,
-      event_match ef args t res ->
-      eval_funcall m (External ef) args t m res
+      forall ef m args t res m',
+      external_call ef args m t res m' ->
+      eval_funcall m (External ef) args t m' res
 
 (** Execution of a statement: [exec_stmt ge sp e m s t e' m' out]
   means that statement [s] executes with outcome [out].
@@ -759,9 +768,9 @@ End NATURALSEM.
 
 Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
   | bigstep_program_terminates_intro:
-      forall b f t m r,
+      forall b f m0 t m r,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
@@ -770,9 +779,9 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
 
 Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
   | bigstep_program_diverges_intro:
-      forall b f t,
+      forall b f m0 t,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
@@ -1116,6 +1125,6 @@ Qed.
 
 End BIGSTEP_TO_TRANSITION.
 
-
+***************************************************)
 
 
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 85338720..231af8fb 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -19,7 +19,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Events.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Cminor.
 Require Import Op.
 Require Import Globalenvs.
@@ -105,7 +105,7 @@ Definition funsig (fd: fundef) :=
 - [lenv]: let environments, map de Bruijn indices to values.
 *)
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 Definition letenv := list val.
 
 (** Continuations *)
@@ -260,11 +260,12 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_skip_block: forall f k sp e m,
       step (State f Sskip (Kblock k) sp e m)
         E0 (State f Sskip k sp e m)
-  | step_skip_call: forall f k sp e m,
+  | step_skip_call: forall f k sp e m m',
       is_call_cont k ->
       f.(fn_sig).(sig_res) = None ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f Sskip k (Vptr sp Int.zero) e m)
-        E0 (Returnstate Vundef k (Mem.free m sp))
+        E0 (Returnstate Vundef k m')
 
   | step_assign: forall f id a k sp e m v,
       eval_expr sp e m nil a v ->
@@ -287,13 +288,14 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid sig a bl) k sp e m)
         E0 (Callstate fd vargs (Kcall optid f sp e k) m)
 
-  | step_tailcall: forall f sig a bl k sp e m vf vargs fd,
+  | step_tailcall: forall f sig a bl k sp e m vf vargs fd m',
       eval_expr (Vptr sp Int.zero) e m nil a vf ->
       eval_exprlist (Vptr sp Int.zero) e m nil bl vargs ->
       Genv.find_funct ge vf = Some fd ->
       funsig fd = sig ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
-        E0 (Callstate fd vargs (call_cont k) (Mem.free m sp))
+        E0 (Callstate fd vargs (call_cont k) m')
 
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)
@@ -327,13 +329,15 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sswitch a cases default) k sp e m)
         E0 (State f (Sexit (switch_target n default cases)) k sp e m)
 
-  | step_return_0: forall f k sp e m,
+  | step_return_0: forall f k sp e m m',
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f (Sreturn None) k (Vptr sp Int.zero) e m)
-        E0 (Returnstate Vundef (call_cont k) (Mem.free m sp))
-  | step_return_1: forall f a k sp e m v,
+        E0 (Returnstate Vundef (call_cont k) m')
+  | step_return_1: forall f a k sp e m v m',
       eval_expr (Vptr sp Int.zero) e m nil a v ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
       step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m)
-        E0 (Returnstate v (call_cont k) (Mem.free m sp))
+        E0 (Returnstate v (call_cont k) m')
 
   | step_label: forall f lbl s k sp e m,
       step (State f (Slabel lbl s) k sp e m)
@@ -349,10 +353,10 @@ Inductive step: state -> trace -> state -> Prop :=
       set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
-  | step_external_function: forall ef vargs k m t vres,
-      event_match ef vargs t vres ->
+  | step_external_function: forall ef vargs k m t vres m',
+      external_call ef vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
-         t (Returnstate vres k m)        
+         t (Returnstate vres k m')        
 
   | step_return: forall v optid f sp e k m,
       step (Returnstate v (Kcall optid f sp e k) m)
@@ -361,9 +365,9 @@ Inductive step: state -> trace -> state -> Prop :=
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index fff9a60d..6671960c 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -19,7 +19,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 Require Import Events.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Op.
@@ -152,7 +152,7 @@ Lemma functions_translated:
   Genv.find_funct tge v = Some (transf_fundef f).
 Proof.  
   intros.
-  exact (Genv.find_funct_transf transf_fundef H).
+  exact (Genv.find_funct_transf transf_fundef _ _ H).
 Qed.
 
 Lemma function_ptr_translated:
@@ -161,7 +161,7 @@ Lemma function_ptr_translated:
   Genv.find_funct_ptr tge b = Some (transf_fundef f).
 Proof.  
   intros. 
-  exact (Genv.find_funct_ptr_transf transf_fundef H).
+  exact (Genv.find_funct_ptr_transf transf_fundef _ _ H).
 Qed.
 
 Lemma sig_function_translated:
@@ -220,21 +220,19 @@ Qed.
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
    match_stackframe_intro:
-      forall res c sp pc rs f,
-      c = f.(RTL.fn_code) ->
+      forall res sp pc rs f,
       (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) ->
     match_stackframes
-        (Stackframe res c sp pc rs)
-        (Stackframe res (transf_code (analyze f) c) sp pc rs).
+        (Stackframe res f sp pc rs)
+        (Stackframe res (transf_function f) sp pc rs).
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
-      forall s c sp pc rs m f s'
-           (CF: c = f.(RTL.fn_code))
+      forall s sp pc rs m f s'
            (MATCH: regs_match_approx ge (analyze f)!!pc rs)
            (STACKS: list_forall2 match_stackframes s s'),
-      match_states (State s c sp pc rs m)
-                   (State s' (transf_code (analyze f) c) sp pc rs m)
+      match_states (State s f sp pc rs m)
+                   (State s' (transf_function f) sp pc rs m)
   | match_states_call:
       forall s f args m s',
       list_forall2 match_stackframes s s' ->
@@ -249,9 +247,9 @@ Inductive match_states: state -> state -> Prop :=
 Ltac TransfInstr :=
   match goal with
   | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr));
-      [ simpl
-      | unfold transf_code; rewrite PTree.gmap; 
+      cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr));
+      [ simpl transf_instr
+      | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
         unfold option_map; rewrite H1; reflexivity ]
   end.
 
@@ -267,7 +265,7 @@ Proof.
   induction 1; intros; inv MS.
 
   (* Inop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
+  exists (State s' (transf_function f) sp pc' rs m); split.
   TransfInstr; intro. eapply exec_Inop; eauto.
   econstructor; eauto.
   eapply analyze_correct_1 with (pc := pc); eauto.
@@ -275,11 +273,11 @@ Proof.
   unfold transfer; rewrite H. auto.
 
   (* Iop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
+  exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
   TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args);
   intros op' args' OSR.
   assert (eval_operation tge sp op' rs##args' = Some v).
-    rewrite (eval_operation_preserved symbols_preserved). 
+    rewrite (eval_operation_preserved _ _ symbols_preserved). 
     generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
                   MATCH op args v).
     rewrite OSR; simpl. auto.
@@ -305,12 +303,12 @@ Proof.
   caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
   intros addr' args' ASR.
   assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved symbols_preserved). 
+    rewrite (eval_addressing_preserved _ _ symbols_preserved). 
     generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
                   MATCH addr args).
     rewrite ASR; simpl. congruence. 
   TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
+  exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split.
   eapply exec_Iload; eauto.
   econstructor; eauto. 
   eapply analyze_correct_1; eauto. simpl; auto. 
@@ -321,12 +319,12 @@ Proof.
   caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
   intros addr' args' ASR.
   assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved symbols_preserved). 
+    rewrite (eval_addressing_preserved _ _ symbols_preserved). 
     generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
                   MATCH addr args).
     rewrite ASR; simpl. congruence. 
   TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
+  exists (State s' (transf_function f) sp pc' rs m'); split.
   eapply exec_Istore; eauto.
   econstructor; eauto. 
   eapply analyze_correct_1; eauto. simpl; auto. 
@@ -351,7 +349,7 @@ Proof.
   constructor; auto. 
 
   (* Icond, true *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. 
+  exists (State s' (transf_function f) sp ifso rs m); split. 
   caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
   intros cond' args' CSR.
   assert (eval_condition cond' rs##args' = Some true).
@@ -371,7 +369,7 @@ Proof.
   unfold transfer; rewrite H; auto.
 
   (* Icond, false *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. 
+  exists (State s' (transf_function f) sp ifnot rs m); split. 
   caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
   intros cond' args' CSR.
   assert (eval_condition cond' rs##args' = Some false).
@@ -391,7 +389,7 @@ Proof.
   unfold transfer; rewrite H; auto.
 
   (* Ijumptable *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
+  exists (State s' (transf_function f) sp pc' rs m); split.
   caseEq (intval (approx_reg (analyze f)!!pc) arg); intros.
   exploit intval_correct; eauto. eexact MATCH. intro VRS.
   eapply exec_Inop; eauto. TransfInstr. rewrite H2. 
@@ -403,7 +401,7 @@ Proof.
   unfold transfer; rewrite  H; auto.
 
   (* Ireturn *)
-  exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split.
+  exists (Returnstate s' (regmap_optget or Vundef rs) m'); split.
   eapply exec_Ireturn; eauto. TransfInstr; auto.
   constructor; auto.
 
@@ -432,15 +430,14 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split.
+  exists (Callstate nil (transf_fundef f) nil m0); split.
   econstructor; eauto.
+  apply Genv.init_mem_transf; auto.
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
   reflexivity.
-  rewrite <- H2. apply sig_function_translated.
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
-  constructor. constructor. auto.
-  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. 
+  rewrite <- H3. apply sig_function_translated.
+  constructor. constructor.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/LTL.v b/backend/LTL.v
index 6a693361..2a1172ab 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -21,7 +21,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Events.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Op.
@@ -67,7 +67,7 @@ Definition funsig (fd: fundef) :=
 
 (** * Operational semantics *)
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 Definition locset := Locmap.t.
 
 Definition locmap_optget (ol: option loc) (dfl: val) (ls: locset) : val :=
@@ -189,12 +189,13 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (Callstate (Stackframe res f sp (postcall_locs rs) pc' :: s)
                       f' (List.map rs args) m)
   | exec_Ltailcall:
-      forall s f stk pc rs m sig ros args f',
+      forall s f stk pc rs m sig ros args f' m',
       (fn_code f)!pc = Some(Ltailcall sig ros args) ->
       find_function ros rs = Some f' ->
       funsig f' = sig ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) pc rs m)
-        E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
+        E0 (Callstate s f' (List.map rs args) m')
   | exec_Lcond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
@@ -215,20 +216,21 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp pc rs m)
         E0 (State s f sp pc' rs m)
   | exec_Lreturn:
-      forall s f stk pc rs m or,
+      forall s f stk pc rs m or m',
       (fn_code f)!pc = Some(Lreturn or) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) pc rs m)
-        E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk))
+        E0 (Returnstate s (locmap_optget or Vundef rs) m')
   | exec_function_internal:
       forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
       step (Callstate s (Internal f) args m)
         E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m')
   | exec_function_external:
-      forall s ef t args res m,
-      event_match ef args t res ->
+      forall s ef t args res m m',
+      external_call ef args m t res m' ->
       step (Callstate s (External ef) args m)
-         t (Returnstate s res m)
+         t (Returnstate s res m')
   | exec_return:
       forall res f sp rs pc s vres m,
       step (Returnstate (Stackframe res f sp rs pc :: s) vres m)
@@ -242,9 +244,9 @@ End RELSEM.
   by the calling conventions. *)
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
diff --git a/backend/LTLin.v b/backend/LTLin.v
index e3533388..c3b432ba 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -21,7 +21,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -72,7 +72,7 @@ Definition funsig (fd: fundef) :=
   | External ef => ef.(ef_sig)
   end.
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 Definition locset := Locmap.t.
 
 (** * Operational semantics *)
@@ -163,13 +163,13 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lload:
       forall s f sp chunk addr args dst b rs m a v,
       eval_addressing ge sp addr (map rs args) = Some a ->
-      loadv chunk m a = Some v ->
+      Mem.loadv chunk m a = Some v ->
       step (State s f sp (Lload chunk addr args dst :: b) rs m)
         E0 (State s f sp b (Locmap.set dst v rs) m)
   | exec_Lstore:
       forall s f sp chunk addr args src b rs m m' a,
       eval_addressing ge sp addr (map rs args) = Some a ->
-      storev chunk m a (rs src) = Some m' ->
+      Mem.storev chunk m a (rs src) = Some m' ->
       step (State s f sp (Lstore chunk addr args src :: b) rs m)
         E0 (State s f sp b rs m')
   | exec_Lcall:
@@ -180,11 +180,12 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (Callstate (Stackframe res f sp (postcall_locs rs) b :: s)
                       f' (List.map rs args) m)
   | exec_Ltailcall:
-      forall s f stk sig ros args b rs m f',
+      forall s f stk sig ros args b rs m f' m',
       find_function ros rs = Some f' ->
       sig = funsig f' ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m)
-        E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
+        E0 (Callstate s f' (List.map rs args) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
@@ -213,19 +214,20 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Ljumptable arg tbl :: b) rs m)
         E0 (State s f sp b' rs m)
   | exec_Lreturn:
-      forall s f stk rs m or b,
+      forall s f stk rs m or b m',
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m)
-        E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk))
+        E0 (Returnstate s (locmap_optget or Vundef rs) m')
   | exec_function_internal:
       forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
       step (Callstate s (Internal f) args m)
         E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m')
   | exec_function_external:
-      forall s ef args t res m,
-      event_match ef args t res ->
+      forall s ef args t res m m',
+      external_call ef args m t res m' ->
       step (Callstate s (External ef) args m)
-         t (Returnstate s res m)
+         t (Returnstate s res m')
   | exec_return:
       forall res f sp rs b s vres m,
       step (Returnstate (Stackframe res f sp rs b :: s) vres m)
@@ -234,9 +236,9 @@ Inductive step: state -> trace -> state -> Prop :=
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 10058907..69422e0c 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
+Require Import Memdata.
 Require Import Op.
 Require Import RTL.
 Require Import Locations.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 9a2322c7..e1e43f56 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
+Require Import Memdata.
 Require Import Op.
 Require Import RTL.
 Require Import Locations.
diff --git a/backend/Linear.v b/backend/Linear.v
index bf21cb7d..be07b827 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -22,7 +22,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -67,7 +67,7 @@ Definition funsig (fd: fundef) :=
   | External ef => ef.(ef_sig)
   end.
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 Definition locset := Locmap.t.
 
 (** * Operational semantics *)
@@ -253,13 +253,13 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lload:
       forall s f sp chunk addr args dst b rs m a v,
       eval_addressing ge sp addr (reglist rs args) = Some a ->
-      loadv chunk m a = Some v ->
+      Mem.loadv chunk m a = Some v ->
       step (State s f sp (Lload chunk addr args dst :: b) rs m)
         E0 (State s f sp b (Locmap.set (R dst) v rs) m)
   | exec_Lstore:
       forall s f sp chunk addr args src b rs m m' a,
       eval_addressing ge sp addr (reglist rs args) = Some a ->
-      storev chunk m a (rs (R src)) = Some m' ->
+      Mem.storev chunk m a (rs (R src)) = Some m' ->
       step (State s f sp (Lstore chunk addr args src :: b) rs m)
         E0 (State s f sp b rs m')
   | exec_Lcall:
@@ -269,11 +269,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Lcall sig ros :: b) rs m)
         E0 (Callstate (Stackframe f sp rs b:: s) f' rs m)
   | exec_Ltailcall:
-      forall s f stk sig ros b rs m f',
+      forall s f stk sig ros b rs m f' m',
       find_function ros rs = Some f' ->
       sig = funsig f' ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m)
-        E0 (Callstate s f' (return_regs (parent_locset s) rs) (Mem.free m stk))
+        E0 (Callstate s f' (return_regs (parent_locset s) rs) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
@@ -302,21 +303,22 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Ljumptable arg tbl :: b) rs m)
         E0 (State s f sp b' rs m)
   | exec_Lreturn:
-      forall s f stk b rs m,
+      forall s f stk b rs m m',
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) (Lreturn :: b) rs m)
-        E0 (Returnstate s (return_regs (parent_locset s) rs) (Mem.free m stk))
+        E0 (Returnstate s (return_regs (parent_locset s) rs) m')
   | exec_function_internal:
       forall s f rs m m' stk,
-      alloc m 0 f.(fn_stacksize) = (m', stk) ->
+      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
       step (Callstate s (Internal f) rs m)
         E0 (State s f (Vptr stk Int.zero) f.(fn_code) (call_regs rs) m')
   | exec_function_external:
-      forall s ef args res rs1 rs2 m t,
-      event_match ef args t res ->
+      forall s ef args res rs1 rs2 m t m',
+      external_call ef args m t res m' ->
       args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) ->
       rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 ->
       step (Callstate s (External ef) rs1 m)
-         t (Returnstate s rs2 m)
+         t (Returnstate s rs2 m')
   | exec_return:
       forall s f sp rs0 c rs m,
       step (Returnstate (Stackframe f sp rs0 c :: s) rs m)
@@ -325,9 +327,9 @@ Inductive step: state -> trace -> state -> Prop :=
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index c79908d6..5d670650 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -19,7 +19,7 @@ Require Import FSets.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Errors.
@@ -49,14 +49,14 @@ Lemma functions_translated:
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial transf_fundef TRANSF).
+Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF).
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   exists tf,
   Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
+Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
 
 Lemma symbols_preserved:
   forall id,
@@ -73,6 +73,14 @@ Proof.
   inv H. reflexivity.
 Qed.
 
+Lemma stacksize_preserved:
+  forall f tf,
+  transf_function f = OK tf ->
+  LTLin.fn_stacksize tf = LTL.fn_stacksize f.
+Proof.
+  intros. monadInv H. auto.
+Qed.
+
 Lemma find_function_translated:
   forall ros ls f,
   LTL.find_function ge ros ls = Some f ->
@@ -593,6 +601,7 @@ Proof.
   econstructor; split.
   apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto.
   symmetry; apply sig_preserved; auto.
+  rewrite (stacksize_preserved _ _ TRF). eauto.
   econstructor; eauto.
   destruct ros; simpl in H0.
   eapply Genv.find_funct_prop; eauto.
@@ -656,6 +665,7 @@ Proof.
   simpl in EQ. subst c.
   econstructor; split.
   apply plus_one. eapply exec_Lreturn; eauto.
+  rewrite (stacksize_preserved _ _ TRF). eauto.
   econstructor; eauto.
  
   (* internal function *)
@@ -692,16 +702,14 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intros [tf [A B]].  
-  exists (Callstate nil tf nil (Genv.init_mem tprog)); split.
-  econstructor; eauto.
+  exists (Callstate nil tf nil m0); split.
+  econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto. 
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
   symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). 
-  rewrite <- H2. apply sig_preserved. auto.
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
+  rewrite <- H3. apply sig_preserved. auto.
   constructor. constructor. auto.
   eapply Genv.find_funct_ptr_prop; eauto.
-  symmetry. apply Genv.init_mem_transf_partial with transf_fundef. auto.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 1fe77378..028e1200 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
+Require Import Memdata.
 Require Import Op.
 Require Import RTL.
 Require Import Locations.
diff --git a/backend/Mach.v b/backend/Mach.v
index f7e85c3e..e89ff3b1 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -22,7 +22,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Op.
@@ -84,7 +84,7 @@ Definition funsig (fd: fundef) :=
   | External ef => ef.(ef_sig)
   end.
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 
 (** * Dynamic semantics *)
 
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index a2630a2b..ceaf9a68 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -15,10 +15,10 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
-Require Import Mem.
+Require Import Memory.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -262,10 +262,11 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mcall sig ros :: c) rs fr m)
         E0 (Callstate (Stackframe f sp c fr :: s) f' rs m)
   | exec_Mtailcall:
-      forall s f stk soff sig ros c rs fr m f',
+      forall s f stk soff sig ros c rs fr m f' m',
       find_function ros rs = Some f' ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m)
-        E0 (Callstate s f' rs (Mem.free m stk))
+        E0 (Callstate s f' rs m')
   | exec_Mgoto:
       forall s f sp lbl c rs fr m c',
       find_label lbl f.(fn_code) = Some c' ->
@@ -290,9 +291,10 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mjumptable arg tbl :: c) rs fr m)
         E0 (State s f sp c' rs fr m)
   | exec_Mreturn:
-      forall s f stk soff c rs fr m,
+      forall s f stk soff c rs fr m m',
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk soff) (Mreturn :: c) rs fr m)
-        E0 (Returnstate s rs (Mem.free m stk))
+        E0 (Returnstate s rs m')
   | exec_function_internal:
       forall s f rs m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -300,12 +302,12 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk (Int.repr (-f.(fn_framesize))))
                   f.(fn_code) rs empty_frame m')
   | exec_function_external:
-      forall s ef args res rs1 rs2 m t,
-      event_match ef args t res ->
+      forall s ef args res rs1 rs2 m t m',
+      external_call ef args m t res m' ->
       extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args ->
       rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       step (Callstate s (External ef) rs1 m)
-         t (Returnstate s rs2 m)
+         t (Returnstate s rs2 m')
   | exec_return:
       forall f sp c fr s rs m,
       step (Returnstate (Stackframe f sp c fr :: s) rs m)
@@ -314,9 +316,9 @@ Inductive step: state -> trace -> state -> Prop :=
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       initial_state p (Callstate nil f (Regmap.init Vundef) m0).
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index 89529fd4..7714f3d5 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -74,19 +74,27 @@ Hypothesis wt_f: wt_function f.
   semantics. [ms] is the current memory state in the concrete semantics.
   The stack pointer is [Vptr sp base] in both semantics. *)
 
-Inductive frame_match (fr: frame)
-                      (sp: block) (base: int) 
-                      (mm ms: mem) : Prop :=
-  frame_match_intro:
-    valid_block ms sp ->
-    low_bound mm sp = 0 ->
-    low_bound ms sp = -f.(fn_framesize) ->
-    high_bound ms sp >= 0 ->
-    base = Int.repr (-f.(fn_framesize)) ->
-    (forall ty ofs,
-       -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) ->
-       load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) ->
-    frame_match fr sp base mm ms.
+Record frame_match (fr: frame)
+                   (sp: block) (base: int) 
+                   (mm ms: mem) : Prop :=
+  mk_frame_match {
+    fm_valid_1: 
+      Mem.valid_block mm sp;
+    fm_valid_2: 
+      Mem.valid_block ms sp;
+    fm_base:
+      base = Int.repr(- f.(fn_framesize));
+    fm_stackdata_pos: 
+      Mem.low_bound mm sp = 0;
+    fm_write_perm:
+      Mem.range_perm ms sp (-f.(fn_framesize)) 0 Freeable;
+    fm_contents_match:
+      forall ty ofs,
+      -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) ->
+      exists v,
+        Mem.load (chunk_of_type ty) ms sp ofs = Some v
+        /\ Val.lessdef (fr ty ofs) v
+  }.
 
 (** The following two innocuous-looking lemmas are the key results
   showing that [sp]-relative memory accesses in the concrete
@@ -94,8 +102,8 @@ Inductive frame_match (fr: frame)
   semantics.  First, a value [v] that has type [ty] is preserved
   when stored in memory with chunk [chunk_of_type ty], then read
   back with the same chunk.  The typing hypothesis is crucial here:
-  for instance, a float value reads back as [Vundef] when stored
-  and load with chunk [Mint32]. *)
+  for instance, a float value is not preserved when stored
+  and loaded with chunk [Mint32]. *)
 
 Lemma load_result_ty:
   forall v ty,
@@ -127,14 +135,15 @@ Lemma frame_match_load_stack:
   frame_match fr sp base mm ms ->
   0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
   (4 | Int.signed ofs) ->
-  load_stack ms (Vptr sp base) ty ofs = 
-  Some (fr ty (Int.signed ofs - f.(fn_framesize))).
+  exists v,
+     load_stack ms (Vptr sp base) ty ofs = Some v
+  /\ Val.lessdef (fr ty (Int.signed ofs - f.(fn_framesize))) v.
 Proof.
   intros. inv H. inv wt_f.
-  unfold load_stack, Val.add, loadv.
+  unfold load_stack, Val.add, Mem.loadv.
   replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs))
      with (Int.signed ofs - fn_framesize f).
-  apply H7. omega. omega.
+  apply fm_contents_match0. omega. omega.
   apply Zdivide_minus_l; auto. 
   assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
     apply Int.signed_repr.
@@ -149,9 +158,9 @@ Lemma frame_match_get_slot:
   forall fr sp base mm ms ty ofs v,
   frame_match fr sp base mm ms ->
   get_slot f fr ty (Int.signed ofs) v ->
-  load_stack ms (Vptr sp base) ty ofs = Some v.
+  exists v', load_stack ms (Vptr sp base) ty ofs = Some v' /\ Val.lessdef v v'.
 Proof.
-  intros. inversion H. inv H0. inv H7. eapply frame_match_load_stack; eauto.
+  intros. inv H0. inv H1. eapply frame_match_load_stack; eauto.
 Qed.
 
 (** Assigning a value to a frame slot (in the abstract semantics)
@@ -160,19 +169,20 @@ Qed.
   and activation records is preserved. *)
 
 Lemma frame_match_store_stack:
-  forall fr sp base mm ms ty ofs v,
+  forall fr sp base mm ms ty ofs v v',
   frame_match fr sp base mm ms ->
-  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
+  0 <= Int.signed ofs -> Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
   (4 | Int.signed ofs) ->
   Val.has_type v ty ->
+  Val.lessdef v v' ->
   Mem.extends mm ms ->
   exists ms',
-    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
+    store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\
     frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\
     Mem.extends mm ms'.
 Proof.
   intros. inv H. inv wt_f.
-  unfold store_stack, Val.add, storev.
+  unfold store_stack, Val.add, Mem.storev.
   assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) =
           Int.signed ofs - fn_framesize f).
   assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
@@ -183,58 +193,84 @@ Proof.
   apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. 
   compute; congruence.
   rewrite H.
-  assert (exists ms', store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v = Some ms').
-    apply valid_access_store. 
-    constructor. auto. omega.
-    rewrite size_type_chunk. omega.
+  assert ({ ms' | Mem.store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v' = Some ms'}).
+    apply Mem.valid_access_store. constructor.
+    apply Mem.range_perm_implies with Freeable; auto with mem.
+    red; intros; apply fm_write_perm0.
+    rewrite <- size_type_chunk in H1.
+    generalize (size_chunk_pos (chunk_of_type ty)).
+    omega.
     replace (align_chunk (chunk_of_type ty)) with 4.
     apply Zdivide_minus_l; auto.
     destruct ty; auto.
-  destruct H8 as [ms' STORE]. 
-  generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB.
-  generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB.
+  destruct X as [ms' STORE].
   exists ms'. 
   split. exact STORE.
   (* frame match *)
-  split. constructor; try congruence.
-    eauto with mem. intros. unfold update.
-    destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0.
+  split. constructor.
+  (* valid *)
+  eauto with mem.
+  eauto with mem.
+  (* base *)
+  auto.
+  (* stackdata_pos *)
+  auto.
+  (* write_perm *)
+  red; intros; eauto with mem.
+  (* contents *)
+  intros. 
+  exploit fm_contents_match0; eauto. intros [v0 [LOAD0 VLD0]]. 
+  assert (exists v1, Mem.load (chunk_of_type ty0) ms' sp ofs0 = Some v1).
+    apply Mem.valid_access_load; eauto with mem. 
+  destruct H9 as [v1 LOAD1].
+  exists v1; split; auto.
+  unfold update. 
+  destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0.
     destruct (typ_eq ty ty0). subst ty0.
     (* same *)
-    transitivity (Some (Val.load_result (chunk_of_type ty) v)).
-    eapply load_store_same; eauto.
-    decEq. apply load_result_ty; auto.
+    inv H4. 
+    assert (Some v1 = Some (Val.load_result (chunk_of_type ty) v')).
+      rewrite <- LOAD1. eapply Mem.load_store_same; eauto.
+      replace (type_of_chunk (chunk_of_type ty)) with ty. auto.
+      destruct ty; auto.
+    inv H4. rewrite load_result_ty; auto. 
+    auto.
     (* mismatch *)
-    eapply load_store_mismatch'; eauto with mem.
-    destruct ty; destruct ty0; simpl; congruence.
+    auto.
     destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)).
     (* disjoint *)
-    rewrite <- H9; auto. eapply load_store_other; eauto.
-    right; left. rewrite size_type_chunk; auto.
+    assert (Some v1 = Some v0).
+      rewrite <- LOAD0; rewrite <- LOAD1. 
+      eapply Mem.load_store_other; eauto.
+      right; left. rewrite size_type_chunk; auto.
+    inv H9. auto.
     destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)).
-    rewrite <- H9; auto. eapply load_store_other; eauto.
-    right; right. rewrite size_type_chunk; auto.
+    assert (Some v1 = Some v0).
+      rewrite <- LOAD0; rewrite <- LOAD1. 
+      eapply Mem.load_store_other; eauto.
+      right; right. rewrite size_type_chunk; auto.
+    inv H9. auto.
     (* overlap *)
-    eapply load_store_overlap'; eauto with mem.
-    rewrite size_type_chunk; auto. 
-    rewrite size_type_chunk; auto.
+    auto.
   (* extends *)
-  eapply store_outside_extends; eauto.
-  left. rewrite size_type_chunk. omega.
+  eapply Mem.store_outside_extends; eauto.
+  left. rewrite fm_stackdata_pos0. 
+  rewrite size_type_chunk. omega.
 Qed.
 
 Lemma frame_match_set_slot:
-  forall fr sp base mm ms ty ofs v fr',
+  forall fr sp base mm ms ty ofs v fr' v',
   frame_match fr sp base mm ms ->
   set_slot f fr ty (Int.signed ofs) v fr' ->
   Val.has_type v ty ->
+  Val.lessdef v v' ->
   Mem.extends mm ms ->
   exists ms',
-    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
+    store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\
     frame_match fr' sp base mm ms' /\
     Mem.extends mm ms'.
 Proof.
-  intros. inv H0. inv H3. eapply frame_match_store_stack; eauto. 
+  intros. inv H0. inv H4. eapply frame_match_store_stack; eauto. 
 Qed.
 
 (** Agreement is preserved by stores within blocks other than the
@@ -243,45 +279,40 @@ Qed.
 Lemma frame_match_store_other:
   forall fr sp base mm ms chunk b ofs v ms',
   frame_match fr sp base mm ms ->
-  store chunk ms b ofs v = Some ms' ->
+  Mem.store chunk ms b ofs v = Some ms' ->
   sp <> b ->
   frame_match fr sp base mm ms'.
 Proof.
-  intros. inv H. 
-  generalize (low_bound_store _ _ _ _ _ _ H0 sp). intro LB.
-  generalize (high_bound_store _ _ _ _ _ _ H0 sp). intro HB.
-  apply frame_match_intro; auto.
-  eauto with mem. 
-  congruence.
-  congruence.
-  intros. rewrite <- H7; auto. 
-  eapply load_store_other; eauto.
+  intros. inv H. constructor; auto.
+  eauto with mem.
+  red; intros; eauto with mem. 
+  intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]].
+  exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto.
 Qed.
 
 (** Agreement is preserved by parallel stores in the Machabstr
   and the Machconcr semantics. *)
 
 Lemma frame_match_store:
-  forall fr sp base mm ms chunk b ofs v mm' ms',
+  forall fr sp base mm ms chunk b ofs v mm' v' ms',
   frame_match fr sp base mm ms ->
-  store chunk mm b ofs v = Some mm' ->
-  store chunk ms b ofs v = Some ms' ->
+  Mem.store chunk mm b ofs v = Some mm' ->
+  Mem.store chunk ms b ofs v' = Some ms' ->
   frame_match fr sp base mm' ms'.
 Proof.
-  intros. inv H.  
-  generalize (low_bound_store _ _ _ _ _ _ H0 sp). intro LBm.
-  generalize (low_bound_store _ _ _ _ _ _ H1 sp). intro LBs.
-  generalize (high_bound_store _ _ _ _ _ _ H0 sp). intro HBm.
-  generalize (high_bound_store _ _ _ _ _ _ H1 sp). intro HBs.
-  apply frame_match_intro; auto.
+  intros. inv H. constructor; auto.
   eauto with mem.
-  congruence. congruence. congruence.
-  intros. rewrite <- H7; auto. eapply load_store_other; eauto.
-  destruct (zeq sp b). subst b. right. 
+  eauto with mem.
+  rewrite (Mem.bounds_store _ _ _ _ _ _ H0). auto.
+  red; intros; eauto with mem.
+  intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]].
+  exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto.
+  destruct (zeq sp b); auto. subst b. right. 
   rewrite size_type_chunk. 
-  assert (valid_access mm chunk sp ofs) by eauto with mem.
-  inv H9. left. omega.
-  auto.
+  assert (Mem.valid_access mm chunk sp ofs Nonempty) by eauto with mem.
+  exploit Mem.store_valid_access_3. eexact H0. intro. 
+  exploit Mem.valid_access_in_bounds. eauto. rewrite fm_stackdata_pos0. 
+  omega.
 Qed.
 
 (** Memory allocation of the Cminor stack data block (in the abstract
@@ -291,68 +322,111 @@ Qed.
   remain true. *)
 
 Lemma frame_match_new:
-  forall mm ms mm' ms' sp sp',
-  mm.(nextblock) = ms.(nextblock) ->
-  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
-  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') ->
-  sp = sp' /\
+  forall mm ms mm' ms' sp,
+  Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
+  Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp) ->
   frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'.
 Proof.
   intros. 
-  assert (sp = sp').
-    exploit alloc_result. eexact H0. exploit alloc_result. eexact H1. 
-    congruence. 
-  subst sp'. split. auto.
-  generalize (low_bound_alloc_same _ _ _ _ _ H0). intro LBm.
-  generalize (low_bound_alloc_same _ _ _ _ _ H1). intro LBs.
-  generalize (high_bound_alloc_same _ _ _ _ _ H0). intro HBm.
-  generalize (high_bound_alloc_same _ _ _ _ _ H1). intro HBs.
   inv wt_f.
   constructor; simpl; eauto with mem.
-  rewrite HBs. auto.
-  intros.
-  eapply load_alloc_same'; eauto.  
+  rewrite (Mem.bounds_alloc_same _ _ _ _ _ H). auto.
+  red; intros. eapply Mem.perm_alloc_2; eauto. omega.
+  intros. exists Vundef; split.
+  eapply Mem.load_alloc_same'; eauto. 
   rewrite size_type_chunk. omega.
-  replace (align_chunk (chunk_of_type ty)) with 4; auto. destruct ty; auto.
+  replace (align_chunk (chunk_of_type ty)) with 4; auto.
+  destruct ty; auto.
+  unfold empty_frame. auto.
 Qed.
 
 Lemma frame_match_alloc:
-  forall mm ms fr sp base lom him los his mm' ms' bm bs,
-  mm.(nextblock) = ms.(nextblock) ->
+  forall mm ms fr sp base lom him los his mm' ms' b,
   frame_match fr sp base mm ms ->
-  alloc mm lom him = (mm', bm) ->
-  alloc ms los his = (ms', bs) ->
+  Mem.alloc mm lom him = (mm', b) ->
+  Mem.alloc ms los his = (ms', b) ->
   frame_match fr sp base mm' ms'.
 Proof.
-  intros. inversion H0.
-  assert (valid_block mm sp). red. rewrite H. auto.
-  exploit low_bound_alloc_other. eexact H1. eexact H9. intro LBm.
-  exploit high_bound_alloc_other. eexact H1. eexact H9. intro HBm.
-  exploit low_bound_alloc_other. eexact H2. eexact H3. intro LBs.
-  exploit high_bound_alloc_other. eexact H2. eexact H3. intro HBs.
-  apply frame_match_intro.
-  eapply valid_block_alloc; eauto.
-  congruence. congruence. congruence. auto. auto.
-  intros. eapply load_alloc_other; eauto. 
+  intros. inversion H.
+  assert (sp <> b). 
+    apply Mem.valid_not_valid_diff with ms; eauto with mem.
+  constructor; auto.
+  eauto with mem.
+  eauto with mem.
+  rewrite (Mem.bounds_alloc_other _ _ _ _ _ H0); auto.
+  red; intros; eauto with mem.
+  intros. exploit fm_contents_match0; eauto. intros [v [LOAD LD]].
+  exists v; split; auto. eapply Mem.load_alloc_other; eauto. 
 Qed.
 
 (** [frame_match] relations are preserved by freeing a block
   other than the one pointed to by [sp]. *)
 
 Lemma frame_match_free:
-  forall fr sp base mm ms b,
+  forall fr sp base mm ms b lom him los his mm' ms',
   frame_match fr sp base mm ms ->
   sp <> b ->
-  frame_match fr sp base (free mm b) (free ms b).
+  Mem.free mm b lom him = Some mm' ->
+  Mem.free ms b los his = Some ms' ->
+  frame_match fr sp base mm' ms'.
+Proof.
+  intros. inversion H. constructor; auto.
+  eauto with mem.
+  eauto with mem.
+  rewrite (Mem.bounds_free _ _ _ _ _ H1). auto.
+  red; intros; eauto with mem. 
+  intros. rewrite (Mem.load_free _ _ _ _ _ H2); auto.
+Qed.
+
+Lemma frame_match_delete:
+  forall fr sp base mm ms mm',
+  frame_match fr sp base mm ms ->
+  Mem.free mm sp 0 f.(fn_stacksize) = Some mm' ->
+  Mem.extends mm ms ->
+  exists ms',
+  Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms'
+  /\ Mem.extends mm' ms'.
 Proof.
   intros. inversion H.
-  generalize (low_bound_free mm _ _ H0); intro LBm.
-  generalize (low_bound_free ms _ _ H0); intro LBs.
-  generalize (high_bound_free mm _ _ H0); intro HBm.
-  generalize (high_bound_free ms _ _ H0); intro HBs.
-  apply frame_match_intro; auto.
-  congruence. congruence. congruence.
-  intros. rewrite <- H6; auto. apply load_free. auto.
+  assert (Mem.range_perm mm sp 0 (fn_stacksize f) Freeable).
+    eapply Mem.free_range_perm; eauto. 
+  assert ({ ms' | Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms' }).
+  apply Mem.range_perm_free. 
+  red; intros. destruct (zlt ofs 0). 
+  apply fm_write_perm0. omega. 
+  eapply Mem.perm_extends; eauto. apply H2. omega.
+  destruct X as [ms' FREE]. exists ms'; split; auto.
+  eapply Mem.free_right_extends; eauto. 
+  eapply Mem.free_left_extends; eauto.
+  intros; red; intros.
+  exploit Mem.perm_in_bounds; eauto. 
+  rewrite (Mem.bounds_free _ _ _ _ _ H0). rewrite fm_stackdata_pos0; intro. 
+  exploit Mem.perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. 
+  auto.
+Qed.
+
+(** [frame_match] is preserved by external calls. *)
+
+Lemma frame_match_external_call:
+  forall fr sp base mm ms mm' ms' ef vargs vres t vargs' vres',
+  frame_match fr sp base mm ms ->
+  Mem.extends mm ms ->
+  external_call ef vargs mm t vres mm' ->
+  Mem.extends mm' ms' ->
+  external_call ef vargs' ms t vres' ms' ->
+  mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
+  frame_match fr sp base mm' ms'.
+Proof.
+  intros. destruct H4 as [A B]. inversion H. constructor.
+  eapply external_call_valid_block; eauto.
+  eapply external_call_valid_block; eauto.
+  auto.
+  rewrite (external_call_bounds _ _ _ _ _ _ _ H1); auto.
+  red; intros. apply A; auto. red. omega.
+  intros. exploit fm_contents_match0; eauto. intros [v [C D]].
+  exists v; split; auto.
+  apply B; auto. 
+  rewrite size_type_chunk; intros; red. omega.
 Qed.
 
 End FRAME_MATCH.
@@ -430,61 +504,130 @@ Proof.
   simpl. omega.
 Qed.
 
+Definition is_pointer_or_int (v: val) : Prop :=
+  match v with
+  | Vint _ => True
+  | Vptr _ _ => True
+  | _ => False
+  end.
+
+Remark is_pointer_has_type:
+  forall v, is_pointer_or_int v -> Val.has_type v Tint.
+Proof.
+  intros; destruct v; elim H; exact I. 
+Qed.
+
+Lemma frame_match_load_stack_pointer:
+  forall fr sp base mm ms ty ofs,
+  frame_match f fr sp base mm ms ->
+  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
+  (4 | Int.signed ofs) ->
+  is_pointer_or_int (fr ty (Int.signed ofs - f.(fn_framesize))) ->
+  load_stack ms (Vptr sp base) ty ofs = Some (fr ty (Int.signed ofs - f.(fn_framesize))).
+Proof.
+  intros. exploit frame_match_load_stack; eauto. 
+  intros [v [LOAD LD]]. 
+  inv LD. auto. rewrite <- H4 in H2. elim H2.
+Qed.
+
 Lemma frame_match_load_link:
   forall fr sp base mm ms,
   frame_match f (extend_frame fr) sp base mm ms ->
-  load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs).
+  is_pointer_or_int (parent_sp cs) ->
+  load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some(parent_sp cs).
 Proof.
   intros. inversion wt_f.
-  replace (parent_sp cs) with
-   (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))).
-  eapply frame_match_load_stack; eauto.
-  
-  unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. 
+  assert (parent_sp cs =
+    extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))).
+  unfold extend_frame. rewrite update_other. rewrite update_same. auto. 
+  simpl. omega.
+  rewrite H1; eapply frame_match_load_stack_pointer; eauto.
+  rewrite <- H1; auto.
 Qed.
 
 Lemma frame_match_load_retaddr:
   forall fr sp base mm ms,
   frame_match f (extend_frame fr) sp base mm ms ->
-  load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs).
+  is_pointer_or_int (parent_ra cs) ->
+  load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some(parent_ra cs).
 Proof.
   intros. inversion wt_f.
-  replace (parent_ra cs) with
-   (extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))).
-  eapply frame_match_load_stack; eauto.
-  unfold extend_frame. apply update_same.
+  assert (parent_ra cs =
+    extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))).
+  unfold extend_frame. rewrite update_same. auto. 
+  rewrite H1; eapply frame_match_load_stack_pointer; eauto.
+  rewrite <- H1; auto.
 Qed.
 
 Lemma frame_match_function_entry:
-  forall mm ms mm' ms1 sp sp',
-  extends mm ms ->
-  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
-  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') ->
-  Val.has_type (parent_sp cs) Tint ->
-  Val.has_type (parent_ra cs) Tint ->
+  forall mm ms mm' sp,
+  Mem.extends mm ms ->
+  Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
+  is_pointer_or_int (parent_sp cs) ->
+  is_pointer_or_int (parent_ra cs) ->
   let base := Int.repr (-f.(fn_framesize)) in
-  exists ms2, exists ms3,
-  sp = sp' /\
+  exists ms1, exists ms2, exists ms3,
+  Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp) /\
   store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\
   store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\
   frame_match f (extend_frame empty_frame) sp base mm' ms3 /\
-  extends mm' ms3.
+  Mem.extends mm' ms3.
 Proof.
   intros. inversion wt_f.
-  exploit alloc_extends; eauto. omega. omega. intros [A EXT0].
-  exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto.
-  fold base. intros [C FM0].
-  destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
-              FM0 wt_function_link wt_function_link_aligned H2 EXT0)
-  as [ms2 [STORE1 [FM1 EXT1]]].
-  destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
-              FM1 wt_function_retaddr wt_function_retaddr_aligned H3 EXT1)
-  as [ms3 [STORE2 [FM3 EXT3]]].
-  exists ms2; exists ms3; auto.
+  exploit Mem.alloc_extends; eauto.
+  instantiate (1 := -f.(fn_framesize)). omega.
+  instantiate (1 := f.(fn_stacksize)). omega.
+  intros [ms1 [A EXT0]].
+  exploit frame_match_new; eauto. fold base. intros FM0.
+  exploit frame_match_store_stack. eauto. eexact FM0. 
+  instantiate (1 := fn_link_ofs f); omega.
+  instantiate (1 := Tint). simpl; omega.
+  auto. apply is_pointer_has_type. eexact H1. constructor. auto.
+  intros [ms2 [STORE1 [FM1 EXT1]]].
+  exploit frame_match_store_stack. eauto. eexact FM1. 
+  instantiate (1 := fn_retaddr_ofs f); omega.
+  instantiate (1 := Tint). simpl; omega.
+  auto. apply is_pointer_has_type. eexact H2. constructor. auto.
+  intros [ms3 [STORE2 [FM2 EXT2]]].
+  exists ms1; exists ms2; exists ms3; auto.
 Qed.
 
 End EXTEND_FRAME.
 
+(** ** The ``less defined than'' relation between register states. *)
+
+Definition regset_lessdef (rs1 rs2: regset) : Prop :=
+  forall r, Val.lessdef (rs1 r) (rs2 r).
+
+Lemma regset_lessdef_list:
+  forall rs1 rs2, regset_lessdef rs1 rs2 ->
+  forall rl, Val.lessdef_list (rs1##rl) (rs2##rl).
+Proof.
+  induction rl; simpl.
+  constructor.
+  constructor; auto.
+Qed.
+
+Lemma regset_lessdef_set:
+  forall rs1 rs2 r v1 v2,
+  regset_lessdef rs1 rs2 -> Val.lessdef v1 v2 ->
+  regset_lessdef (rs1#r <- v1) (rs2#r <- v2).
+Proof.
+  intros; red; intros. unfold Regmap.set.
+  destruct (RegEq.eq r0 r); auto. 
+Qed.
+
+Lemma regset_lessdef_find_function_ptr:
+  forall ge ros rs1 rs2 fb,
+  find_function_ptr ge ros rs1 = Some fb ->
+  regset_lessdef rs1 rs2 ->
+  find_function_ptr ge ros rs2 = Some fb.
+Proof.
+  unfold find_function_ptr; intros; destruct ros; simpl in *.
+  generalize (H0 m); intro LD; inv LD. auto. rewrite <- H2 in H. congruence.
+  auto.
+Qed.
+
 (** ** Invariant for stacks *)
 
 Section SIMULATION.
@@ -518,12 +661,26 @@ Inductive match_stacks:
       wt_function f ->
       frame_match f (extend_frame f ts fr) sp base mm ms ->
       stack_below ts sp ->
-      Val.has_type ra Tint ->
+      is_pointer_or_int ra ->
       match_stacks s ts mm ms ->
       match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s)
                    (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts)
                    mm ms.
 
+Lemma match_stacks_parent_sp_pointer:
+  forall s ts mm ms,
+  match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_sp ts).
+Proof.
+  induction 1; simpl; auto.
+Qed.
+
+Lemma match_stacks_parent_ra_pointer:
+  forall s ts mm ms,
+  match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_ra ts).
+Proof.
+  induction 1; simpl; auto.
+Qed.
+
 (** If [match_stacks] holds, a lookup in the parent frame in the
   Machabstr semantics corresponds to two memory loads in the
   Machconcr semantics, one to load the pointer to the parent's
@@ -533,7 +690,9 @@ Lemma match_stacks_get_parent:
   forall s ts mm ms ty ofs v,
   match_stacks s ts mm ms ->
   get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v ->
-  load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v.
+  exists v',
+     load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v'
+  /\ Val.lessdef v v'.
 Proof.
   intros. inv H; simpl in H0. 
   inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega.
@@ -542,7 +701,7 @@ Proof.
 Qed.
 
 (** Preservation of the [match_stacks] invariant
-    by various kinds of memory stores. *)
+    by various kinds of memory operations. *)
 
 Remark stack_below_trans:
   forall ts b b', 
@@ -556,7 +715,7 @@ Lemma match_stacks_store_other:
   forall s ts ms mm,
   match_stacks s ts mm ms ->
   forall chunk b ofs v ms',
-  store chunk ms b ofs v = Some ms' ->
+  Mem.store chunk ms b ofs v = Some ms' ->
   stack_below ts b ->
   match_stacks s ts mm ms'.
 Proof.
@@ -593,9 +752,9 @@ Qed.
 Lemma match_stacks_store:
   forall s ts ms mm,
   match_stacks s ts mm ms ->
-  forall chunk b ofs v mm' ms',
-  store chunk mm b ofs v = Some mm' ->
-  store chunk ms b ofs v = Some ms' ->
+  forall chunk b ofs v mm' v' ms',
+  Mem.store chunk mm b ofs v = Some mm' ->
+  Mem.store chunk ms b ofs v' = Some ms' ->
   match_stacks s ts mm' ms'.
 Proof.
   induction 1; intros.
@@ -607,28 +766,28 @@ Qed.
 Lemma match_stacks_alloc:
   forall s ts ms mm,
   match_stacks s ts mm ms ->
-  forall lom him mm' bm los his ms' bs,
-  mm.(nextblock) = ms.(nextblock) ->
-  alloc mm lom him = (mm', bm) ->
-  alloc ms los his = (ms', bs) ->
+  forall lom him mm' b los his ms',
+  Mem.alloc mm lom him = (mm', b) ->
+  Mem.alloc ms los his = (ms', b) ->
   match_stacks s ts mm' ms'.
 Proof.
   induction 1; intros.
   constructor.
-  econstructor; eauto.
-  eapply frame_match_alloc; eauto.
+  econstructor; eauto. eapply frame_match_alloc; eauto.
 Qed.
 
 Lemma match_stacks_free:
   forall s ts ms mm,
   match_stacks s ts mm ms ->
-  forall b,
+  forall b lom him los his mm' ms',
+  Mem.free mm b lom him = Some mm' ->
+  Mem.free ms b los his = Some ms' ->
   stack_below ts b ->
-  match_stacks s ts (Mem.free mm b) (Mem.free ms b).
+  match_stacks s ts mm' ms'.
 Proof.
   induction 1; intros.
   constructor.
-  red in H5; simpl in H5.
+  red in H7; simpl in H7.
   econstructor; eauto.
   eapply frame_match_free; eauto. unfold block; omega.
   eapply IHmatch_stacks; eauto.
@@ -636,21 +795,36 @@ Proof.
 Qed.
 
 Lemma match_stacks_function_entry:
-  forall s ts mm ms lom him mm' los his ms' stk,
+  forall s ts ms mm,
   match_stacks s ts mm ms ->
-  alloc mm lom him = (mm', stk) ->
-  alloc ms los his = (ms', stk) ->
+  forall lom him mm' stk los his ms',
+  Mem.alloc mm lom him = (mm', stk) ->
+  Mem.alloc ms los his = (ms', stk) ->
   match_stacks s ts mm' ms' /\ stack_below ts stk.
 Proof.
   intros.
-  assert (stk = nextblock mm). eapply Mem.alloc_result; eauto.
-  assert (stk = nextblock ms). eapply Mem.alloc_result; eauto.
-  split.
-  eapply match_stacks_alloc; eauto. congruence.
-  red. 
-  inv H; simpl.
-  unfold nullptr. apply Zgt_lt. apply nextblock_pos. 
-  inv H6. red in H. rewrite H3. auto. 
+  assert (stk = Mem.nextblock mm) by eauto with mem.
+  split. eapply match_stacks_alloc; eauto.
+  red. inv H; simpl.
+  unfold Mem.nullptr. apply Zgt_lt. apply Mem.nextblock_pos.
+  inv H5. auto. 
+Qed.
+
+Lemma match_stacks_external_call:
+  forall s ts mm ms,
+  match_stacks s ts mm ms ->
+  forall ef vargs t vres mm' ms' vargs' vres',
+  Mem.extends mm ms ->
+  external_call ef vargs mm t vres mm' ->
+  Mem.extends mm' ms' ->
+  external_call ef vargs' ms t vres' ms' ->
+  mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
+  match_stacks s ts mm' ms'.
+Proof.
+  induction 1; intros.
+  constructor.
+  econstructor; eauto. 
+  eapply frame_match_external_call; eauto. 
 Qed.
 
 (** ** Invariant between states. *)
@@ -666,27 +840,30 @@ Qed.
 Inductive match_states:
             Machabstr.state -> Machconcr.state -> Prop :=
   | match_states_intro:
-      forall s f sp base c rs fr mm ts fb ms
+      forall s f sp base c rs fr mm ts trs fb ms
         (STACKS: match_stacks s ts mm ms)
         (FM: frame_match f (extend_frame f ts fr) sp base mm ms)
         (BELOW: stack_below ts sp)
+        (RLD: regset_lessdef rs trs)
         (MEXT: Mem.extends mm ms)
         (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)),
       match_states (Machabstr.State s f (Vptr sp base) c rs fr mm)
-                   (Machconcr.State ts fb (Vptr sp base) c rs ms)
+                   (Machconcr.State ts fb (Vptr sp base) c trs ms)
   | match_states_call:
-      forall s f rs mm ts fb ms
+      forall s f rs mm ts trs fb ms
         (STACKS: match_stacks s ts mm ms)
         (MEXT: Mem.extends mm ms)
+        (RLD: regset_lessdef rs trs)
         (FIND: Genv.find_funct_ptr ge fb = Some f),
       match_states (Machabstr.Callstate s f rs mm)
-                   (Machconcr.Callstate ts fb rs ms)
+                   (Machconcr.Callstate ts fb trs ms)
   | match_states_return:
-      forall s rs mm ts ms
+      forall s rs mm ts trs ms
         (STACKS: match_stacks s ts mm ms)
-        (MEXT: Mem.extends mm ms),
+        (MEXT: Mem.extends mm ms)
+        (RLD: regset_lessdef rs trs),
       match_states (Machabstr.Returnstate s rs mm)
-                   (Machconcr.Returnstate ts rs ms).
+                   (Machconcr.Returnstate ts trs ms).
 
 (** * The proof of simulation *)
 
@@ -725,20 +902,26 @@ Qed.
 (** Preservation of arguments to external functions. *)
 
 Lemma transl_extcall_arguments:
-  forall rs s sg args ts m ms,
+  forall rs s sg args ts trs m ms,
   Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args ->
+  regset_lessdef rs trs ->
   match_stacks s ts m ms ->
-  extcall_arguments rs ms (parent_sp ts) sg args.
+  exists targs,
+     extcall_arguments trs ms (parent_sp ts) sg targs
+  /\ Val.lessdef_list args targs.
 Proof.
   unfold Machabstr.extcall_arguments, extcall_arguments; intros.
-  assert (forall locs vals,
-    Machabstr.extcall_args (parent_function s) rs (parent_frame s) locs vals ->
-    extcall_args rs ms (parent_sp ts) locs vals).
-  induction locs; intros; inv H1.
-  constructor.
+  generalize (Conventions.loc_arguments sg) args H.
+  induction l; intros; inv H2.
+  exists (@nil val); split; constructor.
+  exploit IHl; eauto. intros [targs [A B]].
+  inv H7. exists (trs r :: targs); split.
+  constructor; auto. constructor. 
+  constructor; auto.
+  exploit match_stacks_get_parent; eauto. intros [targ [C D]]. 
+  exists (targ :: targs); split. 
+  constructor; auto. constructor; auto. 
   constructor; auto.
-  inv H6. constructor. constructor. eapply match_stacks_get_parent; eauto.
-  auto.
 Qed.
 
 Hypothesis wt_prog: wt_program p.
@@ -757,11 +940,11 @@ Proof.
 
   (* Mgetstack *)
   assert (WTF: wt_function f) by (inv WTS; auto).
-  exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split.
+  exploit frame_match_get_slot; eauto. eapply get_slot_extends; eauto. 
+  intros [v' [A B]]. 
+  exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split.
   constructor; auto.
-  eapply frame_match_get_slot; eauto.
-  eapply get_slot_extends; eauto.
-  econstructor; eauto with coqlib.
+  econstructor; eauto with coqlib. eapply regset_lessdef_set; eauto. 
 
   (* Msetstack *)
   assert (WTF: wt_function f) by (inv WTS; auto).
@@ -769,41 +952,51 @@ Proof.
     inv WTS. 
     generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI.
     inv WTI. apply WTRS.
-  exploit frame_match_set_slot; eauto.
+  exploit frame_match_set_slot. eauto. eauto. 
     eapply set_slot_extends; eauto.
+    auto. apply RLD. auto. 
   intros [ms' [STORE [FM' EXT']]].
-  exists (State ts fb (Vptr sp0 base) c rs ms'); split.
+  exists (State ts fb (Vptr sp0 base) c trs ms'); split.
   apply exec_Msetstack; auto.
   econstructor; eauto.
   eapply match_stacks_store_slot; eauto.
 
   (* Mgetparam *)
   assert (WTF: wt_function f) by (inv WTS; auto).
-  exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split.
+  exploit match_stacks_get_parent; eauto. intros [v' [A B]].
+  exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split.
   eapply exec_Mgetparam; eauto.
     eapply frame_match_load_link; eauto.
-    eapply match_stacks_get_parent; eauto.
-  econstructor; eauto with coqlib. 
+    eapply match_stacks_parent_sp_pointer; eauto.
+  econstructor; eauto with coqlib. apply regset_lessdef_set; eauto. 
  
   (* Mop *)
-  exists (State ts fb (Vptr sp0 base) c (rs#res <- v) ms); split.
+  exploit eval_operation_lessdef. 2: eauto.
+  eapply regset_lessdef_list; eauto. 
+  intros [v' [A B]].
+  exists (State ts fb (Vptr sp0 base) c (trs#res <- v') ms); split.
   apply exec_Mop; auto.
-  econstructor; eauto with coqlib.
+  econstructor; eauto with coqlib. apply regset_lessdef_set; eauto.
 
   (* Mload *)
-  exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split.
+  exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto.
+  intros [a' [A B]].
+  exploit Mem.loadv_extends. eauto. eauto. eexact B. 
+  intros [v' [C D]].
+  exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split.
   eapply exec_Mload; eauto.
-  destruct a; simpl in H0; try discriminate.
-  simpl. eapply Mem.load_extends; eauto.
-  econstructor; eauto with coqlib.
+  econstructor; eauto with coqlib. apply regset_lessdef_set; eauto.
 
   (* Mstore *)
-  destruct a; simpl in H0; try discriminate.
-  exploit Mem.store_within_extends; eauto. intros [ms' [STORE MEXT']].
-  exists (State ts fb (Vptr sp0 base) c rs ms'); split.
+  exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto.
+  intros [a' [A B]].
+  exploit Mem.storev_extends. eauto. eauto. eexact B. apply RLD. 
+  intros [ms' [C D]].
+  exists (State ts fb (Vptr sp0 base) c trs ms'); split.
   eapply exec_Mstore; eauto.
+  destruct a; simpl in H0; try congruence. inv B. simpl in C. 
   econstructor; eauto with coqlib.
-  eapply match_stacks_store; eauto.
+  eapply match_stacks_store. eauto. eexact H0. eexact C.
   eapply frame_match_store; eauto.
 
   (* Mcall *)
@@ -814,7 +1007,7 @@ Proof.
     inv WTS. eapply is_tail_cons_left; eauto.
   destruct H0 as [ra' RETADDR].
   econstructor; split.
-  eapply exec_Mcall; eauto. 
+  eapply exec_Mcall; eauto. eapply regset_lessdef_find_function_ptr; eauto. 
   econstructor; eauto. 
   econstructor; eauto. inv WTS; auto. exact I.
 
@@ -822,12 +1015,13 @@ Proof.
   assert (WTF: wt_function f) by (inv WTS; auto).
   exploit find_function_find_function_ptr; eauto. 
   intros [fb' [FIND' FINDFUNCT]].
+  exploit frame_match_delete; eauto. intros [ms' [A B]].
   econstructor; split.
   eapply exec_Mtailcall; eauto.
-    eapply frame_match_load_link; eauto.
-    eapply frame_match_load_retaddr; eauto.
-  econstructor; eauto. eapply match_stacks_free; auto.
-  apply free_extends; auto.
+    eapply regset_lessdef_find_function_ptr; eauto. 
+    eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto.
+    eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto.
+  econstructor; eauto. eapply match_stacks_free; eauto.
 
   (* Mgoto *)
   econstructor; split.
@@ -837,49 +1031,50 @@ Proof.
   (* Mcond *)
   econstructor; split.
   eapply exec_Mcond_true; eauto.
+  eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto.
   econstructor; eauto.
   econstructor; split.
   eapply exec_Mcond_false; eauto.
+  eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto.
   econstructor; eauto.
 
   (* Mjumptable *)
   econstructor; split.
-  eapply exec_Mjumptable; eauto. 
+  eapply exec_Mjumptable; eauto.
+  generalize (RLD arg); intro LD. rewrite H in LD. inv LD. auto.  
   econstructor; eauto.
 
   (* Mreturn *)
   assert (WTF: wt_function f) by (inv WTS; auto).
+  exploit frame_match_delete; eauto. intros [ms' [A B]].
   econstructor; split.
   eapply exec_Mreturn; eauto.
-    eapply frame_match_load_link; eauto.
-    eapply frame_match_load_retaddr; eauto.
+    eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto.
+    eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto.
   econstructor; eauto. eapply match_stacks_free; eauto.   
-  apply free_extends; auto.
 
   (* internal function *)
   assert (WTF: wt_function f). inv WTS. inv H5. auto.
-  caseEq (alloc ms (- f.(fn_framesize)) f.(fn_stacksize)).
-  intros ms' stk' ALLOC.
-  assert (Val.has_type (parent_sp ts) Tint).
-    inv STACKS; simpl; auto.
-  assert (Val.has_type (parent_ra ts) Tint).
-    inv STACKS; simpl; auto.
-  destruct (frame_match_function_entry _ WTF _ _ _ _ _ _ _
-              MEXT H ALLOC H0 H1)
-  as [ms2 [ms3 [EQ [STORE1 [STORE2 [FM MEXT']]]]]].
-  subst stk'.
+  exploit frame_match_function_entry. eauto. eauto. eauto. 
+  instantiate (1 := ts). eapply match_stacks_parent_sp_pointer; eauto.
+  eapply match_stacks_parent_ra_pointer; eauto.
+  intros [ms1 [ms2 [ms3 [ALLOC [STORE1 [STORE2 [FM MEXT']]]]]]].
   econstructor; split.
   eapply exec_function_internal; eauto.
   exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW].
   econstructor; eauto.
   eapply match_stacks_store_slot with (ms := ms2); eauto.
-  eapply match_stacks_store_slot with (ms := ms'); eauto.
+  eapply match_stacks_store_slot with (ms := ms1); eauto.
 
   (* external function *)
+  exploit transl_extcall_arguments; eauto. intros [targs [A B]].
+  exploit external_call_mem_extends; eauto. 
+  intros [tres [ms' [C [D [E F]]]]]. 
   econstructor; split.
-  eapply exec_function_external; eauto. 
-  eapply transl_extcall_arguments; eauto.
+  eapply exec_function_external. eauto. eexact C. eexact A. reflexivity.  
   econstructor; eauto.
+  eapply match_stacks_external_call; eauto. 
+  apply regset_lessdef_set; auto. 
 
   (* return *)
   inv STACKS.
@@ -894,8 +1089,10 @@ Lemma equiv_initial_states:
 Proof.
   intros. inversion H.
   econstructor; split.
-  econstructor. eauto. 
-  split. econstructor. constructor. apply Mem.extends_refl. auto.
+  econstructor. eauto. eauto. 
+  split. econstructor. constructor. apply Mem.extends_refl.
+  unfold Regmap.init; red; intros. constructor.
+  auto.
   econstructor. simpl; intros; contradiction.
   eapply Genv.find_funct_ptr_prop; eauto.
   red; intros; exact I.
@@ -906,7 +1103,9 @@ Lemma equiv_final_states:
   match_states st1 st2 /\ wt_state st1 -> Machabstr.final_state st1 r -> Machconcr.final_state st2 r.
 Proof.
   intros. inv H0. destruct H. inv H. inv STACKS.
-  constructor; auto.
+  constructor. 
+  generalize (RLD (Conventions.loc_result (mksignature nil (Some Tint)))).
+  rewrite H1. intro LD. inv LD. auto. 
 Qed.
 
 Theorem exec_program_equiv:
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 84ae0a4f..a6be4bc2 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -179,13 +179,14 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s)
                        f' rs m)
   | exec_Mtailcall:
-      forall s fb stk soff sig ros c rs m f f',
+      forall s fb stk soff sig ros c rs m f f' m',
       find_function_ptr ge ros rs = Some f' ->
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
       load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
       load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+      Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
       step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
-        E0 (Callstate s f' rs (Mem.free m stk))
+        E0 (Callstate s f' rs m')
   | exec_Mgoto:
       forall s fb f sp lbl c rs m c',
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
@@ -213,12 +214,13 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s fb sp (Mjumptable arg tbl :: c) rs m)
         E0 (State s fb sp c' rs m)
   | exec_Mreturn:
-      forall s fb stk soff c rs m f,
+      forall s fb stk soff c rs m f m',
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
       load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
       load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+      Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
       step (State s fb (Vptr stk soff) (Mreturn :: c) rs m)
-        E0 (Returnstate s rs (Mem.free m stk))
+        E0 (Returnstate s rs m')
   | exec_function_internal:
       forall s fb rs m f m1 m2 m3 stk,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
@@ -229,13 +231,13 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate s fb rs m)
         E0 (State s fb sp f.(fn_code) rs m3)
   | exec_function_external:
-      forall s fb rs m t rs' ef args res,
+      forall s fb rs m t rs' ef args res m',
       Genv.find_funct_ptr ge fb = Some (External ef) ->
-      event_match ef args t res ->
+      external_call ef args m t res m' ->
       extcall_arguments rs m (parent_sp s) ef.(ef_sig) args ->
       rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       step (Callstate s fb rs m)
-         t (Returnstate s rs' m)
+         t (Returnstate s rs' m')
   | exec_return:
       forall s f sp ra c rs m,
       step (Returnstate (Stackframe f sp ra c :: s) rs m)
@@ -244,9 +246,9 @@ Inductive step: state -> trace -> state -> Prop :=
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall fb,
+  | initial_state_intro: forall fb m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some fb ->
       initial_state p (Callstate nil fb (Regmap.init Vundef) m0).
 
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 8b40001a..c2e797ae 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -15,10 +15,10 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
-Require Import Mem.
+Require Import Memory.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Op.
@@ -194,14 +194,6 @@ Proof.
   constructor; auto.
 Qed.
 
-Lemma wt_event_match:
-  forall ef args t res,
-  event_match ef args t res ->
-  Val.has_type res (proj_sig_res ef.(ef_sig)).
-Proof.
-  induction 1. inversion H0; exact I.
-Qed.
-
 Section SUBJECT_REDUCTION.
 
 Inductive wt_stackframe: stackframe -> Prop :=
@@ -259,7 +251,7 @@ Proof.
     simpl in H. 
     rewrite <- H2. replace v with (rs r1). apply WTRS. congruence.
     replace (mreg_type res) with (snd (type_of_operation op)).
-    apply type_of_operation_sound with fundef ge rs##args sp; auto.
+    apply type_of_operation_sound with fundef unit ge rs##args sp; auto.
     rewrite <- H5; reflexivity.
 
   apply wt_setreg; auto. inversion H1. rewrite H7.
@@ -267,18 +259,18 @@ Proof.
 
   assert (WTFD: wt_fundef f').
     destruct ros; simpl in H.
-    apply (Genv.find_funct_prop wt_fundef wt_p H).
+    apply (Genv.find_funct_prop wt_fundef _ _ wt_p H).
     destruct (Genv.find_symbol ge i); try discriminate.
-    apply (Genv.find_funct_ptr_prop wt_fundef wt_p H).
+    apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H).
   econstructor; eauto.
   intros. elim H0; intro. subst s0. econstructor; eauto with coqlib.
   auto.
 
   assert (WTFD: wt_fundef f').
     destruct ros; simpl in H.
-    apply (Genv.find_funct_prop wt_fundef wt_p H).
+    apply (Genv.find_funct_prop wt_fundef _ _ wt_p H).
     destruct (Genv.find_symbol ge i); try discriminate.
-    apply (Genv.find_funct_ptr_prop wt_fundef wt_p H).
+    apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H).
   econstructor; eauto.
 
 (*  apply wt_setreg; auto. exact I.  *)
@@ -293,7 +285,7 @@ Proof.
   apply wt_empty_frame.
 
   econstructor; eauto. apply wt_setreg; auto.
-  generalize (wt_event_match _ _ _ _ H). 
+  generalize (external_call_well_typed _ _ _ _ _ _ H).  
   unfold proj_sig_res, Conventions.loc_result.
   destruct (sig_res (ef_sig ef)).
   destruct t0; simpl; auto.
diff --git a/backend/RTL.v b/backend/RTL.v
index b2ee80fc..c5d4d7d0 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -22,7 +22,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Events.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Op.
@@ -115,7 +115,7 @@ Definition funsig (fd: fundef) :=
 
 (** * Operational semantics *)
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 Definition regset := Regmap.t val.
 
 Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
@@ -128,8 +128,8 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   set of transitions between states.  A state captures the current
   point in the execution.  Three kinds of states appear in the transitions:
 
-- [State cs c sp pc rs m] describes an execution point within a function.
-  [c] is the code for the current function (a CFG).
+- [State cs f sp pc rs m] describes an execution point within a function.
+  [f] is the current function.
   [sp] is the pointer to the stack block for its current activation
      (as in Cminor).
   [pc] is the current program point (CFG node) within the code [c].
@@ -145,10 +145,10 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   [v] is the return value and [m] the current memory state.
 
 In all three kinds of states, the [cs] parameter represents the call stack.
-It is a list of frames [Stackframe res c sp pc rs].  Each frame represents
+It is a list of frames [Stackframe res f sp pc rs].  Each frame represents
 a function call in progress.  
 [res] is the pseudo-register that will receive the result of the call.
-[c] is the code of the calling function.
+[f] is the calling function.
 [sp] is its stack pointer.
 [pc] is the program point for the instruction that follows the call.
 [rs] is the state of registers in the calling function.
@@ -157,7 +157,7 @@ a function call in progress.
 Inductive stackframe : Type :=
   | Stackframe:
       forall (res: reg)            (**r where to store the result *)
-             (c: code)             (**r code of calling function *)
+             (f: function)         (**r calling function *)
              (sp: val)             (**r stack pointer in calling function *)
              (pc: node)            (**r program point in calling function *)
              (rs: regset),         (**r register state in calling function *)
@@ -166,7 +166,7 @@ Inductive stackframe : Type :=
 Inductive state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
-             (c: code)                (**r current code *)
+             (f: function)            (**r current function *)
              (sp: val)                (**r stack pointer *)
              (pc: node)               (**r current program point in [c] *)
              (rs: regset)             (**r register state *)
@@ -206,107 +206,109 @@ Definition find_function
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_Inop:
-      forall s c sp pc rs m pc',
-      c!pc = Some(Inop pc') ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp pc' rs m)
+      forall s f sp pc rs m pc',
+      (fn_code f)!pc = Some(Inop pc') ->
+      step (State s f sp pc rs m)
+        E0 (State s f sp pc' rs m)
   | exec_Iop:
-      forall s c sp pc rs m op args res pc' v,
-      c!pc = Some(Iop op args res pc') ->
+      forall s f sp pc rs m op args res pc' v,
+      (fn_code f)!pc = Some(Iop op args res pc') ->
       eval_operation ge sp op rs##args = Some v ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp pc' (rs#res <- v) m)
+      step (State s f sp pc rs m)
+        E0 (State s f sp pc' (rs#res <- v) m)
   | exec_Iload:
-      forall s c sp pc rs m chunk addr args dst pc' a v,
-      c!pc = Some(Iload chunk addr args dst pc') ->
+      forall s f sp pc rs m chunk addr args dst pc' a v,
+      (fn_code f)!pc = Some(Iload chunk addr args dst pc') ->
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = Some v ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp pc' (rs#dst <- v) m)
+      step (State s f sp pc rs m)
+        E0 (State s f sp pc' (rs#dst <- v) m)
   | exec_Istore:
-      forall s c sp pc rs m chunk addr args src pc' a m',
-      c!pc = Some(Istore chunk addr args src pc') ->
+      forall s f sp pc rs m chunk addr args src pc' a m',
+      (fn_code f)!pc = Some(Istore chunk addr args src pc') ->
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.storev chunk m a rs#src = Some m' ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp pc' rs m')
+      step (State s f sp pc rs m)
+        E0 (State s f sp pc' rs m')
   | exec_Icall:
-      forall s c sp pc rs m sig ros args res pc' f,
-      c!pc = Some(Icall sig ros args res pc') ->
-      find_function ros rs = Some f ->
-      funsig f = sig ->
-      step (State s c sp pc rs m)
-        E0 (Callstate (Stackframe res c sp pc' rs :: s) f rs##args m)
+      forall s f sp pc rs m sig ros args res pc' fd,
+      (fn_code f)!pc = Some(Icall sig ros args res pc') ->
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      step (State s f sp pc rs m)
+        E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
   | exec_Itailcall:
-      forall s c stk pc rs m sig ros args f,
-      c!pc = Some(Itailcall sig ros args) ->
-      find_function ros rs = Some f ->
-      funsig f = sig ->
-      step (State s c (Vptr stk Int.zero) pc rs m)
-        E0 (Callstate s f rs##args (Mem.free m stk))
+      forall s f stk pc rs m sig ros args fd m',
+      (fn_code f)!pc = Some(Itailcall sig ros args) ->
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (State s f (Vptr stk Int.zero) pc rs m)
+        E0 (Callstate s fd rs##args m')
   | exec_Icond_true:
-      forall s c sp pc rs m cond args ifso ifnot,
-      c!pc = Some(Icond cond args ifso ifnot) ->
+      forall s f sp pc rs m cond args ifso ifnot,
+      (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
       eval_condition cond rs##args = Some true ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp ifso rs m)
+      step (State s f sp pc rs m)
+        E0 (State s f sp ifso rs m)
   | exec_Icond_false:
-      forall s c sp pc rs m cond args ifso ifnot,
-      c!pc = Some(Icond cond args ifso ifnot) ->
+      forall s f sp pc rs m cond args ifso ifnot,
+      (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
       eval_condition cond rs##args = Some false ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp ifnot rs m)
+      step (State s f sp pc rs m)
+        E0 (State s f sp ifnot rs m)
   | exec_Ijumptable:
-      forall s c sp pc rs m arg tbl n pc',
-      c!pc = Some(Ijumptable arg tbl) ->
+      forall s f sp pc rs m arg tbl n pc',
+      (fn_code f)!pc = Some(Ijumptable arg tbl) ->
       rs#arg = Vint n ->
       list_nth_z tbl (Int.signed n) = Some pc' ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp pc' rs m)
+      step (State s f sp pc rs m)
+        E0 (State s f sp pc' rs m)
   | exec_Ireturn:
-      forall s c stk pc rs m or,
-      c!pc = Some(Ireturn or) ->
-      step (State s c (Vptr stk Int.zero) pc rs m)
-        E0 (Returnstate s (regmap_optget or Vundef rs) (Mem.free m stk))
+      forall s f stk pc rs m or m',
+      (fn_code f)!pc = Some(Ireturn or) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (State s f (Vptr stk Int.zero) pc rs m)
+        E0 (Returnstate s (regmap_optget or Vundef rs) m')
   | exec_function_internal:
       forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
       step (Callstate s (Internal f) args m)
         E0 (State s
-                  f.(fn_code)
+                  f
                   (Vptr stk Int.zero)
                   f.(fn_entrypoint)
                   (init_regs args f.(fn_params))
                   m')
   | exec_function_external:
-      forall s ef args res t m,
-      event_match ef args t res ->
+      forall s ef args res t m m',
+      external_call ef args m t res m' ->
       step (Callstate s (External ef) args m)
-         t (Returnstate s res m)
+         t (Returnstate s res m')
   | exec_return:
-      forall res c sp pc rs s vres m,
-      step (Returnstate (Stackframe res c sp pc rs :: s) vres m)
-        E0 (State s c sp pc (rs#res <- vres) m).
+      forall res f sp pc rs s vres m,
+      step (Returnstate (Stackframe res f sp pc rs :: s) vres m)
+        E0 (State s f sp pc (rs#res <- vres) m).
 
 Lemma exec_Iop':
-  forall s c sp pc rs m op args res pc' rs' v,
-  c!pc = Some(Iop op args res pc') ->
+  forall s f sp pc rs m op args res pc' rs' v,
+  (fn_code f)!pc = Some(Iop op args res pc') ->
   eval_operation ge sp op rs##args = Some v ->
   rs' = (rs#res <- v) ->
-  step (State s c sp pc rs m)
-    E0 (State s c sp pc' rs' m).
+  step (State s f sp pc rs m)
+    E0 (State s f sp pc' rs' m).
 Proof.
   intros. subst rs'. eapply exec_Iop; eauto.
 Qed.
 
 Lemma exec_Iload':
-  forall s c sp pc rs m chunk addr args dst pc' rs' a v,
-  c!pc = Some(Iload chunk addr args dst pc') ->
+  forall s f sp pc rs m chunk addr args dst pc' rs' a v,
+  (fn_code f)!pc = Some(Iload chunk addr args dst pc') ->
   eval_addressing ge sp addr rs##args = Some a ->
   Mem.loadv chunk m a = Some v ->
   rs' = (rs#dst <- v) ->
-  step (State s c sp pc rs m)
-    E0 (State s c sp pc' rs' m).
+  step (State s f sp pc rs m)
+    E0 (State s f sp pc' rs' m).
 Proof.
   intros. subst rs'. eapply exec_Iload; eauto.
 Qed.
@@ -319,9 +321,9 @@ End RELSEM.
   without arguments and with an empty call stack. *)
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index d07bd081..f4d1342a 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Smallstep.
 Require Import Globalenvs.
@@ -337,7 +337,7 @@ Lemma function_ptr_translated:
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
 Proof
-  (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL).
+  (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).
 
 Lemma functions_translated:
   forall (v: val) (f: CminorSel.fundef),
@@ -345,7 +345,7 @@ Lemma functions_translated:
   exists tf,
   Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
 Proof
-  (Genv.find_funct_transf_partial transl_fundef TRANSL).
+  (Genv.find_funct_transf_partial transl_fundef _ TRANSL).
 
 Lemma sig_transl_function:
   forall (f: CminorSel.fundef) (tf: RTL.fundef),
@@ -365,10 +365,10 @@ Qed.
 (** Correctness of the code generated by [add_move]. *)
 
 Lemma tr_move_correct:
-  forall r1 ns r2 nd cs code sp rs m,
-  tr_move code ns r1 nd r2 ->
+  forall r1 ns r2 nd cs f sp rs m,
+  tr_move f.(fn_code) ns r1 nd r2 ->
   exists rs',
-  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\
+  star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\
   rs'#r2 = rs#r1 /\
   (forall r, r <> r2 -> rs'#r = rs#r).
 Proof.
@@ -382,13 +382,13 @@ Qed.
 (** Correctness of the code generated by [store_var] and [store_optvar]. *)
 
 Lemma tr_store_var_correct:
-  forall rs cs code map r id ns nd e sp m,
-  tr_store_var code map r id ns nd ->
+  forall rs cs f map r id ns nd e sp m,
+  tr_store_var f.(fn_code) map r id ns nd ->
   map_wf map ->
   match_env map e nil rs ->
   exists rs',
-     star step tge (State cs code sp ns rs m)
-                E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m)
+                E0 (State cs f sp nd rs' m)
   /\ match_env map (PTree.set id rs#r e) nil rs'.
 Proof.
   intros. destruct H as [rv [A B]].
@@ -402,13 +402,13 @@ Proof.
 Qed.
 
 Lemma tr_store_optvar_correct:
-  forall rs cs code map r optid ns nd e sp m,
-  tr_store_optvar code map r optid ns nd ->
+  forall rs cs f map r optid ns nd e sp m,
+  tr_store_optvar f.(fn_code) map r optid ns nd ->
   map_wf map ->
   match_env map e nil rs ->
   exists rs',
-     star step tge (State cs code sp ns rs m)
-                E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m)
+                E0 (State cs f sp nd rs' m)
   /\ match_env map (set_optvar optid rs#r e) nil rs'.
 Proof.
   intros. destruct optid; simpl in *.
@@ -419,15 +419,15 @@ Qed.
 (** Correctness of the translation of [switch] statements *)
 
 Lemma transl_switch_correct:
-  forall cs sp e m code map r nexits t ns,
-  tr_switch code map r nexits t ns ->
+  forall cs sp e m f map r nexits t ns,
+  tr_switch f.(fn_code) map r nexits t ns ->
   forall rs i act,
   rs#r = Vint i ->
   map_wf map ->
   match_env map e nil rs ->
   comptree_match i t = Some act ->
   exists nd, exists rs',
-  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\
+  star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\
   nth_error nexits act = Some nd /\
   match_env map e nil rs'.
 Proof.
@@ -458,7 +458,7 @@ Proof.
   set (rs1 := rs#rt <- (Vint(Int.sub i ofs))).
   assert (ME1: match_env map e nil rs1).
     unfold rs1. eauto with rtlg.
-  assert (EX1: step tge (State cs code sp n rs m) E0 (State cs code sp n1 rs1 m)).
+  assert (EX1: step tge (State cs f sp n rs m) E0 (State cs f sp n1 rs1 m)).
     eapply exec_Iop; eauto. 
     predSpec Int.eq Int.eq_spec ofs Int.zero; simpl.
     rewrite H10. rewrite Int.sub_zero_l. congruence.
@@ -521,12 +521,12 @@ Variable m: mem.
 
 Definition transl_expr_prop 
      (le: letenv) (a: expr) (v: val) : Prop :=
-  forall cs code map pr ns nd rd rs
+  forall cs f map pr ns nd rd rs
     (MWF: map_wf map)
-    (TE: tr_expr code map pr a ns nd rd)
+    (TE: tr_expr f.(fn_code) map pr a ns nd rd)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m)
   /\ match_env map e le rs'
   /\ rs'#rd = v
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
@@ -536,25 +536,25 @@ Definition transl_expr_prop
 
 Definition transl_exprlist_prop 
      (le: letenv) (al: exprlist) (vl: list val) : Prop :=
-  forall cs code map pr ns nd rl rs
+  forall cs f map pr ns nd rl rs
     (MWF: map_wf map)
-    (TE: tr_exprlist code map pr al ns nd rl)
+    (TE: tr_exprlist f.(fn_code) map pr al ns nd rl)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m)
   /\ match_env map e le rs'
   /\ rs'##rl = vl
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
 
 Definition transl_condition_prop 
      (le: letenv) (a: condexpr) (vb: bool) : Prop :=
-  forall cs code map pr ns ntrue nfalse rs
+  forall cs f map pr ns ntrue nfalse rs
     (MWF: map_wf map)
-    (TE: tr_condition code map pr a ns ntrue nfalse)
+    (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) E0
-                   (State cs code sp (if vb then ntrue else nfalse) rs' m)
+     star step tge (State cs f sp ns rs m) E0
+                   (State cs f sp (if vb then ntrue else nfalse) rs' m)
   /\ match_env map e le rs'
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
 
@@ -604,7 +604,7 @@ Proof.
   split. eapply star_right. eexact EX1.
   eapply exec_Iop; eauto.  
   subst vargs.
-  rewrite (@eval_operation_preserved CminorSel.fundef RTL.fundef ge tge). 
+  rewrite (@eval_operation_preserved CminorSel.fundef _ _ _ ge tge). 
   auto. 
   exact symbols_preserved. traceEq.
 (* Match-env *)
@@ -621,7 +621,7 @@ Lemma transl_expr_Eload_correct:
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
   Op.eval_addressing ge sp addr vargs = Some vaddr ->
-  loadv chunk m vaddr = Some v ->
+  Mem.loadv chunk m vaddr = Some v ->
   transl_expr_prop le (Eload chunk addr args) v.
 Proof.
   intros; red; intros. inv TE.
@@ -629,7 +629,7 @@ Proof.
   exists (rs1#rd <- v).
 (* Exec *)
   split. eapply star_right. eexact EX1. eapply exec_Iload; eauto.
-  rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge).
+  rewrite RES1. rewrite (@eval_addressing_preserved _ _ _ _ ge tge).
   exact H1. exact symbols_preserved. traceEq.
 (* Match-env *)
   split. eauto with rtlg. 
@@ -650,7 +650,7 @@ Lemma transl_expr_Econdition_correct:
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_expr code map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd).
+  assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd).
     destruct vcond; auto.
   exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
   exists rs2.
@@ -767,7 +767,7 @@ Lemma transl_condition_CEcondition_correct:
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_condition code map pr (if vcond then ifso else ifnot)
+  assert (tr_condition f.(fn_code) map pr (if vcond then ifso else ifnot)
              (if vcond then ntrue' else nfalse') ntrue nfalse).
     destruct vcond; auto.
   exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]].
@@ -977,12 +977,13 @@ Qed.
 
 *)
 
-Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function)
+Inductive tr_fun (tf: function) (map: mapping) (f: CminorSel.function)
                      (ngoto: labelmap) (nret: node) (rret: option reg) : Prop :=
-  | tr_funbody_intro: forall nentry r,
+  | tr_fun_intro: forall nentry r,
       rret = ret_reg f.(CminorSel.fn_sig) r ->
-      tr_stmt c map f.(fn_body) nentry nret nil ngoto nret rret ->
-      tr_funbody c map f ngoto nret rret.
+      tr_stmt tf.(fn_code) map f.(fn_body) nentry nret nil ngoto nret rret ->
+      tf.(fn_stacksize) = f.(fn_stackspace) ->
+      tr_fun tf map f ngoto nret rret.
 
 Inductive tr_cont: RTL.code -> mapping -> 
                    CminorSel.cont -> node -> list node -> labelmap -> node -> option reg ->
@@ -1006,25 +1007,25 @@ Inductive tr_cont: RTL.code -> mapping ->
 with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop :=
   | match_stacks_stop:
       match_stacks Kstop nil
-  | match_stacks_call: forall optid f sp e k r c n rs cs map nexits ngoto nret rret n',
+  | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret n',
       map_wf map ->
-      tr_funbody c map f ngoto nret rret ->
+      tr_fun tf map f ngoto nret rret ->
       match_env map e nil rs ->
-      tr_store_optvar c map r optid n n' ->
+      tr_store_optvar tf.(fn_code) map r optid n n' ->
       ~reg_in_map map r ->
-      tr_cont c map k n' nexits ngoto nret rret cs ->
-      match_stacks (Kcall optid f sp e k) (Stackframe r c sp n rs :: cs).
+      tr_cont tf.(fn_code) map k n' nexits ngoto nret rret cs ->
+      match_stacks (Kcall optid f sp e k) (Stackframe r tf sp n rs :: cs).
 
 Inductive match_states: CminorSel.state -> RTL.state -> Prop :=
   | match_state:
-      forall f s k sp e m cs c ns rs map ncont nexits ngoto nret rret
+      forall f s k sp e m cs tf ns rs map ncont nexits ngoto nret rret
         (MWF: map_wf map)
-        (TS: tr_stmt c map s ns ncont nexits ngoto nret rret)
-        (TF: tr_funbody c map f ngoto nret rret)
-        (TK: tr_cont c map k ncont nexits ngoto nret rret cs)
+        (TS: tr_stmt tf.(fn_code) map s ns ncont nexits ngoto nret rret)
+        (TF: tr_fun tf map f ngoto nret rret)
+        (TK: tr_cont tf.(fn_code) map k ncont nexits ngoto nret rret cs)
         (ME: match_env map e nil rs),
       match_states (CminorSel.State f s k sp e m)
-                   (RTL.State cs c sp ns rs m)
+                   (RTL.State cs tf sp ns rs m)
   | match_callstate:
       forall f args k m cs tf
         (TF: transl_fundef f = OK tf)
@@ -1109,15 +1110,19 @@ Proof.
 
   (* skip return *)
   inv TS. 
-  assert (c!ncont = Some(Ireturn rret) /\ match_stacks k cs).
-    inv TK; simpl in H; try contradiction; auto.
-  destruct H1.
+  assert ((fn_code tf)!ncont = Some(Ireturn rret)
+          /\ match_stacks k cs).
+    inv TK; simpl in H; try contradiction; auto. 
+  destruct H2.
   assert (rret = None). 
     inv TF. unfold ret_reg. rewrite H0. auto.
+  assert (fn_stacksize tf = fn_stackspace f).
+    inv TF. auto. 
   subst rret.
   econstructor; split.
   left; apply plus_one. eapply exec_Ireturn. eauto.
-  simpl. constructor; auto.
+  rewrite H5. eauto. 
+  constructor; auto.
   
   (* assign *)
   inv TS. 
@@ -1152,7 +1157,7 @@ Proof.
   intros [rs' [A [B [C D]]]].
   exploit transl_exprlist_correct; eauto.
   intros [rs'' [E [F [G J]]]].
-  exploit functions_translated; eauto. intros [tf [P Q]].
+  exploit functions_translated; eauto. intros [tf' [P Q]].
   econstructor; split.
   left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
   eapply exec_Icall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto.
@@ -1166,12 +1171,14 @@ Proof.
   intros [rs' [A [B [C D]]]].
   exploit transl_exprlist_correct; eauto.
   intros [rs'' [E [F [G J]]]].
-  exploit functions_translated; eauto. intros [tf [P Q]].
+  exploit functions_translated; eauto. intros [tf' [P Q]].
   exploit match_stacks_call_cont; eauto. intros [U V].
+  assert (fn_stacksize tf = fn_stackspace f). inv TF; auto.
   econstructor; split.
   left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
   eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto.
   apply sig_transl_function; auto.
+  rewrite H2; eauto.
   traceEq.
   rewrite G. constructor; auto.
   (* seq *)
@@ -1234,17 +1241,21 @@ Proof.
   (* return none *)
   inv TS.
   exploit match_stacks_call_cont; eauto. intros [U V].
+  inversion TF.
   econstructor; split.
   left; apply plus_one. eapply exec_Ireturn; eauto.
-  simpl. constructor; auto.
+  rewrite H2; eauto.
+  constructor; auto.
 
   (* return some *)
   inv TS.
   exploit transl_expr_correct; eauto.
   intros [rs' [A [B [C D]]]].
-  exploit match_stacks_call_cont; eauto. intros [U V].  
+  exploit match_stacks_call_cont; eauto. intros [U V].
+  inversion TF.
   econstructor; split.
-  left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. traceEq.
+  left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto.
+  rewrite H4; eauto. traceEq.
   simpl. rewrite C. constructor; auto.
 
   (* label *)
@@ -1301,11 +1312,12 @@ Proof.
   induction 1.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   econstructor; split.
-  econstructor. rewrite (transform_partial_program_main _ _ TRANSL). fold tge.
-  rewrite symbols_preserved. eexact H.
+  econstructor. apply (Genv.init_mem_transf_partial _ _ TRANSL); eauto.
+  rewrite (transform_partial_program_main _ _ TRANSL). fold tge.
+  rewrite symbols_preserved. eauto.
   eexact A.
-  rewrite <- H1. apply sig_transl_function; auto.
-  rewrite (Genv.init_mem_transf_partial _ _ TRANSL). constructor. auto. constructor.
+  rewrite <- H2. apply sig_transl_function; auto.
+  constructor. auto. constructor.
 Qed.
 
 Lemma transl_final_states:
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 037eb3fb..51fb945e 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -27,7 +27,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Events.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Switch.
 Require Import Op.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index d8e2f212..68f38c0d 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -20,7 +20,7 @@ Require Import Op.
 Require Import Registers.
 Require Import Globalenvs.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Integers.
 Require Import Events.
 Require Import Smallstep.
@@ -454,14 +454,6 @@ Proof.
   apply wt_regset_assign; auto.
 Qed.
 
-Lemma wt_event_match:
-  forall ef args t res,
-  event_match ef args t res ->
-  Val.has_type res (proj_sig_res ef.(ef_sig)).
-Proof.
-  induction 1. inversion H0; exact I.
-Qed.
-
 Inductive wt_stackframes: list stackframe -> option typ -> Prop :=
   | wt_stackframes_nil:
       wt_stackframes nil (Some Tint)
@@ -471,7 +463,7 @@ Inductive wt_stackframes: list stackframe -> option typ -> Prop :=
       wt_regset env rs ->
       env res = match tyres with None => Tint | Some t => t end ->
       wt_stackframes s (sig_res (fn_sig f)) ->
-      wt_stackframes (Stackframe res (fn_code f) sp pc rs :: s) tyres.
+      wt_stackframes (Stackframe res f sp pc rs :: s) tyres.
 
 Inductive wt_state: state -> Prop :=
   | wt_state_intro:
@@ -479,7 +471,7 @@ Inductive wt_state: state -> Prop :=
         (WT_STK: wt_stackframes s (sig_res (fn_sig f)))
         (WT_FN: wt_function f env)
         (WT_RS: wt_regset env rs),
-      wt_state (State s (fn_code f) sp pc rs m)
+      wt_state (State s f sp pc rs m)
   | wt_state_call:
       forall s f args m,
       wt_stackframes s (sig_res (funsig f)) ->
@@ -517,7 +509,7 @@ Proof.
   econstructor; eauto.
   apply wt_regset_assign. auto.
   replace (env res) with (snd (type_of_operation op)).
-  apply type_of_operation_sound with fundef ge rs##args sp; auto.
+  apply type_of_operation_sound with fundef unit ge rs##args sp; auto.
   rewrite <- H6. reflexivity.
   (* Iload *)
   econstructor; eauto.
@@ -526,29 +518,29 @@ Proof.
   (* Istore *)
   econstructor; eauto.
   (* Icall *)
-  assert (wt_fundef f).
+  assert (wt_fundef fd).
     destruct ros; simpl in H0.
-    pattern f. apply Genv.find_funct_prop with fundef unit p (rs#r).
+    pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r).
     exact wt_p. exact H0. 
     caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0.
-    pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b.
+    pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b.
     exact wt_p. exact H0.
     discriminate.
   econstructor; eauto.
   econstructor; eauto.
   rewrite <- H7. apply wt_regset_list. auto.
   (* Itailcall *)
-  assert (wt_fundef f).
+  assert (wt_fundef fd).
     destruct ros; simpl in H0.
-    pattern f. apply Genv.find_funct_prop with fundef unit p (rs#r).
+    pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r).
     exact wt_p. exact H0. 
     caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0.
-    pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b.
+    pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b.
     exact wt_p. exact H0.
     discriminate.
   econstructor; eauto.
-  rewrite H5; auto.
-  rewrite <- H6. apply wt_regset_list. auto.
+  rewrite H6; auto.
+  rewrite <- H7. apply wt_regset_list. auto.
   (* Icond *)
   econstructor; eauto.
   econstructor; eauto.
@@ -557,7 +549,7 @@ Proof.
   (* Ireturn *)
   econstructor; eauto. 
   destruct or; simpl in *.
-  rewrite <- H1. apply WT_RS. exact I.
+  rewrite <- H2. apply WT_RS. exact I.
   (* internal function *)
   simpl in *. inv H5. inversion H1; subst.  
   econstructor; eauto.
@@ -566,7 +558,7 @@ Proof.
   simpl in *. inv H5. 
   econstructor; eauto. 
   change (Val.has_type res (proj_sig_res (ef_sig ef))).
-  eapply wt_event_match; eauto.
+  eapply external_call_well_typed; eauto.
   (* return *)
   inv H1. econstructor; eauto. 
   apply wt_regset_assign; auto. congruence. 
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 406ca07a..868fb8df 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -16,6 +16,7 @@ open Datatypes
 open Camlcoq
 open Maps
 open AST
+open Memdata
 open Op
 open Registers
 open RTL
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 21d5f380..7d730118 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -875,7 +875,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop :=
         (AG: agree rs ls)
         (WT: wt_function f)
         (TL: is_tail c (LTLin.fn_code f))
-        (MMD: Mem.lessdef m tm),
+        (MMD: Mem.extends m tm),
       match_states (LTLin.State s f sp c rs m)
                    (Linear.State s' (transf_function f) sp (transf_code f c) ls tm)
   | match_states_call:
@@ -885,7 +885,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop :=
         (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
                  ls l = parent_locset s' l)
         (WT: wt_fundef f)
-        (MMD: Mem.lessdef m tm),
+        (MMD: Mem.extends m tm),
       match_states (LTLin.Callstate s f args m)
                    (Linear.Callstate s' (transf_fundef f) ls tm)
   | match_states_return:
@@ -894,7 +894,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop :=
         (AG: Val.lessdef res (ls (R (Conventions.loc_result sig))))
         (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
                  ls l = parent_locset s' l)
-        (MMD: Mem.lessdef m tm),
+        (MMD: Mem.extends m tm),
       match_states (LTLin.Returnstate s res m)
                    (Linear.Returnstate s' ls tm).
 
@@ -1006,8 +1006,7 @@ Proof.
     rewrite B. eapply agree_locs; eauto. 
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
   destruct H1 as [ta [P Q]].
-  exploit Mem.loadv_lessdef; eauto. 
-  intros [tv [R S]].
+  exploit Mem.loadv_extends; eauto. intros [tv [R S]].
   exploit add_spill_correct.
   intros [ls3 [D [E F]]].
   left; econstructor; split.
@@ -1038,7 +1037,7 @@ Proof.
   destruct H1 as [ta [P Q]].
   assert (X: Val.lessdef (rs src) (ls2 (R rsrc))).
     rewrite E. eapply agree_loc; eauto.
-  exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. 
+  exploit Mem.storev_extends. eexact MMD. eauto. eexact Q. eexact X. 
   intros [tm2 [Y Z]].
   left; econstructor; split. 
   eapply plus_right. eauto. 
@@ -1072,7 +1071,7 @@ Proof.
     eapply agree_exten; eauto. 
     apply Loc.diff_sym. apply loc_acceptable_noteq_diff. auto. 
     red; intros; subst src. simpl in H8. intuition congruence.
-  exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. 
+  exploit Mem.storev_extends. eexact MMD. eauto. eexact Q. eexact X.
   intros [tm2 [Y Z]].
   left; econstructor; split.
   eapply star_plus_trans. eauto. 
@@ -1157,15 +1156,16 @@ Proof.
   ExploitWT. inversion WTI. subst ros0 args0.
   assert (WTF': wt_fundef f'). eapply find_function_wt; eauto.
   rewrite <- H0.
+  exploit Mem.free_parallel_extends; eauto. intros [tm' [FREE MMD']].
   destruct ros as [fn | id].
   (* indirect call *)
-  red in H4. destruct H4 as [OK1 [OK2 OK3]].
-  rewrite <- H0 in H3. rewrite <- H0 in OK3.
+  red in H5. destruct H5 as [OK1 [OK2 OK3]].
+  rewrite <- H0 in H4. rewrite <- H0 in OK3.
   destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
               args sig
               (add_reload fn IT1
                 (Ltailcall sig (inl ident IT1) :: transf_code f b))
-              ls tm H3 H5)
+              ls tm H4 H6)
   as [ls2 [A [B C]]].
   destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT1
              (Ltailcall sig (inl ident IT1) :: transf_code f b)
@@ -1191,13 +1191,12 @@ Proof.
   eapply match_stackframes_change_sig; eauto.
   rewrite return_regs_arguments; auto. congruence.
   exact (return_regs_preserve (parent_locset s') ls3).
-  apply Mem.free_lessdef; auto. 
   (* direct call *)
-  rewrite <- H0 in H3.
+  rewrite <- H0 in H4.
   destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
               args sig
               (Ltailcall sig (inr mreg id) :: transf_code f b)
-              ls tm H3 H5)
+              ls tm H4 H6)
   as [ls3 [D [E F]]].
   assert (ARGS: Val.lessdef_list (map rs args) 
                                  (map ls3 (loc_arguments sig))).
@@ -1214,7 +1213,6 @@ Proof.
   eapply match_stackframes_change_sig; eauto.
   rewrite return_regs_arguments; auto. congruence.
   exact (return_regs_preserve (parent_locset s') ls3).
-  apply Mem.free_lessdef; auto. 
 
   (* Llabel *)
   left; econstructor; split.
@@ -1272,29 +1270,29 @@ Proof.
   eapply LTLin.find_label_is_tail; eauto.
 
   (* Lreturn *)
-  ExploitWT; inv WTI. 
+  ExploitWT; inv WTI.
+  exploit Mem.free_parallel_extends; eauto. intros [tm' [FREE MMD']]. 
   destruct or; simpl.
   (* with an argument *)
   exploit add_reload_correct.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
-  eapply plus_right. eauto. eapply exec_Lreturn; eauto. 
+  eapply plus_right. eauto. eapply exec_Lreturn; eauto.
   traceEq.
   econstructor; eauto.
   rewrite return_regs_result. rewrite B. apply agree_loc; auto.
   apply return_regs_preserve.
-  apply Mem.free_lessdef; auto.
   (* without an argument *)
   left; econstructor; split.
   apply plus_one. eapply exec_Lreturn; eauto.  
   econstructor; eauto.
   apply return_regs_preserve.
-  apply Mem.free_lessdef; auto.
 
   (* internal function *)
   simpl in WT. inversion_clear WT. inversion H0. simpl in AG.
-  caseEq (alloc tm 0 (LTLin.fn_stacksize f)). intros tm' tstk TALLOC.
-  exploit Mem.alloc_lessdef; eauto. intros [P Q]. subst tstk.
+  exploit Mem.alloc_extends. eauto. eauto. 
+  instantiate (1 := 0); omega. instantiate (1 := LTLin.fn_stacksize f); omega.
+  intros [tm' [ALLOC MMD']].
   destruct (parallel_move_parameters_correct tge s' (transf_function f)
                (Vptr stk Int.zero) (LTLin.fn_params f) (LTLin.fn_sig f)
                (transf_code f (LTLin.fn_code f)) (call_regs ls) tm'
@@ -1310,8 +1308,8 @@ Proof.
   econstructor; eauto with coqlib.
 
   (* external function *)
-  exploit event_match_lessdef; eauto. 
-  intros [res' [A B]]. 
+  exploit external_call_mem_extends; eauto.
+  intros [res' [tm' [A [B [C D]]]]]. 
   left; econstructor; split.
   apply plus_one. eapply exec_function_external; eauto. 
   econstructor; eauto.
@@ -1338,16 +1336,15 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   econstructor; split.
-  econstructor. 
-  change (prog_main tprog) with (prog_main prog). 
+  econstructor.
+  apply Genv.init_mem_transf; eauto.
   rewrite symbols_preserved. eauto.
   apply function_ptr_translated; eauto. 
   rewrite sig_preserved. auto.
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).  
-  econstructor; eauto. constructor. rewrite H2; auto.
-  rewrite H2. simpl. constructor.
+  econstructor; eauto. constructor. rewrite H3; auto.
+  rewrite H3. simpl. constructor.
   eapply Genv.find_funct_ptr_prop; eauto.
-  apply Mem.lessdef_refl. symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto.
+  apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/Selection.v b/backend/Selection.v
index 4355faf5..e822fdf7 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -28,7 +28,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Cminor.
 Require Import Op.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 70cbeb41..1da7884e 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -18,7 +18,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -300,7 +300,7 @@ Lemma functions_translated:
   Genv.find_funct tge v = Some (sel_fundef f).
 Proof.  
   intros.
-  exact (Genv.find_funct_transf sel_fundef H).
+  exact (Genv.find_funct_transf sel_fundef _ _ H).
 Qed.
 
 Lemma function_ptr_translated:
@@ -309,7 +309,7 @@ Lemma function_ptr_translated:
   Genv.find_funct_ptr tge b = Some (sel_fundef f).
 Proof.  
   intros. 
-  exact (Genv.find_funct_ptr_transf sel_fundef H).
+  exact (Genv.find_funct_ptr_transf sel_fundef _ _ H).
 Qed.
 
 Lemma sig_function_translated:
@@ -428,6 +428,7 @@ Proof.
   econstructor; split. 
   econstructor. destruct k; simpl in H; simpl; auto. 
   rewrite <- H0; reflexivity.
+  simpl. eauto. 
   constructor; auto.
 (*
   (* assign *)
@@ -457,11 +458,11 @@ Proof.
   constructor; auto. destruct b; auto.
   (* Sreturn None *)
   econstructor; split. 
-  econstructor.
+  econstructor. simpl; eauto. 
   constructor; auto. apply call_cont_commut.
   (* Sreturn Some *)
   econstructor; split. 
-  econstructor. simpl. eauto with evalexpr. 
+  econstructor. simpl. eauto with evalexpr. simpl; eauto.
   constructor; auto. apply call_cont_commut.
   (* Sgoto *)
   econstructor; split.
@@ -477,10 +478,10 @@ Proof.
   induction 1.
   econstructor; split.
   econstructor.
-  simpl. fold tge. rewrite symbols_preserved. eexact H.
+  apply Genv.init_mem_transf; eauto.
+  simpl. fold tge. rewrite symbols_preserved. eexact H0.
   apply function_ptr_translated. eauto. 
-  rewrite <- H1. apply sig_function_translated; auto.
-  unfold tprog, sel_program. rewrite Genv.init_mem_transf.
+  rewrite <- H2. apply sig_function_translated; auto.
   constructor; auto.
 Qed.
 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index ba429589..f44eac2e 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -27,7 +27,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Op.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -1145,7 +1145,7 @@ Lemma functions_translated:
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
 Proof
-  (Genv.find_funct_transf_partial transf_fundef TRANSF).
+  (Genv.find_funct_transf_partial transf_fundef _ TRANSF).
 
 Lemma function_ptr_translated:
   forall v f,
@@ -1153,7 +1153,7 @@ Lemma function_ptr_translated:
   exists tf,
   Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
 Proof
-  (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
+  (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
 
 Lemma sig_preserved:
   forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f.
@@ -1166,6 +1166,15 @@ Proof.
   intro. inversion H. reflexivity.
 Qed.
 
+Lemma stacksize_preserved:
+  forall f tf, transf_function f = OK tf -> Mach.fn_stacksize tf = Linear.fn_stacksize f.
+Proof.
+  intros until tf; unfold transf_function. 
+  destruct (zlt (Linear.fn_stacksize f) 0). simpl; congruence.
+  destruct (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). simpl; congruence.
+  intros. inversion H; reflexivity. 
+Qed.
+
 Lemma find_function_translated:
   forall f0 tf0 ls ls0 rs fr cs ros f,
   agree f0 tf0 ls ls0 rs fr cs ->
@@ -1478,10 +1487,12 @@ Proof.
     simpl. intuition congruence. simpl. intuition congruence. 
   econstructor; split.
   eapply plus_right. eexact A. 
-  simpl shift_sp. eapply exec_Mtailcall; eauto. traceEq.
+  simpl shift_sp. eapply exec_Mtailcall; eauto.
+  rewrite (stacksize_preserved _ _ TRANSL); eauto.
+  traceEq.
   econstructor; eauto. 
   intros; symmetry; eapply agree_return_regs; eauto.
-  intros. inv WTI. generalize (H3 _ H0). tauto.
+  intros. inv WTI. generalize (H4 _ H0). tauto.
   apply agree_callee_save_return_regs. 
  
   (* Llabel *)
@@ -1524,7 +1535,9 @@ Proof.
   intros [ls' [A [B C]]].
   econstructor; split.
   eapply plus_right. eauto. 
-  simpl shift_sp. econstructor; eauto. traceEq.
+  simpl shift_sp. econstructor; eauto.
+  rewrite (stacksize_preserved _ _ TRANSL); eauto.
+  traceEq.
   econstructor; eauto. 
   intros. symmetry. eapply agree_return_regs; eauto.
   apply agree_callee_save_return_regs.  
@@ -1583,13 +1596,13 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor. 
+  eapply Genv.init_mem_transf_partial; eauto.
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. eauto.
   eauto. 
-  rewrite (Genv.init_mem_transf_partial _ _ TRANSF).
   econstructor; eauto. constructor. 
   eapply Genv.find_funct_ptr_prop; eauto.
-  intros. rewrite H2 in H4. simpl in H4. contradiction.
+  intros. rewrite H3 in H5. simpl in H5. contradiction.
   simpl; red; auto.
 Qed.
 
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 8681d84a..0ca4c028 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Op.
 Require Import Events.
 Require Import Globalenvs.
@@ -227,66 +227,6 @@ Proof.
   apply regset_set. auto. auto.
 Qed.
 
-(** ** Agreement between the size of a stack block and a function *)
-
-(** To reason over deallocation of empty stack blocks, we need to
-  maintain the invariant that the bounds of a stack block
-  for function [f] are always [0, f.(fn_stacksize)]. *)
-
-Inductive match_stacksize: function -> block -> mem -> Z -> Prop :=
-  | match_stacksize_intro: forall f sp m bound,
-      sp < bound ->
-      low_bound m sp = 0 ->
-      high_bound m sp = f.(fn_stacksize) ->
-      match_stacksize f sp m bound.
-
-Lemma match_stacksize_store:
-  forall m m' chunk  b ofs v f sp bound,
-  store chunk m b ofs v = Some m' ->
-  match_stacksize f sp m bound ->
-  match_stacksize f sp m' bound.
-Proof.
-  intros. inv H0. constructor. auto.
-  rewrite <- H2. eapply Mem.low_bound_store; eauto.
-  rewrite <- H3. eapply Mem.high_bound_store; eauto.
-Qed.
-
-Lemma match_stacksize_alloc_other:
-  forall m m' lo hi b f sp bound,
-  alloc m lo hi = (m', b) ->
-  match_stacksize f sp m bound ->
-  bound <= m.(nextblock) ->
-  match_stacksize f sp m' bound.
-Proof.
-  intros. inv H0.
-  assert (valid_block m sp). red. omega.
-  constructor. auto.
-  rewrite <- H3. eapply low_bound_alloc_other; eauto.
-  rewrite <- H4. eapply high_bound_alloc_other; eauto.
-Qed.
-
-Lemma match_stacksize_alloc_same:
-  forall m f m' sp,
-  alloc m 0 f.(fn_stacksize) = (m', sp) ->
-  match_stacksize f sp m' m'.(nextblock).
-Proof.
-  intros. constructor. 
-  unfold alloc in H. inv H. simpl. omega.
-  eapply low_bound_alloc_same; eauto.
-  eapply high_bound_alloc_same; eauto.
-Qed.
-
-Lemma match_stacksize_free:
-  forall f sp m b bound,
-  match_stacksize f sp m bound ->
-  bound <= b ->
-  match_stacksize f sp (free m b) bound.
-Proof.
-  intros. inv H. constructor. auto.
-  rewrite <- H2. apply low_bound_free. unfold block; omega.
-  rewrite <- H3. apply high_bound_free. unfold block; omega.
-Qed.
-
 (** * Proof of semantic preservation *)
 
 Section PRESERVATION.
@@ -319,6 +259,13 @@ Proof.
   destruct (zeq (fn_stacksize f) 0); auto. 
 Qed.
 
+Lemma stacksize_preserved:
+  forall f, fn_stacksize (transf_function f) = fn_stacksize f.
+Proof.
+  unfold transf_function. intros. 
+  destruct (zeq (fn_stacksize f) 0); auto.
+Qed.
+
 Lemma find_function_translated:
   forall ros rs rs' f,
   find_function ge ros rs = Some f ->
@@ -370,131 +317,58 @@ We first define the simulation invariant between call stacks.
 The first two cases are standard, but the third case corresponds
 to a frame that was eliminated by the transformation. *)
 
-Inductive match_stackframes: mem -> Z -> list stackframe -> list stackframe -> Prop :=
-  | match_stackframes_nil: forall m bound,
-      match_stackframes m bound nil nil
-  | match_stackframes_normal: forall m bound stk stk' res sp pc rs rs' f,
-      match_stackframes m sp stk stk' ->
-      match_stacksize f sp m bound ->
+Inductive match_stackframes: list stackframe -> list stackframe -> Prop :=
+  | match_stackframes_nil:
+      match_stackframes nil nil
+  | match_stackframes_normal: forall stk stk' res sp pc rs rs' f,
+      match_stackframes stk stk' ->
       regset_lessdef rs rs' ->
-      match_stackframes m bound
-        (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk)
-        (Stackframe res (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' :: stk')
-  | match_stackframes_tail: forall m bound stk stk' res sp pc rs f,
-      match_stackframes m sp stk stk' ->
-      match_stacksize f sp m bound ->
+      match_stackframes
+        (Stackframe res f (Vptr sp Int.zero) pc rs :: stk)
+        (Stackframe res (transf_function f) (Vptr sp Int.zero) pc rs' :: stk')
+  | match_stackframes_tail: forall stk stk' res sp pc rs f,
+      match_stackframes stk stk' ->
       is_return_spec f pc res ->
       f.(fn_stacksize) = 0 ->
-      match_stackframes m bound
-        (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk)
+      match_stackframes
+        (Stackframe res f (Vptr sp Int.zero) pc rs :: stk)
         stk'.
 
-(** In [match_stackframes m bound s s'], the memory state [m] is used
-  to check that the sizes of the stack blocks agree with what was
-  declared by the corresponding functions.  The [bound] parameter
-  is used to enforce separation between the stack blocks. *)
-
-Lemma match_stackframes_incr:
-  forall m bound s s' bound',
-  match_stackframes m bound s s' ->
-  bound <= bound' ->
-  match_stackframes m bound' s s'.
-Proof.
-  intros. inv H; econstructor; eauto. 
-  inv H2. constructor; auto. omega.
-  inv H2. constructor; auto. omega.
-Qed.
-
-Lemma match_stackframes_store:
-  forall m bound s s',
-  match_stackframes m bound s s' -> 
-  forall chunk b ofs v m',
-  store chunk m b ofs v = Some m' ->
-  match_stackframes m' bound s s'.
-Proof.
-  induction 1; intros.
-  constructor.
-  econstructor; eauto. eapply match_stacksize_store; eauto.
-  econstructor; eauto. eapply match_stacksize_store; eauto.
-Qed.
-
-Lemma match_stackframes_alloc:
-  forall m lo hi m' sp s s',
-  match_stackframes m (nextblock m) s s' ->
-  alloc m lo hi = (m', sp) ->
-  match_stackframes m' sp s s'.
-Proof.
-  intros. 
-  assert (forall bound s s',
-    match_stackframes m bound s s' ->
-    bound <= m.(nextblock) ->
-    match_stackframes m' bound s s').
-  induction 1; intros. constructor.
-  constructor; auto. apply IHmatch_stackframes; auto. inv H2. omega. 
-  eapply match_stacksize_alloc_other; eauto.
-  econstructor; eauto.  apply IHmatch_stackframes; auto. inv H2. omega. 
-  eapply match_stacksize_alloc_other; eauto.
-  exploit alloc_result; eauto. intro. rewrite H2.
-  eapply H1; eauto. omega.
-Qed. 
-
-Lemma match_stackframes_free:
-  forall f sp m s s',
-  match_stacksize f sp m (nextblock m) ->
-  match_stackframes m sp s s' ->
-  match_stackframes (free m sp) (nextblock (free m sp)) s s'.
-Proof.
-  intros. simpl. 
-  assert (forall bound s s',
-    match_stackframes m bound s s' ->
-    bound <= sp ->
-    match_stackframes (free m sp) bound s s').
-  induction 1; intros. constructor.
-  constructor; auto. apply IHmatch_stackframes; auto. inv H2; omega. 
-  apply match_stacksize_free; auto.
-  econstructor; eauto. apply IHmatch_stackframes; auto. inv H2; omega. 
-  apply match_stacksize_free; auto.
-
-  apply match_stackframes_incr with sp. apply H1; auto. omega.
-  inv H. omega. 
-Qed.
-
 (** Here is the invariant relating two states.  The first three
   cases are standard.  Note the ``less defined than'' conditions
-  over values, register states, and memory states. *)
+  over values and register states, and the corresponding ``extends''
+  relation over memory states. *)
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_normal:
       forall s sp pc rs m s' rs' m' f
-             (STKSZ: match_stacksize f sp m m.(nextblock))
-             (STACKS: match_stackframes m sp s s')
+             (STACKS: match_stackframes s s')
              (RLD: regset_lessdef rs rs')
-             (MLD: Mem.lessdef m m'),
-      match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m)
-                   (State s' (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' m')
+             (MLD: Mem.extends m m'),
+      match_states (State s f (Vptr sp Int.zero) pc rs m)
+                   (State s' (transf_function f) (Vptr sp Int.zero) pc rs' m')
   | match_states_call:
       forall s f args m s' args' m',
-      match_stackframes m m.(nextblock) s s' ->
+      match_stackframes s s' ->
       Val.lessdef_list args args' ->
-      Mem.lessdef m m' ->
+      Mem.extends m m' ->
       match_states (Callstate s f args m)
                    (Callstate s' (transf_fundef f) args' m')
   | match_states_return:
       forall s v m s' v' m',
-      match_stackframes m m.(nextblock) s s' ->
+      match_stackframes s s' ->
       Val.lessdef v v' ->
-      Mem.lessdef m m' ->
+      Mem.extends m m' ->
       match_states (Returnstate s v m)
                    (Returnstate s' v' m')
   | match_states_interm:
       forall s sp pc rs m s' m' f r v'
-             (STKSZ: match_stacksize f sp m m.(nextblock))
-             (STACKS: match_stackframes m sp s s')
-             (MLD: Mem.lessdef m m'),
+             (STACKS: match_stackframes s s')
+             (MLD: Mem.extends m m'),
       is_return_spec f pc r ->
       f.(fn_stacksize) = 0 ->
       Val.lessdef (rs#r) v' ->
-      match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m)
+      match_states (State s f (Vptr sp Int.zero) pc rs m)
                    (Returnstate s' v' m').
 
 (** The last case of [match_states] corresponds to the execution
@@ -516,7 +390,7 @@ Inductive match_states: state -> state -> Prop :=
 
 Definition measure (st: state) : nat :=
   match st with
-  | State s c sp pc rs m => (List.length s * (niter + 2) + return_measure c pc + 1)%nat
+  | State s f sp pc rs m => (List.length s * (niter + 2) + return_measure f.(fn_code) pc + 1)%nat
   | Callstate s f args m => 0%nat
   | Returnstate s v m => (List.length s * (niter + 2))%nat
   end.
@@ -557,7 +431,7 @@ Proof.
   assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. 
   exploit eval_operation_lessdef; eauto. 
   intros [v' [EVAL' VLD]]. 
-  left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split.
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split.
   eapply exec_Iop; eauto.  rewrite <- EVAL'.
   apply eval_operation_preserved. exact symbols_preserved.
   econstructor; eauto. apply regset_set; auto.
@@ -571,9 +445,9 @@ Proof.
   assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. 
   exploit eval_addressing_lessdef; eauto. 
   intros [a' [ADDR' ALD]].
-  exploit loadv_lessdef; eauto. 
+  exploit Mem.loadv_extends; eauto. 
   intros [v' [LOAD' VLD]].
-  left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split.
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split.
   eapply exec_Iload with (a := a'). eauto.  rewrite <- ADDR'.
   apply eval_addressing_preserved. exact symbols_preserved. eauto.
   econstructor; eauto. apply regset_set; auto.
@@ -583,88 +457,91 @@ Proof.
   assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. 
   exploit eval_addressing_lessdef; eauto. 
   intros [a' [ADDR' ALD]].
-  exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD.  
+  exploit Mem.storev_extends. 2: eexact H1. eauto. eauto. apply RLD.  
   intros [m'1 [STORE' MLD']].
-  left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split.
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'1); split.
   eapply exec_Istore with (a := a'). eauto.  rewrite <- ADDR'.
   apply eval_addressing_preserved. exact symbols_preserved. eauto.
   destruct a; simpl in H1; try discriminate.
   econstructor; eauto.
-  eapply match_stacksize_store; eauto. 
-  rewrite (nextblock_store _ _ _ _ _ _ H1). auto.
-  eapply match_stackframes_store; eauto.
 
 (* call *)
   exploit find_function_translated; eauto. intro FIND'.  
   TransfInstr.
 (* call turned tailcall *)
-  left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' sp0)); split.
+  assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}).
+    apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7. 
+    red; intros; omegaContradiction.
+  destruct X as [m'' FREE].
+  left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split.
   eapply exec_Itailcall; eauto. apply sig_preserved. 
   constructor. eapply match_stackframes_tail; eauto. apply regset_get_list; auto.
-  apply Mem.free_right_lessdef; auto. inv STKSZ. omega.  
+  eapply Mem.free_right_extends; eauto.
+  rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction.
 (* call that remains a call *)
-  left. exists (Callstate (Stackframe res (fn_code (transf_function f0)) (Vptr sp0 Int.zero) pc' rs' :: s')
-                          (transf_fundef f) (rs'##args) m'); split.
+  left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Int.zero) pc' rs' :: s')
+                          (transf_fundef fd) (rs'##args) m'); split.
   eapply exec_Icall; eauto. apply sig_preserved. 
   constructor. constructor; auto. apply regset_get_list; auto. auto. 
 
 (* tailcall *) 
-  exploit find_function_translated; eauto. intro FIND'.  
+  exploit find_function_translated; eauto. intro FIND'.
+  exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]].
   TransfInstr.
-  left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' stk)); split.
-  eapply exec_Itailcall; eauto. apply sig_preserved. 
-  constructor. eapply match_stackframes_free; eauto. 
-  apply regset_get_list; auto. apply Mem.free_lessdef; auto.
+  left. exists (Callstate s' (transf_fundef fd) (rs'##args) m'1); split.
+  eapply exec_Itailcall; eauto. apply sig_preserved.
+  rewrite stacksize_preserved; auto.
+  constructor. auto.  apply regset_get_list; auto. auto. 
 
 (* cond true *)
   TransfInstr. 
-  left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifso rs' m'); split.
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split.
   eapply exec_Icond_true; eauto.
   apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto.
   constructor; auto. 
 
 (* cond false *)
   TransfInstr. 
-  left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifnot rs' m'); split.
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifnot rs' m'); split.
   eapply exec_Icond_false; eauto.
   apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto.
   constructor; auto. 
 
 (* jumptable *)
   TransfInstr. 
-  left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'); split.
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'); split.
   eapply exec_Ijumptable; eauto.
   generalize (RLD arg). rewrite H0. intro. inv H2. auto.
   constructor; auto. 
 
 (* return *)
+  exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]].
   TransfInstr.
-  left. exists (Returnstate s' (regmap_optget or Vundef rs') (free m' stk)); split.
-  apply exec_Ireturn; auto.
-  constructor.
-  eapply match_stackframes_free; eauto. 
+  left. exists (Returnstate s' (regmap_optget or Vundef rs') m'1); split.
+  apply exec_Ireturn; auto. rewrite stacksize_preserved; auto.
+  constructor. auto.
   destruct or; simpl. apply RLD. constructor.
-  apply Mem.free_lessdef; auto.
+  auto.
 
 (* eliminated return None *)
   assert (or = None) by congruence. subst or. 
   right. split. simpl. omega. split. auto. 
-  constructor.
-  eapply match_stackframes_free; eauto.
+  constructor. auto.
   simpl. constructor.
-  apply Mem.free_left_lessdef; auto. 
+  eapply Mem.free_left_extends; eauto. 
 
 (* eliminated return Some *)
   assert (or = Some r) by congruence. subst or.
   right. split. simpl. omega. split. auto.
-  constructor.
-  eapply match_stackframes_free; eauto.
+  constructor. auto.
   simpl. auto.
-  apply Mem.free_left_lessdef; auto.
+  eapply Mem.free_left_extends; eauto.
 
 (* internal call *)
-  caseEq (alloc m'0 0 (fn_stacksize f)). intros m'1 stk' ALLOC'.
-  exploit alloc_lessdef; eauto. intros [EQ1 LD']. subst stk'. 
+  exploit Mem.alloc_extends; eauto.
+    instantiate (1 := 0). omega.
+    instantiate (1 := fn_stacksize f). omega.
+  intros [m'1 [ALLOC EXT]].
   assert (fn_stacksize (transf_function f) = fn_stacksize f /\
           fn_entrypoint (transf_function f) = fn_entrypoint f /\
           fn_params (transf_function f) = fn_params f).
@@ -673,13 +550,12 @@ Proof.
   left. econstructor; split.
   simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto.
   rewrite EQ2. rewrite EQ3. constructor; auto.
-  eapply match_stacksize_alloc_same; eauto.
-  eapply match_stackframes_alloc; eauto. 
   apply regset_init_regs. auto. 
 
 (* external call *)
-  exploit event_match_lessdef; eauto. intros [res' [EVM' VLD']]. 
-  left. exists (Returnstate s' res' m'); split.
+  exploit external_call_mem_extends; eauto.
+  intros [res' [m2' [A [B [C D]]]]].
+  left. exists (Returnstate s' res' m2'); split.
   simpl. econstructor; eauto.
   constructor; auto. 
 
@@ -705,15 +581,13 @@ Lemma transf_initial_states:
 Proof.
   intros. inv H. 
   exploit funct_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split.
-  econstructor; eauto.
+  exists (Callstate nil (transf_fundef f) nil m0); split.
+  econstructor; eauto. apply Genv.init_mem_transf. auto.
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
   reflexivity.
-  rewrite <- H2. apply sig_preserved.
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
-  constructor. constructor. constructor. apply lessdef_refl. 
-  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. 
+  rewrite <- H3. apply sig_preserved.
+  constructor. constructor. constructor. apply Mem.extends_refl. 
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 92ec68cf..4cbcbd4f 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import UnionFind.
 Require Import AST.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -348,15 +348,14 @@ Lemma transf_initial_states:
   exists st2, initial_state tp st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. 
-  exists (Callstate nil (tunnel_fundef f) nil (Genv.init_mem tp)); split.
+  exists (Callstate nil (tunnel_fundef f) nil m0); split.
   econstructor; eauto.
+  apply Genv.init_mem_transf; auto.
   change (prog_main tp) with (prog_main p).
   rewrite symbols_preserved. eauto.
   apply function_ptr_translated; auto.
-  rewrite <- H2. apply sig_preserved. 
-  replace (Genv.init_mem tp) with (Genv.init_mem p).
-  constructor. constructor. auto.
-  symmetry. unfold tp, tunnel_program. apply Genv.init_mem_transf.
+  rewrite <- H3. apply sig_preserved. 
+  constructor. constructor.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
index 834e8e18..743b4681 100644
--- a/backend/Tunnelingtyping.v
+++ b/backend/Tunnelingtyping.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import UnionFind.
 Require Import AST.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.