From 36b1620406c711df89263cc63cf0d1b6e393ecb8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 11 Sep 2006 14:23:48 +0000 Subject: Meilleure representation des worklists dans l'algo de Kildall git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@91 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Kildall.v | 271 +++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 206 insertions(+), 65 deletions(-) (limited to 'backend/Kildall.v') diff --git a/backend/Kildall.v b/backend/Kildall.v index 0210b73..a04528e 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -87,10 +87,37 @@ Module Type DATAFLOW_SOLVER. End DATAFLOW_SOLVER. +(** Kildall's algorithm manipulates worklists, which are sets of CFG nodes + equipped with a ``pick next node to examine'' operation. + The algorithm converges faster if the nodes are chosen in an order + consistent with a reverse postorder traversal of the CFG. + For now, we parameterize the dataflow solver over a module + that implements sets of CFG nodes. *) + +Module Type NODE_SET. + + Variable t: Set. + Variable add: positive -> t -> t. + Variable pick: t -> option (positive * t). + Variable initial: positive -> t. + + Variable In: positive -> t -> Prop. + Hypothesis add_spec: + forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. + Hypothesis pick_none: + forall s n, pick s = None -> ~In n s. + Hypothesis pick_some: + forall s n s', pick s = Some(n, s') -> + forall n', In n' s <-> n = n' \/ In n' s'. + Hypothesis initial_spec: + forall numnodes n, Plt n numnodes -> In n (initial numnodes). + +End NODE_SET. + (** We now define a generic solver that works over any semi-lattice structure. *) -Module Dataflow_Solver (LAT: SEMILATTICE): +Module Dataflow_Solver (LAT: SEMILATTICE) (NS: NODE_SET): DATAFLOW_SOLVER with Module L := LAT. Module L := LAT. @@ -109,7 +136,7 @@ Variable entrypoints: list (positive * L.t). *) Record state : Set := - mkstate { st_in: PMap.t L.t; st_wrk: list positive }. + mkstate { st_in: PMap.t L.t; st_wrk: NS.t }. (** Kildall's algorithm, in pseudo-code, is as follows: << @@ -143,19 +170,8 @@ Fixpoint start_state_in (ep: list (positive * L.t)) : PMap.t L.t := let m := start_state_in rem in PMap.set n (L.lub m!!n v) m end. -Definition start_state_wrk := - positive_rec (list positive) nil (@cons positive) topnode. - Definition start_state := - mkstate (start_state_in entrypoints) start_state_wrk. - -(** The worklist is actually treated as a set: it is not useful - (and detrimental to performance) to put the same point twice in the - worklist. The following function adds a point to the worklist if - it was not already there. *) - -Definition add_to_worklist (n: positive) (wrk: list positive) := - if List.In_dec peq n wrk then wrk else n :: wrk. + mkstate (start_state_in entrypoints) (NS.initial topnode). (** [propagate_succ] corresponds, in the pseudocode, to the body of the [for] loop iterating over all successors. *) @@ -165,7 +181,7 @@ Definition propagate_succ (s: state) (out: L.t) (n: positive) := let newl := L.lub oldl out in if L.eq oldl newl then s - else mkstate (PMap.set n newl s.(st_in)) (add_to_worklist n s.(st_wrk)). + else mkstate (PMap.set n newl s.(st_in)) (NS.add n s.(st_wrk)). (** [propagate_succ_list] corresponds, in the pseudocode, to the [for] loop iterating over all successors. *) @@ -181,10 +197,10 @@ Fixpoint propagate_succ_list (s: state) (out: L.t) (succs: list positive) pseudocode. *) Definition step (s: state) : PMap.t L.t + state := - match s.(st_wrk) with - | nil => + match NS.pick s.(st_wrk) with + | None => inl _ s.(st_in) - | n :: rem => + | Some(n, rem) => inr _ (propagate_succ_list (mkstate s.(st_in) rem) (transf n s.(st_in)!!n) @@ -251,11 +267,11 @@ Proof. (fun res => in_incr start_state.(st_in) res)). intros st INCR. unfold step. - destruct st.(st_wrk) as [ | n rem ]. - auto. + destruct (NS.pick st.(st_wrk)) as [ [n rem] | ]. apply in_incr_trans with st.(st_in). auto. - change st.(st_in) with (mkstate st.(st_in) rem).(st_in). - apply propagate_succ_list_incr. + change st.(st_in) with (mkstate st.(st_in) rem).(st_in). + apply propagate_succ_list_incr. + auto. eauto. apply in_incr_refl. Qed. @@ -272,7 +288,7 @@ Qed. Definition good_state (st: state) : Prop := forall n, Plt n topnode -> - In n st.(st_wrk) \/ + NS.In n st.(st_wrk) \/ (forall s, In s (successors n) -> L.ge st.(st_in)!!s (transf n st.(st_in)!!n)). @@ -283,27 +299,7 @@ Lemma start_state_good: good_state start_state. Proof. unfold good_state, start_state; intros. - left; simpl. unfold start_state_wrk. - generalize H. pattern topnode. apply positive_Peano_ind. - intro. compute in H0. destruct n; discriminate. - intros. rewrite positive_rec_succ. - elim (Plt_succ_inv _ _ H1); intro. - auto with coqlib. - subst x; auto with coqlib. -Qed. - -Lemma add_to_worklist_1: - forall n wkl, In n (add_to_worklist n wkl). -Proof. - intros. unfold add_to_worklist. - case (In_dec peq n wkl); auto with coqlib. -Qed. - -Lemma add_to_worklist_2: - forall n wkl n', In n' wkl -> In n' (add_to_worklist n wkl). -Proof. - intros. unfold add_to_worklist. - case (In_dec peq n wkl); auto with coqlib. + left; simpl. apply NS.initial_spec. auto. Qed. Lemma propagate_succ_charact: @@ -344,43 +340,41 @@ Proof. Qed. Lemma propagate_succ_incr_worklist: - forall st out n, - incl st.(st_wrk) (propagate_succ st out n).(st_wrk). + forall st out n x, + NS.In x st.(st_wrk) -> NS.In x (propagate_succ st out n).(st_wrk). Proof. intros. unfold propagate_succ. case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro. - apply incl_refl. - simpl. red; intros. apply add_to_worklist_2; auto. + auto. + simpl. rewrite NS.add_spec. auto. Qed. Lemma propagate_succ_list_incr_worklist: - forall out succs st, - incl st.(st_wrk) (propagate_succ_list st out succs).(st_wrk). + forall out succs st x, + NS.In x st.(st_wrk) -> NS.In x (propagate_succ_list st out succs).(st_wrk). Proof. induction succs; simpl; intros. - apply incl_refl. - apply incl_tran with (propagate_succ st out a).(st_wrk). - apply propagate_succ_incr_worklist. auto. + apply IHsuccs. apply propagate_succ_incr_worklist. auto. Qed. Lemma propagate_succ_records_changes: forall st out n s, let st' := propagate_succ st out n in - In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s. + NS.In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s. Proof. simpl. intros. unfold propagate_succ. case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro. right; auto. case (peq s n); intro. - subst s. left. simpl. apply add_to_worklist_1. + subst s. left. simpl. rewrite NS.add_spec. auto. right. simpl. apply PMap.gso. auto. Qed. Lemma propagate_succ_list_records_changes: forall out succs st s, let st' := propagate_succ_list st out succs in - In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s. + NS.In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s. Proof. induction succs; simpl; intros. right; auto. @@ -391,15 +385,15 @@ Qed. Lemma step_state_good: forall st n rem, - st.(st_wrk) = n :: rem -> + NS.pick st.(st_wrk) = Some(n, rem) -> good_state st -> good_state (propagate_succ_list (mkstate st.(st_in) rem) (transf n st.(st_in)!!n) (successors n)). Proof. unfold good_state. intros st n rem WKL GOOD x LTx. + generalize (NS.pick_some _ _ _ WKL); intro PICK. set (out := transf n st.(st_in)!!n). - rewrite WKL in GOOD. elim (propagate_succ_list_records_changes out (successors n) (mkstate st.(st_in) rem) x). intro; left; auto. @@ -415,7 +409,7 @@ Proof. elim (GOOD x LTx); intro. (* Case 2.1: x was already in worklist, still is *) left. apply propagate_succ_list_incr_worklist. - simpl. elim H; intro. elim n0; auto. auto. + simpl. rewrite PICK in H. elim H; intro. congruence. auto. (* Case 2.2: x was not in worklist *) right; intros. case (In_dec peq s (successors n)); intro. @@ -449,13 +443,13 @@ Proof. eapply (PrimIter.iterate_prop _ _ step good_state). intros st GOOD. unfold step. - caseEq (st.(st_wrk)). + caseEq (NS.pick st.(st_wrk)). + intros [n rem] PICK. apply step_state_good; auto. intros. elim (GOOD n H0); intro. - rewrite H in H2. contradiction. + elim (NS.pick_none _ n H). auto. auto. - intros n rem WRK. apply step_state_good; auto. - eauto. apply start_state_good. eauto. + eauto. apply start_state_good. auto. Qed. (** As a consequence of the monotonicity property, the result of @@ -587,12 +581,12 @@ End BACKWARD_DATAFLOW_SOLVER. semi-lattice structure, by applying the forward dataflow solver with the predecessor relation instead of the successor relation. *) -Module Backward_Dataflow_Solver (LAT: SEMILATTICE): +Module Backward_Dataflow_Solver (LAT: SEMILATTICE) (NS: NODE_SET): BACKWARD_DATAFLOW_SOLVER with Module L := LAT. Module L := LAT. -Module DS := Dataflow_Solver L. +Module DS := Dataflow_Solver L NS. Section Kildall. @@ -1081,3 +1075,150 @@ End Solver. End BBlock_solver. +(** ** Node sets *) + +(** We now define implementations of the [NODE_SET] interface + appropriate for forward and backward dataflow analysis. + As mentioned earlier, we aim for a traversal of the CFG nodes + in reverse postorder (for forward analysis) or postorder + (for backward analysis). We take advantage of the following + fact, valid for all CFG generated by translation from Cminor: + the enumeration [n-1], [n-2], ..., 3, 2, 1 where [n] is the + top CFG node is a reverse postorder traversal. + Therefore, for forward analysis, we will use an implementation + of [NODE_SET] where the greatest node in the working list + is selected by the [pick] operation. For backward analysis, + we will similarly pick the smallest node in the working list. *) + +Require Import FSets. +Require Import FSetAVL. + +Module OrderedPositive <: OrderedType with Definition t := positive. + Definition t := positive. + Definition eq (x y: t) := x = y. + Definition lt := Plt. + + Lemma eq_refl : forall x : t, eq x x. + Proof. unfold eq; auto. Qed. + + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof. unfold eq; auto. Qed. + + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof. unfold eq; intros. transitivity y; auto. Qed. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof Plt_trans. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof Plt_ne. + + Lemma compare : forall x y : t, Compare lt eq x y. + Proof. + intros. + caseEq (Zcompare (Zpos x) (Zpos y)); intros. + apply EQ. unfold eq. generalize (Zcompare_Eq_eq _ _ H). congruence. + apply LT. exact H. + apply GT. rewrite Zcompare_Gt_Lt_antisym in H. exact H. + Qed. +End OrderedPositive. + +Module PositiveSet := FSetAVL.Make(OrderedPositive). +Module PositiveSetFacts := FSetFacts.Facts(PositiveSet). + +Module NodeSetForward <: NODE_SET. + Definition t := PositiveSet.t. + Definition add (n: positive) (s: t) : t := PositiveSet.add n s. + Definition pick (s: t) := + match PositiveSet.max_elt s with + | Some n => Some(n, PositiveSet.remove n s) + | None => None + end. + Definition initial (top: positive) := + positive_rec t PositiveSet.empty PositiveSet.add top. + + Definition In := PositiveSet.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'). + 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. + congruence. + apply PositiveSet.max_elt_3. 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. + congruence. + Qed. + + Lemma initial_spec: + forall numnodes n, Plt n numnodes -> In n (initial numnodes). + Proof. + intros numnodes; pattern numnodes. + apply positive_Peano_ind; unfold initial; intros. + assert (Zpos n > 0). compute; auto. red in H. omegaContradiction. + rewrite positive_rec_succ. rewrite PositiveSetFacts.add_iff. + elim (Plt_succ_inv _ _ H0); intro. + right. apply H. auto. + left. red. red. auto. + Qed. +End NodeSetForward. + +Module NodeSetBackward <: NODE_SET. + Definition t := PositiveSet.t. + Definition add (n: positive) (s: t) : t := PositiveSet.add n s. + Definition pick (s: t) := + match PositiveSet.min_elt s with + | Some n => Some(n, PositiveSet.remove n s) + | None => None + end. + Definition initial (top: positive) := + positive_rec t PositiveSet.empty PositiveSet.add top. + + Definition In := PositiveSet.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. + congruence. + apply PositiveSet.min_elt_3. 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. + congruence. + Qed. + + Lemma initial_spec: + forall numnodes n, Plt n numnodes -> In n (initial numnodes). + Proof NodeSetForward.initial_spec. +End NodeSetBackward. + -- cgit v1.2.3