Refactoring of Constprop and Constpropproof into a machine-dependent part and a machine-independent part.

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

8 files changed, 776 insertions, 1327 deletions

diff --git a/.depend b/.depend
index 8680078..9edeabd 100644
--- a/.depend
+++ b/.depend
@@ -25,8 +25,8 @@ $(ARCH)/Asmgenproof.vo: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/E
 $(ARCH)/Asmgenretaddr.vo: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo
 $(ARCH)/Asmgen.vo: $(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/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
 $(ARCH)/Asm.vo: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Conventions.vo
-$(ARCH)/Constpropproof.vo: $(ARCH)/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/Constprop.vo
-$(ARCH)/Constprop.vo: $(ARCH)/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)/ConstpropOpproof.vo: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo
+$(ARCH)/ConstpropOp.vo: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo
 $(ARCH)/Machregs.vo: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo
 $(ARCH)/Op.vo: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo
 $(ARCH)/SelectOpproof.vo: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
@@ -39,6 +39,8 @@ backend/CminorSel.vo: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.v
 backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo
 backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo
 backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/InterfGraph.vo
+backend/Constpropproof.vo: 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/Mem.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/Constprop.vo: 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
 backend/CSEproof.vo: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo
 backend/CSE.vo: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo
 backend/InterfGraph.vo: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo
@@ -88,5 +90,5 @@ cfrontend/Cshmgenproof3.vo: cfrontend/Cshmgenproof3.v lib/Coqlib.vo common/Error
 cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo backend/Cminor.vo cfrontend/Csharpminor.vo
 cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo
 cfrontend/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo cfrontend/Csyntax.vo
-driver/Compiler.vo: driver/Compiler.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo $(ARCH)/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/Ctyping.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cshmgenproof3.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo $(ARCH)/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo
+driver/Compiler.vo: driver/Compiler.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/Ctyping.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cshmgenproof3.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo
 driver/Complements.vo: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
diff --git a/Makefile b/Makefile
index cba86c6..e82d205 100644
--- a/Makefile
+++ b/Makefile
@@ -53,7 +53,7 @@ BACKEND=\
   Tailcall.v Tailcallproof.v \
   RTLtyping.v \
   Kildall.v \
-  Constprop.v Constpropproof.v \
+  ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
   CSE.v CSEproof.v \
   Machregs.v Locations.v Conventions.v LTL.v LTLtyping.v \
   InterfGraph.v Coloring.v Coloringproof.v \
diff --git a/arm/Constprop.v b/arm/ConstpropOp.v
index 154a5fc..b5e5a03 100644
--- a/arm/Constprop.v
+++ b/arm/ConstpropOp.v
@@ -10,22 +10,16 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Constant propagation over RTL.  This is the first of the two
-  optimizations performed at RTL level.  It proceeds by a standard
-  dataflow analysis and the corresponding code transformation. *)
+(** Static analysis and strength reduction for operators 
+  and conditions.  This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
-Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
 
 (** * Static analysis *)
 
@@ -42,77 +36,6 @@ Inductive approx : Type :=
                          (** The value is the address of the given global
                              symbol plus the given integer offset. *)
 
-(** We equip this set of approximations with a semi-lattice structure.
-  The ordering is inclusion between the sets of values denoted by
-  the approximations. *)
-
-Module Approx <: SEMILATTICE_WITH_TOP.
-  Definition t := approx.
-  Definition eq (x y: t) := (x = y).
-  Definition eq_refl: forall x, eq x x := (@refl_equal t).
-  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
-  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
-  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
-  Proof.
-    decide equality.
-    apply Int.eq_dec.
-    apply Float.eq_dec.
-    apply Int.eq_dec.
-    apply ident_eq.
-  Qed.
-  Definition beq (x y: t) := if eq_dec x y then true else false.
-  Lemma beq_correct: forall x y, beq x y = true -> x = y.
-  Proof.
-    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
-  Qed.
-  Definition ge (x y: t) : Prop :=
-    x = Unknown \/ y = Novalue \/ x = y.
-  Lemma ge_refl: forall x y, eq x y -> ge x y.
-  Proof.
-    unfold eq, ge; tauto.
-  Qed.
-  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
-  Proof.
-    unfold ge; intuition congruence.
-  Qed.
-  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-  Proof.
-    unfold eq, ge; intros; congruence.
-  Qed.
-  Definition bot := Novalue.
-  Definition top := Unknown.
-  Lemma ge_bot: forall x, ge x bot.
-  Proof.
-    unfold ge, bot; tauto.
-  Qed.
-  Lemma ge_top: forall x, ge top x.
-  Proof.
-    unfold ge, bot; tauto.
-  Qed.
-  Definition lub (x y: t) : t :=
-    if eq_dec x y then x else
-    match x, y with
-    | Novalue, _ => y
-    | _, Novalue => x
-    | _, _ => Unknown
-    end.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
-  Proof.
-    unfold lub, eq; intros.
-    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
-    destruct x; destruct y; auto.
-  Qed.
-  Lemma ge_lub_left: forall x y, ge (lub x y) x.
-  Proof.
-    unfold lub; intros.
-    case (eq_dec x y); intro.
-    apply ge_refl. apply eq_refl.
-    destruct x; destruct y; unfold ge; tauto.
-  Qed.
-End Approx.
-
-Module D := LPMap Approx.
-
 (** We now define the abstract interpretations of conditions and operators
   over this set of approximations.  For instance, the abstract interpretation
   of the operator [Oaddf] applied to two expressions [a] and [b] is
@@ -658,59 +581,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       Unknown
   end.
 
-
-(** The transfer function for the dataflow analysis is straightforward:
-  for [Iop] instructions, we set the approximation of the destination
-  register to the result of executing abstractly the operation;
-  for [Iload] and [Icall], we set the approximation of the destination
-  to [Unknown]. *)
-
-Definition approx_regs (rl: list reg) (approx: D.t) :=
-  List.map (fun r => D.get r approx) rl.
-
-Definition transfer (f: function) (pc: node) (before: D.t) :=
-  match f.(fn_code)!pc with
-  | None => before
-  | Some i =>
-      match i with
-      | Inop s =>
-          before
-      | Iop op args res s =>
-          let a := eval_static_operation op (approx_regs args before) in
-          D.set res a before
-      | Iload chunk addr args dst s =>
-          D.set dst Unknown before
-      | Istore chunk addr args src s =>
-          before
-      | Icall sig ros args res s =>
-          D.set res Unknown before
-      | Itailcall sig ros args =>
-          before
-      | Icond cond args ifso ifnot =>
-          before
-      | Ireturn optarg =>
-          before
-      end
-  end.
-
-(** The static analysis itself is then an instantiation of Kildall's
-  generic solver for forward dataflow inequations. [analyze f]
-  returns a mapping from program points to mappings of pseudo-registers
-  to approximations.  It can fail to reach a fixpoint in a reasonable
-  number of iterations, in which case [None] is returned. *)
-
-Module DS := Dataflow_Solver(D)(NodeSetForward).
-
-Definition analyze (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) (transfer f) 
-                    ((f.(fn_entrypoint), D.top) :: nil) with
-  | None => PMap.init D.top
-  | Some res => res
-  end.
-
-(** * Code transformation *)
-
-(** ** Operator strength reduction *)
+(** * Operator strength reduction *)
 
 (** We now define auxiliary functions for strength reduction of
   operators and addressing modes: replacing an operator with a cheaper
@@ -719,10 +590,10 @@ Definition analyze (f: RTL.function): PMap.t D.t :=
 
 Section STRENGTH_REDUCTION.
 
-Variable approx: D.t.
+Variable app: reg -> approx.
 
 Definition intval (r: reg) : option int :=
-  match D.get r approx with I n => Some n | _ => None end.
+  match app r with I n => Some n | _ => None end.
 
 (*
 Definition cond_strength_reduction (cond: condition) (args: list reg) :=
@@ -1159,77 +1030,3 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) :=
   end.
 
 End STRENGTH_REDUCTION.
-
-(** ** Code transformation *)
-
-(** The code transformation proceeds instruction by instruction.
-    Operators whose arguments are all statically known are turned
-    into ``load integer constant'', ``load float constant'' or
-    ``load symbol address'' operations.  Operators for which some
-    but not all arguments are known are subject to strength reduction,
-    and similarly for the addressing modes of load and store instructions.
-    Other instructions are unchanged. *)
-
-Definition transf_ros (approx: D.t) (ros: reg + ident) : reg + ident :=
-  match ros with
-  | inl r =>
-      match D.get r approx with
-      | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
-      | _ => ros
-      end
-  | inr s => ros
-  end.
-
-Definition transf_instr (approx: D.t) (instr: instruction) :=
-  match instr with
-  | Iop op args res s =>
-      match eval_static_operation op (approx_regs args approx) with
-      | I n =>
-          Iop (Ointconst n) nil res s
-      | F n =>
-          Iop (Ofloatconst n) nil res s
-      | S symb ofs =>
-          Iop (Oaddrsymbol symb ofs) nil res s
-      | _ =>
-          let (op', args') := op_strength_reduction approx op args in
-          Iop op' args' res s
-      end
-  | Iload chunk addr args dst s =>
-      let (addr', args') := addr_strength_reduction approx addr args in
-      Iload chunk addr' args' dst s      
-  | Istore chunk addr args src s =>
-      let (addr', args') := addr_strength_reduction approx addr args in
-      Istore chunk addr' args' src s      
-  | Icall sig ros args res s =>
-      Icall sig (transf_ros approx ros) args res s
-  | Itailcall sig ros args =>
-      Itailcall sig (transf_ros approx ros) args
-  | Icond cond args s1 s2 =>
-      match eval_static_condition cond (approx_regs args approx) with
-      | Some b =>
-          if b then Inop s1 else Inop s2
-      | None =>
-          let (cond', args') := cond_strength_reduction approx cond args in
-          Icond cond' args' s1 s2
-      end
-  | _ =>
-      instr
-  end.
-
-Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
-  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
-
-Definition transf_function (f: function) : function :=
-  let approxs := analyze f in
-  mkfunction
-    f.(fn_sig)
-    f.(fn_params)
-    f.(fn_stacksize)
-    (transf_code approxs f.(fn_code))
-    f.(fn_entrypoint).
-
-Definition transf_fundef (fd: fundef) : fundef :=
-  AST.transf_fundef transf_function fd.
-
-Definition transf_program (p: program) : program :=
-  transform_program transf_fundef p.
diff --git a/arm/Constpropproof.v b/arm/ConstpropOpproof.v
index a3e2b82..70fc606 100644
--- a/arm/Constpropproof.v
+++ b/arm/ConstpropOpproof.v
@@ -10,23 +10,19 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Correctness proof for constant propagation. *)
+(** Correctness proof for constant propagation (processor-dependent part). *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Events.
 Require Import Mem.
 Require Import Globalenvs.
-Require Import Smallstep.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
+Require Import ConstpropOp.
 Require Import Constprop.
 
 (** * Correctness of the static analysis *)
@@ -51,16 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop :=
   | _ => False
   end.
 
-Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
-  forall r, val_match_approx (D.get r a) rs#r.
-
-Lemma regs_match_approx_top:
-  forall rs, regs_match_approx D.top rs.
-Proof.
-  intros. red; intros. simpl. rewrite PTree.gempty. 
-  unfold Approx.top, val_match_approx. auto.
-Qed.
-
 Lemma val_match_approx_increasing:
   forall a1 a2 v,
   Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v.
@@ -72,26 +58,6 @@ Proof.
   subst a2. auto.
 Qed.
 
-Lemma regs_match_approx_increasing:
-  forall a1 a2 rs,
-  D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.
-Proof.
-  unfold D.ge, regs_match_approx. intros.
-  apply val_match_approx_increasing with (D.get r a2); auto.
-Qed.
-
-Lemma regs_match_approx_update:
-  forall ra rs a v r,
-  val_match_approx a v ->
-  regs_match_approx ra rs ->
-  regs_match_approx (D.set r a ra) (rs#r <- v).
-Proof.
-  intros; red; intros. rewrite Regmap.gsspec. 
-  case (peq r0 r); intro.
-  subst r0. rewrite D.gss. auto.
-  rewrite D.gso; auto. 
-Qed.
-
 Inductive val_list_match_approx: list approx -> list val -> Prop :=
   | vlma_nil:
       val_list_match_approx nil nil
@@ -101,16 +67,6 @@ Inductive val_list_match_approx: list approx -> list val -> Prop :=
       val_list_match_approx al vl ->
       val_list_match_approx (a :: al) (v :: vl).
 
-Lemma approx_regs_val_list:
-  forall ra rs rl,
-  regs_match_approx ra rs ->
-  val_list_match_approx (approx_regs rl ra) rs##rl.
-Proof.
-  induction rl; simpl; intros.
-  constructor.
-  constructor. apply H. auto.
-Qed.
-
 Ltac SimplVMA :=
   match goal with
   | H: (val_match_approx (I _) ?v) |- _ =>
@@ -208,42 +164,6 @@ Proof.
   auto.
 Qed.
 
-(** The correctness of the static analysis follows from the results
-  above and the fact that the result of the static analysis is
-  a solution of the forward dataflow inequations. *)
-
-Lemma analyze_correct_1:
-  forall f pc rs pc' i,
-  f.(fn_code)!pc = Some i ->
-  In pc' (successors_instr i) ->
-  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
-  regs_match_approx (analyze f)!!pc' rs.
-Proof.
-  intros until i. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
-                      ((fn_entrypoint f, D.top) :: nil)).
-  intros approxs; intros.
-  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
-  eapply DS.fixpoint_solution; eauto.
-  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
-  auto.
-  intros. rewrite PMap.gi. apply regs_match_approx_top. 
-Qed.
-
-Lemma analyze_correct_3:
-  forall f rs,
-  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
-Proof.
-  intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
-                      ((fn_entrypoint f, D.top) :: nil)).
-  intros approxs; intros.
-  apply regs_match_approx_increasing with D.top.
-  eapply DS.fixpoint_entry; eauto. auto with coqlib.
-  apply regs_match_approx_top. 
-  intros. rewrite PMap.gi. apply regs_match_approx_top.
-Qed.
-
 (** * Correctness of strength reduction *)
 
 (** We now show that strength reduction over operators and addressing
@@ -254,49 +174,49 @@ Qed.
 
 Section STRENGTH_REDUCTION.
 
-Variable approx: D.t.
+Variable app: reg -> approx.
 Variable sp: val.
 Variable rs: regset.
-Hypothesis MATCH: regs_match_approx approx rs.
+Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.
 
 Lemma intval_correct:
   forall r n,
-  intval approx r = Some n -> rs#r = Vint n.
+  intval app r = Some n -> rs#r = Vint n.
 Proof.
   intros until n.
-  unfold intval. caseEq (D.get r approx); intros; try discriminate.
+  unfold intval. caseEq (app r); intros; try discriminate.
   generalize (MATCH r). unfold val_match_approx. rewrite H.
   congruence. 
 Qed.
 
 Lemma cond_strength_reduction_correct:
   forall cond args,
-  let (cond', args') := cond_strength_reduction approx cond args in
+  let (cond', args') := cond_strength_reduction app cond args in
   eval_condition cond' rs##args' = eval_condition cond rs##args.
 Proof.
   intros. unfold cond_strength_reduction.
   case (cond_strength_reduction_match cond args); intros.
 
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmp. auto.
   destruct c; reflexivity.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
 
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
 
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H). auto.
   auto.
 
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H). auto.
   auto.
 
@@ -424,24 +344,24 @@ Qed.
 
 Lemma op_strength_reduction_correct:
   forall op args v,
-  let (op', args') := op_strength_reduction approx op args in
+  let (op', args') := op_strength_reduction app op args in
   eval_operation ge sp op rs##args = Some v ->
   eval_operation ge sp op' rs##args' = Some v.
 Proof.
   intros; unfold op_strength_reduction;
   case (op_strength_reduction_match op args); intros; simpl List.map.
   (* Oadd *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)).
   apply make_addimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_addimm_correct.
   assumption.
   (* Oaddshift *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)).
