- Added alignment constraints to memory loads and stores.

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


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

11 files changed, 162 insertions, 367 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index b4490af..69085aa 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -100,7 +100,6 @@ Inductive instruction : Set :=
   | 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 *)
-  | Pallocblock: instruction                                  (**r allocate new heap block *)
   | Pallocframe: Z -> 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 *)
@@ -293,11 +292,6 @@ lbl:    .long   0x43300000, 0x00000000
 >>
   Again, our memory model cannot comprehend that this operation
   frees (logically) the current stack frame.
-- [Pallocheap]: in the formal semantics, this pseudo-instruction
-  allocates a heap block of size the contents of [GPR3], and leaves
-  a pointer to this block in [GPR3].  In the generated assembly code,
-  it is turned into a call to the allocation function of the run-time
-  system.
 *)
 
 Definition code := list instruction.
@@ -554,14 +548,6 @@ 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
-  | Pallocblock =>
-      match rs#GPR3 with
-      | Vint n =>
-          let (m', b) := Mem.alloc m 0 (Int.signed n) in
-          OK (nextinstr (rs#GPR3 <- (Vptr b Int.zero)
-                           #LR <- (Val.add rs#PC Vone))) m'
-      | _ => Error
-      end
   | Pallocframe lo hi ofs =>
       let (m1, stk) := Mem.alloc m lo hi in
       let sp := Vptr stk (Int.repr lo) in
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 2ddaa6d..1dcc399 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -457,8 +457,6 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pmtlr GPR12 ::
       Pfreeframe f.(fn_link_ofs) :: 
       Pbs symb :: k
-  | Malloc =>
-      Pallocblock :: k
   | Mlabel lbl =>
       Plabel lbl :: k
   | Mgoto lbl =>
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 980925b..a96125a 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -537,68 +537,6 @@ Proof.
   intros. apply Pregmap.gso; auto.
 Qed.
 
-(** * Memory properties *)
-
-(** The PowerPC has no instruction for ``load 8-bit signed integer''.
-  We show that it can be synthesized as a ``load 8-bit unsigned integer''
-  followed by a sign extension. *)
-
-Remark valid_access_equiv:
-  forall chunk1 chunk2 m b ofs,
-  size_chunk chunk1 = size_chunk chunk2 ->
-  valid_access m chunk1 b ofs ->
-  valid_access m chunk2 b ofs.
-Proof.
-  intros. inv H0. rewrite H in H3. constructor; auto.
-Qed.
-
-Remark in_bounds_equiv:
-  forall chunk1 chunk2 m b ofs (A: Set) (a1 a2: A),
-  size_chunk chunk1 = size_chunk chunk2 ->
-  (if in_bounds m chunk1 b ofs then a1 else a2) =
-  (if in_bounds m chunk2 b ofs then a1 else a2).
-Proof.
-  intros. destruct (in_bounds m chunk1 b ofs).
-  rewrite in_bounds_true. auto. eapply valid_access_equiv; eauto.
-  destruct (in_bounds m chunk2 b ofs); auto.
-  elim n. eapply valid_access_equiv with (chunk1 := chunk2); eauto.
-Qed.
-
-Lemma loadv_8_signed_unsigned:
-  forall m a,
-  Mem.loadv Mint8signed m a = 
-    option_map (Val.sign_ext 8) (Mem.loadv Mint8unsigned m a).
-Proof.
-  intros. unfold Mem.loadv. destruct a; try reflexivity.
-  unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned).
-  destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto.
-  simpl.
-  destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto.
-  simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto. 
-  auto.
-Qed.
-
-(** Similarly, we show that signed 8- and 16-bit stores can be performed
-  like unsigned stores. *)
-
-Lemma storev_8_signed_unsigned:
-  forall m a v,
-  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
-Proof.
-  intros. unfold storev. destruct a; auto.
-  unfold store. rewrite (in_bounds_equiv Mint8signed Mint8unsigned).
-  auto. auto.
-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 storev. destruct a; auto.
-  unfold store. rewrite (in_bounds_equiv Mint16signed Mint16unsigned).
-  auto. auto.
-Qed.
-
 (** * Proof of semantic preservation *)
 
 (** Semantic preservation is proved using simulation diagrams
@@ -805,7 +743,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 m = Some v ->
+  eval_operation ge sp op ms ## args = 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 ms) m).
 Proof.
@@ -1069,21 +1007,6 @@ Proof.
   unfold rs5; auto with ppcgen.
 Qed.
 
-Lemma exec_Malloc_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (sz : int)
-         (m' : mem) (blk : block),
-  ms Conventions.loc_alloc_argument = Vint sz ->
-  alloc m 0 (Int.signed sz) = (m', blk) ->
-  exec_instr_prop (Machconcr.State s fb sp (Malloc :: c) ms m) E0
-         (Machconcr.State s fb sp c
-             (Regmap.set (Conventions.loc_alloc_result) (Vptr blk Int.zero) ms) m').
-Proof.
-  intros; red; intros; inv MS.
-  left; eapply exec_straight_steps; eauto with coqlib.
-  simpl. eapply transl_alloc_correct; eauto. 
-Qed.
-
 Lemma exec_Mgoto_prop:
   forall (s : list stackframe) (fb : block) (f : function) (sp : val)
          (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
@@ -1113,7 +1036,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 m = Some true ->
+  eval_condition cond ms ## args = 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
@@ -1156,7 +1079,7 @@ 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 m = Some false ->
+  eval_condition cond ms ## args = Some false ->
   exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
                   (Machconcr.State s fb sp c ms m).
 Proof.
@@ -1345,7 +1268,6 @@ Proof
            exec_Mstore_prop
            exec_Mcall_prop
            exec_Mtailcall_prop
-           exec_Malloc_prop
            exec_Mgoto_prop
            exec_Mcond_true_prop
            exec_Mcond_false_prop
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index c17cb73..fdb48be 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1122,7 +1122,7 @@ Lemma transl_cond_correct:
   forall cond args k ms sp rs m b,
   map mreg_type args = type_of_condition cond ->
   agree ms sp rs ->
-  eval_condition cond (map ms args) m = Some b ->
+  eval_condition cond (map ms args) = Some b ->
   exists rs',
      exec_straight (transl_cond cond args k) rs m k rs' m
   /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
@@ -1131,7 +1131,7 @@ Lemma transl_cond_correct:
         else Val.notbool (Val.of_bool b))
   /\ agree ms sp rs'.
 Proof.
-  intros. rewrite <- (eval_condition_weaken _ _ _ H1). 
+  intros. rewrite <- (eval_condition_weaken _ _ H1). 
   apply transl_cond_correct_aux; auto.
 Qed.
 
@@ -1161,12 +1161,12 @@ Lemma transl_op_correct:
   forall op args res k ms sp rs m v,
   wt_instr (Mop op args res) ->
   agree ms sp rs ->
-  eval_operation ge sp op (map ms args) m = Some v ->
+  eval_operation ge sp op (map ms args) = Some v ->
   exists rs',
      exec_straight (transl_op op args res k) rs m k rs' m
   /\ agree (Regmap.set res v ms) sp rs'.
 Proof.
-  intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H1). clear H1; clear v.
+  intros. rewrite <- (eval_operation_weaken _ _ _ _ H1). clear H1; clear v.
   inversion H.
   (* Omove *)
   simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))).
@@ -1602,31 +1602,6 @@ Proof.
   auto. auto.
 Qed.
 
-(** Translation of allocations *)
-
-Lemma transl_alloc_correct:
-  forall ms sp rs sz m m' blk k,
-  agree ms sp rs ->
-  ms Conventions.loc_alloc_argument = Vint sz ->
-  Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
-  let ms' := Regmap.set Conventions.loc_alloc_result (Vptr blk Int.zero) ms in
-  exists rs',
-    exec_straight (Pallocblock :: k) rs m k rs' m'
-  /\ agree ms' sp rs'.
-Proof.
-  intros. 
-  pose (rs' := nextinstr (rs#GPR3 <- (Vptr blk Int.zero) #LR <- (Val.add rs#PC Vone))).
-  exists rs'; split.
-  apply exec_straight_one. unfold exec_instr. 
-  generalize (preg_val _ _ _ Conventions.loc_alloc_argument H).
-  unfold preg_of; intro. simpl in H2. rewrite <- H2. rewrite H0.
-  rewrite H1. reflexivity.
-  reflexivity. 
-  unfold ms', rs'. apply agree_nextinstr. apply agree_set_other. 
-  change (IR GPR3) with (preg_of Conventions.loc_alloc_result).
-  apply agree_set_mreg. auto.
-  simpl. tauto.
-Qed.
 
 End STRAIGHTLINE.
 
diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v
index 75fb148..6ec27a3 100644
--- a/powerpc/Constprop.v
+++ b/powerpc/Constprop.v
@@ -654,8 +654,10 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
           D.set res Unknown before
       | Itailcall sig ros args =>
           before
+(*
       | Ialloc arg res s =>
           D.set res Unknown before
+*)
       | Icond cond args ifso ifnot =>
           before
       | Ireturn optarg =>
@@ -1045,8 +1047,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) :=
       Icall sig (transf_ros approx ros) args res s
   | Itailcall sig ros args =>
       Itailcall sig (transf_ros approx ros) args
-  | Ialloc arg res s =>
-      Ialloc arg res s
   | Icond cond args s1 s2 =>
       match eval_static_condition cond (approx_regs args approx) with
       | Some b =>
diff --git a/powerpc/Constpropproof.v b/powerpc/Constpropproof.v
index e16f322..dbd498f 100644
--- a/powerpc/Constpropproof.v
+++ b/powerpc/Constpropproof.v
@@ -143,10 +143,10 @@ Ltac InvVLMA :=
   approximations returned by [eval_static_operation]. *)
 
 Lemma eval_static_condition_correct:
-  forall cond al vl m b,
+  forall cond al vl b,
   val_list_match_approx al vl ->
   eval_static_condition cond al = Some b ->
-  eval_condition cond vl m = Some b.
+  eval_condition cond vl = Some b.
 Proof.
   intros until b.
   unfold eval_static_condition. 
@@ -155,9 +155,9 @@ Proof.
 Qed.
 
 Lemma eval_static_operation_correct:
-  forall op sp al vl m v,
+  forall op sp al vl v,
   val_list_match_approx al vl ->
-  eval_operation ge sp op vl m = Some v ->
+  eval_operation ge sp op vl = Some v ->
   val_match_approx (eval_static_operation op al) v.
 Proof.
   intros until v.
@@ -203,7 +203,7 @@ Proof.
   rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
 
   caseEq (eval_static_condition c vl0).
-  intros. generalize (eval_static_condition_correct _ _ _ m _ H H1).
+  intros. generalize (eval_static_condition_correct _ _ _ _ H H1).
   intro. rewrite H2 in H0. 
   destruct b; injection H0; intro; subst v; simpl; auto.
   intros; simpl; auto.
@@ -276,9 +276,9 @@ Proof.
 Qed.
 
 Lemma cond_strength_reduction_correct:
-  forall cond args m,
+  forall cond args,
   let (cond', args') := cond_strength_reduction approx cond args in
-  eval_condition cond' rs##args' m = eval_condition cond rs##args m.
+  eval_condition cond' rs##args' = eval_condition cond rs##args.
 Proof.
   intros. unfold cond_strength_reduction.
   case (cond_strength_reduction_match cond args); intros.
@@ -299,10 +299,10 @@ Proof.
 Qed.
 
 Lemma make_addimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_addimm n r in
-  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_addimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -312,10 +312,10 @@ Proof.
 Qed.
   
 Lemma make_shlimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_shlimm n r in
-  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_shlimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -326,10 +326,10 @@ Proof.
 Qed.
 
 Lemma make_shrimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_shrimm n r in
-  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_shrimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -338,10 +338,10 @@ Proof.
 Qed.
 
 Lemma make_shruimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_shruimm n r in
-  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_shruimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -352,10 +352,10 @@ Proof.
 Qed.
 
 Lemma make_mulimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_mulimm n r in
-  eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_mulimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -363,8 +363,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) m)
-     with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m).
+  replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil))
+     with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
   apply make_shlimm_correct. 
   simpl. generalize (Int.is_power2_range _ _ H1). 
   change (Z_of_nat wordsize) with 32. intro. rewrite H2.
