Revised translation of '&&' and '||' to Clight.

The previous translation (in SimplExpr) produced references to the
same temporary variable with two different types (bool and int),
which is not nice if we want to typecheck the generated Clight.
The new translation avoids this and also gets rid of the double
cast to bool then to int.  The trick is to change Eparen
(in CompCert C expressions) to take two types: the type to which the
argument must be converted, and the type with which the resulting
expression is seen.

10 files changed, 108 insertions, 123 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 0e070934..c33068d9 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -797,7 +797,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do b <- bool_val v1 ty1;
-          if b then topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0)
+          if b then topred (Rred (Eparen r2 type_bool ty) m E0)
                else topred (Rred (Eval (Vint Int.zero) ty) m E0)
       | None =>
           incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m)
@@ -807,7 +807,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       | Some(v1, ty1) =>
           do b <- bool_val v1 ty1;
           if b then topred (Rred (Eval (Vint Int.one) ty) m E0)
-               else topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0)
+               else topred (Rred (Eparen r2 type_bool ty) m E0)
       | None =>
           incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m)
       end
@@ -815,7 +815,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do b <- bool_val v1 ty1;
-          topred (Rred (Eparen (if b then r2 else r3) ty) m E0)
+          topred (Rred (Eparen (if b then r2 else r3) ty ty) m E0)
       | None =>
           incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
       end
@@ -869,13 +869,13 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       | None =>
           incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m)
       end
-  | RV, Eparen r1 ty =>
+  | RV, Eparen r1 tycast ty =>
       match is_val r1 with
       | Some (v1, ty1) =>
-          do v <- sem_cast v1 ty1 ty;
+          do v <- sem_cast v1 ty1 tycast;
           topred (Rred (Eval v ty) m E0)
       | None =>
-          incontext (fun x => Eparen x ty) (step_expr RV r1 m)
+          incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m)
       end
   | RV, Ecall r1 rargs ty =>
       match is_val r1, is_val_list rargs with
@@ -1010,8 +1010,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       ty = ty1 /\ deref_loc ge ty m b ofs t v1 /\ possible_trace w t w'
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
-  | Eparen (Eval v1 ty1) ty =>
-      exists v, sem_cast v1 ty1 ty = Some v
+  | Eparen (Eval v1 ty1) tycast ty =>
+      exists v, sem_cast v1 ty1 tycast = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs tyres cconv fd vl,
@@ -1543,7 +1543,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* paren *)
   destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  destruct (sem_cast v ty' ty) as [v'|] eqn:?...
+  destruct (sem_cast v ty' tycast) as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. 
   (* depth *)
   eapply incontext_ok; eauto.
@@ -1791,7 +1791,7 @@ Proof.
   eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto.
   destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* paren *)
