SimplExpr: better translation of casts in a "for effects" context

This is useful for statements such as `(void) expr;` where we would
prefer not to explicitly compute intermediate values of type `void`
and store them in Clight temporary variables.

See issue #361 for a real-world occurrence of this phenomenon.

3 files changed, 166 insertions, 136 deletions

diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 7cdff468..1398317d 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -226,6 +226,8 @@ Definition sd_seqbool_val (tmp: ident) (ty: type) :=
   SDbase type_bool ty tmp.
 Definition sd_seqbool_set (ty: type) (sd: set_destination) :=
   let tmp :=  sd_temp sd in SDcons type_bool ty tmp sd.
+Definition sd_cast_set (ty: type) (sd: set_destination) :=
+  let tmp :=  sd_temp sd in SDcons ty ty tmp sd.
 
 Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) :=
   match a with
@@ -268,8 +270,13 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       do (sl2, a2) <- transl_expr For_val r2;
       ret (finish dst (sl1 ++ sl2) (Ebinop op a1 a2 ty))
   | Csyntax.Ecast r1 ty =>
-      do (sl1, a1) <- transl_expr For_val r1;
-      ret (finish dst sl1 (Ecast a1 ty))
+      match dst with
+      | For_val | For_set _ =>
+          do (sl1, a1) <- transl_expr For_val r1;
+          ret (finish dst sl1 (Ecast a1 ty))
+      | For_effects =>
+          transl_expr For_effects r1
+      end
   | Csyntax.Eseqand r1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       match dst with
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index ee1df409..9a3f32ec 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -145,18 +145,18 @@ Proof.
   assert (A: forall dst a, dst = For_val \/ dst = For_effects -> final dst a = nil).
     intros. destruct H; subst dst; auto.
   apply tr_expr_exprlist; intros; simpl in *; try discriminate; auto.
-  rewrite H0; auto. simpl; auto.
-  rewrite H0; auto. simpl; auto.
-  destruct H1; congruence.
-  destruct (andb_prop _ _ H6). inv H1.
+- rewrite H0; auto. simpl; auto.
+- rewrite H0; auto. simpl; auto.
+- destruct H1; congruence.
+- destruct (andb_prop _ _ H6). inv H1.
     rewrite H0; eauto. simpl; auto.
     unfold chunk_for_volatile_type in H9.
     destruct (type_is_volatile (Csyntax.typeof e1)); simpl in H8; congruence.
-  rewrite H0; auto. simpl; auto.
-  rewrite H0; auto. simpl; auto.
-  destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto.
-  rewrite H0; auto. simpl; auto.
-  destruct (andb_prop _ _ H6). rewrite H0; auto.
+- rewrite H0; auto. simpl; auto.
+- rewrite H0; auto. simpl; auto.
+- destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto.
+- rewrite H0; auto. simpl; auto.
+- destruct (andb_prop _ _ H6). rewrite H0; auto.
 Qed.
 
 Lemma tr_simple_expr_nil:
@@ -234,11 +234,11 @@ Proof.
 Opaque makeif.
   intros e m.
   apply (eval_simple_rvalue_lvalue_ind ge e m); intros until tmps; intros TR; inv TR.
-(* value *)
+- (* value *)
   auto.
-  auto.
-  exists a0; auto.
-(* rvalof *)
+- auto.
+- exists a0; auto.
+- (* rvalof *)
   inv H7; try congruence.
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
@@ -248,53 +248,55 @@ Opaque makeif.
     exploit deref_loc_translated; eauto. unfold chunk_for_volatile_type; rewrite H2. tauto.
   destruct dst; auto.
   econstructor. split. simpl; eauto. auto.