@@ -373,10 +373,10 @@ Proof.
 Qed.
 
 Lemma make_andimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_andimm n r in
-  eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_andimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -387,10 +387,10 @@ Proof.
 Qed.
 
 Lemma make_orimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_orimm n r in
-  eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_orimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -401,10 +401,10 @@ Proof.
 Qed.
 
 Lemma make_xorimm_correct:
-  forall n r m v,
+  forall n r v,
   let (op, args) := make_xorimm n r in
-  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v ->
+  eval_operation ge sp op rs##args = Some v.
 Proof.
   intros; unfold make_xorimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -413,18 +413,18 @@ Proof.
 Qed.
 
 Lemma op_strength_reduction_correct:
-  forall op args m v,
+  forall op args v,
   let (op', args') := op_strength_reduction approx op args in
-  eval_operation ge sp op rs##args m = Some v ->
-  eval_operation ge sp op' rs##args' m = Some v.
+  eval_operation ge sp op rs##args = Some v ->
+  eval_operation ge sp op' rs##args' = Some v.
 Proof.
   intros; unfold op_strength_reduction;
   case (op_strength_reduction_match op args); intros; simpl List.map.
   (* Oadd *)
   caseEq (intval approx r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m).
+  replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil))
+     with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)).
   apply make_addimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto.
   caseEq (intval approx r2); intros.
