Merge of branch value-analysis.

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

9 files changed, 720 insertions, 504 deletions

diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
index 07d5a79..ca54ba1 100644
--- a/ia32/CombineOp.v
+++ b/ia32/CombineOp.v
@@ -17,14 +17,10 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
 Require Import Op.
-Require SelectOp.
+Require Import CSEdomain.
 
 Definition valnum := positive.
 
-Inductive rhs : Type :=
-  | Op: operation -> list valnum -> rhs
-  | Load: memory_chunk -> addressing -> list valnum -> rhs.
-
 Section COMBINE.
 
 Variable get: valnum -> option rhs.
@@ -80,7 +76,7 @@ Function combine_addr (addr: addressing) (args: list valnum) : option(addressing
   match addr, args with
   | Aindexed n, x::nil =>
       match get x with
-      | Some(Op (Olea a) ys) => Some(SelectOp.offset_addressing a n, ys)
+      | Some(Op (Olea a) ys) => Some(offset_addressing_total a n, ys)
       | _ => None
       end
   | _, _ => None
@@ -93,6 +89,21 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       | Some(addr', args') => Some(Olea addr', args')
       | None => None
       end
+  | Oandimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
+      | _ => None
+      end
+  | Oorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
+      | _ => None
+      end
+  | Oxorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
+      | _ => None
+      end
   | Ocmp cond, _ =>
       match combine_cond cond args with
       | Some(cond', args') => Some(Ocmp cond', args')
diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v
index d4565bd..1e5b932 100644
--- a/ia32/CombineOpproof.v
+++ b/ia32/CombineOpproof.v
@@ -19,8 +19,8 @@ Require Import Values.
 Require Import Memory.
 Require Import Op.
 Require Import RTL.
+Require Import CSEdomain.
 Require Import CombineOp.
-Require Import CSE.
 
 Section COMBINE.
 
@@ -29,8 +29,20 @@ Variable sp: val.
 Variable m: mem.
 Variable get: valnum -> option rhs.
 Variable valu: valnum -> val.
-Hypothesis get_sound: forall v rhs, get v = Some rhs -> equation_holds valu ge sp m v rhs.
+Hypothesis get_sound: forall v rhs, get v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v).
 
+Lemma get_op_sound:
+  forall v op vl, get v = Some (Op op vl) -> eval_operation ge sp op (map valu vl) m = Some (valu v).
+Proof.
+  intros. exploit get_sound; eauto. intros REV; inv REV; auto. 
+Qed.
+
+Ltac UseGetSound :=
+  match goal with
+  | [ H: get _ = Some _ |- _ ] =>
+      let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv)
+  end.
+  
 Lemma combine_compimm_ne_0_sound:
   forall x cond args,
   combine_compimm_ne_0 get x = Some(cond, args) ->
@@ -39,12 +51,11 @@ Lemma combine_compimm_ne_0_sound:
 Proof.
   intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ.
   (* of cmp *)
-  exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. 
+  UseGetSound. rewrite <- H. 
   destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
   (* of and *)
-  exploit get_sound; eauto. unfold equation_holds; simpl. 
-  destruct args; try discriminate. destruct args; try discriminate. simpl. 
-  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+  UseGetSound. rewrite <- H. 
+  destruct v; simpl; auto. 
 Qed.
 
 Lemma combine_compimm_eq_0_sound:
@@ -55,13 +66,11 @@ Lemma combine_compimm_eq_0_sound:
 Proof.
   intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ.
   (* of cmp *)
-  exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. 
+  UseGetSound. rewrite <- H.
   rewrite eval_negate_condition. 
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
   (* of and *)
-  exploit get_sound; eauto. unfold equation_holds; simpl. 
-  destruct args; try discriminate. destruct args; try discriminate. simpl. 
-  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+  UseGetSound. rewrite <- H. destruct v; auto. 
 Qed.
 
 Lemma combine_compimm_eq_1_sound:
@@ -72,7 +81,7 @@ Lemma combine_compimm_eq_1_sound:
 Proof.
   intros until args. functional induction (combine_compimm_eq_1 get x); intros EQ; inv EQ.
   (* of cmp *)
-  exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. 
+  UseGetSound. rewrite <- H. 
   destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
 Qed.
 
@@ -84,7 +93,7 @@ Lemma combine_compimm_ne_1_sound:
 Proof.
   intros until args. functional induction (combine_compimm_ne_1 get x); intros EQ; inv EQ.
   (* of cmp *)
-  exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. 
+  UseGetSound. rewrite <- H. 
   rewrite eval_negate_condition.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
 Qed.
@@ -119,22 +128,8 @@ Theorem combine_addr_sound:
   eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
 Proof.
   intros. functional inversion H; subst.
-  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ.
-  assert (forall vl,
-         eval_addressing ge sp (SelectOp.offset_addressing a n) vl =
-         option_map (fun v => Val.add v (Vint n)) (eval_addressing ge sp a vl)).
-    intros. destruct a; simpl; repeat (destruct vl; auto); simpl. 
-    rewrite Val.add_assoc. auto. 
-    repeat rewrite Val.add_assoc. auto.
-    rewrite Val.add_assoc. auto.
-    repeat rewrite Val.add_assoc. auto.
-    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto. 
-    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto.
-      repeat rewrite <- (Val.add_commut v). rewrite Val.add_assoc. auto. 
-    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i0); auto.
-      repeat rewrite <- (Val.add_commut (Val.mul v (Vint i))). rewrite Val.add_assoc. auto.
-    rewrite Val.add_assoc; auto.
-  rewrite H0. rewrite EQ. auto. 
+  (* indexed - lea *)
+  UseGetSound. simpl. eapply eval_offset_addressing_total; eauto. 
 Qed.
 
 Theorem combine_op_sound:
@@ -143,8 +138,14 @@ Theorem combine_op_sound:
   eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
 Proof.
   intros. functional inversion H; subst.
-(* lea *)
+(* lea-lea *)
   simpl. eapply combine_addr_sound; eauto. 
