diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-25 10:42:34 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-25 10:42:34 +0000 |
commit | 65cc3738e7436e46f70c0508638a71fbb49c50a8 (patch) | |
tree | dacf1cc0a9c431dca55461d516fbd12a991d107a /cfrontend/SimplExprspec.v | |
parent | 62316a8e94d8cdcbf9e7aeadd1caf8e29507e6b0 (diff) |
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
Diffstat (limited to 'cfrontend/SimplExprspec.v')
-rw-r--r-- | cfrontend/SimplExprspec.v | 33 |
1 files changed, 30 insertions, 3 deletions
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. |