Merge of the nonstrict-ops branch:

- Most RTL operators now evaluate to Some Vundef instead of None
  when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.


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

1 files changed, 600 insertions, 698 deletions

diff --git a/arm/Op.v b/arm/Op.v
index 17cd0b44..905068f6 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -36,11 +36,11 @@ Require Import Events.
 
 Set Implicit Arguments.
 
-Record shift_amount : Type :=
-  mk_shift_amount { 
-    s_amount: int;
-    s_amount_ltu: Int.ltu s_amount Int.iwordsize = true 
-  }.
+Record shift_amount: Type := 
+  { s_amount: int;
+    s_range: Int.ltu s_amount Int.iwordsize = true }.
+
+Coercion s_amount: shift_amount >-> int.
 
 Inductive shift : Type :=
   | Slsl: shift_amount -> shift
@@ -70,10 +70,6 @@ Inductive operation : Type :=
   | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *)
   | Oaddrstack: int -> operation        (**r [rd] is set to the stack pointer plus the given offset *)
 (*c Integer arithmetic: *)
-  | Ocast8signed: operation             (**r [rd] is 8-bit sign extension of [r1] *)
-  | Ocast8unsigned: operation           (**r [rd] is 8-bit zero extension of [r1] *)
-  | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
-  | Ocast16unsigned: operation          (**r [rd] is 16-bit zero extension of [r1] *)
   | Oadd: operation                     (**r [rd = r1 + r2] *)
   | Oaddshift: shift -> operation       (**r [rd = r1 + shifted r2] *)
   | Oaddimm: int -> operation           (**r [rd = r1 + n] *)
@@ -158,68 +154,39 @@ Proof.
   decide equality.
 Qed.
 
-(** Evaluation of conditions, operators and addressing modes applied
-  to lists of values.  Return [None] when the computation is undefined:
-  wrong number of arguments, arguments of the wrong types, undefined 
-  operations such as division by zero.  [eval_condition] returns a boolean,
-  [eval_operation] and [eval_addressing] return a value. *)
+(** * Evaluation functions *)
 
-Definition eval_compare_mismatch (c: comparison) : option bool :=
-  match c with Ceq => Some false | Cne => Some true | _ => None end.
+Definition symbol_address (F V: Type) (genv: Genv.t F V) (id: ident) (ofs: int) : val :=
+  match Genv.find_symbol genv id with
+  | Some b => Vptr b ofs
+  | None => Vundef
+  end.
 
-Definition eval_compare_null (c: comparison) (n: int) : option bool :=
-  if Int.eq n Int.zero then eval_compare_mismatch c else None.
+(** Evaluation of conditions, operators and addressing modes applied
+  to lists of values.  Return [None] when the computation can trigger an
+  error, e.g. integer division by zero.  [eval_condition] returns a boolean,
+  [eval_operation] and [eval_addressing] return a value. *)
 
-Definition eval_shift (s: shift) (n: int) : int :=
+Definition eval_shift (s: shift) (v: val) : val :=
   match s with
-  | Slsl x => Int.shl n (s_amount x)
-  | Slsr x => Int.shru n (s_amount x)
-  | Sasr x => Int.shr n (s_amount x)
-  | Sror x => Int.ror n (s_amount x)
+  | Slsl x => Val.shl v (Vint x)
+  | Slsr x => Val.shru v (Vint x)
+  | Sasr x => Val.shr v (Vint x)
+  | Sror x => Val.ror v (Vint x)
   end.
 
 Definition eval_condition (cond: condition) (vl: list val) (m: mem):
                option bool :=
   match cond, vl with
-  | Ccomp c, Vint n1 :: Vint n2 :: nil =>
-      Some (Int.cmp c n1 n2)
-  | Ccompu c, Vint n1 :: Vint n2 :: nil =>
-      Some (Int.cmpu c n1 n2)
-  | Ccompu c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
-      if Mem.valid_pointer m b1 (Int.unsigned n1)
-      && Mem.valid_pointer m b2 (Int.unsigned n2) then
-        if eq_block b1 b2
-        then Some (Int.cmpu c n1 n2)
-        else eval_compare_mismatch c
-      else None
-  | Ccompu c, Vptr b1 n1 :: Vint n2 :: nil =>
-      eval_compare_null c n2
-  | Ccompu c, Vint n1 :: Vptr b2 n2 :: nil =>
-      eval_compare_null c n1
-  | Ccompshift c s, Vint n1 :: Vint n2 :: nil =>
-      Some (Int.cmp c n1 (eval_shift s n2))
-  | Ccompushift c s, Vint n1 :: Vint n2 :: nil =>
-      Some (Int.cmpu c n1 (eval_shift s n2))
-  | Ccompushift c s, Vptr b1 n1 :: Vint n2 :: nil =>
-      eval_compare_null c (eval_shift s n2)
-  | Ccompimm c n, Vint n1 :: nil =>
-      Some (Int.cmp c n1 n)
-  | Ccompuimm c n, Vint n1 :: nil =>
-      Some (Int.cmpu c n1 n)
-  | Ccompuimm c n, Vptr b1 n1 :: nil =>
-      eval_compare_null c n
-  | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil =>
-      Some (Float.cmp c f1 f2)
-  | Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil =>
-      Some (negb (Float.cmp c f1 f2))
-  | _, _ =>
-      None
-  end.
-
-Definition offset_sp (sp: val) (delta: int) : option val :=
-  match sp with
-  | Vptr b n => Some (Vptr b (Int.add n delta))
-  | _ => None
+  | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
+  | Ccompu c, v1 :: v2 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 v2
+  | Ccompshift c s, v1 :: v2 :: nil => Val.cmp_bool c v1 (eval_shift s v2)
+  | Ccompushift c s, v1 :: v2 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (eval_shift s v2)
+  | Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n)
+  | Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n)
+  | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2
+  | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2)
+  | _, _ => None
   end.
 
 Definition eval_operation
@@ -229,75 +196,48 @@ Definition eval_operation
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
   | Ofloatconst n, nil => Some (Vfloat n)