@@ -449,10 +369,10 @@ Proof.
   simpl. destruct rs#r1; auto.
   assumption.
   (* Osub *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H) in H0.
   simpl in *. destruct rs#r2; auto. 
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0).
   replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)).
@@ -460,7 +380,7 @@ Proof.
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
   assumption.
   (* Osubshift *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)).
@@ -468,23 +388,23 @@ Proof.
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
   assumption.
   (* Orsubshift *)
-  caseEq (intval approx r2). intros n H.
+  caseEq (intval app r2). intros n H.
   rewrite (intval_correct _ _ H).
   simpl. destruct rs#r1; auto. 
   auto.
   (* Omul *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)).
   apply make_mulimm_correct. apply intval_correct; auto. 
   simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_mulimm_correct.
   apply intval_correct; auto.
   assumption.
   (* Odivu *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.is_power2 i); intros.
   rewrite (intval_correct _ _ H).
   replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil))
@@ -499,107 +419,99 @@ Proof.
   assumption.
   assumption.
   (* Oand *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)).
   apply make_andimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_andimm_correct.
   assumption.
   (* Oandshift *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Oor *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)).
   apply make_orimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_orimm_correct.
   assumption.
   (* Oorshift *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)).
   apply make_orimm_correct. reflexivity.
   assumption.
   (* Oxor *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)).
   apply make_xorimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_xorimm_correct.
   assumption.
   (* Oxorshift *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)).
   apply make_xorimm_correct. reflexivity.
   assumption.
   (* Obic *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Obicshift *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Oshl *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.ltu i (Int.repr 32)); intros.
   rewrite (intval_correct _ _ H). apply make_shlimm_correct.
   assumption.
   assumption.
   (* Oshr *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.ltu i (Int.repr 32)); intros.
   rewrite (intval_correct _ _ H). apply make_shrimm_correct.
   assumption.
   assumption.
   (* Oshru *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.ltu i (Int.repr 32)); intros.
   rewrite (intval_correct _ _ H). apply make_shruimm_correct.
   assumption.
   assumption.
   (* Ocmp *)
   generalize (cond_strength_reduction_correct c rl).
-  destruct (cond_strength_reduction approx c rl).
+  destruct (cond_strength_reduction app c rl).
   simpl. intro. rewrite H. auto.
   (* default *)
   assumption.
 Qed.
-
-Ltac KnownApprox :=
-  match goal with
-  | MATCH: (regs_match_approx ?approx ?rs),
-    H: (D.get ?r ?approx = ?a) |- _ =>
-      generalize (MATCH r); rewrite H; intro; clear H; KnownApprox
-  | _ => idtac
-  end.
  
 Lemma addr_strength_reduction_correct:
   forall addr args,
-  let (addr', args') := addr_strength_reduction approx addr args in
+  let (addr', args') := addr_strength_reduction app addr args in
   eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.
 Proof.
   intros. 
