Updated ARM backend wrt new static analyses and optimizations.

NeedOp, Deadcode: must have distinct needs per argument of an operator.
  This change remains to be propagated to IA32 and PPC.


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

22 files changed, 940 insertions, 612 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 3707b7f..b6cb2b3 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -267,6 +267,14 @@ Definition transl_op
   | Oaddrstack n, nil =>
       do r <- ireg_of res;
       OK (addimm r IR13 n k)
+  | Ocast8signed, a1 :: nil =>
+      do r <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pmov r (SOlslimm r1 (Int.repr 24)) ::
+          Pmov r (SOasrimm r (Int.repr 24)) :: k)
+  | Ocast16signed, a1 :: nil =>
+      do r <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pmov r (SOlslimm r1 (Int.repr 16)) ::
+          Pmov r (SOasrimm r (Int.repr 16)) :: k)
   | Oadd, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (Padd r r1 (SOreg r2) :: k)
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 21d2b73..1e65d72 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -917,6 +917,26 @@ Proof.
   generalize (addimm_correct x IR13 i k rs m). 
   intros [rs' [EX [RES OTH]]].
   exists rs'; auto with asmgen. 
+  (* Ocast8signed *)
+  set (rs1 := nextinstr (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 24))))).
+  set (rs2 := nextinstr (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 24))))).
+  exists rs2.
+  split. apply exec_straight_two with rs1 m; auto. 
+  split. unfold rs2; Simpl. unfold rs1; Simpl.
+  unfold Val.shr, Val.shl; destruct (rs x0); auto. 
+  change (Int.ltu (Int.repr 24) Int.iwordsize) with true; simpl.
+  f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; auto.
+  intros. unfold rs2, rs1; Simpl. 
+  (* Ocast16signed *)
+  set (rs1 := nextinstr (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 16))))).
+  set (rs2 := nextinstr (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 16))))).
+  exists rs2.
+  split. apply exec_straight_two with rs1 m; auto. 
+  split. unfold rs2; Simpl. unfold rs1; Simpl.
+  unfold Val.shr, Val.shl; destruct (rs x0); auto. 
+  change (Int.ltu (Int.repr 16) Int.iwordsize) with true; simpl.
+  f_equal. symmetry. apply (Int.sign_ext_shr_shl 16). compute; auto.
+  intros. unfold rs2, rs1; Simpl. 
   (* Oaddimm *)
   generalize (addimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]]. 
diff --git a/arm/CombineOp.v b/arm/CombineOp.v
index fd347c1..8da6e3a 100644
--- a/arm/CombineOp.v
+++ b/arm/CombineOp.v
@@ -17,13 +17,7 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
 Require Import Op.
-Require SelectOp.
-
-Definition valnum := positive.
-
-Inductive rhs : Type :=
-  | Op: operation -> list valnum -> rhs
-  | Load: memory_chunk -> addressing -> list valnum -> rhs.
+Require Import CSEdomain.
 
 Section COMBINE.
 
@@ -104,7 +98,9 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       end
   | Oandimm n, x :: nil =>
       match get x with
-      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
+      | Some(Op (Oandimm m) ys) => 
+          Some(let p := Int.and m n in
+               if Int.eq p m then (Omove, x :: nil) else (Oandimm p, ys))
       | _ => None
       end
   | Oorimm n, x :: nil =>
diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v
index c95b19c..485857b 100644
--- a/arm/CombineOpproof.v
+++ b/arm/CombineOpproof.v
@@ -21,8 +21,8 @@ Require Import Memory.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
+Require Import CSEdomain.
 Require Import CombineOp.
-Require Import CSE.
 
 Section COMBINE.
 
@@ -31,8 +31,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) ->
@@ -41,7 +53,7 @@ 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.
 Qed.
 
@@ -53,7 +65,7 @@ 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.
 Qed.
@@ -66,7 +78,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.
 
@@ -78,7 +90,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.
@@ -114,8 +126,7 @@ Theorem combine_addr_sound:
 Proof.
   intros. functional inversion H; subst.
   (* indexed - addimm *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
-  rewrite <- H0. rewrite Val.add_assoc. auto. 
+  UseGetSound. simpl. rewrite <- H0. rewrite Val.add_assoc. auto. 
 Qed.
 
 Theorem combine_op_sound:
@@ -125,28 +136,28 @@ Theorem combine_op_sound:
 Proof.
   intros. functional inversion H; subst.
 (* addimm - addimm *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
-  rewrite <- H1. rewrite Val.add_assoc. auto.
+  UseGetSound. FuncInv. simpl.
+  rewrite <- H0. rewrite Val.add_assoc. auto.
 (* addimm - subimm *)
 Opaque Val.sub.
-  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
-  rewrite <- H1. change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)).
-  rewrite Val.sub_add_l. auto.
+  UseGetSound. FuncInv. simpl.
+  change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)).
+  rewrite <- H0. rewrite Val.sub_add_l. auto.
 (* subimm - addimm *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
-  rewrite <- H1.
+  UseGetSound. FuncInv. simpl. rewrite <- H0.
 Transparent Val.sub.
   destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc.
   rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut.
 (* andimm - andimm *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
-  rewrite <- H1. rewrite Val.and_assoc. auto.
+  UseGetSound; simpl. 
+  generalize (Int.eq_spec p m0); rewrite H7; intros. 
+  rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto.
+  UseGetSound; simpl. 
+  rewrite <- H0. rewrite Val.and_assoc. auto.
 (* orimm - orimm *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
-  rewrite <- H1. rewrite Val.or_assoc. auto.
+  UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
 (* xorimm - xorimm *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
-  rewrite <- H1. rewrite Val.xor_assoc. auto.
+  UseGetSound. simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
 (* cmp *)
   simpl. decEq; decEq. eapply combine_cond_sound; eauto.
 Qed.
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 47d2086..0540781 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -19,35 +19,16 @@ Require Import Integers.
 Require Import Floats.
 Require Import Op.
 Require Import Registers.
+Require Import ValueDomain.
 
-(** * 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. *)
-
+(** * Operator strength reduction *)
 
-(** 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 [F f]
-  and [F g] respectively, and [Unknown] otherwise.
+(** We now define auxiliary functions for strength reduction of
+  operators and addressing modes: replacing an operator with a cheaper
+  one if some of its arguments are statically known.  These are again
+  large pattern-matchings expressed in indirect style. *)
 
-  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. *)
+Section STRENGTH_REDUCTION.
 
 Definition eval_static_shift (s: shift) (n: int) : int :=
   match s with
@@ -57,134 +38,8 @@ Definition eval_static_shift (s: shift) (n: int) : int :=
   | Sror x => Int.ror n x
   end.
 
-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)
-  | Ccompshift c s, I n1 :: I n2 :: nil => Some(Int.cmp c n1 (eval_static_shift s n2))
-  | Ccompushift c s, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 (eval_static_shift s 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))
-  | Ccompfzero c, F n1 :: nil => Some(Float.cmp c n1 Float.zero)
-  | Cnotcompfzero c, F n1 :: nil => Some(negb(Float.cmp c n1 Float.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.
-
-Definition eval_static_intuoffloat (f: float) :=
-  match Float.intuoffloat f with Some x => I x | None => 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
-  | Oaddrsymbol s n, nil => G s n
-  | Oaddrstack n, nil => S n
-  | Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2)
-  | Oaddshift s, I n1 :: I n2 :: nil => I(Int.add n1 (eval_static_shift s n2))
-  | Oadd, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 n2)
-  | Oaddshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 (eval_static_shift s n2))
-  | Oadd, S n1 :: I n2 :: nil => S (Int.add n1 n2)
-  | Oaddshift s, S n1 :: I n2 :: nil => S (Int.add n1 (eval_static_shift s n2))
-  | Oadd, I n1 :: G s2 n2 :: nil => G s2 (Int.add n1 n2)
-  | Oadd, I n1 :: S n2 :: nil => S (Int.add n1 n2)
-  | Oaddimm n, I n1 :: nil => I (Int.add n1 n)
-  | Oaddimm n, G s1 n1 :: nil => G s1 (Int.add n1 n)
-  | Oaddimm n, S n1 :: nil => S (Int.add n1 n)
-  | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2)
-  | Osubshift s, I n1 :: I n2 :: nil => I(Int.sub n1 (eval_static_shift s n2))
-  | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
-  | Osub, S n1 :: I n2 :: nil => S (Int.sub n1 n2)
-  | Osubshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 (eval_static_shift s n2))
-  | Orsubshift s, I n1 :: I n2 :: nil => I(Int.sub (eval_static_shift s n2) n1)
-  | Orsubimm n, I n1 :: nil => I (Int.sub n n1)
-  | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
-  | Omla, I n1 :: I n2 :: I n3 :: nil => I(Int.add (Int.mul n1 n2) n3)
-  | 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)
-  | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
-  | Oandshift s, I n1 :: I n2 :: nil => I(Int.and n1 (eval_static_shift s n2))
-  | Oandimm n, I n1 :: nil => I(Int.and n1 n)
-  | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2)
-  | Oorshift s, I n1 :: I n2 :: nil => I(Int.or n1 (eval_static_shift s n2))
-  | Oorimm n, I n1 :: nil => I(Int.or n1 n)
-  | Oxor, I n1 :: I n2 :: nil => I(Int.xor n1 n2)
-  | Oxorshift s, I n1 :: I n2 :: nil => I(Int.xor n1 (eval_static_shift s n2))
-  | Oxorimm n, I n1 :: nil => I(Int.xor n1 n)
-  | Obic, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not n2))
-  | Obicshift s, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not (eval_static_shift s n2)))
-  | Onot, I n1 :: nil => I(Int.not n1)
-  | Onotshift s, I n1 :: nil => I(Int.not (eval_static_shift s n1))
-  | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
-  | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
-  | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
-  | Oshift s, I n1 :: nil => I(eval_static_shift s n1)
-  | 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
-  | Ointuoffloat, F n1 :: nil => eval_static_intuoffloat n1
-  | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown
-  | Ofloatofintu, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofintu 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.
-
-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, I n1::I n2::nil => I (Int.add n1 n2)
-  | Aindexed2, G id ofs::I n2::nil => G id (Int.add ofs n2)
-  | Aindexed2, I n1::G id ofs::nil => G id (Int.add ofs n1)
-  | Aindexed2, S ofs::I n2::nil => S (Int.add ofs n2)
-  | Aindexed2, I n1::S ofs::nil => S (Int.add ofs n1)
-  | Aindexed2shift s, I n1::I n2::nil => I (Int.add n1 (eval_static_shift s n2))
-  | Aindexed2shift s, G id ofs::I n2::nil => G id (Int.add ofs (eval_static_shift s n2))
-  | Aindexed2shift s, S ofs::I n2::nil => S (Int.add ofs (eval_static_shift s n2))
-  | Ainstack ofs, nil => S ofs
-  | _, _ => Unknown
-  end.
-
-
-(** * Operator strength reduction *)
-
-(** We now define auxiliary functions for strength reduction of
-  operators and addressing modes: replacing an operator with a cheaper
-  one if some of its arguments are statically known.  These are again
-  large pattern-matchings expressed in indirect style. *)
-
-Section STRENGTH_REDUCTION.
-
 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)
