- 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

10 files changed, 128 insertions, 424 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 72534c0..3bb2cca 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -145,7 +145,6 @@ Inductive instruction : Set :=
   | Psufd: freg -> freg -> freg -> instruction     (**r float subtraction *)
 
   (* Pseudo-instructions *)
-  | Pallocblock: instruction                       (**r dynamic allocation *)
   | Pallocframe: Z -> Z -> int -> instruction      (**r allocate new stack frame *)
   | Pfreeframe: int -> instruction                 (**r deallocate stack frame and restore previous frame *)
   | Plabel: label -> instruction                   (**r define a code label *)
@@ -232,11 +231,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.
@@ -538,14 +532,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Psufd r1 r2 r3 =>     
       OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
   (* Pseudo-instructions *)
-  | Pallocblock =>
-      match rs#IR0 with
-      | Vint n =>
-          let (m', b) := Mem.alloc m 0 (Int.signed n) in
-          OK (nextinstr (rs#IR0 <- (Vptr b Int.zero)
-                           #IR14 <- (Val.add rs#PC Vone))) m'
-      | _ => Error
-      end
   | Pallocframe lo hi pos =>             
       let (m1, stk) := Mem.alloc m lo hi in
       let sp := (Vptr stk (Int.repr lo)) in
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 5e21e14..7e40949 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -477,8 +477,6 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
   | Mtailcall sig (inr symb) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
         (Pfreeframe f.(fn_link_ofs) :: Pbsymb symb :: k)
-  | Malloc =>
-      Pallocblock :: k
   | Mlabel lbl =>
       Plabel lbl :: k
   | Mgoto lbl =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 69a82de..f9f4cd0 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -523,50 +523,6 @@ Proof.
   intros. apply Pregmap.gso; auto.
 Qed.
 
-(** * Memory properties *)
-
-(** We show that signed 8- and 16-bit stores can be performed
-  like unsigned stores. *)
-
-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 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
@@ -767,7 +723,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.
@@ -940,21 +896,6 @@ Proof.
   intros. rewrite Pregmap.gso; auto.
 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)
@@ -984,7 +925,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
@@ -1020,7 +961,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.
@@ -1197,7 +1138,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/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 32fedf3..b18ae91 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -431,60 +431,6 @@ Qed.
 
 (** * Correctness of ARM constructor functions *)
 
-(** Properties of comparisons. *)
-(*
-Lemma compare_float_spec:
-  forall rs v1 v2,
-  let rs1 := nextinstr (compare_float rs v1 v2) in
-     rs1#CR0_0 = Val.cmpf Clt v1 v2
-  /\ rs1#CR0_1 = Val.cmpf Cgt v1 v2
-  /\ rs1#CR0_2 = Val.cmpf Ceq v1 v2
-  /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
-       r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
-Proof.
-  intros. unfold rs1.
-  split. reflexivity.
-  split. reflexivity.
-  split. reflexivity.
-  intros. rewrite nextinstr_inv; auto.
-  unfold compare_float. repeat (rewrite Pregmap.gso; auto).
-Qed.
-
-Lemma compare_sint_spec:
-  forall rs v1 v2,
-  let rs1 := nextinstr (compare_sint rs v1 v2) in
-     rs1#CR0_0 = Val.cmp Clt v1 v2
-  /\ rs1#CR0_1 = Val.cmp Cgt v1 v2
-  /\ rs1#CR0_2 = Val.cmp Ceq v1 v2
-  /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
-       r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
-Proof.
-  intros. unfold rs1.
-  split. reflexivity.
-  split. reflexivity.
-  split. reflexivity.
-  intros. rewrite nextinstr_inv; auto.
-  unfold compare_sint. repeat (rewrite Pregmap.gso; auto).
-Qed.
-
-Lemma compare_uint_spec:
-  forall rs v1 v2,
-  let rs1 := nextinstr (compare_uint rs v1 v2) in
-     rs1#CR0_0 = Val.cmpu Clt v1 v2
-  /\ rs1#CR0_1 = Val.cmpu Cgt v1 v2
-  /\ rs1#CR0_2 = Val.cmpu Ceq v1 v2
-  /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
-       r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
-Proof.
-  intros. unfold rs1.
-  split. reflexivity.
-  split. reflexivity.
-  split. reflexivity.
-  intros. rewrite nextinstr_inv; auto.
-  unfold compare_uint. repeat (rewrite Pregmap.gso; auto).
-Qed.
-*)
-
 (** Loading a constant. *)
 
 Lemma loadimm_correct:
@@ -868,14 +814,14 @@ 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'#(CR (crbit_for_cond cond)) = Val.of_bool b
   /\ agree ms sp rs'.
 Proof.
   intros.
-  rewrite <- (eval_condition_weaken _ _ _ H1). clear H1. 
+  rewrite <- (eval_condition_weaken _ _ H1). clear H1. 
   destruct cond; simpl in H; TypeInv; simpl.
   (* Ccomp *)
   generalize (compare_int_spec rs ms#m0 ms#m1).
@@ -1008,12 +954,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))).
@@ -1036,29 +982,6 @@ Proof.
   intros [rs' [A [B C]]]. 
   exists rs'. split. auto. 
   apply agree_set_mireg_exten with rs; auto. 
-(*
-  (* Ofloatconst *)
-  exists (nextinstr (rs#(freg_of res) <- (Vfloat f))).
-  split. apply exec_straight_one. reflexivity. reflexivity.
-  auto with ppcgen.
-  (* Oaddrsymbol *)
-  change (find_symbol_offset ge i i0) with (symbol_offset ge i i0).
-  set (v := symbol_offset ge i i0).
-  pose (rs1 := nextinstr (rs#GPR2 <- (high_half v))).
-  exists (nextinstr (rs1#(ireg_of res) <- v)).
-  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. 
-  simpl. rewrite gpr_or_zero_not_zero. 2: congruence. 
-  unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen.
-  rewrite Pregmap.gss. 
-  fold v. rewrite Val.add_commut. unfold v. rewrite low_high_half.
-  reflexivity. reflexivity. reflexivity. 
-  unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto.
-  apply agree_set_mreg. apply agree_nextinstr.
-  apply agree_set_other. auto. simpl. tauto.
-*)
   (* Oaddrstack *)
   generalize (addimm_correct (ireg_of res) IR13 i k rs m). 
   intros [rs' [EX [RES OTH]]].
@@ -1239,13 +1162,13 @@ Proof.
   repeat (rewrite (ireg_val ms sp rs); auto).
   reflexivity. auto 10 with ppcgen.
   (* Ocmp *)
-  assert (exists b, eval_condition c ms##args m = Some b /\ v = Val.of_bool b).
-    simpl in H1. destruct (eval_condition c ms##args m). 
+  assert (exists b, eval_condition c ms##args = Some b /\ v = Val.of_bool b).
+    simpl in H1. destruct (eval_condition c ms##args). 
     destruct b; inv H1. exists true; auto. exists false; auto.
     discriminate.
   destruct H5 as [b [EVC EQ]].
   exploit transl_cond_correct; eauto. intros [rs' [A [B C]]].
-  rewrite (eval_condition_weaken _ _ _ EVC).
+  rewrite (eval_condition_weaken _ _ EVC).
   set (rs1 := nextinstr (rs'#(ireg_of res) <- (Vint Int.zero))).
   set (rs2 := nextinstr (if b then (rs1#(ireg_of res) <- Vtrue) else rs1)).
   exists rs2; split.
@@ -1477,31 +1400,5 @@ Proof.
   auto with ppcgen.
 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#IR0 <- (Vptr blk Int.zero) #IR14 <- (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 IR0) with (preg_of Conventions.loc_alloc_result).
-  apply agree_set_mreg. auto.
-  simpl. tauto.
-Qed.
-
 End STRAIGHTLINE.
 
diff --git a/arm/Constprop.v b/arm/Constprop.v
index 7369012..b51d974 100644
--- a/arm/Constprop.v
+++ b/arm/Constprop.v
@@ -686,8 +686,6 @@ 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 =>
@@ -1206,8 +1204,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/arm/Constpropproof.v b/arm/Constpropproof.v
index e85cadf..7c7b878 100644
--- a/arm/Constpropproof.v
+++ b/arm/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.
@@ -197,7 +197,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.
@@ -270,9 +270,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.
@@ -304,10 +304,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.
@@ -317,10 +317,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.
@@ -331,10 +331,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.
@@ -345,10 +345,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.
@@ -359,11 +359,11 @@ Proof.
 Qed.
 
 Lemma make_mulimm_correct:
-  forall n r r' m v,
+  forall n r r' v,
   rs#r' = Vint n ->
   let (op, args) := make_mulimm n r r' in
-  eval_operation ge sp Omul (rs#r :: Vint n :: nil) 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.
@@ -371,8 +371,8 @@ Proof.
   generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros.
   subst n. simpl in H2. simpl. FuncInv. rewrite Int.mul_one in H1. congruence.
   caseEq (Int.is_power2 n); intros.
-  replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) 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 _ _ H2). 
   change (Z_of_nat wordsize) with 32. intro. rewrite H3.
@@ -381,10 +381,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.
@@ -395,10 +395,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.
@@ -409,10 +409,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.
@@ -423,18 +423,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.
@@ -443,8 +443,8 @@ Proof.
   (* Oaddshift *)
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil) m).
+  replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)).
   apply make_addimm_correct. 
   simpl. destruct rs#r1; auto.
   assumption.
@@ -454,16 +454,16 @@ Proof.
   simpl in *. destruct rs#r2; auto. 
   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.
   (* Osubshift *)
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil) m).
+  replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)).
   apply make_addimm_correct. 
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
   assumption.
@@ -475,8 +475,8 @@ Proof.
   (* 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. apply intval_correct; auto. 
   simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
   caseEq (intval approx r2); intros.
@@ -487,8 +487,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). 
@@ -501,8 +501,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.
@@ -511,15 +511,15 @@ Proof.
   (* Oandshift *)
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil) m).
+  replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* 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.
@@ -528,15 +528,15 @@ Proof.
   (* Oorshift *)
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
+  replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)).
   apply make_orimm_correct. reflexivity.
   assumption.
   (* 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.
@@ -545,22 +545,22 @@ Proof.
   (* Oxorshift *)
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
+  replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)).
   apply make_xorimm_correct. reflexivity.
   assumption.
   (* Obic *)
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil) m).
+  replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Obicshift *)
   caseEq (intval approx r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil) m).
