Ignore self assign in if-conversion

A self assign `x = x` can be classified as a skip in `classify_stmt`.
This helps with the if-conversion of some code that the previous passes
generates, e.g. for nested C conditional expressions.

Closes: #466

2 files changed, 19 insertions, 4 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index ca1f1619..e4be867f 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -348,7 +348,11 @@ Inductive stmt_class : Type :=
 Fixpoint classify_stmt (s: Cminor.stmt) : stmt_class :=
   match s with
   | Cminor.Sskip => SCskip
-  | Cminor.Sassign id a => SCassign id a
+  | Cminor.Sassign id a =>
+      match a with
+      | Cminor.Evar id2 => if ident_eq id id2 then SCskip else SCassign id a
+      | _ =>  SCassign id a
+      end
   | Cminor.Sbuiltin None (EF_debug _ _ _) _ => SCskip
   | Cminor.Sseq s1 s2 =>
       match classify_stmt s1, classify_stmt s2 with
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 5aeceb6b..acd7b7a4 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -918,8 +918,19 @@ Proof.
 - (* skip *)
   exists O; intros. constructor; auto.
 - (* assign *)
-  exists 1%nat; intros. apply eventually_step; intros. inv H0.
-  assert (v0 = v) by eauto using eval_expr_determ. subst v0.
+  assert (BASE:
+           exists n : nat,
+           forall (f : Cminor.function) (k : Cminor.cont) (sp : val) (e0 : env) (m : mem) (v : val),
+           Cminor.eval_expr ge sp e0 m e v ->
+           eventually n (Cminor.State f (Cminor.Sassign i e) k sp e0 m) (eq (Cminor.State f Cminor.Sskip k sp (PTree.set i v e0) m))).
+  {
+    exists 1%nat; intros. apply eventually_step; intros. inv H0.
+    assert (v0 = v) by eauto using eval_expr_determ. subst v0.
+    split; auto. apply eventually_now. auto.
+  }
+  destruct e; try destruct (ident_eq i i0); auto.
+  exists 1%nat. intros. apply eventually_step; intros. inv H.
+  rewrite PTree.gsident by (inv H9; auto).
   split; auto. apply eventually_now. auto.
 - (* builtin *)
   destruct o; auto. destruct e; auto. 
@@ -950,7 +961,7 @@ Lemma classify_stmt_wt:
   wt_expr env a (env id).
 Proof.
   induction s; simpl; intros CL WT; try discriminate.
-- inv CL; inv WT; auto.
+- destruct e; try destruct (ident_eq i i0); inv CL; inv WT; auto.
 - destruct o; try discriminate. destruct e; discriminate.
 - inv WT. destruct (classify_stmt s1), (classify_stmt s2); try discriminate; eauto.
 Qed.