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

3 files changed, 164 insertions, 107 deletions

diff --git a/backend/Inlining.v b/backend/Inlining.v
index c6df3de..cd34734 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 
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index 0fc4613..b5948a2 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -72,61 +72,6 @@ Proof.
   apply H. red; intros. rewrite PTree.gempty in H0; discriminate.
 Qed.
 
-(** ** Soundness of the computed bounds over function resources *)
-
-Remark Pmax_l: forall x y, Ple x (Pmax x y).
-Proof. intros; xomega. Qed.
-
-Remark Pmax_r: forall x y, Ple y (Pmax x y).
-Proof. intros; xomega. Qed.
-
-Lemma max_pc_function_sound:
-  forall f pc i, f.(fn_code)!pc = Some i -> Ple pc (max_pc_function f).
-Proof.
-  intros until i. unfold max_pc_function. 
-  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
-  (* extensionality *)
-  intros. apply H0. rewrite H; auto. 
-  (* base case *)
-  rewrite PTree.gempty. congruence.
-  (* inductive case *)
-  intros. rewrite PTree.gsspec in H2. destruct (peq pc k). 
-  inv H2. apply Pmax_r.
-  apply Ple_trans with a. auto. apply Pmax_l.
-Qed.
-
-Lemma max_def_function_instr:
-  forall f pc i, f.(fn_code)!pc = Some i -> Ple (max_def_instr i) (max_def_function f).
-Proof.
-  intros. unfold max_def_function. eapply Ple_trans. 2: eapply Pmax_l. 
-  revert H. 
-  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple (max_def_instr i) m).
-  (* extensionality *)
-  intros. apply H0. rewrite H; auto. 
-  (* base case *)
-  rewrite PTree.gempty. congruence.
-  (* inductive case *)
-  intros. rewrite PTree.gsspec in H2. destruct (peq pc k). 
-  inv H2. apply Pmax_r. 
-  apply Ple_trans with a. auto. apply Pmax_l.
-Qed.
-
-Lemma max_def_function_params:
-  forall f r, In r f.(fn_params) -> Ple r (max_def_function f).
-Proof.
-  assert (A: forall l m, Ple m (fold_left (fun m r => Pmax m r) l m)).
-    induction l; simpl; intros. 
-    apply Ple_refl.
-    eapply Ple_trans. 2: eauto. apply Pmax_l.
-  assert (B: forall l m r, In r l -> Ple r (fold_left (fun m r => Pmax m r) l m)).
-    induction l; simpl; intros.
-    contradiction.
-    destruct H. subst a. eapply Ple_trans. 2: eapply A. apply Pmax_r. 
-    eauto. 
-  unfold max_def_function; intros. 
-  eapply Ple_trans. 2: eapply Pmax_r. eauto. 
-Qed.
-
 (** ** Properties of shifting *)
 
 Lemma shiftpos_eq: forall x y, Zpos (shiftpos x y) = (Zpos x + Zpos y) - 1.
@@ -509,7 +454,7 @@ Hypothesis rec_spec:
   rec fe' L ctx f s = R x s' i ->
   fenv_agree fe' ->
   Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