@@ -435,16 +435,16 @@ Proof.
   rewrite (intval_correct _ _ H) in H0. assumption. 
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H0). 
-  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).
+  replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)).
   apply make_addimm_correct.
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. 
   assumption.
   (* Omul *)
   caseEq (intval approx r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m).
+  replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil))
+     with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)).
   apply make_mulimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
   caseEq (intval approx r2); intros.
@@ -464,8 +464,8 @@ Proof.
   caseEq (intval approx r2); intros.
   caseEq (Int.is_power2 i); intros.
   rewrite (intval_correct _ _ H).
-  replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m).
+  replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)).
   apply make_shruimm_correct. 
   simpl. destruct rs#r1; auto. 
   change 32 with (Z_of_nat wordsize). 
@@ -478,8 +478,8 @@ Proof.
   (* Oand *)
   caseEq (intval approx r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m).
+  replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil))
+     with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)).
   apply make_andimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto.
   caseEq (intval approx r2); intros.
@@ -488,8 +488,8 @@ Proof.
   (* Oor *)
   caseEq (intval approx r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m).
+  replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil))
+     with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)).
   apply make_orimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto.
   caseEq (intval approx r2); intros.
@@ -498,8 +498,8 @@ Proof.
   (* Oxor *)
   caseEq (intval approx r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m).
