summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-01 16:00:20 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-01 16:00:20 +0000
commit3de3ecc23d8ab5d6d45451075467dd70981f1061 (patch)
treef4cfc65f830d6ec66a8986c890fcda314c391c98 /lib
parent3d67364b52cac702ed3f2336d7d02f742aa0257a (diff)
Process successors in increasing order. Helps preserving the nice CFG
structure that we got from Cminorgen. Otherwise, the linearization heuristic can produce rather bad code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1948 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib')
-rw-r--r--lib/Postorder.v85
1 files changed, 62 insertions, 23 deletions
diff --git a/lib/Postorder.v b/lib/Postorder.v
index fe06da7..3a76b0d 100644
--- a/lib/Postorder.v
+++ b/lib/Postorder.v
@@ -16,6 +16,8 @@
(** Postorder numbering of a directed graph. *)
Require Import Wellfounded.
+Require Import Permutation.
+Require Import Mergesort.
Require Import Coqlib.
Require Import Maps.
Require Import Iteration.
@@ -27,6 +29,25 @@ Definition node: Type := positive.
Definition graph: Type := PTree.t (list node).
+(** A sorting function over lists of positives. While not necessary for
+ correctness, we process the successors of a node in increasing order.
+ This preserves more of the shape of the original graph and is good for
+ our CFG linearization heuristic. *)
+
+Module PositiveOrd.
+ Definition t := positive.
+ Definition leb (x y: t): bool := if plt y x then false else true.
+(* Infix "<=?" := leb (at level 35). *)
+ Theorem leb_total : forall x y, is_true (leb x y) \/ is_true (leb y x).
+ Proof.
+ unfold leb, is_true; intros.
+ destruct (plt x y); auto. destruct (plt y x); auto.
+ elim (Plt_strict x). eapply Plt_trans; eauto.
+ Qed.
+End PositiveOrd.
+
+Module Sort := Mergesort.Sort(PositiveOrd).
+
(** The traversal is presented as an iteration that modifies the following state. *)
Record state : Type := mkstate {
@@ -40,7 +61,7 @@ Definition init_state (g: graph) (root: node) :=
match g!root with
| Some succs =>
{| gr := PTree.remove root g;
- wrk := (root, succs) :: nil;
+ wrk := (root, Sort.sort succs) :: nil;
map := PTree.empty positive;
next := 1%positive |}
| None =>
@@ -52,16 +73,25 @@ Definition init_state (g: graph) (root: node) :=
Definition transition (s: state) : PTree.t positive + state :=
match s.(wrk) with
- | nil =>
+ | nil => (**r empty worklist, we are done *)
inl _ s.(map)
- | (x, nil) :: l =>
- inr _ {| gr := s.(gr); wrk := l; map := PTree.set x s.(next) s.(map); next := Psucc s.(next) |}
- | (x, y :: succs_x) :: l =>
+ | (x, nil) :: l => (**r all successors of [x] are numbered; number [x] itself *)
+ inr _ {| gr := s.(gr);
+ wrk := l;
+ map := PTree.set x s.(next) s.(map);
+ next := Psucc s.(next) |}
+ | (x, y :: succs_x) :: l => (**r consider [y], the next unnumbered successor of [x] *)
match s.(gr)!y with
- | None =>
- inr _ {| gr := s.(gr); wrk := (x, succs_x) :: l; map := s.(map); next := s.(next) |}
- | Some succs_y =>
- inr _ {| gr := PTree.remove y s.(gr); wrk := (y, succs_y) :: (x, succs_x) :: l; map := s.(map); next := s.(next) |}
+ | None => (**r [y] is already numbered: discard from worklist *)
+ inr _ {| gr := s.(gr);
+ wrk := (x, succs_x) :: l;
+ map := s.(map);
+ next := s.(next) |}
+ | Some succs_y => (**r push [y] on the worklist *)
+ inr _ {| gr := PTree.remove y s.(gr);
+ wrk := (y, Sort.sort succs_y) :: (x, succs_x) :: l;
+ map := s.(map);
+ next := s.(next) |}
end
end.
@@ -89,8 +119,8 @@ Inductive invariant (s: state) : Prop :=
(* worklist is well-formed *)
(WKLIST: forall x l, In (x, l) s.(wrk) ->
s.(gr)!x = None /\
- exists l', ginit!x = Some(l' ++ l)
- /\ forall y, In y l' -> s.(gr)!y = None)
+ exists l', ginit!x = Some l'
+ /\ forall y, In y l' -> ~In y l -> s.(gr)!y = None)
(* all grey nodes are on the worklist *)
(GREY: forall x, ginit!x <> None -> s.(gr)!x = None -> s.(map)!x = None ->
exists l, In (x,l) s.(wrk)).
@@ -101,6 +131,14 @@ Inductive postcondition (map: PTree.t positive) : Prop :=
(ROOT: ginit!root <> None -> map!root <> None)
(SUCCS: forall x succs y, ginit!x = Some succs -> map!x <> None -> In y succs -> ginit!y <> None -> map!y <> None).
+Remark In_sort:
+ forall x l, In x l <-> In x (Sort.sort l).
+Proof.
+ intros; split; intros.
+ apply Permutation_in with l. apply Sort.Permuted_sort. auto.
+ apply Permutation_in with (Sort.sort l). apply Permutation_sym. apply Sort.Permuted_sort. auto.
+Qed.
+
Lemma transition_spec:
forall s, invariant s ->
match transition s with inr s' => invariant s' | inl m => postcondition m end.
@@ -138,8 +176,9 @@ Proof.
(* color *)
rewrite PTree.gsspec in H0. destruct (peq x0 x).
inv H0. exploit (WKLIST x nil); auto with coqlib.
- intros [A [l' [B C]]]. rewrite app_nil_r in B.
- assert (l' = succs) by congruence. subst l'. eauto.
+ intros [A [l' [B C]]].
+ assert (l' = succs) by congruence. subst l'.
+ apply C; auto.
eauto.
(* wklist *)
apply WKLIST. auto with coqlib.
@@ -167,21 +206,20 @@ Proof.
rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); eauto.
(* wklist *)
destruct H.
- inv H. split. apply PTree.grs. exists (@nil positive); simpl; intuition.
+ inv H. split. apply PTree.grs. exists succs_y; split. eauto.
+ intros. rewrite In_sort in H. tauto.
destruct H.
inv H. exploit WKLIST; eauto with coqlib. intros [A [l' [B C]]].
split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto.
- exists (l' ++ y :: nil); split. rewrite app_ass. auto.
- intros. rewrite in_app_iff in H. simpl in H. intuition.
- rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto.
- subst y0. apply PTree.grs.
+ exists l'; split. auto. intros. rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto.
+ apply C; auto. simpl. intuition congruence.
exploit (WKLIST x0 l0); eauto with coqlib. intros [A [l' [B C]]].
split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto.
exists l'; split; auto. intros.
rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto.
(* grey *)
rewrite PTree.grspec in H0. destruct (PTree.elt_eq x0 y) in H0.
- subst. exists succs_y; auto with coqlib.
+ subst. exists (Sort.sort succs_y); auto with coqlib.
exploit GREY; eauto. simpl. intros [l1 A]. destruct A.
inv H2. exists succ_x; auto.
exists l1; auto.
@@ -191,8 +229,8 @@ Proof.
(* wklist *)
destruct H. inv H.
exploit (WKLIST x0); eauto with coqlib. intros [A [l' [B C]]].
- split. auto. exists (l' ++ y :: nil); split. rewrite app_ass; auto.
- intros. rewrite in_app_iff in H; simpl in H. intuition. congruence.
+ split. auto. exists l'; split. auto.
+ intros. destruct (peq y y0). congruence. apply C; auto. simpl. intuition congruence.
eapply WKLIST; eauto with coqlib.
(* grey *)
exploit GREY; eauto. intros [l1 A]. simpl in A. destruct A.
@@ -220,10 +258,11 @@ Proof.
rewrite PTree.gempty in H0; inv H0.
(* wklist *)
destruct H; inv H.
- split. apply PTree.grs. exists (@nil positive); simpl; tauto.
+ split. apply PTree.grs. exists succs; split; auto.
+ intros. rewrite In_sort in H. intuition.
(* grey *)
rewrite PTree.grspec in H0. destruct (PTree.elt_eq x root).
- subst. exists succs; auto.
+ subst. exists (Sort.sort succs); auto.
contradiction.
(* root has no succs *)