In compilation of Sassign, avoid systematic move from a fresh temp.

Those moves are not always coalesced during coloring.  The resulting
smaller RTL code also reduces the load on the rest of the back-end.
RTLgenspec.v: use spiffy saturateTrans tactic to speed up proof search.


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

3 files changed, 211 insertions, 105 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 942dc50..ff4f81c 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -524,9 +524,8 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
   | Sskip =>
       ret nd
   | Sassign v b =>
-      do rt <- alloc_reg map b;
-      do no <- store_var map rt v nd;
-      transl_expr map b rt no
+      do r <- find_var map v;
+      transl_expr map b r nd
   | Sstore chunk addr al b =>
       do rl <- alloc_regs map al;
       do r <- alloc_reg map b;
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index f4d1342..a15095b 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -197,6 +197,30 @@ Proof.
   symmetry. apply PMap.gso. red; intros. subst x. eauto. 
 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).
+Proof.
+  intros. inv H0; simpl. 
+  eapply match_env_update_temp; eauto. 
+  eapply match_env_update_var; eauto.
+Qed.
+Hint Resolve match_env_update_dest: rtlg.
+
+(** Matching and [let]-bound variables. *)
+
 Lemma match_env_bind_letvar:
   forall map e le rs r v,
   match_env map e le rs ->
@@ -215,6 +239,8 @@ Proof.
   constructor. auto. congruence.
 Qed.
 
+(** Matching between initial environments. *)
+
 Lemma match_env_empty:
   forall map,
   map.(map_letvars) = nil ->
@@ -521,15 +547,15 @@ Variable m: mem.
 
 Definition transl_expr_prop 
      (le: letenv) (a: expr) (v: val) : Prop :=
-  forall cs f map pr ns nd rd rs
+  forall cs f map pr ns nd rd rs dst
     (MWF: map_wf map)