+  replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil))
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Oshl *)
@@ -779,13 +779,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;
@@ -852,30 +852,20 @@ Proof.
   TransfInstr; intro.
   econstructor; split.
   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.
+  constructor; 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.
@@ -888,14 +878,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/arm/Op.v b/arm/Op.v
index 6a6df7e..bde7252 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -165,9 +165,7 @@ Definition eval_compare_mismatch (c: comparison) : option bool :=
   match c with Ceq => Some false | Cne => Some true | _ => None end.
 
 Definition eval_compare_null (c: comparison) (n: int) : option bool :=
-  if Int.eq n Int.zero 
-  then match c with Ceq => Some false | Cne => Some true | _ => None end
-  else None.
+  if Int.eq n Int.zero then eval_compare_mismatch c else None.
 
 Definition eval_shift (s: shift) (n: int) : int :=
   match s with
@@ -177,18 +175,15 @@ Definition eval_shift (s: shift) (n: int) : int :=
   | Sror x => Int.ror n (s_amount x)
   end.
 
-Definition eval_condition (cond: condition) (vl: list val) (m: mem):
+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 =>
       eval_compare_null c n2
   | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil =>
@@ -223,7 +218,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)
@@ -297,7 +292,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
@@ -358,20 +353,17 @@ Proof.
 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.
   apply eval_negate_compare_null; auto.
   apply eval_negate_compare_null; auto.
