diff options
| -rw-r--r-- | backend/Inlining.v | 32 | ||||
| -rw-r--r-- | backend/Inliningspec.v | 75 | ||||
| -rw-r--r-- | backend/RTL.v | 164 |
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. |