diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-13 09:00:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-13 09:00:12 +0200 |
| commit | 1915258c8b2cd2e171bbce93658047a765232bc9 (patch) | |
| tree | 2f4e5d6acf77a0bc30c9816394a65f868c39a6c0 /cfrontend/SimplExprproof.v | |
| parent | 8d2a0c12b27e82c67acc2693ecd6f1e2fede3b88 (diff) | |
| download | compcert-kvx-1915258c8b2cd2e171bbce93658047a765232bc9.tar.gz compcert-kvx-1915258c8b2cd2e171bbce93658047a765232bc9.zip | |
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.
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 18 |
1 files changed, 8 insertions, 10 deletions
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. |