From 6ce07727bcf4e330f897d9461a924334a0f0980e Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Tue, 21 Mar 2017 15:22:46 +0100
Subject: attempt to optimize empty if/then/else statements

---
 cfrontend/SimplExpr.v      |  5 ++++-
 cfrontend/SimplExprproof.v | 27 +++++++++++++++++++++++----
 cfrontend/SimplExprspec.v  |  7 +++++--
 3 files changed, 32 insertions(+), 7 deletions(-)

(limited to 'cfrontend')

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.
-
-- 
cgit