-(* addrof *)
+- (* addrof *)
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
   assert (eval_expr tge e le m (Eaddrof' a1 ty) (Vptr b ofs)) by (apply eval_Eaddrof'; auto).
   assert (typeof (Eaddrof' a1 ty) = ty) by (apply typeof_Eaddrof').
   destruct dst; auto. simpl; econstructor; eauto.  
-(* unop *)
+- (* unop *)
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
   assert (eval_expr tge e le m (Eunop op a1 ty) v). econstructor; eauto. congruence.
   destruct dst; auto. simpl; econstructor; eauto.
-(* binop *)
+- (* binop *)
   exploit H0; eauto. intros [A [B C]].
   exploit H2; eauto. intros [D [E F]].
   subst sl1 sl2; simpl.
   assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. rewrite comp_env_preserved; congruence.
   destruct dst; auto. simpl; econstructor; eauto.
-(* cast *)
+- (* cast effects *)
+  exploit H0; eauto.
+- (* cast val *)
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
   assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence.
   destruct dst; auto. simpl; econstructor; eauto.
-(* sizeof *)
+- (* sizeof *)
   rewrite <- comp_env_preserved.
   destruct dst.
   split; auto. split; auto. constructor.
   auto.
   exists (Esizeof ty1 ty). split. auto. split. auto. constructor.
-(* alignof *)
+- (* alignof *)
   rewrite <- comp_env_preserved.
   destruct dst.
   split; auto. split; auto. constructor.
   auto.
   exists (Ealignof ty1 ty). split. auto. split. auto. constructor.
-(* var local *)
+- (* var local *)
   split; auto. split; auto. apply eval_Evar_local; auto.
-(* var global *)
+- (* var global *)
   split; auto. split; auto. apply eval_Evar_global; auto.
     rewrite symbols_preserved; auto.
-(* deref *)
+- (* deref *)
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split. rewrite typeof_Ederef'; auto. apply eval_Ederef'; auto. 
-(* field struct *)
+- (* field struct *)
   rewrite <- comp_env_preserved in *.
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. rewrite B in H1. eapply eval_Efield_struct; eauto.
-(* field union *)
+- (* field union *)
   rewrite <- comp_env_preserved in *.
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. rewrite B in H1. eapply eval_Efield_union; eauto.
@@ -408,43 +410,43 @@ Ltac UNCHANGED :=
   (*generalize compat_dest_change; intro CDC.*)
   apply leftcontext_leftcontextlist_ind; intros.
 
-(* base *)
+- (* base *)
   TR. rewrite <- app_nil_end; auto. red; auto.
   intros. rewrite <- app_nil_end; auto.
-(* deref *)
+- (* deref *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* field *)
+- (* field *)
   inv H1.
   exploit H0. eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* rvalof *)
+- (* rvalof *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. red; eauto.
   intros. rewrite <- app_ass; econstructor; eauto.
   exploit typeof_context; eauto. congruence.
-(* addrof *)
+- (* addrof *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* unop *)
+- (* unop *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1; rewrite app_ass; eauto. auto.
   intros. rewrite <- app_ass. econstructor; eauto.
-(* binop left *)
+- (* binop left *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor; eauto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-(* binop right *)
+- (* binop right *)
   inv H2.
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
@@ -452,14 +454,19 @@ Ltac UNCHANGED :=
   red; auto.
   intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor; eauto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-(* cast *)
+- (* cast *)
   inv H1.
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
-  TR. subst sl1; rewrite app_ass; eauto. auto.
+  TR. eauto. auto. 
+  intros. econstructor; eauto.
++ (* generic *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. auto. 
   intros. rewrite <- app_ass. econstructor; eauto.
-(* seqand *)
+- (* seqand *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -467,15 +474,15 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-  auto. auto. auto. auto.
-  (* for set *)
+  auto. auto. auto.
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -483,9 +490,9 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-(* seqor *)
+- (* seqor *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -493,15 +500,15 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
-  auto. auto. auto. auto.
-  (* for set *)
+  auto. auto. auto.
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -509,9 +516,9 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-(* condition *)
+- (* condition *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -520,7 +527,7 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto. auto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -529,7 +536,7 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto.
-  (* for set *)
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR.
   rewrite Q. rewrite app_ass. eauto.
@@ -538,16 +545,16 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto. auto.
-(* assign left *)
+- (* assign left *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
@@ -556,9 +563,9 @@ Ltac UNCHANGED :=
   auto. auto. auto. auto. auto. auto.
   eapply typeof_context; eauto.
   auto.
-(* assign right *)
+- (* assign right *)
   inv H2.
-  (* for effects *)
++ (* for effects *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -567,7 +574,7 @@ Ltac UNCHANGED :=
   econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -577,9 +584,9 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. auto. auto. auto. auto. auto. auto.
   eapply typeof_context; eauto.
-(* assignop left *)
+- (* assignop left *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
@@ -587,7 +594,7 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   symmetry; eapply typeof_context; eauto. eauto.
   auto. auto. auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
   red; auto.
@@ -595,9 +602,9 @@ Ltac UNCHANGED :=
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto.
   eapply typeof_context; eauto.
-(* assignop right *)
+- (* assignop right *)
   inv H2.
-  (* for effects *)
++ (* for effects *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -605,7 +612,7 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. change (sl0 ++ sl2') with (nil ++ sl0 ++ sl2'). rewrite app_ass. econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. eauto. auto. auto. auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto.
@@ -613,35 +620,35 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. change (sl0 ++ sl2') with (nil ++ sl0 ++ sl2'). rewrite app_ass. econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto.
-(* postincr *)
+- (* postincr *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor; eauto.
   symmetry; eapply typeof_context; eauto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor; eauto.
   eapply typeof_context; eauto.
-(* call left *)
+- (* call left *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_exprlist_invariant; eauto. UNCHANGED.
   auto. auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor. auto. apply S; auto.
   eapply tr_exprlist_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto.
-(* call right *)
+- (* call right *)
   inv H2.
-  (* for effects *)
++ (* for effects *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
@@ -650,7 +657,7 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto. auto. auto. auto.
-  (* for val *)
++ (* for val *)
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
@@ -660,42 +667,42 @@ Ltac UNCHANGED :=
   auto. eapply tr_expr_invariant; eauto. UNCHANGED.
   apply S; auto.
   auto. auto. auto. auto.
-(* builtin *)
+- (* builtin *)
   inv H1.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
   red; auto.
   intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
   apply S; auto. auto.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto.
   red; auto.
   intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
   auto. apply S; auto. auto. auto.
-(* comma *)
+- (* comma *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto.
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto.
-(* paren *)
+- (* paren *)
   inv H1.
-  (* for val *)
++ (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q. eauto. red; auto.
   intros. econstructor; eauto.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q. eauto. auto.
   intros. econstructor; eauto.
-  (* for set *)
++ (* for set *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. rewrite Q. eauto. auto.
   intros. econstructor; eauto.
-(* cons left *)
+- (* cons left *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
   TR. subst sl1. rewrite app_ass. eauto.
@@ -703,7 +710,7 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor. apply S; auto.
   eapply tr_exprlist_invariant; eauto.  UNCHANGED.
   auto. auto. auto.
-(* cons right *)
+- (* cons right *)
   inv H2.
   assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]].
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index e7d57a1c..98425311 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -108,7 +108,12 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       tr_expr le dst (Csyntax.Ebinop op e1 e2 ty)
                    (sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty))
                    (Ebinop op a1 a2 ty) tmp
-  | tr_cast: forall le dst e1 ty sl1 a1 tmp,
+  | tr_cast_effects: forall le e1 ty sl1 a1 any tmp,
+      tr_expr le For_effects e1 sl1 a1 tmp ->
+      tr_expr le For_effects (Csyntax.Ecast e1 ty)
+                   sl1
+                   any tmp
+  | tr_cast_val: forall le dst e1 ty sl1 a1 tmp,
       tr_expr le For_val e1 sl1 a1 tmp ->
       tr_expr le dst (Csyntax.Ecast e1 ty)
                    (sl1 ++ final dst (Ecast a1 ty))
@@ -767,58 +772,69 @@ Lemma transl_meets_spec:
     exists tmps, (forall le, tr_exprlist le rl sl al tmps) /\ contained tmps g g').
 Proof.
   apply expr_exprlist_ind; simpl add_dest; intros.
-(* val *)
+- (* val *)
   simpl in H. destruct v; monadInv H; exists (@nil ident); split; auto with gensym.
 Opaque makeif.
-  intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
++ intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-(* var *)
+- (* var *)
   monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
-(* field *)
+- (* field *)
   monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* valof *)
+- (* valof *)
   monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
-(* deref *)
+- (* deref *)
   monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* addrof *)
+- (* addrof *)
   monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. econstructor; eauto.
-(* unop *)
+- (* unop *)
   monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* binop *)
+- (* binop *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
-(* cast *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
-  econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
-(* seqand *)
+- (* cast *)
+  destruct dst.
++ (* for value *)
+  monadInv H0. exploit H; eauto. intros [tmp [A B]].
+  econstructor; split; eauto. intros; apply tr_expr_add_dest.
+  rewrite (app_nil_end sl).
+  apply tr_cast_val with (dst := For_val); auto.
++ (* for effects *)
+  exploit H; eauto. intros [tmp [A B]].
+  econstructor; split; eauto. intros; eapply tr_cast_effects; eauto.
++ (* for set *)
+  monadInv H0. exploit H; eauto. intros [tmp [A B]].
+  econstructor; split; eauto. intros; apply tr_expr_add_dest.
+  apply tr_cast_val with (dst := For_set sd); auto.
+- (* seqand *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
-  (* for value *)
++ (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2); split.
@@ -826,23 +842,23 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   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.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
-(* seqor *)
+- (* seqor *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
-  (* for value *)
++ (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2); split.
@@ -850,23 +866,23 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   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 *)
++ (* for set *)
   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.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
-(* condition *)
+- (* condition *)
   monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
-  (* for value *)
++ (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   exploit H1; eauto with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
@@ -877,14 +893,14 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit H1; eauto. intros [tmp3 [E F]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2 ++ tmp3); split.
   intros; eapply tr_condition_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for test *)
++ (* for test *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
   exploit H1; eauto 10 with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
@@ -895,69 +911,69 @@ Opaque makeif.
   apply contained_cons; eauto with gensym.
   apply contained_app; eauto with gensym.
   apply contained_app; eauto with gensym.
-(* sizeof *)
+- (* sizeof *)
   monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
-(* alignof *)
+- (* alignof *)
   monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
-(* assign *)
+- (* assign *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x1 :: tmp1 ++ tmp2); split.
   intros. eapply tr_assign_val with (dst := For_val); eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exists (x1 :: tmp1 ++ tmp2); split.
   repeat rewrite app_ass. simpl.
   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 *)
+- (* assignop *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]].
   destruct dst; monadInv EQ3; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
   intros. eapply tr_assignop_val with (dst := For_val); eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists (tmp1 ++ tmp2 ++ tmp3); split.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
   repeat rewrite app_ass. simpl.
   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 *)
+- (* postincr *)
   monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x0 :: tmp1); split.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
   eauto with gensym.
-  (* for set *)
++ (* for set *)
   repeat rewrite app_ass; simpl.
   exists (x0 :: tmp1); split.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
-(* comma *)
+- (* comma *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
@@ -967,46 +983,46 @@ Opaque makeif.
   simpl. eapply incl_tran. 2: apply add_dest_incl. auto with gensym.
   destruct dst; simpl; auto with gensym.
   apply contained_app; eauto with gensym.
-(* call *)
+- (* call *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x1 :: tmp1 ++ tmp2); split.
   econstructor; eauto with gensym. congruence.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
-  (* for set *)
++ (* for set *)
   exists (x1 :: tmp1 ++ tmp2); split.
   repeat rewrite app_ass. econstructor; eauto with gensym. congruence.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
-(* builtin *)
+- (* builtin *)
   monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
-  (* for value *)
++ (* for value *)
   exists (x0 :: tmp1); split.
   econstructor; eauto with gensym. congruence.
   apply contained_cons; eauto with gensym.
-  (* for effects *)
++ (* for effects *)
   exists tmp1; split.
   econstructor; eauto with gensym.
   auto.
-  (* for set *)
++ (* for set *)
   exists (x0 :: tmp1); split.
   repeat rewrite app_ass. econstructor; eauto with gensym. congruence.
   apply contained_cons; eauto with gensym.
-(* loc *)
+- (* loc *)
   monadInv H.
-(* paren *)
+- (* paren *)
   monadInv H0.
-(* nil *)
+- (* nil *)
   monadInv H; exists (@nil ident); split; auto with gensym. constructor.
-(* cons *)
+- (* cons *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.