From b6a2f5a9177892fa325e35a845c593902f6f203e Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 15 Mar 2011 12:41:22 +0000 Subject: Special case for while(1), for(..., 1, ...) and do ... while(0) loops. Don't wait until Constprop to get rid of trivial loop tests; instead, produces better-looking Cminor. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1610 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index a54bfcb1..87dfc877 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -425,14 +425,29 @@ Fixpoint transl_exprlist (al: list Clight.expr) (tyl: typelist) (** [exit_if_false e] return the statement that tests the boolean value of the Clight expression [e]. If [e] evaluates to false, an [exit 0] is performed. If [e] evaluates to true, the generated - statement continues in sequence. *) + statement continues in sequence. + + The Clight code generated by [SimplExpr] contains many [while(1)] + and [for(;1;...)] loops, so we optimize the case where [e] is a constant. + *) + +Definition is_constant_bool (e: expr) : option bool := + match e with + | Econst (Ointconst n) => Some (negb (Int.eq n Int.zero)) + | _ => None + end. Definition exit_if_false (e: Clight.expr) : res stmt := do te <- transl_expr e; - OK(Sifthenelse - (make_boolean te (typeof e)) - Sskip - (Sexit 0%nat)). + match is_constant_bool te with + | Some true => OK(Sskip) + | Some false => OK(Sexit 0%nat) + | None => + OK(Sifthenelse + (make_boolean te (typeof e)) + Sskip + (Sexit 0%nat)) + end. (** [transl_statement nbrk ncnt s] returns a Csharpminor statement that performs the same computations as the CabsCoq statement [s]. -- cgit