From 0ba10d800ae221377bf76dc1e5f5b4351a95cf42 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 26 Aug 2009 12:57:11 +0000 Subject: Coloringaux: make identifiers unique; special treatment of precolored nodes a la Appel and George. Maps: in PTree.combine, compress useless subtrees. Lattice: more efficient implementation of LPMap. Makefile: build profiling version git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Camlcoq.ml | 10 ++++++ lib/Lattice.v | 86 +++++++++++++++++++++++++++++++++++++-------------- lib/Maps.v | 98 +++++++++++++++++++++++++++++++++------------------------- 3 files changed, 129 insertions(+), 65 deletions(-) (limited to 'lib') diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index c7abdcc..436583f 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -127,3 +127,13 @@ let print_timers () = let _ = at_exit print_timers *) + +(* Heap profiling facility *) + +(* +let heap_info msg = + Gc.full_major(); + let s = Gc.stat() in + Printf.printf "%s: size %d live %d\n " msg s.Gc.heap_words s.Gc.live_words; + flush stdout +*) diff --git a/lib/Lattice.v b/lib/Lattice.v index 390f49d..a185c43 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -80,23 +80,31 @@ Definition get (p: positive) (x: t) : L.t := Definition set (p: positive) (v: L.t) (x: t) : t := match x with | Bot_except m => - Bot_except (PTree.set p v m) + Bot_except (if L.beq v L.bot then PTree.remove p m else PTree.set p v m) | Top_except m => - Top_except (PTree.set p v m) + Top_except (if L.beq v L.top then PTree.remove p m else PTree.set p v m) end. Lemma gss: forall p v x, - get p (set p v x) = v. + L.eq (get p (set p v x)) v. Proof. - intros. destruct x; simpl; rewrite PTree.gss; auto. + intros. destruct x; simpl. + case_eq (L.beq v L.bot); intros. + rewrite PTree.grs. apply L.eq_sym. apply L.beq_correct; auto. + rewrite PTree.gss. apply L.eq_refl. + case_eq (L.beq v L.top); intros. + rewrite PTree.grs. apply L.eq_sym. apply L.beq_correct; auto. + rewrite PTree.gss. apply L.eq_refl. Qed. Lemma gso: forall p q v x, p <> q -> get p (set q v x) = get p x. Proof. - intros. destruct x; simpl; rewrite PTree.gso; auto. + intros. destruct x; simpl. + destruct (L.beq v L.bot). rewrite PTree.gro; auto. rewrite PTree.gso; auto. + destruct (L.beq v L.top). rewrite PTree.gro; auto. rewrite PTree.gso; auto. Qed. Definition eq (x y: t) : Prop := @@ -177,6 +185,10 @@ Proof. unfold ge; intros. rewrite get_top. apply L.ge_top. Qed. +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. + Definition lub (x y: t) : t := match x, y with | Bot_except m, Bot_except n => @@ -194,7 +206,7 @@ Definition lub (x y: t) : t := (PTree.combine (fun a b => match a, b with - | Some u, Some v => Some (L.lub u v) + | Some u, Some v => opt_lub u v | None, _ => b | _, None => None end) @@ -204,7 +216,7 @@ Definition lub (x y: t) : t := (PTree.combine (fun a b => match a, b with - | Some u, Some v => Some (L.lub u v) + | Some u, Some v => opt_lub u v | None, _ => None | _, None => a end) @@ -214,7 +226,7 @@ Definition lub (x y: t) : t := (PTree.combine (fun a b => match a, b with - | Some u, Some v => Some (L.lub u v) + | Some u, Some v => opt_lub u v | _, _ => None end) m n) @@ -223,37 +235,65 @@ Definition lub (x y: t) : t := Lemma lub_commut: forall x y, eq (lub x y) (lub y x). Proof. - intros x y p. + 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; - try apply L.eq_refl; try apply L.lub_commut. + auto; apply L.eq_refl || apply L.lub_commut. Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. + assert (forall u v, + L.ge (match opt_lub u v with Some x => x | None => L.top end) u). + 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. - rewrite PTree.gcombine. - destruct t0!p. destruct t1!p. apply L.ge_lub_left. + rewrite PTree.gcombine; auto. + destruct t0!p; destruct t1!p. + apply L.ge_lub_left. apply L.ge_refl. apply L.eq_refl. - destruct t1!p. apply L.ge_bot. apply L.ge_refl. apply L.eq_refl. - auto. + apply L.ge_bot. + apply L.ge_refl. apply L.eq_refl. - rewrite PTree.gcombine. - destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_top. destruct t1!p. apply L.ge_bot. apply L.ge_bot. + rewrite PTree.gcombine; auto. + destruct t0!p; destruct t1!p. auto. + apply L.ge_top. + apply L.ge_bot. + apply L.ge_top. - rewrite PTree.gcombine. - destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_refl. apply L.eq_refl. apply L.ge_refl. apply L.eq_refl. auto. + rewrite PTree.gcombine; auto. + destruct t0!p; destruct t1!p. + auto. + apply L.ge_refl. apply L.eq_refl. + apply L.ge_top. + apply L.ge_top. - rewrite PTree.gcombine. - destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_top. apply L.ge_refl. apply L.eq_refl. + rewrite PTree.gcombine; auto. + destruct t0!p; destruct t1!p. auto. + apply L.ge_top. + apply L.ge_top. + apply L.ge_top. Qed. End LPMap. diff --git a/lib/Maps.v b/lib/Maps.v index b607d24..4c0bd50 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -102,9 +102,9 @@ Module Type TREE. Variable combine: forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A. Hypothesis gcombine: - forall (A: Type) (f: option A -> option A -> option A) - (m1 m2: t A) (i: elt), + forall (A: Type) (f: option A -> option A -> option A), f None None = None -> + forall (m1 m2: t A) (i: elt), get i (combine f m1 m2) = f (get i m1) (get i m2). Hypothesis combine_commut: forall (A: Type) (f g: option A -> option A -> option A), @@ -481,70 +481,84 @@ Module PTree <: TREE. rewrite append_neutral_l; auto. Qed. - Fixpoint xcombine_l (A : Type) (f : option A -> option A -> option A) - (m : t A) {struct m} : t A := + Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A := + match l, x, r with + | Leaf, None, Leaf => Leaf + | _, _, _ => Node l x r + end. + + Lemma gnode': + forall (A: Type) (l r: t A) (x: option A) (i: positive), + get i (Node' l x r) = get i (Node l x r). + Proof. + intros. unfold Node'. + destruct l; destruct x; destruct r; auto. + destruct i; simpl; auto; rewrite gleaf; auto. + Qed. + + Section COMBINE. + + Variable A: Type. + Variable f: option A -> option A -> option A. + Hypothesis f_none_none: f None None = None. + + Fixpoint xcombine_l (m : t A) {struct m} : t A := match m with | Leaf => Leaf - | Node l o r => Node (xcombine_l f l) (f o None) (xcombine_l f r) + | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r) end. - Lemma xgcombine_l : - forall (A : Type) (f : option A -> option A -> option A) - (i : positive) (m : t A), - f None None = None -> get i (xcombine_l f m) = f (get i m) None. + Lemma xgcombine_l : + forall (m: t A) (i : positive), + get i (xcombine_l m) = f (get i m) None. Proof. - induction i; intros; destruct m; simpl; auto. + induction m; intros; simpl. + repeat rewrite gleaf. auto. + rewrite gnode'. destruct i; simpl; auto. Qed. - Fixpoint xcombine_r (A : Type) (f : option A -> option A -> option A) - (m : t A) {struct m} : t A := + Fixpoint xcombine_r (m : t A) {struct m} : t A := match m with | Leaf => Leaf - | Node l o r => Node (xcombine_r f l) (f None o) (xcombine_r f r) + | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r) end. - Lemma xgcombine_r : - forall (A : Type) (f : option A -> option A -> option A) - (i : positive) (m : t A), - f None None = None -> get i (xcombine_r f m) = f None (get i m). + Lemma xgcombine_r : + forall (m: t A) (i : positive), + get i (xcombine_r m) = f None (get i m). Proof. - induction i; intros; destruct m; simpl; auto. + induction m; intros; simpl. + repeat rewrite gleaf. auto. + rewrite gnode'. destruct i; simpl; auto. Qed. - Fixpoint combine (A : Type) (f : option A -> option A -> option A) - (m1 m2 : t A) {struct m1} : t A := + Fixpoint combine (m1 m2 : t A) {struct m1} : t A := match m1 with - | Leaf => xcombine_r f m2 + | Leaf => xcombine_r m2 | Node l1 o1 r1 => match m2 with - | Leaf => xcombine_l f m1 - | Node l2 o2 r2 => Node (combine f l1 l2) (f o1 o2) (combine f r1 r2) + | Leaf => xcombine_l m1 + | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2) end end. - Lemma xgcombine: - forall (A: Type) (f: option A -> option A -> option A) (i: positive) - (m1 m2: t A), - f None None = None -> - get i (combine f m1 m2) = f (get i m1) (get i m2). - Proof. - induction i; intros; destruct m1; destruct m2; simpl; auto; - try apply xgcombine_r; try apply xgcombine_l; auto. - Qed. - Theorem gcombine: - forall (A: Type) (f: option A -> option A -> option A) - (m1 m2: t A) (i: positive), - f None None = None -> - get i (combine f m1 m2) = f (get i m1) (get i m2). + forall (m1 m2: t A) (i: positive), + get i (combine m1 m2) = f (get i m1) (get i m2). Proof. - intros A f m1 m2 i H; exact (xgcombine f i m1 m2 H). + induction m1; intros; simpl. + rewrite gleaf. apply xgcombine_r. + destruct m2; simpl. + rewrite gleaf. rewrite <- xgcombine_l. auto. + repeat rewrite gnode'. destruct i; simpl; auto. Qed. - Lemma xcombine_lr : - forall (A : Type) (f g : option A -> option A -> option A) (m : t A), - (forall (i j : option A), f i j = g j i) -> - xcombine_l f m = xcombine_r g m. + End COMBINE. + + Lemma xcombine_lr : + forall (A : Type) (f g : option A -> option A -> option A) (m : t A), + (forall (i j : option A), f i j = g j i) -> + xcombine_l f m = xcombine_r g m. Proof. induction m; intros; simpl; auto. rewrite IHm1; auto. -- cgit v1.2.3