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

13 files changed, 53 insertions, 64 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 5a5e4c4d..daa53e54 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -165,7 +165,7 @@ Proof.
   apply agree_increasing with (live!!n).
   eapply DS.fixpoint_solution. unfold analyze in H; eauto.
   unfold RTL.successors, Kildall.successors_list. 
-  rewrite PTree.gmap. rewrite H0. simpl. auto.
+  rewrite PTree.gmap1. rewrite H0. simpl. auto.
   auto.
 Qed.
 
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index c5670e8d..275b9fd2 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -695,7 +695,7 @@ Proof.
   intros res FIXPOINT WF AT SUCC.
   assert (Numbering.ge res!!pc' (transfer f pc res!!pc)).
     eapply Solver.fixpoint_solution; eauto.
-    unfold successors_list, successors. rewrite PTree.gmap.
+    unfold successors_list, successors. rewrite PTree.gmap1.
     rewrite AT. auto.
   apply H.
   intros. rewrite PMap.gi. apply empty_numbering_satisfiable.
diff --git a/backend/CastOptim.v b/backend/CastOptim.v
index 545564d8..19d0065f 100644
--- a/backend/CastOptim.v
+++ b/backend/CastOptim.v
@@ -136,12 +136,12 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     | Single, Single => Single
     | _, _ => Unknown
     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 lub, eq; intros.
-    destruct x; destruct y; auto.
+    unfold lub, ge; intros.
+    destruct x; destruct y; 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.
     unfold lub, ge; intros.
     destruct x; destruct y; auto. 
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v
index d5076090..b04e061a 100644
--- a/backend/CastOptimproof.v
+++ b/backend/CastOptimproof.v
@@ -118,7 +118,7 @@ Proof.
   intros approxs; intros.
   apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
-  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
+  unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto.
   auto.
   intros. rewrite PMap.gi. apply regs_match_approx_top. 
 Qed.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 03966cdd..47c40e3e 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -87,12 +87,6 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     | _, Novalue => x
     | _, _ => Unknown
     end.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
-  Proof.
-    unfold lub, eq; intros.
-    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
-    destruct x; destruct y; auto.
-  Qed.
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
     unfold lub; intros.
@@ -100,6 +94,13 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     apply ge_refl. apply eq_refl.
     destruct x; destruct y; unfold ge; tauto.
   Qed.
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
+  Proof.
+    unfold lub; intros.
+    case (eq_dec x y); intro.
+    apply ge_refl. subst. apply eq_refl.
+    destruct x; destruct y; unfold ge; tauto.
+  Qed.
 End Approx.
 
 Module D := LPMap Approx.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 714468aa..1dad5187 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -106,7 +106,7 @@ Proof.
   intros approxs; intros.
   apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
-  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
+  unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto.
   auto.
   intros. rewrite PMap.gi. apply regs_match_approx_top. 
 Qed.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index 83206f78..e1e6ea53 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -344,14 +344,12 @@ Proof.
            ((st_in st) !! n) (L.lub (st_in st) !! n out).
   split.
   eapply L.ge_trans. apply L.ge_refl. apply H; auto.
-  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
-  apply L.ge_lub_left. 
+  apply L.ge_lub_right. 
   auto.
 
   simpl. split.
   rewrite PMap.gss.
-  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
-  apply L.ge_lub_left. 
+  apply L.ge_lub_right.
   intros. rewrite PMap.gso; auto.
 Qed.
 
@@ -506,8 +504,7 @@ Proof.
   elim H.
   elim H; intros.
   subst a. rewrite PMap.gss.
-  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
-  apply L.ge_lub_left.
+  apply L.ge_lub_right.
   destruct a. rewrite PMap.gsspec. case (peq n p); intro.
   subst p. apply L.ge_trans with (start_state_in ep)!!n.
   apply L.ge_lub_left. auto.
@@ -1168,49 +1165,41 @@ End BBlock_solver.
   greatest node in the working list.  For backward analysis,
   we will similarly pick the smallest node in the working list. *)
 
