diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cshmgen.v | 25 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 66 |
2 files changed, 69 insertions, 22 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]. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 88f042de..3f6aa62e 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1157,19 +1157,46 @@ Qed. End EXPR. +Lemma is_constant_bool_true: + forall te le m a v ty, + Csharpminor.eval_expr tge te le m a v -> + is_true v ty -> + is_constant_bool a <> Some false. +Proof. + intros. unfold is_constant_bool. destruct a; try congruence. destruct c; try congruence. + inv H. simpl in H2. inv H2. rewrite Int.eq_false. simpl; congruence. + inv H0; auto. +Qed. + +Lemma is_constant_bool_false: + forall te le m a v ty, + Csharpminor.eval_expr tge te le m a v -> + is_false v ty -> + is_constant_bool a <> Some true. +Proof. + intros. unfold is_constant_bool. destruct a; try congruence. destruct c; try congruence. + inv H. simpl in H2. inv H2. + assert (i = Int.zero). inv H0; auto. + subst i. simpl. congruence. +Qed. + Lemma exit_if_false_true: forall a ts e le m v te f tk, exit_if_false a = OK ts -> Clight.eval_expr ge e le m a v -> is_true v (typeof a) -> match_env e te -> - step tge (State f ts tk te le m) E0 (State f Sskip tk te le m). + star step tge (State f ts tk te le m) E0 (State f Sskip tk te le m). Proof. intros. monadInv H. - exploit make_boolean_correct_true. - eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. - eauto. - intros [vb [EVAL ISTRUE]]. + exploit transl_expr_correct; eauto. intros EV. + generalize (is_constant_bool_true _ _ _ _ _ _ EV H1); intros ICB. + destruct (is_constant_bool x). destruct b. + inv EQ0. apply star_refl. + congruence. + inv EQ0. + exploit make_boolean_correct_true; eauto. intros [vb [EVAL ISTRUE]]. + apply star_one. change Sskip with (if true then Sskip else Sexit 0). eapply step_ifthenelse; eauto. apply Val.bool_of_true_val; eauto. @@ -1181,13 +1208,17 @@ Lemma exit_if_false_false: Clight.eval_expr ge e le m a v -> is_false v (typeof a) -> match_env e te -> - step tge (State f ts tk te le m) E0 (State f (Sexit 0) tk te le m). + star step tge (State f ts tk te le m) E0 (State f (Sexit 0) tk te le m). Proof. intros. monadInv H. - exploit make_boolean_correct_false. - eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. - eauto. - intros [vb [EVAL ISFALSE]]. + exploit transl_expr_correct; eauto. intros EV. + generalize (is_constant_bool_false _ _ _ _ _ _ EV H1); intros ICB. + destruct (is_constant_bool x). destruct b. + congruence. + inv EQ0. apply star_refl. + inv EQ0. + exploit make_boolean_correct_false; eauto. intros [vb [EVAL ISFALSE]]. + apply star_one. change (Sexit 0) with (if false then Sskip else Sexit 0). eapply step_ifthenelse; eauto. apply Val.bool_of_false_val; eauto. @@ -1322,7 +1353,8 @@ Variable tyret: type. Remark exit_if_false_no_label: forall a s, exit_if_false a = OK s -> forall k, find_label lbl s k = None. Proof. - intros. unfold exit_if_false in H. monadInv H. simpl. auto. + intros. unfold exit_if_false in H. monadInv H. + destruct (is_constant_bool x). destruct b; inv EQ0; auto. inv EQ0; auto. Qed. Lemma transl_find_label: @@ -1549,7 +1581,7 @@ Proof. eapply star_plus_trans. eapply match_transl_step; eauto. eapply plus_left. constructor. eapply star_left. constructor. - eapply star_left. eapply exit_if_false_false; eauto. + eapply star_trans. eapply exit_if_false_false; eauto. eapply star_left. constructor. eapply star_left. constructor. apply star_one. constructor. @@ -1562,7 +1594,7 @@ Proof. eapply star_plus_trans. eapply match_transl_step; eauto. eapply plus_left. constructor. eapply star_left. constructor. - eapply star_left. eapply exit_if_false_true; eauto. + eapply star_trans. eapply exit_if_false_true; eauto. eapply star_left. constructor. apply star_one. constructor. reflexivity. reflexivity. reflexivity. reflexivity. traceEq. @@ -1608,7 +1640,7 @@ Proof. econstructor; split. eapply plus_left. destruct H2; subst ts'; constructor. eapply star_left. constructor. - eapply star_left. eapply exit_if_false_false; eauto. + eapply star_trans. eapply exit_if_false_false; eauto. eapply star_left. constructor. apply star_one. constructor. reflexivity. reflexivity. reflexivity. traceEq. @@ -1621,7 +1653,7 @@ Proof. econstructor; split. eapply plus_left. destruct H2; subst ts'; constructor. eapply star_left. constructor. - eapply star_left. eapply exit_if_false_true; eauto. + eapply star_trans. eapply exit_if_false_true; eauto. apply star_one. constructor. reflexivity. reflexivity. traceEq. econstructor; eauto. @@ -1643,7 +1675,7 @@ Proof. eapply star_plus_trans. eapply match_transl_step; eauto. eapply plus_left. constructor. eapply star_left. constructor. - eapply star_left. eapply exit_if_false_false; eauto. + eapply star_trans. eapply exit_if_false_false; eauto. eapply star_left. constructor. eapply star_left. constructor. apply star_one. constructor. @@ -1656,7 +1688,7 @@ Proof. eapply star_plus_trans. eapply match_transl_step; eauto. eapply plus_left. constructor. eapply star_left. constructor. - eapply star_left. eapply exit_if_false_true; eauto. + eapply star_trans. eapply exit_if_false_true; eauto. eapply star_left. constructor. eapply star_left. constructor. apply star_one. constructor. |