Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


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

19 files changed, 3659 insertions, 258 deletions

diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 84b47f3..a8e49e8 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -68,8 +68,8 @@ Inductive stmt : Type :=
   | Sskip: stmt
   | Sassign : ident -> expr -> stmt
   | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
-  | Scall : option ident -> signature -> expr -> exprlist -> stmt
-  | Stailcall: signature -> expr -> exprlist -> stmt
+  | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt
+  | Stailcall: signature -> expr + ident -> exprlist -> stmt
   | Sbuiltin : option ident -> external_function -> exprlist -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: condexpr -> stmt -> stmt -> stmt
@@ -208,6 +208,14 @@ Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop
   with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop
   with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop.
 
+Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop :=
+  | eval_eos_e: forall le e v,
+      eval_expr le e v ->
+      eval_expr_or_symbol le (inl _ e) v
+  | eval_eos_s: forall le id b,
+      Genv.find_symbol ge id = Some b ->
+      eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero).
+
 End EVAL_EXPR.
 
 (** Pop continuation until a call or stop *)
@@ -282,7 +290,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f Sskip k sp e m')
 
   | step_call: forall f optid sig a bl k sp e m vf vargs fd,
-      eval_expr sp e m nil a vf ->
+      eval_expr_or_symbol sp e m nil a vf ->
       eval_exprlist sp e m nil bl vargs ->
       Genv.find_funct ge vf = Some fd ->
       funsig fd = sig ->
@@ -290,7 +298,7 @@ Inductive step: state -> trace -> state -> Prop :=
         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 m',
-      eval_expr (Vptr sp Int.zero) e m nil a vf ->
+      eval_expr_or_symbol (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 ->
diff --git a/backend/Constprop.v b/backend/Constprop.v
index c3b9863..19e5d1a 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -107,11 +107,84 @@ End Approx.
 
 Module D := LPMap Approx.
 
-(** The transfer function for the dataflow analysis is straightforward:
-  for [Iop] instructions, we set the approximation of the destination
-  register to the result of executing abstractly the operation;
-  for [Iload] and [Icall], we set the approximation of the destination
-  to [Unknown]. *)
+(** We keep track of read-only global variables (i.e. "const" global
+  variables in C) as a map from their names to their initialization
+  data. *)
+
+Definition global_approx : Type := PTree.t (list init_data).
+
+(** Given some initialization data and a byte offset, compute a static
+  approximation of the result of a memory load from a memory block
+  initialized with this data. *)
+
+Fixpoint eval_load_init (chunk: memory_chunk) (pos: Z) (il: list init_data): approx :=
+  match il with
+  | nil => Unknown
+  | Init_int8 n :: il' =>
+      if zeq pos 0 then
+        match chunk with
+        | Mint8unsigned => I (Int.zero_ext 8 n)
+        | Mint8signed => I (Int.sign_ext 8 n)
+        | _ => Unknown
+        end
+      else eval_load_init chunk (pos - 1) il'
+  | Init_int16 n :: il' =>
+      if zeq pos 0 then
+        match chunk with
+        | Mint16unsigned => I (Int.zero_ext 16 n)
+        | Mint16signed => I (Int.sign_ext 16 n)
+        | _ => Unknown
+        end
+      else eval_load_init chunk (pos - 2) il'
+  | Init_int32 n :: il' =>
+      if zeq pos 0 
+      then match chunk with Mint32 => I n | _ => Unknown end
+      else eval_load_init chunk (pos - 4) il'
+  | Init_float32 n :: il' =>
+      if zeq pos 0
+      then match chunk with 
+           | Mfloat32 => if propagate_float_constants tt then F (Float.singleoffloat n) else Unknown
+           | _ => Unknown
+           end
+      else eval_load_init chunk (pos - 4) il'
+  | Init_float64 n :: il' =>
+      if zeq pos 0 
+      then match chunk with
+           | Mfloat64 => if propagate_float_constants tt then F n else Unknown
+           | _ => Unknown
+           end
+      else eval_load_init chunk (pos - 8) il'
+  | Init_addrof symb ofs :: il' =>
+      if zeq pos 0
+      then match chunk with Mint32 => G symb ofs | _ => Unknown end
+      else eval_load_init chunk (pos - 4) il'
+  | Init_space n :: il' =>
+      eval_load_init chunk (pos - Zmax n 0) il'
+  end.
+
+(** Compute a static approximation for the result of a load at an address whose
+  approximation is known.  If the approximation points to a global variable,
+  and this global variable is read-only, we use its initialization data
+  to determine a static approximation.  Otherwise, [Unknown] is returned. *)
+
+Definition eval_static_load (gapp: global_approx) (chunk: memory_chunk) (addr: approx) : approx :=
+  match addr with
+  | G symb ofs =>
+      match gapp!symb with
+      | None => Unknown
+      | Some il => eval_load_init chunk (Int.unsigned ofs) il
+      end
+  | _ => Unknown
+  end.
+
+(** The transfer function for the dataflow analysis is straightforward.
+  For [Iop] instructions, we set the approximation of the destination
+  register to the result of executing abstractly the operation.
+  For [Iload] instructions, we set the approximation of the destination
+  register to the result of [eval_static_load].
+  For [Icall] and [Ibuiltin], the destination register becomes [Unknown].
+  Other instructions keep the approximations unchanged, as they preserve
+  the values of all registers. *)
 
 Definition approx_reg (app: D.t) (r: reg) := 
   D.get r app.
@@ -119,7 +192,7 @@ Definition approx_reg (app: D.t) (r: reg) :=
 Definition approx_regs (app: D.t) (rl: list reg):=
   List.map (approx_reg app) rl.
 
-Definition transfer (f: function) (pc: node) (before: D.t) :=
+Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t) :=
   match f.(fn_code)!pc with
   | None => before
   | Some i =>
@@ -128,7 +201,9 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
           let a := eval_static_operation op (approx_regs before args) in
           D.set res a before
       | Iload chunk addr args dst s =>
-          D.set dst Unknown before
+          let a := eval_static_load gapp chunk
+                     (eval_static_addressing addr (approx_regs before args)) in
+          D.set dst a before
       | Icall sig ros args res s =>
           D.set res Unknown before
       | Ibuiltin ef args res s =>
@@ -142,12 +217,13 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
   generic solver for forward dataflow inequations. [analyze f]
   returns a mapping from program points to mappings of pseudo-registers
   to approximations.  It can fail to reach a fixpoint in a reasonable
-  number of iterations, in which case [None] is returned. *)
+  number of iterations, in which case we use the trivial mapping
+  (program point -> [D.top]) instead. *)
 
 Module DS := Dataflow_Solver(D)(NodeSetForward).
 
-Definition analyze (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) (transfer f) 
+Definition analyze (gapp: global_approx) (f: RTL.function): PMap.t D.t :=
+  match DS.fixpoint (successors f) (transfer gapp f) 
                     ((f.(fn_entrypoint), D.top) :: nil) with
   | None => PMap.init D.top
   | Some res => res
@@ -158,10 +234,12 @@ Definition analyze (f: RTL.function): PMap.t D.t :=
 (** The code transformation proceeds instruction by instruction.
     Operators whose arguments are all statically known are turned
     into ``load integer constant'', ``load float constant'' or
-    ``load symbol address'' operations.  Operators for which some
+    ``load symbol address'' operations.  Likewise for loads whose
+    result can be statically predicted.  Operators for which some
     but not all arguments are known are subject to strength reduction,
     and similarly for the addressing modes of load and store instructions.
-    Other instructions are unchanged. *)
+    Conditional branches and multi-way branches are statically resolved
+    into [Inop] instructions if possible. Other instructions are unchanged. *)
 
 Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
   match ros with
@@ -173,25 +251,38 @@ Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
   | inr s => ros
   end.
 
-Definition transf_instr (app: D.t) (instr: instruction) :=
+Parameter generate_float_constants : unit -> bool.
+
+Definition const_for_result (a: approx) : option operation :=
+  match a with
+  | I n => Some(Ointconst n)
+  | F n => if generate_float_constants tt then Some(Ofloatconst n) else None
+  | G symb ofs => Some(Oaddrsymbol symb ofs)
+  | S ofs => Some(Oaddrstack ofs)
+  | _ => None
+  end.
+
+Definition transf_instr (gapp: global_approx) (app: D.t) (instr: instruction) :=
   match instr with
   | Iop op args res s =>
-      match eval_static_operation op (approx_regs app args) with
-      | I n =>
-          Iop (Ointconst n) nil res s
-      | F n =>
-          Iop (Ofloatconst n) nil res s
-      | G symb ofs =>
-          Iop (Oaddrsymbol symb ofs) nil res s
-      | S ofs =>
-          Iop (Oaddrstack ofs) nil res s
-      | _ =>
+      let a := eval_static_operation op (approx_regs app args) in
+      match const_for_result a with
+      | Some cop =>
+          Iop cop nil res s
+      | None =>
           let (op', args') := op_strength_reduction op args (approx_regs app args) in
           Iop op' args' res s
       end
   | Iload chunk addr args dst s =>
-      let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in
-      Iload chunk addr' args' dst s      
+      let a := eval_static_load gapp chunk
+                  (eval_static_addressing addr (approx_regs app args)) in
+      match const_for_result a with
+      | Some cop =>
+          Iop cop nil dst s
+      | None =>
+          let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in
+          Iload chunk addr' args' dst s      
+      end
   | Istore chunk addr args src s =>
       let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in
       Istore chunk addr' args' src s      
@@ -223,20 +314,32 @@ Definition transf_instr (app: D.t) (instr: instruction) :=
       instr
   end.
 
-Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
-  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
+Definition transf_code (gapp: global_approx) (app: PMap.t D.t) (instrs: code) : code :=
+  PTree.map (fun pc instr => transf_instr gapp app!!pc instr) instrs.
 
-Definition transf_function (f: function) : function :=
-  let approxs := analyze f in
+Definition transf_function (gapp: global_approx) (f: function) : function :=
+  let approxs := analyze gapp f in
   mkfunction
     f.(fn_sig)
     f.(fn_params)
     f.(fn_stacksize)
-    (transf_code approxs f.(fn_code))
+    (transf_code gapp approxs f.(fn_code))
     f.(fn_entrypoint).
 
-Definition transf_fundef (fd: fundef) : fundef :=
-  AST.transf_fundef transf_function fd.
+Definition transf_fundef (gapp: global_approx) (fd: fundef) : fundef :=
+  AST.transf_fundef (transf_function gapp) fd.
+
+Fixpoint make_global_approx (gapp: global_approx) (vars: list (ident * globvar unit)) : global_approx :=
+  match vars with
+  | nil => gapp
+  | (id, gv) :: vars' =>
+      let gapp1 :=
+        if gv.(gvar_readonly) && negb gv.(gvar_volatile)
+        then PTree.set id gv.(gvar_init) gapp
+        else PTree.remove id gapp in
+      make_global_approx gapp1 vars'
+  end.
 
 Definition transf_program (p: program) : program :=
-  transform_program transf_fundef p.
+  let gapp := make_global_approx (PTree.empty _) p.(prog_vars) in
+  transform_program (transf_fundef gapp) p.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 9affea8..406e613 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -31,11 +31,18 @@ Require Import ConstpropOp.
 Require Import Constprop.
 Require Import ConstpropOpproof.
 
+Section PRESERVATION.
+
+Variable prog: program.
+Let tprog := transf_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+Let gapp := make_global_approx (PTree.empty _) prog.(prog_vars).
+
 (** * Correctness of the static analysis *)
 
 Section ANALYSIS.
 
-Variable ge: genv.
 Variable sp: val.
 
 Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
@@ -97,14 +104,14 @@ Lemma analyze_correct_1:
   forall f pc rs pc' i,
   f.(fn_code)!pc = Some i ->
   In pc' (successors_instr i) ->
-  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
-  regs_match_approx (analyze f)!!pc' rs.
+  regs_match_approx (transfer gapp f pc (analyze gapp f)!!pc) rs ->
+  regs_match_approx (analyze gapp f)!!pc' rs.
 Proof.
   intros until i. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
