From 65cc3738e7436e46f70c0508638a71fbb49c50a8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 25 Feb 2012 10:42:34 +0000 Subject: 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 --- cfrontend/SimplExpr.v | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) (limited to 'cfrontend/SimplExpr.v') 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; -- cgit