diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-03-21 15:22:46 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-04-06 15:16:11 +0200 |
| commit | 6ce07727bcf4e330f897d9461a924334a0f0980e (patch) | |
| tree | 96550377c581d69a61f89069175497dbe7cf725d /cfrontend/SimplExprproof.v | |
| parent | 8d4562d4d3bebb9c62374beaf39d8327acdc647d (diff) | |
| download | compcert-kvx-6ce07727bcf4e330f897d9461a924334a0f0980e.tar.gz compcert-kvx-6ce07727bcf4e330f897d9461a924334a0f0980e.zip | |
attempt to optimize empty if/then/else statements
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 27 |
1 files changed, 23 insertions, 4 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index ad7b296a..191a10de 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -941,6 +941,9 @@ with match_cont_exp : destination -> expr -> Csem.cont -> cont -> Prop := | match_Kdo: forall k a tk, match_cont k tk -> match_cont_exp For_effects a (Csem.Kdo k) tk + | match_Kifthenelse_empty: forall a k tk, + match_cont k tk -> + match_cont_exp For_val a (Csem.Kifthenelse Csyntax.Sskip Csyntax.Sskip k) (Kseq Sskip tk) | match_Kifthenelse_1: forall a s1 s2 k ts1 ts2 tk, tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> match_cont k tk -> @@ -1226,7 +1229,11 @@ Proof. destruct (Csem.find_label lbl s1 (Csem.Kseq s2 k)) as [[s' k'] | ]. intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; auto. intro EQ. rewrite EQ. eapply IHs2; eauto. -(* if *) +(* if empty *) + rename s' into sr. + rewrite (tr_find_label_expression _ _ _ H3). + auto. +(* if not empty *) rename s' into sr. rewrite (tr_find_label_expression _ _ _ H2). exploit (IHs1 k); eauto. @@ -1986,21 +1993,33 @@ Proof. inv H6; inv H7. econstructor; split. left. apply plus_one; constructor. econstructor; eauto. constructor. - (* ifthenelse *) inv H6. +(* ifthenelse empty *) + inv H3. econstructor; split. + left. eapply plus_left. constructor. apply push_seq. + econstructor; eauto. + econstructor; eauto. + econstructor; eauto. +(* ifthenelse non empty *) inv H2. econstructor; split. left. eapply plus_left. constructor. apply push_seq. traceEq. econstructor; eauto. econstructor; eauto. - (* ifthenelse *) inv H8. +(* ifthenelse empty *) + exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. + econstructor; split; simpl. + right. destruct b; econstructor; eauto. + eapply star_left. apply step_skip_seq. econstructor. traceEq. + eapply star_left. apply step_skip_seq. econstructor. traceEq. + destruct b; econstructor; eauto. econstructor; eauto. econstructor; eauto. + (* ifthenelse non empty *) exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left. eapply plus_two. constructor. apply step_ifthenelse with (v1 := v) (b := b); auto. traceEq. destruct b; econstructor; eauto. - (* while *) inv H6. inv H1. econstructor; split. left. eapply plus_left. constructor. |