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/SimplExprspec.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/SimplExprspec.v')
| -rw-r--r-- | cfrontend/SimplExprspec.v | 7 |
1 files changed, 5 insertions, 2 deletions
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. - |