-Require Import FSets.
-Require Import FSetAVL.
-Require Import Ordered.
-
-Module PositiveSet := FSetAVL.Make(OrderedPositive).
-Module PositiveSetFacts := FSetFacts.Facts(PositiveSet).
+Require Import Heaps.
 
 Module NodeSetForward <: NODE_SET.
-  Definition t := PositiveSet.t.
-  Definition add (n: positive) (s: t) : t := PositiveSet.add n s.
+  Definition t := PHeap.t.
+  Definition add (n: positive) (s: t) : t := PHeap.insert n s.
   Definition pick (s: t) :=
-    match PositiveSet.max_elt s with
-    | Some n => Some(n, PositiveSet.remove n s)
+    match PHeap.findMax s with
+    | Some n => Some(n, PHeap.deleteMax s)
     | None => None
     end.
   Definition initial (successors: PTree.t (list positive)) :=
-    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
-  Definition In := PositiveSet.In.
+    PTree.fold (fun s pc scs => PHeap.insert pc s) successors PHeap.empty.
+  Definition In := PHeap.In.
 
   Lemma add_spec:
     forall n n' s, In n' (add n s) <-> n = n' \/ In n' s.
   Proof.
-    intros. exact (PositiveSetFacts.add_iff s n n').
+    intros. rewrite PHeap.In_insert. unfold In. intuition.
   Qed.
     
   Lemma pick_none:
     forall s n, pick s = None -> ~In n s.
   Proof.
-    intros until n; unfold pick. caseEq (PositiveSet.max_elt s); intros.
+    intros until n; unfold pick. caseEq (PHeap.findMax s); intros.
     congruence.
-    apply PositiveSet.max_elt_3. auto.
+    apply PHeap.findMax_empty. auto.
   Qed.
 
   Lemma pick_some:
     forall s n s', pick s = Some(n, s') ->
     forall n', In n' s <-> n = n' \/ In n' s'.
   Proof.
