Cil2Csyntax: added goto and labels; added assignment between structs

Kildall: simplified the interface
Constprop, CSE, Allocation, Linearize: updated for the new Kildall
RTL, LTL: removed the well-formedness condition on the CFG, 
  it is no longer necessary with the new Kildall and it is problematic
  for validated optimizations.
Maps: more efficient implementation of PTree.fold.


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

14 files changed, 346 insertions, 349 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 2389a33..7d843e5 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -116,7 +116,7 @@ Module RegsetLat := LFSet(Regset).
 Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).
 
 Definition analyze (f: RTL.function): option (PMap.t Regset.t) :=
-  DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) nil.
+  DS.fixpoint (successors f)  (transfer f) nil.
 
 (** * Translation from RTL to LTL *)
 
@@ -171,16 +171,6 @@ Definition transf_instr
       Lreturn (option_map assign optarg)
   end.
 
-Lemma transf_body_wf:
-  forall (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc),
-  let tc := PTree.map (transf_instr f live assign) (RTL.fn_code f) in
-  forall (pc: node), Plt pc (RTL.fn_nextpc f) \/ tc!pc = None.
-Proof.
-  intros. elim (RTL.fn_code_wf f pc); intro.
-  left. auto. right. unfold tc. rewrite PTree.gmap.
-  unfold option_map. rewrite H. auto.
-Qed.
-
 Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t)
                       (assign: reg -> loc) : LTL.function :=
   LTL.mkfunction
@@ -188,9 +178,7 @@ Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t)
      (List.map assign (RTL.fn_params f))
      (RTL.fn_stacksize f)
      (PTree.map (transf_instr f live assign) (RTL.fn_code f))
-     (RTL.fn_entrypoint f)
-     (RTL.fn_nextpc f)
-     (transf_body_wf f live assign).
+     (RTL.fn_entrypoint f).
 
 (** The translation of a function performs liveness analysis,
   construction and coloring of the inference graph, and per-instruction
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 7e9334a..fc0a0f3 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -154,21 +154,19 @@ Proof.
 Qed.
 
 Lemma agree_succ:
-  forall n s rs ls live,
+  forall n s rs ls live i,
   analyze f = Some live ->
-  In s (RTL.successors f n) ->
+  f.(RTL.fn_code)!n = Some i ->
+  In s (RTL.successors_instr i) ->
   agree live!!n rs ls ->
   agree (transfer f s live!!s) rs ls.
 Proof.
   intros.
-  elim (RTL.fn_code_wf f n); intro.
-  elim (RTL.fn_code_wf f s); intro.
   apply agree_increasing with (live!!n).
   eapply DS.fixpoint_solution. unfold analyze in H; eauto.
-  auto. auto. auto. auto.
-  unfold transfer. rewrite H3.
-  red; intros. elim (Regset.empty_1 H4).
-  unfold RTL.successors in H0; rewrite H2 in H0; elim H0.
+  unfold RTL.successors, Kildall.successors_list. 
+  rewrite PTree.gmap. rewrite H0. simpl. auto.
+  auto.
 Qed.
 
 (** Some useful special cases of [agree_increasing]. *)
@@ -543,12 +541,11 @@ Ltac MatchStates :=
       eapply match_states_intro; eauto; MatchStates
   | H: (PTree.get ?pc _ = Some _) |- agree _ _ _ _ =>
       eapply agree_succ with (n := pc); eauto; MatchStates
-  | H: (PTree.get _ _ = Some _) |- In _ (RTL.successors _ _) =>
-      unfold RTL.successors; rewrite H; auto with coqlib
+  | |- In _ (RTL.successors_instr _) =>
+      unfold RTL.successors_instr; auto with coqlib
   | _ => idtac
   end.
 
-
 Lemma transl_find_function:
   forall ros f args lv rs ls alloc,
   RTL.find_function ge ros rs = Some f ->
@@ -659,7 +656,7 @@ Proof.
   econstructor; eauto.
   econstructor; eauto.
   intros. eapply agree_succ with (n := pc); eauto.
-  unfold RTL.successors; rewrite H; auto with coqlib.
+  simpl. auto.
   eapply agree_postcall; eauto.
 
   (* Itailcall *)
diff --git a/backend/CSE.v b/backend/CSE.v
index cad3503..ff8d41a 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -364,8 +364,7 @@ Definition transfer (f: function) (pc: node) (before: numbering) :=
   and effectively deactivates the CSE optimization. *)
 
 Definition analyze (f: RTL.function): PMap.t numbering :=
-  match Solver.fixpoint (successors f) f.(fn_nextpc) 
-                        (transfer f) f.(fn_entrypoint) with
+  match Solver.fixpoint (successors f) (transfer f) f.(fn_entrypoint) with
   | None => PMap.init empty_numbering
   | Some res => res
   end.
@@ -410,19 +409,6 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
 Definition transf_code (approxs: PMap.t numbering) (instrs: code) : code :=
   PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
 
-Lemma transf_code_wf:
-  forall f approxs,
-  (forall pc, Plt pc f.(fn_nextpc) \/ f.(fn_code)!pc = None) ->
-  (forall pc, Plt pc f.(fn_nextpc)
-      \/ (transf_code approxs f.(fn_code))!pc = None).
-Proof.
-  intros. 
-  elim (H pc); intro.
-  left; auto.
-  right. unfold transf_code. rewrite PTree.gmap. 
-  unfold option_map; rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   let approxs := analyze f in
   mkfunction
@@ -430,9 +416,7 @@ Definition transf_function (f: function) : function :=
         f.(fn_params)
         f.(fn_stacksize)
         (transf_code approxs f.(fn_code))
-        f.(fn_entrypoint)
-        f.(fn_nextpc)
-        (transf_code_wf f approxs f.(fn_code_wf)).
+        f.(fn_entrypoint).
 
 Definition transf_fundef (f: fundef) : fundef :=
   AST.transf_fundef transf_function f.
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 3751cec..14027bf 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -242,8 +242,7 @@ Theorem wf_analyze:
   forall f pc, wf_numbering (analyze f)!!pc.
 Proof.
   unfold analyze; intros.
-  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
-                          (transfer f) (fn_entrypoint f)).
+  caseEq (Solver.fixpoint (successors f) (transfer f) (fn_entrypoint f)).
   intros approx EQ.
   eapply Solver.fixpoint_invariant with (P := wf_numbering); eauto.
   exact wf_empty_numbering.   