+(* andimm - andimm *)
+  UseGetSound; simpl. rewrite <- H0. rewrite Val.and_assoc. auto.
+(* orimm - orimm *)
+  UseGetSound; simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
+(* xorimm - xorimm *)
+  UseGetSound; simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
 (* cmp *)
   simpl. decEq; decEq. eapply combine_cond_sound; eauto.
 Qed.
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 8c3a7fa..396c94c 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -10,8 +10,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Static analysis and strength reduction for operators 
-  and conditions.  This is the machine-dependent part of [Constprop]. *)
+(** Strength reduction for operators and conditions.
+    This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
 Require Import AST.
@@ -19,141 +19,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Op.
 Require Import Registers.
-
-(** * Static analysis *)
-
-(** To each pseudo-register at each program point, the static analysis 
-  associates a compile-time approximation taken from the following set. *)
-
-Inductive approx : Type :=
-  | Novalue: approx      (** No value possible, code is unreachable. *)
-  | Unknown: approx      (** All values are possible,
-                             no compile-time information is available. *)
-  | I: int -> approx     (** A known integer value. *)
-  | F: float -> approx   (** A known floating-point value. *)
-  | L: int64 -> approx   (** A know 64-bit integer value. *)
-  | G: ident -> int -> approx
-                         (** The value is the address of the given global
-                             symbol plus the given integer offset. *)
-  | S: int -> approx.    (** The value is the stack pointer plus the offset. *)
-
-(** We now define the abstract interpretations of conditions and operators
-  over this set of approximations.  For instance, the abstract interpretation
-  of the operator [Oaddf] applied to two expressions [a] and [b] is
-  [F(Float.add f g)] if [a] and [b] have static approximations [Vfloat f]
-  and [Vfloat g] respectively, and [Unknown] otherwise.
-
-  The static approximations are defined by large pattern-matchings over
-  the approximations of the results.  We write these matchings in the
-  indirect style described in file [SelectOp] to avoid excessive
-  duplication of cases in proofs. *)
-
-Nondetfunction eval_static_condition (cond: condition) (vl: list approx) :=
-  match cond, vl with
-  | Ccomp c, I n1 :: I n2 :: nil => Some(Int.cmp c n1 n2)
-  | Ccompu c, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 n2)
-  | Ccompimm c n, I n1 :: nil => Some(Int.cmp c n1 n)
-  | Ccompuimm c n, I n1 :: nil => Some(Int.cmpu c n1 n)
-  | Ccompf c, F n1 :: F n2 :: nil => Some(Float.cmp c n1 n2)
-  | Cnotcompf c, F n1 :: F n2 :: nil => Some(negb(Float.cmp c n1 n2))
-  | Cmaskzero n, I n1 :: nil => Some(Int.eq (Int.and n1 n) Int.zero)
-  | Cmasknotzero n, I n1::nil => Some(negb(Int.eq (Int.and n1 n) Int.zero))
-  | _, _ => None
-  end.
-
-Definition eval_static_condition_val (cond: condition) (vl: list approx) :=
-  match eval_static_condition cond vl with
-  | None => Unknown
-  | Some b => I(if b then Int.one else Int.zero)
-  end.
-
-Definition eval_static_intoffloat (f: float) :=
-  match Float.intoffloat f with Some x => I x | None => Unknown end.
-
-Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) :=
-  match addr, vl with
-  | Aindexed n, I n1::nil => I (Int.add n1 n)
-  | Aindexed n, G id ofs::nil => G id (Int.add ofs n)
-  | Aindexed n, S ofs::nil => S (Int.add ofs n)
-  | Aindexed2 n, I n1::I n2::nil => I (Int.add (Int.add n1 n2) n)
-  | Aindexed2 n, G id ofs::I n2::nil => G id (Int.add (Int.add ofs n2) n)
-  | Aindexed2 n, I n1::G id ofs::nil => G id (Int.add (Int.add ofs n1) n)
-  | Aindexed2 n, S ofs::I n2::nil => S (Int.add (Int.add ofs n2) n)
-  | Aindexed2 n, I n1::S ofs::nil => S (Int.add (Int.add ofs n1) n)
-  | Ascaled sc n, I n1::nil => I (Int.add (Int.mul n1 sc) n)
-  | Aindexed2scaled sc n, I n1::I n2::nil => I (Int.add n1 (Int.add (Int.mul n2 sc) n))
-  | Aindexed2scaled sc n, G id ofs::I n2::nil => G id (Int.add ofs (Int.add (Int.mul n2 sc) n))
-  | Aindexed2scaled sc n, S ofs::I n2::nil => S (Int.add ofs (Int.add (Int.mul n2 sc) n))
-  | Aglobal id ofs, nil => G id ofs
-  | Abased id ofs, I n1::nil => G id (Int.add ofs n1)
-  | Abasedscaled sc id ofs, I n1::nil => G id (Int.add ofs (Int.mul sc n1))
-  | Ainstack ofs, nil => S ofs
-  | _, _ => Unknown
-  end.
-
-Parameter propagate_float_constants: unit -> bool.
-
-Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
-  match op, vl with
-  | Omove, v1::nil => v1
-  | Ointconst n, nil => I n
-  | Ofloatconst n, nil => if propagate_float_constants tt then F n else Unknown
-  | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1)
-  | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n1)
-  | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n1)
-  | Ocast16unsigned, I n1 :: nil => I(Int.zero_ext 16 n1)
-  | Oneg, I n1 :: nil => I(Int.neg n1)
-  | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2)
-  | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
-  | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
-  | Omulimm n, I n1 :: nil => I(Int.mul n1 n)
-  | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2)
-  | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu n1 n2)
-  | Odiv, I n1 :: I n2 :: nil =>
-      if Int.eq n2 Int.zero then Unknown else
-      if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
-      else I(Int.divs n1 n2)
-  | Odivu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
-  | Omod, I n1 :: I n2 :: nil =>
-      if Int.eq n2 Int.zero then Unknown else
-      if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
-      else I(Int.mods n1 n2)
-  | Omodu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.modu n1 n2)
-  | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
-  | Oandimm n, I n1 :: nil => I(Int.and n1 n)
-  | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2)
-  | Oorimm n, I n1 :: nil => I(Int.or n1 n)
-  | Oxor, I n1 :: I n2 :: nil => I(Int.xor n1 n2)
-  | Oxorimm n, I n1 :: nil => I(Int.xor n1 n)
-  | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
-  | Oshlimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shl n1 n) else Unknown
-  | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
-  | Oshrimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown
-  | Oshrximm n, I n1 :: nil => if Int.ltu n (Int.repr 31) then I(Int.shrx n1 n) else Unknown
-  | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
-  | Oshruimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shru n1 n) else Unknown
-  | Ororimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.ror n1 n) else Unknown
-  | Oshldimm n, I n1 :: I n2 :: nil =>
-      let n' := Int.sub Int.iwordsize n in
-      if Int.ltu n Int.iwordsize && Int.ltu n' Int.iwordsize
-      then I(Int.or (Int.shl n1 n) (Int.shru n2 n')) 
-      else Unknown
-  | Olea mode, vl => eval_static_addressing mode vl
-  | Onegf, F n1 :: nil => F(Float.neg n1)
-  | Oabsf, F n1 :: nil => F(Float.abs n1)
-  | Oaddf, F n1 :: F n2 :: nil => F(Float.add n1 n2)
-  | Osubf, F n1 :: F n2 :: nil => F(Float.sub n1 n2)
-  | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2)
-  | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
-  | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
-  | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
-  | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown
-  | Omakelong, I n1 :: I n2 :: nil => L(Int64.ofwords n1 n2)
-  | Olowlong, L n :: nil => I(Int64.loword n)
-  | Ohighlong, L n :: nil => I(Int64.hiword n)
-  | Ocmp c, vl => eval_static_condition_val c vl
-  | _, _ => Unknown
-  end.
+Require Import ValueDomain.
 
 (** * Operator strength reduction *)
 
@@ -162,12 +28,8 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   one if some of its arguments are statically known.  These are again
   large pattern-matchings expressed in indirect style. *)
 
-Section STRENGTH_REDUCTION.
-
-Variable app: reg -> approx.
-
 Nondetfunction cond_strength_reduction 
-              (cond: condition) (args: list reg) (vl: list approx) :=
+              (cond: condition) (args: list reg) (vl: list aval) :=
   match cond, args, vl with
   | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
       (Ccompimm (swap_comparison c) n1, r2 :: nil)
@@ -182,34 +44,34 @@ Nondetfunction cond_strength_reduction
   end.
 
 Nondetfunction addr_strength_reduction
-                (addr: addressing) (args: list reg) (vl: list approx) :=
+                (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
 
-  | Aindexed ofs, r1 :: nil, G symb n :: nil =>
+  | Aindexed ofs, r1 :: nil, Ptr(Gl symb n) :: nil =>
       (Aglobal symb (Int.add n ofs), nil)
-  | Aindexed ofs, r1 :: nil, S n :: nil =>
+  | Aindexed ofs, r1 :: nil, Ptr(Stk n) :: nil =>
       (Ainstack (Int.add n ofs), nil)
 
-  | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil =>
+  | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil =>
       (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil)
-  | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: G symb n2 :: nil =>
+  | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Gl symb n2) :: nil =>
       (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil)
-  | Aindexed2 ofs, r1 :: r2 :: nil, S n1 :: I n2 :: nil =>
+  | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil =>
       (Ainstack (Int.add (Int.add n1 n2) ofs), nil)
