Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion

21 files changed, 1552 insertions, 150 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index cf62295d..13e14530 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -36,7 +36,7 @@ Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
 - a [Lbranch s] instruction.
 
   The [block_shape] type below describes all possible cases of structural
-  maching between an RTL instruction and an LTL basic block.
+  matching between an RTL instruction and an LTL basic block.
 *)
 
 Inductive move: Type :=
diff --git a/backend/Asmexpandaux.mli b/backend/Asmexpandaux.mli
index d80b4aec..e2320418 100644
--- a/backend/Asmexpandaux.mli
+++ b/backend/Asmexpandaux.mli
@@ -22,7 +22,7 @@ val emit: instruction -> unit
 val new_label: unit -> label
   (* Compute a fresh label *)
 val is_current_function_variadic: unit -> bool
-  (* Test wether the current function is a variadic function *)
+  (* Test whether the current function is a variadic function *)
 val get_current_function_args: unit -> typ list
   (* Get the types of the current function arguments *)
 val get_current_function_sig: unit -> signature
@@ -33,4 +33,4 @@ val get_current_function: unit -> coq_function
   (* Get the current function *)
 val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
   (* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
-     function to get the dwarf mapping of varibale names and for the expansion of simple instructions *)
+     function to get the dwarf mapping of variable names and for the expansion of simple instructions *)
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index d6bde348..a60c316b 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -544,7 +544,7 @@ Lemma kill_loads_after_storebytes_holds:
   bc sp = BCstack ->
   ematch bc rs ae ->
   approx = VA.State ae am ->
-  length bytes = nat_of_Z sz -> sz >= 0 ->
+  length bytes = Z.to_nat sz -> sz >= 0 ->
   numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m'
                            (kill_loads_after_storebytes approx n dst sz).
 Proof.
@@ -557,7 +557,7 @@ Proof.
   simpl.
   rewrite negb_false_iff in H8.
   eapply Mem.load_storebytes_other. eauto.
-  rewrite H6. rewrite nat_of_Z_eq by auto.
+  rewrite H6. rewrite Z2Nat.id by omega.
   eapply pdisjoint_sound. eauto.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
@@ -598,9 +598,9 @@ Proof.
   exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3).
   clear SB23.
   assert (L1: Z.of_nat (length bytes1) = n1).
-  { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n1; omega. }
+  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; omega. }
   assert (L2: Z.of_nat (length bytes2) = n2).
-  { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n2; omega. }
+  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; omega. }
   rewrite L1 in *. rewrite L2 in *.
   assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2).
   { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. }
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 11941da3..ca01ad50 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -591,6 +591,70 @@ Proof.
   red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto.
 Qed.
 
+(** This semantics is determinate. *)
+
+Lemma eval_expr_determ:
+  forall ge sp e m a v, eval_expr ge sp e m a v ->
+  forall v', eval_expr ge sp e m a v' -> v' = v.
+Proof.
+  induction 1; intros v' E'; inv E'.
+- congruence.
+- congruence.
+- assert (v0 = v1) by eauto. congruence.
+- assert (v0 = v1) by eauto. assert (v3 = v2) by eauto. congruence.
+- assert (vaddr0 = vaddr) by eauto. congruence.
+Qed.
+
+Lemma eval_exprlist_determ:
+  forall ge sp e m al vl, eval_exprlist ge sp e m al vl ->
+  forall vl', eval_exprlist ge sp e m al vl' -> vl' = vl.
+Proof.
+  induction 1; intros vl' E'; inv E'.
+  - auto.
+  - f_equal; eauto using eval_expr_determ.
+Qed.
+
+Ltac Determ :=
+  try congruence;
+  match goal with
+  | [ |- match_traces _ E0 E0 /\ (_ -> _) ]  =>
+          split; [constructor|intros _; Determ]
+  | [ H: is_call_cont ?k |- _ ] =>
+          contradiction || (clear H; Determ)
+  | [ H1: eval_expr _ _ _ _ ?a ?v1, H2: eval_expr _ _ _ _ ?a ?v2 |- _ ] =>
+          assert (v1 = v2) by (eapply eval_expr_determ; eauto);
+          clear H1 H2; Determ
+  | [ H1: eval_exprlist _ _ _ _ ?a ?v1, H2: eval_exprlist _ _ _ _ ?a ?v2 |- _ ] =>
+          assert (v1 = v2) by (eapply eval_exprlist_determ; eauto);
+          clear H1 H2; Determ
+  | _ => idtac
+  end.
+
+Lemma semantics_determinate:
+  forall (p: program), determinate (semantics p).
+Proof.
+  intros. constructor; set (ge := Genv.globalenv p); simpl; intros.
+- (* determ *)
+  inv H; inv H0; Determ.
+  + subst vargs0. exploit external_call_determ. eexact H2. eexact H13.
+    intros (A & B). split; intros; auto.
+    apply B in H; destruct H; congruence.
+  + subst v0. assert (b0 = b) by (inv H2; inv H13; auto). subst b0; auto.
+  + assert (n0 = n) by (inv H2; inv H14; auto). subst n0; auto.
+  + exploit external_call_determ. eexact H1. eexact H7.
+    intros (A & B). split; intros; auto.
+    apply B in H; destruct H; congruence.
+- (* single event *)
+  red; simpl. destruct 1; simpl; try omega;
+  eapply external_call_trace_length; eauto.
+- (* initial states *)
+  inv H; inv H0. unfold ge0, ge1 in *. congruence.
+- (* nostep final state *)
+  red; intros; red; intros. inv H; inv H0.
+- (* final states *)
+  inv H; inv H0; auto.
+Qed.
+
 (** * Alternate operational semantics (big-step) *)
 
 (** We now define another semantics for Cminor without [goto] that follows
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
new file mode 100644
index 00000000..ddd0f98b
--- /dev/null
+++ b/backend/Cminortyping.v
@@ -0,0 +1,798 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 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.
+
+(** * Type inference algorithm *)
+
+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 of the type system *)
+
+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.
+
+(** * Safe expressions *)
+
+(** Function parameters and declared local variables are always defined
+  throughout the execution of a function.  The following [known_idents]
+  data structure represents the set of those variables, with efficient membership. *)
+
+Definition known_idents := PTree.t unit.
+
+Definition is_known (ki: known_idents) (id: ident) :=
+  match ki!id with Some _ => true | None => false 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)).
+
+(** A Cminor expression is safe if it always evaluates to a value,
+    never causing a run-time error. *)
+
+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.
+
+(** Soundness of [known_id]. *)
+
+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.
+
+(** Expressions that satisfy [safe_expr] always evaluate to a value. *)
+
+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.
+
+
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 199ac922..2edc0395 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -106,7 +106,7 @@ Local Transparent Mem.loadbytes.
   unfold Mem.loadbytes; intros. destruct H.
   destruct (Mem.range_perm_dec m1 b ofs (ofs + n) Cur Readable); inv H0.
   rewrite pred_dec_true. econstructor; split; eauto.
-  apply GETN. intros. rewrite nat_of_Z_max in H.
+  apply GETN. intros. rewrite Z_to_nat_max in H.
   assert (ofs <= i < ofs + n) by xomega.
   apply ma_memval0; auto.
   red; intros; eauto.
@@ -966,7 +966,7 @@ Ltac UseTransfer :=
   intros. eapply nlive_remove; eauto.
   unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto.
   erewrite Mem.loadbytes_length in H1 by eauto.