@@ -689,22 +688,21 @@ End SATISFIABILITY.
   satisfiability at [pc']. *)
 
 Theorem analysis_correct_1:
-  forall ge sp rs m f pc pc',
-  In pc' (successors f pc) ->
+  forall ge sp rs m f pc pc' i,
+  f.(fn_code)!pc = Some i -> In pc' (successors_instr i) ->
   numbering_satisfiable ge sp rs m (transfer f pc (analyze f)!!pc) ->
   numbering_satisfiable ge sp rs m (analyze f)!!pc'.
 Proof.
-  intros until pc'.
+  intros until i.
   generalize (wf_analyze f pc).
   unfold analyze.
-  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
-                          (transfer f) (fn_entrypoint f)).
-  intros res FIXPOINT WF SUCC NS.
+  caseEq (Solver.fixpoint (successors f) (transfer f) (fn_entrypoint f)).
+  intros res FIXPOINT WF AT SUCC.
   assert (Numbering.ge res!!pc' (transfer f pc res!!pc)).
     eapply Solver.fixpoint_solution; eauto.
-    elim (fn_code_wf f pc); intro. auto.
-    unfold successors in SUCC; rewrite H in SUCC; contradiction.
-  apply H. auto.
+    unfold successors_list, successors. rewrite PTree.gmap.
+    rewrite AT. auto.
+  apply H.
   intros. rewrite PMap.gi. apply empty_numbering_satisfiable.
 Qed.
 
@@ -717,8 +715,7 @@ Proof.
           with empty_numbering.
   apply empty_numbering_satisfiable.
   unfold analyze.
-  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
-                          (transfer f) (fn_entrypoint f)).
+  caseEq (Solver.fixpoint (successors f) (transfer f) (fn_entrypoint f)).
   intros res FIXPOINT. 
   symmetry. change empty_numbering with Solver.L.top.
   eapply Solver.fixpoint_entry; eauto.
@@ -835,8 +832,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
   apply exec_Inop; auto.
   econstructor; eauto. 
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H; auto.
 
   (* Iop *)
@@ -854,8 +850,7 @@ Proof.
   congruence.
   intros. eapply exec_Iop'; eauto.
   econstructor; eauto.
-  apply analysis_correct_1 with pc.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H. 
   eapply add_op_satisfiable; eauto. apply wf_analyze.
 
@@ -874,8 +869,7 @@ Proof.
   congruence.
   intros. eapply exec_Iload'; eauto.
   econstructor; eauto.
-  apply analysis_correct_1 with pc.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   eapply add_load_satisfiable; eauto. apply wf_analyze.
 
@@ -885,8 +879,7 @@ Proof.
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Istore; eauto.
   econstructor; eauto.
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H.
   eapply kill_load_satisfiable; eauto. 
 
@@ -898,8 +891,7 @@ Proof.
   econstructor; eauto. 
   constructor; auto. 
   econstructor; eauto. 
-  intros. apply analysis_correct_1 with pc.
-  unfold successors; rewrite H; auto with coqlib.
+  intros. eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply empty_numbering_satisfiable.
 
@@ -914,16 +906,14 @@ Proof.
   econstructor; split.
   eapply exec_Icond_true; eauto. 
   econstructor; eauto.
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Icond false *)
   econstructor; split.
   eapply exec_Icond_false; eauto. 
   econstructor; eauto.
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Ireturn *)
diff --git a/backend/Kildall.v b/backend/Kildall.v
index 188a23f..83206f7 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -55,6 +55,11 @@ 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]).  *)
@@ -64,32 +69,30 @@ Module Type DATAFLOW_SOLVER.
   Declare Module L: SEMILATTICE.
 
   Variable fixpoint:
-    (positive -> list positive) ->
-    positive ->
-    (positive -> L.t -> L.t) ->
-    list (positive * L.t) ->
+    forall (successors: PTree.t (list positive))
+           (transf: positive -> L.t -> L.t)
+           (entrypoints: list (positive * L.t)),
     option (PMap.t L.t).
 
-  (** [fixpoint successors topnode transf entrypoints] is the solver.
+  (** [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 function returning the list of successors of the given program
-    point.  [topnode] is the maximal number of nodes considered.
-    [transf] is the transfer function, and [entrypoints] the additional
+    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. *)
 
   Hypothesis fixpoint_solution:
-    forall successors topnode transf entrypoints res n s,
-    fixpoint successors topnode transf entrypoints = Some res ->
-    Plt n topnode -> In s (successors n) ->
+    forall successors transf entrypoints res n s,
+    fixpoint successors transf entrypoints = Some res ->
+    In s successors!!!n ->
     L.ge res!!s (transf n res!!n).
 
   (** The [fixpoint_solution] theorem shows that the returned solution,
     if any, satisfies the dataflow inequations. *)
 
   Hypothesis fixpoint_entry:
-    forall successors topnode transf entrypoints res n v,
-    fixpoint successors topnode transf entrypoints = Some res ->
+    forall successors transf entrypoints res n v,
+    fixpoint successors transf entrypoints = Some res ->
     In (n, v) entrypoints ->
     L.ge res!!n v.
 
@@ -97,6 +100,21 @@ Module Type DATAFLOW_SOLVER.
     if any, satisfies the additional constraints expressed 
     by [entrypoints]. *)
 
+  Hypothesis fixpoint_invariant:
+    forall 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 successors transf entrypoints = 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
@@ -111,7 +129,7 @@ Module Type NODE_SET.
   Variable t: Type.
   Variable add: positive -> t -> t.
   Variable pick: t -> option (positive * t).
-  Variable initial: positive -> t.
+  Variable initial: PTree.t (list positive) -> t.
 
   Variable In: positive -> t -> Prop.
   Hypothesis add_spec:
@@ -122,7 +140,8 @@ Module Type NODE_SET.
     forall s n s', pick s = Some(n, s') ->
     forall n', In n' s <-> n = n' \/ In n' s'.
   Hypothesis initial_spec:
-    forall numnodes n, Plt n numnodes -> In n (initial numnodes).
+    forall successors n s,
+    successors!n = Some s -> In n (initial successors).
 
 End NODE_SET.
 
@@ -136,8 +155,7 @@ Module L := LAT.
 
 Section Kildall.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 Variable transf: positive -> L.t -> L.t.
 Variable entrypoints: list (positive * L.t).
 
@@ -172,7 +190,7 @@ The initial state is built as follows:
   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 up to [topnode]. *)
+- The initial worklist contains all the program points. *)
 
 Fixpoint start_state_in (ep: list (positive * L.t)) : PMap.t L.t :=
   match ep with
@@ -183,7 +201,7 @@ Fixpoint start_state_in (ep: list (positive * L.t)) : PMap.t L.t :=
   end.
 
 Definition start_state :=