@@ -272,9 +127,12 @@ Definition make_divuimm (n: int) (r1 r2: reg) :=
   | None   => (Odivu, r1 :: r2 :: nil)
   end.
 
-Definition make_andimm (n: int) (r: reg) :=
+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) :=
@@ -292,9 +150,20 @@ 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_cast16signed (r: reg) (a: aval) :=
+  if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, 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
+  | Ocast16signed, r1 :: nil, v1 :: nil => make_cast16signed r1 v1
   | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_addimm n1 r2
   | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm n2 r1
   | Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (eval_static_shift s n2) r1
@@ -306,20 +175,21 @@ Nondetfunction op_strength_reduction
   | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 r2
   | 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
-  | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2
-  | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1
-  | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (eval_static_shift s 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
+  | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (eval_static_shift s n2) 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
   | Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm (eval_static_shift s n2) r1
   | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2
   | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1
   | Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm (eval_static_shift s n2) r1
-  | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not n2) r1
-  | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not (eval_static_shift s n2)) r1
+  | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not n2) r1 v1
+  | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not (eval_static_shift s n2)) r1 v1
   | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
   | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
   | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
+  | 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')
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
@@ -329,21 +199,21 @@ Nondetfunction op_strength_reduction
 
 
 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
-  | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil =>
+  | Aindexed2, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil =>
       (Ainstack (Int.add n1 n2), nil)
-  | Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil =>
+  | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil =>
       (Ainstack (Int.add n1 n2), nil)
   | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
       (Aindexed n1, r2 :: nil)
   | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed n2, r1 :: nil)
-  | Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil =>
+  | Aindexed2shift s, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil =>
       (Ainstack (Int.add n1 (eval_static_shift s n2)), nil)
   | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed (eval_static_shift s n2), r1 :: nil)
-  | Aindexed n, r1 :: nil, S n1 :: nil =>
+  | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil =>
       (Ainstack (Int.add n1 n), nil)
   | _, _, _ =>
       (addr, args)
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index f0d6b7f..ad7dcd1 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -23,161 +23,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_shift_correct:
-  forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n).
-Proof.
-  intros. destruct s; simpl; rewrite s_range; auto.
-Qed.
-
-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; try (rewrite eval_static_shift_correct); 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_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); try (rewrite eval_static_shift_correct); auto.
-  destruct (propagate_float_constants tt); simpl; auto.
-  rewrite shift_symbol_address; auto. 
-  rewrite shift_symbol_address; auto.
-  rewrite Val.add_assoc; auto.
-  rewrite Val.add_assoc; auto.
-  fold (Val.add (Vint n1) (symbol_address ge s2 n2)).
-  rewrite Int.add_commut. rewrite Val.add_commut. rewrite shift_symbol_address; auto.
-  fold (Val.add (Vint n1) (Val.add sp (Vint n2))). 
-  rewrite Val.add_permut. auto.
-  rewrite shift_symbol_address. auto.
-  rewrite Val.add_assoc. auto.
-  rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
-  rewrite Val.sub_add_opp. rewrite Val.add_assoc. rewrite Int.sub_add_opp. 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.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0; simpl; auto.
-  unfold eval_static_intuoffloat. destruct (Float.intuoffloat n1); simpl in H0; inv H0; simpl; auto.
-  destruct (propagate_float_constants tt); simpl; auto.
-  destruct (propagate_float_constants tt); simpl; auto.
-  unfold eval_static_condition_val, Val.of_optbool.
-  destruct (eval_static_condition c vl0) eqn:?.
-  rewrite (eval_static_condition_correct _ _ _ m _ H Heqo).
-  destruct b; simpl; auto. 
-  simpl; 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); try (rewrite eval_static_shift_correct); 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. apply Val.add_commut.
-  repeat rewrite Val.add_assoc. auto.
-  fold (Val.add (Vint n1) (Val.add sp (Vint ofs))).
-  rewrite Val.add_permut. decEq. rewrite Val.add_commut. auto.
-  rewrite shift_symbol_address. auto.
-  rewrite Val.add_assoc. auto.
-Qed.
 
 (** * Correctness of strength reduction *)
 
@@ -189,50 +36,99 @@ Qed.
 
 Section STRENGTH_REDUCTION.
 
-Variable app: D.t.
+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 rs: regset.
 Variable m: mem.
-Hypothesis MATCH: forall r, val_match_approx (approx_reg app r) rs#r.
+Hypothesis MATCH: ematch bc rs ae.
+
+Lemma match_G:
+  forall r id ofs,
+  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#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 rs#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 eval_static_shift_correct:
+  forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n).
+Proof.
+  intros. destruct s; simpl; rewrite s_range; auto.
+Qed.
+
 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.
 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.
-  rewrite H. rewrite eval_static_shift_correct. auto.
-  rewrite H. rewrite eval_static_shift_correct. auto.
-  auto.
-  destruct (Float.eq_dec n1 Float.zero); simpl; auto.
-  rewrite H0; subst n1. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
-  destruct (Float.eq_dec n2 Float.zero); simpl; auto.
-  congruence.
-  destruct (Float.eq_dec n1 Float.zero); simpl; auto.
-  rewrite H0; subst n1. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
-  destruct (Float.eq_dec n2 Float.zero); simpl; auto.
-  congruence.
-  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.
+- rewrite eval_static_shift_correct. auto.
+- rewrite eval_static_shift_correct. auto. 
+- destruct (Float.eq_dec n1 Float.zero).
+  subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
+  simpl. rewrite H1; auto. 
+- destruct (Float.eq_dec n2 Float.zero).
+  subst n2. simpl. auto.
+  simpl. rewrite H1; auto.
+- destruct (Float.eq_dec n1 Float.zero).
+  subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
+  simpl. rewrite H1; auto. 
+- destruct (Float.eq_dec n2 Float.zero); simpl; auto.
+  subst n2; auto.
+  rewrite H1; auto. 
+- auto.
 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 rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. 
@@ -244,7 +140,7 @@ Lemma make_shlimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_shlimm n r1 r2 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 rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v.
 Proof.
   Opaque mk_shift_amount.
   intros; unfold make_shlimm.
@@ -259,7 +155,7 @@ Lemma make_shrimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_shrimm n r1 r2 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 rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -273,7 +169,7 @@ Lemma make_shruimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_shruimm n r1 r2 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 rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -287,7 +183,7 @@ Lemma make_mulimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_mulimm n r1 r2 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 rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_mulimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -306,7 +202,7 @@ Lemma make_divimm_correct:
   Val.divs rs#r1 rs#r2 = Some v ->
   rs#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 rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -321,7 +217,7 @@ Lemma make_divuimm_correct:
   Val.divu rs#r1 rs#r2 = Some v ->
   rs#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 rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -333,22 +229,35 @@ 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 rs#r x ->
+  let (op, args) := make_andimm n r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#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.
   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.
