Merge of branch "unsigned-offsets":

- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
  (Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
  to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.


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

11 files changed, 913 insertions, 520 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 7ea1a8a..051b7e4 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -165,8 +165,8 @@ Inductive instruction : Type :=
   | Psufd: freg -> freg -> freg -> instruction     (**r float subtraction *)
 
   (* Pseudo-instructions *)
-  | Pallocframe: Z -> Z -> int -> instruction      (**r allocate new stack frame *)
-  | Pfreeframe: Z -> Z -> int -> instruction       (**r deallocate stack frame and restore previous frame *)
+  | Pallocframe: Z -> int -> instruction      (**r allocate new stack frame *)
+  | Pfreeframe: Z -> int -> instruction       (**r deallocate stack frame and restore previous frame *)
   | Plabel: label -> instruction                   (**r define a code label *)
   | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
@@ -186,20 +186,20 @@ lbl:    .word   symbol
 >>
   Initialized data in the constant data section are not modeled here,
   which is why we use a pseudo-instruction for this purpose.
-- [Pallocframe lo hi pos]: in the formal semantics, this pseudo-instruction
-  allocates a memory block with bounds [lo] and [hi], stores the value
+- [Pallocframe sz pos]: in the formal semantics, this pseudo-instruction
+  allocates a memory block with bounds [0] and [sz], stores the value
   of the stack pointer at offset [pos] in this block, and sets the
   stack pointer to the address of the bottom of this block.
   In the printed ASM assembly code, this allocation is:
 <<
         mov     r12, sp
-        sub     sp, sp, #(hi - lo)
+        sub     sp, sp, #sz
         str     r12, [sp, #pos]
 >>
   This cannot be expressed in our memory model, which does not reflect
   the fact that stack frames are adjacent and allocated/freed
   following a stack discipline.
-- [Pfreeframe pos]: in the formal semantics, this pseudo-instruction
+- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction
   reads the word at [pos] of the block pointed by the stack pointer,
   frees this block, and sets the stack pointer to the value read.
   In the printed ASM assembly code, this freeing
@@ -494,20 +494,20 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Psufd r1 r2 r3 =>     
       OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
   (* Pseudo-instructions *)
-  | Pallocframe lo hi pos =>             
-      let (m1, stk) := Mem.alloc m lo hi in
-      let sp := (Vptr stk (Int.repr lo)) in
+  | Pallocframe sz pos =>             
+      let (m1, stk) := Mem.alloc m 0 sz in
+      let sp := (Vptr stk Int.zero) in
       match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with
       | None => Error
-      | Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2
+      | Some m2 => OK (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2
       end
-  | Pfreeframe lo hi pos =>
+  | Pfreeframe sz pos =>
       match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with
       | None => Error
       | Some v =>
           match rs#IR13 with
           | Vptr stk ofs =>
-              match Mem.free m stk lo hi with
+              match Mem.free m stk 0 sz with
               | None => Error
               | Some m' => OK (nextinstr (rs#IR13 <- v)) m'
               end
@@ -521,7 +521,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pbtbl r tbl =>
       match rs#r with
       | Vint n => 
-          let pos := Int.signed n in
+          let pos := Int.unsigned n in
           if zeq (Zmod pos 4) 0 then
             match list_nth_z tbl (pos / 4) with
             | None => Error
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index b3412fb..a1f8d96 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -36,7 +36,7 @@ Require Import Asm.
 
 Fixpoint is_immed_arith_aux (n: nat) (x msk: int) {struct n}: bool :=
   match n with
-  | O => false
+  | Datatypes.O => false
   | Datatypes.S n' =>
       Int.eq (Int.and x (Int.not msk)) Int.zero ||
       is_immed_arith_aux n' x (Int.ror msk (Int.repr 2))
@@ -55,46 +55,65 @@ Definition is_immed_mem_float (x: int) : bool :=
   Int.eq (Int.and x (Int.repr 3)) Int.zero
   && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x.
   
+(** Decomposition of a 32-bit integer into a list of immediate arguments,
+    whose sum or "or" or "xor" equals the integer. *)
+
+Fixpoint decompose_int_rec (N: nat) (n p: int) : list int :=
+  match N with
+  | Datatypes.O =>
+      if Int.eq_dec n Int.zero then nil else n :: nil
+  | Datatypes.S M =>
+      if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
+        decompose_int_rec M n (Int.add p (Int.repr 2))
+      else
+        let m := Int.shl (Int.repr 255) p in
+        Int.and n m ::
+        decompose_int_rec M (Int.and n (Int.not m)) (Int.add p (Int.repr 2))
+  end.
+
+Definition decompose_int (n: int) : list int :=
+  match decompose_int_rec 12%nat n Int.zero with
+  | nil => Int.zero :: nil
+  | l   => l
+  end.
+
+Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code) :=
+  match l with
+  | nil =>
+      op1 (SOimm Int.zero) :: k                 (**r should never happen *)
+  | i :: l' =>
+      op1 (SOimm i) :: map (fun i => op2 (SOimm i)) l' ++ k
+  end.
+
 (** Smart constructors for integer immediate arguments. *)
 
 Definition loadimm (r: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    Pmov r (SOimm n) :: k
-  else if is_immed_arith (Int.not n) then
-    Pmvn r (SOimm (Int.not n)) :: k
-  else                  (* could be much improved! *)
-    Pmov r (SOimm (Int.and n (Int.repr 255))) ::
-    Porr r r (SOimm (Int.and n (Int.repr 65280))) ::
-    Porr r r (SOimm (Int.and n (Int.repr 16711680))) ::
-    Porr r r (SOimm (Int.and n (Int.repr 4278190080))) ::
-    k.
+  let d1 := decompose_int n in
+  let d2 := decompose_int (Int.not n) in
+  if le_dec (List.length d1) (List.length d2)
+  then iterate_op (Pmov r) (Porr r r) d1 k
+  else iterate_op (Pmvn r) (Pbic r r) d2 k.
 
 Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    Padd r1 r2 (SOimm n) :: k
-  else if is_immed_arith (Int.neg n) then
-    Psub r1 r2 (SOimm (Int.neg n)) :: k
-  else
-    Padd r1 r2 (SOimm (Int.and n (Int.repr 255))) ::
-    Padd r1 r1 (SOimm (Int.and n (Int.repr 65280))) ::
-    Padd r1 r1 (SOimm (Int.and n (Int.repr 16711680))) ::
-    Padd r1 r1 (SOimm (Int.and n (Int.repr 4278190080))) ::
-    k.
+  let d1 := decompose_int n in
+  let d2 := decompose_int (Int.neg n) in
+  if le_dec (List.length d1) (List.length d2)
+  then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
+  else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k.
 
 Definition andimm (r1 r2: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    Pand r1 r2 (SOimm n) :: k
-  else if is_immed_arith (Int.not n) then
-    Pbic r1 r2 (SOimm (Int.not n)) :: k
-  else
-    loadimm IR14 n (Pand r1 r2 (SOreg IR14) :: k).
+  if is_immed_arith n 
+  then Pand r1 r2 (SOimm n) :: k
+  else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int (Int.not n)) k.
 
-Definition makeimm (instr: ireg -> ireg -> shift_op -> instruction)
-                   (r1 r2: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    instr r1 r2 (SOimm n) :: k
-  else
-    loadimm IR14 n (instr r1 r2 (SOreg IR14) :: k).
+Definition rsubimm (r1 r2: ireg) (n: int) (k: code) :=
+  iterate_op (Prsb r1 r2) (Padd r1 r1) (decompose_int n) k.
+
+Definition orimm  (r1 r2: ireg) (n: int) (k: code) :=
+  iterate_op (Porr r1 r2) (Porr r1 r1) (decompose_int n) k.
+
+Definition xorimm  (r1 r2: ireg) (n: int) (k: code) :=
+  iterate_op (Peor r1 r2) (Peor r1 r1) (decompose_int n) k.
 
 (** Translation of a shift immediate operation (type [Op.shift]) *)
 
@@ -235,7 +254,7 @@ Definition transl_op
   | Orsubshift s, a1 :: a2 :: nil =>
       Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
   | Orsubimm n, a1 :: nil =>
-      makeimm Prsb (ireg_of r) (ireg_of a1) n k
+      rsubimm (ireg_of r) (ireg_of a1) n k
   | Omul, a1 :: a2 :: nil =>
       if ireg_eq (ireg_of r) (ireg_of a1)
       || ireg_eq (ireg_of r) (ireg_of a2)
@@ -256,13 +275,13 @@ Definition transl_op
   | Oorshift s, a1 :: a2 :: nil =>
       Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
   | Oorimm n, a1 :: nil =>
-      makeimm Porr (ireg_of r) (ireg_of a1) n k
+      orimm (ireg_of r) (ireg_of a1) n k
   | Oxor, a1 :: a2 :: nil =>
       Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
   | Oxorshift s, a1 :: a2 :: nil =>
       Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
   | Oxorimm n, a1 :: nil =>
-      makeimm Peor (ireg_of r) (ireg_of a1) n k
+      xorimm (ireg_of r) (ireg_of a1) n k
   | Obic, a1 :: a2 :: nil =>
       Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
   | Obicshift s, a1 :: a2 :: nil =>
@@ -469,12 +488,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pblsymb symb :: k
   | Mtailcall sig (inl r) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
-         :: Pbreg (ireg_of r) :: k)
+        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k)
   | Mtailcall sig (inr symb) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
-         :: Pbsymb symb :: k)
+        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb :: k)
   | Mbuiltin ef args res =>
       Pbuiltin ef (map preg_of args) (preg_of res) :: k
   | Mlabel lbl =>
@@ -488,8 +505,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pbtbl IR14 tbl :: k
   | Mreturn =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
-         :: Pbreg IR14 :: k)
+        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: k)
   end.
 
 Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
@@ -501,7 +517,7 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
   around, leading to incorrect executions. *)
 
 Definition transl_function (f: Mach.function) :=
-  Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
+  Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
   Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) ::
   transl_code f f.(fn_code).
 
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index d3e082f..0a429cc 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -330,12 +330,26 @@ Section TRANSL_LABEL.
 
 Variable lbl: label.
 
+Remark iterate_op_label:
+  forall op1 op2 l k,
+  (forall so, is_label lbl (op1 so) = false) ->
+  (forall so, is_label lbl (op2 so) = false) ->
+  find_label lbl (iterate_op op1 op2 l k) = find_label lbl k.
+Proof.
+  intros. unfold iterate_op.
+  destruct l as [ | hd tl].
+  simpl. rewrite H. auto.
+  simpl. rewrite H.  
+  induction tl; simpl. auto. rewrite H0; auto.
+Qed.
+Hint Resolve iterate_op_label: labels.
+
 Remark loadimm_label:
   forall r n k, find_label lbl (loadimm r n k) = find_label lbl k.
 Proof.
-  intros. unfold loadimm. 
-  destruct (is_immed_arith n). reflexivity. 
-  destruct (is_immed_arith (Int.not n)); reflexivity.
+  intros. unfold loadimm.
+  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n))));
+  auto with labels.
 Qed.
 Hint Rewrite loadimm_label: labels.
 
@@ -343,9 +357,8 @@ Remark addimm_label:
   forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
 Proof.
   intros; unfold addimm.
-  destruct (is_immed_arith n). reflexivity.
-  destruct (is_immed_arith (Int.neg n)). reflexivity. 
-  autorewrite with labels. reflexivity.
+  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n))));
+  auto with labels.
 Qed.
 Hint Rewrite addimm_label: labels.
 