-  rewrite nat_of_Z_eq in H1 by omega. auto.
+  rewrite Z2Nat.id in H1 by omega. auto.
   eauto.
   intros (tm' & A & B).
   econstructor; split.
@@ -993,7 +993,7 @@ Ltac UseTransfer :=
   intros (bc & A & B & C).
   intros. eapply nlive_contains; eauto.
   erewrite Mem.loadbytes_length in H0 by eauto.
-  rewrite nat_of_Z_eq in H0 by omega. auto.
+  rewrite Z2Nat.id in H0 by omega. auto.
 + (* annot *)
   destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR.
   InvSoundState.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 2dcb8956..181f40bf 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -755,13 +755,13 @@ Proof.
   assert (2 <= sz -> (2 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). auto.
-    destruct (zle sz 4). apply Zdivides_trans with 4; auto. exists 2; auto.
-    apply Zdivides_trans with 8; auto. exists 4; auto.
+    destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto.
+    apply Z.divide_trans with 8; auto. exists 4; auto.
   assert (4 <= sz -> (4 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). omegaContradiction.
     destruct (zle sz 4). auto.
-    apply Zdivides_trans with 8; auto. exists 2; auto.
+    apply Z.divide_trans with 8; auto. exists 2; auto.
   assert (8 <= sz -> (8 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). omegaContradiction.
@@ -1249,7 +1249,7 @@ Proof.
     eapply external_call_nextblock; eauto.
     auto. auto.
 
-- (* return fron noninlined function *)
+- (* return from noninlined function *)
   inv MS0.
 + (* normal case *)
   left; econstructor; split.
diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index 3469bdc6..4e57106f 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -123,15 +123,15 @@ let pp_mnemonics pp mnemonic_names =
   let new_line pp () = pp_print_string pp "\n" in
   pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names
 
-let jdump_magic_number = "CompCertJDUMP" ^ Version.version
+let jdump_magic_number = "CompCertJDUMPRelease: " ^ Version.version
 
 let pp_ast pp pp_inst ast sourcename =
    let get_args () =
     let buf = Buffer.create 100 in
     Buffer.add_string buf Sys.executable_name;
-    for i = 1 to (Array.length  !Commandline.argv - 1) do
+    for i = 1 to (Array.length  Commandline.argv - 1) do
       Buffer.add_string buf " ";
-      Buffer.add_string buf (Responsefile.gnu_quote !Commandline.argv.(i));
+      Buffer.add_string buf (Responsefile.gnu_quote Commandline.argv.(i));
     done;
     Buffer.contents buf in
     let dump_compile_info pp () =
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index bc9fb3ca..1fe23a9d 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -39,7 +39,7 @@ Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
   | Outgoing => zle 0 ofs
   | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig)))
   end
-  && Zdivide_dec (typealign ty) ofs (typealign_pos ty).
+  && Zdivide_dec (typealign ty) ofs.
 
 Definition slot_writable (sl: slot) : bool :=
   match sl with
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index d431f3d8..b35c90b2 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import IntvSets.
 Require Import AST.
+Require Import Zbits.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -300,13 +301,13 @@ Proof.
   rewrite Int.bits_ror.
   replace (((i - Int.unsigned amount) mod Int.zwordsize + Int.unsigned amount)
    mod Int.zwordsize) with i. auto.
-  apply Int.eqmod_small_eq with Int.zwordsize; auto.
-  apply Int.eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
-  apply Int.eqmod_refl2; omega.
-  eapply Int.eqmod_trans. 2: apply Int.eqmod_mod; auto.
-  apply Int.eqmod_add.
-  apply Int.eqmod_mod; auto.
-  apply Int.eqmod_refl.
+  apply eqmod_small_eq with Int.zwordsize; auto.
+  apply eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
+  apply eqmod_refl2; omega.
+  eapply eqmod_trans. 2: apply eqmod_mod; auto.
+  apply eqmod_add.
+  apply eqmod_mod; auto.
+  apply eqmod_refl.
   apply Z_mod_lt; auto.
   apply Z_mod_lt; auto.
 Qed.
@@ -324,16 +325,16 @@ Qed.
 
 Lemma eqmod_iagree:
   forall m x y,
-  Int.eqmod (two_p (Int.size m)) x y ->
+  eqmod (two_p (Int.size m)) x y ->
   iagree (Int.repr x) (Int.repr y) m.
 Proof.
-  intros. set (p := nat_of_Z (Int.size m)).
+  intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
   rewrite EQ in H; rewrite <- two_power_nat_two_p in H.
   red; intros. rewrite ! Int.testbit_repr by auto.
   destruct (zlt i (Int.size m)).
-  eapply Int.same_bits_eqmod; eauto. omega.
+  eapply same_bits_eqmod; eauto. omega.
   assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega).
   congruence.
 Qed.
@@ -343,13 +344,13 @@ Definition complete_mask (m: int) := Int.zero_ext (Int.size m) Int.mone.
 Lemma iagree_eqmod:
   forall x y m,
   iagree x y (complete_mask m) ->
-  Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
+  eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
 Proof.
-  intros. set (p := nat_of_Z (Int.size m)).
+  intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
   rewrite EQ; rewrite <- two_power_nat_two_p.
-  apply Int.eqmod_same_bits. intros. apply H. omega.
+  apply eqmod_same_bits. intros. apply H. omega.
   unfold complete_mask. rewrite Int.bits_zero_ext by omega.
   rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto.
 Qed.
@@ -362,7 +363,7 @@ Proof.
 + assert (Int.unsigned m <> 0).
   { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. }
   assert (0 < Int.size m).
-  { apply Int.Zsize_pos'. generalize (Int.unsigned_range m); omega. }
+  { apply Zsize_pos'. generalize (Int.unsigned_range m); omega. }
   generalize (Int.size_range m); intros.
   f_equal. apply Int.bits_size_4. tauto.
   rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega.
@@ -610,7 +611,7 @@ Proof.
   unfold modarith; intros. destruct x; simpl in *.
 - auto.
 - unfold Val.add; InvAgree.
-  apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto.
+  apply eqmod_iagree. apply eqmod_add; apply iagree_eqmod; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
@@ -626,7 +627,7 @@ Lemma mul_sound:
 Proof.
   unfold mul, add; intros. destruct x; simpl in *.
 - auto.
-- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto.
+- unfold Val.mul; InvAgree. apply eqmod_iagree. apply eqmod_mult; apply iagree_eqmod; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
@@ -638,7 +639,7 @@ Proof.
   intros; destruct x; simpl in *.
 - auto.
 - unfold Val.neg; InvAgree.
-  apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto.
+  apply eqmod_iagree. apply eqmod_neg. apply iagree_eqmod; auto.
 - inv H; simpl; auto.
 Qed.
 
@@ -785,6 +786,34 @@ Proof.
   inv H0. rewrite iagree_and_eq in H. rewrite H. auto.
 Qed.
 
+(** The needs of a select *)
+
+Lemma normalize_sound:
+  forall v w x ty,
+  vagree v w x ->
+  vagree (Val.normalize v ty) (Val.normalize w ty) x.
+Proof.
+  intros. destruct x; simpl in *. 
+- auto.
+- unfold Val.normalize. destruct v. 
+  auto.
+  destruct w; try contradiction. destruct ty; auto.
+  destruct ty; auto.
+  destruct ty; auto.
+  destruct ty; auto.
+  destruct ty; destruct Archi.ptr64; auto.
+- apply Val.normalize_lessdef; auto.
+Qed.
+
+Lemma select_sound:
+  forall ob v1 v2 w1 w2 ty x,
+  vagree v1 w1 x -> vagree v2 w2 x ->
+  vagree (Val.select ob v1 v2 ty) (Val.select ob w1 w2 ty) x.
+Proof.
+  unfold Val.select; intros. destruct ob as [b|]; auto with na.
+  apply normalize_sound. destruct b; auto.
+Qed.
+
 (** The default abstraction: if the result is unused, the arguments are
   unused; otherwise, the arguments are needed in full. *)
 
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 92d465d5..dd428808 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -40,6 +40,7 @@ module Printer(Target:TARGET) =
 
     let print_function oc name fn =
       Hashtbl.clear current_function_labels;
+      Debug.symbol_printed (extern_atom name);
       let (text, lit, jmptbl) = Target.get_section_names name in
       Target.section oc text;
       let alignment =
@@ -117,7 +118,7 @@ module Printer(Target:TARGET) =
       match v.gvar_init with
       | [] -> ()
       | _  ->
-          Debug.variable_printed (extern_atom name);
+          Debug.symbol_printed (extern_atom name);
           let sec =
             match C2C.atom_sections name with
             | [s] -> s
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index f9ed569f..7e075f04 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -289,12 +289,20 @@ let print_inline_asm print_preg oc txt sg args res =
 let print_version_and_options oc comment =
   let version_string =
     if Version.buildnr <> "" && Version.tag <> "" then
-      sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
+      sprintf "Release: %s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
     else
       Version.version in
   fprintf oc "%s File generated by CompCert %s\n" comment version_string;
   fprintf oc "%s Command line:" comment;
-  for i = 1 to Array.length Sys.argv - 1 do
-    fprintf oc " %s" Sys.argv.(i)
+  for i = 1 to Array.length Commandline.argv - 1 do
+    fprintf oc " %s" Commandline.argv.(i)
   done;
   fprintf oc "\n"
+(** Get the name of the common section if it is used otherwise the given section
+    name, with bss as default *)
+
+let common_section ?(sec = ".bss") () =
+  if !Clflags.option_fcommon then
+    "COMM"
+  else
+    sec
diff --git a/backend/RTL.v b/backend/RTL.v
index 16723d96..9599a24a 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -73,7 +73,7 @@ Inductive instruction: Type :=
           it transitions to [ifnot]. *)
   | Ijumptable: reg -> list node -> instruction
       (** [Ijumptable arg tbl] transitions to the node that is the [n]-th
-          element of the list [tbl], where [n] is the signed integer
+          element of the list [tbl], where [n] is the unsigned integer
           value of register [arg]. *)
   | Ireturn: option reg -> instruction.
       (** [Ireturn] terminates the execution of the current function
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index b003eb10..b94ec22f 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -704,7 +704,7 @@ Proof.
   intros; red; intros. inv TE.
   exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]].
   exploit external_call_mem_extends; eauto.
