Issue with simplification of nested ?: expressions of different types.

(Ill-typed Clight/Cminor/RTL code was generated due to incorrect reuse
of destination temporary.)


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

3 files changed, 129 insertions, 85 deletions

diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 98dad93..8e6bc9f 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -187,26 +187,37 @@ Definition make_assign (l r: expr) : statement :=
   assignment.  In this case, [a] is meaningless.
 *)
 
+Inductive set_destination : Type :=
+  | SDbase (ty: type) (tmp: ident)
+  | SDcons (ty: type) (tmp: ident) (sd: set_destination).
+
 Inductive destination : Type := 
   | For_val
   | For_effects
-  | For_set (tyl: list type) (tmp: ident).
+  | For_set (sd: set_destination).
 
 Definition dummy_expr := Econst_int Int.zero type_int32s.
 
-Fixpoint do_set (tmp: ident) (tyl: list type) (a: expr) : list statement :=
-  match tyl with
-  | nil => nil
-  | ty1 :: tys => Sset tmp (Ecast a ty1) :: do_set tmp tys (Etempvar tmp ty1)
+Fixpoint do_set (sd: set_destination) (a: expr) : list statement :=
+  match sd with
+  | SDbase ty tmp => Sset tmp (Ecast a ty) :: nil
+  | SDcons ty tmp sd' => Sset tmp (Ecast a ty) :: do_set sd' (Etempvar tmp ty)
   end.
 
 Definition finish (dst: destination) (sl: list statement) (a: expr) :=
   match dst with
   | For_val => (sl, a)
   | For_effects => (sl, a)
-  | For_set tyl tmp => (sl ++ do_set tmp tyl a, a)
+  | For_set sd => (sl ++ do_set sd a, a)
   end.
 
+Definition sd_temp (sd: set_destination) :=
+  match sd with SDbase _ tmp => tmp | SDcons _ tmp _ => tmp end.
+Definition sd_seqbool_val (tmp: ident) (ty: type) :=
+  SDcons type_bool tmp (SDbase ty tmp).
+Definition sd_seqbool_set (ty: type) (sd: set_destination) :=
+  let tmp :=  sd_temp sd in SDcons type_bool tmp (SDcons ty tmp sd).
+
 Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) :=
   match a with
   | Csyntax.Eloc b ofs ty =>
@@ -253,17 +264,17 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       match dst with
       | For_val =>
           do t <- gensym ty;
-          do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: nil) t) r2;
+          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2;
           ret (sl1 ++ 
                makeif a1 (makeseq sl2) (Sset t (Econst_int Int.zero ty)) :: nil,
                Etempvar t ty)
       | For_effects =>
           do (sl2, a2) <- transl_expr For_effects r2;
           ret (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil, dummy_expr)
-      | For_set tyl t =>
-          do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: tyl) t) r2;
+      | For_set sd =>
+          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2;
           ret (sl1 ++ 
-               makeif a1 (makeseq sl2) (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil,
+               makeif a1 (makeseq sl2) (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil,
                dummy_expr)
       end
   | Csyntax.Eseqor r1 r2 ty =>
@@ -271,17 +282,17 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       match dst with
       | For_val =>
           do t <- gensym ty;
-          do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: nil) t) r2;
+          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2;
           ret (sl1 ++ 
                makeif a1 (Sset t (Econst_int Int.one ty)) (makeseq sl2) :: nil,
                Etempvar t ty)
       | For_effects =>
           do (sl2, a2) <- transl_expr For_effects r2;
           ret (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil, dummy_expr)
-      | For_set tyl t =>
-          do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: tyl) t) r2;
+      | For_set sd =>
+          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2;
           ret (sl1 ++ 
-               makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty))) (makeseq sl2) :: nil,
+               makeif a1 (makeseq (do_set sd (Econst_int Int.one ty))) (makeseq sl2) :: nil,
                dummy_expr)
       end
   | Csyntax.Econdition r1 r2 r3 ty =>
@@ -289,8 +300,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       match dst with
       | For_val =>
           do t <- gensym ty;
-          do (sl2, a2) <- transl_expr (For_set (ty::nil) t) r2;
-          do (sl3, a3) <- transl_expr (For_set (ty::nil) t) r3;
+          do (sl2, a2) <- transl_expr (For_set (SDbase ty t)) r2;
+          do (sl3, a3) <- transl_expr (For_set (SDbase ty t)) r3;
           ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
                Etempvar t ty)
       | For_effects =>