@@ -353,31 +366,30 @@ Remark andimm_label:
   forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k.
 Proof.
   intros; unfold andimm.
-  destruct (is_immed_arith n). reflexivity.
-  destruct (is_immed_arith (Int.not n)). reflexivity. 
-  autorewrite with labels. reflexivity.
+  destruct (is_immed_arith n). reflexivity. auto with labels.
 Qed.
 Hint Rewrite andimm_label: labels.
 
-Remark makeimm_Prsb_label:
-  forall r1 r2 n k, find_label lbl (makeimm Prsb r1 r2 n k) = find_label lbl k.
+Remark rsubimm_label:
+  forall r1 r2 n k, find_label lbl (rsubimm r1 r2 n k) = find_label lbl k.
 Proof.
-  intros; unfold makeimm.
-  destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto.
+  intros; unfold rsubimm. auto with labels.
 Qed.
-Remark makeimm_Porr_label:
-  forall r1 r2 n k, find_label lbl (makeimm Porr r1 r2 n k) = find_label lbl k.
+Hint Rewrite rsubimm_label: labels.
+
+Remark orimm_label:
+  forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k.
 Proof.
-  intros; unfold makeimm.
-  destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto.
+  intros; unfold orimm. auto with labels.
 Qed.
-Remark makeimm_Peor_label:
-  forall r1 r2 n k, find_label lbl (makeimm Peor r1 r2 n k) = find_label lbl k.
+Hint Rewrite orimm_label: labels.
+
+Remark xorimm_label:
+  forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k.
 Proof.
-  intros; unfold makeimm.
-  destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto.
+  intros; unfold xorimm. auto with labels.
 Qed.
-Hint Rewrite makeimm_Prsb_label makeimm_Porr_label makeimm_Peor_label: labels.
+Hint Rewrite xorimm_label: labels.
 
 Remark loadind_int_label:
   forall base ofs dst k, find_label lbl (loadind_int base ofs dst k) = find_label lbl k.
@@ -692,7 +704,7 @@ Proof.
   rewrite (sp_val _ _ _ AG) in A.
   exploit loadind_correct. eexact A. reflexivity. 
   intros [rs2 [EX [RES OTH]]].
-  left; eapply exec_straight_steps; eauto with coqlib.
+  left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. 
   exists m'; split; auto.
   simpl. exists rs2; split. eauto. 
   apply agree_set_mreg with rs; auto. congruence. auto with ppcgen. 
@@ -715,19 +727,19 @@ Proof.
   rewrite (sp_val _ _ _ AG) in B.
   exploit storeind_correct. eexact B. reflexivity. congruence.
   intros [rs2 [EX OTH]].
-  left; eapply exec_straight_steps; eauto with coqlib.
+  left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. 
   exists m2; split; auto.
-  exists rs2; split; eauto.
+  simpl. exists rs2; split. eauto.
   apply agree_exten with rs; auto with ppcgen.
 Qed.
 
 Lemma exec_Mgetparam_prop:
-  forall (s : list stackframe) (fb : block) (f: Mach.function) (sp parent : val)
+  forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : val)
          (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction)
          (ms : Mach.regset) (m : mem) (v : val),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m sp Tint f.(fn_link_ofs) = Some parent ->
