From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Kildall.v | 280 +++++++++++++----------------------------------------- 1 file changed, 66 insertions(+), 214 deletions(-) (limited to 'backend/Kildall.v') diff --git a/backend/Kildall.v b/backend/Kildall.v index 10b2e1d9..0210b73f 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -1,6 +1,7 @@ (** Solvers for dataflow inequations. *) Require Import Coqlib. +Require Import Iteration. Require Import Maps. Require Import Lattice. @@ -40,128 +41,6 @@ sets [X(n) = top] for all merge points [n], that is, program points having several predecessors. This solver is useful when least upper bounds of approximations do not exist or are too expensive to compute. *) -(** * Bounded iteration *) - -(** The three solvers proceed iteratively, increasing the value of one of - the unknowns [X(n)] at each iteration until a solution is reached. - This section defines the general form of iteration used. *) - -Section BOUNDED_ITERATION. - -Variables A B: Set. -Variable step: A -> B + A. - -(** The [step] parameter represents one step of the iteration. From a - current iteration state [a: A], it either returns a value of type [B], - meaning that iteration is over and that this [B] value is the final - result of the iteration, or a value [a' : A] which is the next state - of the iteration. - - The naive way to define the iteration is: -<< -Fixpoint iterate (a: A) : B := - match step a with - | inl b => b - | inr a' => iterate a' - end. ->> - However, this is a general recursion, not guaranteed to terminate, - and therefore not expressible in Coq. The standard way to work around - this difficulty is to use Noetherian recursion (Coq module [Wf]). - This requires that we equip the type [A] with a well-founded ordering [<] - (no infinite ascending chains) and we demand that [step] satisfies - [step a = inr a' -> a < a']. For the types [A] that are of interest to us - in this development, it is however very painful to define adequate - well-founded orderings, even though we know our iterations always - terminate. - - Instead, we choose to bound the number of iterations by an arbitrary - constant. [iterate] then becomes a function that can fail, - of type [A -> option B]. The [None] result denotes failure to reach - a result in the number of iterations prescribed, or, in other terms, - failure to find a solution to the dataflow problem. The compiler - passes that exploit dataflow analysis (the [Constprop], [CSE] and - [Allocation] passes) will, in this case, either fail ([Allocation]) - or turn off the optimization pass ([Constprop] and [CSE]). - - Since we know (informally) that our computations terminate, we can - take a very large constant as the maximal number of iterations. - Failure will therefore never happen in practice, but of - course our proofs also cover the failure case and show that - nothing bad happens in this hypothetical case either. *) - -Definition num_iterations := 1000000000000%positive. - -(** The simple definition of bounded iteration is: -<< -Fixpoint iterate (niter: nat) (a: A) {struct niter} : option B := - match niter with - | O => None - | S niter' => - match step a with - | inl b => b - | inr a' => iterate niter' a' - end - end. ->> - This function is structural recursive over the parameter [niter] - (number of iterations), represented here as a Peano integer (type [nat]). - However, we want to use very large values of [niter]. As Peano integers, - these values would be much too large to fit in memory. Therefore, - we must express iteration counts as a binary integer (type [positive]). - However, Peano induction over type [positive] is not structural recursion, - so we cannot define [iterate] as a Coq fixpoint and must use - Noetherian recursion instead. *) - -Definition iter_step (x: positive) - (next: forall y, Plt y x -> A -> option B) - (s: A) : option B := - match peq x xH with - | left EQ => None - | right NOTEQ => - match step s with - | inl res => Some res - | inr s' => next (Ppred x) (Ppred_Plt x NOTEQ) s' - end - end. - -Definition iterate: positive -> A -> option B := - Fix Plt_wf (fun _ => A -> option B) iter_step. - -(** We then prove the expected unrolling equations for [iterate]. *) - -Remark unroll_iterate: - forall x, iterate x = iter_step x (fun y _ => iterate y). -Proof. - unfold iterate; apply (Fix_eq Plt_wf (fun _ => A -> option B) iter_step). - intros. unfold iter_step. apply extensionality. intro s. - case (peq x xH); intro. auto. - rewrite H. auto. -Qed. - -Lemma iterate_base: - forall s, iterate 1%positive s = None. -Proof. - intro; rewrite unroll_iterate; unfold iter_step. - case (peq 1 1); congruence. -Qed. - -Lemma iterate_step: - forall x s, - iterate (Psucc x) s = - match step s with - | inl res => Some res - | inr s' => iterate x s' - end. -Proof. - intro; rewrite unroll_iterate; unfold iter_step; intros. - case (peq (Psucc x) 1); intro. - destruct x; simpl in e; discriminate. - rewrite Ppred_succ. auto. -Qed. - -End BOUNDED_ITERATION. - (** * Solving forward dataflow problems using Kildall's algorithm *) (** A forward dataflow solver has the following generic interface. @@ -316,7 +195,7 @@ Definition step (s: state) : PMap.t L.t + state := the start state. *) Definition fixpoint : option (PMap.t L.t) := - iterate _ _ step num_iterations start_state. + PrimIter.iterate _ _ step start_state. (** ** Monotonicity properties *) @@ -361,33 +240,24 @@ Proof. apply propagate_succ_incr. auto. Qed. -Lemma iterate_incr: - forall n st res, - iterate _ _ step n st = Some res -> - in_incr st.(st_in) res. -Proof. - intro n; pattern n. apply positive_Peano_ind; intros until res. - rewrite iterate_base. congruence. - rewrite iterate_step. unfold step. - destruct st.(st_wrk); intros. - injection H0; intro; subst res. - red; intros; apply L.ge_refl. - apply in_incr_trans with - (propagate_succ_list (mkstate (st_in st) l) - (transf p (st_in st)!!p) - (successors p)).(st_in). - change (st_in st) with (st_in (mkstate (st_in st) l)). - apply propagate_succ_list_incr. - apply H. auto. -Qed. - Lemma fixpoint_incr: forall res, fixpoint = Some res -> in_incr (start_state_in entrypoints) res. Proof. unfold fixpoint; intros. change (start_state_in entrypoints) with start_state.(st_in). - apply iterate_incr with num_iterations; auto. + eapply (PrimIter.iterate_prop _ _ step + (fun st => in_incr start_state.(st_in) st.(st_in)) + (fun res => in_incr start_state.(st_in) res)). + + intros st INCR. unfold step. + destruct st.(st_wrk) as [ | n rem ]. + auto. + 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. + + eauto. apply in_incr_refl. Qed. (** ** Correctness invariant *) @@ -563,30 +433,8 @@ Qed. (** ** Correctness of the solution returned by [iterate]. *) (** As a consequence of the [good_state] invariant, the result of - [iterate], if defined, is a solution of the dataflow inequations, - since [st_wrk] is empty when [iterate] terminates. *) - -Lemma iterate_solution: - forall niter st res n s, - good_state st -> - iterate _ _ step niter st = Some res -> - Plt n topnode -> In s (successors n) -> - L.ge res!!s (transf n res!!n). -Proof. - intro niter; pattern niter; apply positive_Peano_ind; intros until s. - rewrite iterate_base. congruence. - intro GS. rewrite iterate_step. - unfold step; caseEq (st.(st_wrk)). - intros. injection H1; intros; subst res. - elim (GS n H2); intro. - rewrite H0 in H4. elim H4. - auto. - intros. apply H with - (propagate_succ_list (mkstate st.(st_in) l) - (transf p st.(st_in)!!p) (successors p)). - apply step_state_good; auto. - auto. auto. auto. -Qed. + [fixpoint], if defined, is a solution of the dataflow inequations, + since [st_wrk] is empty when the iteration terminates. *) Theorem fixpoint_solution: forall res n s, @@ -594,10 +442,20 @@ Theorem fixpoint_solution: Plt n topnode -> In s (successors n) -> L.ge res!!s (transf n res!!n). Proof. - unfold fixpoint. intros. - apply iterate_solution with num_iterations start_state. - apply start_state_good. - auto. auto. auto. + assert (forall res, fixpoint = Some res -> + forall n s, Plt n topnode -> In s (successors n) -> + L.ge res!!s (transf n res!!n)). + unfold fixpoint. intros res PI. pattern res. + eapply (PrimIter.iterate_prop _ _ step good_state). + + intros st GOOD. unfold step. + caseEq (st.(st_wrk)). + intros. elim (GOOD n H0); intro. + rewrite H in H2. contradiction. + auto. + intros n rem WRK. apply step_state_good; auto. + + eauto. apply start_state_good. eauto. Qed. (** As a consequence of the monotonicity property, the result of @@ -936,8 +794,7 @@ Definition basic_block_list (bb: bbmap) : list positive := Definition fixpoint : option result := let bb := basic_block_map in - iterate _ _ (step bb) num_iterations - (mkstate (PMap.init L.top) (basic_block_list bb)). + PrimIter.iterate _ _ (step bb) (mkstate (PMap.init L.top) (basic_block_list bb)). (** ** Properties of predecessors and multiple-predecessors nodes *) @@ -1121,23 +978,6 @@ Proof. right. assumption. Qed. -Lemma analyze_invariant: - forall res count st, - iterate _ _ (step basic_block_map) count st = Some res -> - state_invariant st -> - state_invariant (mkstate res nil). -Proof. - intros until count. pattern count. - apply positive_Peano_ind; intros until st. - rewrite iterate_base. congruence. - rewrite iterate_step. unfold step at 1. case st; intros r w; simpl. - case w. - intros. replace res with r. auto. congruence. - intros pc wl. case (plt pc topnode); intros. - eapply H. eauto. apply propagate_successors_invariant; auto. - eapply H. eauto. eapply discard_top_worklist_invariant; eauto. -Qed. - Lemma initial_state_invariant: state_invariant (mkstate (PMap.init L.top) (basic_block_list basic_block_map)). Proof. @@ -1146,6 +986,27 @@ Proof. right. intros. repeat rewrite PMap.gi. apply L.top_ge. Qed. +Lemma analyze_invariant: + forall res, + fixpoint = Some res -> + state_invariant (mkstate res nil). +Proof. + unfold fixpoint; intros. pattern res. + eapply (PrimIter.iterate_prop _ _ (step basic_block_map) + state_invariant). + + intros st INV. destruct st as [stin stwrk]. + unfold step. simpl. caseEq stwrk. + intro. congruence. + + intros pc rem WRK. case (plt pc topnode); intro. + apply propagate_successors_invariant; auto. congruence. + eapply discard_top_worklist_invariant; eauto. congruence. + + eauto. apply initial_state_invariant. +Qed. + + (** ** Correctness of the returned solution *) Theorem fixpoint_solution: @@ -1154,10 +1015,9 @@ Theorem fixpoint_solution: Plt n topnode -> In s (successors n) -> L.ge res!!s (transf n res!!n). Proof. - unfold fixpoint. intros. assert (state_invariant (mkstate res nil)). - eapply analyze_invariant; eauto. apply initial_state_invariant. + eapply analyze_invariant; eauto. elim H2; simpl; intros. elim (H4 n H0); intros. contradiction. @@ -1169,10 +1029,9 @@ Theorem fixpoint_entry: fixpoint = Some res -> res!!entrypoint = L.top. Proof. - unfold fixpoint. intros. assert (state_invariant (mkstate res nil)). - eapply analyze_invariant; eauto. apply initial_state_invariant. + eapply analyze_invariant; eauto. elim H0; simpl; intros. apply H1. unfold basic_block_map, is_basic_block_head. fold predecessors. @@ -1201,28 +1060,21 @@ Proof. auto. apply H0. Qed. -Lemma analyze_P: - forall bb res count st, - iterate _ _ (step bb) count st = Some res -> - Pstate st -> - (forall pc, P res!!pc). -Proof. - intros until count; pattern count; apply positive_Peano_ind; intros until st. - rewrite iterate_base. congruence. - rewrite iterate_step; unfold step at 1; destruct st.(st_wrk). - intros. inversion H0. apply H1. - destruct (plt p topnode). - intros. eapply H. eauto. - apply propagate_successors_P. apply Ptransf. apply H1. - red; intro; simpl. apply H1. - intros. eauto. -Qed. - Theorem fixpoint_invariant: forall res pc, fixpoint = Some res -> P res!!pc. Proof. - intros. unfold fixpoint in H. eapply analyze_P; eauto. - red; intro; simpl. rewrite PMap.gi. apply Ptop. + unfold fixpoint; intros. pattern res. + eapply (PrimIter.iterate_prop _ _ (step basic_block_map) Pstate). + + intros st PS. unfold step. destruct (st.(st_wrk)). + apply PS. + assert (PS2: Pstate (mkstate st.(st_in) l)). + red; intro; simpl. apply PS. + case (plt p topnode); intro. + apply propagate_successors_P. auto. auto. + auto. + + eauto. red; intro; simpl. rewrite PMap.gi. apply Ptop. Qed. End Solver. -- cgit