-  intros [v' [tm2 [A [B [C [D E]]]]]].
+  intros [v' [tm2 [A [B [C D]]]]].
   exists (rs1#rd <- v'); exists tm2.
 (* Exec *)
   split. eapply star_right. eexact EX1.
@@ -736,7 +736,7 @@ Proof.
   intros; red; intros. inv TE.
   exploit H3; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]].
   exploit external_call_mem_extends; eauto.
-  intros [v' [tm2 [A [B [C [D E]]]]]].
+  intros [v' [tm2 [A [B [C D]]]]].
   exploit function_ptr_translated; eauto. simpl. intros [tf [P Q]]. inv Q.
   exists (rs1#rd <- v'); exists tm2.
 (* Exec *)
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index e2249ddb..a8ee8453 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection for integer division *)
 
-Require Import Zquot Coqlib.
+Require Import Zquot Coqlib Zbits.
 Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
 Require Import OpHelpers OpHelpersproof.
@@ -58,13 +58,13 @@ Proof.
     apply Z.mul_nonneg_nonneg; omega.
   assert (k * n <= two_p (N + l) - two_p l).
     apply Z.le_trans with (two_p l * n).
-    apply Zmult_le_compat_r. omega. omega.
+    apply Z.mul_le_mono_nonneg_r; omega.
     replace (N + l) with (l + N) by omega.
     rewrite two_p_is_exp.
     replace (two_p l * two_p N - two_p l)
        with (two_p l * (two_p N - 1))
          by ring.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
     omega. omega.
   assert (0 <= two_p (N + l) * r).
     apply Z.mul_nonneg_nonneg.
@@ -73,7 +73,7 @@ Proof.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1)) by ring.
-    apply Zmult_le_compat_l.
+    apply Z.mul_le_mono_nonneg_l. 
     omega.
     exploit (two_p_gt_ZERO (N + l)). omega. omega.
   assert (0 <= m * n - two_p (N + l) * q).
@@ -139,13 +139,13 @@ Proof.
   rewrite H2.
   assert (k * n <= two_p (N + l)).
     rewrite Z.add_comm. rewrite two_p_is_exp; try omega.
-    apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; omega.
+    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1))
          by ring.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO (N + l)). omega. omega.
+    apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega.
   omega.
 Qed.
 
@@ -247,10 +247,11 @@ Proof.
   unfold Int.max_signed; omega.
   apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos.
   apply Int.modulus_pos.
-  split. apply Z.le_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega.
-  apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto.
+  split. apply Z.le_trans with (Int.min_signed * m). 
+  apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; omega. omega.
+  apply Z.mul_le_mono_nonneg_r. omega. unfold n; generalize (Int.signed_range x); tauto.
   apply Z.le_lt_trans with (Int.half_modulus * m).
-  apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto.
+  apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; omega.
   apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto.
   assert (32 < Int.max_unsigned) by (compute; auto). omega.
   unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr.
@@ -291,7 +292,7 @@ Proof.
   apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned.
   apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2.
   apply (f_equal (fun x => n * x / Int.modulus)).
-  rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption.
+  rewrite Int.signed_repr_eq. rewrite Z.mod_small by assumption.
   apply zlt_false. assumption.
 Qed.
 
@@ -378,7 +379,7 @@ Qed.
 Remark int64_shr'_div_two_p:
   forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shr'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
 Qed.
 
 Lemma divls_mul_shift_gen:
@@ -401,8 +402,9 @@ Proof.
   unfold Int64.max_signed; omega.
   apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos.
   apply Int64.modulus_pos.
-  split. apply Z.le_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega.
-  apply Zmult_le_compat_r. unfold n; generalize (Int64.signed_range x); tauto. tauto.
+  split. apply Z.le_trans with (Int64.min_signed * m).
+  apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; omega. omega.
+  apply Z.mul_le_mono_nonneg_r. tauto. unfold n; generalize (Int64.signed_range x); tauto.
   apply Z.le_lt_trans with (Int64.half_modulus * m).
   apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto.
   apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto.
@@ -445,14 +447,14 @@ Proof.
   apply Int64.eqm_sym. eapply Int64.eqm_trans. apply Int64.eqm_signed_unsigned.
   apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2.
   apply (f_equal (fun x => n * x / Int64.modulus)).
-  rewrite Int64.signed_repr_eq. rewrite Zmod_small by assumption.
+  rewrite Int64.signed_repr_eq. rewrite Z.mod_small by assumption.
   apply zlt_false. assumption.
 Qed.
 
 Remark int64_shru'_div_two_p:
   forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shru'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
 Qed.
 
 Theorem divlu_mul_shift:
diff --git a/backend/Selection.v b/backend/Selection.v
index 3b0948a8..37a78853 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -26,7 +26,7 @@ Require String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Globalenvs Switch.
 Require Cminor.
-Require Import Op CminorSel OpHelpers.
+Require Import Op CminorSel OpHelpers Cminortyping.
 Require Import SelectOp SplitLong SelectLong SelectDiv.
 Require Machregs.
 
@@ -43,6 +43,12 @@ Function condexpr_of_expr (e: expr) : condexpr :=
   | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil)
   end.
 
+Function condition_of_expr (e: expr) : condition * exprlist :=
+  match e with
+  | Eop (Ocmp c) el => (c, el)
+  | _ => (Ccompuimm Cne Int.zero, e ::: Enil)
+  end.
+
 (** Conversion of loads and stores *)
 
 Definition load (chunk: memory_chunk) (e1: expr) :=
@@ -173,6 +179,10 @@ Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
   | a :: bl => Econs (sel_expr a) (sel_exprlist bl)
   end.
 
+Definition sel_select_opt (ty: typ) (arg1 arg2 arg3: Cminor.expr) : option expr :=
+  let (cond, args) := condition_of_expr (sel_expr arg1) in
+  SelectOp.select ty cond args (sel_expr arg2) (sel_expr arg3).
+
 (** Recognition of immediate calls and calls to built-in functions
     that should be inlined *)
 
@@ -267,7 +277,6 @@ Definition sel_switch_long :=
     (fun arg ofs => subl arg (longconst (Int64.repr ofs)))
     lowlong.
 
