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

1 files changed, 313 insertions, 70 deletions

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.