Merge of branch value-analysis.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 740 insertions, 427 deletions

diff --git a/backend/Kildall.v b/backend/Kildall.v
index a071f30..0d414d2 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.