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/SimplExpr.v | |
parent | 62316a8e94d8cdcbf9e7aeadd1caf8e29507e6b0 (diff) | |
download | compcert-65cc3738e7436e46f70c0508638a71fbb49c50a8.tar.gz compcert-65cc3738e7436e46f70c0508638a71fbb49c50a8.zip |
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/SimplExpr.v')
-rw-r--r-- | cfrontend/SimplExpr.v | 33 |
1 files changed, 20 insertions, 13 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 1dae78cc..7b37692a 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; |