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

12 files changed, 536 insertions, 293 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index e49986f6..d698524d 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -130,7 +130,7 @@ Inductive instruction : Type :=
   | Paddi: ireg -> ireg -> constant -> instruction            (**r add immediate *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
   | Paddze: ireg -> ireg -> instruction                       (**r add Carry bit *)
-  | Pallocframe: Z -> Z -> int -> instruction                 (**r allocate new stack frame *)
+  | Pallocframe: Z -> int -> instruction                 (**r allocate new stack frame *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
   | Pandi_: ireg -> ireg -> constant -> instruction           (**r and immediate and set conditions *)
@@ -154,7 +154,7 @@ Inductive instruction : Type :=
   | Peqv: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-xor *)
   | Pextsb: ireg -> ireg -> instruction                       (**r 8-bit sign extension *)
   | Pextsh: ireg -> ireg -> instruction                       (**r 16-bit sign extension *)
-  | Pfreeframe: Z -> Z -> int -> instruction                  (**r deallocate stack frame and restore previous frame *)
+  | Pfreeframe: Z -> int -> instruction                  (**r deallocate stack frame and restore previous frame *)
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
@@ -249,19 +249,19 @@ lbl:    .double floatcst
         lfd     rdst, 0(r1)
         addi    r1, r1, 8
 >>
-- [Pallocframe lo hi ofs]: in the formal semantics, this pseudo-instruction
-  allocates a memory block with bounds [lo] and [hi], stores the value
+- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction
+  allocates a memory block with bounds [0] and [sz], stores the value
   of register [r1] (the stack pointer, by convention) at offset [ofs]
   in this block, and sets [r1] to a pointer to the bottom of this
   block.  In the printed PowerPC assembly code, this allocation
   is just a store-decrement of register [r1], assuming that [ofs = 0]:
 <<
-        stwu    r1, (lo - hi)(r1)
+        stwu    r1, -sz(r1)
 >>
   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 lo hi ofs]: in the formal semantics, this pseudo-instruction
+- [Pfreeframe sz ofs]: in the formal semantics, this pseudo-instruction
   reads the word at offset [ofs] in the block pointed by [r1] (the
   stack pointer), frees this block, and sets [r1] to the value of the
   word at offset [ofs].  In the printed PowerPC assembly code, this
@@ -527,9 +527,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m
   | Paddze rd r1 =>
       OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY))) m
-  | Pallocframe lo hi ofs =>
-      let (m1, stk) := Mem.alloc m lo hi in
-      let sp := Vptr stk (Int.repr lo) in
+  | Pallocframe sz ofs =>
+      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 ofs)) rs#GPR1 with
       | None => Error
       | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2
@@ -570,7 +570,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pbtbl r tbl =>
       match gpr_or_zero 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
@@ -599,13 +599,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m
   | Pextsh rd r1 =>
       OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m
-  | Pfreeframe lo hi ofs =>
+  | Pfreeframe sz ofs =>
       match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with
       | None => Error
       | Some v =>
           match rs#GPR1 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#GPR1 <- v)) m'
               end
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 9c37c42f..5e3d39b3 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -466,12 +466,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pmtctr (ireg_of r) :: 
       Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR0 ::
-      Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: 
+      Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
       Pbctr :: k
   | Mtailcall sig (inr symb) =>
       Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR0 ::
-      Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: 
+      Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
       Pbs symb :: k
   | Mbuiltin ef args res =>
       Pbuiltin ef (map preg_of args) (preg_of res) :: k
@@ -489,7 +489,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
   | Mreturn =>
       Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR0 ::
-      Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
+      Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
       Pblr :: k
   end.
 
@@ -502,7 +502,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) ::
   Pmflr GPR0 ::
   Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
   transl_code f f.(fn_code).
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 54e454e8..83193638 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -750,12 +750,12 @@ Proof.
 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.
@@ -792,7 +792,7 @@ 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.
@@ -800,7 +800,7 @@ Proof.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI.
   left; eapply exec_straight_steps; eauto with coqlib.