-    (TE: tr_expr f.(fn_code) map pr a ns nd rd)
+    (TE: tr_expr f.(fn_code) map pr a ns nd rd dst)
     (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 e le rs'
+  /\ match_env map (assign_dest dst v e) le rs'
   /\ rs'#rd = v
-  /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
+  /\ (forall r, In r pr -> rs'#r = rs#r).
 
 (** The simulation properties for lists of expressions and for
   conditional expressions are similar. *)
@@ -544,7 +570,7 @@ Definition transl_exprlist_prop
      star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m)
   /\ match_env map e le rs'
   /\ rs'##rl = vl
-  /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
+  /\ (forall r, In r pr -> rs'#r = rs#r).
 
 Definition transl_condition_prop 
      (le: letenv) (a: condexpr) (vb: bool) : Prop :=
@@ -556,7 +582,7 @@ Definition transl_condition_prop
      star step tge (State cs f sp ns rs m) E0
                    (State cs f sp (if vb then ntrue else nfalse) rs' m)
   /\ match_env map e le rs'
-  /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
+  /\ (forall r, In r pr -> rs'#r = rs#r).
 
 (** The correctness of the translation is a huge induction over
   the Cminor evaluation derivation for the source program.  To keep
@@ -572,20 +598,22 @@ Lemma transl_expr_Evar_correct:
   transl_expr_prop le (Evar id) v.
 Proof.
   intros; red; intros. inv TE.
+  exploit match_env_find_var; eauto. intro EQ.
   exploit tr_move_correct; eauto. intros [rs' [A [B C]]]. 
   exists rs'; split. eauto.
-  destruct H2 as [D | [E F]].
+  destruct H2 as [[D E] | [D E]].
   (* optimized case *)
-  subst r.
+  subst r dst. simpl.
   assert (forall r, rs'#r = rs#r).
     intros. destruct (Reg.eq r rd). subst r. auto. auto. 
   split. eapply match_env_invariant; eauto.
-  split. rewrite B. eapply match_env_find_var; eauto.
-  auto.
+  split. congruence. auto.
   (* general case *)
-  split. eapply match_env_invariant; eauto. 
-    intros. apply C. congruence. 
-  split. rewrite B. eapply match_env_find_var; eauto. 
+  split.
+  apply match_env_invariant with (rs#rd <- v).
+  apply match_env_update_dest; auto. 
+  intros. rewrite Regmap.gsspec. destruct (peq r0 rd). congruence. auto. 
+  split. congruence. 
   intros. apply C. intuition congruence.
 Qed.
 
@@ -608,7 +636,7 @@ Proof.
   auto. 
   exact symbols_preserved. traceEq.
 (* Match-env *)
-  split. eauto with rtlg.  
+  split. eauto with rtlg.
 (* Result reg *)
   split. apply Regmap.gss.
 (* Other regs *)
@@ -650,7 +678,7 @@ Lemma transl_expr_Econdition_correct:
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd).
+  assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst).
     destruct vcond; auto.
   exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
   exists rs2.
@@ -686,11 +714,7 @@ Proof.
 (* Result *)
   split. assumption.
 (* Other regs *)
-  intros. transitivity (rs1#r0). 
-  apply OTHER2. elim H4; intro; auto.
-  unfold reg_in_map, add_letvar; simpl.
-  unfold reg_in_map in H6; tauto.
-  auto.
+  intros. transitivity (rs1#r0); auto.
 Qed.
 
 Lemma transl_expr_Eletvar_correct:
@@ -704,15 +728,21 @@ Proof.
 (* Exec *)
   split. eexact EX1.
 (* Match-env *)
-  split. apply match_env_invariant with rs. auto.
-  intros. destruct H2 as [A | [B C]]. 
-  subst r. destruct (Reg.eq r0 rd). subst r0; auto. auto.
-  apply OTHER1. intuition congruence.
+  split. 
+  destruct H2 as [[A B] | [A B]].
+  subst r dst; simpl. 
+  apply match_env_invariant with rs. auto.
+  intros. destruct (Reg.eq r rd). subst r. auto. auto.
+  apply match_env_invariant with (rs#rd <- v).
+  apply match_env_update_dest; auto. 
+  intros. rewrite Regmap.gsspec. destruct (peq r0 rd); auto. 
+  subst. rewrite RES1. eapply match_env_find_letvar; eauto. 
 (* Result *)
   split. rewrite RES1. eapply match_env_find_letvar; eauto. 
 (* Other regs *)
-  intros. destruct H2 as [A | [B C]]. 
-  subst r. destruct (Reg.eq r0 rd). subst r0; auto. auto.
+  intros. 
+  destruct H2 as [[A B] | [A B]].
+  destruct (Reg.eq r0 rd); subst; auto.
   apply OTHER1. intuition congruence.
 Qed.
 
@@ -1128,11 +1158,8 @@ Proof.
   inv TS. 
   exploit transl_expr_correct; eauto. 
   intros [rs' [A [B [C D]]]].
-  exploit tr_store_var_correct; eauto. 
-  intros [rs'' [E F]].
-  rewrite C in F.
   econstructor; split.
-  right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state.
+  right; split. eauto. Lt_state.
   econstructor; eauto. constructor.
 
   (* store *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 51fb945..5690bb2 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -132,6 +132,8 @@ Ltac monadInv H :=
 
 (** * Monotonicity properties of the state *)
 
+Hint Resolve state_incr_refl: rtlg.
+
 Lemma instr_at_incr:
   forall s1 s2 n i,
   state_incr s1 s2 -> s1.(st_code)!n = Some i -> s2.(st_code)!n = Some i.
@@ -141,7 +143,23 @@ Proof.
 Qed.
 Hint Resolve instr_at_incr: rtlg.
 
-Hint Resolve state_incr_refl state_incr_trans: rtlg.
+(** The following tactic saturates the hypotheses with
+  [state_incr] properties that follow by transitivity from
+  the known hypotheses. *)
+
+Ltac saturateTrans :=
+  match goal with
+  | H1: state_incr ?x ?y, H2: state_incr ?y ?z |- _ =>
+      match goal with
+      | H: state_incr x z |- _  =>
+         fail 1
+      | _ =>
+         let i := fresh "INCR" in
+         (generalize (state_incr_trans x y z H1 H2); intro i;
+          saturateTrans)
+      end
+  | _ => idtac
+  end.
 
 (** * Validity and freshness of registers *)
 
@@ -619,49 +637,69 @@ Inductive tr_move (c: code):
       c!ns = Some (Iop Omove (rs :: nil) rd nd) ->
       tr_move c ns rs nd rd.
 
-(** [tr_expr c map pr expr ns nd rd] holds if the graph [c],
+(** [reg_map_ok map r optid] characterizes the destination register
+  for an expression: if [optid] is [None], the destination is
+  a fresh register (not associated with any variable);
+  if [optid] is [Some id], the destination is the register
+  associated with local variable [id]. *)
+
+Inductive reg_map_ok: mapping -> reg -> option ident -> Prop :=
+  | reg_map_ok_novar: forall map rd,
+      ~reg_in_map map rd ->
+      reg_map_ok map rd None
+  | reg_map_ok_somevar: forall map rd id,
+      map.(map_vars)!id = Some rd ->
+      reg_map_ok map rd (Some id).
+
+Hint Resolve reg_map_ok_novar: rtlg.
+
+(** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c],
   between nodes [ns] and [nd], contains instructions that compute the
   value of the Cminor expression [expr] and deposit this value in
   register [rd].  [map] is a mapping from Cminor variables to the
   corresponding RTL registers.  [pr] is a list of RTL registers whose
   values must be preserved during this computation.  All registers
   mentioned in [map] must also be preserved during this computation.
-  To ensure this, we demand that the result registers of the instructions
-  appearing on the path from [ns] to [nd] are neither in [pr] nor in [map].
+  (Exception: if [optid = Some id], the register associated with
+  local variable [id] can be assigned, but only at the end of the
+  expression evaluation.)
+  To ensure this property, we demand that the result registers of the
+  instructions appearing on the path from [ns] to [nd] are not in [pr],
+  and moreover that they satisfy the [reg_map_ok] predicate.
 *)
 
 Inductive tr_expr (c: code): 
-       mapping -> list reg -> expr -> node -> node -> reg -> Prop :=
-  | tr_Evar: forall map pr id ns nd r rd,
+       mapping -> list reg -> expr -> node -> node -> reg -> option ident -> Prop :=
+  | tr_Evar: forall map pr id ns nd r rd dst,
       map.(map_vars)!id = Some r ->
-      (rd = r \/ ~reg_in_map map rd /\ ~In rd pr) ->
+      ((rd = r /\ dst = None) \/ (reg_map_ok map rd dst /\ ~In rd pr)) ->
       tr_move c ns r nd rd ->
-      tr_expr c map pr (Evar id) ns nd rd
-  | tr_Eop: forall map pr op al ns nd rd n1 rl,
+      tr_expr c map pr (Evar id) ns nd rd dst
+  | tr_Eop: forall map pr op al ns nd rd n1 rl dst,
       tr_exprlist c map pr al ns n1 rl ->
       c!n1 = Some (Iop op rl rd nd) ->
-      ~reg_in_map map rd -> ~In rd pr ->
-      tr_expr c map pr (Eop op al) ns nd rd
-  | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl,
+      reg_map_ok map rd dst -> ~In rd pr ->
+      tr_expr c map pr (Eop op al) ns nd rd dst
+  | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl dst,
       tr_exprlist c map pr al ns n1 rl ->
       c!n1 = Some (Iload chunk addr rl rd nd) ->
-      ~reg_in_map map rd -> ~In rd pr ->
-      tr_expr c map pr (Eload chunk addr al) ns nd rd
-  | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse,
+      reg_map_ok map rd dst -> ~In rd pr ->
+      tr_expr c map pr (Eload chunk addr al) ns nd rd dst
+  | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse dst,
       tr_condition c map pr b ns ntrue nfalse ->
-      tr_expr c map pr ifso ntrue nd rd ->
-      tr_expr c map pr ifnot nfalse nd rd ->
-      tr_expr c map pr (Econdition b ifso ifnot) ns nd rd
-  | tr_Elet: forall map pr b1 b2 ns nd rd n1 r,
+      tr_expr c map pr ifso ntrue nd rd dst ->
+      tr_expr c map pr ifnot nfalse nd rd dst ->
+      tr_expr c map pr (Econdition b ifso ifnot) ns nd rd dst
+  | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst,
       ~reg_in_map map r ->
-      tr_expr c map pr b1 ns n1 r ->
-      tr_expr c (add_letvar map r) pr b2 n1 nd rd ->
-      tr_expr c map pr (Elet b1 b2) ns nd rd
-  | tr_Eletvar: forall map pr n ns nd rd r,
+      tr_expr c map pr b1 ns n1 r None ->
+      tr_expr c (add_letvar map r) pr b2 n1 nd rd dst ->
+      tr_expr c map pr (Elet b1 b2) ns nd rd dst
+  | tr_Eletvar: forall map pr n ns nd rd r dst,
       List.nth_error map.(map_letvars) n = Some r ->
-      (rd = r \/ ~reg_in_map map rd /\ ~In rd pr) ->
+      ((rd = r /\ dst = None) \/ (reg_map_ok map rd dst /\ ~In rd pr)) ->
       tr_move c ns r nd rd ->
-      tr_expr c map pr (Eletvar n) ns nd rd
+      tr_expr c map pr (Eletvar n) ns nd rd dst
 
 (** [tr_condition c map pr cond ns ntrue nfalse rd] holds if the graph [c],
   starting at node [ns], contains instructions that compute the truth
@@ -694,7 +732,7 @@ with tr_exprlist (c: code):
   | tr_Enil: forall map pr n,
       tr_exprlist c map pr Enil n n nil
   | tr_Econs: forall map pr a1 al ns nd r1 rl n1,
-      tr_expr c map pr a1 ns n1 r1 ->
+      tr_expr c map pr a1 ns n1 r1 None ->
       tr_exprlist c map (r1 :: pr) al n1 nd rl ->
       tr_exprlist c map pr (Econs a1 al) ns nd (r1 :: rl).
 
@@ -757,24 +795,24 @@ Inductive tr_stmt (c: code) (map: mapping):
      stmt -> node -> node -> list node -> labelmap -> node -> option reg -> Prop :=
   | tr_Sskip: forall ns nexits ngoto nret rret,
      tr_stmt c map Sskip ns ns nexits ngoto nret rret
-  | tr_Sassign: forall id a ns nd nexits ngoto nret rret rt n,
-     tr_expr c map nil a ns n rt ->
-     tr_store_var c map rt id n nd ->
+  | tr_Sassign: forall id a ns nd nexits ngoto nret rret r,
+     map.(map_vars)!id = Some r ->
+     tr_expr c map nil a ns nd r (Some id) ->
      tr_stmt c map (Sassign id a) ns nd nexits ngoto nret rret
   | tr_Sstore: forall chunk addr al b ns nd nexits ngoto nret rret rd n1 rl n2,
      tr_exprlist c map nil al ns n1 rl ->
-     tr_expr c map rl b n1 n2 rd ->
+     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_expr c map nil b ns n1 rf ->
+     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 ->
      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 ->
+     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
@@ -799,13 +837,13 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_stmt c map (Sexit n) ns nd nexits ngoto nret rret
   | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t,
      validate_switch default cases t = true ->
-     tr_expr c map nil a ns n r ->
+     tr_expr c map nil a ns n r None ->
      tr_switch c map r nexits t n ->
      tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret
   | tr_Sreturn_none: forall nret nd nexits ngoto,
      tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None
   | tr_Sreturn_some: forall a ns nd nexits ngoto nret rret,
-     tr_expr c map nil a ns nret rret ->
+     tr_expr c map nil a ns nret rret None ->
      tr_stmt c map (Sreturn (Some a)) ns nd nexits ngoto nret (Some rret)
   | tr_Slabel: forall lbl s ns nd nexits ngoto nret rret n,
      ngoto!lbl = Some n ->
@@ -850,9 +888,9 @@ Qed.
 
 Lemma tr_expr_incr:
   forall s1 s2, state_incr s1 s2 ->
-  forall map pr a ns nd rd,
-  tr_expr s1.(st_code) map pr a ns nd rd ->
-  tr_expr s2.(st_code) map pr a ns nd rd
+  forall map pr a ns nd rd dst,
+  tr_expr s1.(st_code) map pr a ns nd rd dst ->
+  tr_expr s2.(st_code) map pr a ns nd rd dst
 with tr_condition_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map pr a ns ntrue nfalse,
@@ -894,7 +932,7 @@ Lemma transl_expr_charact:
      (OK: target_reg_ok map pr a rd)
      (VALID: regs_valid pr s)
      (VALID2: reg_valid rd s),
-   tr_expr s'.(st_code) map pr a ns nd rd
+   tr_expr s'.(st_code) map pr a ns nd rd None
 
 with transl_condexpr_charact:
   forall a map ntrue nfalse s ns s' pr INCR
@@ -913,11 +951,11 @@ with transl_exprlist_charact:
    tr_exprlist s'.(st_code) map pr al ns nd rl.
 
 Proof.
-  induction a; intros; try (monadInv TR).
+  induction a; intros; try (monadInv TR); saturateTrans.
   (* Evar *)
   generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1.
   econstructor; eauto.
-  inv OK. left; congruence. right; eauto.
+  inv OK. left; split; congruence. right; eauto with rtlg.
   eapply add_move_charact; eauto.
   (* Eop *)
   inv OK.
@@ -930,15 +968,14 @@ Proof.
   (* Econdition *)
   inv OK.
   econstructor; eauto with rtlg.
-  eapply transl_condexpr_charact; eauto with rtlg.
   apply tr_expr_incr with s1; auto. 
-  eapply transl_expr_charact; eauto with rtlg. constructor; auto.
+  eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto.
   apply tr_expr_incr with s0; auto. 
-  eapply transl_expr_charact; eauto with rtlg. constructor; auto.
+  eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto.
   (* Elet *)
   inv OK.
   econstructor. eapply new_reg_not_in_map; eauto with rtlg.  
-  eapply transl_expr_charact; eauto with rtlg.
+  eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_expr_incr with s1; auto.
   eapply transl_expr_charact. eauto. 
   apply add_letvar_valid; eauto with rtlg. 
@@ -952,12 +989,12 @@ Proof.
   generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0.
   monadInv EQ1.
   econstructor; eauto with rtlg. 
-  inv OK. left; congruence. right; eauto.
+  inv OK. left; split; congruence. right; eauto with rtlg.
   eapply add_move_charact; eauto.
   monadInv EQ1.
 
 (* Conditions *)
-  induction a; intros; try (monadInv TR).
+  induction a; intros; try (monadInv TR); saturateTrans.
 
   (* CEtrue *)
   constructor.
@@ -976,7 +1013,7 @@ Proof.
 
 (* Lists *)
 
-  induction al; intros; try (monadInv TR).
+  induction al; intros; try (monadInv TR); saturateTrans.
 
   (* Enil *)
   destruct rl; inv TR. constructor.
@@ -991,6 +1028,49 @@ Proof.
   red; intros; apply VALID2; auto with coqlib.
 Qed.
 
+(** A variant of [transl_expr_charact], for use when the destination
+  register is the one associated with a variable. *)
+
+Lemma transl_expr_assign_charact:
+  forall id a map rd nd s ns s' INCR
+     (TR: transl_expr map a rd nd s = OK ns s' INCR)
+     (WF: map_valid map s)
+     (OK: reg_map_ok map rd (Some id)),
+   tr_expr s'.(st_code) map nil a ns nd rd (Some id).
+Proof.
+  induction a; intros; monadInv TR; saturateTrans.
+  (* Evar *)
+  generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1.
+  econstructor; eauto.
+  eapply add_move_charact; eauto.
+  (* Eop *)
+  econstructor; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg.
+  (* Eload *)
+  econstructor; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg. 
+  (* Econdition *)
+  econstructor; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
+  apply tr_expr_incr with s1; auto. 
+  eapply IHa1; eauto 2 with rtlg.
+  apply tr_expr_incr with s0; auto. 
+  eapply IHa2; eauto 2 with rtlg.
+  (* Elet *)
+  econstructor. eapply new_reg_not_in_map; eauto with rtlg.  
+  eapply transl_expr_charact; eauto 3 with rtlg.
+  apply tr_expr_incr with s1; auto.
+  eapply IHa2; eauto.
+  apply add_letvar_valid; eauto with rtlg.
+  inv OK. constructor. auto.
+  (* Eletvar *)
+  generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0.
+  monadInv EQ1.
+  econstructor; eauto with rtlg. 
+  eapply add_move_charact; eauto.
+  monadInv EQ1.
+Qed.
+
 Lemma tr_store_var_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map rs id ns nd,
@@ -1084,17 +1164,18 @@ Lemma transl_switch_charact:
   transl_switch r nexits t s = OK ns s' incr ->
   tr_switch s'.(st_code) map r nexits t ns.
 Proof.
-  induction t; simpl; intros.
+  induction t; simpl; intros; saturateTrans.
+
   exploit transl_exit_charact; eauto. intros [A B].
   econstructor; eauto.
 
   monadInv H1.
   exploit transl_exit_charact; eauto. intros [A B]. subst s1.
-  econstructor; eauto with rtlg. 
+  econstructor; eauto 2 with rtlg. 
   apply tr_switch_incr with s0; eauto with rtlg.
 
   monadInv H1.
-  econstructor; eauto with rtlg. 
+  econstructor; eauto 2 with rtlg. 
   apply tr_switch_incr with s1; eauto with rtlg.
   apply tr_switch_incr with s0; eauto with rtlg.
 
@@ -1115,39 +1196,38 @@ Lemma transl_stmt_charact:
     (OK: return_reg_ok s map rret),
   tr_stmt s'.(st_code) map stmt ns nd nexits ngoto nret rret.
 Proof.
-  induction stmt; intros; simpl in TR; try (monadInv TR).
+  induction stmt; intros; simpl in TR; try (monadInv TR); saturateTrans.
   (* Sskip *)
   constructor.
   (* Sassign *)
-  econstructor. eapply transl_expr_charact; eauto with rtlg.
-  apply tr_store_var_incr with s1; auto with rtlg.
-  eapply store_var_charact; eauto.
+  revert EQ. unfold find_var. case_eq (map_vars map)!i; intros; monadInv EQ.
+  econstructor. eauto. 
+  eapply transl_expr_assign_charact; eauto with rtlg.
+  constructor. auto.
   (* Sstore *)
   econstructor; eauto with rtlg.
-  eapply transl_exprlist_charact; eauto with rtlg.
-  apply tr_expr_incr with s3; eauto with rtlg.
-  eapply transl_expr_charact; eauto with rtlg. 
+  eapply transl_exprlist_charact; eauto 3 with rtlg.
+  apply tr_expr_incr with s3; auto.
+  eapply transl_expr_charact; eauto 4 with rtlg.
   (* Scall *)
-  assert (state_incr s0 s2) by eauto with rtlg.
-  assert (state_incr s2 s4) by eauto with rtlg.
-  assert (state_incr s4 s6) by eauto with rtlg.
-  econstructor; eauto with rtlg.
-  eapply transl_expr_charact; eauto with rtlg.
+  econstructor; eauto 4 with rtlg.
+  eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_exprlist_incr with s6. auto. 
-  eapply transl_exprlist_charact; eauto with rtlg.
-  eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg.
-  apply regs_valid_cons; eauto with rtlg.
-  apply regs_valid_incr with s1; eauto with rtlg.
-  apply regs_valid_cons; eauto with rtlg.
-  apply tr_store_optvar_incr with s4; eauto with rtlg.
+  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.
   (* Stailcall *)
   assert (RV: regs_valid (x :: nil) s1).
-    apply regs_valid_cons; eauto with rtlg. 
-  econstructor; eauto with rtlg.
-  eapply transl_expr_charact; eauto with rtlg.
+    apply regs_valid_cons; eauto 3 with rtlg. 
+  econstructor; eauto 3 with rtlg.
+  eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_exprlist_incr with s4; auto.
-  eapply transl_exprlist_charact; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto 4 with rtlg.
   (* Sseq *)
   econstructor. 
   apply tr_stmt_incr with s0; auto.