-  mkstate (start_state_in entrypoints) (NS.initial topnode).
+  mkstate (start_state_in entrypoints) (NS.initial successors).
 
 (** [propagate_succ] corresponds, in the pseudocode,
   to the body of the [for] loop iterating over all successors. *)
@@ -216,7 +234,7 @@ Definition step (s: state) : PMap.t L.t + state :=
       inr _ (propagate_succ_list
               (mkstate s.(st_in) rem)
               (transf n s.(st_in)!!n)
-              (successors n))
+              (successors!!!n))
   end.
 
 (** The whole fixpoint computation is the iteration of [step] from
@@ -259,10 +277,10 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_incr:
-  forall out succs st,
-  in_incr st.(st_in) (propagate_succ_list st out succs).(st_in).
+  forall out scs st,
+  in_incr st.(st_in) (propagate_succ_list st out scs).(st_in).
 Proof.
-  induction succs; simpl; intros.
+  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.
@@ -291,7 +309,7 @@ Qed.
 (** ** Correctness invariant *)
 
 (** The following invariant is preserved at each iteration of Kildall's
-  algorithm: for all program points [n] below [topnode], either
+  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
@@ -299,10 +317,9 @@ Qed.
 
 Definition good_state (st: state) : Prop :=
   forall n,
-  Plt n topnode ->
   NS.In n st.(st_wrk) \/
-  (forall s, In s (successors n) -> 
-                L.ge st.(st_in)!!s (transf n st.(st_in)!!n)).
+  (forall s, In s (successors!!!n) ->
+             L.ge st.(st_in)!!s (transf n st.(st_in)!!n)).
 
 (** We show that the start state satisfies the invariant, and that
   the [step] function preserves it. *)
@@ -311,7 +328,9 @@ Lemma start_state_good:
   good_state start_state.
 Proof.
   unfold good_state, start_state; intros.
-  left; simpl. apply NS.initial_spec. auto.
+  case_eq (successors!n); intros.
+  left; simpl. eapply NS.initial_spec. eauto.
+  unfold successors_list. rewrite H. right; intros. contradiction.
 Qed.
 
 Lemma propagate_succ_charact:
@@ -337,15 +356,15 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_charact:
-  forall out succs st,
-  let st' := propagate_succ_list st out succs in
+  forall out scs st,
+  let st' := propagate_succ_list st out scs in
   forall s,
-  (In s succs -> L.ge st'.(st_in)!!s out) /\
-  (~(In s succs) -> st'.(st_in)!!s = st.(st_in)!!s).
+  (In s scs -> L.ge st'.(st_in)!!s out) /\
+  (~(In s scs) -> st'.(st_in)!!s = st.(st_in)!!s).
 Proof.
-  induction succs; simpl; intros.
+  induction scs; simpl; intros.
   tauto.
-  generalize (IHsuccs (propagate_succ st out a) s). intros [A B].
+  generalize (IHscs (propagate_succ st out a) s). intros [A B].
   generalize (propagate_succ_charact st out a). intros [C D].
   split; intros.
   elim H; intro.
@@ -369,12 +388,12 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_incr_worklist:
-  forall out succs st x,
-  NS.In x st.(st_wrk) -> NS.In x (propagate_succ_list st out succs).(st_wrk).
+  forall out scs st x,
+  NS.In x st.(st_wrk) -> NS.In x (propagate_succ_list st out scs).(st_wrk).
 Proof.
-  induction succs; simpl; intros.
+  induction scs; simpl; intros.
   auto.
-  apply IHsuccs. apply propagate_succ_incr_worklist. auto.
+  apply IHscs. apply propagate_succ_incr_worklist. auto.
 Qed.
 
 Lemma propagate_succ_records_changes:
@@ -391,11 +410,11 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_records_changes:
-  forall out succs st s,
-  let st' := propagate_succ_list st out succs in
+  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.
 Proof.
-  induction succs; simpl; intros.
+  induction scs; simpl; intros.
   right; auto.
   elim (propagate_succ_records_changes st out a s); intro.
   left. apply propagate_succ_list_incr_worklist. auto.
@@ -408,37 +427,37 @@ Lemma step_state_good:
   good_state st ->
   good_state (propagate_succ_list (mkstate st.(st_in) rem)
                                   (transf n st.(st_in)!!n)
-                                  (successors n)).
+                                  (successors!!!n)).
 Proof.
-  unfold good_state. intros st n rem WKL GOOD x LTx.
+  unfold good_state. intros st n rem WKL 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 n) (mkstate st.(st_in) rem) x).
+          out (successors!!!n) (mkstate st.(st_in) rem) x).
   intro; left; auto.
-  simpl; intro EQ. rewrite EQ.
+  simpl; intros EQ. rewrite EQ.
   (* Case 1: x = n *)
   case (peq x n); intro.
-  subst x. fold out.
+  subst x.
   right; intros.
-  elim (propagate_succ_list_charact out (successors n)
+  elim (propagate_succ_list_charact out (successors!!!n)
           (mkstate st.(st_in) rem) s); intros.
   auto.
   (* Case 2: x <> n *)
-  elim (GOOD x LTx); intro.
+  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 n)); intro.
+  case (In_dec peq s (successors!!!n)); 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. 
   auto.
   (* Case 2.2.2: s is not a successor of n, it did not change *)
-  elim (propagate_succ_list_charact out (successors n)
+  elim (propagate_succ_list_charact out (successors!!!n)
           (mkstate st.(st_in) rem) s); intros.
   rewrite H2. simpl. auto. auto.
 Qed.
@@ -452,23 +471,25 @@ Qed.
 Theorem fixpoint_solution:
   forall res n s,
   fixpoint = Some res ->
-  Plt n topnode -> In s (successors n) ->
+  In s (successors!!!n) ->
   L.ge res!!s (transf n res!!n).
 Proof.
   assert (forall res, fixpoint = Some res ->
-          forall n s, Plt n topnode -> In s (successors n) ->
-                      L.ge res!!s (transf n res!!n)).
+          forall n s,
+          In s successors!!!n ->
+          L.ge res!!s (transf n res!!n)).
   unfold fixpoint. intros res PI. pattern res. 
   eapply (PrimIter.iterate_prop _ _ step good_state).
 
   intros st GOOD. unfold step. 
   caseEq (NS.pick st.(st_wrk)). 
   intros [n rem] PICK. apply step_state_good; auto. 
-  intros. elim (GOOD n H0); intro. 
+  intros. 
+  elim (GOOD n); intro. 
   elim (NS.pick_none _ n H). auto.
   auto.
 