+  replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil))
+     with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)).
   apply make_xorimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto.
   caseEq (intval approx r2); intros.
@@ -763,13 +763,13 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
   TransfInstr. caseEq (op_strength_reduction (analyze f)!!pc op args);
   intros op' args' OSR.
-  assert (eval_operation tge sp op' rs##args' m = Some v).
+  assert (eval_operation tge sp op' rs##args' = Some v).
     rewrite (eval_operation_preserved symbols_preserved). 
     generalize (op_strength_reduction_correct ge (analyze f)!!pc sp rs
-                  MATCH op args m v).
+                  MATCH op args v).
     rewrite OSR; simpl. auto.
   generalize (eval_static_operation_correct ge op sp
-               (approx_regs args (analyze f)!!pc) rs##args m v
+               (approx_regs args (analyze f)!!pc) rs##args v
                (approx_regs_val_list _ _ _ args MATCH) H0).
   case (eval_static_operation op (approx_regs args (analyze f)!!pc)); intros;
   simpl in H2;
@@ -838,28 +838,18 @@ Proof.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
   constructor; auto. 
 
-  (* Ialloc *)
-  TransfInstr; intro.
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- (Vptr b Int.zero)) m'); split.
-  eapply exec_Ialloc; eauto.
-  econstructor; eauto.
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. simpl; auto.
-
   (* Icond, true *)
   exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. 
   caseEq (cond_strength_reduction (analyze f)!!pc cond args);
   intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' m = Some true).
+  assert (eval_condition cond' rs##args' = Some true).
     generalize (cond_strength_reduction_correct
-                  ge (analyze f)!!pc rs MATCH cond args m).
+                  ge (analyze f)!!pc rs MATCH cond args).
     rewrite CSR.  intro. congruence.
   TransfInstr. rewrite CSR. 
   caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)).
   intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ m _
+  generalize (eval_static_condition_correct ge cond _ _ _
                (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
   replace b with true. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_true; eauto.
@@ -872,14 +862,14 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. 
   caseEq (cond_strength_reduction (analyze f)!!pc cond args);
   intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' m = Some false).
+  assert (eval_condition cond' rs##args' = Some false).
     generalize (cond_strength_reduction_correct
-                  ge (analyze f)!!pc rs MATCH cond args m).
+                  ge (analyze f)!!pc rs MATCH cond args).
     rewrite CSR.  intro. congruence.
   TransfInstr. rewrite CSR. 
   caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)).
   intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ m _
