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, 147 insertions, 0 deletions

diff --git a/backend/Liveness.v b/backend/Liveness.v
new file mode 100644
index 0000000..b97455f
--- /dev/null
+++ b/backend/Liveness.v
@@ -0,0 +1,147 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Liveness analysis over RTL *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Lattice.
+Require Import AST.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Kildall.
+
+(** 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: 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: function): option (PMap.t Regset.t) :=
+  DS.fixpoint (successors f)  (transfer f) nil.
+
+(** Basic property of the liveness information computed by [analyze]. *)
+
+Lemma analyze_solution:
+  forall f live n i s,
+  analyze f = Some live ->
+  f.(fn_code)!n = Some i ->
+  In s (successors_instr i) ->
+  Regset.Subset (transfer f s live!!s) live!!n.
+Proof.
+  unfold analyze; intros. eapply DS.fixpoint_solution; eauto. 
+  unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. simpl. auto.
+Qed.
+
+(** Given an RTL function, compute (for every PC) the list of 
+  pseudo-registers that are used for the last time in the instruction
+  at PC.  These are the registers that are used or defined by the instruction
+  and dead afterwards.  *)
+
+Definition last_uses_at (live: PMap.t Regset.t) (pc: node) (i: instruction) : list reg :=
+  let l := live!!pc in
+  let lu := List.filter (fun r => negb (Regset.mem r l)) (instr_uses i) in
+  match instr_defs i with
+  | None => lu
+  | Some r => if Regset.mem r l then lu else r :: lu
+  end.
+
+Definition last_uses (f: function) : PTree.t (list reg) :=
+  match analyze f with
+  | None => PTree.empty (list reg)
+  | Some live => PTree.map (last_uses_at live) f.(fn_code)
+  end.
+
+