If-conversion optimization for Cminorconditional-move

Add an experimental pass that converts some if/then/else statements
into "select" built-ins, which in turn can be compiled down to
branchless instruction sequences if the target architecture supports them.

The statements that are converted are of the form

    if (cond) { x = a1; } else { x = a2; }
    if (cond) { x = a1; }
    if (cond) { /*skip*/; } else { x = a2; }

where a1, a2 are "safe" expressions, containing no operations that can
fail at run-time, such as memory loads or integer divisions.

To support the optimization, I added a type inference and type checking
pass for Cminor, in backend/Cminortyping.v.  The inferred type information
is used to determine the type at which the "select" built-in operates,
and to prove semantic preservation.

5 files changed, 1433 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index 8ab6b5b0..9390c8ee 100644
--- a/Makefile
+++ b/Makefile
@@ -67,7 +67,9 @@ COMMON=Errors.v AST.v Linking.v \
 # Back-end modules (in backend/, $(ARCH)/)
 
 BACKEND=\
-  Cminor.v Op.v CminorSel.v \
+  Cminor.v Cminortyping.v \
+  Ifconv.v Ifconvproof.v \
+  Op.v CminorSel.v \
   SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \
   SelectOpproof.v SelectDivproof.v SplitLongproof.v \
   SelectLongproof.v Selectionproof.v \
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
new file mode 100644
index 00000000..14c80f07
--- /dev/null
+++ b/backend/Cminortyping.v
@@ -0,0 +1,701 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Coqlib Maps Errors.
+Require Import AST Integers Floats Values Memory Globalenvs Events Smallstep.
+Require Import Cminor.
+Require Import Unityping.
+
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
+
+Definition type_constant (c: constant) : typ :=
+  match c with
+  | Ointconst _ => Tint
+  | Ofloatconst _ => Tfloat
+  | Osingleconst _ => Tsingle
+  | Olongconst _ => Tlong
+  | Oaddrsymbol _ _ => Tptr
+  | Oaddrstack _ => Tptr
+  end.
+
+Definition type_unop (op: unary_operation) : typ * typ :=
+  match op with
+  | Ocast8unsigned | Ocast8signed | Ocast16unsigned | Ocast16signed
+  | Onegint | Onotint => (Tint, Tint)
+  | Onegf | Oabsf => (Tfloat, Tfloat)
+  | Onegfs | Oabsfs => (Tsingle, Tsingle)
+  | Osingleoffloat => (Tfloat, Tsingle)
+  | Ofloatofsingle => (Tsingle, Tfloat)
+  | Ointoffloat | Ointuoffloat => (Tfloat, Tint)
+  | Ofloatofint | Ofloatofintu => (Tint, Tfloat)
+  | Ointofsingle | Ointuofsingle => (Tsingle, Tint)
+  | Osingleofint | Osingleofintu => (Tint, Tsingle)
+  | Onegl | Onotl => (Tlong, Tlong)
+  | Ointoflong => (Tlong, Tint)
+  | Olongofint | Olongofintu => (Tint, Tlong)
+  | Olongoffloat | Olonguoffloat => (Tfloat, Tlong)
+  | Ofloatoflong | Ofloatoflongu => (Tlong, Tfloat)
+  | Olongofsingle | Olonguofsingle => (Tsingle, Tlong)
+  | Osingleoflong | Osingleoflongu => (Tlong, Tsingle)
+  end.
+
+Definition type_binop (op: binary_operation) : typ * typ * typ :=
+  match op with
+  | Oadd  | Osub  | Omul  | Odiv  | Odivu  | Omod  | Omodu
+  | Oand  | Oor   | Oxor  | Oshl  | Oshr   | Oshru => (Tint, Tint, Tint)
+  | Oaddf | Osubf | Omulf | Odivf  => (Tfloat, Tfloat, Tfloat)
+  | Oaddfs| Osubfs| Omulfs| Odivfs => (Tsingle, Tsingle, Tsingle)
+  | Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu
+  | Oandl | Oorl  | Oxorl => (Tlong, Tlong, Tlong)
+  | Oshll | Oshrl | Oshrlu => (Tlong, Tint, Tlong)
+  | Ocmp _ | Ocmpu _ => (Tint, Tint, Tint)
+  | Ocmpf _ => (Tfloat, Tfloat, Tint)
+  | Ocmpfs _ => (Tsingle, Tsingle, Tint)
+  | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint)
+  end.
+
+Module RTLtypes <: TYPE_ALGEBRA.
+
+Definition t := typ.
+Definition eq := typ_eq.
+Definition default := Tint.
+
+End RTLtypes.
+
+Module S := UniSolver(RTLtypes).
+
+Definition expect (e: S.typenv) (t1 t2: typ) : res S.typenv :=
+  if typ_eq t1 t2 then OK e else Error (msg "type mismatch").
+
+Fixpoint type_expr (e: S.typenv) (a: expr) (t: typ) : res S.typenv :=
+  match a with
+  | Evar id => S.set e id t
+  | Econst c => expect e (type_constant c) t
+  | Eunop op a1 =>
+      let '(targ1, tres) := type_unop op in
+      do e1 <- type_expr e a1 targ1;
+      expect e1 tres t
+  | Ebinop op a1 a2 =>
+      let '(targ1, targ2, tres) := type_binop op in
+      do e1 <- type_expr e a1 targ1;
+      do e2 <- type_expr e1 a2 targ2;
+      expect e2 tres t
+  | Eload chunk a1 =>
+      do e1 <- type_expr e a1 Tptr;
+      expect e1 (type_of_chunk chunk) t
+  end.
+
+Fixpoint type_exprlist (e: S.typenv) (al: list expr) (tl: list typ) : res S.typenv :=
+  match al, tl with
+  | nil, nil => OK e
+  | a :: al, t :: tl => do e1 <- type_expr e a t; type_exprlist e1 al tl
+  | _, _ => Error (msg "arity mismatch")
+  end.
+
+Definition type_assign (e: S.typenv) (id: ident) (a: expr) : res S.typenv :=
+  match a with
+  | Evar id' =>
+      do (changed, e1) <- S.move e id id'; OK e1
+  | Econst c =>
+      S.set e id (type_constant c)
+  | Eunop op a1 =>
+      let '(targ1, tres) := type_unop op in
+      do e1 <- type_expr e a1 targ1;
+      S.set e1 id tres
+  | Ebinop op a1 a2 =>
+      let '(targ1, targ2, tres) := type_binop op in
+      do e1 <- type_expr e a1 targ1;
+      do e2 <- type_expr e1 a2 targ2;
+      S.set e2 id tres
+  | Eload chunk a1 =>
+      do e1 <- type_expr e a1 Tptr;
+      S.set e1 id (type_of_chunk chunk)
+  end.
+
+Definition opt_set (e: S.typenv) (optid: option ident) (optty: option typ) : res S.typenv :=
+  match optid, optty with
+  | None, _ => OK e
+  | Some id, Some ty => S.set e id ty
+  | _, _ => Error (msg "inconsistent call")
+  end.
+
+Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
+  match s with
+  | Sskip => OK e
+  | Sassign id a => type_assign e id a
+  | Sstore chunk a1 a2 =>
+      do e1 <- type_expr e a1 Tptr; type_expr e1 a2 (type_of_chunk chunk)
+  | Scall optid sg fn args =>
+      do e1 <- type_expr e fn Tptr;
+      do e2 <- type_exprlist e1 args sg.(sig_args);
+      opt_set e2 optid sg.(sig_res)
+  | Stailcall sg fn args =>
+      assertion (opt_typ_eq sg.(sig_res) tret);
+      do e1 <- type_expr e fn Tptr;
+      type_exprlist e1 args sg.(sig_args)
+  | Sbuiltin optid ef args =>
+      let sg := ef_sig ef in
+      do e1 <- type_exprlist e args sg.(sig_args);
+      opt_set e1 optid sg.(sig_res)
+  | Sseq s1 s2 =>
+      do e1 <- type_stmt tret e s1; type_stmt tret e1 s2
+  | Sifthenelse a s1 s2 =>
+      do e1 <- type_expr e a Tint;
+      do e2 <- type_stmt tret e1 s1;
+      type_stmt tret e2 s2
+  | Sloop s1 =>
+      type_stmt tret e s1
+  | Sblock s1 =>
+      type_stmt tret e s1
+  | Sexit n =>
+      OK e
+  | Sswitch sz a tbl dfl =>
+      type_expr e a (if sz then Tlong else Tint)
+  | Sreturn opta =>
+      match tret, opta with
+      | None, None => OK e
+      | Some t, Some a => type_expr e a t
+      | _, _ => Error (msg "inconsistent return")
+      end
+  | Slabel lbl s1 =>
+      type_stmt tret e s1
+  | Sgoto lbl =>
+      OK e
+  end.
+
+Definition typenv := ident -> typ.
+
+Definition type_function (f: function) : res typenv :=
+  do e1 <- S.set_list S.initial f.(fn_params) f.(fn_sig).(sig_args);
+  do e2 <- type_stmt f.(fn_sig).(sig_res) e1 f.(fn_body);
+  S.solve e2.
+
+(** Relational specification of the type system *)
+
+Section SPEC.
+
+Variable env: ident -> typ.
+Variable tret: option typ.
+
+Inductive wt_expr: expr -> typ -> Prop :=
+  | wt_Evar: forall id,
+      wt_expr (Evar id) (env id)
+  | wt_Econst: forall c,
+      wt_expr (Econst c) (type_constant c)
+  | wt_Eunop: forall op a1 targ1 tres,
+      type_unop op = (targ1, tres) ->
+      wt_expr a1 targ1 ->
+      wt_expr (Eunop op a1) tres
+  | wt_Ebinop: forall op a1 a2 targ1 targ2 tres,
+      type_binop op = (targ1, targ2, tres) ->
+      wt_expr a1 targ1 -> wt_expr a2 targ2 ->
+      wt_expr (Ebinop op a1 a2) tres
+  | wt_Eload: forall chunk a1,
+      wt_expr a1 Tptr ->
+      wt_expr (Eload chunk a1) (type_of_chunk chunk).
+
+Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop :=
+  match optid with Some id => optty = Some (env id) | _ => True end.
+
+Inductive wt_stmt: stmt -> Prop :=
+  | wt_Sskip:
+      wt_stmt Sskip
+  | wt_Sassign: forall id a,
+      wt_expr a (env id) ->
+      wt_stmt (Sassign id a)
+  | wt_Sstore: forall chunk a1 a2,
+      wt_expr a1 Tptr -> wt_expr a2 (type_of_chunk chunk) ->
+      wt_stmt (Sstore chunk a1 a2)
+  | wt_Scall: forall optid sg a1 al,
+      wt_expr a1 Tptr -> list_forall2 wt_expr al sg.(sig_args) ->
+      wt_opt_assign optid sg.(sig_res) ->
+      wt_stmt (Scall optid sg a1 al)
+  | wt_Stailcall: forall sg a1 al,
+      wt_expr a1 Tptr -> list_forall2 wt_expr al sg.(sig_args) ->
+      sg.(sig_res) = tret ->
+      wt_stmt (Stailcall sg a1 al)
+  | wt_Sbuiltin: forall optid ef al,
+      list_forall2 wt_expr al (ef_sig ef).(sig_args) ->
+      wt_opt_assign optid (ef_sig ef).(sig_res) ->
+      wt_stmt (Sbuiltin optid ef al)
+  | wt_Sseq: forall s1 s2,
+      wt_stmt s1 -> wt_stmt s2 ->
+      wt_stmt (Sseq s1 s2)
+  | wt_Sifthenelse: forall a s1 s2,
+      wt_expr a Tint -> wt_stmt s1 -> wt_stmt s2 ->
+      wt_stmt (Sifthenelse a s1 s2)
+  | wt_Sloop: forall s1,
+      wt_stmt s1 ->
+      wt_stmt (Sloop s1)
+  | wt_Sblock: forall s1,
+      wt_stmt s1 ->
+      wt_stmt (Sblock s1)
+  | wt_Sexit: forall n,
+      wt_stmt (Sexit n)
+  | wt_Sswitch: forall (sz: bool) a tbl dfl,
+      wt_expr a (if sz then Tlong else Tint) ->
+      wt_stmt (Sswitch sz a tbl dfl)
+  | wt_Sreturn_none:
+      tret = None ->
+      wt_stmt (Sreturn None)
+  | wt_Sreturn_some: forall a t,
+      tret = Some t -> wt_expr a t ->
+      wt_stmt (Sreturn (Some a))
+  | wt_Slabel: forall lbl s1,
+      wt_stmt s1 ->
+      wt_stmt (Slabel lbl s1)
+  | wt_Sgoto: forall lbl,
+      wt_stmt (Sgoto lbl).
+
+End SPEC.
+
+Inductive wt_function (env: typenv) (f: function) : Prop :=
+  wt_function_intro:
+    type_function f = OK env ->     (**r to ensure uniqueness of [env] *)
+    List.map env f.(fn_params) = f.(fn_sig).(sig_args) ->
+    wt_stmt env f.(fn_sig).(sig_res) f.(fn_body) ->
+    wt_function env f.
+
+Inductive wt_fundef: fundef -> Prop :=
+  | wt_fundef_internal: forall env f,
+      wt_function env f ->
+      wt_fundef (Internal f)
+  | wt_fundef_external: forall ef,
+      wt_fundef (External ef).
+
+Definition wt_program (p: program): Prop :=
+  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
+
+(** Soundness of type inference *)
+
+Lemma expect_incr: forall te e t1 t2 e',
+  expect e t1 t2 = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto.
+Qed.
+Hint Resolve expect_incr: ty.
+
+Lemma expect_sound: forall e t1 t2 e',
+  expect e t1 t2 = OK e' -> t1 = t2.
+Proof.
+  unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto.
+Qed.
+
+Lemma type_expr_incr: forall te a t e e',
+  type_expr e a t = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  induction a; simpl; intros until e'; intros T SAT; try (monadInv T); eauto with ty.
+- destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
+- destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
+Qed.
+Hint Resolve type_expr_incr: ty.
+
+Lemma type_expr_sound: forall te a t e e',
+    type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t.
+Proof.
+  induction a; simpl; intros until e'; intros T SAT; try (monadInv T).
+- erewrite <- S.set_sound by eauto. constructor.
+- erewrite <- expect_sound by eauto. constructor.
+- destruct (type_unop u) as [targ1 tres] eqn:TU; monadInv T.
+  erewrite <- expect_sound by eauto. econstructor; eauto with ty.
+- destruct (type_binop b) as [[targ1 targ2] tres] eqn:TB; monadInv T.
+  erewrite <- expect_sound by eauto. econstructor; eauto with ty.
+- erewrite <- expect_sound by eauto. econstructor; eauto with ty.
+Qed.
+
+Lemma type_exprlist_incr: forall te al tl e e',
+  type_exprlist e al tl = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T; eauto with ty.
+Qed.
+Hint Resolve type_exprlist_incr: ty.
+
+Lemma type_exprlist_sound: forall te al tl e e',
+    type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl.
+Proof.
+  induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T.
+- constructor.
+- constructor; eauto using type_expr_sound with ty.
+Qed.
+
+Lemma type_assign_incr: forall te id a e e',
+    type_assign e id a = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  induction a; simpl; intros until e'; intros T SAT; try (monadInv T); eauto with ty.
+- destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
+- destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
+Qed.
+Hint Resolve type_assign_incr: ty.
+
+Lemma type_assign_sound: forall te id a e e',
+    type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id).
+Proof.
+  induction a; simpl; intros until e'; intros T SAT; try (monadInv T).
+- erewrite S.move_sound by eauto. constructor.
+- erewrite S.set_sound by eauto. constructor.
+- destruct (type_unop u) as [targ1 tres] eqn:TU; monadInv T.
+  erewrite S.set_sound by eauto. econstructor; eauto using type_expr_sound with ty.
+- destruct (type_binop b) as [[targ1 targ2] tres] eqn:TB; monadInv T.
+  erewrite S.set_sound by eauto. econstructor; eauto using type_expr_sound with ty.
+- erewrite S.set_sound by eauto. econstructor; eauto using type_expr_sound with ty.
+Qed.
+
+Lemma opt_set_incr: forall te optid optty e e',
+    opt_set e optid optty = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  unfold opt_set; intros. destruct optid, optty; try (monadInv H); eauto with ty.
+Qed.
+Hint Resolve opt_set_incr: ty.
+
+Lemma opt_set_sound: forall te optid optty e e',
+    opt_set e optid optty = OK e' -> S.satisf te e' -> wt_opt_assign te optid optty.
+Proof.
+  unfold opt_set; intros; red. destruct optid; [destruct optty |]; try (monadInv H).
+- erewrite S.set_sound by eauto. auto.
+- auto.
+Qed.
+
+Lemma type_stmt_incr: forall te tret s e e',
+    type_stmt tret e s = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  induction s; simpl; intros e1 e2 T SAT; try (monadInv T); eauto with ty.
+- destruct tret, o; try (monadInv T); eauto with ty.
+Qed.
+Hint Resolve type_stmt_incr: ty.
+
+Lemma type_stmt_sound: forall te tret s e e',
+    type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s.
+Proof.
+  induction s; simpl; intros e1 e2 T SAT; try (monadInv T).
+- constructor.
+- constructor; eauto using type_assign_sound.
+- constructor; eauto using type_expr_sound with ty.
+- constructor; eauto using type_expr_sound, type_exprlist_sound, opt_set_sound with ty.
+- constructor; eauto using type_expr_sound, type_exprlist_sound with ty.
+- constructor; eauto using type_exprlist_sound, opt_set_sound with ty.
+- constructor; eauto with ty.
+- constructor; eauto using type_expr_sound with ty.
+- constructor; eauto.
+- constructor; eauto.
+- constructor.
+- constructor; eauto using type_expr_sound with ty.
+- destruct tret, o; try (monadInv T); econstructor; eauto using type_expr_sound with ty.
+- constructor; eauto.
+- constructor.
+Qed.
+
+Theorem type_function_sound: forall f env,
+  type_function f = OK env -> wt_function env f.
+Proof.
+  intros. generalize H; unfold type_function; intros T; monadInv T.
+  assert (S.satisf env x0) by (apply S.solve_sound; auto).
+  constructor; eauto using S.set_list_sound, type_stmt_sound with ty.
+Qed.
+
+(** Semantic soundness *)
+
+Definition wt_env (env: typenv) (e: Cminor.env) : Prop :=
+  forall id v, e!id = Some v -> Val.has_type v (env id).
+
+Definition def_env (f: function) (e: Cminor.env) : Prop :=
+  forall id, In id f.(fn_params) \/ In id f.(fn_vars) -> exists v, e!id = Some v.
+
+Inductive wt_cont_call: cont -> option typ -> Prop :=
+  | wt_cont_Kstop:
+      wt_cont_call Kstop (Some Tint)
+  | wt_cont_Kcall: forall optid f sp e k tret env
+        (WT_FN: wt_function env f)
+        (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k)
+        (WT_ENV: wt_env env e)
+        (DEF_ENV: def_env f e)
+        (WT_DEST: wt_opt_assign env optid tret),
+      wt_cont_call (Kcall optid f sp e k) tret
+
+with wt_cont: typenv -> option typ -> cont -> Prop :=
+  | wt_cont_Kseq: forall env tret s k,
+      wt_stmt env tret s ->
+      wt_cont env tret k ->
+      wt_cont env tret (Kseq s k)
+  | wt_cont_Kblock: forall env tret k,
+      wt_cont env tret k ->
+      wt_cont env tret (Kblock k)
+  | wt_cont_other: forall env tret k,
+      wt_cont_call k tret ->
+      wt_cont env tret k.
+
+Inductive wt_state: state -> Prop :=
+  | wt_normal_state: forall f s k sp e m env
+        (WT_FN: wt_function env f)
+        (WT_STMT: wt_stmt env f.(fn_sig).(sig_res) s)
+        (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k)
+        (WT_ENV: wt_env env e)
+        (DEF_ENV: def_env f e),
+      wt_state (State f s k sp e m)
+  | wt_call_state: forall f args k m
+        (WT_FD: wt_fundef f)
+        (WT_ARGS: Val.has_type_list args (funsig f).(sig_args))
+        (WT_CONT: wt_cont_call k (funsig f).(sig_res)),
+      wt_state (Callstate f args k m)
+  | wt_return_state: forall v k m tret
+        (WT_RES: Val.has_type v (match tret with None => Tint | Some t => t end))
+        (WT_CONT: wt_cont_call k tret),
+      wt_state (Returnstate v k m).
+
+Lemma wt_is_call_cont:
+  forall env tret k, wt_cont env tret k -> is_call_cont k -> wt_cont_call k tret.
+Proof.
+  destruct 1; intros ICC; contradiction || auto.
+Qed.
+
+Lemma call_cont_wt:
+  forall env tret k, wt_cont env tret k -> wt_cont_call (call_cont k) tret.
+Proof.
+  induction 1; simpl; auto. inversion H; subst; auto.
+Qed.
+
+Lemma wt_env_assign: forall env id e v,
+  wt_env env e -> Val.has_type v (env id) -> wt_env env (PTree.set id v e).
+Proof.
+  intros; red; intros. rewrite PTree.gsspec in H1; destruct (peq id0 id).
+- congruence.
+- auto.
+Qed.
+
+Lemma def_env_assign: forall f e id v,
+  def_env f e -> def_env f (PTree.set id v e).
+Proof.
+  intros; red; intros i IN. rewrite PTree.gsspec. destruct (peq i id).
+  exists v; auto.
+  auto.
+Qed.
+
+Lemma wt_env_set_params: forall env il vl,
+  Val.has_type_list vl (map env il) -> wt_env env (set_params vl il).
+Proof.
+  induction il as [ | i il]; destruct vl as [ | vl]; simpl; intros; try contradiction.
+- red; intros. rewrite PTree.gempty in H0; discriminate.
+- destruct H. apply wt_env_assign; auto.
+Qed.
+
+Lemma def_set_params: forall id il vl,
+  In id il -> exists v, PTree.get id (set_params vl il) = Some v.
+Proof.
+  induction il as [ | i il]; simpl; intros.
+- contradiction.
+- destruct vl as [ | v vl]; rewrite PTree.gsspec; destruct (peq id i).
+  econstructor; eauto.
+  apply IHil; intuition congruence.
+  econstructor; eauto.
+  apply IHil; intuition congruence.
+Qed.
+
+Lemma wt_env_set_locals: forall env il e,
+  wt_env env e -> wt_env env (set_locals il e).
+Proof.
+  induction il as [ | i il]; simpl; intros.
+- auto.
+- apply wt_env_assign; auto. exact I.
+Qed.
+
+Lemma def_set_locals: forall id il e,
+  (exists v, PTree.get id e = Some v) \/ In id il ->
+  exists v, PTree.get id (set_locals il e) = Some v.
+Proof.
+  induction il as [ | i il]; simpl; intros.
+- tauto.
+- rewrite PTree.gsspec; destruct (peq id i).
+  econstructor; eauto.
+  apply IHil; intuition congruence.
+Qed.
+
+Lemma wt_find_label: forall env tret lbl s k,
+  wt_stmt env tret s -> wt_cont env tret k ->
+  match find_label lbl s k with
+  | Some (s', k') => wt_stmt env tret s' /\ wt_cont env tret k'
+  | None => True
+  end.
+Proof.
+  induction s; intros k WS WK; simpl; auto.
+- inv WS. assert (wt_cont env tret (Kseq s2 k)) by (constructor; auto).
+  specialize (IHs1 _ H1 H). destruct (find_label lbl s1 (Kseq s2 k)).
+  auto. apply IHs2; auto.
+- inv WS. specialize (IHs1 _ H3 WK). destruct (find_label lbl s1 k).
+  auto. apply IHs2; auto.
+- inversion WS; subst. apply IHs; auto. constructor; auto.
+- inv WS. apply IHs; auto. constructor; auto.
+- inv WS. destruct (ident_eq lbl l). auto. apply IHs; auto.
+Qed.
+
+Section SUBJECT_REDUCTION.
+
+Variable p: program.
+
+Hypothesis wt_p: wt_program p.
+
+Let ge := Genv.globalenv p.
+
+Ltac VHT :=
+  match goal with
+  | [ |- Val.has_type (if Archi.ptr64 then _ else _) _] => unfold Val.has_type; destruct Archi.ptr64 eqn:?; VHT
+  | [ |- Val.has_type (match ?v with _ => _ end) _] => destruct v; VHT
+  | [ |- Val.has_type (Vptr _ _) Tptr ] => apply Val.Vptr_has_type
+  | [ |- Val.has_type _ _ ] => exact I
+  | [ |- Val.has_type (?f _ _ _ _ _) _ ] => unfold f; VHT
+  | [ |- Val.has_type (?f _ _ _ _) _ ] => unfold f; VHT
+  | [ |- Val.has_type (?f _ _) _ ] => unfold f; VHT
+  | [ |- Val.has_type (?f _ _ _) _ ] => unfold f; VHT
+  | [ |- Val.has_type (?f _) _ ] => unfold f; VHT
+  | [ |- True ] => exact I
+  | [ |- ?x = ?x ] => reflexivity
+  | _ => idtac
+  end.
+
+Ltac VHT' :=
+  match goal with
+  | [ H: None = Some _ |- _ ] => discriminate
+  | [ H: Some _ = Some _ |- _ ] => inv H; VHT
+  | [ H: match ?x with _ => _ end = Some _ |- _ ] => destruct x; VHT'
+  | [ H: ?f _ _ _ _ = Some _ |- _ ] => unfold f in H; VHT'
+  | [ H: ?f _ _ _ = Some _ |- _ ] => unfold f in H; VHT'
+  | [ H: ?f _ _ = Some _ |- _ ] => unfold f in H; VHT'
+  | [ H: ?f _ = Some _ |- _ ] => unfold f in H; VHT'
+  | _ => idtac
+  end.
+
+Lemma type_constant_sound: forall sp cst v,
+  eval_constant ge sp cst = Some v ->
+  Val.has_type v (type_constant cst).
+Proof.
+  intros until v; intros EV. destruct cst; simpl in *; inv EV; VHT.
+Qed.
+
+Lemma type_unop_sound: forall op v1 v,
+  eval_unop op v1 = Some v -> Val.has_type v (snd (type_unop op)).
+Proof.
+  unfold eval_unop; intros op v1 v EV; destruct op; simpl; VHT'.
+Qed.
+
+Lemma type_binop_sound: forall op v1 v2 m v,
+  eval_binop op v1 v2 m = Some v -> Val.has_type v (snd (type_binop op)).
+Proof.
+  unfold eval_binop; intros op v1 v2 m v EV; destruct op; simpl; VHT';
+  destruct (eq_block b b0); VHT.
+Qed.
+
+Lemma wt_eval_expr: forall env sp e m a v,
+  eval_expr ge sp e m a v ->
+  forall t,
+  wt_expr env a t ->
+  wt_env env e ->
+  Val.has_type v t.
+Proof.
+  induction 1; intros t WT ENV.
+- inv WT. apply ENV; auto.
+- inv WT. eapply type_constant_sound; eauto.
+- inv WT. replace t with (snd (type_unop op)) by (rewrite H3; auto). eapply type_unop_sound; eauto.
+- inv WT. replace t with (snd (type_binop op)) by (rewrite H5; auto). eapply type_binop_sound; eauto.
+- inv WT. destruct vaddr; try discriminate. eapply Mem.load_type; eauto.
+Qed.
+
+Lemma wt_eval_exprlist: forall env sp e m al vl,
+  eval_exprlist ge sp e m al vl ->
+  forall tl,
+  list_forall2 (wt_expr env) al tl ->
+  wt_env env e ->
+  Val.has_type_list vl tl.
+Proof.
+  induction 1; intros tl WT ENV; inv WT; simpl.
+- auto.
+- split. eapply wt_eval_expr; eauto. eauto.
+Qed.
+
+Lemma wt_find_funct: forall v fd,
+  Genv.find_funct ge v = Some fd -> wt_fundef fd.
+Proof.
+  intros. eapply Genv.find_funct_prop; eauto.
+Qed.
+
+Lemma subject_reduction:
+  forall st1 t st2, step ge st1 t st2 ->
+  forall (WT: wt_state st1), wt_state st2.
+Proof.
+  destruct 1; intros; inv WT.
+- inv WT_CONT. econstructor; eauto. inv H.
+- inv WT_CONT. econstructor; eauto. inv H.
+- econstructor; eauto using wt_is_call_cont. exact I.
+- inv WT_STMT. econstructor; eauto using wt_Sskip.
+  apply wt_env_assign; auto. eapply wt_eval_expr; eauto.
+  apply def_env_assign; auto.
+- econstructor; eauto using wt_Sskip.
+- inv WT_STMT. econstructor; eauto.
+  eapply wt_find_funct; eauto.
+  eapply wt_eval_exprlist; eauto.
+  econstructor; eauto.
+- inv WT_STMT. econstructor; eauto.
+  eapply wt_find_funct; eauto.
+  eapply wt_eval_exprlist; eauto.
+  rewrite H8; eapply call_cont_wt; eauto.
+- inv WT_STMT. exploit external_call_well_typed; eauto. intros TRES.
+  econstructor; eauto using wt_Sskip.
+  unfold proj_sig_res in TRES; red in H5.
+  destruct optid. rewrite H5 in TRES. apply wt_env_assign; auto. assumption.
+  destruct optid. apply def_env_assign; auto. assumption.
+- inv WT_STMT. econstructor; eauto. econstructor; eauto.
+- inv WT_STMT. destruct b; econstructor; eauto.
+- inv WT_STMT. econstructor; eauto. econstructor; eauto. constructor; auto.
+- inv WT_STMT. econstructor; eauto. econstructor; eauto.
+- inv WT_CONT. econstructor; eauto. inv H.
+- inv WT_CONT. econstructor; eauto using wt_Sskip. inv H.
+- inv WT_CONT. econstructor; eauto using wt_Sexit. inv H.
+- econstructor; eauto using wt_Sexit.
+- inv WT_STMT. econstructor; eauto using call_cont_wt. rewrite H0; exact I.
+- inv WT_STMT. econstructor; eauto using call_cont_wt.
+  rewrite H2. eapply wt_eval_expr; eauto.
+- inv WT_STMT. econstructor; eauto.
+- inversion WT_FN; subst.
+  assert (WT_CK: wt_cont env (sig_res (fn_sig f)) (call_cont k)).
+  { constructor. eapply call_cont_wt; eauto. }
+  generalize (wt_find_label _ _ lbl _ _ H2 WT_CK).
+  rewrite H. intros [WT_STMT' WT_CONT']. econstructor; eauto.
+- inv WT_FD. inversion H1; subst. econstructor; eauto.
+  constructor; auto.
+  apply wt_env_set_locals. apply wt_env_set_params. rewrite H2; auto.
+  red; intros. apply def_set_locals. destruct H4; auto. left; apply def_set_params; auto.
+- exploit external_call_well_typed; eauto. unfold proj_sig_res. simpl in *. intros.
+  econstructor; eauto.
+- inv WT_CONT. econstructor; eauto using wt_Sskip.
+  red in WT_DEST.
+  destruct optid. rewrite WT_DEST in WT_RES. apply wt_env_assign; auto. assumption.
+  destruct optid. apply def_env_assign; auto. assumption.
+Qed.
+
+Lemma subject_reduction_star:
+  forall st1 t st2, star step ge st1 t st2 ->
+  forall (WT: wt_state st1), wt_state st2.
+Proof.
+  induction 1; eauto using subject_reduction.
+Qed.
+
+
+Lemma wt_initial_state:
+  forall S, initial_state p S -> wt_state S.
+Proof.
+  intros. inv H. constructor. eapply Genv.find_funct_ptr_prop; eauto.
+  rewrite H3; constructor.
+  rewrite H3; constructor.
+Qed.
+
+End SUBJECT_REDUCTION.
diff --git a/backend/Ifconv.v b/backend/Ifconv.v
new file mode 100644
index 00000000..0c9c5b5c
--- /dev/null
+++ b/backend/Ifconv.v
@@ -0,0 +1,129 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Coqlib Maps Errors.
+Require Import AST Events Cminor.
+Require Import Cminortyping.
+
+Definition tyenv := ident -> typ.
+Definition known_idents := PTree.t unit.
+
+Definition is_known (ki: known_idents) (id: ident) :=
+  match ki!id with Some _ => true | None => false end.
+
+Definition safe_unop (op: unary_operation) : bool :=
+  match op with
+  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => false
+  | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => false
+  | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => false
+  | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => false
+  | _ => true
+  end.
+
+Definition safe_binop (op: binary_operation) : bool :=
+  match op with
+  | Odiv | Odivu | Omod | Omodu => false
+  | Odivl | Odivlu | Omodl | Omodlu => false
+  | Ocmpl _ | Ocmplu _ => false
+  | _ => true
+  end.
+
+Fixpoint safe_expr (ki: known_idents) (a: expr) : bool :=
+  match a with
+  | Evar v => is_known ki v
+  | Econst c => true
+  | Eunop op e1 => safe_unop op && safe_expr ki e1
+  | Ebinop op e1 e2 => safe_binop op && safe_expr ki e1 && safe_expr ki e2
+  | Eload chunk e => false
+  end.
+
+Definition Sselection (id: ident) (ty: typ) (cond ifso ifnot: expr) : stmt :=
+  Sbuiltin (Some id) (EF_select ty) (cond :: ifso :: ifnot :: nil).
+
+Inductive stmt_class : Type :=
+  | SCskip
+  | SCassign (id: ident) (a: expr)
+  | SCother.
+
+Function classify_stmt (s: stmt) : stmt_class :=
+  match s with
+  | Sskip => SCskip
+  | Sassign id a => SCassign id a
+  | Sseq Sskip s => classify_stmt s
+  | Sseq s Sskip => classify_stmt s
+  | _ => SCother
+  end.
+
+Definition if_conversion_base
+      (ki: known_idents) (env: tyenv)
+      (cond: expr) (id: ident) (ifso ifnot: expr) : option stmt :=
+  if is_known ki id && safe_expr ki ifso && safe_expr ki ifnot
+  then Some (Sselection id (env id) cond ifso ifnot)
+  else None.
+
+Definition if_conversion
+      (ki: known_idents) (env: tyenv)
+      (cond: expr) (ifso ifnot: stmt) : option stmt :=
+  match classify_stmt ifso, classify_stmt ifnot with
+  | SCskip, SCassign id a =>
+      if_conversion_base ki env cond id (Evar id) a
+  | SCassign id a, SCskip =>
+      if_conversion_base ki env cond id a (Evar id)
+  | SCassign id1 a1, SCassign id2 a2 =>
+      if ident_eq id1 id2 then if_conversion_base ki env cond id1 a1 a2 else None
+  | _, _ => None
+  end.
+
+Fixpoint transf_stmt (ki: known_idents) (env: tyenv) (s: stmt) : stmt :=
+  match s with
+  | Sskip => s
+  | Sassign _ _ => s
+  | Sstore _ _ _ => s
+  | Scall _ _ _ _ => s
+  | Stailcall _ _ _ => s
+  | Sbuiltin _ _ _ => s
+  | Sseq s1 s2 => Sseq (transf_stmt ki env s1) (transf_stmt ki env s2)
+  | Sifthenelse e s1 s2 =>
+      match if_conversion ki env e s1 s2 with
+      | Some s => s
+      | None => Sifthenelse e (transf_stmt ki env s1) (transf_stmt ki env s2)
+      end
+  | Sloop s1 => Sloop (transf_stmt ki env s1)
+  | Sblock s1 => Sblock (transf_stmt ki env s1)
+  | Sexit _ => s
+  | Sswitch _ _ _ _ => s
+  | Sreturn _ => s
+  | Slabel lbl s1 => Slabel lbl (transf_stmt ki env s1)
+  | Sgoto _ => s
+  end.
+
+Definition known_id (f: function) : known_idents :=
+  let add (ki: known_idents) (id: ident) := PTree.set id tt ki in
+  List.fold_left add f.(fn_vars)
+      (List.fold_left add f.(fn_params) (PTree.empty unit)).
+
+Local Open Scope error_monad_scope.
+
+Definition transf_function (f: function) : res function :=
+  let ki := known_id f in
+  do env <- type_function f;
+  OK (mkfunction f.(fn_sig) f.(fn_params) f.(fn_vars) f.(fn_stackspace)
+                 (transf_stmt ki env f.(fn_body))).
+
+Definition transf_fundef (fd: fundef) : res fundef :=
+  transf_partial_fundef transf_function fd.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
diff --git a/backend/Ifconvproof.v b/backend/Ifconvproof.v
new file mode 100644
index 00000000..9e14ce2f
--- /dev/null
+++ b/backend/Ifconvproof.v
@@ -0,0 +1,590 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Recdef Coqlib Maps Errors.
+Require Import AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Cminor Cminortyping Ifconv.
+
+Definition match_prog (prog tprog: program) :=
+  match_program (fun cu f tf => transf_fundef f = OK tf) eq prog tprog.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. apply match_transform_partial_program; auto.
+Qed.
+
+Lemma known_id_sound_1:
+  forall f id x, (known_id f)!id = Some x -> In id f.(fn_params) \/ In id f.(fn_vars).
+Proof.
+  unfold known_id.
+  set (add := fun (ki: known_idents) (id: ident) => PTree.set id tt ki).
+  intros.
+  assert (REC: forall l ki, (fold_left add l ki)!id = Some x -> In id l \/ ki!id = Some x).
+  { induction l as [ | i l ]; simpl; intros.
+    - auto.
+    - apply IHl in H0. destruct H0; auto. unfold add in H0; rewrite PTree.gsspec in H0.
+      destruct (peq id i); auto. }
+  apply REC in H. destruct H; auto. apply REC in H. destruct H; auto.
+  rewrite PTree.gempty in H; discriminate.
+Qed.
+
+Lemma known_id_sound_2:
+  forall f id, is_known (known_id f) id = true -> In id f.(fn_params) \/ In id f.(fn_vars).
+Proof.
+  unfold is_known; intros. destruct (known_id f)!id eqn:E; try discriminate.
+  eapply known_id_sound_1; eauto.
+Qed.
+
+Lemma eval_safe_expr:
+  forall ge f sp e m a,
+  def_env f e ->
+  safe_expr (known_id f) a = true ->
+  exists v, eval_expr ge sp e m a v.
+Proof.
+  induction a; simpl; intros.
+  - apply known_id_sound_2 in H0.
+    destruct (H i H0) as [v E].
+    exists v; constructor; auto.
+  - destruct (eval_constant ge sp c) as [v|] eqn:E.
+    exists v; constructor; auto.
+    destruct c; discriminate.
+  - InvBooleans. destruct IHa as [v1 E1]; auto.
+    destruct (eval_unop u v1) as [v|] eqn:E.
+    exists v; econstructor; eauto.
+    destruct u; discriminate.
+  - InvBooleans.
+    destruct IHa1 as [v1 E1]; auto.
+    destruct IHa2 as [v2 E2]; auto.
+    destruct (eval_binop b v1 v2 m) as [v|] eqn:E.
+    exists v; econstructor; eauto.
+    destruct b; discriminate.
+  - discriminate.
+Qed.
+
+Lemma step_selection:
+  forall ge f id ty cond a1 a2 k sp e m v0 b v1 v2,
+  eval_expr ge sp e m cond v0 -> Val.bool_of_val v0 b ->
+  eval_expr ge sp e m a1 v1 ->
+  eval_expr ge sp e m a2 v2 ->
+  Val.has_type v1 ty -> Val.has_type v2 ty ->
+  step ge (State f (Sselection id ty cond a1 a2) k sp e m)
+       E0 (State f Sskip k sp (PTree.set id (if b then v1 else v2) e) m).
+Proof.
+  unfold Sselection; intros.
+  eapply step_builtin with (optid := Some id).
+  eauto 6 using eval_Enil, eval_Econs.
+  replace (if b then v1 else v2) with (Val.select (Some b) v1 v2 ty).
+  constructor; auto.
+  destruct b; apply Val.normalize_idem; auto.
+Qed.
+
+Section PRESERVATION.
+
+Variable prog: program.
+Variable tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma wt_prog : wt_program prog.
+Proof.
+  red; intros.
+  destruct TRANSL as [A _].
+  exploit list_forall2_in_left; eauto.
+  intros ((i' & gd') & B & (C & D)). simpl in *. inv D.
+  destruct f; monadInv H2.
+- monadInv EQ. econstructor; apply type_function_sound; eauto.
+- constructor.
+Qed.
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSL).
+
+Lemma function_ptr_translated:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+Proof
+  (Genv.find_funct_ptr_transf_partial TRANSL).
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  exists tf,
+  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
+Proof
+  (Genv.find_funct_transf_partial TRANSL).
+
+Lemma sig_transf_function:
+  forall f tf,
+  transf_fundef f = OK tf ->
+  funsig tf = funsig f.
+Proof.
+  unfold transf_fundef, transf_partial_fundef; intros. destruct f.
+- monadInv H. monadInv EQ. auto.
+- inv H. auto.
+Qed.
+
+Lemma stackspace_transf_function:
+  forall f tf,
+  transf_function f = OK tf ->
+  tf.(fn_stackspace) = f.(fn_stackspace).
+Proof.
+  intros. monadInv H. auto.
+Qed.
+
+Lemma eval_expr_preserved:
+  forall sp e m a v, eval_expr ge sp e m a v -> eval_expr tge sp e m a v.
+Proof.
+  induction 1; econstructor; eauto.
+  destruct cst; auto.
+  simpl in *. unfold Genv.symbol_address in *. rewrite symbols_preserved. auto.
+Qed.
+
+Lemma eval_exprlist_preserved:
+  forall sp e m al vl, eval_exprlist ge sp e m al vl -> eval_exprlist tge sp e m al vl.
+Proof.
+  induction 1; econstructor; eauto using eval_expr_preserved.
+Qed.
+
+(*
+Lemma classify_stmt_sound:
+  forall f sp e m s,
+    match classify_stmt s with
+    | SCskip =>
+        forall k, star step ge (State f s k sp e m) E0 (State f Sskip k sp e m)
+    | SCassign id a =>
+        forall k v,
+        eval_expr ge sp e m a v ->
+        star step ge (State f s k sp e m) E0 (State f Sskip k sp (PTree.set id v e) m)
+    | SCother => True
+    end.
+Proof.
+  intros until s; functional induction (classify_stmt s).
+  - intros; apply star_refl.
+  - intros; apply star_one; constructor; auto.
+  - assert (A: forall k, star step ge (State f (Sseq Sskip s0) k sp e m)
+                              E0 (State f s0 k sp e m)).
+    { intros. eapply star_two; constructor. }
+    destruct (classify_stmt s0); auto;
+    intros; (eapply star_trans; [apply A| auto | reflexivity]).
+  - destruct (classify_stmt s0); auto.
+    + intros. eapply star_left. constructor. eapply star_right.
+      apply IHs0. constructor. eauto. eauto.
+    + intros. eapply star_left. constructor. eapply star_right.
+      apply IHs0. eauto. constructor. eauto. eauto.
+  - auto.
+Qed.
+*)
+
+Lemma classify_stmt_sound_1:
+  forall f sp e m s k,
+  classify_stmt s = SCskip ->
+  star step ge (State f s k sp e m) E0 (State f Sskip k sp e m).
+Proof.
+  intros until s; functional induction (classify_stmt s); intros; try discriminate.
+  - apply star_refl.
+  - eapply star_trans; eauto. eapply star_two. constructor. constructor.
+    traceEq. traceEq.
+  - eapply star_left. constructor.
+    eapply star_right. eauto. constructor.
+    traceEq. traceEq.
+Qed.
+
+Lemma classify_stmt_sound_2:
+  forall f sp e m a id v,
+  eval_expr ge sp e m a v ->
+  forall s k,
+  classify_stmt s = SCassign id a ->
+  star step ge (State f s k sp e m) E0 (State f Sskip k sp (PTree.set id v e) m).
+Proof.
+  intros until s; functional induction (classify_stmt s); intros; try discriminate.
+  - inv H0. apply star_one. constructor; auto.
+  - eapply star_trans; eauto. eapply star_two. constructor. constructor.
+    traceEq. traceEq.
+  - eapply star_left. constructor.
+    eapply star_right. eauto. constructor.
+    traceEq. traceEq.
+Qed.
+
+Lemma classify_stmt_wt_2:
+  forall env tyret id a s,
+  classify_stmt s = SCassign id a ->
+  wt_stmt env tyret s ->
+  wt_expr env a (env id).
+Proof.
+  intros until s; functional induction (classify_stmt s); intros CL WT;
+  try discriminate.
+- inv CL; inv WT; auto.
+- inv WT; eauto.
+- inv WT; eauto.
+Qed.
+
+Lemma if_conversion_sound:
+  forall f env cond ifso ifnot s vb b k f' k' sp e m,
+  if_conversion (known_id f) env cond ifso ifnot = Some s ->
+  def_env f e -> wt_env env e ->
+  wt_stmt env f.(fn_sig).(sig_res) ifso ->
+  wt_stmt env f.(fn_sig).(sig_res) ifnot ->
+  eval_expr ge sp e m cond vb -> Val.bool_of_val vb b ->
+  let s0 := if b then ifso else ifnot in
+  exists e1,
+     step tge (State f' s k' sp e m) E0 (State f' Sskip k' sp e1 m)
+  /\ star step ge (State f s0 k sp e m) E0 (State f Sskip k sp e1 m).
+Proof.
+  unfold if_conversion; intros until m; intros IFC DE WTE WT1 WT2 EVC BOV.
+  set (s0 := if b then ifso else ifnot). set (ki := known_id f) in *.
+  destruct (classify_stmt ifso) eqn:IFSO; try discriminate;
+  destruct (classify_stmt ifnot) eqn:IFNOT; try discriminate;
+  unfold if_conversion_base in IFC.
+  - destruct (is_known ki id && safe_expr ki (Evar id) && safe_expr ki a) eqn:B; inv IFC.
+    InvBooleans.
+    destruct (eval_safe_expr ge f sp e m (Evar id)) as (v1 & EV1); auto.
+    destruct (eval_safe_expr ge f sp e m a) as (v2 & EV2); auto.
+    assert (Val.has_type v1 (env id)).
+    { eapply wt_eval_expr; eauto using wt_prog. constructor. }
+    assert (Val.has_type v2 (env id)).
+    { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. }
+    econstructor; split.
+    eapply step_selection; eauto using eval_expr_preserved.
+    unfold s0; destruct b.
+    rewrite PTree.gsident by (inv EV1; auto). apply classify_stmt_sound_1; auto.
+    eapply classify_stmt_sound_2; eauto.
+  - destruct (is_known ki id && safe_expr ki a && safe_expr ki (Evar id)) eqn:B; inv IFC.
+    InvBooleans.
+    destruct (eval_safe_expr ge f sp e m a) as (v1 & EV1); auto.
+    destruct (eval_safe_expr ge f sp e m (Evar id)) as (v2 & EV2); auto.
+    assert (Val.has_type v1 (env id)).
+    { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. }
+    assert (Val.has_type v2 (env id)).
+    { eapply wt_eval_expr; eauto using wt_prog. constructor. }
+    econstructor; split.
+    eapply step_selection; eauto using eval_expr_preserved.
+    unfold s0; destruct b.
+    eapply classify_stmt_sound_2; eauto.
+    rewrite PTree.gsident by (inv EV2; auto). apply classify_stmt_sound_1; auto.
+  - destruct (ident_eq id id0); try discriminate. subst id0.
+    destruct (is_known ki id && safe_expr ki a && safe_expr ki a0) eqn:B; inv IFC.
+    InvBooleans.
+    destruct (eval_safe_expr ge f sp e m a) as (v1 & EV1); auto.
+    destruct (eval_safe_expr ge f sp e m a0) as (v2 & EV2); auto.
+    assert (Val.has_type v1 (env id)).
+    { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. }
+    assert (Val.has_type v2 (env id)).
+    { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. }
+    econstructor; split.
+    eapply step_selection; eauto using eval_expr_preserved.
+    unfold s0; destruct b; eapply classify_stmt_sound_2; eauto.
+Qed.
+
+Inductive match_cont: known_idents -> typenv -> cont -> cont -> Prop :=
+  | match_cont_seq: forall ki env s k k',
+      match_cont ki env k k' ->
+      match_cont ki env (Kseq s k) (Kseq (transf_stmt ki env s) k')
+  | match_cont_block: forall ki env k k',
+      match_cont ki env k k' ->
+      match_cont ki env (Kblock k) (Kblock k')
+  | match_cont_call: forall ki env k k',
+      match_call_cont k k' ->
+      match_cont ki env k k'
+
+with match_call_cont: cont -> cont -> Prop :=
+  | match_call_cont_stop:
+      match_call_cont Kstop Kstop
+  | match_call_cont_base: forall optid f sp e k f' k' env
+        (WT_FN: type_function f = OK env)
+        (TR_FN: transf_function f = OK f')
+        (CONT: match_cont (known_id f) env k k'),
+      match_call_cont (Kcall optid f sp e k)
+                      (Kcall optid f' sp e k').
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_gen: forall f s k sp e m f' s' env k'
+        (WT_FN: type_function f = OK env)
+        (TR_FN: transf_function f = OK f')
+        (TR_STMT: transf_stmt (known_id f) env s = s')
+        (CONT: match_cont (known_id f) env k k'),
+      match_states (State f s k sp e m)
+                   (State f' s' k' sp e m)
+  | match_states_call: forall f args k m f' k'
+        (TR_FN: transf_fundef f = OK f')
+        (CONT: match_call_cont k k'),
+      match_states (Callstate f args k m)
+                   (Callstate f' args k' m)
+  | match_states_return: forall v k m k'
+        (CONT: match_call_cont k k'),
+      match_states (Returnstate v k m)
+                   (Returnstate v k' m).
+
+Lemma match_cont_is_call_cont:
+  forall ki env k k',
+  match_cont ki env k k' -> is_call_cont k -> is_call_cont k' /\ match_call_cont k k'.
+Proof.
+  destruct 1; intros; try contradiction.  split; auto. inv H; exact I.
+Qed.
+
+Lemma match_cont_call_cont:
+  forall ki env k k',
+  match_cont ki env k k' -> match_call_cont (call_cont k) (call_cont k').
+Proof.
+  induction 1; auto. inversion H; subst; auto.
+Qed.
+
+Definition nolabel (s: stmt) : Prop :=
+  forall lbl k, find_label lbl s k = None.
+
+Lemma classify_stmt_nolabel:
+  forall s, classify_stmt s <> SCother -> nolabel s.
+Proof.
+  intros s. functional induction (classify_stmt s); intros.
+- red; auto.
+- red; auto.
+- apply IHs0 in H. red; intros; simpl. apply H.
+- apply IHs0 in H. red; intros; simpl. rewrite H; auto.
+- congruence.
+Qed.
+
+Lemma if_conversion_base_nolabel: forall ki env a id a1 a2 s,
+  if_conversion_base ki env a id a1 a2 = Some s ->
+  nolabel s.
+Proof.
+  unfold if_conversion_base; intros.
+  destruct (is_known ki id && safe_expr ki a1 && safe_expr ki a2); inv H.
+  red; auto.
+Qed.
+
+Lemma if_conversion_nolabel: forall ki env a s1 s2 s,
+    if_conversion ki env a s1 s2 = Some s ->
+    nolabel s1 /\ nolabel s2 /\ nolabel s.
+Proof.
+  unfold if_conversion; intros.
+  Ltac conclude :=
+    split; [apply classify_stmt_nolabel;congruence
+           |split; [apply classify_stmt_nolabel;congruence
+                   |eapply if_conversion_base_nolabel; eauto]].
+  destruct (classify_stmt s1) eqn:C1; try discriminate;
+  destruct (classify_stmt s2) eqn:C2; try discriminate.
+  conclude.
+  conclude.
+  destruct (ident_eq id id0). conclude. discriminate.
+Qed.
+
+Lemma transf_find_label: forall lbl ki env s k k',
+  match_cont ki env k k' ->
+  match find_label lbl s k with
+  | Some (s1, k1) =>
+    exists k1', find_label lbl (transf_stmt ki env s) k' = Some (transf_stmt ki env s1, k1')
+             /\ match_cont ki env k1 k1'
+  | None => find_label lbl (transf_stmt ki env s) k' = None
+  end.
+Proof.
+  induction s; intros k k' MC; simpl; auto.
+- exploit (IHs1 (Kseq s2 k)). econstructor; eauto.
+  destruct (find_label lbl s1 (Kseq s2 k)) as [[sx kx]|].
+  + intros (kx' & A & B); rewrite A. exists kx'; auto.
+  + intros A; rewrite A. apply IHs2; auto.
+- destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC.
+  + apply if_conversion_nolabel in IFC. destruct IFC as (L1 & L2 & L3).
+    rewrite L1, L2. apply L3.
+  + simpl. exploit (IHs1 k); eauto. destruct (find_label lbl s1 k) as [[sx kx]|].
+    * intros (kx' & A & B). rewrite A. exists kx'; auto.
+    * intros A; rewrite A. apply IHs2; auto.
+- apply IHs. constructor; auto.
+- apply IHs. constructor; auto.
+- destruct (ident_eq lbl l).
+  + exists k'; auto.
+  + apply IHs; auto.
+Qed.
+
+Lemma simulation:
+  forall S1 t S2, step ge S1 t S2 -> wt_state S1 ->
+  forall R1, match_states S1 R1 ->
+  exists S3 R2, star step ge S2 E0 S3 /\ step tge R1 t R2 /\ match_states S3 R2.
+Proof.
+  assert (DFL: forall R1 t R2 S2,
+             step tge R1 t R2 -> match_states S2 R2 ->
+             exists S3 R2, star step ge S2 E0 S3 /\ step tge R1 t R2 /\ match_states S3 R2).
+  { intros. exists S2, R2; split. apply star_refl. auto. }
+  destruct 1; intros WT R1 MS; inv MS.
+- (* skip Kseq *)
+  inv CONT; simpl. eapply DFL.
+  constructor.
+  econstructor; eauto.
+  inv H.
+- (* skip Kblock *)
+  inv CONT; simpl. eapply DFL.
+  constructor.
+  econstructor; eauto.
+  inv H.
+- (* skip return *)
+  exploit match_cont_is_call_cont; eauto. intros [A B].
+  eapply DFL.
+  eapply step_skip_call; eauto. erewrite stackspace_transf_function; eauto.
+  econstructor; eauto.
+- (* assign *)
+  eapply DFL.
+  econstructor. eapply eval_expr_preserved; eauto.
+  econstructor; eauto.
+- (* store *)
+  eapply DFL.
+  econstructor; eauto using eval_expr_preserved.
+  econstructor; eauto.
+- (* call *)
+  exploit functions_translated; eauto using eval_expr_preserved.
+  intros (tf & A & B).
+  eapply DFL.
+  econstructor; eauto using eval_expr_preserved, eval_exprlist_preserved.
+  apply sig_transf_function; auto.
+  econstructor; eauto. econstructor; eauto.
+- (* tailcall *)
+  exploit functions_translated; eauto using eval_expr_preserved.
+  intros (tf & A & B).
+  eapply DFL.
+  econstructor; eauto using eval_expr_preserved, eval_exprlist_preserved.
+  apply sig_transf_function; auto.
+  erewrite stackspace_transf_function; eauto.
+  econstructor; eauto using match_cont_call_cont.
+- (* builtin *)
+  eapply DFL.
+  econstructor. eapply eval_exprlist_preserved; eauto.
+  eapply external_call_symbols_preserved. eexact senv_preserved. eauto.
+  econstructor; eauto.
+- (* seq *)
+  simpl. eapply DFL.
+  econstructor.
+  econstructor; eauto. econstructor; eauto.
+- (* ifthenelse *)
+  simpl. destruct (if_conversion (known_id f) env a s1 s2) as [s|] eqn:IFC.
+  + inv WT. assert (env0 = env) by (inv WT_FN; inv WT_FN0; congruence); subst env0.
+    inv WT_STMT.
+    exploit if_conversion_sound; eauto.
+    set (s0 := if b then s1 else s2).
+    intros (e1 & A & B).
+    econstructor; econstructor. split. eexact B. split. eexact A.
+    econstructor; eauto.
+  + eapply DFL.
+    econstructor; eauto using eval_expr_preserved.
+    econstructor; eauto. destruct b; auto.
+- (* loop *)
+  eapply DFL.
+  simpl; econstructor.
+  econstructor; eauto. econstructor; eauto.
+- (* block *)
+  eapply DFL.
+  simpl; econstructor.
+  econstructor; eauto. econstructor; eauto.
+- (* exit seq *)
+  inv CONT. eapply DFL.
+  econstructor; eauto.
+  econstructor; eauto.
+  inv H.
+- (* exit block *)
+  inv CONT. eapply DFL.
+  econstructor; eauto.
+  econstructor; eauto.
+  inv H.
+- (* exit block *)
+  inv CONT. eapply DFL.
+  econstructor; eauto.
+  econstructor; eauto.
+  inv H.
+- (* switch *)
+  eapply DFL.
+  econstructor; eauto using eval_expr_preserved.
+  econstructor; eauto.
+- (* return none *)
+  eapply DFL.
+  econstructor.  erewrite stackspace_transf_function; eauto.
+  econstructor; eauto using match_cont_call_cont.
+- (* return some *)
+  eapply DFL.
+  econstructor. eapply eval_expr_preserved; eauto. erewrite stackspace_transf_function; eauto.
+  econstructor; eauto using match_cont_call_cont.
+- (* label *)
+  eapply DFL.
+  simpl; econstructor.
+  econstructor; eauto.
+- (* goto *)
+  exploit (transf_find_label lbl (known_id f) env (fn_body f)).
+  apply match_cont_call. eapply match_cont_call_cont. eauto.
+  rewrite H. intros (k'' & A & B).
+  replace (transf_stmt (known_id f) env (fn_body f)) with (fn_body f') in A
+  by (monadInv TR_FN; simpl; congruence).
+  eapply DFL.
+  econstructor; eauto.
+  econstructor; eauto.
+- (* internal function *)
+  monadInv TR_FN. generalize EQ; intros EQ'; monadInv EQ'.
+  eapply DFL.
+  econstructor; simpl; eauto.
+  econstructor; simpl; eauto. constructor; auto.
+- (* external function *)
+  monadInv TR_FN. eapply DFL.
+  econstructor. eapply external_call_symbols_preserved. eexact senv_preserved. eauto.
+  econstructor; eauto.
+- (* return *)
+  inv CONT. eapply DFL.
+  econstructor.
+  econstructor; eauto.
+Qed.
+
+Lemma initial_states_simulation:
+  forall S, initial_state prog S -> exists R, initial_state tprog R /\ match_states S R.
+Proof.
+  intros; inv H.
+  exploit function_ptr_translated; eauto. intros (tf & FIND & TR).
+  exploit sig_transf_function; eauto. intros SG.
+  econstructor; split.
+  econstructor.  eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+  rewrite symbols_preserved, (match_program_main TRANSL); eauto.
+  eauto.
+  congruence.
+  constructor; auto. constructor.
+Qed.
+
+Lemma final_states_simulation:
+  forall S R r,
+  match_states S R -> final_state S r -> final_state R r.
+Proof.
+  intros. inv H0. inv H. inv CONT. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (semantics prog) (semantics tprog).
+Proof.
+  set (ms := fun S R => wt_state S /\ match_states S R).
+  eapply forward_simulation_determ_one with (match_states := ms).
+- apply Cminor.semantics_determinate.
+- apply senv_preserved.
+- intros. exploit initial_states_simulation; eauto. intros [R [A B]].
+  exists R; split; auto. split; auto.
+  apply wt_initial_state with (p := prog); auto. exact wt_prog.
+- intros. destruct H. eapply final_states_simulation; eauto.
+- intros. destruct H0.
+  exploit simulation; eauto. intros (s1'' & s2' & A & B & C).
+  exists s1'', s2'. intuition auto. split; auto.
+  eapply subject_reduction_star with (st1 := s1). eexact wt_prog.
+  econstructor; eauto. auto.
+Qed.
+
+End PRESERVATION.
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 75247f71..48404b46 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -33,6 +33,7 @@ Require SimplExpr.
 Require SimplLocals.
 Require Cshmgen.
 Require Cminorgen.
+Require Ifconv.
 Require Selection.
 Require RTLgen.
 Require Tailcall.
@@ -54,6 +55,7 @@ Require SimplExprproof.
 Require SimplLocalsproof.
 Require Cshmgenproof.
 Require Cminorgenproof.
+Require Ifconvproof.
 Require Selectionproof.
 Require RTLgenproof.
 Require Tailcallproof.
@@ -149,6 +151,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
 Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
    OK p
    @@ print print_Cminor
+  @@@ time "If-conversion" Ifconv.transf_program
   @@@ time "Instruction selection" Selection.sel_program
   @@@ time "RTL generation" RTLgen.transl_program
   @@@ transf_rtl_program.
@@ -233,6 +236,7 @@ Definition CompCert's_passes :=
   ::: mkpass SimplLocalsproof.match_prog
   ::: mkpass Cshmgenproof.match_prog
   ::: mkpass Cminorgenproof.match_prog
+  ::: mkpass Ifconvproof.match_prog
   ::: mkpass Selectionproof.match_prog
   ::: mkpass RTLgenproof.match_prog
   ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
@@ -275,7 +279,8 @@ Proof.
   destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.
   destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.
   unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
-  destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
+  destruct (Ifconv.transf_program p4) as [p41|e] eqn:P41; simpl in T; try discriminate.
+  destruct (Selection.sel_program p41) as [p5|e] eqn:P5; simpl in T; try discriminate.
   destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
   unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
   set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
@@ -297,6 +302,7 @@ Proof.
   exists p2; split. apply SimplLocalsproof.match_transf_program; auto.
   exists p3; split. apply Cshmgenproof.transf_program_match; auto.
   exists p4; split. apply Cminorgenproof.transf_program_match; auto.
+  exists p41; split. apply Ifconvproof.transf_program_match; auto.
   exists p5; split. apply Selectionproof.transf_program_match; auto.
   exists p6; split. apply RTLgenproof.transf_program_match; auto.
   exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match.
@@ -364,7 +370,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 p21)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -375,6 +381,8 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply Cminorgenproof.transl_program_correct; eassumption.
   eapply compose_forward_simulations.
+    eapply Ifconvproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
     eapply Selectionproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply RTLgenproof.transf_program_correct; eassumption.