From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Kildall.v | 1167 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 740 insertions(+), 427 deletions(-) (limited to 'backend/Kildall.v') diff --git a/backend/Kildall.v b/backend/Kildall.v index a071f305..0d414d28 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -25,7 +25,7 @@ Local Unset Case Analysis Schemes. - [X(s) >= transf n X(n)] if program point [s] is a successor of program point [n] - [X(n) >= a] - if [(n, a)] belongs to a given list of (program points, approximations). + if [n] is an entry point and [a] its minimal approximation. The unknowns are the [X(n)], indexed by program points (e.g. nodes in the CFG graph of a RTL function). They range over a given ordered set that @@ -39,7 +39,7 @@ Symmetrically, a backward dataflow problem is a set of inequations of the form - [X(n) >= transf s X(s)] if program point [s] is a successor of program point [n] - [X(n) >= a] - if [(n, a)] belongs to a given list of (program points, approximations). + if [n] is an entry point and [a] its minimal approximation. The only difference with a forward dataflow problem is that the transfer function [transf] now computes the approximation before a program point [s] @@ -59,11 +59,6 @@ approximations do not exist or are too expensive to compute. *) (** * Solving forward dataflow problems using Kildall's algorithm *) -Definition successors_list (successors: PTree.t (list positive)) (pc: positive) : list positive := - match successors!pc with None => nil | Some l => l end. - -Notation "a !!! b" := (successors_list a b) (at level 1). - (** A forward dataflow solver has the following generic interface. Unknowns range over the type [L.t], which is equipped with semi-lattice operations (see file [Lattice]). *) @@ -72,53 +67,52 @@ Module Type DATAFLOW_SOLVER. Declare Module L: SEMILATTICE. + (** [fixpoint successors transf ep ev] is the solver. + It returns either an error or a mapping from program points to + values of type [L.t] representing the solution. [successors] + is a finite map returning the list of successors of the given program + point. [transf] is the transfer function, [ep] the entry point, + and [ev] the minimal abstract value for [ep]. *) + Variable fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t) - (entrypoints: list (positive * L.t)), + (ep: positive) (ev: L.t), option (PMap.t L.t). - (** [fixpoint successors transf entrypoints] is the solver. - It returns either an error or a mapping from program points to - values of type [L.t] representing the solution. [successors] - is a finite map returning the list of successors of the given program - point. [transf] is the transfer function, and [entrypoints] the additional - constraints imposed on the solution. *) + (** The [fixpoint_solution] theorem shows that the returned solution, + if any, satisfies the dataflow inequations. *) Hypothesis fixpoint_solution: - forall A (code: PTree.t A) successors transf entrypoints res n instr s, - fixpoint code successors transf entrypoints = Some res -> + forall A (code: PTree.t A) successors transf ep ev res n instr s, + fixpoint code successors transf ep ev = Some res -> code!n = Some instr -> In s (successors instr) -> + (forall n, L.eq (transf n L.bot) L.bot) -> L.ge res!!s (transf n res!!n). - (** The [fixpoint_solution] theorem shows that the returned solution, - if any, satisfies the dataflow inequations. *) + (** The [fixpoint_entry] theorem shows that the returned solution, + if any, satisfies the additional constraint over the entry point. *) Hypothesis fixpoint_entry: - forall A (code: PTree.t A) successors transf entrypoints res n v, - fixpoint code successors transf entrypoints = Some res -> - In (n, v) entrypoints -> - L.ge res!!n v. + forall A (code: PTree.t A) successors transf ep ev res, + fixpoint code successors transf ep ev = Some res -> + L.ge res!!ep ev. - (** The [fixpoint_entry] theorem shows that the returned solution, - if any, satisfies the additional constraints expressed - by [entrypoints]. *) + (** Finally, any property that is preserved by [L.lub] and [transf] + and that holds for [L.bot] also holds for the results of + the analysis. *) Hypothesis fixpoint_invariant: - forall A (code: PTree.t A) successors transf entrypoints + forall A (code: PTree.t A) successors transf ep ev (P: L.t -> Prop), P L.bot -> (forall x y, P x -> P y -> P (L.lub x y)) -> (forall pc instr x, code!pc = Some instr -> P x -> P (transf pc x)) -> - (forall n v, In (n, v) entrypoints -> P v) -> + P ev -> forall res pc, - fixpoint code successors transf entrypoints = Some res -> + fixpoint code successors transf ep ev = Some res -> P res!!pc. - (** Finally, any property that is preserved by [L.lub] and [transf] - and that holds for [L.bot] also holds for the results of - the analysis. *) - End DATAFLOW_SOLVER. (** Kildall's algorithm manipulates worklists, which are sets of CFG nodes @@ -131,11 +125,14 @@ End DATAFLOW_SOLVER. Module Type NODE_SET. Variable t: Type. + Variable empty: t. Variable add: positive -> t -> t. Variable pick: t -> option (positive * t). - Variable initial: forall {A: Type}, PTree.t A -> t. + Variable all_nodes: forall {A: Type}, PTree.t A -> t. Variable In: positive -> t -> Prop. + Hypothesis empty_spec: + forall n, ~In n empty. Hypothesis add_spec: forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. Hypothesis pick_none: @@ -143,16 +140,48 @@ Module Type NODE_SET. 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: + Hypothesis all_nodes_spec: forall A (code: PTree.t A) n instr, - code!n = Some instr -> In n (initial code). + code!n = Some instr -> In n (all_nodes code). End NODE_SET. -(** We now define a generic solver that works over - any semi-lattice structure. *) +(** Reachability in a control-flow graph. *) -Module Dataflow_Solver (LAT: SEMILATTICE) (NS: NODE_SET): +Section REACHABLE. + +Context {A: Type} (code: PTree.t A) (successors: A -> list positive). + +Inductive reachable: positive -> positive -> Prop := + | reachable_refl: forall n, reachable n n + | reachable_left: forall n1 n2 n3 i, + code!n1 = Some i -> In n2 (successors i) -> reachable n2 n3 -> + reachable n1 n3. + +Scheme reachable_ind := Induction for reachable Sort Prop. + +Lemma reachable_trans: + forall n1 n2, reachable n1 n2 -> forall n3, reachable n2 n3 -> reachable n1 n3. +Proof. + induction 1; intros. +- auto. +- econstructor; eauto. +Qed. + +Lemma reachable_right: + forall n1 n2 n3 i, + reachable n1 n2 -> code!n2 = Some i -> In n3 (successors i) -> + reachable n1 n3. +Proof. + intros. apply reachable_trans with n2; auto. econstructor; eauto. constructor. +Qed. + +End REACHABLE. + +(** We now define a generic solver for forward dataflow inequations + that works over any semi-lattice structure. *) + +Module Dataflow_Solver (LAT: SEMILATTICE) (NS: NODE_SET) <: DATAFLOW_SOLVER with Module L := LAT. Module L := LAT. @@ -163,61 +192,64 @@ Context {A: Type}. Variable code: PTree.t A. Variable successors: A -> list positive. Variable transf: positive -> L.t -> L.t. -Variable entrypoints: list (positive * L.t). -(** The state of the iteration has two components: -- A mapping from program points to values of type [L.t] representing +(** The state of the iteration has three components: +- [aval]: A mapping from program points to values of type [L.t] representing the candidate solution found so far. -- A worklist of program points that remain to be considered. +- [worklist]: A worklist of program points that remain to be considered. +- [visited]: A set of program points that were visited already + (i.e. put on the worklist at some point in the past). + +Only the first two components are computationally relevant. The third +is a ghost variable used only for stating and proving invariants. +For this reason, [visited] is defined at sort [Prop] so that it is +erased during program extraction. *) Record state : Type := - mkstate { st_in: PMap.t L.t; st_wrk: NS.t }. + mkstate { aval: PTree.t L.t; worklist: NS.t; visited: positive -> Prop }. + +Definition abstr_value (n: positive) (s: state) : L.t := + match s.(aval)!n with + | None => L.bot + | Some v => v + end. (** Kildall's algorithm, in pseudo-code, is as follows: << - while st_wrk is not empty, do - extract a node n from st_wrk - compute out = transf n st_in[n] + while worklist is not empty, do + extract a node n from worklist + compute out = transf n aval[n] for each successor s of n: - compute in = lub st_in[s] out - if in <> st_in[s]: - st_in[s] := in - st_wrk := st_wrk union {s} + compute in = lub aval[s] out + if in <> aval[s]: + aval[s] := in + worklist := worklist union {s} + visited := visited union {s} end if end for end while - return st_in + return aval >> - -The initial state is built as follows: -- The initial mapping sets all program points to [L.bot], except - those mentioned in the [entrypoints] list, for which we take - the associated approximation as initial value. Since a program - point can be mentioned several times in [entrypoints], with different - approximations, we actually take the l.u.b. of these approximations. -- The initial worklist contains all the program points. *) - -Fixpoint start_state_in (ep: list (positive * L.t)) : PMap.t L.t := - match ep with - | nil => - PMap.init L.bot - | (n, v) :: rem => - let m := start_state_in rem in PMap.set n (L.lub m!!n v) m - end. - -Definition start_state := - mkstate (start_state_in entrypoints) (NS.initial code). +*) (** [propagate_succ] corresponds, in the pseudocode, to the body of the [for] loop iterating over all successors. *) Definition propagate_succ (s: state) (out: L.t) (n: positive) := - let oldl := s.(st_in)!!n in - let newl := L.lub oldl out in - if L.beq oldl newl - then s - else mkstate (PMap.set n newl s.(st_in)) (NS.add n s.(st_wrk)). + match s.(aval)!n with + | None => + {| aval := PTree.set n out s.(aval); + worklist := NS.add n s.(worklist); + visited := fun p => p = n \/ s.(visited) p |} + | Some oldl => + let newl := L.lub oldl out in + if L.beq oldl newl + then s + else {| aval := PTree.set n newl s.(aval); + worklist := NS.add n s.(worklist); + visited := fun p => p = n \/ s.(visited) p |} + end. (** [propagate_succ_list] corresponds, in the pseudocode, to the [for] loop iterating over all successors. *) @@ -233,366 +265,530 @@ Fixpoint propagate_succ_list (s: state) (out: L.t) (succs: list positive) pseudocode. *) Definition step (s: state) : PMap.t L.t + state := - match NS.pick s.(st_wrk) with + match NS.pick s.(worklist) with | None => - inl _ s.(st_in) + inl _ (L.bot, s.(aval)) | Some(n, rem) => match code!n with - | None => inr _ (mkstate s.(st_in) rem) + | None => + inr _ {| aval := s.(aval); worklist := rem; visited := s.(visited) |} | Some instr => inr _ (propagate_succ_list - (mkstate s.(st_in) rem) - (transf n s.(st_in)!!n) + {| aval := s.(aval); worklist := rem; visited := s.(visited) |} + (transf n (abstr_value n s)) (successors instr)) end end. (** The whole fixpoint computation is the iteration of [step] from - the start state. *) + an initial state. *) -Definition fixpoint : option (PMap.t L.t) := - PrimIter.iterate _ _ step start_state. +Definition fixpoint_from (start: state) : option (PMap.t L.t) := + PrimIter.iterate _ _ step start. -(** ** Monotonicity properties *) +(** There are several ways to build the initial state. For forward + dataflow analyses, the initial worklist is the function entry point, + and the initial mapping sets the function entry point to the given + abstract value, and leaves unset all other program points, which + corresponds to [L.bot] initial abstract values. *) + +Definition start_state (enode: positive) (eval: L.t) := + {| aval := PTree.set enode eval (PTree.empty L.t); + worklist := NS.add enode NS.empty; + visited := fun n => n = enode |}. + +Definition fixpoint (enode: positive) (eval: L.t) := + fixpoint_from (start_state enode eval). -(** We first show that the [st_in] part of the state evolves monotonically: - at each step, the values of the [st_in[n]] either remain the same or - increase with respect to the [L.ge] ordering. *) +(** For backward analyses (viewed as forward analyses on the reversed CFG), + the following two variants are more useful. Both start with an + empty initial mapping, where all program points start at [L.bot]. + The first initializes the worklist with a given set of entry points + in the reversed CFG. (See the backward dataflow solver below for + how this list is computed.) The second start state construction + initializes the worklist with all program points of the given CFG. *) -Definition in_incr (in1 in2: PMap.t L.t) : Prop := - forall n, L.ge in2!!n in1!!n. +Definition start_state_nodeset (enodes: NS.t) := + {| aval := PTree.empty L.t; + worklist := enodes; + visited := fun n => NS.In n enodes |}. -Lemma in_incr_refl: - forall in1, in_incr in1 in1. +Definition fixpoint_nodeset (enodes: NS.t) := + fixpoint_from (start_state_nodeset enodes). + +Definition start_state_allnodes := + {| aval := PTree.empty L.t; + worklist := NS.all_nodes code; + visited := fun n => exists instr, code!n = Some instr |}. + +Definition fixpoint_allnodes := + fixpoint_from start_state_allnodes. + +(** ** Characterization of the propagation functions *) + +Inductive optge: option L.t -> option L.t -> Prop := + | optge_some: forall l l', + L.ge l l' -> optge (Some l) (Some l') + | optge_none: forall ol, + optge ol None. + +Remark optge_refl: forall ol, optge ol ol. +Proof. destruct ol; constructor. apply L.ge_refl; apply L.eq_refl. Qed. + +Remark optge_trans: forall ol1 ol2 ol3, optge ol1 ol2 -> optge ol2 ol3 -> optge ol1 ol3. Proof. - unfold in_incr; intros. apply L.ge_refl. apply L.eq_refl. + intros. inv H0. + inv H. constructor. eapply L.ge_trans; eauto. + constructor. Qed. -Lemma in_incr_trans: - forall in1 in2 in3, in_incr in1 in2 -> in_incr in2 in3 -> in_incr in1 in3. +Remark optge_abstr_value: + forall st st' n, + optge st.(aval)!n st'.(aval)!n -> + L.ge (abstr_value n st) (abstr_value n st'). Proof. - unfold in_incr; intros. apply L.ge_trans with in2!!n; auto. + intros. unfold abstr_value. inv H. auto. apply L.ge_bot. Qed. -Lemma propagate_succ_incr: +Lemma propagate_succ_charact: forall st out n, - in_incr st.(st_in) (propagate_succ st out n).(st_in). + let st' := propagate_succ st out n in + optge st'.(aval)!n (Some out) + /\ (forall s, n <> s -> st'.(aval)!s = st.(aval)!s) + /\ (forall s, optge st'.(aval)!s st.(aval)!s) + /\ (NS.In n st'.(worklist) \/ st'.(aval)!n = st.(aval)!n) + /\ (forall n', NS.In n' st.(worklist) -> NS.In n' st'.(worklist)) + /\ (forall n', NS.In n' st'.(worklist) -> n' = n \/ NS.In n' st.(worklist)) + /\ (forall n', st.(visited) n' -> st'.(visited) n') + /\ (forall n', st'.(visited) n' -> NS.In n' st'.(worklist) \/ st.(visited) n') + /\ (forall n', st.(aval)!n' = None -> st'.(aval)!n' <> None -> st'.(visited) n'). Proof. - unfold in_incr, propagate_succ; simpl; intros. - case (L.beq st.(st_in)!!n (L.lub st.(st_in)!!n out)). - apply L.ge_refl. apply L.eq_refl. - simpl. case (peq n n0); intro. - subst n0. rewrite PMap.gss. apply L.ge_lub_left. - rewrite PMap.gso; auto. apply L.ge_refl. apply L.eq_refl. + unfold propagate_succ; intros; simpl. + destruct st.(aval)!n as [v|] eqn:E; + [predSpec L.beq L.beq_correct v (L.lub v out) | idtac]. +- (* already there, unchanged *) + repeat split; intros. + + rewrite E. constructor. eapply L.ge_trans. apply L.ge_refl. apply H; auto. apply L.ge_lub_right. + + apply optge_refl. + + right; auto. + + auto. + + auto. + + auto. + + auto. + + congruence. +- (* already there, updated *) + simpl; repeat split; intros. + + rewrite PTree.gss. constructor. apply L.ge_lub_right. + + rewrite PTree.gso by auto. auto. + + rewrite PTree.gsspec. destruct (peq s n). + subst s. rewrite E. constructor. apply L.ge_lub_left. + apply optge_refl. + + rewrite NS.add_spec. auto. + + rewrite NS.add_spec. auto. + + rewrite NS.add_spec in H0. intuition. + + auto. + + destruct H0; auto. subst n'. rewrite NS.add_spec; auto. + + rewrite PTree.gsspec in H1. destruct (peq n' n). auto. congruence. +- (* not previously there, updated *) + simpl; repeat split; intros. + + rewrite PTree.gss. apply optge_refl. + + rewrite PTree.gso by auto. auto. + + rewrite PTree.gsspec. destruct (peq s n). + subst s. rewrite E. constructor. + apply optge_refl. + + rewrite NS.add_spec. auto. + + rewrite NS.add_spec. auto. + + rewrite NS.add_spec in H. intuition. + + auto. + + destruct H; auto. subst n'. rewrite NS.add_spec. auto. + + rewrite PTree.gsspec in H0. destruct (peq n' n). auto. congruence. Qed. -Lemma propagate_succ_list_incr: - forall out scs st, - in_incr st.(st_in) (propagate_succ_list st out scs).(st_in). +Lemma propagate_succ_list_charact: + forall out l st, + let st' := propagate_succ_list st out l in + (forall n, In n l -> optge st'.(aval)!n (Some out)) + /\ (forall n, ~In n l -> st'.(aval)!n = st.(aval)!n) + /\ (forall n, optge st'.(aval)!n st.(aval)!n) + /\ (forall n, NS.In n st'.(worklist) \/ st'.(aval)!n = st.(aval)!n) + /\ (forall n', NS.In n' st.(worklist) -> NS.In n' st'.(worklist)) + /\ (forall n', NS.In n' st'.(worklist) -> In n' l \/ NS.In n' st.(worklist)) + /\ (forall n', st.(visited) n' -> st'.(visited) n') + /\ (forall n', st'.(visited) n' -> NS.In n' st'.(worklist) \/ st.(visited) n') + /\ (forall n', st.(aval)!n' = None -> st'.(aval)!n' <> None -> st'.(visited) n'). Proof. - induction scs; simpl; intros. - apply in_incr_refl. - apply in_incr_trans with (propagate_succ st out a).(st_in). - apply propagate_succ_incr. auto. -Qed. + induction l; simpl; intros. +- repeat split; intros. + + contradiction. + + apply optge_refl. + + auto. + + auto. + + auto. + + auto. + + auto. + + congruence. +- generalize (propagate_succ_charact st out a). + set (st1 := propagate_succ st out a). + intros (A1 & A2 & A3 & A4 & A5 & A6 & A7 & A8 & A9). + generalize (IHl st1). + set (st2 := propagate_succ_list st1 out l). + intros (B1 & B2 & B3 & B4 & B5 & B6 & B7 & B8 & B9). clear IHl. + repeat split; intros. + + destruct H. + * subst n. eapply optge_trans; eauto. + * auto. + + rewrite B2 by tauto. apply A2; tauto. + + eapply optge_trans; eauto. + + destruct (B4 n). auto. + destruct (peq n a). + * subst n. destruct A4. left; auto. right; congruence. + * right. rewrite H. auto. + + eauto. + + exploit B6; eauto. intros [P|P]. auto. + exploit A6; eauto. intuition. + + eauto. + + specialize (B8 n'); specialize (A8 n'). intuition. + + destruct st1.(aval)!n' eqn:ST1. + apply B7. apply A9; auto. congruence. + apply B9; auto. +Qed. -Lemma fixpoint_incr: - forall res, - fixpoint = Some res -> in_incr (start_state_in entrypoints) res. +(** Characterization of [fixpoint_from]. *) + +Inductive steps: state -> state -> Prop := + | steps_base: forall s, steps s s + | steps_right: forall s1 s2 s3, steps s1 s2 -> step s2 = inr s3 -> steps s1 s3. + +Scheme steps_ind := Induction for steps Sort Prop. + +Lemma fixpoint_from_charact: + forall start res, + fixpoint_from start = Some res -> + exists st, steps start st /\ NS.pick st.(worklist) = None /\ res = (L.bot, st.(aval)). Proof. unfold fixpoint; intros. - change (start_state_in entrypoints) with start_state.(st_in). 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 (NS.pick st.(st_wrk)) as [ [n rem] | ]. - destruct (code!n) as [instr | ]. - 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. - auto. - auto. - eauto. - apply in_incr_refl. + (fun st => steps start st) + (fun res => exists st, steps start st /\ NS.pick (worklist st) = None /\ res = (L.bot, aval st))); eauto. + intros. destruct (step a) eqn:E. + exists a; split; auto. + unfold step in E. destruct (NS.pick (worklist a)) as [[n rem]|]. + destruct (code!n); discriminate. + inv E. auto. + eapply steps_right; eauto. + constructor. Qed. -(** ** Correctness invariant *) - -(** The following invariant is preserved at each iteration of Kildall's - algorithm: for all program points [n], either - [n] is in the worklist, or the inequations associated with [n] - ([st_in[s] >= transf n st_in[n]] for all successors [s] of [n]) - hold. In other terms, the worklist contains all nodes that do not - yet satisfy their inequations. *) - -Definition good_state (st: state) : Prop := - forall n, - NS.In n st.(st_wrk) \/ - (forall instr s, - code!n = Some instr -> - In s (successors instr) -> - L.ge st.(st_in)!!s (transf n st.(st_in)!!n)). +(** ** Monotonicity properties *) -(** We show that the start state satisfies the invariant, and that - the [step] function preserves it. *) +(** We first show that the [aval] and [visited] parts of the state +evolve monotonically: +- at each step, the values of the [aval[n]] either remain the same or + increase with respect to the [optge] ordering; +- every node visited in the past remains visited in the future. +*) -Lemma start_state_good: - good_state start_state. +Lemma step_incr: + forall n s1 s2, step s1 = inr s2 -> + optge s2.(aval)!n s1.(aval)!n /\ (s1.(visited) n -> s2.(visited) n). Proof. - unfold good_state, start_state; intros. - destruct (code!n) as [instr|] eqn:INSTR. - left; simpl. eapply NS.initial_spec; eauto. - right; intros. discriminate. + unfold step; intros. + destruct (NS.pick (worklist s1)) as [[p rem] | ]; try discriminate. + destruct (code!p) as [instr|]; inv H. + + generalize (propagate_succ_list_charact + (transf p (abstr_value p s1)) + (successors instr) + {| aval := aval s1; worklist := rem; visited := visited s1 |}). + simpl. + set (s' := propagate_succ_list {| aval := aval s1; worklist := rem; visited := visited s1 |} + (transf p (abstr_value p s1)) (successors instr)). + intros (A1 & A2 & A3 & A4 & A5 & A6 & A7 & A8 & A9). + auto. + + split. apply optge_refl. auto. Qed. -Lemma propagate_succ_charact: - forall st out n, - let st' := propagate_succ st out n in - L.ge st'.(st_in)!!n out /\ - (forall s, n <> s -> st'.(st_in)!!s = st.(st_in)!!s). +Lemma steps_incr: + forall n s1 s2, steps s1 s2 -> + optge s2.(aval)!n s1.(aval)!n /\ (s1.(visited) n -> s2.(visited) n). Proof. - unfold propagate_succ; intros; simpl. - predSpec L.beq L.beq_correct - ((st_in st) !! n) (L.lub (st_in st) !! n out). - split. - eapply L.ge_trans. apply L.ge_refl. apply H; auto. - apply L.ge_lub_right. - auto. - - simpl. split. - rewrite PMap.gss. - apply L.ge_lub_right. - intros. rewrite PMap.gso; auto. + induction 1. +- split. apply optge_refl. auto. +- destruct IHsteps. exploit (step_incr n); eauto. intros [P Q]. + split. eapply optge_trans; eauto. eauto. Qed. -Lemma propagate_succ_list_charact: - forall out scs st, - let st' := propagate_succ_list st out scs in - forall s, - (In s scs -> L.ge st'.(st_in)!!s out) /\ - (~(In s scs) -> st'.(st_in)!!s = st.(st_in)!!s). +(** ** Correctness invariant *) + +(** The following invariant is preserved at each iteration of Kildall's + algorithm: for all visited program point [n], either + [n] is in the worklist, or the inequations associated with [n] + ([aval[s] >= transf n aval[n]] for all successors [s] of [n]) + hold. In other terms, the worklist contains all nodes that were + visited but do not yet satisfy their inequations. + + The second part of the invariant shows that nodes that already have + an abstract value associated with them have been visited. *) + +Record good_state (st: state) : Prop := { + gs_stable: forall n, + st.(visited) n -> + NS.In n st.(worklist) \/ + (forall i s, + code!n = Some i -> In s (successors i) -> + optge st.(aval)!s (Some (transf n (abstr_value n st)))); + gs_defined: forall n v, + st.(aval)!n = Some v -> st.(visited) n +}. + +(** We show that the [step] function preserves this invariant. *) + +Lemma step_state_good: + forall st pc rem instr, + NS.pick st.(worklist) = Some (pc, rem) -> + code!pc = Some instr -> + good_state st -> + good_state (propagate_succ_list (mkstate st.(aval) rem st.(visited)) + (transf pc (abstr_value pc st)) + (successors instr)). Proof. - induction scs; simpl; intros. - tauto. - generalize (IHscs (propagate_succ st out a) s). intros [P Q]. - generalize (propagate_succ_charact st out a). intros [U V]. - split; intros. - elim H; intro. - subst s. - apply L.ge_trans with (propagate_succ st out a).(st_in)!!a. - apply propagate_succ_list_incr. assumption. - apply P. auto. - transitivity (propagate_succ st out a).(st_in)!!s. - apply Q. tauto. - apply V. tauto. + intros until instr; intros PICK CODEAT [GOOD1 GOOD2]. + generalize (NS.pick_some _ _ _ PICK); intro PICK2. + set (out := transf pc (abstr_value pc st)). + generalize (propagate_succ_list_charact out (successors instr) {| aval := aval st; worklist := rem; visited := visited st |}). + set (st' := propagate_succ_list {| aval := aval st; worklist := rem; visited := visited st |} out + (successors instr)). + simpl; intros (A1 & A2 & A3 & A4 & A5 & A6 & A7 & A8 & A9). + constructor; intros. +- (* stable *) + destruct (A8 n H); auto. destruct (A4 n); auto. + replace (abstr_value n st') with (abstr_value n st) + by (unfold abstr_value; rewrite H1; auto). + exploit GOOD1; eauto. intros [P|P]. ++ (* n was on the worklist *) + rewrite PICK2 in P; destruct P. + * (* node n is our node pc *) + subst n. fold out. right; intros. + assert (i = instr) by congruence. subst i. + apply A1; auto. + * (* n was already on the worklist *) + left. apply A5; auto. ++ (* n was stable before, still is *) + right; intros. apply optge_trans with st.(aval)!s; eauto. +- (* defined *) + destruct st.(aval)!n as [v'|] eqn:ST. + + apply A7. eapply GOOD2; eauto. + + apply A9; auto. congruence. Qed. -Lemma propagate_succ_incr_worklist: - forall st out n x, - NS.In x st.(st_wrk) -> NS.In x (propagate_succ st out n).(st_wrk). +Lemma step_state_good_2: + forall st pc rem, + good_state st -> + NS.pick (worklist st) = Some (pc, rem) -> + code!pc = None -> + good_state (mkstate st.(aval) rem st.(visited)). Proof. - intros. unfold propagate_succ. - case (L.beq (st_in st) !! n (L.lub (st_in st) !! n out)). - auto. - simpl. rewrite NS.add_spec. auto. + intros until rem; intros [GOOD1 GOOD2] PICK CODE. + generalize (NS.pick_some _ _ _ PICK); intro PICK2. + constructor; simpl; intros. +- (* stable *) + exploit GOOD1; eauto. intros [P | P]. + + rewrite PICK2 in P. destruct P; auto. + subst n. right; intros. congruence. + + right; exact P. +- (* defined *) + eapply GOOD2; eauto. Qed. -Lemma propagate_succ_list_incr_worklist: - forall out scs st x, - NS.In x st.(st_wrk) -> NS.In x (propagate_succ_list st out scs).(st_wrk). +Lemma steps_state_good: + forall st1 st2, steps st1 st2 -> good_state st1 -> good_state st2. Proof. - induction scs; simpl; intros. - auto. - apply IHscs. apply propagate_succ_incr_worklist. auto. + induction 1; intros. +- auto. +- unfold step in e. + destruct (NS.pick (worklist s2)) as [[n rem] | ] eqn:PICK; try discriminate. + destruct (code!n) as [instr|] eqn:CODE; inv e. + eapply step_state_good; eauto. + eapply step_state_good_2; eauto. Qed. -Lemma propagate_succ_records_changes: - forall st out n s, - let st' := propagate_succ st out n in - NS.In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s. +(** We show that initial states satisfy the invariant. *) + +Lemma start_state_good: + forall enode eval, good_state (start_state enode eval). Proof. - simpl. intros. unfold propagate_succ. - case (L.beq (st_in st) !! n (L.lub (st_in st) !! n out)). - right; auto. - case (peq s n); intro. - subst s. left. simpl. rewrite NS.add_spec. auto. - right. simpl. apply PMap.gso. auto. + intros. unfold start_state; constructor; simpl; intros. +- subst n. rewrite NS.add_spec; auto. +- rewrite PTree.gsspec in H. rewrite PTree.gempty in H. + destruct (peq n enode). auto. discriminate. Qed. -Lemma propagate_succ_list_records_changes: - forall out scs st s, - let st' := propagate_succ_list st out scs in - NS.In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s. +Lemma start_state_nodeset_good: + forall enodes, good_state (start_state_nodeset enodes). Proof. - induction scs; simpl; intros. - right; auto. - elim (propagate_succ_records_changes st out a s); intro. - left. apply propagate_succ_list_incr_worklist. auto. - rewrite <- H. auto. + intros. unfold start_state_nodeset; constructor; simpl; intros. +- left. auto. +- rewrite PTree.gempty in H. congruence. Qed. -Lemma step_state_good: - forall st n instr rem, - NS.pick st.(st_wrk) = Some(n, rem) -> - code!n = Some instr -> - good_state st -> - good_state (propagate_succ_list (mkstate st.(st_in) rem) - (transf n st.(st_in)!!n) - (successors instr)). +Lemma start_state_allnodes_good: + good_state start_state_allnodes. Proof. - unfold good_state. intros st n instr rem WKL INSTR GOOD x. - generalize (NS.pick_some _ _ _ WKL); intro PICK. - set (out := transf n st.(st_in)!!n). - elim (propagate_succ_list_records_changes - out (successors instr) (mkstate st.(st_in) rem) x). - intro; left; auto. - simpl; intros EQ. rewrite EQ. - (* Case 1: x = n *) - destruct (peq x n). subst x. - right; intros. - assert (instr0 = instr) by congruence. subst instr0. - elim (propagate_succ_list_charact out (successors instr) - (mkstate st.(st_in) rem) s); intros. - auto. - (* Case 2: x <> n *) - elim (GOOD x); intro. - (* Case 2.1: x was already in worklist, still is *) - left. apply propagate_succ_list_incr_worklist. - 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 instr)); intro. - (* Case 2.2.1: s is a successor of n, it may have increased *) - apply L.ge_trans with st.(st_in)!!s. - change st.(st_in)!!s with (mkstate st.(st_in) rem).(st_in)!!s. - apply propagate_succ_list_incr. - eauto. - (* Case 2.2.2: s is not a successor of n, it did not change *) - elim (propagate_succ_list_charact out (successors instr) - (mkstate st.(st_in) rem) s); intros. - rewrite H3. simpl. eauto. auto. + unfold start_state_allnodes; constructor; simpl; intros. +- destruct H as [instr CODE]. left. eapply NS.all_nodes_spec; eauto. +- rewrite PTree.gempty in H. congruence. Qed. -Lemma step_state_good_2: - forall st n rem, - good_state st -> - NS.pick (st_wrk st) = Some (n, rem) -> - code!n = None -> - good_state (mkstate st.(st_in) rem). +(** Reachability in final states. *) + +Lemma reachable_visited: + forall st, good_state st -> NS.pick st.(worklist) = None -> + forall p q, reachable code successors p q -> st.(visited) p -> st.(visited) q. Proof. - intros; red; intros; simpl. - destruct (H n0). - erewrite NS.pick_some in H2 by eauto. destruct H2; auto. - subst n0. right; intros; congruence. - right; auto. + intros st [GOOD1 GOOD2] PICK. induction 1; intros. +- auto. +- eapply IHreachable; eauto. + exploit GOOD1; eauto. intros [P | P]. + eelim NS.pick_none; eauto. + exploit P; eauto. intros OGE; inv OGE. eapply GOOD2; eauto. Qed. -(** ** Correctness of the solution returned by [iterate]. *) +(** ** Correctness of the solution returned by [fixpoint]. *) (** As a consequence of the [good_state] invariant, the result of - [fixpoint], if defined, is a solution of the dataflow inequations, - since [st_wrk] is empty when the iteration terminates. *) + [fixpoint], if defined, is a solution of the dataflow inequations. + This assumes that the transfer function maps [L.bot] to [L.bot]. *) Theorem fixpoint_solution: - forall res n instr s, - fixpoint = Some res -> + forall ep ev res n instr s, + fixpoint ep ev = Some res -> code!n = Some instr -> In s (successors instr) -> + (forall n, L.eq (transf n L.bot) L.bot) -> L.ge res!!s (transf n res!!n). Proof. - intros until s. unfold fixpoint. intros PI. revert n instr s. - pattern res. - eapply (PrimIter.iterate_prop _ _ step good_state). - - intros st GOOD. unfold step. - destruct (NS.pick st.(st_wrk)) as [[n rem] | ] eqn:PICK. - destruct (code!n) as [instr | ] eqn:INSTR. - apply step_state_good; auto. - eapply step_state_good_2; eauto. - intros. destruct (GOOD n). elim (NS.pick_none _ n PICK). auto. eauto. + unfold fixpoint; intros. + exploit fixpoint_from_charact; eauto. intros (st & STEPS & PICK & RES). + exploit steps_state_good; eauto. apply start_state_good. intros [GOOD1 GOOD2]. + rewrite RES; unfold PMap.get; simpl. + destruct st.(aval)!n as [v|] eqn:STN. +- destruct (GOOD1 n) as [P|P]; eauto. + eelim NS.pick_none; eauto. + exploit P; eauto. unfold abstr_value; rewrite STN. intros OGE; inv OGE. auto. +- apply L.ge_trans with L.bot. apply L.ge_bot. apply L.ge_refl. apply L.eq_sym. eauto. +Qed. + +(** Moreover, the result of [fixpoint], if defined, satisfies the additional + constraint given on the entry point. *) - eauto. apply start_state_good. +Theorem fixpoint_entry: + forall ep ev res, + fixpoint ep ev = Some res -> + L.ge res!!ep ev. +Proof. + unfold fixpoint; intros. + exploit fixpoint_from_charact; eauto. intros (st & STEPS & PICK & RES). + exploit (steps_incr ep); eauto. simpl. rewrite PTree.gss. intros [P Q]. + rewrite RES; unfold PMap.get; simpl. inv P; auto. Qed. -(** As a consequence of the monotonicity property, the result of - [fixpoint], if defined, is pointwise greater than or equal the - initial mapping. Therefore, it satisfies the additional constraints - stated in [entrypoints]. *) +(** For [fixpoint_allnodes], we show that the result is a solution + without assuming [transf n L.bot = L.bot]. *) -Lemma start_state_in_entry: - forall ep n v, - In (n, v) ep -> - L.ge (start_state_in ep)!!n v. +Theorem fixpoint_allnodes_solution: + forall res n instr s, + fixpoint_allnodes = Some res -> + code!n = Some instr -> + In s (successors instr) -> + L.ge res!!s (transf n res!!n). Proof. - induction ep; simpl; intros. - elim H. - elim H; intros. - subst a. rewrite PMap.gss. - 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. - auto. + unfold fixpoint_allnodes; intros. + exploit fixpoint_from_charact; eauto. intros (st & STEPS & PICK & RES). + exploit steps_state_good; eauto. apply start_state_allnodes_good. intros [GOOD1 GOOD2]. + exploit (steps_incr n); eauto. simpl. intros [U V]. + exploit (GOOD1 n). apply V. exists instr; auto. intros [P|P]. + eelim NS.pick_none; eauto. + exploit P; eauto. intros OGE. rewrite RES; unfold PMap.get; simpl. + inv OGE. assumption. Qed. -Theorem fixpoint_entry: - forall res n v, - fixpoint = Some res -> - In (n, v) entrypoints -> - L.ge res!!n v. +(** For [fixpoint_nodeset], we show that the result is a solution + at all program points that are reachable from the given entry points. *) + +Theorem fixpoint_nodeset_solution: + forall enodes res e n instr s, + fixpoint_nodeset enodes = Some res -> + NS.In e enodes -> + reachable code successors e n -> + code!n = Some instr -> + In s (successors instr) -> + L.ge res!!s (transf n res!!n). Proof. - intros. - apply L.ge_trans with (start_state_in entrypoints)!!n. - apply fixpoint_incr. auto. - apply start_state_in_entry. auto. + unfold fixpoint_nodeset; intros. + exploit fixpoint_from_charact; eauto. intros (st & STEPS & PICK & RES). + exploit steps_state_good; eauto. apply start_state_nodeset_good. intros GOOD. + exploit (steps_incr e); eauto. simpl. intros [U V]. + assert (st.(visited) n). + { eapply reachable_visited; eauto. } + destruct GOOD as [GOOD1 GOOD2]. + exploit (GOOD1 n); eauto. intros [P|P]. + eelim NS.pick_none; eauto. + exploit P; eauto. intros OGE. rewrite RES; unfold PMap.get; simpl. + inv OGE. assumption. Qed. (** ** Preservation of a property over solutions *) -Variable P: L.t -> Prop. -Hypothesis P_bot: P L.bot. -Hypothesis P_lub: forall x y, P x -> P y -> P (L.lub x y). -Hypothesis P_transf: forall pc instr x, code!pc = Some instr -> P x -> P (transf pc x). -Hypothesis P_entrypoints: forall n v, In (n, v) entrypoints -> P v. - Theorem fixpoint_invariant: - forall res pc, - fixpoint = Some res -> + forall ep ev + (P: L.t -> Prop) + (P_bot: P L.bot) + (P_lub: forall x y, P x -> P y -> P (L.lub x y)) + (P_transf: forall pc instr x, code!pc = Some instr -> P x -> P (transf pc x)) + (P_entrypoint: P ev) + res pc, + fixpoint ep ev = Some res -> P res!!pc. Proof. - assert (forall ep, - (forall n v, In (n, v) ep -> P v) -> - forall pc, P (start_state_in ep)!!pc). - induction ep; intros; simpl. - rewrite PMap.gi. auto. - simpl in H. - assert (P (start_state_in ep)!!pc). apply IHep. eauto. - destruct a as [n v]. rewrite PMap.gsspec. destruct (peq pc n). - apply P_lub. subst. auto. eapply H. left; reflexivity. auto. - set (inv := fun st => forall pc, P (st.(st_in)!!pc)). + intros. + set (inv := fun st => forall x, P (abstr_value x st)). + assert (inv (start_state ep ev)). + { + red; simpl; intros. unfold abstr_value, start_state; simpl. + rewrite PTree.gsspec. rewrite PTree.gempty. + destruct (peq x ep). auto. auto. + } assert (forall st v n, inv st -> P v -> inv (propagate_succ st v n)). - unfold inv, propagate_succ. intros. - destruct (LAT.beq (st_in st)!!n (LAT.lub (st_in st)!!n v)). - auto. simpl. rewrite PMap.gsspec. destruct (peq pc n). - apply P_lub. subst n; auto. auto. + { + unfold inv, propagate_succ. intros. + destruct (aval st)!n as [oldl|] eqn:E. + destruct (L.beq oldl (L.lub oldl v)). + auto. + unfold abstr_value. simpl. rewrite PTree.gsspec. destruct (peq x n). + apply P_lub; auto. replace oldl with (abstr_value n st). auto. + unfold abstr_value; rewrite E; auto. + apply H1. + unfold abstr_value. simpl. rewrite PTree.gsspec. destruct (peq x n). auto. + apply H1. + } assert (forall l st v, inv st -> P v -> inv (propagate_succ_list st v l)). + { induction l; intros; simpl. auto. apply IHl; auto. - assert (forall res, fixpoint = Some res -> forall pc, P res!!pc). - unfold fixpoint. intros res0 RES0. pattern res0. - eapply (PrimIter.iterate_prop _ _ step inv). - intros. unfold step. - destruct (NS.pick (st_wrk a)) as [[n rem] | ]. - destruct (code!n) as [instr | ] eqn:INSTR. - apply H1. auto. eapply P_transf; eauto. - assumption. - eauto. - eauto. - unfold inv, start_state; simpl. auto. - intros. auto. + } + assert (forall st1 st2, steps st1 st2 -> inv st1 -> inv st2). + { + induction 1; intros. + auto. + unfold step in e. destruct (NS.pick (worklist s2)) as [[n rem]|]; try discriminate. + destruct (code!n) as [instr|] eqn:INSTR; inv e. + apply H2. apply IHsteps; auto. eapply P_transf; eauto. apply IHsteps; auto. + apply IHsteps; auto. + } + unfold fixpoint in H. exploit fixpoint_from_charact; eauto. + intros (st & STEPS & PICK & RES). + replace (res!!pc) with (abstr_value pc st). eapply H3; eauto. + rewrite RES; auto. Qed. End Kildall. @@ -606,7 +802,12 @@ End Dataflow_Solver. successors. We exploit this observation to cheaply derive a backward solver from the forward solver. *) -(** ** Construction of the predecessor relation *) +(** ** Construction of the reversed flow graph (the predecessor relation) *) + +Definition successors_list (successors: PTree.t (list positive)) (pc: positive) : list positive := + match successors!pc with None => nil | Some l => l end. + +Notation "a !!! b" := (successors_list a b) (at level 1). Section Predecessor. @@ -672,6 +873,17 @@ Proof. contradiction. Qed. +Lemma reachable_predecessors: + forall p q, + reachable code successors p q -> + reachable make_predecessors (fun l => l) q p. +Proof. + induction 1. +- constructor. +- exploit make_predecessors_correct_2; eauto. intros [l [P Q]]. + eapply reachable_right; eauto. +Qed. + End Predecessor. (** ** Solving backward dataflow problems *) @@ -682,33 +894,40 @@ Module Type BACKWARD_DATAFLOW_SOLVER. Declare Module L: SEMILATTICE. + (** [fixpoint successors transf] is the solver. + It returns either an error or a mapping from program points to + values of type [L.t] representing the solution. [successors] + is a finite map returning the list of successors of the given program + point. [transf] is the transfer function. *) + Variable fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) - (transf: positive -> L.t -> L.t) - (entrypoints: list (positive * L.t)), + (transf: positive -> L.t -> L.t), option (PMap.t L.t). + (** The [fixpoint_solution] theorem shows that the returned solution, + if any, satisfies the backward dataflow inequations. *) + Hypothesis fixpoint_solution: - forall A (code: PTree.t A) successors transf entrypoints res n instr s, - fixpoint code successors transf entrypoints = Some res -> + forall A (code: PTree.t A) successors transf res n instr s, + fixpoint code successors transf = Some res -> code!n = Some instr -> In s (successors instr) -> + (forall n a, code!n = None -> L.eq (transf n a) L.bot) -> L.ge res!!n (transf s res!!s). - Hypothesis fixpoint_entry: - forall A (code: PTree.t A) successors transf entrypoints res n v, - fixpoint code successors transf entrypoints = Some res -> - In (n, v) entrypoints -> - L.ge res!!n v. + (** [fixpoint_allnodes] is a variant of [fixpoint], less algorithmically + efficient, but correct without any hypothesis on the transfer function. *) - Hypothesis fixpoint_invariant: - forall A (code: PTree.t A) successors transf entrypoints (P: L.t -> Prop), - P L.bot -> - (forall x y, P x -> P y -> P (L.lub x y)) -> - (forall pc x, P x -> P (transf pc x)) -> - (forall n v, In (n, v) entrypoints -> P v) -> - forall res pc, - fixpoint code successors transf entrypoints = Some res -> - P res!!pc. + Variable fixpoint_allnodes: + forall {A: Type} (code: PTree.t A) (successors: A -> list positive) + (transf: positive -> L.t -> L.t), + option (PMap.t L.t). + + Hypothesis fixpoint_allnodes_solution: + forall A (code: PTree.t A) successors transf res n instr s, + fixpoint_allnodes code successors transf = Some res -> + code!n = Some instr -> In s (successors instr) -> + L.ge res!!n (transf s res!!s). End BACKWARD_DATAFLOW_SOLVER. @@ -729,45 +948,127 @@ Context {A: Type}. Variable code: PTree.t A. Variable successors: A -> list positive. Variable transf: positive -> L.t -> L.t. -Variable entrypoints: list (positive * L.t). + +(** Finding entry points for the reverse control-flow graph. *) + +Section Exit_points. + +(** Assuming that the nodes of the CFG [code] are numbered in reverse + postorder (cf. pass [Renumber]), an edge from [n] to [s] is a + normal edge if [s < n] and a back-edge otherwise. + [sequential_node] returns [true] if the given node has at least one + normal outgoing edge. It returns [false] if the given node is an exit + node (no outgoing edges) or the final node of a loop body + (all outgoing edges are back-edges). As we prove later, the set + of all non-sequential node is an appropriate set of entry points + for exploring the reverse CFG. *) + +Definition sequential_node (pc: positive) (instr: A): bool := + existsb (fun s => match code!s with None => false | Some _ => plt s pc end) + (successors instr). + +Definition exit_points : NS.t := + PTree.fold + (fun ep pc instr => + if sequential_node pc instr + then ep + else NS.add pc ep) + code NS.empty. + +Lemma exit_points_charact: + forall n, + NS.In n exit_points <-> exists i, code!n = Some i /\ sequential_node n i = false. +Proof. + intros n. unfold exit_points. eapply PTree_Properties.fold_rec. +- (* extensionality *) + intros. rewrite <- H. auto. +- (* base case *) + simpl. split; intros. + eelim NS.empty_spec; eauto. + destruct H as [i [P Q]]. rewrite PTree.gempty in P. congruence. +- (* inductive case *) + intros. destruct (sequential_node k v) eqn:SN. + + rewrite H1. rewrite PTree.gsspec. destruct (peq n k). + subst. split; intros [i [P Q]]. congruence. inv P. congruence. + tauto. + + rewrite NS.add_spec. rewrite H1. rewrite PTree.gsspec. destruct (peq n k). + subst. split. intros. exists v; auto. auto. + split. intros [P | [i [P Q]]]. congruence. exists i; auto. + intros [i [P Q]]. right; exists i; auto. +Qed. + +Lemma reachable_exit_points: + forall pc i, + code!pc = Some i -> exists x, NS.In x exit_points /\ reachable code successors pc x. +Proof. + intros pc0. pattern pc0. apply (well_founded_ind Plt_wf). + intros pc HR i CODE. + destruct (sequential_node pc i) eqn:SN. +- (* at least one successor that decreases the pc *) + unfold sequential_node in SN. rewrite existsb_exists in SN. + destruct SN as [s [P Q]]. destruct (code!s) as [i'|] eqn:CS; try discriminate. InvBooleans. + exploit (HR s); eauto. intros [x [U V]]. + exists x; split; auto. eapply reachable_left; eauto. +- (* otherwise we are an exit point *) + exists pc; split. + rewrite exit_points_charact. exists i; auto. constructor. +Qed. + +(** The crucial property of exit points is that any nonempty node in the + CFG is reverse-reachable from an exit point. *) + +Lemma reachable_exit_points_predecessor: + forall pc i, + code!pc = Some i -> + exists x, NS.In x exit_points /\ reachable (make_predecessors code successors) (fun l => l) x pc. +Proof. + intros. exploit reachable_exit_points; eauto. intros [x [P Q]]. + exists x; split; auto. apply reachable_predecessors. auto. +Qed. + +End Exit_points. + +(** The efficient backward solver. *) Definition fixpoint := - DS.fixpoint + DS.fixpoint_nodeset (make_predecessors code successors) (fun l => l) - transf entrypoints. + transf exit_points. Theorem fixpoint_solution: forall res n instr s, fixpoint = Some res -> code!n = Some instr -> In s (successors instr) -> + (forall n a, code!n = None -> L.eq (transf n a) L.bot) -> L.ge res!!n (transf s res!!s). Proof. intros. exploit (make_predecessors_correct_2 code); eauto. intros [l [P Q]]. - eapply DS.fixpoint_solution; eauto. + destruct code!s as [instr'|] eqn:CS. +- exploit reachable_exit_points_predecessor. eexact CS. intros (ep & U & V). + unfold fixpoint in H. eapply DS.fixpoint_nodeset_solution; eauto. +- apply L.ge_trans with L.bot. apply L.ge_bot. + apply L.ge_refl. apply L.eq_sym. auto. Qed. -Theorem fixpoint_entry: - forall res n v, - fixpoint = Some res -> - In (n, v) entrypoints -> - L.ge res!!n v. -Proof. - intros. eapply DS.fixpoint_entry. eexact H. auto. -Qed. +(** The alternate solver that starts with all nodes of the CFG instead + of just the exit points. *) -Theorem fixpoint_invariant: - forall (P: L.t -> Prop), - P L.bot -> - (forall x y, P x -> P y -> P (L.lub x y)) -> - (forall pc x, P x -> P (transf pc x)) -> - (forall n v, In (n, v) entrypoints -> P v) -> - forall res pc, - fixpoint = Some res -> - P res!!pc. +Definition fixpoint_allnodes := + DS.fixpoint_allnodes + (make_predecessors code successors) (fun l => l) + transf. + +Theorem fixpoint_allnodes_solution: + forall res n instr s, + fixpoint_allnodes = Some res -> + code!n = Some instr -> In s (successors instr) -> + L.ge res!!n (transf s res!!s). Proof. - intros. - eapply DS.fixpoint_invariant with (code := make_predecessors code successors) (transf := transf); eauto. + intros. + exploit (make_predecessors_correct_2 code); eauto. intros [l [P Q]]. + unfold fixpoint_allnodes in H. + eapply DS.fixpoint_allnodes_solution; eauto. Qed. End Kildall. @@ -861,24 +1162,24 @@ Definition result := PMap.t L.t. *) Record state : Type := mkstate - { st_in: result; st_wrk: list positive }. + { aval: result; worklist: list positive }. (** The ``extended basic block'' algorithm, in pseudo-code, is as follows: << - st_wrk := the set of all points n having multiple predecessors - st_in := the mapping n -> L.top + worklist := the set of all points n having multiple predecessors + aval := the mapping n -> L.top - while st_wrk is not empty, do - extract a node n from st_wrk - compute out = transf n st_in[n] + while worklist is not empty, do + extract a node n from worklist + compute out = transf n aval[n] for each successor s of n: if s has only one predecessor (namely, n): - st_in[s] := out - st_wrk := st_wrk union {s} + aval[s] := out + worklist := worklist union {s} end if end for end while - return st_in + return aval >> **) @@ -892,22 +1193,22 @@ Fixpoint propagate_successors propagate_successors bb sl l st else propagate_successors bb sl l - (mkstate (PMap.set s1 l st.(st_in)) - (s1 :: st.(st_wrk))) + (mkstate (PMap.set s1 l st.(aval)) + (s1 :: st.(worklist))) end. Definition step (bb: bbmap) (st: state) : result + state := - match st.(st_wrk) with - | nil => inl _ st.(st_in) + match st.(worklist) with + | nil => inl _ st.(aval) | pc :: rem => match code!pc with | None => - inr _ (mkstate st.(st_in) rem) + inr _ (mkstate st.(aval) rem) | Some instr => inr _ (propagate_successors bb (successors instr) - (transf pc st.(st_in)!!pc) - (mkstate st.(st_in) rem)) + (transf pc st.(aval)!!pc) + (mkstate st.(aval) rem)) end end. @@ -989,34 +1290,34 @@ Qed. *) Definition state_invariant (st: state) : Prop := - (forall n, basic_block_map n = true -> st.(st_in)!!n = L.top) + (forall n, basic_block_map n = true -> st.(aval)!!n = L.top) /\ (forall n, - In n st.(st_wrk) \/ + In n st.(worklist) \/ (forall instr s, code!n = Some instr -> In s (successors instr) -> - L.ge st.(st_in)!!s (transf n st.(st_in)!!n))). + L.ge st.(aval)!!s (transf n st.(aval)!!n))). Lemma propagate_successors_charact1: forall bb succs l st, - incl st.(st_wrk) - (propagate_successors bb succs l st).(st_wrk). + incl st.(worklist) + (propagate_successors bb succs l st).(worklist). Proof. induction succs; simpl; intros. apply incl_refl. case (bb a). auto. - apply incl_tran with (a :: st_wrk st). + apply incl_tran with (a :: worklist st). apply incl_tl. apply incl_refl. - set (st1 := (mkstate (PMap.set a l (st_in st)) (a :: st_wrk st))). - change (a :: st_wrk st) with (st_wrk st1). + set (st1 := (mkstate (PMap.set a l (aval st)) (a :: worklist st))). + change (a :: worklist st) with (worklist st1). auto. Qed. Lemma propagate_successors_charact2: forall bb succs l st n, let st' := propagate_successors bb succs l st in - (In n succs -> bb n = false -> In n st'.(st_wrk) /\ st'.(st_in)!!n = l) -/\ (~In n succs \/ bb n = true -> st'.(st_in)!!n = st.(st_in)!!n). + (In n succs -> bb n = false -> In n st'.(worklist) /\ st'.(aval)!!n = l) +/\ (~In n succs \/ bb n = true -> st'.(aval)!!n = st.(aval)!!n). Proof. induction succs; simpl; intros. (* Base case *) @@ -1027,7 +1328,7 @@ Proof. split; intros. apply U; auto. elim H0; intro. subst a. congruence. auto. apply V. tauto. - set (st1 := mkstate (PMap.set a l (st_in st)) (a :: st_wrk st)). + set (st1 := mkstate (PMap.set a l (aval st)) (a :: worklist st)). elim (IHsuccs l st1 n); intros U V. split; intros. elim H0; intros. @@ -1069,7 +1370,7 @@ Proof. right; intros. assert (instr0 = instr) by congruence. subst instr0. elim (U s); intros C D. - replace (st1.(st_in)!!pc) with res!!pc. fold l. + replace (st1.(aval)!!pc) with res!!pc. fold l. destruct (basic_block_map s) eqn:BB. rewrite D. simpl. rewrite INV1. apply L.top_ge. auto. tauto. elim (C H0 (refl_equal _)). intros X Y. rewrite Y. apply L.refl_ge. @@ -1082,7 +1383,7 @@ Proof. (* Case 2.1: n was already in worklist, still is *) left. apply V. simpl. tauto. (* Case 2.2: n was not in worklist *) - assert (INV3: forall s instr', code!n = Some instr' -> In s (successors instr') -> st1.(st_in)!!s = res!!s). + assert (INV3: forall s instr', code!n = Some instr' -> In s (successors instr') -> st1.(aval)!!s = res!!s). (* Amazingly, successors of n do not change. The only way they could change is if they were successors of pc as well, but that gives them two different predecessors, so @@ -1181,7 +1482,7 @@ Qed. (** ** Preservation of a property over solutions *) Definition Pstate (st: state) : Prop := - forall pc, P st.(st_in)!!pc. + forall pc, P st.(aval)!!pc. Lemma propagate_successors_P: forall bb l, @@ -1204,9 +1505,9 @@ Proof. unfold fixpoint; intros. pattern res. eapply (PrimIter.iterate_prop _ _ (step basic_block_map) Pstate). - intros st PS. unfold step. destruct (st.(st_wrk)). + intros st PS. unfold step. destruct (st.(worklist)). apply PS. - assert (PS2: Pstate (mkstate st.(st_in) l)). + assert (PS2: Pstate (mkstate st.(aval) l)). red; intro; simpl. apply PS. destruct (code!p) as [instr|] eqn:CODE. apply propagate_successors_P. eauto. auto. @@ -1239,16 +1540,23 @@ Require Import Heaps. Module NodeSetForward <: NODE_SET. Definition t := PHeap.t. + Definition empty := PHeap.empty. Definition add (n: positive) (s: t) : t := PHeap.insert n s. Definition pick (s: t) := match PHeap.findMax s with | Some n => Some(n, PHeap.deleteMax s) | None => None end. - Definition initial {A: Type} (code: PTree.t A) := + Definition all_nodes {A: Type} (code: PTree.t A) := PTree.fold (fun s pc instr => PHeap.insert pc s) code PHeap.empty. Definition In := PHeap.In. + Lemma empty_spec: + forall n, ~In n empty. + Proof. + intros. apply PHeap.In_empty. + Qed. + Lemma add_spec: forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. Proof. @@ -1273,9 +1581,9 @@ Module NodeSetForward <: NODE_SET. congruence. Qed. - Lemma initial_spec: + Lemma all_nodes_spec: forall A (code: PTree.t A) n instr, - code!n = Some instr -> In n (initial code). + code!n = Some instr -> In n (all_nodes code). Proof. intros A code n instr. apply PTree_Properties.fold_rec with @@ -1292,16 +1600,21 @@ End NodeSetForward. Module NodeSetBackward <: NODE_SET. Definition t := PHeap.t. + Definition empty := PHeap.empty. Definition add (n: positive) (s: t) : t := PHeap.insert n s. Definition pick (s: t) := match PHeap.findMin s with | Some n => Some(n, PHeap.deleteMin s) | None => None end. - Definition initial {A: Type} (code: PTree.t A) := + Definition all_nodes {A: Type} (code: PTree.t A) := PTree.fold (fun s pc instr => PHeap.insert pc s) code PHeap.empty. Definition In := PHeap.In. + Lemma empty_spec: + forall n, ~In n empty. + Proof NodeSetForward.empty_spec. + Lemma add_spec: forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. Proof NodeSetForward.add_spec. @@ -1324,9 +1637,9 @@ Module NodeSetBackward <: NODE_SET. congruence. Qed. - Lemma initial_spec: + Lemma all_nodes_spec: forall A (code: PTree.t A) n instr, - code!n = Some instr -> In n (initial code). - Proof NodeSetForward.initial_spec. + code!n = Some instr -> In n (all_nodes code). + Proof NodeSetForward.all_nodes_spec. End NodeSetBackward. -- cgit