- Added alignment constraints to memory loads and stores.

- In Cminor and below, removed pointer validity check in semantics of 
  comparisons, so that evaluation of expressions is independent of
  memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.


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

38 files changed, 137 insertions, 537 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 3a5960b..2389a33 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -101,8 +101,6 @@ Definition transfer
            (reg_sum_live ros (reg_dead res after))
       | Itailcall sig ros args =>
 	  reg_list_live args (reg_sum_live ros Regset.empty)
-      | Ialloc arg res s =>
-          reg_live arg (reg_dead res after)
       | Icond cond args ifso ifnot =>
           reg_list_live args after
       | Ireturn optarg =>
@@ -167,8 +165,6 @@ Definition transf_instr
                 (assign res) s
   | Itailcall sig ros args =>
       Ltailcall sig (sum_left_map assign ros) (List.map assign args)
-  | Ialloc arg res s =>
-      Lalloc (assign arg) (assign res) s
   | Icond cond args ifso ifnot =>
       Lcond cond (List.map assign args) ifso ifnot
   | Ireturn optarg =>
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 5e38934..3971fb6 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -601,7 +601,7 @@ Proof.
   rewrite <- H1. eapply agree_move_live; eauto.
   (* Not a move *)
   intros INMO CORR CODE.
-  assert (eval_operation tge sp op (map ls (map assign args)) m = Some v).
+  assert (eval_operation tge sp op (map ls (map assign args)) = Some v).
     replace (map ls (map assign args)) with (rs##args).
     rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. 
     eapply agree_eval_regs; eauto.
@@ -671,25 +671,15 @@ Proof.
   rewrite (sig_function_translated _ _ TF). eauto.
   rewrite H1. econstructor; eauto.
 
-  (* Ialloc *)
-  assert (ls (assign arg) = Vint sz).
-    rewrite <- H0. symmetry. eapply agree_eval_reg; eauto.
-  econstructor; split.
-  eapply exec_Lalloc; eauto. TranslInstr.
-  generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). 
-  unfold correct_alloc_instr.  intros [CORR1 CORR2].
-  MatchStates.
-  eapply agree_postcall with (args := arg :: nil) (ros := inr reg 1%positive); eauto.
-
   (* Icond, true *)