-  load_stack m parent ty ofs = Some v ->
+  load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+  load_stack m (parent_sp s) ty ofs = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
                   (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
 Proof.
@@ -738,18 +750,18 @@ Proof.
   unfold load_stack in *.
   exploit Mem.loadv_extends. eauto. eexact H0. eauto. 
   intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  assert (parent' = parent). inv B. auto. simpl in H1; discriminate. subst parent'.
+  assert (parent' = parent_sp s). inv B. auto. rewrite <- H3 in H1; discriminate. subst parent'.
   exploit Mem.loadv_extends. eauto. eexact H1. eauto. 
   intros [v' [C D]]. 
   exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_link_ofs) IR14
-                 rs m' parent (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))).
+                 rs m' (parent_sp s) (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))).
   auto.
   intros [rs1 [EX1 [RES1 OTH1]]].
   exploit (loadind_correct tge (transl_function f) IR14 ofs (mreg_type dst) dst
                 (transl_code f c) rs1 m' v').
   rewrite RES1. auto. auto. 
   intros [rs2 [EX2 [RES2 OTH2]]].
-  left. eapply exec_straight_steps; eauto with coqlib.
+  left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. 
   exists m'; split; auto.
   exists rs2; split; simpl.
   eapply exec_straight_trans; eauto.
@@ -762,20 +774,20 @@ Lemma exec_Mop_prop:
   forall (s : list stackframe) (fb : block) (sp : val) (op : operation)
          (args : list mreg) (res : mreg) (c : list Mach.instruction)
          (ms : mreg -> val) (m : mem) (v : val),
-  eval_operation ge sp op ms ## args = Some v ->
+  eval_operation ge sp op ms ## args m = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0
                   (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI.
-  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. 
+  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto.
   intros [v' [A B]]. 
-  assert (C: eval_operation tge sp op rs ## (preg_of ## args) = Some v').
+  assert (C: eval_operation tge sp op rs ## (preg_of ## args) m' = Some v').
     rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
   rewrite (sp_val _ _ _ AG) in C.
   exploit transl_op_correct; eauto. intros [rs' [P [Q R]]].
-  left; eapply exec_straight_steps; eauto with coqlib.
+  left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. 
   exists m'; split; auto.
   exists rs'; split. simpl. eexact P. 
   assert (agree (Regmap.set res v ms) sp rs').
@@ -809,7 +821,8 @@ Proof.
   eauto; intros; reflexivity.
 Qed.
 
-Lemma storev_8_signed_unsigned:
  forall m a v,
  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_8.
Qed.

Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_16.
Qed.
+Lemma storev_8_signed_unsigned:
  forall m a v,
  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
  intros. unfold Mem.storev. 
+  destruct a; auto.
  apply Mem.store_signed_unsigned_8.
Qed.

Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_16.
Qed.
 

 Lemma exec_Mstore_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
@@ -826,7 +839,7 @@ Proof.
   intro WTI; inv WTI.
   assert (eval_addressing tge sp addr ms##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
-  left; eapply exec_straight_steps; eauto with coqlib. 
+  left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. 
   destruct chunk; simpl; simpl in H6;
   try (rewrite storev_8_signed_unsigned in H0);
   try (rewrite storev_16_signed_unsigned in H0);
@@ -896,8 +909,19 @@ Proof.
   intros. rewrite Pregmap.gso; auto with ppcgen.
 Qed.
 
-
-Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff : int)
         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
  find_function_ptr ge ros ms = Some f' ->
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
  exec_instr_prop
          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
          (Callstate s f' ms m').
Proof.
+Lemma exec_Mtailcall_prop:
+  forall (s : list stackframe) (fb stk : block) (soff : int)
+         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
+         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
+  find_function_ptr ge ros ms = Some f' ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+  exec_instr_prop
+          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
+          (Callstate s f' ms m').
+Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -906,7 +930,7 @@ Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff
          match ros with inl r => Pbreg (ireg_of r) | inr symb => Pbsymb symb end).
   assert (TR: transl_code f (Mtailcall sig ros :: c) =
               loadind_int IR13 (fn_retaddr_ofs f) IR14
-                (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)).
+                (Pfreeframe f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)).
   unfold call_instr; destruct ros; auto.
   unfold load_stack in *.
   exploit Mem.loadv_extends. eauto. eexact H1. auto. 
@@ -918,7 +942,7 @@ Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
                 rs m'0 (parent_ra s) 
-                (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c))
+                (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c))
   as [rs1 [EXEC1 [RES1 OTH1]]].
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
   set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
@@ -1021,7 +1045,7 @@ Lemma exec_Mcond_true_prop:
          (cond : condition) (args : list mreg) (lbl : Mach.label)
          (c : list Mach.instruction) (ms : mreg -> val) (m : mem)
          (c' : Mach.code),
-  eval_condition cond ms ## args = Some true ->
+  eval_condition cond ms ## args m = Some true ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
@@ -1030,7 +1054,8 @@ Proof.
   intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inv WTI.
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A.
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
+  intros A.
   exploit transl_cond_correct. eauto. eauto. 
   intros [rs2 [EX [RES OTH]]].
   inv AT. simpl in H5.
@@ -1057,14 +1082,15 @@ Lemma exec_Mcond_false_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (cond : condition) (args : list mreg) (lbl : Mach.label)
          (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
-  eval_condition cond ms ## args = Some false ->
+  eval_condition cond ms ## args m = Some false ->
   exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
                   (Machconcr.State s fb sp c (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inv WTI.
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A.
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
+  intros A.
   exploit transl_cond_correct. eauto. eauto. 
   intros [rs2 [EX [RES OTH]]].
   left; eapply exec_straight_steps; eauto with coqlib.
@@ -1081,7 +1107,7 @@ Lemma exec_Mjumptable_prop:
          (ms : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
          (c' : Mach.code),
   ms arg = Vint n ->
-  list_nth_z tbl (Int.signed n) = Some lbl ->
+  list_nth_z tbl (Int.unsigned n) = Some lbl ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop
@@ -1093,11 +1119,10 @@ Proof.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inv WTI.
   exploit list_nth_z_range; eauto. intro RANGE.
-  assert (SHIFT: Int.signed (Int.shl n (Int.repr 2)) = Int.signed n * 4).
+  assert (SHIFT: Int.unsigned (Int.shl n (Int.repr 2)) = Int.unsigned n * 4).
     rewrite Int.shl_mul.
-    rewrite Int.mul_signed.
-    apply Int.signed_repr.
-    split. apply Zle_trans with 0. vm_compute; congruence. omega. 
+    unfold Int.mul.
+    apply Int.unsigned_repr.
     omega.
   inv AT. simpl in H7. 
   set (k1 := Pbtbl IR14 tbl :: transl_code f c).
@@ -1122,9 +1147,8 @@ Proof.
   eapply find_instr_tail. unfold k1 in CT1. eauto.
   unfold exec_instr.
   change (rs1 IR14) with (Vint (Int.shl n (Int.repr 2))).
-Opaque Zmod.  Opaque Zdiv.
-  simpl. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true. 
-  rewrite Z_div_mult. 
+  lazy iota beta. rewrite SHIFT. 
+  rewrite Z_mod_mult. rewrite zeq_true. rewrite Z_div_mult. 
   change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
@@ -1133,7 +1157,16 @@ Opaque Zmod.  Opaque Zdiv.
   apply agree_undef_temps; auto.
 Qed.
 
-Lemma exec_Mreturn_prop:
  forall (s : list stackframe) (fb stk : block) (soff : int)
         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
                  (Returnstate s ms m').
Proof.
+Lemma exec_Mreturn_prop:
+  forall (s : list stackframe) (fb stk : block) (soff : int)
+         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
+                  (Returnstate s ms m').
+Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
   unfold load_stack in *.
@@ -1147,13 +1180,13 @@ Lemma exec_Mreturn_prop:
  forall (s : list stackframe) (fb stk : block) (soff :
 
   exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
                 rs m'0 (parent_ra s)
-                (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
+                (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
   intros [rs1 [EXEC1 [RES1 OTH1]]].
   set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
   assert (EXEC2: exec_straight tge (transl_function f)
           (loadind_int IR13 (fn_retaddr_ofs f) IR14
-             (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize)  (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
+             (Pfreeframe f.(fn_stacksize)  (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
           rs m'0 (Pbreg IR14 :: transl_code f c) rs2 m2').
   eapply exec_straight_trans. eexact EXEC1. 
   apply exec_straight_one. simpl. rewrite OTH1; try congruence.
@@ -1188,12 +1221,12 @@ Lemma exec_function_internal_prop:
   forall (s : list stackframe) (fb : block) (ms : Mach.regset)
          (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
-  let sp := Vptr stk (Int.repr (- fn_framesize f)) in
+  Mem.alloc m 0 (fn_stacksize f) = (m1, stk) ->
+  let sp := Vptr stk Int.zero in
   store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
   store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
   exec_instr_prop (Machconcr.Callstate s fb ms m) E0
-                  (Machconcr.State s fb sp (fn_code f) ms m3).
+                  (Machconcr.State s fb sp (fn_code f) (undef_temps ms) m3).
 Proof.
   intros; red; intros; inv MS.
   assert (WTF: wt_function f).
@@ -1201,7 +1234,7 @@ Proof.
     inversion TY; auto.
   exploit functions_transl; eauto. intro TFIND.
   generalize (functions_transl_no_overflow _ _ H); intro NOOV.
-  set (rs2 := nextinstr (rs#IR13 <- sp)).
+  set (rs2 := nextinstr (rs#IR12 <- (rs#IR13) #IR13 <- sp)).
   set (rs3 := nextinstr rs2).
   exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
   intros [m1' [A B]].
@@ -1218,7 +1251,7 @@ Proof.
   unfold transl_function at 2.
   apply exec_straight_two with rs2 m2'.
   unfold exec_instr. rewrite A. fold sp. 
-  rewrite <- (sp_val ms (parent_sp s) rs); auto. rewrite C. auto.
+  rewrite (sp_val ms (parent_sp s) rs) in C; auto. rewrite C. auto.
   unfold exec_instr. unfold eval_shift_addr. unfold exec_store.
   change (rs2 IR13) with sp. change (rs2 IR14) with (rs IR14). rewrite ATLR.
   rewrite E. auto. 
@@ -1231,10 +1264,12 @@ Proof.
     eapply code_tail_next_int; auto.
     change (Int.unsigned Int.zero) with 0. 
     unfold transl_function. constructor.
-  assert (AG3: agree ms sp rs3).
+  assert (AG3: agree (undef_temps ms) sp rs3).
     unfold rs3. apply agree_nextinstr.
     unfold rs2. apply agree_nextinstr. 
-    apply agree_change_sp with (parent_sp s); auto. 
+    apply agree_change_sp with (parent_sp s).
+    apply agree_exten_temps with rs; auto.
+    intros. apply Pregmap.gso; auto with ppcgen.
     unfold sp. congruence.
   left; exists (State rs3 m3'); split.
   (* execution *)
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index c10c9df..fb49cb7 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -441,6 +441,169 @@ Qed.
 
 (** * Correctness of ARM constructor functions *)
 
+(** Decomposition of an integer constant *)
+
+Lemma decompose_int_rec_or:
+  forall N n p x, List.fold_left Int.or (decompose_int_rec N n p) x = Int.or x n.
+Proof.
+  induction N; intros; simpl.
+  destruct (Int.eq_dec n Int.zero); simpl. 
+  subst n. rewrite Int.or_zero. auto.
+  auto.
+  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  auto.
+  simpl. rewrite IHN. rewrite Int.or_assoc. decEq. rewrite <- Int.and_or_distrib.
+  rewrite Int.or_not_self. apply Int.and_mone.
+Qed.
+
+Lemma decompose_int_rec_xor:
+  forall N n p x, List.fold_left Int.xor (decompose_int_rec N n p) x = Int.xor x n.
+Proof.
+  induction N; intros; simpl.
+  destruct (Int.eq_dec n Int.zero); simpl. 
+  subst n. rewrite Int.xor_zero. auto.
+  auto.
+  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  auto.
+  simpl. rewrite IHN. rewrite Int.xor_assoc. decEq. rewrite <- Int.and_xor_distrib.
+  rewrite Int.xor_not_self. apply Int.and_mone.
+Qed.
+
+Lemma decompose_int_rec_add:
+  forall N n p x, List.fold_left Int.add (decompose_int_rec N n p) x = Int.add x n.
+Proof.
+  induction N; intros; simpl.
+  destruct (Int.eq_dec n Int.zero); simpl. 
+  subst n. rewrite Int.add_zero. auto.
+  auto.
+  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  auto.
+  simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. 
+  rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self.
+Qed.
+
+Remark decompose_int_rec_nil:
+  forall N n p, decompose_int_rec N n p = nil -> n = Int.zero.
+Proof.
+  intros. generalize (decompose_int_rec_or N n p Int.zero). rewrite H. simpl. 
+  rewrite Int.or_commut; rewrite Int.or_zero; auto.
+Qed.
+
+Lemma decompose_int_general:
+  forall (f: val -> int -> val) (g: int -> int -> int),
+  (forall v1 n2 n3, f (f v1 n2) n3 = f v1 (g n2 n3)) ->
+  (forall n1 n2 n3, g (g n1 n2) n3 = g n1 (g n2 n3)) ->
+  (forall n, g Int.zero n = n) ->
+  (forall N n p x, List.fold_left g (decompose_int_rec N n p) x = g x n) ->
+  forall n v,
+  List.fold_left f (decompose_int n) v = f v n.
+Proof.
+  intros f g DISTR ASSOC ZERO DECOMP.
+  assert (A: forall l x y, g x (fold_left g l y) = fold_left g l (g x y)).
+    induction l; intros; simpl. auto. rewrite IHl. decEq. rewrite ASSOC; auto.
+  assert (B: forall l v n, fold_left f l (f v n) = f v (fold_left g l n)).
+    induction l; intros; simpl.
+    auto.
+    rewrite IHl. rewrite DISTR. decEq. decEq. auto.
+  intros. unfold decompose_int. 
+  destruct (decompose_int_rec 12 n Int.zero) as []_eqn. 
+  simpl. exploit decompose_int_rec_nil; eauto. congruence.
+  simpl. rewrite B. decEq.  
+  generalize (DECOMP 12%nat n Int.zero Int.zero).
+  rewrite Heql. simpl. repeat rewrite ZERO. auto.
+Qed.
+
+Lemma decompose_int_or:
+  forall n v,
+  List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) v = Val.or v (Vint n).
+Proof.
+  intros. apply decompose_int_general with (f := fun v n => Val.or v (Vint n)) (g := Int.or).
+  intros. rewrite Val.or_assoc. auto.
+  apply Int.or_assoc.
+  intros. rewrite Int.or_commut. apply Int.or_zero.
+  apply decompose_int_rec_or.
+Qed.
+
+Lemma decompose_int_bic:
+  forall n v,
+  List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int n) v = Val.and v (Vint (Int.not n)).
+Proof.
+  intros. apply decompose_int_general with (f := fun v n => Val.and v (Vint (Int.not n))) (g := Int.or).
+  intros. rewrite Val.and_assoc. simpl. decEq. decEq. rewrite Int.not_or_and_not. auto.
+  apply Int.or_assoc.
+  intros. rewrite Int.or_commut. apply Int.or_zero.
+  apply decompose_int_rec_or.
+Qed.
+
+Lemma decompose_int_xor:
+  forall n v,
+  List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) v = Val.xor v (Vint n).
+Proof.
+  intros. apply decompose_int_general with (f := fun v n => Val.xor v (Vint n)) (g := Int.xor).
+  intros. rewrite Val.xor_assoc. auto. 
+  apply Int.xor_assoc.
+  intros. rewrite Int.xor_commut. apply Int.xor_zero.
+  apply decompose_int_rec_xor.
+Qed.
+
+Lemma decompose_int_add:
+  forall n v,
+  List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) v = Val.add v (Vint n).
+Proof.
+  intros. apply decompose_int_general with (f := fun v n => Val.add v (Vint n)) (g := Int.add).
+  intros. rewrite Val.add_assoc. auto. 
+  apply Int.add_assoc.
+  intros. rewrite Int.add_commut. apply Int.add_zero.
+  apply decompose_int_rec_add.
+Qed.
+
+Lemma decompose_int_sub:
+  forall n v,
+  List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int n) v = Val.sub v (Vint n).
+Proof.
+  intros. apply decompose_int_general with (f := fun v n => Val.sub v (Vint n)) (g := Int.add).
+  intros. repeat rewrite Val.sub_add_opp. rewrite Val.add_assoc. decEq. simpl. decEq. 
+  rewrite Int.neg_add_distr; auto.
+  apply Int.add_assoc.
+  intros. rewrite Int.add_commut. apply Int.add_zero.
+  apply decompose_int_rec_add.
+Qed.
+
+Lemma iterate_op_correct:
+  forall op1 op2 (f: val -> int -> val) (rs: regset) (r: ireg) m v0 n k,
+  (forall (rs:regset) n,
+    exec_instr ge fn (op2 (SOimm n)) rs m =
+    OK (nextinstr (rs#r <- (f (rs#r) n))) m) ->
+  (forall n,
+    exec_instr ge fn (op1 (SOimm n)) rs m =
+    OK (nextinstr (rs#r <- (f v0 n))) m) ->
+  exists rs',
+     exec_straight (iterate_op op1 op2 (decompose_int n) k) rs m  k rs' m
+  /\ rs'#r = List.fold_left f (decompose_int n) v0
+  /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+  intros until k; intros SEM2 SEM1.
+  unfold iterate_op.
+  destruct (decompose_int n) as [ | i tl] _eqn.
+  unfold decompose_int in Heql. destruct (decompose_int_rec 12%nat n Int.zero); congruence.
+  revert k. pattern tl. apply List.rev_ind.
+  (* base case *)
+  intros; simpl. econstructor.
+  split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity.
+  split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. auto.
+  intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen.
+  (* inductive case *)
+  intros. 
+  rewrite List.map_app. simpl. rewrite app_ass. simpl. 
+  destruct (H (op2 (SOimm x) :: k)) as [rs' [A [B C]]].
+  econstructor.
+  split. eapply exec_straight_trans. eexact A. apply exec_straight_one.
+  rewrite SEM2. reflexivity. reflexivity.
+  split. rewrite fold_left_app; simpl. rewrite nextinstr_inv; auto with ppcgen.
+  rewrite Pregmap.gss. rewrite B. auto.
+  intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen.
+Qed.
+  
 (** Loading a constant. *)
 
 Lemma loadimm_correct:
@@ -451,46 +614,19 @@ Lemma loadimm_correct:
   /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold loadimm.
-  case (is_immed_arith n).
-  (* single move *)
-  exists (nextinstr (rs#r <- (Vint n))).
-  split. apply exec_straight_one. reflexivity. reflexivity.  
-  split. rewrite nextinstr_inv; auto with ppcgen.
-   apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  case (is_immed_arith (Int.not n)).
-  (* single move-complement *)
-  exists (nextinstr (rs#r <- (Vint n))).
-  split. apply exec_straight_one.
-  simpl. change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)).
-  rewrite Int.not_involutive. auto.
-  reflexivity.
-  split. rewrite nextinstr_inv; auto with ppcgen.
-   apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  (* mov - or - or - or *)
-  set (n1 := Int.and n (Int.repr 255)).
-  set (n2 := Int.and n (Int.repr 65280)).
-  set (n3 := Int.and n (Int.repr 16711680)).
-  set (n4 := Int.and n (Int.repr 4278190080)).
-  set (rs1 := nextinstr (rs#r <- (Vint n1))).
-  set (rs2 := nextinstr (rs1#r <- (Val.or rs1#r (Vint n2)))).
-  set (rs3 := nextinstr (rs2#r <- (Val.or rs2#r (Vint n3)))).
-  set (rs4 := nextinstr (rs3#r <- (Val.or rs3#r (Vint n4)))).
-  exists rs4.
-  split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto. 
-  split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
-  repeat rewrite Val.or_assoc. simpl. decEq. 
-  unfold n4, n3, n2, n1. repeat rewrite <- Int.and_or_distrib. 
-  change (Int.and n Int.mone = n). apply Int.and_mone.
-  intros. 
-  unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))).
+  (* mov - orr* *)
+  replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero).
+  apply iterate_op_correct.
+  auto.
+  intros; simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto.
+  rewrite decompose_int_or. simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto.
+  (* mvn - bic* *)
+  replace (Vint n) with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (Vint Int.mone)).
+  apply iterate_op_correct.
+  auto.
+  intros. simpl. rewrite Int.and_commut; rewrite Int.and_mone; auto.
+  rewrite decompose_int_bic. simpl. rewrite Int.not_involutive. rewrite Int.and_commut. rewrite Int.and_mone; auto.
 Qed.
 
 (** Add integer immediate. *)
@@ -503,46 +639,21 @@ Lemma addimm_correct:
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold addimm.
-  (* addi *)
-  case (is_immed_arith n).
-  exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))).
-  split. apply exec_straight_one; auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  (* subi *)
-  case (is_immed_arith (Int.neg n)).
-  exists (nextinstr (rs#r1 <- (Val.sub rs#r2 (Vint (Int.neg n))))).
-  split. apply exec_straight_one; auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
-    apply Val.sub_opp_add.
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  (* general *)
-  set (n1 := Int.and n (Int.repr 255)).
-  set (n2 := Int.and n (Int.repr 65280)).
-  set (n3 := Int.and n (Int.repr 16711680)).
-  set (n4 := Int.and n (Int.repr 4278190080)).
-  set (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n1)))).
-  set (rs2 := nextinstr (rs1#r1 <- (Val.add rs1#r1 (Vint n2)))).
-  set (rs3 := nextinstr (rs2#r1 <- (Val.add rs2#r1 (Vint n3)))).
-  set (rs4 := nextinstr (rs3#r1 <- (Val.add rs3#r1 (Vint n4)))).
-  exists rs4.
-  split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto. 
-  simpl. 
-  split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
-  repeat rewrite Val.add_assoc. simpl. decEq. decEq. 
-  unfold n4, n3, n2, n1. repeat rewrite Int.add_and.
-  change (Int.and n Int.mone = n). apply Int.and_mone.
-  vm_compute; auto.
-  vm_compute; auto.
-  vm_compute; auto.
-  intros.
-  unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
+  (* add - add* *)
+  replace (Val.add (rs r2) (Vint n))
+     with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)).
+  apply iterate_op_correct.
+  auto.
+  auto.
+  apply decompose_int_add.
+  (* sub - sub* *)
+  replace (Val.add (rs r2) (Vint n))
+     with (List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int (Int.neg n)) (rs r2)).
+  apply iterate_op_correct.
+  auto.
+  auto.
+  rewrite decompose_int_sub. apply Val.sub_opp_add.
 Qed.
 
 (* And integer immediate *)
@@ -553,7 +664,7 @@ Lemma andimm_correct:
   exists rs',
      exec_straight (andimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.and rs#r2 (Vint n)
-  /\ forall r': preg, r' <> r1 -> r' <> IR14 -> r' <> PC -> rs'#r' = rs#r'.
+  /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold andimm.
   (* andi *)
@@ -562,57 +673,72 @@ Proof.
   split. apply exec_straight_one; auto.
   split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
   intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  (* bici *)
-  case (is_immed_arith (Int.not n)).
-  exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))).
-  split. apply exec_straight_one; auto. simpl.
-    change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)).
-    rewrite Int.not_involutive. auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  (* general *)
-  exploit loadimm_correct. intros [rs' [A [B C]]].
-  exists (nextinstr (rs'#r1 <- (Val.and rs#r2 (Vint n)))).
-  split. eapply exec_straight_trans. eauto. apply exec_straight_one.
-  simpl. rewrite B. rewrite C; auto with ppcgen. 
+  (* bic - bic* *)
+  replace (Val.and (rs r2) (Vint n))
+     with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (rs r2)).
+  apply iterate_op_correct.
   auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  auto.
+  rewrite decompose_int_bic. rewrite Int.not_involutive. auto.
 Qed.
 
-(** Other integer immediate *)
+(** Reverse sub immediate *)
 
-Lemma makeimm_correct:
-  forall (instr: ireg -> ireg -> shift_op -> instruction)
-         (sem: val -> val -> val)
-         r1 (r2: ireg) n k (rs : regset) m,
-  (forall c r1 r2 so rs m,
-   exec_instr ge c (instr r1 r2 so) rs m 
-   = OK (nextinstr rs#r1 <- (sem rs#r2 (eval_shift_op so rs))) m) ->
-   r2 <> IR14 ->
+Lemma rsubimm_correct:
+  forall r1 r2 n k rs m,
   exists rs',
-     exec_straight (makeimm instr r1 r2 n k) rs m  k rs' m
-  /\ rs'#r1 = sem rs#r2 (Vint n)
-  /\ forall r': preg, r' <> r1 -> r' <> PC -> r' <> IR14 -> rs'#r' = rs#r'.
+     exec_straight (rsubimm r1 r2 n k) rs m  k rs' m
+  /\ rs'#r1 = Val.sub (Vint n) rs#r2
+  /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
-  intros. unfold makeimm.
-  case (is_immed_arith n).
-  (* one immed instr *)
-  exists (nextinstr (rs#r1 <- (sem rs#r2 (Vint n)))).
-  split. apply exec_straight_one. 
-    change (Vint n) with (eval_shift_op (SOimm n) rs). auto.
-    auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  (* general case *)
-  exploit loadimm_correct. intros [rs' [A [B C]]].
-  exists (nextinstr (rs'#r1 <- (sem rs#r2 (Vint n)))).
-  split. eapply exec_straight_trans. eauto. apply exec_straight_one. 
-    rewrite <- B. rewrite <- (C r2). 
-    change (rs' IR14) with (eval_shift_op (SOreg IR14) rs'). auto.
-    congruence. auto with ppcgen. auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto with ppcgen.
+  intros. unfold rsubimm.
+  (* rsb - add* *)
+  replace (Val.sub (Vint n) (rs r2))
+     with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (Val.neg (rs r2))).
+  apply iterate_op_correct.
+  auto.
+  intros. simpl. destruct (rs r2); auto. simpl. rewrite Int.sub_add_opp.
+  rewrite Int.add_commut; auto.
+  rewrite decompose_int_add. 
+  destruct (rs r2); simpl; auto. rewrite Int.sub_add_opp. rewrite Int.add_commut; auto.
+Qed.
+
+(** Or immediate *)
+
+Lemma orimm_correct:
+  forall r1 r2 n k rs m,
+  exists rs',
+     exec_straight (orimm r1 r2 n k) rs m  k rs' m
+  /\ rs'#r1 = Val.or rs#r2 (Vint n)
+  /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold orimm.
+  (* ori - ori* *)
+  replace (Val.or (rs r2) (Vint n))
+     with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) (rs r2)).
+  apply iterate_op_correct.
+  auto.
+  auto.
+  apply decompose_int_or.
+Qed.
+
+(** Xor immediate *)
+
+Lemma xorimm_correct:
+  forall r1 r2 n k rs m,
+  exists rs',
+     exec_straight (xorimm r1 r2 n k) rs m  k rs' m
+  /\ rs'#r1 = Val.xor rs#r2 (Vint n)
+  /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold xorimm.
+  (* xori - xori* *)
+  replace (Val.xor (rs r2) (Vint n))
+     with (List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) (rs r2)).
+  apply iterate_op_correct.
+  auto.
+  auto.
+  apply decompose_int_xor.
 Qed.
 
 (** Indexed memory loads. *)
@@ -636,8 +762,7 @@ Proof.
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
     simpl. unfold exec_load. rewrite B.
     rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
-    rewrite H. auto.
-    auto.
+    rewrite H. auto. auto.
   split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
   intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
 Qed.
@@ -659,7 +784,8 @@ Proof.
   exploit addimm_correct. eauto. intros [rs' [A [B C]]].
   exists (nextinstr (rs'#dst <- v)).
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
-    simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. 
+    simpl. unfold exec_load. rewrite B.
+    rewrite Val.add_assoc. simpl. 
     rewrite Int.add_zero. rewrite H. auto. auto.
   split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
   intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
@@ -700,8 +826,8 @@ Proof.
   exploit addimm_correct. eauto. intros [rs' [A [B C]]].
   exists (nextinstr rs').
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
-    simpl. unfold exec_store. rewrite B. rewrite C.
-    rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
+    simpl. unfold exec_store. rewrite B.
+    rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
     rewrite H. auto. 
     congruence. auto with ppcgen. auto.
   intros. rewrite nextinstr_inv; auto.
@@ -723,10 +849,11 @@ Proof.
   exploit addimm_correct. eauto. intros [rs' [A [B C]]].
   exists (nextinstr rs').
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
-    simpl. unfold exec_store. rewrite B. rewrite C.
-    rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
+    simpl. unfold exec_store. rewrite B. 
+    rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
     rewrite H. auto.
-    congruence. congruence. auto with ppcgen. auto.
+    congruence. congruence. 
+    auto with ppcgen. 
   intros. rewrite nextinstr_inv; auto.
 Qed.
 
@@ -827,13 +954,14 @@ Ltac TypeInv := TypeInv1; simpl in *; unfold preg_of in *; TypeInv2.
 Lemma transl_cond_correct:
   forall cond args k rs m b,
   map mreg_type args = type_of_condition cond ->
-  eval_condition cond (map rs (map preg_of args)) = Some b ->
+  eval_condition cond (map rs (map preg_of args)) m = Some b ->
   exists rs',
      exec_straight (transl_cond cond args k) rs m k rs' m
   /\ rs'#(CR (crbit_for_cond cond)) = Val.of_bool b
   /\ forall r, important_preg r = true -> rs'#r = rs r.
 Proof.
-  intros until b; intros TY EV. rewrite <- (eval_condition_weaken _ _ EV). clear EV.  
+  intros until b; intros TY EV. 
+  rewrite <- (eval_condition_weaken _ _ _ EV). clear EV.  
   destruct cond; simpl in TY; TypeInv.
   (* Ccomp *)
   generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))).
@@ -917,11 +1045,11 @@ Qed.
 
 Ltac Simpl :=
   match goal with
-  | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
-  | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
-  | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
-  | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
-  | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
+  | [ |- context[nextinstr _ _] ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
+  | [ |- context[Pregmap.get ?x (Pregmap.set ?x _ _)] ] => rewrite Pregmap.gss; auto
+  | [ |- context[Pregmap.set ?x _ _ ?x] ] => rewrite Pregmap.gss; auto
+  | [ |- context[Pregmap.get _ (Pregmap.set _ _ _)] ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
+  | [ |- context[Pregmap.set _ _ _ _] ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
   end.
 
 Ltac TranslOpSimpl :=
@@ -932,13 +1060,13 @@ Ltac TranslOpSimpl :=
 Lemma transl_op_correct:
   forall op args res k (rs: regset) m v,
   wt_instr (Mop op args res) ->
-  eval_operation ge rs#IR13 op (map rs (map preg_of args)) = Some v ->
+  eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v ->
   exists rs',
      exec_straight (transl_op op args res k) rs m k rs' m
   /\ rs'#(preg_of res) = v
   /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
 Proof.
-  intros. rewrite <- (eval_operation_weaken _ _ _ _ H0). inv H.
+  intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H0). inv H.
   (* Omove *)
   simpl.
   exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))).
@@ -952,7 +1080,7 @@ Proof.
   congruence.
   (* Ointconst *)
   generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. split. auto. intros. auto with ppcgen.
+  exists rs'. split. auto. split. rewrite B; auto. intros. auto with ppcgen.
   (* Oaddrstack *)
   generalize (addimm_correct (ireg_of res) IR13 i k rs m). 
   intros [rs' [EX [RES OTH]]].
@@ -960,41 +1088,43 @@ Proof.
   (* Ocast8signed *)
   econstructor; split.
   eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+  split. Simpl. Simpl. Simpl. Simpl. 
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. 
+  reflexivity.
   compute; auto.
   intros. repeat Simpl. 
   (* Ocast8unsigned *)
   econstructor; split.
-  eapply exec_straight_one. simpl; eauto. auto. 
-  split. Simpl. Simpl.
-  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. reflexivity.
+  eapply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. Simpl. 
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. auto.
   compute; auto.
-  intros. repeat Simpl.
+  intros. repeat Simpl. 
   (* Ocast16signed *)
   econstructor; split.
   eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+  split. Simpl. Simpl. Simpl. Simpl. 
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. auto.
   compute; auto.
   intros. repeat Simpl. 
   (* Ocast16unsigned *)
   econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
+  split. Simpl. Simpl. Simpl. Simpl. 
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl; auto.
   compute; auto.
-  intros. repeat Simpl.
+  intros. repeat Simpl. 
   (* Oaddimm *)
   generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m).
   intros [rs' [A [B C]]]. 
   exists rs'. split. auto. split. auto. auto with ppcgen.
   (* Orsbimm *)
-  exploit (makeimm_correct Prsb (fun v1 v2 => Val.sub v2 v1) (ireg_of res) (ireg_of m0));
-  auto with ppcgen.
+  generalize (rsubimm_correct (ireg_of res) (ireg_of m0) i k rs m).
   intros [rs' [A [B C]]].
   exists rs'.
-  split. eauto. split. rewrite B. auto. auto with ppcgen. 
+  split. eauto. split. rewrite B. 
+  destruct (rs (ireg_of m0)); auto. 
+  auto with ppcgen. 
   (* Omul *)
   destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)).
   econstructor; split.
@@ -1006,17 +1136,15 @@ Proof.
   generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
                             (ireg_of_not_IR14 m0)).
   intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. split. auto. auto with ppcgen.
+  exists rs'; auto with ppcgen.
   (* Oorimm *)
-  exploit (makeimm_correct Porr Val.or (ireg_of res) (ireg_of m0));
-  auto with ppcgen.
+  generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m).
   intros [rs' [A [B C]]]. 
-  exists rs'. split. eauto. split. auto. auto with ppcgen.
+  exists rs'; auto with ppcgen.
   (* Oxorimm *)
-  exploit (makeimm_correct Peor Val.xor (ireg_of res) (ireg_of m0));
-  auto with ppcgen.
+  generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m).
   intros [rs' [A [B C]]]. 
-  exists rs'. split. eauto. split. auto. auto with ppcgen.
+  exists rs'; auto with ppcgen.
   (* Oshrximm *)
   assert (exists n, rs (ireg_of m0) = Vint n /\ Int.ltu i (Int.repr 31) = true).
     destruct (rs (ireg_of m0)); try discriminate.
@@ -1050,8 +1178,11 @@ Proof.
   auto. unfold rs3. case islt; auto. auto.
   split. unfold rs4. repeat Simpl. rewrite ARG1. simpl. rewrite LTU'. rewrite Int.shrx_shr.
   fold islt. unfold rs3. rewrite nextinstr_inv; auto with ppcgen. 
-  destruct islt. rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). 
-  rewrite ARG1. simpl. rewrite LTU'. auto.
+  destruct islt. 
+  rewrite RES2. 
+  change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))).
+  rewrite ARG1.
+  simpl. rewrite LTU'. auto.
   rewrite Pregmap.gss. simpl. rewrite LTU'. auto. 
   assumption.
   intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl. 
@@ -1059,10 +1190,10 @@ Proof.
   rewrite OTH2; auto with ppcgen.
   (* Ocmp *)
   fold preg_of in *.
-  assert (exists b, eval_condition c rs ## (preg_of ## args) = Some b /\ v = Val.of_bool b).
-    fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args)).
+  assert (exists b, eval_condition c rs ## (preg_of ## args) m = Some b /\ v = Val.of_bool b).
+    fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args) m).
     exists b; split; auto. destruct b; inv H0; auto. congruence.
-  clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ EVC).
+  clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ _ EVC).
   destruct (transl_cond_correct c args 
              (Pmov (ireg_of res) (SOimm Int.zero)
               :: Pmovc (crbit_for_cond c) (ireg_of res) (SOimm Int.one) :: k)
diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v
index 359aaf2..97250a6 100644
--- a/arm/Asmgenretaddr.v
+++ b/arm/Asmgenretaddr.v
@@ -102,6 +102,16 @@ Ltac IsTail :=
   | _ => idtac
   end.
 
+Lemma iterate_op_tail:
+  forall op1 op2 l k, is_tail k (iterate_op op1 op2 l k).
+Proof. 
+  intros. unfold iterate_op. 
+  destruct l.
+  auto with coqlib.
+  constructor. revert l; induction l; simpl; auto with coqlib.
+Qed.
+Hint Resolve iterate_op_tail: ppcretaddr.
+
 Lemma loadimm_tail:
   forall r n k, is_tail k (loadimm r n k).
 Proof. unfold loadimm; intros; IsTail. Qed.
@@ -117,10 +127,20 @@ Lemma andimm_tail:
 Proof. unfold andimm; intros; IsTail. Qed.
 Hint Resolve andimm_tail: ppcretaddr.
 
-Lemma makeimm_tail:
-  forall f r1 r2 n k, is_tail k (makeimm f r1 r2 n k).
-Proof. unfold makeimm; intros; IsTail. Qed.
-Hint Resolve makeimm_tail: ppcretaddr.
+Lemma rsubimm_tail:
+  forall r1 r2 n k, is_tail k (rsubimm r1 r2 n k).
+Proof. unfold rsubimm; intros; IsTail. Qed.
+Hint Resolve rsubimm_tail: ppcretaddr.
+
+Lemma orimm_tail:
+  forall r1 r2 n k, is_tail k (orimm r1 r2 n k).
+Proof. unfold orimm; intros; IsTail. Qed.
+Hint Resolve orimm_tail: ppcretaddr.
+
+Lemma xorimm_tail:
+  forall r1 r2 n k, is_tail k (xorimm r1 r2 n k).
+Proof. unfold xorimm; intros; IsTail. Qed.
+Hint Resolve xorimm_tail: ppcretaddr.
 
 Lemma transl_cond_tail:
   forall cond args k, is_tail k (transl_cond cond args k).
@@ -189,11 +209,11 @@ Proof.
 Qed.
 
 Lemma return_address_exists:
-  forall f c, is_tail c f.(fn_code) ->
+  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
   intros. assert (is_tail (transl_code f c) (transl_function f)).
-  unfold transl_function. IsTail. apply transl_code_tail; auto.
+  unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib.
   destruct (is_tail_code_tail _ _ H0) as [ofs A].
   exists (Int.repr ofs). constructor. auto.
 Qed.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 3f98b88..25758cc 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -88,10 +88,10 @@ Ltac InvVLMA :=
   approximations returned by [eval_static_operation]. *)
 
 Lemma eval_static_condition_correct:
-  forall cond al vl b,
+  forall cond al vl m b,
   val_list_match_approx al vl ->
   eval_static_condition cond al = Some b ->
-  eval_condition cond vl = Some b.
+  eval_condition cond vl m = Some b.
 Proof.
   intros until b.
   unfold eval_static_condition. 
@@ -100,9 +100,9 @@ Proof.
 Qed.
 
 Lemma eval_static_operation_correct:
-  forall op sp al vl v,
+  forall op sp al vl m v,
   val_list_match_approx al vl ->
-  eval_operation ge sp op vl = Some v ->
+  eval_operation ge sp op vl m = Some v ->
   val_match_approx (eval_static_operation op al) v.
 Proof.
   intros until v.
@@ -144,7 +144,7 @@ Proof.
   inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto.
 
   caseEq (eval_static_condition c vl0).
-  intros. generalize (eval_static_condition_correct _ _ _ _ H H1).
+  intros. generalize (eval_static_condition_correct _ _ _ m _ H H1).
   intro. rewrite H2 in H0. 
   destruct b; injection H0; intro; subst v; simpl; auto.
   intros; simpl; auto.
@@ -168,6 +168,7 @@ Section STRENGTH_REDUCTION.
 Variable app: reg -> approx.
 Variable sp: val.
 Variable rs: regset.
+Variable m: mem.
 Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.
 
 Lemma intval_correct:
@@ -183,7 +184,7 @@ Qed.
 Lemma cond_strength_reduction_correct:
   forall cond args,
   let (cond', args') := cond_strength_reduction app cond args in
-  eval_condition cond' rs##args' = eval_condition cond rs##args.
+  eval_condition cond' rs##args' m = eval_condition cond rs##args m.
 Proof.
   intros. unfold cond_strength_reduction.
   case (cond_strength_reduction_match cond args); intros.
@@ -191,7 +192,6 @@ Proof.
   caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmp. auto.
-  destruct c; reflexivity.
   caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
@@ -199,6 +199,7 @@ Proof.
   caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto.
+  destruct c; reflexivity.
   caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
@@ -217,8 +218,8 @@ Qed.
 Lemma make_addimm_correct:
   forall n r v,
   let (op, args) := make_addimm n r in
-  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_addimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -230,8 +231,8 @@ Qed.
 Lemma make_shlimm_correct:
   forall n r v,
   let (op, args) := make_shlimm n r in
-  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_shlimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -244,8 +245,8 @@ Qed.
 Lemma make_shrimm_correct:
   forall n r v,
   let (op, args) := make_shrimm n r in
-  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_shrimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -258,8 +259,8 @@ Qed.
 Lemma make_shruimm_correct:
   forall n r v,
   let (op, args) := make_shruimm n r in
-  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_shruimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -273,8 +274,8 @@ Lemma make_mulimm_correct:
   forall n r r' v,
   rs#r' = Vint n ->
   let (op, args) := make_mulimm n r r' in
-  eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_mulimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -282,8 +283,8 @@ Proof.
   generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros.
   subst n. simpl in H2. simpl. FuncInv. rewrite Int.mul_one in H1. congruence.
   caseEq (Int.is_power2 n); intros.
-  replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil))
-     with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
+  replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) m)
+     with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m).
   apply make_shlimm_correct. 
   simpl. generalize (Int.is_power2_range _ _ H2). 
   change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3.
@@ -294,8 +295,8 @@ Qed.
 Lemma make_andimm_correct:
   forall n r v,
   let (op, args) := make_andimm n r in
-  eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_andimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -308,8 +309,8 @@ Qed.
 Lemma make_orimm_correct:
   forall n r v,
   let (op, args) := make_orimm n r in
-  eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_orimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -322,8 +323,8 @@ Qed.
 Lemma make_xorimm_correct:
   forall n r v,
   let (op, args) := make_xorimm n r in
-  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_xorimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -336,16 +337,16 @@ Qed.
 Lemma op_strength_reduction_correct:
   forall op args v,
   let (op', args') := op_strength_reduction app op args in
-  eval_operation ge sp op rs##args = Some v ->
-  eval_operation ge sp op' rs##args' = Some v.
+  eval_operation ge sp op rs##args m = Some v ->
+  eval_operation ge sp op' rs##args' m = Some v.
 Proof.
   intros; unfold op_strength_reduction;
   case (op_strength_reduction_match op args); intros; simpl List.map.
   (* Oadd *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m).
   apply make_addimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto.
   caseEq (intval app r2); intros.
@@ -354,8 +355,8 @@ Proof.
   (* Oaddshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_addimm_correct. 
   simpl. destruct rs#r1; auto.
   assumption.
@@ -365,16 +366,16 @@ Proof.
   simpl in *. destruct rs#r2; auto. 
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0).
-  replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)).
+  replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil) m).
   apply make_addimm_correct.
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
   assumption.
   (* Osubshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)).
+  replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil) m).
   apply make_addimm_correct. 
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
   assumption.
@@ -386,8 +387,8 @@ Proof.
   (* Omul *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m).
   apply make_mulimm_correct. apply intval_correct; auto. 
   simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
   caseEq (intval app r2); intros.
@@ -398,8 +399,8 @@ Proof.
   caseEq (intval app r2); intros.
   caseEq (Int.is_power2 i); intros.
   rewrite (intval_correct _ _ H).
-  replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)).
+  replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m).
   apply make_shruimm_correct. 
   simpl. destruct rs#r1; auto. 
   change 32 with (Z_of_nat Int.wordsize). 
@@ -412,8 +413,8 @@ Proof.
   (* Oand *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m).
   apply make_andimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto.
   caseEq (intval app r2); intros.
@@ -422,15 +423,15 @@ Proof.
   (* Oandshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Oor *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m).
   apply make_orimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto.
   caseEq (intval app r2); intros.
@@ -439,15 +440,15 @@ Proof.
   (* Oorshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_orimm_correct. reflexivity.
   assumption.
   (* Oxor *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m).
   apply make_xorimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto.
   caseEq (intval app r2); intros.
@@ -456,22 +457,22 @@ Proof.
   (* Oxorshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_xorimm_correct. reflexivity.
   assumption.
   (* Obic *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)).
+  replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil) m).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Obicshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)).
+  replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil) m).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Oshl *)
diff --git a/arm/Op.v b/arm/Op.v
index 0a3504e..bb688ce 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -32,6 +32,7 @@ Require Import Floats.
 Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
+Require Import Events.
 
 Set Implicit Arguments.
 
@@ -175,33 +176,36 @@ Definition eval_shift (s: shift) (n: int) : int :=
   | Sror x => Int.ror n (s_amount x)
   end.
 
-Definition eval_condition (cond: condition) (vl: list val):
+Definition eval_condition (cond: condition) (vl: list val) (m: mem):
                option bool :=
   match cond, vl with
   | Ccomp c, Vint n1 :: Vint n2 :: nil =>
       Some (Int.cmp c n1 n2)
-  | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
-      if eq_block b1 b2
-      then Some (Int.cmp c n1 n2)
-      else eval_compare_mismatch c
-  | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil =>
-      eval_compare_null c n2
-  | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil =>
-      eval_compare_null c n1
   | Ccompu c, Vint n1 :: Vint n2 :: nil =>
       Some (Int.cmpu c n1 n2)
+  | Ccompu c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
+      if Mem.valid_pointer m b1 (Int.unsigned n1)
+      && Mem.valid_pointer m b2 (Int.unsigned n2) then
+        if eq_block b1 b2
+        then Some (Int.cmpu c n1 n2)
+        else eval_compare_mismatch c
+      else None
+  | Ccompu c, Vptr b1 n1 :: Vint n2 :: nil =>
+      eval_compare_null c n2
+  | Ccompu c, Vint n1 :: Vptr b2 n2 :: nil =>
+      eval_compare_null c n1
   | Ccompshift c s, Vint n1 :: Vint n2 :: nil =>
       Some (Int.cmp c n1 (eval_shift s n2))
-  | Ccompshift c s, Vptr b1 n1 :: Vint n2 :: nil =>
-      eval_compare_null c (eval_shift s n2)
   | Ccompushift c s, Vint n1 :: Vint n2 :: nil =>
       Some (Int.cmpu c n1 (eval_shift s n2))
+  | Ccompushift c s, Vptr b1 n1 :: Vint n2 :: nil =>
+      eval_compare_null c (eval_shift s n2)
   | Ccompimm c n, Vint n1 :: nil =>
       Some (Int.cmp c n1 n)
-  | Ccompimm c n, Vptr b1 n1 :: nil =>
-      eval_compare_null c n
   | Ccompuimm c n, Vint n1 :: nil =>
       Some (Int.cmpu c n1 n)
+  | Ccompuimm c n, Vptr b1 n1 :: nil =>
+      eval_compare_null c n
   | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil =>
       Some (Float.cmp c f1 f2)
   | Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil =>
@@ -218,7 +222,7 @@ Definition offset_sp (sp: val) (delta: int) : option val :=
 
 Definition eval_operation
     (F V: Type) (genv: Genv.t F V) (sp: val)
-    (op: operation) (vl: list val): option val :=
+    (op: operation) (vl: list val) (m: mem): option val :=
   match op, vl with
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
@@ -285,7 +289,7 @@ Definition eval_operation
   | Ointoffloat, Vfloat f1 :: nil => option_map Vint (Float.intoffloat f1)
   | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1))
   | Ocmp c, _ =>
-      match eval_condition c vl with
+      match eval_condition c vl m with
       | None => None
       | Some false => Some Vfalse
       | Some true => Some Vtrue
@@ -346,24 +350,26 @@ Proof.
 Qed.
 
 Lemma eval_negate_condition:
-  forall (cond: condition) (vl: list val) (b: bool),
-  eval_condition cond vl = Some b ->
-  eval_condition (negate_condition cond) vl = Some (negb b).
+  forall (cond: condition) (vl: list val) (b: bool) (m: mem),
+  eval_condition cond vl m = Some b ->
+  eval_condition (negate_condition cond) vl m = Some (negb b).
 Proof.
   intros. 
   destruct cond; simpl in H; FuncInv; try subst b; simpl.
   rewrite Int.negate_cmp. auto.
+  rewrite Int.negate_cmpu. auto.
   apply eval_negate_compare_null; auto.
   apply eval_negate_compare_null; auto.
-  destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence.
+  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+           Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
+  destruct (eq_block b0 b1). rewrite Int.negate_cmpu. congruence.
   destruct c; simpl in H; inv H; auto.
-  rewrite Int.negate_cmpu. auto.
   rewrite Int.negate_cmp. auto.
-  apply eval_negate_compare_null; auto.
   rewrite Int.negate_cmpu. auto.
-  rewrite Int.negate_cmp. auto.
   apply eval_negate_compare_null; auto.
+  rewrite Int.negate_cmp. auto.
   rewrite Int.negate_cmpu. auto.
+  apply eval_negate_compare_null; auto.
   auto.
   rewrite negb_elim. auto.
 Qed.
@@ -382,8 +388,8 @@ Hypothesis agree_on_symbols:
   forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
 
 Lemma eval_operation_preserved:
-  forall sp op vl,
-  eval_operation ge2 sp op vl = eval_operation ge1 sp op vl.
+  forall sp op vl m,
+  eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
 Proof.
   intros.
   unfold eval_operation; destruct op; try rewrite agree_on_symbols;
@@ -518,9 +524,9 @@ Variable A V: Type.
 Variable genv: Genv.t A V.
 
 Lemma type_of_operation_sound:
-  forall op vl sp v,
+  forall op vl sp v m,
   op <> Omove ->
-  eval_operation genv sp op vl = Some v ->
+  eval_operation genv sp op vl m = Some v ->
   Val.has_type v (snd (type_of_operation op)).
 Proof.
   intros.
@@ -684,22 +690,24 @@ Proof.
 Qed.
 
 Lemma eval_condition_weaken:
-  forall c vl b,
-  eval_condition c vl = Some b ->
+  forall c vl b m,
+  eval_condition c vl m = Some b ->
   eval_condition_total c vl = Val.of_bool b.
 Proof.
   intros. 
   unfold eval_condition in H; destruct c; FuncInv;
   try subst b; try reflexivity; simpl;
   try (apply eval_compare_null_weaken; auto).
+  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+           Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
   unfold eq_block in H. destruct (zeq b0 b1); try congruence.
   apply eval_compare_mismatch_weaken; auto.
   symmetry. apply Val.notbool_negb_1. 
 Qed.
 
 Lemma eval_operation_weaken:
-  forall sp op vl v,
-  eval_operation genv sp op vl = Some v ->
+  forall sp op vl v m,
+  eval_operation genv sp op vl m = Some v ->
   eval_operation_total sp op vl = v.
 Proof.
   intros.
@@ -721,7 +729,7 @@ Proof.
   assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
   omega. discriminate.
   destruct (Float.intoffloat f); simpl in H; inv H. auto.
-  caseEq (eval_condition c vl); intros; rewrite H0 in H.
+  caseEq (eval_condition c vl m); intros; rewrite H0 in H.
   replace v with (Val.of_bool b).
   eapply eval_condition_weaken; eauto.
   destruct b; simpl; congruence.
@@ -783,12 +791,20 @@ Ltac InvLessdef :=
   end.
 
 Lemma eval_condition_lessdef:
-  forall cond vl1 vl2 b,
+  forall cond vl1 vl2 b m1 m2,
   Val.lessdef_list vl1 vl2 ->
-  eval_condition cond vl1 = Some b ->
-  eval_condition cond vl2 = Some b.
+  Mem.extends m1 m2 ->
+  eval_condition cond vl1 m1 = Some b ->
+  eval_condition cond vl2 m2 = Some b.
 Proof.
   intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto.
+  destruct (Mem.valid_pointer m1 b0 (Int.unsigned i) &&
+            Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate.
+  destruct (andb_prop _ _ Heqb2) as [A B].
+  assert (forall b ofs, Mem.valid_pointer m1 b ofs = true -> Mem.valid_pointer m2 b ofs = true).
+    intros until ofs. repeat rewrite Mem.valid_pointer_nonempty_perm. 
+    apply Mem.perm_extends; auto.
+  rewrite (H _ _ A). rewrite (H _ _ B). auto. 
 Qed.
 
 Ltac TrivialExists :=
@@ -799,34 +815,36 @@ Ltac TrivialExists :=
   end.
 
 Lemma eval_operation_lessdef:
-  forall sp op vl1 vl2 v1,
+  forall sp op vl1 vl2 v1 m1 m2,
   Val.lessdef_list vl1 vl2 ->
-  eval_operation genv sp op vl1 = Some v1 ->
-  exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v1 v2.
+  Mem.extends m1 m2 ->
+  eval_operation genv sp op vl1 m1 = Some v1 ->
+  exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
   intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists.
   exists v2; auto.
-  destruct (Genv.find_symbol genv i); inv H0. TrivialExists.
+  destruct (Genv.find_symbol genv i); inv H1. TrivialExists.
   exists v1; auto. 
   exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto.
   exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto.
   exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto.
   exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto.
-  destruct (eq_block b b0); inv H0. TrivialExists.
-  destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
-  destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
-  destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
-  destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
-  destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
+  destruct (eq_block b b0); inv H1. TrivialExists.
+  destruct (Int.eq i0 Int.zero); inv H1; TrivialExists.
+  destruct (Int.eq i0 Int.zero); inv H1; TrivialExists.
   destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
   destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
-  destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists.
+  destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists.
+  destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists.
+  destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists.
+  destruct (Int.ltu i (Int.repr 31)); inv H1; TrivialExists.
   exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
-  destruct (Float.intoffloat f); simpl in *; inv H0. TrivialExists.
-  caseEq (eval_condition c vl1); intros. rewrite H1 in H0. 
-  rewrite (eval_condition_lessdef c H H1).
-  destruct b; inv H0; TrivialExists.
-  rewrite H1 in H0. discriminate.
+  destruct (Float.intoffloat f); simpl in *; inv H1. TrivialExists.
+  exists v1; split; auto. 
+  destruct (eval_condition c vl1 m1) as [] _eqn. 
+  rewrite (eval_condition_lessdef c H H0 Heqo).
+  auto.
+  discriminate.
 Qed.
 
 Lemma eval_addressing_lessdef:
@@ -841,6 +859,154 @@ Qed.
 
 End EVAL_LESSDEF.
 
+(** Shifting stack-relative references.  This is used in [Stacking]. *)
+
+Definition shift_stack_addressing (delta: int) (addr: addressing) :=
+  match addr with
+  | Ainstack ofs => Ainstack (Int.add delta ofs)
+  | _ => addr
+  end.
+
+Definition shift_stack_operation (delta: int) (op: operation) :=
+  match op with
+  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
+  | _ => op
+  end.
+
+Lemma type_shift_stack_addressing:
+  forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
+Proof.
+  intros. destruct addr; auto. 
+Qed.
+
+Lemma type_shift_stack_operation:
+  forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
+Proof.
+  intros. destruct op; auto.
+Qed.
+
+(** Compatibility of the evaluation functions with memory injections. *)
+
+Section EVAL_INJECT.
+
+Variable F V: Type.
+Variable genv: Genv.t F V.
+Variable f: meminj.
+Hypothesis globals: meminj_preserves_globals genv f.
+Variable sp1: block.
+Variable sp2: block.
+Variable delta: Z.
+Hypothesis sp_inj: f sp1 = Some(sp2, delta).
+
+Ltac InvInject :=
+  match goal with
+  | [ H: val_inject _ (Vint _) _ |- _ ] =>
+      inv H; InvInject
+  | [ H: val_inject _ (Vfloat _) _ |- _ ] =>
+      inv H; InvInject
+  | [ H: val_inject _ (Vptr _ _) _ |- _ ] =>
+      inv H; InvInject
+  | [ H: val_list_inject _ nil _ |- _ ] =>
+      inv H; InvInject
+  | [ H: val_list_inject _ (_ :: _) _ |- _ ] =>
+      inv H; InvInject
+  | _ => idtac
+  end.
+
+Lemma eval_condition_inject:
+  forall cond vl1 vl2 b m1 m2,
+  val_list_inject f vl1 vl2 ->
+  Mem.inject f m1 m2 ->
+  eval_condition cond vl1 m1 = Some b ->
+  eval_condition cond vl2 m2 = Some b.
+Proof.
+  intros. destruct cond; simpl in *; FuncInv; InvInject; auto.
+  destruct (Mem.valid_pointer m1 b0 (Int.unsigned i)) as [] _eqn; try discriminate.
+  destruct (Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate.
+  simpl in H1.
+  exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. 
+  intros V1. rewrite V1.
+  exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb2. econstructor; eauto. 
+  intros V2. rewrite V2.
+  simpl. 
+  destruct (eq_block b0 b1); inv H1.
+  rewrite H3 in H5; inv H5. rewrite dec_eq_true.
+  decEq. apply Int.translate_cmpu.
+  eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  exploit Mem.different_pointers_inject; eauto. intros P.
+  destruct (eq_block b3 b4); auto.
+  destruct P. contradiction.
+  destruct c; unfold eval_compare_mismatch in *; inv H2. 
+  unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. 
+  unfold Int.cmpu. rewrite Int.eq_false; auto. congruence.
+Qed.
+
+Ltac TrivialExists2 :=
+  match goal with
+  | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] =>
+      exists v1; split; [auto | econstructor; eauto]
+  | _ => idtac
+  end.
+
+Lemma eval_addressing_inject:
+  forall addr vl1 vl2 v1,
+  val_list_inject f vl1 vl2 ->
+  eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
+  exists v2, 
+     eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
+  /\ val_inject f v1 v2.
+Proof.
+  assert (UNUSED: meminj_preserves_globals genv f). exact globals.
+  intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists2.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. 
+  repeat rewrite Int.add_assoc. auto.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. 
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+Qed.
+
+Lemma eval_operation_inject:
+  forall op vl1 vl2 v1 m1 m2,
+  val_list_inject f vl1 vl2 ->
+  Mem.inject f m1 m2 ->
+  eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
+  exists v2,
+     eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
+  /\ val_inject f v1 v2.
+Proof.
+  intros. destruct op; simpl in *; FuncInv; InvInject; TrivialExists2.
+  exists v'; auto.
+  destruct (Genv.find_symbol genv i) as [] _eqn; inv H1.
+  TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  exists (Val.sign_ext 8 v'); split; auto. inv H4; simpl; auto.
+  exists (Val.zero_ext 8 v'); split; auto. inv H4; simpl; auto.
+  exists (Val.sign_ext 16 v'); split; auto. inv H4; simpl; auto.
+  exists (Val.zero_ext 16 v'); split; auto. inv H4; simpl; auto.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  rewrite Int.sub_add_l. auto.
+  destruct (eq_block b b0); inv H1. rewrite H3 in H5; inv H5. rewrite dec_eq_true.
+  rewrite Int.sub_shifted. TrivialExists2.
+  rewrite Int.sub_add_l. auto.
+  destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2.
+  destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2.
+  destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
+  destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
+  destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
+  destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists2.
+  exists (Val.singleoffloat v'); split; auto. inv H4; simpl; auto.
+  destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists2.
+  destruct (eval_condition c vl1 m1) as [] _eqn; try discriminate.
+  exploit eval_condition_inject; eauto. intros EQ; rewrite EQ. 
+  destruct b; inv H1; TrivialExists2.
+Qed.
+
+End EVAL_INJECT.
+
 (** Recognition of integers that are valid shift amounts. *)
 
 Definition is_shift_amount_aux (n: int) :
@@ -891,10 +1057,10 @@ Definition op_for_binary_addressing (addr: addressing) : operation :=
   end.
 
 Lemma eval_op_for_binary_addressing:
-  forall (F V: Type) (ge: Genv.t F V) sp addr args v,
+  forall (F V: Type) (ge: Genv.t F V) sp addr args v m,
   (length args >= 2)%nat ->
   eval_addressing ge sp addr args = Some v ->
-  eval_operation ge sp (op_for_binary_addressing addr) args = Some v.
+  eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
 Proof.
   intros.
   unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl.
@@ -926,54 +1092,22 @@ Definition is_trivial_op (op: operation) : bool :=
   | _ => false
   end.
 
-(** Shifting stack-relative references.  This is used in [Stacking]. *)
 
-Definition shift_stack_addressing (delta: int) (addr: addressing) :=
-  match addr with
-  | Ainstack ofs => Ainstack (Int.add delta ofs)
-  | _ => addr
-  end.
+(** Operations that depend on the memory state. *)
 
-Definition shift_stack_operation (delta: int) (op: operation) :=
+Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
-  | _ => op
+  | Ocmp (Ccompu _) => true
+  | _ => false
   end.
 
-Lemma shift_stack_eval_addressing:
-  forall (F V: Type) (ge: Genv.t F V) sp addr args delta,
-  eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args =
-  eval_addressing ge sp addr args.
+Lemma op_depends_on_memory_correct:
+  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
+  op_depends_on_memory op = false ->
+  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros. destruct addr; simpl; auto. 
-  destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. 
-  decEq. decEq. rewrite <- Int.add_assoc. decEq. 
-  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
-  rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. 
-  rewrite Int.sub_idem. apply Int.add_zero. 
+  intros until m2. destruct op; simpl; try congruence.
+  destruct c; simpl; congruence.
 Qed.
 
-Lemma shift_stack_eval_operation:
-  forall (F V: Type) (ge: Genv.t F V) sp op args delta,
-  eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args =
-  eval_operation ge sp op args.
-Proof.
-  intros. destruct op; simpl; auto.
-  destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. 
-  decEq. decEq. rewrite <- Int.add_assoc. decEq. 
-  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
-  rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. 
-  rewrite Int.sub_idem. apply Int.add_zero. 
-Qed.
 
-Lemma type_shift_stack_addressing:
-  forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
-Proof.
-  intros. destruct addr; auto. 
-Qed.
-
-Lemma type_shift_stack_operation:
-  forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
-Proof.
-  intros. destruct op; auto.
-Qed.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 4f470ce..883ee72 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -453,30 +453,21 @@ let print_instruction oc labels = function
   | Psufd(r1, r2, r3) ->
       fprintf oc "	sufd	%a, %a, %a\n" freg r1 freg r2 freg r3; 1
   (* Pseudo-instructions *)
-  | Pallocframe(lo, hi, ofs) ->
-      let lo = camlint_of_coqint lo
-      and hi = camlint_of_coqint hi
-      and ofs = camlint_of_coqint ofs in
-      let sz = Int32.sub hi lo in
-      (* Keep stack 4-aligned *)
-      let sz4 = Int32.logand (Int32.add sz 3l) 0xFFFF_FFFCl in
-      (* FIXME: consider a store multiple? *)
-      (* R12 = first int temporary is unused at this point,
-         but this should be reflected in the proof *)
+  | Pallocframe(sz, ofs) ->
       fprintf oc "	mov	r12, sp\n";
       let ninstr = ref 0 in
       List.iter
-        (fun mask ->
-          let b = Int32.logand sz4 mask in
-          if b <> 0l then begin
-            fprintf oc "	sub	sp, sp, #%ld\n" b;
-            incr ninstr
-          end)
-        [0xFF000000l; 0x00FF0000l; 0x0000FF00l; 0x000000FFl];
-      fprintf oc "	str	r12, [sp, #%ld]\n" ofs;
+        (fun n ->
+           fprintf oc "	sub	sp, sp, #%a\n" coqint n;
+           incr ninstr)
+        (Asmgen.decompose_int sz);
+      fprintf oc "	str	r12, [sp, #%a]\n" coqint ofs;
       2 + !ninstr
-  | Pfreeframe(lo, hi, ofs) ->
-      fprintf oc "	ldr	sp, [sp, #%a]\n" coqint ofs; 1
+  | Pfreeframe(sz, ofs) ->
+      if Asmgen.is_immed_arith sz
+      then fprintf oc "	add	sp, sp, #%a\n" coqint sz
+      else fprintf oc "	ldr	sp, [sp, #%a]\n" coqint ofs;
+      1
   | Plabel lbl ->
       if Labelset.mem lbl labels then
         fprintf oc "%a:\n" print_label lbl; 0
diff --git a/arm/SelectOp.v b/arm/SelectOp.v
index df2413a..44528c6 100644
--- a/arm/SelectOp.v
+++ b/arm/SelectOp.v
@@ -146,7 +146,7 @@ Definition notint (e: expr) :=
 (** ** Boolean negation *)
 
 Definition notbool_base (e: expr) :=
-  Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil).
+  Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil).
 
 Fixpoint notbool (e: expr) {struct e} : expr :=
   match e with
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index cdb21cb..7602b11 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -64,13 +64,13 @@ Ltac InvEval1 :=
 
 Ltac InvEval2 :=
   match goal with
-  | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] =>
       simpl in H; inv H
-  | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] =>
       simpl in H; FuncInv
-  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] =>
       simpl in H; FuncInv
-  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] =>
       simpl in H; FuncInv
   | _ =>
       idtac
@@ -162,12 +162,12 @@ Proof.
   eapply eval_notbool_base; eauto.
 
   inv H. eapply eval_Eop; eauto.
-  simpl. assert (eval_condition c vl = Some b).
+  simpl. assert (eval_condition c vl m = Some b).
   generalize H6. simpl. 
   case (eval_condition c vl); intros.
   destruct b0; inv H1; inversion H0; auto; congruence.
   congruence.
-  rewrite (Op.eval_negate_condition _ _ H). 
+  rewrite (Op.eval_negate_condition _ _ _ H). 
   destruct b; reflexivity.
 
   inv H. eapply eval_Econdition; eauto. 
@@ -524,9 +524,9 @@ Qed.
 
 Lemma eval_mod_aux:
   forall divop semdivop,
-  (forall sp x y,
+  (forall sp x y m,
    y <> Int.zero ->
-   eval_operation ge sp divop (Vint x :: Vint y :: nil) =
+   eval_operation ge sp divop (Vint x :: Vint y :: nil) m =
    Some (Vint (semdivop x y))) ->
   forall le a b x y,
   eval_expr ge sp e m le a (Vint x) ->
@@ -757,7 +757,7 @@ Theorem eval_singleoffloat:
   eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v).
 Proof. TrivialOp singleoffloat. Qed. 
 
-Theorem eval_comp_int:
+Theorem eval_comp:
   forall le c a x b y,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vint y) ->
@@ -767,11 +767,26 @@ Proof.
   unfold comp; case (comp_match a b); intros; InvEval.
   EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity.
   EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
-  EvalOp. simpl. rewrite Int.swap_cmp. rewrite H. destruct (Int.cmp c x y); reflexivity.
+  EvalOp. simpl. rewrite H. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity.
   EvalOp. simpl. rewrite H0. destruct (Int.cmp c x y); reflexivity.
   EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
 Qed.
 
+Theorem eval_compu_int:
+  forall le c a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).
+Proof.
+  intros until y.
+  unfold compu; case (comp_match a b); intros; InvEval.
+  EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. rewrite Int.swap_cmpu. rewrite H. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+Qed.
+
 Remark eval_compare_null_trans:
   forall c x v,
   (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
@@ -786,15 +801,15 @@ Proof.
   destruct c; try discriminate; auto.
 Qed.
 
-Theorem eval_comp_ptr_int:
+Theorem eval_compu_ptr_int:
   forall le c a x1 x2 b y v,
   eval_expr ge sp e m le a (Vptr x1 x2) ->
   eval_expr ge sp e m le b (Vint y) ->
   (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
-  eval_expr ge sp e m le (comp c a b) v.
+  eval_expr ge sp e m le (compu c a b) v.
 Proof.
   intros until v.
-  unfold comp; case (comp_match a b); intros; InvEval.
+  unfold compu; case (comp_match a b); intros; InvEval.
   EvalOp. simpl. apply eval_compare_null_trans; auto. 
   EvalOp. simpl. rewrite H0. apply eval_compare_null_trans; auto. 
   EvalOp. simpl. apply eval_compare_null_trans; auto.
@@ -814,61 +829,49 @@ Proof.
   destruct c; simpl; try discriminate; auto.
 Qed.
 
-Theorem eval_comp_int_ptr:
+Theorem eval_compu_int_ptr:
   forall le c a x b y1 y2 v,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vptr y1 y2) ->
   (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
-  eval_expr ge sp e m le (comp c a b) v.
+  eval_expr ge sp e m le (compu c a b) v.
 Proof.
   intros until v.
-  unfold comp; case (comp_match a b); intros; InvEval.
+  unfold compu; case (comp_match a b); intros; InvEval.
   EvalOp. simpl. apply eval_swap_compare_null_trans; auto. 
   EvalOp. simpl. rewrite H. apply eval_swap_compare_null_trans; auto. 
   EvalOp. simpl. apply eval_compare_null_trans; auto.
 Qed.
 
-Theorem eval_comp_ptr_ptr:
+Theorem eval_compu_ptr_ptr:
   forall le c a x1 x2 b y1 y2,
   eval_expr ge sp e m le a (Vptr x1 x2) ->
   eval_expr ge sp e m le b (Vptr y1 y2) ->
+  Mem.valid_pointer m x1 (Int.unsigned x2)
+  && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
   x1 = y1 ->
-  eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)).
+  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)).
 Proof.
   intros until y2.
-  unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. subst y1. rewrite dec_eq_true. 
-  destruct (Int.cmp c x2 y2); reflexivity.
+  unfold compu; case (comp_match a b); intros; InvEval.
+  EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. 
+  destruct (Int.cmpu c x2 y2); reflexivity.
 Qed.
 
-Theorem eval_comp_ptr_ptr_2:
+Theorem eval_compu_ptr_ptr_2:
   forall le c a x1 x2 b y1 y2 v,
   eval_expr ge sp e m le a (Vptr x1 x2) ->
   eval_expr ge sp e m le b (Vptr y1 y2) ->
+  Mem.valid_pointer m x1 (Int.unsigned x2)
+  && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
   x1 <> y1 ->
   Cminor.eval_compare_mismatch c = Some v ->
-  eval_expr ge sp e m le (comp c a b) v.
+  eval_expr ge sp e m le (compu c a b) v.
 Proof.
   intros until y2.
-  unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite dec_eq_false; auto.
-  destruct c; simpl in H2; inv H2; auto.
-Qed.
-
-
-Theorem eval_compu:
-  forall le c a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).
-Proof.
-  intros until y.
   unfold compu; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. rewrite H. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto.