-  ctx.(mreg) = max_def_function f ->
+  ctx.(mreg) = max_reg_function f ->
   Ple (Pplus ctx.(dreg) ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> 
   ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
@@ -535,7 +480,7 @@ Ltac inv_incr :=
 Lemma expand_instr_spec:
   forall ctx pc instr s x s' i c,
   expand_instr fe rec ctx pc instr s = R x s' i ->
-  Ple (max_def_instr instr) ctx.(mreg) ->
+  (forall r, instr_defs instr = Some r -> Ple r ctx.(mreg)) ->
   Plt (spc ctx pc) s.(st_nextnode) ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 ->
@@ -555,7 +500,7 @@ Proof.
   (* inlined *)
   subst s1.
   monadInv EXP. unfold inline_function in EQ; monadInv EQ.
-  set (ctx' := callcontext ctx x1 x2 (max_def_function f) (fn_stacksize f) n r).
+  set (ctx' := callcontext ctx x1 x2 (max_reg_function f) (fn_stacksize f) n r).
   inversion EQ0; inversion EQ1; inversion EQ. inv_incr. 
   apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto.
   eapply BASE; eauto. 
@@ -586,7 +531,7 @@ Proof.
   (* inlined *)
   subst s1.
   monadInv EXP. unfold inline_function in EQ; monadInv EQ.
-  set (ctx' := tailcontext ctx x1 x2 (max_def_function f) (fn_stacksize f)) in *.
+  set (ctx' := tailcontext ctx x1 x2 (max_reg_function f) (fn_stacksize f)) in *.
   inversion EQ0; inversion EQ1; inversion EQ. inv_incr. 
   apply tr_tailcall_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto.
   eapply BASE; eauto. 
@@ -618,7 +563,7 @@ Lemma iter_expand_instr_spec:
   forall ctx l s x s' i c,
   mlist_iter2 (expand_instr fe rec ctx) l s = R x s' i ->
   list_norepet (List.map (@fst _ _) l) ->
-  (forall pc instr, In (pc, instr) l -> Ple (max_def_instr instr) ctx.(mreg)) ->
+  (forall pc instr r, In (pc, instr) l -> instr_defs instr = Some r -> Ple r ctx.(mreg)) ->
   (forall pc instr, In (pc, instr) l -> Plt (spc ctx pc) s.(st_nextnode)) ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 ->
@@ -665,7 +610,7 @@ Lemma expand_cfg_rec_spec:
   forall ctx f s x s' i c,
   expand_cfg_rec fe rec ctx f s = R x s' i ->
   Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
-  ctx.(mreg) = max_def_function f ->
+  ctx.(mreg) = max_reg_function f ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> 
   ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
@@ -677,11 +622,11 @@ Lemma expand_cfg_rec_spec:
 Proof.
   intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. 
   constructor. 
-  intros. rewrite H1. eapply max_def_function_params; eauto. 
+  intros. rewrite H1. eapply max_reg_function_params; eauto. 
   intros. exploit ptree_mfold_spec; eauto. intros [INCR' ITER].
   eapply iter_expand_instr_spec; eauto. 
     apply PTree.elements_keys_norepet. 
-    intros. rewrite H1. eapply max_def_function_instr; eauto. 
+    intros. rewrite H1. eapply max_reg_function_def with (i := instr); eauto. 
     eapply PTree.elements_complete; eauto.
   intros.
     assert (Ple pc0 (max_pc_function f)).
@@ -718,7 +663,7 @@ Lemma expand_cfg_spec:
   expand_cfg fe ctx f s = R x s' i ->
   fenv_agree fe ->  
   Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
-  ctx.(mreg) = max_def_function f ->
+  ctx.(mreg) = max_reg_function f ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> 
   ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
@@ -756,7 +701,7 @@ Proof.
   intros. unfold transf_function in H.
   destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. 
   destruct (zlt (st_stksize s) Int.max_unsigned); inv H.
-  monadInv Heqr. set (ctx := initcontext x x0 (max_def_function f) (fn_stacksize f)) in *.
+  monadInv Heqr. set (ctx := initcontext x x0 (max_reg_function f) (fn_stacksize f)) in *.
 Opaque initstate.
   destruct INCR3. inversion EQ1. inversion EQ.
   apply tr_function_intro with ctx; auto.
diff --git a/backend/RTL.v b/backend/RTL.v
index 045250d..e8ec139 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -367,6 +367,24 @@ Qed.
 
 (** * Operations on RTL abstract syntax *)
 
+(** Transformation of a RTL function instruction by instruction.
+  This applies a given transformation function to all instructions
+  of a function and constructs a transformed function from that. *)
+
+Section TRANSF.
+
+Variable transf: node -> instruction -> instruction.
+
+Definition transf_function (f: function) : function :=
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (PTree.map transf f.(fn_code))
+    f.(fn_entrypoint).
+
+End TRANSF.
+
 (** Computation of the possible successors of an instruction.
   This is used in particular for dataflow analyses. *)
 
@@ -422,20 +440,140 @@ Definition instr_defs (i: instruction) : option reg :=
   | Ireturn optarg => None
   end.
 
-(** Transformation of a RTL function instruction by instruction.
-  This applies a given transformation function to all instructions
-  of a function and constructs a transformed function from that. *)
+(** 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). *)
 
-Section TRANSF.
+Definition max_pc_function (f: function) :=
+  PTree.fold (fun m pc i => Pmax m pc) f.(fn_code) 1%positive.
 
-Variable transf: node -> instruction -> instruction.
+Lemma max_pc_function_sound:
+  forall f pc i, f.(fn_code)!pc = Some i -> Ple pc (max_pc_function f).
+Proof.
+  intros until i. unfold max_pc_function. 
+  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
+  (* extensionality *)
+  intros. apply H0. rewrite H; auto. 
+  (* base case *)
+  rewrite PTree.gempty. congruence.
+  (* inductive case *)
+  intros. rewrite PTree.gsspec in H2. destruct (peq pc k). 
+  inv H2. xomega. 
+  apply Ple_trans with a. auto. xomega.
+Qed.
 
-Definition transf_function (f: function) : function :=
-  mkfunction
-    f.(fn_sig)
-    f.(fn_params)
-    f.(fn_stacksize)
-    (PTree.map transf f.(fn_code))
-    f.(fn_entrypoint).
+(** Maximum pseudo-register mentioned in a function.  All results or arguments
+  of an instruction of [f], as well as all parameters of [f], are between
+  1 and [max_reg_function] (inclusive). *)
 
-End TRANSF.
+Definition max_reg_instr (m: positive) (pc: node) (i: instruction) :=
+  match i with
+  | Inop s => m
+  | Iop op args res s => fold_left Pmax args (Pmax res m)
+  | Iload chunk addr args dst s => fold_left Pmax args (Pmax dst m)
+  | Istore chunk addr args src s => fold_left Pmax args (Pmax src m)
+  | Icall sig (inl r) args res s => fold_left Pmax args (Pmax r (Pmax res m))
+  | Icall sig (inr id) args res s => fold_left Pmax args (Pmax res m)
+  | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m)
+  | Itailcall sig (inr id) args => fold_left Pmax args m
+  | Ibuiltin ef args res s => fold_left Pmax args (Pmax res m)
+  | Icond cond args ifso ifnot => fold_left Pmax args m
+  | Ijumptable arg tbl => Pmax arg m
+  | Ireturn None => m
+  | Ireturn (Some arg) => Pmax arg m
+  end.
+
+Definition max_reg_function (f: function) :=
+  Pmax
+    (PTree.fold max_reg_instr f.(fn_code) 1%positive)
+    (fold_left Pmax f.(fn_params) 1%positive).
+
+Remark max_reg_instr_ge:
+  forall m pc i, Ple m (max_reg_instr m pc i).
+Proof.
+  intros. 
+  assert (X: forall l n, Ple m n -> Ple m (fold_left Pmax l n)).
+  { induction l; simpl; intros. 
+    auto.
+    apply IHl. xomega. }
+  destruct i; simpl; try (destruct s0); try (apply X); try xomega.
+  destruct o; xomega.
+Qed.
+
+Remark max_reg_instr_def:
+  forall m pc i r, instr_defs i = Some r -> Ple r (max_reg_instr m pc i).
+Proof.
+  intros.
+  assert (X: forall l n, Ple r n -> Ple r (fold_left Pmax l n)).
+  { induction l; simpl; intros. xomega. apply IHl. xomega. }
+  destruct i; simpl in *; inv H.
+- apply X. xomega.
+- apply X. xomega.
+- destruct s0; apply X; xomega.
+- apply X. xomega.
+Qed.
+
+Remark max_reg_instr_uses:
+  forall m pc i r, In r (instr_uses i) -> Ple r (max_reg_instr m pc i).
+Proof.
+  intros. 
+  assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)).
+  { induction l; simpl; intros. 
+    tauto.
+    apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
+  destruct i; simpl in *; try (destruct s0); try (apply X; auto).
+- contradiction.
+- destruct H. right; subst; xomega. auto.
+- destruct H. right; subst; xomega. auto.
+- destruct H. right; subst; xomega. auto.
+- intuition. subst; xomega.
+- destruct o; simpl in H; intuition. subst; xomega.
+Qed.
+
+Lemma max_reg_function_def:
+  forall f pc i r,
+  f.(fn_code)!pc = Some i -> instr_defs i = Some r -> Ple r (max_reg_function f).
+Proof.
+  intros. 
+  assert (Ple r (PTree.fold max_reg_instr f.(fn_code) 1%positive)).
+  {  revert H. 
+     apply PTree_Properties.fold_rec with
+       (P := fun c m => c!pc = Some i -> Ple r m).
+   - intros. rewrite H in H1; auto.
+   - rewrite PTree.gempty; congruence.
+   - intros. rewrite PTree.gsspec in H3. destruct (peq pc k). 
+     + inv H3. eapply max_reg_instr_def; eauto. 
+     + apply Ple_trans with a. auto. apply max_reg_instr_ge.
+  }
+  unfold max_reg_function. xomega. 
+Qed.
+
+Lemma max_reg_function_use:
+  forall f pc i r,
+  f.(fn_code)!pc = Some i -> In r (instr_uses i) -> Ple r (max_reg_function f).
+Proof.
+  intros. 
+  assert (Ple r (PTree.fold max_reg_instr f.(fn_code) 1%positive)).
+  {  revert H. 
+     apply PTree_Properties.fold_rec with
+       (P := fun c m => c!pc = Some i -> Ple r m).
+   - intros. rewrite H in H1; auto.
+   - rewrite PTree.gempty; congruence.
+   - intros. rewrite PTree.gsspec in H3. destruct (peq pc k). 
+     + inv H3. eapply max_reg_instr_uses; eauto. 
+     + apply Ple_trans with a. auto. apply max_reg_instr_ge.
+  }
+  unfold max_reg_function. xomega. 
+Qed.
+
+Lemma max_reg_function_params:
+  forall f r, In r f.(fn_params) -> Ple r (max_reg_function f).
+Proof.
+  intros.
+  assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)).
+  { induction l; simpl; intros. 
+    tauto.
+    apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
+  assert (Y: Ple r (fold_left Pmax f.(fn_params) 1%positive)).
+  { apply X; auto. }
+  unfold max_reg_function. xomega.
+Qed.