-  eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto.
+  eapply reducts_incl_trans with (C' := fun x => Eparen x tycast ty); eauto.
   destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 
   induction 1; simpl; intros.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 55c37c99..06cea006 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -248,7 +248,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
   | red_seqand_true: forall v1 ty1 r2 ty m,
       bool_val v1 ty1 = Some true ->
       rred (Eseqand (Eval v1 ty1) r2 ty) m
-        E0 (Eparen (Eparen r2 type_bool) ty) m
+        E0 (Eparen r2 type_bool ty) m
   | red_seqand_false: forall v1 ty1 r2 ty m,
       bool_val v1 ty1 = Some false ->
       rred (Eseqand (Eval v1 ty1) r2 ty) m
@@ -260,11 +260,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
   | red_seqor_false: forall v1 ty1 r2 ty m,
       bool_val v1 ty1 = Some false ->
       rred (Eseqor (Eval v1 ty1) r2 ty) m
-        E0 (Eparen (Eparen r2 type_bool) ty) m
+        E0 (Eparen r2 type_bool ty) m
   | red_condition: forall v1 ty1 r1 r2 ty b m,
       bool_val v1 ty1 = Some b ->
       rred (Econdition (Eval v1 ty1) r1 r2 ty) m
-        E0 (Eparen (if b then r1 else r2) ty) m
+        E0 (Eparen (if b then r1 else r2) ty ty) m
   | red_sizeof: forall ty1 ty m,
       rred (Esizeof ty1 ty) m
         E0 (Eval (Vint (Int.repr (sizeof ty1))) ty) m
@@ -295,9 +295,9 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
       typeof r2 = ty ->
       rred (Ecomma (Eval v ty1) r2 ty) m
         E0 r2 m
-  | red_paren: forall v1 ty1 ty m v,
-      sem_cast v1 ty1 ty = Some v ->
-      rred (Eparen (Eval v1 ty1) ty) m
+  | red_paren: forall v1 ty1 ty2 ty m v,
+      sem_cast v1 ty1 ty2 = Some v ->
+      rred (Eparen (Eval v1 ty1) ty2 ty) m
         E0 (Eval v ty) m
   | red_builtin: forall ef tyargs el ty m vargs t vres m',
       cast_arguments el tyargs vargs ->
@@ -379,8 +379,8 @@ Inductive context: kind -> kind -> (expr -> expr) -> Prop :=
       contextlist k C -> context k RV (fun x => Ebuiltin ef tyargs (C x) ty)
   | ctx_comma: forall k C e2 ty,
       context k RV C -> context k RV (fun x => Ecomma (C x) e2 ty)
-  | ctx_paren: forall k C ty,
-      context k RV C -> context k RV (fun x => Eparen (C x) ty)
+  | ctx_paren: forall k C tycast ty,
+      context k RV C -> context k RV (fun x => Eparen (C x) tycast ty)
 
 with contextlist: kind -> (expr -> exprlist) -> Prop :=
   | ctx_list_head: forall k C el,
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 676f3faf..f8c3963e 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -68,7 +68,7 @@ Fixpoint simple (a: expr) : bool :=
   | Ecomma _ _ _ => false
   | Ecall _ _ _ => false
   | Ebuiltin _ _ _ _ => false
-  | Eparen _ _ => false
+  | Eparen _ _ _ => false
   end.
 
 Fixpoint simplelist (rl: exprlist) : bool :=
@@ -199,8 +199,8 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop :=
       leftcontext k RV (fun x => Ebuiltin ef tyargs (C x) ty)
   | lctx_comma: forall k C e2 ty,
       leftcontext k RV C -> leftcontext k RV (fun x => Ecomma (C x) e2 ty)
-  | lctx_paren: forall k C ty,
-      leftcontext k RV C -> leftcontext k RV (fun x => Eparen (C x) ty)
+  | lctx_paren: forall k C tycast ty,
+      leftcontext k RV C -> leftcontext k RV (fun x => Eparen (C x) tycast ty)
 
 with leftcontextlist: kind -> (expr -> exprlist) -> Prop :=
   | lctx_list_head: forall k C el,
@@ -248,7 +248,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       eval_simple_rvalue e m r1 v ->
       bool_val v (typeof r1) = Some true ->
       estep (ExprState f (C (Eseqand r1 r2 ty)) k e m)
-         E0 (ExprState f (C (Eparen (Eparen r2 type_bool) ty)) k e m)
+         E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m)
   | step_seqand_false: forall f C r1 r2 ty k e m v,
       leftcontext RV RV C ->
       eval_simple_rvalue e m r1 v ->
@@ -267,14 +267,14 @@ Inductive estep: state -> trace -> state -> Prop :=
       eval_simple_rvalue e m r1 v ->
       bool_val v (typeof r1) = Some false ->
       estep (ExprState f (C (Eseqor r1 r2 ty)) k e m)
-         E0 (ExprState f (C (Eparen (Eparen r2 type_bool) ty)) k e m)
+         E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m)
 
   | step_condition: forall f C r1 r2 r3 ty k e m v b,
       leftcontext RV RV C ->
       eval_simple_rvalue e m r1 v ->
       bool_val v (typeof r1) = Some b ->
       estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m)