+  caseEq (DS.fixpoint (successors f) (transfer gapp f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
-  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
+  apply regs_match_approx_increasing with (transfer gapp f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
   unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto.
   auto.
@@ -113,10 +120,10 @@ Qed.
 
 Lemma analyze_correct_3:
   forall f rs,
-  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
+  regs_match_approx (analyze gapp f)!!(f.(fn_entrypoint)) rs.
 Proof.
   intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
+  caseEq (DS.fixpoint (successors f) (transfer gapp f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with D.top.
@@ -125,6 +132,301 @@ Proof.
   intros. rewrite PMap.gi. apply regs_match_approx_top.
 Qed.
 
+(** eval_static_load *)
+
+Definition mem_match_approx (m: mem) : Prop :=
+  forall id il b,
+  gapp!id = Some il -> Genv.find_symbol ge id = Some b ->
+  Genv.load_store_init_data ge m b 0 il /\
+  Mem.valid_block m b /\
+  (forall ofs, ~Mem.perm m b ofs Max Writable).
+
+Lemma eval_load_init_sound:
+  forall chunk m b il base ofs pos v,
+  Genv.load_store_init_data ge m b base il ->
+  Mem.load chunk m b ofs = Some v ->
+  ofs = base + pos ->
+  val_match_approx ge sp (eval_load_init chunk pos il) v.
+Proof.
+  induction il; simpl; intros.
+(* base case il = nil *)
+  auto.
+(* inductive case *)
+  destruct a.
+  (* Init_int8 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  rewrite Mem.load_int8_signed_unsigned in H0. rewrite H in H0. simpl in H0.
+  inv H0. decEq. apply Int.sign_ext_zero_ext. compute; auto. 
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_int16 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  rewrite Mem.load_int16_signed_unsigned in H0. rewrite H in H0. simpl in H0.
+  inv H0. decEq. apply Int.sign_ext_zero_ext. compute; auto. 
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_int32 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_float32 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto. destruct (propagate_float_constants tt); simpl; auto.
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_float64 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto. destruct (propagate_float_constants tt); simpl; auto.
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_space *)
+  eapply IHil; eauto. omega.
+  (* Init_symbol *)
+  destruct H as [[b' [A B]] C].
+  destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  unfold symbol_address. rewrite A. congruence.
+  eapply IHil; eauto. omega.
+Qed.
+
+Lemma eval_static_load_sound:
+  forall chunk m addr vaddr v,
+  Mem.loadv chunk m vaddr = Some v ->
+  mem_match_approx m ->  
+  val_match_approx ge sp addr vaddr ->
+  val_match_approx ge sp (eval_static_load gapp chunk addr) v.
+Proof.
+  intros. unfold eval_static_load. destruct addr; simpl; auto. 
+  destruct (gapp!i) as [il|]_eqn; auto.
+  red in H1. subst vaddr. unfold symbol_address in H. 
+  destruct (Genv.find_symbol ge i) as [b'|]_eqn; simpl in H; try discriminate.
+  exploit H0; eauto. intros [A [B C]]. 
+  eapply eval_load_init_sound; eauto. 
+  red; auto. 
+Qed.
+
+Lemma mem_match_approx_store:
+  forall chunk m addr v m',
+  mem_match_approx m ->
+  Mem.storev chunk m addr v = Some m' ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  destruct addr; simpl in H0; try discriminate.
+  exploit Mem.store_valid_access_3; eauto. intros [P Q].
+  split. apply Genv.load_store_init_data_invariant with m; auto. 
+  intros. eapply Mem.load_store_other; eauto. left; red; intro; subst b0.
+  eapply C. apply Mem.perm_cur_max. eapply P. instantiate (1 := Int.unsigned i).
+  generalize (size_chunk_pos chunk). omega.
+  split. eauto with mem.
+  intros; red; intros. eapply C. eapply Mem.perm_store_2; eauto.
+Qed.
+
+Lemma mem_match_approx_alloc:
+  forall m lo hi b m',
+  mem_match_approx m ->
+  Mem.alloc m lo hi = (m', b) ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  split. apply Genv.load_store_init_data_invariant with m; auto.
+  intros. eapply Mem.load_alloc_unchanged; eauto. 
+  split. eauto with mem.
+  intros; red; intros. exploit Mem.perm_alloc_inv; eauto. 
+  rewrite zeq_false. apply C. eapply Mem.valid_not_valid_diff; eauto with mem.
+Qed.
+
+Lemma mem_match_approx_free:
+  forall m lo hi b m',
+  mem_match_approx m ->
+  Mem.free m b lo hi = Some m' ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  split. apply Genv.load_store_init_data_invariant with m; auto.
+  intros. eapply Mem.load_free; eauto.
+  destruct (zeq b0 b); auto. subst b0.
+  right. destruct (zlt lo hi); auto. 
+  elim (C lo). apply Mem.perm_cur_max. 
+  exploit Mem.free_range_perm; eauto. instantiate (1 := lo); omega. 
+  intros; eapply Mem.perm_implies; eauto with mem.
+  split. eauto with mem.
+  intros; red; intros. eapply C. eauto with mem. 
+Qed.
+
+Lemma mem_match_approx_extcall:
+  forall ef vargs m t vres m',
+  mem_match_approx m ->
+  external_call ef ge vargs m t vres m' ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  split. apply Genv.load_store_init_data_invariant with m; auto.
+  intros. eapply external_call_readonly; eauto. 
+  split. eapply external_call_valid_block; eauto.
+  intros; red; intros. elim (C ofs). eapply external_call_max_perm; eauto. 
+Qed.
+
+(* Show that mem_match_approx holds initially *)
+
+Definition global_approx_charact (g: genv) (ga: global_approx) : Prop :=
+  forall id il b,
+  ga!id = Some il -> 
+  Genv.find_symbol g id = Some b -> 
+  Genv.find_var_info g b = Some (mkglobvar tt il true false).
+
+Lemma make_global_approx_correct:
+  forall vl g ga,
+  global_approx_charact g ga ->
+  global_approx_charact (Genv.add_variables g vl) (make_global_approx ga vl).
+Proof.
+  induction vl; simpl; intros.
+  auto.
+  destruct a as [id gv]. apply IHvl. 
+  red; intros. 
+  assert (EITHER: id0 = id /\ gv = mkglobvar tt il true false
+               \/ id0 <> id /\ ga!id0 = Some il).
+  destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn.
+  rewrite PTree.gsspec in H0. destruct (peq id0 id).
+  inv H0. left. split; auto. 
+  destruct gv; simpl in *. 
+  destruct gvar_readonly; try discriminate.
+  destruct gvar_volatile; try discriminate.
+  destruct gvar_info. auto.
+  right; auto.
+  rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); try discriminate.
+  right; auto.
+  unfold Genv.add_variable, Genv.find_symbol, Genv.find_var_info in *;
+  simpl in *.
+  destruct EITHER as [[A B] | [A B]].
+  subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto.
+  rewrite PTree.gso in H1; auto. rewrite ZMap.gso. eapply H. eauto. auto.
+  exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega.
+Qed.
+
+Theorem mem_match_approx_init:
+  forall m, Genv.init_mem prog = Some m -> mem_match_approx m.
+Proof.
+  intros. 
+  assert (global_approx_charact ge gapp).
+    unfold ge, gapp.   unfold Genv.globalenv.
+    apply make_global_approx_correct.
+    red; intros. rewrite PTree.gempty in H0; discriminate.
+  red; intros. 
+  exploit Genv.init_mem_characterization.
+  unfold ge in H0. eapply H0; eauto. eauto. 
+  unfold Genv.perm_globvar; simpl.
+  intros [A [B C]].
+  split. auto. split. eapply Genv.find_symbol_not_fresh; eauto. 
+  intros; red; intros. exploit B; eauto. intros [P Q]. inv Q.
+Qed.
+
+(**********************
+Definition mem_match_approx_gen (g: genv) (ga: global_approx) (m: mem) : Prop :=
+  forall id il b,
+  ga!id = Some il -> Genv.find_symbol g id = Some b ->
+  Genv.load_store_init_data ge m b 0 il /\
+  Mem.valid_block m b /\
+  (forall ofs, ~Mem.perm m b ofs Max Writable).
+
+Lemma mem_match_approx_alloc_variables:
+  forall vl g ga m m',
+  mem_match_approx_gen g ga m ->
+  Genv.genv_nextvar g = Mem.nextblock m ->
+  Genv.alloc_variables ge m vl = Some m' ->
+  mem_match_approx_gen (Genv.add_variables g vl) (make_global_approx ga vl) m'.
+Proof.
+  induction vl; simpl; intros.
+(* base case *)
+  inv H1. auto.
+(* inductive case *)
+  destruct a as [id gv].
+  set (ga1 := if gv.(gvar_readonly) && negb gv.(gvar_volatile)
+        then PTree.set id gv.(gvar_init) ga
+        else PTree.remove id ga).
+  revert H1. unfold Genv.alloc_variable. simpl.
+  set (il := gvar_init gv) in *.
+  set (sz := Genv.init_data_list_size il) in *.
+  destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
+  destruct (Genv.store_zeros m1 b sz) as [m2|]_eqn; try congruence.
+  destruct (Genv.store_init_data_list ge m2 b 0 il) as [m3|]_eqn; try congruence.
+  destruct (Mem.drop_perm m3 b 0 sz (Genv.perm_globvar gv)) as [m4|]_eqn; try congruence.
+  intros. 
+  exploit Mem.alloc_result; eauto. intro NB. 
+  assert (NB': Mem.nextblock m4 = Mem.nextblock m1).
+  rewrite (Mem.nextblock_drop _ _ _ _ _ _ Heqo1).
+  rewrite (Genv.store_init_data_list_nextblock _ _ _ _ _ Heqo0).
+  rewrite (Genv.store_zeros_nextblock _ _ _ Heqo). 
+  auto.
+  apply IHvl with m4. 
+  (* mem_match_approx for intermediate state *)
+  red; intros.
+  unfold Genv.find_symbol in H3. simpl in H3. 
+  rewrite H0 in H3. rewrite <- NB in H3. 
+  assert (EITHER: id0 <> id /\ ga!id0 = Some il0
+       \/ id0 = id /\ il0 = il /\ gvar_readonly gv = true /\ gvar_volatile gv = false).
+  unfold ga1 in H2. destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn. 
+  rewrite PTree.gsspec in H2. destruct (peq id0 id).
+  inv H2. right. split; auto. split; auto. 
+  destruct (gvar_readonly gv); simpl in Heqb1; try discriminate.
+  destruct (gvar_volatile gv); simpl in Heqb1; try discriminate.
+  auto. auto.
+  rewrite PTree.grspec in H2. destruct (PTree.elt_eq id0 id); try discriminate.
+  auto.   
+  destruct EITHER as [[A B] | [A [B [C D]]]].
+  (* older blocks *)
+  rewrite PTree.gso in H3; auto. exploit H; eauto. intros [P [Q R]].
+  assert (b0 <> b). eapply Mem.valid_not_valid_diff; eauto with mem.
+  split. apply Genv.load_store_init_data_invariant with m; auto. 
+  intros. transitivity (Mem.load chunk m3 b0 ofs). eapply Mem.load_drop; eauto.
+  transitivity (Mem.load chunk m2 b0 ofs). eapply Genv.store_init_data_list_outside; eauto.
+  transitivity (Mem.load chunk m1 b0 ofs). eapply Genv.store_zeros_outside; eauto.
+  eapply Mem.load_alloc_unchanged; eauto.  
+  split. red. rewrite NB'.  change (Mem.valid_block m1 b0). eauto with mem.
+  intros; red; intros. elim (R ofs). 
+  eapply Mem.perm_alloc_4; eauto.
+  rewrite Genv.store_zeros_perm; [idtac|eauto].
+  rewrite Genv.store_init_data_list_perm; [idtac|eauto].
+  eapply Mem.perm_drop_4; eauto.
+  (* same block *)
+  subst id0 il0. rewrite PTree.gss in H3. injection H3; intro EQ; subst b0.
+  unfold Genv.perm_globvar in Heqo1.
+  rewrite D in Heqo1. rewrite C in Heqo1.
+  split. apply Genv.load_store_init_data_invariant with m3.
+  intros. eapply Mem.load_drop; eauto. do 3 right. auto with mem. 
+  eapply Genv.store_init_data_list_charact; eauto. 
+  split. red. rewrite NB'. change (Mem.valid_block m1 b). eauto with mem.
+  intros; red; intros. 
+  assert (0 <= ofs < sz).
+    eapply Mem.perm_alloc_3; eauto.
+    rewrite Genv.store_zeros_perm; [idtac|eauto].
+    rewrite Genv.store_init_data_list_perm; [idtac|eauto].
+    eapply Mem.perm_drop_4; eauto.
+  assert (PO: perm_order Readable Writable).
+    eapply Mem.perm_drop_2; eauto. 
+  inv PO. 
+  (* nextvar hyp *)
+  simpl. rewrite NB'. rewrite (Mem.nextblock_alloc _ _ _ _ _ Heqp).
+  unfold block in *; omega.
+  (* alloc vars hyp *)
+  auto.
+Qed.
+
+Theorem mem_match_approx_init:
+  forall m, Genv.init_mem prog = Some m -> mem_match_approx m.
+Proof.
+  intros. unfold Genv.init_mem in H. 
+  eapply mem_match_approx_alloc_variables; eauto.
+(* mem_match_approx on empty list *)
+  red; intros. rewrite PTree.gempty in H0. discriminate.
+(* nextvar *)
+  rewrite Genv.add_functions_nextvar. auto.
+Qed.
+********************************)
+
 End ANALYSIS.
 
 (** * Correctness of the code transformation *)
@@ -132,13 +434,6 @@ End ANALYSIS.
 (** We now show that the transformed code after constant propagation
   has the same semantics as the original code. *)
 
-Section PRESERVATION.
-
-Variable prog: program.
-Let tprog := transf_program prog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
@@ -156,24 +451,24 @@ Qed.
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef f).
+  Genv.find_funct tge v = Some (transf_fundef gapp f).
 Proof.  
   intros.
-  exact (Genv.find_funct_transf transf_fundef _ _ H).
+  exact (Genv.find_funct_transf (transf_fundef gapp) _ _ H).
 Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (transf_fundef f).
+  Genv.find_funct_ptr tge b = Some (transf_fundef gapp f).
 Proof.  
   intros. 
-  exact (Genv.find_funct_ptr_transf transf_fundef _ _ H).
+  exact (Genv.find_funct_ptr_transf (transf_fundef gapp) _ _ H).
 Qed.
 
 Lemma sig_function_translated:
   forall f,
-  funsig (transf_fundef f) = funsig f.
+  funsig (transf_fundef gapp f) = funsig f.
 Proof.
   intros. destruct f; reflexivity.
 Qed.
@@ -209,17 +504,17 @@ Qed.
 
 Lemma transf_ros_correct:
   forall sp ros rs rs' f approx,
-  regs_match_approx ge sp approx rs ->
+  regs_match_approx sp approx rs ->
   find_function ge ros rs = Some f ->
   regs_lessdef rs rs' ->
-  find_function tge (transf_ros approx ros) rs' = Some (transf_fundef f).
+  find_function tge (transf_ros approx ros) rs' = Some (transf_fundef gapp f).
 Proof.
   intros. destruct ros; simpl in *.
   generalize (H r); intro MATCH. generalize (H1 r); intro LD.
   destruct (rs#r); simpl in H0; try discriminate.
   destruct (Int.eq_dec i Int.zero); try discriminate.
   inv LD. 
-  assert (find_function tge (inl _ r) rs' = Some (transf_fundef f)).
+  assert (find_function tge (inl _ r) rs' = Some (transf_fundef gapp f)).
     simpl. rewrite <- H4. simpl. rewrite dec_eq_true. apply function_ptr_translated. auto.
   destruct (D.get r approx); auto.
   predSpec Int.eq Int.eq_spec i0 Int.zero; intros; auto.
@@ -230,6 +525,20 @@ Proof.
   apply function_ptr_translated; auto.
 Qed.
 
+Lemma const_for_result_correct:
+  forall a op sp v m,
+  const_for_result a = Some op ->
+  val_match_approx ge sp a v ->
+  eval_operation tge sp op nil m = Some v.
+Proof.
+  unfold const_for_result; intros. 
+  destruct a; inv H; simpl in H0.
+  simpl. congruence.
+  destruct (generate_float_constants tt); inv H2.  simpl. congruence.
+  simpl. subst v. unfold symbol_address. rewrite symbols_preserved. auto.
+  simpl. congruence.
+Qed.
+
 (** The proof of semantic preservation is a simulation argument
   based on diagrams of the following form:
 <<
@@ -259,29 +568,32 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop :=
    match_stackframe_intro:
       forall res sp pc rs f rs',
       regs_lessdef rs rs' ->
-      (forall v, regs_match_approx ge sp (analyze f)!!pc (rs#res <- v)) ->
+      (forall v, regs_match_approx sp (analyze gapp f)!!pc (rs#res <- v)) ->
     match_stackframes
         (Stackframe res f sp pc rs)
-        (Stackframe res (transf_function f) sp pc rs').
+        (Stackframe res (transf_function gapp f) sp pc rs').
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
       forall s sp pc rs m f s' rs' m'
-           (MATCH: regs_match_approx ge sp (analyze f)!!pc rs)
+           (MATCH: regs_match_approx sp (analyze gapp f)!!pc rs)
+           (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
            (REGS: regs_lessdef rs rs')
            (MEM: Mem.extends m m'),
       match_states (State s f sp pc rs m)
-                   (State s' (transf_function f) sp pc rs' m')
+                   (State s' (transf_function gapp f) sp pc rs' m')
   | match_states_call:
       forall s f args m s' args' m'
+           (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
            (ARGS: Val.lessdef_list args args')
            (MEM: Mem.extends m m'),
       match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef f) args' m')
+                   (Callstate s' (transf_fundef gapp f) args' m')
   | match_states_return:
       forall s v m s' v' m'
+           (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
            (RES: Val.lessdef v v')
            (MEM: Mem.extends m m'),
@@ -292,7 +604,7 @@ Inductive match_states: state -> state -> Prop :=
 Ltac TransfInstr :=
   match goal with
   | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr));
+      cut ((transf_function gapp f).(fn_code)!pc = Some(transf_instr gapp (analyze gapp f)!!pc instr));
       [ simpl transf_instr
       | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
         unfold option_map; rewrite H1; reflexivity ]
@@ -310,7 +622,7 @@ Proof.
   induction 1; intros; inv MS.
 
   (* Inop *)
-  exists (State s' (transf_function f) sp pc' rs' m'); split.
+  exists (State s' (transf_function gapp f) sp pc' rs' m'); split.
   TransfInstr; intro. eapply exec_Inop; eauto.
   econstructor; eauto.
   eapply analyze_correct_1 with (pc := pc); eauto.
@@ -318,70 +630,73 @@ Proof.
   unfold transfer; rewrite H. auto.
 
   (* Iop *)
-  assert (MATCH': regs_match_approx ge sp (analyze f) # pc' rs # res <- v).
+  TransfInstr.
+  set (a := eval_static_operation op (approx_regs (analyze gapp f)#pc args)).
+  assert (VMATCH: val_match_approx ge sp a v).  
+    eapply eval_static_operation_correct; eauto.
+    apply approx_regs_val_list; auto.
+  assert (MATCH': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v).
     eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
     unfold transfer; rewrite H. 
     apply regs_match_approx_update; auto. 
-    eapply eval_static_operation_correct; eauto.
-    apply approx_regs_val_list; auto.
-  TransfInstr.
-  exploit eval_static_operation_correct; eauto. eapply approx_regs_val_list; eauto. intros VM.
-  destruct (eval_static_operation op (approx_regs (analyze f) # pc args)); intros; simpl in VM.
-  (* Novalue *)
-  contradiction.
-  (* Unknown *)
+  destruct (const_for_result a) as [cop|]_eqn; intros.
+  (* constant is propagated *)
+  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v) m'); split.
+  eapply exec_Iop; eauto. 
+  eapply const_for_result_correct; eauto.
+  econstructor; eauto. 
+  apply set_reg_lessdef; auto.
+  (* operator is strength-reduced *)
   exploit op_strength_reduction_correct. eexact MATCH. reflexivity. eauto. 
-  destruct (op_strength_reduction op args (approx_regs (analyze f) # pc args)) as [op' args'].
+  destruct (op_strength_reduction op args (approx_regs (analyze gapp f) # pc args)) as [op' args'].
   intros [v' [EV' LD']].
   assert (EV'': exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v'').
-    eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto.
+  eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto.
   destruct EV'' as [v'' [EV'' LD'']].
-  exists (State s' (transf_function f) sp pc' (rs'#res <- v'') m'); split.
+  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v'') m'); split.
   econstructor. eauto. rewrite <- EV''. apply eval_operation_preserved. exact symbols_preserved.
   econstructor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
-  (* I i *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vint i)) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
-  (* F *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vfloat f0)) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
-  (* G *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (symbol_address tge i i0)) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
-  unfold symbol_address. rewrite symbols_preserved; auto. 
-  (* S *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Val.add sp (Vint i))) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
 
   (* Iload *)
   TransfInstr. 
-  generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs
-                  MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)).
-  destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args'].
-  intros P Q. rewrite H0 in P.
+  set (ap1 := eval_static_addressing addr
+               (approx_regs (analyze gapp f) # pc args)).
+  set (ap2 := eval_static_load gapp chunk ap1).
+  assert (VM1: val_match_approx ge sp ap1 a).
+    eapply eval_static_addressing_correct; eauto.
+    eapply approx_regs_val_list; eauto.
+  assert (VM2: val_match_approx ge sp ap2 v).
+    eapply eval_static_load_sound; eauto.
+  assert (MATCH': regs_match_approx sp (analyze gapp f) # pc' rs # dst <- v).
+    eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
+    unfold transfer; rewrite H. 
+    apply regs_match_approx_update; auto. 
+  destruct (const_for_result ap2) as [cop|]_eqn; intros.
+  (* constant-propagated *)
+  exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v) m'); split.
+  eapply exec_Iop; eauto. eapply const_for_result_correct; eauto.
+  econstructor; eauto. apply set_reg_lessdef; auto.
+  (* strength-reduced *)
+  generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
+                  MATCH addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+  destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args'].
+  rewrite H0. intros P.
   assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
     eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto.
   destruct ADDR' as [a' [A B]].
   assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
     rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
   exploit Mem.loadv_extends; eauto. intros [v' [D E]].
-  exists (State s' (transf_function f) sp pc' (rs'#dst <- v') m'); split.
+  exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v') m'); split.
   eapply exec_Iload; eauto.
   econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. simpl; auto.
   apply set_reg_lessdef; auto. 
 
   (* Istore *)
   TransfInstr.
-  generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs
-                  MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)).
-  destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args'].
+  generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
+                  MATCH addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+  destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args'].
   intros P Q. rewrite H0 in P.
   assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
     eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto.
@@ -389,11 +704,12 @@ Proof.
   assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
     rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
   exploit Mem.storev_extends; eauto. intros [m2' [D E]].
-  exists (State s' (transf_function f) sp pc' rs' m2'); split.
+  exists (State s' (transf_function gapp f) sp pc' rs' m2'); split.
   eapply exec_Istore; eauto.
   econstructor; eauto. 
   eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. auto. 
+  eapply mem_match_approx_store; eauto.
 
   (* Icall *)
   exploit transf_ros_correct; eauto. intro FIND'.
@@ -413,18 +729,20 @@ Proof.
   TransfInstr; intro.
   econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
-  constructor; auto. apply regs_lessdef_regs; auto. 
+  constructor; auto. 
+  eapply mem_match_approx_free; eauto.
+  apply regs_lessdef_regs; auto. 
 
   (* Ibuiltin *)
 Opaque builtin_strength_reduction.
-  destruct (builtin_strength_reduction ef args (approx_regs (analyze f)#pc args)) as [ef' args']_eqn.
-  generalize (builtin_strength_reduction_correct ge sp (analyze f)!!pc rs
-                  MATCH ef args (approx_regs (analyze f) # pc args) _ _ _ _ (refl_equal _) H0).
+  destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args']_eqn.
+  generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
+                  MATCH ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0).
   rewrite Heqp. intros P.
   exploit external_call_mem_extends; eauto. 
   instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto.
   intros [v' [m2' [A [B [C D]]]]].
-  exists (State s' (transf_function f) sp pc' (rs'#res <- v') m2'); split.
+  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v') m2'); split.
   eapply exec_Ibuiltin. TransfInstr. rewrite Heqp. eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
@@ -432,16 +750,17 @@ Opaque builtin_strength_reduction.
   eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
+  eapply mem_match_approx_extcall; eauto. 
   apply set_reg_lessdef; auto.
 
   (* Icond *)
   TransfInstr. 
-  generalize (cond_strength_reduction_correct ge sp (analyze f)#pc rs m
-                    MATCH cond args (approx_regs (analyze f) # pc args) (refl_equal _)).
-  destruct (cond_strength_reduction cond args (approx_regs (analyze f) # pc args)) as [cond' args'].
+  generalize (cond_strength_reduction_correct ge sp (analyze gapp f)#pc rs m
+                    MATCH cond args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+  destruct (cond_strength_reduction cond args (approx_regs (analyze gapp f) # pc args)) as [cond' args'].
   intros EV1. 
-  exists (State s' (transf_function f) sp (if b then ifso else ifnot) rs' m'); split. 
-  destruct (eval_static_condition cond (approx_regs (analyze f) # pc args)) as []_eqn.
+  exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. 
+  destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) as []_eqn.
   assert (eval_condition cond rs ## args m = Some b0).
     eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto.
   assert (b = b0) by congruence. subst b0.
@@ -453,14 +772,14 @@ Opaque builtin_strength_reduction.
   unfold transfer; rewrite H. auto. 
 
   (* Ijumptable *)
-  assert (A: (fn_code (transf_function f))!pc = Some(Ijumptable arg tbl)
-             \/ (fn_code (transf_function f))!pc = Some(Inop pc')).
-  TransfInstr. destruct (approx_reg (analyze f) # pc arg) as []_eqn; auto.
+  assert (A: (fn_code (transf_function gapp f))!pc = Some(Ijumptable arg tbl)
+             \/ (fn_code (transf_function gapp f))!pc = Some(Inop pc')).
+  TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) as []_eqn; auto.
   generalize (MATCH arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. 
   simpl. intro EQ; inv EQ. rewrite H1. auto.
   assert (B: rs'#arg = Vint n).
   generalize (REGS arg); intro LD; inv LD; congruence.
-  exists (State s' (transf_function f) sp pc' rs' m'); split.
+  exists (State s' (transf_function gapp f) sp pc' rs' m'); split.
   destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. 
   econstructor; eauto.
   eapply analyze_correct_1; eauto.
@@ -472,6 +791,7 @@ Opaque builtin_strength_reduction.
   exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split.
   eapply exec_Ireturn; eauto. TransfInstr; auto.
   constructor; auto.
+  eapply mem_match_approx_free; eauto.
   destruct or; simpl; auto. 
 
   (* internal function *)
@@ -482,6 +802,7 @@ Opaque builtin_strength_reduction.
   eapply exec_function_internal; simpl; eauto.
   simpl. econstructor; eauto.
   apply analyze_correct_3; auto.
+  eapply mem_match_approx_alloc; eauto.
   apply init_regs_lessdef; auto.
 
   (* external function *)
@@ -492,6 +813,7 @@ Opaque builtin_strength_reduction.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
+  eapply mem_match_approx_extcall; eauto.
 
   (* return *)
   inv H3. inv H1. 
@@ -506,14 +828,16 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef f) nil m0); split.
+  exists (Callstate nil (transf_fundef gapp 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 <- H3. apply sig_function_translated.
-  constructor. constructor. constructor. apply Mem.extends_refl.
+  constructor. 
+  eapply mem_match_approx_init; eauto.
+  constructor. constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/Inlining.v b/backend/Inlining.v
new file mode 100644
index 0000000..406447b
--- /dev/null
+++ b/backend/Inlining.v
@@ -0,0 +1,477 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** RTL function inlining *)
+
+Require Import Coqlib.
+Require Import Wfsimpl.
+Require Import Errors.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+
+Ltac xomega := unfold Plt, Ple in *; zify; omega.
+
+(** ** Environment of inlinable functions *)
+
+(** We maintain a mapping from function names to their definitions.
+  In this mapping, we only include functions that are eligible for
+  inlining, as determined by the external heuristic
+  [should_inline]. *)
+
+Definition funenv : Type := PTree.t function.
+
+Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv.
+
+Parameter should_inline: ident -> function -> bool.
+
+Definition add_fundef (fenv: funenv) (idf: ident * fundef) : funenv :=
+  match idf with
+  | (id, External ef) =>
+      PTree.remove id fenv
+  | (id, Internal f) =>
+      if should_inline id f
+      then PTree.set id f fenv
+      else PTree.remove id fenv
+  end.
+
+Definition remove_vardef (fenv: funenv) (idv: ident * globvar unit) : funenv :=
+  PTree.remove (fst idv) fenv.
+
+Definition funenv_program (p: program) : funenv :=
+  List.fold_left remove_vardef p.(prog_vars)
+    (List.fold_left add_fundef p.(prog_funct) (PTree.empty function)).
+
+(** Resources used by a function. *)
+
+(** Maximum PC (node number) in the CFG of a function.  All nodes of
+  the CFG of [f] are between 1 and [max_pc_function f] (inclusive). *)
+
+Definition max_pc_function (f: function) :=
+  PTree.fold (fun m pc i => Pmax m pc) f.(fn_code) 1%positive.
+
+(** Maximum pseudo-register defined in a function.  All results of
+  an instruction of [f], as well as all parameters of [f], are between
+  1 and [max_def_function] (inclusive). *)
+
+Definition max_def_instr (i: instruction) :=
+  match i with
+  | Iop op args res s => res
+  | Iload chunk addr args dst s => dst
+  | Icall sg ros args res s => res
+  | Ibuiltin ef args res s => res
+  | _ => 1%positive
+  end.
+
+Definition max_def_function (f: function) :=
+  Pmax
+    (PTree.fold (fun m pc i => Pmax m (max_def_instr i)) f.(fn_code) 1%positive)
+    (List.fold_left (fun m r => Pmax m r) f.(fn_params) 1%positive).
+
+(** State monad *)
+
+(** To construct incrementally the CFG of a function after inlining,
+  we use a state monad similar to that used in module [RTLgen].
+  It records the current state of the CFG, plus counters to generate
+  fresh pseudo-registers and fresh CFG nodes.  It also records the
+  stack size needed for the inlined function. *)
+
+Record state : Type := mkstate {
+  st_nextreg: positive;                 (**r last used pseudo-register *)
+  st_nextnode: positive;                (**r last used CFG node *)
+  st_code: code;                        (**r current CFG  *)
+  st_stksize: Z                         (**r current stack size *)
+}.
+
+(** Monotone evolution of the state. *)
+
+Inductive sincr (s1 s2: state) : Prop :=
+  Sincr (NEXTREG: Ple s1.(st_nextreg) s2.(st_nextreg))
+        (NEXTNODE: Ple s1.(st_nextnode) s2.(st_nextnode))
+        (STKSIZE: s1.(st_stksize) <= s2.(st_stksize)).
+
+Remark sincr_refl: forall s, sincr s s.
+Proof.
+  intros; constructor; xomega.
+Qed.
+
+Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3.
+Proof.
+  intros. inv H; inv H0. constructor; xomega.
+Qed.
+
+(** Dependently-typed state monad, ensuring that the final state is
+  greater or equal (in the sense of predicate [sincr] above) than
+  the initial state. *)
+
+Inductive res {A: Type} {s: state}: Type := R (x: A) (s': state) (I: sincr s s').
+
+Definition mon (A: Type) : Type := forall (s: state), @res A s.
+
+(** Operations on this monad. *)
+
+Definition ret {A: Type} (x: A): mon A :=
+  fun s => R x s (sincr_refl s).
+
+Definition bind {A B: Type} (x: mon A) (f: A -> mon B): mon B :=
+  fun s1 => match x s1 with R vx s2 I1 =>
+              match f vx s2 with R vy s3 I2 =>
+                R vy s3 (sincr_trans s1 s2 s3 I1 I2)
+              end
+            end.
+
+Notation "'do' X <- A ; B" := (bind A (fun X => B))
+   (at level 200, X ident, A at level 100, B at level 200).
+
+Definition initstate :=
+  mkstate 1%positive 1%positive (PTree.empty instruction) 0.
+
+Program Definition set_instr (pc: node) (i: instruction): mon unit :=
+  fun s => 
+    R tt
+      (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize))
+      _.
+Next Obligation.
+  intros; constructor; simpl; xomega.
+Qed.
+
+Program Definition add_instr (i: instruction): mon node :=
+  fun s =>
+    let pc := Psucc s.(st_nextnode) in
+    R pc
+      (mkstate s.(st_nextreg) pc (PTree.set pc i s.(st_code)) s.(st_stksize))
+      _.
+Next Obligation.
+  intros; constructor; simpl; xomega.
+Qed.
+
+Program Definition reserve_nodes (numnodes: positive): mon positive :=
+  fun s =>
+    R s.(st_nextnode)
+      (mkstate s.(st_nextreg) (Pplus s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize))
+      _.
+Next Obligation.
+  intros; constructor; simpl; xomega.
+Qed.
+
+Program Definition reserve_regs (numregs: positive): mon positive :=
+  fun s =>
+    R s.(st_nextreg)
+      (mkstate (Pplus s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize))
+      _.
+Next Obligation.
+  intros; constructor; simpl; xomega.
+Qed.
+
+Program Definition request_stack (sz: Z): mon unit :=
+  fun s => 
+    R tt
+      (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Zmax s.(st_stksize) sz))
+      _.
+Next Obligation.
+  intros; constructor; simpl; xomega.
+Qed.
+
+Fixpoint mlist_iter2 {A B: Type} (f: A -> B -> mon unit) (l: list (A*B)): mon unit :=
+  match l with
+  | nil => ret tt
+  | (x,y) :: l' => do z <- f x y; mlist_iter2 f l'
+  end.
+
+(** ** Inlining contexts *)
+
+(** A context describes how to insert the CFG for a source function into
+  the CFG for the function after inlining:
+- a source instruction at PC [n] is relocated to PC [n + ctx.(dpc)];
+- all pseudo-registers of this instruction are shifted by [ctx.(dreg)];
+- all stack references are shifted by [ctx.(dstk)];
+- "return" instructions are transformed into "return" or "move" instructions
+  as governed by [ctx.(retinfo)].
+*)
+
+Record context: Type := mkcontext {
+  dpc: positive;                        (**r offset for PCs *)
+  dreg: positive;                       (**r offset for pseudo-regs *)
+  dstk: Z;                              (**r offset for stack references *)
+  mreg: positive;                       (**r max pseudo-reg number *)
+  mstk: Z;                              (**r original stack block size *)
+  retinfo: option(node * reg)           (**r where to branch on return *)
+                                        (**r and deposit return value *)
+}.
+
+(** The following functions "shift" (relocate) PCs, registers, operations, etc. *)
+
+Definition spc (ctx: context) (pc: node) := Pplus pc ctx.(dpc).
+
+Definition sreg (ctx: context) (r: reg) := Pplus r ctx.(dreg).
+
+Definition sregs (ctx: context) (rl: list reg) := List.map (sreg ctx) rl.
+
+Definition sros (ctx: context) (ros: reg + ident) := sum_left_map (sreg ctx) ros.
+
+Definition sop (ctx: context) (op: operation) :=
+  shift_stack_operation (Int.repr ctx.(dstk)) op.
+
+Definition saddr (ctx: context) (addr: addressing) :=
+  shift_stack_addressing (Int.repr ctx.(dstk)) addr.
+
+(** The initial context, used to copy the CFG of a toplevel function. *)
+
+Definition initcontext (dpc dreg nreg: positive) (sz: Z) :=
+  {| dpc := dpc;
+     dreg := dreg;
+     dstk := 0;
+     mreg := nreg;
+     mstk := Zmax sz 0;
+     retinfo := None |}.
+
+(** The context used to inline a call to another function. *)
+
+Definition min_alignment (sz: Z) :=
+  if zle sz 1 then 1
+  else if zle sz 2 then 2
+  else if zle sz 4 then 4 else 8.
+
+Definition callcontext (ctx: context)
+                      (dpc dreg nreg: positive) (sz: Z)
+                      (retpc: node) (retreg: reg) :=
+  {| dpc := dpc;
+     dreg := dreg;
+     dstk := align (ctx.(dstk) + ctx.(mstk)) (min_alignment sz);
+     mreg := nreg;
+     mstk := Zmax sz 0;
+     retinfo := Some (spc ctx retpc, sreg ctx retreg) |}.
+
+(** The context used to inline a tail call to another function. *)
+
+Definition tailcontext (ctx: context) (dpc dreg nreg: positive) (sz: Z) :=
+  {| dpc := dpc;
+     dreg := dreg;
+     dstk := align ctx.(dstk) (min_alignment sz);
+     mreg := nreg;
+     mstk := Zmax sz 0;
+     retinfo := ctx.(retinfo) |}.
+
+(** ** Recursive expansion and copying of a CFG *)
+
+(** Insert "move" instructions to copy the arguments of an inlined
+    function into its parameters. *)
+
+Fixpoint add_moves (srcs dsts: list reg) (succ: node): mon node :=
+  match srcs, dsts with
+  | s1 :: sl, d1 :: dl =>
+      do n <- add_instr (Iop Omove (s1 :: nil) d1 succ);
+      add_moves sl dl n
+  | _, _ =>
+      ret succ
+  end.
+
+(** To prevent infinite inlining of a recursive function, when we
+  inline the body of a function [f], this function is removed from the
+  environment of inlinable functions and therefore becomes ineligible
+  for inlining.  This decreases the size (number of entries) of the
+  environment and guarantees termination.  Inlining is, therefore,
+  presented as a well-founded recursion over the size of the environment. *)
+
+Section EXPAND_CFG.
+
+Variable fenv: funenv.
+
+(** The [rec] parameter is the recursor: [rec fenv' P ctx f] copies 
+  the body of function [f], with inline expansion within, as governed
+  by context [ctx].  It can only be called for function environments
+  [fenv'] strictly smaller than the current environment [fenv]. *)
+
+Variable rec: forall fenv', (size_fenv fenv' < size_fenv fenv)%nat -> context -> function -> mon unit.
+
+(** Given a register-or-symbol [ros], can we inline the corresponding call? *)
+
+Inductive inline_decision (ros: reg + ident) : Type :=
+  | Cannot_inline
+  | Can_inline (id: ident) (f: function) (P: ros = inr reg id) (Q: fenv!id = Some f).
+
+Program Definition can_inline (ros: reg + ident): inline_decision ros :=
+  match ros with
+  | inl r => Cannot_inline _
+  | inr id => match fenv!id with Some f => Can_inline _ id f _ _ | None => Cannot_inline _ end
+  end.
+
+(** Inlining of a call to function [f].  An appropriate context is
+  created, then the CFG of [f] is recursively copied, then moves
+  are inserted to copy the arguments of the call to the parameters of [f]. *)
+
+Definition inline_function (ctx: context) (id: ident) (f: function)
+                           (P: PTree.get id fenv = Some f)
+                           (args: list reg)
+                           (retpc: node) (retreg: reg) : mon node :=
+  let npc := max_pc_function f in
+  let nreg := max_def_function f in
+  do dpc <- reserve_nodes npc;
+  do dreg <- reserve_regs nreg;
+  let ctx' := callcontext ctx dpc dreg nreg f.(fn_stacksize) retpc retreg in 
+  do x <- rec (PTree.remove id fenv) (PTree_Properties.cardinal_remove P) ctx' f;
+  add_moves (sregs ctx args) (sregs ctx' f.(fn_params)) (spc ctx' f.(fn_entrypoint)).
+
+(** Inlining of a tail call to function [f].  Similar to [inline_function],
+  but the new context is different. *)
+
+Definition inline_tail_function (ctx: context) (id: ident) (f: function)
+                               (P: PTree.get id fenv = Some f)
+                               (args: list reg): mon node :=
+  let npc := max_pc_function f in
+  let nreg := max_def_function f in
+  do dpc <- reserve_nodes npc;
+  do dreg <- reserve_regs nreg;
+  let ctx' := tailcontext ctx dpc dreg nreg f.(fn_stacksize) in 
+  do x <- rec (PTree.remove id fenv) (PTree_Properties.cardinal_remove P) ctx' f;
+  add_moves (sregs ctx args) (sregs ctx' f.(fn_params)) (spc ctx' f.(fn_entrypoint)).
+
+(** The instruction generated for a [Ireturn] instruction found in an
+  inlined function body. *)
+
+Definition inline_return (ctx: context) (or: option reg) (retinfo: node * reg) :=
+  match retinfo, or with
+  | (retpc, retreg), Some r => Iop Omove (sreg ctx r :: nil) retreg retpc
+  | (retpc, retreg), None   => Inop retpc
+  end.
+
+(** Expansion and copying of an instruction.  For most instructions,
+  its registers and successor PC are shifted as per the context [ctx],
+  then the instruction is inserted in the final CFG at its final position
+  [spc ctx pc].  
+
+  [Icall] instructions are either replaced by a "goto" to the expansion
+  of the called function, or shifted as described above.
+
+  [Itailcall] instructions are similar, with one additional case.  If
+  the [Itailcall] occurs in the body of an inlined function, and
+  cannot be inlined itself, it must be turned into an [Icall]
+  instruction that branches to the return point of the inlined
+  function.
+
+  Finally, [Ireturn] instructions within an inlined function are
+  turned into a "move" or "goto" that stores the result, if any,
+  into the destination register, then branches back to the successor
+  of the inlined call. *)
+
+Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit :=
+  match i with
+  | Inop s =>
+      set_instr (spc ctx pc) (Inop (spc ctx s))
+  | Iop op args res s =>
+      set_instr (spc ctx pc)
+                (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s))
+  | Iload chunk addr args dst s =>
+      set_instr (spc ctx pc)
+                (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s))
+  | Istore chunk addr args src s =>
+      set_instr (spc ctx pc)
+                (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s))
+  | Icall sg ros args res s =>
+      match can_inline ros with
+      | Cannot_inline =>
+          set_instr (spc ctx pc)
+                    (Icall sg (sros ctx ros) (sregs ctx args) (sreg ctx res) (spc ctx s))
+      | Can_inline id f P Q =>
+          do n <- inline_function ctx id f Q args s res;
+          set_instr (spc ctx pc) (Inop n)
+      end
+  | Itailcall sg ros args =>
+      match can_inline ros with
+      | Cannot_inline =>
+          match ctx.(retinfo) with
+          | None =>
+              set_instr (spc ctx pc)
+                        (Itailcall sg (sros ctx ros) (sregs ctx args))
+          | Some(rpc, rreg) =>
+              set_instr (spc ctx pc)
+                        (Icall sg (sros ctx ros) (sregs ctx args) rreg rpc)
+          end
+      | Can_inline id f P Q =>
+          do n <- inline_tail_function ctx id f Q args;
+          set_instr (spc ctx pc) (Inop n)
+      end          
+  | Ibuiltin ef args res s =>
+      set_instr (spc ctx pc)
+                (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s))
+  | Icond cond args s1 s2 =>
+      set_instr (spc ctx pc)
+                (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2))
+  | Ijumptable r tbl =>
+      set_instr (spc ctx pc)
+                (Ijumptable (sreg ctx r) (List.map (spc ctx) tbl))
+  | Ireturn or =>
+      match ctx.(retinfo) with
+      | None =>
+          set_instr (spc ctx pc) (Ireturn (option_map (sreg ctx) or))
+      | Some rinfo =>
+          set_instr (spc ctx pc) (inline_return ctx or rinfo)
+      end
+  end.
+
+(** The expansion of a function [f] iteratively expands all its
+  instructions, after recording how much stack it needs. *)
+
+Definition expand_cfg_rec (ctx: context) (f: function): mon unit :=
+  do x <- request_stack (ctx.(dstk) + ctx.(mstk));
+  mlist_iter2 (expand_instr ctx) (PTree.elements f.(fn_code)).
+
+End EXPAND_CFG.
+
+(** Here we "tie the knot" of the recursion, taking the fixpoint
+  of [expand_cfg_rec]. *)
+
+Definition expand_cfg := Fixm size_fenv expand_cfg_rec.
+
+(** Start of the recursion: copy and inline function [f] in the
+  initial context. *)
+
+Definition expand_function (fenv: funenv) (f: function): mon context :=
+  let npc := max_pc_function f in
+  let nreg := max_def_function f in
+  do dpc <- reserve_nodes npc;
+  do dreg <- reserve_regs nreg;
+  let ctx := initcontext dpc dreg nreg f.(fn_stacksize) in 
+  do x <- expand_cfg fenv ctx f;
+  ret ctx.
+
+(** ** Inlining in functions and whole programs. *)
+
+Local Open Scope string_scope.
+
+(** Inlining can increase the size of the function's stack block.  We must
+  make sure that the new size does not exceed [Int.max_unsigned], otherwise
+  address computations within the stack would overflow and produce incorrect
+  results. *)
+
+Definition transf_function (fenv: funenv) (f: function) : Errors.res function :=
+  let '(R ctx s _) := expand_function fenv f initstate in
+  if zle s.(st_stksize) Int.max_unsigned then
+    OK (mkfunction f.(fn_sig) 
+                   (sregs ctx f.(fn_params))
+                   s.(st_stksize)
+                   s.(st_code)
+                   (spc ctx f.(fn_entrypoint)))
+  else
+    Error(msg "Inlining: stack too big").
+
+Definition transf_fundef (fenv: funenv) (fd: fundef) : Errors.res fundef :=
+  AST.transf_partial_fundef (transf_function fenv) fd.
+
+Definition transf_program (p: program): Errors.res program :=
+  let fenv := funenv_program p in
+  AST.transform_partial_program (transf_fundef fenv) p.
+
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
new file mode 100644
index 0000000..4212916
--- /dev/null
+++ b/backend/Inliningaux.ml
@@ -0,0 +1,18 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Camlcoq
+
+(* To be considered: heuristics based on size of function? *)
+
+let should_inline (id: AST.ident) (f: RTL.coq_function) =
+  C2C.atom_is_inline id
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
new file mode 100644
index 0000000..c62e173
--- /dev/null
+++ b/backend/Inliningproof.v
@@ -0,0 +1,1240 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** RTL function inlining: semantic preservation *)
+
+Require Import Coqlib.
+Require Import Errors.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Op.
+Require Import Registers.
+Require Import Inlining.
+Require Import Inliningspec.
+Require Import RTL.
+
+Section INLINING.
+
+Variable prog: program.
+Variable tprog: program.
+Hypothesis TRANSF: transf_program prog = OK tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+Let fenv := funenv_program prog.
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  intros. apply Genv.find_symbol_transf_partial with (transf_fundef fenv); auto.
+Qed.
+
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof.
+  intros. apply Genv.find_var_info_transf_partial with (transf_fundef fenv); auto.
+Qed.
+
+Lemma functions_translated:
+  forall (v: val) (f: fundef),
+  Genv.find_funct ge v = Some f ->
+  exists f', Genv.find_funct tge v = Some f' /\ transf_fundef fenv f = OK f'.
+Proof (Genv.find_funct_transf_partial (transf_fundef fenv) _ TRANSF).
+
+Lemma function_ptr_translated:
+  forall (b: block) (f: fundef),
+  Genv.find_funct_ptr ge b = Some f ->
+  exists f', Genv.find_funct_ptr tge b = Some f' /\ transf_fundef fenv f = OK f'.
+Proof (Genv.find_funct_ptr_transf_partial (transf_fundef fenv) _ TRANSF).
+
+Lemma sig_function_translated:
+  forall f f', transf_fundef fenv f = OK f' -> funsig f' = funsig f.
+Proof.
+  intros. destruct f; Errors.monadInv H.
+  exploit transf_function_spec; eauto. intros SP; inv SP. auto. 
+  auto.
+Qed.
+
+(** ** Properties of contexts and relocations *)
+
+Remark sreg_below_diff:
+  forall ctx r r', Ple r' ctx.(dreg) -> sreg ctx r <> r'.
+Proof.
+  intros. unfold sreg. xomega. 
+Qed.
+
+Remark context_below_diff:
+  forall ctx1 ctx2 r1 r2,
+  context_below ctx1 ctx2 -> Ple r1 ctx1.(mreg) -> sreg ctx1 r1 <> sreg ctx2 r2.
+Proof.
+  intros. red in H. unfold sreg. xomega. 
+Qed.
+
+Remark context_below_le:
+  forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Ple (sreg ctx1 r) ctx2.(dreg).
+Proof.
+  intros. red in H. unfold sreg. xomega.
+Qed.
+
+(** ** Agreement between register sets before and after inlining. *)
+
+Definition agree_regs (F: meminj) (ctx: context) (rs rs': regset) :=
+  (forall r, Ple r ctx.(mreg) -> val_inject F rs#r rs'#(sreg ctx r))
+/\(forall r, Plt ctx.(mreg) r -> rs#r = Vundef).
+
+Definition val_reg_charact (F: meminj) (ctx: context) (rs': regset) (v: val) (r: reg) :=
+  (Plt ctx.(mreg) r /\ v = Vundef) \/ (Ple r ctx.(mreg) /\ val_inject F v rs'#(sreg ctx r)).
+
+Remark Plt_Ple_dec:
+  forall p q, {Plt p q} + {Ple q p}.
+Proof.
+  intros. destruct (plt p q). left; auto. right; xomega.
+Qed.
+
+Lemma agree_val_reg_gen:
+  forall F ctx rs rs' r, agree_regs F ctx rs rs' -> val_reg_charact F ctx rs' rs#r r.
+Proof.
+  intros. destruct H as [A B].
+  destruct (Plt_Ple_dec (mreg ctx) r). 
+  left. rewrite B; auto. 
+  right. auto.
+Qed.
+
+Lemma agree_val_regs_gen:
+  forall F ctx rs rs' rl,
+  agree_regs F ctx rs rs' -> list_forall2 (val_reg_charact F ctx rs') rs##rl rl.
+Proof.
+  induction rl; intros; constructor; auto. apply agree_val_reg_gen; auto.
+Qed.
+
+Lemma agree_val_reg:
+  forall F ctx rs rs' r, agree_regs F ctx rs rs' -> val_inject F rs#r rs'#(sreg ctx r).
+Proof.
+  intros. exploit agree_val_reg_gen; eauto. instantiate (1 := r). intros [[A B] | [A B]].
+  rewrite B; auto.
+  auto.
+Qed.
+
+Lemma agree_val_regs:
+  forall F ctx rs rs' rl, agree_regs F ctx rs rs' -> val_list_inject F rs##rl rs'##(sregs ctx rl).
+Proof.
+  induction rl; intros; simpl. constructor. constructor; auto. apply agree_val_reg; auto.
+Qed.
+
+Lemma agree_set_reg:
+  forall F ctx rs rs' r v v',
+  agree_regs F ctx rs rs' ->
+  val_inject F v v' ->
+  Ple r ctx.(mreg) ->
+  agree_regs F ctx (rs#r <- v) (rs'#(sreg ctx r) <- v').
+Proof.
+  unfold agree_regs; intros. destruct H. split; intros.
+  repeat rewrite Regmap.gsspec. 
+  destruct (peq r0 r). subst r0. rewrite peq_true. auto.
+  rewrite peq_false. auto. unfold sreg; xomega. 
+  rewrite Regmap.gso. auto. xomega. 
+Qed.
+
+Lemma agree_set_reg_undef:
+  forall F ctx rs rs' r v',
+  agree_regs F ctx rs rs' ->
+  agree_regs F ctx (rs#r <- Vundef) (rs'#(sreg ctx r) <- v').
+Proof.
+  unfold agree_regs; intros. destruct H. split; intros.
+  repeat rewrite Regmap.gsspec. 
+  destruct (peq r0 r). subst r0. rewrite peq_true. auto.
+  rewrite peq_false. auto. unfold sreg; xomega.
+  rewrite Regmap.gsspec. destruct (peq r0 r); auto. 
+Qed.
+
+Lemma agree_set_reg_undef':
+  forall F ctx rs rs' r,
+  agree_regs F ctx rs rs' ->
+  agree_regs F ctx (rs#r <- Vundef) rs'.
+Proof.
+  unfold agree_regs; intros. destruct H. split; intros.
+  rewrite Regmap.gsspec. 
+  destruct (peq r0 r). subst r0. auto. auto.
+  rewrite Regmap.gsspec. destruct (peq r0 r); auto. 
+Qed.
+
+Lemma agree_regs_invariant:
+  forall F ctx rs rs1 rs2,
+  agree_regs F ctx rs rs1 ->
+  (forall r, Plt ctx.(dreg) r -> Ple r (ctx.(dreg) + ctx.(mreg)) -> rs2#r = rs1#r) ->
+  agree_regs F ctx rs rs2.
+Proof.
+  unfold agree_regs; intros. destruct H. split; intros.
+  rewrite H0. auto. unfold sreg; xomega. unfold sreg; xomega. 
+  apply H1; auto.
+Qed.
+
+Lemma agree_regs_incr:
+  forall F ctx rs1 rs2 F',
+  agree_regs F ctx rs1 rs2 ->
+  inject_incr F F' ->
+  agree_regs F' ctx rs1 rs2.
+Proof.
+  intros. destruct H. split; intros. eauto. auto. 
+Qed.
+
+Remark agree_regs_init:
+  forall F ctx rs, agree_regs F ctx (Regmap.init Vundef) rs.
+Proof.
+  intros; split; intros. rewrite Regmap.gi; auto. rewrite Regmap.gi; auto. 
+Qed.
+
+Lemma agree_regs_init_regs:
+  forall F ctx rl vl vl',
+  val_list_inject F vl vl' ->
+  (forall r, In r rl -> Ple r ctx.(mreg)) ->
+  agree_regs F ctx (init_regs vl rl) (init_regs vl' (sregs ctx rl)).
+Proof.
+  induction rl; simpl; intros.
+  apply agree_regs_init.
+  inv H. apply agree_regs_init.
+  apply agree_set_reg; auto. 
+Qed.
+
+(** ** Executing sequences of moves *)
+
+Lemma tr_moves_init_regs:
+  forall F stk f sp m ctx1 ctx2, context_below ctx1 ctx2 ->
+  forall rdsts rsrcs vl pc1 pc2 rs1,
+  tr_moves f.(fn_code) pc1 (sregs ctx1 rsrcs) (sregs ctx2 rdsts) pc2 ->
+  (forall r, In r rdsts -> Ple r ctx2.(mreg)) ->
+  list_forall2 (val_reg_charact F ctx1 rs1) vl rsrcs ->
+  exists rs2,
+    star step tge (State stk f sp pc1 rs1 m)
+               E0 (State stk f sp pc2 rs2 m)
+  /\ agree_regs F ctx2 (init_regs vl rdsts) rs2
+  /\ forall r, Ple r ctx2.(dreg) -> rs2#r = rs1#r.
+Proof.
+  induction rdsts; simpl; intros.
+(* rdsts = nil *)
+  inv H0. exists rs1; split. apply star_refl. split. apply agree_regs_init. auto.
+(* rdsts = a :: rdsts *)
+  inv H2. inv H0. 
+  exists rs1; split. apply star_refl. split. apply agree_regs_init. auto.
+  simpl in H0. inv H0.
+  exploit IHrdsts; eauto. intros [rs2 [A [B C]]].
+  exists (rs2#(sreg ctx2 a) <- (rs2#(sreg ctx1 b1))).
+  split. eapply star_right. eauto. eapply exec_Iop; eauto. traceEq.
+  split. destruct H3 as [[P Q] | [P Q]].
+  subst a1. eapply agree_set_reg_undef; eauto.
+  eapply agree_set_reg; eauto. rewrite C; auto. apply context_below_le; auto.
+  intros. rewrite Regmap.gso. auto. apply sym_not_equal. eapply sreg_below_diff; eauto.
+  destruct H2; discriminate.
+Qed.
+
+(** ** Memory invariants *)
+
+(** A stack location is private if it is not the image of a valid
+   location and we have full rights on it. *)
+
+Definition loc_private (F: meminj) (m m': mem) (sp: block) (ofs: Z) : Prop :=
+  Mem.perm m' sp ofs Cur Freeable /\
+  (forall b delta, F b = Some(sp, delta) -> ~Mem.perm m b (ofs - delta) Max Nonempty).
+
+(** Likewise, for a range of locations. *)
+
+Definition range_private (F: meminj) (m m': mem) (sp: block) (lo hi: Z) : Prop :=
+  forall ofs, lo <= ofs < hi -> loc_private F m m' sp ofs.
+
+Lemma range_private_invariant:
+  forall F m m' sp lo hi F1 m1 m1',
+  range_private F m m' sp lo hi ->
+  (forall b delta ofs,
+      F1 b = Some(sp, delta) ->
+      Mem.perm m1 b ofs Max Nonempty ->
+      lo <= ofs + delta < hi ->
+      F b = Some(sp, delta) /\ Mem.perm m b ofs Max Nonempty) ->
+  (forall ofs, Mem.perm m' sp ofs Cur Freeable -> Mem.perm m1' sp ofs Cur Freeable) ->
+  range_private F1 m1 m1' sp lo hi.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A B]. split; auto.
+  intros; red; intros. exploit H0; eauto. omega. intros [P Q]. 
+  eelim B; eauto.
+Qed.
+
+Lemma range_private_perms:
+  forall F m m' sp lo hi,
+  range_private F m m' sp lo hi ->
+  Mem.range_perm m' sp lo hi Cur Freeable.
+Proof.
+  intros; red; intros. eapply H; eauto.
+Qed.
+
+Lemma range_private_alloc_left:
+  forall F m m' sp' base hi sz m1 sp F1,
+  range_private F m m' sp' base hi ->
+  Mem.alloc m 0 sz = (m1, sp) ->
+  F1 sp = Some(sp', base) ->
+  (forall b, b <> sp -> F1 b = F b) ->
+  range_private F1 m1 m' sp' (base + Zmax sz 0) hi.
+Proof.
+  intros; red; intros. 
+  exploit (H ofs). generalize (Zmax2 sz 0). omega. intros [A B].
+  split; auto. intros; red; intros.
+  exploit Mem.perm_alloc_inv; eauto.
+  destruct (zeq b sp); intros.
+  subst b. rewrite H1 in H4; inv H4. 
+  rewrite Zmax_spec in H3. destruct (zlt 0 sz); omega.
+  rewrite H2 in H4; auto. eelim B; eauto. 
+Qed.
+
+Lemma range_private_free_left:
+  forall F m m' sp base sz hi b m1,
+  range_private F m m' sp (base + Zmax sz 0) hi ->
+  Mem.free m b 0 sz = Some m1 ->
+  F b = Some(sp, base) ->
+  Mem.inject F m m' ->
+  range_private F m1 m' sp base hi.
+Proof.
+  intros; red; intros. 
+  destruct (zlt ofs (base + Zmax sz 0)).
+  red; split. 
+  replace ofs with ((ofs - base) + base) by omega.
+  eapply Mem.perm_inject; eauto.
+  eapply Mem.free_range_perm; eauto.
+  rewrite Zmax_spec in z. destruct (zlt 0 sz); omega. 
+  intros; red; intros. destruct (eq_block b b0).
+  subst b0. rewrite H1 in H4; inv H4.
+  eelim Mem.perm_free_2; eauto. rewrite Zmax_spec in z. destruct (zlt 0 sz); omega.
+  exploit Mem.mi_no_overlap; eauto. 
+  apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
+  eapply Mem.free_range_perm. eauto. 
+  instantiate (1 := ofs - base). rewrite Zmax_spec in z. destruct (zlt 0 sz); omega.
+  eapply Mem.perm_free_3; eauto. 
+  intros [A | A]. congruence. omega. 
+
+  exploit (H ofs). omega. intros [A B]. split. auto.
+  intros; red; intros. eelim B; eauto. eapply Mem.perm_free_3; eauto.
+Qed.
+
+Lemma range_private_extcall:
+  forall F F' m1 m2 m1' m2' sp base hi,
+  range_private F m1 m1' sp base hi ->
+  (forall b ofs p,
+     Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
+  mem_unchanged_on (loc_out_of_reach F m1) m1' m2' ->
+  Mem.inject F m1 m1' ->
+  inject_incr F F' ->
+  inject_separated F F' m1 m1' ->
+  Mem.valid_block m1' sp ->
+  range_private F' m2 m2' sp base hi.
+Proof.
+  intros until hi; intros RP PERM UNCH INJ INCR SEP VB.
+  red; intros. exploit RP; eauto. intros [A B].
+  destruct UNCH as [U1 U2].
+  split. auto. 
+  intros. red in SEP. destruct (F b) as [[sp1 delta1] |]_eqn.
+  exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. 
+  red; intros; eelim B; eauto. eapply PERM; eauto. 
+  red. destruct (zlt b (Mem.nextblock m1)); auto. 
+  exploit Mem.mi_freeblocks; eauto. congruence.
+  exploit SEP; eauto. tauto. 
+Qed.
+
+(** ** Relating global environments *)
+
+Inductive match_globalenvs (F: meminj) (bound: Z): Prop :=
+  | mk_match_globalenvs
+      (POS: bound > 0)
+      (DOMAIN: forall b, b < bound -> F b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
+      (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+
+Lemma find_function_agree:
+  forall ros rs fd F ctx rs' bound,
+  find_function ge ros rs = Some fd ->
+  agree_regs F ctx rs rs' ->
+  match_globalenvs F bound ->
+  exists fd',
+  find_function tge (sros ctx ros) rs' = Some fd' /\ transf_fundef fenv fd = OK fd'.
+Proof.
+  intros. destruct ros as [r | id]; simpl in *.
+  (* register *)
+  assert (rs'#(sreg ctx r) = rs#r).
+    exploit Genv.find_funct_inv; eauto. intros [b EQ].
+    assert (A: val_inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto.
+    rewrite EQ in A; inv A.
+    inv H1. rewrite DOMAIN in H5. inv H5. auto. 
+    rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H.
+    exploit Genv.find_funct_ptr_negative. unfold ge in H; eexact H. omega.
+  rewrite H2. eapply functions_translated; eauto.
+  (* symbol *)
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+(** ** Relating stacks *)
+
+Inductive match_stacks (F: meminj) (m m': mem):
+             list stackframe -> list stackframe -> block -> Prop :=
+  | match_stacks_nil: forall bound1 bound
+        (MG: match_globalenvs F bound1)
+        (BELOW: bound1 <= bound),
+      match_stacks F m m' nil nil bound
+  | match_stacks_cons: forall res f sp pc rs stk f' sp' rs' stk' bound ctx
+        (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
+        (FB: tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code))
+        (AG: agree_regs F ctx rs rs')
+        (SP: F sp = Some(sp', ctx.(dstk)))
+        (PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
+        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
+        (RES: Ple res ctx.(mreg))
+        (BELOW: sp' < bound),
+      match_stacks F m m'
+                   (Stackframe res f (Vptr sp Int.zero) pc rs :: stk)
+                   (Stackframe (sreg ctx res) f' (Vptr sp' Int.zero) (spc ctx pc) rs' :: stk')
+                   bound
+  | match_stacks_untailcall: forall stk res f' sp' rpc rs' stk' bound ctx
+        (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
+        (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
+        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
+        (RET: ctx.(retinfo) = Some (rpc, res))
+        (BELOW: sp' < bound),
+      match_stacks F m m'
+                   stk
+                   (Stackframe res f' (Vptr sp' Int.zero) rpc rs' :: stk')
+                   bound
+
+with match_stacks_inside (F: meminj) (m m': mem):
+        list stackframe -> list stackframe -> function -> context -> block -> regset -> Prop :=
+  | match_stacks_inside_base: forall stk stk' f' ctx sp' rs'
+        (MS: match_stacks F m m' stk stk' sp')
+        (RET: ctx.(retinfo) = None)
+        (DSTK: ctx.(dstk) = 0),
+      match_stacks_inside F m m' stk stk' f' ctx sp' rs'
+  | match_stacks_inside_inlined: forall res f sp pc rs stk stk' f' ctx sp' rs' ctx'
+        (MS: match_stacks_inside F m m' stk stk' f' ctx' sp' rs')
+        (FB: tr_funbody fenv f'.(fn_stacksize) ctx' f f'.(fn_code))
+        (AG: agree_regs F ctx' rs rs')
+        (SP: F sp = Some(sp', ctx'.(dstk)))
+        (PAD: range_private F m m' sp' (ctx'.(dstk) + ctx'.(mstk)) ctx.(dstk))
+        (RES: Ple res ctx'.(mreg))
+        (RET: ctx.(retinfo) = Some (spc ctx' pc, sreg ctx' res))
+        (BELOW: context_below ctx' ctx)
+        (SBELOW: context_stack_call ctx' ctx),
+      match_stacks_inside F m m' (Stackframe res f (Vptr sp Int.zero) pc rs :: stk)
+                                 stk' f' ctx sp' rs'.
+
+(** Properties of match_stacks *)
+
+Section MATCH_STACKS.
+
+Variable F: meminj.
+Variables m m': mem.
+
+Lemma match_stacks_globalenvs:
+  forall stk stk' bound,
+  match_stacks F m m' stk stk' bound -> exists b, match_globalenvs F b
+with match_stacks_inside_globalenvs:
+  forall stk stk' f ctx sp rs', 
+  match_stacks_inside F m m' stk stk' f ctx sp rs' -> exists b, match_globalenvs F b.
+Proof.
+  induction 1; eauto.
+  induction 1; eauto.
+Qed.
+
+Lemma match_globalenvs_preserves_globals:
+  forall b, match_globalenvs F b -> meminj_preserves_globals ge F.
+Proof.
+  intros. inv H. red. split. eauto. split. eauto.
+  intros. symmetry. eapply IMAGE; eauto.
+Qed. 
+
+Lemma match_stacks_inside_globals:
+  forall stk stk' f ctx sp rs', 
+  match_stacks_inside F m m' stk stk' f ctx sp rs' -> meminj_preserves_globals ge F.
+Proof.
+  intros. exploit match_stacks_inside_globalenvs; eauto. intros [b A]. 
+  eapply match_globalenvs_preserves_globals; eauto.
+Qed.
+
+Lemma match_stacks_bound:
+  forall stk stk' bound bound1,
+  match_stacks F m m' stk stk' bound ->
+  bound <= bound1 ->
+  match_stacks F m m' stk stk' bound1.
+Proof.
+  intros. inv H.
+  apply match_stacks_nil with bound0. auto. omega.
+  eapply match_stacks_cons; eauto. omega.
+  eapply match_stacks_untailcall; eauto. omega. 
+Qed. 
+
+Variable F1: meminj.
+Variables m1 m1': mem.
+Hypothesis INCR: inject_incr F F1.
+
+Lemma match_stacks_invariant:
+  forall stk stk' bound, match_stacks F m m' stk stk' bound ->
+  forall (INJ: forall b1 b2 delta, 
+               F1 b1 = Some(b2, delta) -> b2 < bound -> F b1 = Some(b2, delta))
+         (PERM1: forall b1 b2 delta ofs,
+               F1 b1 = Some(b2, delta) -> b2 < bound ->
+               Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
+         (PERM2: forall b ofs, b < bound ->
+               Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
+         (PERM3: forall b ofs k p, b < bound ->
+               Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p),
+  match_stacks F1 m1 m1' stk stk' bound
+
+with match_stacks_inside_invariant:
+  forall stk stk' f' ctx sp' rs1, 
+  match_stacks_inside F m m' stk stk' f' ctx sp' rs1 ->
+  forall rs2
+         (RS: forall r, Ple r ctx.(dreg) -> rs2#r = rs1#r)
+         (INJ: forall b1 b2 delta, 
+               F1 b1 = Some(b2, delta) -> b2 <= sp' -> F b1 = Some(b2, delta))
+         (PERM1: forall b1 b2 delta ofs,
+               F1 b1 = Some(b2, delta) -> b2 <= sp' ->
+               Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
+         (PERM2: forall b ofs, b <= sp' ->
+               Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
+         (PERM3: forall b ofs k p, b <= sp' ->
+               Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p),
+  match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs2.
+
+Proof.
+  induction 1; intros.
+  (* nil *)
+  apply match_stacks_nil with (bound1 := bound1).
+  inv MG. constructor; auto. 
+  intros. apply IMAGE with delta. eapply INJ; eauto. omega. auto. 
+  omega.
+  (* cons *)
+  apply match_stacks_cons with (ctx := ctx); auto.
+  eapply match_stacks_inside_invariant; eauto.
+  intros; eapply INJ; eauto; omega.
+  intros; eapply PERM1; eauto; omega.
+  intros; eapply PERM2; eauto; omega.
+  intros; eapply PERM3; eauto; omega.
+  eapply agree_regs_incr; eauto.
+  eapply range_private_invariant; eauto. 
+  (* untailcall *)
+  apply match_stacks_untailcall with (ctx := ctx); auto. 
+  eapply match_stacks_inside_invariant; eauto.
+  intros; eapply INJ; eauto; omega.
+  intros; eapply PERM1; eauto; omega.
+  intros; eapply PERM2; eauto; omega.
+  intros; eapply PERM3; eauto; omega.
+  eapply range_private_invariant; eauto. 
+
+  induction 1; intros.
+  (* base *)
+  eapply match_stacks_inside_base; eauto.
+  eapply match_stacks_invariant; eauto. 
+  intros; eapply INJ; eauto; omega.
+  intros; eapply PERM1; eauto; omega.
+  intros; eapply PERM2; eauto; omega.
+  intros; eapply PERM3; eauto; omega.
+  (* inlined *)
+  apply match_stacks_inside_inlined with (ctx' := ctx'); auto. 
+  apply IHmatch_stacks_inside; auto.
+  intros. apply RS. red in BELOW. xomega. 
+  apply agree_regs_incr with F; auto. 
+  apply agree_regs_invariant with rs'; auto. 
+  intros. apply RS. red in BELOW. xomega. 
+  eapply range_private_invariant; eauto.
+    intros. split. eapply INJ; eauto. omega. eapply PERM1; eauto. omega.
+    intros. eapply PERM2; eauto. omega.
+Qed.
+
+Lemma match_stacks_empty:
+  forall stk stk' bound,
+  match_stacks F m m' stk stk' bound -> stk = nil -> stk' = nil
+with match_stacks_inside_empty:
+  forall stk stk' f ctx sp rs,
+  match_stacks_inside F m m' stk stk' f ctx sp rs -> stk = nil -> stk' = nil /\ ctx.(retinfo) = None.
+Proof.
+  induction 1; intros.
+  auto.
+  discriminate.
+  exploit match_stacks_inside_empty; eauto. intros [A B]. congruence.
+  induction 1; intros.
+  split. eapply match_stacks_empty; eauto. auto.
+  discriminate.
+Qed.
+
+End MATCH_STACKS.
+
+(** Preservation by assignment to a register *)
+
+Lemma match_stacks_inside_set_reg:
+  forall F m m' stk stk' f' ctx sp' rs' r v, 
+  match_stacks_inside F m m' stk stk' f' ctx sp' rs' ->
+  match_stacks_inside F m m' stk stk' f' ctx sp' (rs'#(sreg ctx r) <- v).
+Proof.
+  intros. eapply match_stacks_inside_invariant; eauto. 
+  intros. apply Regmap.gso. unfold sreg. xomega. 
+Qed.
+
+(** Preservation by a memory store *)
+
+Lemma match_stacks_inside_store:
+  forall F m m' stk stk' f' ctx sp' rs' chunk b ofs v m1 chunk' b' ofs' v' m1', 
+  match_stacks_inside F m m' stk stk' f' ctx sp' rs' ->
+  Mem.store chunk m b ofs v = Some m1 ->
+  Mem.store chunk' m' b' ofs' v' = Some m1' ->
+  match_stacks_inside F m1 m1' stk stk' f' ctx sp' rs'.
+Proof.
+  intros. 
+  eapply match_stacks_inside_invariant; eauto with mem.
+Qed.
+
+(** Preservation by an allocation *)
+
+Lemma match_stacks_inside_alloc_left:
+  forall F m m' stk stk' f' ctx sp' rs',
+  match_stacks_inside F m m' stk stk' f' ctx sp' rs' ->
+  forall sz m1 b F1 delta,
+  Mem.alloc m 0 sz = (m1, b) ->
+  inject_incr F F1 ->
+  F1 b = Some(sp', delta) ->
+  (forall b1, b1 <> b -> F1 b1 = F b1) ->
+  delta >= ctx.(dstk) ->
+  match_stacks_inside F1 m1 m' stk stk' f' ctx sp' rs'.
+Proof.
+  induction 1; intros.
+  (* base *)
+  eapply match_stacks_inside_base; eauto. 
+  eapply match_stacks_invariant; eauto.
+  intros. destruct (eq_block b1 b).
+  subst b1. rewrite H1 in H4; inv H4. omegaContradiction.
+  rewrite H2 in H4; auto. 
+  intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b1 b); intros; auto.
+  subst b1. rewrite H1 in H4. inv H4. omegaContradiction.
+  (* inlined *)
+  eapply match_stacks_inside_inlined; eauto. 
+  eapply IHmatch_stacks_inside; eauto. destruct SBELOW. omega. 
+  eapply agree_regs_incr; eauto.
+  eapply range_private_invariant; eauto. 
+  intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b); intros.
+  subst b0. rewrite H2 in H5; inv H5. omegaContradiction. 
+  rewrite H3 in H5; auto. 
+Qed.
+
+(** Preservation by freeing *)
+
+Lemma match_stacks_free_left:
+  forall F m m' stk stk' sp b lo hi m1,
+  match_stacks F m m' stk stk' sp ->
+  Mem.free m b lo hi = Some m1 ->
+  match_stacks F m1 m' stk stk' sp.
+Proof.
+  intros. eapply match_stacks_invariant; eauto.
+  intros. eapply Mem.perm_free_3; eauto. 
+Qed.
+
+Lemma match_stacks_free_right:
+  forall F m m' stk stk' sp lo hi m1',
+  match_stacks F m m' stk stk' sp ->
+  Mem.free m' sp lo hi = Some m1' ->
+  match_stacks F m m1' stk stk' sp.
+Proof.
+  intros. eapply match_stacks_invariant; eauto. 
+  intros. eapply Mem.perm_free_1; eauto. left. unfold block; omega.
+  intros. eapply Mem.perm_free_3; eauto.
+Qed.
+
+Lemma min_alignment_sound:
+  forall sz n, (min_alignment sz | n) -> Mem.inj_offset_aligned n sz.
+Proof.
+  intros; red; intros. unfold min_alignment in H. 
+  assert (2 <= sz -> (2 | n)). intros.
+    destruct (zle sz 1). omegaContradiction.
+    destruct (zle sz 2). auto. 
+    destruct (zle sz 4). apply Zdivides_trans with 4; auto. exists 2; auto.
+    apply Zdivides_trans with 8; auto. exists 4; auto.
+  assert (4 <= sz -> (4 | n)). intros.
+    destruct (zle sz 1). omegaContradiction.
+    destruct (zle sz 2). omegaContradiction.
+    destruct (zle sz 4). auto.
+    apply Zdivides_trans with 8; auto. exists 2; auto.
+  destruct chunk; simpl in *; auto.
+  apply Zone_divide.
+  apply Zone_divide.
+  apply H2; omega.
+Qed.
+
+(** Preservation by external calls *)
+
+Section EXTCALL.
+
+Variables F1 F2: meminj.
+Variables m1 m2 m1' m2': mem.
+Hypothesis MAXPERM: forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p.
+Hypothesis MAXPERM': forall b ofs p, Mem.valid_block m1' b -> Mem.perm m2' b ofs Max p -> Mem.perm m1' b ofs Max p.
+Hypothesis UNCHANGED: mem_unchanged_on (loc_out_of_reach F1 m1) m1' m2'.
+Hypothesis INJ: Mem.inject F1 m1 m1'.
+Hypothesis INCR: inject_incr F1 F2.
+Hypothesis SEP: inject_separated F1 F2 m1 m1'.
+
+Lemma match_stacks_extcall:
+  forall stk stk' bound, 
+  match_stacks F1 m1 m1' stk stk' bound ->
+  bound <= Mem.nextblock m1' ->
+  match_stacks F2 m2 m2' stk stk' bound
+with match_stacks_inside_extcall:
+  forall stk stk' f' ctx sp' rs',
+  match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs' ->
+  sp' < Mem.nextblock m1' ->
+  match_stacks_inside F2 m2 m2' stk stk' f' ctx sp' rs'.
+Proof.
+  induction 1; intros.
+  apply match_stacks_nil with bound1; auto. 
+    inv MG. constructor; intros; eauto. 
+    destruct (F1 b1) as [[b2' delta']|]_eqn.
+    exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto. 
+    exploit SEP; eauto. intros [A B]. elim B. red. omega. 
+  eapply match_stacks_cons; eauto. 
+    eapply match_stacks_inside_extcall; eauto. omega. 
+    eapply agree_regs_incr; eauto. 
+    eapply range_private_extcall; eauto. red; omega. 
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; omega.
+  eapply match_stacks_untailcall; eauto. 
+    eapply match_stacks_inside_extcall; eauto. omega. 
+    eapply range_private_extcall; eauto. red; omega. 
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; omega.
+  induction 1; intros.
+  eapply match_stacks_inside_base; eauto.
+    eapply match_stacks_extcall; eauto. omega. 
+  eapply match_stacks_inside_inlined; eauto. 
+    eapply agree_regs_incr; eauto. 
+    eapply range_private_extcall; eauto.
+Qed.
+
+End EXTCALL.
+
+(** Change of context corresponding to an inlined tailcall *)
+
+Lemma align_unchanged:
+  forall n amount, amount > 0 -> (amount | n) -> align n amount = n.
+Proof.
+  intros. destruct H0 as [p EQ]. subst n. unfold align. decEq. 
+  apply Zdiv_unique with (b := amount - 1). omega. omega.
+Qed.
+
+Lemma match_stacks_inside_inlined_tailcall:
+  forall F m m' stk stk' f' ctx sp' rs' ctx' f,
+  match_stacks_inside F m m' stk stk' f' ctx sp' rs' ->
+  context_below ctx ctx' ->
+  context_stack_tailcall ctx f ctx' ->
+  ctx'.(retinfo) = ctx.(retinfo) ->
+  range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize) ->
+  tr_funbody fenv f'.(fn_stacksize) ctx' f f'.(fn_code) ->
+  match_stacks_inside F m m' stk stk' f' ctx' sp' rs'.
+Proof.
+  intros. inv H.
+  (* base *)
+  eapply match_stacks_inside_base; eauto. congruence. 
+  rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Zdivide_0.
+  (* inlined *)
+  assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos.
+  eapply match_stacks_inside_inlined; eauto. 
+  red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply H3. inv H4. xomega. 
+  congruence. 
+  unfold context_below in *. xomega.
+  unfold context_stack_call in *. omega. 
+Qed.
+
+(** ** Relating states *)
+
+Inductive match_states: state -> state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk' f' sp' rs' m' F ctx
+        (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
+        (FB: tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code))
+        (AG: agree_regs F ctx rs rs')
+        (SP: F sp = Some(sp', ctx.(dstk)))
+        (MINJ: Mem.inject F m m')
+        (VB: Mem.valid_block m' sp')
+        (PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
+        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
+      match_states (State stk f (Vptr sp Int.zero) pc rs m)
+                   (State stk' f' (Vptr sp' Int.zero) (spc ctx pc) rs' m')
+  | match_call_states: forall stk fd args m stk' fd' args' m' F
+        (MS: match_stacks F m m' stk stk' (Mem.nextblock m'))
+        (FD: transf_fundef fenv fd = OK fd')
+        (VINJ: val_list_inject F args args')
+        (MINJ: Mem.inject F m m'),
+      match_states (Callstate stk fd args m)
+                   (Callstate stk' fd' args' m')
+  | match_call_regular_states: forall stk f vargs m stk' f' sp' rs' m' F ctx ctx' pc' pc1' rargs
+        (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
+        (FB: tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code))
+        (BELOW: context_below ctx' ctx)
+        (NOP: f'.(fn_code)!pc' = Some(Inop pc1'))
+        (MOVES: tr_moves f'.(fn_code) pc1' (sregs ctx' rargs) (sregs ctx f.(fn_params)) (spc ctx f.(fn_entrypoint)))
+        (VINJ: list_forall2 (val_reg_charact F ctx' rs') vargs rargs)
+        (MINJ: Mem.inject F m m')
+        (VB: Mem.valid_block m' sp')
+        (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
+        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
+      match_states (Callstate stk (Internal f) vargs m)
+                   (State stk' f' (Vptr sp' Int.zero) pc' rs' m')
+  | match_return_states: forall stk v m stk' v' m' F
+        (MS: match_stacks F m m' stk stk' (Mem.nextblock m'))
+        (VINJ: val_inject F v v')
+        (MINJ: Mem.inject F m m'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v' m')
+  | match_return_regular_states: forall stk v m stk' f' sp' rs' m' F ctx pc' or rinfo
+        (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
+        (RET: ctx.(retinfo) = Some rinfo)
+        (AT: f'.(fn_code)!pc' = Some(inline_return ctx or rinfo))
+        (VINJ: match or with None => v = Vundef | Some r => val_inject F v rs'#(sreg ctx r) end)
+        (MINJ: Mem.inject F m m')
+        (VB: Mem.valid_block m' sp')
+        (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
+        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
+      match_states (Returnstate stk v m)
+                   (State stk' f' (Vptr sp' Int.zero) pc' rs' m').
+
+(** ** Forward simulation *)
+
+Definition measure (S: state) : nat :=
+  match S with
+  | State _ _ _ _ _ _ => 1%nat
+  | Callstate _ _ _ _ => 0%nat
+  | Returnstate _ _ _ => 0%nat
+  end.
+
+Lemma tr_funbody_inv:
+  forall sz cts f c pc i,
+  tr_funbody fenv sz cts f c -> f.(fn_code)!pc = Some i -> tr_instr fenv sz cts pc i c.
+Proof.
+  intros. inv H. eauto. 
+Qed.
+
+Theorem step_simulation:
+  forall S1 t S2,
+  step ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
+Proof.
+  induction 1; intros; inv MS.
+
+(* nop *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  left; econstructor; split. 
+  eapply plus_one. eapply exec_Inop; eauto.
+  econstructor; eauto.
+
+(* op *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  exploit eval_operation_inject. 
+    eapply match_stacks_inside_globals; eauto.
+    eexact SP.
+    instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
+    eexact MINJ. eauto.
+  fold (sop ctx op). intros [v' [A B]].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Iop; eauto. erewrite eval_operation_preserved; eauto.
+  exact symbols_preserved. 
+  econstructor; eauto. 
+  apply match_stacks_inside_set_reg; auto.
+  apply agree_set_reg; auto. 
+  
+(* load *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  exploit eval_addressing_inject. 
+    eapply match_stacks_inside_globals; eauto.
+    eexact SP.
+    instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
+    eauto.
+  fold (saddr ctx addr). intros [a' [P Q]].
+  exploit Mem.loadv_inject; eauto. intros [v' [U V]].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto.
+  exact symbols_preserved. 
+  econstructor; eauto. 
+  apply match_stacks_inside_set_reg; auto.
+  apply agree_set_reg; auto. 
+
+(* store *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  exploit eval_addressing_inject. 
+    eapply match_stacks_inside_globals; eauto.
+    eexact SP.
+    instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
+    eauto.
+  fold saddr. intros [a' [P Q]].
+  exploit Mem.storev_mapped_inject; eauto. eapply agree_val_reg; eauto. 
+  intros [m1' [U V]].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto.
+  exact symbols_preserved. 
+  destruct a; simpl in H1; try discriminate.
+  destruct a'; simpl in U; try discriminate.
+  econstructor; eauto.
+  eapply match_stacks_inside_store; eauto.
+  eapply Mem.store_valid_block_1; eauto.
+  eapply range_private_invariant; eauto.
+  intros; split; auto. eapply Mem.perm_store_2; eauto.
+  intros; eapply Mem.perm_store_1; eauto.
+  intros. eapply SSZ2. eapply Mem.perm_store_2; eauto.
+
+(* call *)
+  exploit match_stacks_inside_globalenvs; eauto. intros [bound G].
+  exploit find_function_agree; eauto. intros [fd' [A B]].
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+(* not inlined *)
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Icall; eauto.
+  eapply sig_function_translated; eauto.
+  econstructor; eauto.
+  eapply match_stacks_cons; eauto. 
+  eapply agree_val_regs; eauto. 
+(* inlined *)
+  assert (fd = Internal f0).
+    simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate.
+    exploit (funenv_program_compat prog); eauto. intros. 
+    unfold ge in H0. congruence.
+  subst fd.
+  right; split. simpl; omega. split. auto. 
+  econstructor; eauto. 
+  eapply match_stacks_inside_inlined; eauto.
+  red; intros. apply PRIV. inv H13. destruct H16. xomega.
+  apply agree_val_regs_gen; auto.
+  red; intros; apply PRIV. destruct H16. omega. 
+
+(* tailcall *)
+  exploit match_stacks_inside_globalenvs; eauto. intros [bound G].
+  exploit find_function_agree; eauto. intros [fd' [A B]].
+  assert (PRIV': range_private F m' m'0 sp' (dstk ctx) f'.(fn_stacksize)).
+    eapply range_private_free_left; eauto. inv FB. rewrite <- H4. auto. 
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+(* within the original function *)
+  inv MS0; try congruence.
+  assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}).
+    apply Mem.range_perm_free. red; intros.
+    destruct (zlt ofs f.(fn_stacksize)). 
+    replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto.
+    eapply Mem.free_range_perm; eauto. omega.
+    inv FB. eapply range_private_perms; eauto. xomega.
+  destruct X as [m1' FREE].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Itailcall; eauto.
+  eapply sig_function_translated; eauto.
+  econstructor; eauto.
+  eapply match_stacks_bound with (bound := sp'). 
+  eapply match_stacks_invariant; eauto.
+    intros. eapply Mem.perm_free_3; eauto. 
+    intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega.
+    intros. eapply Mem.perm_free_3; eauto.
+  erewrite Mem.nextblock_free; eauto. red in VB; omega.
+  eapply agree_val_regs; eauto.
+  eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto.
+  (* show that no valid location points into the stack block being freed *)
+  intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [P Q]. 
+  eelim Q; eauto. replace (ofs + delta - delta) with ofs by omega. 
+  apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
+(* turned into a call *)
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Icall; eauto.
+  eapply sig_function_translated; eauto.
+  econstructor; eauto.
+  eapply match_stacks_untailcall; eauto.
+  eapply match_stacks_inside_invariant; eauto. 
+    intros. eapply Mem.perm_free_3; eauto.
+  eapply agree_val_regs; eauto.
+  eapply Mem.free_left_inject; eauto.
+(* inlined *)
+  assert (fd = Internal f0).
+    simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate.
+    exploit (funenv_program_compat prog); eauto. intros. 
+    unfold ge in H0. congruence.
+  subst fd.
+  right; split. simpl; omega. split. auto. 
+  econstructor; eauto.
+  eapply match_stacks_inside_inlined_tailcall; eauto.
+  eapply match_stacks_inside_invariant; eauto.
+    intros. eapply Mem.perm_free_3; eauto.
+  apply agree_val_regs_gen; auto.
+  eapply Mem.free_left_inject; eauto.
+  red; intros; apply PRIV'. 
+    assert (dstk ctx <= dstk ctx'). red in H14; rewrite H14. apply align_le. apply min_alignment_pos.
+    omega.
+
+(* builtin *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  exploit external_call_mem_inject; eauto. 
+    eapply match_stacks_inside_globals; eauto.
+    instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. 
+  intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Ibuiltin; eauto. 
+    eapply external_call_symbols_preserved; eauto. 
+    exact symbols_preserved. exact varinfo_preserved.
+  econstructor.
+    eapply match_stacks_inside_set_reg. 
+    eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
+    intros; eapply external_call_max_perm; eauto. 
+    intros; eapply external_call_max_perm; eauto. 
+  auto. 
+  eapply agree_set_reg. eapply agree_regs_incr; eauto. auto. auto. 
+  apply J; auto.
+  auto. 
+  eapply external_call_valid_block; eauto. 
+  eapply range_private_extcall; eauto. 
+    intros; eapply external_call_max_perm; eauto. 
+  auto. 
+  intros. apply SSZ2. eapply external_call_max_perm; eauto. 
+
+(* cond *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  assert (eval_condition cond rs'##(sregs ctx args) m' = Some b).
+    eapply eval_condition_inject; eauto. eapply agree_val_regs; eauto. 
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Icond; eauto. 
+  destruct b; econstructor; eauto. 
+
+(* jumptable *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  assert (val_inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto.
+  rewrite H0 in H2; inv H2. 
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Ijumptable; eauto.
+  rewrite list_nth_z_map. rewrite H1. simpl; reflexivity. 
+  econstructor; eauto. 
+
+(* return *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  (* not inlined *)
+  inv MS0; try congruence.
+  assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}).
+    apply Mem.range_perm_free. red; intros.
+    destruct (zlt ofs f.(fn_stacksize)). 
+    replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto.
+    eapply Mem.free_range_perm; eauto. omega.
+    inv FB. eapply range_private_perms; eauto.
+    generalize (Zmax_spec (fn_stacksize f) 0). destruct (zlt 0 (fn_stacksize f)); omega.
+  destruct X as [m1' FREE].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Ireturn; eauto. 
+  econstructor; eauto.
+  eapply match_stacks_bound with (bound := sp'). 
+  eapply match_stacks_invariant; eauto.
+    intros. eapply Mem.perm_free_3; eauto. 
+    intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega.
+    intros. eapply Mem.perm_free_3; eauto.
+  erewrite Mem.nextblock_free; eauto. red in VB; omega.
+  destruct or; simpl. apply agree_val_reg; auto. auto.
+  eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto.
+  (* show that no valid location points into the stack block being freed *)
+  intros. inversion FB; subst.
+  assert (PRIV': range_private F m' m'0 sp' (dstk ctx) f'.(fn_stacksize)).
+    rewrite H8 in PRIV. eapply range_private_free_left; eauto. 
+  rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [A B]. 
+  eelim B; eauto. replace (ofs + delta - delta) with ofs by omega. 
+  apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
+
+  (* inlined *)
+  right. split. simpl. omega. split. auto. 
+  econstructor; eauto.
+  eapply match_stacks_inside_invariant; eauto. 
+    intros. eapply Mem.perm_free_3; eauto.
+  destruct or; simpl. apply agree_val_reg; auto. auto.
+  eapply Mem.free_left_inject; eauto.
+  inv FB. rewrite H4 in PRIV. eapply range_private_free_left; eauto. 
+
+(* internal function, not inlined *)
+  assert (A: exists f', tr_function fenv f f' /\ fd' = Internal f'). 
+    Errors.monadInv FD. exists x. split; auto. eapply transf_function_spec; eauto. 
+  destruct A as [f' [TR EQ]]. inversion TR; subst.
+  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. 
+    instantiate (1 := fn_stacksize f'). inv H0. xomega. 
+  intros [F' [m1' [sp' [A [B [C [D E]]]]]]].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_function_internal; eauto.
+  rewrite H5. econstructor.
+  instantiate (1 := F'). apply match_stacks_inside_base.
+  assert (SP: sp' = Mem.nextblock m'0) by (eapply Mem.alloc_result; eauto).
+  rewrite <- SP in MS0. 
+  eapply match_stacks_invariant; eauto.
+    intros. destruct (eq_block b1 stk). 
+    subst b1. rewrite D in H7; inv H7. unfold block in *; omegaContradiction.
+    rewrite E in H7; auto. 
+    intros. exploit Mem.perm_alloc_inv. eexact H. eauto. 
+    destruct (zeq b1 stk); intros; auto. 
+    subst b1. rewrite D in H7; inv H7. unfold block in *; omegaContradiction.
+    intros. eapply Mem.perm_alloc_1; eauto. 
+    intros. exploit Mem.perm_alloc_inv. eexact A. eauto. 
+    rewrite zeq_false; auto. unfold block; omega.
+  auto. auto. auto. 
+  rewrite H4. apply agree_regs_init_regs. eauto. auto. inv H0; auto. congruence. auto.
+  eapply Mem.valid_new_block; eauto.
+  red; intros. split.
+  eapply Mem.perm_alloc_2; eauto. inv H0; xomega.
+  intros; red; intros. exploit Mem.perm_alloc_inv. eexact H. eauto.
+  destruct (zeq b stk); intros. 
+  subst. rewrite D in H8; inv H8. inv H0; xomega.
+  rewrite E in H8; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto.
+  auto.
+  intros. exploit Mem.perm_alloc_inv; eauto. rewrite zeq_true. omega. 
+
+(* internal function, inlined *)
+  inversion FB; subst.
+  exploit Mem.alloc_left_mapped_inject. 
+    eauto.
+    eauto.
+    (* sp' is valid *)
+    instantiate (1 := sp'). auto.
+    (* offset is representable *)
+    instantiate (1 := dstk ctx). generalize (Zmax2 (fn_stacksize f) 0). omega.
+    (* size of target block is representable *)
+    intros. right. exploit SSZ2; eauto with mem. inv FB; omega.
+    (* we have full permissions on sp' at and above dstk ctx *)
+    intros. apply Mem.perm_cur. apply Mem.perm_implies with Freeable; auto with mem.
+    eapply range_private_perms; eauto. xomega.
+    (* offset is aligned *)
+    replace (fn_stacksize f - 0) with (fn_stacksize f) by omega.
+    inv FB. apply min_alignment_sound; auto.
+    (* nobody maps to (sp, dstk ctx...) *)
+    intros. exploit (PRIV (ofs + delta')); eauto. xomega.
+    intros [A B]. eelim B; eauto.
+    replace (ofs + delta' - delta') with ofs by omega.
+    apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
+  intros [F' [A [B [C D]]]].
+  exploit tr_moves_init_regs; eauto. intros [rs'' [P [Q R]]].
+  left; econstructor; split. 
+  eapply plus_left. eapply exec_Inop; eauto. eexact P. traceEq.
+  econstructor.
+  eapply match_stacks_inside_alloc_left; eauto.
+  eapply match_stacks_inside_invariant; eauto.
+  omega.
+  auto.
+  apply agree_regs_incr with F; auto.
+  auto. auto. auto.
+  rewrite H2. eapply range_private_alloc_left; eauto.
+  auto. auto.
+
+(* external function *)
+  exploit match_stacks_globalenvs; eauto. intros [bound MG].
+  exploit external_call_mem_inject; eauto. 
+    eapply match_globalenvs_preserves_globals; eauto.
+  intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]].
+  simpl in FD. inv FD. 
+  left; econstructor; split.
+  eapply plus_one. eapply exec_function_external; eauto. 
+    eapply external_call_symbols_preserved; eauto. 
+    exact symbols_preserved. exact varinfo_preserved.
+  econstructor.
+    eapply match_stacks_bound with (Mem.nextblock m'0).
+    eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
+    intros; eapply external_call_max_perm; eauto. 
+    intros; eapply external_call_max_perm; eauto.
+    omega.
+    eapply external_call_nextblock; eauto. 
+    auto. auto.
+
+(* return fron noninlined function *)
+  inv MS0.
+  (* normal case *)
+  left; econstructor; split.
+  eapply plus_one. eapply exec_return.
+  econstructor; eauto. 
+  apply match_stacks_inside_set_reg; auto. 
+  apply agree_set_reg; auto.
+  (* untailcall case *)
+  inv MS; try congruence.
+  rewrite RET in RET0; inv RET0.
+(*
+  assert (rpc = pc). unfold spc in H0; unfold node in *; xomega.
+  assert (res0 = res). unfold sreg in H1; unfold reg in *; xomega.
+  subst rpc res0.
+*)
+  left; econstructor; split.
+  eapply plus_one. eapply exec_return.
+  eapply match_regular_states. 
+  eapply match_stacks_inside_set_reg; eauto.
+  auto. 
+  apply agree_set_reg; auto.
+  auto. auto. auto.
+  red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply PRIV; omega.
+  auto. auto. 
+  
+(* return from inlined function *)
+  inv MS0; try congruence. rewrite RET0 in RET; inv RET. 
+  unfold inline_return in AT. 
+  assert (PRIV': range_private F m m' sp' (dstk ctx' + mstk ctx') f'.(fn_stacksize)).
+    red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. omega. apply PRIV. omega.
+  destruct or.
+  (* with a result *)
+  left; econstructor; split. 
+  eapply plus_one. eapply exec_Iop; eauto. simpl. reflexivity. 
+  econstructor; eauto. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto.
+  (* without a result *)
+  left; econstructor; split. 
+  eapply plus_one. eapply exec_Inop; eauto.
+  econstructor; eauto. subst vres. apply agree_set_reg_undef'; auto.
+Qed.
+
+Lemma transf_initial_states:
+  forall st1, initial_state prog st1 -> exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inv H.
+  exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
+  exists (Callstate nil tf nil m0); split.
+  econstructor; eauto.
+    unfold transf_program in TRANSF. eapply Genv.init_mem_transf_partial; eauto.
+    rewrite symbols_preserved. 
+    rewrite (transform_partial_program_main _ _ TRANSF).  auto.
+    rewrite <- H3. apply sig_function_translated; auto. 
+  econstructor; eauto. 
+  instantiate (1 := Mem.flat_inj (Mem.nextblock m0)). 
+  apply match_stacks_nil with (Mem.nextblock m0).
+  constructor; intros. 
+    apply Mem.nextblock_pos.
+    unfold Mem.flat_inj. apply zlt_true; auto. 
+    unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); congruence.
+    eapply Genv.find_symbol_not_fresh; eauto. 
+    eapply Genv.find_var_info_not_fresh; eauto. 
+    omega.
+  eapply Genv.initmem_inject; eauto.
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r, 
+  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+Proof.
+  intros. inv H0. inv H.
+  exploit match_stacks_empty; eauto. intros EQ; subst. inv VINJ. constructor.
+  exploit match_stacks_inside_empty; eauto. intros [A B]. congruence. 
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (semantics prog) (semantics tprog).
+Proof.
+  eapply forward_simulation_star.
+  eexact symbols_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  eexact step_simulation. 
+Qed.
+
+End INLINING.
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
new file mode 100644
index 0000000..ec72290
--- /dev/null
+++ b/backend/Inliningspec.v
@@ -0,0 +1,712 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** RTL function inlining: relational specification *)
+
+Require Import Coqlib.
+Require Import Wfsimpl.
+Require Import Errors.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Inlining.
+
+(** ** Soundness of function environments. *)
+
+(** A (compile-time) function environment is compatible with a
+  (run-time) global environment if the following condition holds. *)
+
+Definition fenv_compat (ge: genv) (fenv: funenv) : Prop :=
+  forall id b f,
+  fenv!id = Some f -> Genv.find_symbol ge id = Some b ->
+  Genv.find_funct_ptr ge b = Some (Internal f).
+
+Remark add_fundef_compat:
+  forall ge fenv idf,
+  fenv_compat ge fenv ->
+  fenv_compat (Genv.add_function ge idf) (Inlining.add_fundef fenv idf).
+Proof.
+  intros. destruct idf as [id fd]. red; simpl; intros.
+  unfold Genv.find_symbol in H1; simpl in H1. 
+  unfold Genv.find_funct_ptr; simpl.
+  rewrite PTree.gsspec in H1. destruct (peq id0 id).
+  (* same *)
+  subst id0. inv H1. rewrite ZMap.gss. 
+  destruct fd. destruct (should_inline id f0).
+  rewrite PTree.gss in H0. inv H0; auto.
+  rewrite PTree.grs in H0; discriminate.
+  rewrite PTree.grs in H0; discriminate.
+  (* different *)
+  rewrite ZMap.gso. eapply H; eauto.
+  destruct fd. destruct (should_inline id f0).
+  rewrite PTree.gso in H0; auto.
+  rewrite PTree.gro in H0; auto.
+  rewrite PTree.gro in H0; auto.
+  exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega. 
+Qed.
+
+Remark remove_vardef_compat:
+  forall ge fenv idv,
+  fenv_compat ge fenv ->
+  fenv_compat (Genv.add_variable ge idv) (Inlining.remove_vardef fenv idv).
+Proof.
+  intros. destruct idv as [id vi]. red; simpl; intros.
+  unfold Genv.find_symbol in H1; simpl in H1. 
+  unfold Genv.find_funct_ptr; simpl.
+  unfold remove_vardef in H0; simpl in H0.
+  rewrite PTree.gsspec in H1. rewrite PTree.grspec in H0. 
+  unfold PTree.elt_eq in H0. destruct (peq id0 id).
+  discriminate.
+  eapply H; eauto.
+Qed.
+
+Lemma funenv_program_compat:
+  forall p, fenv_compat (Genv.globalenv p) (funenv_program p).
+Proof.
+  intros.
+  unfold Genv.globalenv, funenv_program.
+  assert (forall funs ge fenv,
+         fenv_compat ge fenv ->
+         fenv_compat (Genv.add_functions ge funs) (fold_left add_fundef funs fenv)).
+    unfold Genv.add_functions. induction funs; simpl; intros.
+    auto. apply IHfuns. apply add_fundef_compat; auto.
+  assert (forall vars ge fenv,
+         fenv_compat ge fenv ->
+         fenv_compat (Genv.add_variables ge vars) (fold_left remove_vardef vars fenv)).
+    unfold Genv.add_variables. induction vars; simpl; intros.
+    auto. apply IHvars. apply remove_vardef_compat; auto.
+  apply H0. apply H. red; intros. rewrite PTree.gempty in H1; discriminate.
+Qed.
+
+(** ** Soundness of the computed bounds over function resources *)
+
+Remark Pmax_l: forall x y, Ple x (Pmax x y).
+Proof. intros; xomega. Qed.
+
+Remark Pmax_r: forall x y, Ple y (Pmax x y).
+Proof. intros; xomega. Qed.
+
+Lemma max_pc_function_sound:
+  forall f pc i, f.(fn_code)!pc = Some i -> Ple pc (max_pc_function f).
+Proof.
+  intros until i. unfold max_pc_function. 
+  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
+  (* extensionality *)
+  intros. apply H0. rewrite H; auto. 
+  (* base case *)
+  rewrite PTree.gempty. congruence.
+  (* inductive case *)
+  intros. rewrite PTree.gsspec in H2. destruct (peq pc k). 
+  inv H2. apply Pmax_r.
+  apply Ple_trans with a. auto. apply Pmax_l.
+Qed.
+
+Lemma max_def_function_instr:
+  forall f pc i, f.(fn_code)!pc = Some i -> Ple (max_def_instr i) (max_def_function f).
+Proof.
+  intros. unfold max_def_function. eapply Ple_trans. 2: eapply Pmax_l. 
+  revert H. 
+  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple (max_def_instr i) m).
+  (* extensionality *)
+  intros. apply H0. rewrite H; auto. 
+  (* base case *)
+  rewrite PTree.gempty. congruence.
+  (* inductive case *)
+  intros. rewrite PTree.gsspec in H2. destruct (peq pc k). 
+  inv H2. apply Pmax_r. 
+  apply Ple_trans with a. auto. apply Pmax_l.
+Qed.
+
+Lemma max_def_function_params:
+  forall f r, In r f.(fn_params) -> Ple r (max_def_function f).
+Proof.
+  assert (A: forall l m, Ple m (fold_left (fun m r => Pmax m r) l m)).
+    induction l; simpl; intros. 
+    apply Ple_refl.
+    eapply Ple_trans. 2: eauto. apply Pmax_l.
+  assert (B: forall l m r, In r l -> Ple r (fold_left (fun m r => Pmax m r) l m)).
+    induction l; simpl; intros.
+    contradiction.
+    destruct H. subst a. eapply Ple_trans. 2: eapply A. apply Pmax_r. 
+    eauto. 
+  unfold max_def_function; intros. 
+  eapply Ple_trans. 2: eapply Pmax_r. eauto. 
+Qed.
+
+(** ** Working with the state monad *)
+
+Remark bind_inversion:
+  forall (A B: Type) (f: mon A) (g: A -> mon B) 
+         (y: B) (s1 s3: state) (i: sincr s1 s3),
+  bind f g s1 = R y s3 i ->
+  exists x, exists s2, exists i1, exists i2,
+  f s1 = R x s2 i1 /\ g x s2 = R y s3 i2.
+Proof.
+  unfold bind; intros. destruct (f s1). exists x; exists s'; exists I.
+  destruct (g x s'). inv H. exists I0; auto.
+Qed.
+
+Ltac monadInv1 H :=
+  match type of H with
+  | (R _ _ _ = R _ _ _) =>
+      inversion H; clear H; try subst
+  | (ret _ _ = R _ _ _) =>
+      inversion H; clear H; try subst
+  | (bind ?F ?G ?S = R ?X ?S' ?I) =>
+      let x := fresh "x" in (
+      let s := fresh "s" in (
+      let i1 := fresh "INCR" in (
+      let i2 := fresh "INCR" in (
+      let EQ1 := fresh "EQ" in (
+      let EQ2 := fresh "EQ" in (
+      destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]];
+      clear H;
+      try (monadInv1 EQ2)))))))
+  end.
+
+Ltac monadInv H :=
+  match type of H with
+  | (ret _ _ = R _ _ _) => monadInv1 H
+  | (bind ?F ?G ?S = R ?X ?S' ?I) => monadInv1 H
+  | (?F _ _ _ _ _ _ _ _ = R _ _ _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ _ = R _ _ _) =>
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ = R _ _ _) =>
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ = R _ _ _) =>
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ = R _ _ _) =>
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ = R _ _ _) =>
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ = R _ _ _) =>
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ = R _ _ _) =>
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  end.
+
+(** ** Relational specification of the translation of moves *)
+
+Inductive tr_moves (c: code) : node -> list reg -> list reg -> node -> Prop :=
+  | tr_moves_cons: forall pc1 src srcs dst dsts pc2 pc3,
+      tr_moves c pc1 srcs dsts pc2 ->
+      c!pc2 = Some(Iop Omove (src :: nil) dst pc3) ->
+      tr_moves c pc1 (src :: srcs) (dst :: dsts) pc3
+  | tr_moves_nil: forall srcs dsts pc,
+      srcs = nil \/ dsts = nil ->
+      tr_moves c pc srcs dsts pc.
+
+Lemma add_moves_unchanged:
+  forall srcs dsts pc2 s pc1 s' i pc,
+  add_moves srcs dsts pc2 s = R pc1 s' i ->
+  Ple pc s.(st_nextnode) \/ Plt s'.(st_nextnode) pc ->
+  s'.(st_code)!pc = s.(st_code)!pc.
+Proof.
+  induction srcs; simpl; intros. 
+  monadInv H. auto.
+  destruct dsts; monadInv H. auto.
+  transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. xomega. 
+  monadInv EQ; simpl. apply PTree.gso.
+  inversion INCR0; simpl in *. xomega. 
+Qed.
+
+Lemma add_moves_spec:
+  forall srcs dsts pc2 s pc1 s' i c,
+  add_moves srcs dsts pc2 s = R pc1 s' i ->
+  (forall pc, Plt s.(st_nextnode) pc -> Ple pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) ->
+  tr_moves c pc1 srcs dsts pc2.
+Proof.
+  induction srcs; simpl; intros. 
+  monadInv H. apply tr_moves_nil; auto.
+  destruct dsts; monadInv H. apply tr_moves_nil; auto. 
+  apply tr_moves_cons with x. eapply IHsrcs; eauto. 
+  intros. inversion INCR. apply H0; xomega.
+  monadInv EQ.
+  rewrite H0. erewrite add_moves_unchanged; eauto. 
+  simpl. apply PTree.gss. 
+  simpl. xomega. 
+  xomega.
+  inversion INCR; inversion INCR0; simpl in *; xomega.
+Qed.
+
+(** ** Relational specification of CFG expansion *)
+
+Section INLINING_SPEC.
+
+Variable fenv: funenv.
+
+Definition context_below (ctx1 ctx2: context): Prop :=
+  Ple (Pplus ctx1.(dreg) ctx1.(mreg)) ctx2.(dreg).
+
+Definition context_stack_call (ctx1 ctx2: context): Prop :=
+  ctx1.(mstk) >= 0 /\ ctx1.(dstk) + ctx1.(mstk) <= ctx2.(dstk).
+
+Definition context_stack_tailcall (ctx1: context) (f: function) (ctx2: context) : Prop :=
+  ctx2.(dstk) = align ctx1.(dstk) (min_alignment f.(fn_stacksize)).
+
+Section INLINING_BODY_SPEC.
+
+Variable stacksize: Z.
+
+Inductive tr_instr: context -> node -> instruction -> code -> Prop :=
+  | tr_nop: forall ctx pc c s,
+      c!(spc ctx pc) = Some (Inop (spc ctx s)) ->
+      tr_instr ctx pc (Inop s) c
+  | tr_op: forall ctx pc c op args res s,
+      Ple res ctx.(mreg) ->
+      c!(spc ctx pc) = Some (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
+      tr_instr ctx pc (Iop op args res s) c
+  | tr_load: forall ctx pc c chunk addr args res s,
+      Ple res ctx.(mreg) ->
+      c!(spc ctx pc) = Some (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
+      tr_instr ctx pc (Iload chunk addr args res s) c
+  | tr_store: forall ctx pc c chunk addr args src s,
+      c!(spc ctx pc) = Some (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s)) ->
+      tr_instr ctx pc (Istore chunk addr args src s) c
+  | tr_call: forall ctx pc c sg ros args res s,
+      Ple res ctx.(mreg) ->
+      c!(spc ctx pc) = Some (Icall sg (sros ctx ros) (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
+      tr_instr ctx pc (Icall sg ros args res s) c
+  | tr_call_inlined:forall ctx pc sg id args res s c f pc1 ctx',
+      Ple res ctx.(mreg) ->
+      fenv!id = Some f ->
+      c!(spc ctx pc) = Some(Inop pc1) ->
+      tr_moves c pc1 (sregs ctx args) (sregs ctx' f.(fn_params)) (spc ctx' f.(fn_entrypoint)) ->
+      tr_funbody ctx' f c ->
+      ctx'.(retinfo) = Some(spc ctx s, sreg ctx res) ->
+      context_below ctx ctx' ->
+      context_stack_call ctx ctx' ->
+      tr_instr ctx pc (Icall sg (inr _ id) args res s) c
+  | tr_tailcall: forall ctx pc c sg ros args,
+      c!(spc ctx pc) = Some (Itailcall sg (sros ctx ros) (sregs ctx args)) ->
+      ctx.(retinfo) = None ->
+      tr_instr ctx pc (Itailcall sg ros args) c
+  | tr_tailcall_call: forall ctx pc c sg ros args res s,
+      c!(spc ctx pc) = Some (Icall sg (sros ctx ros) (sregs ctx args) res s) ->
+      ctx.(retinfo) = Some(s, res) ->
+      tr_instr ctx pc (Itailcall sg ros args) c
+  | tr_tailcall_inlined: forall ctx pc sg id args c f pc1 ctx',
+      fenv!id = Some f ->
+      c!(spc ctx pc) = Some(Inop pc1) ->
+      tr_moves c pc1 (sregs ctx args) (sregs ctx' f.(fn_params)) (spc ctx' f.(fn_entrypoint)) ->
+      tr_funbody ctx' f c ->
+      ctx'.(retinfo) = ctx.(retinfo) ->
+      context_below ctx ctx' ->
+      context_stack_tailcall ctx f ctx' ->
+      tr_instr ctx pc (Itailcall sg (inr _ id) args) c
+  | tr_builtin: forall ctx pc c ef args res s,
+      Ple res ctx.(mreg) ->
+      c!(spc ctx pc) = Some (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
+      tr_instr ctx pc (Ibuiltin ef args res s) c
+  | tr_cond: forall ctx pc cond args s1 s2 c,
+      c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) ->
+      tr_instr ctx pc (Icond cond args s1 s2) c
+  | tr_jumptable: forall ctx pc r tbl c,
+      c!(spc ctx pc) = Some (Ijumptable (sreg ctx r) (List.map (spc ctx) tbl)) ->
+      tr_instr ctx pc (Ijumptable r tbl) c
+  | tr_return: forall ctx pc or c,
+      c!(spc ctx pc) = Some (Ireturn (option_map (sreg ctx) or)) ->
+      ctx.(retinfo) = None ->
+      tr_instr ctx pc (Ireturn or) c
+  | tr_return_inlined: forall ctx pc or c rinfo,
+      c!(spc ctx pc) = Some (inline_return ctx or rinfo) ->
+      ctx.(retinfo) = Some rinfo ->
+      tr_instr ctx pc (Ireturn or) c
+
+with tr_funbody: context -> function -> code -> Prop :=
+  | tr_funbody_intro: forall ctx f c,
+      (forall r, In r f.(fn_params) -> Ple r ctx.(mreg)) ->
+      (forall pc i, f.(fn_code)!pc = Some i -> tr_instr ctx pc i c) ->
+      ctx.(mstk) = Zmax f.(fn_stacksize) 0 ->
+      (min_alignment f.(fn_stacksize) | ctx.(dstk)) ->
+      ctx.(dstk) >= 0 -> ctx.(dstk) + ctx.(mstk) <= stacksize ->
+      tr_funbody ctx f c.
+
+Definition fenv_agree (fe: funenv) : Prop :=
+  forall id f, fe!id = Some f -> fenv!id = Some f.
+
+Section EXPAND_INSTR.
+
+Variable fe: funenv.
+Hypothesis FE: fenv_agree fe.
+
+Variable rec: forall fe', (size_fenv fe' < size_fenv fe)%nat -> context -> function -> mon unit.
+
+Hypothesis rec_unchanged:
+  forall fe' (L: (size_fenv fe' < size_fenv fe)%nat) ctx f s x s' i pc,
+  rec fe' L ctx f s = R x s' i ->
+  Ple ctx.(dpc) s.(st_nextnode) ->
+  Ple pc ctx.(dpc) ->
+  s'.(st_code)!pc = s.(st_code)!pc.
+
+Remark set_instr_other:
+  forall pc instr s x s' i pc',
+  set_instr pc instr s = R x s' i ->
+  pc' <> pc ->
+  s'.(st_code)!pc' = s.(st_code)!pc'.
+Proof.
+  intros. monadInv H; simpl. apply PTree.gso; auto.
+Qed.
+
+Remark set_instr_same:
+  forall pc instr s x s' i c,
+  set_instr pc instr s = R x s' i ->
+  c!(pc) = s'.(st_code)!pc ->
+  c!(pc) = Some instr.
+Proof.
+  intros. rewrite H0. monadInv H; simpl. apply PTree.gss.
+Qed.
+
+Lemma expand_instr_unchanged:
+  forall ctx pc instr s x s' i pc',
+  expand_instr fe rec ctx pc instr s = R x s' i ->
+  Ple ctx.(dpc) s.(st_nextnode) ->
+  Ple pc' s.(st_nextnode) ->
+  pc' <> spc ctx pc ->
+  s'.(st_code)!pc' = s.(st_code)!pc'.
+Proof.
+  generalize set_instr_other; intros A.
+  intros. unfold expand_instr in H; destruct instr; eauto.
+(* call *)
+  destruct (can_inline fe s1). eauto. 
+  monadInv H. unfold inline_function in EQ. monadInv EQ.
+  transitivity (s2.(st_code)!pc'). eauto. 
+  transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto.
+    left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. 
+  transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. 
+    simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega.
+    simpl. monadInv EQ1; simpl. auto. 
+  monadInv EQ; simpl. monadInv EQ1; simpl. auto.
+(* tailcall *)
+  destruct (can_inline fe s1).
+  destruct (retinfo ctx) as [[rpc rreg]|]; eauto.
+  monadInv H. unfold inline_tail_function in EQ. monadInv EQ.
+  transitivity (s2.(st_code)!pc'). eauto. 
+  transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto.
+    left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. 
+  transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. 
+    simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega.
+    simpl. monadInv EQ1; simpl. auto. 
+  monadInv EQ; simpl. monadInv EQ1; simpl. auto.
+(* return *)
+  destruct (retinfo ctx) as [[rpc rreg]|]; eauto.
+Qed.
+
+Lemma iter_expand_instr_unchanged:
+  forall ctx pc l s x s' i,
+  mlist_iter2 (expand_instr fe rec ctx) l s = R x s' i ->
+  Ple ctx.(dpc) s.(st_nextnode) ->
+  Ple pc s.(st_nextnode) ->
+  ~In pc (List.map (spc ctx) (List.map (@fst _ _) l)) ->
+  list_norepet (List.map (@fst _ _) l) ->
+  s'.(st_code)!pc = s.(st_code)!pc.
+Proof.
+  induction l; simpl; intros.
+  (* base case *)
+  monadInv H. auto.
+  (* inductive case *)
+  destruct a as [pc1 instr1]; simpl in *.
+  monadInv H. inv H3.
+  transitivity ((st_code s0)!pc). 
+  eapply IHl; eauto. destruct INCR; xomega. destruct INCR; xomega. 
+  eapply expand_instr_unchanged; eauto.
+Qed.
+
+Lemma expand_cfg_rec_unchanged:
+  forall ctx f s x s' i pc,
+  expand_cfg_rec fe rec ctx f s = R x s' i ->
+  Ple ctx.(dpc) s.(st_nextnode) ->
+  Ple pc ctx.(dpc) ->
+  s'.(st_code)!pc = s.(st_code)!pc.
+Proof.
+  intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ.
+  transitivity ((st_code s0)!pc).
+  eapply iter_expand_instr_unchanged; eauto. 
+    subst s0; auto. 
+    subst s0; simpl. xomega.
+    red; intros. exploit list_in_map_inv; eauto. intros [pc1 [A B]]. 
+    subst pc. unfold spc in H1. xomega.
+    apply PTree.elements_keys_norepet.
+  subst s0; auto.
+Qed.
+
+Hypothesis rec_spec:
+  forall fe' (L: (size_fenv fe' < size_fenv fe)%nat) ctx f s x s' i c,
+  rec fe' L ctx f s = R x s' i ->
+  fenv_agree fe' ->
+  Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
+  ctx.(mreg) = max_def_function f ->
+  Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
+  ctx.(mstk) >= 0 -> 
+  ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
+  (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
+  ctx.(dstk) >= 0 ->
+  s'.(st_stksize) <= stacksize ->
+  (forall pc, Plt ctx.(dpc) pc -> Ple pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) ->
+  tr_funbody ctx f c.
+
+Remark min_alignment_pos:
+  forall sz, min_alignment sz > 0.
+Proof.
+  intros; unfold min_alignment.
+  destruct (zle sz 1). omega. destruct (zle sz 2). omega. destruct (zle sz 4); omega.
+Qed.
+
+Ltac inv_incr :=
+  match goal with
+  | [ H: sincr _ _ |- _ ] => destruct H; inv_incr
+  | _ => idtac
+  end.
+
+Lemma expand_instr_spec:
+  forall ctx pc instr s x s' i c,
+  expand_instr fe rec ctx pc instr s = R x s' i ->
+  Ple (max_def_instr instr) ctx.(mreg) ->
+  Ple (spc ctx pc) s.(st_nextnode) ->
+  Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
+  ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 ->
+  s'.(st_stksize) <= stacksize ->
+  (forall pc', Plt s.(st_nextnode) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  c!(spc ctx pc) = s'.(st_code)!(spc ctx pc) ->
+  tr_instr ctx pc instr c.
+Proof.
+  intros until c; intros EXP DEFS OPC OREG STK1 STK2 STK3 S1 S2.
+  generalize set_instr_same; intros BASE.
+  unfold expand_instr in EXP; destruct instr; simpl in DEFS;
+  try (econstructor; eauto; fail).
+(* call *)
+  destruct (can_inline fe s1) as [|id f P Q].
+  (* not inlined *)
+  eapply tr_call; eauto. 
+  (* inlined *)
+  subst s1.
+  monadInv EXP. unfold inline_function in EQ; monadInv EQ.
+  set (ctx' := callcontext ctx x1 x2 (max_def_function f) (fn_stacksize f) n r).
+  inversion EQ0; inversion EQ1; inversion EQ. inv_incr. 
+  apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto.
+  eapply BASE; eauto. 
+  eapply add_moves_spec; eauto.
+    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega.
+  eapply rec_spec; eauto.
+    red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto.
+    simpl. subst s2; simpl in *; xomega.
+    simpl. subst s3; simpl in *; xomega.
+    simpl. xomega.
+    simpl. apply align_divides. apply min_alignment_pos.
+    assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega.
+    omega.
+    intros. simpl in H. rewrite S1.
+    transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
+    eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. 
+  red; simpl. subst s2; simpl in *; xomega.
+  red; simpl. split. auto. apply align_le. apply min_alignment_pos.
+(* tailcall *)
+  destruct (can_inline fe s1) as [|id f P Q].
+  (* not inlined *)
+  destruct (retinfo ctx) as [[rpc rreg] | ]_eqn. 
+  (* turned into a call *)
+  eapply tr_tailcall_call; eauto. 
+  (* preserved *)
+  eapply tr_tailcall; eauto. 
+  (* inlined *)
+  subst s1.
+  monadInv EXP. unfold inline_function in EQ; monadInv EQ.
+  set (ctx' := tailcontext ctx x1 x2 (max_def_function f) (fn_stacksize f)) in *.
+  inversion EQ0; inversion EQ1; inversion EQ. inv_incr. 
+  apply tr_tailcall_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto.
+  eapply BASE; eauto. 
+  eapply add_moves_spec; eauto.
+    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega.
+  eapply rec_spec; eauto.
+    red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto.
+    simpl. subst s2; simpl in *; xomega.
+    simpl. subst s3; simpl in *; xomega.
+    simpl. xomega.
+    simpl. apply align_divides. apply min_alignment_pos.
+    assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega.
+    omega.
+    intros. simpl in H. rewrite S1.
+    transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
+    eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. 
+  red; simpl. subst s2; simpl in *; xomega.
+  red; auto.
+(* return *)
+  destruct (retinfo ctx) as [[rpc rreg] | ]_eqn. 
+  (* inlined *)
+  eapply tr_return_inlined; eauto. 
+  (* unchanged *)
+  eapply tr_return; eauto. 
+Qed.
+
+Lemma iter_expand_instr_spec:
+  forall ctx l s x s' i c,
+  mlist_iter2 (expand_instr fe rec ctx) l s = R x s' i ->
+  list_norepet (List.map (@fst _ _) l) ->
+  (forall pc instr, In (pc, instr) l -> Ple (max_def_instr instr) ctx.(mreg)) ->
+  (forall pc instr, In (pc, instr) l -> Ple (spc ctx pc) s.(st_nextnode)) ->
+  Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
+  ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 ->
+  s'.(st_stksize) <= stacksize ->
+  (forall pc', Plt s.(st_nextnode) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  (forall pc instr, In (pc, instr) l -> c!(spc ctx pc) = s'.(st_code)!(spc ctx pc)) ->
+  forall pc instr, In (pc, instr) l -> tr_instr ctx pc instr c.
+Proof.
+  induction l; simpl; intros.
+  (* base case *)
+  contradiction.
+  (* inductive case *)
+  destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
+  assert (A: Ple ctx.(dpc) s0.(st_nextnode)).
+    assert (B: Ple (spc ctx pc) (st_nextnode s)) by eauto. unfold spc in B; xomega.
+  destruct H9. inv H.
+  (* same pc *)
+  eapply expand_instr_spec; eauto.
+  omega.
+  intros.
+    transitivity ((st_code s')!pc'). 
+    apply H7. auto. xomega. 
+    eapply iter_expand_instr_unchanged; eauto. 
+    red; intros. rewrite list_map_compose in H9. exploit list_in_map_inv; eauto. 
+    intros [[pc0 instr0] [P Q]]. simpl in P. 
+    assert (Ple (spc ctx pc0) (st_nextnode s)) by eauto. xomega.
+  transitivity ((st_code s')!(spc ctx pc)). 
+    eapply H8; eauto. 
+    eapply iter_expand_instr_unchanged; eauto. 
+    assert (Ple (spc ctx pc) (st_nextnode s)) by eauto. xomega.
+    red; intros. rewrite list_map_compose in H. exploit list_in_map_inv; eauto. 
+    intros [[pc0 instr0] [P Q]]. simpl in P. unfold spc in P. 
+    assert (pc = pc0) by (unfold node; xomega). subst pc0.
+    elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto.
+  (* older pc *)
+  inv_incr. eapply IHl; eauto. 
+  intros. eapply Ple_trans; eauto. 
+  intros; eapply Ple_trans; eauto.
+  intros. apply H7; auto. xomega.
+Qed.
+
+Lemma expand_cfg_rec_spec:
+  forall ctx f s x s' i c,
+  expand_cfg_rec fe rec ctx f s = R x s' i ->
+  Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
+  ctx.(mreg) = max_def_function f ->
+  Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
+  ctx.(mstk) >= 0 -> 
+  ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
+  (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
+  ctx.(dstk) >= 0 ->
+  s'.(st_stksize) <= stacksize ->
+  (forall pc', Plt ctx.(dpc) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  tr_funbody ctx f c.
+Proof.
+  intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. 
+  constructor. 
+  intros. rewrite H1. eapply max_def_function_params; eauto. 
+  intros. eapply iter_expand_instr_spec; eauto. 
+    apply PTree.elements_keys_norepet. 
+    intros. rewrite H1. eapply max_def_function_instr; eauto. 
+    eapply PTree.elements_complete; eauto.
+  intros.
+    assert (Ple pc0 (max_pc_function f)).
+      eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.  
+    unfold spc. subst s0; simpl; xomega.
+  subst s0; simpl; auto.
+  intros. apply H8; auto. subst s0; simpl in H11; xomega.
+  intros. apply H8. unfold spc; xomega. 
+    assert (Ple pc0 (max_pc_function f)).
+      eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.  
+    unfold spc. inversion i; xomega.
+  apply PTree.elements_correct; auto.
+  auto. auto. auto.
+  inversion INCR0. subst s0; simpl in STKSIZE; xomega.
+Qed.
+
+End EXPAND_INSTR.
+
+Lemma expand_cfg_unchanged:
+  forall fe ctx f s x s' i pc,
+  expand_cfg fe ctx f s = R x s' i ->
+  Ple ctx.(dpc) s.(st_nextnode) ->
+  Ple pc ctx.(dpc) ->
+  s'.(st_code)!pc = s.(st_code)!pc.
+Proof.
+  intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv).
+  apply well_founded_ltof.
+  intros. unfold expand_cfg in H0. rewrite unroll_Fixm in H0.
+  eapply expand_cfg_rec_unchanged; eauto. assumption. 
+Qed.
+
+Lemma expand_cfg_spec:
+  forall fe ctx f s x s' i c,
+  expand_cfg fe ctx f s = R x s' i ->
+  fenv_agree fe ->  
+  Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
+  ctx.(mreg) = max_def_function f ->
+  Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
+  ctx.(mstk) >= 0 -> 
+  ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
+  (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
+  ctx.(dstk) >= 0 ->
+  s'.(st_stksize) <= stacksize ->
+  (forall pc', Plt ctx.(dpc) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  tr_funbody ctx f c.
+Proof.
+  intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv).
+  apply well_founded_ltof.
+  intros. unfold expand_cfg in H0. rewrite unroll_Fixm in H0.
+  eapply expand_cfg_rec_spec; eauto. 
+  simpl. intros. eapply expand_cfg_unchanged; eauto. assumption.
+Qed.
+
+End INLINING_BODY_SPEC.
+
+(** ** Relational specification of the translation of a function *)
+
+Inductive tr_function: function -> function -> Prop :=
+  | tr_function_intro: forall f f' ctx,
+      tr_funbody f'.(fn_stacksize) ctx f f'.(fn_code) ->
+      ctx.(dstk) = 0 ->
+      ctx.(retinfo) = None ->
+      f'.(fn_sig) = f.(fn_sig) ->
+      f'.(fn_params) = sregs ctx f.(fn_params) ->
+      f'.(fn_entrypoint) = spc ctx f.(fn_entrypoint) ->
+      0 <= fn_stacksize f' <= Int.max_unsigned ->
+      tr_function f f'.
+
+Lemma transf_function_spec:
+  forall f f', transf_function fenv f = OK f' -> tr_function f f'.
+Proof.
+  intros. unfold transf_function in H.
+  destruct (expand_function fenv f initstate) as [ctx s i]_eqn. 
+  destruct (zle (st_stksize s) Int.max_unsigned); inv H.
+  monadInv Heqr. set (ctx := initcontext x x0 (max_def_function f) (fn_stacksize f)) in *.
+Opaque initstate.
+  destruct INCR3. inversion EQ1. inversion EQ.
+  apply tr_function_intro with ctx; auto.
+  eapply expand_cfg_spec with (fe := fenv); eauto.
+    red; auto.
+    unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega.
+    unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega.
+    simpl. xomega.
+    simpl. apply Zdivide_0. 
+    simpl. omega.
+  simpl. omega.
+  simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. 
+  simpl. change 0 with (st_stksize initstate). omega. 
+Qed.
+
+End INLINING_SPEC.
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index adff483..bb360eb 100644
--- a/backend/PrintLTLin.ml
+++ b/backend/PrintLTLin.ml
@@ -90,29 +90,26 @@ let print_instruction pp i =
   | Lreturn (Some arg) ->
       fprintf pp "return %a@ " reg arg
 
-let print_function pp f =
-  fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params;
+let print_function pp id f =
+  fprintf pp "@[<v 2>%s(%a) {@ " (extern_atom id) regs f.fn_params;
   List.iter (print_instruction pp) f.fn_code;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef pp fd =
+let print_fundef pp (id, fd) =
   match fd with
-  | Internal f -> print_function pp f
+  | Internal f -> print_function pp id f
   | External _ -> ()
 
+let print_program pp prog =
+  List.iter (print_fundef pp) prog.prog_funct
+
 let destination : string option ref = ref None
-let currpp : formatter option ref = ref None
 
-let print_if fd =
+let print_if prog =
   match !destination with
   | None -> ()
   | Some f ->
-      let pp =
-        match !currpp with
-        | Some pp -> pp
-        | None ->
-            let oc = open_out f in
-            let pp = formatter_of_out_channel oc in
-            currpp := Some pp;
-            pp
-      in print_fundef pp fd
+      let oc = open_out f in
+      let pp = formatter_of_out_channel oc in
+      print_program pp prog;
+      close_out oc
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index a6a1cc5..03977a6 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -97,29 +97,26 @@ let print_instruction pp i =
   | Mreturn ->
       fprintf pp "return@ "
 
-let print_function pp f =
-  fprintf pp "@[<v 2>f() {@ ";
+let print_function pp id f =
+  fprintf pp "@[<v 2>%s() {@ " (extern_atom id);
   List.iter (print_instruction pp) f.fn_code;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef pp fd =
+let print_fundef pp (id, fd) =
   match fd with
-  | Internal f -> print_function pp f
+  | Internal f -> print_function pp id f
   | External _ -> ()
 
+let print_program pp prog =
+  List.iter (print_fundef pp) prog.prog_funct
+
 let destination : string option ref = ref None
-let currpp : formatter option ref = ref None
 
-let print_if fd =
+let print_if prog =
   match !destination with
   | None -> ()
   | Some f ->
-      let pp =
-        match !currpp with
-        | Some pp -> pp
-        | None ->
-            let oc = open_out f in
-            let pp = formatter_of_out_channel oc in
-            currpp := Some pp;
-            pp
-      in print_fundef pp fd
+      let oc = open_out f in
+      let pp = formatter_of_out_channel oc in
+      print_program pp prog;
+      close_out oc
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 985bd63..4fc8f56 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -90,8 +90,8 @@ let print_instruction pp (pc, i) =
   | Ireturn (Some arg) ->
       fprintf pp "return %a@ " reg arg
 
-let print_function pp f =
-  fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params;
+let print_function pp id f =
+  fprintf pp "@[<v 2>%s(%a) {@ " (extern_atom id) regs f.fn_params;
   let instrs =
     List.sort
       (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
@@ -103,42 +103,35 @@ let print_function pp f =
   List.iter (print_instruction pp) instrs;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef pp fd =
+let print_fundef pp (id, fd) =
   match fd with
-  | Internal f -> print_function pp f
+  | Internal f -> print_function pp id f
   | External _ -> ()
 
-let print_if optdest currpp fd =
+let print_program pp (prog: RTL.program) =
+  List.iter (print_fundef pp) prog.prog_funct
+
+let print_if optdest prog =
   match !optdest with
   | None -> ()
   | Some f ->
-      let pp =
-        match !currpp with
-        | Some pp -> pp
-        | None ->
-            let oc = open_out f in
-            let pp = formatter_of_out_channel oc in
-            currpp := Some pp;
-            pp
-      in print_fundef pp fd
+      let oc = open_out f in
+      let pp = formatter_of_out_channel oc in
+      print_program pp prog;
+      close_out oc
 
 let destination_rtl : string option ref = ref None
-let pp_rtl : formatter option ref = ref None
-let print_rtl = print_if destination_rtl pp_rtl
+let print_rtl = print_if destination_rtl
 
 let destination_tailcall : string option ref = ref None
-let pp_tailcall : formatter option ref = ref None
-let print_tailcall = print_if destination_tailcall pp_tailcall
+let print_tailcall = print_if destination_tailcall
 
-let destination_castopt : string option ref = ref None
-let pp_castopt : formatter option ref = ref None
-let print_castopt = print_if destination_castopt pp_castopt
+let destination_inlining : string option ref = ref None
+let print_inlining = print_if destination_inlining
 
 let destination_constprop : string option ref = ref None
-let pp_constprop : formatter option ref = ref None
-let print_constprop = print_if destination_constprop pp_constprop
+let print_constprop = print_if destination_constprop
 
 let destination_cse : string option ref = ref None
-let pp_cse : formatter option ref = ref None
-let print_cse = print_if destination_cse pp_cse
+let print_cse = print_if destination_cse
 
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 28d2b06..86c1177 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -557,19 +557,28 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do no <- add_instr (Istore chunk addr rl r nd);
       do ns <- transl_expr map b r no;
          transl_exprlist map al rl ns
-  | Scall optid sig b cl =>
+  | Scall optid sig (inl b) cl =>
       do rf <- alloc_reg map b;
       do rargs <- alloc_regs map cl;
       do r <- alloc_optreg map optid;
       do n1 <- add_instr (Icall sig (inl _ rf) rargs r nd);
       do n2 <- transl_exprlist map cl rargs n1;
          transl_expr map b rf n2
-  | Stailcall sig b cl =>
+  | Scall optid sig (inr id) cl =>
+      do rargs <- alloc_regs map cl;
+      do r <- alloc_optreg map optid;
+      do n1 <- add_instr (Icall sig (inr _ id) rargs r nd);
+      transl_exprlist map cl rargs n1
+  | Stailcall sig (inl b) cl =>
       do rf <- alloc_reg map b;
       do rargs <- alloc_regs map cl;
       do n1 <- add_instr (Itailcall sig (inl _ rf) rargs);
       do n2 <- transl_exprlist map cl rargs n1;
          transl_expr map b rf n2
+  | Stailcall sig (inr id) cl =>
+      do rargs <- alloc_regs map cl;
+      do n1 <- add_instr (Itailcall sig (inr _ id) rargs);
+      transl_exprlist map cl rargs n1
   | Sbuiltin optid ef al =>
       do rargs <- alloc_regs map al;
       do r <- alloc_optreg map optid;
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index c5182db..e06224a 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1142,7 +1142,8 @@ Proof.
   econstructor; eauto. constructor.
 
   (* call *)
-  inv TS. 
+  inv TS; inv H.
+  (* indirect *)
   exploit transl_expr_correct; eauto.
   intros [rs' [A [B [C D]]]].
   exploit transl_exprlist_correct; eauto.
@@ -1154,9 +1155,21 @@ Proof.
   apply sig_transl_function; auto.
   traceEq.
   rewrite G. constructor. auto. econstructor; eauto.
+  (* direct *)
+  exploit transl_exprlist_correct; eauto.
+  intros [rs'' [E [F [G J]]]].
+  exploit functions_translated; eauto. intros [tf' [P Q]].
+  econstructor; split.
+  left; eapply plus_right. eexact E.
+  eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H4. 
+    rewrite Genv.find_funct_find_funct_ptr in P. eauto. 
+  apply sig_transl_function; auto.
+  traceEq.
+  rewrite G. constructor. auto. econstructor; eauto.
 
   (* tailcall *)
-  inv TS. 
+  inv TS; inv H.
+  (* indirect *)
   exploit transl_expr_correct; eauto.
   intros [rs' [A [B [C D]]]].
   exploit transl_exprlist_correct; eauto.
@@ -1168,7 +1181,21 @@ Proof.
   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.
+  rewrite H; eauto.
+  traceEq.
+  rewrite G. constructor; auto.
+  (* direct *)
+  exploit transl_exprlist_correct; eauto.
+  intros [rs'' [E [F [G J]]]].
+  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. eexact E.
+  eapply exec_Itailcall; eauto. simpl. rewrite symbols_preserved. rewrite H5. 
+  rewrite Genv.find_funct_find_funct_ptr in P. eauto. 
+  apply sig_transl_function; auto.
+  rewrite H; eauto.
   traceEq.
   rewrite G. constructor; auto.
 
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 9b2e63e..f6c59fc 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -865,12 +865,21 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
      c!n2 = Some (Icall sig (inl _ rf) rargs rd nd) ->
      reg_map_ok map rd optid ->
-     tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret
+     tr_stmt c map (Scall optid sig (inl _ b) cl) ns nd nexits ngoto nret rret
+  | tr_Scall_imm: forall optid sig id cl ns nd nexits ngoto nret rret rd n2 rargs,
+     tr_exprlist c map nil cl ns n2 rargs ->
+     c!n2 = Some (Icall sig (inr _ id) rargs rd nd) ->
+     reg_map_ok map rd optid ->
+     tr_stmt c map (Scall optid sig (inr _ id) cl) ns nd nexits ngoto nret rret
   | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs,
      tr_expr c map nil b ns n1 rf None ->
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
      c!n2 = Some (Itailcall sig (inl _ rf) rargs) ->
-     tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret
+     tr_stmt c map (Stailcall sig (inl _ b) cl) ns nd nexits ngoto nret rret
+  | tr_Stailcall_imm: forall sig id cl ns nd nexits ngoto nret rret n2 rargs,
+     tr_exprlist c map nil cl ns n2 rargs ->
+     c!n2 = Some (Itailcall sig (inr _ id) rargs) ->
+     tr_stmt c map (Stailcall sig (inr _ id) cl) ns nd nexits ngoto nret rret
   | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 rargs,
      tr_exprlist c map nil al ns n1 rargs ->
      c!n1 = Some (Ibuiltin ef rargs rd nd) ->
@@ -1251,23 +1260,34 @@ Proof.
   apply tr_expr_incr with s3; auto.
   eapply transl_expr_charact; eauto 4 with rtlg.
   (* Scall *)
+  destruct s0 as [b | id]; monadInv TR; saturateTrans.
+  (* indirect *)
   econstructor; eauto 4 with rtlg.
   eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_exprlist_incr with s5. auto. 
   eapply transl_exprlist_charact; eauto 3 with rtlg.
-  eapply alloc_regs_target_ok with (s1 := s1); eauto 3 with rtlg.
+  eapply alloc_regs_target_ok with (s1 := s0); eauto 3 with rtlg.
   apply regs_valid_cons; eauto 3 with rtlg.
-  apply regs_valid_incr with s1; eauto 3 with rtlg.
+  apply regs_valid_incr with s0; eauto 3 with rtlg.
   apply regs_valid_cons; eauto 3 with rtlg.
   apply regs_valid_incr with s2; eauto 3 with rtlg.
   eapply alloc_optreg_map_ok with (s1 := s2); eauto 3 with rtlg.
+  (* direct *)
+  econstructor; eauto 4 with rtlg.
+  eapply transl_exprlist_charact; eauto 3 with rtlg.
+  eapply alloc_optreg_map_ok with (s1 := s0); eauto 3 with rtlg.
   (* Stailcall *)
-  assert (RV: regs_valid (x :: nil) s1).
+  destruct s0 as [b | id]; monadInv TR; saturateTrans.
+  (* indirect *)
+  assert (RV: regs_valid (x :: nil) s0).
     apply regs_valid_cons; eauto 3 with rtlg. 
   econstructor; eauto 3 with rtlg.
   eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_exprlist_incr with s4; auto.
   eapply transl_exprlist_charact; eauto 4 with rtlg.
+  (* direct *)
+  econstructor; eauto 3 with rtlg.
+  eapply transl_exprlist_charact; eauto 4 with rtlg.
   (* Sbuiltin *)
   econstructor; eauto 4 with rtlg.
   eapply transl_exprlist_charact; eauto 3 with rtlg.
diff --git a/backend/Renumber.v b/backend/Renumber.v
new file mode 100644
index 0000000..b933bba
--- /dev/null
+++ b/backend/Renumber.v
@@ -0,0 +1,81 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Postorder renumbering of RTL control-flow graphs. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Postorder.
+Require Import AST.
+Require Import RTL.
+
+(** CompCert's dataflow analyses (module [Kildall]) are more precise
+  and run faster when the sequence [1, 2, 3, ...]  is a postorder
+  enumeration of the nodes of the control-flow graph.  This property
+  can be guaranteed when generating the CFG (module [RTLgen]), but
+  is, however, invalidated by further RTL optimization passes such as
+  [Inlining].  
+
+  In this module, we renumber the nodes of RTL control-flow graphs
+  to restore the postorder property given above.  In passing,
+  we also eliminate CFG nodes that are not reachable from the entry point:
+  these nodes are dead code. *)
+
+Section RENUMBER.
+
+Variable pnum: PTree.t positive.   (**r a postorder numbering *)
+
+Definition renum_pc (pc: node) : node :=
+  match pnum!pc with
+  | Some pc' => pc'
+  | None => 1%positive          (**r impossible case, never exercised *)
+  end.
+
+Definition renum_instr (i: instruction) : instruction :=
+  match i with
+  | Inop s => Inop (renum_pc s)
+  | Iop op args res s => Iop op args res (renum_pc s)
+  | Iload chunk addr args res s => Iload chunk addr args res (renum_pc s)
+  | Istore chunk addr args src s => Istore chunk addr args src (renum_pc s)
+  | Icall sg ros args res s => Icall sg ros args res (renum_pc s)
+  | Itailcall sg ros args => i
+  | Ibuiltin ef args res s => Ibuiltin ef args res (renum_pc s)
+  | Icond cond args s1 s2 => Icond cond args (renum_pc s1) (renum_pc s2)
+  | Ijumptable arg tbl => Ijumptable arg (List.map renum_pc tbl)
+  | Ireturn or => i
+  end.
+
+Definition renum_node (c': code) (pc: node) (i: instruction) : code :=
+  match pnum!pc with
+  | None => c'
+  | Some pc' => PTree.set pc' (renum_instr i) c'
+  end.
+
+Definition renum_cfg (c: code) : code :=
+  PTree.fold renum_node c (PTree.empty instruction).
+
+End RENUMBER.
+
+Definition transf_function (f: function) : function :=
+  let pnum := postorder (successors f) f.(fn_entrypoint) in
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (renum_cfg pnum f.(fn_code))
+    (renum_pc pnum f.(fn_entrypoint)).
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  AST.transform_program transf_fundef p.
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
new file mode 100644
index 0000000..a1b32b8
--- /dev/null
+++ b/backend/Renumberproof.v
@@ -0,0 +1,268 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Postorder renumbering of RTL control-flow graphs. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Postorder.
+Require Import AST.
+Require Import Values.
+Require Import Events.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Smallstep.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Renumber.
+
+Section PRESERVATION.
+
+Variable prog: program.
+Let tprog := transf_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog).
+
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof (@Genv.find_var_info_transf _ _ _ transf_fundef prog).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; reflexivity.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  unfold find_function; intros. destruct ros as [r|id]. 
+  eapply functions_translated; eauto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+(** Effect of an injective renaming of nodes on a CFG. *)
+
+Section RENUMBER.
+
+Variable f: PTree.t positive.
+
+Hypothesis f_inj: forall x1 x2 y, f!x1 = Some y -> f!x2 = Some y -> x1 = x2.
+
+Lemma renum_cfg_nodes:
+  forall c x y i,
+  c!x = Some i -> f!x = Some y -> (renum_cfg f c)!y = Some(renum_instr f i).
+Proof.
+  set (P := fun (c c': code) =>
+              forall x y i, c!x = Some i -> f!x = Some y -> c'!y = Some(renum_instr f i)).
+  intros c0. change (P c0 (renum_cfg f c0)). unfold renum_cfg. 
+  apply PTree_Properties.fold_rec; unfold P; intros.
+  (* extensionality *)
+  eapply H0; eauto. rewrite H; auto. 
+  (* base *)
+  rewrite PTree.gempty in H; congruence.
+  (* induction *)
+  rewrite PTree.gsspec in H2. unfold renum_node. destruct (peq x k). 
+  inv H2. rewrite H3. apply PTree.gss. 
+  destruct f!k as [y'|]_eqn. 
+  rewrite PTree.gso. eauto. red; intros; subst y'. elim n. eapply f_inj; eauto. 
+  eauto. 
+Qed.
+
+End RENUMBER.
+
+Definition pnum (f: function) := postorder (successors f) f.(fn_entrypoint).
+
+Definition reach (f: function) (pc: node) := reachable (successors f) f.(fn_entrypoint) pc.
+
+Lemma transf_function_at:
+  forall f pc i,
+  f.(fn_code)!pc = Some i ->
+  reach f pc ->
+  (transf_function f).(fn_code)!(renum_pc (pnum f) pc) = Some(renum_instr (pnum f) i).
+Proof.
+  intros. 
+  destruct (postorder_correct (successors f) f.(fn_entrypoint)) as [A B].
+  fold (pnum f) in *. 
+  unfold renum_pc. destruct (pnum f)! pc as [pc'|]_eqn.
+  simpl. eapply renum_cfg_nodes; eauto.
+  elim (B pc); auto. unfold successors. rewrite PTree.gmap1. rewrite H. simpl. congruence.
+Qed.
+
+Ltac TR_AT :=
+  match goal with
+  | [ A: (fn_code _)!_ = Some _ , B: reach _ _ |- _ ] =>
+        generalize (transf_function_at _ _ _ A B); simpl renum_instr; intros
+  end.
+
+Lemma reach_succ:
+  forall f pc i s,
+  f.(fn_code)!pc = Some i -> In s (successors_instr i) ->
+  reach f pc -> reach f s.
+Proof.
+  unfold reach; intros. econstructor; eauto. 
+  unfold successors. rewrite PTree.gmap1. rewrite H. auto. 
+Qed.
+  
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+  | match_frames_intro: forall res f sp pc rs
+        (REACH: reach f pc),
+      match_frames (Stackframe res f sp pc rs)
+                   (Stackframe res (transf_function f) sp (renum_pc (pnum f) pc) rs).
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+        (STACKS: list_forall2 match_frames stk stk')
+        (REACH: reach f pc),
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp (renum_pc (pnum f) pc) rs m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | match_returnstates: forall stk v m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v m).
+
+Lemma step_simulation:
+  forall S1 t S2, RTL.step ge S1 t S2 ->
+  forall S1', match_states S1 S1' ->
+  exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
+Proof.
+  induction 1; intros S1' MS; inv MS; try TR_AT.
+(* nop *)
+  econstructor; split. eapply exec_Inop; eauto. 
+  constructor; auto. eapply reach_succ; eauto. simpl; auto. 
+(* op *)
+  econstructor; split.
+  eapply exec_Iop; eauto.
+  instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. 
+  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+(* load *)
+  econstructor; split.
+  eapply exec_Iload; eauto.
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. 
+  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+(* store *)
+  econstructor; split.
+  eapply exec_Istore; eauto.
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. 
+  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+(* call *)
+  econstructor; split.
+  eapply exec_Icall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. constructor; auto. constructor. eapply reach_succ; eauto. simpl; auto.
+(* tailcall *)
+  econstructor; split.
+  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. auto.
+(* builtin *)
+  econstructor; split.
+  eapply exec_Ibuiltin; eauto.
+    eapply external_call_symbols_preserved; eauto.
+    exact symbols_preserved. exact varinfo_preserved.
+  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+(* cond *)
+  econstructor; split.
+  eapply exec_Icond; eauto. 
+  replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot)
+     with (renum_pc (pnum f) (if b then ifso else ifnot)).
+  constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto. 
+  destruct b; auto.
+(* jumptbl *)
+  econstructor; split.
+  eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto. 
+  constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto. 
+(* return *)
+  econstructor; split.
+  eapply exec_Ireturn; eauto. 
+  constructor; auto.
+(* internal function *)
+  simpl. econstructor; split.
+  eapply exec_function_internal; eauto. 
+  constructor; auto. unfold reach. constructor. 
+(* external function *)
+  econstructor; split.
+  eapply exec_function_external; eauto.
+    eapply external_call_symbols_preserved; eauto.
+    exact symbols_preserved. exact varinfo_preserved.
+  constructor; auto.
+(* return *)
+  inv STACKS. inv H1.
+  econstructor; split. 
+  eapply exec_return; eauto. 
+  constructor; auto.
+Qed.
+
+Lemma transf_initial_states:
+  forall S1, RTL.initial_state prog S1 ->
+  exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
+Proof.
+  intros. inv H. econstructor; split.
+  econstructor. 
+    eapply Genv.init_mem_transf; eauto. 
+    simpl. rewrite symbols_preserved. eauto. 
+    eapply function_ptr_translated; eauto. 
+    rewrite <- H3; apply sig_preserved.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_step.
+  eexact symbols_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation. 
+Qed.
+
+End PRESERVATION.
+
+
+
+ 
+
+  
+
diff --git a/backend/Selection.v b/backend/Selection.v
index ef627d7..11654f1 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -171,7 +171,13 @@ Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
   | a :: bl => Econs (sel_expr a) (sel_exprlist bl)
   end.
 
-(** Recognition of calls to built-in functions that should be inlined *)
+(** Recognition of immediate calls and calls to built-in functions
+    that should be inlined *)
+
+Inductive call_kind : Type :=
+  | Call_default
+  | Call_imm (id: ident)
+  | Call_builtin (ef: external_function).
 
 Definition expr_is_addrof_ident (e: Cminor.expr) : option ident :=
   match e with
@@ -180,16 +186,16 @@ Definition expr_is_addrof_ident (e: Cminor.expr) : option ident :=
   | _ => None
   end.
 
-Definition expr_is_addrof_builtin (ge: Cminor.genv) (e: Cminor.expr) : option external_function :=
+Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind :=
   match expr_is_addrof_ident e with
-  | None => None
+  | None => Call_default
   | Some id =>
       match Genv.find_symbol ge id with
-      | None => None
+      | None => Call_imm id
       | Some b =>
           match Genv.find_funct_ptr ge b with
-          | Some(External ef) => if ef_inline ef then Some ef else None
-          | _ => None
+          | Some(External ef) => if ef_inline ef then Call_builtin ef else Call_imm id
+          | _ => Call_imm id
           end
       end
   end.
@@ -202,14 +208,18 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt :=
   | Cminor.Sassign id e => Sassign id (sel_expr e)
   | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
   | Cminor.Scall optid sg fn args =>
-      match expr_is_addrof_builtin ge fn with
-      | None => Scall optid sg (sel_expr fn) (sel_exprlist args)
-      | Some ef => Sbuiltin optid ef (sel_exprlist args)
+      match classify_call ge fn with
+      | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)
+      | Call_imm id  => Scall optid sg (inr _ id) (sel_exprlist args)
+      | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args)
       end
   | Cminor.Sbuiltin optid ef args =>
       Sbuiltin optid ef (sel_exprlist args)
   | Cminor.Stailcall sg fn args => 
-      Stailcall sg (sel_expr fn) (sel_exprlist args)
+      match classify_call ge fn with
+      | Call_imm id  => Stailcall sg (inr _ id) (sel_exprlist args)
+      | _            => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args)
+      end
   | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2)
   | Cminor.Sifthenelse e ifso ifnot =>
       Sifthenelse (condexpr_of_expr (sel_expr e))
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 2a0efd5..4e67181 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -270,21 +270,27 @@ Proof.
   predSpec Int.eq Int.eq_spec i0 Int.zero; congruence.
 Qed.
 
-Lemma expr_is_addrof_builtin_correct:
-  forall ge sp e m a v ef fd,
-  expr_is_addrof_builtin ge a = Some ef ->
+Lemma classify_call_correct:
+  forall ge sp e m a v fd,
   Cminor.eval_expr ge sp e m a v ->
   Genv.find_funct ge v = Some fd ->
-  fd = External ef.
+  match classify_call ge a with
+  | Call_default => True
+  | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Int.zero
+  | Call_builtin ef => fd = External ef
+  end.
 Proof.
-  intros until fd; unfold expr_is_addrof_builtin.
-  case_eq (expr_is_addrof_ident a); intros; try congruence.
-  exploit expr_is_addrof_ident_correct; eauto. intro EQ; subst a.
-  inv H1. inv H4. 
-  destruct (Genv.find_symbol ge i); try congruence.
-  rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. 
-  destruct fd; try congruence. 
-  destruct (ef_inline e0); congruence.
+  unfold classify_call; intros. 
+  destruct (expr_is_addrof_ident a) as [id|]_eqn. 
+  exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a.
+  inv H. inv H2. 
+  destruct (Genv.find_symbol ge id) as [b|]_eqn. 
+  rewrite Genv.find_funct_find_funct_ptr in H0. 
+  rewrite H0. 
+  destruct fd. exists b; auto. 
+  destruct (ef_inline e0). auto. exists b; auto.
+  simpl in H0. discriminate.
+  auto.
 Qed.
 
 (** Compatibility of evaluation functions with the "less defined than" relation. *)
@@ -539,7 +545,9 @@ Proof.
 (* store *)
   unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
 (* call *)
-  destruct (expr_is_addrof_builtin ge e); simpl; auto.
+  destruct (classify_call ge e); simpl; auto.
+(* tailcall *)
+  destruct (classify_call ge e); simpl; auto.
 (* seq *)
   exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. 
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
@@ -598,27 +606,38 @@ Proof.
   eapply eval_store; eauto.
   constructor; auto.
   (* Scall *)
-  exploit sel_expr_correct; eauto. intros [vf' [A B]].
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
-  destruct (expr_is_addrof_builtin ge a) as [ef|]_eqn.
-  (* Scall turned into Sbuiltin *)
-  exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd.
-  right; split. omega. split. auto. 
-  econstructor; eauto.
-  (* Scall preserved *)
+  exploit classify_call_correct; eauto. 
+  destruct (classify_call ge a) as [ | id | ef].
+  (* indirect *)
+  exploit sel_expr_correct; eauto. intros [vf' [A B]].
   left; econstructor; split.
-  econstructor; eauto.
+  econstructor; eauto. econstructor; eauto. 
   eapply functions_translated; eauto. 
   apply sig_function_translated.
   constructor; auto. constructor; auto.
+  (* direct *)
+  intros [b [U V]]. 
+  left; econstructor; split.
+  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto.
+  eapply functions_translated; eauto. subst vf; auto. 
+  apply sig_function_translated.
+  constructor; auto. constructor; auto.
+  (* turned into Sbuiltin *)
+  intros EQ. subst fd. 
+  right; split. omega. split. auto. 
+  econstructor; eauto.
   (* Stailcall *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   exploit sel_expr_correct; eauto. intros [vf' [A B]].
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
   left; econstructor; split.
-  econstructor; eauto.
-  eapply functions_translated; eauto. 
-  apply sig_function_translated.
+  exploit classify_call_correct; eauto. 
+  destruct (classify_call ge a) as [ | id | ef]; intros. 
+  econstructor; eauto. econstructor; eauto. eapply functions_translated; eauto. apply sig_function_translated.
+  destruct H2 as [b [U V]].
+  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. eapply functions_translated; eauto. subst vf; auto. apply sig_function_translated.
+  econstructor; eauto. econstructor; eauto. eapply functions_translated; eauto. apply sig_function_translated.
   constructor; auto. apply call_cont_commut; auto.
   (* Sbuiltin *)
   exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]].
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 2ec14aa..be5e4b9 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -423,13 +423,13 @@ Definition frame_perm_freeable (m: mem) (sp: block): Prop :=
   forall ofs,
   0 <= ofs < fe.(fe_size) ->
   ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
-  Mem.perm m sp ofs Freeable.
+  Mem.perm m sp ofs Cur Freeable.
 
 Lemma offset_of_index_perm:
   forall m sp idx,
   index_valid idx ->
   frame_perm_freeable m sp ->
-  Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Freeable.
+  Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Cur Freeable.
 Proof.
   intros.
   exploit offset_of_index_valid; eauto. intros [A B].
@@ -612,7 +612,7 @@ Record agree_frame (j: meminj) (ls ls0: locset)
 
     (** Bounds of the Linear stack data block *)
     agree_bounds:
-      Mem.bounds m sp = (0, f.(Linear.fn_stacksize));
+      forall ofs p, Mem.perm m sp ofs Max p -> 0 <= ofs < f.(Linear.fn_stacksize);
 
     (** Permissions on the frame part of the Mach stack block *)
     agree_perm:
@@ -928,16 +928,16 @@ Lemma agree_frame_invariant:
   forall j ls ls0 m sp m' sp' parent retaddr m1 m1',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   (Mem.valid_block m sp -> Mem.valid_block m1 sp) ->
-  (Mem.bounds m1 sp = Mem.bounds m sp) ->
+  (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) ->
   (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') ->
   (forall chunk ofs v,
      ofs + size_chunk chunk <= fe.(fe_stack_data) \/
      fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
      Mem.load chunk m' sp' ofs = Some v ->
      Mem.load chunk m1' sp' ofs = Some v) ->
-  (forall ofs p,
+  (forall ofs k p,
      ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
-     Mem.perm m' sp' ofs p -> Mem.perm m1' sp' ofs p) ->
+     Mem.perm m' sp' ofs k p -> Mem.perm m1' sp' ofs k p) ->
   agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
 Proof.
   intros.
@@ -950,7 +950,7 @@ Proof.
               index_contains_inj j m' sp' idx v -> index_contains_inj j m1' sp' idx v).
     intros. destruct H5 as [v' [A B]]. exists v'; split; auto. 
   inv H; constructor; auto; intros.
-  rewrite H1; auto.
+  eauto.
   red; intros. apply H4; auto.
 Qed.
 
@@ -960,7 +960,7 @@ Lemma agree_frame_extcall_invariant:
   forall j ls ls0 m sp m' sp' parent retaddr m1 m1',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   (Mem.valid_block m sp -> Mem.valid_block m1 sp) ->
-  (Mem.bounds m1 sp = Mem.bounds m sp) ->
+  (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) ->
   (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') ->
   mem_unchanged_on (loc_out_of_reach j m) m' m1' ->
   agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
@@ -970,7 +970,7 @@ Proof.
      ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
     loc_out_of_reach j m sp' ofs).
   intros; red; intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst.
-  rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H). unfold fst, snd. omega.
+  red; intros. exploit agree_bounds; eauto. omega. 
   eapply agree_frame_invariant; eauto.
   intros. apply H3. intros. apply REACH. omega. auto. 
   intros. apply H3; auto. 
@@ -992,17 +992,23 @@ Opaque Int.add.
   inv VINJ; simpl in *; try discriminate.
   eapply agree_frame_invariant; eauto.
   eauto with mem.
-  eapply Mem.bounds_store; eauto. 
+  eauto with mem.
   eauto with mem.
   intros. rewrite <- H1. eapply Mem.load_store_other; eauto. 
     destruct (zeq sp' b2); auto.
     subst b2. right.
     exploit agree_inj_unique; eauto. intros [P Q]. subst b1 delta.
     exploit Mem.store_valid_access_3. eexact STORE1. intros [A B].
-    exploit Mem.range_perm_in_bounds. eexact A. generalize (size_chunk_pos chunk); omega.
-    rewrite (agree_bounds _ _ _ _ _ _ _ _ _ AG). unfold fst,snd. intros [C D].
-    rewrite shifted_stack_offset_no_overflow. omega.
-    generalize (size_chunk_pos chunk); omega. 
+    rewrite shifted_stack_offset_no_overflow.
+    exploit agree_bounds. eauto. apply Mem.perm_cur_max. apply A. 
+    instantiate (1 := Int.unsigned ofs1). generalize (size_chunk_pos chunk). omega.
+    intros C.
+    exploit agree_bounds. eauto. apply Mem.perm_cur_max. apply A. 
+    instantiate (1 := Int.unsigned ofs1 + size_chunk chunk - 1). generalize (size_chunk_pos chunk). omega.
+    intros D.
+    omega.
+    eapply agree_bounds. eauto. apply Mem.perm_cur_max. apply A. 
+    generalize (size_chunk_pos chunk). omega.
   intros; eauto with mem.
 Qed.
 
@@ -1325,7 +1331,7 @@ Qed.
 Lemma stores_in_frame_inject:
   forall j sp sp' m,
   (forall b delta, j b = Some(sp', delta) -> b = sp /\ delta = fe.(fe_stack_data)) ->
-  Mem.bounds m sp = (0, f.(Linear.fn_stacksize)) ->
+  (forall ofs k p, Mem.perm m sp ofs k p -> 0 <= ofs < f.(Linear.fn_stacksize)) ->
   forall m1 m2, stores_in_frame sp' m1 m2 -> Mem.inject j m m1 -> Mem.inject j m m2.
 Proof.
   induction 3; intros.
@@ -1333,7 +1339,7 @@ Proof.
   apply IHstores_in_frame.
   intros. eapply Mem.store_outside_inject; eauto.
   intros. exploit H; eauto. intros [A B]; subst.
-  rewrite H0; unfold fst, snd. omega.
+  exploit H0; eauto. omega. 
 Qed.
 
 Lemma stores_in_frame_valid:
@@ -1343,7 +1349,7 @@ Proof.
 Qed.
 
 Lemma stores_in_frame_perm:
-  forall b ofs p sp m m', stores_in_frame sp m m' -> Mem.perm m b ofs p -> Mem.perm m' b ofs p.
+  forall b ofs k p sp m m', stores_in_frame sp m m' -> Mem.perm m b ofs k p -> Mem.perm m' b ofs k p.
 Proof.
   induction 1; intros. auto. apply IHstores_in_frame. eauto with mem.
 Qed.
@@ -1396,8 +1402,9 @@ Proof.
     instantiate (1 := sp'). eauto with mem.
     instantiate (1 := fe_stack_data fe).
     generalize stack_data_offset_valid (bound_stack_data_pos b) size_no_overflow; omega.
-    right. rewrite (Mem.bounds_alloc_same _ _ _ _ _ ALLOC'). unfold fst, snd.
-    split. omega. apply size_no_overflow.
+    intros; right. 
+    exploit Mem.perm_alloc_inv. eexact ALLOC'. eauto. rewrite zeq_true. 
+    generalize size_no_overflow. omega. 
     intros. apply Mem.perm_implies with Freeable; auto with mem. 
     eapply Mem.perm_alloc_2; eauto.
     generalize stack_data_offset_valid bound_stack_data_stacksize; omega.
@@ -1495,7 +1502,7 @@ Proof.
     (* valid sp' *)
     eapply stores_in_frame_valid with (m := m2'); eauto with mem.
     (* bounds *)
-    eapply Mem.bounds_alloc_same; eauto.
+    exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto.
     (* perms *)
     auto.
     (* wt *)
@@ -1506,7 +1513,7 @@ Proof.
   split. eapply inject_alloc_separated; eauto with mem.
   (* inject *)
   split. eapply stores_in_frame_inject; eauto.
-  eapply Mem.bounds_alloc_same; eauto.
+  intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto.
   (* stores in frame *)
   auto.
 Qed.
@@ -1690,8 +1697,7 @@ Proof.
   simpl. rewrite H2. auto.
   intros. exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta.
   exists 0; exists (Linear.fn_stacksize f); split. auto with coqlib.
-  exploit Mem.perm_in_bounds; eauto. 
-  rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H0). auto.
+  eapply agree_bounds. eauto. eapply Mem.perm_max. eauto.  
   (* can execute epilogue *)
   exploit restore_callee_save_correct; eauto.
     instantiate (1 := rs). red; intros. 
@@ -1775,7 +1781,7 @@ Lemma match_stacks_change_linear_mem:
   forall j m1 m2 m' cs cs' sg bound bound',
   match_stacks j m1 m' cs cs' sg bound bound' ->
   (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
-  (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   match_stacks j m2 m' cs cs' sg bound bound'.
 Proof.
   induction 1; intros.
@@ -1784,7 +1790,7 @@ Proof.
   eapply agree_frame_invariant; eauto. 
   apply IHmatch_stacks.
   intros. apply H0; auto. omega.
-  intros. apply H1. omega.
+  intros. apply H1. omega. auto.
 Qed.
 
 (** Invariance with respect to change of [m']. *)
@@ -1793,7 +1799,7 @@ Lemma match_stacks_change_mach_mem:
   forall j m m1' m2' cs cs' sg bound bound',
   match_stacks j m m1' cs cs' sg bound bound' ->
   (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
-  (forall b ofs p, b < bound' -> Mem.perm m1' b ofs p -> Mem.perm m2' b ofs p) ->
+  (forall b ofs k p, b < bound' -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) ->
   (forall chunk b ofs v, b < bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) ->
   match_stacks j m m2' cs cs' sg bound bound'.
 Proof.
@@ -1813,7 +1819,7 @@ Lemma match_stacks_change_mem_extcall:
   forall j m1 m2 m1' m2' cs cs' sg bound bound',
   match_stacks j m1 m1' cs cs' sg bound bound' ->
   (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
-  (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
   mem_unchanged_on (loc_out_of_reach j m1) m1' m2' ->
   match_stacks j m2 m2' cs cs' sg bound bound'.
@@ -1824,7 +1830,7 @@ Proof.
   eapply agree_frame_extcall_invariant; eauto.
   apply IHmatch_stacks. 
   intros; apply H0; auto; omega.
-  intros; apply H1; omega.
+  intros; apply H1. omega. auto.
   intros; apply H2; auto; omega.
   auto.
 Qed.
@@ -1888,7 +1894,7 @@ Proof.
   eapply match_stacks_change_meminj; eauto. 
   eapply match_stacks_change_mem_extcall; eauto.
   intros; eapply external_call_valid_block; eauto.
-  intros; eapply external_call_bounds; eauto. red; omega.
+  intros; eapply external_call_max_perm; eauto. red; omega.
   intros; eapply external_call_valid_block; eauto.
 Qed.
 
@@ -2435,9 +2441,9 @@ Proof.
   econstructor; eauto with coqlib.
   eapply Mem.store_outside_inject; eauto. 
     intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta.
-    rewrite (agree_bounds _ _ _ _ _ _ _ _ _ _ AGFRAME). unfold fst, snd. rewrite Zplus_0_l. 
-    rewrite size_type_chunk. 
+    rewrite size_type_chunk in H5.
     exploit offset_of_index_disj_stack_data_2; eauto.
+    exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. 
     omega.
   apply match_stacks_change_mach_mem with m'; auto.
   eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega.
@@ -2546,7 +2552,7 @@ Proof.
   auto. 
   eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
   intros. rewrite <- H2. eapply Mem.load_free; eauto. left; unfold block; omega.
-  eauto with mem. intros. eapply Mem.bounds_free; eauto.
+  eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
   apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
   eapply find_function_well_typed; eauto.
@@ -2570,7 +2576,7 @@ Proof.
   eapply agree_frame_inject_incr; eauto. 
   apply agree_frame_extcall_invariant with m m'0; auto.
   eapply external_call_valid_block; eauto.
-  eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto.
+  intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto.
   eapply external_call_valid_block; eauto.
   eapply agree_valid_mach; eauto.
   inv WTI. simpl; rewrite H4. eapply external_call_well_typed; eauto.
@@ -2594,7 +2600,7 @@ Proof.
   eapply agree_frame_inject_incr; eauto. 
   apply agree_frame_extcall_invariant with m m'0; auto.
   eapply external_call_valid_block; eauto.
-  eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto.
+  intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto.
   eapply external_call_valid_block; eauto.
   eapply agree_valid_mach; eauto.
 
@@ -2652,7 +2658,7 @@ Proof.
   eauto. 
   eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
   intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega.
-  eauto with mem. intros. eapply Mem.bounds_free; eauto.
+  eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
   apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
   apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
@@ -2677,7 +2683,8 @@ Proof.
   apply match_stacks_change_linear_mem with m.
   rewrite SP_EQ; rewrite SP'_EQ.
   eapply match_stacks_change_meminj; eauto. omega.
-  eauto with mem. intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega. 
+  eauto with mem. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. 
+  rewrite zeq_false. auto. omega. 
   intros. eapply stores_in_frame_valid; eauto with mem. 
   intros. eapply stores_in_frame_perm; eauto with mem.
   intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto.
diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml
new file mode 100644
index 0000000..4139678
--- /dev/null
+++ b/backend/Unusedglob.ml
@@ -0,0 +1,91 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Removing unused definitions of static functions and global variables *)
+
+open Camlcoq
+open Maps
+open AST
+open Asm
+open Unusedglob1
+
+module IdentSet = Set.Make(struct type t = ident let compare = compare end)
+
+(* The set of globals referenced from a function definition *)
+
+let add_referenced_instr rf i =
+  List.fold_right IdentSet.add (referenced_instr i) rf
+
+let referenced_function f =
+  List.fold_left add_referenced_instr IdentSet.empty (code_of_function f)
+
+let referenced_fundef = function
+  | Internal f -> referenced_function f
+  | External ef -> IdentSet.empty
+
+(* The set of globals referenced from a variable definition (initialization) *)
+
+let add_referenced_init_data rf = function
+  | Init_addrof(id, ofs) -> IdentSet.add id rf
+  | _ -> rf
+
+let referenced_globvar gv =
+  List.fold_left add_referenced_init_data IdentSet.empty gv.gvar_init
+
+(* The map global |-> set of globals it references *)
+
+let use_map p =
+  List.fold_left (fun m (id, gv) -> PTree.set id (referenced_globvar gv) m)
+  (List.fold_left (fun m (id, fd) -> PTree.set id (referenced_fundef fd) m)
+   PTree.empty p.prog_funct) p.prog_vars
+
+(* Worklist algorithm computing the set of used globals *)
+
+let rec used_idents usemap used wrk =
+  match wrk with
+  | [] -> used
+  | id :: wrk ->
+      if IdentSet.mem id used then used_idents usemap used wrk else
+        match PTree.get id usemap with
+        | None -> used_idents usemap used wrk
+        | Some s -> used_idents usemap (IdentSet.add id used)
+                                       (IdentSet.fold (fun id l -> id::l) s wrk)
+
+(* The worklist is initially populated with all nonstatic globals *)
+
+let add_nonstatic wrk id =
+  if C2C.atom_is_static id then wrk else id :: wrk
+
+let initial_worklist p =
+  List.fold_left (fun wrk (id, gv) -> add_nonstatic wrk id)
+   (List.fold_left (fun wrk (id, fd) -> add_nonstatic wrk id)
+     [] p.prog_funct) p.prog_vars
+
+(* Eliminate unused definitions *)
+
+let rec filter used = function
+  | [] -> []
+  | (id, def) :: rem ->
+      if IdentSet.mem id used
+      then (id, def) :: filter used rem
+      else filter used rem
+
+let filter_prog used p =
+  { prog_funct = filter used p.prog_funct;
+    prog_main = p.prog_main;
+    prog_vars = filter used p.prog_vars }
+
+(* Entry point *)
+
+let transf_program p =
+  filter_prog (used_idents (use_map p) IdentSet.empty (initial_worklist p)) p
+