@@ -298,9 +309,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
           do (sl3, a3) <- transl_expr For_effects r3;
           ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
                dummy_expr)
-      | For_set tyl t =>
-          do (sl2, a2) <- transl_expr (For_set (ty::tyl) t) r2;
-          do (sl3, a3) <- transl_expr (For_set (ty::tyl) t) r3;
+      | For_set sd =>
+          do t <- gensym ty;
+          do (sl2, a2) <- transl_expr (For_set (SDcons ty t sd)) r2;
+          do (sl3, a3) <- transl_expr (For_set (SDcons ty t sd)) r3;
           ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
                dummy_expr)
       end
@@ -310,7 +322,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       let ty1 := Csyntax.typeof l1 in
       let ty2 := Csyntax.typeof r2 in
       match dst with
-      | For_val | For_set _ _ =>
+      | For_val | For_set _ =>
           do t <- gensym ty2;
           ret (finish dst 
                  (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil)
@@ -325,7 +337,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       do (sl2, a2) <- transl_expr For_val r2;
       do (sl3, a3) <- transl_valof ty1 a1;
       match dst with
-      | For_val | For_set _ _ =>
+      | For_val | For_set _ =>
           do t <- gensym tyres;
           ret (finish dst
                  (sl1 ++ sl2 ++ sl3 ++
@@ -340,7 +352,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       let ty1 := Csyntax.typeof l1 in
       do (sl1, a1) <- transl_expr For_val l1;
       match dst with
-      | For_val | For_set _ _ =>
+      | For_val | For_set _ =>
           do t <- gensym ty1;
           ret (finish dst
                  (sl1 ++ make_set t a1 ::
@@ -359,7 +371,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       do (sl1, a1) <- transl_expr For_val r1;
       do (sl2, al2) <- transl_exprlist rl2;
       match dst with
-      | For_val | For_set _ _ =>
+      | For_val | For_set _ =>
           do t <- gensym ty;
           ret (finish dst (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: nil)
                           (Etempvar t ty))
@@ -369,7 +381,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
   | Csyntax.Ebuiltin ef tyargs rl ty =>
       do (sl, al) <- transl_exprlist rl;
       match dst with
-      | For_val | For_set _ _ =>
+      | For_val | For_set _ =>
           do t <- gensym ty;
           ret (finish dst (sl ++ Sbuiltin (Some t) ef tyargs al :: nil)
                           (Etempvar t ty))
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 150ed76..a2b8e61 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -192,8 +192,8 @@ Lemma tr_simple:
   match dst with
   | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v
   | For_effects => sl = nil
-  | For_set tyl t =>
-      exists b, sl = do_set t tyl b
+  | For_set sd =>
+      exists b, sl = do_set sd b
              /\ Csyntax.typeof r = typeof b
              /\ eval_expr tge e le m b v
   end)
@@ -277,8 +277,8 @@ Lemma tr_simple_rvalue:
   match dst with
   | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v
   | For_effects => sl = nil
-  | For_set tyl t =>
-      exists b, sl = do_set t tyl b
+  | For_set sd =>
+      exists b, sl = do_set sd b
              /\ Csyntax.typeof r = typeof b
              /\ eval_expr tge e le m b v
   end.
@@ -1063,9 +1063,9 @@ Proof.
 Qed.
 
 Lemma nolabel_do_set:
-  forall tmp tyl a, nolabel_list (do_set tmp tyl a).
+  forall sd a, nolabel_list (do_set sd a).
 Proof.
-  induction tyl; intros; simpl; split; auto; red; auto.
+  induction sd; intros; simpl; split; auto; red; auto.
 Qed.
 
 Lemma nolabel_final:
@@ -1418,8 +1418,9 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; eauto.
-  apply S. apply tr_paren_set with (a1 := dummy_expr); auto. econstructor; eauto. 
-  apply tr_expr_monotone with tmp2; eauto. auto. auto.
+  apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto.
+  apply tr_paren_set with (a1 := a2) (t := sd_temp sd).
+  apply tr_expr_monotone with tmp2; eauto. auto. auto. auto.
 (* seqand false *)
   exploit tr_top_leftcontext; eauto. clear H9. 
   intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [R S]]]]]]]].