-  eauto. apply start_state_good. auto.
+  eauto. apply start_state_good. eauto.
 Qed.
 
 (** As a consequence of the monotonicity property, the result of
@@ -505,6 +526,49 @@ Proof.
   apply start_state_in_entry. auto.
 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 x, 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 ->
+  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)).
+  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.
+    auto.
+  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] | ].
+    apply H1. auto. apply P_transf. apply H2.
+    assumption.
+    eauto. 
+    unfold inv, start_state; simpl. auto. 
+  intros. auto.
+Qed.
+
 End Kildall.
 
 End Dataflow_Solver.
@@ -520,51 +584,53 @@ End Dataflow_Solver.
 
 Section Predecessor.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 
-Fixpoint add_successors (pred: PMap.t (list positive))
+Fixpoint add_successors (pred: PTree.t (list positive))
                         (from: positive) (tolist: list positive)
-                        {struct tolist} : PMap.t (list positive) :=
+                        {struct tolist} : PTree.t (list positive) :=
   match tolist with
   | nil => pred
-  | to :: rem =>
-      add_successors (PMap.set to (from :: pred!!to) pred) from rem
+  | to :: rem => add_successors (PTree.set to (from :: pred!!!to) pred) from rem
   end.
 
 Lemma add_successors_correct:
   forall tolist from pred n s,
-  In n pred!!s \/ (n = from /\ In s tolist) -> 
-  In n (add_successors pred from tolist)!!s.
+  In n pred!!!s \/ (n = from /\ In s tolist) -> 
+  In n (add_successors pred from tolist)!!!s.
 Proof.
   induction tolist; simpl; intros.
   tauto.
   apply IHtolist.
-  rewrite PMap.gsspec. case (peq s a); intro.
-  subst a. elim H; intro. left; auto with coqlib.
-  elim H0; intros. subst n. left; auto with coqlib.
-  intuition. elim n0; auto.
+  unfold successors_list at 1. rewrite PTree.gsspec. destruct (peq s a).
+  subst a. destruct H. auto with coqlib. 
+  destruct H. subst n. auto with coqlib. 
+  fold (successors_list pred s). intuition congruence.
 Qed.
 
-Definition make_predecessors : PMap.t (list positive) :=
-  positive_rec (PMap.t (list positive)) (PMap.init nil)
-    (fun n pred => add_successors pred n (successors n))
-    topnode.
+Definition make_predecessors : PTree.t (list positive) :=
+  PTree.fold add_successors successors (PTree.empty (list positive)).
 
 Lemma make_predecessors_correct:
   forall n s,
-  Plt n topnode ->
-  In s (successors n) ->
-  In n make_predecessors!!s.
+  In s successors!!!n ->
+  In n make_predecessors!!!s.
 Proof.
-  unfold make_predecessors. pattern topnode. 
-  apply positive_Peano_ind; intros.
-  compute in H. destruct n; discriminate.
-  rewrite positive_rec_succ.
-  apply add_successors_correct.
-  elim (Plt_succ_inv _ _ H0); intro.
-  left; auto.
-  right. subst x. tauto.
+  set (P := fun succ pred =>
+          forall n s, In s succ!!!n -> In n pred!!!s).
+  unfold make_predecessors.
+  apply PTree_Properties.fold_rec with (P := P).
+(* extensionality *)
+  unfold P; unfold successors_list; intros.
+  rewrite <- H in H1. auto.
+(* base case *)
+  red; unfold successors_list. intros n s. repeat rewrite PTree.gempty. auto.
+(* inductive case *)
+  unfold P; intros. apply add_successors_correct.
+  unfold successors_list in H2. rewrite PTree.gsspec in H2. 
+  destruct (peq n k).
+  subst k. auto.
+  fold (successors_list m n) in H2. auto.
 Qed.
 
 End Predecessor.
@@ -578,24 +644,33 @@ Module Type BACKWARD_DATAFLOW_SOLVER.
   Declare Module L: SEMILATTICE.
 
   Variable fixpoint:
-    (positive -> list positive) ->
-    positive ->
+    PTree.t (list positive) ->
     (positive -> L.t -> L.t) ->
     list (positive * L.t) ->
     option (PMap.t L.t).
 
   Hypothesis fixpoint_solution:
-    forall successors topnode transf entrypoints res n s,
-    fixpoint successors topnode transf entrypoints = Some res ->
-    Plt n topnode -> Plt s topnode -> In s (successors n) ->
+    forall successors transf entrypoints res n s,
+    fixpoint successors transf entrypoints = Some res ->
+    In s (successors!!!n) ->
     L.ge res!!n (transf s res!!s).
 
   Hypothesis fixpoint_entry:
-    forall successors topnode transf entrypoints res n v,
-    fixpoint successors topnode transf entrypoints = Some res ->
+    forall successors transf entrypoints res n v,
+    fixpoint successors transf entrypoints = Some res ->
     In (n, v) entrypoints ->
     L.ge res!!n v.
 
