Merge of branches/full-expr-4:

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



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

9 files changed, 1404 insertions, 168 deletions

diff --git a/backend/CastOptim.v b/backend/CastOptim.v
new file mode 100644
index 00000000..3ae5ab0b
--- /dev/null
+++ b/backend/CastOptim.v
@@ -0,0 +1,276 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Elimination of redundant conversions to small numerical types. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Lattice.
+Require Import Kildall.
+
+(** * Static analysis *)
+
+(** Compile-time approximations *)
+
+Inductive approx : Type :=
+  | Unknown               (**r any value *)
+  | Int7                  (**r [[0,127]] *)
+  | Int8s                 (**r [[-128,127] *)
+  | Int8u                 (**r [[0,255]] *)
+  | Int15                 (**r [[0,32767]] *)
+  | Int16s                (**r [[-32768,32767]] *)
+  | Int16u                (**r [[0,65535] *)
+  | Single                (**r single-precision float *)
+  | Novalue.              (**r empty *)
+
+(** We equip this type of approximations with a semi-lattice structure.
+  The ordering is inclusion between the sets of values denoted by
+  the approximations. *)
+
+Module Approx <: SEMILATTICE_WITH_TOP.
+  Definition t := approx.
+  Definition eq (x y: t) := (x = y).
+  Definition eq_refl: forall x, eq x x := (@refl_equal t).
+  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
+  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
+  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
+  Proof.
+    decide equality.
+  Qed.
+  Definition beq (x y: t) := if eq_dec x y then true else false.
+  Lemma beq_correct: forall x y, beq x y = true -> x = y.
+  Proof.
+    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
+  Qed.
+  Definition ge (x y: t) : Prop :=
+    match x, y with
+    | Unknown, _ => True
+    | _, Novalue => True
+    | Int7, Int7 => True
+    | Int8s, (Int7 | Int8s) => True
+    | Int8u, (Int7 | Int8u) => True
+    | Int15, (Int7 | Int8u | Int15) => True
+    | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => True
+    | Int16u, (Int7 | Int8u | Int15 | Int16u) => True
+    | Single, Single => True
+    | _, _ => False
+    end.
+  Lemma ge_refl: forall x y, eq x y -> ge x y.
+  Proof.
+    unfold eq, ge; intros. subst y. destruct x; auto.
+  Qed.
+  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Proof.
+    unfold ge; intros.
+    destruct x; auto; (destruct y; auto; try contradiction; destruct z; auto).
+  Qed.
+  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
+  Proof.
+    unfold eq; intros. congruence.
+  Qed.
+  Definition bge (x y: t) : bool :=
+    match x, y with
+    | Unknown, _ => true
+    | _, Novalue => true
+    | Int7, Int7 => true
+    | Int8s, (Int7 | Int8s) => true
+    | Int8u, (Int7 | Int8u) => true
+    | Int15, (Int7 | Int8u | Int15) => true
+    | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => true
+    | Int16u, (Int7 | Int8u | Int15 | Int16u) => true
+    | Single, Single => true
+    | _, _ => false
+    end.
+  Lemma bge_correct: forall x y, bge x y = true -> ge x y.
+  Proof.
+    destruct x; destruct y; simpl; auto || congruence.
+  Qed.
+  Definition bot := Novalue.
+  Definition top := Unknown.
+  Lemma ge_bot: forall x, ge x bot.
+  Proof.
+    unfold ge, bot. destruct x; auto. 
+  Qed.
+  Lemma ge_top: forall x, ge top x.
+  Proof.
+    unfold ge, top. auto.
+  Qed.
+  Definition lub (x y: t) : t :=
+    match x, y with
+    | Novalue, _ => y
+    | _, Novalue => x
+    | Int7, Int7 => Int7
+    | Int7, Int8u => Int8u
+    | Int7, Int8s => Int8s
+    | Int7, Int15 => Int15
+    | Int7, Int16u => Int16u
+    | Int7, Int16s => Int16s
+    | Int8u, (Int7|Int8u) => Int8u
+    | Int8u, Int15 => Int15
+    | Int8u, Int16u => Int16u
+    | Int8u, Int16s => Int16s
+    | Int8s, (Int7|Int8s) => Int8s
+    | Int8s, (Int15|Int16s) => Int16s
+    | Int15, (Int7|Int8u|Int15) => Int15
+    | Int15, Int16u => Int16u
+    | Int15, (Int8s|Int16s) => Int16s
+    | Int16u, (Int7|Int8u|Int15|Int16u) => Int16u
+    | Int16s, (Int7|Int8u|Int8s|Int15|Int16s) => Int16s
+    | Single, Single => Single
+    | _, _ => Unknown
+    end.
+  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
+  Proof.
+    unfold lub, eq; intros.
+    destruct x; destruct y; auto.
+  Qed.
+  Lemma ge_lub_left: forall x y, ge (lub x y) x.
+  Proof.
+    unfold lub, ge; intros.
+    destruct x; destruct y; auto. 
+  Qed.
+End Approx.
+
+Module D := LPMap Approx.
+
+(** Abstract interpretation of operators *)
+
+Definition approx_bitwise_op (v1 v2: approx) : approx :=
+  if Approx.bge Int8u v1 && Approx.bge Int8u v2 then Int8u
+  else if Approx.bge Int16u v1 && Approx.bge Int16u v2 then Int16u
+  else Unknown.
+
+Function approx_operation (op: operation) (vl: list approx) : approx :=
+  match op, vl with
+  | Omove, v1 :: nil => v1
+  | Ointconst n, _ =>
+      if Int.eq_dec n (Int.zero_ext 7 n) then Int7
+      else if Int.eq_dec n (Int.zero_ext 8 n) then Int8u
+      else if Int.eq_dec n (Int.sign_ext 8 n) then Int8s
+      else if Int.eq_dec n (Int.zero_ext 15 n) then Int15
+      else if Int.eq_dec n (Int.zero_ext 16 n) then Int16u
+      else if Int.eq_dec n (Int.sign_ext 16 n) then Int16s
+      else Unknown
+  | Ofloatconst n, _ =>
+      if Float.eq_dec n (Float.singleoffloat n) then Single else Unknown
+  | Ocast8signed, _ => Int8s
+  | Ocast8unsigned, _ => Int8u
+  | Ocast16signed, _ => Int16s
+  | Ocast16unsigned, _ => Int16u
+  | Osingleoffloat, _ => Single
+  | Oand, v1 :: v2 :: nil => approx_bitwise_op v1 v2
+  | Oor, v1 :: v2 :: nil => approx_bitwise_op v1 v2
+  | Oxor, v1 :: v2 :: nil => approx_bitwise_op v1 v2
+  (* Problem: what about and/or/xor immediate? and other
+     machine-specific operators? *)
+  | Ocmp c, _ => Int7
+  | _, _ => Unknown
+  end.
+
+Definition approx_of_chunk (chunk: memory_chunk) :=
+  match chunk with
+  | Mint8signed => Int8s
+  | Mint8unsigned => Int8u
+  | Mint16signed => Int16s
+  | Mint16unsigned => Int16u
+  | Mint32 => Unknown
+  | Mfloat32 => Single
+  | Mfloat64 => Unknown
+  end.
+
+(** Transfer function for the analysis *)
+
+Definition approx_reg (app: D.t) (r: reg) := 
+  D.get r app.
+
+Definition approx_regs (app: D.t) (rl: list reg):=
+  List.map (approx_reg app) rl.
+
+Definition transfer (f: function) (pc: node) (before: D.t) :=
+  match f.(fn_code)!pc with
+  | None => before
+  | Some i =>
+      match i with
+      | Iop op args res s =>
+          let a := approx_operation op (approx_regs before args) in
+          D.set res a before
+      | Iload chunk addr args dst s =>
+          D.set dst (approx_of_chunk chunk) before
+      | Icall sig ros args res s =>
+          D.set res Unknown before
+      | Ibuiltin ef args res s =>
+          D.set res Unknown before
+      | _ =>
+          before
+      end
+  end.
+
+(** The static analysis is a forward dataflow analysis. *)
+
+Module DS := Dataflow_Solver(D)(NodeSetForward).
+
+Definition analyze (f: RTL.function): PMap.t D.t :=
+  match DS.fixpoint (successors f) (transfer f) 
+                    ((f.(fn_entrypoint), D.top) :: nil) with
+  | None => PMap.init D.top
+  | Some res => res
+  end.
+
+(** * Code transformation *)
+
+(** Cast operations that have no effect (because the argument is already
+    in the right range) are turned into moves. *)
+
+Function transf_operation (op: operation) (vl: list approx) : operation :=
+  match op, vl with
+  | Ocast8signed, v :: nil => if Approx.bge Int8s v then Omove else op
+  | Ocast8unsigned, v :: nil => if Approx.bge Int8u v then Omove else op
+  | Ocast16signed, v :: nil => if Approx.bge Int16s v then Omove else op
+  | Ocast16unsigned, v :: nil => if Approx.bge Int16u v then Omove else op
+  | Osingleoffloat, v :: nil => if Approx.bge Single v then Omove else op
+  | _, _ => op
+  end.
+
+Definition transf_instr (app: D.t) (instr: instruction) :=
+  match instr with
+  | Iop op args res s =>
+      let op' := transf_operation op (approx_regs app args) in
+      Iop op' args res s
+  | _ =>
+      instr
+  end.
+
+Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
+  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
+
+Definition transf_function (f: function) : function :=
+  let approxs := analyze f in
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (transf_code approxs f.(fn_code))
+    f.(fn_entrypoint).
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v
new file mode 100644
index 00000000..60b10c2c
--- /dev/null
+++ b/backend/CastOptimproof.v
@@ -0,0 +1,577 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for cast optimization. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Events.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Smallstep.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Lattice.
+Require Import Kildall.
+Require Import CastOptim.
+
+(** * Correctness of the static analysis *)
+
+Section ANALYSIS.
+
+Definition val_match_approx (a: approx) (v: val) : Prop :=
+  match a with
+  | Novalue => False
+  | Int7 => v = Val.zero_ext 8 v /\ v = Val.sign_ext 8 v
+  | Int8u => v = Val.zero_ext 8 v
+  | Int8s => v = Val.sign_ext 8 v
+  | Int15 => v = Val.zero_ext 16 v /\ v = Val.sign_ext 16 v
+  | Int16u => v = Val.zero_ext 16 v
+  | Int16s => v = Val.sign_ext 16 v
+  | Single => v = Val.singleoffloat v
+  | Unknown => True
+  end.
+
+Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
+  forall r, val_match_approx (D.get r a) rs#r.
+
+Lemma regs_match_approx_top:
+  forall rs, regs_match_approx D.top rs.
+Proof.
+  intros. red; intros. simpl. rewrite PTree.gempty. 
+  unfold Approx.top, val_match_approx. auto.
+Qed.
+
+Lemma val_match_approx_increasing:
+  forall a1 a2 v,
+  Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v.
+Proof.
+  assert (A: forall v, v = Val.zero_ext 8 v -> v = Val.zero_ext 16 v).
+    intros. rewrite H.
+    destruct v; simpl; auto. decEq. symmetry. 
+    apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
+  assert (B: forall v, v = Val.sign_ext 8 v -> v = Val.sign_ext 16 v).
+    intros. rewrite H.
+    destruct v; simpl; auto. decEq. symmetry. 
+    apply Int.sign_ext_widen. compute; auto. split. omega. compute; auto.
+  assert (C: forall v, v = Val.zero_ext 8 v -> v = Val.sign_ext 16 v).
+    intros. rewrite H.
+    destruct v; simpl; auto. decEq. symmetry. 
+    apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto.
+  intros. destruct a1; destruct a2; simpl in *; intuition; auto.
+Qed.
+
+Lemma regs_match_approx_increasing:
+  forall a1 a2 rs,
+  D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.
+Proof.
+  unfold D.ge, regs_match_approx. intros.
+  apply val_match_approx_increasing with (D.get r a2); auto.
+Qed.
+
+Lemma regs_match_approx_update:
+  forall ra rs a v r,
+  val_match_approx a v ->
+  regs_match_approx ra rs ->
+  regs_match_approx (D.set r a ra) (rs#r <- v).
+Proof.
+  intros; red; intros. rewrite Regmap.gsspec. 
+  case (peq r0 r); intro.
+  subst r0. rewrite D.gss. auto.
+  rewrite D.gso; auto. 
+Qed.
+
+Lemma approx_regs_val_list:
+  forall ra rs rl,
+  regs_match_approx ra rs ->
+  list_forall2 val_match_approx (approx_regs ra rl) rs##rl.
+Proof.
+  induction rl; simpl; intros.
+  constructor.
+  constructor. apply H. auto.
+Qed.
+
+Lemma analyze_correct:
+  forall f pc rs pc' i,
+  f.(fn_code)!pc = Some i ->
+  In pc' (successors_instr i) ->
+  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
+  regs_match_approx (analyze f)!!pc' rs.
+Proof.
+  intros until i. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
+                      ((fn_entrypoint f, D.top) :: nil)).
+  intros approxs; intros.
+  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
+  eapply DS.fixpoint_solution; eauto.
+  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
+  auto.
+  intros. rewrite PMap.gi. apply regs_match_approx_top. 
+Qed.
+
+Lemma analyze_correct_start:
+  forall f rs,
+  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
+Proof.
+  intros. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
+                      ((fn_entrypoint f, D.top) :: nil)).
+  intros approxs; intros.
+  apply regs_match_approx_increasing with D.top.
+  eapply DS.fixpoint_entry; eauto. auto with coqlib.
+  apply regs_match_approx_top. 
+  intros. rewrite PMap.gi. apply regs_match_approx_top.
+Qed.
+
+Lemma approx_bitwise_correct:
+  forall (sem_op: int -> int -> int) a1 n1 a2 n2,
+  (forall a b c, sem_op (Int.and a c) (Int.and b c) = Int.and (sem_op a b) c) ->
+  val_match_approx a1 (Vint n1) -> val_match_approx a2 (Vint n2) ->
+  val_match_approx (approx_bitwise_op a1 a2) (Vint (sem_op n1 n2)).
+Proof.
+  intros.
+  assert (forall N, 0 < N < Z_of_nat Int.wordsize ->
+    sem_op (Int.zero_ext N n1) (Int.zero_ext N n2) =
+    Int.zero_ext N (sem_op (Int.zero_ext N n1) (Int.zero_ext N n2))).
+  intros. repeat rewrite Int.zero_ext_and; auto. rewrite H. 
+  rewrite Int.and_assoc. rewrite Int.and_idem. auto.
+  unfold approx_bitwise_op. 
+  caseEq (Approx.bge Int8u a1 && Approx.bge Int8u a2); intro EQ1.
+  destruct (andb_prop _ _ EQ1).
+  assert (V1: val_match_approx Int8u (Vint n1)).
+    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
+  assert (V2: val_match_approx Int8u (Vint n2)).
+    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
+  simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto.
+  caseEq (Approx.bge Int16u a1 && Approx.bge Int16u a2); intro EQ2.
+  destruct (andb_prop _ _ EQ2).
+  assert (V1: val_match_approx Int16u (Vint n1)).
+    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
+  assert (V2: val_match_approx Int16u (Vint n2)).
+    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
+  simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto.
+  exact I.
+Qed.
+
+Lemma approx_operation_correct:
+  forall app rs (ge: genv) sp op args v,
+  regs_match_approx app rs ->
+  eval_operation ge sp op rs##args = Some v ->
+  val_match_approx (approx_operation op (approx_regs app args)) v.
+Proof.
+  intros. destruct op; simpl; try (exact I). 
+(* move *)
+  destruct args; try (exact I). destruct args; try (exact I). 
+  simpl. simpl in H0. inv H0. apply H. 
+(* const int *)
+  destruct args; simpl in H0; inv H0.
+  destruct (Int.eq_dec i (Int.zero_ext 7 i)). red; simpl.
+    split.
+    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
+    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. 
+  destruct (Int.eq_dec i (Int.zero_ext 8 i)). red; simpl; congruence.
+  destruct (Int.eq_dec i (Int.sign_ext 8 i)). red; simpl; congruence.
+  destruct (Int.eq_dec i (Int.zero_ext 15 i)). red; simpl.
+    split.
+    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
+    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. 
+  destruct (Int.eq_dec i (Int.zero_ext 16 i)). red; simpl; congruence.
+  destruct (Int.eq_dec i (Int.sign_ext 16 i)). red; simpl; congruence.
+  exact I.
+(* const float *)
+  destruct args; simpl in H0; inv H0. 
+  destruct (Float.eq_dec f (Float.singleoffloat f)). red; simpl; congruence.
+  exact I.
+(* cast8signed *)
+  destruct args; simpl in H0; try congruence.
+  destruct args; simpl in H0; try congruence.
+  inv H0. destruct (rs#p); simpl; auto.
+  decEq. symmetry. apply Int.sign_ext_idem. compute; auto.
+(* cast8unsigned *)
+  destruct args; simpl in H0; try congruence.
+  destruct args; simpl in H0; try congruence.
+  inv H0. destruct (rs#p); simpl; auto.
+  decEq. symmetry. apply Int.zero_ext_idem. compute; auto.
+(* cast16signed *)
+  destruct args; simpl in H0; try congruence.
+  destruct args; simpl in H0; try congruence.
+  inv H0. destruct (rs#p); simpl; auto.
+  decEq. symmetry. apply Int.sign_ext_idem. compute; auto.
+(* cast16unsigned *)
+  destruct args; simpl in H0; try congruence.
+  destruct args; simpl in H0; try congruence.
+  inv H0. destruct (rs#p); simpl; auto.
+  decEq. symmetry. apply Int.zero_ext_idem. compute; auto.
+(* and *)
+  destruct args; try (exact I).
+  destruct args; try (exact I).
+  destruct args; try (exact I).
+  generalize (H p) (H p0). simpl in *. FuncInv. subst. 
+  apply approx_bitwise_correct; auto.
+  intros. repeat rewrite Int.and_assoc. decEq. 
+  rewrite (Int.and_commut b c). rewrite <- Int.and_assoc. rewrite Int.and_idem. auto.
+(* or *)
+  destruct args; try (exact I).
+  destruct args; try (exact I).
+  destruct args; try (exact I).
+  generalize (H p) (H p0). simpl in *. FuncInv. subst. 
+  apply approx_bitwise_correct; auto.
+  intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). 
+  rewrite <- Int.and_or_distrib. apply Int.and_commut.
+(* xor *)
+  destruct args; try (exact I).
+  destruct args; try (exact I).
+  destruct args; try (exact I).
+  generalize (H p) (H p0). simpl in *. FuncInv. subst. 
+  apply approx_bitwise_correct; auto.
+  intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). 
+  rewrite <- Int.and_xor_distrib. apply Int.and_commut.
+(* singleoffloat *)
+  destruct args; simpl in H0; try congruence.
+  destruct args; simpl in H0; try congruence.
+  inv H0. destruct (rs#p); simpl; auto.
+  decEq. rewrite Float.singleoffloat_idem; auto.
+(* comparison *)
+  simpl in H0. destruct (eval_condition c rs##args); try discriminate.
+  destruct b; inv H0; auto.
+Qed.
+
+Lemma approx_of_chunk_correct:
+  forall chunk m a v,
+  Mem.loadv chunk m a = Some v ->
+  val_match_approx (approx_of_chunk chunk) v.
+Proof.
+  intros. destruct a; simpl in H; try discriminate.
+  exploit Mem.load_cast; eauto. 
+  destruct chunk; intros; simpl; auto.
+Qed.
+
+End ANALYSIS.
+
+(** * Correctness of the code transformation *)
+
+Section PRESERVATION.
+
+Variable prog: program.
+Let tprog := transf_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  intros; unfold ge, tge, tprog, transf_program. 
+  apply Genv.find_symbol_transf.
+Qed.
+
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof.
+  intros; unfold ge, tge, tprog, transf_program. 
+  apply Genv.find_var_info_transf.
+Qed.
+
+Lemma functions_translated:
+  forall (v: val) (f: fundef),
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof.  
+  intros.
+  exact (Genv.find_funct_transf transf_fundef _ _ H).
+Qed.
+
+Lemma function_ptr_translated:
+  forall (b: block) (f: fundef),
+  Genv.find_funct_ptr ge b = Some f ->
+  Genv.find_funct_ptr tge b = Some (transf_fundef f).
+Proof.  
+  intros. 
+  exact (Genv.find_funct_ptr_transf transf_fundef _ _ H).
+Qed.
+
+Lemma sig_function_translated:
+  forall f,
+  funsig (transf_fundef f) = funsig f.
+Proof.
+  intros. destruct f; reflexivity.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  intros. destruct ros; simpl in *. 
+  apply functions_translated; auto. 
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence.
+  apply function_ptr_translated; auto.
+Qed.
+
+(** Correctness of [transf_operation]. *)
+
+Lemma transf_operation_correct:
+  forall (ge: genv) app rs sp op args v,
+  regs_match_approx app rs ->
+  eval_operation ge sp op rs##args = Some v ->
+  eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args = Some v.
+Proof.
+  intros until v. intro RMA.
+  assert (A: forall a r, Approx.bge a (approx_reg app r) = true -> val_match_approx a rs#r).
+    intros. eapply val_match_approx_increasing. apply Approx.bge_correct; eauto. apply RMA.
+Opaque Approx.bge.
+  destruct op; simpl; auto.
+(* cast8signed *)
+  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
+  intros EQ; inv EQ.
+  caseEq (Approx.bge Int8s (approx_reg app p)); intros.
+  exploit A; eauto. unfold val_match_approx. simpl. congruence.
+  auto.
+(* cast8unsigned *)
+  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
+  intros EQ; inv EQ.
+  caseEq (Approx.bge Int8u (approx_reg app p)); intros.
+  exploit A; eauto. unfold val_match_approx. simpl. congruence.
+  auto.
+(* cast8signed *)
+  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
+  intros EQ; inv EQ.
+  caseEq (Approx.bge Int16s (approx_reg app p)); intros.
+  exploit A; eauto. unfold val_match_approx. simpl. congruence.
+  auto.
+(* cast8unsigned *)
+  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
+  intros EQ; inv EQ.
+  caseEq (Approx.bge Int16u (approx_reg app p)); intros.
+  exploit A; eauto. unfold val_match_approx. simpl. congruence.
+  auto.
+(* singleoffloat *)
+  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
+  intros EQ; inv EQ.
+  caseEq (Approx.bge Single (approx_reg app p)); intros.
+  exploit A; eauto. unfold val_match_approx. simpl. congruence.
+  auto.
+Qed.
+
+(** Matching between states. *)
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+   match_stackframe_intro:
+      forall res sp pc rs f,
+      (forall v, regs_match_approx (analyze f)!!pc (rs#res <- v)) ->
+    match_stackframes
+        (Stackframe res f sp pc rs)
+        (Stackframe res (transf_function f) sp pc rs).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro:
+      forall s sp pc rs m f s'
+           (MATCH: regs_match_approx (analyze f)!!pc rs)
+           (STACKS: list_forall2 match_stackframes s s'),
+      match_states (State s f sp pc rs m)
+                   (State s' (transf_function f) sp pc rs m)
+  | match_states_call:
+      forall s f args m s',
+      list_forall2 match_stackframes s s' ->
+      match_states (Callstate s f args m)
+                   (Callstate s' (transf_fundef f) args m)
+  | match_states_return:
+      forall s s' v m,
+      list_forall2 match_stackframes s s' ->
+      match_states (Returnstate s v m)
+                   (Returnstate s' v m).
+
+Ltac TransfInstr :=
+  match goal with
+  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
+      cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr));
+      [ simpl transf_instr
+      | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
+        unfold option_map; rewrite H1; reflexivity ]
+  end.
+
+(** The proof of semantic preservation follows from the lock-step simulation lemma below. *)
+
+Lemma transf_step_correct:
+  forall s1 t s2,
+  step ge s1 t s2 ->
+  forall s1' (MS: match_states s1 s1'),
+  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
+Proof.
+  induction 1; intros; inv MS.
+
+  (* Inop *)
+  econstructor; split. 
+  TransfInstr; intro. eapply exec_Inop; eauto.
+  econstructor; eauto.
+  eapply analyze_correct with (pc := pc); eauto.
+  simpl; auto.
+  unfold transfer; rewrite H. auto.
+
+  (* Iop *)
+  exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
+  TransfInstr; intro. eapply exec_Iop; eauto.
+  apply transf_operation_correct; auto.
+  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  econstructor; eauto.
+  eapply analyze_correct with (pc := pc); eauto.
+  simpl; auto.
+  unfold transfer; rewrite H. apply regs_match_approx_update; auto. 
+  eapply approx_operation_correct; eauto. 
+
+  (* Iload *)
+  econstructor; split. 
+  TransfInstr; intro. eapply exec_Iload; eauto.
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  econstructor; eauto.
+  eapply analyze_correct with (pc := pc); eauto.
+  simpl; auto.
+  unfold transfer; rewrite H. apply regs_match_approx_update; auto.
+  eapply approx_of_chunk_correct; eauto. 
+
+  (* Istore *)
+  econstructor; split. 
+  TransfInstr; intro. eapply exec_Istore; eauto.
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  econstructor; eauto.
+  eapply analyze_correct with (pc := pc); eauto.
+  simpl; auto.
+  unfold transfer; rewrite H. auto.
+
+  (* Icall *)
+  TransfInstr; intro.
+  econstructor; split.
+  eapply exec_Icall. eauto. apply find_function_translated; eauto.
+  apply sig_function_translated; auto.
+  constructor; auto. constructor; auto.
+  econstructor; eauto. 
+  intros. eapply analyze_correct; eauto. simpl; auto.
+  unfold transfer; rewrite H.
+  apply regs_match_approx_update; auto. exact I.
+
+  (* Itailcall *)
+  TransfInstr; intro.
+  econstructor; split.
+  eapply exec_Itailcall. eauto. apply find_function_translated; eauto.
+  apply sig_function_translated; auto.
+  simpl; eauto. 
+  constructor; auto.
+
+  (* Ibuiltin *)
+  TransfInstr. intro.
+  exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split.
+  eapply exec_Ibuiltin; eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto. 
+  eapply analyze_correct; eauto. simpl; auto. 
+  unfold transfer; rewrite H. 
+  apply regs_match_approx_update; auto. exact I.
+
+  (* Icond, true *)
+  exists (State s' (transf_function f) sp ifso rs m); split. 
+  TransfInstr. intro.
+  eapply exec_Icond_true; eauto.
+  econstructor; eauto.
+  eapply analyze_correct; eauto.
+  simpl; auto.
+  unfold transfer; rewrite H; auto.
+
+  (* Icond, false *)
+  exists (State s' (transf_function f) sp ifnot rs m); split. 
+  TransfInstr. intro.
+  eapply exec_Icond_false; eauto.
+  econstructor; eauto.
+  eapply analyze_correct; eauto.
+  simpl; auto.
+  unfold transfer; rewrite H; auto.
+
+  (* Ijumptable *)
+  exists (State s' (transf_function f) sp pc' rs m); split.
+  TransfInstr. intro.
+  eapply exec_Ijumptable; eauto.
+  constructor; auto.
+  eapply analyze_correct; eauto.
+  simpl. eapply list_nth_z_in; eauto.
+  unfold transfer; rewrite  H; auto.
+
+  (* Ireturn *)
+  exists (Returnstate s' (regmap_optget or Vundef rs) m'); split.
+  eapply exec_Ireturn; eauto. TransfInstr; auto.
+  constructor; auto.
+
+  (* internal function *)
+  simpl. unfold transf_function.
+  econstructor; split.
+  eapply exec_function_internal; simpl; eauto.
+  simpl. econstructor; eauto.
+  apply analyze_correct_start; auto.
+
+  (* external function *)
+  simpl. econstructor; split.
+  eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  constructor; auto.
+
+  (* return *)
+  inv H3. inv H1. 
+  econstructor; split.
+  eapply exec_return; eauto. 
+  econstructor; eauto. 
+Qed.
+
+Lemma transf_initial_states:
+  forall st1, initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inversion H.
+  exploit function_ptr_translated; eauto. intro FIND.
+  exists (Callstate nil (transf_fundef f) nil m0); split.
+  econstructor; eauto.
+  apply Genv.init_mem_transf; auto.
+  replace (prog_main tprog) with (prog_main prog).
+  rewrite symbols_preserved. eauto.
+  reflexivity.
+  rewrite <- H3. apply sig_function_translated.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r, 
+  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+Proof.
+  intros. inv H0. inv H. inv H4. constructor. 
+Qed.
+
+(** The preservation of the observable behavior of the program then
+  follows, using the generic preservation theorem
+  [Smallstep.simulation_step_preservation]. *)
+
+Theorem transf_program_correct:
+  forall (beh: program_behavior), not_wrong beh ->
+  exec_program prog beh -> exec_program tprog beh.
+Proof.
+  unfold exec_program; intros.
+  eapply simulation_step_preservation; eauto.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact transf_step_correct. 
+Qed.
+
+End PRESERVATION.
+
+
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index 63f21906..922506f0 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -39,6 +39,7 @@ open Conventions
 type node =
   { ident: int;                         (*r unique identifier *)
     typ: typ;                           (*r its type *)
+    regname: reg option;                (*r the RTL register it comes from *)
     regclass: int;                      (*r identifier of register class *)
     mutable spillcost: float;           (*r estimated cost of spilling *)
     mutable adjlist: node list;         (*r all nodes it interferes with *)
@@ -84,14 +85,15 @@ and movestate =
 
 (*i
 let name_of_node n =
-  match n.color with
-  | Some(R r) ->
+  match n.color, n.regname with
+  | Some(R r), _ ->
       begin match Machregsaux.name_of_register r with
                 | None -> "fixed-reg"
                 | Some s -> s
       end
-  | Some(S _) -> "fixed-slot"
-  | None -> string_of_int n.ident
+  | Some(S _), _ -> "fixed-slot"
+  | None, Some r -> Printf.sprintf "x%ld" (camlint_of_positive r)
+  | None, None   -> "unknown-reg"
 *)
 
 (* The algorithm manipulates partitions of the nodes and of the moves
@@ -106,7 +108,7 @@ module DLinkNode = struct
   type t = node
   let make state =
     let rec empty =
-      { ident = 0; typ = Tint; regclass = 0;
+      { ident = 0; typ = Tint; regname = None; regclass = 0;
         adjlist = []; degree = 0; spillcost = 0.0;
         movelist = []; alias = None; color = None;
         nstate = state; nprev = empty; nnext = empty }
@@ -363,7 +365,8 @@ let checkInvariants () =
 let nodeOfReg r typenv spillcosts =
   let ty = typenv r in
   incr nextRegIdent;
-  { ident = !nextRegIdent; typ = ty; regclass = class_of_type ty;
+  { ident = !nextRegIdent; typ = ty; 
+    regname = Some r; regclass = class_of_type ty;
     spillcost = float(spillcosts r);
     adjlist = []; degree = 0; movelist = []; alias = None;
     color = None;
@@ -373,7 +376,8 @@ let nodeOfReg r typenv spillcosts =
 let nodeOfMreg mr =
   let ty = mreg_type mr in
   incr nextRegIdent;
-  { ident = !nextRegIdent; typ = ty; regclass = class_of_type ty;
+  { ident = !nextRegIdent; typ = ty; 
+    regname = None; regclass = class_of_type ty;
     spillcost = 0.0;
     adjlist = []; degree = 0; movelist = []; alias = None;
     color = Some (R mr);
@@ -521,8 +525,10 @@ let canCoalesceBriggs u v =
   try
     iterAdjacent (consider v) u;
     iterAdjacent (consider u) v;
+    (*i Printf.printf "  Briggs: OK\n"; *)
     true
   with Exit ->
+    (*i Printf.printf "  Briggs: no\n"; *)
     false
 
 (* George's conservative coalescing criterion: all high-degree neighbors
@@ -537,8 +543,11 @@ let canCoalesceGeorge u v =
       if t.degree < k || interfere t u then () else raise Exit
   in
   try
-    iterAdjacent isOK v; true
+    iterAdjacent isOK v;
+    (*i Printf.printf "  George: OK\n"; *)
+    true
   with Exit ->
+    (*i Printf.printf "  George: no\n"; *)
     false
 
 (* The combined coalescing criterion.  [u] can be precolored, but
@@ -603,7 +612,7 @@ let coalesce () =
   let m = DLinkMove.pick worklistMoves in
   let x = getAlias m.src and y = getAlias m.dst in
   let (u, v) = if y.nstate = Colored then (y, x) else (x, y) in
-  (*i Printf.printf "Attempt coalescing %s and %s\n" (name_of_node u) (name_of_node v);*)
+  (*i Printf.printf "Attempt coalescing %s and %s\n" (name_of_node u) (name_of_node v); *)
   if u == v then begin
     DLinkMove.insert m coalescedMoves;
     addWorkList u
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
new file mode 100644
index 00000000..6a745060
--- /dev/null
+++ b/backend/PrintCminor.ml
@@ -0,0 +1,285 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printer for Cminor *)
+
+open Format
+open Camlcoq
+open Datatypes
+open BinPos
+open Integers
+open AST
+open Cminor
+
+(* Precedences and associativity -- like those of C *)
+
+type associativity = LtoR | RtoL | NA
+
+let rec precedence = function
+  | Evar _ -> (16, NA)
+  | Econst _ -> (16, NA)
+  | Eunop _ -> (15, RtoL)
+  | Ebinop((Omul|Odiv|Odivu|Omod|Omodu|Omulf|Odivf), _, _) -> (13, LtoR)
+  | Ebinop((Oadd|Osub|Oaddf|Osubf), _, _) -> (12, LtoR)
+  | Ebinop((Oshl|Oshr|Oshru), _, _) -> (11, LtoR)
+  | Ebinop((Ocmp _|Ocmpu _|Ocmpf _), _, _) -> (10, LtoR)
+  | Ebinop(Oand, _, _) -> (8, LtoR)
+  | Ebinop(Oxor, _, _) -> (7, LtoR)
+  | Ebinop(Oor, _, _) -> (6, LtoR)
+  | Eload _ -> (15, RtoL)
+  | Econdition _ -> (3, RtoL)
+
+(* Naming idents.  We assume we run after Cminorgen, which encoded idents. *)
+
+let ident_name id =
+  match id with
+  | Coq_xO n -> extern_atom n
+  | Coq_xI n -> Printf.sprintf "$%ld" (camlint_of_positive n)
+  | Coq_xH -> "$0"
+
+(* Naming operators *)
+
+let name_of_unop = function
+  | Ocast8unsigned -> "int8u"
+  | Ocast8signed -> "int8s"
+  | Ocast16unsigned -> "int16u"
+  | Ocast16signed -> "int16s"
+  | Onegint -> "-"
+  | Onotbool -> "!"
+  | Onotint -> "~"
+  | Onegf -> "-f"
+  | Oabsf -> "absf"
+  | Osingleoffloat -> "float32"
+  | Ointoffloat -> "intoffloat"
+  | Ointuoffloat -> "intuoffloat"
+  | Ofloatofint -> "floatofint"
+  | Ofloatofintu -> "floatofintu"
+
+let comparison_name = function
+  | Ceq -> "=="
+  | Cne -> "!="
+  | Clt -> "<"
+  | Cle -> "<="
+  | Cgt -> ">"
+  | Cge -> ">="
+
+let name_of_binop = function
+  | Oadd -> "+"
+  | Osub -> "-"
+  | Omul -> "*"
+  | Odiv -> "/"
+  | Odivu -> "/u"
+  | Omod -> "%"
+  | Omodu -> "%u"
+  | Oand -> "&"
+  | Oor -> "|"
+  | Oxor -> "^"
+  | Oshl -> "<<"
+  | Oshr -> ">>"
+  | Oshru -> ">>u"
+  | Oaddf -> "+f"
+  | Osubf -> "-f"
+  | Omulf -> "*f"
+  | Odivf -> "/f"
+  | Ocmp c -> comparison_name c
+  | Ocmpu c -> comparison_name c ^ "u"
+  | Ocmpf c -> comparison_name c ^ "f"
+
+let name_of_chunk = function
+  | Mint8signed -> "int8signed"
+  | Mint8unsigned -> "int8unsigned"
+  | Mint16signed -> "int16signed"
+  | Mint16unsigned -> "int16unsigned"
+  | Mint32 -> "int32"
+  | Mfloat32 -> "float32"
+  | Mfloat64 -> "float64"
+
+(* Expressions *)
+
+let rec expr p (prec, e) =
+  let (prec', assoc) = precedence e in
+  let (prec1, prec2) =
+    if assoc = LtoR
+    then (prec', prec' + 1)
+    else (prec' + 1, prec') in
+  if prec' < prec 
+  then fprintf p "@[<hov 2>("
+  else fprintf p "@[<hov 2>";
+  begin match e with
+  | Evar id ->
+      fprintf p "%s" (ident_name id)
+  | Econst(Ointconst n) ->
+      fprintf p "%ld" (camlint_of_coqint n)
+  | Econst(Ofloatconst f) ->
+      fprintf p "%F" f
+  | Econst(Oaddrsymbol(id, ofs)) ->
+      let ofs = camlint_of_coqint ofs in
+      if ofs = 0l
+      then fprintf p "\"%s\"" (extern_atom id)
+      else fprintf p "(\"%s\" + %ld)" (extern_atom id) ofs
+  | Econst(Oaddrstack n) ->
+      fprintf p "&%ld" (camlint_of_coqint n)
+  | Eunop(op, a1) ->
+      fprintf p "%s %a" (name_of_unop op) expr (prec', a1)
+  | Ebinop(op, a1, a2) ->
+      fprintf p "%a@ %s %a"
+                 expr (prec1, a1) (name_of_binop op) expr (prec2, a2)
+  | Eload(chunk, a1) ->
+      fprintf p "%s[%a]" (name_of_chunk chunk) expr (0, a1)
+  | Econdition(a1, a2, a3) ->
+      fprintf p "%a@ ? %a@ : %a" expr (4, a1) expr (4, a2) expr (4, a3)
+  end;
+  if prec' < prec then fprintf p ")@]" else fprintf p "@]"
+
+let print_expr p e = expr p (0, e)
+
+let rec print_expr_list p (first, rl) =
+  match rl with
+  | [] -> ()
+  | r :: rl ->
+      if not first then fprintf p ",@ ";
+      expr p (2, r);
+      print_expr_list p (false, rl)
+
+(* Types *)
+
+let name_of_type = function
+  | Tint -> "int"
+  | Tfloat -> "float"
+
+let rec print_sig p = function
+  | {sig_args = []; sig_res = None} -> fprintf p "void"
+  | {sig_args = []; sig_res = Some ty} -> fprintf p "%s" (name_of_type ty)
+  | {sig_args = t1 :: tl; sig_res = tres} ->
+      fprintf p "%s ->@ " (name_of_type t1);
+      print_sig p {sig_args = tl; sig_res = tres}
+
+(* Statements *)
+
+let rec print_stmt p s =
+  match s with
+  | Sskip ->
+      fprintf p "/*skip*/;"
+  | Sassign(id, e2) ->
+      fprintf p "@[<hv 2>%s =@ %a;@]" (ident_name id) print_expr e2
+  | Sstore(chunk, a1, a2) ->
+      fprintf p "@[<hv 2>%s[%a] =@ %a;@]"
+              (name_of_chunk chunk) print_expr a1 print_expr a2
+  | Scall(None, sg, e1, el) ->
+      fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@])@ : @[<hov 0>%a@];@]"
+                print_expr e1
+                print_expr_list (true, el)
+                print_sig sg
+  | Scall(Some id, sg, e1, el) ->
+      fprintf p "@[<hv 2>%s =@ %a@,(@[<hov 0>%a@]);@] : @[<hov 0>%a@]"
+                (ident_name id)
+                print_expr e1
+                print_expr_list (true, el)
+                print_sig sg
+  | Stailcall(sg, e1, el) ->
+      fprintf p "@[<hv 2>tailcall %a@,(@[<hov 0>%a@])@ : @[<hov 0>%a@];@]"
+                print_expr e1
+                print_expr_list (true, el)
+                print_sig sg
+  | Sseq(Sskip, s2) ->
+      print_stmt p s2
+  | Sseq(s1, Sskip) ->
+      print_stmt p s1
+  | Sseq(s1, s2) ->
+      fprintf p "%a@ %a" print_stmt s1 print_stmt s2
+  | Sifthenelse(e, s1, Sskip) ->
+      fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
+              print_expr e
+              print_stmt s1
+  | Sifthenelse(e, Sskip, s2) ->
+      fprintf p "@[<v 2>if (! %a) {@ %a@;<0 -2>}@]"
+              expr (15, e)
+              print_stmt s2
+  | Sifthenelse(e, s1, s2) ->
+      fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
+              print_expr e
+              print_stmt s1
+              print_stmt s2
+  | Sloop(s) ->
+      fprintf p "@[<v 2>loop {@ %a@;<0 -2>}@]"
+              print_stmt s
+  | Sblock(s) ->
+      fprintf p "@[<v 3>{{ %a@;<0 -3>}}@]"
+              print_stmt s
+  | Sexit n ->
+      fprintf p "exit %d;" (camlint_of_nat n + 1)
+  | Sswitch(e, cases, dfl) ->
+      fprintf p "@[<v 2>switch (%a) {" print_expr e;
+      List.iter
+        (fun (Coq_pair(n, x)) ->
+           fprintf p "@ case %ld: exit %d;\n" 
+                     (camlint_of_coqint n) (camlint_of_nat x))
+        cases;
+      fprintf p "@ default: exit %d;\n" (camlint_of_nat dfl);
+      fprintf p "@;<0 -2>}@]"
+  | Sreturn None ->
+      fprintf p "return;"
+  | Sreturn (Some e) ->
+      fprintf p "return %a;" print_expr e
+  | Slabel(lbl, s1) ->
+      fprintf p "%s:@ %a" (extern_atom lbl) print_stmt s1
+  | Sgoto lbl ->
+      fprintf p "goto %s;" (extern_atom lbl)
+
+(* Functions *)
+
+let rec print_varlist p (vars, first) =
+  match vars with
+  | [] -> ()
+  | v1 :: vl ->
+      if not first then fprintf p ",@ ";
+      fprintf p "%s" (ident_name v1);
+      print_varlist p (vl, false)
+
+let print_function p id f =
+  fprintf p "@[<hov 4>\"%s\"(@[<hov 0>%a@])@ : @[<hov 0>%a@]@]@ "
+            (extern_atom id)
+            print_varlist (f.fn_params, true)
+            print_sig f.fn_sig;
+  fprintf p "@[<v 2>{@ ";
+  let stksz = camlint_of_z f.fn_stackspace in
+  if stksz <> 0l then
+    fprintf p "stack %ld;@ " stksz;
+  if f.fn_vars <> [] then
+    fprintf p "var @[<hov 0>%a;@]@ " print_varlist (f.fn_vars, true);
+  print_stmt p f.fn_body;
+  fprintf p "@;<0 -2>}@]@ "
+
+let print_fundef p (Coq_pair(id, fd)) =
+  match fd with
+  | External ef ->
+      () (* Todo? *)
+  | Internal f ->
+      print_function p id f
+
+let print_program p prog =
+  fprintf p "@[<v 0>";
+  List.iter (print_fundef p) prog.prog_funct;
+  fprintf p "@]@."
+
+let destination : string option ref = ref None
+
+let print_if prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+      let oc = open_out f in
+      print_program (formatter_of_out_channel oc) prog;
+      close_out oc
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
new file mode 100644
index 00000000..0f38a3f6
--- /dev/null
+++ b/backend/PrintLTLin.ml
@@ -0,0 +1,130 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printer for LTLin code *)
+
+open Format
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open Integers
+open Locations
+open Machregsaux
+open LTLin
+open PrintOp
+
+let name_of_chunk = function
+  | Mint8signed -> "int8signed"
+  | Mint8unsigned -> "int8unsigned"
+  | Mint16signed -> "int16signed"
+  | Mint16unsigned -> "int16unsigned"
+  | Mint32 -> "int32"
+  | Mfloat32 -> "float32"
+  | Mfloat64 -> "float64"
+
+let name_of_type = function
+  | Tint -> "int"
+  | Tfloat -> "float"
+
+let reg pp loc =
+  match loc with
+  | R r ->
+      begin match name_of_register r with
+      | Some s -> fprintf pp "%s" s
+      | None -> fprintf pp "<unknown reg>"
+      end
+  | S (Local(ofs, ty)) ->
+      fprintf pp "local(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
+  | S (Incoming(ofs, ty)) ->
+      fprintf pp "incoming(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
+  | S (Outgoing(ofs, ty)) ->
+      fprintf pp "outgoing(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_instruction pp i =
+  match i with
+  | Lop(op, args, res) ->
+      fprintf pp "%a = %a@ "
+         reg res (PrintOp.print_operation reg) (op, args)
+  | Lload(chunk, addr, args, dst) ->
+      fprintf pp "%a = %s[%a]@ "
+         reg dst (name_of_chunk chunk)
+         (PrintOp.print_addressing reg) (addr, args)
+  | Lstore(chunk, addr, args, src) ->
+      fprintf pp "%s[%a] = %a@ "
+         (name_of_chunk chunk)
+         (PrintOp.print_addressing reg) (addr, args)
+         reg src
+  | Lcall(sg, fn, args, res) ->
+      fprintf pp "%a = %a(%a)@ "
+        reg res ros fn regs args
+  | Ltailcall(sg, fn, args) ->
+      fprintf pp "tailcall %a(%a)@ "
+        ros fn regs args
+  | Lbuiltin(ef, args, res) ->
+      fprintf pp "%a = builtin \"%s\"(%a)@ "
+        reg res (extern_atom ef.ef_id) regs args
+  | Llabel lbl ->
+      fprintf pp "%5ld: " (camlint_of_positive lbl)
+  | Lgoto lbl ->
+      fprintf pp "goto %ld@ " (camlint_of_positive lbl)
+  | Lcond(cond, args, lbl) ->
+      fprintf pp "if (%a) goto %ld@ "
+        (PrintOp.print_condition reg) (cond, args)
+        (camlint_of_positive lbl)
+  | Ljumptable(arg, tbl) ->
+      let tbl = Array.of_list tbl in
+      fprintf pp "@[<v 2>jumptable (%a)" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i))
+      done;
+      fprintf pp "@]@ "
+  | Lreturn None ->
+      fprintf pp "return@ "
+  | Lreturn (Some arg) ->
+      fprintf pp "return %a@ " reg arg
+
+let print_function pp f =
+  fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params;
+  List.iter (print_instruction pp) f.fn_code;
+  fprintf pp "@;<0 -2>}@]@."
+
+let print_fundef pp fd =
+  match fd with
+  | Internal f -> print_function pp f
+  | External _ -> ()
+
+let destination : string option ref = ref None
+let currpp : formatter option ref = ref None
+
+let print_if fd =
+  match !destination with
+  | None -> ()
+  | Some f ->
+      let pp =
+        match !currpp with
+        | Some pp -> pp
+        | None ->
+            let oc = open_out f in
+            let pp = formatter_of_out_channel oc in
+            currpp := Some pp;
+            pp
+      in print_fundef pp fd
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 6e8c5785..62ee2c99 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -21,6 +21,8 @@ open Integers
 open RTL
 open PrintOp
 
+(* Printing of RTL code *)
+
 let name_of_chunk = function
   | Mint8signed -> "int8signed"
   | Mint8unsigned -> "int8unsigned"
@@ -55,15 +57,19 @@ let print_instruction pp (pc, i) =
       then fprintf pp "nop@ "
       else fprintf pp "goto %ld@ " s
   | Iop(op, args, res, s) ->
-      fprintf pp "%a = %a@ " reg res (print_operator reg) (op, args);
+      fprintf pp "%a = %a@ "
+         reg res (PrintOp.print_operation reg) (op, args);
       print_succ pp s (Int32.pred pc)
   | Iload(chunk, addr, args, dst, s) ->
       fprintf pp "%a = %s[%a]@ "
-         reg dst (name_of_chunk chunk) (print_addressing reg) (addr, args);
+         reg dst (name_of_chunk chunk)
+         (PrintOp.print_addressing reg) (addr, args);
       print_succ pp s (Int32.pred pc)
   | Istore(chunk, addr, args, src, s) ->
       fprintf pp "%s[%a] = %a@ "
-         (name_of_chunk chunk) (print_addressing reg) (addr, args) reg src;
+         (name_of_chunk chunk)
+         (PrintOp.print_addressing reg) (addr, args)
+         reg src;
       print_succ pp s (Int32.pred pc)
   | Icall(sg, fn, args, res, s) ->
       fprintf pp "%a = %a(%a)@ "
@@ -72,9 +78,13 @@ let print_instruction pp (pc, i) =
   | Itailcall(sg, fn, args) ->
       fprintf pp "tailcall %a(%a)@ "
         ros fn regs args
+  | Ibuiltin(ef, args, res, s) ->
+      fprintf pp "%a = builtin \"%s\"(%a)@ "
+        reg res (extern_atom ef.ef_id) regs args;
+      print_succ pp s (Int32.pred pc)
   | Icond(cond, args, s1, s2) ->
       fprintf pp "if (%a) goto %ld else goto %ld@ "
-        (print_condition reg) (cond, args)
+        (PrintOp.print_condition reg) (cond, args)
         (camlint_of_positive s1) (camlint_of_positive s2)
   | Ijumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
@@ -101,11 +111,42 @@ let print_function pp f =
   List.iter (print_instruction pp) instrs;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef fd =
-  begin match fd with
-  | Internal f -> print_function std_formatter f
+let print_fundef pp fd =
+  match fd with
+  | Internal f -> print_function pp f
   | External _ -> ()
-  end;
-  fd
 
+let print_if optdest currpp fd =
+  match !optdest with
+  | None -> ()
+  | Some f ->
+      let pp =
+        match !currpp with
+        | Some pp -> pp
+        | None ->
+            let oc = open_out f in
+            let pp = formatter_of_out_channel oc in
+            currpp := Some pp;
+            pp
+      in print_fundef pp fd
+
+let destination_rtl : string option ref = ref None
+let pp_rtl : formatter option ref = ref None
+let print_rtl = print_if destination_rtl pp_rtl
+
+let destination_tailcall : string option ref = ref None
+let pp_tailcall : formatter option ref = ref None
+let print_tailcall = print_if destination_tailcall pp_tailcall
+
+let destination_castopt : string option ref = ref None
+let pp_castopt : formatter option ref = ref None
+let print_castopt = print_if destination_castopt pp_castopt
+
+let destination_constprop : string option ref = ref None
+let pp_constprop : formatter option ref = ref None
+let print_constprop = print_if destination_constprop pp_constprop
+
+let destination_cse : string option ref = ref None
+let pp_cse : formatter option ref = ref None
+let print_cse = print_if destination_cse pp_cse
 
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index aec2c867..b728829f 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -363,6 +363,16 @@ Fixpoint alloc_regs (map: mapping) (al: exprlist)
       ret (r :: rl)
   end.
 
+(** [alloc_optreg] is used for function calls.  If a destination is
+  specified for the call, it is returned.  Otherwise, a fresh
+  register is returned. *)
+
+Definition alloc_optreg (map: mapping) (dest: option ident) : mon reg :=
+  match dest with
+  | Some id => find_var map id
+  | None => new_reg
+  end.
+
 (** * RTL generation **)
 
 (** Insertion of a register-to-register move instruction. *)
@@ -440,20 +450,6 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
       error (Errors.msg "RTLgen.transl_exprlist")
   end.
 
-(** Generation of code for variable assignments. *)
-
-Definition store_var
-       (map: mapping) (rs: reg) (id: ident) (nd: node) : mon node :=
-  do rv <- find_var map id;
-  add_move rs rv nd.
-
-Definition store_optvar
-       (map: mapping) (rs: reg) (optid: option ident) (nd: node) : mon node :=
-  match optid with
-  | None => ret nd
-  | Some id => store_var map rs id nd
-  end.
-
 (** Auxiliary for branch prediction.  When compiling an if/then/else
   statement, we have a choice between translating the ``then'' branch
   first or the ``else'' branch first.  Linearization of RTL control-flow
@@ -535,11 +531,10 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
   | Scall optid sig b cl =>
       do rf <- alloc_reg map b;
       do rargs <- alloc_regs map cl;
-      do r <- new_reg;
-      do n1 <- store_optvar map r optid nd;
-      do n2 <- add_instr (Icall sig (inl _ rf) rargs r n1);
-      do n3 <- transl_exprlist map cl rargs n2;
-         transl_expr map b rf n3
+      do r <- alloc_optreg map optid;
+      do n1 <- add_instr (Icall sig (inl _ rf) rargs r nd);
+      do n2 <- transl_exprlist map cl rargs n1;
+         transl_expr map b rf n2
   | Stailcall sig b cl =>
       do rf <- alloc_reg map b;
       do rargs <- alloc_regs map cl;
@@ -548,10 +543,9 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
          transl_expr map b rf n2
   | Sbuiltin optid ef al =>
       do rargs <- alloc_regs map al;
-      do r <- new_reg;
-      do n1 <- store_optvar map r optid nd;
-      do n2 <- add_instr (Ibuiltin ef rargs r n1);
-      transl_exprlist map al rargs n2
+      do r <- alloc_optreg map optid;
+      do n1 <- add_instr (Ibuiltin ef rargs r nd);
+         transl_exprlist map al rargs n1
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index a1bd6618..12a8e2be 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -200,18 +200,12 @@ Qed.
 (** A variant of [match_env_update_var] where a variable is optionally
   assigned to, depending on the [dst] parameter. *)
 
-Definition assign_dest (dst: option ident) (v: val) (e: Cminor.env) : Cminor.env :=
-  match dst with
-  | None => e
-  | Some id => PTree.set id v e
-  end.
-
 Lemma match_env_update_dest:
   forall map e le rs dst r v,
   map_wf map ->
   reg_map_ok map r dst ->
   match_env map e le rs ->
-  match_env map (assign_dest dst v e) le (rs#r <- v).
+  match_env map (set_optvar dst v e) le (rs#r <- v).
 Proof.
   intros. inv H0; simpl. 
   eapply match_env_update_temp; eauto. 
@@ -410,43 +404,6 @@ Proof.
   split. apply Regmap.gss. intros; apply Regmap.gso; auto.
 Qed.
 
-(** Correctness of the code generated by [store_var] and [store_optvar]. *)
-
-Lemma tr_store_var_correct:
-  forall rs cs f map r id ns nd e sp m,
-  tr_store_var f.(fn_code) map r id ns nd ->
-  map_wf map ->
-  match_env map e nil rs ->
-  exists rs',
-     star step tge (State cs f sp ns rs m)
-                E0 (State cs f sp nd rs' m)
-  /\ match_env map (PTree.set id rs#r e) nil rs'.
-Proof.
-  intros. destruct H as [rv [A B]].
-  exploit tr_move_correct; eauto. intros [rs' [EX [RES OTHER]]].
-  exists rs'; split. eexact EX.
-  apply match_env_invariant with (rs#rv <- (rs#r)).
-  apply match_env_update_var; auto.
-  intros. rewrite Regmap.gsspec. destruct (peq r0 rv).
-  subst r0; auto.
-  auto.
-Qed.
-
-Lemma tr_store_optvar_correct:
-  forall rs cs f map r optid ns nd e sp m,
-  tr_store_optvar f.(fn_code) map r optid ns nd ->
-  map_wf map ->
-  match_env map e nil rs ->
-  exists rs',
-     star step tge (State cs f sp ns rs m)
-                E0 (State cs f sp nd rs' m)
-  /\ match_env map (set_optvar optid rs#r e) nil rs'.
-Proof.
-  intros. destruct optid; simpl in *.
-  eapply tr_store_var_correct; eauto.
-  exists rs; split. subst nd. apply star_refl. auto.  
-Qed.
-
 (** Correctness of the translation of [switch] statements *)
 
 Lemma transl_switch_correct:
@@ -558,7 +515,7 @@ Definition transl_expr_prop
     (ME: match_env map e le rs),
   exists rs',
      star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m)
-  /\ match_env map (assign_dest dst v e) le rs'
+  /\ match_env map (set_optvar dst v e) le rs'
   /\ rs'#rd = v
   /\ (forall r, In r pr -> rs'#r = rs#r).
 
@@ -1042,13 +999,12 @@ Inductive tr_cont: RTL.code -> mapping ->
 with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop :=
   | match_stacks_stop:
       match_stacks Kstop nil
-  | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret n',
+  | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret,
       map_wf map ->
       tr_fun tf map f ngoto nret rret ->
       match_env map e nil rs ->
-      tr_store_optvar tf.(fn_code) map r optid n n' ->
-      ~reg_in_map map r ->
-      tr_cont tf.(fn_code) map k n' nexits ngoto nret rret cs ->
+      reg_map_ok map r optid ->
+      tr_cont tf.(fn_code) map k n nexits ngoto nret rret cs ->
       match_stacks (Kcall optid f sp e k) (Stackframe r tf sp n rs :: cs).
 
 Inductive match_states: CminorSel.state -> RTL.state -> Prop :=
@@ -1218,16 +1174,14 @@ Proof.
   inv TS. 
   exploit transl_exprlist_correct; eauto.
   intros [rs' [E [F [G J]]]].
-  exploit tr_store_optvar_correct. eauto. eauto.
-  apply match_env_update_temp. eexact F. eauto. 
-  intros [rs'' [A B]].
   econstructor; split.
-  left. eapply star_plus_trans. eexact E. eapply plus_left.
+  left. eapply plus_right. eexact E.
   eapply exec_Ibuiltin. eauto. rewrite G. 
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
-  eexact A. reflexivity. traceEq. 
-  econstructor; eauto. constructor. rewrite Regmap.gss in B. auto. 
+  traceEq. 
+  econstructor; eauto. constructor.
+  eapply match_env_update_dest; eauto.
 
   (* seq *)
   inv TS. 
@@ -1347,12 +1301,10 @@ Proof.
 
   (* return *)
   inv MS.
-  set (rs' := (rs#r <- v)).
-  assert (match_env map e nil rs'). unfold rs'; eauto with rtlg. 
-  exploit tr_store_optvar_correct. eauto. eauto. eexact H. intros [rs'' [A B]].
-  econstructor; split.
-  left; eapply plus_left. constructor. eexact A. traceEq.
-  econstructor; eauto. constructor. unfold rs' in B. rewrite Regmap.gss in B. auto.
+  econstructor; split. 
+  left; apply plus_one; constructor. 
+  econstructor; eauto. constructor. 
+  eapply match_env_update_dest; eauto.
 Qed.
 
 Lemma transl_initial_states:
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 0b18a99b..22a1e79d 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -483,6 +483,27 @@ Proof.
   intros [A|B]. auto. right; eauto with rtlg.
 Qed.
 
+Lemma alloc_optreg_valid:
+  forall dest s1 s2 map r i,
+  map_valid map s1 ->
+  alloc_optreg map dest s1 = OK r s2 i -> reg_valid r s2.
+Proof.
+  intros until r.  unfold alloc_reg.
+  case dest; eauto with rtlg.
+Qed.
+Hint Resolve alloc_optreg_valid: rtlg.
+
+Lemma alloc_optreg_fresh_or_in_map:
+  forall map dest s r s' i,
+  map_valid map s ->
+  alloc_optreg map dest s = OK r s' i ->
+  reg_in_map map r \/ reg_fresh r s.
+Proof.
+  intros until s'. unfold alloc_optreg. destruct dest; intros. 
+  left; eauto with rtlg.
+  right; eauto with rtlg.
+Qed.
+
 (** A register is an adequate target for holding the value of an
   expression if
 - either the register is associated with a Cminor let-bound variable
@@ -736,19 +757,6 @@ with tr_exprlist (c: code):
       tr_exprlist c map (r1 :: pr) al n1 nd rl ->
       tr_exprlist c map pr (Econs a1 al) ns nd (r1 :: rl).
 
-(** Auxiliary for the compilation of variable assignments. *)
-
-Definition tr_store_var (c: code) (map: mapping)
-                        (rs: reg) (id: ident) (ns nd: node): Prop :=
-  exists rv, map.(map_vars)!id = Some rv /\ tr_move c ns rs nd rv.
-
-Definition tr_store_optvar (c: code) (map: mapping)
-                 (rs: reg) (optid: option ident) (ns nd: node): Prop :=
-  match optid with
-  | None => ns = nd
-  | Some id => tr_store_var c map rs id ns nd
-  end.
-
 (** Auxiliary for the compilation of [switch] statements. *)
 
 Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) : Prop :=
@@ -804,23 +812,21 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_expr c map rl b n1 n2 rd None ->
      c!n2 = Some (Istore chunk addr rl rd nd) ->
      tr_stmt c map (Sstore chunk addr al b) ns nd nexits ngoto nret rret
-  | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 n3 rargs,
+  | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 rargs,
      tr_expr c map nil b ns n1 rf None ->
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
-     c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) ->
-     tr_store_optvar c map rd optid n3 nd ->
-     ~reg_in_map map rd ->
+     c!n2 = Some (Icall sig (inl _ rf) rargs rd nd) ->
+     reg_map_ok map rd optid ->
      tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret
   | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs,
      tr_expr c map nil b ns n1 rf None ->
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
      c!n2 = Some (Itailcall sig (inl _ rf) rargs) ->
      tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret
-  | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 n2 rargs,
+  | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 rargs,
      tr_exprlist c map nil al ns n1 rargs ->
-     c!n1 = Some (Ibuiltin ef rargs rd n2) ->
-     tr_store_optvar c map rd optid n2 nd ->
-     ~reg_in_map map rd ->
+     c!n1 = Some (Ibuiltin ef rargs rd nd) ->
+     reg_map_ok map rd optid ->
      tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret
   | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n,
      tr_stmt c map s2 n nd nexits ngoto nret rret ->
@@ -1077,25 +1083,15 @@ Proof.
   monadInv EQ1.
 Qed.
 
-Lemma tr_store_var_incr:
-  forall s1 s2, state_incr s1 s2 ->
-  forall map rs id ns nd,
-  tr_store_var s1.(st_code) map rs id ns nd ->
-  tr_store_var s2.(st_code) map rs id ns nd.
-Proof.
-  intros. destruct H0 as [rv [A B]]. 
-  econstructor; split. eauto. eapply tr_move_incr; eauto.
-Qed.
- 
-Lemma tr_store_optvar_incr:
-  forall s1 s2, state_incr s1 s2 ->
-  forall map rs optid ns nd,
-  tr_store_optvar s1.(st_code) map rs optid ns nd ->
-  tr_store_optvar s2.(st_code) map rs optid ns nd.
+Lemma alloc_optreg_map_ok:
+  forall map optid s1 r s2 i,
+  map_valid map s1 ->
+  alloc_optreg map optid s1 = OK r s2 i ->
+  reg_map_ok map r optid.
 Proof.
-  intros until nd. destruct optid; simpl. 
-  apply tr_store_var_incr; auto.
-  auto.
+  unfold alloc_optreg; intros. destruct optid.
+  constructor. unfold find_var in H0. destruct (map_vars map)!i0; monadInv H0. auto.
+  constructor. eapply new_reg_not_in_map; eauto.
 Qed.
 
 Lemma tr_switch_incr:
@@ -1116,32 +1112,10 @@ Proof.
   intros s1 s2 EXT.
   generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3.
   pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
-  pose (STV := tr_store_var_incr s1 s2 EXT).
-  pose (STOV := tr_store_optvar_incr s1 s2 EXT).
   induction 1; econstructor; eauto.
   eapply tr_switch_incr; eauto.
 Qed.
 
-Lemma store_var_charact:
-  forall map rs id nd s ns s' incr,
-  store_var map rs id nd s = OK ns s' incr ->
-  tr_store_var s'.(st_code) map rs id ns nd.
-Proof.
-  intros. monadInv H. generalize EQ. unfold find_var.
-  caseEq ((map_vars map)!id). 2: intros; discriminate. intros. monadInv EQ1.
-  exists x; split. auto. eapply add_move_charact; eauto.
-Qed.
-
-Lemma store_optvar_charact:
-  forall map rs optid nd s ns s' incr,
-  store_optvar map rs optid nd s = OK ns s' incr ->
-  tr_store_optvar s'.(st_code) map rs optid ns nd.
-Proof.
-  intros. destruct optid; simpl in H; simpl.
-  eapply store_var_charact; eauto.
-  monadInv H. auto. 
-Qed. 
-
 Lemma transl_exit_charact:
   forall nexits n s ne s' incr,
   transl_exit nexits n s = OK ne s' incr ->
@@ -1218,15 +1192,14 @@ Proof.
   (* Scall *)
   econstructor; eauto 4 with rtlg.
   eapply transl_expr_charact; eauto 3 with rtlg.
-  apply tr_exprlist_incr with s6. auto. 
+  apply tr_exprlist_incr with s5. auto. 
   eapply transl_exprlist_charact; eauto 3 with rtlg.
   eapply alloc_regs_target_ok with (s1 := s1); eauto 3 with rtlg.
   apply regs_valid_cons; eauto 3 with rtlg.
   apply regs_valid_incr with s1; eauto 3 with rtlg.
   apply regs_valid_cons; eauto 3 with rtlg.
   apply regs_valid_incr with s2; eauto 3 with rtlg.
-  apply tr_store_optvar_incr with s4; auto.
-  eapply store_optvar_charact; eauto with rtlg.
+  eapply alloc_optreg_map_ok with (s1 := s2); eauto 3 with rtlg.
   (* Stailcall *)
   assert (RV: regs_valid (x :: nil) s1).
     apply regs_valid_cons; eauto 3 with rtlg. 
@@ -1237,8 +1210,7 @@ Proof.
   (* Sbuiltin *)
   econstructor; eauto 4 with rtlg.
   eapply transl_exprlist_charact; eauto 3 with rtlg.
-  apply tr_store_optvar_incr with s2; auto.
-  eapply store_optvar_charact; eauto with rtlg.
+  eapply alloc_optreg_map_ok with (s1 := s0); eauto with rtlg.
   (* Sseq *)
   econstructor. 
   apply tr_stmt_incr with s0; auto.