diff options
Diffstat (limited to 'cfrontend/Cshmgen.v')
-rw-r--r-- | cfrontend/Cshmgen.v | 25 |
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]. |