@@ -608,15 +520,15 @@ Proof.
   case (addr_strength_reduction_match addr args); intros.
 
   (* Aindexed2 *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   simpl; rewrite (intval_correct _ _ H).
   destruct rs#r2; auto. rewrite Int.add_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl; rewrite (intval_correct _ _ H0). auto.
   auto.
 
   (* Aindexed2shift *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl; rewrite (intval_correct _ _ H). auto.
   auto.
 
@@ -627,331 +539,3 @@ Qed.
 End STRENGTH_REDUCTION.
 
 End ANALYSIS.
-
-(** * Correctness of the code transformation *)
-
-(** We now show that the transformed code after constant propagation
-  has the same semantics as the original code. *)
-
-Section PRESERVATION.
-
-Variable prog: program.
-Let tprog := transf_program prog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-Lemma symbols_preserved:
-  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros; unfold ge, tge, tprog, transf_program. 
-  apply Genv.find_symbol_transf.
-Qed.
-
-Lemma functions_translated:
-  forall (v: val) (f: fundef),
-  Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef f).
-Proof.  
-  intros.
-  exact (Genv.find_funct_transf transf_fundef H).
-Qed.
-
-Lemma function_ptr_translated:
-  forall (b: block) (f: fundef),
-  Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (transf_fundef f).
-Proof.  
-  intros. 
-  exact (Genv.find_funct_ptr_transf transf_fundef H).
-Qed.
-
-Lemma sig_function_translated:
-  forall f,
-  funsig (transf_fundef f) = funsig f.
-Proof.
-  intros. destruct f; reflexivity.
-Qed.
-
-Lemma transf_ros_correct:
-  forall ros rs f approx,
-  regs_match_approx ge approx rs ->
-  find_function ge ros rs = Some f ->
-  find_function tge (transf_ros approx ros) rs = Some (transf_fundef f).
-Proof.
-  intros until approx; intro MATCH.
-  destruct ros; simpl.
-  intro.
-  exploit functions_translated; eauto. intro FIND.  
-  caseEq (D.get r approx); intros; auto.
-  generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto.
-  generalize (MATCH r). rewrite H0. intros [b [A B]].
-  rewrite <- symbols_preserved in A.
-  rewrite B in FIND. rewrite H1 in FIND. 
-  rewrite Genv.find_funct_find_funct_ptr in FIND.
-  simpl. rewrite A. auto.
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
-  intro. apply function_ptr_translated. auto.
-  congruence.
-Qed.
-
-(** The proof of semantic preservation is a simulation argument
-  based on diagrams of the following form:
-<<
-           st1 --------------- st2
-            |                   |
-           t|                   |t
-            |                   |
-            v                   v
-           st1'--------------- st2'
->>
-  The left vertical arrow represents a transition in the
-  original RTL code.  The top horizontal bar is the [match_states]
-  invariant between the initial state [st1] in the original RTL code
-  and an initial state [st2] in the transformed code.
-  This invariant expresses that all code fragments appearing in [st2]
-  are obtained by [transf_code] transformation of the corresponding
-  fragments in [st1].  Moreover, the values of registers in [st1]
-  must match their compile-time approximations at the current program
-  point.
-  These two parts of the diagram are the hypotheses.  In conclusions,
-  we want to prove the other two parts: the right vertical arrow,
-  which is a transition in the transformed RTL code, and the bottom
-  horizontal bar, which means that the [match_state] predicate holds
-  between the final states [st1'] and [st2']. *)
-
-Inductive match_stackframes: stackframe -> stackframe -> Prop :=
-   match_stackframe_intro:
-      forall res c sp pc rs f,
-      c = f.(RTL.fn_code) ->
-      (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) ->
-    match_stackframes
-        (Stackframe res c sp pc rs)
-        (Stackframe res (transf_code (analyze f) c) sp pc rs).
-
-Inductive match_states: state -> state -> Prop :=
-  | match_states_intro:
-      forall s c sp pc rs m f s'
-           (CF: c = f.(RTL.fn_code))
-           (MATCH: regs_match_approx ge (analyze f)!!pc rs)
-           (STACKS: list_forall2 match_stackframes s s'),
-      match_states (State s c sp pc rs m)
-                   (State s' (transf_code (analyze f) c) sp pc rs m)
-  | match_states_call:
-      forall s f args m s',
-      list_forall2 match_stackframes s s' ->
-      match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef f) args m)
-  | match_states_return:
-      forall s s' v m,
-      list_forall2 match_stackframes s s' ->
-      match_states (Returnstate s v m)
-                   (Returnstate s' v m).
-
-Ltac TransfInstr :=
-  match goal with
-  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr));
-      [ simpl
-      | unfold transf_code; rewrite PTree.gmap; 
-        unfold option_map; rewrite H1; reflexivity ]
-  end.
-
-(** The proof of simulation proceeds by case analysis on the transition
-  taken in the source code. *)
-
-Lemma transf_step_correct:
-  forall s1 t s2,
-  step ge s1 t s2 ->
-  forall s1' (MS: match_states s1 s1'),
-  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
-Proof.
-  induction 1; intros; inv MS.
-
-  (* Inop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
-  TransfInstr; intro. eapply exec_Inop; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1 with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. auto.
-
-  (* Iop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
-  TransfInstr. caseEq (op_strength_reduction (analyze f)!!pc op args);
-  intros op' args' OSR.
-  assert (eval_operation tge sp op' rs##args' = Some v).
-    rewrite (eval_operation_preserved symbols_preserved). 
-    generalize (op_strength_reduction_correct ge (analyze f)!!pc sp rs
-                  MATCH op args v).
-    rewrite OSR; simpl. auto.
-  generalize (eval_static_operation_correct ge op sp
-               (approx_regs args (analyze f)!!pc) rs##args v
-               (approx_regs_val_list _ _ _ args MATCH) H0).
-  case (eval_static_operation op (approx_regs args (analyze f)!!pc)); intros;
-  simpl in H2;
-  eapply exec_Iop; eauto; simpl.
-  congruence.
-  congruence.
-  elim H2; intros b [A B]. rewrite symbols_preserved. 
-  rewrite A; rewrite B; auto.
-  econstructor; eauto. 
-  eapply analyze_correct_1 with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. 
-  eapply eval_static_operation_correct; eauto.
-  apply approx_regs_val_list; auto.
-
-  (* Iload *)
-  caseEq (addr_strength_reduction (analyze f)!!pc addr args);
-  intros addr' args' ASR.
-  assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved symbols_preserved). 
-    generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs
-                  MATCH addr args).
-    rewrite ASR; simpl. congruence. 
-  TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
-  eapply exec_Iload; eauto.
-  econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. simpl; auto.
-
-  (* Istore *)
-  caseEq (addr_strength_reduction (analyze f)!!pc addr args);
-  intros addr' args' ASR.
-  assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved symbols_preserved). 
-    generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs
-                  MATCH addr args).
-    rewrite ASR; simpl. congruence. 
-  TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
-  eapply exec_Istore; eauto.
-  econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. auto. 
-
-  (* Icall *)
-  exploit transf_ros_correct; eauto. intro FIND'.
-  TransfInstr; intro.
-  econstructor; split.
-  eapply exec_Icall; eauto. apply sig_function_translated; auto.
-  constructor; auto. constructor; auto.
-  econstructor; eauto. 
-  intros. eapply analyze_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H.
-  apply regs_match_approx_update; auto. simpl. auto.
-
-  (* Itailcall *)
-  exploit transf_ros_correct; eauto. intros FIND'.
-  TransfInstr; intro.
-  econstructor; split.
-  eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
-  constructor; auto. 
-
-  (* Icond, true *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. 
-  caseEq (cond_strength_reduction (analyze f)!!pc cond args);
-  intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' = Some true).
-    generalize (cond_strength_reduction_correct
-                  ge (analyze f)!!pc rs MATCH cond args).
-    rewrite CSR.  intro. congruence.
-  TransfInstr. rewrite CSR. 
-  caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)).
-  intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ _
-               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
-  replace b with true. intro; eapply exec_Inop; eauto. congruence.
-  intros. eapply exec_Icond_true; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Icond, false *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. 
-  caseEq (cond_strength_reduction (analyze f)!!pc cond args);
-  intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' = Some false).
-    generalize (cond_strength_reduction_correct
-                  ge (analyze f)!!pc rs MATCH cond args).
-    rewrite CSR.  intro. congruence.
-  TransfInstr. rewrite CSR. 
-  caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)).
-  intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ _
-               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
-  replace b with false. intro; eapply exec_Inop; eauto. congruence.
-  intros. eapply exec_Icond_false; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Ireturn *)
-  exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split.
-  eapply exec_Ireturn; eauto. TransfInstr; auto.
-  constructor; auto.
-
-  (* internal function *)
-  simpl. unfold transf_function.
-  econstructor; split.
-  eapply exec_function_internal; simpl; eauto.
-  simpl. econstructor; eauto.
-  apply analyze_correct_3; auto.
-
-  (* external function *)
-  simpl. econstructor; split.
-  eapply exec_function_external; eauto.
-  constructor; auto.
-
-  (* return *)
-  inv H3. inv H1. 
-  econstructor; split.
-  eapply exec_return; eauto. 
-  econstructor; eauto. 
-Qed.
-
-Lemma transf_initial_states:
-  forall st1, initial_state prog st1 ->
-  exists st2, initial_state tprog st2 /\ match_states st1 st2.
-Proof.
-  intros. inversion H.
-  exploit function_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split.
-  econstructor; eauto.
-  replace (prog_main tprog) with (prog_main prog).
-  rewrite symbols_preserved. eauto.
-  reflexivity.
-  rewrite <- H2. apply sig_function_translated.
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
-  constructor. constructor. auto.
-  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. 
-Qed.
-
-Lemma transf_final_states:
-  forall st1 st2 r, 
-  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
-Proof.
-  intros. inv H0. inv H. inv H4. constructor. 
-Qed.
-
-(** The preservation of the observable behavior of the program then
-  follows, using the generic preservation theorem
-  [Smallstep.simulation_step_preservation]. *)
-
-Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> exec_program tprog beh.
-Proof.
-  unfold exec_program; intros.
-  eapply simulation_step_preservation; eauto.
-  eexact transf_initial_states.
-  eexact transf_final_states.
-  exact transf_step_correct. 
-Qed.
-
-End PRESERVATION.
diff --git a/backend/Constprop.v b/backend/Constprop.v
new file mode 100644
index 0000000..cccce9a
--- /dev/null
+++ b/backend/Constprop.v
@@ -0,0 +1,235 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Constant propagation over RTL.  This is one of the optimizations
+  performed at RTL level.  It proceeds by a standard dataflow analysis
+  and the corresponding code rewriting. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Lattice.
+Require Import Kildall.
+Require Import ConstpropOp.
+
+(** * Static analysis *)
+
+(** The type [approx] of compile-time approximations of values is
+  defined in the machine-dependent part [ConstpropOp]. *)
+
+(** We equip this type of approximations with a semi-lattice structure.
+  The ordering is inclusion between the sets of values denoted by
+  the approximations. *)
+
+Module Approx <: SEMILATTICE_WITH_TOP.
+  Definition t := approx.
+  Definition eq (x y: t) := (x = y).
+  Definition eq_refl: forall x, eq x x := (@refl_equal t).
+  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
+  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
+  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
+  Proof.
+    decide equality.
+    apply Int.eq_dec.
+    apply Float.eq_dec.
+    apply Int.eq_dec.
+    apply ident_eq.
+  Qed.
+  Definition beq (x y: t) := if eq_dec x y then true else false.
+  Lemma beq_correct: forall x y, beq x y = true -> x = y.
+  Proof.
+    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
+  Qed.
+  Definition ge (x y: t) : Prop :=
+    x = Unknown \/ y = Novalue \/ x = y.
+  Lemma ge_refl: forall x y, eq x y -> ge x y.
+  Proof.
+    unfold eq, ge; tauto.
+  Qed.
+  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Proof.
+    unfold ge; intuition congruence.
+  Qed.
+  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
+  Proof.
+    unfold eq, ge; intros; congruence.
+  Qed.
+  Definition bot := Novalue.
+  Definition top := Unknown.
+  Lemma ge_bot: forall x, ge x bot.
+  Proof.
+    unfold ge, bot; tauto.
+  Qed.
+  Lemma ge_top: forall x, ge top x.
+  Proof.
+    unfold ge, bot; tauto.
+  Qed.
+  Definition lub (x y: t) : t :=
+    if eq_dec x y then x else
+    match x, y with
+    | Novalue, _ => y
+    | _, Novalue => x
+    | _, _ => Unknown
+    end.
+  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
+  Proof.
+    unfold lub, eq; intros.
+    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
+    destruct x; destruct y; auto.
+  Qed.
+  Lemma ge_lub_left: forall x y, ge (lub x y) x.
+  Proof.
+    unfold lub; intros.
+    case (eq_dec x y); intro.
+    apply ge_refl. apply eq_refl.
+    destruct x; destruct y; unfold ge; tauto.
+  Qed.
+End Approx.
+
+Module D := LPMap Approx.
+
+(** The transfer function for the dataflow analysis is straightforward:
+  for [Iop] instructions, we set the approximation of the destination
+  register to the result of executing abstractly the operation;
+  for [Iload] and [Icall], we set the approximation of the destination
+  to [Unknown]. *)
+
+Definition approx_reg (app: D.t) (r: reg) := 
+  D.get r app.
+
+Definition approx_regs (app: D.t) (rl: list reg):=
+  List.map (approx_reg app) rl.
+
+Definition transfer (f: function) (pc: node) (before: D.t) :=
+  match f.(fn_code)!pc with
+  | None => before
+  | Some i =>
+      match i with
+      | Inop s =>
+          before
+      | Iop op args res s =>
+          let a := eval_static_operation op (approx_regs before args) in
+          D.set res a before
+      | Iload chunk addr args dst s =>
+          D.set dst Unknown before
+      | Istore chunk addr args src s =>
+          before
+      | Icall sig ros args res s =>
+          D.set res Unknown before
+      | Itailcall sig ros args =>
+          before
+(*
+      | Ialloc arg res s =>
+          D.set res Unknown before
+*)
+      | Icond cond args ifso ifnot =>
+          before
+      | Ireturn optarg =>
+          before
+      end
+  end.
+
+(** The static analysis itself is then an instantiation of Kildall's
+  generic solver for forward dataflow inequations. [analyze f]
+  returns a mapping from program points to mappings of pseudo-registers
+  to approximations.  It can fail to reach a fixpoint in a reasonable
+  number of iterations, in which case [None] is returned. *)
+
+Module DS := Dataflow_Solver(D)(NodeSetForward).
+
+Definition analyze (f: RTL.function): PMap.t D.t :=
+  match DS.fixpoint (successors f) (transfer f) 
+                    ((f.(fn_entrypoint), D.top) :: nil) with
+  | None => PMap.init D.top
+  | Some res => res
+  end.
+
+(** * Code transformation *)
+
+(** The code transformation proceeds instruction by instruction.
+    Operators whose arguments are all statically known are turned
+    into ``load integer constant'', ``load float constant'' or
+    ``load symbol address'' operations.  Operators for which some
+    but not all arguments are known are subject to strength reduction,
+    and similarly for the addressing modes of load and store instructions.
+    Other instructions are unchanged. *)
+
+Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
+  match ros with
+  | inl r =>
+      match D.get r app with
+      | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
+      | _ => ros
+      end
+  | inr s => ros
+  end.
+
+Definition transf_instr (app: D.t) (instr: instruction) :=
+  match instr with
+  | Iop op args res s =>
+      match eval_static_operation op (approx_regs app args) with
+      | I n =>
+          Iop (Ointconst n) nil res s
+      | F n =>
+          Iop (Ofloatconst n) nil res s
+      | S symb ofs =>
+          Iop (Oaddrsymbol symb ofs) nil res s
+      | _ =>
+          let (op', args') := op_strength_reduction (approx_reg app) op args in
+          Iop op' args' res s
+      end
+  | Iload chunk addr args dst s =>
+      let (addr', args') := addr_strength_reduction (approx_reg app) addr args in
+      Iload chunk addr' args' dst s      
+  | Istore chunk addr args src s =>
+      let (addr', args') := addr_strength_reduction (approx_reg app) addr args in
+      Istore chunk addr' args' src s      
+  | Icall sig ros args res s =>
+      Icall sig (transf_ros app ros) args res s
+  | Itailcall sig ros args =>
+      Itailcall sig (transf_ros app ros) args
+  | Icond cond args s1 s2 =>
+      match eval_static_condition cond (approx_regs app args) with
+      | Some b =>
+          if b then Inop s1 else Inop s2
+      | None =>
+          let (cond', args') := cond_strength_reduction (approx_reg app) cond args in
+          Icond cond' args' s1 s2
+      end
+  | _ =>
+      instr
+  end.
+
+Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
+  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
+
+Definition transf_function (f: function) : function :=
+  let approxs := analyze f in
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (transf_code approxs f.(fn_code))
+    f.(fn_entrypoint).
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
new file mode 100644
index 0000000..e628d42
--- /dev/null
+++ b/backend/Constpropproof.v
@@ -0,0 +1,445 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for constant propagation. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Events.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Smallstep.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Lattice.
+Require Import Kildall.
+Require Import ConstpropOp.
+Require Import Constprop.
+Require Import ConstpropOpproof.
+
+(** * Correctness of the static analysis *)
+
+Section ANALYSIS.
+
+Variable ge: genv.
+
+Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
+  forall r, val_match_approx ge (D.get r a) rs#r.
+
+Lemma regs_match_approx_top:
+  forall rs, regs_match_approx D.top rs.
+Proof.
+  intros. red; intros. simpl. rewrite PTree.gempty. 
+  unfold Approx.top, val_match_approx. auto.
+Qed.
+
+Lemma regs_match_approx_increasing:
+  forall a1 a2 rs,
+  D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.
+Proof.
+  unfold D.ge, regs_match_approx. intros.
+  apply val_match_approx_increasing with (D.get r a2); auto.
+Qed.
+
+Lemma regs_match_approx_update:
+  forall ra rs a v r,
+  val_match_approx ge a v ->
+  regs_match_approx ra rs ->
+  regs_match_approx (D.set r a ra) (rs#r <- v).
+Proof.
+  intros; red; intros. rewrite Regmap.gsspec. 
+  case (peq r0 r); intro.
+  subst r0. rewrite D.gss. auto.
+  rewrite D.gso; auto. 
+Qed.
+
+Lemma approx_regs_val_list:
+  forall ra rs rl,
+  regs_match_approx ra rs ->
+  val_list_match_approx ge (approx_regs ra rl) rs##rl.
+Proof.
+  induction rl; simpl; intros.
+  constructor.
+  constructor. apply H. auto.
+Qed.
+
+
+(** The correctness of the static analysis follows from the results
+  of module [ConstpropOpproof] and the fact that the result of
+  the static analysis is a solution of the forward dataflow inequations. *)
+
+Lemma analyze_correct_1:
+  forall f pc rs pc' i,
+  f.(fn_code)!pc = Some i ->
+  In pc' (successors_instr i) ->
+  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
+  regs_match_approx (analyze f)!!pc' rs.
+Proof.
+  intros until i. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
+                      ((fn_entrypoint f, D.top) :: nil)).
+  intros approxs; intros.
+  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
+  eapply DS.fixpoint_solution; eauto.
+  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
+  auto.
+  intros. rewrite PMap.gi. apply regs_match_approx_top. 
+Qed.
+
+Lemma analyze_correct_3:
+  forall f rs,
+  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
+Proof.
+  intros. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
+                      ((fn_entrypoint f, D.top) :: nil)).
+  intros approxs; intros.
+  apply regs_match_approx_increasing with D.top.
+  eapply DS.fixpoint_entry; eauto. auto with coqlib.
+  apply regs_match_approx_top. 
+  intros. rewrite PMap.gi. apply regs_match_approx_top.
+Qed.
+
+End ANALYSIS.
+
+(** * Correctness of the code transformation *)
+
+(** We now show that the transformed code after constant propagation
+  has the same semantics as the original code. *)
+
+Section PRESERVATION.
+
+Variable prog: program.
+Let tprog := transf_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  intros; unfold ge, tge, tprog, transf_program. 
+  apply Genv.find_symbol_transf.
+Qed.
+
+Lemma functions_translated:
+  forall (v: val) (f: fundef),
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof.  
+  intros.
+  exact (Genv.find_funct_transf transf_fundef H).
+Qed.
+
+Lemma function_ptr_translated:
+  forall (b: block) (f: fundef),
+  Genv.find_funct_ptr ge b = Some f ->
+  Genv.find_funct_ptr tge b = Some (transf_fundef f).
+Proof.  
+  intros. 
+  exact (Genv.find_funct_ptr_transf transf_fundef H).
+Qed.
+
+Lemma sig_function_translated:
+  forall f,
+  funsig (transf_fundef f) = funsig f.
+Proof.
+  intros. destruct f; reflexivity.
+Qed.
+
+Lemma transf_ros_correct:
+  forall ros rs f approx,
+  regs_match_approx ge approx rs ->
+  find_function ge ros rs = Some f ->
+  find_function tge (transf_ros approx ros) rs = Some (transf_fundef f).
+Proof.
+  intros until approx; intro MATCH.
+  destruct ros; simpl.
+  intro.
+  exploit functions_translated; eauto. intro FIND.  
+  caseEq (D.get r approx); intros; auto.
+  generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto.
+  generalize (MATCH r). rewrite H0. intros [b [A B]].
+  rewrite <- symbols_preserved in A.
+  rewrite B in FIND. rewrite H1 in FIND. 
+  rewrite Genv.find_funct_find_funct_ptr in FIND.
+  simpl. rewrite A. auto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
+  intro. apply function_ptr_translated. auto.
+  congruence.
+Qed.
+
+(** The proof of semantic preservation is a simulation argument
+  based on diagrams of the following form:
+<<
+           st1 --------------- st2
+            |                   |
+           t|                   |t
+            |                   |
+            v                   v
+           st1'--------------- st2'
+>>
+  The left vertical arrow represents a transition in the
+  original RTL code.  The top horizontal bar is the [match_states]
+  invariant between the initial state [st1] in the original RTL code
+  and an initial state [st2] in the transformed code.
+  This invariant expresses that all code fragments appearing in [st2]
+  are obtained by [transf_code] transformation of the corresponding
+  fragments in [st1].  Moreover, the values of registers in [st1]
+  must match their compile-time approximations at the current program
+  point.
+  These two parts of the diagram are the hypotheses.  In conclusions,
+  we want to prove the other two parts: the right vertical arrow,
+  which is a transition in the transformed RTL code, and the bottom
+  horizontal bar, which means that the [match_state] predicate holds
+  between the final states [st1'] and [st2']. *)
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+   match_stackframe_intro:
+      forall res c sp pc rs f,
+      c = f.(RTL.fn_code) ->
+      (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) ->
+    match_stackframes
+        (Stackframe res c sp pc rs)
+        (Stackframe res (transf_code (analyze f) c) sp pc rs).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro:
+      forall s c sp pc rs m f s'
+           (CF: c = f.(RTL.fn_code))
+           (MATCH: regs_match_approx ge (analyze f)!!pc rs)
+           (STACKS: list_forall2 match_stackframes s s'),
+      match_states (State s c sp pc rs m)
+                   (State s' (transf_code (analyze f) c) sp pc rs m)
+  | match_states_call:
+      forall s f args m s',
+      list_forall2 match_stackframes s s' ->
+      match_states (Callstate s f args m)
+                   (Callstate s' (transf_fundef f) args m)
+  | match_states_return:
+      forall s s' v m,
+      list_forall2 match_stackframes s s' ->
+      match_states (Returnstate s v m)
+                   (Returnstate s' v m).
+
+Ltac TransfInstr :=
+  match goal with
+  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
+      cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr));
+      [ simpl
+      | unfold transf_code; rewrite PTree.gmap; 
+        unfold option_map; rewrite H1; reflexivity ]
+  end.
+
+(** The proof of simulation proceeds by case analysis on the transition
+  taken in the source code. *)
+
+Lemma transf_step_correct:
+  forall s1 t s2,
+  step ge s1 t s2 ->
+  forall s1' (MS: match_states s1 s1'),
+  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
+Proof.
+  induction 1; intros; inv MS.
+
+  (* Inop *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
+  TransfInstr; intro. eapply exec_Inop; eauto.
+  econstructor; eauto.
+  eapply analyze_correct_1 with (pc := pc); eauto.
+  simpl; auto.
+  unfold transfer; rewrite H. auto.
+
+  (* Iop *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
+  TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args);
+  intros op' args' OSR.
+  assert (eval_operation tge sp op' rs##args' = Some v).
+    rewrite (eval_operation_preserved symbols_preserved). 
+    generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
+                  MATCH op args v).
+    rewrite OSR; simpl. auto.
+  generalize (eval_static_operation_correct ge op sp
+               (approx_regs (analyze f)!!pc args) rs##args v
+               (approx_regs_val_list _ _ _ args MATCH) H0).
+  case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros;
+  simpl in H2;
+  eapply exec_Iop; eauto; simpl.
+  congruence.
+  congruence.
+  elim H2; intros b [A B]. rewrite symbols_preserved. 
+  rewrite A; rewrite B; auto.
+  econstructor; eauto. 
+  eapply analyze_correct_1 with (pc := pc); eauto.
+  simpl; auto.
+  unfold transfer; rewrite H. 
+  apply regs_match_approx_update; auto. 
+  eapply eval_static_operation_correct; eauto.
+  apply approx_regs_val_list; auto.
+
+  (* Iload *)
+  caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
+  intros addr' args' ASR.
+  assert (eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite (eval_addressing_preserved symbols_preserved). 
+    generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
+                  MATCH addr args).
+    rewrite ASR; simpl. congruence. 
+  TransfInstr. rewrite ASR. intro.
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
+  eapply exec_Iload; eauto.
+  econstructor; eauto. 
+  eapply analyze_correct_1; eauto. simpl; auto. 
+  unfold transfer; rewrite H. 
+  apply regs_match_approx_update; auto. simpl; auto.
+
+  (* Istore *)
+  caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
+  intros addr' args' ASR.
+  assert (eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite (eval_addressing_preserved symbols_preserved). 
+    generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
+                  MATCH addr args).
+    rewrite ASR; simpl. congruence. 
+  TransfInstr. rewrite ASR. intro.
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
+  eapply exec_Istore; eauto.
+  econstructor; eauto. 
+  eapply analyze_correct_1; eauto. simpl; auto. 
+  unfold transfer; rewrite H. auto. 
+
+  (* Icall *)
+  exploit transf_ros_correct; eauto. intro FIND'.
+  TransfInstr; intro.
+  econstructor; split.
+  eapply exec_Icall; eauto. apply sig_function_translated; auto.
+  constructor; auto. constructor; auto.
+  econstructor; eauto. 
+  intros. eapply analyze_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H.
+  apply regs_match_approx_update; auto. simpl. auto.
+
+  (* Itailcall *)
+  exploit transf_ros_correct; eauto. intros FIND'.
+  TransfInstr; intro.
+  econstructor; split.
+  eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
+  constructor; auto. 
+
+  (* Icond, true *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. 
+  caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
+  intros cond' args' CSR.
+  assert (eval_condition cond' rs##args' = Some true).
+    generalize (cond_strength_reduction_correct
+                  ge (approx_reg (analyze f)!!pc) rs MATCH cond args).
+    rewrite CSR.  intro. congruence.
+  TransfInstr. rewrite CSR. 
+  caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
+  intros b ESC. 
+  generalize (eval_static_condition_correct ge cond _ _ _
+               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
+  replace b with true. intro; eapply exec_Inop; eauto. congruence.
+  intros. eapply exec_Icond_true; eauto.
+  econstructor; eauto.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
+  unfold transfer; rewrite H; auto.
+
+  (* Icond, false *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. 
+  caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
+  intros cond' args' CSR.
+  assert (eval_condition cond' rs##args' = Some false).
+    generalize (cond_strength_reduction_correct
+                  ge (approx_reg (analyze f)!!pc) rs MATCH cond args).
+    rewrite CSR.  intro. congruence.
+  TransfInstr. rewrite CSR. 
+  caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
+  intros b ESC. 
+  generalize (eval_static_condition_correct ge cond _ _ _
+               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
+  replace b with false. intro; eapply exec_Inop; eauto. congruence.
+  intros. eapply exec_Icond_false; eauto.
+  econstructor; eauto.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
+  unfold transfer; rewrite H; auto.
+
+  (* Ireturn *)
+  exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split.
+  eapply exec_Ireturn; eauto. TransfInstr; auto.
+  constructor; auto.
+
+  (* internal function *)
+  simpl. unfold transf_function.
+  econstructor; split.
+  eapply exec_function_internal; simpl; eauto.
+  simpl. econstructor; eauto.
+  apply analyze_correct_3; auto.
+
+  (* external function *)
+  simpl. econstructor; split.
+  eapply exec_function_external; eauto.
+  constructor; auto.
+
+  (* return *)
+  inv H3. inv H1. 
+  econstructor; split.
+  eapply exec_return; eauto. 
+  econstructor; eauto. 
+Qed.
+
+Lemma transf_initial_states:
+  forall st1, initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inversion H.
+  exploit function_ptr_translated; eauto. intro FIND.
+  exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split.
+  econstructor; eauto.
+  replace (prog_main tprog) with (prog_main prog).
+  rewrite symbols_preserved. eauto.
+  reflexivity.
+  rewrite <- H2. apply sig_function_translated.
+  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
+  constructor. constructor. auto.
+  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. 
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r, 
+  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+Proof.
+  intros. inv H0. inv H. inv H4. constructor. 
+Qed.
+
+(** The preservation of the observable behavior of the program then
+  follows, using the generic preservation theorem
+  [Smallstep.simulation_step_preservation]. *)
+
+Theorem transf_program_correct:
+  forall (beh: program_behavior), not_wrong beh ->
+  exec_program prog beh -> exec_program tprog beh.
+Proof.
+  unfold exec_program; intros.
+  eapply simulation_step_preservation; eauto.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact transf_step_correct. 
+Qed.
+
+End PRESERVATION.
diff --git a/powerpc/Constprop.v b/powerpc/ConstpropOp.v
index 109125c..87b2cfa 100644
--- a/powerpc/Constprop.v
+++ b/powerpc/ConstpropOp.v
@@ -10,22 +10,16 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Constant propagation over RTL.  This is the first of the two
-  optimizations performed at RTL level.  It proceeds by a standard
-  dataflow analysis and the corresponding code transformation. *)
+(** Static analysis and strength reduction for operators 
+  and conditions.  This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
-Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
 
 (** * Static analysis *)
 
@@ -42,77 +36,6 @@ Inductive approx : Type :=
                          (** The value is the address of the given global
                              symbol plus the given integer offset. *)
 
-(** We equip this set of approximations with a semi-lattice structure.
-  The ordering is inclusion between the sets of values denoted by
-  the approximations. *)
-
-Module Approx <: SEMILATTICE_WITH_TOP.
-  Definition t := approx.
-  Definition eq (x y: t) := (x = y).
-  Definition eq_refl: forall x, eq x x := (@refl_equal t).
-  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
-  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
-  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
-  Proof.
-    decide equality.
-    apply Int.eq_dec.
-    apply Float.eq_dec.
-    apply Int.eq_dec.
-    apply ident_eq.
-  Qed.
-  Definition beq (x y: t) := if eq_dec x y then true else false.
-  Lemma beq_correct: forall x y, beq x y = true -> x = y.
-  Proof.
-    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
-  Qed.
-  Definition ge (x y: t) : Prop :=
-    x = Unknown \/ y = Novalue \/ x = y.
-  Lemma ge_refl: forall x y, eq x y -> ge x y.
-  Proof.
-    unfold eq, ge; tauto.
-  Qed.
-  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
-  Proof.
-    unfold ge; intuition congruence.
-  Qed.
-  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-  Proof.
-    unfold eq, ge; intros; congruence.
-  Qed.
-  Definition bot := Novalue.
-  Definition top := Unknown.
-  Lemma ge_bot: forall x, ge x bot.
-  Proof.
-    unfold ge, bot; tauto.
-  Qed.
-  Lemma ge_top: forall x, ge top x.
-  Proof.
-    unfold ge, bot; tauto.
-  Qed.
-  Definition lub (x y: t) : t :=
-    if eq_dec x y then x else
-    match x, y with
-    | Novalue, _ => y
-    | _, Novalue => x
-    | _, _ => Unknown
-    end.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
-  Proof.
-    unfold lub, eq; intros.
-    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
-    destruct x; destruct y; auto.
-  Qed.
-  Lemma ge_lub_left: forall x y, ge (lub x y) x.
-  Proof.
-    unfold lub; intros.
-    case (eq_dec x y); intro.
-    apply ge_refl. apply eq_refl.
-    destruct x; destruct y; unfold ge; tauto.
-  Qed.
-End Approx.
-
-Module D := LPMap Approx.
-
 (** We now define the abstract interpretations of conditions and operators
   over this set of approximations.  For instance, the abstract interpretation
   of the operator [Oaddf] applied to two expressions [a] and [b] is
@@ -627,62 +550,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       Unknown
   end.
 
-(** The transfer function for the dataflow analysis is straightforward:
-  for [Iop] instructions, we set the approximation of the destination
-  register to the result of executing abstractly the operation;
-  for [Iload] and [Icall], we set the approximation of the destination
-  to [Unknown]. *)
-
-Definition approx_regs (rl: list reg) (approx: D.t) :=
-  List.map (fun r => D.get r approx) rl.
-
-Definition transfer (f: function) (pc: node) (before: D.t) :=
-  match f.(fn_code)!pc with
-  | None => before
-  | Some i =>
-      match i with
-      | Inop s =>
-          before
-      | Iop op args res s =>
-          let a := eval_static_operation op (approx_regs args before) in
-          D.set res a before
-      | Iload chunk addr args dst s =>
-          D.set dst Unknown before
-      | Istore chunk addr args src s =>
-          before
-      | Icall sig ros args res s =>
-          D.set res Unknown before
-      | Itailcall sig ros args =>
-          before
-(*
-      | Ialloc arg res s =>
-          D.set res Unknown before
-*)
-      | Icond cond args ifso ifnot =>
-          before
-      | Ireturn optarg =>
-          before
-      end
-  end.
-
-(** The static analysis itself is then an instantiation of Kildall's
-  generic solver for forward dataflow inequations. [analyze f]
-  returns a mapping from program points to mappings of pseudo-registers
-  to approximations.  It can fail to reach a fixpoint in a reasonable
-  number of iterations, in which case [None] is returned. *)
-
-Module DS := Dataflow_Solver(D)(NodeSetForward).
-
-Definition analyze (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) (transfer f) 
-                    ((f.(fn_entrypoint), D.top) :: nil) with
-  | None => PMap.init D.top
-  | Some res => res
-  end.
-
-(** * Code transformation *)
-
-(** ** Operator strength reduction *)
+(** * Operator strength reduction *)
 
 (** We now define auxiliary functions for strength reduction of
   operators and addressing modes: replacing an operator with a cheaper
@@ -691,10 +559,10 @@ Definition analyze (f: RTL.function): PMap.t D.t :=
 
 Section STRENGTH_REDUCTION.
 
-Variable approx: D.t.
+Variable app: reg -> approx.
 
 Definition intval (r: reg) : option int :=
-  match D.get r approx with I n => Some n | _ => None end.
+  match app r with I n => Some n | _ => None end.
 
 Inductive cond_strength_reduction_cases: condition -> list reg -> Type :=
   | csr_case1:
@@ -978,7 +846,7 @@ Definition addr_strength_reduction_match (addr: addressing) (args: list reg) :=
 Definition addr_strength_reduction (addr: addressing) (args: list reg) :=
   match addr_strength_reduction_match addr args with
   | addr_strength_reduction_case1 r1 r2 => (* Aindexed2 *)
-      match D.get r1 approx, D.get r2 approx with
+      match app r1, app r2 with
       | S symb n1, I n2 => (Aglobal symb (Int.add n1 n2), nil)
       | S symb n1, _ => (Abased symb n1, r2 :: nil)
       | I n1, S symb n2 => (Aglobal symb (Int.add n1 n2), nil)
@@ -993,7 +861,7 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) :=
       | _ => (addr, args)
       end
   | addr_strength_reduction_case3 n r1 => (* Aindexed *)
-      match D.get r1 approx with
+      match app r1 with
       | S symb ofs => (Aglobal symb (Int.add ofs n), nil)
       | _ => (addr, args)
       end
@@ -1002,77 +870,3 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) :=
   end.
 
 End STRENGTH_REDUCTION.
-
-(** ** Code transformation *)
-
-(** The code transformation proceeds instruction by instruction.
-    Operators whose arguments are all statically known are turned
-    into ``load integer constant'', ``load float constant'' or
-    ``load symbol address'' operations.  Operators for which some
-    but not all arguments are known are subject to strength reduction,
-    and similarly for the addressing modes of load and store instructions.
-    Other instructions are unchanged. *)
-
-Definition transf_ros (approx: D.t) (ros: reg + ident) : reg + ident :=
-  match ros with
-  | inl r =>
-      match D.get r approx with
-      | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
-      | _ => ros
-      end
-  | inr s => ros
-  end.
-
-Definition transf_instr (approx: D.t) (instr: instruction) :=
-  match instr with
-  | Iop op args res s =>
-      match eval_static_operation op (approx_regs args approx) with
-      | I n =>
-          Iop (Ointconst n) nil res s
-      | F n =>
-          Iop (Ofloatconst n) nil res s
-      | S symb ofs =>
-          Iop (Oaddrsymbol symb ofs) nil res s
-      | _ =>
-          let (op', args') := op_strength_reduction approx op args in
-          Iop op' args' res s
-      end
-  | Iload chunk addr args dst s =>
-      let (addr', args') := addr_strength_reduction approx addr args in
-      Iload chunk addr' args' dst s      
-  | Istore chunk addr args src s =>
-      let (addr', args') := addr_strength_reduction approx addr args in
-      Istore chunk addr' args' src s      
-  | Icall sig ros args res s =>
-      Icall sig (transf_ros approx ros) args res s
-  | Itailcall sig ros args =>
-      Itailcall sig (transf_ros approx ros) args
-  | Icond cond args s1 s2 =>
-      match eval_static_condition cond (approx_regs args approx) with
-      | Some b =>
-          if b then Inop s1 else Inop s2
-      | None =>
-          let (cond', args') := cond_strength_reduction approx cond args in
-          Icond cond' args' s1 s2
-      end
-  | _ =>
-      instr
-  end.
-
-Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
-  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
-
-Definition transf_function (f: function) : function :=
-  let approxs := analyze f in
-  mkfunction
-    f.(fn_sig)
-    f.(fn_params)
-    f.(fn_stacksize)
-    (transf_code approxs f.(fn_code))
-    f.(fn_entrypoint).
-
-Definition transf_fundef (fd: fundef) : fundef :=
-  AST.transf_fundef transf_function fd.
-
-Definition transf_program (p: program) : program :=
-  transform_program transf_fundef p.
diff --git a/powerpc/Constpropproof.v b/powerpc/ConstpropOpproof.v
index 6e17f30..3fd81a6 100644
--- a/powerpc/Constpropproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -13,20 +13,16 @@
 (** Correctness proof for constant propagation. *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Events.
 Require Import Mem.
 Require Import Globalenvs.
-Require Import Smallstep.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
+Require Import ConstpropOp.
 Require Import Constprop.
 
 (** * Correctness of the static analysis *)
@@ -51,16 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop :=
   | _ => False
   end.
 
-Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
-  forall r, val_match_approx (D.get r a) rs#r.
-
-Lemma regs_match_approx_top:
-  forall rs, regs_match_approx D.top rs.
-Proof.
-  intros. red; intros. simpl. rewrite PTree.gempty. 
-  unfold Approx.top, val_match_approx. auto.
-Qed.
-
 Lemma val_match_approx_increasing:
   forall a1 a2 v,
   Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v.
@@ -72,26 +58,6 @@ Proof.
   subst a2. auto.
 Qed.
 
-Lemma regs_match_approx_increasing:
-  forall a1 a2 rs,
-  D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.
-Proof.
-  unfold D.ge, regs_match_approx. intros.
-  apply val_match_approx_increasing with (D.get r a2); auto.
-Qed.
-
-Lemma regs_match_approx_update:
-  forall ra rs a v r,
-  val_match_approx a v ->
-  regs_match_approx ra rs ->
-  regs_match_approx (D.set r a ra) (rs#r <- v).
-Proof.
-  intros; red; intros. rewrite Regmap.gsspec. 
-  case (peq r0 r); intro.
-  subst r0. rewrite D.gss. auto.
-  rewrite D.gso; auto. 
-Qed.
-
 Inductive val_list_match_approx: list approx -> list val -> Prop :=
   | vlma_nil:
       val_list_match_approx nil nil
@@ -101,16 +67,6 @@ Inductive val_list_match_approx: list approx -> list val -> Prop :=
       val_list_match_approx al vl ->
       val_list_match_approx (a :: al) (v :: vl).
 
-Lemma approx_regs_val_list:
-  forall ra rs rl,
-  regs_match_approx ra rs ->
-  val_list_match_approx (approx_regs rl ra) rs##rl.
-Proof.
-  induction rl; simpl; intros.
-  constructor.
-  constructor. apply H. auto.
-Qed.
-
 Ltac SimplVMA :=
   match goal with
   | H: (val_match_approx (I _) ?v) |- _ =>
@@ -214,42 +170,6 @@ Proof.
   auto.
 Qed.
 
-(** The correctness of the static analysis follows from the results
-  above and the fact that the result of the static analysis is
-  a solution of the forward dataflow inequations. *)
-
-Lemma analyze_correct_1:
-  forall f pc rs pc' i,
-  f.(fn_code)!pc = Some i ->
-  In pc' (successors_instr i) ->
-  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
-  regs_match_approx (analyze f)!!pc' rs.
-Proof.
-  intros until i. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
-                      ((fn_entrypoint f, D.top) :: nil)).
-  intros approxs; intros.
-  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
-  eapply DS.fixpoint_solution; eauto.
-  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
-  auto.
-  intros. rewrite PMap.gi. apply regs_match_approx_top. 
-Qed.
-
-Lemma analyze_correct_3:
-  forall f rs,
-  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
-Proof.
-  intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
-                      ((fn_entrypoint f, D.top) :: nil)).
-  intros approxs; intros.
-  apply regs_match_approx_increasing with D.top.
-  eapply DS.fixpoint_entry; eauto. auto with coqlib.
-  apply regs_match_approx_top. 
-  intros. rewrite PMap.gi. apply regs_match_approx_top.
-Qed.
-
 (** * Correctness of strength reduction *)
 
 (** We now show that strength reduction over operators and addressing
@@ -260,39 +180,39 @@ Qed.
 
 Section STRENGTH_REDUCTION.
 
-Variable approx: D.t.
+Variable app: reg -> approx.
 Variable sp: val.
 Variable rs: regset.
-Hypothesis MATCH: regs_match_approx approx rs.
+Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.
 
 Lemma intval_correct:
   forall r n,
-  intval approx r = Some n -> rs#r = Vint n.
+  intval app r = Some n -> rs#r = Vint n.
 Proof.
   intros until n.
-  unfold intval. caseEq (D.get r approx); intros; try discriminate.
+  unfold intval. caseEq (app r); intros; try discriminate.
   generalize (MATCH r). unfold val_match_approx. rewrite H.
   congruence. 
 Qed.
 
 Lemma cond_strength_reduction_correct:
   forall cond args,
-  let (cond', args') := cond_strength_reduction approx cond args in
+  let (cond', args') := cond_strength_reduction app cond args in
   eval_condition cond' rs##args' = eval_condition cond rs##args.
 Proof.
   intros. unfold cond_strength_reduction.
   case (cond_strength_reduction_match cond args); intros.
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmp. auto.
   destruct c; reflexivity.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
   auto.
@@ -414,26 +334,26 @@ Qed.
 
 Lemma op_strength_reduction_correct:
   forall op args v,
-  let (op', args') := op_strength_reduction approx op args in
+  let (op', args') := op_strength_reduction app op args in
   eval_operation ge sp op rs##args = Some v ->
   eval_operation ge sp op' rs##args' = Some v.
 Proof.
   intros; unfold op_strength_reduction;
   case (op_strength_reduction_match op args); intros; simpl List.map.
   (* Oadd *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)).
   apply make_addimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_addimm_correct.
   assumption.
   (* Osub *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H) in H0. assumption. 
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). 
   replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil))
      with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)).