-  destruct (valid_pointer m b0 (Int.signed i) &&
-            valid_pointer m b1 (Int.signed i0)).
   destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence.
   destruct c; simpl in H; inv H; auto.
-  discriminate.
   rewrite Int.negate_cmpu. auto.
   rewrite Int.negate_cmp. auto.
   apply eval_negate_compare_null; auto.
@@ -397,8 +389,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;
@@ -418,74 +410,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
@@ -603,9 +527,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.
@@ -771,25 +695,22 @@ Proof.
 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); try congruence.
   apply eval_compare_mismatch_weaken; auto.
-  discriminate.
   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.
@@ -810,7 +731,7 @@ Proof.
   unfold Int.ltu. rewrite zlt_true. congruence. 
   assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto.
   omega. discriminate.
-  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.
@@ -855,8 +776,6 @@ 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
@@ -876,15 +795,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 :=
@@ -897,8 +811,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.
@@ -918,7 +832,7 @@ Proof.
   destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists.
   destruct (Int.ltu i (Int.repr 31)); 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.
@@ -986,10 +900,10 @@ Definition op_for_binary_addressing (addr: addressing) : operation :=
   end.
 
 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; simpl.
diff --git a/arm/Selection.v b/arm/Selection.v
index 1b5411b..d04a4ca 100644
--- a/arm/Selection.v
+++ b/arm/Selection.v
@@ -1359,7 +1359,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/arm/Selectionproof.v b/arm/Selectionproof.v
index a307597..10f93f3 100644
--- a/arm/Selectionproof.v
+++ b/arm/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
@@ -229,12 +229,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. 
@@ -591,9 +591,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) ->
@@ -912,15 +912,12 @@ 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. simpl. 
-  subst y1. rewrite dec_eq_true. 
+  EvalOp. simpl. subst y1. rewrite dec_eq_true. 
   destruct (Int.cmp c x2 y2); reflexivity.
 Qed.
 
@@ -928,16 +925,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.
 
 
@@ -1021,7 +1016,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.
@@ -1041,7 +1036,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).
@@ -1069,8 +1064,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.
@@ -1195,7 +1190,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.
@@ -1231,12 +1226,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.
@@ -1417,10 +1409,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/arm/linux/Conventions.v b/arm/linux/Conventions.v
index 0342521..a35162c 100644
--- a/arm/linux/Conventions.v
+++ b/arm/linux/Conventions.v
@@ -852,7 +852,3 @@ Proof.
   intros; simpl. tauto.
 Qed.
 
-(** ** Location of argument and result for dynamic memory allocation *)
-
-Definition loc_alloc_argument := R0.
-Definition loc_alloc_result := R0.