-    intros until s'; unfold pick. caseEq (PositiveSet.max_elt s); intros.
-    inversion H0; clear H0; subst. 
-    split; intros. 
-    destruct (peq n n'). auto. right. apply PositiveSet.remove_2; assumption.
-    elim H0; intro. subst n'. apply PositiveSet.max_elt_1. auto. 
-    apply PositiveSet.remove_3 with n; assumption.
+    intros until s'; unfold pick. caseEq (PHeap.findMax s); intros.
+    inv H0.
+    generalize (PHeap.In_deleteMax s n n' H). unfold In. intuition.
     congruence.
   Qed.
 
@@ -1233,39 +1222,36 @@ Module NodeSetForward <: NODE_SET.
 End NodeSetForward.
 
 Module NodeSetBackward <: NODE_SET.
-  Definition t := PositiveSet.t.
-  Definition add (n: positive) (s: t) : t := PositiveSet.add n s.
+  Definition t := PHeap.t.
+  Definition add (n: positive) (s: t) : t := PHeap.insert n s.
   Definition pick (s: t) :=
-    match PositiveSet.min_elt s with
-    | Some n => Some(n, PositiveSet.remove n s)
+    match PHeap.findMin s with
+    | Some n => Some(n, PHeap.deleteMin s)
     | None => None
     end.
   Definition initial (successors: PTree.t (list positive)) :=
-    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
-  Definition In := PositiveSet.In.
+    PTree.fold (fun s pc scs => PHeap.insert pc s) successors PHeap.empty.
+  Definition In := PHeap.In.
 
   Lemma add_spec:
     forall n n' s, In n' (add n s) <-> n = n' \/ In n' s.
   Proof NodeSetForward.add_spec.
-    
+
   Lemma pick_none:
     forall s n, pick s = None -> ~In n s.
   Proof.
-    intros until n; unfold pick. caseEq (PositiveSet.min_elt s); intros.
+    intros until n; unfold pick. caseEq (PHeap.findMin s); intros.
     congruence.
-    apply PositiveSet.min_elt_3. auto.
+    apply PHeap.findMin_empty. auto.
   Qed.
 
   Lemma pick_some:
     forall s n s', pick s = Some(n, s') ->
     forall n', In n' s <-> n = n' \/ In n' s'.
   Proof.
-    intros until s'; unfold pick. caseEq (PositiveSet.min_elt s); intros.
-    inversion H0; clear H0; subst. 
-    split; intros. 
-    destruct (peq n n'). auto. right. apply PositiveSet.remove_2; assumption.
-    elim H0; intro. subst n'. apply PositiveSet.min_elt_1. auto. 
-    apply PositiveSet.remove_3 with n; assumption.
+    intros until s'; unfold pick. caseEq (PHeap.findMin s); intros.
+    inv H0.
+    generalize (PHeap.In_deleteMin s n n' H). unfold In. intuition.
     congruence.
   Qed.
 
diff --git a/backend/LTL.v b/backend/LTL.v
index 2eff67cd..a68352fc 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -290,4 +290,4 @@ Definition successors_instr (i: instruction) : list node :=
   end.
 
 Definition successors (f: function): PTree.t (list node) :=
-  PTree.map (fun pc i => successors_instr i) f.(fn_code).
+  PTree.map1 successors_instr f.(fn_code).
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index df750008..abc497ec 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -128,7 +128,7 @@ Proof.
   assert (LBoolean.ge reach!!pc' reach!!pc).
   change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)).
   eapply DS.fixpoint_solution. eexact H.
-  unfold Kildall.successors_list, successors. rewrite PTree.gmap.
+  unfold Kildall.successors_list, successors. rewrite PTree.gmap1.
   rewrite H0; auto.
   elim H3; intro. congruence. auto.
   intros. apply PMap.gi.
diff --git a/backend/RTL.v b/backend/RTL.v
index 1c309a0c..208c7b13 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -368,7 +368,7 @@ Definition successors_instr (i: instruction) : list node :=
   end.
 
 Definition successors (f: function) : PTree.t (list node) :=
-  PTree.map (fun pc i => successors_instr i) f.(fn_code).
+  PTree.map1 successors_instr f.(fn_code).
 
 (** Transformation of a RTL function instruction by instruction.
   This applies a given transformation function to all instructions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index e9184494..a9c8f97c 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -591,7 +591,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do n1 <- reserve_instr;
       do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret;
       do xx <- update_instr n1 (Inop n2);
-      ret n1
+      add_instr (Inop n2)
   | Sblock sbody =>
       transl_stmt map sbody nd (nd :: nexits) ngoto nret rret
   | Sexit n =>
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index b49b671a..24f8c1a7 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1069,7 +1069,7 @@ Proof.
   inv H2. eapply IHs2; eauto.
   (* loop *)
   intros. inversion H1; subst.
-  eapply IHs; eauto. econstructor; eauto.
+  eapply IHs; eauto. econstructor; eauto. econstructor; eauto.
   (* block *)
   intros. inv H1.
   eapply IHs; eauto. econstructor; eauto.
@@ -1216,6 +1216,7 @@ Proof.
   left. apply plus_one. eapply exec_Inop; eauto. 
   econstructor; eauto. 
   econstructor; eauto.
+  econstructor; eauto.
 
   (* block *)
   inv TS.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 44e7c418..9b2e63e8 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -885,9 +885,10 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_stmt c map sfalse nfalse nd nexits ngoto nret rret ->
      tr_condition c map nil a ns ntrue nfalse ->
      tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret
-  | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop,
-     tr_stmt c map sbody nloop ns nexits ngoto nret rret ->
+  | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend,
+     tr_stmt c map sbody nloop nend nexits ngoto nret rret ->
      c!ns = Some(Inop nloop) ->
+     c!nend = Some(Inop nloop) ->
      tr_stmt c map (Sloop sbody) ns nd nexits ngoto nret rret
   | tr_Sblock: forall sbody ns nd nexits ngoto nret rret,
      tr_stmt c map sbody ns nd (nd :: nexits) ngoto nret rret ->
@@ -1294,7 +1295,7 @@ Proof.
   econstructor. 
   apply tr_stmt_incr with s1; auto. 
   eapply IHstmt; eauto with rtlg.
-  eauto with rtlg.
+  eauto with rtlg. eauto with rtlg. 
   (* Sblock *)
   econstructor. 
   eapply IHstmt; eauto with rtlg.