From 336a1f906a9c617e68e9d43e244bf42e9bdbae64 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 9 Apr 2014 13:26:16 +0000
Subject: Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0
 comparisons over booleans. Select*: more systematic constant propagation;
 don't CP shifts by amounts outside of [0..31]. Driver: timer for whole
 compilation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 .depend                    | 14 ++++----
 arm/ConstpropOp.vp         | 20 +++++++++--
 arm/ConstpropOpproof.v     | 50 ++++++++++++++++++++++++++--
 arm/SelectOp.vp            | 43 ++++++++++++++++++++----
 arm/SelectOpproof.v        | 49 +++++++++++++++++++--------
 backend/SelectLong.vp      | 38 ++++++++++++---------
 backend/SelectLongproof.v  | 20 +++--------
 backend/ValueDomain.v      | 14 ++++++++
 cfrontend/Cminorgen.v      | 10 ++----
 driver/Driver.ml           |  2 +-
 ia32/ConstpropOp.vp        | 55 ++++++++++++++++++++-----------
 ia32/ConstpropOpproof.v    | 82 +++++++++++++++++++++++++++++++++++++---------
 ia32/SelectOp.vp           | 75 ++++++++++++++++++++----------------------
 ia32/SelectOpproof.v       | 12 -------
 lib/Integers.v             | 10 ++++++
 powerpc/ConstpropOp.vp     | 24 +++++++++++---
 powerpc/ConstpropOpproof.v | 54 +++++++++++++++++++++++++++---
 powerpc/SelectOp.vp        | 57 ++++++++++++++++++++++++++------
 powerpc/SelectOpproof.v    | 46 ++++++++++++++++++++------
 19 files changed, 489 insertions(+), 186 deletions(-)

diff --git a/.depend b/.depend
index 7307c32..c92c487 100644
--- a/.depend
+++ b/.depend
@@ -35,7 +35,7 @@ $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)
 backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
 backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo
 backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo
-$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
+$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
 backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.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 backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo
 backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo
 backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo
@@ -59,18 +59,18 @@ $(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)
 backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo
 $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/ValueDomain.vo
 backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo
-$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.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 backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo
+$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.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 backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo
 backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.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 backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo
 backend/CSEdomain.vo backend/CSEdomain.glob backend/CSEdomain.v.beautified: backend/CSEdomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo
 $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/CSEdomain.vo
 backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: 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 $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/CSEdomain.vo backend/Kildall.vo $(ARCH)/CombineOp.vo
-$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(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 backend/CSEdomain.vo $(ARCH)/CombineOp.vo
+$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo
 backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: 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/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo
 backend/NeedDomain.vo backend/NeedDomain.glob backend/NeedDomain.v.beautified: backend/NeedDomain.v lib/Coqlib.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Registers.vo backend/ValueDomain.vo $(ARCH)/Op.vo backend/RTL.vo
 $(ARCH)/NeedOp.vo $(ARCH)/NeedOp.glob $(ARCH)/NeedOp.v.beautified: $(ARCH)/NeedOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/NeedDomain.vo backend/RTL.vo
 backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend/Deadcode.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memory.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo
 backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo
-$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo
+$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo
 backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo
 $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo
 backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo
@@ -91,10 +91,10 @@ $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob $(ARCH)/$(
 backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Lineartyping.vo
 backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo
 $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(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.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
+$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
 backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
-$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/Errors.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 backend/Conventions.vo backend/Asmgenproof0.vo
-$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(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 $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo
+$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.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 backend/Asmgenproof0.vo backend/Conventions.vo
+$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.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/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo
 cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo
 cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo
 cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index bf08610..2b658a4 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -74,6 +74,23 @@ Nondetfunction cond_strength_reduction
       (cond, args)
   end.
 
+Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
+  let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+
+Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
+  match c, args, vl with
+  | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | _, _, _ =>
+      make_cmp_base c args vl
+  end.
+
 Definition make_addimm (n: int) (r: reg) :=
   if Int.eq n Int.zero
   then (Omove, r :: nil)
@@ -191,8 +208,7 @@ Nondetfunction op_strength_reduction
   | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
   | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
   | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
-  | Ocmp c, args, vl =>
-      let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
+  | Ocmp c, args, vl => make_cmp c args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
   | _, _, _ => (op, args)
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 90e18f2..7cf5879 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -126,6 +126,52 @@ Proof.
 - auto.
 Qed.
 
+Lemma make_cmp_base_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp_base c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+  intros. unfold make_cmp_base. 
+  generalize (cond_strength_reduction_correct c args vl H). 
+  destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ. auto. 
+Qed.
+
+Lemma make_cmp_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+  intros c args vl.
+  assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true ->
+             rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one).
+  { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
+  unfold make_cmp. case (make_cmp_match c args vl); intros.
+- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (rs#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (rs#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- apply make_cmp_base_correct; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -416,9 +462,7 @@ Proof.
 (* singleoffloat *)
   InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cmp *)
-  generalize (cond_strength_reduction_correct c args0 vl0). 
-  destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
-  rewrite <- H1 in H0; auto. econstructor; split; eauto.
+  inv H0. apply make_cmp_correct; auto.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2).
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 43745ca..efd9e48 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -58,9 +58,11 @@ Definition addrstack (ofs: int) :=
 
 Nondetfunction notint (e: expr) :=
   match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil
   | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil)
   | Eop Onot (t1:::Enil) => t1
   | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil)
+  | Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil)
   | _ => Eop Onot (e:::Enil)
   end.
 
