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.

1 files changed, 14 insertions, 16 deletions

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.