-
 Definition sel_builtin_default optid ef args :=
   OK (Sbuiltin (sel_builtin_res optid) ef
                (sel_builtin_args args
@@ -328,11 +337,64 @@ Definition sel_builtin optid ef args :=
        else
          sel_builtin_default optid ef args)
     | _ => sel_builtin_default optid ef args
+
+(** "If conversion": conversion of certain if-then-else statements
+  into branchless conditional move instructions. *)
+
+(** Recognition of "then" and "else" statements that support if-conversion.
+  Basically we are interested in assignments to local variables [id = e].
+  However the front-end may have put [skip] statements around these
+  assignments. *)
+
+Inductive stmt_class : Type :=
+  | SCskip
+  | SCassign (id: ident) (a: Cminor.expr)
+  | SCother.
+
+Function classify_stmt (s: Cminor.stmt) : stmt_class :=
+  match s with
+  | Cminor.Sskip => SCskip
+  | Cminor.Sassign id a => SCassign id a
+  | Cminor.Sseq Cminor.Sskip s => classify_stmt s
+  | Cminor.Sseq s Cminor.Sskip => classify_stmt s
+  | _ => SCother
+  end.
+
+(** External heuristic to limit the amount of if-conversion performed.
+    Arguments are: the condition, the "then" and the "else" expressions,
+    and the type at which selection is done. *)
+
+Parameter if_conversion_heuristic:
+  Cminor.expr -> Cminor.expr -> Cminor.expr -> AST.typ -> bool.
+
+Definition if_conversion_base
+      (ki: known_idents) (env: typenv)
+      (cond: Cminor.expr) (id: ident) (ifso ifnot:  Cminor.expr) : option stmt :=
+  let ty := env id in
+  if is_known ki id
+  && safe_expr ki ifso && safe_expr ki ifnot
+  && if_conversion_heuristic cond ifso ifnot ty
+  then option_map
+         (fun sel => Sassign id sel)
+         (sel_select_opt ty cond ifso ifnot)
+  else None.
+
+Definition if_conversion
+      (ki: known_idents) (env: typenv)
+      (cond: Cminor.expr) (ifso ifnot: Cminor.stmt) : option stmt :=
+  match classify_stmt ifso, classify_stmt ifnot with
+  | SCskip, SCassign id a =>
+      if_conversion_base ki env cond id (Cminor.Evar id) a
+  | SCassign id a, SCskip =>
+      if_conversion_base ki env cond id a (Cminor.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.
 
 (** Conversion from Cminor statements to Cminorsel statements. *)
 
-Fixpoint sel_stmt (s: Cminor.stmt) : res stmt :=
+Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :=
   match s with
   | Cminor.Sskip => OK Sskip
   | Cminor.Sassign id e => OK (Sassign id (sel_expr e))
@@ -357,15 +419,19 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt :=
       | _            => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args)
       end)
   | Cminor.Sseq s1 s2 =>
-      do s1' <- sel_stmt s1; do s2' <- sel_stmt s2;
+      do s1' <- sel_stmt ki env s1; do s2' <- sel_stmt ki env s2;
       OK (Sseq s1' s2')
   | Cminor.Sifthenelse e ifso ifnot =>
-      do ifso' <- sel_stmt ifso; do ifnot' <- sel_stmt ifnot;
-      OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot')
+      match if_conversion ki env e ifso ifnot with
+      | Some s => OK s
+      | None =>
+          do ifso' <- sel_stmt ki env ifso; do ifnot' <- sel_stmt ki env ifnot;
+          OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot')
+      end
   | Cminor.Sloop body =>
-      do body' <- sel_stmt body; OK (Sloop body')
+      do body' <- sel_stmt ki env body; OK (Sloop body')
   | Cminor.Sblock body =>
-      do body' <- sel_stmt body; OK (Sblock body')
+      do body' <- sel_stmt ki env body; OK (Sblock body')
   | Cminor.Sexit n => OK (Sexit n)
   | Cminor.Sswitch false e cases dfl =>
       let t := compile_switch Int.modulus dfl cases in
@@ -380,7 +446,7 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt :=
   | Cminor.Sreturn None => OK (Sreturn None)
   | Cminor.Sreturn (Some e) => OK (Sreturn (Some (sel_expr e)))
   | Cminor.Slabel lbl body =>
-      do body' <- sel_stmt body; OK (Slabel lbl body')
+      do body' <- sel_stmt ki env body; OK (Slabel lbl body')
   | Cminor.Sgoto lbl => OK (Sgoto lbl)
   end.
 
@@ -388,8 +454,15 @@ End SELECTION.
 
 (** Conversion of functions. *)
 
+Definition known_id (f: Cminor.function) : known_idents :=
+  let add (ki: known_idents) (id: ident) := PTree.set id tt ki in
+  List.fold_left add f.(Cminor.fn_vars)
+      (List.fold_left add f.(Cminor.fn_params) (PTree.empty unit)).
+
 Definition sel_function (dm: PTree.t globdef) (hf: helper_functions) (f: Cminor.function) : res function :=