@@ -1527,7 +1528,8 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; eauto.
-  apply S. apply tr_paren_set with (a1 := dummy_expr); auto. econstructor; eauto. 
+  apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto.
+  apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto.
   apply tr_expr_monotone with tmp2; eauto. auto. auto.
 (* condition *)
   exploit tr_top_leftcontext; eauto. clear H9. 
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 1e7a84c..d063c4e 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -46,7 +46,7 @@ Definition final (dst: destination) (a: expr) : list statement :=
   match dst with
   | For_val => nil
   | For_effects => nil
-  | For_set tyl t => do_set t tyl a
+  | For_set sd => do_set sd a
   end.
 
 Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Prop :=
@@ -78,13 +78,13 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
          eval_expr tge e le' m a v) ->
       tr_expr le For_val (Csyntax.Eval v ty) 
                            nil a tmp
-  | tr_val_set: forall le tyl t v ty a any tmp,
+  | tr_val_set: forall le sd v ty a any tmp,
       typeof a = ty ->
       (forall tge e le' m,
          (forall id, In id tmp -> le'!id = le!id) ->
          eval_expr tge e le' m a v) ->
-      tr_expr le (For_set tyl t) (Csyntax.Eval v ty) 
-                   (do_set t tyl a) any tmp
+      tr_expr le (For_set sd) (Csyntax.Eval v ty) 
+                   (do_set sd a) any tmp
   | tr_sizeof: forall le dst ty' ty tmp,
       tr_expr le dst (Csyntax.Esizeof ty' ty)
                    (final dst (Esizeof ty' ty))
@@ -124,7 +124,7 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
                    (Ecast a1 ty) tmp
   | tr_seqand_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
-      tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (sd_seqbool_val t ty)) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
       tr_expr le For_val (Csyntax.Eseqand e1 e2 ty)
@@ -139,18 +139,18 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       tr_expr le For_effects (Csyntax.Eseqand e1 e2 ty)
                     (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil)
                     any tmp
-  | tr_seqand_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
+  | tr_seqand_set: forall le sd e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
-      tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (sd_seqbool_set ty sd)) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
-      incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
-      tr_expr le (For_set tyl t) (Csyntax.Eseqand e1 e2 ty)
+      incl tmp1 tmp -> incl tmp2 tmp -> In (sd_temp sd) tmp ->
+      tr_expr le (For_set sd) (Csyntax.Eseqand e1 e2 ty)
                     (sl1 ++ makeif a1 (makeseq sl2)
-                                      (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil)
+                                      (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil)
                     any tmp
   | tr_seqor_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
-      tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (sd_seqbool_val t ty)) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
       tr_expr le For_val (Csyntax.Eseqor e1 e2 ty)
@@ -165,19 +165,19 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       tr_expr le For_effects (Csyntax.Eseqor e1 e2 ty)
                     (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil)
                     any tmp
-  | tr_seqor_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
+  | tr_seqor_set: forall le sd e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
-      tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (sd_seqbool_set ty sd)) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
-      incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
-      tr_expr le (For_set tyl t) (Csyntax.Eseqor e1 e2 ty)
-                    (sl1 ++ makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty)))
+      incl tmp1 tmp -> incl tmp2 tmp -> In (sd_temp sd) tmp ->
+      tr_expr le (For_set sd) (Csyntax.Eseqor e1 e2 ty)
+                    (sl1 ++ makeif a1 (makeseq (do_set sd (Econst_int Int.one ty)))
                                       (makeseq sl2) :: nil)
                     any tmp
   | tr_condition_val: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
-      tr_expr le (For_set (ty::nil) t) e2 sl2 a2 tmp2 ->
-      tr_expr le (For_set (ty::nil) t) e3 sl3 a3 tmp3 ->
+      tr_expr le (For_set (SDbase ty t)) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (SDbase ty t)) e3 sl3 a3 tmp3 ->
       list_disjoint tmp1 tmp2 ->
       list_disjoint tmp1 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp ->  incl tmp3 tmp -> In t tmp ->
@@ -194,14 +194,14 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       tr_expr le For_effects (Csyntax.Econdition e1 e2 e3 ty)
                        (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
                        any tmp
-  | tr_condition_set: forall le tyl t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
+  | tr_condition_set: forall le sd t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
-      tr_expr le (For_set (ty::tyl) t) e2 sl2 a2 tmp2 ->
-      tr_expr le (For_set (ty::tyl) t) e3 sl3 a3 tmp3 ->
+      tr_expr le (For_set (SDcons ty t sd)) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (SDcons ty t sd)) e3 sl3 a3 tmp3 ->
       list_disjoint tmp1 tmp2 ->
       list_disjoint tmp1 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp ->
