From 707b6a1ae9660b13cf6f68c7c0ce74017f5981c5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 16 Mar 2013 16:51:42 +0000 Subject: Assorted changes to reduce stack and heap requirements when compiling very big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CleanupLabelsproof.v | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'backend/CleanupLabelsproof.v') diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index dbd33c1..70f0eb3 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -143,6 +143,20 @@ Qed. (** Commutation with [find_label]. *) +Lemma remove_unused_labels_cons: + forall bto i c, + remove_unused_labels bto (i :: c) = + match i with + | Llabel lbl => + if Labelset.mem lbl bto then i :: remove_unused_labels bto c else remove_unused_labels bto c + | _ => + i :: remove_unused_labels bto c + end. +Proof. + unfold remove_unused_labels; intros. rewrite list_fold_right_eq. auto. +Qed. + + Lemma find_label_commut: forall lbl bto, Labelset.In lbl bto -> @@ -152,6 +166,7 @@ Lemma find_label_commut: Proof. induction c; simpl; intros. congruence. + rewrite remove_unused_labels_cons. unfold is_label in H0. destruct a; simpl; auto. destruct (peq lbl l). subst l. inv H0. rewrite Labelset.mem_1; auto. @@ -222,7 +237,7 @@ Theorem transf_step_correct: (exists s2', step tge s1' t s2' /\ match_states s2 s2') \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. Proof. - induction 1; intros; inv MS; simpl. + induction 1; intros; inv MS; try rewrite remove_unused_labels_cons. (* Lop *) left; econstructor; split. econstructor; eauto. instantiate (1 := v). rewrite <- H. @@ -263,7 +278,7 @@ Proof. constructor. econstructor; eauto with coqlib. (* eliminated *) - right. split. omega. split. auto. econstructor; eauto with coqlib. + right. split. simpl. omega. split. auto. econstructor; eauto with coqlib. (* Lgoto *) left; econstructor; split. econstructor. eapply find_label_translated; eauto. red; auto. -- cgit v1.2.3