+  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 (rs#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 rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v.
 Proof.
   intros; unfold make_orimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -361,7 +270,7 @@ 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 rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v.
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -376,7 +285,7 @@ Lemma make_mulfimm_correct:
   forall n r1 r2,
   rs#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 rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
   destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
@@ -389,7 +298,7 @@ Lemma make_mulfimm_correct_2:
   forall n r1 r2,
   rs#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 rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
   destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
@@ -399,92 +308,151 @@ Proof.
   simpl. econstructor; split; eauto. 
 Qed.
 
+Lemma make_cast8signed_correct:
+  forall r x,
+  vmatch bc rs#r x ->
+  let (op, args) := make_cast8signed r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v.
+Proof.
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. 
+  exists rs#r; split; auto. 
+  assert (V: vmatch bc rs#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_cast16signed_correct:
+  forall r x,
+  vmatch bc rs#r x ->
+  let (op, args) := make_cast16signed r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v.
+Proof.
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. 
+  exists rs#r; split; auto. 
+  assert (V: vmatch bc rs#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_singleoffloat_correct:
+  forall r x,
+  vmatch bc rs#r x ->
+  let (op, args) := make_singleoffloat r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.singleoffloat rs#r) v.
+Proof.
+  intros; unfold make_singleoffloat. 
+  destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. 
+  InvBooleans. exists rs#r; split; auto. 
+  assert (V: vmatch bc rs#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 rs##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' rs##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.
+(* cast8signed *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto.
 (* add *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.add_commut. apply make_addimm_correct.
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_addimm_correct.
+  InvApproxRegs; SimplVM. inv H0. 
+  fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. apply make_addimm_correct.
+  InvApproxRegs; SimplVM. inv H0. apply make_addimm_correct.
 (* addshift *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_addimm_correct.
+  InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_addimm_correct.
 (* sub *)
-  InvApproxRegs; SimplVMA. inv H0. rewrite H1. econstructor; split; eauto. 
-  InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite Val.sub_add_opp. apply make_addimm_correct.
+  InvApproxRegs; SimplVM. inv H0. econstructor; split; eauto. 
+  InvApproxRegs; SimplVM. inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct.
 (* subshift *)
-  InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. rewrite Val.sub_add_opp. apply make_addimm_correct.
+  InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. rewrite Val.sub_add_opp. apply make_addimm_correct.
 (* rsubshift *)
-  InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. econstructor; split; eauto.
+  InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. econstructor; split; eauto.
 (* 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.
+  InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2).
+  rewrite Val.mul_commut. 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 (rs#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 (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divuimm_correct; auto.
 (* and *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.and_commut. apply make_andimm_correct.
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_andimm_correct.
+  InvApproxRegs; SimplVM. inv H0. fold (Val.and (Vint n1) rs#r2). rewrite Val.and_commut. apply make_andimm_correct; auto.
+  InvApproxRegs; SimplVM. inv H0. apply make_andimm_correct; auto.
 (* andshift *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_andimm_correct.
+  InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_andimm_correct; auto.
 (* or *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.or_commut. apply make_orimm_correct.
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_orimm_correct.
+  InvApproxRegs; SimplVM. inv H0. fold (Val.or (Vint n1) rs#r2). rewrite Val.or_commut. apply make_orimm_correct.
+  InvApproxRegs; SimplVM. inv H0. apply make_orimm_correct.
 (* orshift *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_orimm_correct.
+  InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_orimm_correct.
 (* xor *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.xor_commut. apply make_xorimm_correct.
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_xorimm_correct.
+  InvApproxRegs; SimplVM. inv H0. fold (Val.xor (Vint n1) rs#r2). rewrite Val.xor_commut. apply make_xorimm_correct.
+  InvApproxRegs; SimplVM. inv H0. apply make_xorimm_correct.
 (* xorshift *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_xorimm_correct.
+  InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_xorimm_correct.
 (* bic *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_andimm_correct.
+  InvApproxRegs; SimplVM. inv H0. apply make_andimm_correct; auto.
 (* bicshift *)
-  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_andimm_correct.
+  InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_andimm_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.
+(* singleoffloat *)
+  InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cmp *)
   generalize (cond_strength_reduction_correct c args0 vl0). 
   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) rs#r2).
+  rewrite <- H2. apply make_mulfimm_correct_2; auto.
 (* default *)
   exists v; 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 rs##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' rs##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 H; rewrite H0. rewrite Val.add_assoc; auto.
-  rewrite H; rewrite H0. rewrite Val.add_permut; auto. 
-  rewrite H0. rewrite Val.add_commut. auto.
-  rewrite H. auto.
-  rewrite H; rewrite H0. rewrite Val.add_assoc. rewrite eval_static_shift_correct. auto.
-  rewrite H. rewrite eval_static_shift_correct. auto.
-  rewrite H. rewrite Val.add_assoc. 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 Int.add_zero_l. 
+  change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)).
+  econstructor; split; eauto. apply Val.add_lessdef; auto.
+- fold (Val.add (Vint n1) rs#r2).  rewrite Int.add_zero_l. rewrite Int.add_commut.
+  change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)).
+  rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto.
+- fold (Val.add (Vint n1) rs#r2).
+  rewrite Val.add_commut. econstructor; split; eauto.
+- econstructor; split; eauto.
+- rewrite eval_static_shift_correct. rewrite Int.add_zero_l. 
+  change (Vptr sp (Int.add n1 (eval_static_shift s n2)))
+    with (Val.add (Vptr sp n1) (Vint (eval_static_shift s n2))).
+  econstructor; split; eauto. apply Val.add_lessdef; auto.
+- rewrite eval_static_shift_correct. econstructor; split; eauto. 
+- rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). 
+  econstructor; split; eauto. apply Val.add_lessdef; auto.
+- exists res; auto.
 Qed.
 
 End STRENGTH_REDUCTION.
-
-End ANALYSIS.
diff --git a/arm/NeedOp.v b/arm/NeedOp.v
new file mode 100644
index 0000000..3fb0d72
--- /dev/null
+++ b/arm/NeedOp.v
@@ -0,0 +1,204 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+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 ARM operators *)
+
+Definition needs_of_condition (cond: condition): list nval := nil.
+
+Definition needs_of_shift (s: shift) (nv: nval): nval :=
+  match s with
+  | Slsl x => shlimm nv x
+  | Slsr x => shruimm nv x
+  | Sasr x => shrimm nv x
+  | Sror x => ror nv x
+  end.
+
+Definition op1 (nv: nval) := nv :: nil.
+Definition op2 (nv: nval) := nv :: nv :: nil.
+Definition op2shift (s: shift) (nv: nval) := nv :: needs_of_shift s nv :: nil.
+
+Definition needs_of_operation (op: operation) (nv: nval): list nval :=
+  match op with
+  | Omove => nv::nil
+  | Ointconst n => nil
+  | Ofloatconst n => nil
+  | Oaddrsymbol id ofs => nil
+  | Oaddrstack ofs => nil
+  | Ocast8signed => op1 (sign_ext 8 nv)
+  | Ocast16signed => op1 (sign_ext 16 nv)
+  | Oadd => op2 (modarith nv)
+  | Oaddshift s => op2shift s (modarith nv)
+  | Oaddimm _ => op1 (modarith nv)
+  | Osub => op2 (default nv)
+  | Osubshift s => op2shift s (default nv)
+  | Orsubshift s => op2shift s (default nv)
+  | Orsubimm _ => op1 (default nv)
+  | Omul => op2 (modarith nv)
+  | Omla => let n := modarith nv in let n2 := modarith n in n2::n2::n::nil
+  | Omulhu | Omulhs | Odiv | Odivu => let n := default nv in n::n::nil
+  | Oand => op2 (bitwise nv)
+  | Oandshift s => op2shift s (bitwise nv)
+  | Oandimm n => op1 (andimm nv n)
+  | Oor => op2 (bitwise nv)
+  | Oorshift s => op2shift s (bitwise nv)
+  | Oorimm n => op1 (orimm nv n)
+  | Oxor => op2 (bitwise nv)
+  | Oxorshift s => op2shift s (bitwise nv)
+  | Oxorimm n => op1 (bitwise nv)
+  | Obic => let n := bitwise nv in n::bitwise n::nil
+  | Obicshift s => let n := bitwise nv in n::needs_of_shift s (bitwise n)::nil
+  | Onot => op1 (bitwise nv)
+  | Onotshift s => op1 (needs_of_shift s (bitwise nv))
+  | Oshl | Oshr | Oshru => op2 (default nv)
+  | Oshift s => op1 (needs_of_shift s nv)
+  | Oshrximm _ => op1 (default nv)
+  | Onegf | Oabsf => op1 (default nv)
+  | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
+  | Osingleoffloat => op1 (singleoffloat nv)
+  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
+  | Omakelong => op2 (default nv)
+  | Olowlong | Ohighlong => op1 (default nv)
+  | Ocmp c => needs_of_condition c
+  end.
+
+Definition operation_is_redundant (op: operation) (nv: nval): bool :=
+  match op with
+  | Ocast8signed => sign_ext_redundant 8 nv
+  | Ocast16signed => sign_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
+  | _ => 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. unfold needs_of_condition in H0. 
+  eapply default_needs_of_condition_sound; eauto.
+Qed.
+
+Lemma needs_of_shift_sound:
+  forall v v' s nv,
+  vagree v v' (needs_of_shift s nv) ->
+  vagree (eval_shift s v) (eval_shift s v') nv.
+Proof.
+  intros. destruct s; simpl in *. 
+  apply shlimm_sound; auto.
+  apply shruimm_sound; auto.
+  apply shrimm_sound; auto. 
+  apply ror_sound; auto.
+Qed.
+
+Lemma val_sub_lessdef:
+  forall v1 v1' v2 v2',
+  Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.sub v1 v2) (Val.sub v1' v2').
+Proof.
+  intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.
+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.
+- apply sign_ext_sound; auto. compute; auto.
+- apply sign_ext_sound; auto. compute; auto.
+- apply add_sound; auto.
+- apply add_sound; auto. apply needs_of_shift_sound; auto. 
+- apply add_sound; auto with na.
+- replace (default nv) with All in *. 
+  apply vagree_lessdef. apply val_sub_lessdef; auto with na. 
+  apply lessdef_vagree. apply needs_of_shift_sound; auto with na.
+  destruct nv; simpl; congruence.
+- replace (default nv) with All in *. 
+  apply vagree_lessdef. apply val_sub_lessdef; auto with na. 
+  apply lessdef_vagree. apply needs_of_shift_sound; auto with na.
+  destruct nv; simpl; congruence.
+- apply mul_sound; auto. 
+- apply add_sound; auto. apply mul_sound; auto. 
+- apply and_sound; auto.
+- apply and_sound; auto. apply needs_of_shift_sound; auto. 
+- apply andimm_sound; auto.
+- apply or_sound; auto.
+- apply or_sound; auto. apply needs_of_shift_sound; auto. 
+- apply orimm_sound; auto.
+- apply xor_sound; auto.
+- apply xor_sound; auto. apply needs_of_shift_sound; auto. 
+- apply xor_sound; auto with na.
+- apply and_sound; auto. apply notint_sound; auto. 
+- apply and_sound; auto. apply notint_sound. apply needs_of_shift_sound; auto. 
+- apply notint_sound; auto. 
+- apply notint_sound. apply needs_of_shift_sound; auto.
+- apply needs_of_shift_sound; auto. 
+- apply singleoffloat_sound; auto. 
+Qed.
+
+Lemma operation_is_redundant_sound:
+  forall op nv arg1 args v arg1' args',
+  operation_is_redundant op nv = true ->
+  eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v ->
+  vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) ->
+  vagree v arg1' nv.
+Proof.
+  intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst.
+- apply sign_ext_redundant_sound; auto. omega.
+- apply sign_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/arm/Op.v b/arm/Op.v
index fe97d36..7323abc 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -73,6 +73,8 @@ 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] *)
+  | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
   | Oadd: operation                     (**r [rd = r1 + r2] *)
   | Oaddshift: shift -> operation       (**r [rd = r1 + shifted r2] *)
   | Oaddimm: int -> operation           (**r [rd = r1 + n] *)
@@ -219,6 +221,8 @@ Definition eval_operation
   | Ofloatconst n, nil => Some (Vfloat n)
   | Oaddrsymbol s ofs, nil => Some (symbol_address genv s ofs)
   | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
+  | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1)
+  | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
   | 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))
@@ -314,6 +318,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat)
   | Oaddrsymbol _ _ => (nil, Tint)
   | Oaddrstack _ => (nil, Tint)
+  | Ocast8signed => (Tint :: nil, Tint)
+  | Ocast16signed => (Tint :: nil, Tint)
   | Oadd => (Tint :: Tint :: nil, Tint)
   | Oaddshift _ => (Tint :: Tint :: nil, Tint)
   | Oaddimm _ => (Tint :: nil, Tint)
@@ -393,6 +399,8 @@ Proof with (try exact I).
   destruct (Float.is_single_dec f); red; auto. 
   unfold symbol_address. destruct (Genv.find_symbol genv i)...
   destruct sp...
+  destruct v0...
+  destruct v0...
   destruct v0; destruct v1...
   generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto.
   destruct v0...
@@ -820,6 +828,8 @@ Lemma eval_operation_inj:
 Proof.
   intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply Values.val_add_inject; auto.
+  inv H4; simpl; auto.
+  inv H4; simpl; auto.
   apply Values.val_add_inject; auto.
   apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
   apply Values.val_add_inject; auto.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 6398ba3..99dfa46 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -106,9 +106,9 @@ let movimm oc dst n =
   match Asmgen.decompose_int n with
   | [] -> assert false
   | hd::tl as l ->
-      fprintf oc "	mov	%s, #%a\n" dst coqint hd
+      fprintf oc "	mov	%s, #%a\n" dst coqint hd;
       List.iter
-        (fun n -> fprintf oc "	orr	%s, %s, #%a" dst dst coqint n)
+        (fun n -> fprintf oc "	orr	%s, %s, #%a\n" dst dst coqint n)
         tl;
       List.length l
 
@@ -116,9 +116,9 @@ let addimm oc dst src n =
   match Asmgen.decompose_int n with
   | [] -> assert false
   | hd::tl as l ->
-      fprintf oc "	add	%s, %s, #%a\n" dst src coqint hd
+      fprintf oc "	add	%s, %s, #%a\n" dst src coqint hd;
       List.iter
-        (fun n -> fprintf oc "	add	%s, %s, #%a" dst dst coqint n)
+        (fun n -> fprintf oc "	add	%s, %s, #%a\n" dst dst coqint n)
         tl;
       List.length l
 
@@ -126,9 +126,9 @@ let subimm oc dst src n =
   match Asmgen.decompose_int n with
   | [] -> assert false
   | hd::tl as l ->
-      fprintf oc "	sub	%s, %s, #%a\n" dst src coqint hd
+      fprintf oc "	sub	%s, %s, #%a\n" dst src coqint hd;
       List.iter
-        (fun n -> fprintf oc "	sub	%s, %s, #%a" dst dst coqint n)
+        (fun n -> fprintf oc "	sub	%s, %s, #%a\n" dst dst coqint n)
         tl;
       List.length l
 
@@ -425,7 +425,7 @@ let print_builtin_va_start oc r =
     Int32.add
       (next_arg_location 0 0 (!current_function_sig).sig_args)
       !current_function_stacksize in
-  let n = addimm oc "r14" "sp" (coqint_of_camlint ofs);
+  let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in
   fprintf oc "	str	r14, [%a, #0]\n" ireg r;
   n + 1
 
@@ -716,10 +716,10 @@ let print_instruction oc = function
       fprintf oc "	mov	r12, sp\n";
       if (!current_function_sig).sig_cc.cc_vararg then begin
         fprintf oc "	push	{r0, r1, r2, r3}\n";
-        cfi_adjust oc 16
+        cfi_adjust oc 16l
       end;
       let sz' = camlint_of_coqint sz in
-      let ninstr = subimm "sp" "sp" sz in
+      let ninstr = subimm oc "sp" "sp" sz in
       cfi_adjust oc sz';
       fprintf oc "	str	r12, [sp, #%a]\n" coqint ofs;
       current_function_stacksize := sz';
@@ -727,7 +727,7 @@ let print_instruction oc = function
   | Pfreeframe(sz, ofs) ->
       let sz =
         if (!current_function_sig).sig_cc.cc_vararg
-        then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz)
+        then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz))
         else sz in
       if Asmgen.is_immed_arith sz
       then fprintf oc "	add	sp, sp, #%a\n" coqint sz
@@ -805,6 +805,7 @@ let rec print_instructions oc instrs =
 let print_function oc name fn =
   Hashtbl.clear current_function_labels;
   reset_constants();
+  current_function_sig := fn.fn_sig;
   currpos := 0;
   let text =
     match C2C.atom_sections name with
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index 4be41eb..96d1394 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -63,6 +63,8 @@ let print_operation reg pp = function
       fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs)
   | Oaddrstack ofs, [] ->
       fprintf pp "stack(%ld)" (camlint_of_coqint ofs)
+  | Ocast8signed, [r1] -> fprintf pp "int8signed(%a)" reg r1
+  | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1
   | Oadd, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2
   | Oaddshift s, [r1;r2] -> fprintf pp "%a + %a %a" reg r1 reg r2 shift s
   | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n)
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 4cd09d1..767e747 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -369,11 +369,11 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
 
 Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
 
-Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24).
+Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
 
 Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
 
-Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16).
+Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
 
 (** ** Floating-point conversions *)
 
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 9beb1ad..9fbab44 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -716,12 +716,7 @@ Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
-  red; intros. unfold cast8signed.
-  exploit (eval_shlimm (Int.repr 24)); eauto. intros [v1 [A1 B1]].
-  exploit (eval_shrimm (Int.repr 24)). eexact A1. intros [v2 [A2 B2]].
-  exists v2; split; auto. 
-  destruct x; simpl; auto. simpl in *. inv B1. simpl in *. inv B2. 
-  rewrite Int.sign_ext_shr_shl. auto. compute; auto.
+  red; intros. unfold cast8signed. TrivialExists.
 Qed.
 
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
@@ -732,12 +727,7 @@ Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
 Proof.
-  red; intros. unfold cast16signed.
-  exploit (eval_shlimm (Int.repr 16)); eauto. intros [v1 [A1 B1]].
-  exploit (eval_shrimm (Int.repr 16)). eexact A1. intros [v2 [A2 B2]].
-  exists v2; split; auto. 
-  destruct x; simpl; auto. simpl in *. inv B1. simpl in *. inv B2. 
-  rewrite Int.sign_ext_shr_shl. auto. compute; auto.
+  red; intros. unfold cast16signed. TrivialExists.
 Qed.
 
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
new file mode 100644
index 0000000..c968213
--- /dev/null
+++ b/arm/ValueAOp.v
@@ -0,0 +1,193 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+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 ARM operators *)
+
+Definition eval_static_shift (s: shift) (v: aval): aval :=
+  match s with
+  | Slsl x => shl v (I x)
+  | Slsr x => shru v (I x)
+  | Sasr x => shr v (I x)
+  | Sror x => ror v (I x)
+  end.
+
+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
+  | Ccompshift c s, v1 :: v2 :: nil => cmp_bool c v1 (eval_static_shift s v2)
+  | Ccompushift c s, v1 :: v2 :: nil => cmpu_bool c v1 (eval_static_shift s 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)
+  | Ccompfzero c, v1 :: nil => cmpf_bool c v1 (F Float.zero)
+  | Cnotcompfzero c, v1 :: nil => cnot (cmpf_bool c v1 (F Float.zero))
+  | _, _ => 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, v1::v2::nil => add v1 v2
+  | Aindexed2shift s, v1::v2::nil => add v1 (eval_static_shift s v2)
+  | 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
+  | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs)
+  | Oaddrstack ofs, nil => Ptr (Stk ofs)
+  | Ocast8signed, v1 :: nil => sign_ext 8 v1
+  | Ocast16signed, v1 :: nil => sign_ext 16 v1
+  | Oadd, v1::v2::nil => add v1 v2
+  | Oaddshift s, v1::v2::nil => add v1 (eval_static_shift s v2)
+  | Oaddimm n, v1::nil => add v1 (I n)
+  | Osub, v1::v2::nil => sub v1 v2
+  | Osubshift s, v1::v2::nil => sub v1 (eval_static_shift s v2)
+  | Orsubshift s, v1::v2::nil => sub (eval_static_shift s v2) v1
+  | Orsubimm n, v1::nil => sub (I n) v1
+  | Omul, v1::v2::nil => mul v1 v2
+  | Omla, v1::v2::v3::nil => add (mul v1 v2) v3
+  | 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
+  | Oand, v1::v2::nil => and v1 v2
+  | Oandshift s, v1::v2::nil => and v1 (eval_static_shift s v2)
+  | Oandimm n, v1::nil => and v1 (I n)
+  | Oor, v1::v2::nil => or v1 v2
+  | Oorshift s, v1::v2::nil => or v1 (eval_static_shift s v2)
+  | Oorimm n, v1::nil => or v1 (I n)
+  | Oxor, v1::v2::nil => xor v1 v2
+  | Oxorshift s, v1::v2::nil => xor v1 (eval_static_shift s v2)
+  | Oxorimm n, v1::nil => xor v1 (I n)
+  | Obic, v1::v2::nil => and v1 (notint v2)
+  | Obicshift s, v1::v2::nil => and v1 (notint (eval_static_shift s v2))
+  | Onot, v1::nil => notint v1
+  | Onotshift s, v1::nil => notint (eval_static_shift s v1)
+  | Oshl, v1::v2::nil => shl v1 v2
+  | Oshr, v1::v2::nil => shr v1 v2
+  | Oshru, v1::v2::nil => shru v1 v2
+  | Oshift s, v1::nil => eval_static_shift s v1
+  | Oshrximm n, v1::nil => shrx v1 (I n)
+  | 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
+  | Ointuoffloat, v1::nil => intuoffloat v1
+  | Ofloatofint, v1::nil => floatofint v1
+  | Ofloatofintu, v1::nil => floatofintu 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.
+
+Lemma eval_static_shift_sound:
+  forall s v a,
+  vmatch bc v a ->
+  vmatch bc (eval_shift s v) (eval_static_shift s a).
+Proof.
+  intros. unfold eval_shift, eval_static_shift. destruct s; eauto with va.
+Qed.
+
+Hint Resolve eval_static_shift_sound: va.
+
+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.
+  rewrite Int.add_zero_l; eauto with va.
+  fold (Val.sub (Vint i) a1). auto with va.
+  apply of_optbool_sound. eapply eval_static_condition_sound; eauto. 
+Qed.
+
+End SOUNDNESS.
+
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 9efeca1..98bc14a 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -31,24 +31,34 @@ Require Import NeedOp.
 
 (** * Part 1: the static analysis *)
 