-         E0 (ExprState f (C (Eparen (if b then r2 else r3) ty)) k e m)
+         E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m)
 
   | step_assign: forall f C l r ty k e m b ofs v v' t m',
       leftcontext RV RV C ->
@@ -351,11 +351,11 @@ Inductive estep: state -> trace -> state -> Prop :=
       estep (ExprState f (C (Ecomma r1 r2 ty)) k e m)
          E0 (ExprState f (C r2) k e m)
 
-  | step_paren: forall f C r ty k e m v1 v,
+  | step_paren: forall f C r tycast ty k e m v1 v,
       leftcontext RV RV C ->
       eval_simple_rvalue e m r v1 ->
-      sem_cast v1 (typeof r) ty = Some v ->
-      estep (ExprState f (C (Eparen r ty)) k e m)
+      sem_cast v1 (typeof r) tycast = Some v ->
+      estep (ExprState f (C (Eparen r tycast ty)) k e m)
          E0 (ExprState f (C (Eval v ty)) k e m)
 
   | step_call: forall f C rf rargs ty k e m targs tres cconv vf vargs fd,
@@ -557,8 +557,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       /\ deref_loc ge ty m b ofs t v1
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
-  | Eparen (Eval v1 ty1) ty =>
-      exists v, sem_cast v1 ty1 ty = Some v
+  | Eparen (Eval v1 ty1) ty2 ty =>
+      exists v, sem_cast v1 ty1 ty2 = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs tyres cconv fd vl,
@@ -1039,7 +1039,7 @@ Definition simple_side_effect (r: expr) : Prop :=
   | Ecomma r1 r2 _ => simple r1 = true
   | Ecall r1 rl _ => simple r1 = true /\ simplelist rl = true
   | Ebuiltin ef tyargs rl _ => simplelist rl = true
-  | Eparen r1 _ => simple r1 = true
+  | Eparen r1 _ _ => simple r1 = true
   | _ => False
   end.
 
@@ -1114,7 +1114,7 @@ Ltac Base :=
   Base.
   right; exists (fun x => Ebuiltin ef tyargs (C' x) ty); exists a'. rewrite D; simpl; auto.
 (* rparen *)
-  Kind. Rec H RV C (fun x => (Eparen x ty)). Base.
+  Kind. Rec H RV C (fun x => (Eparen x tycast ty)). Base.
 (* cons *)
   destruct (H RV (fun x => C (Econs x rl))) as [A | [C' [a' [A [B D]]]]].
     eapply contextlist'_head; eauto. auto.
@@ -1253,7 +1253,7 @@ Proof.
   left; apply step_rred; eauto. econstructor; eauto. auto.
 (* paren *)
   eapply plus_right; eauto.
-  eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x ty)); eauto.
+  eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x tycast ty)); eauto.
   left; apply step_rred; eauto. econstructor; eauto. auto.
 (* call *)
   exploit eval_simple_list_implies; eauto. intros [vl' [A B]].
@@ -1383,7 +1383,7 @@ Proof.
   econstructor; econstructor; eapply step_builtin; eauto.
   eapply can_eval_simple_list; eauto. 
 (* paren *)
-  exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x ty))); eauto.
+  exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x tycast ty))); eauto.
   intros [v1 [E1 S1]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [v CAST].
   econstructor; econstructor; eapply step_paren; eauto.
@@ -1688,23 +1688,21 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
   | eval_cast: forall e m a t m' a' ty,
       eval_expr e m RV a t m' a' ->
       eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty)
-  | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v' v,
+  | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) = Some true ->
       eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 ->
-      sem_cast v2 (typeof a2) type_bool = Some v' ->
-      sem_cast v' type_bool ty = Some v ->
+      sem_cast v2 (typeof a2) type_bool = Some v ->
       eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty)
   | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) = Some false ->
       eval_expr e m RV (Eseqand a1 a2 ty) t1 m' (Eval (Vint Int.zero) ty)
-  | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v' v,
+  | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) = Some false ->
       eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 ->