@@ -441,17 +361,17 @@ Proof.
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. 
   assumption.
   (* Omul *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)).
   apply make_mulimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_mulimm_correct.
   assumption.
   (* Odiv *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.is_power2 i); intros.
   rewrite (intval_correct _ _ H) in H1.   
   simpl in *; FuncInv. destruct (Int.eq i Int.zero). congruence.
@@ -461,7 +381,7 @@ Proof.
   assumption.
   assumption.
   (* Odivu *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.is_power2 i); intros.
   rewrite (intval_correct _ _ H).
   replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil))
@@ -476,56 +396,56 @@ Proof.
   assumption.
   assumption.
   (* Oand *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)).
   apply make_andimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_andimm_correct.
   assumption.
   (* Oor *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)).
   apply make_orimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_orimm_correct.
   assumption.
   (* Oxor *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
   replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil))
      with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)).
   apply make_xorimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto.
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0). apply make_xorimm_correct.
   assumption.
   (* Oshl *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.ltu i (Int.repr 32)); intros.
   rewrite (intval_correct _ _ H). apply make_shlimm_correct.
   assumption.
   assumption.
   (* Oshr *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.ltu i (Int.repr 32)); intros.
   rewrite (intval_correct _ _ H). apply make_shrimm_correct.
   assumption.
   assumption.
   (* Oshru *)