+  Hypothesis fixpoint_invariant:
+    forall 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 successors transf entrypoints = Some res ->
+    P res!!pc.
+
 End BACKWARD_DATAFLOW_SOLVER.
 
 (** We construct a generic backward dataflow solver, working over any
@@ -611,26 +686,22 @@ Module DS := Dataflow_Solver L NS.
 
 Section Kildall.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 Variable transf: positive -> L.t -> L.t.
 Variable entrypoints: list (positive * L.t).
 
 Definition fixpoint :=
-  let pred := make_predecessors successors topnode in
-  DS.fixpoint (fun s => pred!!s) topnode transf entrypoints.
+  DS.fixpoint (make_predecessors successors) transf entrypoints.
 
 Theorem fixpoint_solution:
   forall res n s,
   fixpoint = Some res ->
-  Plt n topnode -> Plt s topnode ->
-  In s (successors n) ->
+  In s (successors!!!n) ->
   L.ge res!!n (transf s res!!s).
 Proof.
   intros. apply DS.fixpoint_solution with
-    (fun s => (make_predecessors successors topnode)!!s) topnode entrypoints.
+    (make_predecessors successors) entrypoints.
   exact H.
-  assumption.
   apply make_predecessors_correct; auto.
 Qed.
 
@@ -641,10 +712,24 @@ Theorem fixpoint_entry:
   L.ge res!!n v.
 Proof.
   intros. apply DS.fixpoint_entry with
-    (fun s => (make_predecessors successors topnode)!!s) topnode transf entrypoints.
+    (make_predecessors successors) transf entrypoints.
   exact H. auto.
 Qed.
 
+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.
+Proof.
+  intros. apply DS.fixpoint_invariant with 
+    (make_predecessors successors) transf entrypoints; auto. 
+Qed.
+
 End Kildall.
 
 End Backward_Dataflow_Solver.
@@ -681,30 +766,29 @@ Module Type BBLOCK_SOLVER.
   Declare Module L: ORDERED_TYPE_WITH_TOP.
 
   Variable fixpoint:
-    (positive -> list positive) ->
-    positive ->
+    PTree.t (list positive) ->
     (positive -> L.t -> L.t) ->
     positive ->
     option (PMap.t L.t).
 
   Hypothesis fixpoint_solution:
-    forall successors topnode transf entrypoint res n s,
-    fixpoint successors topnode transf entrypoint = Some res ->
-    Plt n topnode -> In s (successors n) ->
+    forall successors transf entrypoint res n s,
+    fixpoint successors transf entrypoint = Some res ->
+    In s (successors!!!n) ->
     L.ge res!!s (transf n res!!n).
 
   Hypothesis fixpoint_entry:
-    forall successors topnode transf entrypoint res,
-    fixpoint successors topnode transf entrypoint = Some res ->
+    forall successors transf entrypoint res,
+    fixpoint successors transf entrypoint = Some res ->
     res!!entrypoint = L.top.
 
   Hypothesis fixpoint_invariant:
-    forall successors topnode transf entrypoint 
+    forall successors transf entrypoint 
            (P: L.t -> Prop),
     P L.top ->
     (forall pc x, P x -> P (transf pc x)) ->
     forall res pc,
-    fixpoint successors topnode transf entrypoint = Some res ->
+    fixpoint successors transf entrypoint = Some res ->
     P res!!pc.
 
 End BBLOCK_SOLVER.
@@ -719,8 +803,7 @@ Module L := LAT.
 
 Section Solver.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 Variable transf: positive -> L.t -> L.t.
 Variable entrypoint: positive.
 Variable P: L.t -> Prop.
@@ -748,9 +831,8 @@ Record state : Type := mkstate
         extract a node n from st_wrk
         compute out = transf n st_in[n]
         for each successor s of n:
-            compute in = lub st_in[s] out
             if s has only one predecessor (namely, n):
-                st_in[s] := in
+                st_in[s] := out
                 st_wrk := st_wrk union {s}
             end if
         end for
@@ -777,33 +859,29 @@ Definition step (bb: bbmap) (st: state) : result + state :=
   match st.(st_wrk) with
   | nil => inl _ st.(st_in)
   | pc :: rem =>
-      if plt pc topnode then
         inr _ (propagate_successors 
-                 bb (successors pc)
+                 bb (successors!!!pc)
                  (transf pc st.(st_in)!!pc)
                  (mkstate st.(st_in) rem))
-      else
-        inr _ (mkstate st.(st_in) rem)
   end.
 
 (** Recognition of program points that have more than one predecessor. *)
 
 Definition is_basic_block_head 
-    (preds: PMap.t (list positive)) (pc: positive) : bool :=
-  match preds!!pc with
-  | nil => true
-  | s :: nil => 
-      if peq s pc then true else
-      if peq pc entrypoint then true else false
-  | _ :: _ :: _ => true
-  end.
+    (preds: PTree.t (list positive)) (pc: positive) : bool :=
+  if peq pc entrypoint then true else
+    match preds!!!pc with
+    | nil => false
+    | s :: nil => peq s pc
+    | _ :: _ :: _ => true
+    end.
 
 Definition basic_block_map : bbmap :=
-  is_basic_block_head (make_predecessors successors topnode).
+  is_basic_block_head (make_predecessors successors).
 
 Definition basic_block_list (bb: bbmap) : list positive :=
-  positive_rec (list positive) nil
-    (fun pc l => if bb pc then pc :: l else  l) topnode.
+  PTree.fold (fun l pc scs => if bb pc then pc :: l else l)
+             successors nil.
 
 (** The computation of the approximate solution. *)
 
@@ -813,43 +891,45 @@ Definition fixpoint : option result :=
 
 (** ** Properties of predecessors and multiple-predecessors nodes *)
 
-Definition predecessors := make_predecessors successors topnode.
+Definition predecessors := make_predecessors successors.
 
 Lemma predecessors_correct:
   forall n s,
-  Plt n topnode -> In s (successors n) -> In n predecessors!!s.
+  In s successors!!!n -> In n predecessors!!!s.
 Proof.
   intros. unfold predecessors. eapply make_predecessors_correct; eauto.
 Qed.
 
 Lemma multiple_predecessors:
   forall s n1 n2,
-  Plt n1 topnode -> In s (successors n1) ->
-  Plt n2 topnode -> In s (successors n2) ->
+  In s (successors!!!n1) ->
+  In s (successors!!!n2) ->
   n1 <> n2 ->
   basic_block_map s = true.
 Proof.
   intros. 
-  assert (In n1 predecessors!!s). apply predecessors_correct; auto.
-  assert (In n2 predecessors!!s). apply predecessors_correct; auto.
+  assert (In n1 predecessors!!!s). apply predecessors_correct; auto.
+  assert (In n2 predecessors!!!s). apply predecessors_correct; auto.
   unfold basic_block_map, is_basic_block_head.
+  destruct (peq s entrypoint). auto. 
   fold predecessors.
-  destruct (predecessors!!s). 
+  destruct (predecessors!!!s). 
   auto.
   destruct l.
-  simpl in H4. simpl in H5. intuition congruence. 
+  simpl in H2. simpl in H3. intuition congruence. 
   auto.
 Qed.
 
 Lemma no_self_loop:
   forall n,
-  Plt n topnode -> In n (successors n) -> basic_block_map n = true.
+  In n (successors!!!n) -> basic_block_map n = true.
 Proof.
   intros. unfold basic_block_map, is_basic_block_head.
+  destruct (peq n entrypoint). auto. 
   fold predecessors. 
-  generalize (predecessors_correct n n H H0). intro.
-  destruct (predecessors!!n). auto.
-  destruct l. replace n with p. apply peq_true. simpl in H1. tauto. 
+  generalize (predecessors_correct n n H). intro.
+  destruct (predecessors!!!n). auto.
+  destruct l. replace n with p. apply peq_true. simpl in H0. tauto. 
   auto.
 Qed.
 
@@ -864,9 +944,9 @@ Qed.
 Definition state_invariant (st: state) : Prop :=
   (forall n, basic_block_map n = true -> st.(st_in)!!n = L.top)
 /\
-  (forall n, Plt n topnode ->
+  (forall n,
    In n st.(st_wrk) \/
-   (forall s, In s (successors n) -> 
+   (forall s, In s (successors!!!n) -> 
                L.ge st.(st_in)!!s (transf n st.(st_in)!!n))).
 
 Lemma propagate_successors_charact1:
@@ -917,22 +997,21 @@ Qed.
 
 Lemma propagate_successors_invariant:
   forall pc res rem,
-  Plt pc topnode ->
   state_invariant (mkstate res (pc :: rem)) ->
   state_invariant 
-    (propagate_successors basic_block_map (successors pc)
+    (propagate_successors basic_block_map (successors!!!pc)
                           (transf pc res!!pc)
                           (mkstate res rem)).
 Proof.
-  intros until rem. intros PC [INV1 INV2]. simpl in INV1. simpl in INV2.
+  intros until rem. intros [INV1 INV2]. simpl in INV1. simpl in INV2.
   set (l := transf pc res!!pc).
   generalize (propagate_successors_charact1 basic_block_map
-                (successors pc) l (mkstate res rem)).
+                (successors!!! pc) l (mkstate res rem)).
   generalize (propagate_successors_charact2 basic_block_map
-                (successors pc) l (mkstate res rem)).
+                (successors!!!pc) l (mkstate res rem)).
   set (st1 := propagate_successors basic_block_map
-                 (successors pc) l (mkstate res rem)).
-  intros A B.
+                 (successors!!!pc) l (mkstate res rem)).
+  intros A B. simpl in A. 
   (* First part: BB entries remain at top *)
   split; intros.
   elim (A n); intros C D. rewrite D. simpl. apply INV1. auto. tauto. 
@@ -944,55 +1023,40 @@ Proof.
   replace (st1.(st_in)!!pc) with res!!pc. fold l. 
   caseEq (basic_block_map s); intro.
   rewrite D. simpl. rewrite INV1. apply L.top_ge. auto. tauto. 
-  elim (C H0 H1); intros. rewrite H3. apply L.refl_ge. 
+  elim (C H H0); intros. rewrite H2. apply L.refl_ge. 
   elim (A pc); intros E F. rewrite F. reflexivity. 
-  case (In_dec peq pc (successors pc)); intro.
+  case (In_dec peq pc (successors!!!pc)); intro.
   right. apply no_self_loop; auto. 
   left; auto.
   (* Case 2: n <> pc *)
-  elim (INV2 n H); intro.
+  elim (INV2 n); intro.
   (* Case 2.1: n was already in worklist, still is *)
-  left. apply B. simpl.  simpl in H0. tauto.
+  left. apply B. simpl. tauto.
   (* Case 2.2: n was not in worklist *)
-  assert (INV3: forall s, In s (successors n) -> st1.(st_in)!!s = res!!s).
+  assert (INV3: forall s, In s (successors!!!n) -> st1.(st_in)!!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
        they are basic block heads, and thus do not change! *)
     intros. elim (A s); intros C D. rewrite D. reflexivity. 
-    case (In_dec peq s (successors pc)); intro.
+    case (In_dec peq s (successors!!!pc)); intro.
     right. apply multiple_predecessors with n pc; auto.
     left; auto.
-  case (In_dec peq n (successors pc)); intro.
+  case (In_dec peq n (successors!!!pc)); intro.
   (* Case 2.2.1: n is a successor of pc. Either it is in the
      worklist or it did not change *)
   caseEq (basic_block_map n); intro.
   right; intros. 
-  elim (A n); intros C D. rewrite D. simpl. 
-  rewrite INV3; auto.
+  elim (A n); intros C D. rewrite D. rewrite INV3; auto.
   tauto.
-  left. elim (A n); intros C D. elim (C i H1); intros. auto.
+  left. elim (A n); intros C D. elim (C i H0); intros. auto.
   (* Case 2.2.2: n is not a successor of pc. It did not change. *)
   right; intros.
-  elim (A n); intros C D. rewrite D. simpl. 
+  elim (A n); intros C D. rewrite D. 
   rewrite INV3; auto.
   tauto.
 Qed.
 
-Lemma discard_top_worklist_invariant:
-  forall pc res rem,
-  ~(Plt pc topnode) ->
-  state_invariant (mkstate res (pc :: rem)) ->
-  state_invariant (mkstate res rem).
-Proof.
-  intros; red; intros.
-  elim H0; simpl; intros A B.
-  split. assumption. 
-  intros. elim (B n H1); intros.
-  left. elim H2; intro. subst n. contradiction. auto.
-  right. assumption.
-Qed.
-
 Lemma initial_state_invariant:
   state_invariant (mkstate (PMap.init L.top) (basic_block_list basic_block_map)).
 Proof.
@@ -1014,27 +1078,25 @@ Proof.
   unfold step. simpl. caseEq stwrk.
   intro. congruence.
 
-  intros pc rem WRK. case (plt pc topnode); intro.
+  intros pc rem WRK. 
   apply propagate_successors_invariant; auto. congruence. 
-  eapply discard_top_worklist_invariant; eauto. congruence.
 
   eauto. apply initial_state_invariant.
 Qed.
 
-
 (** ** Correctness of the returned solution *)
 
 Theorem fixpoint_solution:
   forall res n s,
   fixpoint = Some res ->
-  Plt n topnode -> In s (successors n) ->
+  In s (successors!!!n) ->
   L.ge res!!s (transf n res!!n).
 Proof.
   intros. 
   assert (state_invariant (mkstate res nil)).
   eapply analyze_invariant; eauto. 
-  elim H2; simpl; intros. 
-  elim (H4 n H0); intros. 
+  elim H1; simpl; intros. 
+  elim (H3 n); intros. 
   contradiction.
   auto.
 Qed.
@@ -1049,10 +1111,7 @@ Proof.
   eapply analyze_invariant; eauto. 
   elim H0; simpl; intros. 
   apply H1. unfold basic_block_map, is_basic_block_head.
-  fold predecessors. 
-  destruct (predecessors!!entrypoint). auto.
-  destruct l. destruct (peq p entrypoint). auto. apply peq_true.
-  auto.
+  fold predecessors. apply peq_true. 
 Qed. 
 
 (** ** Preservation of a property over solutions *)
@@ -1085,11 +1144,9 @@ Proof.
   apply PS.
   assert (PS2: Pstate (mkstate st.(st_in) l)).
     red; intro; simpl. apply PS.
-  case (plt p topnode); intro.
-  apply propagate_successors_P. auto. auto. 
-  auto.
+  apply propagate_successors_P. auto. auto. eauto. 
 
-  eauto. red; intro; simpl. rewrite PMap.gi. apply Ptop.
+  red; intro; simpl. rewrite PMap.gi. apply Ptop.
 Qed.
 
 End Solver.
@@ -1107,8 +1164,8 @@ End BBlock_solver.
   the enumeration [n-1], [n-2], ..., 3, 2, 1 where [n] is the
   top CFG node is a reverse postorder traversal.
   Therefore, for forward analysis, we will use an implementation
-  of [NODE_SET] where the greatest node in the working list 
-  is selected by the [pick] operation.  For backward analysis,
+  of [NODE_SET] where the [pick] operation selects the 
+  greatest node in the working list.  For backward analysis,
   we will similarly pick the smallest node in the working list. *)
 
 Require Import FSets.
