Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr if

b and c are simple.


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

4 files changed, 197 insertions, 98 deletions

diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index e088c26..4bb550f 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -44,30 +44,30 @@ Variable ge: genv.
 
 (** Simple expressions are defined as follows. *)
 
-Fixpoint simple (a: expr) : Prop :=
+Fixpoint simple (a: expr) : bool :=
   match a with
-  | Eloc _ _ _ => True
-  | Evar _ _ => True
+  | Eloc _ _ _ => true
+  | Evar _ _ => true
   | Ederef r _ => simple r
   | Efield r _ _ => simple r
-  | Eval _ _ => True
-  | Evalof l _ => simple l /\ type_is_volatile (typeof l) = false
+  | Eval _ _ => true
+  | Evalof l _ => simple l && negb(type_is_volatile (typeof l))
   | Eaddrof l _ => simple l
   | Eunop _ r1 _ => simple r1
-  | Ebinop _ r1 r2 _ => simple r1 /\ simple r2
+  | Ebinop _ r1 r2 _ => simple r1 && simple r2
   | Ecast r1 _ => simple r1
-  | Econdition _ _ _ _ => False
-  | Esizeof _ _ => True
-  | Eassign _ _ _ => False
-  | Eassignop _ _ _ _ _ => False
-  | Epostincr _ _ _ => False
-  | Ecomma _ _ _ => False
-  | Ecall _ _ _ => False
-  | Eparen _ _ => False
+  | Econdition r1 r2 r3 _ => simple r1 && simple r2 && simple r3
+  | Esizeof _ _ => true
+  | Eassign _ _ _ => false
+  | Eassignop _ _ _ _ _ => false
+  | Epostincr _ _ _ => false
+  | Ecomma _ _ _ => false
+  | Ecall _ _ _ => false
+  | Eparen _ _ => false
   end.
 
-Fixpoint simplelist (rl: exprlist) : Prop :=
-  match rl with Enil => True | Econs r rl' => simple r /\ simplelist rl' end.
+Fixpoint simplelist (rl: exprlist) : bool :=
+  match rl with Enil => true | Econs r rl' => simple r && simplelist rl' end.
 
 (** Simple expressions have interesting properties: their evaluations always
   terminate, are deterministic, and preserve the memory state.
@@ -125,6 +125,13 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue r1 v1 ->
       sem_cast v1 (typeof r1) ty = Some v ->
       eval_simple_rvalue (Ecast r1 ty) v
+  | esr_condition: forall r1 r2 r3 ty v1 b v2 v,
+      simple r2 = true -> simple r3 = true ->
+      eval_simple_rvalue r1 v1 -> 
+      bool_val v1 (typeof r1) = Some b ->
+      eval_simple_rvalue (if b then r2 else r3) v2 ->
+      sem_cast v2 (typeof (if b then r2 else r3)) ty = Some v ->
+      eval_simple_rvalue (Econdition r1 r2 r3 ty) v
   | esr_sizeof: forall ty1 ty,
       eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))).
 
@@ -161,7 +168,7 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop :=
   | lctx_binop_left: forall k C op e2 ty,
       leftcontext k RV C -> leftcontext k RV (fun x => Ebinop op (C x) e2 ty)
   | lctx_binop_right: forall k C op e1 ty,
-      simple e1 -> leftcontext k RV C ->
+      simple e1 = true -> leftcontext k RV C ->
       leftcontext k RV (fun x => Ebinop op e1 (C x) ty)
   | lctx_cast: forall k C ty,
       leftcontext k RV C -> leftcontext k RV (fun x => Ecast (C x) ty)
@@ -170,19 +177,19 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop :=
   | lctx_assign_left: forall k C e2 ty,
       leftcontext k LV C -> leftcontext k RV (fun x => Eassign (C x) e2 ty)
   | lctx_assign_right: forall k C e1 ty,
-      simple e1 -> leftcontext k RV C ->
+      simple e1 = true -> leftcontext k RV C ->
       leftcontext k RV (fun x => Eassign e1 (C x) ty)
   | lctx_assignop_left: forall k C op e2 tyres ty,
       leftcontext k LV C -> leftcontext k RV (fun x => Eassignop op (C x) e2 tyres ty)
   | lctx_assignop_right: forall k C op e1 tyres ty,