+  destruct c; simpl in H3; inv H3; auto.
 Qed.
 
 Theorem eval_compf:
diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v
index b374bfd..4521114 100644
--- a/arm/linux/Stacklayout.v
+++ b/arm/linux/Stacklayout.v
@@ -28,12 +28,6 @@ Require Import Bounds.
 - Pointer to activation record of the caller.
 - Space for the stack-allocated data declared in Cminor.
 
-To facilitate some of the proofs, the Cminor stack-allocated data
-starts at offset 0; the preceding areas in the activation record
-therefore have negative offsets.  This part (with negative offsets)
-is called the ``frame'', by opposition with the ``Cminor stack data''
-which is the part with positive offsets.
-
 The [frame_env] compilation environment records the positions of
 the boundaries between areas in the frame part.
 *)
@@ -49,7 +43,8 @@ Record frame_env : Type := mk_frame_env {
   fe_num_int_callee_save: Z;
   fe_ofs_float_local: Z;
   fe_ofs_float_callee_save: Z;
-  fe_num_float_callee_save: Z
+  fe_num_float_callee_save: Z;
+  fe_stack_data: Z
 }.
 
 (** Computation of the frame environment from the bounds of the current
@@ -63,17 +58,84 @@ Definition make_env (b: bounds) :=
   let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
   let ora := ofcs + 8 * b.(bound_float_callee_save) in (* retaddr *)
   let olink := ora + 4 in (* back link *)
-  let sz := olink + 4 in (* total frame size *)
+  let ostkdata := olink + 4 in (* stack data *)
+  let sz := align (ostkdata + b.(bound_stack_data)) 8 in
   mk_frame_env sz olink ora
                   oil oics b.(bound_int_callee_save)
-                  ofl ofcs b.(bound_float_callee_save).
+                  ofl ofcs b.(bound_float_callee_save)
+                  ostkdata.
 
+(** Separation property *)
 
-Remark align_float_part:
+Remark frame_env_separated:
   forall b,
-  4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <=
-  align (4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8.
+  let fe := make_env b in
+  0 <= fe_ofs_arg
+  /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local)
+  /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save)
+  /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local)
+  /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save)
+  /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_ofs_retaddr)
+  /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_ofs_link)
+  /\ fe.(fe_ofs_link) + 4 <= fe.(fe_stack_data)
+  /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size).
 Proof.