-  | Oaddrsymbol s ofs, nil =>
-      match Genv.find_symbol genv s with
-      | None => None
-      | Some b => Some (Vptr b ofs)
-      end
-  | Oaddrstack ofs, nil => offset_sp sp ofs
-  | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
-  | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
-  | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
-  | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1)
-  | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2))
-  | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1))
-  | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2))
-  | Oaddshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 (eval_shift s n2)))
-  | Oaddshift s, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 (eval_shift s n2)))
-  | Oaddimm n, Vint n1 :: nil => Some (Vint (Int.add n1 n))
-  | Oaddimm n, Vptr b1 n1 :: nil => Some (Vptr b1 (Int.add n1 n))
-  | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2))
-  | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2))
-  | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
-      if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None
-  | Osubshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 (eval_shift s n2)))
-  | Osubshift s, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 (eval_shift s n2)))
-  | Orsubshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub (eval_shift s n2) n1))
-  | Orsubimm n, Vint n1 :: nil => Some (Vint (Int.sub n n1))
-  | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2))
-  | Odiv, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2))
-  | Odivu, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
-  | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2))
-  | Oandshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 (eval_shift s n2)))
-  | Oandimm n, Vint n1 :: nil => Some (Vint (Int.and n1 n))
-  | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2))
-  | Oorshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 (eval_shift s n2)))
-  | Oorimm n, Vint n1 :: nil => Some (Vint (Int.or n1 n))
-  | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2))
-  | Oxorshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 (eval_shift s n2)))
-  | Oxorimm n, Vint n1 :: nil => Some (Vint (Int.xor n1 n))
-  | Obic, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 (Int.not n2)))
-  | Obicshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 (Int.not (eval_shift s n2))))
-  | Onot, Vint n1 :: nil => Some (Vint (Int.not n1))
-  | Onotshift s, Vint n1 :: nil => Some (Vint (Int.not (eval_shift s n1)))
-  | Oshl, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None
-  | Oshr, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
-  | Oshru, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
-  | Oshift s, Vint n :: nil => Some (Vint (eval_shift s n))
-  | Oshrximm n, Vint n1 :: nil =>
-      if Int.ltu n (Int.repr 31) then Some (Vint (Int.shrx n1 n)) else None
-  | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1))
-  | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1))
-  | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2))
-  | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2))
-  | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2))
-  | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2))
-  | Osingleoffloat, v1 :: nil => Some (Val.singleoffloat v1)
-  | Ointoffloat, Vfloat f1 :: nil => option_map Vint (Float.intoffloat f1)
-  | Ointuoffloat, Vfloat f1 :: nil => option_map Vint (Float.intuoffloat f1)
-  | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1))
-  | Ofloatofintu, Vint n1 :: nil => Some (Vfloat (Float.floatofintu n1))
-  | Ocmp c, _ =>
-      match eval_condition c vl m with
-      | None => None
-      | Some false => Some Vfalse
-      | Some true => Some Vtrue
-      end
+  | Oaddrsymbol s ofs, nil => Some (symbol_address genv s ofs)
+  | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
+  | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2)
+  | Oaddshift s, v1 :: v2 :: nil => Some (Val.add v1 (eval_shift s v2))
+  | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n))
+  | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2)
+  | Osubshift s, v1 :: v2 :: nil => Some (Val.sub v1 (eval_shift s v2))
+  | Orsubshift s, v1 :: v2 :: nil => Some (Val.sub (eval_shift s v2) v1)
+  | Orsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1)
+  | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
+  | Odiv, v1 :: v2 :: nil => Val.divs v1 v2
+  | Odivu, v1 :: v2 :: nil => Val.divu v1 v2
+  | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2)
+  | Oandshift s, v1 :: v2 :: nil => Some (Val.and v1 (eval_shift s v2))
+  | Oandimm n, v1 :: nil => Some (Val.and v1 (Vint n))
+  | Oor, v1 :: v2 :: nil => Some (Val.or v1 v2)
+  | Oorshift s, v1 :: v2 :: nil => Some (Val.or v1 (eval_shift s v2))
+  | Oorimm n, v1 :: nil => Some (Val.or v1 (Vint n))
+  | Oxor, v1 :: v2 :: nil => Some (Val.xor v1 v2)
+  | Oxorshift s, v1 :: v2 :: nil => Some (Val.xor v1 (eval_shift s v2))
+  | Oxorimm n, v1 :: nil => Some (Val.xor v1 (Vint n))
+  | Obic, v1 :: v2 :: nil => Some (Val.and v1 (Val.notint v2))
+  | Obicshift s, v1 :: v2 :: nil => Some (Val.and v1 (Val.notint (eval_shift s v2)))
+  | Onot, v1 :: nil => Some (Val.notint v1)
+  | Onotshift s, v1 :: nil => Some (Val.notint (eval_shift s v1))
+  | Oshl, v1 :: v2 :: nil => Some (Val.shl v1 v2)
+  | Oshr, v1 :: v2 :: nil => Some (Val.shr v1 v2)
+  | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2)
+  | Oshift s, v1 :: nil => Some (eval_shift s v1)
+  | Oshrximm n, v1 :: nil => Val.shrx v1 (Vint n)
+  | Onegf, v1::nil => Some(Val.negf v1)
+  | Oabsf, v1::nil => Some(Val.absf v1)
+  | Oaddf, v1::v2::nil => Some(Val.addf v1 v2)
+  | Osubf, v1::v2::nil => Some(Val.subf v1 v2)
+  | Omulf, v1::v2::nil => Some(Val.mulf v1 v2)
+  | Odivf, v1::v2::nil => Some(Val.divf v1 v2)
+  | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
+  | Ointoffloat, v1::nil => Val.intoffloat v1
+  | Ointuoffloat, v1::nil => Val.intuoffloat v1
+  | Ofloatofint, v1::nil => Val.floatofint v1
+  | Ofloatofintu, v1::nil => Val.floatofintu v1
+  | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m))
   | _, _ => None
   end.
 
@@ -305,31 +245,13 @@ Definition eval_addressing
     (F V: Type) (genv: Genv.t F V) (sp: val)
     (addr: addressing) (vl: list val) : option val :=
   match addr, vl with
-  | Aindexed n, Vptr b1 n1 :: nil =>
-      Some (Vptr b1 (Int.add n1 n))
-  | Aindexed2, Vptr b1 n1 :: Vint n2 :: nil =>
-      Some (Vptr b1 (Int.add n1 n2))
-  | Aindexed2, Vint n1 :: Vptr b2 n2 :: nil =>
-      Some (Vptr b2 (Int.add n1 n2))
-  | Aindexed2shift s, Vptr b1 n1 :: Vint n2 :: nil =>
-      Some (Vptr b1 (Int.add n1 (eval_shift s n2)))
-  | Ainstack ofs, nil =>
-      offset_sp sp ofs
+  | Aindexed n, v1 :: nil => Some (Val.add v1 (Vint n))
+  | Aindexed2, v1 :: v2 :: nil => Some (Val.add v1 v2)
+  | Aindexed2shift s, v1 :: v2 :: nil => Some (Val.add v1 (eval_shift s v2))
+  | Ainstack ofs, nil => Some (Val.add sp (Vint ofs))
   | _, _ => None
   end.
 
-Definition negate_condition (cond: condition): condition :=
-  match cond with
-  | Ccomp c => Ccomp(negate_comparison c)
-  | Ccompu c => Ccompu(negate_comparison c)
-  | Ccompshift c s => Ccompshift (negate_comparison c) s
-  | Ccompushift c s => Ccompushift (negate_comparison c) s
-  | Ccompimm c n => Ccompimm (negate_comparison c) n
-  | Ccompuimm c n => Ccompuimm (negate_comparison c) n
-  | Ccompf c => Cnotcompf c
-  | Cnotcompf c => Ccompf c
-  end.
-
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
@@ -342,99 +264,7 @@ Ltac FuncInv :=
       idtac
   end.
 