@@ -1126,9 +1183,8 @@ Module NodeSetForward <: NODE_SET.
     | Some n => Some(n, PositiveSet.remove n s)
     | None => None
     end.
-  Definition initial (top: positive) :=
-    positive_rec t PositiveSet.empty PositiveSet.add top.
-
+  Definition initial (successors: PTree.t (list positive)) :=
+    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
   Definition In := PositiveSet.In.
 
   Lemma add_spec:
@@ -1159,15 +1215,20 @@ Module NodeSetForward <: NODE_SET.
   Qed.
 
   Lemma initial_spec:
-    forall numnodes n, Plt n numnodes -> In n (initial numnodes).
+    forall successors n s, 
+    successors!n = Some s -> In n (initial successors).
   Proof.
-    intros numnodes; pattern numnodes. 
-    apply positive_Peano_ind; unfold initial; intros.
-    assert (Zpos n > 0). compute; auto. red in H. omegaContradiction.
-    rewrite positive_rec_succ. rewrite PositiveSetFacts.add_iff. 
-    elim (Plt_succ_inv _ _ H0); intro.
-    right. apply H. auto.
-    left. auto.
+    intros successors.
+    apply PTree_Properties.fold_rec with
+      (P := fun succ set =>
+              forall n s, succ!n = Some s -> In n set).
+    (* extensionality *)
+    intros. rewrite <- H in H1. eauto.
+    (* base case *)
+    intros. rewrite PTree.gempty in H. congruence.
+    (* inductive case *)
+    intros. rewrite PTree.gsspec in H2. rewrite add_spec.
+    destruct (peq n k). auto. eauto.
   Qed.
 End NodeSetForward.
 