-  assert (COND: eval_condition cond (map ls (map assign args)) m = Some true).
+  assert (COND: eval_condition cond (map ls (map assign args)) = Some true).
     replace (map ls (map assign args)) with (rs##args). auto.
     eapply agree_eval_regs; eauto.
   econstructor; split.
   eapply exec_Lcond_true; eauto. TranslInstr.
   MatchStates. eapply agree_reg_list_live. eauto.
   (* Icond, false *)
-  assert (COND: eval_condition cond (map ls (map assign args)) m = Some false).
+  assert (COND: eval_condition cond (map ls (map assign args)) = Some false).
     replace (map ls (map assign args)) with (rs##args). auto.
     eapply agree_eval_regs; eauto.
   econstructor; split.
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v
index d9ab17b..aba9660 100644
--- a/backend/Alloctyping.v
+++ b/backend/Alloctyping.v
@@ -139,8 +139,6 @@ Proof.
   split. autorewrite with allocty; auto.
   split. auto with allocty. auto.
   rewrite transf_unroll; auto.
-  (* alloc *)
-  WT.
   (* cond *)
   WT.
   (* return *)
diff --git a/backend/Bounds.v b/backend/Bounds.v
index e598245..d1ed28d 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -26,8 +26,7 @@ Require Import Conventions.
 (** The [bounds] record capture how many local and outgoing stack slots
   and callee-save registers are used by a function. *)
 
-(** We demand that all bounds are positive or null,
-  and moreover [bound_outgoing] is greater or equal to 6.
+(** We demand that all bounds are positive or null.
   These properties are used later to reason about the layout of
   the activation record. *)
 
@@ -104,7 +103,6 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lstore chunk addr args src => nil
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
-  | Lalloc => nil
   | Llabel lbl => nil
   | Lgoto lbl => nil
   | Lcond cond args lbl => nil
diff --git a/backend/CSE.v b/backend/CSE.v
index 49b8489..13e9be8 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -260,7 +260,7 @@ Definition equation_holds
      (vres: valnum) (rh: rhs) : Prop :=
   match rh with
   | Op op vl =>
-      eval_operation ge sp op (List.map valuation vl) m =
+      eval_operation ge sp op (List.map valuation vl) =
       Some (valuation vres)
   | Load chunk addr vl =>
       exists a,
@@ -348,8 +348,6 @@ Definition transfer (f: function) (pc: node) (before: numbering) :=
           empty_numbering
       | Itailcall sig ros args =>
           empty_numbering
-      | Ialloc arg res s =>
-          add_unknown before res
       | Icond cond args ifso ifnot =>
           before
       | Ireturn optarg =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index a87cd75..265bb20 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -232,7 +232,7 @@ Proof.
   apply wf_kill_loads; auto.
   apply wf_empty_numbering.
   apply wf_empty_numbering.
-  apply wf_add_unknown; auto.
+(*  apply wf_add_unknown; auto. *)
 Qed.
 
 (** As a consequence, the numberings computed by the static analysis
@@ -401,7 +401,7 @@ Definition rhs_evals_to
     (valu: valnum -> val) (rh: rhs) (v: val) : Prop :=
   match rh with
   | Op op vl => 
-      eval_operation ge sp op (List.map valu vl) m = Some v
+      eval_operation ge sp op (List.map valu vl) = Some v
   | Load chunk addr vl =>
       exists a,
       eval_addressing ge sp addr (List.map valu vl) = Some a /\
@@ -482,7 +482,7 @@ Lemma add_op_satisfiable:
   forall n rs op args dst v,
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
-  eval_operation ge sp op rs##args m = Some v ->
+  eval_operation ge sp op rs##args = Some v ->
   numbering_satisfiable ge sp (rs#dst <- v) m (add_op n dst op args).
 Proof.
   intros. inversion H0.
@@ -559,7 +559,7 @@ Proof.
   intros. destruct H0 as [valu [A B]].
   exists valu; split; intros.
   generalize (A _ _ H0). destruct rh; simpl.
-  intro. eapply eval_operation_alloc; eauto. 
+  auto.
   intros [addr [C D]]. exists addr; split. auto.
   destruct addr; simpl in *; try discriminate. 
   eapply Mem.load_alloc_other; eauto. 
@@ -595,7 +595,7 @@ Proof.
   generalize (kill_load_eqs_ops _ _ _ H5).
   destruct rh; simpl.
   intros. destruct addr; simpl in H; try discriminate. 
-  eapply eval_operation_store; eauto.
+  auto.
   tauto.
   apply H3. assumption.
 Qed.
@@ -651,7 +651,7 @@ Lemma find_op_correct:
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
   find_op n op args = Some r ->
-  eval_operation ge sp op rs##args m = Some rs#r.
+  eval_operation ge sp op rs##args = Some rs#r.
 Proof.
   intros until r. intros WF [valu NH].
   unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND.
@@ -841,14 +841,14 @@ Proof.
 
   (* Iop *)
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
-  assert (eval_operation tge sp op rs##args m = Some v).
+  assert (eval_operation tge sp op rs##args = Some v).
     rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
   generalize C; clear C.
   case (is_trivial_op op).
   intro. eapply exec_Iop'; eauto. 
   caseEq (find_op (analyze f)!!pc op args). intros r FIND CODE.
   eapply exec_Iop'; eauto. simpl. 
-  assert (eval_operation ge sp op rs##args m = Some rs#r).
+  assert (eval_operation ge sp op rs##args = Some rs#r).
     eapply find_op_correct; eauto.
     eapply wf_analyze; eauto.
   congruence.
@@ -910,16 +910,6 @@ Proof.
   apply sig_preserved. 
   econstructor; eauto. 
 
-  (* Ialloc *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- (Vptr b Int.zero)) m'); split.
-  eapply exec_Ialloc; eauto.
-  econstructor; eauto.
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
-  unfold transfer; rewrite H. 
-  apply add_unknown_satisfiable. apply wf_analyze; auto.
-  eapply alloc_satisfiable; eauto.
-
   (* Icond true *)
   econstructor; split.
   eapply exec_Icond_true; eauto. 
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 16f7c3d..35bf391 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -103,7 +103,6 @@ Inductive stmt : Set :=
   | Sstore : memory_chunk -> expr -> expr -> stmt
   | Scall : option ident -> signature -> expr -> list expr -> stmt
   | Stailcall: signature -> expr -> list expr -> stmt
-  | Salloc : ident -> expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: expr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -251,8 +250,11 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
 Definition eval_compare_mismatch (c: comparison) : option val :=
   match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end.
 
+Definition eval_compare_null (c: comparison) (n: int) : option val :=
+  if Int.eq n Int.zero then eval_compare_mismatch c else None.
+
 Definition eval_binop
-            (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
+            (op: binary_operation) (arg1 arg2: val): option val :=
   match op, arg1, arg2 with
   | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
   | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1))
@@ -286,17 +288,13 @@ Definition eval_binop
   | Ocmp c, Vint n1, Vint n2 =>
       Some (Val.of_bool(Int.cmp c n1 n2))
   | Ocmp c, Vptr b1 n1, Vptr b2 n2 =>
-      if valid_pointer m b1 (Int.signed n1)
-      && valid_pointer m b2 (Int.signed n2) then
-        if eq_block b1 b2
-        then Some(Val.of_bool(Int.cmp c n1 n2))
-        else eval_compare_mismatch c
-      else
-        None
+      if eq_block b1 b2
+      then Some(Val.of_bool(Int.cmp c n1 n2))
+      else eval_compare_mismatch c
   | Ocmp c, Vptr b1 n1, Vint n2 =>
-      if Int.eq n2 Int.zero then eval_compare_mismatch c else None
+      eval_compare_null c n2
   | Ocmp c, Vint n1, Vptr b2 n2 =>
-      if Int.eq n1 Int.zero then eval_compare_mismatch c else None
+      eval_compare_null c n1
   | Ocmpu c, Vint n1, Vint n2 =>
       Some (Val.of_bool(Int.cmpu c n1 n2))
   | Ocmpf c, Vfloat f1, Vfloat f2 =>
@@ -332,7 +330,7 @@ Inductive eval_expr: expr -> val -> Prop :=
   | eval_Ebinop: forall op a1 a2 v1 v2 v,
       eval_expr a1 v1 ->
       eval_expr a2 v2 ->
-      eval_binop op v1 v2 m = Some v ->
+      eval_binop op v1 v2 = Some v ->
       eval_expr (Ebinop op a1 a2) v
   | eval_Eload: forall chunk addr vaddr v,
       eval_expr addr vaddr ->
@@ -438,12 +436,6 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
         E0 (Callstate fd vargs (call_cont k) (Mem.free m sp))
 
-  | step_alloc: forall f id a k sp e m n m' b,
-      eval_expr sp e m a (Vint n) ->
-      Mem.alloc m 0 (Int.signed n) = (m', b) ->
-      step (State f (Salloc id a) k sp e m)
-        E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m')
-
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)
         E0 (State f s1 (Kseq s2 k) sp e m)
@@ -633,12 +625,6 @@ with exec_stmt:
       eval_funcall m f vargs t m' vres ->
       e' = set_optvar optid vres e ->
       exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal
-  | exec_Salloc:
-      forall sp e m id a n m' b,
-      eval_expr ge sp e m a (Vint n) ->
-      Mem.alloc m 0 (Int.signed n) = (m', b) ->
-      exec_stmt sp e m (Salloc id a) 
-                E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal
   | exec_Sifthenelse:
       forall sp e m a s1 s2 v b t e' m' out,
       eval_expr ge sp e m a v ->
@@ -805,10 +791,10 @@ Definition eval_funcall_exec_stmt_ind2
   (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop)
   (P2: val -> env -> mem -> stmt -> trace ->
               env -> mem -> outcome -> Prop) :=
-  fun a b c d e f g h i j k l m n o p q r =>
+  fun a b c d e f g h i j k l m n o p q =>
   conj
-    (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r)
-    (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r ).
+    (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q)
+    (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q).
 
 Inductive outcome_state_match
         (sp: val) (e: env) (m: mem) (f: function) (k: cont):
@@ -918,11 +904,6 @@ Proof.
   constructor. reflexivity. traceEq.
   subst e'. constructor.
 
-(* alloc *)
-  exists (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m'); split.
-  apply star_one. econstructor; eauto.
-  constructor.
-
 (* ifthenelse *)
   destruct (H2 f k) as [S [A B]].
   exists S; split.
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 1d5c8c0..bfe92a4 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -68,7 +68,6 @@ Inductive stmt : Set :=
   | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
   | Scall : option ident -> signature -> expr -> exprlist -> stmt
   | Stailcall: signature -> expr -> exprlist -> stmt
-  | Salloc : ident -> expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: condexpr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -162,7 +161,7 @@ Inductive eval_expr: letenv -> expr -> val -> Prop :=
       eval_expr le (Evar id) v
   | eval_Eop: forall le op al vl v,
       eval_exprlist le al vl ->
-      eval_operation ge sp op vl m = Some v ->
+      eval_operation ge sp op vl = Some v ->
       eval_expr le (Eop op al) v
   | eval_Eload: forall le chunk addr al vl vaddr v,
       eval_exprlist le al vl ->
@@ -188,7 +187,7 @@ with eval_condexpr: letenv -> condexpr -> bool -> Prop :=
       eval_condexpr le CEfalse false
   | eval_CEcond: forall le cond al vl b,
       eval_exprlist le al vl ->
-      eval_condition cond vl m = Some b ->
+      eval_condition cond vl = Some b ->
       eval_condexpr le (CEcond cond al) b
   | eval_CEcondition: forall le a b c vb1 vb2,
       eval_condexpr le a vb1 ->
@@ -294,12 +293,6 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
         E0 (Callstate fd vargs (call_cont k) (Mem.free m sp))
 
-  | step_alloc: forall f id a k sp e m n m' b,
-      eval_expr sp e m nil a (Vint n) ->
-      Mem.alloc m 0 (Int.signed n) = (m', b) ->
-      step (State f (Salloc id a) k sp e m)
-        E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m')
-
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)
         E0 (State f s1 (Kseq s2 k) sp e m)
diff --git a/backend/Coloring.v b/backend/Coloring.v
index 056aaa5..7204bc7 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -183,12 +183,6 @@ Definition add_edges_instr
       let largs := loc_arguments sig in
       add_prefs_call args largs
         (add_interf_call ros largs g)
-  | Ialloc arg res s =>
-      add_pref_mreg arg loc_alloc_argument
-        (add_pref_mreg res loc_alloc_result
-          (add_interf_op res live
-            (add_interf_destroyed
-              (Regset.remove res live) destroyed_at_call_regs g)))
   | Ireturn (Some r) =>
       add_pref_mreg r (loc_result sig) g
   | _ => g
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index ea31a29..c86652a 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -384,10 +384,6 @@ Proof.
   apply add_interf_destroyed_incl.
   eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
   apply add_interfs_call_incl.
-  eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
-  eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
-  eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
-  apply add_interf_destroyed_incl.
   destruct o.
   apply add_pref_mreg_incl.
   apply graph_incl_refl.
@@ -437,15 +433,6 @@ Definition correct_interf_instr
                                  interfere_mreg rfun mr g
         | inr idfun => True
       end
-  | Ialloc arg res s =>
-      (forall r mr,
-        Regset.In r live ->
-        In mr destroyed_at_call_regs ->
-        r <> res ->
-        interfere_mreg r mr g)
-   /\ (forall r,
-        Regset.In r live ->
-        r <> res -> interfere r res g)
   | _ =>
       True
   end.
@@ -467,9 +454,6 @@ Proof.
   split. intros. eapply interfere_incl; eauto.
   destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. 
   destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. 
-  intros [A B]. split.
-  intros. eapply interfere_mreg_incl; eauto.
-  intros. eapply interfere_incl; eauto.
 Qed.
 
 Lemma add_edges_instr_correct:
@@ -516,20 +500,6 @@ Proof.
   eapply interfere_mreg_incl.
   apply add_prefs_call_incl.
   apply add_interfs_call_correct. auto.
-
-  (* Ialloc *)
-  split; intros.
-  apply interfere_mreg_incl with
-    (add_interf_destroyed (Regset.remove r0 live) destroyed_at_call_regs g).
-  eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
-  eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
-  apply add_interf_op_incl.
-  apply add_interf_destroyed_correct; auto.
-  apply Regset.remove_2; auto.
-
-  eapply interfere_incl.
-  eapply graph_incl_trans; apply add_pref_mreg_incl.
-  apply add_interf_op_correct; auto.
 Qed.
 
 Lemma add_edges_instrs_incl_aux:
@@ -826,14 +796,6 @@ Definition correct_alloc_instr
         | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
         | inr idfun => True
         end)
-  | Ialloc arg res s =>
-      (forall r,
-        Regset.In r live!!pc ->
-        r <> res ->
-        ~(In (alloc r) Conventions.destroyed_at_call))
-   /\ (forall r,
-        Regset.In r live!!pc ->
-        r <> res -> alloc r <> alloc res)
   | _ =>
       True
   end.
@@ -927,15 +889,6 @@ Proof.
   caseEq (alloc r). intros.
   elim (ALL2 r m). apply H; auto. congruence. auto. 
   destruct s0; auto.
-  (* Ialloc *)
-  intros [A B]. split. 
-  intros; red; intros. 
-  unfold destroyed_at_call in H1.
-  generalize (list_in_map_inv R _ _ H1). 
-  intros [mr [EQ IN]]. 
-  generalize (A r1 mr H IN H0). intro.
-  generalize (ALL2 _ _ H2). contradiction.
-  auto.
 Qed.
   
 Lemma regalloc_correct_1:
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v
index c9891c2..433c074 100644
--- a/backend/InterfGraph.v
+++ b/backend/InterfGraph.v
@@ -52,12 +52,6 @@ Module OrderedRegReg := OrderedPair(OrderedReg)(OrderedReg).
 Module OrderedMreg := OrderedIndexed(IndexedMreg).
 Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg).
 
-(*
-Module SetDepRegReg := FSetAVL.Make(OrderedRegReg).
-Module SetRegReg := NodepOfDep(SetDepRegReg).
-Module SetDepRegMreg := FSetAVL.Make(OrderedRegMreg).
-Module SetRegMreg := NodepOfDep(SetDepRegMreg).
-*)
 Module SetRegReg := FSetAVL.Make(OrderedRegReg).
 Module SetRegMreg := FSetAVL.Make(OrderedRegMreg).
 
@@ -226,16 +220,6 @@ Definition all_interf_regs (g: graph) : Regset.t :=
       g.(interf_reg_mreg)
       Regset.empty).
 
-(*
-Lemma mem_add_tail:
-  forall r r' u,
-  Regset.mem r u = true -> Regset.mem r (Regset.add r' u) = true.
-Proof.
-  intros. case (Reg.eq r r'); intro.
-  subst r'. apply Regset.mem_add_same.
-  rewrite Regset.mem_add_other; auto.
-Qed.
-*)
 Lemma in_setregreg_fold:
   forall g r1 r2 u,
   SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u ->
diff --git a/backend/LTL.v b/backend/LTL.v
index 6ee07f7..0db5495 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -41,7 +41,6 @@ Inductive instruction: Set :=
   | Lstore: memory_chunk -> addressing -> list loc -> loc -> node -> instruction
   | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction
   | Ltailcall: signature -> loc + ident -> list loc -> instruction
-  | Lalloc: loc -> loc -> node -> instruction
   | Lcond: condition -> list loc -> node -> node -> instruction
   | Lreturn: option loc -> instruction.
 
@@ -165,7 +164,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lop:
       forall s f sp pc rs m op args res pc' v,
       (fn_code f)!pc = Some(Lop op args res pc') ->
-      eval_operation ge sp op (map rs args) m = Some v ->
+      eval_operation ge sp op (map rs args) = Some v ->
       step (State s f sp pc rs m)
         E0 (State s f sp pc' (Locmap.set res v rs) m)
   | exec_Lload:
@@ -197,23 +196,16 @@ Inductive step: state -> trace -> state -> Prop :=
       funsig f' = sig ->
       step (State s f (Vptr stk Int.zero) pc rs m)
         E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
-  | exec_Lalloc:
-      forall s f sp pc rs m pc' arg res sz m' b,
-      (fn_code f)!pc = Some(Lalloc arg res pc') ->
-      rs arg = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', b) ->
-      step (State s f sp pc rs m)
-        E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_locs rs)) m')
   | exec_Lcond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) m = Some true ->
+      eval_condition cond (map rs args) = Some true ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifso rs m)
   | exec_Lcond_false:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) m = Some false ->
+      eval_condition cond (map rs args) = Some false ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifnot rs m)
   | exec_Lreturn:
@@ -275,7 +267,6 @@ Definition successors (f: function) (pc: node) : list node :=
       | Lstore chunk addr args src s => s :: nil
       | Lcall sig ros args res s => s :: nil
       | Ltailcall sig ros args => nil
-      | Lalloc arg res s => s :: nil
       | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
       | Lreturn optarg => nil
       end
diff --git a/backend/LTLin.v b/backend/LTLin.v
index fae6417..4c87c0d 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -47,7 +47,6 @@ Inductive instruction: Set :=
   | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction
   | Lcall: signature -> loc + ident -> list loc -> loc -> instruction
   | Ltailcall: signature -> loc + ident -> list loc -> instruction
-  | Lalloc: loc -> loc -> instruction
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list loc -> label -> instruction
@@ -157,7 +156,7 @@ Definition find_function (ros: loc + ident) (rs: locset) : option fundef :=
 Inductive step: state -> trace -> state -> Prop :=
   | exec_Lop:
       forall s f sp op args res b rs m v,
-      eval_operation ge sp op (map rs args) m = Some v ->
+      eval_operation ge sp op (map rs args) = Some v ->
       step (State s f sp (Lop op args res :: b) rs m)
         E0 (State s f sp b (Locmap.set res v rs) m)
   | exec_Lload:
@@ -185,12 +184,6 @@ Inductive step: state -> trace -> state -> Prop :=
       sig = funsig f' ->
       step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m)
         E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
-  | exec_Lalloc:
-      forall s f sp arg res b rs m sz m' blk,
-      rs arg = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
-      step (State s f sp (Lalloc arg res :: b) rs m)
-        E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_locs rs)) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
@@ -202,13 +195,13 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp b' rs m)
   | exec_Lcond_true:
       forall s f sp cond args lbl b rs m b',
-      eval_condition cond (map rs args) m = Some true ->
+      eval_condition cond (map rs args) = Some true ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b' rs m)
   | exec_Lcond_false:
       forall s f sp cond args lbl b rs m,
-      eval_condition cond (map rs args) m = Some false ->
+      eval_condition cond (map rs args) = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b rs m)
   | exec_Lreturn:
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 26ec066..9f3f589 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -67,11 +67,6 @@ Inductive wt_instr : instruction -> Prop :=
       sig.(sig_res) = funsig.(sig_res) ->
       Conventions.tailcall_possible sig ->
       wt_instr (Ltailcall sig ros args)
-  | wt_Lalloc:
-      forall arg res,
-      Loc.type arg = Tint -> Loc.type res = Tint ->
-      loc_acceptable arg -> loc_acceptable res ->
-      wt_instr (Lalloc arg res)
   | wt_Llabel: forall lbl,
       wt_instr (Llabel lbl)
   | wt_Lgoto: forall lbl,
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 950154a..0461c9a 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -88,12 +88,6 @@ Inductive wt_instr : instruction -> Prop :=
       sig.(sig_res) = funct.(fn_sig).(sig_res) ->
       Conventions.tailcall_possible sig ->
       wt_instr (Ltailcall sig ros args)
-  | wt_Lalloc:
-      forall arg res s,
-      Loc.type arg = Tint -> Loc.type res = Tint ->
-      loc_acceptable arg -> loc_acceptable res ->
-      valid_successor s ->
-      wt_instr (Lalloc arg res s)
   | wt_Lcond:
       forall cond args s1 s2,
       List.map Loc.type args = type_of_condition cond ->
diff --git a/backend/Linear.v b/backend/Linear.v
index 629dcc5..34d6e5c 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -43,7 +43,6 @@ Inductive instruction: Set :=
   | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Lcall: signature -> mreg + ident -> instruction
   | Ltailcall: signature -> mreg + ident -> instruction
-  | Lalloc: instruction
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list mreg -> label -> instruction
@@ -247,7 +246,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) rs) m)
   | exec_Lop:
       forall s f sp op args res b rs m v,