-      tr_expr le (For_set tyl t) (Csyntax.Econdition e1 e2 e3 ty)
+      tr_expr le (For_set sd) (Csyntax.Econdition e1 e2 e3 ty)
                        (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
                        any tmp
   | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
@@ -305,7 +305,7 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
                    (sl ++ Sbuiltin (Some t) ef tyargs al :: final dst (Etempvar t ty))
                    (Etempvar t ty) tmp
   | tr_paren_val: forall le e1 ty sl1 a1 t tmp,
-      tr_expr le (For_set (ty :: nil) t) e1 sl1 a1 tmp ->
+      tr_expr le (For_set (SDbase ty t)) e1 sl1 a1 tmp ->
       In t tmp -> 
       tr_expr le For_val (Csyntax.Eparen e1 ty)
                        sl1
@@ -313,10 +313,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
   | tr_paren_effects: forall le e1 ty sl1 a1 tmp any,
       tr_expr le For_effects e1 sl1 a1 tmp ->
       tr_expr le For_effects (Csyntax.Eparen e1 ty) sl1 any tmp
-  | tr_paren_set: forall le tyl t e1 ty sl1 a1 tmp any,
-      tr_expr le (For_set (ty::tyl) t) e1 sl1 a1 tmp ->
+  | tr_paren_set: forall le t sd e1 ty sl1 a1 tmp any,
+      tr_expr le (For_set (SDcons ty t sd)) e1 sl1 a1 tmp ->
       In t tmp ->
-      tr_expr le (For_set tyl t) (Csyntax.Eparen e1 ty) sl1 any tmp
+      tr_expr le (For_set sd) (Csyntax.Eparen e1 ty) sl1 any tmp
 
 with tr_exprlist: temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop :=
   | tr_nil: forall le tmp,
@@ -646,7 +646,7 @@ Qed.
 
 Definition dest_below (dst: destination) (g: generator) : Prop :=
   match dst with
-  | For_set tyl tmp => Plt tmp g.(gen_next)
+  | For_set sd => Plt (sd_temp sd) g.(gen_next)
   | _ => True
   end.
 
@@ -656,20 +656,37 @@ Proof. intros; simpl; auto. Qed.
 Remark dest_for_effect_below: forall g, dest_below For_effects g.
 Proof. intros; simpl; auto. Qed.
 
-Lemma dest_below_notin:
-  forall tyl tmp g1 g2 l,
-  dest_below (For_set tyl tmp) g1 -> contained l g1 g2 -> ~In tmp l.
+Lemma dest_for_set_seqbool_val:
+  forall tmp ty g1 g2,
+  within tmp g1 g2 -> dest_below (For_set (sd_seqbool_val tmp ty)) g2.
+Proof.
+  intros. destruct H. simpl. auto.
+Qed.
+
+Lemma dest_for_set_seqbool_set:
+  forall sd ty g, dest_below (For_set sd) g -> dest_below (For_set (sd_seqbool_set ty sd)) g.
+Proof.
+  intros. assumption. 
+Qed.
+
+Lemma dest_for_set_condition_val:
+  forall tmp ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase ty tmp)) g2.
 Proof.
-  simpl; intros. red in H0. red; intros. destruct (H0 _ H1). 
-  elim (Plt_strict tmp). apply Plt_Ple_trans with (gen_next g1); auto.
+  intros. destruct H. simpl. auto.
 Qed.
 
-Lemma within_dest_below:
-  forall tyl tmp g1 g2,
-  within tmp g1 g2 -> dest_below (For_set tyl tmp) g2.
+Lemma dest_for_set_condition_set:
+  forall sd tmp ty g1 g2, dest_below (For_set sd) g2 -> within tmp g1 g2 -> dest_below (For_set (SDcons ty tmp sd)) g2.
 Proof.
-  intros; simpl. destruct H. tauto.
-Qed. 
+  intros. destruct H0. simpl. auto.
+Qed.
+
+Lemma sd_temp_notin:
+  forall sd g1 g2 l, dest_below (For_set sd) g1 -> contained l g1 g2 -> ~In (sd_temp sd) l.
+Proof.
+  intros. simpl in H. red; intros. exploit H0; eauto. intros [A B]. 
+  elim (Plt_strict (sd_temp sd)). apply Plt_Ple_trans with (gen_next g1); auto.
+Qed.
 
 Lemma dest_below_le:
   forall dst g1 g2,