-      simple e1 -> leftcontext k RV C ->
+      simple e1 = true -> leftcontext k RV C ->
       leftcontext k RV (fun x => Eassignop op e1 (C x) tyres ty)
   | lctx_postincr: forall k C id ty,
       leftcontext k LV C -> leftcontext k RV (fun x => Epostincr id (C x) ty)
   | lctx_call_left: forall k C el ty,
       leftcontext k RV C -> leftcontext k RV (fun x => Ecall (C x) el ty)
   | lctx_call_right: forall k C e1 ty,
-      simple e1 -> leftcontextlist k C ->
+      simple e1 = true -> leftcontextlist k C ->
       leftcontext k RV (fun x => Ecall e1 (C x) ty)
   | lctx_comma: forall k C e2 ty,
       leftcontext k RV C -> leftcontext k RV (fun x => Ecomma (C x) e2 ty)
@@ -193,7 +200,7 @@ with leftcontextlist: kind -> (expr -> exprlist) -> Prop :=
   | lctx_list_head: forall k C el,
       leftcontext k RV C -> leftcontextlist k (fun x => Econs (C x) el)
   | lctx_list_tail: forall k C e1,
-      simple e1 -> leftcontextlist k C ->
+      simple e1 = true -> leftcontextlist k C ->
       leftcontextlist k (fun x => Econs e1 (C x)).
 
 Lemma leftcontext_context:
@@ -231,6 +238,7 @@ Inductive estep: state -> trace -> state -> Prop :=
           t (ExprState f (C (Eval v ty)) k e m)
 
   | step_condition: forall f C r1 r2 r3 ty k e m v b,
+      simple r2 = false \/ simple r3 = false ->
       leftcontext RV RV C ->
       eval_simple_rvalue e m r1 v ->
       bool_val v (typeof r1) = Some b ->
@@ -670,6 +678,12 @@ Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econst
   FinishR.
 (* cast *)
   Steps H0 (fun x => C(Ecast x ty)). FinishR. 
+(* condition *)
+  Steps H2 (fun x => C(Econdition x r2 r3 ty)).
+  eapply star_left with (s2 := ExprState f (C (Eparen (if b then r2 else r3) ty)) k e m).
+  left; apply step_rred; eauto. constructor; auto. 
+  Steps H5 (fun x => C(Eparen x ty)). 
+  FinishR. auto.
 (* sizeof *)
   FinishR.
 (* loc *)
@@ -720,7 +734,7 @@ Qed.
 
 Lemma simple_can_eval:
   forall a from C,
-  simple a -> context from RV C -> safe (ExprState f (C a) k e m) ->
+  simple a = true -> context from RV C -> safe (ExprState f (C a) k e m) ->
   match from with
   | LV => exists b, exists ofs, eval_simple_lvalue e m a b ofs
   | RV => exists v, eval_simple_rvalue e m a v
@@ -742,7 +756,7 @@ Ltac StepR REC C' a :=
 
   induction a; intros from C S CTX SAFE;
   generalize (safe_expr_kind _ _ _ _ _ _ _ CTX SAFE); intro K; subst;
-  simpl in S; try contradiction; simpl.
+  simpl in S; try discriminate; simpl.
 (* val *)
   exists v; constructor.
 (* var *)
@@ -756,7 +770,8 @@ Ltac StepR REC C' a :=
   destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto.
   exists b; exists ofs; econstructor; eauto.
 (* valof *)