+  generalize (eval_static_condition_correct ge cond _ _ _
                (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
   replace b with false. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_false; eauto.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 20ebf70..300a804 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -139,28 +139,28 @@ Qed.
 Definition eval_compare_mismatch (c: comparison) : option bool :=
   match c with Ceq => Some false | Cne => Some true | _ => None end.
 
-Definition eval_condition (cond: condition) (vl: list val) (m: mem):
+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):
                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 valid_pointer m b1 (Int.signed n1)
-      && valid_pointer m b2 (Int.signed n2) then
-        if eq_block b1 b2
-        then Some (Int.cmp c n1 n2)
-        else eval_compare_mismatch c
-      else None
+      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 =>
-      if Int.eq n2 Int.zero then eval_compare_mismatch c else None
+      eval_compare_null c n2
   | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil =>
-      if Int.eq n1 Int.zero then eval_compare_mismatch c else None
+      eval_compare_null c n1
   | Ccompu c, Vint n1 :: Vint n2 :: nil =>
       Some (Int.cmpu c n1 n2)
   | Ccompimm c n, Vint n1 :: nil =>
       Some (Int.cmp c n1 n)
   | Ccompimm c n, Vptr b1 n1 :: nil =>
-      if Int.eq n Int.zero then eval_compare_mismatch c else None
+      eval_compare_null c n
   | Ccompuimm c n, Vint n1 :: nil =>
       Some (Int.cmpu c n1 n)
   | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil =>
@@ -183,7 +183,7 @@ Definition offset_sp (sp: val) (delta: int) : option val :=
 
 Definition eval_operation
     (F: Set) (genv: Genv.t F) (sp: val)
-    (op: operation) (vl: list val) (m: mem): option val :=
+    (op: operation) (vl: list val): option val :=
   match op, vl with
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
@@ -256,7 +256,7 @@ Definition eval_operation
   | Ofloatofintu, Vint n1 :: nil => 
       Some (Vfloat (Float.floatofintu n1))
   | Ocmp c, _ =>
-      match eval_condition c vl m with
+      match eval_condition c vl with
       | None => None
       | Some false => Some Vfalse
       | Some true => Some Vtrue
@@ -322,24 +322,30 @@ Proof.
   destruct c; intro EQ; inv EQ; auto. 
 Qed.
 
+Remark eval_negate_compare_null:
+  forall c i b,
+  eval_compare_null c i = Some b ->
+  eval_compare_null (negate_comparison c) i = Some (negb b).
+Proof.
+  unfold eval_compare_null; intros.
+  destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. congruence.
+Qed.
+
 Lemma eval_negate_condition:
-  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).
+  forall (cond: condition) (vl: list val) (b: bool),
+  eval_condition cond vl = Some b ->
+  eval_condition (negate_condition cond) vl = Some (negb b).
 Proof.
   intros. 
   destruct cond; simpl in H; FuncInv; try subst b; simpl.
   rewrite Int.negate_cmp. auto.
-  destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate.
-  destruct (Int.eq i0 Int.zero). apply eval_negate_compare_mismatch; auto. discriminate.
-  destruct (valid_pointer m b0 (Int.signed i) &&
-            valid_pointer m b1 (Int.signed i0)).
+  apply eval_negate_compare_null; auto.
+  apply eval_negate_compare_null; auto.
   destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence.
   apply eval_negate_compare_mismatch; auto. 
-  discriminate.
   rewrite Int.negate_cmpu. auto.
   rewrite Int.negate_cmp. auto.
-  destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate.
+  apply eval_negate_compare_null; auto.
   rewrite Int.negate_cmpu. auto.
   auto.
   rewrite negb_elim. auto.
@@ -361,8 +367,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 m,
-  eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
+  forall sp op vl,
+  eval_operation ge2 sp op vl = eval_operation ge1 sp op vl.
 Proof.
   intros.
   unfold eval_operation; destruct op; try rewrite agree_on_symbols;
@@ -380,74 +386,6 @@ Qed.
 
 End GENV_TRANSF.
 