@@ -680,9 +697,12 @@ Qed.
 
 Hint Resolve gensym_within within_widen contained_widen
              contained_cons contained_app contained_disjoint
-             contained_notin contained_nil dest_below_notin
+             contained_notin contained_nil
+             dest_for_set_seqbool_val dest_for_set_seqbool_set
+             dest_for_set_condition_val dest_for_set_condition_set
+             sd_temp_notin dest_below_le
              incl_refl incl_tl incl_app incl_appl incl_appr incl_same_head
-             in_eq in_cons within_dest_below dest_below_le
+             in_eq in_cons 
              Ple_trans Ple_refl: gensym.
 
 Hint Resolve dest_for_val_below dest_for_effect_below.
@@ -711,16 +731,24 @@ Ltac UseFinish :=
       repeat rewrite app_ass
   end.
 
+(*
+Fixpoint add_set_dest (sd: set_destination) (tmps: list ident) :=
+  match sd with
+  | SDbase ty tmp => tmp :: tmps
+  | SDcons ty tmp sd' => tmp :: add_set_dest sd' tmps
+  end.
+*)
+
 Definition add_dest (dst: destination) (tmps: list ident) :=
   match dst with
-  | For_set tyl t => t :: tmps
+  | For_set sd => sd_temp sd :: tmps
   | _ => tmps
   end.
 
 Lemma add_dest_incl:
   forall dst tmps, incl tmps (add_dest dst tmps).
 Proof.
-  intros. destruct dst; simpl; auto with coqlib.
+  intros. destruct dst; simpl; eauto with coqlib.
 Qed.
 
 Lemma tr_expr_add_dest:
@@ -805,7 +833,7 @@ Opaque makeif.
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
-  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+  exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_val; eauto with gensym.
@@ -819,7 +847,7 @@ Opaque makeif.
   intros; eapply tr_seqand_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
   (* for set *)
-  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+  exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_set; eauto with gensym.
@@ -834,16 +862,16 @@ Opaque makeif.
   exists (x0 :: tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_val; eauto with gensym.
   apply list_disjoint_cons_r; eauto with gensym.
-  apply contained_cons. eauto with gensym. 
+  apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
   (* for effects *)
-  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+  exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
   (* for set *)
-  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+  exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_set; eauto with gensym.
@@ -853,7 +881,7 @@ Opaque makeif.
   monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
-  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+  exploit H0; eauto with gensym. intros [tmp2 [C D]].
   exploit H1; eauto with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split. 
@@ -871,13 +899,15 @@ Opaque makeif.
   intros; eapply tr_condition_effects; eauto with gensym. 
   apply contained_app; eauto with gensym.
   (* for test *)
-  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
-  exploit H1; eauto with gensym. intros [tmp3 [E F]].
+  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H1; eauto 10 with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
-  exists (tmp1 ++ tmp2 ++ tmp3); split.
+  exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split.
   intros; eapply tr_condition_set; eauto with gensym.
   apply list_disjoint_cons_r; eauto with gensym.
   apply list_disjoint_cons_r; eauto with gensym.
+  apply contained_cons; eauto with gensym. 
+  apply contained_app; eauto with gensym.
   apply contained_app; eauto with gensym.
 (* sizeof *)
   monadInv H. UseFinish.
@@ -901,7 +931,7 @@ Opaque makeif.
   (* for set *)
   exists (x1 :: tmp1 ++ tmp2); split.
   repeat rewrite app_ass. simpl. 
-  intros. eapply tr_assign_val with (dst := For_set tyl tmp); eauto with gensym.
+  intros. eapply tr_assign_val with (dst := For_set sd); eauto with gensym.
   apply contained_cons. eauto with gensym. 
   apply contained_app; eauto with gensym.
 (* assignop *)
@@ -921,7 +951,7 @@ Opaque makeif.
   (* for set *)
   exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
   repeat rewrite app_ass. simpl.
-  intros. eapply tr_assignop_val with (dst := For_set tyl tmp); eauto with gensym.
+  intros. eapply tr_assignop_val with (dst := For_set sd); eauto with gensym.
   apply contained_cons. eauto with gensym. 
   apply contained_app; eauto with gensym.
 (* postincr *)