-  | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: S n2 :: nil =>
+  | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil =>
       (Ainstack (Int.add (Int.add n1 n2) ofs), nil)
-  | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil =>
+  | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil =>
       (Abased symb (Int.add n1 ofs), r2 :: nil)
-  | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: G symb n2 :: nil =>
+  | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: Ptr(Gl symb n2) :: nil =>
       (Abased symb (Int.add n2 ofs), r1 :: nil)
   | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
       (Aindexed (Int.add n1 ofs), r2 :: nil)
   | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed (Int.add n2 ofs), r1 :: nil)
 
-  | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil =>
+  | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil =>
       (Aglobal symb (Int.add (Int.add n1 (Int.mul n2 sc)) ofs), nil)
-  | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil =>
+  | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil =>
       (Abasedscaled sc symb (Int.add n1 ofs), r2 :: nil)
   | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed (Int.add (Int.mul n2 sc) ofs), r1 :: nil)
@@ -255,10 +117,12 @@ Definition make_mulimm (n: int) (r: reg) :=
     | None => (Omulimm n, r :: nil)
     end.
 
-Definition make_andimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Ointconst Int.zero, nil)
+Definition make_andimm (n: int) (r: reg) (a: aval) :=
+  if Int.eq n Int.zero then (Ointconst Int.zero, nil)
   else if Int.eq n Int.mone then (Omove, r :: nil)
+  else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero
+                     | _ => false end
+  then (Omove, r :: nil)
   else (Oandimm n, r :: nil).
 
 Definition make_orimm (n: int) (r: reg) :=
@@ -296,17 +160,35 @@ Definition make_mulfimm (n: float) (r r1 r2: reg) :=
   then (Oaddf, r :: r :: nil)
   else (Omulf, r1 :: r2 :: nil).
 
+Definition make_cast8signed (r: reg) (a: aval) :=
+  if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil).
+Definition make_cast8unsigned (r: reg) (a: aval) :=
+  if vincl a (Uns 8) then (Omove, r :: nil) else (Ocast8unsigned, r :: nil).
+Definition make_cast16signed (r: reg) (a: aval) :=
+  if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil).
+Definition make_cast16unsigned (r: reg) (a: aval) :=
+  if vincl a (Uns 16) then (Omove, r :: nil) else (Ocast16unsigned, r :: nil).
+Definition make_singleoffloat (r: reg) (a: aval) :=
+  if vincl a Fsingle && generate_float_constants tt
+  then (Omove, r :: nil)
+  else (Osingleoffloat, r :: nil).
+
 Nondetfunction op_strength_reduction 
-              (op: operation) (args: list reg) (vl: list approx) :=
+              (op: operation) (args: list reg) (vl: list aval) :=
   match op, args, vl with
+  | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1
+  | Ocast8unsigned, r1 :: nil, v1 :: nil => make_cast8unsigned r1 v1
+  | Ocast16signed, r1 :: nil, v1 :: nil => make_cast16signed r1 v1
+  | Ocast16unsigned, r1 :: nil, v1 :: nil => make_cast16unsigned r1 v1
   | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1
   | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2
   | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1
   | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2
   | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2
   | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_moduimm n2 r1 r2
-  | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2
-  | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1
+  | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 v2
+  | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 v1
+  | Oandimm n, r1 :: nil, v1 :: nil => make_andimm n r1 v1
   | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2
   | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1
   | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2
@@ -317,6 +199,7 @@ Nondetfunction op_strength_reduction
   | Olea addr, args, vl =>
       let (addr', args') := addr_strength_reduction addr args vl in
       (Olea addr', args')
+  | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
   | Ocmp c, args, vl =>
       let (c', args') := cond_strength_reduction c args vl in 
       (Ocmp c', args')
@@ -324,5 +207,3 @@ Nondetfunction op_strength_reduction
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
   | _, _, _ => (op, args)
   end.
-
-End STRENGTH_REDUCTION.
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index a4cb402..d9e6068 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Correctness proof for constant propagation (processor-dependent part). *)
+(** Correctness proof for operator strength reduction. *)
 
 Require Import Coqlib.
 Require Import Integers.
@@ -22,157 +22,8 @@ Require Import Events.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
+Require Import ValueDomain.
 Require Import ConstpropOp.
