From 6ce07727bcf4e330f897d9461a924334a0f0980e Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Tue, 21 Mar 2017 15:22:46 +0100 Subject: attempt to optimize empty if/then/else statements --- cfrontend/SimplExprproof.v | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) (limited to 'cfrontend/SimplExprproof.v') 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. -- cgit