-  caseEq (intval approx r2); intros.
+  caseEq (intval app r2); intros.
   caseEq (Int.ltu i (Int.repr 32)); intros.
   rewrite (intval_correct _ _ H). apply make_shruimm_correct.
   assumption.
   assumption.
   (* Ocmp *)
   generalize (cond_strength_reduction_correct c rl).
-  destruct (cond_strength_reduction approx c rl).
+  destruct (cond_strength_reduction app c rl).
   simpl. intro. rewrite H. auto.
   (* default *)
   assumption.
@@ -533,15 +453,14 @@ Qed.
 
 Ltac KnownApprox :=
   match goal with
-  | MATCH: (regs_match_approx ?approx ?rs),
-    H: (D.get ?r ?approx = ?a) |- _ =>
+  | H: ?approx ?r = ?a |- _ =>
       generalize (MATCH r); rewrite H; intro; clear H; KnownApprox
   | _ => idtac
   end.
  
 Lemma addr_strength_reduction_correct:
   forall addr args,
-  let (addr', args') := addr_strength_reduction approx addr args in
+  let (addr', args') := addr_strength_reduction app addr args in
   eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.
 Proof.
   intros. 
@@ -589,18 +508,18 @@ Proof.
   case (addr_strength_reduction_match addr args); intros.
 
   (* Aindexed2 *)
