From b54721f58c2ecb65ce554d8b34f214d5121a2b0c Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 27 Oct 2010 09:23:19 +0000 Subject: Various algorithmic improvements that reduce compile times (thanks Alexandre Pilkiewicz): - Lattice: preserve sharing in "combine" operation - Kildall: use splay heaps (lib/Heaps.v) for node sets - RTLgen: add a "nop" before loops so that natural enumeration of nodes coincides with (reverse) postorder - Maps: add PTree.map1 operation, use it in RTL and LTL. - Driver: increase minor heap size git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Lattice.v | 383 +++++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 313 insertions(+), 70 deletions(-) (limited to 'lib/Lattice.v') diff --git a/lib/Lattice.v b/lib/Lattice.v index a185c43a..c200fc8d 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -35,12 +35,11 @@ Module Type SEMILATTICE. Variable ge: t -> t -> Prop. Hypothesis ge_refl: forall x y, eq x y -> ge x y. Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. Variable bot: t. Hypothesis ge_bot: forall x, ge x bot. Variable lub: t -> t -> t. - Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x). Hypothesis ge_lub_left: forall x y, ge (lub x y) x. + Hypothesis ge_lub_right: forall x y, ge (lub x y) y. End SEMILATTICE. @@ -57,6 +56,8 @@ End SEMILATTICE_WITH_TOP. (** * Semi-lattice over maps *) +Set Implicit Arguments. + (** Given a semi-lattice with top [L], the following functor implements a semi-lattice structure over finite maps from positive numbers to [L.t]. The default value for these maps is either [L.top] or [L.bot]. *) @@ -156,11 +157,6 @@ Proof. unfold ge; intros. apply L.ge_trans with (get p y); auto. Qed. -Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. -Proof. - unfold eq,ge; intros. eapply L.ge_compat; eauto. -Qed. - Definition bot := Bot_except (PTree.empty L.t). Lemma get_bot: forall p, get p bot = L.bot. @@ -185,6 +181,232 @@ Proof. unfold ge; intros. rewrite get_top. apply L.ge_top. Qed. +(** A [combine] operation over the type [PTree.t L.t] that attempts + to share its result with its arguments. *) + +Section COMBINE. + +Variable f: option L.t -> option L.t -> option L.t. +Hypothesis f_none_none: f None None = None. + +Definition opt_eq (ox oy: option L.t) : Prop := + match ox, oy with + | None, None => True + | Some x, Some y => L.eq x y + | _, _ => False + end. + +Lemma opt_eq_refl: forall ox, opt_eq ox ox. +Proof. + intros. unfold opt_eq. destruct ox. apply L.eq_refl. auto. +Qed. + +Lemma opt_eq_sym: forall ox oy, opt_eq ox oy -> opt_eq oy ox. +Proof. + unfold opt_eq. destruct ox; destruct oy; auto. apply L.eq_sym. +Qed. + +Lemma opt_eq_trans: forall ox oy oz, opt_eq ox oy -> opt_eq oy oz -> opt_eq ox oz. +Proof. + unfold opt_eq. destruct ox; destruct oy; destruct oz; intuition. + eapply L.eq_trans; eauto. +Qed. + +Definition opt_beq (ox oy: option L.t) : bool := + match ox, oy with + | None, None => true + | Some x, Some y => L.beq x y + | _, _ => false + end. + +Lemma opt_beq_correct: + forall ox oy, opt_beq ox oy = true -> opt_eq ox oy. +Proof. + unfold opt_beq, opt_eq. destruct ox; destruct oy; try congruence. + intros. apply L.beq_correct; auto. + auto. +Qed. + +Definition tree_eq (m1 m2: PTree.t L.t) : Prop := + forall i, opt_eq (PTree.get i m1) (PTree.get i m2). + +Lemma tree_eq_refl: forall m, tree_eq m m. +Proof. intros; red; intros; apply opt_eq_refl. Qed. + +Lemma tree_eq_sym: forall m1 m2, tree_eq m1 m2 -> tree_eq m2 m1. +Proof. intros; red; intros; apply opt_eq_sym; auto. Qed. + +Lemma tree_eq_trans: forall m1 m2 m3, tree_eq m1 m2 -> tree_eq m2 m3 -> tree_eq m1 m3. +Proof. intros; red; intros; apply opt_eq_trans with (PTree.get i m2); auto. Qed. + +Lemma tree_eq_node: + forall l1 o1 r1 l2 o2 r2, + tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> + tree_eq (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2). +Proof. + intros; red; intros. destruct i; simpl; auto. +Qed. + +Lemma tree_eq_node': + forall l1 o1 r1 l2 o2 r2, + tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> + tree_eq (PTree.Node l1 o1 r1) (PTree.Node' l2 o2 r2). +Proof. + intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto. +Qed. + +Lemma tree_eq_node'': + forall l1 o1 r1 l2 o2 r2, + tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> + tree_eq (PTree.Node' l1 o1 r1) (PTree.Node' l2 o2 r2). +Proof. + intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto. +Qed. + +Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym + tree_eq_refl tree_eq_sym + tree_eq_node tree_eq_node' tree_eq_node'' : combine. + +Inductive changed: Type := Unchanged | Changed (m: PTree.t L.t). + +Fixpoint combine_l (m : PTree.t L.t) {struct m} : changed := + match m with + | PTree.Leaf => + Unchanged + | PTree.Node l o r => + let o' := f o None in + match combine_l l, combine_l r with + | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) + | Unchanged, Changed r' => Changed (PTree.Node' l o' r') + | Changed l', Unchanged => Changed (PTree.Node' l' o' r) + | Changed l', Changed r' => Changed (PTree.Node' l' o' r') + end + end. + +Lemma combine_l_eq: + forall m, + tree_eq (match combine_l m with Unchanged => m | Changed m' => m' end) + (PTree.xcombine_l f m). +Proof. + induction m; simpl. + auto with combine. + destruct (combine_l m1) as [ | l']; destruct (combine_l m2) as [ | r']; + auto with combine. + case_eq (opt_beq (f o None) o); auto with combine. +Qed. + +Fixpoint combine_r (m : PTree.t L.t) {struct m} : changed := + match m with + | PTree.Leaf => + Unchanged + | PTree.Node l o r => + let o' := f None o in + match combine_r l, combine_r r with + | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) + | Unchanged, Changed r' => Changed (PTree.Node' l o' r') + | Changed l', Unchanged => Changed (PTree.Node' l' o' r) + | Changed l', Changed r' => Changed (PTree.Node' l' o' r') + end + end. + +Lemma combine_r_eq: + forall m, + tree_eq (match combine_r m with Unchanged => m | Changed m' => m' end) + (PTree.xcombine_r f m). +Proof. + induction m; simpl. + auto with combine. + destruct (combine_r m1) as [ | l']; destruct (combine_r m2) as [ | r']; + auto with combine. + case_eq (opt_beq (f None o) o); auto with combine. +Qed. + +Inductive changed2 : Type := + | Same + | Same1 + | Same2 + | CC(m: PTree.t L.t). + +Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 := + match m1, m2 with + | PTree.Leaf, PTree.Leaf => + Same + | PTree.Leaf, _ => + match combine_r m2 with + | Unchanged => Same2 + | Changed m => CC m + end + | _, PTree.Leaf => + match combine_l m1 with + | Unchanged => Same1 + | Changed m => CC m + end + | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => + let o := f o1 o2 in + match xcombine l1 l2, xcombine r1 r2 with + | Same, Same => + match opt_beq o o1, opt_beq o o2 with + | true, true => Same + | true, false => Same1 + | false, true => Same2 + | false, false => CC(PTree.Node' l1 o r1) + end + | Same1, Same | Same, Same1 | Same1, Same1 => + if opt_beq o o1 then Same1 else CC(PTree.Node' l1 o r1) + | Same2, Same | Same, Same2 | Same2, Same2 => + if opt_beq o o2 then Same2 else CC(PTree.Node' l2 o r2) + | Same1, Same2 => CC(PTree.Node' l1 o r2) + | (Same|Same1), CC r => CC(PTree.Node' l1 o r) + | Same2, Same1 => CC(PTree.Node' l2 o r1) + | Same2, CC r => CC(PTree.Node' l2 o r) + | CC l, (Same|Same1) => CC(PTree.Node' l o r1) + | CC l, Same2 => CC(PTree.Node' l o r2) + | CC l, CC r => CC(PTree.Node' l o r) + end + end. + +Lemma xcombine_eq: + forall m1 m2, + match xcombine m1 m2 with + | Same => tree_eq m1 (PTree.combine f m1 m2) /\ tree_eq m2 (PTree.combine f m1 m2) + | Same1 => tree_eq m1 (PTree.combine f m1 m2) + | Same2 => tree_eq m2 (PTree.combine f m1 m2) + | CC m => tree_eq m (PTree.combine f m1 m2) + end. +Proof. +Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r. + induction m1; destruct m2; simpl. + split; apply tree_eq_refl. + generalize (combine_r_eq (PTree.Node m2_1 o m2_2)). + destruct (combine_r (PTree.Node m2_1 o m2_2)); auto. + generalize (combine_l_eq (PTree.Node m1_1 o m1_2)). + destruct (combine_l (PTree.Node m1_1 o m1_2)); auto. + generalize (IHm1_1 m2_1) (IHm1_2 m2_2). + destruct (xcombine m1_1 m2_1); + destruct (xcombine m1_2 m2_2); auto with combine; + intuition; case_eq (opt_beq (f o o0) o); case_eq (opt_beq (f o o0) o0); auto with combine. +Qed. + +Definition combine (m1 m2: PTree.t L.t) : PTree.t L.t := + match xcombine m1 m2 with + | Same|Same1 => m1 + | Same2 => m2 + | CC m => m + end. + +Lemma gcombine: + forall m1 m2 i, opt_eq (PTree.get i (combine m1 m2)) (f (PTree.get i m1) (PTree.get i m2)). +Proof. + intros. + assert (tree_eq (combine m1 m2) (PTree.combine f m1 m2)). + unfold combine. + generalize (xcombine_eq m1 m2). + destruct (xcombine m1 m2); tauto. + eapply opt_eq_trans. apply H. rewrite PTree.gcombine; auto. apply opt_eq_refl. +Qed. + +End COMBINE. + Definition opt_lub (x y: L.t) : option L.t := let z := L.lub x y in if L.beq z L.top then None else Some z. @@ -193,7 +415,7 @@ Definition lub (x y: t) : t := match x, y with | Bot_except m, Bot_except n => Bot_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => Some (L.lub u v) @@ -203,7 +425,7 @@ Definition lub (x y: t) : t := m n) | Bot_except m, Top_except n => Top_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => opt_lub u v @@ -213,7 +435,7 @@ Definition lub (x y: t) : t := m n) | Top_except m, Bot_except n => Top_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => opt_lub u v @@ -223,7 +445,7 @@ Definition lub (x y: t) : t := m n) | Top_except m, Top_except n => Top_except - (PTree.combine + (combine (fun a b => match a, b with | Some u, Some v => opt_lub u v @@ -232,29 +454,26 @@ Definition lub (x y: t) : t := m n) end. -Lemma lub_commut: - forall x y, eq (lub x y) (lub y x). +Lemma gcombine_top: + forall f t1 t2 p, + f None None = None -> + L.eq (get p (Top_except (combine f t1 t2))) + (match f t1!p t2!p with Some x => x | None => L.top end). Proof. - intros x y p. - assert (forall u v, - L.eq (match opt_lub u v with - | Some x => x - | None => L.top end) - (match opt_lub v u with - | Some x => x - | None => L.top - end)). - intros. unfold opt_lub. - case_eq (L.beq (L.lub u v) L.top); - case_eq (L.beq (L.lub v u) L.top); intros. - apply L.eq_refl. - eapply L.eq_trans. apply L.eq_sym. apply L.beq_correct; eauto. apply L.lub_commut. - eapply L.eq_trans. apply L.lub_commut. apply L.beq_correct; auto. - apply L.lub_commut. - destruct x; destruct y; simpl; - repeat rewrite PTree.gcombine; auto; - destruct t0!p; destruct t1!p; - auto; apply L.eq_refl || apply L.lub_commut. + intros. simpl. generalize (gcombine f H t1 t2 p). unfold opt_eq. + destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p). + auto. contradiction. contradiction. intros; apply L.eq_refl. +Qed. + +Lemma gcombine_bot: + forall f t1 t2 p, + f None None = None -> + L.eq (get p (Bot_except (combine f t1 t2))) + (match f t1!p t2!p with Some x => x | None => L.bot end). +Proof. + intros. simpl. generalize (gcombine f H t1 t2 p). unfold opt_eq. + destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p). + auto. contradiction. contradiction. intros; apply L.eq_refl. Qed. Lemma ge_lub_left: @@ -265,31 +484,70 @@ Proof. intros; unfold opt_lub. case_eq (L.beq (L.lub u v) L.top); intros. apply L.ge_top. apply L.ge_lub_left. - unfold ge, get, lub; intros; destruct x; destruct y. + unfold ge, lub; intros. destruct x; destruct y. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot. auto. + simpl. destruct t0!p; destruct t1!p. apply L.ge_lub_left. apply L.ge_refl. apply L.eq_refl. apply L.ge_bot. apply L.ge_refl. apply L.eq_refl. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. auto. apply L.ge_top. apply L.ge_bot. apply L.ge_top. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. + auto. + apply L.ge_refl. apply L.eq_refl. + apply L.ge_top. + apply L.ge_top. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. + auto. + apply L.ge_top. + apply L.ge_top. + apply L.ge_top. +Qed. + +Lemma ge_lub_right: + forall x y, ge (lub x y) y. +Proof. + assert (forall u v, + L.ge (match opt_lub u v with Some x => x | None => L.top end) v). + intros; unfold opt_lub. + case_eq (L.beq (L.lub u v) L.top); intros. apply L.ge_top. apply L.ge_lub_right. + + unfold ge, lub; intros. destruct x; destruct y. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot. auto. + simpl. destruct t0!p; destruct t1!p. + apply L.ge_lub_right. + apply L.ge_bot. + apply L.ge_refl. apply L.eq_refl. + apply L.ge_refl. apply L.eq_refl. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. auto. + apply L.ge_top. apply L.ge_refl. apply L.eq_refl. apply L.ge_top. + + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. + auto. + apply L.ge_bot. + apply L.ge_top. apply L.ge_top. - rewrite PTree.gcombine; auto. - destruct t0!p; destruct t1!p. + eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. + simpl. destruct t0!p; destruct t1!p. auto. apply L.ge_top. apply L.ge_top. @@ -303,7 +561,7 @@ End LPMap. (** Given a set [S: FSetInterface.S], the following functor implements a semi-lattice over these sets, ordered by inclusion. *) -Module LFSet (S: FSetInterface.S) <: SEMILATTICE. +Module LFSet (S: FSetInterface.WS) <: SEMILATTICE. Definition t := S.t. @@ -323,10 +581,6 @@ Module LFSet (S: FSetInterface.S) <: SEMILATTICE. Proof. unfold ge, S.Subset; intros. eauto. Qed. - Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. - Proof. - unfold ge, eq, S.Subset, S.Equal; intros. firstorder. - Qed. Definition bot: t := S.empty. Lemma ge_bot: forall x, ge x bot. @@ -335,18 +589,17 @@ Module LFSet (S: FSetInterface.S) <: SEMILATTICE. Qed. Definition lub: t -> t -> t := S.union. - Lemma lub_commut: forall x y, eq (lub x y) (lub y x). - Proof. - unfold lub, eq, S.Equal; intros. split; intro. - destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. - destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. - Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. unfold lub, ge, S.Subset; intros. apply S.union_2; auto. Qed. + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold lub, ge, S.Subset; intros. apply S.union_3; auto. + Qed. + End LFSet. (** * Flat semi-lattice *) @@ -403,11 +656,6 @@ Proof. transitivity t1; auto. Qed. -Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. -Proof. - unfold eq; intros; congruence. -Qed. - Definition bot: t := Bot. Lemma ge_bot: forall x, ge x bot. @@ -431,13 +679,13 @@ Definition lub (x y: t) : t := | Inj a, Inj b => if X.eq a b then Inj a else Top end. -Lemma lub_commut: forall x y, eq (lub x y) (lub y x). +Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. - unfold eq; destruct x; destruct y; simpl; auto. - case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence. + destruct x; destruct y; simpl; auto. + case (X.eq t0 t1); simpl; auto. Qed. -Lemma ge_lub_left: forall x y, ge (lub x y) x. +Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. destruct x; destruct y; simpl; auto. case (X.eq t0 t1); simpl; auto. @@ -472,11 +720,6 @@ Proof. unfold ge; tauto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. unfold ge; intuition congruence. Qed. -Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. -Proof. - unfold eq; intros; congruence. -Qed. - Definition bot := false. Lemma ge_bot: forall x, ge x bot. @@ -489,10 +732,10 @@ Proof. unfold ge, top; tauto. Qed. Definition lub (x y: t) := x || y. -Lemma lub_commut: forall x y, eq (lub x y) (lub y x). -Proof. intros; unfold eq, lub. apply orb_comm. Qed. - Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. destruct x; destruct y; compute; tauto. Qed. +Lemma ge_lub_right: forall x y, ge (lub x y) y. +Proof. destruct x; destruct y; compute; tauto. Qed. + End LBoolean. -- cgit