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, 14 deletions

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.