-  simpl. eapply transl_op_correct; auto.
+  simpl. eapply transl_op_correct; eauto.
   rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
 Qed.
 
@@ -810,8 +810,8 @@ Remark loadv_8_signed_unsigned:
   exists v', Mem.loadv Mint8unsigned m a = Some v' /\ v = Val.sign_ext 8 v'.
 Proof.
   unfold Mem.loadv; intros. destruct a; try congruence.
-  generalize (Mem.load_int8_signed_unsigned m b (Int.signed i)).
-  rewrite H. destruct (Mem.load Mint8unsigned m b (Int.signed i)).
+  generalize (Mem.load_int8_signed_unsigned m b (Int.unsigned i)).
+  rewrite H. destruct (Mem.load Mint8unsigned m b (Int.unsigned i)).
   simpl; intros. exists v0; split; congruence.
   simpl; congruence.
 Qed.
@@ -987,7 +987,7 @@ Lemma exec_Mtailcall_prop:
   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' ->
+  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').
@@ -1155,7 +1155,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
@@ -1168,8 +1168,7 @@ Proof.
          if snd (crbit_for_cond cond)
          then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c
          else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c).
-  generalize (transl_cond_correct tge (transl_function f)
-                cond args k1 ms sp rs m' true H3 AG H).
+  exploit transl_cond_correct; eauto. 
   simpl. intros [rs2 [EX [RES AG2]]].
   inv AT. simpl in H5.
   generalize (functions_transl _ _ H4); intro FN.
@@ -1198,29 +1197,22 @@ 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. inversion WTI.
-  pose (k1 := 
-         if snd (crbit_for_cond cond)
-         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c
-         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c).
-  generalize (transl_cond_correct tge (transl_function f)
-                cond args k1 ms sp rs m' false H1 AG H).
+  exploit transl_cond_correct; eauto.
   simpl. intros [rs2 [EX [RES AG2]]].
   left; eapply exec_straight_steps; eauto with coqlib.
   exists (nextinstr rs2); split.
   simpl. eapply exec_straight_trans. eexact EX. 
   caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES.
-  unfold k1; rewrite ISSET; apply exec_straight_one. 
-  simpl. rewrite RES. reflexivity.
+  apply exec_straight_one. simpl. rewrite RES. reflexivity.
   reflexivity.
-  unfold k1; rewrite ISSET; apply exec_straight_one. 
-  simpl. rewrite RES. reflexivity.
+  apply exec_straight_one. simpl. rewrite RES. reflexivity.
   reflexivity.
   auto with ppcgen.
 Qed.
@@ -1231,7 +1223,7 @@ Lemma exec_Mjumptable_prop:
          (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
          (c' : Mach.code),
   rs 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
@@ -1243,13 +1235,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.rolm n (Int.repr 2) (Int.repr (-4))) = Int.signed n * 4).
+  assert (SHIFT: Int.unsigned (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.unsigned n * 4).
     replace (Int.repr (-4)) with (Int.shl Int.mone (Int.repr 2)).
     rewrite <- Int.shl_rolm. rewrite Int.shl_mul.
-    rewrite Int.mul_signed.
-    apply Int.signed_repr.
-    split. apply Zle_trans with 0. compute; congruence. omega. 
-    omega.
+    unfold Int.mul. apply Int.unsigned_repr. omega.
     compute. reflexivity.
     apply Int.mkint_eq. compute. reflexivity.
   inv AT. simpl in H7. 
@@ -1274,11 +1263,10 @@ Proof.
   eapply exec_straight_steps_1; eauto.
   econstructor; eauto. 
   eapply find_instr_tail. unfold k1 in CT1. eauto.
-  unfold exec_instr.
+  unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen.  
   change (rs1 GPR12) with (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))).
-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.
@@ -1295,7 +1283,7 @@ Lemma exec_Mreturn_prop:
   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' ->
+  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.
@@ -1356,12 +1344,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).
@@ -1405,7 +1393,7 @@ Proof.
   assert (AG2: agree ms sp rs2).
     split. reflexivity. unfold sp. congruence. 
     intros. unfold rs2. rewrite nextinstr_inv. 
