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

1 files changed, 7 insertions, 9 deletions

diff --git a/backend/Linearize.v b/backend/Linearize.v
index 636cb224..6fc8e489 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -198,17 +198,15 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code :=
 
 (** Linearize a function body according to an enumeration of its nodes.  *)
 
-Fixpoint linearize_body (f: LTL.function) (enum: list node)
-                        {struct enum} : code :=
-  match enum with
-  | nil => nil
-  | pc :: rem =>
-      match f.(LTL.fn_code)!pc with
-      | None => linearize_body f rem
-      | Some b => Llabel pc :: linearize_instr b (linearize_body f rem)
-      end
+Definition linearize_node (f: LTL.function) (pc: node) (k: code) : code :=
+  match f.(LTL.fn_code)!pc with
+  | None => k
+  | Some b => Llabel pc :: linearize_instr b k
   end.
 
+Definition linearize_body (f: LTL.function) (enum: list node) : code :=
+  list_fold_right (linearize_node f) enum nil.
+
 (** * Entry points for code linearization *)
 
 Definition transf_function (f: LTL.function) : res LTLin.function :=