-  caseEq (D.get r1 approx); intros;
-  caseEq (D.get r2 approx); intros;
+  caseEq (app r1); intros;
+  caseEq (app r2); intros;
   try reflexivity; KnownApprox; auto.
   rewrite A0. rewrite Int.add_commut. apply A5; auto.
 
   (* Abased *)
-  caseEq (intval approx r1); intros.
+  caseEq (intval app r1); intros.
   simpl; rewrite (intval_correct _ _ H). auto.
   auto.
 
   (* Aindexed *)
-  caseEq (D.get r1 approx); intros; auto.
+  caseEq (app r1); intros; auto.
   simpl; KnownApprox. 
   elim H0. intros b [A B]. rewrite A; rewrite B. auto.
 
@@ -612,330 +531,3 @@ End STRENGTH_REDUCTION.
 
 End ANALYSIS.
 
-(** * Correctness of the code transformation *)
-
-(** We now show that the transformed code after constant propagation
-  has the same semantics as the original code. *)
-
-Section PRESERVATION.
-
-Variable prog: program.
-Let tprog := transf_program prog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-Lemma symbols_preserved:
-  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros; unfold ge, tge, tprog, transf_program. 
-  apply Genv.find_symbol_transf.
-Qed.
-
-Lemma functions_translated:
-  forall (v: val) (f: fundef),
-  Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef f).
-Proof.  
-  intros.
-  exact (Genv.find_funct_transf transf_fundef H).
-Qed.
-
-Lemma function_ptr_translated:
-  forall (b: block) (f: fundef),
-  Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (transf_fundef f).
-Proof.  
-  intros. 
-  exact (Genv.find_funct_ptr_transf transf_fundef H).
-Qed.
-
-Lemma sig_function_translated:
-  forall f,
-  funsig (transf_fundef f) = funsig f.
-Proof.
-  intros. destruct f; reflexivity.
-Qed.
-
-Lemma transf_ros_correct:
-  forall ros rs f approx,
-  regs_match_approx ge approx rs ->
-  find_function ge ros rs = Some f ->
-  find_function tge (transf_ros approx ros) rs = Some (transf_fundef f).
-Proof.
-  intros until approx; intro MATCH.
-  destruct ros; simpl.
-  intro.
-  exploit functions_translated; eauto. intro FIND.  
-  caseEq (D.get r approx); intros; auto.
-  generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto.
-  generalize (MATCH r). rewrite H0. intros [b [A B]].
-  rewrite <- symbols_preserved in A.
-  rewrite B in FIND. rewrite H1 in FIND. 
-  rewrite Genv.find_funct_find_funct_ptr in FIND.
-  simpl. rewrite A. auto.
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
-  intro. apply function_ptr_translated. auto.
-  congruence.
-Qed.
-
-(** The proof of semantic preservation is a simulation argument
-  based on diagrams of the following form:
-<<
-           st1 --------------- st2
-            |                   |
-           t|                   |t
-            |                   |
-            v                   v
-           st1'--------------- st2'
->>
-  The left vertical arrow represents a transition in the
-  original RTL code.  The top horizontal bar is the [match_states]
-  invariant between the initial state [st1] in the original RTL code
-  and an initial state [st2] in the transformed code.
-  This invariant expresses that all code fragments appearing in [st2]
-  are obtained by [transf_code] transformation of the corresponding
-  fragments in [st1].  Moreover, the values of registers in [st1]
-  must match their compile-time approximations at the current program
-  point.
-  These two parts of the diagram are the hypotheses.  In conclusions,
-  we want to prove the other two parts: the right vertical arrow,
-  which is a transition in the transformed RTL code, and the bottom
-  horizontal bar, which means that the [match_state] predicate holds
-  between the final states [st1'] and [st2']. *)
-
-Inductive match_stackframes: stackframe -> stackframe -> Prop :=
-   match_stackframe_intro:
-      forall res c sp pc rs f,
-      c = f.(RTL.fn_code) ->
-      (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) ->
-    match_stackframes
-        (Stackframe res c sp pc rs)
-        (Stackframe res (transf_code (analyze f) c) sp pc rs).
-
-Inductive match_states: state -> state -> Prop :=
-  | match_states_intro:
-      forall s c sp pc rs m f s'
-           (CF: c = f.(RTL.fn_code))
-           (MATCH: regs_match_approx ge (analyze f)!!pc rs)
-           (STACKS: list_forall2 match_stackframes s s'),
-      match_states (State s c sp pc rs m)
-                   (State s' (transf_code (analyze f) c) sp pc rs m)
-  | match_states_call:
-      forall s f args m s',
-      list_forall2 match_stackframes s s' ->
-      match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef f) args m)
-  | match_states_return:
-      forall s s' v m,
-      list_forall2 match_stackframes s s' ->
-      match_states (Returnstate s v m)
-                   (Returnstate s' v m).
-
-Ltac TransfInstr :=
-  match goal with
-  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr));
-      [ simpl
-      | unfold transf_code; rewrite PTree.gmap; 
-        unfold option_map; rewrite H1; reflexivity ]
-  end.
-
-(** The proof of simulation proceeds by case analysis on the transition
-  taken in the source code. *)
-
-Lemma transf_step_correct:
-  forall s1 t s2,
-  step ge s1 t s2 ->
-  forall s1' (MS: match_states s1 s1'),
-  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
-Proof.
-  induction 1; intros; inv MS.
-
-  (* Inop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
-  TransfInstr; intro. eapply exec_Inop; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1 with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. auto.
-
-  (* Iop *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
-  TransfInstr. caseEq (op_strength_reduction (analyze f)!!pc op args);
-  intros op' args' OSR.
-  assert (eval_operation tge sp op' rs##args' = Some v).
-    rewrite (eval_operation_preserved symbols_preserved). 
-    generalize (op_strength_reduction_correct ge (analyze f)!!pc sp rs
-                  MATCH op args v).
-    rewrite OSR; simpl. auto.
-  generalize (eval_static_operation_correct ge op sp
-               (approx_regs args (analyze f)!!pc) rs##args v
-               (approx_regs_val_list _ _ _ args MATCH) H0).
-  case (eval_static_operation op (approx_regs args (analyze f)!!pc)); intros;
-  simpl in H2;
-  eapply exec_Iop; eauto; simpl.
-  congruence.
-  congruence.
-  elim H2; intros b [A B]. rewrite symbols_preserved. 
-  rewrite A; rewrite B; auto.
-  econstructor; eauto. 
-  eapply analyze_correct_1 with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. 
-  eapply eval_static_operation_correct; eauto.
-  apply approx_regs_val_list; auto.
-
-  (* Iload *)
-  caseEq (addr_strength_reduction (analyze f)!!pc addr args);
-  intros addr' args' ASR.
-  assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved symbols_preserved). 
-    generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs
-                  MATCH addr args).
-    rewrite ASR; simpl. congruence. 
-  TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
-  eapply exec_Iload; eauto.
-  econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. simpl; auto.
-
-  (* Istore *)
-  caseEq (addr_strength_reduction (analyze f)!!pc addr args);
-  intros addr' args' ASR.
-  assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved symbols_preserved). 
-    generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs
-                  MATCH addr args).
-    rewrite ASR; simpl. congruence. 
-  TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
-  eapply exec_Istore; eauto.
-  econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. auto. 
-
-  (* Icall *)
-  exploit transf_ros_correct; eauto. intro FIND'.
-  TransfInstr; intro.
-  econstructor; split.
-  eapply exec_Icall; eauto. apply sig_function_translated; auto.
-  constructor; auto. constructor; auto.
-  econstructor; eauto. 
-  intros. eapply analyze_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H.
-  apply regs_match_approx_update; auto. simpl. auto.
-
-  (* Itailcall *)
-  exploit transf_ros_correct; eauto. intros FIND'.
-  TransfInstr; intro.
-  econstructor; split.
-  eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
-  constructor; auto. 
-
-  (* Icond, true *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. 
-  caseEq (cond_strength_reduction (analyze f)!!pc cond args);
-  intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' = Some true).
-    generalize (cond_strength_reduction_correct
-                  ge (analyze f)!!pc rs MATCH cond args).
-    rewrite CSR.  intro. congruence.
-  TransfInstr. rewrite CSR. 
-  caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)).
-  intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ _
-               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
-  replace b with true. intro; eapply exec_Inop; eauto. congruence.
-  intros. eapply exec_Icond_true; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Icond, false *)
-  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. 
-  caseEq (cond_strength_reduction (analyze f)!!pc cond args);
-  intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' = Some false).
-    generalize (cond_strength_reduction_correct
-                  ge (analyze f)!!pc rs MATCH cond args).
-    rewrite CSR.  intro. congruence.
-  TransfInstr. rewrite CSR. 
-  caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)).
-  intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ _
-               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
-  replace b with false. intro; eapply exec_Inop; eauto. congruence.
-  intros. eapply exec_Icond_false; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Ireturn *)
-  exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split.
-  eapply exec_Ireturn; eauto. TransfInstr; auto.
-  constructor; auto.
-
-  (* internal function *)
-  simpl. unfold transf_function.
-  econstructor; split.
-  eapply exec_function_internal; simpl; eauto.
-  simpl. econstructor; eauto.
-  apply analyze_correct_3; auto.
-
-  (* external function *)
-  simpl. econstructor; split.
-  eapply exec_function_external; eauto.
-  constructor; auto.
-
-  (* return *)
-  inv H3. inv H1. 
-  econstructor; split.
-  eapply exec_return; eauto. 
-  econstructor; eauto. 
-Qed.
-
-Lemma transf_initial_states:
-  forall st1, initial_state prog st1 ->
-  exists st2, initial_state tprog st2 /\ match_states st1 st2.
-Proof.
-  intros. inversion H.
-  exploit function_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split.
-  econstructor; eauto.
-  replace (prog_main tprog) with (prog_main prog).
-  rewrite symbols_preserved. eauto.
-  reflexivity.
-  rewrite <- H2. apply sig_function_translated.
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
-  constructor. constructor. auto.
-  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. 
-Qed.
-
-Lemma transf_final_states:
-  forall st1 st2 r, 
-  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
-Proof.
-  intros. inv H0. inv H. inv H4. constructor. 
-Qed.
-
-(** The preservation of the observable behavior of the program then
-  follows, using the generic preservation theorem
-  [Smallstep.simulation_step_preservation]. *)
-
-Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> exec_program tprog beh.
-Proof.
-  unfold exec_program; intros.
-  eapply simulation_step_preservation; eauto.
-  eexact transf_initial_states.
-  eexact transf_final_states.
-  exact transf_step_correct. 
-Qed.
-
-End PRESERVATION.