summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backend/Inlining.v32
-rw-r--r--backend/Inliningspec.v75
-rw-r--r--backend/RTL.v164
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.