-    repeat (rewrite Pregmap.gso). elim AG; auto.
+    repeat (rewrite Pregmap.gso). inv AG; auto.
     auto with ppcgen. auto with ppcgen. auto with ppcgen.
   assert (AG4: agree ms sp rs4).
     unfold rs4, rs3; auto with ppcgen.
@@ -1414,7 +1402,7 @@ Proof.
   eapply exec_straight_steps_1; eauto.
   change (Int.unsigned Int.zero) with 0. constructor.
   (* match states *)
-  econstructor; eauto with coqlib.
+  econstructor; eauto with coqlib. auto with ppcgen.
 Qed.
 
 Lemma exec_function_external_prop:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index d428543c..16dd923e 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1110,12 +1110,13 @@ Proof.
 Qed.
 
 Lemma transl_cond_correct:
-  forall cond args k ms sp rs m b,
+  forall cond args k ms sp rs m m' b,
   map mreg_type args = type_of_condition cond ->
   agree ms sp rs ->
-  eval_condition cond (map ms args) = Some b ->
+  eval_condition cond (map ms args) m = Some b ->
+  Mem.extends m m' ->
   exists rs',
-     exec_straight (transl_cond cond args k) rs m k rs' m
+     exec_straight (transl_cond cond args k) rs m' k rs' m'
   /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
        (if snd (crbit_for_cond cond)
         then Val.of_bool b
@@ -1124,9 +1125,9 @@ Lemma transl_cond_correct:
 Proof.
   intros.
   assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b).
-    apply eval_condition_weaken. eapply eval_condition_lessdef; eauto. 
+    apply eval_condition_weaken with m'. eapply eval_condition_lessdef; eauto. 
     eapply preg_vals; eauto.
-  rewrite <- H2. eapply transl_cond_correct_aux; eauto.
+  rewrite <- H3. eapply transl_cond_correct_aux; eauto.
 Qed.
 
 (** Translation of arithmetic operations. *)
@@ -1155,21 +1156,22 @@ Ltac TranslOpSimpl :=
 *)
 
 Lemma transl_op_correct:
-  forall op args res k ms sp rs m v,
+  forall op args res k ms sp rs m v m',
   wt_instr (Mop op args res) ->
   agree ms sp rs ->
-  eval_operation ge sp op (map ms args) = Some v ->
+  eval_operation ge sp op (map ms args) m = Some v ->
+  Mem.extends m m' ->
   exists rs',
