diff options
| -rw-r--r-- | cfrontend/SimplExpr.v | 5 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 27 | ||||
| -rw-r--r-- | cfrontend/SimplExprspec.v | 7 |
3 files changed, 32 insertions, 7 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 8725edd1..a5306b4b 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -436,7 +436,10 @@ Fixpoint transl_stmt (s: Csyntax.statement) : mon statement := do ts1 <- transl_stmt s1; do ts2 <- transl_stmt s2; do (s', a) <- transl_expression e; - ret (Ssequence s' (Sifthenelse a ts1 ts2)) + if is_Sskip s1 && is_Sskip s2 then + ret (Ssequence s' Sskip) + else + ret (Ssequence s' (Sifthenelse a ts1 ts2)) | Csyntax.Swhile e s1 => do s' <- transl_if e Sskip Sbreak; do ts1 <- transl_stmt s1; 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. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 453a4c9a..e317a728 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -411,6 +411,9 @@ Inductive tr_stmt: Csyntax.statement -> statement -> Prop := | tr_seq: forall s1 s2 ts1 ts2, tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> tr_stmt (Csyntax.Ssequence s1 s2) (Ssequence ts1 ts2) + | tr_ifthenelse_empty: forall r s' a, + tr_expression r s' a -> + tr_stmt (Csyntax.Sifthenelse r Csyntax.Sskip Csyntax.Sskip) (Ssequence s' Sskip) | tr_ifthenelse: forall r s1 s2 s' a ts1 ts2, tr_expression r s' a -> tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> @@ -1058,11 +1061,12 @@ Opaque transl_expression transl_expr_stmt. clear transl_stmt_meets_spec. induction s; simpl; intros until I; intros TR; try (monadInv TR); try (constructor; eauto). + destruct (is_Sskip s1); destruct (is_Sskip s2) eqn:?; monadInv EQ3; try (constructor; eauto). + eapply tr_ifthenelse_empty; eauto. destruct (is_Sskip s1); monadInv EQ4. apply tr_for_1; eauto. apply tr_for_2; eauto. destruct o; monadInv TR; constructor; eauto. - clear transl_lblstmt_meets_spec. induction s; simpl; intros until I; intros TR; monadInv TR; constructor; eauto. @@ -1108,4 +1112,3 @@ Proof. Qed. End SPEC. - |