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/CleanupLabels.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'backend/CleanupLabels.v') diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v index 0ed2be10..8db871e9 100644 --- a/backend/CleanupLabels.v +++ b/backend/CleanupLabels.v @@ -44,17 +44,17 @@ Definition labels_branched_to (c: code) : Labelset.t := (** Remove label declarations for labels that are not in the [bto] (branched-to) set. *) -Fixpoint remove_unused_labels (bto: Labelset.t) (c: code) : code := - match c with - | nil => nil - | Llabel lbl :: c' => - if Labelset.mem lbl bto - then Llabel lbl :: remove_unused_labels bto c' - else remove_unused_labels bto c' - | i :: c' => - i :: remove_unused_labels bto c' +Definition remove_unused (bto: Labelset.t) (i: instruction) (k: code) : code := + match i with + | Llabel lbl => + if Labelset.mem lbl bto then i :: k else k + | _ => + i :: k end. +Definition remove_unused_labels (bto: Labelset.t) (c: code) : code := + list_fold_right (remove_unused bto) c nil. + Definition cleanup_labels (c: code) := remove_unused_labels (labels_branched_to c) c. -- cgit