-      eval_operation ge sp op (reglist rs args) m = Some v ->
+      eval_operation ge sp op (reglist rs args) = Some v ->
       step (State s f sp (Lop op args res :: b) rs m)
         E0 (State s f sp b (Locmap.set (R res) v rs) m)
   | exec_Lload:
@@ -274,15 +273,6 @@ Inductive step: state -> trace -> state -> Prop :=
       sig = funsig f' ->
       step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m)
         E0 (Callstate s f' (return_regs (parent_locset s) rs) (Mem.free m stk))
-  | exec_Lalloc:
-      forall s f sp b rs m sz m' blk,
-      rs (R Conventions.loc_alloc_argument) = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
-      step (State s f sp (Lalloc :: b) rs m)
-        E0 (State s f sp b
-                    (Locmap.set (R Conventions.loc_alloc_result)
-                                (Vptr blk Int.zero) rs)
-                    m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
@@ -294,13 +284,13 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp b' rs m)
   | exec_Lcond_true:
       forall s f sp cond args lbl b rs m b',
-      eval_condition cond (reglist rs args) m = Some true ->
+      eval_condition cond (reglist rs args) = Some true ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b' rs m)
   | exec_Lcond_false:
       forall s f sp cond args lbl b rs m,
-      eval_condition cond (reglist rs args) m = Some false ->
+      eval_condition cond (reglist rs args) = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b rs m)
   | exec_Lreturn:
diff --git a/backend/Linearize.v b/backend/Linearize.v
index de372cc..866d05b 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -186,8 +186,6 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code :=
       Lcall sig ros args res :: add_branch s k
   | LTL.Ltailcall sig ros args =>
       Ltailcall sig ros args :: k
-  | LTL.Lalloc arg res s =>
-      Lalloc arg res :: add_branch s k
   | LTL.Lcond cond args s1 s2 =>
       if starts_with s1 k then
         Lcond (negate_condition cond) args s2 :: add_branch s1 k
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 8378332..b385429 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -604,22 +604,6 @@ Proof.
   destruct (Genv.find_symbol ge i); try discriminate.  
   eapply Genv.find_funct_ptr_prop; eauto.
 
-  (* Lalloc *)
-  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
-  simpl in EQ. subst c.
-  assert (REACH': (reachable f)!!pc' = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
-  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
-  econstructor; split.
-  eapply plus_left'. 
-  eapply exec_Lalloc; eauto.
-  eapply add_branch_correct; eauto.
-  eapply is_tail_add_branch. eapply is_tail_cons_left. 
-  eapply is_tail_find_label. eauto.
-  traceEq.
-  econstructor; eauto.
-
   (* Lcond true *)
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v
index ba54723..627c878 100644
--- a/backend/Linearizetyping.v
+++ b/backend/Linearizetyping.v
@@ -55,7 +55,6 @@ Proof.
   apply wt_add_instr. constructor; auto. apply wt_add_branch; auto.
   apply wt_add_instr. constructor; auto. apply wt_add_branch; auto.
   apply wt_add_instr. constructor; auto. auto.
-  apply wt_add_instr. constructor; auto. apply wt_add_branch; auto.
   destruct (starts_with s1 k); apply wt_add_instr.
   constructor; auto. rewrite H. destruct cond; auto. 
   apply wt_add_branch; auto.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 9ef6e31..33b570b 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -85,8 +85,6 @@ Inductive wt_instr : instruction -> Prop :=
       tailcall_possible sig ->
       match ros with inl r => r = IT1 | _ => True end ->
       wt_instr (Ltailcall sig ros)
-  | wt_Lalloc:
-      wt_instr Lalloc
   | wt_Llabel:
       forall lbl,
       wt_instr (Llabel lbl)
diff --git a/backend/Mach.v b/backend/Mach.v
index c64903b..3f25137 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -58,7 +58,6 @@ Inductive instruction: Set :=
   | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Mcall: signature -> mreg + ident -> instruction
   | Mtailcall: signature -> mreg + ident -> instruction
-  | Malloc: instruction
   | Mlabel: label -> instruction
   | Mgoto: label -> instruction
   | Mcond: condition -> list mreg -> label -> instruction
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index e145c89..25819f7 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -94,8 +94,9 @@ Section FRAME_ACCESSES.
 Variable f: function.
 
 (** A slot [(ty, ofs)] within a frame is valid in function [f] if it lies
-  within the bounds of [f]'s frame, and it does not overlap with
-  the slots reserved for the return address and the back link. *)
+  within the bounds of [f]'s frame, it does not overlap with
+  the slots reserved for the return address and the back link,
+  and it is aligned on a 4-byte boundary. *)
 
 Inductive slot_valid: typ -> Z -> Prop :=
   slot_valid_intro:
@@ -106,6 +107,7 @@ Inductive slot_valid: typ -> Z -> Prop :=
        \/ Int.signed f.(fn_link_ofs) + 4 <= ofs) ->
     (ofs + AST.typesize ty <= Int.signed f.(fn_retaddr_ofs)
        \/ Int.signed f.(fn_retaddr_ofs) + 4 <= ofs) ->