@@ -93,6 +95,14 @@ Nondetfunction add (e1: expr) (e2: expr) :=
 
 (** ** Integer and pointer subtraction *)
 
+Nondetfunction rsubimm (n: int) (e: expr) :=
+  match e with
+  | Eop (Ointconst m) Enil => Eop (Ointconst (Int.sub n m)) Enil
+  | Eop (Oaddimm m) (t:::Enil) => Eop (Orsubimm (Int.sub n m)) (t:::Enil)
+  | Eop (Orsubimm m) (t:::Enil) => Eop (Oaddimm (Int.sub n m)) (t:::Enil)
+  | _ => Eop (Orsubimm n) (e:::Enil)
+  end.
+
 Nondetfunction sub (e1: expr) (e2: expr) :=
   match e1, e2 with
   | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1
@@ -102,13 +112,13 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
       addimm n1 (Eop Osub (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
-  | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil)
+  | Eop (Ointconst n1) Enil, t2 => rsubimm n1 t2
   | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil)
   | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil)
   | _, _ => Eop Osub (e1:::e2:::Enil)
   end.
 
-Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil).
+Definition negint (e: expr) := rsubimm Int.zero e.
 
 (** ** Immediate shifts *)
 
@@ -247,9 +257,11 @@ Nondetfunction or (e1: expr) (e2: expr) :=
 
 Nondetfunction xorimm (n1: int) (e2: expr) :=
   if Int.eq n1 Int.zero then e2 else
+  if Int.eq n1 Int.mone then notint e2 else
   match e2 with
   | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
   | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+  | Eop Onot (t2:::Enil) => Eop (Oxorimm (Int.not n1)) (t2:::Enil)
   | _ => Eop (Oxorimm n1) (e2:::Enil)
   end.
 
@@ -315,7 +327,6 @@ Definition absf (e: expr) :=  Eop Oabsf (e ::: Enil).
 Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
 Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
 Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
-Definition divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
 
 (** ** Comparisons *)
 
@@ -370,19 +381,37 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
 
 Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
 
-Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
+Nondetfunction cast8signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
+  | _ => Eop Ocast8signed (e ::: Enil)
+  end.
 
 Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
 
-Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
+Nondetfunction cast16signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
+  | _ => Eop Ocast16signed (e ::: Enil)
+  end.
 
 (** ** Floating-point conversions *)
 
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
-Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
-Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil).
+
+Nondetfunction floatofint (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil
+  | _ => Eop Ofloatofint (e ::: Enil)
+  end.
+
+Nondetfunction floatofintu (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil
+  | _ => Eop Ofloatofintu (e ::: Enil)
+  end.
 
 (** ** Recognition of addressing modes for load and store operations *)
 
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 9fbab44..d10e7fc 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -133,9 +133,11 @@ Qed.
 Theorem eval_notint: unary_constructor_sound notint Val.notint.
 Proof.
   unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
+  TrivialExists.
   subst x. TrivialExists.
   exists v1; split; auto. subst. destruct v1; simpl; auto. rewrite Int.not_involutive; auto.
   exists (eval_shift s v1); split. EvalOp. subst x. destruct (eval_shift s v1); simpl; auto. rewrite Int.not_involutive; auto.
+  subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -177,6 +179,20 @@ Proof.
   TrivialExists.
 Qed.
 
+Theorem eval_rsubimm: forall n, unary_constructor_sound (rsubimm n) (fun v => Val.sub (Vint n) v).
+Proof.
+  red; intros until x. unfold rsubimm; case (rsubimm_match a); intros.
+  InvEval. TrivialExists.
+  InvEval. subst x. econstructor; split. EvalOp. unfold eval_operation; eauto.
+  destruct v1; simpl; auto. rewrite Int.sub_add_r. rewrite <- Int.sub_add_opp. 
+  auto.
+  InvEval. subst x. econstructor; split. EvalOp. simpl; eauto.
+  fold (Val.sub (Vint m0) v1). destruct v1; simpl; auto.
+  rewrite ! Int.sub_add_opp.  rewrite Int.neg_add_distr. rewrite Int.neg_involutive.
+  rewrite (Int.add_permut i). rewrite (Int.add_commut i). auto.
+  TrivialExists.
+Qed.
+
 Theorem eval_sub: binary_constructor_sound sub Val.sub.
 Proof.
   red; intros until y.
@@ -187,7 +203,7 @@ Proof.
     apply eval_addimm; EvalOp.
   subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
   subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp.
-  TrivialExists.
+  apply eval_rsubimm; auto.
   subst. TrivialExists.
   subst. TrivialExists.
   TrivialExists.
@@ -195,7 +211,7 @@ Qed.
 
 Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
 Proof.
-  red; intros. unfold negint. TrivialExists.
+  red; intros. unfold negint. apply eval_rsubimm; auto. 
 Qed.
 
 Theorem eval_shlimm:
@@ -426,9 +442,13 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero. 
   intros. exists x; split. auto.  
   destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto.
-  destruct (xorimm_match a); intros; InvEval.
+  predSpec Int.eq Int.eq_spec n Int.mone.
+  intros. subst n. rewrite <- Val.not_xor. apply eval_notint; auto.
+  intros. destruct (xorimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.xor_commut; auto.
-  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. 
+  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
+  subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. 
+  rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists.
   TrivialExists.
 Qed.
 
@@ -614,11 +634,6 @@ Proof.
   red; intros; TrivialExists.
 Qed.
 
-Theorem eval_divf: binary_constructor_sound divf Val.divf.
-Proof.
-  red; intros; TrivialExists.
-Qed.
-
 Section COMP_IMM.
 
 Variable default: comparison -> int -> condition.
@@ -716,7 +731,9 @@ Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
-  red; intros. unfold cast8signed. TrivialExists.
+  red; intros until x. unfold cast8signed; case (cast8signed_match a); intros.
+  InvEval. TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
@@ -727,7 +744,9 @@ Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
 Proof.
-  red; intros. unfold cast16signed. TrivialExists.
+  red; intros until x. unfold cast16signed; case (cast16signed_match a); intros.
+  InvEval. TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
@@ -756,7 +775,9 @@ Theorem eval_floatofint:
   Val.floatofint x = Some y ->
   exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold floatofint. TrivialExists. 
+  intros until y; unfold floatofint. case (floatofint_match a); intros.
+  InvEval. simpl in H0. TrivialExists. 
+  TrivialExists. 
 Qed.
 
 Theorem eval_intuoffloat:
@@ -774,7 +795,9 @@ Theorem eval_floatofintu:
   Val.floatofintu x = Some y ->
   exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold floatofintu. TrivialExists. 
+  intros until y; unfold floatofintu. case (floatofintu_match a); intros.
+  InvEval. simpl in H0. TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_addressing:
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index 09f29af..0c1cbb3 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -27,10 +27,10 @@ Open Local Scope cminorsel_scope.
   the names of these functions. *)
 
 Record helper_functions : Type := mk_helper_functions {
-  i64_dtos: ident;                      (**r float -> signed long *)
-  i64_dtou: ident;                      (**r float -> unsigned long *)
-  i64_stod: ident;                      (**r signed long -> float *)
-  i64_utod: ident;                      (**r unsigned long -> float *)
+  i64_dtos: ident;                      (**r float64 -> signed long *)
+  i64_dtou: ident;                      (**r float64 -> unsigned long *)
+  i64_stod: ident;                      (**r signed long -> float64 *)
+  i64_utod: ident;                      (**r unsigned long -> float64 *)
   i64_stof: ident;                      (**r signed long -> float32 *)
   i64_utof: ident;                      (**r unsigned long -> float32 *)
   i64_neg: ident;                       (**r opposite *)
@@ -304,13 +304,16 @@ Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) :=
 Definition cmplu (c: comparison) (e1 e2: expr) :=
   match c with
   | Ceq =>
-      if is_longconst_zero e2
-      then cmpl_eq_zero e1
-      else cmpl_eq_zero (xorl e1 e2)
+      cmpl_eq_zero (xorl e1 e2)
+(*
+        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Cne =>
-      if is_longconst_zero e2
-      then cmpl_ne_zero e1
-      else cmpl_ne_zero (xorl e1 e2)
+      cmpl_ne_zero (xorl e1 e2)
+(*        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Clt =>
       cmplu_gen Clt Clt e1 e2
   | Cle =>
@@ -330,13 +333,16 @@ Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) :=
 Definition cmpl (c: comparison) (e1 e2: expr) :=
   match c with
   | Ceq =>
-      if is_longconst_zero e2
-      then cmpl_eq_zero e1
-      else cmpl_eq_zero (xorl e1 e2)
+      cmpl_eq_zero (xorl e1 e2)
+(*
+        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Cne =>
-      if is_longconst_zero e2
-      then cmpl_ne_zero e1
-      else cmpl_ne_zero (xorl e1 e2)
+      cmpl_ne_zero (xorl e1 e2)
+(*        (if is_longconst_zero e2 then e1
+         else if is_longconst_zero e1 then e2
+         else xorl e1 e2) *)
   | Clt =>
       if is_longconst_zero e2
       then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil)
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index 26f33da..ec0dd2c 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -1024,16 +1024,10 @@ Proof.
   rename i into x. rename i0 into y.
   destruct c; simpl.
 - (* Ceq *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_eq_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
   rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.  
 - (* Cne *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_ne_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
   rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.  
 - (* Clt *)
   exploit (eval_cmplu_gen Clt Clt). eexact H. eexact H0. simpl.
@@ -1095,16 +1089,10 @@ Proof.
   rename i into x. rename i0 into y.
   destruct c; simpl.
 - (* Ceq *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_eq_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
   rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.
 - (* Cne *)
-  destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
-  apply eval_cmpl_ne_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
+  exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
   rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.
 - (* Clt *)
   destruct (is_longconst_zero b) eqn:LC.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 239dd47..2ece8cd 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -681,6 +681,14 @@ Qed.
 
 Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va.
 
+Lemma is_uns_1:
+  forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one.
+Proof.
+  intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros.
+  rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. 
+  rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega.
+Qed.
+
 (** Smart constructors for [Uns] and [Sgn]. *)
 
 Definition uns (n: Z) : aval :=
@@ -749,6 +757,12 @@ Qed.
 
 Hint Resolve vmatch_uns vmatch_uns_undef vmatch_sgn vmatch_sgn_undef : va.
 
+Lemma vmatch_Uns_1:
+  forall v, vmatch v (Uns 1) -> v = Vundef \/ v = Vint Int.zero \/ v = Vint Int.one.
+Proof.
+  intros. inv H; auto. right. exploit is_uns_1; eauto. intuition congruence.
+Qed.
+
 (** Ordering *)
 
 Inductive vge: aval -> aval -> Prop :=
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 724e80c..8ecf498 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -39,13 +39,9 @@ Local Open Scope error_monad_scope.
   taken in the Csharpminor code can be mapped to Cminor local
   variable, since the latter do not reside in memory.  
 
-  Another task performed during the translation to Cminor is to eliminate
-  redundant casts to small numerical types (8- and 16-bit integers,
-  single-precision floats).  
-
-  Finally, the Clight-like [switch] construct of Csharpminor
-  is transformed into the simpler, lower-level [switch] construct
-  of Cminor.
+  Another task performed during the translation to Cminor is to
+  transform the Clight-like [switch] construct of Csharpminor
+  into the simpler, lower-level [switch] constructs of Cminor.
 *)
 
 (** * Handling of variables *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index e768fa2..88871f7 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -574,7 +574,7 @@ let _ =
     eprintf "Ambiguous '-o' option (multiple source files)\n";
     exit 2
   end;
-  let linker_args = perform_actions () in
+  let linker_args = time "Total compilation time" perform_actions () in
   if (not nolink) && linker_args <> [] then begin
     linker (output_filename_default "a.out") linker_args
   end
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 172f7a4..b27f405 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -44,6 +44,23 @@ Nondetfunction cond_strength_reduction
       (cond, args)
   end.
 
+Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
+  let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+
+Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
+  match c, args, vl with
+  | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | _, _, _ =>
+      make_cmp_base c args vl
+  end.
+
 Nondetfunction addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
@@ -92,20 +109,20 @@ Definition make_addimm (n: int) (r: reg) :=
   then (Omove, r :: nil)
   else (Olea (Aindexed n), r :: nil).
 
-Definition make_shlimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
-  else (Oshlimm n, r :: nil).
+Definition make_shlimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then (Oshlimm n, r1 :: nil)
+  else (Oshl, r1 :: r2 :: nil).
 
-Definition make_shrimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
-  else (Oshrimm n, r :: nil).
+Definition make_shrimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then (Oshrimm n, r1 :: nil)
+  else (Oshr, r1 :: r2 :: nil).
 
-Definition make_shruimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
-  else (Oshruimm n, r :: nil).
+Definition make_shruimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then (Oshruimm n, r1 :: nil)
+  else (Oshru, r1 :: r2 :: nil).
 
 Definition make_mulimm (n: int) (r: reg) :=
   if Int.eq n Int.zero then
@@ -114,7 +131,7 @@ Definition make_mulimm (n: int) (r: reg) :=
     (Omove, r :: nil)
   else
     match Int.is_power2 n with
-    | Some l => make_shlimm l r
+    | Some l => (Oshlimm l, r :: nil)
     | None => (Omulimm n, r :: nil)
     end.
 
@@ -146,7 +163,7 @@ Definition make_divimm n (r1 r2: reg) :=
 
 Definition make_divuimm n (r1 r2: reg) :=
   match Int.is_power2 n with
-  | Some l => make_shruimm l r1
+  | Some l => (Oshruimm l, r1 :: nil)
   | None   => (Odivu, r1 :: r2 :: nil)
   end.
 
@@ -194,16 +211,14 @@ Nondetfunction op_strength_reduction
   | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1
   | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2
   | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1
-  | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1
-  | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1
-  | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1
+  | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
+  | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
+  | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
   | Olea addr, args, vl =>
       let (addr', args') := addr_strength_reduction addr args vl in
       (Olea addr', args')
   | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
-  | Ocmp c, args, vl =>
-      let (c', args') := cond_strength_reduction c args vl in 
-      (Ocmp c', args')
+  | Ocmp c, args, vl => make_cmp c args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
   | _, _, _ => (op, args)
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 6a83c1a..8a05534 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -160,6 +160,52 @@ Proof.
 - econstructor; eauto.
 Qed.
 
+Lemma make_cmp_base_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp_base c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
+Proof.
+  intros. unfold make_cmp_base. 
+  generalize (cond_strength_reduction_correct c args vl H). 
+  destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ. auto. 
+Qed.
+
+Lemma make_cmp_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
+Proof.
+  intros c args vl.
+  assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true ->
+             e#r = Vundef \/ e#r = Vint Int.zero \/ e#r = Vint Int.one).
+  { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
+  unfold make_cmp. case (make_cmp_match c args vl); intros.
+- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (e#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (e#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- apply make_cmp_base_correct; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -172,36 +218,45 @@ Proof.
 Qed.
   
 Lemma make_shlimm_correct:
-  forall n r1,
-  let (op, args) := make_shlimm n r1 in
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shlimm n r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shl e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto.
+  destruct (Int.ltu n Int.iwordsize). 
   econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shrimm_correct:
-  forall n r1,
-  let (op, args) := make_shrimm n r1 in
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shrimm n r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shr e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto.
-  econstructor; split; eauto. simpl. auto.
+  destruct (Int.ltu n Int.iwordsize). 
+  econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shruimm_correct:
-  forall n r1,
-  let (op, args) := make_shruimm n r1 in
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shruimm n r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shru e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto.
-  econstructor; split; eauto. simpl. congruence.
+  destruct (Int.ltu n Int.iwordsize). 
+  econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_mulimm_correct:
@@ -215,7 +270,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
-  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). apply make_shlimm_correct; auto. 
+  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. simpl; eauto. auto.
   econstructor; split; eauto. auto. 
 Qed.
 
@@ -243,9 +298,8 @@ Lemma make_divuimm_correct:
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
-  replace v with (Val.shru e#r1 (Vint i)). 
-  eapply make_shruimm_correct; eauto.
-  eapply Val.divu_pow2; eauto. congruence.
+  econstructor; split. simpl; eauto. 
+  rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto.
   exists v; auto.
 Qed.
 
@@ -466,9 +520,7 @@ Proof.
 (* singleoffloat *)
   InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cond *)
-  generalize (cond_strength_reduction_correct c args0 vl0 H). 
-  destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
-  rewrite <- H1 in H0; auto. econstructor; split; eauto.
+  inv H0. apply make_cmp_correct; auto.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) e#r2).
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 5f47df2..e82d0a3 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -144,39 +144,48 @@ Definition shift_is_scale (n: int) : bool :=
   Int.eq n (Int.repr 1) || Int.eq n (Int.repr 2) || Int.eq n (Int.repr 3).
 
 Nondetfunction shlimm (e1: expr) (n: int) :=
-  if Int.eq n Int.zero then e1 else
-  match e1 with
-  | Eop (Ointconst n1) Enil =>
-      Eop (Ointconst(Int.shl n1 n)) Enil
-  | Eop (Oshlimm n1) (t1:::Enil) =>
-      if Int.ltu (Int.add n n1) Int.iwordsize
-      then Eop (Oshlimm (Int.add n n1)) (t1:::Enil)
-      else Eop (Oshlimm n) (e1:::Enil)
-  | Eop (Olea (Aindexed n1)) (t1:::Enil) =>
-      if shift_is_scale n
-      then Eop (Olea (Ascaled (Int.shl Int.one n) (Int.shl n1 n))) (t1:::Enil)
-      else Eop (Oshlimm n) (e1:::Enil)
-  | _ =>
-      if shift_is_scale n
-      then Eop (Olea (Ascaled (Int.shl Int.one n) Int.zero)) (e1:::Enil)
-      else Eop (Oshlimm n) (e1:::Enil)
-  end.
+  if Int.eq n Int.zero then e1
+  if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshl (e1:::Eop (Ointconst n):::Enil)
+  else
+    match e1 with
+    | Eop (Ointconst n1) Enil =>
+        Eop (Ointconst(Int.shl n1 n)) Enil
+    | Eop (Oshlimm n1) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshlimm (Int.add n n1)) (t1:::Enil)
+        else Eop (Oshlimm n) (e1:::Enil)
+    | Eop (Olea (Aindexed n1)) (t1:::Enil) =>
+        if shift_is_scale n
+        then Eop (Olea (Ascaled (Int.shl Int.one n) (Int.shl n1 n))) (t1:::Enil)
+        else Eop (Oshlimm n) (e1:::Enil)
+    | _ =>
+        if shift_is_scale n
+        then Eop (Olea (Ascaled (Int.shl Int.one n) Int.zero)) (e1:::Enil)
+        else Eop (Oshlimm n) (e1:::Enil)
+    end.
 
 Nondetfunction shruimm (e1: expr) (n: int) :=
   if Int.eq n Int.zero then e1 else
-  match e1 with
-  | Eop (Ointconst n1) Enil =>
-      Eop (Ointconst(Int.shru n1 n)) Enil
-  | Eop (Oshruimm n1) (t1:::Enil) =>
-      if Int.ltu (Int.add n n1) Int.iwordsize
-      then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
-      else Eop (Oshruimm n) (e1:::Enil)
-  | _ =>
-      Eop (Oshruimm n) (e1:::Enil)
-  end.
+  if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshru (e1:::Eop (Ointconst n):::Enil)
+  else
+    match e1 with
+    | Eop (Ointconst n1) Enil =>
+        Eop (Ointconst(Int.shru n1 n)) Enil
+    | Eop (Oshruimm n1) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
+        else Eop (Oshruimm n) (e1:::Enil)
+    | _ =>
+        Eop (Oshruimm n) (e1:::Enil)
+    end.
 
 Nondetfunction shrimm (e1: expr) (n: int) :=
   if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshr (e1:::Eop (Ointconst n):::Enil)
+  else
   match e1 with
   | Eop (Ointconst n1) Enil =>
       Eop (Ointconst(Int.shr n1 n)) Enil
@@ -337,18 +346,6 @@ Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
 Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
 Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
 
-Definition divfimm (e: expr) (n: float) :=
-  match Float.exact_inverse n with
-  | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil)
-  | None    => Eop Odivf (e ::: Eop (Ofloatconst n) Enil ::: Enil)
-  end.
-
-Nondetfunction divf (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ofloatconst n2) Enil => divfimm e1 n2
-  | _ => Eop Odivf (e1 ::: e2 ::: Enil)
-  end.
-
 (** ** Comparisons *)
 
 Nondetfunction compimm (default: comparison -> int -> condition)
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 30e8c5b..16879c0 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -565,18 +565,6 @@ Proof.
   red; intros; TrivialExists.
 Qed.
 
-Theorem eval_divf: binary_constructor_sound divf Val.divf.
-Proof.
-  red. intros until y. unfold divf. destruct (divf_match b); intros.
-- unfold divfimm. destruct (Float.exact_inverse n2) as [n2' | ] eqn:EINV.
-  + inv H0. inv H4. simpl in H6. inv H6. econstructor; split.
-    EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. 
-    simpl; eauto. 
-    destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. 
-  + TrivialExists. 
-- TrivialExists.
-Qed.
-
 Section COMP_IMM.
 
 Variable default: comparison -> int -> condition.
diff --git a/lib/Integers.v b/lib/Integers.v
index d85007b..4464d26 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1202,6 +1202,11 @@ Qed.
 Remark Ztestbit_0: forall n, Z.testbit 0 n = false.
 Proof Z.testbit_0_l.
 
+Remark Ztestbit_1: forall n, Z.testbit 1 n = zeq n 0.
+Proof.
+  intros. destruct n; simpl; auto.
+Qed.
+
 Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true.
 Proof.
   intros. destruct n; simpl; auto. 
@@ -1515,6 +1520,11 @@ Proof.
   intros. unfold testbit. rewrite unsigned_zero. apply Ztestbit_0. 
 Qed.
 
+Remark bits_one: forall n, testbit one n = zeq n 0.
+Proof.
+  unfold testbit; intros. rewrite unsigned_one. apply Ztestbit_1. 
+Qed.
+
 Lemma bits_mone:
   forall i, 0 <= i < zwordsize -> testbit mone i = true.
 Proof.
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 6aa0925..e1e1960 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -46,6 +46,23 @@ Nondetfunction cond_strength_reduction
       (cond, args)
   end.
 
+Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
+  let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+
+Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
+  match c, args, vl with
+  | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
+      if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      else make_cmp_base c args vl
+  | _, _, _ =>
+      make_cmp_base c args vl
+  end.
+
 Definition make_addimm (n: int) (r: reg) :=
   if Int.eq n Int.zero
   then (Omove, r :: nil)
@@ -114,8 +131,8 @@ Definition make_orimm (n: int) (r: reg) :=
   else (Oorimm n, r :: nil).
 
 Definition make_xorimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
+  if Int.eq n Int.zero then (Omove, r :: nil)
+  else if Int.eq n Int.mone then (Onot, r :: nil)
   else (Oxorimm n, r :: nil).
 
 Definition make_mulfimm (n: float) (r r1 r2: reg) :=
@@ -158,8 +175,7 @@ Nondetfunction op_strength_reduction
   | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
   | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
   | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1
-  | Ocmp c, args, vl =>
-      let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
+  | Ocmp c, args, vl => make_cmp c args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
   | _, _, _ => (op, args)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 0c88246..a28d908 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -106,6 +106,52 @@ Proof.
 - auto.
 Qed.
 
+Lemma make_cmp_base_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp_base c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+  intros. unfold make_cmp_base. 
+  generalize (cond_strength_reduction_correct c args vl H). 
+  destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ. auto. 
+Qed.
+
+Lemma make_cmp_correct:
+  forall c args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_cmp c args vl in
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+         /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+  intros c args vl.
+  assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true ->
+             rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one).
+  { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
+  unfold make_cmp. case (make_cmp_match c args vl); intros.
+- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (rs#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (rs#r1); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  simpl in H; inv H. InvBooleans. subst n. 
+  exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+  apply make_cmp_base_correct; auto.
+- apply make_cmp_base_correct; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -256,7 +302,9 @@ Lemma make_xorimm_correct:
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
+  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto. 
+  predSpec Int.eq Int.eq_spec n Int.mone; intros.
+  subst n. exists (Val.notint rs#r); split; auto. 
   econstructor; split; eauto. auto. 
 Qed.
 
@@ -379,9 +427,7 @@ Proof.
 (* singleoffloat *)
   InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cmp *)
-  generalize (cond_strength_reduction_correct c args0 vl0). 
-  destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
-  rewrite <- H1 in H0; auto. econstructor; split; eauto.
+  inv H0. apply make_cmp_correct; auto.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2).
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index ad4f3b9..371a08a 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -68,6 +68,7 @@ Nondetfunction notint (e: expr) :=
   | Eop Onxor (t1:::t2:::Enil) => Eop Oxor (t1:::t2:::Enil)
   | Eop Oandc (t1:::t2:::Enil) => Eop Oorc (t2:::t1:::Enil)
   | Eop Oorc (t1:::t2:::Enil) => Eop Oandc (t2:::t1:::Enil)
+  | Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil)
   | _ => Eop Onot (e:::Enil)
   end.
 
@@ -121,10 +122,22 @@ Nondetfunction add (e1: expr) (e2: expr) :=
 
 (** ** Integer and pointer subtraction *)
 
+Nondetfunction subimm (n1: int) (e: expr) :=
+  match e with
+  | Eop (Ointconst n2) Enil =>
+      Eop (Ointconst (Int.sub n1 n2)) Enil
+  | Eop (Oaddimm n2) (t2:::Enil) =>
+      Eop (Osubimm (Int.sub n1 n2)) (t2 ::: Enil)
+  | _ =>
+      Eop (Osubimm n1) (e ::: Enil)
+  end.
+
 Nondetfunction sub (e1: expr) (e2: expr) :=
   match e1, e2 with
   | t1, Eop (Ointconst n2) Enil =>
       addimm (Int.neg n2) t1
+  | Eop (Ointconst n1) Enil, t2 =>
+      subimm n1 t2
   | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
   | Eop (Oaddimm n1) (t1:::Enil), t2 =>
@@ -135,7 +148,7 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
       Eop Osub (e1:::e2:::Enil)
   end.
 
-Definition negint (e: expr) := Eop (Osubimm Int.zero) (e ::: Enil).
+Definition negint (e: expr) := subimm Int.zero e.
 
 (** ** Rotates and immediate shifts *)
 
@@ -174,8 +187,12 @@ Definition shruimm (e1: expr) (n2: int) :=
 Nondetfunction shrimm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then
     e1
+  else if negb (Int.ltu n2 Int.iwordsize) then
+    Eop Oshr (e1:::Eop (Ointconst n2) Enil:::Enil)
   else
     match e1 with
+    | Eop (Ointconst n1) Enil =>
+        Eop (Ointconst (Int.shr n1 n2)) Enil
     | Eop (Oandimm mask1) (t1:::Enil) =>
         if Int.lt mask1 Int.zero
         then Eop (Oshrimm n2) (e1:::Enil)
@@ -293,9 +310,11 @@ Nondetfunction or (e1: expr) (e2: expr) :=
 
 Nondetfunction xorimm (n1: int) (e2: expr) :=
   if Int.eq n1 Int.zero then e2 else
+  if Int.eq n1 Int.mone then notint e2 else
   match e2 with
   | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
   | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+  | Eop Onot (t2:::Enil) => Eop (Oxorimm (Int.not n1)) (t2:::Enil)
   | _ => Eop (Oxorimm n1) (e2:::Enil)
   end.
 
@@ -418,11 +437,19 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
 
 Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
 
-Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
+Nondetfunction cast8signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
+  | _ => Eop Ocast8signed (e ::: Enil)
+  end.
 
 Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
 
-Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
+Nondetfunction cast16signed (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
+  | _ => Eop Ocast16signed (e ::: Enil)
+  end.
 
 (** ** Floating-point conversions *)
 
@@ -435,14 +462,24 @@ Definition intuoffloat (e: expr) :=
       (intoffloat (Eletvar 1))
       (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
-Definition floatofintu (e: expr) :=
-  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
-       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
+Nondetfunction floatofintu (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ofloatconst (Float.floatofintu n)) Enil
+  | _ =>
+      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
+           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
+  end.
 
-Definition floatofint (e: expr) :=
-  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
-                           ::: addimm Float.ox8000_0000 e ::: Enil))
-       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
+Nondetfunction floatofint (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ofloatconst (Float.floatofint n)) Enil
+  | _ =>
+      subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
+                               ::: addimm Float.ox8000_0000 e ::: Enil))
+           (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
+  end.
 
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 4d26cf6..b6412c0 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -150,6 +150,7 @@ Proof.
   subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. 
     destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive.
     rewrite Int.and_commut. auto.
+  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. auto.
   TrivialExists. 
 Qed.
 
@@ -218,11 +219,23 @@ Proof.
 - TrivialExists. 
 Qed.
 
+Theorem eval_subimm:
+  forall n, unary_constructor_sound (subimm n) (fun v => Val.sub (Vint n) v).
+Proof.
+  intros; red; intros until x. unfold subimm. destruct (subimm_match a); intros.
+  InvEval. TrivialExists. 
+  InvEval. subst x. TrivialExists. unfold eval_operation. destruct v1; simpl; auto.
+  rewrite ! Int.sub_add_opp. rewrite Int.add_assoc. f_equal. f_equal. f_equal.
+  rewrite Int.neg_add_distr.  apply Int.add_commut.
+  TrivialExists.
+Qed.
+
 Theorem eval_sub: binary_constructor_sound sub Val.sub.
 Proof.
   red; intros until y.
   unfold sub; case (sub_match a b); intros; InvEval.
   rewrite Val.sub_add_opp. apply eval_addimm; auto.
+  apply eval_subimm; auto.
   subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. 
     rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
     apply eval_addimm; EvalOp.
@@ -233,7 +246,7 @@ Qed.
 
 Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
 Proof.
-  red; intros. unfold negint. TrivialExists.
+  red; intros. unfold negint. apply eval_subimm; auto. 
 Qed.
 
 Lemma eval_rolm:
@@ -280,15 +293,19 @@ Proof.
   red; intros until x. unfold shrimm. 
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
+  destruct (Int.ltu n Int.iwordsize) eqn:WS.
   case (shrimm_match a); intros.
-  destruct (Int.lt mask1 Int.zero) eqn:?. 
+  InvEval. exists (Vint (Int.shr n1 n)); split. EvalOp. simpl; rewrite WS; auto.
+  simpl; destruct (Int.lt mask1 Int.zero) eqn:?. 
   TrivialExists.
   replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). 
   apply eval_shruimm; auto.
-  destruct x; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. 
+  destruct x; simpl; auto. rewrite WS.
   decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. 
   apply Int.shr_and_is_shru_and; auto.
-  TrivialExists.
+  simpl. TrivialExists.
+  intros. simpl. TrivialExists.
+  constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
 Lemma eval_mulimm_base:
@@ -475,7 +492,9 @@ Proof.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.xor_zero; auto.
   clear H. destruct (xorimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.xor_commut; auto.
-  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. 
+  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
+  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. 
+  simpl. rewrite Int.xor_commut; auto.
   TrivialExists.
 Qed.
 
@@ -735,7 +754,9 @@ Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
-  red; intros. unfold cast8signed. TrivialExists.
+  red; intros until x. unfold cast8signed. destruct (cast8signed_match a); intros.
+  InvEval; TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
@@ -746,7 +767,9 @@ Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
 Proof.
-  red; intros. unfold cast16signed. TrivialExists.
+  red; intros until x. unfold cast16signed. destruct (cast16signed_match a); intros.
+  InvEval; TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
@@ -813,9 +836,10 @@ Theorem eval_floatofint:
   Val.floatofint x = Some y ->
   exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
 Proof.
-  intros. destruct x; simpl in H0; inv H0.
+  intros until y. unfold floatofint. destruct (floatofint_match a); intros.
+  InvEval. TrivialExists. 
+  rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.floatofint i)); split; auto.
-  unfold floatofint.
   set (t1 := addimm Float.ox8000_0000 a).
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
@@ -834,7 +858,9 @@ Theorem eval_floatofintu:
   Val.floatofintu x = Some y ->
   exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
 Proof.
-  intros. destruct x; simpl in H0; inv H0.
+  intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
+  InvEval. TrivialExists.
+  rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.floatofintu i)); split; auto.
   unfold floatofintu.
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
-- 
cgit v1.2.3