-Remark eval_negate_compare_null:
-  forall c n b,
-  eval_compare_null c n = Some b ->
-  eval_compare_null (negate_comparison c) n = Some (negb b).
-Proof.
-  intros until b. unfold eval_compare_null.
-  case (Int.eq n Int.zero). 
-  destruct c; intro EQ; simplify_eq EQ; intros; subst b; reflexivity.
-  intro; discriminate. 
-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).
-Proof.
-  intros. 
-  destruct cond; simpl in H; FuncInv; try subst b; simpl.
-  rewrite Int.negate_cmp. auto.
-  rewrite Int.negate_cmpu. auto.
-  apply eval_negate_compare_null; auto.
-  apply eval_negate_compare_null; auto.
-  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
-           Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
-  destruct (eq_block b0 b1). rewrite Int.negate_cmpu. congruence.
-  destruct c; simpl in H; inv H; auto.
-  rewrite Int.negate_cmp. auto.
-  rewrite Int.negate_cmpu. auto.
-  apply eval_negate_compare_null; auto.
-  rewrite Int.negate_cmp. auto.
-  rewrite Int.negate_cmpu. auto.
-  apply eval_negate_compare_null; auto.
-  auto.
-  rewrite negb_elim. auto.
-Qed.
-
-(** [eval_operation] and [eval_addressing] depend on a global environment
-  for resolving references to global symbols.  We show that they give
-  the same results if a global environment is replaced by another that
-  assigns the same addresses to the same symbols. *)
-
-Section GENV_TRANSF.
-
-Variable F1 F2 V1 V2: Type.
-Variable ge1: Genv.t F1 V1.
-Variable ge2: Genv.t F2 V2.
-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.
-Proof.
-  intros.
-  unfold eval_operation; destruct op; try rewrite agree_on_symbols;
-  reflexivity.
-Qed.
-
-Lemma eval_addressing_preserved:
-  forall sp addr vl,
-  eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl.
-Proof.
-  intros.
-  assert (UNUSED: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s).
-  exact agree_on_symbols.
-  unfold eval_addressing; destruct addr; try rewrite agree_on_symbols;
-  reflexivity.
-Qed.
-
-End GENV_TRANSF.
-
-(** Recognition of move operations. *)
-
-Definition is_move_operation
-    (A: Type) (op: operation) (args: list A) : option A :=
-  match op, args with
-  | Omove, arg :: nil => Some arg
-  | _, _ => None
-  end.
-
-Lemma is_move_operation_correct:
-  forall (A: Type) (op: operation) (args: list A) (a: A),
-  is_move_operation op args = Some a ->
-  op = Omove /\ args = a :: nil.
-Proof.
-  intros until a. unfold is_move_operation; destruct op;
-  try (intros; discriminate).
-  destruct args. intros; discriminate.
-  destruct args. intros. intuition congruence. 
-  intros; discriminate.
-Qed.
-
-(** Static typing of conditions, operators and addressing modes. *)
+(** * Static typing of conditions, operators and addressing modes. *)
 
 Definition type_of_condition (c: condition) : list typ :=
   match c with
@@ -455,10 +285,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ofloatconst _ => (nil, Tfloat)
   | Oaddrsymbol _ _ => (nil, Tint)
   | Oaddrstack _ => (nil, Tint)
-  | Ocast8signed => (Tint :: nil, Tint)
-  | Ocast8unsigned => (Tint :: nil, Tint)
-  | Ocast16signed => (Tint :: nil, Tint)
-  | Ocast16unsigned => (Tint :: nil, Tint)
   | Oadd => (Tint :: Tint :: nil, Tint)
   | Oaddshift _ => (Tint :: Tint :: nil, Tint)
   | Oaddimm _ => (Tint :: nil, Tint)
@@ -534,37 +360,54 @@ Lemma type_of_operation_sound:
   op <> Omove ->
   eval_operation genv sp op vl m = Some v ->
   Val.has_type v (snd (type_of_operation op)).
-Proof.
+Proof with (try exact I).
+  assert (S: forall s v, Val.has_type (eval_shift s v) Tint).
+    intros. unfold eval_shift. destruct s; destruct v; simpl; auto; rewrite s_range; exact I.
   intros.
-  destruct op; simpl in H0; FuncInv; try subst v; try exact I.
+  destruct op; simpl; simpl in H0; FuncInv; try subst v...
   congruence.
-  destruct (Genv.find_symbol genv i); simplify_eq H0; intro; subst v; exact I.
-  simpl. unfold offset_sp in H0. destruct sp; try discriminate.
-  inversion H0. exact I.
-  destruct v0; exact I. 
-  destruct v0; exact I. 
-  destruct v0; exact I. 
-  destruct v0; exact I. 
-  destruct (eq_block b b0). injection H0; intro; subst v; exact I.
-  discriminate.
-  destruct (Int.eq i0 Int.zero). discriminate. 
-  injection H0; intro; subst v; exact I.
-  destruct (Int.eq i0 Int.zero). discriminate. 
-  injection H0; intro; subst v; exact I.
-  destruct (Int.ltu i0 Int.iwordsize).
-  injection H0; intro; subst v; exact I. discriminate.
-  destruct (Int.ltu i0 Int.iwordsize).
-  injection H0; intro; subst v; exact I. discriminate.
-  destruct (Int.ltu i0 Int.iwordsize).
-  injection H0; intro; subst v; exact I. discriminate.
-  destruct (Int.ltu i (Int.repr 31)).
-  injection H0; intro; subst v; exact I. discriminate.
-  destruct v0; exact I.
-  destruct (Float.intoffloat f); simpl in H0; inv H0. exact I.
-  destruct (Float.intuoffloat f); simpl in H0; inv H0. exact I.
-  destruct (eval_condition c vl). 
-  destruct b; injection H0; intro; subst v; exact I.
-  discriminate.
+  unfold symbol_address. destruct (Genv.find_symbol genv i)...
+  destruct sp...
+  destruct v0; destruct v1...
+  generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto.
+  destruct v0...
+  destruct v0; destruct v1... simpl. destruct (zeq b b0)...
+  generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (zeq b b0)...
+  generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (zeq b0 b)...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
+  destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
+  destruct v0; destruct v1...
+  generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto.
+  destruct v0...
+  destruct v0; destruct v1...
+  generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto.
+  destruct v0...
+  destruct v0; destruct v1...
+  generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto.
+  destruct v0...
+  destruct v0; destruct v1...
+  generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto.
+  destruct v0...
+  generalize (S s v0). destruct (eval_shift s v0); simpl; tauto.
+  destruct v0; destruct v1... simpl. destruct (Int.ltu i0 Int.iwordsize)...
+  destruct v0; destruct v1... simpl. destruct (Int.ltu i0 Int.iwordsize)...
+  destruct v0; destruct v1... simpl. destruct (Int.ltu i0 Int.iwordsize)...
+  apply S.
+  destruct v0; simpl in H0; inv H0. destruct (Int.ltu i (Int.repr 31)); inv H2...
+  destruct v0...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); simpl in H2; inv H2...
+  destruct v0; simpl in H0; inv H0. destruct (Float.intuoffloat f); simpl in H2; inv H2...
+  destruct v0; simpl in H0; inv H0...
+  destruct v0; simpl in H0; inv H0...
+  destruct (eval_condition c vl m)... destruct b...
 Qed.
 
 Lemma type_of_chunk_correct:
@@ -582,332 +425,263 @@ Qed.
 
 End SOUNDNESS.
 
-(** Alternate definition of [eval_condition], [eval_op], [eval_addressing]
-  as total functions that return [Vundef] when not applicable
-  (instead of [None]).  Used in the proof of [PPCgen]. *)
+(** * Manipulating and transforming operations *)
 
-Section EVAL_OP_TOTAL.
+(** Constructing shift amounts. *)
 