+    (4 | ofs) ->
     slot_valid ty ofs.
 
 (** [get_slot f fr ty ofs v] holds if the frame [fr] contains value [v]
@@ -239,7 +241,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp c (rs#dst <- v) fr m)
   | exec_Mop:
       forall s f sp op args res c rs fr m v,
-      eval_operation ge sp op rs##args m = Some v ->
+      eval_operation ge sp op rs##args = Some v ->
       step (State s f sp (Mop op args res :: c) rs fr m)
         E0 (State s f sp c (rs#res <- v) fr m)
   | exec_Mload:
@@ -264,15 +266,6 @@ Inductive step: state -> trace -> state -> Prop :=
       find_function ros rs = Some f' ->
       step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m)
         E0 (Callstate s f' rs (Mem.free m stk))
-
-  | exec_Malloc:
-      forall s f sp c rs fr m sz m' blk,
-      rs (Conventions.loc_alloc_argument) = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
-      step (State s f sp (Malloc :: c) rs fr m)
-        E0 (State s f sp c
-                   (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero))
-                    fr m')
   | exec_Mgoto:
       forall s f sp lbl c rs fr m c',
       find_label lbl f.(fn_code) = Some c' ->
@@ -280,13 +273,13 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp c' rs fr m)
   | exec_Mcond_true:
       forall s f sp cond args lbl c rs fr m c',
-      eval_condition cond rs##args m = Some true ->
+      eval_condition cond rs##args = Some true ->
       find_label lbl f.(fn_code) = Some c' ->
       step (State s f sp (Mcond cond args lbl :: c) rs fr m)
         E0 (State s f sp c' rs fr m)
   | exec_Mcond_false:
       forall s f sp cond args lbl c rs fr m,
-      eval_condition cond rs##args m = Some false ->
+      eval_condition cond rs##args = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs fr m)
         E0 (State s f sp c rs fr m)
   | exec_Mreturn:
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index 7eae610..6e331f3 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -84,7 +84,7 @@ Inductive frame_match (fr: frame)
     high_bound ms sp >= 0 ->
     base = Int.repr (-f.(fn_framesize)) ->
     (forall ty ofs,
-       -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 ->
+       -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) ->
        load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) ->
     frame_match fr sp base mm ms.
 
@@ -126,15 +126,16 @@ Lemma frame_match_load_stack:
   forall fr sp base mm ms ty ofs,
   frame_match fr sp base mm ms ->
   0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
+  (4 | Int.signed ofs) ->
   load_stack ms (Vptr sp base) ty ofs = 
   Some (fr ty (Int.signed ofs - f.(fn_framesize))).
 Proof.
-  intros. inv H.
+  intros. inv H. inv wt_f.
   unfold load_stack, Val.add, loadv.
   replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs))
      with (Int.signed ofs - fn_framesize f).
-  apply H6. omega. omega.
-  inv wt_f.
+  apply H7. omega. omega.
+  apply Zdivide_minus_l; auto. 
   assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
     apply Int.signed_repr.
     assert (0 <= Int.max_signed). compute; congruence. omega.
@@ -150,8 +151,7 @@ Lemma frame_match_get_slot:
   get_slot f fr ty (Int.signed ofs) v ->
   load_stack ms (Vptr sp base) ty ofs = Some v.
 Proof.
-  intros. inversion H. inv H0. eapply frame_match_load_stack; eauto.
-  inv H7. auto.
+  intros. inversion H. inv H0. inv H7. eapply frame_match_load_stack; eauto.
 Qed.
 
 (** Assigning a value to a frame slot (in the abstract semantics)
@@ -163,6 +163,7 @@ Lemma frame_match_store_stack:
   forall fr sp base mm ms ty ofs v,
   frame_match fr sp base mm ms ->
   0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
+  (4 | Int.signed ofs) ->
   Val.has_type v ty ->
   Mem.extends mm ms ->
   exists ms',
@@ -186,7 +187,10 @@ Proof.
     apply valid_access_store. 
     constructor. auto. omega.
     rewrite size_type_chunk. omega.
-  destruct H7 as [ms' STORE]. 
+    replace (align_chunk (chunk_of_type ty)) with 4.
+    apply Zdivide_minus_l; auto.
+    destruct ty; auto.
+  destruct H8 as [ms' STORE]. 
   generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB.
   generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB.
   exists ms'. 
@@ -205,10 +209,10 @@ Proof.
     destruct ty; destruct ty0; simpl; congruence.
     destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)).
     (* disjoint *)
-    rewrite <- H8; auto. eapply load_store_other; eauto.
+    rewrite <- H9; auto. eapply load_store_other; eauto.
     right; left. rewrite size_type_chunk; auto.
     destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)).
-    rewrite <- H8; auto. eapply load_store_other; eauto.
+    rewrite <- H9; auto. eapply load_store_other; eauto.
     right; right. rewrite size_type_chunk; auto.
     (* overlap *)
     eapply load_store_overlap'; eauto with mem.
@@ -230,8 +234,7 @@ Lemma frame_match_set_slot:
     frame_match fr' sp base mm ms' /\
     Mem.extends mm ms'.
 Proof.
-  intros. inv H0. eapply frame_match_store_stack; eauto. 
-  inv H3. auto.
+  intros. inv H0. inv H3. eapply frame_match_store_stack; eauto. 
 Qed.
 
 (** Agreement is preserved by stores within blocks other than the
@@ -277,7 +280,7 @@ Proof.
   destruct (zeq sp b). subst b. right. 
   rewrite size_type_chunk. 
   assert (valid_access mm chunk sp ofs) by eauto with mem.
-  inv H8. left. omega.
+  inv H9. left. omega.
   auto.
 Qed.
 
@@ -310,6 +313,7 @@ Proof.
   intros.
   eapply load_alloc_same'; eauto.  
   rewrite size_type_chunk. omega.
+  replace (align_chunk (chunk_of_type ty)) with 4; auto. destruct ty; auto.
 Qed.
 
 Lemma frame_match_alloc:
@@ -435,6 +439,7 @@ Proof.
   replace (parent_sp cs) with
    (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))).
   eapply frame_match_load_stack; eauto.