-  do body' <- sel_stmt dm f.(Cminor.fn_body);
+  let ki := known_id f in
+  do env <- Cminortyping.type_function f;
+  do body' <- sel_stmt dm ki env f.(Cminor.fn_body);
   OK (mkfunction
         f.(Cminor.fn_sig)
         f.(Cminor.fn_params)
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
new file mode 100644
index 00000000..52ddd799
--- /dev/null
+++ b/backend/Selectionaux.ml
@@ -0,0 +1,109 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open Cminor
+
+(* Heuristics to guide if conversion *)
+
+(* Estimate a cost for evaluating a safe expression.
+   Unsafe operators need not be estimated.
+   Basic integer operations (add, and, ...) have cost 1 by convention.
+   The other costs are rough estimates. *)
+
+let cost_unop = function
+  | Ocast8unsigned | Ocast8signed
+  | Ocast16unsigned | Ocast16signed
+  | Onegint | Onotint -> 1
+  | Onegf | Oabsf -> 1
+  | Onegfs | Oabsfs -> 1
+  | Osingleoffloat | Ofloatofsingle -> 2
+  | Ointoffloat | Ointuoffloat
+  | Ofloatofint | Ofloatofintu
+  | Ointofsingle | Ointuofsingle
+  | Osingleofint | Osingleofintu -> assert false
+  | Onegl | Onotl -> if Archi.splitlong then 2 else 1
+  | Ointoflong | Olongofint | Olongofintu -> 1
+  | Olongoffloat | Olonguoffloat
+  | Ofloatoflong | Ofloatoflongu
+  | Olongofsingle | Olonguofsingle
+  | Osingleoflong | Osingleoflongu -> assert false
+
+let cost_binop = function
+  | Oadd  | Osub -> 1
+  | Omul -> 2
+  | Odiv  | Odivu | Omod  | Omodu -> assert false
+  | Oand  | Oor   | Oxor  | Oshl  | Oshr  | Oshru -> 1
+  | Oaddf | Osubf | Omulf -> 2
+  | Odivf -> 10
+  | Oaddfs| Osubfs| Omulfs -> 2
+  | Odivfs -> 10
+  | Oaddl | Osubl -> if Archi.splitlong then 3 else 1
+  | Omull -> if Archi.splitlong then 6 else 2
+  | Odivl | Odivlu | Omodl | Omodlu -> assert false
+  | Oandl | Oorl  | Oxorl -> if Archi.splitlong then 2 else 1
+  | Oshll | Oshrl | Oshrlu -> if Archi.splitlong then 4 else 1
+  | Ocmp _ | Ocmpu _ -> 2
+  | Ocmpf _ | Ocmpfs _ -> 2
+  | Ocmpl _ | Ocmplu _ -> assert false
+
+let rec cost_expr = function
+  | Evar _ -> 0
+  | Econst _ -> 1
+  | Eunop(op, e1) -> cost_unop op + cost_expr e1
+  | Ebinop(op, e1, e2) -> cost_binop op + cost_expr e1 + cost_expr e2
+  | Eload(_, e1) -> assert false
+
+(* Does the target architecture support an efficient "conditional move"
+   at the given type? *)
+
+let fast_cmove ty =
+  match Configuration.arch, Configuration.model with
+  | "arm", _ ->
+      (match ty with Tint | Tfloat | Tsingle -> true | _ -> false)
+  | "powerpc", "e5500" -> 
+      (match ty with Tint | Tlong -> true | _ -> false)
+  | "powerpc", _ -> false
+  | "riscV", _ -> false
+  | "x86", _ -> 
+      (match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
+  | _, _ ->
+      assert false
+
+(* The if-conversion heuristic depend on the
+   -fif-conversion and -ffavor-branchless flags.
+
+With [-fno-if-conversion] or [-0O], if-conversion is turned off entirely.
+With [-ffavor-branchless], if-conversion is performed whenever semantically
+correct, regardless of how much it could cost.
+Otherwise (and by default), optimization is performed when it seems beneficial.
+
+If-conversion seems beneficial if:
+- the target architecture supports an efficient "conditional move" instruction
+  (not an emulation that takes several instructions)
+- the total cost the "then" and "else" branches is not too high
+- the cost difference between the "then" and "else" branches is low enough.
+
+Intuition: on a modern processor, the "then" and the "else" branches
+can generally be computed in parallel, there is enough ILP for that.
+So, the bad case is if the most taken branch is much cheaper than the
+other branch.  Since our cost estimates are very imprecise, the
+bound on the total cost acts as a safety guard, 
+*)
+
+let if_conversion_heuristic cond ifso ifnot ty =
+  if not !Clflags.option_fifconversion then false else
+  if !Clflags.option_ffavor_branchless then true else
+  if not (fast_cmove ty) then false else
+  let c1 = cost_expr ifso and c2 = cost_expr ifnot in
+  c1 + c2 <= 30 && abs (c1 - c2) <= 8
+
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 23d10382..40db5d4b 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -15,7 +15,7 @@
 Require Import FunInd.
 Require Import Coqlib Maps.
 Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep.
-Require Import Switch Cminor Op CminorSel.
+Require Import Switch Cminor Op CminorSel Cminortyping.
 Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectDiv SplitLong SelectLong Selection.
 Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof.
@@ -120,6 +120,16 @@ Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 Hypothesis TRANSF: match_prog prog tprog.
 
+Lemma wt_prog : wt_program prog.
+Proof.
+  red; intros. destruct TRANSF as [A _].
+  exploit list_forall2_in_left; eauto.
+  intros ((i' & gd') & B & (C & D)). simpl in *. inv D. 
+  destruct H2 as (hf & P & Q). destruct f; monadInv Q.
+- 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 TRANSF).
@@ -203,6 +213,25 @@ Proof.
   simpl. inv H0. auto.
 Qed.
 
+Lemma eval_condition_of_expr:
+  forall a le v b,
+  eval_expr tge sp e m le a v ->
+  Val.bool_of_val v b ->
+  let (cond, al) := condition_of_expr a in
+  exists vl,
+     eval_exprlist tge sp e m le al vl
+  /\ eval_condition cond vl m = Some b.
+Proof.
+  intros until a. functional induction (condition_of_expr a); intros.
+(* compare *)
+  inv H. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool in H0.
+  exists vl; auto.
+(* default *)
+  exists (v :: nil); split.
+  econstructor. auto. constructor.
+  simpl. inv H0. auto.
+Qed.
+
 Lemma eval_load:
   forall le a v chunk v',
   eval_expr tge sp e m le a v ->
@@ -461,7 +490,7 @@ Qed.
 
 End SEL_SWITCH.
 
-Section SEL_SWITH_INT.
+Section SEL_SWITCH_INT.
 
 Variable cunit: Cminor.program.
 Variable hf: helper_functions.
@@ -507,7 +536,7 @@ Proof.
   unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal.
   apply Int.unsigned_repr. unfold Int.max_unsigned; omega.
 - intros until i0; intros EVAL R. exists v; split; auto.
-  inv R. rewrite Zmod_small by (apply Int.unsigned_range). constructor.
+  inv R. rewrite Z.mod_small by (apply Int.unsigned_range). constructor.
 - constructor.
 - apply Int.unsigned_range.
 Qed.
@@ -548,7 +577,7 @@ Proof.
 - apply Int64.unsigned_range.
 Qed.
 
-End SEL_SWITH_INT.
+End SEL_SWITCH_INT.
 
 (** Compatibility of evaluation functions with the "less defined than" relation. *)
 
@@ -699,6 +728,29 @@ Proof.
   exists (v1' :: vl'); split; auto. constructor; eauto.
 Qed.
 
+Lemma sel_select_opt_correct:
+  forall ty cond a1 a2 a sp e m vcond v1 v2 b e' m' le,
+  sel_select_opt ty cond a1 a2 = Some a ->
+  Cminor.eval_expr ge sp e m cond vcond ->
+  Cminor.eval_expr ge sp e m a1 v1 ->
+  Cminor.eval_expr ge sp e m a2 v2 ->
+  Val.bool_of_val vcond b ->
+  env_lessdef e e' -> Mem.extends m m' ->
+  exists v', eval_expr tge sp e' m' le a v' /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v'.
+Proof.
+  unfold sel_select_opt; intros. 
+  destruct (condition_of_expr (sel_expr cond)) as [cnd args] eqn:C.
+  exploit sel_expr_correct. eexact H0. eauto. eauto. intros (vcond' & EVC & LDC).
+  exploit sel_expr_correct. eexact H1. eauto. eauto. intros (v1' & EV1 & LD1).
+  exploit sel_expr_correct. eexact H2. eauto. eauto. intros (v2' & EV2 & LD2).
+  assert (Val.bool_of_val vcond' b) by (inv H3; inv LDC; constructor).
+  exploit eval_condition_of_expr. eexact EVC. eauto. rewrite C. intros (vargs' & EVARGS & EVCOND).
+  exploit eval_select; eauto. intros (v' & X & Y). 
+  exists v'; split; eauto. 
+  eapply Val.lessdef_trans; [|eexact Y].
+  apply Val.select_lessdef; auto.
+Qed.
+
 Lemma sel_builtin_arg_correct:
   forall sp e e' m m' a v c,
   env_lessdef e e' -> Mem.extends m m' ->
@@ -742,37 +794,174 @@ Proof.
   intros. destruct oid; simpl; auto. apply set_var_lessdef; auto.
 Qed.
 
+(** If-conversion *)
+
+Lemma classify_stmt_sound_1:
+  forall f sp e m s k,
+  classify_stmt s = SCskip ->
+  star Cminor.step ge (Cminor.State f s k sp e m) E0 (Cminor.State f Cminor.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,
+  Cminor.eval_expr ge sp e m a v ->
+  forall s k,
+  classify_stmt s = SCassign id a ->
+  star Cminor.step ge (Cminor.State f s k sp e m) E0 (Cminor.State f Cminor.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:
+  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 eval_select_safe_exprs:
+  forall a1 a2 f env ty e e' m m' sp cond vb b id s,
+  safe_expr (known_id f) a1 = true ->
+  safe_expr (known_id f) a2 = true ->
+  option_map (fun sel => Sassign id sel) (sel_select_opt ty cond a1 a2) = Some s ->
+  Cminor.eval_expr ge sp e m cond vb -> Val.bool_of_val vb b ->
+  wt_expr env a1 ty ->
+  wt_expr env a2 ty ->
+  def_env f e -> wt_env env e ->
+  Cminor.eval_expr ge sp e m cond vb -> Val.bool_of_val vb b ->
+  env_lessdef e e' -> Mem.extends m m' ->
+  exists a' v1 v2 v',
+     s = Sassign id a'
+  /\ Cminor.eval_expr ge sp e m a1 v1
+  /\ Cminor.eval_expr ge sp e m a2 v2
+  /\ eval_expr tge sp e' m' nil a' v'
+  /\ Val.lessdef (if b then v1 else v2) v'.
+Proof.
+  intros.
+  destruct (sel_select_opt ty cond a1 a2) as [a'|] eqn:SSO; simpl in H1; inv H1.
+  destruct (eval_safe_expr ge f sp e m a1) as (v1 & EV1); auto.
+  destruct (eval_safe_expr ge f sp e m a2) as (v2 & EV2); auto.
+  assert (TY1: Val.has_type v1 ty) by (eapply wt_eval_expr; eauto).
+  assert (TY2: Val.has_type v2 ty) by (eapply wt_eval_expr; eauto).
+  exploit sel_select_opt_correct; eauto. intros (v' & EV' & LD).
+  exists a', v1, v2, v'; intuition eauto.
+  apply Val.lessdef_trans with (Val.select (Some b) v1 v2 ty).
+  simpl. rewrite Val.normalize_idem; auto. destruct b; auto.
+  assumption.
+Qed. 
+
+Lemma if_conversion_correct:
+  forall f env tyret cond ifso ifnot s vb b k f' k' sp e m e' m',
+  if_conversion (known_id f) env cond ifso ifnot = Some s ->
+  def_env f e -> wt_env env e ->
+  wt_stmt env tyret ifso ->
+  wt_stmt env tyret ifnot ->
+  Cminor.eval_expr ge sp e m cond vb -> Val.bool_of_val vb b ->
+  env_lessdef e e' -> Mem.extends m m' ->
+  let s0 := if b then ifso else ifnot in
+  exists e1 e1',
+     step tge (State f' s k' sp e' m') E0 (State f' Sskip k' sp e1' m')
+  /\ star Cminor.step ge (Cminor.State f s0 k sp e m) E0 (Cminor.State f Cminor.Sskip k sp e1 m)
+  /\ env_lessdef e1 e1'.
+Proof.
+  unfold if_conversion; intros until m'; intros IFC DE WTE WT1 WT2 EVC BOV ELD MEXT.
+  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 (Cminor.Evar id) && safe_expr ki a
+            && if_conversion_heuristic cond (Cminor.Evar id) a (env id)) eqn:B; inv IFC.
+  InvBooleans.
+  exploit (eval_select_safe_exprs (Cminor.Evar id) a); eauto.
+  constructor. eapply classify_stmt_wt; eauto.
+  intros (a' & v1 & v2 & v' & A & B & C & D & E).
+  exists (PTree.set id (if b then v1 else v2) e), (PTree.set id v' e').
+  split. subst s. constructor; auto.
+  split. unfold s0; destruct b. 
+  rewrite PTree.gsident by (inv B; auto). apply classify_stmt_sound_1; auto.
+  eapply classify_stmt_sound_2; eauto.
+  apply set_var_lessdef; auto.
+- destruct (is_known ki id && safe_expr ki a && safe_expr ki (Cminor.Evar id)
+            && if_conversion_heuristic cond a (Cminor.Evar id) (env id)) eqn:B; inv IFC.
+  InvBooleans.
+  exploit (eval_select_safe_exprs a (Cminor.Evar id)); eauto.
+  eapply classify_stmt_wt; eauto. constructor. 
+  intros (a' & v1 & v2 & v' & A & B & C & D & E).
+  exists (PTree.set id (if b then v1 else v2) e), (PTree.set id v' e').
+  split. subst s. constructor; auto.
+  split. unfold s0; destruct b. 
+  eapply classify_stmt_sound_2; eauto.
+  rewrite PTree.gsident by (inv C; auto). apply classify_stmt_sound_1; auto.
+  apply set_var_lessdef; auto.
+- destruct (ident_eq id id0); try discriminate. subst id0.
+  destruct (is_known ki id && safe_expr ki a && safe_expr ki a0
+            && if_conversion_heuristic cond a a0 (env id)) eqn:B; inv IFC.
+  InvBooleans.
+  exploit (eval_select_safe_exprs a a0); eauto.
+  eapply classify_stmt_wt; eauto. eapply classify_stmt_wt; eauto.
+  intros (a' & v1 & v2 & v' & A & B & C & D & E).
+  exists (PTree.set id (if b then v1 else v2) e), (PTree.set id v' e').
+  split. subst s. constructor; auto.
+  split. unfold s0; destruct b; eapply classify_stmt_sound_2; eauto.
+  apply set_var_lessdef; auto.
+Qed.
+
 End EXPRESSIONS.
 
 (** Semantic preservation for functions and statements. *)
 
-Inductive match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop :=
-  | match_cont_stop: forall cunit hf,
-      match_cont cunit hf Cminor.Kstop Kstop
-  | match_cont_seq: forall cunit hf s s' k k',
-      sel_stmt (prog_defmap cunit) s = OK s' ->
-      match_cont cunit hf k k' ->
-      match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k')
-  | match_cont_block: forall cunit hf k k',
-      match_cont cunit hf k k' ->
-      match_cont cunit hf (Cminor.Kblock k) (Kblock k')
-  | match_cont_call: forall cunit' hf' cunit hf id f sp e k f' e' k',
+Inductive match_cont: Cminor.program -> helper_functions -> known_idents -> typenv -> Cminor.cont -> CminorSel.cont -> Prop :=
+  | match_cont_seq: forall cunit hf ki env s s' k k',
+      sel_stmt (prog_defmap cunit) ki env s = OK s' ->
+      match_cont cunit hf ki env k k' ->
+      match_cont cunit hf ki env (Cminor.Kseq s k) (Kseq s' k')
+  | match_cont_block: forall cunit hf ki env k k',
+      match_cont cunit hf ki env k k' ->
+      match_cont cunit hf ki env (Cminor.Kblock k) (Kblock k')
+  | match_cont_other: forall cunit hf ki env k k',
+      match_call_cont k k' ->
+      match_cont cunit hf ki env k k'
+
+with match_call_cont: Cminor.cont -> CminorSel.cont -> Prop :=
+  | match_cont_stop:
+      match_call_cont Cminor.Kstop Kstop
+  | match_cont_call: forall cunit hf env id f sp e k f' e' k',
       linkorder cunit prog ->
       helper_functions_declared cunit hf ->
       sel_function (prog_defmap cunit) hf f = OK f' ->
-      match_cont cunit hf k k' -> env_lessdef e e' ->
-      match_cont cunit' hf' (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').
-
-Definition match_call_cont (k: Cminor.cont) (k': CminorSel.cont) : Prop :=
-  forall cunit hf, match_cont cunit hf k k'.
+      type_function f = OK env ->
+      match_cont cunit hf (known_id f) env k k' ->
+      env_lessdef e e' ->
+      match_call_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').
 
 Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
-  | match_state: forall cunit hf f f' s k s' k' sp e m e' m'
+  | match_state: forall cunit hf f f' s k s' k' sp e m e' m' env
         (LINK: linkorder cunit prog)
         (HF: helper_functions_declared cunit hf)
         (TF: sel_function (prog_defmap cunit) hf f = OK f')
-        (TS: sel_stmt (prog_defmap cunit) s = OK s')
-        (MC: match_cont cunit hf k k')
+        (TYF: type_function f = OK env)
+        (TS: sel_stmt (prog_defmap cunit) (known_id f) env s = OK s')
+        (MC: match_cont cunit hf (known_id f) env k k')
         (LD: env_lessdef e e')
         (ME: Mem.extends m m'),
       match_states
@@ -794,11 +983,12 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
       match_states
         (Cminor.Returnstate v k m)
         (Returnstate v' k' m')
-  | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m'
+  | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m' env
         (LINK: linkorder cunit prog)
         (HF: helper_functions_declared cunit hf)
         (TF: sel_function (prog_defmap cunit) hf f = OK f')
-        (MC: match_cont cunit hf k k')
+        (TYF: type_function f = OK env)
+        (MC: match_cont cunit hf (known_id f) env k k')
         (LDA: Val.lessdef_list args args')
         (LDE: env_lessdef e e')
         (ME: Mem.extends m m')
@@ -806,11 +996,12 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
       match_states
         (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
         (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m')
-  | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k'
+  | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k' env
         (LINK: linkorder cunit prog)
         (HF: helper_functions_declared cunit hf)
         (TF: sel_function (prog_defmap cunit) hf f = OK f')
-        (MC: match_cont cunit hf k k')
+        (TYF: type_function f = OK env)
+        (MC: match_cont cunit hf (known_id f) env k k')
         (LDV: Val.lessdef v v')
         (LDE: env_lessdef e e')
         (ME: Mem.extends m m'),
@@ -819,23 +1010,23 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
         (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m').
 
 Remark call_cont_commut:
-  forall cunit hf k k', match_cont cunit hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k').
+  forall cunit hf ki env k k',
+  match_cont cunit hf ki env k k' -> match_call_cont (Cminor.call_cont k) (call_cont k').
 Proof.
-  induction 1; simpl; auto; red; intros.
-- constructor.
-- eapply match_cont_call with (hf := hf); eauto.
+  induction 1; simpl; auto. inversion H; subst; auto.
 Qed.
 
 Remark match_is_call_cont:
-  forall cunit hf k k', match_cont cunit hf k k' -> Cminor.is_call_cont k -> match_call_cont k k'.
+  forall cunit hf ki env k k',
+  match_cont cunit ki env hf k k' -> Cminor.is_call_cont k ->
+  match_call_cont k k' /\ is_call_cont k'.
 Proof.
-  destruct 1; intros; try contradiction; red; intros.
-- constructor.
-- eapply match_cont_call with (hf := hf); eauto.
+  destruct 1; intros; try contradiction. split; auto. inv H; auto.
 Qed.
 
+(*
 Remark match_call_cont_cont:
-  forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'.
+  forall k k', match_call_cont k k' -> exists cunit hf ki env, match_cont cunit hf ki env k k'.
 Proof.
   intros. simple refine (let cunit : Cminor.program := _ in _).
   econstructor. apply nil. apply nil. apply xH.
@@ -843,14 +1034,58 @@ Proof.
   econstructor; apply xH.
   exists cunit, hf; auto.
 Qed.
+*)
+
+Definition nolabel (s: Cminor.stmt) : Prop :=
+  forall lbl k, Cminor.find_label lbl s k = None.
+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 (hf: helper_functions) 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 &&
+            if_conversion_heuristic a a1 a2 (env id)); try discriminate.
+  destruct (sel_select_opt (env id) a a1 a2); inv H. 
+  red; auto.
+Qed.
+
+Lemma if_conversion_nolabel: forall (hf: helper_functions) 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.
 
 Remark find_label_commut:
-  forall cunit hf lbl s k s' k',
-  match_cont cunit hf k k' ->
-  sel_stmt (prog_defmap cunit) s = OK s' ->
+  forall cunit hf ki env lbl s k s' k',
+  match_cont cunit hf ki env k k' ->
+  sel_stmt (prog_defmap cunit) ki env s = OK s' ->
   match Cminor.find_label lbl s k, find_label lbl s' k' with
   | None, None => True
-  | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) s1 = OK s1' /\ match_cont cunit hf k1 k1'
+  | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) ki env s1 = OK s1' /\ match_cont cunit hf ki env k1 k1'
   | _, _ => False
   end.
 Proof.
@@ -867,7 +1102,11 @@ Proof.
   destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ];
   intuition. apply IHs2; auto.
 (* ifthenelse *)
-- exploit (IHs1 k); eauto.
+- destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC.
+  inv SE. exploit if_conversion_nolabel; eauto. intros (A & B & C).
+  rewrite A, B, C. auto.
+  monadInv SE; simpl.
+  exploit (IHs1 k); eauto.
   destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ];
   destruct (find_label lbl x k') as [[sy ky] | ];
   intuition. apply IHs2; auto.
@@ -896,20 +1135,22 @@ Definition measure (s: Cminor.state) : nat :=
 
 Lemma sel_step_correct:
   forall S1 t S2, Cminor.step ge S1 t S2 ->
-  forall T1, match_states S1 T1 ->
+  forall T1, match_states S1 T1 -> wt_state S1 ->
   (exists T2, step tge T1 t T2 /\ match_states S2 T2)
-  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat
+  \/ (exists S3 T2, star Cminor.step ge S2 E0 S3 /\ step tge T1 t T2 /\ match_states S3 T2).
 Proof.
-  induction 1; intros T1 ME; inv ME; try (monadInv TS).
+  induction 1; intros T1 ME WTS; inv ME; try (monadInv TS).
 - (* skip seq *)
   inv MC. left; econstructor; split. econstructor. econstructor; eauto.
+  inv H.
 - (* skip block *)
   inv MC. left; econstructor; split. econstructor. econstructor; eauto.
+  inv H.
 - (* skip call *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   left; econstructor; split.
-  econstructor. inv MC; simpl in H; simpl; auto.
-  eauto.
+  econstructor. eapply match_is_call_cont; eauto.
   erewrite stackspace_function_translated; eauto.
   econstructor; eauto. eapply match_is_call_cont; eauto.
 - (* assign *)
@@ -935,7 +1176,7 @@ Proof.
   econstructor; eauto. econstructor; eauto.
   eapply sig_function_translated; eauto.
   eapply match_callstate with (cunit := cunit'); eauto.
-  red; intros. eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
+  eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
 + (* direct *)
   intros [b [U V]].
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
@@ -945,11 +1186,11 @@ Proof.
   subst vf. econstructor; eauto. rewrite symbols_preserved; eauto.
   eapply sig_function_translated; eauto.
   eapply match_callstate with (cunit := cunit'); eauto.
-  red; intros; eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
+  eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
 + (* turned into Sbuiltin *)
   intros EQ. subst fd.
   exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]].
-  right; split. simpl. omega. split. auto.
+  right; left; split. simpl. omega. split. auto.
   econstructor; eauto.
 - (* Stailcall *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
@@ -978,7 +1219,13 @@ Proof.
   constructor.
   econstructor; eauto. constructor; auto.
 - (* Sifthenelse *)
-  exploit sel_expr_correct; eauto. intros [v' [A B]].
+  simpl in TS. destruct (if_conversion (known_id f) env a s1 s2) as [s|] eqn:IFC; monadInv TS.
++ inv WTS. inv WT_FN. assert (env0 = env) by congruence. subst env0. inv WT_STMT.
+  exploit if_conversion_correct; eauto.
+  set (s0 := if b then s1 else s2). intros (e1 & e1' & A & B & C).
+  right; right. econstructor; econstructor.
+  split. eexact B. split. eexact A. econstructor; eauto. 
++ exploit sel_expr_correct; eauto. intros [v' [A B]].
   assert (Val.bool_of_val v' b). inv B. auto. inv H0.
   left; exists (State f' (if b then x else x0) k' sp e' m'); split.
   econstructor; eauto. eapply eval_condexpr_of_expr; eauto.
@@ -990,10 +1237,13 @@ Proof.
   left; econstructor; split. constructor. econstructor; eauto. constructor; auto.
 - (* Sexit seq *)
   inv MC. left; econstructor; split. constructor. econstructor; eauto.
+  inv H.
 - (* Sexit0 block *)
   inv MC. left; econstructor; split. constructor. econstructor; eauto.
+  inv H.
 - (* SexitS block *)
   inv MC. left; econstructor; split. constructor. econstructor; eauto.
+  inv H.
 - (* Sswitch *)
   inv H0; simpl in TS.
 + set (ct := compile_switch Int.modulus default cases) in *.
@@ -1024,10 +1274,10 @@ Proof.
 - (* Slabel *)
   left; econstructor; split. constructor. econstructor; eauto.
 - (* Sgoto *)
-  assert (sel_stmt (prog_defmap cunit) (Cminor.fn_body f) = OK (fn_body f')).
-  { monadInv TF; simpl; auto. }
-  exploit (find_label_commut cunit hf lbl (Cminor.fn_body f) (Cminor.call_cont k)).
-    eapply call_cont_commut; eauto. eauto.
+  assert (sel_stmt (prog_defmap cunit) (known_id f) env (Cminor.fn_body f) = OK (fn_body f')).
+  { monadInv TF; simpl. congruence. }
+  exploit (find_label_commut cunit hf (known_id f) env lbl (Cminor.fn_body f) (Cminor.call_cont k)).
+    apply match_cont_other. eapply call_cont_commut; eauto. eauto.
   rewrite H.
   destruct (find_label lbl (fn_body f') (call_cont k'0))
   as [[s'' k'']|] eqn:?; intros; try contradiction.
@@ -1036,13 +1286,15 @@ Proof.
   econstructor; eauto.
   econstructor; eauto.
 - (* internal function *)
-  destruct TF as (hf & HF & TF). specialize (MC cunit hf).
+  destruct TF as (hf & HF & TF). 
   monadInv TF. generalize EQ; intros TF; monadInv TF.
   exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros [m2' [A B]].
   left; econstructor; split.
   econstructor; simpl; eauto.
-  econstructor; simpl; eauto. apply set_locals_lessdef. apply set_params_lessdef; auto.
+  econstructor; simpl; eauto.
+  apply match_cont_other; auto.
+  apply set_locals_lessdef. apply set_params_lessdef; auto.
 - (* external call *)
   destruct TF as (hf & HF & TF).
   monadInv TF.
@@ -1058,13 +1310,12 @@ Proof.
   econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 - (* return *)
-  apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC).
   inv MC.
   left; econstructor; split.
   econstructor.
   econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
 - (* return of an external call turned into a Sbuiltin *)
-  right; split. simpl; omega. split. auto. econstructor; eauto.
+  right; left; split. simpl; omega. split. auto. econstructor; eauto.
   apply sel_builtin_res_correct; auto.
 Qed.
 
@@ -1080,26 +1331,35 @@ Proof.
   rewrite (match_program_main TRANSF). fold tge. rewrite symbols_preserved. eauto.
   eexact A.
   rewrite <- H2. eapply sig_function_translated; eauto.
-  econstructor; eauto. red; intros; constructor. apply Mem.extends_refl.
+  econstructor; eauto. constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma sel_final_states:
   forall S R r,
   match_states S R -> Cminor.final_state S r -> final_state R r.
 Proof.
-  intros. inv H0. inv H.
-  apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC).
-  inv MC. inv LD. constructor.
+  intros. inv H0. inv H. inv MC. inv LD. constructor.
 Qed.
 
 Theorem transf_program_correct:
   forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog).
 Proof.
-  apply forward_simulation_opt with (match_states := match_states) (measure := measure).
-  apply senv_preserved.
-  apply sel_initial_states; auto.
-  apply sel_final_states; auto.
-  apply sel_step_correct; auto.
+  set (MS := fun S T => match_states S T /\ wt_state S).
+  apply forward_simulation_determ_star with (match_states := MS) (measure := measure).
+- apply Cminor.semantics_determinate.
+- apply senv_preserved.
+- intros. exploit sel_initial_states; eauto. intros (T & P & Q). 
+  exists T; split; auto; split; auto. eapply wt_initial_state. eexact wt_prog. auto. 
+- intros. destruct H. eapply sel_final_states; eauto.
+- intros S1 t S2 A T1 [B C].
+  assert (wt_state S2) by (eapply subject_reduction; eauto using wt_prog).
+  unfold MS.
+  exploit sel_step_correct; eauto.
+  intros [(T2 & D & E) | [(D & E & F) | (S3 & T2 & D & E & F)]].
++ exists S2, T2. intuition auto using star_refl, plus_one.
++ subst t. exists S2, T1. intuition auto using star_refl.
++ assert (wt_state S3) by (eapply subject_reduction_star; eauto using wt_prog).
+  exists S3, T2. intuition auto using plus_one.
 Qed.
 
 End PRESERVATION.
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v
index 916e111b..8ac7c4ce 100644
--- a/backend/Unusedglob.v
+++ b/backend/Unusedglob.v
@@ -107,7 +107,7 @@ Definition used_globals (p: program) (pm: prog_map) : option IS.t :=
 
 (** * Elimination of unreferenced global definitions *)
 
-(** We also eliminate multiple definitions of the same global name, keeping ony
+(** We also eliminate multiple definitions of the same global name, keeping only
   the last definition (in program definition order). *)
 
 Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef unit)) :=
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 7899a04c..680daba7 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -1160,10 +1160,10 @@ Local Transparent Mem.loadbytes.
   generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1.
   generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2.
   rewrite Z.add_0_r.
-  apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))).
+  apply Mem_getN_forall2 with (p := 0) (n := Z.to_nat (init_data_list_size (gvar_init v))).
   rewrite H3, H4. apply bytes_of_init_inject. auto.
   omega.
-  rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega.
+  rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). omega.
 Qed.
 
 Lemma init_mem_inj_2:
@@ -1373,9 +1373,9 @@ Proof.
   * apply Y with id; auto.
   * exists gd1; auto.
   * exists gd2; auto.
-  * eapply used_not_defined_2 in GD1; eauto. eapply used_not_defined_2 in GD2; eauto.
+  * eapply used_not_defined_2 in GD1; [ | eauto | congruence ].
+    eapply used_not_defined_2 in GD2; [ | eauto | congruence ].
     tauto.
-    congruence.
   }
   destruct E as [g LD].
   left. unfold prog_defs_names; simpl.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index e7e44e29..f6afa836 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -11,7 +11,7 @@
 (* *********************************************************************)
 
 Require Import FunInd.
-Require Import Zwf Coqlib Maps Integers Floats Lattice.
+Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Events.
 Require Import Registers RTL.
@@ -1492,12 +1492,12 @@ Proof.
   inv H; auto with va.
 - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto.
   generalize (Int.unsigned_range n); intros.
-  rewrite Zmod_small by omega.
+  rewrite Z.mod_small by omega.
   apply H1. omega. omega.
 - destruct (zlt n0 Int.zwordsize); auto with va.
   apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega.
   generalize (Int.unsigned_range n); intros.
-  rewrite ! Zmod_small by omega.
+  rewrite ! Z.mod_small by omega.
   rewrite H1 by omega. symmetry. rewrite H1 by omega. auto.
 - destruct (zlt n0 Int.zwordsize); auto with va.
 Qed.
@@ -1670,7 +1670,7 @@ Proof.
   assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
   {
     intros. apply is_uns_mon with (usize (Int.modu i j)); auto with va.
-    unfold usize, Int.size. apply Int.Zsize_monotone.
+    unfold usize, Int.size. apply Zsize_monotone.
     generalize (Int.unsigned_range_2 j); intros RANGE.
     assert (Int.unsigned j <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
@@ -2824,6 +2824,64 @@ Proof.
   intros. inv H; simpl in H0; congruence.
 Qed.
 
+(** Select either returns one of its arguments, or Vundef. *)
+
+Definition add_undef (x: aval) :=
+  match x with
+  | Vbot => ntop
+  | I i =>
+      if Int.lt i Int.zero
+      then sgn Pbot (ssize i)
+      else uns Pbot (usize i)
+  | L _ | F _ | FS _ => ntop
+  | _ => x
+  end.
+
+Lemma add_undef_sound:
+  forall v x, vmatch v x -> vmatch v (add_undef x).
+Proof.
+  destruct 1; simpl; auto with va.
+  destruct (Int.lt i Int.zero).
+  apply vmatch_sgn; apply is_sgn_ssize.
+  apply vmatch_uns; apply is_uns_usize.
+Qed.
+
+Lemma add_undef_undef:
+  forall x, vmatch Vundef (add_undef x).
+Proof.
+  destruct x; simpl; auto with va.
+  destruct (Int.lt n Int.zero); auto with va.
+Qed.
+
+Lemma add_undef_normalize:
+  forall v x ty, vmatch v x -> vmatch (Val.normalize v ty) (add_undef x).
+Proof.
+  intros. destruct (Val.lessdef_normalize v ty);
+  auto using add_undef_sound, add_undef_undef.
+Qed.
+
+Definition select (ab: abool) (x y: aval) :=
+  match ab with
+  | Bnone => ntop
+  | Just b | Maybe b => add_undef (if b then x else y)
+  | Btop => add_undef (vlub x y)
+  end.
+
+Lemma select_sound:
+  forall ob v w ab x y ty,
+  cmatch ob ab -> vmatch v x -> vmatch w y ->
+  vmatch (Val.select ob v w ty) (select ab x y).
+Proof.
+  unfold Val.select, select; intros. inv H.
+- auto with va.
+- apply add_undef_normalize; destruct b; auto.
+- apply add_undef_undef.
+- apply add_undef_normalize; destruct b; auto.
+- destruct ob as [b|]. 
++ apply add_undef_normalize. destruct b; [apply vmatch_lub_l|apply vmatch_lub_r]; auto.
++ apply add_undef_undef.
+Qed.
+
 (** Normalization at load time *)
 
 Definition vnormalize (chunk: memory_chunk) (v: aval) :=
@@ -3134,7 +3192,7 @@ Proof.
     omega.
     intros (bytes1 & bytes2 & LOAD1 & LOAD2 & CONCAT).
     subst bytes.
-    exploit Mem.loadbytes_length. eexact LOAD1. change (nat_of_Z 1) with 1%nat. intros LENGTH1.
+    exploit Mem.loadbytes_length. eexact LOAD1. change (Z.to_nat 1) with 1%nat. intros LENGTH1.
     rewrite in_app_iff in IN. destruct IN.
   * destruct bytes1; try discriminate. destruct bytes1; try discriminate.
     simpl in H. destruct H; try contradiction. subst m0.
@@ -3492,7 +3550,7 @@ Qed.
 Lemma ablock_storebytes_sound:
   forall m b ofs bytes m' p ab sz,
   Mem.storebytes m b ofs bytes = Some m' ->
-  length bytes = nat_of_Z sz ->
+  length bytes = Z.to_nat sz ->
   (forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p) ->
   bmatch m b ab ->
   bmatch m' b (ablock_storebytes ab p ofs sz).
@@ -3509,7 +3567,7 @@ Proof.
   exploit ablock_storebytes_contents; eauto. intros [A B].
   assert (Mem.load chunk' m b ofs' = Some v').
   { rewrite <- LOAD'; symmetry. eapply Mem.load_storebytes_other; eauto.
-    rewrite U. rewrite LENGTH. rewrite nat_of_Z_max. right; omega. }
+    rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; omega. }
   exploit BM2; eauto. unfold ablock_load. rewrite A. rewrite COMPAT. auto.
 Qed.
 
@@ -3992,7 +4050,7 @@ Theorem storebytes_sound:
   Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
   mmatch m am ->
   pmatch b ofs p ->
-  length bytes = nat_of_Z sz ->
+  length bytes = Z.to_nat sz ->
   (forall b' ofs' qt i, In (Fragment (Vptr b' ofs') qt i) bytes -> pmatch b' ofs' q) ->
   mmatch m' (storebytes am p sz q).
 Proof.