Inlining: preserve all RTL regs mentioned in the function, not just

those defined in the function.  Semantically, both are correct, but the latter may cause RTLtyping to fail if some regs are uninitialized and a collision occurs between regs of different types.
RTL: move the function resource computations there, as it could be useful for other passes some day.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2440 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 3 insertions, 29 deletions

diff --git a/backend/Inlining.v b/backend/Inlining.v
index c6df3de0..cd347345 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -48,32 +48,6 @@ Definition add_globdef (fenv: funenv) (idg: ident * globdef fundef unit) : funen
 Definition funenv_program (p: program) : funenv :=
   List.fold_left add_globdef p.(prog_defs) (PTree.empty function).
 
-(** Resources used by a function. *)
-
-(** Maximum PC (node number) in the CFG of a function.  All nodes of
-  the CFG of [f] are between 1 and [max_pc_function f] (inclusive). *)
-
-Definition max_pc_function (f: function) :=
-  PTree.fold (fun m pc i => Pmax m pc) f.(fn_code) 1%positive.
-
-(** Maximum pseudo-register defined in a function.  All results of
-  an instruction of [f], as well as all parameters of [f], are between
-  1 and [max_def_function] (inclusive). *)
-
-Definition max_def_instr (i: instruction) :=
-  match i with
-  | Iop op args res s => res
-  | Iload chunk addr args dst s => dst
-  | Icall sg ros args res s => res
-  | Ibuiltin ef args res s => res
-  | _ => 1%positive
-  end.
-
-Definition max_def_function (f: function) :=
-  Pmax
-    (PTree.fold (fun m pc i => Pmax m (max_def_instr i)) f.(fn_code) 1%positive)
-    (List.fold_left (fun m r => Pmax m r) f.(fn_params) 1%positive).
-
 (** State monad *)
 
 (** To construct incrementally the CFG of a function after inlining,
@@ -319,7 +293,7 @@ Definition inline_function (ctx: context) (id: ident) (f: function)
                            (args: list reg)
                            (retpc: node) (retreg: reg) : mon node :=
   let npc := max_pc_function f in
-  let nreg := max_def_function f in
+  let nreg := max_reg_function f in
   do dpc <- reserve_nodes npc;
   do dreg <- reserve_regs nreg;
   let ctx' := callcontext ctx dpc dreg nreg f.(fn_stacksize) retpc retreg in 
@@ -333,7 +307,7 @@ Definition inline_tail_function (ctx: context) (id: ident) (f: function)
                                (P: PTree.get id fenv = Some f)
                                (args: list reg): mon node :=
   let npc := max_pc_function f in
-  let nreg := max_def_function f in
+  let nreg := max_reg_function f in
   do dpc <- reserve_nodes npc;
   do dreg <- reserve_regs nreg;
   let ctx' := tailcontext ctx dpc dreg nreg f.(fn_stacksize) in 
@@ -442,7 +416,7 @@ Definition expand_cfg := Fixm size_fenv expand_cfg_rec.
 
 Definition expand_function (fenv: funenv) (f: function): mon context :=
   let npc := max_pc_function f in
-  let nreg := max_def_function f in
+  let nreg := max_reg_function f in
   do dpc <- reserve_nodes npc;
   do dreg <- reserve_regs nreg;
   let ctx := initcontext dpc dreg nreg f.(fn_stacksize) in