CSE: add recognition of some combined operators, conditions, and addressing modes (cf. CombineOp.v)

Memory model: cleaning up Memdata
Inlining and new Constprop: updated for ARM.


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

28 files changed, 1172 insertions, 471 deletions

diff --git a/.depend b/.depend
index 1b50427..5cc392f 100644
--- a/.depend
+++ b/.depend
@@ -49,7 +49,9 @@ $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob: $(ARCH)/ConstpropOp.v lib/Coqli
 backend/Constprop.vo backend/Constprop.glob: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo
 $(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo
 backend/Constpropproof.vo backend/Constpropproof.glob: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo
-backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo
+$(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo $(ARCH)/SelectOp.vo
+backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo
+$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo
 backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/CSE.vo
 $(ARCH)/Machregs.vo $(ARCH)/Machregs.glob: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo
 backend/Locations.vo backend/Locations.glob: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo
@@ -93,9 +95,9 @@ backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v
 backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo
 $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo
 $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
-$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo
-$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
-$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo
+$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo
+$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
+$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo
 cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo
 cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
 cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
diff --git a/Makefile b/Makefile
index 8c73798..793a4d4 100644
--- a/Makefile
+++ b/Makefile
@@ -60,7 +60,7 @@ BACKEND=\
   RTLtyping.v \
   Kildall.v \
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
-  CSE.v CSEproof.v \
+  CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
   Machregs.v Locations.v Conventions1.v Conventions.v LTL.v LTLtyping.v \
   InterfGraph.v Coloring.v Coloringproof.v \
   Allocation.v Allocproof.v Alloctyping.v \
diff --git a/arm/CombineOp.v b/arm/CombineOp.v
new file mode 100644
index 0000000..8048653
--- /dev/null
+++ b/arm/CombineOp.v
@@ -0,0 +1,107 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+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.
+
+Section COMBINE.
+
+Variable get: valnum -> option rhs.
+
+Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | _ => None
+  end.
+
+Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | _ => None
+  end.
+
+Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) :=
+  match cond, args with
+  | Ccompimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | Ccompuimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompuimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | _, _ => None
+  end.
+
+Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+  match addr, args with
+  | Aindexed n, x::nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys)
+      | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None
+      | Some(Op (Oaddshift s) ys) => if Int.eq_dec n Int.zero then Some(Aindexed2shift s, ys) else None
+      | _ => None
+      end
+  | _, _ => None
+  end.
+
+Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
+  match op, args with
+  | Oaddimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Oaddimm (Int.add m n), ys)
+      | Some(Op (Orsubimm m) ys) => Some(Orsubimm (Int.add m n), ys)
+      | _ => None
+      end
+  | Orsubimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Orsubimm (Int.sub n m), ys)
+      | _ => None
+      end
+  | Oandimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
+      | _ => None
+      end
+  | Oorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
+      | _ => None
+      end
+  | Oxorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
+      | _ => None
+      end
+  | Ocmp cond, _ =>
+      match combine_cond cond args with
+      | Some(cond', args') => Some(Ocmp cond', args')
+      | None => None
+      end
+  | _, _ => None
+  end.
+
+End COMBINE.
+
+
diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v
new file mode 100644
index 0000000..9d297ac
--- /dev/null
+++ b/arm/CombineOpproof.v
@@ -0,0 +1,127 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import CombineOp.
+Require Import CSE.
+
+Section COMBINE.
+
+Variable ge: genv.
+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.
+
+Lemma combine_compimm_ne_0_sound:
+  forall x cond args,
+  combine_compimm_ne_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero).
+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. 
+  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+Qed.
+
+Lemma combine_compimm_eq_0_sound:
+  forall x cond args,
+  combine_compimm_eq_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero).
+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. 
+  rewrite eval_negate_condition. 
+  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+Qed.
+
+Theorem combine_cond_sound:
+  forall cond args cond' args',
+  combine_cond get cond args = Some(cond', args') ->
+  eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+  (* compimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+  (* compuimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compuimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+Qed.
+
+Theorem combine_addr_sound:
+  forall addr args addr' args',
+  combine_addr get addr args = Some(addr', args') ->
+  eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
+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. 
+  (* indexed 0 - add *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
+  rewrite <- H0. destruct v; destruct v0; simpl; auto; rewrite Int.add_zero; auto.
+  (* indexed 0 - addshift *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
+  rewrite <- H0. destruct v; destruct (eval_shift s v0); simpl; auto; rewrite Int.add_zero; auto.
+Qed.
+
+Theorem combine_op_sound:
+  forall op args op' args',
+  combine_op get op args = Some(op', args') ->
+  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
+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.
+(* 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.
+(* subimm - addimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1.
+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.
+(* orimm - orimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.or_assoc. auto.
+(* xorimm - xorimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.xor_assoc. auto.
+(* cmp *)
+  simpl. decEq; decEq. eapply combine_cond_sound; eauto.
+Qed.
+
+End COMBINE.
diff --git a/arm/Op.v b/arm/Op.v
index a5502c0..3353416 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -492,22 +492,20 @@ Definition negate_condition (cond: condition): condition :=
   end.
 
 Lemma eval_negate_condition:
-  forall (cond: condition) (vl: list val) (b: bool) (m: mem),
-  eval_condition cond vl m = Some b ->
-  eval_condition (negate_condition cond) vl m = Some (negb b).
+  forall cond vl m,
+  eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m).
 Proof.
-  intros. 
-  destruct cond; simpl in H; FuncInv; simpl.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite H; auto.
-  destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. 
-  rewrite H; auto.
-  destruct (Val.cmpf_bool c v (Vfloat Float.zero)); simpl in H; inv H. rewrite negb_elim; auto. 
+  intros. destruct cond; simpl.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
+  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v (Vfloat Float.zero)); auto. destruct b; auto.
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 27b5f53..6049017 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -111,10 +111,10 @@ Nondetfunction addimm (n: int) (e: expr) :=
 Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
+  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
   | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
   | Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil))
-  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
   | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
   | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
   | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil)
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 1a2f560..dc4fb54 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -179,13 +179,9 @@ Proof.
 (* intconst *)
   destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
 (* cmp *)
-  inv H. simpl in H5.
-  destruct (eval_condition c vl m) as []_eqn. 
-  TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto.
-  inv H5. simpl. 
-  destruct (eval_condition (negate_condition c) vl m) as []_eqn.
-  destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto.
-  exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto.
+  inv H. simpl in H5. inv H5.
+  TrivialExists. simpl. rewrite eval_negate_condition.
+  destruct (eval_condition c vl m); auto. destruct b; auto. 
 (* condition *)
   inv H. destruct v1.
   exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
@@ -211,6 +207,7 @@ Proof.
   red; intros until y.
   unfold add; case (add_match a b); intros; InvEval.
   rewrite Val.add_commut. apply eval_addimm; auto.
+  apply eval_addimm; auto.
   subst. 
   replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
      with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
@@ -221,7 +218,6 @@ Proof.
      with (Val.add (Val.add v1 y) (Vint n1)).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_commut.
-  apply eval_addimm; auto.
   subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
   subst. rewrite Val.add_commut. TrivialExists.
   subst. TrivialExists.
diff --git a/arm/Unusedglob1.ml b/arm/Unusedglob1.ml
index 04ef89a..33a9bf8 100644
--- a/arm/Unusedglob1.ml
+++ b/arm/Unusedglob1.ml
@@ -26,7 +26,7 @@ let referenced_instr = function
   | Pbsymb(s, _) -> [s]
   | Pblsymb(s, _) -> [s]
   | Ploadsymbol(_, s, _) -> [s]
-  | Pbuiltin ef -> referenced_builtin ef
+  | Pbuiltin(ef, _, _) -> referenced_builtin ef
   | _ -> []
 
 let code_of_function f = f.fn_code
diff --git a/backend/CSE.v b/backend/CSE.v
index d46afdc..e9613c9 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -27,6 +27,7 @@ Require Import Registers.
 Require Import RTL.
 Require Import RTLtyping.
 Require Import Kildall.
+Require Import CombineOp.
 
 (** * Value numbering *)
 
@@ -49,11 +50,13 @@ Require Import Kildall.
   Equations are of the form [valnum = rhs], where the right-hand sides
   [rhs] are either arithmetic operations or memory loads. *)
 
+(*
 Definition valnum := positive.
 
 Inductive rhs : Type :=
   | Op: operation -> list valnum -> rhs
   | Load: memory_chunk -> addressing -> list valnum -> rhs.
+*)
 
 Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq.
 
@@ -272,8 +275,8 @@ Definition add_store (n: numbering) (chunk: memory_chunk) (addr: addressing)
   | _ => n2
   end.
 
-(* [reg_valnum n vn] returns a register that is mapped to value number
-   [vn], or [None] if no such register exists. *)
+(** [reg_valnum n vn] returns a register that is mapped to value number
+    [vn], or [None] if no such register exists. *)
 
 Definition reg_valnum (n: numbering) (vn: valnum) : option reg :=
   match PMap.get vn n.(num_val) with
@@ -281,10 +284,19 @@ Definition reg_valnum (n: numbering) (vn: valnum) : option reg :=
   | r :: rs => Some r
   end.
 
-(* [find_rhs] and its specializations [find_op] and [find_load]
-   return a register that already holds the result of the given arithmetic
-   operation or memory load, according to the given numbering.
-   [None] is returned if no such register exists. *)
+Fixpoint regs_valnums (n: numbering) (vl: list valnum) : option (list reg) :=
+  match vl with
+  | nil => Some nil
+  | v1 :: vs =>
+      match reg_valnum n v1, regs_valnums n vs with
+      | Some r1, Some rs => Some (r1 :: rs)
+      | _, _ => None
+      end
+  end.
+
+(** [find_rhs] return a register that already holds the result of the given arithmetic
+    operation or memory load, according to the given numbering.
+    [None] is returned if no such register exists. *)
 
 Definition find_rhs (n: numbering) (rh: rhs) : option reg :=
   match find_valnum_rhs rh n.(num_eqs) with
@@ -292,15 +304,44 @@ Definition find_rhs (n: numbering) (rh: rhs) : option reg :=
   | Some vres => reg_valnum n vres
   end.
 
-Definition find_op
-    (n: numbering) (op: operation) (rs: list reg) : option reg :=
-  let (n1, vl) := valnum_regs n rs in
-  find_rhs n1 (Op op vl).
+(** Experimental: take advantage of known equations to select more efficient
+  forms of operations, addressing modes, and conditions. *)
+
+Section REDUCE.
+
+Variable A: Type.
+Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
+Variable n: numbering.
+
+Fixpoint reduce_rec (niter: nat) (op: A) (args: list valnum) : option(A * list reg) :=
+  match niter with
+  | O => None
+  | S niter' =>
+      match f (fun v => find_valnum_num v n.(num_eqs)) op args with
+      | None => None
+      | Some(op', args') =>
+          match reduce_rec niter' op' args' with
+          | None =>
+              match regs_valnums n args' with Some rl => Some(op', rl) | None => None end
+          | Some _ as res =>
+              res
+          end
+      end
+  end.
+
+Definition reduce (op: A) (rl: list reg) (vl: list valnum) : A * list reg :=
+  match reduce_rec 4%nat op vl with
+  | None     => (op, rl)
+  | Some res => res
+  end.
+
+End REDUCE.
 
-Definition find_load
-    (n: numbering) (chunk: memory_chunk) (addr: addressing) (rs: list reg) : option reg :=
-  let (n1, vl) := valnum_regs n rs in
-  find_rhs n1 (Load chunk addr vl).
+(*
+Parameter combine_cond: (valnum -> option rhs) -> condition -> list valnum -> option (condition * list valnum).
+Parameter combine_addr: (valnum -> option rhs) -> addressing -> list valnum -> option (addressing * list valnum).
+Parameter combine_op: (valnum -> option rhs) -> operation -> list valnum -> option (operation * list valnum).
+*)
 
 (** * The static analysis *)
 
@@ -442,15 +483,31 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
   match instr with
   | Iop op args res s =>
       if is_trivial_op op then instr else
-        match find_op n op args with
-        | None => instr
-        | Some r => Iop Omove (r :: nil) res s
+        let (n1, vl) := valnum_regs n args in
+        match find_rhs n1 (Op op vl) with
+        | Some r =>
+            Iop Omove (r :: nil) res s
+        | None =>
+            let (op', args') := reduce _ combine_op n1 op args vl in
+            Iop op' args' res s
         end
   | Iload chunk addr args dst s =>
-      match find_load n chunk addr args with
-      | None => instr
-      | Some r => Iop Omove (r :: nil) dst s
+      let (n1, vl) := valnum_regs n args in
+      match find_rhs n1 (Load chunk addr vl) with
+      | Some r =>
+          Iop Omove (r :: nil) dst s
+      | None =>
+          let (addr', args') := reduce _ combine_addr n1 addr args vl in
+          Iload chunk addr' args' dst s
       end
+  | Istore chunk addr args src s =>
+      let (n1, vl) := valnum_regs n args in
+      let (addr', args') := reduce _ combine_addr n1 addr args vl in
+      Istore chunk addr' args' src s
+  | Icond cond args s1 s2 =>
+      let (n1, vl) := valnum_regs n args in
+      let (cond', args') := reduce _ combine_cond n1 cond args vl in
+      Icond cond' args' s1 s2
   | _ =>
       instr
   end.
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index fa07716..49b213b 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -28,6 +28,8 @@ Require Import Registers.
 Require Import RTL.
 Require Import RTLtyping.
 Require Import Kildall.
+Require Import CombineOp.
+Require Import CombineOpproof.
 Require Import CSE.
 
 (** * Semantic properties of value numberings *)
@@ -708,7 +710,7 @@ Proof.
   eapply VAL. rewrite Heql. auto with coqlib.
 Qed.
 
-(** Correctness of [find_op] and [find_load]: if successful and in a
+(** Correctness of [find_rhs]: if successful and in a
   satisfiable numbering, the returned register does contain the 
   result value of the operation or memory load. *)
 
@@ -730,42 +732,73 @@ Proof.
   discriminate.
 Qed.
 
-Lemma find_op_correct:
-  forall rs m n op args r,
-  wf_numbering n ->
-  numbering_satisfiable ge sp rs m n ->
-  find_op n op args = Some r ->
-  eval_operation ge sp op rs##args m = Some rs#r.
+(** Correctness of operator reduction *)
+
+Section REDUCE.
+
+Variable A: Type.
+Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
+Variable V: Type.
+Variable rs: regset.
+Variable m: mem.
+Variable sem: A -> list val -> option V.
+Hypothesis f_sound:
+  forall eqs valu op args op' args',
+  (forall v rhs, eqs v = Some rhs -> equation_holds valu ge sp m v rhs) ->
+  f eqs op args = Some(op', args') ->
+  sem op' (map valu args') = sem op (map valu args).
+Variable n: numbering.
+Variable valu: valnum -> val.
+Hypothesis n_holds: numbering_holds valu ge sp rs m n.
+Hypothesis n_wf: wf_numbering n.
+
+Lemma regs_valnums_correct:
+  forall vl rl, regs_valnums n vl = Some rl -> rs##rl = map valu vl.
 Proof.
-  intros until r. intros WF [valu NH].
-  unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND.
-  assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto).
-  generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR).
-  intros [valu2 [NH2 [EQ AG]]].
-  rewrite <- EQ. 
-  change (rhs_evals_to valu2 (Op op vl) m rs#r).
-  eapply find_rhs_correct; eauto.
+  induction vl; simpl; intros.
+  inv H. auto.
+  destruct (reg_valnum n a) as [r1|]_eqn; try discriminate.
+  destruct (regs_valnums n vl) as [rx|]_eqn; try discriminate.
+  inv H. simpl; decEq; auto. 
+  eapply (proj2 n_holds); eauto. eapply reg_valnum_correct; eauto.
 Qed.
 
-Lemma find_load_correct:
-  forall rs m n chunk addr args r,
-  wf_numbering n ->
-  numbering_satisfiable ge sp rs m n ->
-  find_load n chunk addr args = Some r ->
-  exists a,
-  eval_addressing ge sp addr rs##args = Some a /\
-  Mem.loadv chunk m a = Some rs#r.
+Lemma reduce_rec_sound:
+  forall niter op args op' rl' res,
+  reduce_rec A f n niter op args = Some(op', rl') ->
+  sem op (map valu args) = Some res ->
+  sem op' (rs##rl') = Some res.
 Proof.