-(** [eval_condition] and [eval_operation] depend on a memory store
-    (to check pointer validity in pointer comparisons).
-    We show that their results are preserved by a change of
-    memory if this change preserves pointer validity.
-    In particular, this holds in case of a memory allocation
-    or a memory store. *)
-
-Lemma eval_condition_change_mem:
-  forall m m' c args b,
-  (forall b ofs, valid_pointer m b ofs = true -> valid_pointer m' b ofs = true) ->
-  eval_condition c args m = Some b -> eval_condition c args m' = Some b.
-Proof.
-  intros until b. intro INV. destruct c; simpl; auto.
-  destruct args; auto. destruct v; auto. destruct args; auto.
-  destruct v; auto. destruct args; auto. 
-  caseEq (valid_pointer m b0 (Int.signed i)); intro.
-  caseEq (valid_pointer m b1 (Int.signed i0)); intro.
-  simpl. rewrite (INV _ _ H). rewrite (INV _ _ H0). auto.
-  simpl; congruence. simpl; congruence.
-Qed.
-
-Lemma eval_operation_change_mem:
-  forall (F: Set) m m' (ge: Genv.t F) sp op args v,
-  (forall b ofs, valid_pointer m b ofs = true -> valid_pointer m' b ofs = true) ->
-  eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v.
-Proof.
-  intros until v; intro INV. destruct op; simpl; auto.
-  caseEq (eval_condition c args m); intros.
-  rewrite (eval_condition_change_mem _ _ _ _ INV H). auto.
-  discriminate.
-Qed.
-
-Lemma eval_condition_alloc:
-  forall m lo hi m' b c args v,
-  Mem.alloc m lo hi = (m', b) ->
-  eval_condition c args m = Some v -> eval_condition c args m' = Some v.
-Proof.
-  intros. apply eval_condition_change_mem with m; auto.
-  intros. eapply valid_pointer_alloc; eauto.
-Qed.
-
-Lemma eval_operation_alloc:
-  forall (F: Set) m lo hi m' b (ge: Genv.t F) sp op args v,
-  Mem.alloc m lo hi = (m', b) ->
-  eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v.
-Proof.
-  intros. apply eval_operation_change_mem with m; auto.
-  intros. eapply valid_pointer_alloc; eauto.
-Qed.
-
-Lemma eval_condition_store:
-  forall chunk m b ofs v' m' c args v,
-  Mem.store chunk m b ofs v' = Some m' ->
-  eval_condition c args m = Some v -> eval_condition c args m' = Some v.
-Proof.
-  intros. apply eval_condition_change_mem with m; auto.
-  intros. eapply valid_pointer_store; eauto.
-Qed.
-
-Lemma eval_operation_store:
-  forall (F: Set) chunk m b ofs v' m' (ge: Genv.t F) sp op args v,
-  Mem.store chunk m b ofs v' = Some m' ->
-  eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v.
-Proof.
-  intros. apply eval_operation_change_mem with m; auto.
-  intros. eapply valid_pointer_store; eauto.
-Qed.
-
 (** Recognition of move operations. *)
 
 Definition is_move_operation
@@ -563,9 +501,9 @@ Variable A: Set.
 Variable genv: Genv.t A.
 
 Lemma type_of_operation_sound:
-  forall op vl sp v m,
+  forall op vl sp v,
   op <> Omove ->
-  eval_operation genv sp op vl m = Some v ->
+  eval_operation genv sp op vl = Some v ->
   Val.has_type v (snd (type_of_operation op)).
 Proof.
   intros.
@@ -716,35 +654,33 @@ Qed.
 
 Lemma eval_compare_null_weaken:
   forall n c b,
-  (if Int.eq n Int.zero then eval_compare_mismatch c else None) = Some b ->
+  eval_compare_null c n = Some b ->
   (if Int.eq n Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b.
 Proof.
+  unfold eval_compare_null.
   intros. destruct (Int.eq n Int.zero). apply eval_compare_mismatch_weaken. auto.
   discriminate.
 Qed.
 
 Lemma eval_condition_weaken:
-  forall c vl m b,
-  eval_condition c vl m = Some b ->
+  forall c vl b,
+  eval_condition c vl = 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 (valid_pointer m b0 (Int.signed i) &&
-            valid_pointer m b1 (Int.signed i0)).
   unfold eq_block in H. destruct (zeq b0 b1).
   congruence.
   apply eval_compare_mismatch_weaken; auto.
-  discriminate.
   symmetry. apply Val.notbool_negb_1. 
   symmetry. apply Val.notbool_negb_1. 
 Qed.
 
 Lemma eval_operation_weaken:
-  forall sp op vl m v,
-  eval_operation genv sp op vl m = Some v ->
+  forall sp op vl v,
+  eval_operation genv sp op vl = Some v ->
   eval_operation_total sp op vl = v.
 Proof.
   intros.
@@ -763,7 +699,7 @@ Proof.
   destruct (Int.ltu i (Int.repr 32)); congruence.
   destruct (Int.ltu i (Int.repr 32)); congruence.
   destruct (Int.ltu i0 (Int.repr 32)); congruence.
-  caseEq (eval_condition c vl m); intros; rewrite H0 in H.
+  caseEq (eval_condition c vl); intros; rewrite H0 in H.
   replace v with (Val.of_bool b).
   eapply eval_condition_weaken; eauto.
   destruct b; simpl; congruence.
@@ -806,14 +742,12 @@ Qed.
 End EVAL_OP_TOTAL.
 
 (** Compatibility of the evaluation functions with the
-    ``is less defined'' relation over values and memory states. *)
+    ``is less defined'' relation over values. *)
 
 Section EVAL_LESSDEF.
 
 Variable F: Set.
 Variable genv: Genv.t F.
-Variables m1 m2: mem.
-Hypothesis MEM: Mem.lessdef m1 m2.
 
 Ltac InvLessdef :=
   match goal with
@@ -833,16 +767,10 @@ Ltac InvLessdef :=
 Lemma eval_condition_lessdef:
   forall cond vl1 vl2 b,
   Val.lessdef_list vl1 vl2 ->
-  eval_condition cond vl1 m1 = Some b ->
-  eval_condition cond vl2 m2 = Some b.
+  eval_condition cond vl1 = Some b ->
+  eval_condition cond vl2 = Some b.
 Proof.
   intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto.
-  generalize H0.
-  caseEq (valid_pointer m1 b0 (Int.signed i)); intro; simpl; try congruence.
-  caseEq (valid_pointer m1 b1 (Int.signed i0)); intro; simpl; try congruence.
-  rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H1).
-  rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H). simpl.
-  auto.
 Qed.
 
 Ltac TrivialExists :=
@@ -855,8 +783,8 @@ Ltac TrivialExists :=
 Lemma eval_operation_lessdef:
   forall sp op vl1 vl2 v1,
   Val.lessdef_list vl1 vl2 ->
-  eval_operation genv sp op vl1 m1 = Some v1 ->
-  exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
+  eval_operation genv sp op vl1 = Some v1 ->
+  exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
   intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists.
   exists v2; auto.
@@ -875,7 +803,7 @@ Proof.
   destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists.
   destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
   exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
-  caseEq (eval_condition c vl1 m1); intros. rewrite H1 in H0. 
+  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.
@@ -906,10 +834,10 @@ End EVAL_LESSDEF.
 Definition op_for_binary_addressing (addr: addressing) : operation := Oadd.
 
 Lemma eval_op_for_binary_addressing:
-  forall (F: Set) (ge: Genv.t F) sp addr args m v,
+  forall (F: Set) (ge: Genv.t F) sp addr args v,
   (length args >= 2)%nat ->
   eval_addressing ge sp addr args = Some v ->
-  eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
+  eval_operation ge sp (op_for_binary_addressing addr) args = Some v.
 Proof.
   intros.
   unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction;
diff --git a/powerpc/Selection.v b/powerpc/Selection.v
index 1de6ae3..f1c5a73 100644
--- a/powerpc/Selection.v
+++ b/powerpc/Selection.v
@@ -1161,7 +1161,6 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
       Scall optid sg (sel_expr fn) (sel_exprlist args)
   | Cminor.Stailcall sg fn args => 
       Stailcall sg (sel_expr fn) (sel_exprlist args)
-  | Cminor.Salloc id b => Salloc id (sel_expr b)
   | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2)
   | Cminor.Sifthenelse e ifso ifnot =>
       Sifthenelse (condexpr_of_expr (sel_expr e))
diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v
index 5e0b2b2..b6e838c 100644
--- a/powerpc/Selectionproof.v
+++ b/powerpc/Selectionproof.v
@@ -149,13 +149,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
@@ -234,12 +234,12 @@ Proof.
   eapply eval_notbool_base; eauto.
 
   inv H. eapply eval_Eop; eauto.
-  simpl. assert (eval_condition c vl m = Some b).
+  simpl. assert (eval_condition c vl = Some b).
   generalize H6. simpl. 
-  case (eval_condition c vl m); intros.
+  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. 
@@ -545,9 +545,9 @@ Qed.
 
 Lemma eval_mod_aux:
   forall divop semdivop,
-  (forall sp x y m,
+  (forall sp x y,
    y <> Int.zero ->
-   eval_operation ge sp divop (Vint x :: Vint y :: nil) m =
+   eval_operation ge sp divop (Vint x :: Vint y :: nil) =
    Some (Vint (semdivop x y))) ->
   forall le a b x y,
   eval_expr ge sp e m le a (Vint x) ->
@@ -812,52 +812,66 @@ Proof.
   EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
 Qed.
 
+Remark eval_compare_null_transf:
+  forall c x v,
+  Cminor.eval_compare_null c x = Some v ->
+  match eval_compare_null c x with
+  | Some true => Some Vtrue
+  | Some false => Some Vfalse
+  | None => None (A:=val)
+  end = Some v.
+Proof.
+  unfold Cminor.eval_compare_null, eval_compare_null; intros.
+  destruct (Int.eq x Int.zero); try discriminate. 
+  destruct c; try discriminate; auto.
+Qed.
+
 Theorem eval_comp_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 ->
+  Cminor.eval_compare_null c y = Some v ->
   eval_expr ge sp e m le (comp c a b) v.
 Proof.
   intros until v.
   unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate.
-  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
-  destruct c; try discriminate; auto.
-  EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate.
-  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
-  destruct c; try discriminate; auto.
+  EvalOp. simpl. apply eval_compare_null_transf; auto.
+  EvalOp. simpl. apply eval_compare_null_transf; auto.
+Qed.
+
+Remark eval_compare_null_swap:
+  forall c x,
+  Cminor.eval_compare_null (swap_comparison c) x = 
+  Cminor.eval_compare_null c x.
+Proof.
+  intros. unfold Cminor.eval_compare_null. 
+  destruct (Int.eq x Int.zero). destruct c; auto. auto.
 Qed.
 
 Theorem eval_comp_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 ->
+  Cminor.eval_compare_null c x = Some v ->
   eval_expr ge sp e m le (comp c a b) v.
 Proof.
   intros until v.
   unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate.
-  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
-  destruct c; try discriminate; auto.
-  EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate.
-  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
-  destruct c; try discriminate; auto.
+  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:
   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) ->
-  valid_pointer m x1 (Int.signed x2) &&
-  valid_pointer m y1 (Int.signed y2) = true ->
   x1 = y1 ->
   eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)).
 Proof.
   intros until y2.
   unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. 