-  destruct S. StepL IHa (fun x => C(Evalof x ty)) a.
+  destruct (andb_prop _ _ S) as [S1 S2]. clear S. rewrite negb_true_iff in S2.
+  StepL IHa (fun x => C(Evalof x ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [TY [t [v LOAD]]].
   assert (t = E0). inv LOAD; auto. congruence. subst t.
   exists v; econstructor; eauto. congruence.
@@ -772,7 +787,7 @@ Ltac StepR REC C' a :=
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' EQ].
   exists v'; econstructor; eauto.
 (* binop *)
-  destruct S.
+  destruct (andb_prop _ _ S) as [S1 S2]; clear S.
   StepR IHa1 (fun x => C(Ebinop op x a2 ty)) a1.
   StepR IHa2 (fun x => C(Ebinop op (Eval v (typeof a1)) x ty)) a2.
   exploit safe_inv. eexact SAFE1. eauto. simpl. intros [v' EQ].
@@ -781,6 +796,23 @@ Ltac StepR REC C' a :=
   StepR IHa (fun x => C(Ecast x ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' CAST].
   exists v'; econstructor; eauto.
+(* condition *)
+  destruct (andb_prop _ _ S) as [S' S3]. destruct (andb_prop _ _ S') as [S1 S2]. clear S S'.
+  StepR IHa1 (fun x => C(Econdition x a2 a3 ty)) a1.
+  exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b BV].
+  set (a' := if b then a2 else a3).
+  assert (SAFE1: safe (ExprState f (C (Eparen a' ty)) k e m)).
+    eapply safe_steps. eexact SAFE0. apply star_one. left; apply step_rred; auto. 
+    unfold a'; constructor; auto.
+  assert (EV': exists v, eval_simple_rvalue e m a' v).
+    unfold a'; destruct b. 
+    eapply (IHa2 RV (fun x => C(Eparen x ty))); eauto.
+    eapply (IHa3 RV (fun x => C(Eparen x ty))); eauto.
+  destruct EV' as [v1 E1].
+  exploit safe_inv. eapply (eval_simple_rvalue_safe (fun x => C(Eparen x ty))). 
+  eexact E1. eauto. auto. eauto. 
+  simpl. intros [v2 CAST].
+  exists v2. econstructor; eauto. 
 (* sizeof *)
   econstructor; econstructor.
 (* loc *)
@@ -789,7 +821,7 @@ Qed.
 
 Lemma simple_can_eval_rval:
   forall r C, 
-  simple r -> context RV RV C -> safe (ExprState f (C r) k e m) ->
+  simple r = true -> context RV RV C -> safe (ExprState f (C r) k e m) ->
   exists v, eval_simple_rvalue e m r v
         /\ safe (ExprState f (C (Eval v (typeof r))) k e m).
 Proof.
@@ -799,7 +831,7 @@ Qed.
 
 Lemma simple_can_eval_lval:
   forall l C, 
-  simple l -> context LV RV C -> safe (ExprState f (C l) k e m) ->
+  simple l = true -> context LV RV C -> safe (ExprState f (C l) k e m) ->
   exists b, exists ofs, eval_simple_lvalue e m l b ofs
          /\ safe (ExprState f (C (Eloc b ofs (typeof l))) k e m).
 Proof.
@@ -916,14 +948,14 @@ Qed.
 
 Lemma simple_list_can_eval:
   forall rl C,
-  simplelist rl ->
+  simplelist rl = true ->
   contextlist' C ->
   safe (ExprState f (C rl) k e m) ->
   exists vl, eval_simple_list' rl vl.
 Proof.
   induction rl; intros.
   econstructor; constructor.
-  simpl in H; destruct H. 
+  simpl in H. destruct (andb_prop _ _ H). 
   exploit (simple_can_eval r1 RV (fun x => C(Econs x rl))); eauto.
   intros [v1 EV1].
   exploit (IHrl (fun x => C(Econs (Eval v1 (typeof r1)) x))); eauto.
@@ -952,14 +984,14 @@ Variable m: mem.
 
 Definition simple_side_effect (r: expr) : Prop :=
   match r with
-  | Evalof l _ => simple l /\ type_is_volatile (typeof l) = true
-  | Econdition r1 r2 r3 _ => simple r1
-  | Eassign l1 r2 _ => simple l1 /\ simple r2
-  | Eassignop _ l1 r2 _ _ => simple l1 /\ simple r2
-  | Epostincr _ l1 _ => simple l1
-  | Ecomma r1 r2 _ => simple r1
-  | Ecall r1 rl _ => simple r1 /\ simplelist rl
-  | Eparen r1 _ => simple r1
+  | Evalof l _ => simple l = true /\ type_is_volatile (typeof l) = true
+  | Econdition r1 r2 r3 _ => simple r1 = true /\ (simple r2 = false \/ simple r3 = false)
+  | Eassign l1 r2 _ => simple l1 = true /\ simple r2 = true
+  | Eassignop _ l1 r2 _ _ => simple l1 = true /\ simple r2 = true
+  | Epostincr _ l1 _ => simple l1 = true
+  | Ecomma r1 r2 _ => simple r1 = true
+  | Ecall r1 rl _ => simple r1 = true /\ simplelist rl = true
+  | Eparen r1 _ => simple r1 = true
   | _ => False
   end.
 
@@ -972,11 +1004,11 @@ Hint Constructors leftcontext leftcontextlist.
 Lemma decompose_expr:
   (forall a from C,
    context from RV C -> safe (ExprState f (C a) k e m) ->
-       simple a
+       simple a = true
     \/ exists C', exists a', a = C' a' /\ simple_side_effect a' /\ leftcontext RV from C')
 /\(forall rl C,
    contextlist' C -> safe (ExprState f (C rl) k e m) ->
-       simplelist rl
+       simplelist rl = true
     \/ exists C', exists a', rl = C' a' /\ simple_side_effect a' /\ leftcontextlist RV C').
 Proof.
   apply expr_expr_list_ind; intros; simpl; auto.
@@ -995,7 +1027,7 @@ Ltac Base :=
 (* rvalof *)
   Kind. Rec H LV C (fun x => Evalof x ty).
   destruct (type_is_volatile (typeof l)) as []_eqn.
-  Base. auto.
+  Base. rewrite H2; auto.
 (* deref *)
   Kind. Rec H RV C (fun x => Ederef x ty).
 (* addrof *)
@@ -1003,11 +1035,14 @@ Ltac Base :=
 (* unop *)
   Kind. Rec H RV C (fun x => Eunop op x ty).
 (* binop *)
-  Kind. Rec H RV C (fun x => Ebinop op x r2 ty). Rec H0 RV C (fun x => Ebinop op r1 x ty).
+  Kind. Rec H RV C (fun x => Ebinop op x r2 ty). rewrite H3.
+  Rec H0 RV C (fun x => Ebinop op r1 x ty).
 (* cast *)
   Kind. Rec H RV C (fun x => Ecast x ty).
 (* condition *)
-  Kind. Rec H RV C (fun x => Econdition x r2 r3 ty). Base.
+  Kind. Rec H RV C (fun x => Econdition x r2 r3 ty). rewrite H4; simpl. 
+  destruct (simple r2 && simple r3) as []_eqn. auto. 
+  rewrite andb_false_iff in Heqb. Base.
 (* assign *)
   Kind. Rec H LV C (fun x => Eassign x r ty). Rec H0 RV C (fun x => Eassign l x ty). Base.
 (* assignop *)
@@ -1028,8 +1063,8 @@ Ltac Base :=
   destruct (H RV (fun x => C (Econs x rl))) as [A | [C' [a' [A [B D]]]]].
     eapply contextlist'_head; eauto. auto.
   destruct (H0 (fun x => C (Econs r1 x))) as [A' | [C' [a' [A' [B D]]]]].
-    eapply contextlist'_tail; eauto. auto. 
-  auto.
+    eapply contextlist'_tail; eauto. auto.
+  rewrite A; rewrite A'; auto. 
   right; exists (fun x => Econs r1 (C' x)); exists a'. rewrite A'; eauto.
   right; exists (fun x => Econs (C' x) rl); exists a'. rewrite A; eauto.
 Qed.
@@ -1037,7 +1072,7 @@ Qed.
 Lemma decompose_topexpr:
   forall a,
   safe (ExprState f a k e m) ->
-       simple a
+       simple a = true
     \/ exists C, exists a', a = C a' /\ simple_side_effect a' /\ leftcontext RV RV C.
 Proof.
   intros. eapply (proj1 decompose_expr). apply ctx_top. auto.
@@ -1178,6 +1213,7 @@ Proof.
   exploit safe_inv. eexact S1. eauto. simpl. intros [A [t [v B]]].
   econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence. 
 (* condition *)
+  destruct Q.
   exploit (simple_can_eval_rval f k e m b1 (fun x => C(Econdition x b2 b3 ty))); eauto.
   intros [v1 [E1 S1]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [b BV].
@@ -1541,6 +1577,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV a t m' a' ->
       eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty)
   | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v,
+      simple a2 = false \/ simple a3 = false ->
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) = Some b ->
       eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' ->
@@ -1774,7 +1811,8 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop :=
   | evalinf_condition: forall e m a1 a2 a3 ty t1,
       evalinf_expr e m RV a1 t1 ->
       evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1
-  | evalinf_condition_true: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b,
+  | evalinf_condition_2: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b,
+      simple a2 = false \/ simple a3 = false ->
       eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 ->
       bool_val v1 (typeof a1) = Some b ->
       evalinf_expr e m' RV (if b then a2 else a3) t2 ->
@@ -1973,17 +2011,18 @@ Qed.
 
 Lemma exprlist_app_leftcontext:
   forall rl1 rl2,
-  simplelist rl1 -> leftcontextlist RV (fun x => exprlist_app rl1 (Econs x rl2)).
+  simplelist rl1 = true -> leftcontextlist RV (fun x => exprlist_app rl1 (Econs x rl2)).
 Proof.
   induction rl1; simpl; intros. 
   apply lctx_list_head. constructor.
-  destruct H. apply lctx_list_tail. auto. auto. 
+  destruct (andb_prop _ _ H). apply lctx_list_tail. auto. auto. 
 Qed.
 
 Lemma exprlist_app_simple:
-  forall rl1 rl2, simplelist rl1 -> simplelist rl2 -> simplelist (exprlist_app rl1 rl2).
+  forall rl1 rl2,
+  simplelist (exprlist_app rl1 rl2) = simplelist rl1 && simplelist rl2.
 Proof.
-  induction rl1; simpl; intros. auto. destruct H; auto. 
+  induction rl1; intros; simpl. auto. rewrite IHrl1. apply andb_assoc. 
 Qed.
 
 Lemma bigstep_to_steps:
@@ -1994,12 +2033,12 @@ Lemma bigstep_to_steps:
 /\(forall e m K a t m' a',
    eval_expr e m K a t m' a' ->
    forall C f k, leftcontext K RV C ->
-   simple a' /\ typeof a' = typeof a /\
+   simple a' = true /\ typeof a' = typeof a /\
    star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m'))
 /\(forall e m al t m' al',
    eval_exprlist e m al t m' al' ->
-   forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 -> simplelist al2 ->
-   simplelist al' /\
+   forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 = true -> simplelist al2 = true ->
+   simplelist al' = true /\
    star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m)
               t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m'))
 /\(forall e m s t m' out,
@@ -2033,7 +2072,7 @@ Proof.
 (* valof *)
   exploit (H1 (fun x => C(Evalof x ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
-  simpl; intuition; eauto. congruence.
+  simpl; intuition; eauto. rewrite A; rewrite B; rewrite H; auto.
 (* valof volatile *)
   exploit (H1 (fun x => C(Evalof x ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
@@ -2064,11 +2103,11 @@ Proof.
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
   simpl; intuition; eauto.
 (* condition *)
-  exploit (H0 (fun x => C(Econdition x a2 a3 ty))).
+  exploit (H1 (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 (H5 (fun x => C(Eparen x ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]].
-  simpl; intuition.
+  simpl. split; auto. split; auto. 
   eapply star_trans. eexact D.
   eapply star_left. left; eapply step_condition; eauto. rewrite B; eauto. 
   eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. 
@@ -2115,7 +2154,7 @@ Proof.
 (* call *)
   exploit (H0 (fun x => C(Ecall x rargs ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
-  exploit (H2 rf' Enil ty C); eauto. red; auto. intros [E F].
+  exploit (H2 rf' Enil ty C); eauto. intros [E F].
   simpl; intuition. 
   eapply star_trans. eexact D.
   eapply star_trans. eexact F. 
@@ -2130,10 +2169,9 @@ Proof.
     eapply leftcontext_compose; eauto. repeat constructor. auto.
     apply exprlist_app_leftcontext; auto. intros [A [B D]].
   exploit (H2 a0 (exprlist_app al2 (Econs a1' Enil))); eauto.
-  apply exprlist_app_simple; auto. simpl. auto. 
+  rewrite exprlist_app_simple. simpl. rewrite H5; rewrite A; auto. 
   repeat rewrite exprlist_app_assoc. simpl.  
   intros [E F].
-
   simpl; intuition. 
   eapply star_trans; eauto.
 
@@ -2398,15 +2436,15 @@ Lemma eval_expr_to_steps:
    forall e m K a t m' a',
    eval_expr e m K a t m' a' ->
    forall C f k, leftcontext K RV C ->
-   simple a' /\ typeof a' = typeof a /\
+   simple a' = true /\ typeof a' = typeof a /\
    star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m').
 Proof (proj1 (proj2 bigstep_to_steps)).
 
 Lemma eval_exprlist_to_steps:
    forall e m al t m' al',
    eval_exprlist e m al t m' al' ->
-   forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 -> simplelist al2 ->
-   simplelist al' /\
+   forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 = true -> simplelist al2 = true ->
+   simplelist al' = true /\
    star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m)
               t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m').
 Proof (proj1 (proj2 (proj2 bigstep_to_steps))).
@@ -2495,7 +2533,7 @@ Proof.
   assert (COEL:
     forall e m a t C f k a1 al ty,
     evalinf_exprlist e m a t ->
-    leftcontext RV RV C -> simple a1 -> simplelist al ->
+    leftcontext RV RV C -> simple a1 = true -> simplelist al = true ->
     forever_N step lt ge (esizelist a)
                    (ExprState f (C (Ecall a1 (exprlist_app al a) ty)) k e m) t).
   cofix COEL.
@@ -2516,7 +2554,8 @@ Proof.
   change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0).
   rewrite <- exprlist_app_assoc.  
   eapply COEL. eauto. auto. auto. 
-  apply exprlist_app_simple. auto. simpl; auto. traceEq.
+  rewrite exprlist_app_simple. simpl. rewrite H2; rewrite P; auto.
+  auto.
 
   intros. inv H.
 (* field *)
@@ -2559,7 +2598,7 @@ Proof.
   eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. 
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* condition *)
-  destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 ty)) f k)
+  destruct (eval_expr_to_steps _ _ _ _ _ _ _ H2 (fun x => C(Econdition x a2 a3 ty)) f k)
   as [P [Q R]]. 
   eapply leftcontext_compose; eauto. repeat constructor.
   eapply forever_N_plus. eapply plus_right. eexact R. 
@@ -2613,7 +2652,7 @@ Proof.
   as [P [Q R]]. 
   eapply leftcontext_compose; eauto. repeat constructor.
   eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega.
-  eapply COEL with (al := Enil). eauto. auto. auto. red; auto. traceEq.
+  eapply COEL with (al := Enil). eauto. auto. auto. auto. traceEq.
 (* call *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k)
   as [P [Q R]]. 
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 1dae78c..7b37692 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -21,6 +21,7 @@ Require Import Values.
 Require Import AST.
 Require Import Csyntax.
 Require Import Csem.
+Require Cstrategy.
 Require Import Clight.
 
 Module C := Csyntax.
@@ -231,19 +232,25 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
       do (sl1, a1) <- transl_expr For_val r1;
       ret (finish dst sl1 (Ecast a1 ty))
   | C.Econdition r1 r2 r3 ty =>
-      do (sl1, a1) <- transl_expr For_val r1;
-      do (sl2, a2) <- transl_expr (cast_destination ty dst) r2;
-      do (sl3, a3) <- transl_expr (cast_destination ty dst) r3;
-      match dst with
-      | For_val =>
-          do t <- gensym ty;
-          ret (sl1 ++ makeif a1 (Ssequence (makeseq sl2) (Sset t (Ecast a2 ty)))
-                                (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil,
-               Etempvar t ty)
-      | For_effects | For_test _ _ _ =>
-          ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
-               dummy_expr)
-      end
+      if Cstrategy.simple r2 && Cstrategy.simple r3 then (
+        do (sl1, a1) <- transl_expr For_val r1;
+        do (sl2, a2) <- transl_expr For_val r2;
+        do (sl3, a3) <- transl_expr For_val r3;
+        ret (finish dst sl1 (Econdition a1 a2 a3 ty))
+      ) else (
+        do (sl1, a1) <- transl_expr For_val r1;
+        do (sl2, a2) <- transl_expr (cast_destination ty dst) r2;
+        do (sl3, a3) <- transl_expr (cast_destination ty dst) r3;
+        match dst with
+        | For_val =>
+            do t <- gensym ty;
+            ret (sl1 ++ makeif a1 (Ssequence (makeseq sl2) (Sset t (Ecast a2 ty)))
+                                  (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil,
+                 Etempvar t ty)
+        | For_effects | For_test _ _ _ =>
+            ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
+                 dummy_expr)
+        end)
   | C.Eassign l1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val l1;
       do (sl2, a2) <- transl_expr For_val r2;
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 4df5f03..a88e4c3 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -110,32 +110,38 @@ Qed.
 
 Lemma tr_simple_nil:
   (forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
-   dst = For_val \/ dst = For_effects -> simple r -> sl = nil)
+   dst = For_val \/ dst = For_effects -> simple r = true -> sl = nil)
 /\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
-   simplelist rl -> sl = nil).
+   simplelist rl = true -> sl = nil).
 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 contradiction; 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 H6. inv H1; try congruence. rewrite H0; auto. simpl; auto.
+  destruct (andb_prop _ _ H6). inv H1.
   rewrite H0; auto. simpl; auto.
+  rewrite H9 in H8; discriminate.
   rewrite H0; auto. simpl; auto.
-  destruct H7. rewrite H0; auto. rewrite H2; auto. simpl; auto.
   rewrite H0; auto. simpl; auto.
-  destruct H6. rewrite H0; auto.
+  destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto.
+  rewrite H0; auto. simpl; auto.
+  destruct (andb_prop _ _ H13). destruct (andb_prop _ _ H14).
+  rewrite H2; auto. simpl; auto.
+  destruct (andb_prop _ _ H14). destruct (andb_prop _ _ H15). intuition congruence.
+  destruct (andb_prop _ _ H13). destruct (andb_prop _ _ H14). intuition congruence.
+  destruct (andb_prop _ _ H6). rewrite H0; auto.
 Qed.
 
 Lemma tr_simple_expr_nil:
   forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
-  dst = For_val \/ dst = For_effects -> simple r -> sl = nil.
+  dst = For_val \/ dst = For_effects -> simple r = true -> sl = nil.
 Proof (proj1 tr_simple_nil).
 
 Lemma tr_simple_exprlist_nil:
   forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
-  simplelist rl -> sl = nil.
+  simplelist rl = true -> sl = nil.
 Proof (proj2 tr_simple_nil).
 
 (** Evaluation of simple expressions and of their translation *)
@@ -222,6 +228,16 @@ Opaque makeif.
   subst sl1; simpl.
   assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence.
   destruct dst; auto. simpl; econstructor; eauto.
+(* condition *)
+  exploit H2; eauto. intros [A [B C]]. subst sl1. 
+  assert (tr_expr le For_val (if b then r2 else r3) (if b then sl2 else sl3) (if b then a2 else a3) (if b then tmp2 else tmp3)).
+    destruct b; auto.
+  exploit H5; eauto. intros [D [E F]]. 
+  assert (eval_expr tge e le m (Econdition a1 a2 a3 ty) v).
+    econstructor; eauto. congruence. rewrite <- E. auto. 
+  destruct dst; auto. simpl; econstructor; eauto. 
+  intuition congruence.
+  intuition congruence.
 (* sizeof *)
   destruct dst.
   split; auto. split; auto. constructor.
@@ -445,12 +461,20 @@ Ltac UNCHANGED :=
   intros. rewrite <- app_ass. econstructor; eauto.
 (* condition *)
   inv H1.
+  (* simple *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. econstructor. auto. auto. eauto.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto. auto. auto. 
   (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
   TR. 
   rewrite Q. rewrite app_ass. eauto. 
   red; auto.
-  intros. rewrite <- app_ass. econstructor. apply S; auto. 
+  intros. rewrite <- app_ass. econstructor. auto. apply S; auto. 
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto. auto. auto. 
@@ -459,7 +483,7 @@ Ltac UNCHANGED :=
   TR. 
   rewrite Q. rewrite app_ass. eauto. 
   red; auto.
-  intros. rewrite <- app_ass. econstructor. auto. apply S; auto. 
+  intros. rewrite <- app_ass. econstructor. auto. auto. apply S; auto. 
   eapply tr_expr_invariant; eauto. UNCHANGED.
   eapply tr_expr_invariant; eauto. UNCHANGED.
   auto. auto. auto. auto. auto.
@@ -1065,8 +1089,8 @@ Proof.
   rewrite (makeseq_nolabel sl2); auto.
   rewrite (makeseq_nolabel sl3); auto.
   apply makeif_nolabel; NoLabelTac.
-  rewrite (makeseq_nolabel sl2). auto. apply H3. apply nolabel_dest_cast; auto. 
-  rewrite (makeseq_nolabel sl3). auto. apply H5. apply nolabel_dest_cast; auto.
+  rewrite (makeseq_nolabel sl2). auto. apply H4. apply nolabel_dest_cast; auto. 
+  rewrite (makeseq_nolabel sl3). auto. apply H6. apply nolabel_dest_cast; auto.
   eapply tr_rvalof_nolabel; eauto.
   eapply tr_rvalof_nolabel; eauto.
   eapply tr_rvalof_nolabel; eauto.
@@ -1341,10 +1365,12 @@ Proof.
   apply S. apply tr_val_gen. auto. intros. constructor. rewrite H5; auto. apply PTree.gss.
   intros. apply PTree.gso. red; intros; subst; elim H5; auto. 
   auto.
-(* condition true *)
-  exploit tr_top_leftcontext; eauto. clear H9. 
+(* condition *)
+  exploit tr_top_leftcontext; eauto. clear H10. 
   intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
-  inv P. inv H2. 
+  inv P. inv H3. 
+  (* simple *)
+  intuition congruence.
   (* for value *)
   exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
   subst sl0; simpl Kseqlist. destruct b.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index b3efd7f..647e048 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -21,6 +21,7 @@ Require Import Values.
 Require Import Memory.
 Require Import AST.
 Require Import Csyntax.
+Require Cstrategy.
 Require Import Clight.
 Require Import SimplExpr.
 
@@ -117,7 +118,19 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le dst (C.Ecast e1 ty)
                    (sl1 ++ final dst (Ecast a1 ty))
                    (Ecast a1 ty) tmp
+  | tr_condition_simple: forall le dst e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 tmp,
+      Cstrategy.simple e2 = true -> Cstrategy.simple e3 = true ->
+      tr_expr le For_val e1 sl1 a1 tmp1 ->
+      tr_expr le For_val e2 sl2 a2 tmp2 ->
+      tr_expr le For_val e3 sl3 a3 tmp3 ->
+      list_disjoint tmp1 tmp2 ->
+      list_disjoint tmp1 tmp3 ->
+      incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
+      tr_expr le dst (C.Econdition e1 e2 e3 ty)
+                       (sl1 ++ final dst (Econdition a1 a2 a3 ty))
+                       (Econdition a1 a2 a3 ty) tmp
   | tr_condition_val: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp,
+      Cstrategy.simple e2 = false \/ Cstrategy.simple e3 = false ->
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
       tr_expr le For_val e3 sl3 a3 tmp3 ->
@@ -131,6 +144,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
                                 (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil)
                       (Etempvar t ty) tmp
   | tr_condition_effects: forall le dst e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
+      Cstrategy.simple e2 = false \/ Cstrategy.simple e3 = false ->
       dst <> For_val ->
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le (cast_destination ty dst) e2 sl2 a2 tmp2 ->
@@ -671,23 +685,36 @@ Opaque makeif.
   monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. 
   econstructor; split; eauto. constructor; auto.
 (* condition *) 
+  simpl in H2. 
+  destruct (Cstrategy.simple r2 && Cstrategy.simple r3) as []_eqn.
+  (* simple *)
+  monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
+  exploit H0; eauto. intros [tmp2 [C D]].
+  exploit H1; eauto. intros [tmp3 [E F]].
+  UseFinish. destruct (andb_prop _ _ Heqb). 
+  exists (tmp1 ++ tmp2 ++ tmp3); split.
+  intros; eapply tr_condition_simple; eauto with gensym. 
+  apply contained_app. eauto with gensym.
+  apply contained_app; eauto with gensym.
+  (* not simple *)
   monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [C D]].
   exploit H1; eauto. intros [tmp3 [E F]].
+  rewrite andb_false_iff in Heqb.
   destruct dst; monadInv EQ3.
   (* for value *)
   exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split. 
-  econstructor; eauto with gensym.
+  intros; eapply tr_condition_val; eauto with gensym.
   apply contained_cons. eauto with gensym. 
   apply contained_app. eauto with gensym.
   apply contained_app; eauto with gensym.
   (* for effects *)
   exists (tmp1 ++ tmp2 ++ tmp3); split.
-  econstructor; eauto with gensym. congruence.
+  intros; eapply tr_condition_effects; eauto with gensym. congruence.
   apply contained_app; eauto with gensym.
   (* for test *)
   exists (tmp1 ++ tmp2 ++ tmp3); split.
-  econstructor; eauto with gensym. congruence.
+  intros; eapply tr_condition_effects; eauto with gensym. congruence.
   apply contained_app; eauto with gensym.
 (* sizeof *)
   monadInv H. UseFinish.