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, 15 insertions, 1 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index 2f3123f3..f85405d6 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -24,6 +24,7 @@ Require Import Registers.
 Require Import RTL.
 Require Import Lattice.
 Require Import Kildall.
+Require Import Liveness.
 Require Import ConstpropOp.
 
 (** * Static analysis *)
@@ -211,6 +212,18 @@ Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t)
       end
   end.
 
+(** To reduce the size of approximations, we preventively set to [Top]
+  the approximations of registers used for the last time in the
+  current instruction. *)
+
+Definition transfer' (gapp: global_approx) (f: function) (lastuses: PTree.t (list reg))
+                     (pc: node) (before: D.t) :=
+  let after := transfer gapp f pc before in
+  match lastuses!pc with
+  | None => after
+  | Some regs => List.fold_left (fun a r => D.set r Unknown a) regs after
+  end.
+
 (** The static analysis itself is then an instantiation of Kildall's
   generic solver for forward dataflow inequations. [analyze f]
   returns a mapping from program points to mappings of pseudo-registers
@@ -221,7 +234,8 @@ Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t)
 Module DS := Dataflow_Solver(D)(NodeSetForward).
 
 Definition analyze (gapp: global_approx) (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) (transfer gapp f) 
+  let lu := Liveness.last_uses f in
+  match DS.fixpoint (successors f) (transfer' gapp f lu) 
                     ((f.(fn_entrypoint), D.top) :: nil) with
   | None => PMap.init D.top
   | Some res => res