-  intros. apply align_le. omega.
+  intros.
+  generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)).
+  generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 8 (refl_equal _)).
+  unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
+    fe_ofs_int_local, fe_ofs_int_callee_save,
+    fe_num_int_callee_save,
+    fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
+    fe_stack_data, fe_ofs_arg.
+  intros.
+  generalize (bound_int_local_pos b); intro;
+  generalize (bound_float_local_pos b); intro;
+  generalize (bound_int_callee_save_pos b); intro;
+  generalize (bound_float_callee_save_pos b); intro;
+  generalize (bound_outgoing_pos b); intro;
+  generalize (bound_stack_data_pos b); intro.
+  omega.
 Qed.
 
+(** Alignment property *)
+
+Remark frame_env_aligned:
+  forall b,
+  let fe := make_env b in
+  (4 | fe.(fe_ofs_link))
+  /\ (4 | fe.(fe_ofs_int_local))
+  /\ (4 | fe.(fe_ofs_int_callee_save))
+  /\ (8 | fe.(fe_ofs_float_local))
+  /\ (8 | fe.(fe_ofs_float_callee_save))
+  /\ (4 | fe.(fe_ofs_retaddr))
+  /\ (4 | fe.(fe_stack_data))
+  /\ (8 | fe.(fe_size)).
+Proof.
+  intros.
+  unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
+    fe_ofs_int_local, fe_ofs_int_callee_save,
+    fe_num_int_callee_save,
+    fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
+    fe_stack_data.
+  set (x1 := 4 * bound_outgoing b).
+  assert (4 | x1). unfold x1; exists (bound_outgoing b); ring.
+  set (x2 := x1 + 4 * bound_int_local b).
+  assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring.
+  set (x3 := x2 + 4 * bound_int_callee_save b).
+  set (x4 := align x3 8).
+  assert (8 | x4). unfold x4. apply align_divides. omega.
+  set (x5 := x4 + 8 * bound_float_local b).
+  assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring.
+  set (x6 := x5 + 8 * bound_float_callee_save b).
+  assert (4 | x6).
+    apply Zdivides_trans with 8. exists 2; auto.
+    unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
+  set (x7 := x6 + 4).
+  assert (4 | x7). unfold x7; apply Zdivide_plus_r; auto. exists 1; auto.
+  set (x8 := x7 + 4).
+  assert (4 | x8). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto.
+  set (x9 := align (x8 + bound_stack_data b) 8).
+  assert (8 | x9). unfold x9; apply align_divides. omega.
+  tauto.
+Qed.