-Variable F V: Type.
-Variable genv: Genv.t F V.
+Program Definition mk_shift_amount (n: int) : shift_amount :=
+  {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}.
+Next Obligation.
+  assert (0 <= Zmod (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega.
+  unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32. 
+  rewrite Int.unsigned_repr. apply zlt_true. omega. 
+  assert (32 < Int.max_unsigned). compute; auto. omega.
+Qed.
 
-Definition find_symbol_offset (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol genv id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
+Lemma mk_shift_amount_eq:
+  forall n, Int.ltu n Int.iwordsize = true -> s_amount (mk_shift_amount n) = n.
+Proof.
+  intros; simpl. unfold Int.modu. transitivity (Int.repr (Int.unsigned n)). 
+  decEq. apply Zmod_small. apply Int.ltu_inv; auto.
+  apply Int.repr_unsigned.
+Qed.
 
-Definition eval_shift_total (s: shift) (v: val) : val :=
-  match v with
-  | Vint n => Vint(eval_shift s n)
-  | _ => Vundef
+(** Recognition of move operations. *)
+
+Definition is_move_operation
+    (A: Type) (op: operation) (args: list A) : option A :=
+  match op, args with
+  | Omove, arg :: nil => Some arg
+  | _, _ => None
   end.
 
-Definition eval_condition_total (cond: condition) (vl: list val) : val :=
-  match cond, vl with
-  | Ccomp c, v1::v2::nil => Val.cmp c v1 v2
-  | Ccompu c, v1::v2::nil => Val.cmpu c v1 v2
-  | Ccompshift c s, v1::v2::nil => Val.cmp c v1 (eval_shift_total s v2)
-  | Ccompushift c s, v1::v2::nil => Val.cmpu c v1 (eval_shift_total s v2)
-  | Ccompimm c n, v1::nil => Val.cmp c v1 (Vint n)
-  | Ccompuimm c n, v1::nil => Val.cmpu c v1 (Vint n)
-  | Ccompf c, v1::v2::nil => Val.cmpf c v1 v2
-  | Cnotcompf c, v1::v2::nil => Val.notbool(Val.cmpf c v1 v2)
-  | _, _ => Vundef
+Lemma is_move_operation_correct:
+  forall (A: Type) (op: operation) (args: list A) (a: A),
+  is_move_operation op args = Some a ->
+  op = Omove /\ args = a :: nil.
+Proof.
+  intros until a. unfold is_move_operation; destruct op;
+  try (intros; discriminate).
+  destruct args. intros; discriminate.
+  destruct args. intros. intuition congruence. 
+  intros; discriminate.
+Qed.
+
+(** [negate_condition cond] returns a condition that is logically
+  equivalent to the negation of [cond]. *)
+
+Definition negate_condition (cond: condition): condition :=
+  match cond with
+  | Ccomp c => Ccomp(negate_comparison c)
+  | Ccompu c => Ccompu(negate_comparison c)
+  | Ccompshift c s => Ccompshift (negate_comparison c) s
+  | Ccompushift c s => Ccompushift (negate_comparison c) s
+  | Ccompimm c n => Ccompimm (negate_comparison c) n
+  | Ccompuimm c n => Ccompuimm (negate_comparison c) n
+  | Ccompf c => Cnotcompf c
+  | Cnotcompf c => Ccompf c
   end.
 
-Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :=
-  match op, vl with
-  | Omove, v1::nil => v1
-  | Ointconst n, nil => Vint n
-  | Ofloatconst n, nil => Vfloat n
-  | Oaddrsymbol s ofs, nil => find_symbol_offset s ofs
-  | Oaddrstack ofs, nil => Val.add sp (Vint ofs)
-  | Ocast8signed, v1::nil => Val.sign_ext 8 v1
-  | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1
-  | Ocast16signed, v1::nil => Val.sign_ext 16 v1
-  | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1
-  | Oadd, v1::v2::nil => Val.add v1 v2
-  | Oaddshift s, v1::v2::nil => Val.add v1 (eval_shift_total s v2)
-  | Oaddimm n, v1::nil => Val.add v1 (Vint n)
-  | Osub, v1::v2::nil => Val.sub v1 v2
-  | Osubshift s, v1::v2::nil => Val.sub v1 (eval_shift_total s v2)
-  | Orsubshift s, v1::v2::nil => Val.sub (eval_shift_total s v2) v1
-  | Orsubimm n, v1::nil => Val.sub (Vint n) v1
-  | Omul, v1::v2::nil => Val.mul v1 v2
-  | Odiv, v1::v2::nil => Val.divs v1 v2
-  | Odivu, v1::v2::nil => Val.divu v1 v2
-  | Oand, v1::v2::nil => Val.and v1 v2
-  | Oandshift s, v1::v2::nil => Val.and v1 (eval_shift_total s v2)
-  | Oandimm n, v1::nil => Val.and v1 (Vint n)
-  | Oor, v1::v2::nil => Val.or v1 v2
-  | Oorshift s, v1::v2::nil => Val.or v1 (eval_shift_total s v2)
-  | Oorimm n, v1::nil => Val.or v1 (Vint n)
-  | Oxor, v1::v2::nil => Val.xor v1 v2
-  | Oxorshift s, v1::v2::nil => Val.xor v1 (eval_shift_total s v2)
-  | Oxorimm n, v1::nil => Val.xor v1 (Vint n)
-  | Obic, v1::v2::nil => Val.and v1 (Val.notint v2)
-  | Obicshift s, v1::v2::nil => Val.and v1 (Val.notint (eval_shift_total s v2))
-  | Onot, v1::nil => Val.notint v1
-  | Onotshift s, v1::nil => Val.notint (eval_shift_total s v1)
-  | Oshl, v1::v2::nil => Val.shl v1 v2
-  | Oshr, v1::v2::nil => Val.shr v1 v2
-  | Oshru, v1::v2::nil => Val.shru v1 v2
-  | Oshrximm n, v1::nil => Val.shrx v1 (Vint n)
-  | Oshift s, v1::nil => eval_shift_total s v1
-  | Onegf, v1::nil => Val.negf v1
-  | Oabsf, v1::nil => Val.absf v1
-  | Oaddf, v1::v2::nil => Val.addf v1 v2
-  | Osubf, v1::v2::nil => Val.subf v1 v2
-  | Omulf, v1::v2::nil => Val.mulf v1 v2
-  | Odivf, v1::v2::nil => Val.divf v1 v2
-  | Osingleoffloat, v1::nil => Val.singleoffloat v1
-  | Ointoffloat, v1::nil => Val.intoffloat v1
-  | Ointuoffloat, v1::nil => Val.intuoffloat v1
-  | Ofloatofint, v1::nil => Val.floatofint v1
-  | Ofloatofintu, v1::nil => Val.floatofintu v1
-  | Ocmp c, _ => eval_condition_total c vl
-  | _, _ => Vundef
+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).
+Proof.
+  intros. 
+  destruct cond; simpl in H; FuncInv; simpl.
+  rewrite Val.negate_cmp_bool; rewrite H; auto.
+  rewrite Val.negate_cmpu_bool; rewrite H; auto.
+  rewrite Val.negate_cmp_bool; rewrite H; auto.
+  rewrite Val.negate_cmpu_bool; rewrite H; auto.
+  rewrite Val.negate_cmp_bool; rewrite H; auto.
+  rewrite Val.negate_cmpu_bool; rewrite H; auto.
+  rewrite H; auto.
+  destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. 
+Qed.
+
+(** Shifting stack-relative references.  This is used in [Stacking]. *)
+
+Definition shift_stack_addressing (delta: int) (addr: addressing) :=
+  match addr with
+  | Ainstack ofs => Ainstack (Int.add delta ofs)
+  | _ => addr
   end.
 
-Definition eval_addressing_total
-    (sp: val) (addr: addressing) (vl: list val) : val :=
-  match addr, vl with
-  | Aindexed n, v1::nil => Val.add v1 (Vint n)
-  | Aindexed2, v1::v2::nil => Val.add v1 v2
-  | Aindexed2shift s, v1::v2::nil => Val.add v1 (eval_shift_total s v2)
-  | Ainstack ofs, nil => Val.add sp (Vint ofs)
-  | _, _ => Vundef
+Definition shift_stack_operation (delta: int) (op: operation) :=
+  match op with
+  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
+  | _ => op
   end.
 
-Lemma eval_compare_mismatch_weaken:
-  forall c b,
-  eval_compare_mismatch c = Some b ->
-  Val.cmp_mismatch c = Val.of_bool b.
+Lemma type_shift_stack_addressing:
+  forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
 Proof.
-  unfold eval_compare_mismatch. intros. destruct c; inv H; auto.
+  intros. destruct addr; auto. 
 Qed.
 
-Lemma eval_compare_null_weaken:
-  forall c i b,
-  eval_compare_null c i = Some b ->
-  (if Int.eq i Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b.
+Lemma type_shift_stack_operation:
+  forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
 Proof.
-  unfold eval_compare_null. intros. 
-  destruct (Int.eq i Int.zero); try discriminate.
-  apply eval_compare_mismatch_weaken; auto.
+  intros. destruct op; auto.
 Qed.
 
-Lemma eval_condition_weaken:
-  forall c vl b m,
-  eval_condition c vl m = Some b ->
-  eval_condition_total c vl = Val.of_bool b.
+Lemma eval_shift_stack_addressing:
+  forall F V (ge: Genv.t F V) sp addr vl delta,
+  eval_addressing ge sp (shift_stack_addressing delta addr) vl =
+  eval_addressing ge (Val.add sp (Vint delta)) addr vl.
 Proof.
-  intros. 
-  unfold eval_condition in H; destruct c; FuncInv;
-  try subst b; try reflexivity; simpl;
-  try (apply eval_compare_null_weaken; auto).
-  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
-           Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
-  unfold eq_block in H. destruct (zeq b0 b1); try congruence.
-  apply eval_compare_mismatch_weaken; auto.
-  symmetry. apply Val.notbool_negb_1. 
+  intros. destruct addr; simpl; auto.
+  rewrite Val.add_assoc. simpl. auto.
 Qed.
 
-Lemma eval_operation_weaken:
-  forall sp op vl v m,
-  eval_operation genv sp op vl m = Some v ->
-  eval_operation_total sp op vl = v.
+Lemma eval_shift_stack_operation:
+  forall F V (ge: Genv.t F V) sp op vl m delta,
+  eval_operation ge sp (shift_stack_operation delta op) vl m =
+  eval_operation ge (Val.add sp (Vint delta)) op vl m.
 Proof.
-  intros.
-  unfold eval_operation in H; destruct op; FuncInv;
-  try subst v; try reflexivity; simpl.
-  unfold find_symbol_offset. 
-  destruct (Genv.find_symbol genv i); try discriminate.
-  congruence.
-  unfold offset_sp in H. 
-  destruct sp; try discriminate. simpl. congruence.
-  unfold eq_block in H. destruct (zeq b b0); congruence.
-  destruct (Int.eq i0 Int.zero); congruence.
-  destruct (Int.eq i0 Int.zero); congruence.
-  destruct (Int.ltu i0 Int.iwordsize); congruence.
-  destruct (Int.ltu i0 Int.iwordsize); congruence.
-  destruct (Int.ltu i0 Int.iwordsize); congruence.
-  unfold Int.ltu in H. destruct (zlt (Int.unsigned i) (Int.unsigned (Int.repr 31))).
-  unfold Int.ltu. rewrite zlt_true. congruence. 
-  assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
-  omega. discriminate.
-  destruct (Float.intoffloat f); simpl in H; inv H. auto.
-  destruct (Float.intuoffloat f); simpl in H; inv H. auto.
-  caseEq (eval_condition c vl m); intros; rewrite H0 in H.
-  replace v with (Val.of_bool b).
-  eapply eval_condition_weaken; eauto.
-  destruct b; simpl; congruence.
-  discriminate.
+  intros. destruct op; simpl; auto.
+  rewrite Val.add_assoc. simpl. auto.
 Qed.
 
-Lemma eval_addressing_weaken:
-  forall sp addr vl v,
-  eval_addressing genv sp addr vl = Some v ->
-  eval_addressing_total sp addr vl = v.
+(** Transformation of addressing modes with two operands or more
+  into an equivalent arithmetic operation.  This is used in the [Reload]
+  pass when a store instruction cannot be reloaded directly because
+  it runs out of temporary registers. *)
+
+(** For the ARM, there are only two binary addressing mode: [Aindexed2]
+  and [Aindexed2shift].  The corresponding operations are [Oadd]
+  and [Oaddshift]. *)
+
+Definition op_for_binary_addressing (addr: addressing) : operation :=
+  match addr with
+  | Aindexed2 => Oadd
+  | Aindexed2shift s => Oaddshift s
+  | _ => Ointconst Int.zero (* never happens *)
+  end.
+
+Lemma eval_op_for_binary_addressing:
+  forall (F V: Type) (ge: Genv.t F V) sp addr args v m,
+  (length args >= 2)%nat ->
+  eval_addressing ge sp addr args = Some v ->
+  eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
 Proof.
   intros.
-  unfold eval_addressing in H; destruct addr; FuncInv;
-  try subst v; simpl; try reflexivity.
-  decEq. apply Int.add_commut.
-  unfold offset_sp in H. destruct sp; simpl; congruence.
+  unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl.
+  congruence.
+  congruence.
 Qed.
 
-Lemma eval_condition_total_is_bool:
-  forall cond vl, Val.is_bool (eval_condition_total cond vl).
+Lemma type_op_for_binary_addressing:
+  forall addr,
+  (length (type_of_addressing addr) >= 2)%nat ->
+  type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint).
 Proof.
-  intros; destruct cond;
-  destruct vl; try apply Val.undef_is_bool;
-  destruct vl; try apply Val.undef_is_bool;
-  try (destruct vl; try apply Val.undef_is_bool); simpl.
-  apply Val.cmp_is_bool.
-  apply Val.cmpu_is_bool.
-  apply Val.cmp_is_bool.
-  apply Val.cmpu_is_bool.
-  apply Val.cmp_is_bool.
-  apply Val.cmpu_is_bool.
-  apply Val.cmpf_is_bool.
-  apply Val.notbool_is_bool.
+  intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
 Qed.
 
-End EVAL_OP_TOTAL.
-
-(** Compatibility of the evaluation functions with the
-    ``is less defined'' relation over values and memory states. *)
+(** Two-address operations.  There are none in the ARM architecture. *)
 
-Section EVAL_LESSDEF.
+Definition two_address_op (op: operation) : bool := false.
 
-Variable F V: Type.
-Variable genv: Genv.t F V.
+(** Operations that are so cheap to recompute that CSE should not factor them out. *)
 
-Ltac InvLessdef :=
-  match goal with
-  | [ H: Val.lessdef (Vint _) _ |- _ ] =>
-      inv H; InvLessdef
-  | [ H: Val.lessdef (Vfloat _) _ |- _ ] =>
-      inv H; InvLessdef
-  | [ H: Val.lessdef (Vptr _ _) _ |- _ ] =>
-      inv H; InvLessdef
-  | [ H: Val.lessdef_list nil _ |- _ ] =>
-      inv H; InvLessdef
-  | [ H: Val.lessdef_list (_ :: _) _ |- _ ] =>
-      inv H; InvLessdef
-  | _ => idtac
+Definition is_trivial_op (op: operation) : bool :=
+  match op with
+  | Omove => true
+  | Ointconst _ => true
+  | Oaddrstack _ => true
+  | _ => false
   end.
 
-Lemma eval_condition_lessdef:
-  forall cond vl1 vl2 b m1 m2,
-  Val.lessdef_list vl1 vl2 ->
-  Mem.extends m1 m2 ->
-  eval_condition cond vl1 m1 = Some b ->
-  eval_condition cond vl2 m2 = Some b.
-Proof.
-  intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned i) &&
-            Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate.
-  destruct (andb_prop _ _ Heqb2) as [A B].
-  assert (forall b ofs, Mem.valid_pointer m1 b ofs = true -> Mem.valid_pointer m2 b ofs = true).
-    intros until ofs. repeat rewrite Mem.valid_pointer_nonempty_perm. 
-    apply Mem.perm_extends; auto.
-  rewrite (H _ _ A). rewrite (H _ _ B). auto. 
-Qed.
+(** Operations that depend on the memory state. *)
 
-Ltac TrivialExists :=
-  match goal with
-  | [ |- exists v2, Some ?v1 = Some v2 /\ Val.lessdef ?v1 v2 ] =>
-      exists v1; split; [auto | constructor]
-  | _ => idtac
+Definition op_depends_on_memory (op: operation) : bool :=
+  match op with
+  | Ocmp (Ccompu _ | Ccompushift _ _) => true
+  | _ => false
   end.
 
-Lemma eval_operation_lessdef:
-  forall sp op vl1 vl2 v1 m1 m2,
-  Val.lessdef_list vl1 vl2 ->
-  Mem.extends m1 m2 ->
-  eval_operation genv sp op vl1 m1 = Some v1 ->
-  exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
-Proof.
-  intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists.
-  exists v2; auto.
-  destruct (Genv.find_symbol genv i); inv H1. TrivialExists.
-  exists v1; auto. 
-  exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto.
-  exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto.
-  exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto.
-  exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto.
-  destruct (eq_block b b0); inv H1. TrivialExists.
-  destruct (Int.eq i0 Int.zero); inv H1; TrivialExists.
-  destruct (Int.eq i0 Int.zero); inv H1; TrivialExists.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
-  destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists.
-  destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists.
-  destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists.
-  destruct (Int.ltu i (Int.repr 31)); inv H1; TrivialExists.
-  exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
-  destruct (Float.intoffloat f); simpl in *; inv H1. TrivialExists.
-  destruct (Float.intuoffloat f); simpl in *; inv H1. TrivialExists.
-  exists v1; split; auto. 
-  destruct (eval_condition c vl1 m1) as [] _eqn. 
-  rewrite (eval_condition_lessdef c H H0 Heqo).
-  auto.
-  discriminate.
-Qed.
-
-Lemma eval_addressing_lessdef:
-  forall sp addr vl1 vl2 v1,
-  Val.lessdef_list vl1 vl2 ->
-  eval_addressing genv sp addr vl1 = Some v1 ->
-  exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2.
+Lemma op_depends_on_memory_correct:
+  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
+  op_depends_on_memory op = false ->
+  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros. destruct addr; simpl in *; FuncInv; InvLessdef; TrivialExists.
-  exists v1; auto.
+  intros until m2. destruct op; simpl; try congruence.
+  intros. destruct c; simpl; auto; congruence.
 Qed.
 
-End EVAL_LESSDEF.
+(** * Invariance and compatibility properties. *)
 
-(** Shifting stack-relative references.  This is used in [Stacking]. *)
+(** [eval_operation] and [eval_addressing] depend on a global environment
+  for resolving references to global symbols.  We show that they give
+  the same results if a global environment is replaced by another that
+  assigns the same addresses to the same symbols. *)
 
-Definition shift_stack_addressing (delta: int) (addr: addressing) :=
-  match addr with
-  | Ainstack ofs => Ainstack (Int.add delta ofs)
-  | _ => addr
-  end.
+Section GENV_TRANSF.
 
-Definition shift_stack_operation (delta: int) (op: operation) :=
-  match op with
-  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
-  | _ => op
-  end.
+Variable F1 F2 V1 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
+Hypothesis agree_on_symbols:
+  forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
 
-Lemma type_shift_stack_addressing:
-  forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
+Lemma eval_operation_preserved:
+  forall sp op vl m,
+  eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
 Proof.
-  intros. destruct addr; auto. 
+  intros.
+  unfold eval_operation; destruct op; auto. 
+  unfold symbol_address. rewrite agree_on_symbols; auto.
 Qed.
 
-Lemma type_shift_stack_operation:
-  forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
+Lemma eval_addressing_preserved:
+  forall sp addr vl,
+  eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl.
 Proof.
-  intros. destruct op; auto.
+  intros.
+  assert (UNUSED: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s).
+  exact agree_on_symbols.
+  unfold eval_addressing; destruct addr; auto.
 Qed.
 
-(** Compatibility of the evaluation functions with memory injections. *)
+End GENV_TRANSF.
 
-Section EVAL_INJECT.
+(** Compatibility of the evaluation functions with value injections. *)
+
+Section EVAL_COMPAT.
 
 Variable F V: Type.
 Variable genv: Genv.t F V.
 Variable f: meminj.
-Hypothesis globals: meminj_preserves_globals genv f.
-Variable sp1: block.
-Variable sp2: block.
-Variable delta: Z.
-Hypothesis sp_inj: f sp1 = Some(sp2, delta).
+
+Hypothesis symbol_address_inj: 
+  forall id ofs,
+  val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+
+Variable m1: mem.
+Variable m2: mem.
+
+Hypothesis valid_pointer_inj:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+
+Hypothesis valid_different_pointers_inj:
+  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+  b1 <> b2 ->
+  Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true ->
+  Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true ->
+  f b1 = Some (b1', delta1) ->
+  f b2 = Some (b2', delta2) ->
+  b1' <> b2' \/
+  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
 
 Ltac InvInject :=
   match goal with
@@ -924,202 +698,330 @@ Ltac InvInject :=
   | _ => idtac
   end.
 
-Lemma eval_condition_inject:
-  forall cond vl1 vl2 b m1 m2,
+Remark val_add_inj:
+  forall v1 v1' v2 v2',
+  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
+Proof.
+  intros. inv H; inv H0; simpl; econstructor; eauto. 
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+Qed.
+
+Remark val_sub_inj:
+  forall v1 v1' v2 v2',
+  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.sub v1 v2) (Val.sub v1' v2').
+Proof.
+  intros. inv H; inv H0; simpl; auto.
+  econstructor; eauto. rewrite Int.sub_add_l. auto.
+  destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true. 
+  rewrite Int.sub_shifted. auto.
+Qed.
+
+Remark eval_shift_inj:
+  forall s v v', val_inject f v v' -> val_inject f (eval_shift s v) (eval_shift s v').
+Proof.
+  intros. inv H; destruct s; simpl; auto; rewrite s_range; auto. 
+Qed.
+
+Lemma eval_condition_inj:
+  forall cond vl1 vl2 b,
   val_list_inject f vl1 vl2 ->
-  Mem.inject f m1 m2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
-  intros. destruct cond; simpl in *; FuncInv; InvInject; auto.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned i)) as [] _eqn; try discriminate.
-  destruct (Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate.
-  simpl in H1.
-  exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. 
-  intros V1. rewrite V1.
-  exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb2. econstructor; eauto. 
-  intros V2. rewrite V2.
-  simpl. 
-  destruct (eq_block b0 b1); inv H1.
-  rewrite H3 in H5; inv H5. rewrite dec_eq_true.
+Opaque Int.add.
+  assert (CMP:
+    forall c v1 v2 v1' v2' b,
+    val_inject f v1 v1' ->
+    val_inject f v2 v2' ->
+    Val.cmp_bool c v1 v2 = Some b ->
+    Val.cmp_bool c v1' v2' = Some b).
+  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
+
+  assert (CMPU:
+    forall c v1 v2 v1' v2' b,
+    val_inject f v1 v1' ->
+    val_inject f v2 v2' ->
+    Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
+    Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
+  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
+  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) as []_eqn; try discriminate.
+  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) as []_eqn; try discriminate.
+  rewrite (valid_pointer_inj _ H2 Heqb4).
+  rewrite (valid_pointer_inj _ H Heqb0). simpl.
+  destruct (zeq b1 b0); simpl in H1.
+  inv H1. rewrite H in H2; inv H2. rewrite zeq_true. 
   decEq. apply Int.translate_cmpu.
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  exploit Mem.different_pointers_inject; eauto. intros P.
-  destruct (eq_block b3 b4); auto.
-  destruct P. contradiction.
-  destruct c; unfold eval_compare_mismatch in *; inv H2. 
-  unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. 
-  unfold Int.cmpu. rewrite Int.eq_false; auto. congruence.
+  eapply valid_pointer_no_overflow; eauto.
+  eapply valid_pointer_no_overflow; eauto.
+  exploit valid_different_pointers_inj; eauto. intros P.
+  destruct (zeq b2 b3); auto.
+  destruct P. congruence. 
+  destruct c; simpl in H1; inv H1.
+  simpl; decEq. rewrite Int.eq_false; auto. congruence.
+  simpl; decEq. rewrite Int.eq_false; auto. congruence.
+
+  intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl.
+  eapply CMP; eauto.
+  eapply CMPU; eauto.
+  eapply CMP. eauto. eapply eval_shift_inj. eauto. auto.
+  eapply CMPU. eauto. eapply eval_shift_inj. eauto. auto.
+  eapply CMP; eauto. 
+  eapply CMPU; eauto.
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+  inv H3; inv H2; simpl in H0; inv H0; auto.
 Qed.
 
-Ltac TrivialExists2 :=
+Ltac TrivialExists :=
   match goal with
   | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] =>