@@ -1179,9 +1240,8 @@ Module NodeSetBackward <: NODE_SET.
     | Some n => Some(n, PositiveSet.remove n s)
     | None => None
     end.
-  Definition initial (top: positive) :=
-    positive_rec t PositiveSet.empty PositiveSet.add top.
-
+  Definition initial (successors: PTree.t (list positive)) :=
+    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
   Definition In := PositiveSet.In.
 
   Lemma add_spec:
@@ -1210,7 +1270,8 @@ Module NodeSetBackward <: NODE_SET.
   Qed.
 
   Lemma initial_spec:
-    forall numnodes n, Plt n numnodes -> In n (initial numnodes).
+    forall successors n s, 
+    successors!n = Some s -> In n (initial successors).
   Proof NodeSetForward.initial_spec.
 End NodeSetBackward.
 
diff --git a/backend/LTL.v b/backend/LTL.v
index 3a61e6d..2505566 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -51,9 +51,7 @@ Record function: Type := mkfunction {
   fn_params: list loc;
   fn_stacksize: Z;
   fn_code: code;
-  fn_entrypoint: node;
-  fn_nextpc: node;
-  fn_code_wf: forall (pc: node), Plt pc fn_nextpc \/ fn_code!pc = None
+  fn_entrypoint: node
 }.
 
 Definition fundef := AST.fundef function.
@@ -256,18 +254,17 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
 (** Computation of the possible successors of an instruction.
   This is used in particular for dataflow analyses. *)
 
-Definition successors (f: function) (pc: node) : list node :=
-  match f.(fn_code)!pc with
-  | None => nil
-  | Some i =>
-      match i with
-      | Lnop s => s :: nil
-      | Lop op args res s => s :: nil
-      | Lload chunk addr args dst s => s :: nil
-      | Lstore chunk addr args src s => s :: nil
-      | Lcall sig ros args res s => s :: nil
-      | Ltailcall sig ros args => nil
-      | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
-      | Lreturn optarg => nil
-      end
+Definition successors_instr (i: instruction) : list node :=
+  match i with
+  | Lnop s => s :: nil
+  | Lop op args res s => s :: nil
+  | Lload chunk addr args dst s => s :: nil
+  | Lstore chunk addr args src s => s :: nil
+  | Lcall sig ros args res s => s :: nil
+  | Ltailcall sig ros args => nil
+  | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Lreturn optarg => nil
   end.
+
+Definition successors (f: function): PTree.t (list node) :=
+  PTree.map (fun pc i => successors_instr i) f.(fn_code).
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 866d05b..431fe17 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -95,7 +95,6 @@ Module DS := Dataflow_Solver(LBoolean)(NodeSetForward).
 Definition reachable_aux (f: LTL.function) : option (PMap.t bool) :=
   DS.fixpoint
     (successors f)
-    (f.(fn_nextpc))
     (fun pc r => r)
     ((f.(fn_entrypoint), true) :: nil).
 
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 239e2a6..b273860 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -50,6 +50,7 @@ module IntSet = Set.Make(struct type t = int let compare = compare end)
 (* Determine join points: reachable nodes that have > 1 predecessor *)
 
 let join_points f =
+  let succs = LTL.successors f in
   let reached = ref IntSet.empty in
   let reached_twice = ref IntSet.empty in
   let rec traverse pc =
@@ -59,7 +60,7 @@ let join_points f =
         reached_twice := IntSet.add npc !reached_twice
     end else begin
       reached := IntSet.add npc !reached;
-      List.iter traverse (LTL.successors f pc)
+      List.iter traverse (Kildall.successors_list succs pc)
     end
   in traverse f.fn_entrypoint; !reached_twice
 
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 1fb068d..e35fb11 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -105,20 +105,20 @@ Qed.
 (** The successors of a reachable instruction are reachable. *)
 
 Lemma reachable_successors:
-  forall f pc pc',
-  In pc' (successors f pc) ->
+  forall f pc pc' i,
+  f.(LTL.fn_code)!pc = Some i -> In pc' (successors_instr i) ->
   (reachable f)!!pc = true ->
   (reachable f)!!pc' = true.
 Proof.
   intro f. unfold reachable.
   caseEq (reachable_aux f).
   unfold reachable_aux. intro reach; intros.
-  elim (LTL.fn_code_wf f pc); intro.
   assert (LBoolean.ge reach!!pc' reach!!pc).
   change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)).
