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

1 files changed, 20 insertions, 5 deletions

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].