-    exec_straight (transl_op op args res k) rs m k rs' m
+    exec_straight (transl_op op args res k) rs m' k rs' m'
   /\ agree (Regmap.set res v (undef_op op ms)) sp rs'.
 Proof.
   intros.
   assert (exists v', Val.lessdef v v' /\
           eval_operation_total ge sp op (map rs (map preg_of args)) = v').
-    exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. 
+    exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto.
     intros [v' [A B]]. exists v'; split; auto.
-    apply eval_operation_weaken; eauto. 
-  destruct H2 as [v' [LD EQ]]. clear H1.
+    eapply eval_operation_weaken; eauto. 
+  destruct H3 as [v' [LD EQ]]. clear H1 H2.
   inv H.
   (* Omove *)
   simpl in *. 
@@ -1183,7 +1185,7 @@ Proof.
   (* Omove again *)
   congruence.
   (* Ointconst *)
-  destruct (loadimm_correct (ireg_of res) i k rs m)
+  destruct (loadimm_correct (ireg_of res) i k rs m')
   as [rs' [A [B C]]]. 
   exists rs'. split. auto. 
   rewrite <- B in LD. eauto with ppcgen. 
@@ -1198,7 +1200,7 @@ Proof.
   set (v' := symbol_offset ge i i0) in *.
   pose (rs1 := nextinstr (rs#GPR12 <- (high_half v'))).
   exists (nextinstr (rs1#(ireg_of res) <- v')).
-  split. apply exec_straight_two with rs1 m.
+  split. apply exec_straight_two with rs1 m'.
   unfold exec_instr. rewrite gpr_or_zero_zero.
   unfold const_high. rewrite Val.add_commut. 
   rewrite high_half_zero. reflexivity. 
@@ -1213,7 +1215,7 @@ Proof.
   intros. apply Pregmap.gso; auto.
   (* Oaddrstack *)
   assert (GPR1 <> GPR0). discriminate.
-  generalize (addimm_correct (ireg_of res) GPR1 i k rs m (ireg_of_not_GPR0 res) H1). 
+  generalize (addimm_correct (ireg_of res) GPR1 i k rs m' (ireg_of_not_GPR0 res) H1). 
   intros [rs' [EX [RES OTH]]].
   exists rs'. split. auto. 
   apply agree_set_mireg_exten with rs; auto with ppcgen.
@@ -1235,7 +1237,7 @@ Proof.
   unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto.
   rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
   (* Oaddimm *)
-  generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m
+  generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m'
                             (ireg_of_not_GPR0 res) (ireg_of_not_GPR0 m0)).
   intros [rs' [A [B C]]]. 
   exists rs'. split. auto.
@@ -1245,7 +1247,7 @@ Proof.
   econstructor; split.
   apply exec_straight_one. simpl; eauto. auto.
   auto 7 with ppcgen.
-  generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m).
+  generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m').
   intros [rs1 [EX [RES OTH]]].
   econstructor; split.
   eapply exec_straight_trans. eexact EX. 
@@ -1258,7 +1260,7 @@ Proof.
   econstructor; split.
   apply exec_straight_one. simpl; eauto. auto. 
   auto with ppcgen.
-  generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m).
+  generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m').
   intros [rs1 [EX [RES OTH]]].
   assert (agree (undef_temps ms) sp rs1). eauto with ppcgen.
   econstructor; split.
@@ -1275,22 +1277,22 @@ Proof.
   apply agree_exten_2 with rs1. unfold rs1; auto with ppcgen.
   auto.
   (* Oandimm *)
-  generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
+  generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m'
                              (ireg_of_not_GPR0 m0)).
   intros [rs' [A [B [C D]]]]. 
   exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen.
   (* Oorimm *)
-  generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m).
+  generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m').
   intros [rs' [A [B C]]]. 
   exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. 
   (* Oxorimm *)
-  generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m).
+  generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m').
   intros [rs' [A [B C]]]. 
   exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen.
   (* Oxhrximm *)
   pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (rs (ireg_of m0)) (Vint i)) #CARRY <- (Val.shr_carry (rs (ireg_of m0)) (Vint i)))).
   exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (rs (ireg_of m0)) (Vint i)))).
-  split. apply exec_straight_two with rs1 m.
+  split. apply exec_straight_two with rs1 m'.
   auto. simpl. decEq. decEq. decEq. 
   unfold rs1. repeat (rewrite nextinstr_inv; try discriminate).
   rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. 
@@ -1312,7 +1314,7 @@ Proof.
   set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))).
   set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.xor (rs1#(ireg_of res)) (Vint Int.one)))).
   exists rs2.
-  split. apply exec_straight_two with rs1 m; auto.
+  split. apply exec_straight_two with rs1 m'; auto.
   rewrite <- Val.rolm_ge_zero in LD.
   unfold rs2. apply agree_nextinstr.
   unfold rs1. apply agree_nextinstr_commut. fold rs1.
@@ -1334,19 +1336,19 @@ Proof.
         (if isset
          then k
          else Pxori (ireg_of res) (ireg_of res) (Cint Int.one) :: k)).
-  generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m H1 H0).
+  generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m' H1 H0).
   fold bit; fold isset. 
   intros [rs1 [EX1 [RES1 AG1]]].
   set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#(reg_of_crbit bit)))).
   destruct isset.
   exists rs2.
-  split. apply exec_straight_trans with k1 rs1 m. assumption.
+  split. apply exec_straight_trans with k1 rs1 m'. assumption.
   unfold k1. apply exec_straight_one. 
   reflexivity. reflexivity. 
   unfold rs2. rewrite RES1. auto with ppcgen. 
   econstructor. 
-  split. apply exec_straight_trans with k1 rs1 m. assumption.
-  unfold k1. apply exec_straight_two with rs2 m.
+  split. apply exec_straight_trans with k1 rs1 m'. assumption.
+  unfold k1. apply exec_straight_two with rs2 m'.
   reflexivity. simpl. eauto. auto. auto. 
   apply agree_nextinstr. 
   unfold rs2 at 1. rewrite nextinstr_inv. rewrite Pregmap.gss. 
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v
index ae3c2bdb..a15bf736 100644
--- a/powerpc/Asmgenretaddr.v
+++ b/powerpc/Asmgenretaddr.v
@@ -179,11 +179,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/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index ac15c0d3..bf065b78 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/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.
@@ -150,7 +150,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.
@@ -174,6 +174,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:
@@ -189,20 +190,20 @@ 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.
   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.
   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.
@@ -212,8 +213,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.
@@ -225,8 +226,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.
@@ -239,8 +240,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.
@@ -251,8 +252,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.
@@ -265,8 +266,8 @@ Qed.
 Lemma make_mulimm_correct:
   forall n r v,
   let (op, args) := make_mulimm n 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.
@@ -274,8 +275,8 @@ Proof.
   generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros.
   subst n. simpl in H1. simpl. FuncInv. rewrite Int.mul_one in H0. 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 _ _ H1). 
   change (Z_of_nat Int.wordsize) with 32. intro. rewrite H2.
@@ -286,8 +287,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.
@@ -300,8 +301,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.
@@ -314,8 +315,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.
@@ -326,16 +327,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.
@@ -346,16 +347,16 @@ Proof.
   rewrite (intval_correct _ _ H) in H0. assumption. 
   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.
   (* 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. 
   simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
   caseEq (intval app r2); intros.
@@ -375,8 +376,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). 
@@ -389,8 +390,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.
@@ -399,8 +400,8 @@ Proof.
   (* 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.
@@ -409,8 +410,8 @@ Proof.
   (* 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.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 6f05e550..d4669613 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -32,6 +32,7 @@ Require Import Values.
 Require Import Memdata.
 Require Import Memory.
 Require Import Globalenvs.
+Require Import Events.
 
 Set Implicit Arguments.
 
@@ -141,27 +142,30 @@ Definition eval_compare_mismatch (c: comparison) : option bool :=
 Definition eval_compare_null (c: comparison) (n: int) : option bool :=
   if Int.eq n Int.zero then eval_compare_mismatch c else None.
 
-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
   | 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 =>
@@ -182,7 +186,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)
@@ -251,7 +255,7 @@ Definition eval_operation
   | Ofloatofwords, Vint i1 :: Vint i2 :: nil =>
       Some (Vfloat (Float.from_words i1 i2))
   | 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
@@ -327,21 +331,23 @@ 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 vl m b,
+  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 congruence.
+  destruct (eq_block b0 b1). rewrite Int.negate_cmpu. congruence.
   apply eval_negate_compare_mismatch; auto. 
-  rewrite Int.negate_cmpu. auto.
   rewrite Int.negate_cmp. auto.
-  apply eval_negate_compare_null; auto.
   rewrite Int.negate_cmpu. auto.
+  apply eval_negate_compare_null; auto.
   auto.
   rewrite negb_elim. auto.
   auto.
@@ -362,8 +368,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;
@@ -483,9 +489,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.
@@ -643,14 +649,16 @@ 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 congruence.
   unfold eq_block in H. destruct (zeq b0 b1).
   congruence.
   apply eval_compare_mismatch_weaken; auto.
@@ -659,8 +667,8 @@ Proof.
 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.
@@ -680,7 +688,7 @@ Proof.
   destruct (Int.ltu i Int.iwordsize); congruence.
   destruct (Int.ltu i0 Int.iwordsize); congruence.
   destruct (Float.intoffloat f); 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.
@@ -746,12 +754,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 :=
@@ -762,33 +778,34 @@ 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 (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
-  destruct (Int.ltu i0 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.iwordsize); inv H1; TrivialExists.
+  destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists.
+  destruct (Int.ltu i0 Int.iwordsize); 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.
+  caseEq (eval_condition c vl1 m1); intros. rewrite H2 in H1. 
+  rewrite (eval_condition_lessdef c H H0 H2).
+  destruct b; inv H1; TrivialExists.
+  rewrite H2 in H1. discriminate.
 Qed.
 
 Lemma eval_addressing_lessdef:
@@ -805,6 +822,159 @@ 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.
+  intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists2.
+  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.
+  destruct (Genv.find_symbol genv i) as [] _eqn; inv H0.
+  TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto.
+  destruct (Genv.find_symbol genv i) as [] _eqn; inv H0.
+  TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto.
+  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.
+  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.
+  destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2.
+  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 H2. TrivialExists2.
+  destruct (Int.ltu i0 Int.iwordsize); inv H2. TrivialExists2.
+  destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
+  destruct (Int.ltu i Int.iwordsize); inv H1. TrivialExists2.
+  destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists2.
+  destruct (Int.ltu i Int.iwordsize); inv H2. TrivialExists2.
+  destruct (Int.ltu i Int.iwordsize); inv H2. TrivialExists2.
+  destruct (Int.ltu i0 Int.iwordsize); 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.
+
 (** Transformation of addressing modes with two operands or more
   into an equivalent arithmetic operation.  This is used in the [Reload]
   pass when a store instruction cannot be reloaded directly because
@@ -816,10 +986,10 @@ End EVAL_LESSDEF.
 Definition op_for_binary_addressing (addr: addressing) : operation := Oadd.
 
 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;
@@ -849,57 +1019,20 @@ 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.
-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. 
-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.
+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 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. 
+  intros until m2. destruct op; simpl; try congruence.
+  destruct c; simpl; congruence.
 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/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 60741975..c0f9294e 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -433,14 +433,11 @@ let print_instruction oc labels = function
       fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
   | Paddze(r1, r2) ->
       fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
-  | Pallocframe(lo, hi, ofs) ->
-      let lo = camlint_of_coqint lo
-      and hi = camlint_of_coqint hi
+  | Pallocframe(sz, ofs) ->
+      let sz = camlint_of_coqint sz
       and ofs = camlint_of_coqint ofs in
-      let sz = Int32.sub hi lo in
       assert (ofs = 0l);
-      (* Keep stack 16-aligned *)
-      let adj = Int32.neg (Int32.logand (Int32.add sz 15l) 0xFFFF_FFF0l) in
+      let adj = Int32.neg sz in
       if adj >= -0x8000l then
         fprintf oc "	stwu	%a, %ld(%a)\n" ireg GPR1 adj ireg GPR1
       else begin
@@ -509,8 +506,8 @@ let print_instruction oc labels = function
       fprintf oc "	extsb	%a, %a\n" ireg r1 ireg r2
   | Pextsh(r1, r2) ->
       fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
-  | Pfreeframe(lo, hi, ofs) ->
-      (* Note: could also do an add on GPR1 using lo and hi *)
+  | Pfreeframe(sz, ofs) ->
+      (* Note: could also do an add on GPR1 using sz *)
       fprintf oc "	lwz	%a, %ld(%a)\n" ireg GPR1  (camlint_of_coqint ofs)  ireg GPR1
   | Pfabs(r1, r2) ->
       fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index c421cdc5..b735fad0 100644
--- a/powerpc/SelectOp.v
+++ b/powerpc/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/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 1f2c7362..6d1e3c5c 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/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
@@ -167,12 +167,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.
+  case (eval_condition c vl m); 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. 
@@ -542,9 +542,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) ->
@@ -715,7 +715,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) ->
@@ -728,6 +728,19 @@ Proof.
   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. destruct (Int.cmpu c x y); reflexivity.
+Qed.
+
 Remark eval_compare_null_transf:
   forall c x v,
   Cminor.eval_compare_null c x = Some v ->
@@ -742,15 +755,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) ->
   Cminor.eval_compare_null c y = 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_transf; auto.
   EvalOp. simpl. apply eval_compare_null_transf; auto.
 Qed.
@@ -764,58 +777,49 @@ Proof.
   destruct (Int.eq x Int.zero). destruct c; auto. 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) ->
   Cminor.eval_compare_null c x = 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_transf. 
   rewrite eval_compare_null_swap; auto.
   EvalOp. simpl. apply eval_compare_null_transf. 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. 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/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v
index 0de1ccd6..22a28269 100644
--- a/powerpc/eabi/Stacklayout.v
+++ b/powerpc/eabi/Stacklayout.v
@@ -33,12 +33,6 @@ Require Import Bounds.
 - Saved values of float callee-save registers used by the function.
 - 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.
 *)