-Require Import Constprop.
-
-(** * Correctness of the static analysis *)
-
-Section ANALYSIS.
-
-Variable ge: genv.
-Variable sp: val.
-
-(** We first show that the dataflow analysis is correct with respect
-  to the dynamic semantics: the approximations (sets of values) 
-  of a register at a program point predicted by the static analysis
-  are a superset of the values actually encountered during concrete
-  executions.  We formalize this correspondence between run-time values and
-  compile-time approximations by the following predicate. *)
-
-Definition val_match_approx (a: approx) (v: val) : Prop :=
-  match a with
-  | Unknown => True
-  | I p => v = Vint p
-  | F p => v = Vfloat p
-  | L p => v = Vlong p
-  | G symb ofs => v = symbol_address ge symb ofs
-  | S ofs => v = Val.add sp (Vint ofs)
-  | Novalue => False
-  end.
-
-Inductive val_list_match_approx: list approx -> list val -> Prop :=
-  | vlma_nil:
-      val_list_match_approx nil nil
-  | vlma_cons:
-      forall a al v vl,
-      val_match_approx a v ->
-      val_list_match_approx al vl ->
-      val_list_match_approx (a :: al) (v :: vl).
-
-Ltac SimplVMA :=
-  match goal with
-  | H: (val_match_approx (I _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (F _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (L _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (G _ _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (S _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | _ =>
-      idtac
-  end.
-
-Ltac InvVLMA :=
-  match goal with
-  | H: (val_list_match_approx nil ?vl) |- _ =>
-      inv H
-  | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ =>
-      inv H; SimplVMA; InvVLMA
-  | _ =>
-      idtac
-  end.
-
-(** We then show that [eval_static_operation] is a correct abstract
-  interpretations of [eval_operation]: if the concrete arguments match
-  the given approximations, the concrete results match the
-  approximations returned by [eval_static_operation]. *)
-
-Lemma eval_static_condition_correct:
-  forall cond al vl m b,
-  val_list_match_approx al vl ->
-  eval_static_condition cond al = Some b ->
-  eval_condition cond vl m = Some b.
-Proof.
-  intros until b.
-  unfold eval_static_condition. 
-  case (eval_static_condition_match cond al); intros;
-  InvVLMA; simpl; congruence.
-Qed.
-
-Remark shift_symbol_address:
-  forall symb ofs n,
-  symbol_address ge symb (Int.add ofs n) = Val.add (symbol_address ge symb ofs) (Vint n).
-Proof.
-  unfold symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. 
-Qed.
-
-Lemma eval_static_addressing_correct:
-  forall addr al vl v,
-  val_list_match_approx al vl ->
-  eval_addressing ge sp addr vl = Some v ->
-  val_match_approx (eval_static_addressing addr al) v.
-Proof.
-  intros until v. unfold eval_static_addressing.
-  case (eval_static_addressing_match addr al); intros;
-  InvVLMA; simpl in *; FuncInv; try subst v; auto.
-  rewrite shift_symbol_address; auto.
-  rewrite Val.add_assoc. auto.
-  repeat rewrite shift_symbol_address. auto.
-  fold (Val.add (Vint n1) (symbol_address ge id ofs)).
-  repeat rewrite shift_symbol_address. repeat rewrite Val.add_assoc. rewrite Val.add_permut. auto.
-  repeat rewrite Val.add_assoc. decEq; simpl. rewrite Int.add_assoc. auto.
-  fold (Val.add (Vint n1) (Val.add sp (Vint ofs))).
-  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_assoc. 
-  simpl. rewrite Int.add_assoc; auto.
-  rewrite shift_symbol_address. auto.
-  rewrite Val.add_assoc. auto. 
-  rewrite shift_symbol_address. auto.
-  rewrite shift_symbol_address. rewrite Int.mul_commut; auto. 
-Qed.
-
-Lemma eval_static_operation_correct:
-  forall op al vl m v,
-  val_list_match_approx al vl ->
-  eval_operation ge sp op vl m = Some v ->
-  val_match_approx (eval_static_operation op al) v.
-Proof.
-  intros until v.
-  unfold eval_static_operation. 
-  case (eval_static_operation_match op al); intros;
-  InvVLMA; simpl in *; FuncInv; try subst v; auto.
-  destruct (propagate_float_constants tt); simpl; auto.
-  rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
-  destruct (Int.eq n2 Int.zero). inv H0. 
-    destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero). inv H0. 
-    destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n (Int.repr 31)); inv H0. simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize);
-  destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize); simpl; auto.
-  eapply eval_static_addressing_correct; eauto.
-  unfold eval_static_intoffloat.
-  destruct (Float.intoffloat n1) eqn:?; simpl in H0; inv H0.
-  simpl; auto.
-  destruct (propagate_float_constants tt); simpl; auto.
-  unfold eval_static_condition_val. destruct (eval_static_condition c vl0) as [b|] eqn:?.
-  rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). 
-  destruct b; simpl; auto.
-  simpl; auto.
-Qed.
-
-(** * Correctness of strength reduction *)
 
 (** We now show that strength reduction over operators and addressing
   modes preserve semantics: the strength-reduced operations and
@@ -182,130 +33,197 @@ Qed.
 
 Section STRENGTH_REDUCTION.
 
-Variable app: D.t.
-Variable rs: regset.
+Variable bc: block_classification.
+Variable ge: genv.
+Hypothesis GENV: genv_match bc ge.
+Variable sp: block.
+Hypothesis STACK: bc sp = BCstack.
+Variable ae: AE.t.
+Variable e: regset.
 Variable m: mem.
-Hypothesis MATCH: forall r, val_match_approx (approx_reg app r) rs#r.
+Hypothesis MATCH: ematch bc e ae.
+
+Lemma match_G:
+  forall r id ofs,
+  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (symbol_address ge id ofs).
+Proof.
+  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
+Qed.
+
+Lemma match_S:
+  forall r ofs,
+  AE.get r ae = Ptr(Stk ofs) -> Val.lessdef e#r (Vptr sp ofs).
+Proof.
+  intros. apply vmatch_ptr_stk with bc; auto. rewrite <- H. apply MATCH.
+Qed.
 
 Ltac InvApproxRegs :=
   match goal with
   | [ H: _ :: _ = _ :: _ |- _ ] => 
         injection H; clear H; intros; InvApproxRegs
-  | [ H: ?v = approx_reg app ?r |- _ ] => 
+  | [ H: ?v = AE.get ?r ae |- _ ] => 
         generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
   | _ => idtac
   end.
 
+Ltac SimplVM :=
+  match goal with
+  | [ H: vmatch _ ?v (I ?n) |- _ ] =>
+      let E := fresh in
+      assert (E: v = Vint n) by (inversion H; auto);
+      rewrite E in *; clear H; SimplVM
+  | [ H: vmatch _ ?v (F ?n) |- _ ] =>
+      let E := fresh in
+      assert (E: v = Vfloat n) by (inversion H; auto);
+      rewrite E in *; clear H; SimplVM
+  | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
+      let E := fresh in
+      assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      clear H; SimplVM
+  | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
+      let E := fresh in
+      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto); 
+      clear H; SimplVM
+  | _ => idtac
+  end.
+
 Lemma cond_strength_reduction_correct:
   forall cond args vl,
-  vl = approx_regs app args ->
+  vl = map (fun r => AE.get r ae) args ->
   let (cond', args') := cond_strength_reduction cond args vl in
-  eval_condition cond' rs##args' m = eval_condition cond rs##args m.
+  eval_condition cond' e##args' m = eval_condition cond e##args m.
 Proof.
   intros until vl. unfold cond_strength_reduction.
-  case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  rewrite H0. apply Val.swap_cmp_bool. 
-  rewrite H. auto.
-  rewrite H0. apply Val.swap_cmpu_bool.
-  rewrite H. auto.
-  auto.
+  case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM.
+- apply Val.swap_cmp_bool.
+- auto.
+- apply Val.swap_cmpu_bool.
+- auto.
+- auto.
+Qed.
+
+Remark shift_symbol_address:
+  forall symb ofs n,
+  Op.symbol_address ge symb (Int.add ofs n) = Val.add (Op.symbol_address ge symb ofs) (Vint n).
+Proof.
+  unfold Op.symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. 
 Qed.
 
 Lemma addr_strength_reduction_correct:
-  forall addr args vl,
-  vl = approx_regs app args ->
+  forall addr args vl res,
+  vl = map (fun r => AE.get r ae) args ->
+  eval_addressing ge (Vptr sp Int.zero) addr e##args = Some res ->
   let (addr', args') := addr_strength_reduction addr args vl in
-  eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.
+  exists res', eval_addressing ge (Vptr sp Int.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
 Proof.
-  intros until vl. unfold addr_strength_reduction.
-  destruct (addr_strength_reduction_match addr args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  rewrite shift_symbol_address; congruence.
-  rewrite H. rewrite Val.add_assoc; auto.
-  rewrite H; rewrite H0. repeat rewrite shift_symbol_address. auto.
-  rewrite H; rewrite H0. rewrite Int.add_assoc. rewrite Int.add_permut. repeat rewrite shift_symbol_address.
-  rewrite Val.add_assoc. rewrite Val.add_permut. auto.
-  rewrite H; rewrite H0. repeat rewrite Val.add_assoc. rewrite Int.add_assoc. auto.
-  rewrite H; rewrite H0. repeat rewrite Val.add_assoc. rewrite Val.add_permut. 
-  rewrite Int.add_assoc. auto.
-  rewrite H0. rewrite shift_symbol_address. repeat rewrite Val.add_assoc. 
-  decEq; decEq. apply Val.add_commut.
-  rewrite H. rewrite shift_symbol_address. repeat rewrite Val.add_assoc.
-  rewrite (Val.add_permut (rs#r1)). decEq; decEq. apply Val.add_commut.
-  rewrite H0. rewrite Val.add_assoc. rewrite Val.add_permut. auto.
-  rewrite H. rewrite Val.add_assoc. auto.
-  rewrite H; rewrite H0. rewrite Int.add_assoc. repeat rewrite shift_symbol_address. auto.
-  rewrite H0. rewrite shift_symbol_address. rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
-  rewrite H. auto.
-  rewrite H. rewrite shift_symbol_address. auto.
-  rewrite H. rewrite shift_symbol_address. rewrite Int.mul_commut; auto.
-  auto.
+  intros until res. unfold addr_strength_reduction.
+  destruct (addr_strength_reduction_match addr args vl); simpl;
+  intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
+- rewrite shift_symbol_address. econstructor; split. eauto. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Int.add_zero_l.
+  change (Vptr sp (Int.add n ofs)) with (Val.add (Vptr sp n) (Vint ofs)). apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Int.add_assoc. rewrite shift_symbol_address. 
+  rewrite Val.add_assoc. apply Val.add_lessdef; auto.
+- econstructor; split; eauto.
+  fold (Val.add (Vint n1) e#r2). rewrite (Val.add_commut (Vint n1)).
+  rewrite shift_symbol_address. apply Val.add_lessdef; auto.
+  rewrite Int.add_commut. rewrite shift_symbol_address. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite Int.add_zero_l. rewrite Int.add_assoc. 
+  change (Vptr sp (Int.add n1 (Int.add n2 ofs)))
+    with (Val.add (Vptr sp n1) (Vint (Int.add n2 ofs))).
+  rewrite Val.add_assoc. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite Int.add_zero_l. 
+  fold (Val.add (Vint n1) e#r2). rewrite (Int.add_commut n1). 
+  change (Vptr sp (Int.add (Int.add n2 n1) ofs))
+    with (Val.add (Val.add (Vint n1) (Vptr sp n2)) (Vint ofs)).
+  apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite shift_symbol_address. 
+  rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. 
+  rewrite Val.add_commut. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite shift_symbol_address.
+  rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc.
+  apply Val.add_lessdef; auto. rewrite Val.add_commut. apply Val.add_lessdef; auto.
+- fold (Val.add (Vint n1) e#r2). econstructor; split; eauto. 
+  rewrite (Val.add_commut (Vint n1)). rewrite Val.add_assoc. 
+  apply Val.add_lessdef; eauto. 
+- econstructor; split; eauto.  rewrite ! Val.add_assoc.
+  apply Val.add_lessdef; eauto. 
+- econstructor; split; eauto. rewrite Int.add_assoc. 
+  rewrite shift_symbol_address. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. 
+  rewrite shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
+  rewrite Val.add_commut; auto.
+- econstructor; split; eauto.
+- econstructor; split; eauto. rewrite shift_symbol_address. auto.
+- econstructor; split; eauto. rewrite shift_symbol_address. rewrite Int.mul_commut; auto.
+- econstructor; eauto.
 Qed.
 
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.add e#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. 
-  subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto.
-  exists (Val.add rs#r (Vint n)); auto.
+  subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite Int.add_zero; auto.
+  exists (Val.add e#r (Vint n)); auto.
 Qed.
   
 Lemma make_shlimm_correct:
   forall n r1,
   let (op, args) := make_shlimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shl e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto.
   econstructor; split. simpl. eauto. auto.
 Qed.
 
 Lemma make_shrimm_correct:
   forall n r1,
   let (op, args) := make_shrimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shr e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shr_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto.
   econstructor; split; eauto. simpl. auto.
 Qed.
 
 Lemma make_shruimm_correct:
   forall n r1,
   let (op, args) := make_shruimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shru e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
 Lemma make_mulimm_correct:
   forall n r1,
   let (op, args) := make_mulimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mul e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_mulimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (Vint Int.zero); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_zero; auto.
+  exists (Vint Int.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
-  rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). apply make_shlimm_correct; auto. 
+  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). apply make_shlimm_correct; auto. 
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_divimm_correct:
   forall n r1 r2 v,
-  Val.divs rs#r1 rs#r2 = Some v ->
-  rs#r2 = Vint n ->
+  Val.divs e#r1 e#r2 = Some v ->
+  e#r2 = Vint n ->
   let (op, args) := make_divimm n r1 r2 in
-  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -317,14 +235,14 @@ Qed.
 
 Lemma make_divuimm_correct:
   forall n r1 r2 v,
-  Val.divu rs#r1 rs#r2 = Some v ->
-  rs#r2 = Vint n ->
+  Val.divu e#r1 e#r2 = Some v ->
+  e#r2 = Vint n ->
   let (op, args) := make_divuimm n r1 r2 in
-  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
-  replace v with (Val.shru rs#r1 (Vint i)). 
+  replace v with (Val.shru e#r1 (Vint i)). 
   eapply make_shruimm_correct; eauto.
   eapply Val.divu_pow2; eauto. congruence.
   exists v; auto.
@@ -332,10 +250,10 @@ Qed.
 
 Lemma make_moduimm_correct:
   forall n r1 r2 v,
-  Val.modu rs#r1 rs#r2 = Some v ->
-  rs#r2 = Vint n ->
+  Val.modu e#r1 e#r2 = Some v ->
+  e#r2 = Vint n ->
   let (op, args) := make_moduimm n r1 r2 in
-  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_moduimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -344,125 +262,216 @@ Proof.
 Qed.
 
 Lemma make_andimm_correct:
-  forall n r,
-  let (op, args) := make_andimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v.
+  forall n r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_andimm n r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.and e#r (Vint n)) v.
 Proof.
   intros; unfold make_andimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto.
+  subst n. exists (Vint Int.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_mone; auto.
+  destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
+                       | _ => false end) eqn:UNS.
+  destruct x; try congruence. 
+  exists (e#r); split; auto.
+  inv H; auto. simpl. replace (Int.and i n) with i; auto.
+  generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ.
+  Int.bit_solve. destruct (zlt i0 n0).
+  replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
+  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. 
+  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. 
+  rewrite Int.bits_not by auto. apply negb_involutive. 
+  rewrite H5 by auto. auto. 
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_orimm_correct:
   forall n r,
   let (op, args) := make_orimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.or e#r (Vint n)) v.
 Proof.
   intros; unfold make_orimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (Vint Int.mone); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_mone; auto.
+  subst n. exists (Vint Int.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_mone; auto.
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_xorimm_correct:
   forall n r,
   let (op, args) := make_xorimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.xor e#r (Vint n)) v.
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto.
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_mulfimm_correct:
   forall n r1 r2,
-  rs#r2 = Vfloat n ->
+  e#r2 = Vfloat n ->
   let (op, args) := make_mulfimm n r1 r1 r2 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
   destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. 
+  destruct (e#r1); simpl; auto. rewrite Float.mul2_add; auto. 
   simpl. econstructor; split; eauto. 
 Qed.
 
 Lemma make_mulfimm_correct_2:
   forall n r1 r2,
-  rs#r1 = Vfloat n ->
+  e#r1 = Vfloat n ->
   let (op, args) := make_mulfimm n r2 r1 r2 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
   destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. 
+  destruct (e#r2); simpl; auto. rewrite Float.mul2_add; auto. 
   rewrite Float.mul_commut; auto. 
   simpl. econstructor; split; eauto. 
 Qed.
 
+Lemma make_cast8signed_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast8signed r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 8 e#r) v.
+Proof.
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Sgn 8)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_cast8unsigned_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast8unsigned r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 8 e#r) v.
+Proof.
+  intros; unfold make_cast8unsigned. destruct (vincl x (Uns 8)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Uns 8)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_uns_zero_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_cast16signed_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast16signed r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 16 e#r) v.
+Proof.
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Sgn 16)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_cast16unsigned_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast16unsigned r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 16 e#r) v.
+Proof.
+  intros; unfold make_cast16unsigned. destruct (vincl x (Uns 16)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Uns 16)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_uns_zero_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_singleoffloat_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_singleoffloat r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.singleoffloat e#r) v.
+Proof.
+  intros; unfold make_singleoffloat.
+  destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. 
+  InvBooleans. exists e#r; split; auto. 
+  assert (V: vmatch bc e#r Fsingle).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite Float.singleoffloat_of_single by auto. auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
 Lemma op_strength_reduction_correct:
   forall op args vl v,
-  vl = approx_regs app args ->
-  eval_operation ge sp op rs##args m = Some v ->
+  vl = map (fun r => AE.get r ae) args ->
+  eval_operation ge (Vptr sp Int.zero) op e##args m = Some v ->
   let (op', args') := op_strength_reduction op args vl in
-  exists w, eval_operation ge sp op' rs##args' m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some w /\ Val.lessdef v w.
 Proof.
   intros until v; unfold op_strength_reduction;
   case (op_strength_reduction_match op args vl); simpl; intros.
+(* cast8signed *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto.
+(* cast8unsigned *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast8unsigned_correct; auto.
+(* cast16signed *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto.
+(* cast16unsigned *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast16unsigned_correct; auto.
 (* sub *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. rewrite Val.sub_add_opp. apply make_addimm_correct; auto. 
+  InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct; auto. 
 (* mul *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.mul_commut. apply make_mulimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_mulimm_correct; auto.
+  rewrite Val.mul_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
 (* divs *) 
-  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divimm_correct; auto.
 (* divu *) 
-  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divuimm_correct; auto.
 (* modu *) 
-  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_moduimm_correct; auto.
 (* and *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.and_commut. apply make_andimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_andimm_correct; auto.
+  rewrite Val.and_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto.
+  inv H; inv H0. apply make_andimm_correct; auto.
 (* or *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.or_commut. apply make_orimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_orimm_correct; auto.
+  rewrite Val.or_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_orimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_orimm_correct; auto.
 (* xor *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.xor_commut. apply make_xorimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_xorimm_correct; auto.
+  rewrite Val.xor_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_xorimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_xorimm_correct; auto.
 (* shl *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_shlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_shlimm_correct; auto.
 (* shr *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_shrimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto.
 (* shru *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_shruimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto.
 (* lea *)
-  generalize (addr_strength_reduction_correct addr args0 vl0 H). 
+  exploit addr_strength_reduction_correct; eauto. 
   destruct (addr_strength_reduction addr args0 vl0) as [addr' args'].
-  intro EQ. exists v; split; auto. simpl. congruence.
+  auto.
+(* singleoffloat *)
+  InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cond *)
   generalize (cond_strength_reduction_correct c args0 vl0 H). 
   destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
   rewrite <- H1 in H0; auto. econstructor; split; eauto.
 (* mulf *)
-  inv H0. assert (rs#r2 = Vfloat n2). InvApproxRegs; SimplVMA; auto.
-  apply make_mulfimm_correct; auto.
-  inv H0. assert (rs#r1 = Vfloat n1). InvApproxRegs; SimplVMA; auto.
-  apply make_mulfimm_correct_2; auto.
+  InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) e#r2).
+  rewrite <- H2. apply make_mulfimm_correct_2; auto.
 (* default *)
   exists v; auto.
 Qed.
 
 End STRENGTH_REDUCTION.
-
-End ANALYSIS.
-
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v
new file mode 100644
index 0000000..2853bf1
--- /dev/null
+++ b/ia32/NeedOp.v
@@ -0,0 +1,169 @@
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Op.
+Require Import NeedDomain.
+Require Import RTL.
+
+(** Neededness analysis for IA32 operators *)
+
+Definition needs_of_condition (cond: condition): nval :=
+  match cond with
+  | Cmaskzero n | Cmasknotzero n => maskzero n
+  | _ => All
+  end.
+
+Definition needs_of_addressing (addr: addressing) (nv: nval): nval :=
+  modarith nv.
+
+Definition needs_of_operation (op: operation) (nv: nval): nval :=
+  match op with
+  | Omove => nv
+  | Ointconst n => Nothing
+  | Ofloatconst n => Nothing
+  | Oindirectsymbol id => Nothing
+  | Ocast8signed => sign_ext 8 nv
+  | Ocast8unsigned => zero_ext 8 nv
+  | Ocast16signed => sign_ext 16 nv
+  | Ocast16unsigned => zero_ext 16 nv
+  | Omul => modarith nv
+  | Omulimm n => modarith nv
+  | Oand => bitwise nv
+  | Oandimm n => andimm nv n
+  | Oor => bitwise nv
+  | Oorimm n => orimm nv n
+  | Oxor => bitwise nv
+  | Oxorimm n => bitwise nv
+  | Oshlimm n => shlimm nv n
+  | Oshrimm n => shrimm nv n
+  | Oshruimm n => shruimm nv n
+  | Ororimm n => ror nv n
+  | Olea addr => needs_of_addressing addr nv
+  | Ocmp c => needs_of_condition c
+  | Osingleoffloat => singleoffloat nv
+  | _ => default nv
+  end.
+
+Definition operation_is_redundant (op: operation) (nv: nval): bool :=
+  match op with
+  | Ocast8signed => sign_ext_redundant 8 nv
+  | Ocast8unsigned => zero_ext_redundant 8 nv
+  | Ocast16signed => sign_ext_redundant 16 nv
+  | Ocast16unsigned => zero_ext_redundant 16 nv
+  | Oandimm n => andimm_redundant nv n
+  | Oorimm n => orimm_redundant nv n
+  | Osingleoffloat => singleoffloat_redundant nv
+  | _ => false
+  end.
+
+Ltac InvAgree :=
+  match goal with
+  | [H: vagree_list nil _ _ |- _ ] => inv H; InvAgree
+  | [H: vagree_list (_::_) _ _ |- _ ] => inv H; InvAgree
+  | [H: list_forall2 _ nil _ |- _ ] => inv H; InvAgree
+  | [H: list_forall2 _ (_::_) _ |- _ ] => inv H; InvAgree
+  | _ => idtac
+  end.
+
+Ltac TrivialExists :=
+  match goal with
+  | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto
+  | _ => idtac
+  end.
+
+Section SOUNDNESS.
+
+Variable ge: genv.
+Variable sp: block.
+Variables m m': mem.
+Hypothesis PERM: forall b ofs k p, Mem.perm m b ofs k p -> Mem.perm m' b ofs k p.
+
+Lemma needs_of_condition_sound:
+  forall cond args b args',
+  eval_condition cond args m = Some b ->
+  vagree_list args args' (needs_of_condition cond) ->
+  eval_condition cond args' m' = Some b.
+Proof.
+  intros. destruct cond; simpl in H;
+  try (eapply default_needs_of_condition_sound; eauto; fail);
+  simpl in *; FuncInv; InvAgree.
+- eapply maskzero_sound; eauto. 
+- destruct (Val.maskzero_bool v i) as [b'|] eqn:MZ; try discriminate.
+  erewrite maskzero_sound; eauto.
+Qed.
+
+Lemma needs_of_addressing_sound:
+  forall (ge: genv) sp addr args v nv args',
+  eval_addressing ge (Vptr sp Int.zero) addr args = Some v ->
+  vagree_list args args' (needs_of_addressing addr nv) ->
+  exists v',
+     eval_addressing ge (Vptr sp Int.zero) addr args' = Some v'
+  /\ vagree v v' nv.
+Proof.
+  unfold needs_of_addressing; intros.
+  destruct addr; simpl in *; FuncInv; InvAgree; TrivialExists;
+  auto using add_sound, add_sound_2, mul_sound, mul_sound_2 with na.
+Qed.
+
+Lemma needs_of_operation_sound:
+  forall op args v nv args',
+  eval_operation ge (Vptr sp Int.zero) op args m = Some v ->
+  vagree_list args args' (needs_of_operation op nv) ->
+  nv <> Nothing ->
+  exists v',
+     eval_operation ge (Vptr sp Int.zero) op args' m' = Some v'
+  /\ vagree v v' nv.
+Proof.
+  unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail);
+  simpl in *; FuncInv; InvAgree; TrivialExists.
+- auto with na.
+- auto with na.
+- auto with na.
+- apply sign_ext_sound; auto. compute; auto. 
+- apply zero_ext_sound; auto. omega.
+- apply sign_ext_sound; auto. compute; auto. 
+- apply zero_ext_sound; auto. omega.
+- apply mul_sound; auto.
+- apply mul_sound; auto with na.
+- apply and_sound; auto.
+- apply andimm_sound; auto.
+- apply or_sound; auto.
+- apply orimm_sound; auto.
+- apply xor_sound; auto.
+- apply xor_sound; auto with na.
+- apply shlimm_sound; auto.
+- apply shrimm_sound; auto.
+- apply shruimm_sound; auto. 
+- apply ror_sound; auto. 
+- eapply needs_of_addressing_sound; eauto.
+- apply singleoffloat_sound; auto. 
+- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. 
+  erewrite needs_of_condition_sound by eauto.
+  subst v; simpl. auto with na.
+  subst v; auto with na.
+Qed.
+
+Lemma operation_is_redundant_sound:
+  forall op nv arg1 args v arg1',
+  operation_is_redundant op nv = true ->
+  eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v ->
+  vagree arg1 arg1' (needs_of_operation op nv) ->
+  vagree v arg1' nv.
+Proof.
+  intros. destruct op; simpl in *; try discriminate; FuncInv; subst.
+- apply sign_ext_redundant_sound; auto. omega.
+- apply zero_ext_redundant_sound; auto. omega.
+- apply sign_ext_redundant_sound; auto. omega.
+- apply zero_ext_redundant_sound; auto. omega.
+- apply andimm_redundant_sound; auto. 
+- apply orimm_redundant_sound; auto.
+- apply singleoffloat_redundant_sound; auto.
+Qed.
+
+End SOUNDNESS.
+
+
diff --git a/ia32/Op.v b/ia32/Op.v
index f2e6b13..26e6688 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -174,8 +174,8 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | 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)
-  | Cmaskzero n, Vint n1 :: nil => Some (Int.eq (Int.and n1 n) Int.zero)
-  | Cmasknotzero n, Vint n1 :: nil => Some (negb (Int.eq (Int.and n1 n) Int.zero))
+  | Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n
+  | Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n)
   | _, _ => None
   end.
 
@@ -483,9 +483,9 @@ Proof.
   repeat (destruct vl; auto). apply Val.negate_cmp_bool.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
   repeat (destruct vl; auto). 
-  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
-  destruct vl; auto. destruct v; auto. destruct vl; auto. 
-  destruct vl; auto. destruct v; auto. destruct vl; auto. simpl. rewrite negb_involutive. auto.
+  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto.
+  destruct vl; auto. destruct vl; auto.
+  destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v i) as [[]|]; auto.
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
@@ -534,27 +534,32 @@ Qed.
 
 (** Offset an addressing mode [addr] by a quantity [delta], so that
   it designates the pointer [delta] bytes past the pointer designated
-  by [addr].  May be undefined, in which case [None] is returned. *)
+  by [addr].  On PowerPC and ARM, this may be undefined, in which case
+  [None] is returned.  On IA32, it is always defined, but we keep the
+  same interface. *)
 
-Definition offset_addressing (addr: addressing) (delta: int) : option addressing :=
+Definition offset_addressing_total (addr: addressing) (delta: int) : addressing :=
   match addr with
-  | Aindexed n => Some(Aindexed (Int.add n delta))
-  | Aindexed2 n => Some(Aindexed2 (Int.add n delta))
-  | Ascaled sc n => Some(Ascaled sc (Int.add n delta))
-  | Aindexed2scaled sc n => Some(Aindexed2scaled sc (Int.add n delta))
-  | Aglobal s n => Some(Aglobal s (Int.add n delta))
-  | Abased s n => Some(Abased s (Int.add n delta))
-  | Abasedscaled sc s n => Some(Abasedscaled sc s (Int.add n delta))
-  | Ainstack n => Some(Ainstack (Int.add n delta))
+  | Aindexed n => Aindexed (Int.add n delta)
+  | Aindexed2 n => Aindexed2 (Int.add n delta)
+  | Ascaled sc n => Ascaled sc (Int.add n delta)
+  | Aindexed2scaled sc n => Aindexed2scaled sc (Int.add n delta)
+  | Aglobal s n => Aglobal s (Int.add n delta)
+  | Abased s n => Abased s (Int.add n delta)
+  | Abasedscaled sc s n => Abasedscaled sc s (Int.add n delta)
+  | Ainstack n => Ainstack (Int.add n delta)
   end.
 
-Lemma eval_offset_addressing:
-  forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v,
-  offset_addressing addr delta = Some addr' ->
+Definition offset_addressing (addr: addressing) (delta: int) : option addressing :=
+  Some(offset_addressing_total addr delta).
+
+Lemma eval_offset_addressing_total:
+  forall (F V: Type) (ge: Genv.t F V) sp addr args delta v,
   eval_addressing ge sp addr args = Some v ->
-  eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)).
+  eval_addressing ge sp (offset_addressing_total addr delta) args =
+    Some(Val.add v (Vint delta)).
 Proof.
-  intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; inv H.
+  intros. destruct addr; simpl in *; FuncInv; subst.
   rewrite Val.add_assoc; auto.
   rewrite !Val.add_assoc; auto.
   rewrite !Val.add_assoc; auto.
@@ -567,6 +572,16 @@ Proof.
   rewrite Val.add_assoc. auto. 
 Qed.
 
+Lemma eval_offset_addressing:
+  forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v,
+  offset_addressing addr delta = Some addr' ->
+  eval_addressing ge sp addr args = Some v ->
+  eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)).
+Proof.
+  intros. unfold offset_addressing in H; inv H. 
+  eapply eval_offset_addressing_total; eauto.
+Qed.
+
 (** Operations that are so cheap to recompute that CSE should not factor them out. *)
 
 Definition is_trivial_op (op: operation) : bool :=
@@ -757,8 +772,8 @@ Proof.
   eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
-  inv H3; try discriminate; inv H5; auto.
-  inv H3; try discriminate; inv H5; auto.
+  inv H3; try discriminate; auto.
+  inv H3; try discriminate; auto.
 Qed.
 
 Ltac TrivialExists :=
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 1471405..d8a2127 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -71,24 +71,12 @@ Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil).
 
 (** ** Integer addition and pointer addition *)
 
-Definition offset_addressing (a: addressing) (ofs: int) : addressing :=
-  match a with
-  | Aindexed n => Aindexed (Int.add n ofs)
-  | Aindexed2 n => Aindexed2 (Int.add n ofs)
-  | Ascaled sc n => Ascaled sc (Int.add n ofs)
-  | Aindexed2scaled sc n => Aindexed2scaled sc (Int.add n ofs)
-  | Aglobal id n => Aglobal id (Int.add n ofs)
-  | Abased id n => Abased id (Int.add n ofs)
-  | Abasedscaled sc id n => Abasedscaled sc id (Int.add n ofs)
-  | Ainstack n => Ainstack (Int.add n ofs)
-  end.
-
 Nondetfunction addimm (n: int) (e: expr) :=
   if Int.eq n Int.zero then e else
   match e with
-  | Eop (Ointconst m) Enil       => Eop (Ointconst(Int.add n m)) Enil
-  | Eop (Olea addr) args         => Eop (Olea (offset_addressing addr n)) args
-  | _                            => Eop (Olea (Aindexed n)) (e ::: Enil)
+  | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil
+  | Eop (Olea addr) args   => Eop (Olea (offset_addressing_total addr n)) args
+  | _                      => Eop (Olea (Aindexed n)) (e ::: Enil)
   end.
 
 Nondetfunction add (e1: expr) (e2: expr) :=
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index cec3b59..02d3bee 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -145,22 +145,6 @@ Proof.
   intros. unfold symbol_address. destruct (Genv.find_symbol); auto. 
 Qed.
 
-Lemma eval_offset_addressing:
-  forall addr n args v,
-  eval_addressing ge sp addr args = Some v ->
-  eval_addressing ge sp (offset_addressing addr n) args = Some (Val.add v (Vint n)).
-Proof.
-  intros. destruct addr; simpl in *; FuncInv; subst; simpl.
-  rewrite Val.add_assoc. auto. 
-  repeat rewrite Val.add_assoc. auto.
-  rewrite Val.add_assoc. auto.
-  repeat rewrite Val.add_assoc. auto.
-  rewrite shift_symbol_address. auto. 
-  rewrite shift_symbol_address. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
-  rewrite shift_symbol_address. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
-  rewrite Val.add_assoc. auto.
-Qed.
-
 Theorem eval_addimm:
   forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
 Proof.
@@ -170,7 +154,7 @@ Proof.
   destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto.
   case (addimm_match a); intros; InvEval; simpl.
   TrivialExists; simpl. rewrite Int.add_commut. auto.
-  inv H0. simpl in H6. TrivialExists. simpl. eapply eval_offset_addressing; eauto.
+  inv H0. simpl in H6. TrivialExists. simpl. eapply eval_offset_addressing_total; eauto.
   TrivialExists. 
 Qed.
 
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
new file mode 100644
index 0000000..a7c72d3
--- /dev/null
+++ b/ia32/ValueAOp.v
@@ -0,0 +1,158 @@
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Op.
+Require Import ValueDomain.
+Require Import RTL.
+
+(** Value analysis for IA32 operators *)
+
+Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
+  match cond, vl with
+  | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
+  | Ccompu c, v1 :: v2 :: nil => cmpu_bool c v1 v2
+  | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n)
+  | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n)
+  | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2
+  | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
+  | Cmaskzero n, v1 :: nil => maskzero v1 n
+  | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n)
+  | _, _ => Bnone
+  end.
+
+Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
+  match addr, vl with
+  | Aindexed n, v1::nil => add v1 (I n)
+  | Aindexed2 n, v1::v2::nil => add (add v1 v2) (I n)
+  | Ascaled sc ofs, v1::nil => add (mul v1 (I sc)) (I ofs)
+  | Aindexed2scaled sc ofs, v1::v2::nil => add v1 (add (mul v2 (I sc)) (I ofs))
+  | Aglobal s ofs, nil => Ptr (Gl s ofs)
+  | Abased s ofs, v1::nil => add (Ptr (Gl s ofs)) v1
+  | Abasedscaled sc s ofs, v1::nil => add (Ptr (Gl s ofs)) (mul v1 (I sc))
+  | Ainstack ofs, nil => Ptr(Stk ofs)
+  | _, _ => Vbot
+  end.
+
+Definition eval_static_operation (op: operation) (vl: list aval): aval :=
+  match op, vl with
+  | Omove, v1::nil => v1
+  | Ointconst n, nil => I n
+  | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop
+  | Oindirectsymbol id, nil => Ptr (Gl id Int.zero)
+  | Ocast8signed, v1 :: nil => sign_ext 8 v1
+  | Ocast8unsigned, v1 :: nil => zero_ext 8 v1
+  | Ocast16signed, v1 :: nil => sign_ext 16 v1
+  | Ocast16unsigned, v1 :: nil => zero_ext 16 v1
+  | Oneg, v1::nil => neg v1
+  | Osub, v1::v2::nil => sub v1 v2
+  | Omul, v1::v2::nil => mul v1 v2
+  | Omulimm n, v1::nil => mul v1 (I n)
+  | Omulhs, v1::v2::nil => mulhs v1 v2
+  | Omulhu, v1::v2::nil => mulhu v1 v2
+  | Odiv, v1::v2::nil => divs v1 v2
+  | Odivu, v1::v2::nil => divu v1 v2
+  | Omod, v1::v2::nil => mods v1 v2
+  | Omodu, v1::v2::nil => modu v1 v2
+  | Oand, v1::v2::nil => and v1 v2
+  | Oandimm n, v1::nil => and v1 (I n)
+  | Oor, v1::v2::nil => or v1 v2
+  | Oorimm n, v1::nil => or v1 (I n)
+  | Oxor, v1::v2::nil => xor v1 v2
+  | Oxorimm n, v1::nil => xor v1 (I n)
+  | Oshl, v1::v2::nil => shl v1 v2
+  | Oshlimm n, v1::nil => shl v1 (I n)
+  | Oshr, v1::v2::nil => shr v1 v2
+  | Oshrimm n, v1::nil => shr v1 (I n)
+  | Oshrximm n, v1::nil => shrx v1 (I n)
+  | Oshru, v1::v2::nil => shru v1 v2
+  | Oshruimm n, v1::nil => shru v1 (I n)
+  | Ororimm n, v1::nil => ror v1 (I n)
+  | Oshldimm n, v1::v2::nil => or (shl v1 (I n)) (shru v2 (I (Int.sub Int.iwordsize n)))
+  | Olea addr, _ => eval_static_addressing addr vl
+  | Onegf, v1::nil => negf v1
+  | Oabsf, v1::nil => absf v1
+  | Oaddf, v1::v2::nil => addf v1 v2
+  | Osubf, v1::v2::nil => subf v1 v2
+  | Omulf, v1::v2::nil => mulf v1 v2
+  | Odivf, v1::v2::nil => divf v1 v2
+  | Osingleoffloat, v1::nil => singleoffloat v1
+  | Ointoffloat, v1::nil => intoffloat v1
+  | Ofloatofint, v1::nil => floatofint v1
+  | Omakelong, v1::v2::nil => longofwords v1 v2
+  | Olowlong, v1::nil => loword v1
+  | Ohighlong, v1::nil => hiword v1
+  | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | _, _ => Vbot
+  end.
+
+Section SOUNDNESS.
+
+Variable bc: block_classification.
+Variable ge: genv.
+Hypothesis GENV: genv_match bc ge.
+Variable sp: block.
+Hypothesis STACK: bc sp = BCstack.
+
+Theorem eval_static_condition_sound:
+  forall cond vargs m aargs,
+  list_forall2 (vmatch bc) vargs aargs ->
+  cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs).
+Proof.
+  intros until aargs; intros VM.
+  inv VM.
+  destruct cond; auto with va.
+  inv H0.
+  destruct cond; simpl; eauto with va.
+  inv H2.
+  destruct cond; simpl; eauto with va.
+  destruct cond; auto with va.
+Qed.
+
+Lemma symbol_address_sound:
+  forall id ofs,
+  vmatch bc (symbol_address ge id ofs) (Ptr (Gl id ofs)).
+Proof.
+  intros; apply symbol_address_sound; apply GENV.
+Qed.
+
+Hint Resolve symbol_address_sound: va.
+
+Ltac InvHyps :=
+  match goal with
+  | [H: None = Some _ |- _ ] => discriminate
+  | [H: Some _ = Some _ |- _] => inv H
+  | [H1: match ?vl with nil => _ | _ :: _ => _ end = Some _ ,
+     H2: list_forall2 _ ?vl _ |- _ ] => inv H2; InvHyps
+  | _ => idtac
+  end.
+
+Theorem eval_static_addressing_sound:
+  forall addr vargs vres aargs,
+  eval_addressing ge (Vptr sp Int.zero) addr vargs = Some vres ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  vmatch bc vres (eval_static_addressing addr aargs).
+Proof.
+  unfold eval_addressing, eval_static_addressing; intros;
+  destruct addr; InvHyps; eauto with va.
+  rewrite Int.add_zero_l; auto with va. 
+Qed.
+
+Theorem eval_static_operation_sound:
+  forall op vargs m vres aargs,
+  eval_operation ge (Vptr sp Int.zero) op vargs m = Some vres ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  vmatch bc vres (eval_static_operation op aargs).
+Proof.
+  unfold eval_operation, eval_static_operation; intros;
+  destruct op; InvHyps; eauto with va.
+  destruct (propagate_float_constants tt); constructor.
+  eapply eval_static_addressing_sound; eauto.
+  apply of_optbool_sound. eapply eval_static_condition_sound; eauto. 
+Qed.
+
+End SOUNDNESS.
+