+Definition add_need_all (r: reg) (ne: nenv) : nenv :=
+  NE.set r All ne.
+
 Definition add_need (r: reg) (nv: nval) (ne: nenv) : nenv :=
   NE.set r (nlub nv (NE.get r ne)) ne.
 
-Fixpoint add_needs (rl: list reg) (nv: nval) (ne: nenv) : nenv :=
+Fixpoint add_needs_all (rl: list reg) (ne: nenv) : nenv :=
   match rl with
   | nil => ne
-  | r1 :: rs => add_need r1 nv (add_needs rs nv ne)
+  | r1 :: rs => add_need_all r1 (add_needs_all rs ne)
+  end.
+
+Fixpoint add_needs (rl: list reg) (nvl: list nval) (ne: nenv) : nenv :=
+  match rl, nvl with
+  | nil, _ => ne
+  | r1 :: rs, nil => add_needs_all rl ne
+  | r1 :: rs, nv1 :: nvs => add_need r1 nv1 (add_needs rs nvs ne)
   end.
 
-Definition add_ros_need (ros: reg + ident) (ne: nenv) : nenv :=
+Definition add_ros_need_all (ros: reg + ident) (ne: nenv) : nenv :=
   match ros with
-  | inl r => add_need r All ne
+  | inl r => add_need_all r ne
   | inr s => ne
   end.
 
-Definition add_opt_need (or: option reg) (ne: nenv) : nenv :=
+Definition add_opt_need_all (or: option reg) (ne: nenv) : nenv :=
   match or with
-  | Some r => add_need r All ne
+  | Some r => add_need_all r ne
   | None => ne
   end.
 
