diff options
| -rw-r--r-- | backend/Selection.v | 6 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 17 |
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. |