-  eapply DS.fixpoint_solution. eexact H. auto. auto.
+  eapply DS.fixpoint_solution. eexact H.
+  unfold Kildall.successors_list, successors. rewrite PTree.gmap.
+  rewrite H0; auto.
   elim H3; intro. congruence. auto.
-  unfold successors in H0. rewrite H2 in H0. contradiction.
   intros. apply PMap.gi.
 Qed.
 
@@ -514,8 +514,7 @@ Proof.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply add_branch_correct; eauto.
@@ -525,8 +524,7 @@ Proof.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply plus_left'.
@@ -541,8 +539,7 @@ Proof.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply plus_left'.
@@ -558,8 +555,7 @@ Proof.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply plus_left'.
@@ -575,8 +571,7 @@ Proof.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   assert (VALID: valid_successor f pc'). inv WTI; auto.
   exploit find_function_translated; eauto. intros [tf' [A B]].
   econstructor; split.
@@ -608,8 +603,7 @@ Proof.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!ifso = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   destruct (starts_with ifso c').
   econstructor; split.
@@ -629,8 +623,7 @@ Proof.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!ifnot = true).
-  eapply reachable_successors; eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   destruct (starts_with ifso c').
   econstructor; split.
diff --git a/backend/RTL.v b/backend/RTL.v
index 344d271..5de073e 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -87,9 +87,7 @@ Record function: Type := mkfunction {
   fn_params: list reg;
   fn_stacksize: Z;
   fn_code: code;
-  fn_entrypoint: node;
-  fn_nextpc: node;
-  fn_code_wf: forall (pc: node), Plt pc fn_nextpc \/ fn_code!pc = None
+  fn_entrypoint: node
 }.
 
 (** A function description comprises a control-flow graph (CFG) [fn_code]
@@ -332,6 +330,22 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
 (** Computation of the possible successors of an instruction.
   This is used in particular for dataflow analyses. *)
 
+Definition successors_instr (i: instruction) : list node :=
+  match i with
+  | Inop s => s :: nil
+  | Iop op args res s => s :: nil
+  | Iload chunk addr args dst s => s :: nil
+  | Istore chunk addr args src s => s :: nil
+  | Icall sig ros args res s => s :: nil
+  | Itailcall sig ros args => nil
+  | Icond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Ireturn optarg => nil
+  end.
+
+Definition successors (f: function) : PTree.t (list node) :=
+  PTree.map (fun pc i => successors_instr i) f.(fn_code).
+
+(*
 Definition successors (f: function) (pc: node) : list node :=
   match f.(fn_code)!pc with
   | None => nil
@@ -347,6 +361,7 @@ Definition successors (f: function) (pc: node) : list node :=
       | Ireturn optarg => nil
       end
   end.
+*)
 
 (** Transformation of a RTL function instruction by instruction.
   This applies a given transformation function to all instructions
@@ -356,24 +371,12 @@ Section TRANSF.
 
 Variable transf: node -> instruction -> instruction.
 
-Lemma transf_code_wf:
-  forall (c: code) (nextpc: node),
-  (forall (pc: node), Plt pc nextpc \/ c!pc = None) ->
-  (forall (pc: node), Plt pc nextpc \/ (PTree.map transf c)!pc = None).
-Proof.
-  intros. elim (H pc); intro.
-  left; assumption.
-  right. rewrite PTree.gmap. rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   mkfunction
     f.(fn_sig)
     f.(fn_params)
     f.(fn_stacksize)
     (PTree.map transf f.(fn_code))
-    f.(fn_entrypoint)
-    f.(fn_nextpc)
-    (transf_code_wf f.(fn_code) f.(fn_nextpc) f.(fn_code_wf)).
+    f.(fn_entrypoint).
 
 End TRANSF.
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 65e873e..39add98 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -630,9 +630,7 @@ Definition transl_function (f: CminorSel.function) : Errors.res RTL.function :=
                    rparams
                    f.(CminorSel.fn_stackspace)
                    s.(st_code)
-                   nentry
-                   s.(st_nextnode)
-                   s.(st_wf))
+                   nentry)
   end.
 
 Definition transl_fundef := transf_partial_fundef transl_function.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 8e61271..caf93c8 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -807,7 +807,7 @@ Inductive tr_stmt (c: code) (map: mapping):
 
 Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
   | tr_function_intro:
-      forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret nextnode wfcode,
+      forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret,
       add_vars init_mapping f.(CminorSel.fn_params) s0 = OK (rparams, map1) s1 i1 ->
       add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 i2 ->
       orret = ret_reg f.(CminorSel.fn_sig) rret ->
@@ -818,9 +818,7 @@ Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
                        rparams
                        f.(CminorSel.fn_stackspace)
                        code
-                       nentry
-                       nextnode
-                       wfcode).
+                       nentry).
 
 (** * Correctness proof of the translation functions *)
 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 83e82e1..2df9d5d 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -393,7 +393,7 @@ Qed.
 
 (** The type system for RTL is not sound in that it does not guarantee
   progress: well-typed instructions such as [Icall] can fail because
-  of run-time type tests (such as the equality between calle and caller's
+  of run-time type tests (such as the equality between callee and caller's
   signatures).  However, the type system guarantees a type preservation
   property: if the execution does not fail because of a failed run-time
   test, the result values and register states match the static
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 4b1417f..ef55a15 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -110,16 +110,6 @@ Definition tunnel_instr (uf: U.t) (b: instruction) : instruction :=
       Lreturn or
   end.
 
-Lemma wf_tunneled_code:
-  forall (f: LTL.function) (uf: U.t),
-  let tc := PTree.map (fun pc b => tunnel_instr uf b) (fn_code f) in
-  forall (pc: node), Plt pc (fn_nextpc f) \/ tc!pc = None.
-Proof.
-  intros. elim (fn_code_wf f pc); intro.
-  left; auto. right; unfold tc.
-  rewrite PTree.gmap; unfold option_map; rewrite H; auto.
-Qed.
-
 Definition tunnel_function (f: LTL.function) : LTL.function :=
   let uf := record_gotos f in
   mkfunction
@@ -127,9 +117,7 @@ Definition tunnel_function (f: LTL.function) : LTL.function :=
     (fn_params f)
     (fn_stacksize f)
     (PTree.map (fun pc b => tunnel_instr uf b) (fn_code f))
-    (U.repr uf (fn_entrypoint f))
-    (fn_nextpc f)
-    (wf_tunneled_code f uf).
+    (U.repr uf (fn_entrypoint f)).
 
 Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef :=
   transf_fundef tunnel_function f.