@@ -64,26 +74,26 @@ Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (
                           (ne: NE.t) (nm: nmem) : NA.t :=
   match ef, args with
   | EF_vload chunk, a1::nil =>
-      (add_needs args All (kill res ne),
+      (add_needs_all args (kill res ne),
        nmem_add nm (aaddr app a1) (size_chunk chunk))
   | EF_vload_global chunk id ofs, nil =>
-      (add_needs args All (kill res ne),
+      (add_needs_all args (kill res ne),
        nmem_add nm (Gl id ofs) (size_chunk chunk))
   | EF_vstore chunk, a1::a2::nil =>
-      (add_need a1 All (add_need a2 (store_argument chunk) (kill res ne)), nm)
+      (add_need_all a1 (add_need a2 (store_argument chunk) (kill res ne)), nm)
   | EF_vstore_global chunk id ofs, a1::nil =>
       (add_need a1 (store_argument chunk) (kill res ne), nm)
   | EF_memcpy sz al, dst::src::nil =>
       if nmem_contains nm (aaddr app dst) sz then
-       (add_needs args All (kill res ne),
+       (add_needs_all args (kill res ne),
         nmem_add (nmem_remove nm (aaddr app dst) sz) (aaddr app src) sz)
       else (ne, nm)
   | EF_annot txt targs, _ =>
-      (add_needs args All (kill res ne), nm)
+      (add_needs_all args (kill res ne), nm)
   | EF_annot_val txt targ, _ =>
-      (add_needs args All (kill res ne), nm)
+      (add_needs_all args (kill res ne), nm)
   | _, _ =>
-      (add_needs args All (kill res ne), nmem_all) 
+      (add_needs_all args (kill res ne), nmem_all) 
   end.
 
 Definition transfer (f: function) (approx: PMap.t VA.t)
@@ -103,27 +113,27 @@ Definition transfer (f: function) (approx: PMap.t VA.t)
       let ndst := nreg ne dst in
       if is_dead ndst then after
       else if is_int_zero ndst then (kill dst ne, nm)
-      else (add_needs args All (kill dst ne),
+      else (add_needs_all args (kill dst ne),
             nmem_add nm (aaddressing approx!!pc addr args) (size_chunk chunk))
   | Some (Istore chunk addr args src s) =>
       let p := aaddressing approx!!pc addr args in
       if nmem_contains nm p (size_chunk chunk)
-      then (add_needs args All (add_need src (store_argument chunk) ne),
+      then (add_needs_all args (add_need src (store_argument chunk) ne),
             nmem_remove nm p (size_chunk chunk))
       else after
   | Some(Icall sig ros args res s) =>
-      (add_needs args All (add_ros_need ros (kill res ne)), nmem_all)
+      (add_needs_all args (add_ros_need_all ros (kill res ne)), nmem_all)
   | Some(Itailcall sig ros args) =>
-      (add_needs args All (add_ros_need ros NE.bot),
+      (add_needs_all args (add_ros_need_all ros NE.bot),
        nmem_dead_stack f.(fn_stacksize))
   | Some(Ibuiltin ef args res s) =>
       transfer_builtin approx!!pc ef args res ne nm
   | Some(Icond cond args s1 s2) =>
       (add_needs args (needs_of_condition cond) ne, nm)
   | Some(Ijumptable arg tbl) =>
-      (add_need arg All ne, nm)
+      (add_need_all arg ne, nm)
   | Some(Ireturn optarg) =>
-      (add_opt_need optarg ne, nmem_dead_stack f.(fn_stacksize))
+      (add_opt_need_all optarg ne, nmem_dead_stack f.(fn_stacksize))
   end.
 
 Module DS := Backward_Dataflow_Solver(NA)(NodeSetBackward).
@@ -144,7 +154,10 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t)
       else if is_int_zero nres then
         Iop (Ointconst Int.zero) nil res s
       else if operation_is_redundant op nres then 
-        match args with arg :: _ => Iop Omove (arg :: nil) res s | nil => instr end
+        match args with
+        | arg :: _ => Iop Omove (arg :: nil) res s
+        | nil => instr
+        end
       else
         instr
   | Iload chunk addr args dst s =>
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index deb8628..2fdedc6 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -264,83 +264,90 @@ Qed.
 
 (** * Properties of the need environment *)
 
-Lemma add_need_ge:
-  forall r nv ne,
-  nge (NE.get r (add_need r nv ne)) nv /\ NE.ge (add_need r nv ne) ne.
+Lemma add_need_all_eagree:
+  forall e e' r ne,
+  eagree e e' (add_need_all r ne) -> eagree e e' ne.
 Proof.
-  intros. unfold add_need. split. 
-  rewrite NE.gsspec; rewrite peq_true. apply nge_lub_l. 
-  red. intros. rewrite NE.gsspec. destruct (peq p r).
-  subst. apply NVal.ge_lub_right. 
-  apply NVal.ge_refl. apply NVal.eq_refl. 
+  intros; red; intros. generalize (H r0). unfold add_need_all. 
+  rewrite NE.gsspec. destruct (peq r0 r); auto with na. 
 Qed.
 
-Lemma add_needs_ge:
-  forall rl nv ne,
-  (forall r, In r rl -> nge (NE.get r (add_needs rl nv ne)) nv)
-  /\ NE.ge (add_needs rl nv ne) ne.
+Lemma add_need_all_lessdef:
+  forall e e' r ne,
+  eagree e e' (add_need_all r ne) -> Val.lessdef e#r e'#r.
 Proof.
-  induction rl; simpl; intros. 
-  split. tauto. apply NE.ge_refl. apply NE.eq_refl.
-  destruct (IHrl nv ne) as [A B].
-  split; intros. 
-  destruct H. subst a. apply add_need_ge. 
-  apply nge_trans with (NE.get r (add_needs rl nv ne)). 
-  apply add_need_ge. apply A; auto.
-  eapply NE.ge_trans; eauto. apply add_need_ge.
+  intros. generalize (H r); unfold add_need_all. 
+  rewrite NE.gsspec, peq_true. auto with na.
 Qed.
 
 Lemma add_need_eagree:
-  forall e e' r nv ne, eagree e e' (add_need r nv ne) -> eagree e e' ne.
+  forall e e' r nv ne,
+  eagree e e' (add_need r nv ne) -> eagree e e' ne.
 Proof.
-  intros. eapply eagree_ge; eauto. apply add_need_ge. 
+  intros; red; intros. generalize (H r0); unfold add_need.
+  rewrite NE.gsspec. destruct (peq r0 r); auto.
+  subst r0. intros. eapply nge_agree; eauto. apply nge_lub_r.
 Qed.
 
 Lemma add_need_vagree:
-  forall e e' r nv ne, eagree e e' (add_need r nv ne) -> vagree e#r e'#r nv.
+  forall e e' r nv ne,
+  eagree e e' (add_need r nv ne) -> vagree e#r e'#r nv.
 Proof.
-  intros. eapply nge_agree. eapply add_need_ge. apply H. 
+  intros. generalize (H r); unfold add_need.
+  rewrite NE.gsspec, peq_true. intros. eapply nge_agree; eauto. apply nge_lub_l.
 Qed.
 
-Lemma add_needs_eagree:
-  forall nv rl e e' ne, eagree e e' (add_needs rl nv ne) -> eagree e e' ne.
+Lemma add_needs_all_eagree:
+  forall rl e e' ne,
+  eagree e e' (add_needs_all rl ne) -> eagree e e' ne.
 Proof.
-  intros. eapply eagree_ge; eauto. apply add_needs_ge. 
+  induction rl; simpl; intros.
+  auto.
+  apply IHrl. eapply add_need_all_eagree; eauto. 
 Qed.
 
-Lemma add_needs_vagree:
-  forall nv rl e e' ne, eagree e e' (add_needs rl nv ne) -> vagree_list e##rl e'##rl nv.
+Lemma add_needs_all_lessdef:
+  forall rl e e' ne,
+  eagree e e' (add_needs_all rl ne) -> Val.lessdef_list e##rl e'##rl.
 Proof.
-  intros. destruct (add_needs_ge rl nv ne) as [A B].
-  set (ne' := add_needs rl nv ne) in *. 
-  revert A; generalize rl. induction rl0; simpl; intros.
+  induction rl; simpl; intros. 
   constructor.
-  constructor. eapply nge_agree; eauto. apply IHrl0. auto. 
+  constructor. eapply add_need_all_lessdef; eauto. 
+  eapply IHrl. eapply add_need_all_eagree; eauto. 
 Qed.
 
-Lemma add_need_lessdef:
-  forall e e' r ne, eagree e e' (add_need r All ne) -> Val.lessdef e#r e'#r.
+Lemma add_needs_eagree:
+  forall rl nvl e e' ne,
+  eagree e e' (add_needs rl nvl ne) -> eagree e e' ne.
 Proof.
-  intros. apply lessdef_vagree. eapply add_need_vagree; eauto. 
+  induction rl; simpl; intros.
+  auto.
+  destruct nvl. apply add_needs_all_eagree with (a :: rl); auto.
+  eapply IHrl. eapply add_need_eagree; eauto. 
 Qed.
 
-Lemma add_needs_lessdef:
-  forall e e' rl ne, eagree e e' (add_needs rl All ne) -> Val.lessdef_list e##rl e'##rl.
+Lemma add_needs_vagree:
+  forall rl nvl e e' ne,
+  eagree e e' (add_needs rl nvl ne) -> vagree_list e##rl e'##rl nvl.
 Proof.
-  intros. exploit add_needs_vagree; eauto. 
-  generalize rl. induction rl0; simpl; intros V; inv V. 
+  induction rl; simpl; intros.
   constructor.
-  constructor; auto.
+  destruct nvl.
+  apply vagree_lessdef_list. eapply add_needs_all_lessdef with (rl := a :: rl); eauto.
+  constructor. eapply add_need_vagree; eauto. 
+  eapply IHrl. eapply add_need_eagree; eauto. 
 Qed.
 
 Lemma add_ros_need_eagree:
-  forall e e' ros ne, eagree e e' (add_ros_need ros ne) -> eagree e e' ne.
+  forall e e' ros ne, eagree e e' (add_ros_need_all ros ne) -> eagree e e' ne.
 Proof.
-  intros. destruct ros; simpl in *. eapply add_need_eagree; eauto. auto. 
+  intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto. 
 Qed.
 
-Hint Resolve add_need_eagree add_need_vagree add_need_lessdef
-             add_needs_eagree add_needs_vagree add_needs_lessdef
+Hint Resolve add_need_all_eagree add_need_all_lessdef
+             add_need_eagree add_need_vagree
+             add_needs_all_eagree add_needs_all_lessdef
+             add_needs_eagree add_needs_vagree
              add_ros_need_eagree: na.
 
 Lemma eagree_init_regs:
@@ -449,7 +456,7 @@ Qed.
 Lemma find_function_translated:
   forall ros rs fd trs ne,
   find_function ge ros rs = Some fd ->
-  eagree rs trs (add_ros_need ros ne) ->
+  eagree rs trs (add_ros_need_all ros ne) ->
   exists tfd, find_function tge ros trs = Some tfd /\ transf_fundef rm fd = OK tfd.
 Proof.
   intros. destruct ros as [r|id]; simpl in *.
@@ -659,22 +666,23 @@ Ltac UseTransfer :=
   eapply match_succ_states; eauto. simpl; auto. 
   apply eagree_update; auto.
   * (* turned into a move *)
-  simpl in *. 
-  exploit operation_is_redundant_sound. eauto. eauto. eapply add_need_vagree. eauto. 
-  intros VA.
+  unfold fst in ENV. unfold snd in MEM. simpl in H0.
+  assert (VA: vagree v te#r (nreg ne res)).
+  { eapply operation_is_redundant_sound with (arg1' := te#r) (args' := te##args).
+    eauto. eauto. exploit add_needs_vagree; eauto. }
   econstructor; split.
   eapply exec_Iop; eauto. simpl; reflexivity. 
   eapply match_succ_states; eauto. simpl; auto. 
-  eapply eagree_update; eauto with na. 
+  eapply eagree_update; eauto 2 with na. 
 + (* preserved operation *)
   simpl in *.
-  exploit needs_of_operation_sound. eapply ma_perm; eauto. eauto. eauto with na. eauto with na.
+  exploit needs_of_operation_sound. eapply ma_perm; eauto. eauto. eauto 2 with na. eauto with na.
   intros [tv [A B]].
   econstructor; split. 
   eapply exec_Iop with (v := tv); eauto.
   rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
   eapply match_succ_states; eauto. simpl; auto. 
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
 
 - (* load *)
   TransfInstr; UseTransfer.
@@ -694,7 +702,7 @@ Ltac UseTransfer :=
   rewrite is_int_zero_sound by auto.
   destruct v; simpl; auto. apply iagree_zero.
 + (* preserved *)
-  exploit eval_addressing_lessdef. eapply add_needs_lessdef; eauto. eauto. 
+  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. 
   intros (ta & U & V). inv V; try discriminate.
   destruct ta; simpl in H1; try discriminate.
   exploit magree_load; eauto. 
@@ -702,10 +710,11 @@ Ltac UseTransfer :=
   intros. apply nlive_add with bc i; assumption. 
   intros (tv & P & Q).
   econstructor; split.
-  eapply exec_Iload with (a := Vptr b i); eauto.
+  eapply exec_Iload with (a := Vptr b i). eauto. 
   rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto. 
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na. 
+  apply eagree_update; eauto 2 with na. 
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. 
 
 - (* store *)
@@ -714,7 +723,7 @@ Ltac UseTransfer :=
              (size_chunk chunk)) eqn:CONTAINS.
 + (* preserved *)
   simpl in *. 
-  exploit eval_addressing_lessdef. eapply add_needs_lessdef; eauto. eauto. 
+  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. 
   intros (ta & U & V). inv V; try discriminate.
   destruct ta; simpl in H1; try discriminate.
   exploit magree_store_parallel. eauto. eauto. instantiate (1 := te#src). eauto with na.
@@ -723,10 +732,11 @@ Ltac UseTransfer :=
   intros. apply nlive_remove with bc b i; assumption. 
   intros (tm' & P & Q).
   econstructor; split.
-  eapply exec_Istore with (a := Vptr b i); eauto.
+  eapply exec_Istore with (a := Vptr b i). eauto. 
   rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto.
   eapply match_succ_states; eauto. simpl; auto.
-  eauto with na. 
+  eauto 3 with na. 
 + (* dead instruction, turned into a nop *)
   destruct a; simpl in H1; try discriminate.
   econstructor; split.
@@ -738,7 +748,7 @@ Ltac UseTransfer :=
 
 - (* call *)
   TransfInstr; UseTransfer.
-  exploit find_function_translated; eauto with na. intros (tfd & A & B).
+  exploit find_function_translated; eauto 2 with na. intros (tfd & A & B).
   econstructor; split.
   eapply exec_Icall; eauto. apply sig_function_translated; auto. 
   constructor. 
@@ -747,25 +757,25 @@ Ltac UseTransfer :=
   edestruct analyze_successors; eauto. simpl; eauto. 
   eapply eagree_ge; eauto. rewrite ANPC. simpl. 
   apply eagree_update; eauto with na.
-  auto. eauto with na. eapply magree_extends; eauto. apply nlive_all. 
+  auto. eauto 2 with na. eapply magree_extends; eauto. apply nlive_all. 
 
 - (* tailcall *)
   TransfInstr; UseTransfer.
-  exploit find_function_translated; eauto with na. intros (tfd & A & B).
+  exploit find_function_translated; eauto 2 with na. intros (tfd & A & B).
   exploit magree_free. eauto. eauto. instantiate (1 := nlive ge stk nmem_all). 
   intros; eapply nlive_dead_stack; eauto. 
   intros (tm' & C & D). 
   econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto. 
   erewrite stacksize_translated by eauto. eexact C.
-  constructor; eauto with na. eapply magree_extends; eauto. apply nlive_all.
+  constructor; eauto 2 with na. eapply magree_extends; eauto. apply nlive_all.
 
 - (* builtin *)
   TransfInstr; UseTransfer. revert ENV MEM TI. 
   functional induction (transfer_builtin (vanalyze rm f)#pc ef args res ne nm);
   simpl in *; intros.
 + (* volatile load *)
-  assert (LD: Val.lessdef rs#a1 te#a1) by eauto with na.
+  assert (LD: Val.lessdef rs#a1 te#a1) by eauto 2 with na.
   inv H0. rewrite <- H1 in LD; inv LD.
   assert (X: exists tv, volatile_load ge chunk tm b ofs t tv /\ Val.lessdef v tv).
   {
@@ -784,7 +794,7 @@ Ltac UseTransfer :=
   simpl. rewrite <- H4. constructor. eauto.   
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. 
 + (* volatile global load *)
   inv H0. 
@@ -804,12 +814,12 @@ Ltac UseTransfer :=
   simpl. econstructor; eauto.   
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. 
 + (* volatile store *)
   exploit transf_volatile_store. eauto. 
-  instantiate (1 := te#a1). eauto with na.
-  instantiate (1 := te#a2). eauto with na. 
+  instantiate (1 := te#a1). eauto 3 with na.
+  instantiate (1 := te#a2). eauto 3 with na. 
   eauto.
   intros (EQ & tm' & A & B). subst v. 
   econstructor; split.
@@ -817,11 +827,11 @@ Ltac UseTransfer :=
   eapply external_call_symbols_preserved. simpl; eauto. 
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
 + (* volatile global store *)
   rewrite volatile_store_global_charact in H0. destruct H0 as (b & P & Q).
   exploit transf_volatile_store. eauto. eauto. 
-  instantiate (1 := te#a1). eauto with na. 
+  instantiate (1 := te#a1). eauto 2 with na. 
   eauto.
   intros (EQ & tm' & A & B). subst v. 
   econstructor; split.
@@ -830,7 +840,7 @@ Ltac UseTransfer :=
   rewrite volatile_store_global_charact. exists b; split; eauto. 
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
 + (* memcpy *)
   rewrite e1 in TI.
   inv H0. 
@@ -854,15 +864,15 @@ Ltac UseTransfer :=
   rewrite nat_of_Z_eq in H10 by omega. auto.
   eauto. 
   intros (tm' & A & B).
-  assert (LD1: Val.lessdef rs#src te#src) by eauto with na. rewrite <- H2 in LD1.
-  assert (LD2: Val.lessdef rs#dst te#dst) by eauto with na. rewrite <- H1 in LD2.
+  assert (LD1: Val.lessdef rs#src te#src) by eauto 3 with na. rewrite <- H2 in LD1.
+  assert (LD2: Val.lessdef rs#dst te#dst) by eauto 3 with na. rewrite <- H1 in LD2.
   econstructor; split.
   eapply exec_Ibuiltin; eauto.
   eapply external_call_symbols_preserved. simpl.
   inv LD1. inv LD2. econstructor; eauto.  
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
 + (* memcpy eliminated *)
   rewrite e1 in TI. inv H0.
   set (adst := aaddr (vanalyze rm f) # pc dst) in *.
@@ -882,26 +892,26 @@ Ltac UseTransfer :=
   econstructor; split. 
   eapply exec_Ibuiltin; eauto. 
   eapply external_call_symbols_preserved. simpl; constructor. 
-  eapply eventval_list_match_lessdef; eauto with na.
+  eapply eventval_list_match_lessdef; eauto 2 with na.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
 + (* annot val *)  
   inv H0. destruct _x; inv H1. destruct _x; inv H4.
   econstructor; split. 
   eapply exec_Ibuiltin; eauto. 
   eapply external_call_symbols_preserved. simpl; constructor. 
-  eapply eventval_match_lessdef; eauto with na.
+  eapply eventval_match_lessdef; eauto 2 with na.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
 + (* all other builtins *)
   assert ((fn_code tf)!pc = Some(Ibuiltin _x _x0 res pc')).
   {
     destruct _x; auto. destruct _x0; auto. destruct _x0; auto. destruct _x0; auto. contradiction. 
   }
   clear y TI. 
-  exploit external_call_mem_extends; eauto with na. 
+  exploit external_call_mem_extends; eauto 2 with na. 
   eapply magree_extends; eauto. intros. apply nlive_all. 
   intros (v' & tm' & A & B & C & D & E). 
   econstructor; split.
@@ -909,7 +919,7 @@ Ltac UseTransfer :=
   eapply external_call_symbols_preserved. eauto.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
   eapply mextends_agree; eauto. 
 
 - (* conditional *)
@@ -917,16 +927,16 @@ Ltac UseTransfer :=
   econstructor; split.
   eapply exec_Icond; eauto. 
   eapply needs_of_condition_sound. eapply ma_perm; eauto. eauto. eauto with na. 
-  eapply match_succ_states; eauto with na. 
+  eapply match_succ_states; eauto 2 with na. 
   simpl; destruct b; auto. 
 
 - (* jumptable *)
   TransfInstr; UseTransfer.
-  assert (LD: Val.lessdef rs#arg te#arg) by eauto with na. 
+  assert (LD: Val.lessdef rs#arg te#arg) by eauto 2 with na. 
   rewrite H0 in LD. inv LD. 
   econstructor; split.
   eapply exec_Ijumptable; eauto. 
-  eapply match_succ_states; eauto with na. 
+  eapply match_succ_states; eauto 2 with na. 
   simpl. eapply list_nth_z_in; eauto. 
 
 - (* return *)
@@ -938,7 +948,7 @@ Ltac UseTransfer :=
   eapply exec_Ireturn; eauto. 
   erewrite stacksize_translated by eauto. eexact A. 
   constructor; auto.
-  destruct or; simpl; eauto with na.
+  destruct or; simpl; eauto 2 with na.
   eapply magree_extends; eauto. apply nlive_all.
 
 - (* internal function *)
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 568c80e..99d70a8 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -82,19 +82,28 @@ Qed.
 
 Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
 
-Definition vagree_list (vl1 vl2: list val) (nv: nval) : Prop :=
-  list_forall2 (fun v1 v2 => vagree v1 v2 nv) vl1 vl2.
+Inductive vagree_list: list val -> list val -> list nval -> Prop :=
+  | vagree_list_nil: forall nvl,
+      vagree_list nil nil nvl
+  | vagree_list_default: forall v1 vl1 v2 vl2,
+      vagree v1 v2 All -> vagree_list vl1 vl2 nil ->
+      vagree_list (v1 :: vl1) (v2 :: vl2) nil
+  | vagree_list_cons: forall v1 vl1 v2 vl2 nv1 nvl,
+      vagree v1 v2 nv1 -> vagree_list vl1 vl2 nvl ->
+      vagree_list (v1 :: vl1) (v2 :: vl2) (nv1 :: nvl).
 
 Lemma lessdef_vagree_list:
-  forall vl1 vl2, vagree_list vl1 vl2 All -> Val.lessdef_list vl1 vl2.
+  forall vl1 vl2, vagree_list vl1 vl2 nil -> Val.lessdef_list vl1 vl2.
 Proof.
-  induction 1; constructor; auto with na.
+  induction vl1; intros; inv H; constructor; auto with na.
 Qed.
 
 Lemma vagree_lessdef_list:
-  forall x vl1 vl2, Val.lessdef_list vl1 vl2 -> vagree_list vl1 vl2 x.
+  forall vl1 vl2, Val.lessdef_list vl1 vl2 -> forall nvl, vagree_list vl1 vl2 nvl.
 Proof.
-  induction 1; constructor; auto with na.
+  induction 1; intros.
+  constructor.
+  destruct nvl; constructor; auto with na.
 Qed.
 
 Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
@@ -621,14 +630,6 @@ Proof.
   destruct nv; simpl; auto. f_equal; apply complete_mask_idem.
 Qed.
 
-Lemma add_sound_2:
-  forall v1 w1 v2 w2 x,
-  vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
-  vagree (Val.add v1 v2) (Val.add w1 w2) (modarith x).
-Proof.
-  intros. apply add_sound; rewrite modarith_idem; auto.
-Qed.
-
 Lemma mul_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
@@ -641,14 +642,6 @@ Proof.
 - inv H; auto. inv H0; auto. destruct w1; auto. 
 Qed.
 
-Lemma mul_sound_2:
-  forall v1 w1 v2 w2 x,
-  vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
-  vagree (Val.mul v1 v2) (Val.mul w1 w2) (modarith x).
-Proof.
-  intros. apply mul_sound; rewrite modarith_idem; auto.
-Qed.
-
 (** Conversions: zero extension, sign extension, single-of-float *)
 
 Definition zero_ext (n: Z) (x: nval) :=
@@ -880,7 +873,7 @@ Qed.
 Lemma default_needs_of_condition_sound:
   forall cond args1 b args2,
   eval_condition cond args1 m1 = Some b ->
-  vagree_list args1 args2 All ->
+  vagree_list args1 args2 nil ->
   eval_condition cond args2 m2 = Some b.
 Proof.
   intros. apply eval_condition_inj with (f := inject_id) (m1 := m1) (vl1 := args1); auto.
@@ -890,7 +883,9 @@ Qed.
 Lemma default_needs_of_operation_sound:
   forall op args1 v1 args2 nv,
   eval_operation ge (Vptr sp Int.zero) op args1 m1 = Some v1 ->
-  vagree_list args1 args2 (default nv) ->
+  vagree_list args1 args2 nil 
+  \/ vagree_list args1 args2 (default nv :: nil)
+  \/ vagree_list args1 args2 (default nv :: default nv :: nil) ->
   nv <> Nothing ->
   exists v2,
      eval_operation ge (Vptr sp Int.zero) op args2 m2 = Some v2
@@ -898,11 +893,17 @@ Lemma default_needs_of_operation_sound:
 Proof.
   intros. assert (default nv = All) by (destruct nv; simpl; congruence). 
   rewrite H2 in H0.
+  assert (Val.lessdef_list args1 args2).
+  {
+    destruct H0. auto with na. 
+    destruct H0. inv H0; constructor; auto with na. 
+    inv H0; constructor; auto with na. inv H8; constructor; auto with na.
+  }
   exploit (@eval_operation_inj _ _ ge inject_id).
   intros. apply val_inject_lessdef. auto.
   eassumption. auto. auto. auto.
   apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto.
-  apply val_list_inject_lessdef. apply lessdef_vagree_list. eauto.
+  apply val_list_inject_lessdef. eauto.
   eauto. 
   intros (v2 & A & B). exists v2; split; auto.
   apply vagree_lessdef. apply val_inject_lessdef. auto. 
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 0709f5d..f580438 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 5d0e3ae..f11cd52 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
 Require Import Coqlib.
 Require Import Zwf.
 Require Import Maps.
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index a7c72d3..022e015 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 12cb8e4..3789953 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
diff --git a/test/regression/Results/varargs2 b/test/regression/Results/varargs2
index 35728be..f954927 100644
--- a/test/regression/Results/varargs2
+++ b/test/regression/Results/varargs2
@@ -2,10 +2,10 @@ An int: 42
 A long long: 123456789012345
 A string: Hello world
 A double: 3.141592654
-A char: x and A string: Hello, world! and An int: 42 and A long: 123456789012345 and A double: 3.141592654 and A float: 2.718281746
+A mixture: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746
 Twice: -1 1.23
 Twice: -1 1.23
 With va_copy: -1 1.23
 With va_copy: -1 1.23
-With extra args: A char: x and A string: Hello, world! and An int: 42 and A long: 123456789012345 and A double: 3.141592654 and A float: 2.718281746
-va_list compatibility: A char: x and A string: Hello, world! and An int: 42 and A long: 123456789012345 and A double: 3.141592654 and A float: 2.718281746
+With extra args: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746
+va_list compatibility: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746
diff --git a/test/regression/varargs2.c b/test/regression/varargs2.c
index e2eefce..6c091d8 100644
--- a/test/regression/varargs2.c
+++ b/test/regression/varargs2.c
@@ -111,12 +111,7 @@ int main()
   miniprintf("A long long: %l\n", 123456789012345LL);
   miniprintf("A string: %s\n", "Hello world");
   miniprintf("A double: %e\n", 3.141592654);
-  miniprintf("A char: %c and "
-             "A string: %s and "
-             "An int: %d and "
-             "A long: %l and "
-             "A double: %e and "
-             "A float: %f\n",
+  miniprintf("A mixture: %c & %s & %d & %l & %e & %f\n",
              'x',
              "Hello, world!",
              42,
@@ -127,26 +122,14 @@ int main()
   miniprintf3("With va_copy: %d %e\n", -1, 1.23);
   miniprintf_extra(0, 1, 2, 3, 4, 5, 6, 7,
                    0.0, 0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7,
-             "With extra args: "
-             "A char: %c and "
-             "A string: %s and "
-             "An int: %d and "
-             "A long: %l and "
-             "A double: %e and "
-             "A float: %f\n",
-             'x',
-             "Hello, world!",
-             42,
-             123456789012345LL,
-             3.141592654,
-             2.71828182);
-  printf_compat("va_list compatibility: "  
-                "A char: %c and "
-                "A string: %s and "
-                "An int: %d and "
-                "A long: %lld and "
-                "A double: %.10g and "
-                "A float: %.10g\n",
+                   "With extra args: %c & %s & %d & %l & %e & %f\n",
+                   'x',
+                   "Hello, world!",
+                   42,
+                   123456789012345LL,
+                   3.141592654,
+                   2.71828182);
+  printf_compat("va_list compatibility: %c & %s & %d & %lld & %.10g & %.10g\n",
                 'x',
                 "Hello, world!",
                 42,