-  intros until r. intros WF [valu NH].
-  unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND.
-  assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto).
-  generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR).
-  intros [valu2 [NH2 [EQ AG]]].
-  rewrite <- EQ. 
-  change (rhs_evals_to valu2 (Load chunk addr vl) m rs#r).
-  eapply find_rhs_correct; eauto.
+  induction niter; simpl; intros.
+  discriminate.
+  destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args)
+           as [[op1 args1] | ]_eqn.
+  assert (sem op1 (map valu args1) = Some res).
+    rewrite <- H0. eapply f_sound; eauto.
+    simpl; intros. apply (proj1 n_holds). eapply find_valnum_num_correct; eauto. 
+  destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ]_eqn.
+  inv H. eapply IHniter; eauto.
+  destruct (regs_valnums n args1) as [rl|]_eqn.
+  inv H. erewrite regs_valnums_correct; eauto.
+  discriminate.
+  discriminate.
 Qed.
 
+Lemma reduce_sound:
+  forall op rl vl op' rl' res,
+  reduce A f n op rl vl = (op', rl') ->
+  map valu vl = rs##rl ->
+  sem op rs##rl = Some res ->
+  sem op' rs##rl' = Some res.
+Proof.
+  unfold reduce; intros. 
+  destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ]_eqn; inv H.
+  eapply reduce_rec_sound; eauto. congruence.
+  auto.
+Qed.
+
+End REDUCE.
+
 End SATISFIABILITY.
 
 (** The numberings associated to each instruction by the static analysis
@@ -942,17 +975,27 @@ Proof.
 
   (* Iop *)
   exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split.
-  assert (eval_operation tge sp op rs##args m = Some v).
-    rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
   destruct (is_trivial_op op) as []_eqn.
-  eapply exec_Iop'; eauto. 
-  destruct (find_op approx!!pc op args) as [r|]_eqn. 
-  eapply exec_Iop'; eauto. simpl. 
-  assert (eval_operation ge sp op rs##args m = Some rs#r).
-    eapply find_op_correct; eauto.
-    eapply wf_analyze; eauto.
-  congruence.
   eapply exec_Iop'; eauto.
+  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (find_rhs n1 (Op op vl)) as [r|]_eqn.
+  (* replaced by move *)
+  assert (EV: rhs_evals_to ge sp valu2 (Op op vl) m rs#r). eapply find_rhs_correct; eauto.
+  assert (RES: rs#r = v). red in EV. congruence.
+  eapply exec_Iop'; eauto. simpl. congruence. 
+  (* possibly simplified *)
+  destruct (reduce operation combine_op n1 op args vl) as [op' args']_eqn.
+  assert (RES: eval_operation ge sp op' rs##args' m = Some v).
+    eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. 
+    intros; eapply combine_op_sound; eauto.
+  eapply exec_Iop'; eauto.
+  rewrite <- RES. apply eval_operation_preserved. exact symbols_preserved.
+  (* state matching *)
   econstructor; eauto.
   apply wt_regset_assign; auto. 
   generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
@@ -966,17 +1009,25 @@ Proof.
 
   (* Iload *)
   exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split.
-  assert (eval_addressing tge sp addr rs##args = Some a).
-    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  destruct (find_load approx!!pc chunk addr args) as [r|]_eqn.
-  eapply exec_Iop'; eauto. simpl. 
-  assert (exists a, eval_addressing ge sp addr rs##args = Some a
-                 /\ Mem.loadv chunk m a = Some rs#r).
-    eapply find_load_correct; eauto.
-    eapply wf_analyze; eauto.
-  destruct H3 as [a' [A B]].
-  congruence.
-  eapply exec_Iload'; eauto.
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (find_rhs n1 (Load chunk addr vl)) as [r|]_eqn.
+  (* replaced by move *)
+  assert (EV: rhs_evals_to ge sp valu2 (Load chunk addr vl) m rs#r). eapply find_rhs_correct; eauto.
+  assert (RES: rs#r = v). red in EV. destruct EV as [a' [EQ1 EQ2]]. congruence.
+  eapply exec_Iop'; eauto. simpl. congruence. 
+  (* possibly simplified *)
+  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn.
+  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
+    eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
+    intros; eapply combine_addr_sound; eauto.
+  assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload; eauto.
+  (* state matching *)
   econstructor; eauto.
   generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
   apply wt_regset_assign. auto. rewrite H8. eapply type_of_chunk_correct; eauto.
@@ -986,8 +1037,17 @@ Proof.
 
   (* Istore *)
   exists (State s' (transf_function' f approx) sp pc' rs m'); split.
-  assert (eval_addressing tge sp addr rs##args = Some a).
-    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn.
+  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
+    eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
+    intros; eapply combine_addr_sound; eauto.
+  assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Istore; eauto.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto. 
@@ -1035,6 +1095,15 @@ Proof.
   eapply kill_loads_satisfiable; eauto. 
 
   (* Icond *)
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  elim SAT; intros valu1 NH1.
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (reduce condition combine_cond n1 cond args vl) as [cond' args']_eqn.
+  assert (RES: eval_condition cond' rs##args' m = Some b).
+    eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. 
+    intros; eapply combine_cond_sound; eauto.
   econstructor; split.
   eapply exec_Icond; eauto. 
   econstructor; eauto.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index c62e173..f88ca81 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -868,9 +868,10 @@ Proof.
     eauto.
   fold (saddr ctx addr). intros [a' [P Q]].
   exploit Mem.loadv_inject; eauto. intros [v' [U V]].
+  assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a').
+  rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
   left; econstructor; split.
-  eapply plus_one. eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto.
-  exact symbols_preserved. 
+  eapply plus_one. eapply exec_Iload; eauto.
   econstructor; eauto. 
   apply match_stacks_inside_set_reg; auto.
   apply agree_set_reg; auto. 
@@ -885,9 +886,10 @@ Proof.
   fold saddr. intros [a' [P Q]].
   exploit Mem.storev_mapped_inject; eauto. eapply agree_val_reg; eauto. 
   intros [m1' [U V]].
+  assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a').
+    rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
   left; econstructor; split.
-  eapply plus_one. eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto.
-  exact symbols_preserved. 
+  eapply plus_one. eapply exec_Istore; eauto.
   destruct a; simpl in H1; try discriminate.
   destruct a'; simpl in U; try discriminate.
   econstructor; eauto.
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 50db0c6..b72268a 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -641,7 +641,7 @@ Proof.
   econstructor; split.
   eapply plus_left'.  
   eapply exec_Lcond_false; eauto.
-  change false with (negb true). apply eval_negate_condition; auto.
+  rewrite eval_negate_condition; rewrite H0; auto.
   eapply add_branch_correct; eauto.
   eapply is_tail_add_branch. eapply is_tail_cons_left. 
   eapply is_tail_find_label. eauto.
@@ -657,7 +657,7 @@ Proof.
   destruct (starts_with ifso c').
   econstructor; split.
   apply plus_one. eapply exec_Lcond_true; eauto.
-  change true with (negb false). apply eval_negate_condition; auto.
+  rewrite eval_negate_condition; rewrite H0; auto.
   econstructor; eauto.
   econstructor; split.
   eapply plus_left'. 
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index a1b32b8..5ec29e2 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -171,13 +171,15 @@ Proof.
   constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* load *)
   econstructor; split.
-  eapply exec_Iload; eauto.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. 
+  eapply exec_Iload; eauto.
   constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* store *)
   econstructor; split.
-  eapply exec_Istore; eauto.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. 
+  eapply exec_Istore; eauto.
   constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* call *)
   econstructor; split.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 4e67181..0aa2b6b 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -50,7 +50,7 @@ Proof.
   induction 1; simpl.
   constructor.
   constructor.
-  econstructor. eauto. apply eval_negate_condition. auto.
+  econstructor. eauto. rewrite eval_negate_condition. rewrite H0. auto.
   econstructor. eauto. destruct vb1; auto.
 Qed. 
 
@@ -124,7 +124,7 @@ Proof.
   intros. apply is_compare_neq_zero_correct with (negate_condition c).
   destruct c; simpl in H; simpl; try discriminate;
   destruct c; simpl; try discriminate; auto.
-  apply eval_negate_condition; auto.
+  rewrite eval_negate_condition. rewrite H0. auto.
 Qed.
 
 Lemma eval_condition_of_expr:
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index f94e081..f725662 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -373,9 +373,9 @@ Proof.
     assert (b0 = b) by congruence. subst.
     assert (chunk0 = chunk) by congruence. subst.
     econstructor. eauto. 
-    eapply Mem.load_store_same; eauto. apply val_normalized_has_type; auto. auto. 
+    eapply Mem.load_store_same; eauto. auto. 
     rewrite PTree.gss. reflexivity.
-    red in H0. rewrite H0. auto. 
+    red in H0. rewrite H0. auto.
     (* a different variable *)
     econstructor; eauto.
     rewrite <- H6. eapply Mem.load_store_other; eauto. 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index d7449f9..ba038f8 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -897,7 +897,6 @@ Proof.
   assert (A: forall chunk v m b p m1 il m',
     Mem.store chunk m b p v = Some m1 ->
     store_init_data_list m1 b (p + size_chunk chunk) il = Some m' ->
-    Val.has_type v (type_of_chunk chunk) ->
     Mem.load chunk m' b p = Some(Val.load_result chunk v)).
   intros. transitivity (Mem.load chunk m1 b p).
   eapply store_init_data_list_outside; eauto. right. omega. 
@@ -909,13 +908,13 @@ Proof.
   intros m1 B C.
   exploit IHil; eauto. intro D. 
   destruct a; simpl in B; intuition.
-  eapply (A Mint8unsigned (Vint i)); eauto. simpl; auto.
-  eapply (A Mint16unsigned (Vint i)); eauto. simpl; auto.
-  eapply (A Mint32 (Vint i)); eauto. simpl; auto.
-  eapply (A Mfloat32 (Vfloat f)); eauto. simpl; auto.
-  eapply (A Mfloat64 (Vfloat f)); eauto. simpl; auto.
+  eapply (A Mint8unsigned (Vint i)); eauto.
+  eapply (A Mint16unsigned (Vint i)); eauto.
+  eapply (A Mint32 (Vint i)); eauto.
+  eapply (A Mfloat32 (Vfloat f)); eauto.
+  eapply (A Mfloat64 (Vfloat f)); eauto.
   destruct (find_symbol ge i); try congruence. exists b0; split; auto. 
-  eapply (A Mint32 (Vptr b0 i0)); eauto. simpl; auto. 
+  eapply (A Mint32 (Vptr b0 i0)); eauto. 
 Qed.
 
 Remark load_alloc_variables:
diff --git a/common/Memdata.v b/common/Memdata.v
index 47ed79e..fd77638 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -122,7 +122,7 @@ Inductive memval: Type :=
 (** * Encoding and decoding integers *)
 
 (** We define functions to convert between integers and lists of bytes
-  according to a given memory chunk. *)
+  of a given length *)
 
 Fixpoint bytes_of_int (n: nat) (x: Z) {struct n}: list byte :=
   match n with
@@ -208,201 +208,88 @@ Proof.
   auto.
 Qed.
 
-Definition encode_int (c: memory_chunk) (x: int) : list byte :=
-  let n := Int.unsigned x in
-  rev_if_be (match c with
-  | Mint8signed | Mint8unsigned => bytes_of_int 1%nat n
-  | Mint16signed | Mint16unsigned => bytes_of_int 2%nat n
-  | Mint32 => bytes_of_int 4%nat n
-  | Mfloat32 => bytes_of_int 4%nat 0
-  | Mfloat64 => bytes_of_int 8%nat 0
-  end).
-
-Definition decode_int (c: memory_chunk) (b: list byte) : int :=
-  let b' := rev_if_be b in
-  match c with
-  | Mint8signed => Int.sign_ext 8 (Int.repr (int_of_bytes b'))
-  | Mint8unsigned => Int.zero_ext 8 (Int.repr (int_of_bytes b'))
-  | Mint16signed => Int.sign_ext 16 (Int.repr (int_of_bytes b'))
-  | Mint16unsigned => Int.zero_ext 16 (Int.repr (int_of_bytes b'))
-  | Mint32 => Int.repr (int_of_bytes b')
-  | Mfloat32 => Int.zero
-  | Mfloat64 => Int.zero
-  end.
+Definition encode_int (sz: nat) (x: int) : list byte :=
+  rev_if_be (bytes_of_int sz (Int.unsigned x)).
 
-Lemma encode_int_length:
-  forall chunk n, length(encode_int chunk n) = size_chunk_nat chunk.
-Proof.
-  intros. unfold encode_int. rewrite rev_if_be_length.
-  destruct chunk; rewrite length_bytes_of_int; reflexivity.
-Qed.
+Definition decode_int (b: list byte) : int :=
+  Int.repr (int_of_bytes (rev_if_be b)).
 
-Lemma decode_encode_int:
-  forall c x,
-  decode_int c (encode_int c x) =
-  match c with
-  | Mint8signed => Int.sign_ext 8 x
-  | Mint8unsigned => Int.zero_ext 8 x
-  | Mint16signed => Int.sign_ext 16 x
-  | Mint16unsigned => Int.zero_ext 16 x
-  | Mint32 => x
-  | Mfloat32 => Int.zero
-  | Mfloat64 => Int.zero
-  end.
-Proof.
-  intros. unfold decode_int, encode_int; destruct c; auto;
-  rewrite rev_if_be_involutive.
-  rewrite int_of_bytes_of_int_2; auto.
-  apply Int.sign_ext_zero_ext. compute; auto.
-  rewrite int_of_bytes_of_int_2; auto.
-  apply Int.zero_ext_idem. compute; auto.
-  rewrite int_of_bytes_of_int_2; auto.
-  apply Int.sign_ext_zero_ext. compute; auto.
-  rewrite int_of_bytes_of_int_2; auto.
-  apply Int.zero_ext_idem. compute; auto.
-  rewrite int_of_bytes_of_int. 
-  transitivity (Int.repr (Int.unsigned x)). 
-  apply Int.eqm_samerepr. apply Int.eqm_sym. apply Int.eqmod_mod. apply two_p_gt_ZERO. omega. 
-  apply Int.repr_unsigned.
-Qed.
-
-Lemma encode_int8_signed_unsigned: forall n,
-  encode_int Mint8signed n = encode_int Mint8unsigned n.
+Lemma encode_int_length:
+  forall sz x, length(encode_int sz x) = sz.
 Proof.
-  intros; reflexivity.
+  intros. unfold encode_int. rewrite rev_if_be_length. apply length_bytes_of_int.
 Qed.
 
-Remark encode_8_mod:
-  forall x y,
-  Int.eqmod (two_p 8) (Int.unsigned x) (Int.unsigned y) ->
-  encode_int Mint8unsigned x = encode_int Mint8unsigned y.
+Lemma decode_encode_int_1:
+  forall x, decode_int (encode_int 1%nat x) = Int.zero_ext 8 x.
 Proof.
-  intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto.
+  intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. 
+  rewrite int_of_bytes_of_int_2. reflexivity. auto.
 Qed.
 
-Lemma encode_int8_zero_ext:
-  forall x,
-  encode_int Mint8unsigned (Int.zero_ext 8 x) = encode_int Mint8unsigned x.
+Lemma decode_encode_int_2:
+  forall x, decode_int (encode_int 2%nat x) = Int.zero_ext 16 x.
 Proof.
-  intros. apply encode_8_mod. apply Int.eqmod_zero_ext. compute; auto.
+  intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. 
+  rewrite int_of_bytes_of_int_2. reflexivity. auto.
 Qed.
 
-Lemma encode_int8_sign_ext:
-  forall x,
-  encode_int Mint8signed (Int.sign_ext 8 x) = encode_int Mint8signed x.
+Lemma decode_encode_int_4:
+  forall x, decode_int (encode_int 4%nat x) = x.
 Proof.
-  intros. repeat rewrite encode_int8_signed_unsigned. 
-  apply encode_8_mod. eapply Int.eqmod_trans.
-  apply Int.eqm_eqmod_two_p. compute; auto. 
-  apply Int.eqm_sym. apply Int.eqm_signed_unsigned.
-  apply Int.eqmod_sign_ext. compute; auto.
+  intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. 
+  rewrite int_of_bytes_of_int.
+  transitivity (Int.repr (Int.unsigned x)). 
+  apply Int.eqm_samerepr. apply Int.eqm_sym. apply Int.eqmod_mod. apply two_p_gt_ZERO. omega. 
+  apply Int.repr_unsigned.
 Qed.
 
-Lemma encode_int16_signed_unsigned: forall n,
-  encode_int Mint16signed n = encode_int Mint16unsigned n.
+Lemma encode_int_8_mod:
+  forall x y,
+  Int.eqmod (two_p 8) (Int.unsigned x) (Int.unsigned y) ->
+  encode_int 1%nat x = encode_int 1%nat y.
 Proof.
-  intros; reflexivity.
+  intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto.
 Qed.
 
-Remark encode_16_mod:
+Lemma encode_16_mod:
   forall x y,
   Int.eqmod (two_p 16) (Int.unsigned x) (Int.unsigned y) ->
-  encode_int Mint16unsigned x = encode_int Mint16unsigned y.
+  encode_int 2%nat x = encode_int 2%nat y.
 Proof.
   intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto.
 Qed.
 
-Lemma encode_int16_zero_ext:
-  forall x,
-  encode_int Mint16unsigned (Int.zero_ext 16 x) = encode_int Mint16unsigned x.
-Proof.
-  intros. apply encode_16_mod. apply Int.eqmod_zero_ext. compute; auto.
-Qed.
-
-Lemma encode_int16_sign_ext:
-  forall x,
-  encode_int Mint16signed (Int.sign_ext 16 x) = encode_int Mint16signed x.
-Proof.
-  intros. repeat rewrite encode_int16_signed_unsigned. 
-  apply encode_16_mod. eapply Int.eqmod_trans.
-  apply Int.eqm_eqmod_two_p. compute; auto. 
-  apply Int.eqm_sym. apply Int.eqm_signed_unsigned.
-  apply Int.eqmod_sign_ext. compute; auto.
-Qed.
-
-Lemma decode_int8_zero_ext:
-  forall l,
-  Int.zero_ext 8 (decode_int Mint8unsigned l) = decode_int Mint8unsigned l.
-Proof.
-  intros; simpl. apply Int.zero_ext_idem. vm_compute; auto.
-Qed.
+(** * Encoding and decoding floats *)
 
-Lemma decode_int8_sign_ext:
-  forall l,
-  Int.sign_ext 8 (decode_int Mint8signed l) = decode_int Mint8signed l.
-Proof.
-  intros; simpl. apply Int.sign_ext_idem. vm_compute; auto.
-Qed.
+Definition encode_float_32 (f: float) : list byte :=
+  rev_if_be (bytes_of_int 4%nat (Int.unsigned (Float.bits_of_single f))).
 
-Lemma decode_int16_zero_ext:
-  forall l,
-  Int.zero_ext 16 (decode_int Mint16unsigned l) = decode_int Mint16unsigned l.
-Proof.
-  intros; simpl. apply Int.zero_ext_idem. vm_compute; auto.
-Qed.
+Definition encode_float_64 (f: float) : list byte :=
+  rev_if_be (bytes_of_int 8%nat (Int64.unsigned (Float.bits_of_double f))).
 
-Lemma decode_int16_sign_ext:
-  forall l,
-  Int.sign_ext 16 (decode_int Mint16signed l) = decode_int Mint16signed l.
-Proof.
-  intros; simpl. apply Int.sign_ext_idem. vm_compute; auto.
-Qed.
+Definition decode_float_32 (b: list byte) : float :=
+  Float.single_of_bits (Int.repr (int_of_bytes (rev_if_be b))).
 
-Lemma decode_int8_signed_unsigned:
-  forall l,
-  decode_int Mint8signed l = Int.sign_ext 8 (decode_int Mint8unsigned l).
-Proof.
-  intros; simpl. rewrite Int.sign_ext_zero_ext; auto. vm_compute; auto.
-Qed.
+Definition decode_float_64 (b: list byte) : float :=
+  Float.double_of_bits (Int64.repr (int_of_bytes (rev_if_be b))).
 
-Lemma decode_int16_signed_unsigned:
-  forall l,
-  decode_int Mint16signed l = Int.sign_ext 16 (decode_int Mint16unsigned l).
+Lemma encode_float_32_length:
+  forall n, length(encode_float_32 n) = 4%nat.
 Proof.
-  intros; simpl. rewrite Int.sign_ext_zero_ext; auto. vm_compute; auto.
+  unfold encode_float_32; intros. rewrite rev_if_be_length. apply length_bytes_of_int. 
 Qed.
 
-(** * Encoding and decoding floats *)
-
-Definition encode_float (c: memory_chunk) (f: float) : list byte :=
-  rev_if_be (match c with
-  | Mint8signed | Mint8unsigned => bytes_of_int 1%nat 0
-  | Mint16signed | Mint16unsigned => bytes_of_int 2%nat 0
-  | Mint32 => bytes_of_int 4%nat 0
-  | Mfloat32 => bytes_of_int 4%nat (Int.unsigned (Float.bits_of_single f))
-  | Mfloat64 => bytes_of_int 8%nat (Int64.unsigned (Float.bits_of_double f))
-  end).
-
-Definition decode_float (c: memory_chunk) (b: list byte) : float :=
-  let b' := rev_if_be b in
-  match c with
-  | Mfloat32 => Float.single_of_bits (Int.repr (int_of_bytes b'))
-  | Mfloat64 => Float.double_of_bits (Int64.repr (int_of_bytes b'))
-  | _ => Float.zero
-  end.
-
-Lemma encode_float_length:
-  forall chunk n, length(encode_float chunk n) = size_chunk_nat chunk.
+Lemma encode_float_64_length:
+  forall n, length(encode_float_64 n) = 8%nat.
 Proof.
-  unfold encode_float; intros. 
-  rewrite rev_if_be_length. 
-  destruct chunk; apply length_bytes_of_int. 
+  unfold encode_float_64; intros. rewrite rev_if_be_length. apply length_bytes_of_int. 
 Qed.
 
 Lemma decode_encode_float32: forall n,
-  decode_float Mfloat32 (encode_float Mfloat32 n) = Float.singleoffloat n.
+  decode_float_32 (encode_float_32 n) = Float.singleoffloat n.
 Proof.
-  intros; unfold decode_float, encode_float. 
+  intros; unfold decode_float_32, encode_float_32. 
   rewrite rev_if_be_involutive. 
   rewrite int_of_bytes_of_int. rewrite <- Float.single_of_bits_of_single. 
   decEq. 
@@ -412,9 +299,9 @@ Proof.
 Qed.
 
 Lemma decode_encode_float64: forall n,
-  decode_float Mfloat64 (encode_float Mfloat64 n) = n.
+  decode_float_64 (encode_float_64 n) = n.
 Proof.
-  intros; unfold decode_float, encode_float. 
+  intros; unfold decode_float_64, encode_float_64. 
   rewrite rev_if_be_involutive. 
   rewrite int_of_bytes_of_int.
   set (x := Float.bits_of_double n).
@@ -424,32 +311,34 @@ Proof.
   rewrite Int64.repr_unsigned. apply Float.double_of_bits_of_double.
 Qed.
 
-Lemma encode_float8_signed_unsigned: forall n,
-  encode_float Mint8signed n = encode_float Mint8unsigned n.
+Lemma encode_float32_eq:
+  forall f, encode_float_32 f = encode_int 4%nat (Float.bits_of_single f).
 Proof.
-  intros. reflexivity. 
+  auto.
 Qed.
 
-Lemma encode_float16_signed_unsigned: forall n,
-  encode_float Mint16signed n = encode_float Mint16unsigned n.
+Lemma decode_float32_eq:
+  forall bl, decode_float_32 bl = Float.single_of_bits (decode_int bl).
 Proof.
-  intros. reflexivity.
+  auto.
 Qed.
 
+(*
 Lemma encode_float32_cast:
   forall f,
-  encode_float Mfloat32 (Float.singleoffloat f) = encode_float Mfloat32 f.
+  encode_float_32 (Float.singleoffloat f) = encode_float_32 f.
 Proof.
-  intros; unfold encode_float. decEq. decEq. decEq. 
+  intros; unfold encode_float_32. decEq. decEq. decEq. 
   apply Float.bits_of_singleoffloat.
 Qed.
 
 Lemma decode_float32_cast:
   forall l,
-  Float.singleoffloat (decode_float Mfloat32 l) = decode_float Mfloat32 l.
+  Float.singleoffloat (decode_float_32 l) = decode_float_32 l.
 Proof.
-  intros; unfold decode_float. rewrite Float.singleoffloat_of_bits. auto.
+  intros; unfold decode_float_32. rewrite Float.singleoffloat_of_bits. auto.
 Qed.
+*)
 
 (** * Encoding and decoding values *)
 
@@ -503,17 +392,18 @@ Fixpoint check_pointer (n: nat) (b: block) (ofs: int) (vl: list memval)
 Definition proj_pointer (vl: list memval) : val :=
   match vl with
   | Pointer b ofs n :: vl' =>
-      if check_pointer (size_chunk_nat Mint32) b ofs vl
-      then Vptr b ofs
-      else Vundef
+      if check_pointer 4%nat b ofs vl then Vptr b ofs else Vundef
   | _ => Vundef
   end.
 
 Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
   match v, chunk with
-  | Vptr b ofs, Mint32 => inj_pointer (size_chunk_nat Mint32) b ofs
-  | Vint n, _ => inj_bytes (encode_int chunk n)
-  | Vfloat f, _ => inj_bytes (encode_float chunk f)
+  | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat n)
+  | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat n)
+  | Vint n, Mint32 => inj_bytes (encode_int 4%nat n)
+  | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs
+  | Vfloat n, Mfloat32 => inj_bytes (encode_float_32 n)
+  | Vfloat n, Mfloat64 => inj_bytes (encode_float_64 n)
   | _, _ => list_repeat (size_chunk_nat chunk) Undef
   end.
 
@@ -521,11 +411,13 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
   match proj_bytes vl with
   | Some bl =>
       match chunk with
-      | Mint8signed | Mint8unsigned
-      | Mint16signed | Mint16unsigned | Mint32 =>
-          Vint(decode_int chunk bl)
-      | Mfloat32 | Mfloat64 =>
-          Vfloat(decode_float chunk bl)
+      | Mint8signed => Vint(Int.sign_ext 8 (decode_int bl))
+      | Mint8unsigned => Vint(Int.zero_ext 8 (decode_int bl))
+      | Mint16signed => Vint(Int.sign_ext 16 (decode_int bl))
+      | Mint16unsigned => Vint(Int.zero_ext 16 (decode_int bl))
+      | Mint32 => Vint(decode_int bl)
+      | Mfloat32 => Vfloat(decode_float_32 bl)
+      | Mfloat64 => Vfloat(decode_float_64 bl)
       end
   | None =>
       match chunk with
@@ -537,11 +429,8 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
 Lemma encode_val_length:
   forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk.
 Proof.
-  intros. destruct v; simpl. 
-  apply length_list_repeat.
-  rewrite length_inj_bytes. apply encode_int_length.
-  rewrite length_inj_bytes. apply encode_float_length.
-  destruct chunk; try (apply length_list_repeat). reflexivity.
+  intros. destruct v; simpl; destruct chunk; try (apply length_list_repeat); auto;
+  rewrite length_inj_bytes; try (apply encode_int_length). apply encode_float_64_length.
 Qed.
 
 Lemma check_inj_pointer:
@@ -564,73 +453,62 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) :
   | Vint n, Mint16signed, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
   | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
   | Vint n, Mint32, Mint32 => v2 = Vint n
-  | Vint n, Mint32, Mfloat32 => v2 = Vfloat(decode_float Mfloat32 (encode_int Mint32 n))
-  | Vint n, _, _ => True   (* nothing interesting to say about v2 *)
+  | Vint n, Mint32, Mfloat32 => v2 = Vfloat(Float.single_of_bits n)
+  | Vint n, (Mfloat32 | Mfloat64), _ => v2 = Vundef
+  | Vint n, _, _ => True (**r nothing meaningful to say about v2 *)
   | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs
   | Vptr b ofs, _, _ => v2 = Vundef
   | Vfloat f, Mfloat32, Mfloat32 => v2 = Vfloat(Float.singleoffloat f)
-  | Vfloat f, Mfloat32, Mint32 => v2 = Vint(decode_int Mint32 (encode_float Mfloat32 f))
+  | Vfloat f, Mfloat32, Mint32 => v2 = Vint(Float.bits_of_single f)
   | Vfloat f, Mfloat64, Mfloat64 => v2 = Vfloat f
+  | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32), _ => v2 = Vundef
   | Vfloat f, _, _ => True   (* nothing interesting to say about v2 *)
   end.
 
+Remark decode_val_undef:
+  forall bl chunk, decode_val chunk (Undef :: bl) = Vundef.
+Proof.
+  intros. unfold decode_val. simpl. destruct chunk; auto.
+Qed.
+
 Lemma decode_encode_val_general:
   forall v chunk1 chunk2,
   decode_encode_val v chunk1 chunk2 (decode_val chunk2 (encode_val chunk1 v)).
 Proof.
-  intros. destruct v.
-(* Vundef *)
-  simpl. destruct (size_chunk_nat_pos chunk1) as [psz EQ]. 
-  rewrite EQ. simpl.
-  unfold decode_val. simpl. destruct chunk2; auto.
-(* Vint *)
-  simpl.
-  destruct chunk1; auto; destruct chunk2; auto; unfold decode_val;
-  rewrite proj_inj_bytes.
-  rewrite decode_encode_int. auto.
-  rewrite encode_int8_signed_unsigned. rewrite decode_encode_int. auto.
-  rewrite <- encode_int8_signed_unsigned.  rewrite decode_encode_int. auto.
-  rewrite decode_encode_int. auto.
-  rewrite decode_encode_int. auto.
-  rewrite encode_int16_signed_unsigned. rewrite decode_encode_int. auto.
-  rewrite <- encode_int16_signed_unsigned.  rewrite decode_encode_int. auto.
-  rewrite decode_encode_int. auto.
-  rewrite decode_encode_int. auto.
-  reflexivity. 
-(* Vfloat *)
-  unfold decode_val, encode_val, decode_encode_val;
-  destruct chunk1; auto; destruct chunk2; auto; unfold decode_val;
-  rewrite proj_inj_bytes.
-  auto.
+Opaque inj_pointer.
+  intros.
+  destruct v; destruct chunk1; simpl; try (apply decode_val_undef);
+  destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes).
+  (* int-int *)
+  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto.
+  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto.
+  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto.
+  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto.
+  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto.
+  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto.
+  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto.
+  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto.
+  rewrite decode_encode_int_4. auto.
+  rewrite decode_float32_eq. rewrite decode_encode_int_4. auto.
+  rewrite encode_float32_eq. rewrite decode_encode_int_4. auto.
   rewrite decode_encode_float32. auto.
   rewrite decode_encode_float64. auto.
-(* Vptr *)
-  unfold decode_val, encode_val, decode_encode_val;
-  destruct chunk1; auto; destruct chunk2; auto.
-  simpl. generalize (check_inj_pointer b i (size_chunk_nat Mint32)).
-  simpl. intro. rewrite H. auto.
+  change (proj_bytes (inj_pointer 4 b i)) with (@None (list byte)). simpl. 
+  unfold proj_pointer. generalize (check_inj_pointer b i 4%nat). 
+Transparent inj_pointer.
+  simpl. intros EQ; rewrite EQ; auto.
 Qed.
 
 Lemma decode_encode_val_similar:
   forall v1 chunk1 chunk2 v2,
   type_of_chunk chunk1 = type_of_chunk chunk2 ->
   size_chunk chunk1 = size_chunk chunk2 ->
-  Val.has_type v1 (type_of_chunk chunk1) ->
   decode_encode_val v1 chunk1 chunk2 v2 ->
   v2 = Val.load_result chunk2 v1.
 Proof.
-  intros. 
-  destruct v1.
-  simpl in *. destruct chunk2; simpl; auto. 
-  red in H1.
-  destruct chunk1; simpl in H1; try contradiction;
-  destruct chunk2; simpl in *; discriminate || auto.
-  red in H1.
-  destruct chunk1; simpl in H1; try contradiction;
-  destruct chunk2; simpl in *; discriminate || auto.
-  red in H1.
-  destruct chunk1; simpl in H1; try contradiction;
-  destruct chunk2; simpl in *; discriminate || auto.
+  intros until v2; intros TY SZ DE. 
+  destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try omegaContradiction;
+  destruct v1; auto.
 Qed.
 
 Lemma decode_val_type:
@@ -643,7 +521,7 @@ Proof.
   destruct chunk; simpl; auto.
   unfold proj_pointer. destruct cl; try (exact I).
   destruct m; try (exact I).
-  destruct (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: cl));
+  destruct (check_pointer 4%nat b i (Pointer b i n :: cl));
   exact I.
 Qed.
 
@@ -662,54 +540,25 @@ Qed.
 Lemma encode_val_int8_zero_ext:
   forall n, encode_val Mint8unsigned (Vint (Int.zero_ext 8 n)) = encode_val Mint8unsigned (Vint n).
 Proof.
-  intros; unfold encode_val. rewrite encode_int8_zero_ext. auto.
+  intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_zero_ext. compute; auto.
 Qed.
 
 Lemma encode_val_int8_sign_ext:
   forall n, encode_val Mint8signed (Vint (Int.sign_ext 8 n)) = encode_val Mint8signed (Vint n).
 Proof.
-  intros; unfold encode_val. rewrite encode_int8_sign_ext. auto.
+  intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_sign_ext'. compute; auto.
 Qed.
 
 Lemma encode_val_int16_zero_ext:
   forall n, encode_val Mint16unsigned (Vint (Int.zero_ext 16 n)) = encode_val Mint16unsigned (Vint n).
 Proof.
-  intros; unfold encode_val. rewrite encode_int16_zero_ext. auto.
+  intros; unfold encode_val. decEq. apply encode_16_mod. apply Int.eqmod_zero_ext. compute; auto.
 Qed.
 
 Lemma encode_val_int16_sign_ext:
   forall n, encode_val Mint16signed (Vint (Int.sign_ext 16 n)) = encode_val Mint16signed (Vint n).
 Proof.
-  intros; unfold encode_val. rewrite encode_int16_sign_ext. auto.
-Qed.
-
-Lemma decode_val_int_inv:
-  forall chunk cl n,
-  decode_val chunk cl = Vint n ->
-  type_of_chunk chunk = Tint /\
-  exists bytes, proj_bytes cl = Some bytes /\ n = decode_int chunk bytes.
-Proof.
-  intros until n. unfold decode_val. destruct (proj_bytes cl). 
-Opaque decode_int.
-  destruct chunk; intro EQ; inv EQ; split; auto; exists l; auto. 
-  destruct chunk; try congruence. unfold proj_pointer. 
-  destruct cl; try congruence. destruct m; try congruence. 
-  destruct (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n0 :: cl));
-  congruence.
-Qed.
-
-Lemma decode_val_float_inv:
-  forall chunk cl f,
-  decode_val chunk cl = Vfloat f ->
-  type_of_chunk chunk = Tfloat /\
-  exists bytes, proj_bytes cl = Some bytes /\ f = decode_float chunk bytes.
-Proof.
-  intros until f. unfold decode_val. destruct (proj_bytes cl). 
-  destruct chunk; intro EQ; inv EQ; split; auto; exists l; auto. 
-  destruct chunk; try congruence. unfold proj_pointer. 
-  destruct cl; try congruence. destruct m; try congruence.
-  destruct (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: cl));
-  congruence.
+  intros; unfold encode_val. decEq. apply encode_16_mod. apply Int.eqmod_sign_ext'. compute; auto.
 Qed.
 
 Lemma decode_val_cast:
@@ -725,24 +574,24 @@ Lemma decode_val_cast:
   end.
 Proof.
   unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto.
-  unfold Val.sign_ext. decEq. symmetry. apply decode_int8_sign_ext.
-  unfold Val.zero_ext. decEq. symmetry. apply decode_int8_zero_ext.
-  unfold Val.sign_ext. decEq. symmetry. apply decode_int16_sign_ext.
-  unfold Val.zero_ext. decEq. symmetry. apply decode_int16_zero_ext.
-  unfold Val.singleoffloat. decEq. symmetry. apply decode_float32_cast. 
+  unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto.
+  unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto.
+  unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto.
+  unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto.
+  simpl. rewrite decode_float32_eq. rewrite Float.singleoffloat_of_bits. auto.
 Qed.
 
 (** Pointers cannot be forged. *)
 
 Definition memval_valid_first (mv: memval) : Prop :=
   match mv with
-  | Pointer b ofs n => n = pred (size_chunk_nat Mint32)
+  | Pointer b ofs n => n = 3%nat
   | _ => True
   end.
 
 Definition memval_valid_cont (mv: memval) : Prop :=
   match mv with
-  | Pointer b ofs n => n <> pred (size_chunk_nat Mint32)
+  | Pointer b ofs n => n <> 3%nat
   | _ => True
   end.
 
@@ -765,11 +614,8 @@ Proof.
     intros. destruct bl; simpl in *. congruence. 
     constructor. exact I. unfold inj_bytes. intros.
     exploit list_in_map_inv; eauto. intros [x [A B]]. subst mv. exact I.
-  destruct v; simpl. 
-  auto.
-  apply H0. apply encode_int_length. 
-  apply H0. apply encode_float_length.
-  destruct chunk; auto. 
+  destruct v; auto; destruct chunk; simpl; auto; try (apply H0); try (apply encode_int_length).
+  apply encode_float_64_length. 
   constructor. red. auto.
   simpl; intros. intuition; subst mv; red; simpl; congruence.
 Qed.
@@ -812,7 +658,7 @@ Proof.
   subst mv. split. red; auto. congruence.
   intros. destruct chunk; auto. unfold proj_pointer.
   destruct mvl; auto. destruct m; auto. 
-  caseEq (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: mvl)); auto.
+  caseEq (check_pointer 4%nat b i (Pointer b i n :: mvl)); auto.
   intros. right. exploit check_pointer_inv; eauto. simpl; intros; inv H2.
   constructor. red. auto. congruence. 
   simpl; intros. intuition; subst mv; simpl; congruence.
@@ -821,29 +667,34 @@ Qed.
 Lemma encode_val_pointer_inv:
   forall chunk v b ofs n mvl,
   encode_val chunk v = Pointer b ofs n :: mvl ->
-  chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer (pred (size_chunk_nat Mint32)) b ofs.
-Proof.
-  intros until mvl. 
-  destruct (size_chunk_nat_pos chunk) as [sz SZ].
-  unfold encode_val. rewrite SZ. destruct v.
-  simpl. congruence. 
-  generalize (encode_int_length chunk i). destruct (encode_int chunk i); simpl; congruence.
-  generalize (encode_float_length chunk f). destruct (encode_float chunk f); simpl; congruence.
-  destruct chunk; try (simpl; congruence). 
-  simpl. intuition congruence. 
+  chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3%nat b ofs.
+Proof.
+  intros until mvl.
+  assert (A: list_repeat (size_chunk_nat chunk) Undef = Pointer b ofs n :: mvl ->
+            chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs).
+    intros. destruct (size_chunk_nat_pos chunk) as [sz SZ]. rewrite SZ in H. simpl in H. discriminate.
+  assert (B: forall bl, length bl <> 0%nat -> inj_bytes bl = Pointer b ofs n :: mvl ->
+            chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs).
+    intros. destruct bl; simpl in *; congruence.
+  unfold encode_val; destruct v; destruct chunk;
+  (apply A; assumption) ||
+  (apply B; try (rewrite encode_int_length; congruence)) || idtac.
+  rewrite encode_float_32_length; congruence.
+  rewrite encode_float_64_length; congruence.
+  simpl. intros EQ; inv EQ; auto. 
 Qed.
 
 Lemma decode_val_pointer_inv:
   forall chunk mvl b ofs,
   decode_val chunk mvl = Vptr b ofs ->
-  chunk = Mint32 /\ mvl = inj_pointer (size_chunk_nat Mint32) b ofs.
+  chunk = Mint32 /\ mvl = inj_pointer 4%nat b ofs.
 Proof.
   intros until ofs; unfold decode_val.
   destruct (proj_bytes mvl). 
   destruct chunk; congruence.
   destruct chunk; try congruence.
   unfold proj_pointer. destruct mvl. congruence. destruct m; try congruence.
-  case_eq (check_pointer (size_chunk_nat Mint32) b0 i (Pointer b0 i n :: mvl)); intros.
+  case_eq (check_pointer 4%nat b0 i (Pointer b0 i n :: mvl)); intros.
   inv H0. split; auto. apply check_pointer_inv; auto. 
   congruence.
 Qed.
@@ -937,7 +788,7 @@ Lemma proj_pointer_inject:
 Proof.
   intros. unfold proj_pointer.
   inversion H; subst. auto. inversion H0; subst; auto.
-  case_eq (check_pointer (size_chunk_nat Mint32) b0 ofs1 (Pointer b0 ofs1 n :: al)); intros.
+  case_eq (check_pointer 4%nat b0 ofs1 (Pointer b0 ofs1 n :: al)); intros.
   exploit check_pointer_inject. eexact H. eauto. eauto. 
   intro. rewrite H4. econstructor; eauto. 
   constructor.
@@ -1021,10 +872,10 @@ Theorem encode_val_inject:
   list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
 Proof.
   intros. inv H; simpl.
-  apply inj_bytes_inject.
-  apply inj_bytes_inject.
-  destruct chunk; try apply repeat_Undef_inject_self. 
-  unfold inj_pointer; simpl; repeat econstructor; auto. 
+  destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
+  destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
+  destruct chunk; try (apply repeat_Undef_inject_self). 
+  repeat econstructor; eauto. 
   replace (size_chunk_nat chunk) with (length (encode_val chunk v2)).
   apply repeat_Undef_inject_any. apply encode_val_length. 
 Qed.
@@ -1037,4 +888,4 @@ Proof.
   red. destruct mv; econstructor.
   unfold inject_id; reflexivity. rewrite Int.add_zero; auto. 
 Qed.
- 
+
diff --git a/common/Memory.v b/common/Memory.v
index 0fc663f..49dcd7b 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -659,7 +659,8 @@ Proof.
   set (cl := getN (size_chunk_nat Mint8unsigned) ofs m.(mem_contents)#b).
   destruct (valid_access_dec m Mint8signed b ofs Readable).
   rewrite pred_dec_true; auto. unfold decode_val. 
-  destruct (proj_bytes cl); auto. rewrite decode_int8_signed_unsigned. auto.
+  destruct (proj_bytes cl); auto.
+  simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto.
   rewrite pred_dec_false; auto.
 Qed.
 
@@ -672,7 +673,8 @@ Proof.
   set (cl := getN (size_chunk_nat Mint16unsigned) ofs m.(mem_contents)#b).
   destruct (valid_access_dec m Mint16signed b ofs Readable).
   rewrite pred_dec_true; auto. unfold decode_val. 
-  destruct (proj_bytes cl); auto. rewrite decode_int16_signed_unsigned. auto.
+  destruct (proj_bytes cl); auto.
+  simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto.
   rewrite pred_dec_false; auto.
 Qed.
 
@@ -939,13 +941,20 @@ Proof.
   apply inj_eq_rev; auto.
 Qed.
 
+Theorem load_store_similar_2:
+  forall chunk',
+  size_chunk chunk' = size_chunk chunk ->
+  type_of_chunk chunk' = type_of_chunk chunk ->
+  load chunk' m2 b ofs = Some (Val.load_result chunk' v).
+Proof.
+  intros. destruct (load_store_similar chunk') as [v' [A B]]. auto.
+  rewrite A. decEq. eapply decode_encode_val_similar with (chunk1 := chunk); eauto.
+Qed.
+
 Theorem load_store_same:
-  Val.has_type v (type_of_chunk chunk) ->
   load chunk m2 b ofs = Some (Val.load_result chunk v).
 Proof.
-  intros.
-  destruct (load_store_similar chunk) as [v' [A B]]. auto.
-  rewrite A. decEq. eapply decode_encode_val_similar; eauto. 
+  apply load_store_similar_2; auto.
 Qed.
 
 Theorem load_store_other:
@@ -1276,7 +1285,10 @@ Theorem store_float32_truncate:
   forall m b ofs n,
   store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) =
   store Mfloat32 m b ofs (Vfloat n).
-Proof. intros. apply store_similar_chunks. simpl. decEq. apply encode_float32_cast. Qed.
+Proof.
+  intros. apply store_similar_chunks. simpl. decEq.
+  repeat rewrite encode_float32_eq. rewrite Float.bits_of_singleoffloat. auto. 
+Qed.
 
 (** ** Properties related to [storebytes]. *)
 
diff --git a/common/Memtype.v b/common/Memtype.v
index a13e861..b7d953f 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -418,7 +418,6 @@ Axiom load_store_similar:
 
 Axiom load_store_same:
   forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 ->
-  Val.has_type v (type_of_chunk chunk) ->
   load chunk m2 b ofs = Some (Val.load_result chunk v).
 
 Axiom load_store_other:
diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
new file mode 100644
index 0000000..61f26e7
--- /dev/null
+++ b/ia32/CombineOp.v
@@ -0,0 +1,101 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+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.
+
+Section COMBINE.
+
+Variable get: valnum -> option rhs.
+
+Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys)
+  | _ => None
+  end.
+
+Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys)
+  | _ => None
+  end.
+
+Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) :=
+  match cond, args with
+  | Ccompimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | Ccompuimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompuimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | _, _ => None
+  end.
+
+Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+  match addr, args with
+  | Aindexed n, x::nil =>
+      match get x with
+      | Some(Op (Olea a) ys) => Some(SelectOp.offset_addressing a n, ys)
+      | _ => None
+      end
+  | _, _ => None
+  end.
+
+Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
+  match op, args with
+  | Oandimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
+      | _ => None
+      end
+  | Oorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
+      | _ => None
+      end
+  | Oxorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
+      | _ => None
+      end
+  | Olea addr, _ =>
+      match combine_addr addr args with
+      | Some(addr', args') => Some(Olea addr', args')
+      | None => None
+      end
+  | Ocmp cond, _ =>
+      match combine_cond cond args with
+      | Some(cond', args') => Some(Ocmp cond', args')
+      | None => None
+      end
+  | _, _ => None
+  end.
+
+End COMBINE.
+
+
diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v
new file mode 100644
index 0000000..c6d2509
--- /dev/null
+++ b/ia32/CombineOpproof.v
@@ -0,0 +1,130 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import CombineOp.
+Require Import CSE.
+
+Section COMBINE.
+
+Variable ge: genv.
+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.
+
+Lemma combine_compimm_ne_0_sound:
+  forall x cond args,
+  combine_compimm_ne_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero).
+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. 
+  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+  (* of and *)
+  exploit get_sound; eauto. unfold equation_holds; simpl. 
+  destruct args; try discriminate. destruct args; try discriminate. simpl. 
+  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+Qed.
+
+Lemma combine_compimm_eq_0_sound:
+  forall x cond args,
+  combine_compimm_eq_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero).
+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. 
+  rewrite eval_negate_condition. 
+  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+  (* of and *)
+  exploit get_sound; eauto. unfold equation_holds; simpl. 
+  destruct args; try discriminate. destruct args; try discriminate. simpl. 
+  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+Qed.
+
+Theorem combine_cond_sound:
+  forall cond args cond' args',
+  combine_cond get cond args = Some(cond', args') ->
+  eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+  (* compimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+  (* compuimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compuimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+Qed.
+
+Theorem combine_addr_sound:
+  forall addr args addr' args',
+  combine_addr get addr args = Some(addr', args') ->
+  eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
+Proof.
+  intros. functional inversion H; subst.
+  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ.
+  assert (forall vl,
+         eval_addressing ge sp (SelectOp.offset_addressing a n) vl =
+         option_map (fun v => Val.add v (Vint n)) (eval_addressing ge sp a vl)).
+    intros. destruct a; simpl; repeat (destruct vl; auto); simpl. 
+    rewrite Val.add_assoc. auto. 
+    repeat rewrite Val.add_assoc. auto.
+    rewrite Val.add_assoc. auto.
+    repeat rewrite Val.add_assoc. auto.
+    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto. 
+    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto.
+      repeat rewrite <- (Val.add_commut v). rewrite Val.add_assoc. auto. 
+    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i0); auto.
+      repeat rewrite <- (Val.add_commut (Val.mul v (Vint i))). rewrite Val.add_assoc. auto.
+    rewrite Val.add_assoc; auto.
+  rewrite H0. rewrite EQ. auto. 
+Qed.
+
+Theorem combine_op_sound:
+  forall op args op' args',
+  combine_op get op args = Some(op', args') ->
+  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+(* andimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.and_assoc. auto.
+(* orimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.or_assoc. auto.
+(* xorimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.xor_assoc. auto.
+(* lea *)
+  simpl. eapply combine_addr_sound; eauto. 
+(* cmp *)
+  simpl. decEq; decEq. eapply combine_cond_sound; eauto.
+Qed.
+
+End COMBINE.
diff --git a/ia32/Op.v b/ia32/Op.v
index 896badf..0b32b88 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -446,20 +446,18 @@ Definition negate_condition (cond: condition): condition :=
   end.
 
 Lemma eval_negate_condition:
-  forall cond vl m b,
-  eval_condition cond vl m = Some b ->
-  eval_condition (negate_condition cond) vl m = Some (negb b).
+  forall cond vl m,
+  eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m).
 Proof.
-  intros. 
-  destruct cond; simpl in H; FuncInv; simpl.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite H; auto.
-  destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. 
-  rewrite H0; auto.
-  rewrite <- H0. rewrite negb_elim; auto.
+  intros. destruct cond; simpl.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
+  destruct vl; auto. destruct v; auto. destruct vl; auto. 
+  destruct vl; auto. destruct v; auto. destruct vl; auto. simpl. rewrite negb_involutive. auto.
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 658a755..9b1cd89 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -176,13 +176,9 @@ Proof.
 (* intconst *)
   destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
 (* cmp *)
-  inv H. simpl in H5.
-  destruct (eval_condition c vl m) as []_eqn. 
-  TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto.
-  inv H5. simpl. 
-  destruct (eval_condition (negate_condition c) vl m) as []_eqn.
-  destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto.
-  exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto.
+  inv H. simpl in H5. inv H5.
+  TrivialExists. simpl. rewrite eval_negate_condition. 
+  destruct (eval_condition c vl m); auto. destruct b; auto. 
 (* condition *)
   inv H. destruct v1.
   exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
diff --git a/powerpc/CombineOp.v b/powerpc/CombineOp.v
new file mode 100644
index 0000000..243da4e
--- /dev/null
+++ b/powerpc/CombineOp.v
@@ -0,0 +1,119 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+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.
+
+Section COMBINE.
+
+Variable get: valnum -> option rhs.
+
+Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys)
+  | _ => None
+  end.
+
+Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys)
+  | _ => None
+  end.
+
+Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) :=
+  match cond, args with
+  | Ccompimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | Ccompuimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompuimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | _, _ => None
+  end.
+
+Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+  match addr, args with
+  | Aindexed n, x::nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys)
+      | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None
+      | _ => None
+      end
+  | _, _ => None
+  end.
+
+Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
+  match op, args with
+  | Oaddimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Oaddimm (Int.add m n), ys)
+      | Some(Op (Osubimm m) ys) => Some(Osubimm (Int.add m n), ys)
+      | _ => None
+      end
+  | Osubimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Osubimm (Int.sub n m), ys)
+      | _ => None
+      end
+  | Oandimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
+      | Some(Op (Orolm amount m) ys) => Some(Orolm amount (Int.and m n), ys)
+      | _ => None
+      end
+  | Oorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
+      | _ => None
+      end
+  | Oxorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
+      | _ => None
+      end
+  | Orolm amount2 mask2, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm mask1) ys) =>
+           Some(Orolm (Int.modu amount2 Int.iwordsize)
+                     (Int.and (Int.rol mask1 amount2) mask2), ys)
+      | Some(Op (Orolm amount1 mask1) ys) =>
+           Some(Orolm (Int.modu (Int.add amount1 amount2) Int.iwordsize)
+                     (Int.and (Int.rol mask1 amount2) mask2), ys)
+      | _ => None
+      end
+  | Ocmp cond, _ =>
+      match combine_cond cond args with
+      | Some(cond', args') => Some(Ocmp cond', args')
+      | None => None
+      end
+  | _, _ => None
+  end.
+
+End COMBINE.
+
+
diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v
new file mode 100644
index 0000000..f493c16
--- /dev/null
+++ b/powerpc/CombineOpproof.v
@@ -0,0 +1,142 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import CombineOp.
+Require Import CSE.
+
+Section COMBINE.
+
+Variable ge: genv.
+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.
+
+Lemma combine_compimm_ne_0_sound:
+  forall x cond args,
+  combine_compimm_ne_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero).
+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. 
+  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+  (* of and *)
+  exploit get_sound; eauto. unfold equation_holds; simpl. 
+  destruct args; try discriminate. destruct args; try discriminate. simpl. 
+  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+Qed.
+
+Lemma combine_compimm_eq_0_sound:
+  forall x cond args,
+  combine_compimm_eq_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero).
+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. 
+  rewrite eval_negate_condition. 
+  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+  (* of and *)
+  exploit get_sound; eauto. unfold equation_holds; simpl. 
+  destruct args; try discriminate. destruct args; try discriminate. simpl. 
+  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+Qed.
+
+Theorem combine_cond_sound:
+  forall cond args cond' args',
+  combine_cond get cond args = Some(cond', args') ->
+  eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+  (* compimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+  (* compuimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compuimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+Qed.
+
+Theorem combine_addr_sound:
+  forall addr args addr' args',
+  combine_addr get addr args = Some(addr', args') ->
+  eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
+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. 
+  (* indexed 0 - add *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
+  rewrite <- H0. destruct v; destruct v0; simpl; auto; rewrite Int.add_zero; auto.
+Qed.
+
+Theorem combine_op_sound:
+  forall op args op' args',
+  combine_op get op args = Some(op', args') ->
+  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
+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.
+(* 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.
+(* subimm - addimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1.
+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.
+(* andimm - rolm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. destruct v; simpl; auto. unfold Int.rolm. rewrite Int.and_assoc. auto.
+(* orimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.or_assoc. auto.
+(* xorimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.xor_assoc. auto.
+(* rolm - andimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm. 
+  rewrite (Int.add_commut Int.zero). rewrite Int.add_zero. auto.
+(* rolm - rolm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.rolm_rolm. auto. 
+(* cmp *)
+  simpl. decEq; decEq. eapply combine_cond_sound; eauto.
+Qed.
+
+End COMBINE.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 76c426b..986ea8c 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -420,20 +420,18 @@ Definition negate_condition (cond: condition): condition :=
   end.
 
 Lemma eval_negate_condition:
-  forall cond vl m b,
-  eval_condition cond vl m = Some b ->
-  eval_condition (negate_condition cond) vl m = Some (negb b).
+  forall cond vl m,
+  eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m).
 Proof.
-  intros. 
-  destruct cond; simpl in H; FuncInv; simpl.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite H; auto.
-  destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. 
-  rewrite H0; auto.
-  rewrite <- H0. rewrite negb_elim; auto.
+  intros. destruct cond; simpl.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
+  destruct vl; auto. destruct v; auto. destruct vl; auto. 
+  destruct vl; auto. destruct v; auto. destruct vl; auto. simpl. rewrite negb_involutive. auto.
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index c54beed..6c83ab7 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -119,6 +119,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 =>
       addimm n1 t2
+  | t1, Eop (Ointconst n2) Enil =>
+      addimm n2 t1
   | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
   | Eop (Oaddimm n1) (t1:::Enil), t2 =>
@@ -127,8 +129,6 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       Eop Oadd (Eop (Oaddrsymbol s (Int.add n1 n2)) Enil ::: t2 ::: Enil)
   | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
       Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil)
-  | t1, Eop (Ointconst n2) Enil =>
-      addimm n2 t1
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
   | _, _ =>
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index b42503f..e4f981d 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -192,13 +192,9 @@ Proof.
 (* intconst *)
   destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
 (* cmp *)
-  inv H. simpl in H5.
-  destruct (eval_condition c vl m) as []_eqn. 
-  TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto.
-  inv H5. simpl. 
-  destruct (eval_condition (negate_condition c) vl m) as []_eqn.
-  destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto.
-  exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto.
+  inv H. simpl in H5. inv H5. 
+  TrivialExists. simpl. rewrite eval_negate_condition.
+  destruct (eval_condition c vl m); auto. destruct b; auto.
 (* condition *)
   inv H. destruct v1.
   exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
@@ -224,6 +220,7 @@ Proof.
   red; intros until y.
   unfold add; case (add_match a b); intros; InvEval.
   rewrite Val.add_commut. apply eval_addimm; auto.
+  apply eval_addimm; auto.
   subst. 
   replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
      with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
@@ -242,7 +239,6 @@ Proof.
     econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. 
     simpl. repeat rewrite Val.add_assoc. decEq; decEq.
     rewrite Val.add_commut. rewrite Val.add_permut. auto.
-  apply eval_addimm; auto.
   subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
   TrivialExists. 
 Qed.