+  EvalOp. simpl. subst y1. rewrite dec_eq_true. 
   destruct (Int.cmp c x2 y2); reflexivity.
 Qed.
 
@@ -865,16 +879,14 @@ Theorem eval_comp_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) ->
-  valid_pointer m x1 (Int.signed x2) &&
-  valid_pointer m y1 (Int.signed y2) = true ->
   x1 <> y1 ->
   Cminor.eval_compare_mismatch c = Some v ->
   eval_expr ge sp e m le (comp c a b) v.
 Proof.
   intros until y2.
   unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto.
-  destruct c; simpl in H3; inv H3; auto.
+  EvalOp. simpl. rewrite dec_eq_false; auto.
+  destruct c; simpl in H2; inv H2; auto.
 Qed.
 
 Theorem eval_compu:
@@ -955,7 +967,7 @@ Qed.
 Lemma is_compare_neq_zero_correct:
   forall c v b,
   is_compare_neq_zero c = true ->
-  eval_condition c (v :: nil) m = Some b ->
+  eval_condition c (v :: nil) = Some b ->
   Val.bool_of_val v b.
 Proof.
   intros.
@@ -975,7 +987,7 @@ Qed.
 Lemma is_compare_eq_zero_correct:
   forall c v b,
   is_compare_eq_zero c = true ->
