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/Linearizeproof.v | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) (limited to 'backend/Linearizeproof.v') diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index b72268a6..d3683110 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -293,6 +293,18 @@ Proof. case (starts_with n k); simpl; auto. Qed. +Remark linearize_body_cons: + forall f pc enum, + linearize_body f (pc :: enum) = + match f.(LTL.fn_code)!pc with + | None => linearize_body f enum + | Some b => Llabel pc :: linearize_instr b (linearize_body f enum) + end. +Proof. + intros. unfold linearize_body. rewrite list_fold_right_eq. + unfold linearize_node. destruct (LTL.fn_code f)!pc; auto. +Qed. + Lemma find_label_lin_rec: forall f enum pc b, In pc enum -> @@ -301,12 +313,13 @@ Lemma find_label_lin_rec: Proof. induction enum; intros. elim H. - case (peq a pc); intro. + rewrite linearize_body_cons. + destruct (peq a pc). subst a. exists (linearize_body f enum). - simpl. rewrite H0. simpl. rewrite peq_true. auto. + rewrite H0. simpl. rewrite peq_true. auto. assert (In pc enum). simpl in H. tauto. - elim (IHenum pc b H1 H0). intros k FIND. - exists k. simpl. destruct (LTL.fn_code f)!a. + destruct (IHenum pc b H1 H0) as [k FIND]. + exists k. destruct (LTL.fn_code f)!a. simpl. rewrite peq_false. rewrite find_label_lin_instr. auto. auto. auto. Qed. @@ -377,7 +390,7 @@ Lemma label_in_lin_rec: Proof. induction enum. simpl; auto. - simpl. destruct (LTL.fn_code f)!a. + rewrite linearize_body_cons. destruct (LTL.fn_code f)!a. simpl. intros [A|B]. left; congruence. right. apply IHenum. eapply label_in_lin_instr; eauto. intro; right; auto. @@ -406,7 +419,8 @@ Lemma unique_labels_lin_rec: Proof. induction enum. simpl; auto. - intro. simpl. destruct (LTL.fn_code f)!a. + rewrite linearize_body_cons. + intro. destruct (LTL.fn_code f)!a. simpl. split. red. intro. inversion H. elim H3. apply label_in_lin_rec with f. apply label_in_lin_instr with i. auto. -- cgit