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, 2 insertions, 96 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 4a4c219..caaf09d 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -21,107 +21,13 @@ Require Import Op.
 Require Import Registers.
 Require Import RTL.
 Require Import RTLtyping.
-Require Import Kildall.
+Require Import Liveness.
 Require Import Locations.
+Require Import LTL.
 Require Import Coloring.
 
-(** * Liveness analysis over RTL *)
-
-(** A register [r] is live at a point [p] if there exists a path
-  from [p] to some instruction that uses [r] as argument,
-  and [r] is not redefined along this path.
-  Liveness can be computed by a backward dataflow analysis.
-  The analysis operates over sets of (live) pseudo-registers. *)
-
-Notation reg_live := Regset.add.
-Notation reg_dead := Regset.remove.
-
-Definition reg_option_live (or: option reg) (lv: Regset.t) :=
-  match or with None => lv | Some r => reg_live r lv end.
-
-Definition reg_sum_live (ros: reg + ident) (lv: Regset.t) :=
-  match ros with inl r => reg_live r lv | inr s => lv end.
-
-Fixpoint reg_list_live
-             (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t :=
-  match rl with
-  | nil => lv
-  | r1 :: rs => reg_list_live rs (reg_live r1 lv)
-  end.
-
-Fixpoint reg_list_dead
-             (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t :=
-  match rl with
-  | nil => lv
-  | r1 :: rs => reg_list_dead rs (reg_dead r1 lv)
-  end.
-
-(** Here is the transfer function for the dataflow analysis.
-  Since this is a backward dataflow analysis, it takes as argument
-  the abstract register set ``after'' the given instruction,
-  i.e. the registers that are live after; and it returns as result
-  the abstract register set ``before'' the given instruction,
-  i.e. the registers that must be live before.
-  The general relation between ``live before'' and ``live after''
-  an instruction is that a register is live before if either
-  it is one of the arguments of the instruction, or it is not the result
-  of the instruction and it is live after.
-  However, if the result of a side-effect-free instruction is not 
-  live ``after'', the whole instruction will be removed later
-  (since it computes a useless result), thus its arguments need not
-  be live ``before''. *)
-
-Definition transfer
-            (f: RTL.function) (pc: node) (after: Regset.t) : Regset.t :=
-  match f.(fn_code)!pc with
-  | None =>
-      Regset.empty
-  | Some i =>
-      match i with
-      | Inop s =>
-          after
-      | Iop op args res s =>
-          if Regset.mem res after then
-            reg_list_live args (reg_dead res after)
-          else
-            after
-      | Iload chunk addr args dst s =>
-          if Regset.mem dst after then
-            reg_list_live args (reg_dead dst after)
-          else
-            after
-      | Istore chunk addr args src s =>
-          reg_list_live args (reg_live src after)
-      | Icall sig ros args res s =>
-          reg_list_live args
-           (reg_sum_live ros (reg_dead res after))
-      | Itailcall sig ros args =>
-          reg_list_live args (reg_sum_live ros Regset.empty)
-      | Ibuiltin ef args res s =>
-          reg_list_live args (reg_dead res after)
-      | Icond cond args ifso ifnot =>
-          reg_list_live args after
-      | Ijumptable arg tbl =>
-          reg_live arg after
-      | Ireturn optarg =>
-          reg_option_live optarg Regset.empty
-      end
-  end.
-
-(** The liveness analysis is then obtained by instantiating the
-  general framework for backward dataflow analysis provided by
-  module [Kildall].  *)
-
-Module RegsetLat := LFSet(Regset).
-Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).
-
-Definition analyze (f: RTL.function): option (PMap.t Regset.t) :=
-  DS.fixpoint (successors f)  (transfer f) nil.
-
 (** * Translation from RTL to LTL *)
 
-Require Import LTL.
-
 (** Each [RTL] instruction translates to an [LTL] instruction.
   The register assignment [assign] returned by register allocation
   is applied to the arguments and results of the RTL