-      exists v1; split; [auto | econstructor; eauto]
+      exists v1; split; auto
   | _ => idtac
   end.
 
-Lemma eval_addressing_inject:
-  forall addr vl1 vl2 v1,
+Lemma eval_operation_inj:
+  forall op sp1 vl1 sp2 vl2 v1,
+  val_inject f sp1 sp2 ->
   val_list_inject f vl1 vl2 ->
-  eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
-  exists v2, 
-     eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
-  /\ val_inject f v1 v2.
+  eval_operation genv sp1 op vl1 m1 = Some v1 ->
+  exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
 Proof.
-  assert (UNUSED: meminj_preserves_globals genv f). exact globals.
-  intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists2.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. 
-  repeat rewrite Int.add_assoc. auto.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. 
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  apply val_add_inj; auto.
+  apply val_add_inj; auto.
+  apply val_add_inj; auto. apply eval_shift_inj; auto.
+  apply val_add_inj; auto.
+
+  apply val_sub_inj; auto.
+  apply val_sub_inj; auto. apply eval_shift_inj; auto.
+  apply val_sub_inj; auto. apply eval_shift_inj; auto.
+  apply (@val_sub_inj (Vint i) (Vint i) v v'); auto.
+
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H3; simpl in H1; inv H1. simpl. 
+    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+  inv H4; inv H3; simpl in H1; inv H1. simpl. 
+    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+
+  inv H4; inv H2; simpl; auto.
+  exploit (eval_shift_inj s). eexact H2. intros IS. inv H4; inv IS; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  exploit (eval_shift_inj s). eexact H2. intros IS. inv H4; inv IS; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  exploit (eval_shift_inj s). eexact H2. intros IS. inv H4; inv IS; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  exploit (eval_shift_inj s). eexact H2. intros IS. inv H4; inv IS; simpl; auto.
+
+  inv H4; simpl; auto.
+  exploit (eval_shift_inj s). eexact H4. intros IS. inv IS; simpl; auto.
+
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
+  apply eval_shift_inj; auto.
+  inv H4; simpl in H1; inv H1. simpl. destruct (Int.ltu i (Int.repr 31)); inv H2. TrivialExists.
+
+  inv H4; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+
+  inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2.
+  exists (Vint i); auto.
+  inv H4; simpl in H1; inv H1. simpl. destruct (Float.intuoffloat f0); simpl in H2; inv H2.
+  exists (Vint i); auto.
+  inv H4; simpl in *; inv H1. TrivialExists.
+  inv H4; simpl in *; inv H1. TrivialExists.
+
+  subst v1. destruct (eval_condition c vl1 m1) as []_eqn.
+  exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
+  destruct b; simpl; constructor.
+  simpl; constructor.
 Qed.
 
-Lemma eval_operation_inject:
-  forall op vl1 vl2 v1 m1 m2,
+Lemma eval_addressing_inj:
+  forall addr sp1 vl1 sp2 vl2 v1,
+  val_inject f sp1 sp2 ->
   val_list_inject f vl1 vl2 ->
-  Mem.inject f m1 m2 ->
-  eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
-  exists v2,
-     eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
-  /\ val_inject f v1 v2.
+  eval_addressing genv sp1 addr vl1 = Some v1 ->
+  exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
 Proof.
-  intros. destruct op; simpl in *; FuncInv; InvInject; TrivialExists2.
-  exists v'; auto.
-  destruct (Genv.find_symbol genv i) as [] _eqn; inv H1.
-  TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  exists (Val.sign_ext 8 v'); split; auto. inv H4; simpl; auto.
-  exists (Val.zero_ext 8 v'); split; auto. inv H4; simpl; auto.
-  exists (Val.sign_ext 16 v'); split; auto. inv H4; simpl; auto.
-  exists (Val.zero_ext 16 v'); split; auto. inv H4; simpl; auto.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  rewrite Int.sub_add_l. auto.
-  destruct (eq_block b b0); inv H1. rewrite H3 in H5; inv H5. rewrite dec_eq_true.
-  rewrite Int.sub_shifted. TrivialExists2.
-  rewrite Int.sub_add_l. auto.
-  destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2.
-  destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
-  destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists2.
-  exists (Val.singleoffloat v'); split; auto. inv H4; simpl; auto.
-  destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists2.
-  destruct (Float.intuoffloat f0); simpl in *; inv H1. TrivialExists2.
-  destruct (eval_condition c vl1 m1) as [] _eqn; try discriminate.
-  exploit eval_condition_inject; eauto. intros EQ; rewrite EQ. 
-  destruct b; inv H1; TrivialExists2.
+  assert (UNUSED: forall id ofs,
+            val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs)).
+  exact symbol_address_inj.
+  intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  apply val_add_inj; auto.
+  apply val_add_inj; auto.
+  apply val_add_inj; auto. apply eval_shift_inj; auto.
+  apply val_add_inj; auto.
 Qed.
 
-End EVAL_INJECT.
+End EVAL_COMPAT.
 
-(** Recognition of integers that are valid shift amounts. *)
+(** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *)
 
-Definition is_shift_amount_aux (n: int) :
-  { Int.ltu n Int.iwordsize = true } +
-  { Int.ltu n Int.iwordsize = false }.
-Proof.
-   case (Int.ltu n Int.iwordsize). left; auto. right; auto.
-Defined.
+Section EVAL_LESSDEF.
 
-Definition is_shift_amount (n: int) : option shift_amount :=
-  match is_shift_amount_aux n with
-  | left H => Some(mk_shift_amount n H)
-  | right _ => None
-  end.
+Variable F V: Type.
+Variable genv: Genv.t F V.
 
-Lemma is_shift_amount_Some:
-  forall n s, is_shift_amount n = Some s -> s_amount s = n.
+Remark valid_pointer_extends:
+  forall m1 m2, Mem.extends m1 m2 ->
+  forall b1 ofs b2 delta,
+  Some(b1, 0) = Some(b2, delta) ->
+  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 Proof.
-  intros until s. unfold is_shift_amount. 
-  destruct (is_shift_amount_aux n). 
-  simpl. intros. inv H. reflexivity.
-  congruence.
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. 
 Qed.
 
-Lemma is_shift_amount_None:
-  forall n, is_shift_amount n = None -> Int.ltu n Int.iwordsize = true -> False.
+Remark valid_pointer_no_overflow_extends:
+  forall m1 b1 ofs b2 delta,
+  Some(b1, 0) = Some(b2, delta) ->
+  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
-  intro n. unfold is_shift_amount.
-  destruct (is_shift_amount_aux n). 
-  congruence.
-  congruence.
+  intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
 Qed.
 
-(** Transformation of addressing modes with two operands or more
-  into an equivalent arithmetic operation.  This is used in the [Reload]
-  pass when a store instruction cannot be reloaded directly because
-  it runs out of temporary registers. *)
-
-(** For the ARM, there are only two binary addressing mode: [Aindexed2]
-  and [Aindexed2shift].  The corresponding operations are [Oadd]
-  and [Oaddshift]. *)
+Remark valid_different_pointers_extends:
+  forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+  b1 <> b2 ->
+  Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true ->
+  Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true ->
+  Some(b1, 0) = Some (b1', delta1) ->
+  Some(b2, 0) = Some (b2', delta2) ->
+  b1' <> b2' \/
+  Int.unsigned(Int.add ofs1 (Int.repr delta1)) <> Int.unsigned(Int.add ofs2 (Int.repr delta2)).
+Proof.
+  intros. inv H2; inv H3. auto.
+Qed.
 
-Definition op_for_binary_addressing (addr: addressing) : operation :=
-  match addr with
-  | Aindexed2 => Oadd
-  | Aindexed2shift s => Oaddshift s
-  | _ => Ointconst Int.zero (* never happens *)
-  end.
+Lemma eval_condition_lessdef:
+  forall cond vl1 vl2 b m1 m2,
+  Val.lessdef_list vl1 vl2 ->
+  Mem.extends m1 m2 ->
+  eval_condition cond vl1 m1 = Some b ->
+  eval_condition cond vl2 m2 = Some b.
+Proof.
+  intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
+  apply valid_pointer_extends; auto.
+  apply valid_pointer_no_overflow_extends; auto. 
+  apply valid_different_pointers_extends; auto.
+  rewrite <- val_list_inject_lessdef. eauto. auto.
+Qed.
 
-Lemma eval_op_for_binary_addressing:
-  forall (F V: Type) (ge: Genv.t F V) sp addr args v m,
-  (length args >= 2)%nat ->
-  eval_addressing ge sp addr args = Some v ->
-  eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
+Lemma eval_operation_lessdef:
+  forall sp op vl1 vl2 v1 m1 m2,
+  Val.lessdef_list vl1 vl2 ->
+  Mem.extends m1 m2 ->
+  eval_operation genv sp op vl1 m1 = Some v1 ->
+  exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros.
-  unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl.
-  rewrite Int.add_commut. congruence.
-  congruence.
-  congruence.
+  intros. rewrite val_list_inject_lessdef in H.
+  assert (exists v2 : val,
+          eval_operation genv sp op vl2 m2 = Some v2
+          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+  eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
+  intros. rewrite <- val_inject_lessdef; auto.
+  apply valid_pointer_extends; auto.
+  apply valid_pointer_no_overflow_extends; auto. 
+  apply valid_different_pointers_extends; auto.
+  rewrite <- val_inject_lessdef; auto.
+  eauto. auto. 
+  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
 Qed.
 
-Lemma type_op_for_binary_addressing:
-  forall addr,
-  (length (type_of_addressing addr) >= 2)%nat ->
-  type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint).
+Lemma eval_addressing_lessdef:
+  forall sp addr vl1 vl2 v1,
+  Val.lessdef_list vl1 vl2 ->
+  eval_addressing genv sp addr vl1 = Some v1 ->
+  exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
+  intros. rewrite val_list_inject_lessdef in H.
+  assert (exists v2 : val,
+          eval_addressing genv sp addr vl2 = Some v2
+          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+  eapply eval_addressing_inj with (sp1 := sp).
+  intros. rewrite <- val_inject_lessdef; auto. 
+  rewrite <- val_inject_lessdef; auto. 
+  eauto. auto. 
+  destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
 Qed.
 
-(** Two-address operations.  There are none in the ARM architecture. *)
+End EVAL_LESSDEF.
 
-Definition two_address_op (op: operation) : bool := false.
+(** Compatibility of the evaluation functions with memory injections. *)
 
-(** Operations that are so cheap to recompute that CSE should not factor them out. *)
+Section EVAL_INJECT.
 
-Definition is_trivial_op (op: operation) : bool :=
-  match op with
-  | Omove => true
-  | Ointconst _ => true
-  | Oaddrsymbol _ _ => true
-  | Oaddrstack _ => true
-  | _ => false
-  end.
+Variable F V: Type.
+Variable genv: Genv.t F V.
+Variable f: meminj.
+Hypothesis globals: meminj_preserves_globals genv f.
+Variable sp1: block.
+Variable sp2: block.
+Variable delta: Z.
+Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
+Remark symbol_address_inject:
+  forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+Proof.
+  intros. unfold symbol_address. destruct (Genv.find_symbol genv id) as []_eqn; auto.
+  exploit (proj1 globals); eauto. intros. 
+  econstructor; eauto. rewrite Int.add_zero; auto.
+Qed.
 
-(** Operations that depend on the memory state. *)
+Lemma eval_condition_inject:
+  forall cond vl1 vl2 b m1 m2,
+  val_list_inject f vl1 vl2 ->
+  Mem.inject f m1 m2 ->
+  eval_condition cond vl1 m1 = Some b ->
+  eval_condition cond vl2 m2 = Some b.
+Proof.
+  intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
+  intros; eapply Mem.valid_pointer_inject_val; eauto.
+  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.different_pointers_inject; eauto.
+Qed.
 
-Definition op_depends_on_memory (op: operation) : bool :=
-  match op with
-  | Ocmp (Ccompu _) => true
-  | _ => false
-  end.
+Lemma eval_addressing_inject:
+  forall addr vl1 vl2 v1,
+  val_list_inject f vl1 vl2 ->
+  eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
+  exists v2, 
+     eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
+  /\ val_inject f v1 v2.
+Proof.
+  intros. 
+  rewrite eval_shift_stack_addressing. simpl.
+  eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto.
+  exact symbol_address_inject.
+Qed.
 
-Lemma op_depends_on_memory_correct:
-  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
-  op_depends_on_memory op = false ->
-  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
+Lemma eval_operation_inject:
+  forall op vl1 vl2 v1 m1 m2,
+  val_list_inject f vl1 vl2 ->
+  Mem.inject f m1 m2 ->
+  eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
+  exists v2,
+     eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
+  /\ val_inject f v1 v2.
 Proof.
-  intros until m2. destruct op; simpl; try congruence.
-  destruct c; simpl; congruence.
+  intros. 
+  rewrite eval_shift_stack_operation. simpl.
+  eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
+  exact symbol_address_inject.
+  intros; eapply Mem.valid_pointer_inject_val; eauto.
+  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
+End EVAL_INJECT.