+  
   unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. 
 Qed.
 
@@ -470,10 +475,10 @@ Proof.
   exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto.
   fold base. intros [C FM0].
   destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
-              FM0 wt_function_link H2 EXT0)
+              FM0 wt_function_link wt_function_link_aligned H2 EXT0)
   as [ms2 [STORE1 [FM1 EXT1]]].
   destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
-              FM1 wt_function_retaddr H3 EXT1)
+              FM1 wt_function_retaddr wt_function_retaddr_aligned H3 EXT1)
   as [ms3 [STORE2 [FM3 EXT3]]].
   exists ms2; exists ms3; auto.
 Qed.
@@ -783,8 +788,6 @@ Proof.
   (* Mop *)
   exists (State ts fb (Vptr sp0 base) c (rs#res <- v) ms); split.
   apply exec_Mop; auto.
-  eapply eval_operation_change_mem with (m := m); eauto.
-  intros. eapply Mem.valid_pointer_extends; eauto.
   econstructor; eauto with coqlib.
 
   (* Mload *)
@@ -826,15 +829,6 @@ Proof.
   econstructor; eauto. eapply match_stacks_free; auto.
   apply free_extends; auto.
 
-  (* Malloc *)
-  caseEq (alloc ms 0 (Int.signed sz)). intros ms' blk' ALLOC.
-  exploit alloc_extends; eauto. omega. omega. intros [EQ MEXT']. subst blk'.
-  exists (State ts fb (Vptr sp0 base) c (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) ms'); split.
-  eapply exec_Malloc; eauto.
-  econstructor; eauto.
-  eapply match_stacks_alloc; eauto. inv MEXT; auto. 
-  eapply frame_match_alloc with (mm := m) (ms := ms); eauto. inv MEXT; auto.
-
   (* Mgoto *)
   econstructor; split.
   eapply exec_Mgoto; eauto.
@@ -843,13 +837,9 @@ Proof.
   (* Mcond *)
   econstructor; split.
   eapply exec_Mcond_true; eauto.
-  eapply eval_condition_change_mem with (m := m); eauto.
-  intros. eapply Mem.valid_pointer_extends; eauto.
   econstructor; eauto.
   econstructor; split.
   eapply exec_Mcond_false; eauto.
-  eapply eval_condition_change_mem with (m := m); eauto.
-  intros. eapply Mem.valid_pointer_extends; eauto.
   econstructor; eauto.
 
   (* Mreturn *)
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 41216d2..4417cc6 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -155,7 +155,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s fb sp c (rs#dst <- v) m)
   | exec_Mop:
       forall s f sp op args res c rs m v,
-      eval_operation ge sp op rs##args m = Some v ->
+      eval_operation ge sp op rs##args = Some v ->
       step (State s f sp (Mop op args res :: c) rs m)
         E0 (State s f sp c (rs#res <- v) m)
   | exec_Mload:
@@ -186,14 +186,6 @@ Inductive step: state -> trace -> state -> Prop :=
       load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
       step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
         E0 (Callstate s f' rs (Mem.free m stk))
-  | exec_Malloc:
-      forall s f sp c rs m sz m' blk,
-      rs (Conventions.loc_alloc_argument) = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
-      step (State s f sp (Malloc :: c) rs m)
-        E0 (State s f sp c
-                  (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero))
-                   m')
   | exec_Mgoto:
       forall s fb f sp lbl c rs m c',
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
@@ -202,14 +194,14 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s fb sp c' rs m)
   | exec_Mcond_true:
       forall s fb f sp cond args lbl c rs m c',
-      eval_condition cond rs##args m = Some true ->
+      eval_condition cond rs##args = Some true ->
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
       step (State s fb sp (Mcond cond args lbl :: c) rs m)
         E0 (State s fb sp c' rs m)
   | exec_Mcond_false:
       forall s f sp cond args lbl c rs m,
-      eval_condition cond rs##args m = Some false ->
+      eval_condition cond rs##args = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs m)
         E0 (State s f sp c rs m)
   | exec_Mreturn:
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index f9f76d8..ef59e6f 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -72,8 +72,6 @@ Inductive wt_instr : instruction -> Prop :=
       Conventions.tailcall_possible sig ->
       match ros with inl r => mreg_type r = Tint | inr s => True end ->
       wt_instr (Mtailcall sig ros)
-  | wt_Malloc:
-      wt_instr Malloc
   | wt_Mgoto:
       forall lbl,
       wt_instr (Mgoto lbl)
@@ -91,12 +89,18 @@ Record wt_function (f: function) : Prop := mk_wt_function {
     f.(fn_stacksize) >= 0;
   wt_function_framesize:
     0 <= f.(fn_framesize) <= -Int.min_signed;
+  wt_function_framesize_aligned:
+    (4 | f.(fn_framesize));
   wt_function_link:
     0 <= Int.signed f.(fn_link_ofs)
     /\ Int.signed f.(fn_link_ofs) + 4 <= f.(fn_framesize);
+  wt_function_link_aligned:
+    (4 | Int.signed f.(fn_link_ofs));
   wt_function_retaddr:
     0 <= Int.signed f.(fn_retaddr_ofs)
     /\ Int.signed f.(fn_retaddr_ofs) + 4 <= f.(fn_framesize);
+  wt_function_retaddr_aligned:
+    (4 | Int.signed f.(fn_retaddr_ofs));
   wt_function_link_retaddr:
     Int.signed f.(fn_retaddr_ofs) + 4 <= Int.signed f.(fn_link_ofs)
     \/ Int.signed f.(fn_link_ofs) + 4 <= Int.signed f.(fn_retaddr_ofs)
@@ -250,7 +254,7 @@ Proof.
     simpl in H. 
     rewrite <- H2. replace v with (rs r1). apply WTRS. congruence.
     replace (mreg_type res) with (snd (type_of_operation op)).
-    apply type_of_operation_sound with fundef ge rs##args sp m; auto.
+    apply type_of_operation_sound with fundef ge rs##args sp; auto.
     rewrite <- H5; reflexivity.
 
   apply wt_setreg; auto. inversion H1. rewrite H7.
@@ -272,7 +276,7 @@ Proof.
     apply (Genv.find_funct_ptr_prop wt_fundef wt_p H).
   econstructor; eauto.
 
-  apply wt_setreg; auto. exact I. 
+(*  apply wt_setreg; auto. exact I.  *)
 
   apply is_tail_find_label with lbl; congruence.
   apply is_tail_find_label with lbl; congruence. 
@@ -293,17 +297,6 @@ Proof.
   econstructor; eauto. 
   eauto with coqlib.
 Qed.
-(*
-Lemma subject_reduction_2:
-  forall s1 t s2, step ge s1 t s2 ->
-  forall (WTS: wt_state s1), wt_state s2.
-Proof.
-  induction 1; intros.
-  auto.
-  eapply subject_reduction; eauto.
-  auto.
-Qed.
-*)
 
 End SUBJECT_REDUCTION.
 
diff --git a/backend/RTL.v b/backend/RTL.v
index abecd4a..5fad2f2 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -68,10 +68,8 @@ Inductive instruction: Set :=
           as arguments.  It stores the return value in [dest] and branches
           to [succ]. *)
   | Itailcall: signature -> reg + ident -> list reg -> instruction
-  | Ialloc: reg -> reg -> node -> instruction
-      (** [Ialloc arg dest succ] allocates a fresh block of size
-          the contents of register [arg], stores a pointer to this
-          block in [dest], and branches to [succ]. *)
+      (** [Itailcall sig fn args] performs a function invocation
+          in tail-call position.  *)
   | Icond: condition -> list reg -> node -> node -> instruction
       (** [Icond cond args ifso ifnot] evaluates the boolean condition
           [cond] over the values of registers [args].  If the condition
@@ -213,7 +211,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Iop:
       forall s c sp pc rs m op args res pc' v,
       c!pc = Some(Iop op args res pc') ->
-      eval_operation ge sp op rs##args m = Some v ->
+      eval_operation ge sp op rs##args = Some v ->
       step (State s c sp pc rs m)
         E0 (State s c sp pc' (rs#res <- v) m)
   | exec_Iload:
@@ -244,23 +242,16 @@ Inductive step: state -> trace -> state -> Prop :=
       funsig f = sig ->
       step (State s c (Vptr stk Int.zero) pc rs m)
         E0 (Callstate s f rs##args (Mem.free m stk))
-  | exec_Ialloc:
-      forall s c sp pc rs m pc' arg res sz m' b,
-      c!pc = Some(Ialloc arg res pc') ->
-      rs#arg = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', b) ->
-      step (State s c sp pc rs m)
-        E0 (State s c sp pc' (rs#res <- (Vptr b Int.zero)) m')
   | exec_Icond_true:
       forall s c sp pc rs m cond args ifso ifnot,
       c!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args m = Some true ->
+      eval_condition cond rs##args = Some true ->
       step (State s c sp pc rs m)
         E0 (State s c sp ifso rs m)
   | exec_Icond_false:
       forall s c sp pc rs m cond args ifso ifnot,
       c!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args m = Some false ->
+      eval_condition cond rs##args = Some false ->
       step (State s c sp pc rs m)
         E0 (State s c sp ifnot rs m)
   | exec_Ireturn:
@@ -291,7 +282,7 @@ Inductive step: state -> trace -> state -> Prop :=
 Lemma exec_Iop':
   forall s c sp pc rs m op args res pc' rs' v,
   c!pc = Some(Iop op args res pc') ->
-  eval_operation ge sp op rs##args m = Some v ->
+  eval_operation ge sp op rs##args = Some v ->
   rs' = (rs#res <- v) ->
   step (State s c sp pc rs m)
     E0 (State s c sp pc' rs' m).
@@ -352,7 +343,6 @@ Definition successors (f: function) (pc: node) : list node :=
       | Istore chunk addr args src s => s :: nil
       | Icall sig ros args res s => s :: nil
       | Itailcall sig ros args => nil
-      | Ialloc arg res s => s :: nil
       | Icond cond args ifso ifnot => ifso :: ifnot :: nil
       | Ireturn optarg => nil
       end
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 5fde3d8..709dc78 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -530,12 +530,6 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do n1 <- add_instr (Itailcall sig (inl _ rf) rargs);
       do n2 <- transl_exprlist map cl rargs n1;
          transl_expr map b rf n2
-  | Salloc id a =>
-      do ra <- alloc_reg map a;
-      do rr <- new_reg;
-      do n1 <- store_var map rr id nd;
-      do n2 <- add_instr (Ialloc ra rr n1);
-         transl_expr map a ra n2
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 1074ddd..6d5cd8e 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -568,7 +568,7 @@ Lemma transl_expr_Eop_correct:
          (vargs : list val) (v : val),
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
-  eval_operation ge sp op vargs m = Some v ->
+  eval_operation ge sp op vargs = Some v ->
   transl_expr_prop le (Eop op args) v.
 Proof.
   intros; red; intros. inv TE. 
@@ -711,7 +711,7 @@ Lemma transl_condition_CEcond_correct:
          (vargs : list val) (b : bool),
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
-  eval_condition cond vargs m = Some b ->
+  eval_condition cond vargs = Some b ->
   transl_condition_prop le (CEcond cond args) b.
 Proof.
   intros; red; intros; inv TE.
@@ -1154,22 +1154,6 @@ Proof.
   apply sig_transl_function; auto.
   traceEq.
   rewrite G. constructor; auto.
-
-  (* alloc *)
-  inv TS. 
-  exploit transl_expr_correct; eauto. 
-  intros [rs1 [A [B [C D]]]].
-  set (rs2 := rs1#rd <- (Vptr b Int.zero)).
-  assert (match_env map e nil rs2). unfold rs2; eauto with rtlg. 
-  exploit tr_store_var_correct. eauto. auto. eexact H1. 
-  intros [rs3 [E F]].
-  unfold rs2 in F. rewrite Regmap.gss in F.
-  econstructor; split.
-  left. apply plus_star_trans with E0 (State cs c sp n2 rs2 m') E0.
-  eapply plus_right. eexact A. unfold rs2. eapply exec_Ialloc; eauto. traceEq.
-  eexact E. traceEq.
-  econstructor; eauto. constructor.
-
   (* seq *)
   inv TS. 
   econstructor; split.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 59a5dd7..e6adeb0 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -141,21 +141,6 @@ Proof.
 Qed.
 Hint Resolve instr_at_incr: rtlg.
 
-(*
-(** A useful tactic to reason over transitivity and reflexivity of [state_incr]. *)
-
-Ltac Show_state_incr :=
-  eauto;
-  match goal with
-  | |- (state_incr ?c ?c) => 
-         apply state_incr_refl
-  | |- (state_incr ?c1 ?c2) =>
-         eapply state_incr_trans; [eauto; fail | idtac]; Show_state_incr
-  end.
-
-Hint Extern 2 (state_incr _ _) => Show_state_incr : rtlg.
-*)
-
 Hint Resolve state_incr_refl state_incr_trans: rtlg.
 
 (** * Validity and freshness of registers *)
@@ -779,12 +764,6 @@ Inductive tr_stmt (c: code) (map: mapping):
      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_Salloc: forall id a ns nd nexits ngoto nret rret rd n1 n2 r,
-     tr_expr c map nil a ns n1 r ->
-     c!n1 = Some (Ialloc r rd n2) ->
-     tr_store_var c map rd id n2 nd ->
-     ~reg_in_map map rd ->
-     tr_stmt c map (Salloc id a) ns nd nexits ngoto nret rret
   | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n,
      tr_stmt c map s2 n nd nexits ngoto nret rret ->
      tr_stmt c map s1 ns n nexits ngoto nret rret ->
@@ -1197,11 +1176,6 @@ Proof.
   eapply A; eauto with rtlg.
   apply tr_exprlist_incr with s4; auto.
   eapply C; eauto with rtlg.
-  (* Salloc *)
-  econstructor; eauto with rtlg.
-  eapply transl_expr_charact; eauto with rtlg.
-  apply tr_store_var_incr with s2; eauto with rtlg.
-  eapply store_var_charact; eauto with rtlg.
   (* Sseq *)
   econstructor. 
   apply tr_stmt_incr with s0; auto. 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index fa9dd21..60b1d72 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -100,11 +100,6 @@ Inductive wt_instr : instruction -> Prop :=
       List.map env args = sig.(sig_args) ->
       Conventions.tailcall_possible sig ->
       wt_instr (Itailcall sig ros args)
-  | wt_Ialloc:
-      forall arg res s,
-      env arg = Tint -> env res = Tint ->
-      valid_successor s ->
-      wt_instr (Ialloc arg res s)
   | wt_Icond:
       forall cond args s1 s2,
       List.map env args = type_of_condition cond ->
@@ -225,10 +220,6 @@ Definition check_instr (i: instruction) : bool :=
       && check_regs args sig.(sig_args)
       && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res)
       && Conventions.tailcall_is_possible sig
-  | Ialloc arg res s =>
-      check_reg arg Tint 
-      && check_reg res Tint
-      && check_successor s
   | Icond cond args s1 s2 =>
       check_regs args (type_of_condition cond)
       && check_successor s1
@@ -331,11 +322,6 @@ Proof.
   eapply proj_sumbool_true; eauto.
   apply check_regs_correct; auto.
   apply Conventions.tailcall_is_possible_correct; auto.
-  (* alloc *)
-  constructor. 
-  apply check_reg_correct; auto.
-  apply check_reg_correct; auto.
-  apply check_successor_correct; auto.
   (* cond *)
   constructor. apply check_regs_correct; auto.
   apply check_successor_correct; auto.
@@ -524,7 +510,7 @@ Proof.
   econstructor; eauto.
   apply wt_regset_assign. auto.
   replace (env res) with (snd (type_of_operation op)).
-  apply type_of_operation_sound with fundef ge rs##args sp m; auto.
+  apply type_of_operation_sound with fundef ge rs##args sp; auto.
   rewrite <- H6. reflexivity.
   (* Iload *)
   econstructor; eauto.
@@ -556,9 +542,6 @@ Proof.
   econstructor; eauto.
   rewrite H5; auto.
   rewrite <- H6. apply wt_regset_list. auto.
-  (* Ialloc *)  
-  econstructor; eauto.
-  apply wt_regset_assign. auto. rewrite H6; exact I.
   (* Icond *)
   econstructor; eauto.
   econstructor; eauto.
diff --git a/backend/Reload.v b/backend/Reload.v
index 17664b6..621e75b 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -235,9 +235,6 @@ Definition transf_instr
           parallel_move args largs
             (Ltailcall sig (inr _ id) :: k)
       end
-  | LTLin.Lalloc arg res =>
-      add_reload arg loc_alloc_argument
-        (Lalloc :: add_spill loc_alloc_result res k)
   | LTLin.Llabel lbl =>
       Llabel lbl :: k
   | LTLin.Lgoto lbl =>
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 5a3acd3..ea7c5d1 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -178,10 +178,10 @@ Proof.
 Qed.
 
 Lemma not_enough_temporaries_addr:
-  forall (ge: genv) sp addr src args ls m v,
+  forall (ge: genv) sp addr src args ls v,
   enough_temporaries (src :: args) = false ->
   eval_addressing ge sp addr (List.map ls args) = Some v ->
-  eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) m = Some v.
+  eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) = Some v.
 Proof.
   intros.
   apply eval_op_for_binary_addressing; auto.
@@ -631,21 +631,6 @@ Proof.
   apply temporaries_not_acceptable; auto.
 Qed.
 
-Lemma agree_postcall_alloc:
-  forall rs ls ls2 v,
-  agree rs ls ->
-  (forall l, Loc.diff (R loc_alloc_argument) l -> ls2 l = ls l) ->
-  agree (LTL.postcall_locs rs) (Locmap.set (R loc_alloc_result) v ls2).
-Proof.
-  intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto.
-  intros. destruct (Loc.eq l (R loc_alloc_result)).
-  subst l. elim H2. simpl. tauto. 
-  rewrite Locmap.gso. apply H0.
-  red. destruct l; auto. red; intro. subst m. elim H2.
-  simpl. tauto.
-  apply Loc.diff_sym. apply loc_acceptable_noteq_diff; auto. 
-Qed.
-
 Lemma agree_init_locs:
   forall ls dsts vl,
   locs_acceptable dsts ->
@@ -991,9 +976,9 @@ Proof.
     eapply enough_temporaries_op_args; eauto.
     apply locs_acceptable_disj_temporaries; auto.
   intros [ls2 [A [B C]]]. instantiate (1 := ls) in B. 
-  assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv
+  assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) = Some tv
                      /\ Val.lessdef v tv).
-    apply eval_operation_lessdef with m (map rs args); auto.
+    apply eval_operation_lessdef with (map rs args); auto.
     rewrite B. eapply agree_locs; eauto. 
     rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
   destruct H1 as [tv [P Q]].
@@ -1231,28 +1216,6 @@ Proof.
   exact (return_regs_preserve (parent_locset s') ls3).
   apply Mem.free_lessdef; auto. 
 
-  (* Lalloc *)
-  ExploitWT; inv WTI.
-  caseEq (alloc tm 0 (Int.signed sz)). intros tm' blk' TALLOC.
-  assert (blk = blk' /\ Mem.lessdef m' tm'). 
-    eapply Mem.alloc_lessdef; eauto.
-  exploit add_reload_correct. intros [ls2 [A [B C]]]. 
-  exploit add_spill_correct. intros [ls3 [D [E F]]].
-  destruct H1 as [P Q]. subst blk'. 
-  assert (ls arg = Vint sz).
-    assert (Val.lessdef (rs arg) (ls arg)). eapply agree_loc; eauto. 
-    rewrite H in H1; inversion H1; auto.
-  left; econstructor; split.
-  eapply star_plus_trans. eauto. 
-  eapply plus_left. eapply exec_Lalloc; eauto.
-    rewrite B. eauto. 
-  eauto. eauto. traceEq.
-  econstructor; eauto with coqlib.
-  apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2).
-  auto. rewrite E. rewrite Locmap.gss. constructor. 
-  auto. 
-  apply agree_postcall_alloc with ls; auto. 
-
   (* Llabel *)
   left; econstructor; split.
   apply plus_one. apply exec_Llabel.
@@ -1272,7 +1235,7 @@ Proof.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
   eapply plus_right. eauto. eapply exec_Lcond_true; eauto.
-  rewrite B. apply eval_condition_lessdef with m (map rs args); auto.
+  rewrite B. apply eval_condition_lessdef with (map rs args); auto.
   eapply agree_locs; eauto. 
   apply find_label_transf_function; eauto.
   traceEq.
@@ -1288,7 +1251,7 @@ Proof.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
   eapply plus_right. eauto. eapply exec_Lcond_false; eauto.
-  rewrite B. apply eval_condition_lessdef with m (map rs args); auto.
+  rewrite B. apply eval_condition_lessdef with (map rs args); auto.
   eapply agree_locs; eauto. 
   traceEq.
   econstructor; eauto with coqlib.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index e531c54..375bbfd 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -34,7 +34,7 @@ Require Import Reloadproof.
   given sufficient typing and well-formedness hypotheses over the locations involved. *)
 
 Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove
-             wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lalloc
+             wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall
              wt_Llabel wt_Lgoto wt_Lcond wt_Lreturn: reloadty.
 
 Remark wt_code_cons:
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 1cf010b..158af8f 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -179,8 +179,6 @@ Definition transl_instr
   | Ltailcall sig ros =>
       restore_callee_save fe
         (Mtailcall sig ros :: k)
-  | Lalloc =>
-      Malloc :: k
   | Llabel lbl =>
       Mlabel lbl :: k
   | Lgoto lbl =>
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index e17f67a..a7560d0 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -172,6 +172,45 @@ Proof.
   assert (z <> z0). intuition auto. omega.
 Qed.
 
+Remark aligned_4_4x: forall x, (4 | 4 * x).
+Proof. intro. exists x; ring. Qed.
+
+Remark aligned_4_8x: forall x, (4 | 8 * x).
+Proof. intro. exists (x * 2); ring. Qed.
+
+Remark aligned_4_align8: forall x, (4 | align x 8).
+Proof. 
+  intro. apply Zdivides_trans with 8. exists 2; auto. apply align_divides. omega.
+Qed.
+
+Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r
+             aligned_4_4x aligned_4_8x aligned_4_align8: align_4.
+
+Hint Extern 4 (?X | ?Y) => (exists (Y/X); reflexivity) : align_4.
+
+Lemma offset_of_index_aligned:
+  forall idx, (4 | offset_of_index fe idx).
+Proof.
+  intros.
+  destruct idx;
+  unfold offset_of_index, fe, make_env,
+    fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
+    fe_ofs_float_local, fe_ofs_float_callee_save,
+    fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg;
+  auto with align_4.
+  destruct t; auto with align_4.
+Qed.
+
+Lemma frame_size_aligned:
+  (4 | fe_size fe).
+Proof.
+  unfold offset_of_index, fe, make_env,
+    fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
+    fe_ofs_float_local, fe_ofs_float_callee_save,
+    fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg;
+  auto with align_4.
+Qed.
+
 (** The following lemmas give sufficient conditions for indices
   of various kinds to be valid. *)
 
@@ -232,7 +271,7 @@ Proof.
     fe_ofs_float_local, fe_ofs_float_callee_save,
     fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg,
     type_of_index, typesize;
-  simpl in H5;
+  unfold index_valid in H5; simpl typesize in H5;
   omega.
 Qed. 
 
@@ -287,6 +326,7 @@ Proof.
     auto. exact I. red. destruct idx; auto || congruence.
   intro. rewrite typesize_typesize. assumption.
   exact I.
+  apply offset_of_index_aligned.
 Qed.
 
 Lemma get_slot_index:
@@ -535,96 +575,6 @@ Proof.
   intros. rewrite get_set_index_val_other; eauto with stacking. red; auto.
 Qed.
 
-(*
-Lemma agree_set_int_callee_save:
-  forall ls ls0 rs fr r v,
-  agree ls ls0 rs fr ->
-  In r int_callee_save_regs ->
-  index_int_callee_save r < fe.(fe_num_int_callee_save) ->
-  exists fr',
-    set_slot tf fr Tint 
-             (Int.signed (Int.repr
-               (offset_of_index fe (FI_saved_int (index_int_callee_save r)))))
-             v fr' /\
-    agree ls (Locmap.set (R r) v ls0) rs fr'.
-Proof.
-  intros.
-  set (idx := FI_saved_int (index_int_callee_save r)).
-  exists (set_index_val idx v fr); split.
-  change Tint with (type_of_index idx).
-  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
-  constructor; eauto with stacking.
-  (* agree_unused_reg *)
-  intros. rewrite Locmap.gso. eauto with stacking.
-  red; red; intro. subst r0. elim H2. red. 
-  rewrite (int_callee_save_type r H0). auto.
-  (* agree_local *)
-  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
-  red; auto.
-  (* agree_outgoing *)
-  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
-  red; auto.
-  (* agree_incoming *)
-  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
-  (* saved ints *)
-  intros. destruct (mreg_eq r r0). 
-  subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. 
-  rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking.
-  unfold idx. auto with stacking. auto with stacking.
-  unfold idx; red. apply index_int_callee_save_inj; auto.
-  red; auto.
-  (* saved floats *)
-  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
-  unfold idx. auto with stacking. 
-  unfold idx; red; auto.
-  red. apply int_float_callee_save_disjoint; auto.
-Qed.
-
-Lemma agree_set_float_callee_save:
-  forall ls ls0 rs fr r v,
-  agree ls ls0 rs fr ->
-  In r float_callee_save_regs ->
-  index_float_callee_save r < fe.(fe_num_float_callee_save) ->
-  exists fr',
-    set_slot tf fr Tfloat
-             (Int.signed (Int.repr
-               (offset_of_index fe (FI_saved_float (index_float_callee_save r)))))
-             v fr' /\
-    agree ls (Locmap.set (R r) v ls0) rs fr'.
-Proof.
-  intros.
-  set (idx := FI_saved_float (index_float_callee_save r)).
-  exists (set_index_val idx v fr); split.
-  change Tfloat with (type_of_index idx).
-  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
-  constructor; eauto with stacking.
-  (* agree_unused_reg *)
-  intros. rewrite Locmap.gso. eauto with stacking.
-  red; red; intro. subst r0. elim H2. red. 
-  rewrite (float_callee_save_type r H0). auto.
-  (* agree_local *)
-  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
-  red; auto.
-  (* agree_outgoing *)
-  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
-  red; auto.
-  (* agree_incoming *)
-  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
-  (* saved ints *)
-  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
-  unfold idx. auto with stacking. 
-  unfold idx; red; auto.
-  red. apply sym_not_equal. apply int_float_callee_save_disjoint; auto.
-  (* saved floats *)
-  intros. destruct (mreg_eq r r0). 
-  subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. 
-  rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking.
-  unfold idx. auto with stacking. auto with stacking.
-  unfold idx; red. apply index_float_callee_save_inj; auto.
-  red; auto.
-Qed.
-*)
-
 Lemma agree_return_regs:
   forall ls ls0 rs fr cs rs',
   agree ls ls0 rs fr cs ->
@@ -1270,12 +1220,11 @@ Proof.
 Qed.
 
 Lemma shift_eval_operation:
-  forall f tf sp op args m v,
+  forall f tf sp op args v,
   transf_function f = OK tf ->
-  eval_operation ge sp op args m = Some v ->
+  eval_operation ge sp op args = Some v ->
   eval_operation tge (shift_sp tf sp) 
-                 (transl_op (make_env (function_bounds f)) op) args m =
-  Some v.
+                 (transl_op (make_env (function_bounds f)) op) args = Some v.
 Proof.
   intros until v. destruct op; intros; auto.
   simpl in *. rewrite symbols_preserved. auto.
@@ -1535,15 +1484,6 @@ Proof.
   intros. inv WTI. generalize (H3 _ H0). tauto.
   apply agree_callee_save_return_regs. 
  
-  (* Lalloc *)
-  exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b)
-                          (rs0#loc_alloc_result <- (Vptr blk Int.zero)) fr m'); split.
-  apply plus_one; eapply exec_Malloc; eauto.
-  rewrite (agree_eval_reg _ _ _ _ _ _ _ loc_alloc_argument AG). auto.
-  econstructor; eauto with coqlib.
-  apply agree_set_reg; auto.
-  red. simpl. generalize (max_over_regs_of_funct_pos f int_callee_save). omega.
-
   (* Llabel *)
   econstructor; split.
   apply plus_one; apply exec_Mlabel.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index f1fe2cf..b88dd50 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -176,8 +176,6 @@ Proof.
   apply wt_restore_callee_save. apply wt_instrs_cons; auto.
   constructor; auto.
   destruct s0; auto. rewrite H5; auto.
-  (* alloc *)
-  apply wt_instrs_cons; auto. constructor. 
   (* label *)
   apply wt_instrs_cons; auto.
   constructor.
@@ -227,10 +225,13 @@ Proof.
   red; intros. elim H5.
   subst tf; simpl; auto.
   rewrite H2. generalize (size_pos f). fold b; fold fe; omega.
+  rewrite H1. change (4 | fe_size fe). unfold fe, b. apply frame_size_aligned.   
   rewrite H3; rewrite H2. change 4 with (4 * typesize (type_of_index FI_link)).
   unfold fe, b; apply offset_of_index_valid. red; auto.
+  rewrite H3. unfold fe,b; apply offset_of_index_aligned.
   rewrite H4; rewrite H2. change 4 with (4 * typesize (type_of_index FI_retaddr)).
   unfold fe, b; apply offset_of_index_valid. red; auto.
+  rewrite H4. unfold fe,b; apply offset_of_index_aligned.
   rewrite H3; rewrite H4.
   apply (offset_of_index_disj f FI_retaddr FI_link); red; auto.
 Qed.
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 2f520c6..32d1b59 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -112,8 +112,6 @@ Definition tunnel_instr (f: LTL.function) (b: instruction) : instruction :=
       Lcall sig ros args res (branch_target f s)
   | Ltailcall sig ros args =>
       Ltailcall sig ros args
-  | Lalloc arg res s =>
-      Lalloc arg res (branch_target f s)
   | Lcond cond args s1 s2 =>
       Lcond cond args (branch_target f s1) (branch_target f s2)
   | Lreturn or =>
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 7ad75ba..49bf894 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -297,12 +297,6 @@ Proof.
   rewrite sig_preserved. auto.
   apply find_function_translated; auto.
   econstructor; eauto.
-  (* Lalloc *)
-  rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
-  left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_locs rs)) m'); split.
-  eapply exec_Lalloc; eauto.
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
-  econstructor; eauto.
   (* cond *)
   rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
   left; econstructor; split.