-  eval_condition c (v :: nil) m = Some b ->
+  eval_condition c (v :: nil) = Some b ->
   Val.bool_of_val v (negb b).
 Proof.
   intros. apply is_compare_neq_zero_correct with (negate_condition c).
@@ -1003,8 +1015,8 @@ Proof.
   eapply eval_base_condition_of_expr; eauto.
 
   inv H0. simpl in H7.
-  assert (eval_condition c vl m = Some b).
-    destruct (eval_condition c vl m); try discriminate.
+  assert (eval_condition c vl = Some b).
+    destruct (eval_condition c vl); try discriminate.
     destruct b0; inv H7; inversion H1; congruence.
   assert (eval_condexpr ge sp e m le (CEcond c e0) b).
     eapply eval_CEcond; eauto.
@@ -1119,7 +1131,7 @@ Lemma eval_sel_binop:
   forall le op a1 a2 v1 v2 v,
   eval_expr ge sp e m le a1 v1 ->
   eval_expr ge sp e m le a2 v2 ->
-  eval_binop op v1 v2 m = Some v ->
+  eval_binop op v1 v2 = Some v ->
   eval_expr ge sp e m le (sel_binop op a1 a2) v.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
@@ -1154,12 +1166,9 @@ Proof.
   apply eval_comp_int; auto.
   eapply eval_comp_int_ptr; eauto.
   eapply eval_comp_ptr_int; eauto.
-  generalize H1; clear H1.
-  case_eq (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)); intros.
-  destruct (eq_block b b0); inv H2.
+  destruct (eq_block b b0); inv H1.
   eapply eval_comp_ptr_ptr; eauto.
   eapply eval_comp_ptr_ptr_2; eauto.
-  discriminate.
   eapply eval_compu; eauto.
   eapply eval_compf; eauto.
 Qed.
@@ -1340,10 +1349,6 @@ Proof.
   apply functions_translated; eauto. 
   apply sig_function_translated.
   constructor; auto. apply call_cont_commut.
-  (* Salloc *)
-  exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id (Vptr b Int.zero) e) m'); split.
-  econstructor; eauto with evalexpr.
-  constructor; auto.
   (* Sifthenelse *)
   exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split.
   constructor. eapply eval_condition_of_expr; eauto with evalexpr.
diff --git a/powerpc/eabi/Conventions.v b/powerpc/eabi/Conventions.v
index 6e27b9d..90e14a0 100644
--- a/powerpc/eabi/Conventions.v
+++ b/powerpc/eabi/Conventions.v
@@ -792,7 +792,3 @@ Proof.
   intros; simpl. tauto.
 Qed.
 
-(** ** Location of argument and result for dynamic memory allocation *)
-
-Definition loc_alloc_argument := R3.
-Definition loc_alloc_result := R3.
diff --git a/powerpc/macosx/Conventions.v b/powerpc/macosx/Conventions.v
index 4f06b41..6d1ccb1 100644
--- a/powerpc/macosx/Conventions.v
+++ b/powerpc/macosx/Conventions.v
@@ -799,7 +799,3 @@ Proof.
   intros; simpl. tauto.
 Qed.
 
-(** ** Location of argument and result for dynamic memory allocation *)
-
-Definition loc_alloc_argument := R3.
-Definition loc_alloc_result := R3.