Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2

8 files changed, 1865 insertions, 11 deletions

diff --git a/Makefile b/Makefile
index d2c81266..27ca8e96 100644
--- a/Makefile
+++ b/Makefile
@@ -86,6 +86,7 @@ BACKEND=\
   ValueDomain.v ValueAOp.v ValueAnalysis.v \
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
   CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
+  CSE2.v CSE2proof.v \
   NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \
   Unusedglob.v Unusedglobproof.v \
   Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \
diff --git a/backend/CSE2.v b/backend/CSE2.v
new file mode 100644
index 00000000..a1c1d9cb
--- /dev/null
+++ b/backend/CSE2.v
@@ -0,0 +1,503 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+(* Static analysis *)
+
+Inductive sym_val : Type :=
+| SMove (src : reg)
+| SOp (op : operation) (args : list reg)
+| SLoad (chunk : memory_chunk) (addr : addressing) (args : list reg).
+                                                   
+Definition eq_args (x y : list reg) : { x = y } + { x <> y } :=
+  list_eq_dec peq x y.
+
+Definition eq_sym_val : forall x y : sym_val,
+    {x = y} + { x <> y }.
+Proof.
+  generalize eq_operation.
+  generalize eq_args.
+  generalize peq.
+  generalize eq_addressing.
+  generalize chunk_eq.
+  decide equality.
+Defined.
+
+Module RELATION.
+  
+Definition t := (PTree.t sym_val).
+Definition eq (r1 r2 : t) :=
+  forall x, (PTree.get x r1) = (PTree.get x r2).
+
+Definition top : t := PTree.empty sym_val.
+
+Lemma eq_refl: forall x, eq x x.
+Proof.
+  unfold eq.
+  intros; reflexivity.
+Qed.
+
+Lemma eq_sym: forall x y, eq x y -> eq y x.
+Proof.
+  unfold eq.
+  intros; eauto.
+Qed.
+
+Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+Proof.
+  unfold eq.
+  intros; congruence.
+Qed.
+
+Definition sym_val_beq (x y : sym_val) :=
+  if eq_sym_val x y then true else false.
+
+Definition beq (r1 r2 : t) := PTree.beq sym_val_beq r1 r2.
+
+Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2.
+Proof.
+  unfold beq, eq. intros r1 r2 EQ x.
+  pose proof (PTree.beq_correct sym_val_beq r1 r2) as CORRECT.
+  destruct CORRECT as [CORRECTF CORRECTB].
+  pose proof (CORRECTF EQ x) as EQx.
+  clear CORRECTF CORRECTB EQ.
+  unfold sym_val_beq in *.
+  destruct (r1 ! x) as [R1x | ] in *;
+    destruct (r2 ! x) as [R2x | ] in *;
+    trivial; try contradiction.
+  destruct (eq_sym_val R1x R2x) in *; congruence.
+Qed.
+
+Definition ge (r1 r2 : t) :=
+  forall x,
+    match PTree.get x r1 with
+    | None => True
+    | Some v => (PTree.get x r2) = Some v
+    end.
+
+Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2.
+Proof.
+  unfold eq, ge.
+  intros r1 r2 EQ x.
+  pose proof (EQ x) as EQx.
+  clear EQ.
+  destruct (r1 ! x).
+  - congruence.
+  - trivial.
+Qed.
+
+Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+Proof.
+  unfold ge.
+  intros r1 r2 r3 GE12 GE23 x.
+  pose proof (GE12 x) as GE12x; clear GE12.
+  pose proof (GE23 x) as GE23x; clear GE23.
+  destruct (r1 ! x); trivial.
+  destruct (r2 ! x); congruence.
+Qed.
+
+Definition lub (r1 r2 : t) :=
+  PTree.combine
+    (fun ov1 ov2 =>
+       match ov1, ov2 with
+       | (Some v1), (Some v2) =>
+         if eq_sym_val v1 v2
+         then ov1
+         else None
+       | None, _
+       | _, None => None
+       end)
+    r1 r2.
+
+Lemma ge_lub_left: forall x y, ge (lub x y) x.
+Proof.
+  unfold ge, lub.
+  intros r1 r2 x.
+  rewrite PTree.gcombine by reflexivity.
+  destruct (_ ! _); trivial.
+  destruct (_ ! _); trivial.
+  destruct (eq_sym_val _ _); trivial.
+Qed.
+
+Lemma ge_lub_right: forall x y, ge (lub x y) y.
+Proof.
+  unfold ge, lub.
+  intros r1 r2 x.
+  rewrite PTree.gcombine by reflexivity.
+  destruct (_ ! _); trivial.
+  destruct (_ ! _); trivial.
+  destruct (eq_sym_val _ _); trivial.
+  congruence.
+Qed.
+
+End RELATION.
+
+Module Type SEMILATTICE_WITHOUT_BOTTOM.
+
+  Parameter t: Type.
+  Parameter eq: t -> t -> Prop.
+  Axiom eq_refl: forall x, eq x x.
+  Axiom eq_sym: forall x y, eq x y -> eq y x.
+  Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+  Parameter beq: t -> t -> bool.
+  Axiom beq_correct: forall x y, beq x y = true -> eq x y.
+  Parameter ge: t -> t -> Prop.
+  Axiom ge_refl: forall x y, eq x y -> ge x y.
+  Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Parameter lub: t -> t -> t.
+  Axiom ge_lub_left: forall x y, ge (lub x y) x.
+  Axiom ge_lub_right: forall x y, ge (lub x y) y.
+
+End SEMILATTICE_WITHOUT_BOTTOM.
+
+Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM).
+  Definition t := option L.t.
+  Definition eq (a b : t) :=
+    match a, b with
+    | None, None => True
+    | Some x, Some y => L.eq x y
+    | Some _, None | None, Some _ => False
+    end.
+  
+  Lemma eq_refl: forall x, eq x x.
+  Proof.
+    unfold eq; destruct x; trivial.
+    apply L.eq_refl.
+  Qed.
+
+  Lemma eq_sym: forall x y, eq x y -> eq y x.
+  Proof.
+    unfold eq; destruct x; destruct y; trivial.
+    apply L.eq_sym.
+  Qed.
+  
+  Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+  Proof.
+    unfold eq; destruct x; destruct y; destruct z; trivial.
+    - apply L.eq_trans.
+    - contradiction.
+  Qed.
+  
+  Definition beq (x y : t) :=
+    match x, y with
+    | None, None => true
+    | Some x, Some y => L.beq x y
+    | Some _, None | None, Some _ => false
+    end.
+  
+  Lemma beq_correct: forall x y, beq x y = true -> eq x y.
+  Proof.
+    unfold beq, eq.
+    destruct x; destruct y; trivial; try congruence.
+    apply L.beq_correct.
+  Qed.
+  
+  Definition ge (x y : t) :=
+    match x, y with
+    | None, Some _ => False
+    | _, None => True
+    | Some a, Some b => L.ge a b
+    end.
+  
+  Lemma ge_refl: forall x y, eq x y -> ge x y.
+  Proof.
+    unfold eq, ge.
+    destruct x; destruct y; trivial.
+    apply L.ge_refl.
+  Qed.
+  
+  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Proof.
+    unfold ge.
+    destruct x; destruct y; destruct z; trivial; try contradiction.
+    apply L.ge_trans.
+  Qed.
+  
+  Definition bot: t := None.
+  Lemma ge_bot: forall x, ge x bot.
+  Proof.
+    unfold ge, bot.
+    destruct x; trivial.
+  Qed.
+  
+  Definition lub (a b : t) :=
+    match a, b with
+    | None, _ => b
+    | _, None => a
+    | (Some x), (Some y) => Some (L.lub x y)
+    end.
+
+  Lemma ge_lub_left: forall x y, ge (lub x y) x.
+  Proof.
+    unfold ge, lub.
+    destruct x; destruct y; trivial.
+    - apply L.ge_lub_left.
+    - apply L.ge_refl.
+      apply L.eq_refl.
+  Qed.
+  
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
+  Proof.
+    unfold ge, lub.
+    destruct x; destruct y; trivial.
+    - apply L.ge_lub_right.
+    - apply L.ge_refl.
+      apply L.eq_refl.
+  Qed.
+End ADD_BOTTOM.
+
+Module RB := ADD_BOTTOM(RELATION).
+Module DS := Dataflow_Solver(RB)(NodeSetForward).
+
+Definition kill_sym_val (dst : reg) (sv : sym_val) :=
+  match sv with
+  | SMove src => if peq dst src then true else false
+  | SOp op args => List.existsb (peq dst) args
+  | SLoad chunk addr args => List.existsb (peq dst) args
+  end.
+                                                 
+Definition kill_reg (dst : reg) (rel : RELATION.t) :=
+  PTree.filter1 (fun x => negb (kill_sym_val dst x))
+                (PTree.remove dst rel).
+
+Definition kill_sym_val_mem (sv: sym_val) :=
+  match sv with
+  | SMove _ => false
+  | SOp op _ => op_depends_on_memory op
+  | SLoad _ _ _ => true
+  end.
+
+Definition kill_mem (rel : RELATION.t) :=
+  PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel.
+
+
+Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
+  match rel ! x with
+  | Some (SMove org) => org
+  | _ => x
+  end.
+
+Definition move (src dst : reg) (rel : RELATION.t) :=
+  PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel).
+
+Definition find_op_fold op args (already : option reg) x sv :=
+                match already with
+                | Some found => already
+                | None =>
+                  match sv with
+                  | (SOp op' args') =>
+                    if (eq_operation op op') && (eq_args args args')
+                    then Some x
+                    else None
+                  | _ => None
+                  end
+                end.
+
+Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) :=
+  PTree.fold (find_op_fold op args) rel None.
+
+Definition find_load_fold chunk addr args (already : option reg) x sv :=
+                match already with
+                | Some found => already
+                | None =>
+                  match sv with
+                  | (SLoad chunk' addr' args') =>
+                    if (chunk_eq chunk chunk') &&
+                       (eq_addressing addr addr') &&
+                       (eq_args args args')
+                    then Some x
+                    else None
+                  | _ => None
+                  end
+                end.
+
+Definition find_load (rel : RELATION.t) (chunk : memory_chunk) (addr : addressing) (args : list reg) :=
+  PTree.fold (find_load_fold chunk addr args) rel None.
+
+Definition oper2 (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  let rel' := kill_reg dst rel in
+  PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'.
+
+Definition oper1 (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  if List.in_dec peq dst args
+  then kill_reg dst rel
+  else oper2 op dst args rel.
+
+Definition oper (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  match find_op rel op (List.map (forward_move rel) args) with
+  | Some r => move r dst rel
+  | None => oper1 op dst args rel
+  end.
+
+Definition gen_oper (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  match op, args with
+  | Omove, src::nil => move src dst rel
+  | _, _ => oper op dst args rel
+  end.
+
+Definition load2 (chunk: memory_chunk) (addr : addressing)
+           (dst : reg) (args : list reg) (rel : RELATION.t) :=
+  let rel' := kill_reg dst rel in
+  PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) rel'.
+
+Definition load1 (chunk: memory_chunk) (addr : addressing)
+           (dst : reg) (args : list reg) (rel : RELATION.t) :=
+  if List.in_dec peq dst args
+  then kill_reg dst rel
+  else load2 chunk addr dst args rel.
+
+Definition load (chunk: memory_chunk) (addr : addressing)
+           (dst : reg) (args : list reg) (rel : RELATION.t) :=
+  match find_load rel chunk addr (List.map (forward_move rel) args) with
+  | Some r => move r dst rel
+  | None => load1 chunk addr dst args rel
+  end.
+
+(* NO LONGER NEEDED
+Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop :=
+  match l with
+  | nil => True
+  | (r,sv)::tail => (tr ! r) = Some sv /\ list_represents tail tr
+  end.
+
+Lemma elements_represent :
+  forall { X : Type },
+  forall tr : (PTree.t X),
+    (list_represents (PTree.elements tr) tr).
+Proof.
+  intros.
+  generalize (PTree.elements_complete tr).
+  generalize (PTree.elements tr).
+  induction l; simpl; trivial.
+  intro COMPLETE.
+  destruct a as [ r sv ].
+  split.
+  {
+    apply COMPLETE.
+    left; reflexivity.
+  }
+  apply IHl; auto.
+Qed.
+*)
+    
+Definition apply_instr instr (rel : RELATION.t) : RB.t :=
+  match instr with
+  | Inop _
+  | Icond _ _ _ _
+  | Ijumptable _ _ => Some rel
+  | Istore _ _ _ _ _ => Some (kill_mem rel)
+  | Iop op args dst _ => Some (gen_oper op dst args rel)
+  | Iload TRAP chunk addr args dst _ => Some (load chunk addr dst args rel)
+  | Iload NOTRAP chunk addr args dst _ => Some (kill_reg dst rel)
+  | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
+  | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *)
+  | Itailcall _ _ _ | Ireturn _ => RB.bot
+  end.
+
+Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
+  match ro with
+  | None => None
+  | Some x =>
+    match code ! pc with
+    | None => RB.bot
+    | Some instr => apply_instr instr x
+    end
+  end.
+
+Definition forward_map (f : RTL.function) := DS.fixpoint
+  (RTL.fn_code f) RTL.successors_instr
+  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
+
+Definition forward_move_b (rb : RB.t) (x : reg) :=
+  match rb with
+  | None => x
+  | Some rel => forward_move rel x
+  end.
+
+Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg :=
+  match fmap with
+  | None => x
+  | Some inv => forward_move_b (PMap.get pc inv) x
+  end.
+
+Definition subst_args fmap pc := List.map (subst_arg fmap pc).
+
+(* Transform *)
+Definition find_op_in_fmap fmap pc op args :=
+  match fmap with
+  | None => None
+  | Some map =>
+    match PMap.get pc map with
+    | Some rel => find_op rel op args
+    | None => None
+    end
+  end.
+
+Definition find_load_in_fmap fmap pc chunk addr args :=
+  match fmap with
+  | None => None
+  | Some map =>
+    match PMap.get pc map with
+    | Some rel => find_load rel chunk addr args
+    | None => None
+    end
+  end.
+
+Definition transf_instr (fmap : option (PMap.t RB.t))
+           (pc: node) (instr: instruction) :=
+  match instr with
+  | Iop op args dst s =>
+    let args' := subst_args fmap pc args in
+    match find_op_in_fmap fmap pc op args' with
+    | None => Iop op args' dst s
+    | Some src => Iop Omove (src::nil) dst s
+    end
+  | Iload TRAP chunk addr args dst s =>
+    let args' := subst_args fmap pc args in
+    match find_load_in_fmap fmap pc chunk addr args' with
+    | None => Iload TRAP chunk addr args' dst s
+    | Some src => Iop Omove (src::nil) dst s
+    end
+  | Iload NOTRAP chunk addr args dst s =>
+    Iload NOTRAP chunk addr (subst_args fmap pc args) dst s
+  | Istore chunk addr args src s =>
+    Istore chunk addr (subst_args fmap pc args) src s
+  | Icall sig ros args dst s =>
+    Icall sig ros (subst_args fmap pc args) dst s
+  | Itailcall sig ros args =>
+    Itailcall sig ros (subst_args fmap pc args)
+  | Icond cond args s1 s2 =>
+    Icond cond (subst_args fmap pc args) s1 s2
+  | Ijumptable arg tbl =>
+    Ijumptable (subst_arg fmap pc arg) tbl
+  | Ireturn (Some arg) =>
+    Ireturn (Some (subst_arg fmap pc arg))
+  | _ => instr
+  end.
+
+Definition transf_function (f: function) : function :=
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := PTree.map (transf_instr (forward_map f)) f.(fn_code);
+     fn_entrypoint := 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.
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
new file mode 100644
index 00000000..f0351c3a
--- /dev/null
+++ b/backend/CSE2proof.v
@@ -0,0 +1,1331 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2.
+
+Lemma args_unaffected:
+  forall rs : regset,
+  forall dst : reg,
+  forall v,
+  forall args : list reg,
+    existsb (fun y : reg => peq dst y) args = false ->
+    (rs # dst <- v ## args) = (rs ## args).
+Proof.
+  induction args; simpl; trivial.
+  destruct (peq dst a) as [EQ | NEQ]; simpl.
+  { discriminate.
+  }
+  intro EXIST.
+  f_equal.
+  {
+    apply Regmap.gso.
+    congruence.
+  }
+  apply IHargs.
+  assumption.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section SAME_MEMORY.
+  Variable m : mem.
+
+Definition sem_sym_val sym rs :=
+  match sym with
+  | SMove src => Some (rs # src)
+  | SOp op args =>
+    eval_operation genv sp op (rs ## args) m
+  | SLoad chunk addr args =>
+    match eval_addressing genv sp addr rs##args with
+    | Some a => Mem.loadv chunk m a
+    | None   => None
+    end
+  end.
+    
+Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val :=
+  match rel ! x with
+  | None => Some (rs # x)
+  | Some sym => sem_sym_val sym rs
+  end.
+
+Definition sem_rel (rel : RELATION.t) (rs : regset) :=
+  forall x : reg, (sem_reg rel x rs) = Some (rs # x).
+
+Definition sem_rel_b (relb : RB.t) (rs : regset) :=
+  match relb with
+  | Some rel => sem_rel rel rs
+  | None => False
+  end.
+
+Definition fmap_sem (fmap : option (PMap.t RB.t))
+  (pc : node) (rs : regset) :=
+  match fmap with
+  | None => True
+  | Some m => sem_rel_b (PMap.get pc m) rs
+  end.
+
+Lemma subst_arg_ok:
+  forall f,
+  forall pc,
+  forall rs,
+  forall arg,
+    fmap_sem (forward_map f) pc rs ->
+    rs # (subst_arg (forward_map f) pc arg) = rs # arg.
+Proof.
+  intros until arg.
+  intro SEM.
+  unfold fmap_sem in SEM.
+  destruct (forward_map f) as [map |]in *; trivial.
+  simpl.
+  unfold sem_rel_b, sem_rel, sem_reg in *.
+  destruct (map # pc).
+  2: contradiction.
+  pose proof (SEM arg) as SEMarg.
+  simpl. unfold forward_move.
+  unfold sem_sym_val in *.
+  destruct (t ! arg); trivial.
+  destruct s; congruence.
+Qed.
+
+Lemma subst_args_ok:
+  forall f,
+  forall pc,
+  forall rs,
+  fmap_sem (forward_map f) pc rs ->
+  forall args,
+    rs ## (subst_args (forward_map f) pc args) = rs ## args.
+Proof.
+  induction args; trivial.
+  simpl.
+  f_equal.
+  apply subst_arg_ok; assumption.
+  assumption.
+Qed.
+
+Lemma kill_reg_sound :
+  forall rel : RELATION.t,
+  forall dst : reg,
+  forall rs,
+  forall v,
+    sem_rel rel rs ->
+    sem_rel (kill_reg dst rel) (rs # dst <- v).
+Proof.
+  unfold sem_rel, kill_reg, sem_reg, sem_sym_val.
+  intros until v.
+  intros REL x.
+  rewrite PTree.gfilter1.
+  destruct (Pos.eq_dec dst x).
+  {
+    subst x.
+    rewrite PTree.grs.
+    rewrite Regmap.gss.
+    reflexivity.
+  }
+  rewrite PTree.gro by congruence.
+  rewrite Regmap.gso by congruence.
+  destruct (rel ! x) as [relx | ] eqn:RELx.
+  2: reflexivity.
+  unfold kill_sym_val.
+  pose proof (REL x) as RELinstx.
+  rewrite RELx in RELinstx.
+  destruct relx eqn:SYMVAL.
+  {
+    destruct (peq dst src); simpl.
+    { reflexivity. }
+    rewrite Regmap.gso by congruence.
+    assumption.
+  }
+  { destruct existsb eqn:EXISTS; simpl.
+    { reflexivity. }
+    rewrite args_unaffected by exact EXISTS.
+    assumption.
+  }
+  { destruct existsb eqn:EXISTS; simpl.
+    { reflexivity. }
+    rewrite args_unaffected by exact EXISTS.
+    assumption.
+  }
+Qed.
+
+Lemma write_same:
+  forall rs : regset,
+  forall src dst : reg,
+    (rs # dst <- (rs # src)) # src = rs # src.
+Proof.
+  intros.
+  destruct (peq src dst).
+  {
+    subst dst.
+    apply Regmap.gss.
+  }
+  rewrite Regmap.gso by congruence.
+  reflexivity.
+Qed.
+
+Lemma move_sound :
+  forall rel : RELATION.t,
+  forall src dst : reg,
+  forall rs,
+    sem_rel rel rs ->
+    sem_rel (move src dst rel) (rs # dst <- (rs # src)).
+Proof.
+  intros until rs. intros REL x.
+  pose proof (kill_reg_sound rel dst rs (rs # src) REL x) as KILL.
+  pose proof (REL src) as RELsrc.
+  unfold move.
+  destruct (peq x dst).
+  {
+    subst x.
+    unfold sem_reg.
+    rewrite PTree.gss.
+    rewrite Regmap.gss.
+    unfold sem_reg in RELsrc.
+    simpl.
+    unfold forward_move.
+    destruct (rel ! src) as [ sv |]; simpl.
+    destruct sv; simpl in *.
+    {
+      destruct (peq dst src0).
+      {
+        subst src0.
+        rewrite Regmap.gss.
+        reflexivity.
+      }
+      rewrite Regmap.gso by congruence.
+      assumption.
+    }
+    all: f_equal; apply write_same.
+  }
+  rewrite Regmap.gso by congruence.
+  unfold sem_reg.
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso in KILL by congruence.
+  exact KILL.
+Qed.
+
+Lemma move_cases_neq:
+  forall dst rel a,
+    a <> dst ->
+    (forward_move (kill_reg dst rel) a) <> dst.
+Proof.
+  intros until a. intro NEQ.
+  unfold kill_reg, forward_move.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by congruence.
+  destruct (rel ! a); simpl.
+  2: congruence.
+  destruct s.
+  {
+    unfold kill_sym_val.
+    destruct peq; simpl; congruence.
+  }
+  all: simpl;
+    destruct negb; simpl; congruence.
+Qed.
+
+Lemma args_replace_dst :
+  forall rel,
+  forall args : list reg,
+  forall dst : reg,
+  forall rs : regset,
+  forall v,
+    (sem_rel rel rs) ->
+    not (In dst args) ->
+    (rs # dst <- v)
+    ## (map
+          (forward_move (kill_reg dst rel)) args) = rs ## args.
+Proof.
+  induction args; simpl.
+  1: reflexivity.
+  intros until v.
+  intros REL NOT_IN.
+  rewrite IHargs by auto.
+  f_equal.
+  pose proof (REL a) as RELa.
+  rewrite Regmap.gso by (apply move_cases_neq; auto).
+  unfold kill_reg.
+  unfold sem_reg in RELa.
+  unfold forward_move.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by auto.
+  destruct (rel ! a); simpl; trivial.
+  destruct s; simpl in *; destruct negb; simpl; congruence.
+Qed.
+
+Lemma oper2_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    not (In dst args) ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (oper2 op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL NOT_IN EVAL x.
+  pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
+  unfold oper2.
+  destruct (peq x dst).
+  {
+    subst x.
+    unfold sem_reg.
+    rewrite PTree.gss.
+    rewrite Regmap.gss.
+    simpl.
+    rewrite args_replace_dst by auto.
+    assumption.
+  }
+  rewrite Regmap.gso by congruence.
+  unfold sem_reg.
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso in KILL by congruence.
+  exact KILL.
+Qed.
+
+Lemma oper1_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (oper1 op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold oper1.
+  destruct in_dec.
+  {
+    apply kill_reg_sound; auto. 
+  }
+  apply oper2_sound; auto.
+Qed.
+
+Lemma find_op_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall src : reg,
+  forall args: list reg,
+  forall rs : regset,
+    sem_rel rel rs ->
+    find_op rel op args = Some src ->
+    (eval_operation genv sp op (rs ## args) m) = Some (rs # src).
+Proof.
+  intros until rs.
+  unfold find_op.
+  rewrite PTree.fold_spec.
+  intro REL.
+  assert (
+     forall start,
+             match start with
+             | None => True
+             | Some src => eval_operation genv sp op rs ## args m = Some rs # src
+             end -> fold_left
+    (fun (a : option reg) (p : positive * sym_val) =>
+     find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start =
+                    Some src ->
+             eval_operation genv sp op rs ## args m = Some rs # src) as REC.
+  {
+    unfold sem_rel, sem_reg in REL.
+    generalize (PTree.elements_complete rel).
+    generalize (PTree.elements rel).
+    induction l; simpl.
+    {
+      intros.
+      subst start.
+      assumption.
+    }
+    destruct a as [r sv]; simpl.
+    intros COMPLETE start GEN.
+    apply IHl.
+    {
+      intros.
+      apply COMPLETE.
+      right.
+      assumption.
+    }
+    unfold find_op_fold.
+    destruct start.
+    assumption.
+    destruct sv; trivial.
+    destruct eq_operation; trivial.
+    subst op0.
+    destruct eq_args; trivial.
+    subst args0.
+    simpl.
+    assert ((rel ! r) = Some (SOp op args)) as RELatr.
+    {
+      apply COMPLETE.
+      left.
+      reflexivity.
+    }
+    pose proof (REL r) as RELr.
+    rewrite RELatr in RELr.
+    simpl in RELr.
+    assumption.
+  }
+  apply REC; auto.
+Qed.
+
+Lemma find_load_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall src : reg,
+  forall args: list reg,
+  forall rs : regset,
+    sem_rel rel rs ->
+    find_load rel chunk addr args = Some src ->
+    match eval_addressing genv sp addr rs##args with
+    | Some a => (Mem.loadv chunk m a) = Some (rs # src)
+    | None => True
+    end.
+Proof.
+  intros until rs.
+  unfold find_load.
+  rewrite PTree.fold_spec.
+  intro REL.
+  assert (
+     forall start,
+             match start with
+             | None => True
+             | Some src =>
+               match eval_addressing genv sp addr rs##args with
+               | Some a => (Mem.loadv chunk m a) = Some (rs # src)
+               | None => True
+               end               
+             end ->
+    fold_left
+    (fun (a : option reg) (p : positive * sym_val) =>
+     find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start =
+    Some src ->
+    match eval_addressing genv sp addr rs##args with
+               | Some a => (Mem.loadv chunk m a) = Some (rs # src)
+               | None => True
+               end ) as REC.
+  
+  {
+    unfold sem_rel, sem_reg in REL.
+    generalize (PTree.elements_complete rel).
+    generalize (PTree.elements rel).
+    induction l; simpl.
+    {
+      intros.
+      subst start.
+      assumption.
+    }
+    destruct a as [r sv]; simpl.
+    intros COMPLETE start GEN.
+    apply IHl.
+    {
+      intros.
+      apply COMPLETE.
+      right.
+      assumption.
+    }
+    unfold find_load_fold.
+    destruct start.
+    assumption.
+    destruct sv; trivial.
+    destruct chunk_eq; trivial.
+    subst chunk0.
+    destruct eq_addressing; trivial.
+    subst addr0.
+    destruct eq_args; trivial.
+    subst args0.
+    simpl.
+    assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr.
+    {
+      apply COMPLETE.
+      left.
+      reflexivity.
+    }
+    pose proof (REL r) as RELr.
+    rewrite RELatr in RELr.
+    simpl in RELr.
+    destruct eval_addressing; trivial.
+  }
+  apply REC; auto.
+Qed.
+
+Lemma find_load_sound' :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall src : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+    sem_rel rel rs ->
+    find_load rel chunk addr args = Some src ->
+    eval_addressing genv sp addr rs##args = Some a ->
+    (Mem.loadv chunk m a) = Some (rs # src).
+Proof.
+  intros until a. intros REL LOAD ADDR.
+  pose proof (find_load_sound rel chunk addr src args rs REL LOAD) as Z.
+  destruct eval_addressing in *; congruence.
+Qed.
+
+Lemma forward_move_map:
+  forall rel args rs,
+    sem_rel rel rs ->
+    rs ## (map (forward_move rel) args) = rs ## args.
+Proof.
+  induction args; simpl; trivial.
+  intros rs REL.
+  f_equal.
+  2: (apply IHargs; assumption).
+  unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
+  pose proof (REL a) as RELa.
+  destruct (rel ! a); trivial.
+  destruct s; congruence.
+Qed.
+
+Lemma oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold oper.
+  destruct find_op eqn:FIND.
+  {
+    assert (eval_operation genv sp op rs ## (map (forward_move rel) args) m = Some rs # r) as FIND_OP.
+    {
+      apply (find_op_sound rel); trivial.
+    }
+    rewrite forward_move_map in FIND_OP by assumption.
+    replace v with (rs # r) by congruence.
+    apply move_sound; auto.
+  }
+  apply oper1_sound; trivial.
+Qed.
+
+Lemma gen_oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (gen_oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold gen_oper.
+  destruct op.
+  { destruct args as [ | h0 t0].
+    apply oper_sound; auto.
+    destruct t0.
+    {
+      simpl in *.
+      replace v with (rs # h0) by congruence.
+      apply move_sound; auto.
+    }
+    apply oper_sound; auto.
+  }
+  all: apply oper_sound; auto.
+Qed.
+
+
+Lemma load2_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+  forall v,
+    sem_rel rel rs ->
+    not (In dst args) ->
+    eval_addressing genv sp addr (rs ## args) = Some a ->
+    Mem.loadv chunk m a = Some v ->
+    sem_rel (load2 chunk addr dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL NOT_IN ADDR LOAD x.
+  pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
+  unfold load2.
+  destruct (peq x dst).
+  {
+    subst x.
+    unfold sem_reg.
+    rewrite PTree.gss.
+    rewrite Regmap.gss.
+    simpl.
+    rewrite args_replace_dst by auto.
+    destruct eval_addressing; congruence.
+  }
+  rewrite Regmap.gso by congruence.
+  unfold sem_reg.
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso in KILL by congruence.
+  exact KILL.
+Qed.
+
+Lemma load1_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+  forall v,
+    sem_rel rel rs ->
+    eval_addressing genv sp addr (rs ## args) = Some a ->
+    Mem.loadv chunk m a = Some v ->
+    sem_rel (load1 chunk addr dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL ADDR LOAD.
+  unfold load1.
+  destruct in_dec.
+  {
+    apply kill_reg_sound; auto. 
+  }
+  apply load2_sound with (a := a); auto.
+Qed.
+
+Lemma load_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+  forall v,
+    sem_rel rel rs ->
+    eval_addressing genv sp addr (rs ## args) = Some a ->
+    Mem.loadv chunk m a = Some v ->
+    sem_rel (load chunk addr dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL ADDR LOAD.
+  unfold load.
+  destruct find_load eqn:FIND.
+  {
+    assert (match eval_addressing genv sp addr rs##(map (forward_move rel) args) with
+    | Some a => (Mem.loadv chunk m a) = Some (rs # r)
+    | None => True
+    end) as FIND_LOAD.
+    {
+      apply (find_load_sound rel); trivial.
+    }
+    rewrite forward_move_map in FIND_LOAD by assumption.
+    destruct eval_addressing in *.
+    2: discriminate.
+    replace v with (rs # r) by congruence.
+    apply move_sound; auto.
+  }
+  apply load1_sound with (a := a); trivial.
+Qed.
+
+Lemma kill_reg_weaken:
+  forall res mpc rs,
+    sem_rel mpc rs ->
+    sem_rel (kill_reg res mpc) rs.
+Proof.
+  intros until rs.
+  intros REL x.
+  pose proof (REL x) as RELx.
+  unfold kill_reg, sem_reg in *.
+  rewrite PTree.gfilter1.
+  destruct (peq res x).
+  { subst x.
+    rewrite PTree.grs.
+    reflexivity.
+  }
+  rewrite PTree.gro by congruence.
+  destruct (mpc ! x) as [sv | ]; trivial.
+  destruct negb; trivial.
+Qed.
+
+Lemma top_ok:
+  forall rs, sem_rel RELATION.top rs.
+Proof.
+  unfold sem_rel, sem_reg, RELATION.top.
+  intros.
+  rewrite PTree.gempty.
+  reflexivity.
+Qed.
+
+Lemma sem_rel_ge:
+  forall r1 r2 : RELATION.t,
+    (RELATION.ge r1 r2) ->
+    forall rs : regset,
+      (sem_rel r2 rs) -> (sem_rel r1 rs).
+Proof.
+  intros r1 r2 GE rs RE x.
+  pose proof (RE x) as REx.
+  pose proof (GE x) as GEx.
+  unfold sem_reg in *.
+  destruct (r1 ! x) as [r1x | ] in *;
+    destruct (r2 ! x) as [r2x | ] in *;
+    congruence.
+Qed.
+End SAME_MEMORY.
+
+Lemma kill_mem_sound :
+  forall m m' : mem,
+  forall rel : RELATION.t,
+  forall rs,
+    sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs.
+Proof.
+  unfold sem_rel, sem_reg.
+  intros until rs.
+  intros SEM x.
+  pose proof (SEM x) as SEMx.
+  unfold kill_mem.
+  rewrite PTree.gfilter1.
+  unfold kill_sym_val_mem.
+  destruct (rel ! x) as [ sv | ].
+  2: reflexivity.
+  destruct sv; simpl in *; trivial.
+  {
+    destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial.
+    rewrite <- SEMx.
+    apply op_depends_on_memory_correct; auto.
+  }
+Qed.
+
+End SOUNDNESS.
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. apply match_transform_program; auto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_transf TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_ptr_transf TRANSL).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_transf TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; trivial.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  unfold find_function; intros. destruct ros as [r|id].
+  eapply functions_translated; eauto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+Lemma transf_function_at:
+  forall (f : function) (pc : node) (i : instruction),
+  (fn_code f)!pc = Some i ->
+  (fn_code (transf_function f))!pc =
+    Some(transf_instr (forward_map f) pc i).
+Proof.
+  intros until i. intro CODE.
+  unfold transf_function; simpl.
+  rewrite PTree.gmap.
+  unfold option_map.
+  rewrite CODE.
+  reflexivity.
+Qed.
+
+Definition is_killed_in_map (map : PMap.t RB.t) pc res :=
+  match PMap.get pc map with
+  | None => True
+  | Some rel => exists rel', RELATION.ge rel (kill_reg res rel')
+  end.
+
+Definition is_killed_in_fmap fmap pc res :=
+  match fmap with
+  | None => True
+  | Some map => is_killed_in_map map pc res
+  end.
+
+Definition sem_rel_b' := sem_rel_b fundef unit ge.
+Definition fmap_sem' := fmap_sem fundef unit ge.
+Definition subst_arg_ok' := subst_arg_ok fundef unit ge.
+Definition subst_args_ok' := subst_args_ok fundef unit ge.
+Definition kill_mem_sound' := kill_mem_sound fundef unit ge.
+
+Lemma sem_rel_b_ge:
+  forall rb1 rb2 : RB.t,
+    (RB.ge rb1 rb2) ->
+    forall sp m,
+    forall rs : regset,
+      (sem_rel_b' sp m rb2 rs) -> (sem_rel_b' sp m rb1 rs).
+Proof.
+  unfold sem_rel_b', sem_rel_b.
+  destruct rb1 as [r1 | ];
+    destruct rb2 as [r2 | ]; simpl;
+      intros GE sp m rs RE; try contradiction.
+  apply sem_rel_ge with (r2 := r2); assumption.
+Qed.
+
+Lemma apply_instr'_bot :
+  forall code,
+  forall pc,
+    RB.eq (apply_instr' code pc RB.bot) RB.bot.
+Proof.
+  reflexivity.
+Qed.
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+| match_frames_intro: forall res f sp pc rs,
+    (forall m : mem,
+     forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) ->
+    match_frames (Stackframe res f sp pc rs)
+                 (Stackframe res (transf_function f) sp pc rs).
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+                                 (STACKS: list_forall2 match_frames stk stk'),
+      (fmap_sem' sp m (forward_map f) pc rs) ->
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp pc rs m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | match_returnstates: forall stk v m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v m).
+  
+Ltac TR_AT :=
+  match goal with
+  | [ A: (fn_code _)!_ = Some _ |- _ ] =>
+        generalize (transf_function_at _ _ _ A); intros
+  end.
+
+Lemma step_simulation:
+  forall S1 t S2, RTL.step ge S1 t S2 ->
+  forall S1', match_states S1 S1' ->
+              exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
+Proof.
+  induction 1; intros S1' MS; inv MS; try TR_AT.
+- (* nop *)
+  econstructor; split. eapply exec_Inop; eauto.
+  constructor; auto.
+  
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply sem_rel_b_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl. tauto.
+  }
+  unfold apply_instr'.
+  unfold sem_rel_b in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
+- (* op *)
+  unfold transf_instr in *.
+  destruct find_op_in_fmap eqn:FIND_OP.
+  {
+    unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
+    destruct (forward_map f) as [map |] eqn:MAP.
+    2: discriminate.
+    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+    destruct (map # pc) as [mpc | ] eqn:MPC.
+    2: discriminate.
+    econstructor; split.
+    {
+      eapply exec_Iop with (v := v); eauto.
+      simpl.
+      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
+      {
+        rewrite MAP in H0.
+        rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption.
+        assumption.
+      }
+      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
+    }
+    constructor; eauto.
+    unfold fmap_sem', fmap_sem in *.
+    rewrite MAP.
+    apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)).
+    {
+      replace (Some (gen_oper op res args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+      {
+        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+        2: apply apply_instr'_bot.
+        simpl. tauto.
+      }
+      unfold apply_instr'.
+      rewrite H.
+      rewrite MPC.
+      reflexivity.
+    }
+    unfold sem_rel_b', sem_rel_b.
+    apply gen_oper_sound; auto.
+  }
+  {
+    econstructor; split.
+    {
+      eapply exec_Iop with (v := v); eauto.
+      rewrite (subst_args_ok' sp m) by assumption.
+      rewrite <- H0.
+      apply eval_operation_preserved. exact symbols_preserved.
+    }
+    constructor; eauto.
+    unfold fmap_sem', fmap_sem in *.
+    unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
+    destruct (forward_map f) as [map |] eqn:MAP.
+    2: constructor.
+    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+    destruct (map # pc) as [mpc | ] eqn:MPC.
+    2: contradiction.
+
+    apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)).
+    {
+      replace (Some (gen_oper op res args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+      {
+        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+        2: apply apply_instr'_bot.
+        simpl. tauto.
+      }
+      unfold apply_instr'.
+      rewrite H.
+      rewrite MPC.
+      reflexivity.
+    }
+    unfold sem_rel_b', sem_rel_b.
+    apply gen_oper_sound; auto.
+  }
+    
+(* load *)
+- unfold transf_instr in *.
+  destruct trap.
+  { (* TRAP *)
+    destruct find_load_in_fmap eqn:FIND_LOAD.
+    {
+      unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
+      destruct (forward_map f) as [map |] eqn:MAP.
+      2: discriminate.
+      change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+      destruct (map # pc) as [mpc | ] eqn:MPC.
+      2: discriminate.
+      econstructor; split.
+      {
+        eapply exec_Iop with (v := v); eauto.
+        simpl.
+        rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
+        {
+          rewrite find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs) in H1; trivial.
+          rewrite MAP in H0.
+          assumption.
+        }
+        unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
+      }
+      constructor; eauto.
+      unfold fmap_sem', fmap_sem in *.
+      rewrite MAP.
+      apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+      {
+        replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+        {
+          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+          2: apply apply_instr'_bot.
+          simpl. tauto.
+        }
+        unfold apply_instr'.
+        rewrite H.
+        rewrite MPC.
+        simpl.
+        reflexivity.
+      }
+      unfold sem_rel_b', sem_rel_b.
+      apply load_sound with (a := a); auto.
+    }
+    {  
+      econstructor; split.
+      assert (eval_addressing tge sp addr rs ## args = Some a).
+      rewrite <- H0.
+      apply eval_addressing_preserved. exact symbols_preserved.
+      eapply exec_Iload; eauto.
+      rewrite (subst_args_ok' sp m); assumption.
+      constructor; auto.
+      
+      simpl in *.
+      unfold fmap_sem', fmap_sem in *.
+      destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+      destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+      apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+      {
+        replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+        {
+          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+          2: apply apply_instr'_bot.
+          simpl. tauto.
+        }
+        unfold apply_instr'.
+        rewrite H.
+        rewrite MPC.
+        simpl.
+        reflexivity.
+      }
+      apply load_sound with (a := a); assumption.
+    }
+  }
+
+  { (* NOTRAP *)
+    econstructor; split.
+    assert (eval_addressing tge sp addr rs ## args = Some a).
+    rewrite <- H0.
+    apply eval_addressing_preserved. exact symbols_preserved.
+    eapply exec_Iload; eauto.
+    rewrite (subst_args_ok' sp m); assumption.
+    constructor; auto.
+    
+    simpl in *.
+    unfold fmap_sem', fmap_sem in *.
+    destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+    destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+    apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)).
+    {
+      replace (Some (kill_reg dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+      {
+        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+        2: apply apply_instr'_bot.
+        simpl. tauto.
+      }
+      unfold apply_instr'.
+      rewrite H.
+      rewrite MPC.
+      simpl.
+      reflexivity.
+    }
+    apply kill_reg_sound; assumption.
+  }
+  
+- (* load notrap1 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = None).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap1; eauto.
+  rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption.
+  constructor; auto.
+
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)).
+  {
+    replace (Some (kill_reg dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    simpl.
+    reflexivity.
+  }
+  apply kill_reg_sound; assumption.
+  
+- (* load notrap2 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap2; eauto.
+  rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption.
+  constructor; auto.
+
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)).
+  {
+    replace (Some (kill_reg dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    simpl.
+    reflexivity.
+  }
+  apply kill_reg_sound; assumption.
+  
+- (* store *)
+  econstructor. split.
+  {
+    assert (eval_addressing tge sp addr rs ## args = Some a).
+    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+    eapply exec_Istore; eauto.
+    rewrite (subst_args_ok' sp m); assumption.
+  }
+  
+  constructor; auto.
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  apply sem_rel_b_ge with (rb2 := Some (kill_mem mpc)); trivial.
+  {
+  replace (Some (kill_mem mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl. tauto.
+  }
+  unfold apply_instr'.
+  unfold sem_rel_b in *.
+  rewrite MPC.
+  rewrite H.
+  reflexivity.
+  }
+  apply (kill_mem_sound' sp m).
+  assumption.
+  
+(* call *)
+- econstructor; split.
+  eapply exec_Icall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  rewrite (subst_args_ok' sp m) by assumption.
+  constructor. constructor; auto.
+
+  constructor.
+  {
+    intros m' vres.
+    unfold fmap_sem', fmap_sem in *.
+    destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+    destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+    apply sem_rel_b_ge with (rb2 := Some (kill_reg res (kill_mem mpc))).
+    {
+      replace (Some (kill_reg res (kill_mem mpc))) with (apply_instr' (fn_code f) pc (map # pc)).
+      {
+        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+        2: apply apply_instr'_bot.
+        simpl. tauto.
+      }
+      unfold apply_instr'.
+      rewrite H.
+      rewrite MPC.
+      reflexivity.
+    }
+    apply kill_reg_sound.
+    apply (kill_mem_sound' sp m).
+    assumption.
+  }
+  
+(* tailcall *)
+- econstructor; split.
+  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption.
+  constructor. auto.
+
+(* builtin *)
+- econstructor; split.
+  eapply exec_Ibuiltin; eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  
+  apply sem_rel_b_ge with (rb2 := Some RELATION.top).
+  {
+    replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    reflexivity.
+  }
+  apply top_ok.
+  
+
+(* cond *)
+- econstructor; split.
+  eapply exec_Icond; eauto.
+  rewrite (subst_args_ok' sp m); eassumption.
+  constructor; auto.
+
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply sem_rel_b_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl.
+    destruct b; tauto.
+  }
+  unfold apply_instr'.
+  unfold sem_rel_b in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
+
+(* jumptbl *)
+- econstructor; split.
+  eapply exec_Ijumptable; eauto.
+  rewrite (subst_arg_ok' sp m); eassumption.
+  constructor; auto.
+
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply sem_rel_b_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl.
+    apply list_nth_z_in with (n := Int.unsigned n).
+    assumption.
+  }
+  unfold apply_instr'.
+  unfold sem_rel_b in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
+  
+(* return *)
+- destruct or as [arg | ].
+  {
+    econstructor; split.
+    eapply exec_Ireturn; eauto.
+    unfold regmap_optget.
+    rewrite (subst_arg_ok' (Vptr stk Ptrofs.zero) m) by eassumption.
+    constructor; auto.
+  }
+    econstructor; split.
+    eapply exec_Ireturn; eauto.
+    constructor; auto.
+  
+  
+(* internal function *)
+-  simpl. econstructor; split.
+  eapply exec_function_internal; eauto.
+  constructor; auto.
+
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply sem_rel_b_ge with (rb2 := Some RELATION.top).
+  {
+    eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption.
+  }
+  apply top_ok.
+  
+(* external function *)
+- econstructor; split.
+  eapply exec_function_external; eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+    constructor; auto.
+
+(* return *)
+- inv STACKS. inv H1.
+  econstructor; split.
+  eapply exec_return; eauto.
+  constructor; auto.
+Admitted.
+
+
+Lemma transf_initial_states:
+  forall S1, RTL.initial_state prog S1 ->
+  exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
+Proof.
+  intros. inv H. econstructor; split.
+  econstructor.
+    eapply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
+    eapply function_ptr_translated; eauto.
+    rewrite <- H3; apply sig_preserved.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_step.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
+Qed.
+
+End PRESERVATION.
\ No newline at end of file
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 9aa4a2bf..ba0246df 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -26,6 +26,7 @@ let option_ffloatconstprop = ref 2
 let option_ftailcalls = ref true
 let option_fconstprop = ref true
 let option_fcse = ref true
+let option_fcse2 = ref true
 let option_fredundancy = ref true
 let option_fpostpass = ref true
 let option_fpostpass_sched = ref "list"
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 24964237..24c3518b 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -42,6 +42,7 @@ Require Duplicate.
 Require Constprop.
 Require CSE.
 Require ForwardMoves.
+Require CSE2.
 Require Deadcode.
 Require Unusedglob.
 Require Allnontrap.
@@ -66,6 +67,7 @@ Require Duplicateproof.
 Require Constpropproof.
 Require CSEproof.
 Require ForwardMovesproof.
+Require CSE2proof.
 Require Deadcodeproof.
 Require Unusedglobproof.
 Require Allnontrapproof.
@@ -140,14 +142,16 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 6)
   @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 7)
-   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
+   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
    @@ print (print_RTL 8)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
    @@ print (print_RTL 9)
-   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 10)
-  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
    @@ print (print_RTL 11)
+  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ print (print_RTL 12)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
@@ -254,6 +258,7 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
   ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog)
   ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog)
   ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
   ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
@@ -300,8 +305,9 @@ Proof.
   set (p11 := total_if optim_constprop Constprop.transf_program p10) in *.
   set (p12 := total_if optim_constprop Renumber.transf_program p11) in *.
   destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
-  set (p13bis := total_if optim_forward_moves ForwardMoves.transf_program p13) in *.
-  destruct (partial_if optim_redundancy Deadcode.transf_program p13bis) as [p14|e] eqn:P14; simpl in T; try discriminate.
+  set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *.
+  set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *.
+  destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate.
   set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *.
   destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate.
   destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate.
@@ -324,7 +330,8 @@ Proof.
   exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match.
   exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match.
   exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
-  exists p13bis; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match.
+  exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match.
+  exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match.
   exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
   exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match.
   exists p15; split. apply Unusedglobproof.transf_program_match; auto.
@@ -385,7 +392,7 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p24)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -412,7 +419,9 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct.
   eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption.
+  eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct.
+  eapply compose_forward_simulations.
+  eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index fdd2b1d6..4d6a096c 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -36,6 +36,9 @@ Parameter optim_constprop: unit -> bool.
 (** Flag -fcse.  For common subexpression elimination. *)
 Parameter optim_CSE: unit -> bool.
 
+(** Flag -fcse2.  For DMonniaux's common subexpression elimination. *)
+Parameter optim_CSE2: unit -> bool.
+
 (** Flag -fredundancy.  For dead code elimination. *)
 Parameter optim_redundancy: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 992cf8c4..3c97e17f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -195,6 +195,7 @@ Processing options:
   -ffloat-const-prop <n>  Control constant propagation of floats
                    (<n>=0: none, <n>=1: limited, <n>=2: full; default is full)
   -fcse          Perform common subexpression elimination [on]
+  -fcse2         Perform inter-loop common subexpression elimination [on]
   -fredundancy   Perform redundancy elimination [on]
   -fpostpass     Perform postpass scheduling (only for K1 architecture) [on]
   -fpostpass= <optim> Perform postpass scheduling with the specified optimization [list]
@@ -258,8 +259,10 @@ let dump_mnemonics destfile =
   exit 0
 
 let optimization_options = [
-  option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse;
-  option_fpostpass; option_fredundancy; option_finline_functions_called_once;
+    option_ftailcalls; option_fifconversion; option_fconstprop;
+    option_fcse; option_fcse2;
+    option_fpostpass;
+    option_fredundancy; option_finline; option_finline_functions_called_once;
 ]
 
 let set_all opts () = List.iter (fun r -> r := true) opts
@@ -382,6 +385,7 @@ let cmdline_actions =
   @ f_opt "if-conversion" option_fifconversion
   @ f_opt "const-prop" option_fconstprop
   @ f_opt "cse" option_fcse
+  @ f_opt "cse2" option_fcse2
   @ f_opt "redundancy" option_fredundancy
   @ f_opt "postpass" option_fpostpass
   @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 0c19ea70..ba6b080b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -109,6 +109,8 @@ Extract Constant Compopts.optim_constprop =>
   "fun _ -> !Clflags.option_fconstprop".
 Extract Constant Compopts.optim_CSE =>
   "fun _ -> !Clflags.option_fcse".
+Extract Constant Compopts.optim_CSE2 =>
+  "fun _ -> !Clflags.option_fcse2".
 Extract Constant Compopts.optim_redundancy =>
   "fun _ -> !Clflags.option_fredundancy".
 Extract Constant Compopts.optim_postpass =>