@@ -54,7 +48,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
@@ -67,17 +62,81 @@ Definition make_env (b: bounds) :=
   let oendi := oics + 4 * b.(bound_int_callee_save) in
   let ofl := align oendi 8 in       (* float locals *)
   let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
-  let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *)
+  let ostkdata := ofcs + 8 * b.(bound_float_callee_save) in (* stack data *)
+  let sz := align (ostkdata + b.(bound_stack_data)) 16 in
   mk_frame_env sz 0 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,
-  8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b <=
-  align (8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b) 8.
+  let fe := make_env b in
+  0 <= fe.(fe_ofs_link)
+  /\ fe.(fe_ofs_link) + 4 <= 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_retaddr)
+  /\ fe.(fe_ofs_retaddr) + 4 <= 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_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)) 16 (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))
+  /\ (16 | 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 := 8 + 4 * bound_outgoing b).
+  assert (4 | x1). unfold x1; apply Zdivide_plus_r. exists 2; auto. 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).
+  assert (4 | x3). unfold x3; apply Zdivide_plus_r; auto. exists 1; auto.
+  set (x4 := align (x3 + 4 * bound_int_callee_save b) 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 := align (x6 + bound_stack_data b) 16).
+  assert (16 | x7). unfold x7; apply align_divides. omega.
+  intuition.
+Qed.
diff --git a/powerpc/macosx/Stacklayout.v b/powerpc/macosx/Stacklayout.v
index c57f3f92..57592a8c 100644
--- a/powerpc/macosx/Stacklayout.v
+++ b/powerpc/macosx/Stacklayout.v
@@ -30,12 +30,6 @@ Require Import Bounds.
 - Saved values of float callee-save registers used by the function.
 - 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.
 *)
@@ -51,7 +45,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,81 @@ Definition make_env (b: bounds) :=
   let oendi := oics + 4 * b.(bound_int_callee_save) in
   let ofl := align oendi 8 in       (* float locals *)
   let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
-  let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *)
+  let ostkdata := ofcs + 8 * b.(bound_float_callee_save) in (* stack data *)
+  let sz := align (ostkdata + b.(bound_stack_data)) 16 in
   mk_frame_env sz 0 12
                   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,
-  24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <=
-  align (24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8.
+  let fe := make_env b in
+  0 <= fe.(fe_ofs_link)
+  /\ fe.(fe_ofs_link) + 4 <= fe.(fe_ofs_retaddr)
+  /\ fe.(fe_ofs_retaddr) + 4 <= 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_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)) 16 (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))
+  /\ (16 | 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 := 24 + 4 * bound_outgoing b).
+  assert (4 | x1). unfold x1; apply Zdivide_plus_r. exists 6; auto. 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 := align (x6 + bound_stack_data b) 16).
+  assert (16 | x7). unfold x7; apply align_divides. omega.
+  intuition.
+  exists 3; auto.
+Qed.