-      sem_cast v2 (typeof a2) type_bool = Some v' ->
-      sem_cast v' type_bool ty = Some v ->
+      sem_cast v2 (typeof a2) type_bool = Some v ->
       eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty)
   | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1,
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
@@ -2257,18 +2255,13 @@ Proof.
 (* seqand true *)
   exploit (H0 (fun x => C(Eseqand x a2 ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
-  exploit (H4 (fun x => C(Eparen (Eparen x type_bool) ty))).
+  exploit (H4 (fun x => C(Eparen x type_bool ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]].
   simpl; intuition. eapply star_trans. eexact D. 
   eapply star_left. left; eapply step_seqand_true; eauto. rewrite B; auto. 
-  eapply star_trans. eexact G.
-  set (C' := fun x => C (Eparen x ty)).
-  change (C (Eparen (Eparen a2' type_bool) ty)) with (C' (Eparen a2' type_bool)).
-  eapply star_two.
-  left; eapply step_paren; eauto. unfold C'; eapply leftcontext_compose; eauto. repeat constructor.
-  rewrite F; eauto.
-  unfold C'. left; eapply step_paren; eauto. constructor. 
-  eauto. eauto. eauto. traceEq. 
+  eapply star_right. eexact G.
+  left; eapply step_paren; eauto. rewrite F; eauto.
+  eauto. eauto. traceEq. 
 (* seqand false *)
   exploit (H0 (fun x => C(Eseqand x a2 ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
@@ -2278,18 +2271,13 @@ Proof.
 (* seqor false *)
   exploit (H0 (fun x => C(Eseqor x a2 ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
-  exploit (H4 (fun x => C(Eparen (Eparen x type_bool) ty))).
+  exploit (H4 (fun x => C(Eparen x type_bool ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]].
   simpl; intuition. eapply star_trans. eexact D. 
   eapply star_left. left; eapply step_seqor_false; eauto. rewrite B; auto. 
-  eapply star_trans. eexact G.
-  set (C' := fun x => C (Eparen x ty)).
-  change (C (Eparen (Eparen a2' type_bool) ty)) with (C' (Eparen a2' type_bool)).
-  eapply star_two.
-  left; eapply step_paren; eauto. unfold C'; eapply leftcontext_compose; eauto. repeat constructor.
-  rewrite F; eauto.
-  unfold C'. left; eapply step_paren; eauto. constructor. 
-  eauto. eauto. eauto. traceEq. 
+  eapply star_right. eexact G.
+  left; eapply step_paren; eauto. rewrite F; eauto.
+  eauto. eauto. traceEq. 
 (* seqor true *)
   exploit (H0 (fun x => C(Eseqor x a2 ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
@@ -2299,7 +2287,7 @@ Proof.
 (* condition *)
   exploit (H0 (fun x => C(Econdition x a2 a3 ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
-  exploit (H4 (fun x => C(Eparen x ty))).
+  exploit (H4 (fun x => C(Eparen x ty ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]].
   simpl. split; auto. split; auto. 
   eapply star_trans. eexact D.
@@ -2684,7 +2672,7 @@ Fixpoint esize (a: expr) : nat :=
   | Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat
   | Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat
   | Ebuiltin ef tyargs rl _ => S(esizelist rl)
-  | Eparen r1 _ => S(esize r1)
+  | Eparen r1 _ _ => S(esize r1)
   end
 
 with esizelist (el: exprlist) : nat :=
@@ -2807,7 +2795,7 @@ Proof.
   eapply forever_N_plus. eapply plus_right. eexact R. 
   left; eapply step_seqand_true; eauto. rewrite Q; eauto.
   reflexivity. 
-  eapply COE with (C := fun x => (C (Eparen (Eparen x type_bool) ty))). eauto.
+  eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqor left *)
   eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
@@ -2820,7 +2808,7 @@ Proof.
   eapply forever_N_plus. eapply plus_right. eexact R. 
   left; eapply step_seqor_false; eauto. rewrite Q; eauto.
   reflexivity. 
-  eapply COE with (C := fun x => (C (Eparen (Eparen x type_bool) ty))). eauto.
+  eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* condition top *)
   eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
@@ -2833,7 +2821,7 @@ Proof.
   eapply forever_N_plus. eapply plus_right. eexact R. 
   left; eapply step_condition; eauto. rewrite Q; eauto.
   reflexivity. 
-  eapply COE with (C := fun x => (C (Eparen x ty))). eauto.
+  eapply COE with (C := fun x => (C (Eparen x ty ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* assign left *)
   eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index a926bc3b..fa74f11c 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -61,7 +61,7 @@ Inductive expr : Type :=
                                                  (**r builtin function call *)
   | Eloc (b: block) (ofs: int) (ty: type)
                        (**r memory location, result of evaluating a l-value *)
-  | Eparen (r: expr) (ty: type)                   (**r marked subexpression *)
+  | Eparen (r: expr) (tycast: type) (ty: type)   (**r marked subexpression *)
 
 with exprlist : Type :=
   | Enil
@@ -87,7 +87,8 @@ but appear during reduction.  These forms are:
 - [Eval v] where [v] is a pointer or [Vundef].  ([Eval] of an integer or 
   float value can occur in a source term and represents a numeric literal.)
 - [Eloc b ofs], which appears during reduction of l-values.
-- [Eparen r], which appears during reduction of conditionals [r1 ? r2 : r3].
+- [Eparen r tycast ty], which appears during reduction of conditionals
+  [r1 ? r2 : r3] as well as sequential `and' / `or'.
 
 Some C expressions are derived forms.  Array access [r1[r2]] is expressed
 as [*(r1 + r2)].
@@ -128,7 +129,7 @@ Definition typeof (a: expr) : type :=
   | Ecomma _ _ ty => ty
   | Ecall _ _ ty => ty
   | Ebuiltin _ _ _ ty => ty
-  | Eparen _ ty => ty
+  | Eparen _ _ ty => ty
   end.
 
 (** ** Statements *)
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 3454ddcf..6f193cd9 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -88,7 +88,7 @@ Fixpoint constval (a: expr) : res val :=
       do v1 <- constval r1;
       do v2 <- constval r2;
       match bool_val v1 (typeof r1) with
-      | Some true => do v3 <- do_cast v2 (typeof r2) type_bool; do_cast v3 type_bool ty
+      | Some true => do_cast v2 (typeof r2) type_bool
       | Some false => OK (Vint Int.zero)
       | None => Error(msg "undefined && operation")
       end
@@ -96,7 +96,7 @@ Fixpoint constval (a: expr) : res val :=
       do v1 <- constval r1;
       do v2 <- constval r2;
       match bool_val v1 (typeof r1) with
-      | Some false => do v3 <- do_cast v2 (typeof r2) type_bool; do_cast v3 type_bool ty
+      | Some false => do_cast v2 (typeof r2) type_bool
       | Some true => OK (Vint Int.one)
       | None => Error(msg "undefined || operation")
       end
@@ -126,8 +126,8 @@ Fixpoint constval (a: expr) : res val :=
       | _ =>
           Error(msg "ill-typed field access")
       end
-  | Eparen r ty =>
-      do v <- constval r; do_cast v (typeof r) ty
+  | Eparen r tycast ty =>
+      do v <- constval r; do_cast v (typeof r) tycast
   | _ =>
     Error(msg "not a compile-time constant")
   end.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 16004fc0..73fd90b7 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -63,7 +63,7 @@ Fixpoint simple (a: expr) : Prop :=
   | Ecomma r1 r2 _ => simple r1 /\ simple r2
   | Ecall _ _ _ => False
   | Ebuiltin _ _ _ _ => False
-  | Eparen r1 _ => simple r1
+  | Eparen r1 _ _ => simple r1
   end.
 
 (** A big-step semantics for simple expressions.  Similar to the
@@ -126,21 +126,19 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1)))
   | esr_alignof: forall ty1 ty,
       eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1)))
-  | esr_seqand_true: forall r1 r2 ty v1 v2 v3 v4,
+  | esr_seqand_true: forall r1 r2 ty v1 v2 v3,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true ->
       eval_simple_rvalue r2 v2 ->
       sem_cast v2 (typeof r2) type_bool = Some v3 ->
-      sem_cast v3 type_bool ty = Some v4 ->
-      eval_simple_rvalue (Eseqand r1 r2 ty) v4
+      eval_simple_rvalue (Eseqand r1 r2 ty) v3
   | esr_seqand_false: forall r1 r2 ty v1,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false ->
       eval_simple_rvalue (Eseqand r1 r2 ty) (Vint Int.zero)
-  | esr_seqor_false: forall r1 r2 ty v1 v2 v3 v4,
+  | esr_seqor_false: forall r1 r2 ty v1 v2 v3,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false ->
       eval_simple_rvalue r2 v2 ->
       sem_cast v2 (typeof r2) type_bool = Some v3 ->
-      sem_cast v3 type_bool ty = Some v4 ->
-      eval_simple_rvalue (Eseqor r1 r2 ty) v4
+      eval_simple_rvalue (Eseqor r1 r2 ty) v3
   | esr_seqor_true: forall r1 r2 ty v1,
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true ->
       eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one)
@@ -152,9 +150,9 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_comma: forall r1 r2 ty v1 v,
       eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v ->
       eval_simple_rvalue (Ecomma r1 r2 ty) v
-  | esr_paren: forall r ty v v',
-      eval_simple_rvalue r v -> sem_cast v (typeof r) ty = Some v' ->
-      eval_simple_rvalue (Eparen r ty) v'.
+  | esr_paren: forall r tycast ty v v',
+      eval_simple_rvalue r v -> sem_cast v (typeof r) tycast = Some v' ->
+      eval_simple_rvalue (Eparen r tycast ty) v'.
 
 End SIMPLE_EXPRS.
 
@@ -206,10 +204,10 @@ Proof.
   inv EV. econstructor; eauto. constructor. 
   inv EV. econstructor; eauto. constructor. constructor.
   inv EV. econstructor; eauto. constructor.
-  inv EV. inv H2. eapply esr_seqand_true; eauto. constructor.
+  inv EV. eapply esr_seqand_true; eauto. constructor.
   inv EV. eapply esr_seqand_false; eauto. constructor.
   inv EV. eapply esr_seqor_true; eauto. constructor.
-  inv EV. inv H2. eapply esr_seqor_false; eauto. constructor.
+  inv EV. eapply esr_seqor_false; eauto. constructor.
   inv EV. eapply esr_condition; eauto. constructor. 
   inv EV. constructor.
   inv EV. constructor.
@@ -413,16 +411,16 @@ Proof.
   (* seqand *)
   destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
   exploit bool_val_inject. eexact E. eauto. intros E'.
-  assert (b = true) by congruence. subst b. monadInv H5. 
-  eapply sem_cast_match; eauto. eapply sem_cast_match; eauto.
+  assert (b = true) by congruence. subst b.
+  eapply sem_cast_match; eauto.
   destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
   exploit bool_val_inject. eexact E. eauto. intros E'.
   assert (b = false) by congruence. subst b. inv H2. auto.
   (* seqor *)
   destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
   exploit bool_val_inject. eexact E. eauto. intros E'.
-  assert (b = false) by congruence. subst b. monadInv H5. 
-  eapply sem_cast_match; eauto. eapply sem_cast_match; eauto.
+  assert (b = false) by congruence. subst b. 
+  eapply sem_cast_match; eauto.
   destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
   exploit bool_val_inject. eexact E. eauto. intros E'.
   assert (b = true) by congruence. subst b. inv H2. auto.
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 4e0ee7f3..e1b53af8 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -272,8 +272,8 @@ let rec expr p (prec, e) =
       fprintf p "%s@[<hov 1>(%a)@]" (extern_atom id) exprlist (true, args)
   | Ebuiltin(_, _, args, _) ->
       fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
-  | Eparen(a1, ty) ->
-      fprintf p "(%s) %a" (name_type ty) expr (prec', a1)
+  | Eparen(a1, tycast, ty) ->
+      fprintf p "(%s) %a" (name_type tycast) expr (prec', a1)
   end;
   if prec' < prec then fprintf p ")@]" else fprintf p "@]"
 
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 05d9c860..df33d727 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -197,8 +197,8 @@ Definition make_assign (l r: expr) : statement :=
 *)
 
 Inductive set_destination : Type :=
-  | SDbase (ty: type) (tmp: ident)
-  | SDcons (ty: type) (tmp: ident) (sd: set_destination).
+  | SDbase (tycast ty: type) (tmp: ident)
+  | SDcons (tycast ty: type) (tmp: ident) (sd: set_destination).
 
 Inductive destination : Type := 
   | For_val
@@ -209,8 +209,8 @@ Definition dummy_expr := Econst_int Int.zero type_int32s.
 
 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)
+  | SDbase tycast ty tmp => Sset tmp (Ecast a tycast) :: nil
+  | SDcons tycast ty tmp sd' => Sset tmp (Ecast a tycast) :: do_set sd' (Etempvar tmp ty)
   end.
 
 Definition finish (dst: destination) (sl: list statement) (a: expr) :=
@@ -221,11 +221,11 @@ Definition finish (dst: destination) (sl: list statement) (a: expr) :=
   end.
 
 Definition sd_temp (sd: set_destination) :=
-  match sd with SDbase _ tmp => tmp | SDcons _ tmp _ => tmp end.
+  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).
+  SDbase type_bool 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).
+  let tmp :=  sd_temp sd in SDcons type_bool ty tmp sd.
 
 Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) :=
   match a with
@@ -311,8 +311,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 (SDbase ty t)) r2;
-          do (sl3, a3) <- transl_expr (For_set (SDbase ty t)) r3;
+          do (sl2, a2) <- transl_expr (For_set (SDbase ty ty t)) r2;
+          do (sl3, a3) <- transl_expr (For_set (SDbase ty ty t)) r3;
           ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
                Etempvar t ty)
       | For_effects =>
@@ -322,8 +322,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
                dummy_expr)
       | 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;
+          do (sl2, a2) <- transl_expr (For_set (SDcons ty ty t sd)) r2;
+          do (sl3, a3) <- transl_expr (For_set (SDcons ty ty t sd)) r3;
           ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
                dummy_expr)
       end
@@ -399,7 +399,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       | For_effects =>
           ret (sl ++ Sbuiltin None ef tyargs al :: nil, dummy_expr)
       end
-  | Csyntax.Eparen r1 ty =>
+  | Csyntax.Eparen r1 tycast ty =>
       error (msg "SimplExpr.transl_expr: paren")
   end
 
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index c907f77d..3802b957 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -1301,7 +1301,7 @@ Fixpoint esize (a: Csyntax.expr) : nat :=
   | Csyntax.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat
   | Csyntax.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat
   | Csyntax.Ebuiltin ef _ rl _ => S(esizelist rl)%nat
-  | Csyntax.Eparen r1 _ => S(esize r1)
+  | Csyntax.Eparen r1 _ _ => S(esize r1)
   end
 
 with esizelist (el: Csyntax.exprlist) : nat :=
@@ -1404,7 +1404,7 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; eauto.
-  apply S. apply tr_paren_val with (a1 := dummy_expr); auto. econstructor; eauto. 
+  apply S. apply tr_paren_val with (a1 := a2); auto. 
   apply tr_expr_monotone with tmp2; eauto. auto. auto.
   (* for effects *)
   exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
@@ -1415,7 +1415,7 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; eauto.
-  apply S. apply tr_paren_effects with (a1 := dummy_expr); auto. econstructor; eauto. 
+  apply S. apply tr_paren_effects with (a1 := a2); auto.
   apply tr_expr_monotone with tmp2; eauto. auto. auto.
   (* for set *)
   exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
@@ -1426,9 +1426,8 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; 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).
-  apply tr_expr_monotone with tmp2; eauto. auto. auto. auto.
+  apply S. apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto.
+  apply tr_expr_monotone with tmp2; eauto. auto. auto.
 (* seqand false *)
   exploit tr_top_leftcontext; eauto. clear H9. 
   intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [R S]]]]]]]].
@@ -1514,7 +1513,7 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; eauto.
-  apply S. apply tr_paren_val with (a1 := dummy_expr); auto. econstructor; eauto. 
+  apply S. apply tr_paren_val with (a1 := a2); auto.  
   apply tr_expr_monotone with tmp2; eauto. auto. auto.
   (* for effects *)
   exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
@@ -1525,7 +1524,7 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; eauto.
-  apply S. apply tr_paren_effects with (a1 := dummy_expr); auto. econstructor; eauto. 
+  apply S. apply tr_paren_effects with (a1 := a2); auto.
   apply tr_expr_monotone with tmp2; eauto. auto. auto.
   (* for set *)
   exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
@@ -1536,8 +1535,7 @@ Proof.
   apply push_seq. reflexivity. reflexivity.
   rewrite <- Kseqlist_app.
   eapply match_exprstates; 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 S. 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 1ef2e76d..83ddd1f4 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -176,8 +176,8 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
                     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 (SDbase ty t)) e2 sl2 a2 tmp2 ->
-      tr_expr le (For_set (SDbase ty t)) e3 sl3 a3 tmp3 ->
+      tr_expr le (For_set (SDbase ty ty t)) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (SDbase ty 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 ->
@@ -196,8 +196,8 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
                        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 (SDcons ty t sd)) e2 sl2 a2 tmp2 ->
-      tr_expr le (For_set (SDcons ty t sd)) e3 sl3 a3 tmp3 ->
+      tr_expr le (For_set (SDcons ty ty t sd)) e2 sl2 a2 tmp2 ->
+      tr_expr le (For_set (SDcons ty 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 ->
@@ -304,19 +304,19 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       tr_expr le dst (Csyntax.Ebuiltin ef tyargs el ty)
                    (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 (SDbase ty t)) e1 sl1 a1 tmp ->
+  | tr_paren_val: forall le e1 tycast ty sl1 a1 t tmp,
+      tr_expr le (For_set (SDbase tycast ty t)) e1 sl1 a1 tmp ->
       In t tmp -> 
-      tr_expr le For_val (Csyntax.Eparen e1 ty)
+      tr_expr le For_val (Csyntax.Eparen e1 tycast ty)
                        sl1
                        (Etempvar t ty) tmp
-  | tr_paren_effects: forall le e1 ty sl1 a1 tmp any,
+  | tr_paren_effects: forall le e1 tycast 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 t sd e1 ty sl1 a1 tmp any,
-      tr_expr le (For_set (SDcons ty t sd)) e1 sl1 a1 tmp ->
+      tr_expr le For_effects (Csyntax.Eparen e1 tycast ty) sl1 any tmp
+  | tr_paren_set: forall le t sd e1 tycast ty sl1 a1 tmp any,
+      tr_expr le (For_set (SDcons tycast ty t sd)) e1 sl1 a1 tmp ->
       In t tmp ->
-      tr_expr le (For_set sd) (Csyntax.Eparen e1 ty) sl1 any tmp
+      tr_expr le (For_set sd) (Csyntax.Eparen e1 tycast ty) sl1 any tmp
 
 with tr_exprlist: temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop :=
   | tr_nil: forall le tmp,
@@ -669,13 +669,13 @@ Proof.
 Qed.
 
 Lemma dest_for_set_condition_val:
-  forall tmp ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase ty tmp)) g2.
+  forall tmp tycast ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase tycast ty tmp)) g2.
 Proof.
   intros. destruct H. simpl. auto.
 Qed.
 
 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.
+  forall sd tmp tycast ty g1 g2, dest_below (For_set sd) g2 -> within tmp g1 g2 -> dest_below (For_set (SDcons tycast ty tmp sd)) g2.
 Proof.
   intros. destruct H0. simpl. auto.
 Qed.